Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits

Initial plan was only to add shiftl/shiftr/land/... to N and
other number type, this is only partly done, but this work has
diverged into a big reorganisation and improvement session
of PArith,NArith,ZArith.

Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a)

PArith/BinPos:
 - added a power function Ppow
 - iterator iter_pos moved from Zmisc to here + some lemmas
 - added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2
 - more lemmas on Pcompare and succ/+/* and order, allow
   to simplify a lot some old proofs elsewhere.
 - new/revised results on Pminus (including some direct proof of
   stuff from Pnat)

PArith/Pnat:
 - more direct proofs (limit the need of stuff about Pmult_nat).
 - provide nicer names for some lemmas (eg. Pplus_plus instead of
   nat_of_P_plus_morphism), compatibility notations provided.
 - kill some too-specific lemmas unused in stdlib + contribs

NArith/BinNat:
 - N_of_nat, nat_of_N moved from Nnat to here.
 - a lemma relating Npred and Nminus
 - revised definitions and specification proofs of Npow and Nlog2

NArith/Nnat:
 - shorter proofs.
 - stuff about Z_of_N is moved to Znat. This way, NArith is
   entirely independent from ZArith.

NArith/Ndigits:
 - added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr
 - revised proofs about Nxor, still using functional bit stream
 - use the same approach to prove properties of Nand Nor Ndiff

ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff

ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat

ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N

ZArith/Zmisc: almost empty new, only contain stuff about badly-named
 iter. Should be reformed more someday.

ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes
 proofs and avoid slowdown due to adding 1 in Z instead of in positive

Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt
 as long as I dont't know why it's slower on powers of two.

Elsewhere: propagate new names + some nicer proofs

NB: Impact on compatibility is probably non-zero, but should be
really moderate. We'll see on contribs, but a few Require here
and there might be necessary.

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

1 files changed, 78 insertions, 254 deletions

diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 93fdfff7a9..05ca4a5500 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -6,149 +6,86 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Arith_base.
-Require Import Compare_dec.
-Require Import Sumbool.
-Require Import Div2.
-Require Import Min.
-Require Import Max.
-Require Import BinPos.
-Require Import BinNat.
-Require Import BinInt.
-Require Import Pnat.
-Require Import Znat.
-
-(** Translation from [N] to [nat] and back. *)
-
-Definition nat_of_N (a:N) :=
-  match a with
-  | N0 => 0%nat
-  | Npos p => nat_of_P p
-  end.
-
-Definition N_of_nat (n:nat) :=
-  match n with
-  | O => N0
-  | S n' => Npos (P_of_succ_nat n')
-  end.
+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 in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *.
-  rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H.
+  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.
 
 Lemma nat_of_N_of_nat : forall n:nat, nat_of_N (N_of_nat n) = n.
 Proof.
   induction n. trivial.
-  intros. simpl in |- *. apply nat_of_P_o_P_of_succ_nat_eq_succ.
+  intros. simpl. apply nat_of_P_of_succ_nat.
 Qed.
 
-(** Interaction of this translation and usual operations. *)
-
-Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a).
+Lemma nat_of_N_inj : forall n n', nat_of_N n = nat_of_N n' -> n = n'.
 Proof.
-  destruct a; simpl nat_of_N; auto.
-  apply nat_of_P_xO.
+  intros n n' H.
+  rewrite <- (N_of_nat_of_N n), <- (N_of_nat_of_N n'). now f_equal.
 Qed.
 
-Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n).
+Lemma N_of_nat_inj : forall n n', N_of_nat n = N_of_nat n' -> n = n'.
 Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  rewrite <- nat_of_Ndouble.
-  apply N_of_nat_of_N.
+  intros n n' H.
+  rewrite <- (nat_of_N_of_nat n), <- (nat_of_N_of_nat n'). now f_equal.
 Qed.
 
-Lemma nat_of_Ndouble_plus_one :
-  forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)).
+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).
 Proof.
-  destruct a; simpl nat_of_N; auto.
-  apply nat_of_P_xI.
+  destruct a; simpl nat_of_N; trivial. apply nat_of_P_xO.
 Qed.
 
-Lemma N_of_double_plus_one :
-  forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n).
+Lemma nat_of_Ndouble_plus_one :
+  forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)).
 Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  rewrite <- nat_of_Ndouble_plus_one.
-  apply N_of_nat_of_N.
+  destruct a; simpl nat_of_N; trivial. apply nat_of_P_xI.
 Qed.
 
 Lemma nat_of_Nsucc : forall a, nat_of_N (Nsucc a) = S (nat_of_N a).
 Proof.
   destruct a; simpl.
   apply nat_of_P_xH.
-  apply nat_of_P_succ_morphism.
-Qed.
-
-Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n).
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  rewrite <- nat_of_Nsucc.
-  apply N_of_nat_of_N.
+  apply Psucc_S.
 Qed.
 
 Lemma nat_of_Nplus :
   forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a').
 Proof.
   destruct a; destruct a'; simpl; auto.
-  apply nat_of_P_plus_morphism.
+  apply Pplus_plus.
 Qed.
 
-Lemma N_of_plus :
-  forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n').
+Lemma nat_of_Nmult :
+  forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a').
 Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nplus.
-  apply N_of_nat_of_N.
+  destruct a; destruct a'; simpl; auto.
+  apply Pmult_mult.
 Qed.
 
 Lemma nat_of_Nminus :
   forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat.
 Proof.
-  destruct a; destruct a'; simpl; auto with arith.
-  case_eq (Pcompare p p0 Eq); simpl; intros.
-  rewrite (Pcompare_Eq_eq _ _ H); auto with arith.
-  rewrite Pminus_mask_diag. simpl. apply minus_n_n.
-  rewrite Pminus_mask_Lt. pose proof (nat_of_P_lt_Lt_compare_morphism _ _ H). simpl.
-  symmetry; apply not_le_minus_0. auto with arith. assumption.
-  pose proof (Pminus_mask_Gt p p0 H) as H1. destruct H1 as [q [H1 _]]. rewrite H1; simpl.
-  replace q with (Pminus p p0) by (unfold Pminus; now rewrite H1).
-  apply nat_of_P_minus_morphism; auto.
-Qed.
-
-Lemma N_of_minus :
-  forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n').
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nminus.
-  apply N_of_nat_of_N.
-Qed.
-
-Lemma nat_of_Nmult :
-  forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a').
-Proof.
-  destruct a; destruct a'; simpl; auto.
-  apply nat_of_P_mult_morphism.
+  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.
 Qed.
 
-Lemma N_of_mult :
-  forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n').
+Lemma nat_of_Npred : forall a, nat_of_N (Npred a) = pred (nat_of_N a).
 Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nmult.
-  apply N_of_nat_of_N.
+ intros. rewrite pred_of_minus, Npred_minus. apply nat_of_Nminus.
 Qed.
 
 Lemma nat_of_Ndiv2 :
@@ -162,205 +99,92 @@ Proof.
   rewrite div2_double; auto.
 Qed.
 
-Lemma N_of_div2 :
-  forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n).
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  rewrite <- nat_of_Ndiv2.
-  apply N_of_nat_of_N.
-Qed.
-
 Lemma nat_of_Ncompare :
  forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a').
 Proof.
-  destruct a; destruct a'; simpl.
-  reflexivity.
-  assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P.
-  destruct nat_of_P; [inversion NZ|auto].
-  assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P.
-  destruct nat_of_P; [inversion NZ|auto].
-  apply nat_of_P_compare_morphism.
-Qed.
-
-Lemma N_of_nat_compare :
- forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n').
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  symmetry; apply nat_of_Ncompare.
-Qed.
-
-Lemma nat_of_Nmin :
-  forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a').
-Proof.
-  intros; unfold Nmin; rewrite nat_of_Ncompare.
-  rewrite nat_compare_equiv; unfold nat_compare_alt.
-  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|];
-    simpl; intros; symmetry; auto with arith.
-  apply min_l; rewrite e; auto with arith.
-Qed.
-
-Lemma N_of_min :
-  forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n').
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nmin.
-  apply N_of_nat_of_N.
+  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.
 Qed.
 
 Lemma nat_of_Nmax :
   forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a').
 Proof.
-  intros; unfold Nmax; rewrite nat_of_Ncompare.
-  rewrite nat_compare_equiv; unfold nat_compare_alt.
-  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|];
-    simpl; intros; symmetry; auto with arith.
-  apply max_r; rewrite e; auto with arith.
-Qed.
-
-Lemma N_of_max :
-  forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n').
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nmax.
-  apply N_of_nat_of_N.
+  intros; unfold Nmax; rewrite nat_of_Ncompare. symmetry.
+  case nat_compare_spec; intros H; try rewrite H; auto with arith.
 Qed.
 
-(** Properties concerning [Z_of_N] *)
-
-Lemma Z_of_nat_of_N : forall n:N, Z_of_nat (nat_of_N n) = Z_of_N n.
-Proof.
-  destruct n; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
-Qed.
-
-Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m.
-Proof.
- intros; f_equal; assumption.
-Qed.
-
-Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m.
-Proof.
- intros [|n] [|m]; simpl; intros; try discriminate; congruence.
-Qed.
-
-Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m.
-Proof.
- split; [apply Z_of_N_eq | apply Z_of_N_eq_rev].
-Qed.
-
-Lemma Z_of_N_le : forall n m, (n<=m)%N -> (Z_of_N n <= Z_of_N m)%Z.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_le_rev : forall n m, (Z_of_N n <= Z_of_N m)%Z -> (n<=m)%N.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> (Z_of_N n <= Z_of_N m)%Z.
-Proof.
- split; [apply Z_of_N_le | apply Z_of_N_le_rev].
-Qed.
-
-Lemma Z_of_N_lt : forall n m, (n<m)%N -> (Z_of_N n < Z_of_N m)%Z.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_lt_rev : forall n m, (Z_of_N n < Z_of_N m)%Z -> (n<m)%N.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> (Z_of_N n < Z_of_N m)%Z.
-Proof.
- split; [apply Z_of_N_lt | apply Z_of_N_lt_rev].
-Qed.
-
-Lemma Z_of_N_ge : forall n m, (n>=m)%N -> (Z_of_N n >= Z_of_N m)%Z.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_ge_rev : forall n m, (Z_of_N n >= Z_of_N m)%Z -> (n>=m)%N.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> (Z_of_N n >= Z_of_N m)%Z.
-Proof.
- split; [apply Z_of_N_ge | apply Z_of_N_ge_rev].
-Qed.
-
-Lemma Z_of_N_gt : forall n m, (n>m)%N -> (Z_of_N n > Z_of_N m)%Z.
+Lemma nat_of_Nmin :
+  forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a').
 Proof.
- intros [|n] [|m]; simpl; auto.
+  intros; unfold Nmin; rewrite nat_of_Ncompare. symmetry.
+  case nat_compare_spec; intros H; try rewrite H; auto with arith.
 Qed.
 
-Lemma Z_of_N_gt_rev : forall n m, (Z_of_N n > Z_of_N m)%Z -> (n>m)%N.
-Proof.
- intros [|n] [|m]; simpl; auto.
-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 Z_of_N_gt_iff : forall n m, (n>m)%N <-> (Z_of_N n > Z_of_N m)%Z.
+Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n).
 Proof.
- split; [apply Z_of_N_gt | apply Z_of_N_gt_rev].
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n.
+Lemma N_of_double_plus_one :
+  forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n).
 Proof.
- destruct n; simpl; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p.
+Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n).
 Proof.
- destruct p; simpl; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z.
+Lemma N_of_pred : forall n, N_of_nat (pred n) = Npred (N_of_nat n).
 Proof.
- destruct z; simpl; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z.
+Lemma N_of_plus :
+  forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n').
 Proof.
- destruct n; intro; discriminate.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_plus : forall n m:N, Z_of_N (n+m) = (Z_of_N n + Z_of_N m)%Z.
+Lemma N_of_minus :
+  forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n').
 Proof.
- destruct n; destruct m; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_mult : forall n m:N, Z_of_N (n*m) = (Z_of_N n * Z_of_N m)%Z.
+Lemma N_of_mult :
+  forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n').
 Proof.
- destruct n; destruct m; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m).
+Lemma N_of_div2 :
+  forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n).
 Proof.
- intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n).
+Lemma N_of_nat_compare :
+ forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n').
 Proof.
- intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S.
+  intros. rewrite nat_of_Ncompare. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m).
+Lemma N_of_min :
+  forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n').
 Proof.
- intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m).
+Lemma N_of_max :
+  forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n').
 Proof.
- intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
-