Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)

This way, no more references to NBinDefs.N when doing "Print N".
Long-term migration to theories/Numbers is still planned, but it needs
more works, for instance to adapt both positive and N and Z at once.



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

1 files changed, 25 insertions, 166 deletions

diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index 66402f761..3110da36a 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -11,166 +11,25 @@
 (*i i*)
 
 Require Import BinPos.
+Require Export BinNat.
 Require Import NMinus.
 
-(** Definitions *)
+Open Local Scope N_scope.
 
-Inductive N : Set :=
-| N0 : N
-| Npos : positive -> N.
-
-Definition succ n :=
-match n with
-| N0 => Npos 1
-| Npos p => Npos (Psucc p)
-end.
-
-Definition pred (n : N) :=
-match n with
-| N0 => N0
-| Npos p =>
-  match p with
-  | xH => N0
-  | _ => Npos (Ppred p)
-  end
-end.
-
-Definition plus n m :=
-match n, m with
-| N0, _ => m
-| _, N0 => n
-| Npos p, Npos q => Npos (p + q)
-end.
-
-Definition minus (n m : N) :=
-match n, m with
-| N0, _ => N0
-| n, N0 => n
-| Npos n', Npos m' =>
-  match Pminus_mask n' m' with
-  | IsPos p => Npos p
-  | _ => N0
-  end
-end.
-
-Definition times n m :=
-match n, m with
-| N0, _ => N0
-| _, N0 => N0
-| Npos p, Npos q => Npos (p * q)
-end.
-
-Definition Ncompare n m :=
-match n, m with
-| N0, N0 => Eq
-| N0, Npos m' => Lt
-| Npos n', N0 => Gt
-| Npos n', Npos m' => (n' ?= m')%positive Eq
-end.
-
-Definition lt (x y : N) := (Ncompare x y) = Lt.
-Definition le (x y : N) := (Ncompare x y) <> Gt.
-
-Definition min (n m : N) :=
-match Ncompare n m with
-| Lt | Eq => n
-| Gt => m
-end.
-
-Definition max (n m : N) :=
-match Ncompare n m with
-| Lt | Eq => m
-| Gt => n
-end.
-
-Delimit Scope NatScope with Nat.
-Bind Scope NatScope with N.
-
-Notation "0" := N0 : NatScope.
-Notation "1" := (Npos xH) : NatScope.
-Infix "+" := plus : NatScope.
-Infix "-" := minus : NatScope.
-Infix "*" := times : NatScope.
-Infix "?=" := Ncompare (at level 70, no associativity) : NatScope.
-Infix "<" := lt : NatScope.
-Infix "<=" := le : NatScope.
-
-Open Local Scope NatScope.
-
-(** Peano induction on binary natural numbers *)
-
-Definition Nrect
-  (P : N -> Type) (a : P N0)
-    (f : forall n : N, P n -> P (succ 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.
-reflexivity.
-Qed.
-
-Theorem Nrect_step : forall P a f n, Nrect P a f (succ 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.*)
-
-(** Results about the order *)
-
-Theorem Ncompare_eq_correct : forall n m : N, (n ?= m) = Eq <-> n = m.
-Proof.
-destruct n as [| n]; destruct m as [| m]; simpl;
-split; intro H; try reflexivity; try discriminate H.
-apply Pcompare_Eq_eq in H; now rewrite H.
-injection H; intro H1; rewrite H1; apply Pcompare_refl.
-Qed.
-
-Theorem Ncompare_diag : forall n : N, n ?= n = Eq.
-Proof.
-intro n; now apply <- Ncompare_eq_correct.
-Qed.
-
-Theorem Ncompare_antisymm :
-  forall (n m : N) (c : comparison), n ?= m = c -> m ?= n = CompOpp c.
-Proof.
-destruct n; destruct m; destruct c; simpl; intro H; try discriminate H; try reflexivity;
-replace Eq with (CompOpp Eq) by reflexivity; rewrite <- Pcompare_antisym;
-now rewrite H.
-Qed.
-
-(** Implementation of NAxiomsSig module type *)
+(** Implementation of [NAxiomsSig] module type via [BinNat.N] *)
 
 Module NBinaryAxiomsMod <: NAxiomsSig.
 Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
 Module Export NZAxiomsMod <: NZAxiomsSig.
 
 Definition NZ := N.
-Definition NZeq := (@eq N).
+Definition NZeq := @eq N.
 Definition NZ0 := N0.
-Definition NZsucc := succ.
-Definition NZpred := pred.
-Definition NZplus := plus.
-Definition NZminus := minus.
-Definition NZtimes := times.
+Definition NZsucc := Nsucc.
+Definition NZpred := Npred.
+Definition NZplus := Nplus.
+Definition NZminus := Nminus.
+Definition NZtimes := Nmult.
 
 Theorem NZeq_equiv : equiv N NZeq.
 Proof (eq_equiv N).
@@ -229,7 +88,7 @@ Theorem NZplus_succ_l : forall n m : NZ, (NZsucc n) + m = NZsucc (n + m).
 Proof.
 destruct n; destruct m.
 simpl in |- *; reflexivity.
-unfold NZsucc, NZplus, succ, plus. rewrite <- Pplus_one_succ_l; reflexivity.
+unfold NZsucc, NZplus, Nsucc, Nplus. rewrite <- Pplus_one_succ_l; reflexivity.
 simpl in |- *; reflexivity.
 simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity.
 Qed.
@@ -260,10 +119,10 @@ Qed.
 
 End NZAxiomsMod.
 
-Definition NZlt := lt.
-Definition NZle := le.
-Definition NZmin := min.
-Definition NZmax := max.
+Definition NZlt := Nlt.
+Definition NZle := Nle.
+Definition NZmin := Nmin.
+Definition NZmax := Nmax.
 
 Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
 Proof.
@@ -287,19 +146,19 @@ Qed.
 
 Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m.
 Proof.
-intros n m. unfold le, lt. rewrite <- Ncompare_eq_correct.
+intros n m. unfold Nle, Nlt. rewrite <- Ncompare_eq_correct.
 destruct (n ?= m); split; intro H1; (try discriminate); try (now left); try now right.
 now elim H1. destruct H1; discriminate.
 Qed.
 
 Theorem NZlt_irrefl : forall n : NZ, ~ n < n.
 Proof.
-intro n; unfold lt; now rewrite Ncompare_diag.
+intro n; unfold Nlt; now rewrite Ncompare_refl.
 Qed.
 
 Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc m) <-> n <= m.
 Proof.
-intros n m; unfold lt, le; destruct n as [| p]; destruct m as [| q]; simpl;
+intros n m; unfold Nlt, Nle; destruct n as [| p]; destruct m as [| q]; simpl;
 split; intro H; try reflexivity; try discriminate.
 destruct p; simpl; intros; discriminate. elimtype False; now apply H.
 apply -> Pcompare_p_Sq in H. destruct H as [H | H].
@@ -310,29 +169,29 @@ Qed.
 
 Theorem NZmin_l : forall n m : N, n <= m -> NZmin n m = n.
 Proof.
-unfold NZmin, min, le; intros n m H.
+unfold NZmin, Nmin, Nle; intros n m H.
 destruct (n ?= m); try reflexivity. now elim H.
 Qed.
 
 Theorem NZmin_r : forall n m : N, m <= n -> NZmin n m = m.
 Proof.
-unfold NZmin, min, le; intros n m H.
+unfold NZmin, Nmin, Nle; intros n m H.
 case_eq (n ?= m); intro H1; try reflexivity.
 now apply -> Ncompare_eq_correct.
-apply Ncompare_antisymm in H1. now elim H.
+rewrite <- Ncompare_antisym, H1 in H; elim H; auto.
 Qed.
 
 Theorem NZmax_l : forall n m : N, m <= n -> NZmax n m = n.
 Proof.
-unfold NZmax, max, le; intros n m H.
+unfold NZmax, Nmax, Nle; intros n m H.
 case_eq (n ?= m); intro H1; try reflexivity.
 symmetry; now apply -> Ncompare_eq_correct.
-apply Ncompare_antisymm in H1. now elim H.
+rewrite <- Ncompare_antisym, H1 in H; elim H; auto.
 Qed.
 
 Theorem NZmax_r : forall n m : N, n <= m -> NZmax n m = m.
 Proof.
-unfold NZmax, max, le; intros n m H.
+unfold NZmax, Nmax, Nle; intros n m H.
 destruct (n ?= m); try reflexivity. now elim H.
 Qed.
 
@@ -342,7 +201,7 @@ Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) :=
   Nrect (fun _ => A) a f n.
 Implicit Arguments recursion [A].
 
-Theorem pred_0 : pred N0 = N0.
+Theorem pred_0 : Npred N0 = N0.
 Proof.
 reflexivity.
 Qed.
@@ -373,7 +232,7 @@ Qed.
 Theorem recursion_succ :
   forall (A : Set) (Aeq : relation A) (a : A) (f : N -> A -> A),
     Aeq a a -> fun2_wd NZeq Aeq Aeq f ->
-      forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)).
+      forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)).
 Proof.
 unfold NZeq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect.
 rewrite Nrect_step; rewrite Nrect_base; now apply f_wd.