Numbers and bitwise functions.

 See NatInt/NZBits.v for the common axiomatization of bitwise functions
 over naturals / integers. Some specs aren't pretty, but easier to
 prove, see alternate statements in property functors {N,Z}Bits.
 Negative numbers are considered via the two's complement convention.

 We provide implementations for N (in Ndigits.v), for nat (quite dummy,
 just for completeness), for Z (new file Zdigits_def), for BigN
 (for the moment partly by converting to N, to be improved soon)
 and for BigZ.

 NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
 the reversed order (for consistency with the rest of the world):
 for instance BigN.shiftl 1 10 is 2^10.

 NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
 on negative numbers. For the moment I've kept it intact, and have
 just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
 To reorganize someday ?

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

1 files changed, 9 insertions, 150 deletions

diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v
index bd6588686..6a1e20ce0 100644
--- a/theories/Numbers/Natural/Abstract/NParity.v
+++ b/theories/Numbers/Natural/Abstract/NParity.v
@@ -6,172 +6,31 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Bool NSub.
+Require Import Bool NSub NZParity.
 
-(** Properties of [even], [odd]. *)
-
-(** NB: most parts of [NParity] and [ZParity] are common,
-    but it is difficult to share them in NZ, since
-    initial proofs [Even_or_Odd] and [Even_Odd_False] must
-    be proved differently *)
+(** Some additionnal properties of [even], [odd]. *)
 
 Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N).
 
-Instance Even_wd : Proper (eq==>iff) Even.
-Proof. unfold Even. solve_predicate_wd. Qed.
-
-Instance Odd_wd : Proper (eq==>iff) Odd.
-Proof. unfold Odd. solve_predicate_wd. Qed.
-
-Instance even_wd : Proper (eq==>Logic.eq) even.
-Proof.
- intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now apply Even_wd.
-Qed.
-
-Instance odd_wd : Proper (eq==>Logic.eq) odd.
-Proof.
- intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now apply Odd_wd.
-Qed.
-
-Lemma Even_or_Odd : forall x, Even x \/ Odd x.
-Proof.
- induct x.
- left. exists 0. now nzsimpl.
- intros x.
- intros [(y,H)|(y,H)].
- right. exists y. rewrite H. now nzsimpl.
- left. exists (S y). rewrite H. now nzsimpl'.
-Qed.
-
-Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
-Proof.
- intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono.
-Qed.
-
-Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.
-Proof.
- intros. nzsimpl'.
- rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r.
- apply add_le_mono; now apply le_succ_l.
-Qed.
-
-Lemma Even_Odd_False : forall x, Even x -> Odd x -> False.
-Proof.
-intros x (y,E) (z,O). rewrite O in E; clear O.
-destruct (le_gt_cases y z) as [LE|GT].
-generalize (double_below _ _ LE); order.
-generalize (double_above _ _ GT); order.
-Qed.
-
-Lemma orb_even_odd : forall n, orb (even n) (odd n) = true.
-Proof.
- intros.
- destruct (Even_or_Odd n) as [H|H].
- rewrite <- even_spec in H. now rewrite H.
- rewrite <- odd_spec in H. now rewrite H, orb_true_r.
-Qed.
-
-Lemma negb_odd_even : forall n, negb (odd n) = even n.
-Proof.
- intros.
- generalize (Even_or_Odd n) (Even_Odd_False n).
- rewrite <- even_spec, <- odd_spec.
- destruct (odd n), (even n); simpl; intuition.
-Qed.
-
-Lemma negb_even_odd : forall n, negb (even n) = odd n.
-Proof.
- intros. rewrite <- negb_odd_even. apply negb_involutive.
-Qed.
-
-Lemma even_0 : even 0 = true.
-Proof.
- rewrite even_spec. exists 0. now nzsimpl.
-Qed.
+Include NZParityProp N N NP.
 
-Lemma odd_1 : odd 1 = true.
-Proof.
- rewrite odd_spec. exists 0. now nzsimpl'.
-Qed.
-
-Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n.
-Proof.
- split; intros (m,H).
- exists m. apply succ_inj. now rewrite add_1_r in H.
- exists m. rewrite add_1_r. now apply succ_wd.
-Qed.
-
-Lemma odd_succ_even : forall n, odd (S n) = even n.
-Proof.
- intros. apply eq_iff_eq_true. rewrite even_spec, odd_spec.
- apply Odd_succ_Even.
-Qed.
-
-Lemma even_succ_odd : forall n, even (S n) = odd n.
-Proof.
- intros. now rewrite <- negb_odd_even, odd_succ_even, negb_even_odd.
-Qed.
-
-Lemma Even_succ_Odd : forall n, Even (S n) <-> Odd n.
-Proof.
- intros. now rewrite <- even_spec, even_succ_odd, odd_spec.
-Qed.
-
-Lemma odd_pred_even : forall n, n~=0 -> odd (P n) = even n.
+Lemma odd_pred : forall n, n~=0 -> odd (P n) = even n.
 Proof.
  intros. rewrite <- (succ_pred n) at 2 by trivial.
- symmetry. apply even_succ_odd.
+ symmetry. apply even_succ.
 Qed.
 
-Lemma even_pred_odd : forall n, n~=0 -> even (P n) = odd n.
+Lemma even_pred : forall n, n~=0 -> even (P n) = odd n.
 Proof.
  intros. rewrite <- (succ_pred n) at 2 by trivial.
- symmetry. apply odd_succ_even.
-Qed.
-
-Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m).
-Proof.
- intros.
- case_eq (even n); case_eq (even m);
-  rewrite <- ?negb_true_iff, ?negb_even_odd, ?odd_spec, ?even_spec;
-  intros (m',Hm) (n',Hn).
- exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
- exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
- exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
- exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1.
-Qed.
-
-Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
-Proof.
- intros. rewrite <- !negb_even_odd. rewrite even_add.
- now destruct (even n), (even m).
-Qed.
-
-Lemma even_mul : forall n m, even (mul n m) = even n || even m.
-Proof.
- intros.
- case_eq (even n); simpl; rewrite ?even_spec.
- intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc.
- case_eq (even m); simpl; rewrite ?even_spec.
- intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2).
- (* odd / odd *)
- rewrite <- !negb_true_iff, !negb_even_odd, !odd_spec.
- intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m').
- rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r.
- now rewrite add_shuffle1, add_assoc, !mul_assoc.
-Qed.
-
-Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m.
-Proof.
- intros. rewrite <- !negb_even_odd. rewrite even_mul.
- now destruct (even n), (even m).
+ symmetry. apply odd_succ.
 Qed.
 
 Lemma even_sub : forall n m, m<=n -> even (n-m) = Bool.eqb (even n) (even m).
 Proof.
  intros.
  case_eq (even n); case_eq (even m);
-  rewrite <- ?negb_true_iff, ?negb_even_odd, ?odd_spec, ?even_spec;
+  rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec;
   intros (m',Hm) (n',Hn).
  exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm.
  exists (n'-m'-1).
@@ -197,7 +56,7 @@ Qed.
 
 Lemma odd_sub : forall n m, m<=n -> odd (n-m) = xorb (odd n) (odd m).
 Proof.
- intros. rewrite <- !negb_even_odd. rewrite even_sub by trivial.
+ intros. rewrite <- !negb_even. rewrite even_sub by trivial.
  now destruct (even n), (even m).
 Qed.