Added the following theorems to BinPos:

Pplus_xO
Pmult_Sn_m
Pcompare_eq_Lt (a generalization of Pcompare_Gt_Lt)
Pcompare_eq_Gt (a generalization of Pcompare_Lt_Gt)
Pcompare_refl_id (a generalization of Pcompare_refl)
Pcompare_Lt_eq_Lt (a generalization of Pcompare_Lt_Lt)
Pcompare_Gt_eq_Gt (a generalization of Pcompare_Gt_Gt)
Pcompare_p_Sp
Pcompare_p_Sq (one of the defining axioms of < )
Pcompare_1 (1 is the least positive number)

Added the following theorems to BinNat:
Nrect (defined in terms of new Prect)
Nrect_base
Nrect_step (the analogout statement in BinPos is called Prect_succ)
Nrec_base
Nrec_step
Nmult_Sn_m
Nsucc_0
Ncompare_0 (0 is the least natural number)
Ncompare_n_Sm (one of the defining axioms of < )

Also, defined Nind and Nrec in terms of Nrect.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9738 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 180 insertions, 18 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index f79d09b51d..0f2782bd96 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -123,15 +123,39 @@ Qed.
 
 (** Peano induction on binary natural numbers *)
 
-Theorem Nind :
- forall P:N -> Prop,
-   P N0 -> (forall n:N, P n -> P (Nsucc n)) -> forall n:N, P n.
-Proof.
-destruct n.
-  assumption.
-  apply Pind with (P := fun p => P (Npos p)).
-exact (H0 N0 H).
-intro p'; exact (H0 (Npos p')).
+Definition Nrect
+  (P : N -> Type) (a : P N0)
+    (f : forall n : N, P n -> P (Nsucc n)) (n : N) : P n :=
+let f' (p : positive) (x : P (Npos p)) := f (Npos p) x in
+let P' (p : positive) := P (Npos p) in
+match n return (P n) with
+| N0 => a
+| Npos p => Prect P' (f N0 a) f' p
+end.
+
+Theorem Nrect_base : forall P a f, Nrect P a f N0 = a.
+Proof.
+intros P a f; simpl; reflexivity.
+Qed.
+
+Theorem Nrect_step : forall P a f n, Nrect P a f (Nsucc n) = f n (Nrect P a f n).
+Proof.
+intros P a f; destruct n as [| p]; simpl;
+[rewrite Prect_base | rewrite Prect_succ]; reflexivity.
+Qed.
+
+Definition Nind (P : N -> Prop) := Nrect P.
+
+Definition Nrec (P : N -> Set) := Nrect P.
+
+Theorem Nrec_base : forall P a f, Nrec P a f N0 = a.
+Proof.
+intros P a f; unfold Nrec; apply Nrect_base.
+Qed.
+
+Theorem Nrec_step : forall P a f n, Nrec P a f (Nsucc n) = f n (Nrec P a f n).
+Proof.
+intros P a f; unfold Nrec; apply Nrect_step.
 Qed.
 
 (** Properties of addition *)
@@ -171,6 +195,11 @@ destruct n; destruct m.
   simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity.
 Qed.
 
+Theorem Nsucc_0 : forall n : N, Nsucc n <> N0.
+Proof.
+intro n; elim n; simpl Nsucc; intros; discriminate.
+Qed.
+
 Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m.
 Proof.
 destruct n; destruct m; simpl in |- *; intro H; reflexivity || injection H;
@@ -190,11 +219,22 @@ Qed.
 
 (** Properties of multiplication *)
 
+Theorem Nmult_0_l : forall n:N, N0 * n = N0.
+Proof.
+reflexivity.
+Qed.
+
 Theorem Nmult_1_l : forall n:N, Npos 1 * n = n.
 Proof.
 destruct n; reflexivity.
 Qed.
 
+Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m.
+Proof.
+destruct n as [| n]; destruct m as [| m]; simpl; auto.
+rewrite Pmult_Sn_m; reflexivity.
+Qed.
+
 Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n.
 Proof.
 destruct n; simpl in |- *; try reflexivity.
@@ -233,11 +273,6 @@ destruct n; destruct m; reflexivity || (try discriminate H).
 injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity.
 Qed. 
 
