Modularization of Nnat

 For instance, nat_of_Nplus is now N2Nat.inj_add

 Note that we add an iter function in BinNat.N

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

2 files changed, 163 insertions, 123 deletions

diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 535f88c86..ec91dc5db 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -351,14 +351,22 @@ Definition testbit a n :=
 
 Definition to_nat (a:N) :=
   match a with
-  | 0 => O
-  | Npos p => Pos.to_nat p
+    | 0 => O
+    | Npos p => Pos.to_nat p
   end.
 
 Definition of_nat (n:nat) :=
   match n with
-  | O => 0
-  | S n' => Npos (Pos.of_succ_nat n')
+    | O => 0
+    | S n' => Npos (Pos.of_succ_nat n')
+  end.
+
+(** Iteration of a function *)
+
+Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
+  match n with
+    | 0 => x
+    | Npos p => Pos.iter p f x
   end.
 
 End N.
\ No newline at end of file
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 05ca4a550..ccf1e9dc6 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -9,182 +9,214 @@
 Require Import Arith_base Compare_dec Sumbool Div2 Min Max.
 Require Import BinPos BinNat Pnat.
 
-Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a.
-Proof.
-  destruct a as [| p]. reflexivity.
-  simpl. elim (nat_of_P_is_S p). intros n H. rewrite H. simpl.
-  rewrite <- nat_of_P_of_succ_nat in H.
-  rewrite nat_of_P_inj with (1 := H). reflexivity.
-Qed.
+(** * Conversions from [N] to [nat] *)
 
-Lemma nat_of_N_of_nat : forall n:nat, nat_of_N (N_of_nat n) = n.
-Proof.
-  induction n. trivial.
-  intros. simpl. apply nat_of_P_of_succ_nat.
-Qed.
+Module N2Nat.
 
-Lemma nat_of_N_inj : forall n n', nat_of_N n = nat_of_N n' -> n = n'.
+(** [N.to_nat] is a bijection between [N] and [nat],
+    with [Pos.of_nat] as reciprocal.
+    See [Nat2N.bij] below for the dual equation. *)
+
+Lemma bij a : N.of_nat (N.to_nat a) = a.
 Proof.
-  intros n n' H.
-  rewrite <- (N_of_nat_of_N n), <- (N_of_nat_of_N n'). now f_equal.
+ 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.
 Qed.
 
-Lemma N_of_nat_inj : forall n n', N_of_nat n = N_of_nat n' -> n = n'.
+(** [N.to_nat] is hence injective *)
+
+Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'.
 Proof.
-  intros n n' H.
-  rewrite <- (nat_of_N_of_nat n), <- (nat_of_N_of_nat n'). now f_equal.
+ intro H. rewrite <- (bij a), <- (bij a'). now f_equal.
 Qed.
 
-Hint Rewrite nat_of_N_of_nat N_of_nat_of_N : Nnat.
-
 (** Interaction of this translation and usual operations. *)
 
-Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a).
+Lemma inj_double a : N.to_nat (N.double a) = 2*(N.to_nat a).
 Proof.
-  destruct a; simpl nat_of_N; trivial. apply nat_of_P_xO.
+ destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xO.
 Qed.
 
-Lemma nat_of_Ndouble_plus_one :
-  forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)).
+Lemma inj_succ_double a : N.to_nat (N.succ_double a) = S (2*(N.to_nat a)).
 Proof.
-  destruct a; simpl nat_of_N; trivial. apply nat_of_P_xI.
+ destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xI.
 Qed.
 
-Lemma nat_of_Nsucc : forall a, nat_of_N (Nsucc a) = S (nat_of_N a).
+Lemma inj_succ a : N.to_nat (N.succ a) = S (N.to_nat a).
 Proof.
-  destruct a; simpl.
-  apply nat_of_P_xH.
-  apply Psucc_S.
+ destruct a; simpl; trivial. apply Pos2Nat.inj_succ.
 Qed.
 
