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.