1 files changed, 151 insertions, 57 deletions

diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0240f29b1a..aa5ac99cfe 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -1,66 +1,165 @@
-(*Require Import Minus.*)
-
-Require Export NPlus.
-(*Require Export NDepRec.
-Require Export NTimesOrder.
-Require Export NMinus.
-Require Export NMiscFunct.*)
-
-(* First we define the functions that will be suppled as
-implementations. The parameters in module types, to which these
-functions are going to be assigned, are declared Inline,
-so in the properties functors the definitions are going to
-be unfolded and the theorems proved in these functors
-will contain these functions in their statements. *)
-
-(* Decidable equality *)
-Fixpoint e (x y : nat) {struct x} : bool :=
-match x, y with
-| 0, 0 => true
-| S x', S y' => e x' y'
-| _, _ => false
-end.
+Require Import Arith.
+Require Import NMinus.
 
-(* The boolean < function can be defined as follows using the
-standard library:
+Module NPeanoAxiomsMod <: NAxiomsSig.
 
-fun n m => proj1_sig (nat_lt_ge_bool n m)
+Definition N := nat.
+Definition E := (@eq nat).
+Definition O := 0.
+Definition S := S.
+Definition P := pred.
+Definition plus := plus.
+Definition minus := minus.
+Definition times := mult.
+Definition lt := lt.
+Definition le := le.
+Definition recursion : forall A : Set, A -> (N -> A -> A) -> N -> A :=
+  fun A : Set => nat_rec (fun _ => A).
+Implicit Arguments recursion [A].
 
-However, this definition seems too complex. First, there are many
-functions involved: nat_lt_ge_bool is defined (in Coq.Arith.Bool_nat)
-using bool_of_sumbool and
+Theorem E_equiv : equiv nat E.
+Proof (eq_equiv nat).
 
-lt_ge_dec : forall x y : nat, {x < y} + {x >= y},
+Add Relation nat E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
 
-where the latter function is defined using sumbool_not and
+(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat E"
+then the theorem generated for succ_wd below is forall x, succ x = succ x,
+which does not match the axioms in NAxiomsSig *)
 
-le_lt_dec : forall n m : nat, {n <= m} + {m < n}.
+Add Morphism S with signature E ==> E as succ_wd.
+Proof.
+congruence.
+Qed.
 
-Second, this definition is not the most efficient, especially since
-le_lt_dec is proved using tactics, not by giving the explicit proof
-term. *)
+Add Morphism P with signature E ==> E as pred_wd.
+Proof.
+congruence.
+Qed.
 
-Fixpoint lt (n m : nat) {struct n} : bool :=
-match n, m with
-| _, 0 => false
-| 0, S _ => true
-| S n', S m' => lt n' m'
-end.
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+congruence.
+Qed.
 
-Fixpoint le (n m : nat) {struct n} : bool :=
-match n, m with
-| 0, _ => true
-| S n', S m' => le n' m'
-| S _, 0 => false
-end.
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Proof.
+congruence.
+Qed.
 
-Delimit Scope NatScope with Nat.
-Open Scope NatScope.
+Add Morphism times with signature E ==> E ==> E as times_wd.
+Proof.
+congruence.
+Qed.
 
-Module NPeanoBaseMod <: NBaseSig.
+Add Morphism lt with signature E ==> E ==> iff as lt_wd.
+Proof.
+unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
 
-Theorem E_equiv : equiv nat (@eq nat).
-Proof (eq_equiv nat).
+Add Morphism le with signature E ==> E ==> iff as le_wd.
+Proof.
+unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
+
+Theorem induction :
+  forall A : nat -> Prop, predicate_wd (@eq nat) A ->
+    A 0 -> (forall n : nat, A n -> A (S n)) -> forall n : nat, A n.
+Proof.
+intros; now apply nat_ind.
+Qed.
+
+Theorem pred_0 : pred 0 = 0.
+Proof.
+reflexivity.
+Qed.
+
+Theorem pred_succ : forall n : nat, pred (S n) = n.
+Proof.
+reflexivity.
+Qed.
+
+Theorem plus_0_l : forall n : nat, 0 + n = n.
+Proof.
+reflexivity.
+Qed.
+
+Theorem plus_succ_l : forall n m : nat, (S n) + m = S (n + m).
+Proof.
+reflexivity.
+Qed.
+
+Theorem minus_0_r : forall n : nat, n - 0 = n.
+Proof.
+intro n; now destruct n.
+Qed.
+
+Theorem minus_succ_r : forall n m : nat, n - (S m) = pred (n - m).
+Proof.
+intros n m; induction n m using nat_double_ind; simpl; auto. apply minus_0_r.
+Qed.
+
+Theorem times_0_r : forall n : nat, n * 0 = 0.
+Proof.
+exact mult_0_r.
+Qed.
+
+Theorem times_succ_r : forall n m : nat, n * (S m) = n * m + n.
+Proof.
+intros n m; symmetry; apply mult_n_Sm.
+Qed.
+
+Theorem le_lt_or_eq : forall n m : nat, n <= m <-> n < m \/ n = m.
+Proof.
+intros n m; split.
+apply le_lt_or_eq.
+intro H; destruct H as [H | H].
+now apply lt_le_weak. rewrite H; apply le_refl.
+Qed.
+
+Theorem nlt_0_r : forall n : nat, ~ (n < 0).
+Proof.
+exact lt_n_O.
+Qed.
+
+Theorem lt_succ_le : forall n m : nat, n < S m <-> n <= m.
+Proof.
+intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm].
+Qed.
+
+Theorem recursion_wd : forall (A : Set) (EA : relation A),
+  forall a a' : A, EA a a' ->
+    forall f f' : N -> A -> A, eq_fun2 (@eq nat) EA EA f f' ->
+      forall n n' : N, n = n' ->
+        EA (recursion a f n) (recursion a' f' n').
+Proof.
+unfold eq_fun2; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
+Qed.
+
+Theorem recursion_0 :
+  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
+Proof.
+reflexivity.
+Qed.
+
+Theorem recursion_succ :
+  forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd (@eq nat) EA EA f ->
+      forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)).
+Proof.
+unfold eq_fun2; induction n; simpl; auto.
+Qed.
+
+End NPeanoAxiomsMod.
+
+(* Now we apply the largest property functor *)
+
+Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod.
+
+(*
 
 Theorem succ_wd : fun_wd (@eq nat) (@eq nat) S.
 Proof.
@@ -77,12 +176,6 @@ Proof.
 intros n H; simplify_eq H.
 Qed.
 
-Theorem induction :
-  forall A : nat -> Prop, predicate_wd (@eq nat) A ->
-    A 0 -> (forall n : nat, A n -> A (S n)) -> forall n : nat, A n.
-Proof.
-intros; now apply nat_ind.
-Qed.
 
 Definition N := nat.
 Definition E := (@eq nat).
@@ -318,6 +411,7 @@ Qed.
 Add Ring SR : semi_ring (decidable e_implies_E).
 
 Goal forall x y : nat, x + y = y + x. intros. ring.*)
+*)
 
 
 (*