-Theorem Nmult_0_l : forall n:N, N0 * n = N0.
-Proof.
-reflexivity.
-Qed.
-
 (** Properties of comparison *)
 
 Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m.
@@ -259,6 +294,25 @@ destruct n; destruct m; simpl; auto.
 exact (Pcompare_antisym p p0 Eq).
 Qed.
 
+(** 0 is the least natural number *)
+
+Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
+Proof.
+destruct n; discriminate.
+Qed.
+
+Theorem Ncompare_n_Sm :
+  forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m.
+Proof.
+intros n m; split; destruct n as [| p]; destruct m as [| q]; simpl; auto.
+destruct p; simpl; intros; discriminate.
+pose proof (proj1 (Pcompare_p_Sq p q));
+assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
+intros H; destruct H; discriminate.
+pose proof (proj2 (Pcompare_p_Sq p q));
+assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
+Qed.
+
 (** Dividing by 2 *)
 
 Definition Ndiv2 (n:N) :=
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index dc6156d6a7..0adc07faa0 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -472,6 +472,11 @@ Qed.
 
 (** Commutation of addition with the double of a positive number *)
 
+Lemma Pplus_xO : forall m n : positive, xO (m + n) = xO m + xO n.
+Proof.
+destruct n; destruct m; simpl; auto.
+Qed.
+
 Lemma Pplus_xI_double_minus_one :
  forall p q:positive, xO (p + q) = xI p + Pdouble_minus_one q.
 Proof.
@@ -611,6 +616,17 @@ intro x; induction x; simpl in |- *.
   reflexivity.
 Qed.
 
+(** Successor and multiplication *)
+
+Lemma Pmult_Sn_m : forall n m : positive, (Psucc n) * m = m + n * m.
+Proof.
+induction n as [n IH | n IH |]; simpl; intro m.
+rewrite IH; rewrite Pplus_assoc; rewrite Pplus_diag;
+rewrite <- Pplus_xO; reflexivity.
+reflexivity.
+symmetry; apply Pplus_diag.
+Qed.
+
 (** Right reduction properties for multiplication *)
 
 Lemma Pmult_xO_permute_r : forall p q:positive, p * xO q = xO (p * q).
@@ -726,6 +742,16 @@ Qed.
 (**********************************************************************)
 (** Properties of comparison on binary positive numbers *)
 
+Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq.
+intro x; induction  x as [x Hrecx| x Hrecx| ]; auto.
+Qed.
+
+(* A generalization of Pcompare_refl *)
+
+Theorem Pcompare_refl_id : forall (p : positive) (r : comparison), (p ?= p) r = r.
+induction p; auto.
+Qed.
+
 Theorem Pcompare_not_Eq :
  forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq.
 Proof.
@@ -759,6 +785,14 @@ intro x; induction  x as [x Hrecx| x Hrecx| ]; intro y;
  auto; discriminate || intros H; discriminate H.
 Qed.
 
+Lemma Pcompare_eq_Lt :
+ forall p q : positive, (p ?= q) Eq = Lt <-> (p ?= q) Gt = Lt.
+Proof.
+intros p q; split; [| apply Pcompare_Gt_Lt].
+generalize q; clear q; induction p; induction q; simpl; auto.
+intro; discriminate.
+Qed.
+
 Lemma Pcompare_Lt_Gt :
  forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt.
 Proof.
@@ -769,6 +803,14 @@ intro x; induction  x as [x Hrecx| x Hrecx| ]; intro y;
  auto; discriminate || intros H; discriminate H.
 Qed.
 
+Lemma Pcompare_eq_Gt :
+  forall p q : positive, (p ?= q) Eq = Gt <-> (p ?= q) Lt = Gt.
+Proof.
+intros p q; split; [| apply Pcompare_Lt_Gt].
+generalize q; clear q; induction p; induction q; simpl; auto.
+intro; discriminate.
+Qed.
+
 Lemma Pcompare_Lt_Lt :
  forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q.
 Proof.
@@ -777,6 +819,16 @@ intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
  auto; intros E; rewrite E; auto.
 Qed.
 