-Lemma nat_of_Nplus :
-  forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a').
+Lemma inj_add a a' :
+  N.to_nat (a + a') = N.to_nat a + N.to_nat a'.
 Proof.
-  destruct a; destruct a'; simpl; auto.
-  apply Pplus_plus.
+ destruct a, a'; simpl; trivial. apply Pos2Nat.inj_add.
 Qed.
 
-Lemma nat_of_Nmult :
-  forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a').
+Lemma inj_mul a a' :
+  N.to_nat (a * a') = N.to_nat a * N.to_nat a'.
 Proof.
-  destruct a; destruct a'; simpl; auto.
-  apply Pmult_mult.
+ destruct a, a'; simpl; trivial. apply Pos2Nat.inj_mul.
 Qed.
 
-Lemma nat_of_Nminus :
-  forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat.
+Lemma inj_sub a a' :
+  N.to_nat (a - a') = N.to_nat a - N.to_nat a'.
 Proof.
-  intros [|a] [|a']; simpl; auto with arith.
-  destruct (Pcompare_spec a a').
-  subst. now rewrite Pminus_mask_diag, <- minus_n_n.
-  rewrite Pminus_mask_Lt by trivial. apply Plt_lt in H.
-  simpl; symmetry; apply not_le_minus_0; auto with arith.
-  destruct (Pminus_mask_Gt a a' (ZC2 _ _ H)) as (q & -> & Hq & _).
-  simpl. apply plus_minus. now rewrite <- Hq, Pplus_plus.
+ destruct a as [|a], a' as [|a']; simpl; auto with arith.
+ destruct (Pos.compare_spec a a').
+ subst. now rewrite Pos.sub_mask_diag, <- minus_n_n.
+ rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H.
+ simpl; symmetry; apply not_le_minus_0; auto with arith.
+ destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq).
+ simpl. apply plus_minus. now rewrite <- Hq, Pos2Nat.inj_add.
 Qed.
 
-Lemma nat_of_Npred : forall a, nat_of_N (Npred a) = pred (nat_of_N a).
+Lemma inj_pred a : N.to_nat (N.pred a) = pred (N.to_nat a).
 Proof.
- intros. rewrite pred_of_minus, Npred_minus. apply nat_of_Nminus.
+ intros. rewrite pred_of_minus, N.pred_sub. apply inj_sub.
 Qed.
 
-Lemma nat_of_Ndiv2 :
-  forall a, nat_of_N (Ndiv2 a) = div2 (nat_of_N a).
+Lemma inj_div2 a : N.to_nat (N.div2 a) = div2 (N.to_nat a).
 Proof.
-  destruct a; simpl in *; auto.
-  destruct p; auto.
-  rewrite nat_of_P_xI.
-  rewrite div2_double_plus_one; auto.
-  rewrite nat_of_P_xO.
-  rewrite div2_double; auto.
+ destruct a as [|[p|p| ]]; trivial.
+ simpl N.to_nat. now rewrite Pos2Nat.inj_xI, div2_double_plus_one.
+ simpl N.to_nat. now rewrite Pos2Nat.inj_xO, div2_double.
 Qed.
 
-Lemma nat_of_Ncompare :
- forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a').
+Lemma inj_compare a a' :
+ N.compare a a' = nat_compare (N.to_nat a) (N.to_nat a').
 Proof.
-  destruct a; destruct a'; simpl; trivial.
-  now destruct (nat_of_P_is_S p) as (n,->).
-  now destruct (nat_of_P_is_S p) as (n,->).
-  apply Pcompare_nat_compare.
+ destruct a, a'; simpl; trivial.
+ now destruct (Pos2Nat.is_succ p) as (n,->).
+ now destruct (Pos2Nat.is_succ p) as (n,->).
+ apply Pos2Nat.inj_compare.
 Qed.
 
-Lemma nat_of_Nmax :
-  forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a').
+Lemma inj_max a a' :
+  N.to_nat (N.max a a') = max (N.to_nat a) (N.to_nat a').
 Proof.
-  intros; unfold Nmax; rewrite nat_of_Ncompare. symmetry.
-  case nat_compare_spec; intros H; try rewrite H; auto with arith.
+ unfold N.max. rewrite inj_compare; symmetry.
+ case nat_compare_spec; intros H; try rewrite H; auto with arith.
 Qed.
 
-Lemma nat_of_Nmin :
-  forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a').
+Lemma inj_min a a' :
+  N.to_nat (N.min a a') = min (N.to_nat a) (N.to_nat a').
 Proof.
-  intros; unfold Nmin; rewrite nat_of_Ncompare. symmetry.
+  unfold N.min; rewrite inj_compare. symmetry.
   case nat_compare_spec; intros H; try rewrite H; auto with arith.
 Qed.
 
-Hint Rewrite nat_of_Ndouble nat_of_Ndouble_plus_one
- nat_of_Nsucc nat_of_Nplus nat_of_Nmult nat_of_Nminus
- nat_of_Npred nat_of_Ndiv2 nat_of_Nmax nat_of_Nmin : Nnat.
-
-Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n).
+Lemma inj_iter a {A} (f:A->A) (x:A) :
+  N.iter a f x = nat_iter (N.to_nat a) f x.
 Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
+ destruct a as [|a]. trivial. apply Pos2Nat.inj_iter.
 Qed.
 
-Lemma N_of_double_plus_one :
-  forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n).
-Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
-Qed.
+End N2Nat.
 
-Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n).
-Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
-Qed.
+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
+ : Nnat.
 
-Lemma N_of_pred : forall n, N_of_nat (pred n) = Npred (N_of_nat n).
-Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
-Qed.
 
-Lemma N_of_plus :
-  forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n').
-Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
-Qed.
+(** * Conversions from [nat] to [N] *)
 
-Lemma N_of_minus :
-  forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n').
-Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
-Qed.
+Module Nat2N.
 
-Lemma N_of_mult :
-  forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n').
-Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
-Qed.
+(** [N.of_nat] is a bijection between [nat] and [N],
+    with [Pos.to_nat] as reciprocal.
+    See [N2Nat.bij] above for the dual equation. *)
 
-Lemma N_of_div2 :
-  forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n).
+Lemma bij n : N.to_nat (N.of_nat n) = n.
 Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
