From 9764ebbb67edf73a147c536a3c4f4ed0f1a7ce9e Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 6 Dec 2010 15:47:32 +0000 Subject: 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 --- theories/Numbers/Integer/Abstract/ZParity.v | 160 ++-------------------------- 1 file changed, 8 insertions(+), 152 deletions(-) (limited to 'theories/Numbers/Integer/Abstract/ZParity.v') diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index 4c752043c..5c7e9eb14 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -6,167 +6,23 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Bool ZMulOrder. +Require Import Bool ZMulOrder NZParity. -(** Properties of [even] and [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 more properties of [even] and [odd]. *) Module Type ZParityProp (Import Z : ZAxiomsSig') (Import ZP : ZMulOrderProp Z). -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. - nzinduct x. - left. exists 0. now nzsimpl. - intros x. - split; intros [(y,H)|(y,H)]. - right. exists y. rewrite H. now nzsimpl. - left. exists (S y). rewrite H. now nzsimpl'. - right. exists (P y). rewrite <- succ_inj_wd. rewrite H. - nzsimpl'. now rewrite <- add_succ_l, <- add_succ_r, succ_pred. - left. exists y. rewrite <- succ_inj_wd. 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 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. - -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, odd (P n) = even n. -Proof. - intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ_odd. -Qed. - -Lemma even_pred_odd : forall n, even (P n) = odd n. -Proof. - intros. rewrite <- (succ_pred n) at 2. 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. +Include NZParityProp Z Z ZP. -Lemma even_mul : forall n m, even (mul n m) = even n || even m. +Lemma odd_pred : forall n, odd (P n) = even n. 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. + intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ. Qed. -Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m. +Lemma even_pred : forall n, even (P n) = odd n. Proof. - intros. rewrite <- !negb_even_odd. rewrite even_mul. - now destruct (even n), (even m). + intros. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ. Qed. Lemma even_opp : forall n, even (-n) = even n. @@ -180,7 +36,7 @@ Qed. Lemma odd_opp : forall n, odd (-n) = odd n. Proof. - intros. rewrite <- !negb_even_odd. now rewrite even_opp. + intros. rewrite <- !negb_even. now rewrite even_opp. Qed. Lemma even_sub : forall n m, even (n-m) = Bool.eqb (even n) (even m). -- cgit v1.2.3