+Lemma Pcompare_Lt_eq_Lt :
+ forall p q:positive, (p ?= q) Lt = Lt <-> (p ?= q) Eq = Lt \/ p = q.
+Proof.
+intros p q; split; [apply Pcompare_Lt_Lt |].
+intro H; destruct H as [H | H]; [ | rewrite H; apply Pcompare_refl_id].
+generalize q H. clear q H.
+induction p as [p' IH | p' IH |]; destruct q as [q' | q' |]; simpl; intro H;
+try (reflexivity || assumption || discriminate H); apply IH; assumption.
+Qed.
+
 Lemma Pcompare_Gt_Gt :
  forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q.
 Proof.
@@ -785,6 +837,16 @@ intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
  auto; intros E; rewrite E; auto.
 Qed.
 
+Lemma Pcompare_Gt_eq_Gt :
+ forall p q:positive, (p ?= q) Gt = Gt <-> (p ?= q) Eq = Gt \/ p = q.
+Proof.
+intros p q; split; [apply Pcompare_Gt_Gt |].
+intro H; destruct H as [H | H]; [ | rewrite H; apply Pcompare_refl_id].
+generalize q H. clear q H.
+induction p as [p' IH | p' IH |]; destruct q as [q' | q' |]; simpl; intro H;
+try (reflexivity || assumption || discriminate H); apply IH; assumption.
+Qed.
+
 Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt.
 Proof.
 simple induction r; auto. 
@@ -795,10 +857,6 @@ Ltac ElimPcompare c1 c2 :=
    [ idtac | let x := fresh "H" in
              (intro x; case x; clear x) ].
 
-Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq.
-intro x; induction  x as [x Hrecx| x Hrecx| ]; auto.
-Qed.
-
 Lemma Pcompare_antisym :
  forall (p q:positive) (r:comparison),
    CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r).
@@ -836,6 +894,56 @@ intros; change Eq at 1 with (CompOpp Eq) in |- *.
 symmetry  in |- *; apply Pcompare_antisym.
 Qed.
 
+(** Comparison and the successor *)
+
+Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.
+Proof.
+induction p as [p' IH | p' IH |]; simpl in *;
+[apply -> Pcompare_eq_Lt; assumption | apply Pcompare_refl_id | reflexivity].
+Qed.
+
+Theorem Pcompare_p_Sq : forall p q : positive,
+  (p ?= Psucc q) Eq = Lt <-> (p ?= q) Eq = Lt \/ p = q.
+Proof.
+intros p q; split.
+generalize p q; clear p q.
+induction p as [p' IH | p' IH |]; destruct q as [q' | q' |]; simpl; intro H.
+assert (T : xI p' = xI q' <-> p' = q').
+split; intro HH; [inversion HH; trivial | rewrite HH; reflexivity].
+cut ((p' ?= q') Eq = Lt \/ p' = q'). firstorder.
+apply IH. apply Pcompare_Gt_Lt; assumption.
+left; apply -> Pcompare_eq_Lt; assumption.
+destruct p'; discriminate.
+apply IH in H. left.
+destruct H as [H | H]; [apply <- Pcompare_Lt_eq_Lt; left; assumption |
+rewrite H; apply Pcompare_refl_id].
+assert (T : xO p' = xO q' <-> p' = q').
+split; intro HH; [inversion HH; trivial | rewrite HH; reflexivity].
+cut ((p' ?= q') Eq = Lt \/ p' = q'); [firstorder | ].
+apply -> Pcompare_Lt_eq_Lt; assumption.
+destruct p'; discriminate.
+left; reflexivity.
+left; reflexivity.
+right; reflexivity.
+intro H; destruct H as [H | H].
+generalize q H; clear q H. induction p as [p' IH | p' IH |];
+destruct q as [q' | q' |]; simpl in *; intro H;
+try (reflexivity || discriminate H).
+apply -> Pcompare_eq_Lt; apply IH; assumption.
+apply <- Pcompare_eq_Lt; assumption.
+assert (H1 : (p' ?= q') Eq = Lt \/ p' = q'); [apply -> Pcompare_Lt_eq_Lt; assumption |].
+destruct H1 as [H1 | H1]; [apply IH; assumption | rewrite H1; apply Pcompare_p_Sp].
+apply <- Pcompare_Lt_eq_Lt; left; assumption.
+rewrite H; apply Pcompare_p_Sp.
+Qed.
+
+(** 1 is the least positive number *)
+
+Lemma Pcompare_1 : forall p, ~ (p ?= xH) Eq = Lt.
+Proof.
+destruct p; discriminate.
+Qed.
+
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)