+ induction n; simpl; trivial. apply SuccNat2Pos.bij.
 Qed.
 
-Lemma N_of_nat_compare :
- forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n').
-Proof.
-  intros. rewrite nat_of_Ncompare. now autorewrite with Nnat.
-Qed.
+Hint Rewrite bij : Nnat.
+Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat.
 
-Lemma N_of_min :
-  forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n').
-Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
-Qed.
+(** [N.of_nat] is hence injective *)
 
-Lemma N_of_max :
-  forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n').
+Lemma inj n n' : N.of_nat n = N.of_nat n' -> n = n'.
 Proof.
-  intros. apply nat_of_N_inj. now autorewrite with Nnat.
+ intros H. rewrite <- (bij n), <- (bij n'). now f_equal.
 Qed.
+
+(** Interaction of this translation and usual operations. *)
+
+Lemma inj_double n : N.of_nat (2*n) = N.double (N.of_nat n).
+Proof. nat2N. Qed.
+
+Lemma inj_succ_double n : N.of_nat (S (2*n)) = N.succ_double (N.of_nat n).
+Proof. nat2N. Qed.
+
+Lemma inj_succ n : N.of_nat (S n) = N.succ (N.of_nat n).
+Proof. nat2N. Qed.
+
+Lemma inj_pred n : N.of_nat (pred n) = N.pred (N.of_nat n).
+Proof. nat2N. Qed.
+
+Lemma inj_add n n' : N.of_nat (n+n') = (N.of_nat n + N.of_nat n')%N.
+Proof. nat2N. Qed.
+
+Lemma inj_sub n n' : N.of_nat (n-n') = (N.of_nat n - N.of_nat n')%N.
+Proof. nat2N. Qed.
+
+Lemma inj_mul n n' : N.of_nat (n*n') = (N.of_nat n * N.of_nat n')%N.
+Proof. nat2N. Qed.
+
+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.
+
+Lemma inj_min n n' :
+  N.of_nat (min n n') = N.min (N.of_nat n) (N.of_nat n').
+Proof. nat2N. Qed.
+
+Lemma inj_max n n' :
+  N.of_nat (max n n') = N.max (N.of_nat n) (N.of_nat n').
+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.
+
+End Nat2N.
+
+Hint Rewrite Nat2N.bij : Nnat.
+
+(** Compatibility notations *)
+
+Notation nat_of_N_inj := N2Nat.inj (only parsing).
+Notation N_of_nat_of_N := N2Nat.bij (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).
+Notation nat_of_Nplus := N2Nat.inj_add (only parsing).
+Notation nat_of_Nmult := N2Nat.inj_mul (only parsing).
+Notation nat_of_Nminus := N2Nat.inj_sub (only parsing).
+Notation nat_of_Npred := N2Nat.inj_pred (only parsing).
+Notation nat_of_Ndiv2 := N2Nat.inj_div2 (only parsing).
+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 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).
+Notation N_of_S := Nat2N.inj_succ (only parsing).
+Notation N_of_pred := Nat2N.inj_pred (only parsing).
+Notation N_of_plus := Nat2N.inj_add (only parsing).
+Notation N_of_minus := Nat2N.inj_sub (only parsing).
+Notation N_of_mult := Nat2N.inj_mul (only parsing).
+Notation N_of_div2 := Nat2N.inj_div2 (only parsing).
+Notation N_of_nat_compare := Nat2N.inj_compare (only parsing).
+Notation N_of_min := Nat2N.inj_min (only parsing).
+Notation N_of_max := Nat2N.inj_max (only parsing).