Modularisation of Znat, a few name changed elsewhere

 For instance inj_plus is now Nat2Z.inj_add

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

1 files changed, 28 insertions, 18 deletions

diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index ccf1e9dc6..133d4c23b 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -15,20 +15,25 @@ Module N2Nat.
 
 (** [N.to_nat] is a bijection between [N] and [nat],
     with [Pos.of_nat] as reciprocal.
-    See [Nat2N.bij] below for the dual equation. *)
+    See [Nat2N.id] below for the dual equation. *)
 
-Lemma bij a : N.of_nat (N.to_nat a) = a.
+Lemma id a : N.of_nat (N.to_nat a) = a.
 Proof.
  destruct a as [| p]; simpl; trivial.
  destruct (Pos2Nat.is_succ p) as (n,H). rewrite H. simpl. f_equal.
- apply Pos2Nat.inj. rewrite H. apply SuccNat2Pos.bij.
+ apply Pos2Nat.inj. rewrite H. apply SuccNat2Pos.id_succ.
 Qed.
 
 (** [N.to_nat] is hence injective *)
 
 Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'.
 Proof.
- intro H. rewrite <- (bij a), <- (bij a'). now f_equal.
+ intro H. rewrite <- (id a), <- (id a'). now f_equal.
+Qed.
+
+Lemma inj_iff a a' : N.to_nat a = N.to_nat a' <-> a = a'.
+Proof.
+ split. apply inj. intros; now subst.
 Qed.
 
 (** Interaction of this translation and usual operations. *)
@@ -85,7 +90,7 @@ Proof.
 Qed.
 
 Lemma inj_compare a a' :
- N.compare a a' = nat_compare (N.to_nat a) (N.to_nat a').
+ (a ?= a')%N = nat_compare (N.to_nat a) (N.to_nat a').
 Proof.
  destruct a, a'; simpl; trivial.
  now destruct (Pos2Nat.is_succ p) as (n,->).
@@ -118,7 +123,7 @@ End N2Nat.
 Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double
  N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub
  N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min
- N2Nat.bij
+ N2Nat.id
  : Nnat.
 
 
@@ -126,23 +131,28 @@ Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double
 
 Module Nat2N.
 
-(** [N.of_nat] is a bijection between [nat] and [N],
+(** [N.of_nat] is an bijection between [nat] and [N],
     with [Pos.to_nat] as reciprocal.
-    See [N2Nat.bij] above for the dual equation. *)
+    See [N2Nat.id] above for the dual equation. *)
 
-Lemma bij n : N.to_nat (N.of_nat n) = n.
+Lemma id n : N.to_nat (N.of_nat n) = n.
 Proof.
- induction n; simpl; trivial. apply SuccNat2Pos.bij.
+ induction n; simpl; trivial. apply SuccNat2Pos.id_succ.
 Qed.
 
-Hint Rewrite bij : Nnat.
+Hint Rewrite id : Nnat.
 Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat.
 
 (** [N.of_nat] is hence injective *)
 
 Lemma inj n n' : N.of_nat n = N.of_nat n' -> n = n'.
 Proof.
- intros H. rewrite <- (bij n), <- (bij n'). now f_equal.
+ intros H. rewrite <- (id n), <- (id n'). now f_equal.
+Qed.
+
+Lemma inj_iff n n' : N.of_nat n = N.of_nat n' <-> n = n'.
+Proof.
+ split. apply inj. intros; now subst.
 Qed.
 
 (** Interaction of this translation and usual operations. *)
@@ -172,8 +182,8 @@ Lemma inj_div2 n : N.of_nat (div2 n) = N.div2 (N.of_nat n).
 Proof. nat2N. Qed.
 
 Lemma inj_compare n n' :
-  nat_compare n n' = N.compare (N.of_nat n) (N.of_nat n').
-Proof. now rewrite N2Nat.inj_compare, !bij. Qed.
+  nat_compare n n' = (N.of_nat n ?= N.of_nat n')%N.
+Proof. now rewrite N2Nat.inj_compare, !id. Qed.
 
 Lemma inj_min n n' :
   N.of_nat (min n n') = N.min (N.of_nat n) (N.of_nat n').
@@ -185,16 +195,16 @@ Proof. nat2N. Qed.
 
 Lemma inj_iter n {A} (f:A->A) (x:A) :
   nat_iter n f x = N.iter (N.of_nat n) f x.
-Proof. now rewrite N2Nat.inj_iter, !bij. Qed.
+Proof. now rewrite N2Nat.inj_iter, !id. Qed.
 
 End Nat2N.
 
-Hint Rewrite Nat2N.bij : Nnat.
+Hint Rewrite Nat2N.id : Nnat.
 
 (** Compatibility notations *)
 
 Notation nat_of_N_inj := N2Nat.inj (only parsing).
-Notation N_of_nat_of_N := N2Nat.bij (only parsing).
+Notation N_of_nat_of_N := N2Nat.id (only parsing).
 Notation nat_of_Ndouble := N2Nat.inj_double (only parsing).
 Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing).
 Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing).
@@ -207,7 +217,7 @@ Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing).
 Notation nat_of_Nmax := N2Nat.inj_max (only parsing).
 Notation nat_of_Nmin := N2Nat.inj_min (only parsing).
 
-Notation nat_of_N_of_nat := Nat2N.bij (only parsing).
+Notation nat_of_N_of_nat := Nat2N.id (only parsing).
 Notation N_of_nat_inj := Nat2N.inj (only parsing).
 Notation N_of_double := Nat2N.inj_double (only parsing).
 Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing).