diff options
Diffstat (limited to 'theories/Numbers/Integer')
21 files changed, 682 insertions, 117 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index aff298117..2c386a980 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -10,8 +10,8 @@ Require Export ZBase. -Module ZAddPropFunct (Import Z : ZAxiomsSig'). -Include ZBasePropFunct Z. +Module ZAddProp (Import Z : ZAxiomsMiniSig'). +Include ZBaseProp Z. (** Theorems that are either not valid on N or have different proofs on N and Z *) @@ -287,5 +287,5 @@ Qed. (** Of course, there are many other variants *) -End ZAddPropFunct. +End ZAddProp. diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index bdc4d21e9..eb27e6378 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -10,8 +10,8 @@ Require Export ZLt. -Module ZAddOrderPropFunct (Import Z : ZAxiomsSig'). -Include ZOrderPropFunct Z. +Module ZAddOrderProp (Import Z : ZAxiomsMiniSig'). +Include ZOrderProp Z. (** Theorems that are either not valid on N or have different proofs on N and Z *) @@ -293,6 +293,6 @@ End PosNeg. Ltac zero_pos_neg n := induction_maker n ltac:(apply zero_pos_neg). -End ZAddOrderPropFunct. +End ZAddOrderProp. diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index c0d3db92b..38855a85d 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -9,8 +9,18 @@ (************************************************************************) Require Export NZAxioms. +Require Import NZPow. -Set Implicit Arguments. +(** We obtain integers by postulating that successor of predecessor + is identity. *) + +Module Type ZAxiom (Import Z : NZAxiomsSig'). + Axiom succ_pred : forall n, S (P n) == n. +End ZAxiom. + +(** For historical reasons, ZAxiomsMiniSig isn't just NZ + ZAxiom, + we also add an [opp] function, that can be seen as a shortcut + for [sub 0]. *) Module Type Opp (Import T:Typ). Parameter Inline opp : t -> t. @@ -22,15 +32,59 @@ End OppNotation. Module Type Opp' (T:Typ) := Opp T <+ OppNotation T. -(** We obtain integers by postulating that every number has a predecessor. *) - Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z). Declare Instance opp_wd : Proper (eq==>eq) opp. - Axiom succ_pred : forall n, S (P n) == n. Axiom opp_0 : - 0 == 0. Axiom opp_succ : forall n, - (S n) == P (- n). End IsOpp. -Module Type ZAxiomsSig := NZOrdAxiomsSig <+ Opp <+ IsOpp. -Module Type ZAxiomsSig' := NZOrdAxiomsSig' <+ Opp' <+ IsOpp. +Module Type ZAxiomsMiniSig := NZOrdAxiomsSig <+ ZAxiom <+ Opp <+ IsOpp. +Module Type ZAxiomsMiniSig' := NZOrdAxiomsSig' <+ ZAxiom <+ Opp' <+ IsOpp. + +(** Other functions and their specifications *) + +(** Absolute value *) + +Module Type HasAbs(Import Z : ZAxiomsMiniSig'). + Parameter Inline abs : t -> t. + Axiom abs_eq : forall n, 0<=n -> abs n == n. + Axiom abs_neq : forall n, n<=0 -> abs n == -n. +End HasAbs. + +(** A sign function *) + +Module Type HasSgn (Import Z : ZAxiomsMiniSig'). + Parameter Inline sgn : t -> t. + Axiom sgn_null : forall n, n==0 -> sgn n == 0. + Axiom sgn_pos : forall n, 0<n -> sgn n == 1. + Axiom sgn_neg : forall n, n<0 -> sgn n == -(1). +End HasSgn. + +(** Parity functions *) + +Module Type Parity (Import Z : ZAxiomsMiniSig'). + Parameter Inline even odd : t -> bool. + Definition Even n := exists m, n == 2*m. + Definition Odd n := exists m, n == 2*m+1. + Axiom even_spec : forall n, even n = true <-> Even n. + Axiom odd_spec : forall n, odd n = true <-> Odd n. +End Parity. + +(** For the power function, we just add to NZPow an addition spec *) + +Module Type ZPowSpecNeg (Import Z : ZAxiomsMiniSig')(Import P : Pow' Z). + Axiom pow_neg : forall a b, b<0 -> a^b == 0. +End ZPowSpecNeg. + + +(** Let's group everything *) + +Module Type ZAxiomsSig := + ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity + <+ NZPow.NZPow <+ ZPowSpecNeg. +Module Type ZAxiomsSig' := + ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity + <+ NZPow.NZPow' <+ ZPowSpecNeg. + +(** Division is left apart, since many different flavours are available *) diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 1c9844322..f9bd8dba3 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -12,8 +12,8 @@ Require Export Decidable. Require Export ZAxioms. Require Import NZProperties. -Module ZBasePropFunct (Import Z : ZAxiomsSig'). -Include NZPropFunct Z. +Module ZBaseProp (Import Z : ZAxiomsMiniSig'). +Include NZProp Z. (* Theorems that are true for integers but not for natural numbers *) @@ -27,5 +27,5 @@ Proof. intros n1 n2; split; [apply pred_inj | apply pred_wd]. Qed. -End ZBasePropFunct. +End ZBaseProp. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 076815b2e..bb5c2410f 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -23,17 +23,17 @@ Require Import ZAxioms ZProperties NZDiv. -Module Type ZDivSpecific (Import Z : ZAxiomsExtSig')(Import DM : DivMod' Z). +Module Type ZDivSpecific (Import Z : ZAxiomsSig')(Import DM : DivMod' Z). Axiom mod_always_pos : forall a b, 0 <= a mod b < abs b. End ZDivSpecific. -Module Type ZDiv (Z:ZAxiomsExtSig) +Module Type ZDiv (Z:ZAxiomsSig) := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. -Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. +Module Type ZDivSig := ZAxiomsSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. -Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). +Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z). (** We benefit from what already exists for NZ *) @@ -49,7 +49,7 @@ Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). apply mod_always_pos. Qed. End ZD. - Module Import NZDivP := NZDivPropFunct Z ZP ZD. + Module Import NZDivP := NZDivProp Z ZP ZD. (** Another formulation of the main equation *) @@ -601,5 +601,5 @@ now apply mod_mul. Qed. -End ZDivPropFunct. +End ZDivProp. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index fd052c2ef..c619d8b07 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -34,10 +34,10 @@ End ZDivSpecific. Module Type ZDiv (Z:ZAxiomsSig) := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. -Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. +Module Type ZDivSig := ZAxiomsSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. -Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). +Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z). (** We benefit from what already exists for NZ *) @@ -50,7 +50,7 @@ Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. Proof. intros. now apply mod_pos_bound. Qed. End ZD. - Module Import NZDivP := NZDivPropFunct Z ZP ZD. + Module Import NZDivP := NZDivProp Z ZP ZD. (** Another formulation of the main equation *) @@ -628,5 +628,5 @@ rewrite Hc, mul_comm. now apply mod_mul. Qed. -End ZDivPropFunct. +End ZDivProp. diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 4411b8dca..027223415 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -35,14 +35,14 @@ End ZDivSpecific. Module Type ZDiv (Z:ZAxiomsSig) := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. -Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. +Module Type ZDivSig := ZAxiomsSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. -Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). +Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z). (** We benefit from what already exists for NZ *) - Module Import NZDivP := NZDivPropFunct Z ZP Z. + Module Import NZDivP := NZDivProp Z ZP Z. Ltac pos_or_neg a := let LT := fresh "LT" in @@ -528,5 +528,5 @@ Proof. intros (c,Hc). rewrite Hc, mul_comm. now apply mod_mul. Qed. -End ZDivPropFunct. +End ZDivProp. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index ed812fcc3..540e17cb4 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -10,8 +10,8 @@ Require Export ZMul. -Module ZOrderPropFunct (Import Z : ZAxiomsSig'). -Include ZMulPropFunct Z. +Module ZOrderProp (Import Z : ZAxiomsMiniSig'). +Include ZMulProp Z. (** Instances of earlier theorems for m == 0 *) @@ -128,5 +128,5 @@ setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m. apply <- eq_opp_r. now rewrite opp_pred, opp_0. Qed. -End ZOrderPropFunct. +End ZOrderProp. diff --git a/theories/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v index 53709a906..4e653fee4 100644 --- a/theories/Numbers/Integer/Abstract/ZMaxMin.v +++ b/theories/Numbers/Integer/Abstract/ZMaxMin.v @@ -10,8 +10,8 @@ Require Import ZAxioms ZMulOrder GenericMinMax. (** * Properties of minimum and maximum specific to integer numbers *) -Module Type ZMaxMinProp (Import Z : ZAxiomsSig'). -Include ZMulOrderPropFunct Z. +Module Type ZMaxMinProp (Import Z : ZAxiomsMiniSig'). +Include ZMulOrderProp Z. (** The following results are concrete instances of [max_monotone] and similar lemmas. *) diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 05a285f21..68eca3305 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -10,8 +10,8 @@ Require Export ZAdd. -Module ZMulPropFunct (Import Z : ZAxiomsSig'). -Include ZAddPropFunct Z. +Module ZMulProp (Import Z : ZAxiomsMiniSig'). +Include ZAddProp Z. (** A note on naming: right (correspondingly, left) distributivity happens when the sum is multiplied by a number on the right @@ -65,6 +65,6 @@ intros n m p; rewrite (mul_comm (n - m) p), (mul_comm n p), (mul_comm m p); now apply mul_sub_distr_l. Qed. -End ZMulPropFunct. +End ZMulProp. diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 4682ad8b6..76428584d 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -10,8 +10,8 @@ Require Export ZAddOrder. -Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig'). -Include ZAddOrderPropFunct Z. +Module Type ZMulOrderProp (Import Z : ZAxiomsMiniSig'). +Include ZAddOrderProp Z. Local Notation "- 1" := (-(1)). @@ -227,5 +227,5 @@ apply mul_lt_mono_nonneg. now apply lt_le_incl. assumption. apply le_0_1. assumption. Qed. -End ZMulOrderPropFunct. +End ZMulOrderProp. diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v new file mode 100644 index 000000000..1ababfe5c --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -0,0 +1,196 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Bool ZMulOrder. + +(** 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 *) + +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<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. + +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. + +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). +Qed. + +Lemma even_opp : forall n, even (-n) = even n. +Proof. + assert (H : forall n, Even n -> Even (-n)). + intros n (m,H). exists (-m). rewrite mul_opp_r. now apply opp_wd. + intros. rewrite eq_iff_eq_true, !even_spec. + split. rewrite <- (opp_involutive n) at 2. apply H. + apply H. +Qed. + +Lemma odd_opp : forall n, odd (-n) = odd n. +Proof. + intros. rewrite <- !negb_even_odd. now rewrite even_opp. +Qed. + +Lemma even_sub : forall n m, even (n-m) = Bool.eqb (even n) (even m). +Proof. + intros. now rewrite <- add_opp_r, even_add, even_opp. +Qed. + +Lemma odd_sub : forall n m, odd (n-m) = xorb (odd n) (odd m). +Proof. + intros. now rewrite <- add_opp_r, odd_add, odd_opp. +Qed. + +End ZParityProp. diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v new file mode 100644 index 000000000..9de681375 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -0,0 +1,151 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Properties of the power function *) + +Require Import Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow. + +Module ZPowProp (Import Z : ZAxiomsSig')(Import ZM : ZMulOrderProp Z) + (Import ZP : ZParityProp Z ZM)(Import ZS : ZSgnAbsProp Z ZM). + Include NZPowProp Z ZM Z. + +(** Many results are directly the same as in NZPow, hence + the Include above. We extend nonetheless a few of them, + and add some results concerning negative first arg. +*) + +Lemma pow_mul_l' : forall a b c, (a*b)^c == a^c * b^c. +Proof. + intros a b c. destruct (le_gt_cases 0 c). now apply pow_mul_l. + rewrite !pow_neg by trivial. now nzsimpl. +Qed. + +Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b. +Proof. + intros a b Ha. destruct (le_gt_cases 0 b). + now apply pow_nonneg_nonneg. + rewrite !pow_neg by trivial. order. +Qed. + +Lemma pow_le_mono_l' : forall a b c, 0<=a<=b -> a^c <= b^c. +Proof. + intros a b c. destruct (le_gt_cases 0 c). now apply pow_le_mono_l. + rewrite !pow_neg by trivial. order. +Qed. + +(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *) + +Lemma pow_le_mono_r' : forall a b c, 0<a -> b<=c -> a^b <= a^c. +Proof. + intros a b c. destruct (le_gt_cases 0 b). + intros. apply pow_le_mono_r; try split; trivial. + rewrite !pow_neg by trivial. + intros. apply pow_nonneg. order. +Qed. + +Lemma pow_le_mono' : forall a b c d, 0<a<=c -> b<=d -> + a^b <= c^d. +Proof. + intros a b c d. destruct (le_gt_cases 0 b). + intros. apply pow_le_mono. trivial. split; trivial. + rewrite !pow_neg by trivial. + intros. apply pow_nonneg. intuition order. +Qed. + +(** Parity of power *) + +Lemma even_pow : forall a b, 0<b -> even (a^b) = even a. +Proof. + intros a b Hb. apply lt_ind with (4:=Hb). solve_predicate_wd. + now nzsimpl. + clear b Hb. intros b Hb IH. nzsimpl; [|order]. + rewrite even_mul, IH. now destruct (even a). +Qed. + +Lemma odd_pow : forall a b, 0<b -> odd (a^b) = odd a. +Proof. + intros. now rewrite <- !negb_even_odd, even_pow. +Qed. + +(** Properties of power of negative numbers *) + +Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b. +Proof. + intros a b (c,H). rewrite H. + destruct (le_gt_cases 0 c). + assert (0 <= 2) by (apply le_le_succ_r, le_0_1). + rewrite 2 pow_mul_r; trivial. + rewrite 2 pow_2_r. + now rewrite mul_opp_opp. + assert (2*c < 0). + apply mul_pos_neg; trivial. rewrite lt_succ_r. apply le_0_1. + now rewrite !pow_neg. +Qed. + +Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b). +Proof. + intros a b (c,H). rewrite H. + destruct (le_gt_cases 0 c) as [LE|GT]. + assert (0 <= 2*c). + apply mul_nonneg_nonneg; trivial. + apply le_le_succ_r, le_0_1. + rewrite add_succ_r, add_0_r, !pow_succ_r; trivial. + rewrite pow_opp_even by (now exists c). + apply mul_opp_l. + apply double_above in GT. rewrite mul_0_r in GT. + rewrite !pow_neg by trivial. now rewrite opp_0. +Qed. + +Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b. +Proof. + intros. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ. + reflexivity. + symmetry. now apply pow_opp_even. +Qed. + +Lemma pow_even_nonneg : forall a b, Even b -> 0 <= a^b. +Proof. + intros. rewrite pow_even_abs by trivial. + apply pow_nonneg, abs_nonneg. +Qed. + +Lemma pow_odd_abs_sgn : forall a b, Odd b -> a^b == sgn a * (abs a)^b. +Proof. + intros a b H. + destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. + nzsimpl. + rewrite abs_eq; order. + rewrite <- EQ'. nzsimpl. + destruct (le_gt_cases 0 b). + apply pow_0_l. + assert (b~=0) by + (contradict H; now rewrite H, <-odd_spec, <-negb_even_odd, even_0). + order. + now rewrite pow_neg. + rewrite abs_neq by order. + rewrite pow_opp_odd; trivial. + now rewrite mul_opp_opp, mul_1_l. +Qed. + +Lemma pow_odd_sgn : forall a b, 0<=b -> Odd b -> sgn (a^b) == sgn a. +Proof. + intros a b Hb H. + destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. + apply sgn_pos. apply pow_pos_nonneg; trivial. + rewrite <- EQ'. rewrite pow_0_l. apply sgn_0. + assert (b~=0) by + (contradict H; now rewrite H, <-odd_spec, <-negb_even_odd, even_0). + order. + apply sgn_neg. + rewrite <- (opp_involutive a). rewrite pow_opp_odd by trivial. + apply opp_neg_pos. + apply pow_pos_nonneg; trivial. + now apply opp_pos_neg. +Qed. + +End ZPowProp. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 5463bf2b1..7b9c6f452 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -6,17 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Export ZAxioms ZMaxMin ZSgnAbs. +Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow. -(** This functor summarizes all known facts about Z. - For the moment it is only an alias to the last functor which - subsumes all others, plus properties of [sgn] and [abs]. -*) +(** This functor summarizes all known facts about Z. *) -Module Type ZPropSig (Z:ZAxiomsExtSig) := - ZMaxMinProp Z <+ ZSgnAbsPropSig Z. +Module Type ZProp (Z:ZAxiomsSig) := + ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z. -Module ZPropFunct (Z:ZAxiomsExtSig) <: ZPropSig Z. - Include ZPropSig Z. -End ZPropFunct. diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v index 540749632..6d90bc0fd 100644 --- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v +++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v @@ -6,20 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Export ZMulOrder. +(** Properties of [abs] and [sgn] *) -(** An axiomatization of [abs]. *) - -Module Type HasAbs(Import Z : ZAxiomsSig'). - Parameter Inline abs : t -> t. - Axiom abs_eq : forall n, 0<=n -> abs n == n. - Axiom abs_neq : forall n, n<=0 -> abs n == -n. -End HasAbs. +Require Import ZMulOrder. (** Since we already have [max], we could have defined [abs]. *) -Module GenericAbs (Import Z : ZAxiomsSig') - (Import ZP : ZMulOrderPropFunct Z) <: HasAbs Z. +Module GenericAbs (Import Z : ZAxiomsMiniSig') + (Import ZP : ZMulOrderProp Z) <: HasAbs Z. Definition abs n := max n (-n). Lemma abs_eq : forall n, 0<=n -> abs n == n. Proof. @@ -35,22 +29,13 @@ Module GenericAbs (Import Z : ZAxiomsSig') Qed. End GenericAbs. -(** An Axiomatization of [sgn]. *) - -Module Type HasSgn (Import Z : ZAxiomsSig'). - Parameter Inline sgn : t -> t. - Axiom sgn_null : forall n, n==0 -> sgn n == 0. - Axiom sgn_pos : forall n, 0<n -> sgn n == 1. - Axiom sgn_neg : forall n, n<0 -> sgn n == -(1). -End HasSgn. - (** We can deduce a [sgn] function from a [compare] function *) -Module Type ZDecAxiomsSig := ZAxiomsSig <+ HasCompare. -Module Type ZDecAxiomsSig' := ZAxiomsSig' <+ HasCompare. +Module Type ZDecAxiomsSig := ZAxiomsMiniSig <+ HasCompare. +Module Type ZDecAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare. Module Type GenericSgn (Import Z : ZDecAxiomsSig') - (Import ZP : ZMulOrderPropFunct Z) <: HasSgn Z. + (Import ZP : ZMulOrderProp Z) <: HasSgn Z. Definition sgn n := match compare 0 n with Eq => 0 | Lt => 1 | Gt => -(1) end. Lemma sgn_null : forall n, n==0 -> sgn n == 0. @@ -61,11 +46,11 @@ Module Type GenericSgn (Import Z : ZDecAxiomsSig') Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. End GenericSgn. -Module Type ZAxiomsExtSig := ZAxiomsSig <+ HasAbs <+ HasSgn. -Module Type ZAxiomsExtSig' := ZAxiomsSig' <+ HasAbs <+ HasSgn. -Module Type ZSgnAbsPropSig (Import Z : ZAxiomsExtSig') - (Import ZP : ZMulOrderPropFunct Z). +(** Derived properties of [abs] and [sgn] *) + +Module Type ZSgnAbsProp (Import Z : ZAxiomsSig') + (Import ZP : ZMulOrderProp Z). Ltac destruct_max n := destruct (le_ge_cases 0 n); @@ -343,6 +328,15 @@ Proof. rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl. Qed. -End ZSgnAbsPropSig. +Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x. +Proof. + intros. + destruct (sgn_spec x) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. + apply sgn_pos, lt_0_1. + now apply sgn_null. + apply sgn_neg. rewrite opp_neg_pos. apply lt_0_1. +Qed. + +End ZSgnAbsProp. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 64553161f..6c9dc77c1 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -29,7 +29,7 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder := ZMake.Make BigN <+ ZTypeIsZAxioms - <+ !ZPropSig <+ !ZDivPropFunct <+ HasEqBool2Dec + <+ !ZProp <+ !ZDivProp <+ HasEqBool2Dec <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. (** Notations about [BigZ] *) @@ -60,8 +60,9 @@ Arguments Scope BigZ.compare [bigZ_scope bigZ_scope]. Arguments Scope BigZ.min [bigZ_scope bigZ_scope]. Arguments Scope BigZ.max [bigZ_scope bigZ_scope]. Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.power_pos [bigZ_scope positive_scope]. -Arguments Scope BigZ.power [bigZ_scope N_scope]. +Arguments Scope BigZ.pow_pos [bigZ_scope positive_scope]. +Arguments Scope BigZ.pow_N [bigZ_scope N_scope]. +Arguments Scope BigZ.pow [bigZ_scope bigZ_scope]. Arguments Scope BigZ.sqrt [bigZ_scope]. Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope]. Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope]. @@ -74,7 +75,7 @@ Infix "-" := BigZ.sub : bigZ_scope. Notation "- x" := (BigZ.opp x) : bigZ_scope. Infix "*" := BigZ.mul : bigZ_scope. Infix "/" := BigZ.div : bigZ_scope. -Infix "^" := BigZ.power : bigZ_scope. +Infix "^" := BigZ.pow : bigZ_scope. Infix "?=" := BigZ.compare : bigZ_scope. Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope. Notation "x != y" := (~x==y)%bigZ (at level 70, no associativity) : bigZ_scope. @@ -136,11 +137,13 @@ Qed. Lemma BigZeqb_correct : forall x y, BigZ.eq_bool x y = true -> x==y. Proof. now apply BigZ.eqb_eq. Qed. -Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq (@id N) BigZ.power. +Definition BigZ_of_N n := BigZ.of_Z (Z_of_N n). + +Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq BigZ_of_N BigZ.pow. Proof. constructor. -intros. red. rewrite BigZ.spec_power. unfold id. -destruct Zpower_theory as [EQ]. rewrite EQ. +intros. unfold BigZ.eq, BigZ_of_N. rewrite BigZ.spec_pow, BigZ.spec_of_Z. +rewrite Zpower_theory.(rpow_pow_N). destruct n; simpl. reflexivity. induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto. Qed. @@ -178,16 +181,25 @@ Ltac BigZcst t := | false => constr:NotConstant end. +Ltac BigZ_to_N t := + match t with + | BigZ.Pos ?t => BigN_to_N t + | BigZ.zero => constr:0%N + | BigZ.one => constr:1%N + | _ => constr:NotConstant + end. + (** Registration for the "ring" tactic *) Add Ring BigZr : BigZring (decidable BigZeqb_correct, constants [BigZcst], - power_tac BigZpower [Ncst], + power_tac BigZpower [BigZ_to_N], div BigZdiv). Section TestRing. -Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x. +Local Notation "2" := (BigZ.Pos (BigN.N0 2%int31)) : bigZ_scope. +Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x. Proof. intros. ring_simplify. reflexivity. Qed. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 6d14337ab..fb760bdf5 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -271,23 +271,23 @@ Module Make (N:NType) <: ZType. unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring. Qed. - Definition power_pos x p := + Definition pow_pos x p := match x with - | Pos nx => Pos (N.power_pos nx p) + | Pos nx => Pos (N.pow_pos nx p) | Neg nx => match p with | xH => x - | xO _ => Pos (N.power_pos nx p) - | xI _ => Neg (N.power_pos nx p) + | xO _ => Pos (N.pow_pos nx p) + | xI _ => Neg (N.pow_pos nx p) end end. - Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n. + Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n. Proof. assert (F0: forall x, (-x)^2 = x^2). intros x; rewrite Zpower_2; ring. - unfold power_pos, to_Z; intros [x | x] [p | p |]; - try rewrite N.spec_power_pos; try ring. + unfold pow_pos, to_Z; intros [x | x] [p | p |]; + try rewrite N.spec_pow_pos; try ring. assert (F: 0 <= 2 * Zpos p). assert (0 <= Zpos p); auto with zarith. rewrite Zpos_xI; repeat rewrite Zpower_exp; auto with zarith. @@ -300,18 +300,32 @@ Module Make (N:NType) <: ZType. rewrite F0; ring. Qed. - Definition power x n := + Definition pow_N x n := match n with | N0 => one - | Npos p => power_pos x p + | Npos p => pow_pos x p end. - Theorem spec_power: forall x n, to_Z (power x n) = to_Z x ^ Z_of_N n. + Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z_of_N n. Proof. - destruct n; simpl. rewrite N.spec_1; reflexivity. - apply spec_power_pos. + destruct n; simpl. apply N.spec_1. + apply spec_pow_pos. Qed. + Definition pow x y := + match to_Z y with + | Z0 => one + | Zpos p => pow_pos x p + | Zneg p => zero + end. + + Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y. + Proof. + intros. unfold pow. destruct (to_Z y); simpl. + apply N.spec_1. + apply spec_pow_pos. + apply N.spec_0. + Qed. Definition sqrt x := match x with @@ -451,4 +465,28 @@ Module Make (N:NType) <: ZType. rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith. Qed. + Definition even z := + match z with + | Pos n => N.even n + | Neg n => N.even n + end. + + Definition odd z := + match z with + | Pos n => N.odd n + | Neg n => N.odd n + end. + + Lemma spec_even : forall z, even z = Zeven_bool (to_Z z). + Proof. + intros [n|n]; simpl; rewrite N.spec_even; trivial. + destruct (N.to_Z n) as [|p|p]; now try destruct p. + Qed. + + Lemma spec_odd : forall z, odd z = Zodd_bool (to_Z z). + Proof. + intros [n|n]; simpl; rewrite N.spec_odd; trivial. + destruct (N.to_Z n) as [|p|p]; now try destruct p. + Qed. + End Make. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index e50eac17a..28a37abf8 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -10,10 +10,40 @@ Require Import ZAxioms ZProperties. -Require Import BinInt Zcompare Zorder ZArith_dec Zbool. +Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven. Local Open Scope Z_scope. +(** An alternative Zpow *) + +(** The Zpow is extensionnaly equal to Zpower in ZArith, but not + convertible with it. This Zpow uses a logarithmic number of + multiplications instead of a linear one. We should try someday to + replace Zpower with this Zpow. +*) + +Definition Zpow n m := + match m with + | Z0 => 1 + | Zpos p => Piter_op Zmult p n + | Zneg p => 0 + end. + +Lemma Zpow_0_r : forall n, Zpow n 0 = 1. +Proof. reflexivity. Qed. + +Lemma Zpow_succ_r : forall a b, 0<=b -> Zpow a (Zsucc b) = a * Zpow a b. +Proof. + intros a [|b|b] Hb; [ | |now elim Hb]; simpl. + now rewrite Zmult_1_r. + rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc. +Qed. + +Lemma Zpow_neg : forall a b, b<0 -> Zpow a b = 0. +Proof. + now destruct b. +Qed. + Theorem Z_bi_induction : forall A : Z -> Prop, Proper (eq ==> iff) A -> A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. @@ -24,11 +54,10 @@ intros; rewrite <- Zsucc_succ'. now apply -> AS. intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply <- AS. Qed. - -(** * Implementation of [ZAxiomsSig] by [BinInt.Z] *) +(** * Implementation of [ZAxiomsMiniSig] by [BinInt.Z] *) Module Z - <: ZAxiomsExtSig <: UsualOrderedTypeFull <: TotalOrder + <: ZAxiomsSig <: UsualOrderedTypeFull <: TotalOrder <: UsualDecidableTypeFull. Definition t := Z. @@ -110,13 +139,36 @@ Definition sgn_null := Zsgn_0. Definition sgn_pos := Zsgn_1. Definition sgn_neg := Zsgn_m1. +(** Even and Odd *) + +Definition Even n := exists m, n=2*m. +Definition Odd n := exists m, n=2*m+1. + +Lemma even_spec n : Zeven_bool n = true <-> Even n. +Proof. rewrite Zeven_bool_iff. exact (Zeven_ex_iff n). Qed. + +Lemma odd_spec n : Zodd_bool n = true <-> Odd n. +Proof. rewrite Zodd_bool_iff. exact (Zodd_ex_iff n). Qed. + +Definition even := Zeven_bool. +Definition odd := Zodd_bool. + +(** Power *) + +Program Instance pow_wd : Proper (eq==>eq==>eq) Zpow. + +Definition pow_0_r := Zpow_0_r. +Definition pow_succ_r := Zpow_succ_r. +Definition pow_neg := Zpow_neg. +Definition pow := Zpow. + (** We define [eq] only here to avoid refering to this [eq] above. *) Definition eq := (@eq Z). (** Now the generic properties. *) -Include ZPropFunct +Include ZProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. End Z. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 00ee19b3a..7df1871e1 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -8,16 +8,17 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Import NProperties. (* The most complete file for N *) -Require Export ZProperties. (* The most complete file for Z *) +Require Import NSub ZAxioms. Require Export Ring. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. Open Local Scope pair_scope. -Module ZPairsAxiomsMod (Import N : NAxiomsSig) <: ZAxiomsSig. -Module Import NPropMod := NPropFunct N. (* Get all properties of N *) +Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig. + Module Import NProp. + Include NSubProp N. + End NProp. Delimit Scope NScope with N. Bind Scope NScope with N.t. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index 021f4b1bf..b33ed5f8e 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -46,8 +46,9 @@ Module Type ZType. Parameter opp : t -> t. Parameter mul : t -> t -> t. Parameter square : t -> t. - Parameter power_pos : t -> positive -> t. - Parameter power : t -> N -> t. + Parameter pow_pos : t -> positive -> t. + Parameter pow_N : t -> N -> t. + Parameter pow : t -> t -> t. Parameter sqrt : t -> t. Parameter div_eucl : t -> t -> t * t. Parameter div : t -> t -> t. @@ -55,6 +56,8 @@ Module Type ZType. Parameter gcd : t -> t -> t. Parameter sgn : t -> t. Parameter abs : t -> t. + Parameter even : t -> bool. + Parameter odd : t -> bool. Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y]. Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y]. @@ -70,8 +73,9 @@ Module Type ZType. Parameter spec_opp: forall x, [opp x] = - [x]. Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. Parameter spec_square: forall x, [square x] = [x] * [x]. - Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. - Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. + Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n. + Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n. + Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n]. Parameter spec_sqrt: forall x, 0 <= [x] -> [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. Parameter spec_div_eucl: forall x y, @@ -81,6 +85,8 @@ Module Type ZType. Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). Parameter spec_sgn : forall x, [sgn x] = Zsgn [x]. Parameter spec_abs : forall x, [abs x] = Zabs [x]. + Parameter spec_even : forall x, even x = Zeven_bool [x]. + Parameter spec_odd : forall x, odd x = Zodd_bool [x]. End ZType. @@ -91,6 +97,7 @@ Module Type ZType_Notation (Import Z:ZType). Infix "+" := add. Infix "-" := sub. Infix "*" := mul. + Infix "^" := pow. Notation "- x" := (opp x). Infix "<=" := le. Infix "<" := lt. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 48cf9e868..90bda6343 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import ZArith ZAxioms ZDivFloor ZSig. +Require Import ZArith Nnat ZAxioms ZDivFloor ZSig. (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] @@ -20,6 +20,7 @@ Hint Rewrite spec_0 spec_1 spec_add spec_sub spec_pred spec_succ spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn + spec_pow spec_even spec_odd : zsimpl. Ltac zsimpl := autorewrite with zsimpl. @@ -188,13 +189,15 @@ Qed. (** Part specific to integers, not natural numbers *) -Program Instance opp_wd : Proper (eq ==> eq) opp. - Theorem succ_pred : forall n, succ (pred n) == n. Proof. intros. zify. auto with zarith. Qed. +(** Opp *) + +Program Instance opp_wd : Proper (eq ==> eq) opp. + Theorem opp_0 : - 0 == 0. Proof. intros. zify. auto with zarith. @@ -205,6 +208,8 @@ Proof. intros. zify. auto with zarith. Qed. +(** Abs / Sgn *) + Theorem abs_eq : forall n, 0 <= n -> abs n == n. Proof. intros n. zify. omega with *. @@ -230,6 +235,67 @@ Proof. intros n. zify. omega with *. Qed. +(** Power *) + +Program Instance pow_wd : Proper (eq==>eq==>eq) pow. + +Local Notation "1" := (succ 0). +Local Notation "2" := (succ 1). + +Lemma pow_0_r : forall a, a^0 == 1. +Proof. + intros. now zify. +Qed. + +Lemma pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b. +Proof. + intros a b. zify. intros Hb. + rewrite Zpower_exp; auto with zarith. + simpl. unfold Zpower_pos; simpl. ring. +Qed. + +Lemma pow_neg : forall a b, b<0 -> a^b == 0. +Proof. + intros a b. zify. intros Hb. + destruct [b]; reflexivity || discriminate. +Qed. + +Lemma pow_pow_N : forall a b, 0<=b -> a^b == pow_N a (Zabs_N (to_Z b)). +Proof. + intros a b. zify. intros Hb. + now rewrite spec_pow_N, Z_of_N_abs, Zabs_eq. +Qed. + +Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p). +Proof. + intros a b. red. now rewrite spec_pow_N, spec_pow_pos. +Qed. + +(** Even / Odd *) + +Definition Even n := exists m, n == 2*m. +Definition Odd n := exists m, n == 2*m+1. + +Lemma even_spec : forall n, even n = true <-> Even n. +Proof. + intros n. unfold Even. zify. + rewrite Zeven_bool_iff, Zeven_ex_iff. + split; intros (m,Hm). + exists (of_Z m). now zify. + exists [m]. revert Hm. now zify. +Qed. + +Lemma odd_spec : forall n, odd n = true <-> Odd n. +Proof. + intros n. unfold Odd. zify. + rewrite Zodd_bool_iff, Zodd_ex_iff. + split; intros (m,Hm). + exists (of_Z m). now zify. + exists [m]. revert Hm. now zify. +Qed. + +(** Div / Mod *) + Program Instance div_wd : Proper (eq==>eq==>eq) div. Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. |