Library Coq.Numbers.Natural.Abstract.NBase
Require Export Decidable.
Require Export NAxioms.
Require Import NZMulOrder.
Module NBasePropFunct (
Import NAxiomsMod :
NAxiomsSig).
Open Local Scope NatScope.
Module Export NZMulOrderMod :=
NZMulOrderPropFunct NZOrdAxiomsMod.
Theorem succ_wd :
forall n1 n2 :
N,
n1 ==
n2 ->
S n1 ==
S n2.
Theorem pred_wd :
forall n1 n2 :
N,
n1 ==
n2 ->
P n1 ==
P n2.
Theorem pred_succ :
forall n :
N,
P (
S n) ==
n.
Theorem pred_0 :
P 0 == 0.
Theorem Neq_refl :
forall n :
N,
n ==
n.
Theorem Neq_sym :
forall n m :
N,
n ==
m ->
m ==
n.
Theorem Neq_trans :
forall n m p :
N,
n ==
m ->
m ==
p ->
n ==
p.
Theorem neq_sym :
forall n m :
N,
n ~=
m ->
m ~=
n.
Theorem succ_inj :
forall n1 n2 :
N,
S n1 ==
S n2 ->
n1 ==
n2.
Theorem succ_inj_wd :
forall n1 n2 :
N,
S n1 ==
S n2 <->
n1 ==
n2.
Theorem succ_inj_wd_neg :
forall n m :
N,
S n ~=
S m <->
n ~=
m.
Theorem eq_dec :
forall n m :
N,
decidable (
n ==
m).
Theorem eq_dne :
forall n m :
N, ~ ~
n ==
m <->
n ==
m.
Definition if_zero (
A :
Set) (
a b :
A) (
n :
N) :
A :=
recursion a (
fun _ _ =>
b)
n.
Add Parametric Morphism (
A :
Set) : (
if_zero A)
with signature (@
eq _ ==> @
eq _ ==>
Neq ==> @
eq _)
as if_zero_wd.
Theorem if_zero_0 :
forall (
A :
Set) (
a b :
A),
if_zero A a b 0 =
a.
Theorem if_zero_succ :
forall (
A :
Set) (
a b :
A) (
n :
N),
if_zero A a b (
S n) =
b.
Implicit Arguments if_zero [
A].
Theorem neq_succ_0 :
forall n :
N,
S n ~= 0.
Theorem neq_0_succ :
forall n :
N, 0 ~=
S n.
Theorem le_0_l :
forall n :
N, 0 <=
n.
Theorem induction :
forall A :
N ->
Prop,
predicate_wd Neq A ->
A 0 -> (
forall n :
N,
A n ->
A (
S n)) ->
forall n :
N,
A n.
Ltac induct n :=
induction_maker n ltac:(apply
induction).
Theorem case_analysis :
forall A :
N ->
Prop,
predicate_wd Neq A ->
A 0 -> (
forall n :
N,
A (
S n)) ->
forall n :
N,
A n.
Ltac cases n :=
induction_maker n ltac:(apply
case_analysis).
Theorem neq_0 : ~
forall n,
n == 0.
Theorem neq_0_r :
forall n,
n ~= 0 <->
exists m,
n ==
S m.
Theorem zero_or_succ :
forall n,
n == 0 \/
exists m,
n ==
S m.
Theorem eq_pred_0 :
forall n :
N,
P n == 0 <->
n == 0 \/
n == 1.
Theorem succ_pred :
forall n :
N,
n ~= 0 ->
S (
P n) ==
n.
Theorem pred_inj :
forall n m :
N,
n ~= 0 ->
m ~= 0 ->
P n ==
P m ->
n ==
m.
Section PairInduction.
Variable A :
N ->
Prop.
Hypothesis A_wd :
predicate_wd Neq A.
Add Morphism A with signature Neq ==>
iff as A_morph.
Theorem pair_induction :
A 0 ->
A 1 ->
(
forall n,
A n ->
A (
S n) ->
A (
S (
S n))) ->
forall n,
A n.
End PairInduction.
Section TwoDimensionalInduction.
Variable R :
N ->
N ->
Prop.
Hypothesis R_wd :
relation_wd Neq Neq R.
Add Morphism R with signature Neq ==>
Neq ==>
iff as R_morph.
Theorem two_dim_induction :
R 0 0 ->
(
forall n m,
R n m ->
R n (
S m)) ->
(
forall n, (
forall m,
R n m) ->
R (
S n) 0) ->
forall n m,
R n m.
End TwoDimensionalInduction.
Section DoubleInduction.
Variable R :
N ->
N ->
Prop.
Hypothesis R_wd :
relation_wd Neq Neq R.
Add Morphism R with signature Neq ==>
Neq ==>
iff as R_morph1.
Theorem double_induction :
(
forall m :
N,
R 0
m) ->
(
forall n :
N,
R (
S n) 0) ->
(
forall n m :
N,
R n m ->
R (
S n) (
S m)) ->
forall n m :
N,
R n m.
End DoubleInduction.
Ltac double_induct n m :=
try intros until n;
try intros until m;
pattern n,
m;
apply double_induction;
clear n m;
[
solve_relation_wd | | | ].
End NBasePropFunct.