diff options
57 files changed, 1909 insertions, 368 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. diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index bceea42b7..7d7cc4ac5 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -10,8 +10,7 @@ Require Import NZAxioms NZBase. -Module Type NZAddPropSig - (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ). +Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). Hint Rewrite pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz. @@ -76,8 +75,7 @@ Qed. Theorem add_shuffle2 : forall n m p q, (n + m) + (p + q) == (n + q) + (m + p). Proof. -intros n m p q. -rewrite 2 add_assoc, add_shuffle0, add_cancel_r. apply add_shuffle0. +intros n m p q. rewrite (add_comm p). apply add_shuffle1. Qed. Theorem sub_1_r : forall n, n - 1 == P n. @@ -85,4 +83,4 @@ Proof. intro n; now nzsimpl. Qed. -End NZAddPropSig. +End NZAddProp. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index b715b4b00..3aa6f41d3 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -10,8 +10,8 @@ Require Import NZAxioms NZBase NZMul NZOrder. -Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig'). -Include NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ. +Module Type NZAddOrderProp (Import NZ : NZOrdAxiomsSig'). +Include NZBaseProp NZ <+ NZMulProp NZ <+ NZOrderProp NZ. Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m. Proof. @@ -147,5 +147,22 @@ Proof. intros n m H; apply add_le_cases; now nzsimpl. Qed. -End NZAddOrderPropSig. +(** Substraction *) + +(** We can prove the existence of a subtraction of any number by + a smaller one *) + +Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p. +Proof. + intros n m H. apply le_ind with (4:=H). solve_predicate_wd. + exists 0; nzsimpl; split; order. + clear m H. intros m H (p & EQ & LE). exists (S p). + split. nzsimpl. now apply succ_wd. now apply le_le_succ_r. +Qed. + +(** For the moment, it doesn't seem possible to relate + this existing subtraction with [sub]. +*) + +End NZAddOrderProp. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index d2437e354..a86fec3fd 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -10,7 +10,7 @@ Require Import NZAxioms. -Module Type NZBasePropSig (Import NZ : NZDomainSig'). +Module Type NZBaseProp (Import NZ : NZDomainSig'). Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *) @@ -83,5 +83,5 @@ Tactic Notation "nzinduct" ident(n) := Tactic Notation "nzinduct" ident(n) constr(u) := induction_maker n ltac:(apply central_induction with (z := u)). -End NZBasePropSig. +End NZBaseProp. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 75f0206f8..3b9720f32 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -45,11 +45,10 @@ Module Type NZDiv (NZ:NZOrdAxiomsSig) Module Type NZDiv' (NZ:NZOrdAxiomsSig) := NZDiv NZ <+ DivModNotation NZ. -Module NZDivPropFunct +Module NZDivProp (Import NZ : NZOrdAxiomsSig') - (Import NZP : NZMulOrderPropSig NZ) - (Import NZD : NZDiv' NZ) -. + (Import NZP : NZMulOrderProp NZ) + (Import NZD : NZDiv' NZ). (** Uniqueness theorems *) @@ -538,5 +537,5 @@ Proof. rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. Qed. -End NZDivPropFunct. +End NZDivProp. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index f07c55524..a26e93d76 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -305,7 +305,7 @@ End NZOfNat. Module NZOfNatOrd (Import NZ:NZOrdSig'). Include NZOfNat NZ. -Include NZOrderPropFunct NZ. +Include NZBaseProp NZ <+ NZOrderProp NZ. Local Open Scope ofnat. Theorem ofnat_S_gt_0 : diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index a87d6ac62..55ec3f30e 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -10,9 +10,8 @@ Require Import NZAxioms NZBase NZAdd. -Module Type NZMulPropSig - (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ). -Include NZAddPropSig NZ NZBase. +Module Type NZMulProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). +Include NZAddProp NZ NZBase. Theorem mul_0_r : forall n, n * 0 == 0. Proof. @@ -65,4 +64,19 @@ Proof. intro n. now nzsimpl. Qed. -End NZMulPropSig. +Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m. +Proof. +intros n m p. now rewrite <- 2 mul_assoc, (mul_comm m). +Qed. + +Theorem mul_shuffle1 : forall n m p q, (n * m) * (p * q) == (n * p) * (m * q). +Proof. +intros n m p q. now rewrite 2 mul_assoc, (mul_shuffle0 n). +Qed. + +Theorem mul_shuffle2 : forall n m p q, (n * m) * (p * q) == (n * q) * (m * p). +Proof. +intros n m p q. rewrite (mul_comm p). apply mul_shuffle1. +Qed. + +End NZMulProp. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 414931ba8..530044ab0 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -11,8 +11,8 @@ Require Import NZAxioms. Require Import NZAddOrder. -Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig'). -Include NZAddOrderPropSig NZ. +Module Type NZMulOrderProp (Import NZ : NZOrdAxiomsSig'). +Include NZAddOrderProp NZ. Theorem mul_lt_pred : forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). @@ -302,4 +302,4 @@ rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l. apply add_pos_pos; now apply lt_0_1. Qed. -End NZMulOrderPropSig. +End NZMulOrderProp. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 8fdf8b47e..93201964e 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -10,8 +10,8 @@ Require Import NZAxioms NZBase Decidable OrdersTac. -Module Type NZOrderPropSig - (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ). +Module Type NZOrderProp + (Import NZ : NZOrdSig')(Import NZBase : NZBaseProp NZ). Instance le_wd : Proper (eq==>eq==>iff) le. Proof. @@ -357,6 +357,13 @@ intros z n H; apply lt_exists_pred_strong with (z := z) (n := n). assumption. apply le_refl. Qed. +Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n. +Proof. + intros z n H. + destruct (lt_exists_pred _ _ H) as (n' & EQ & LE). + rewrite EQ. now rewrite pred_succ. +Qed. + (** Stronger variant of induction with assumptions n >= 0 (n < 0) in the induction step *) @@ -557,7 +564,7 @@ apply right_induction with (S n); [assumption | | now apply <- le_succ_l]. intros; apply H2; try assumption. now apply -> le_succ_l. Qed. -(** Elimintation principle for <= *) +(** Elimination principle for <= *) Theorem le_ind : forall (n : t), A n -> @@ -628,15 +635,12 @@ Qed. End WF. -End NZOrderPropSig. - -Module NZOrderPropFunct (NZ : NZOrdSig) := - NZBasePropSig NZ <+ NZOrderPropSig NZ. +End NZOrderProp. (** If we have moreover a [compare] function, we can build an [OrderedType] structure. *) -Module NZOrderedTypeFunct (NZ : NZDecOrdSig') - <: DecidableTypeFull <: OrderedTypeFull := - NZ <+ NZOrderPropFunct <+ Compare2EqBool <+ HasEqBool2Dec. +Module NZOrderedType (NZ : NZDecOrdSig') + <: DecidableTypeFull <: OrderedTypeFull + := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v new file mode 100644 index 000000000..cbc286fbb --- /dev/null +++ b/theories/Numbers/NatInt/NZPow.v @@ -0,0 +1,358 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Power Function *) + +Require Import NZAxioms NZMulOrder. + +(** Interface of a power function, then its specification on naturals *) + +Module Type Pow (Import T:Typ). + Parameters Inline pow : t -> t -> t. +End Pow. + +Module Type PowNotation (T:Typ)(Import NZ:Pow T). + Infix "^" := pow. +End PowNotation. + +Module Type Pow' (T:Typ) := Pow T <+ PowNotation T. + +Module Type NZPowSpec (Import NZ : NZOrdAxiomsSig')(Import P : Pow' NZ). + Declare Instance pow_wd : Proper (eq==>eq==>eq) pow. + Axiom pow_0_r : forall a, a^0 == 1. + Axiom pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b. +End NZPowSpec. + +Module Type NZPow (NZ:NZOrdAxiomsSig) := Pow NZ <+ NZPowSpec NZ. +Module Type NZPow' (NZ:NZOrdAxiomsSig) := Pow' NZ <+ NZPowSpec NZ. + +(** Derived properties of power *) + +Module NZPowProp + (Import NZ : NZOrdAxiomsSig') + (Import NZP : NZMulOrderProp NZ) + (Import NZP' : NZPow' NZ). + +Hint Rewrite pow_0_r pow_succ_r : nz. + +Lemma lt_0_2 : 0 < 2. +Proof. + apply lt_succ_r, le_0_1. +Qed. + +Ltac order' := generalize lt_0_1 lt_0_2; order. + +(** Power and basic constants *) + +Lemma pow_0_l : forall a, 0<a -> 0^a == 0. +Proof. + intros a Ha. + destruct (lt_exists_pred _ _ Ha) as (a' & EQ & Ha'). + rewrite EQ. now nzsimpl. +Qed. + +Lemma pow_1_r : forall a, a^1 == a. +Proof. + intros. now nzsimpl. +Qed. + +Lemma pow_1_l : forall a, 0<=a -> 1^a == 1. +Proof. + apply le_ind; intros. solve_predicate_wd. + now nzsimpl. + now nzsimpl. +Qed. + +Hint Rewrite pow_1_l : nz. + +Lemma pow_2_r : forall a, a^2 == a*a. +Proof. + intros. nzsimpl; order'. +Qed. + +(** Power and addition, multiplication *) + +Lemma pow_add_r : forall a b c, 0<=b -> 0<=c -> + a^(b+c) == a^b * a^c. +Proof. + intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + now nzsimpl. + clear b Hb. intros b Hb IH Hc. + nzsimpl; trivial. + rewrite IH; trivial. apply mul_assoc. + now apply add_nonneg_nonneg. +Qed. + +Lemma pow_mul_l : forall a b c, 0<=c -> + (a*b)^c == a^c * b^c. +Proof. + intros a b c Hc. apply le_ind with (4:=Hc). solve_predicate_wd. + now nzsimpl. + clear c Hc. intros c Hc IH. + nzsimpl; trivial. + rewrite IH; trivial. apply mul_shuffle1. +Qed. + +Lemma pow_mul_r : forall a b c, 0<=b -> 0<=c -> + a^(b*c) == (a^b)^c. +Proof. + intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + intros. now nzsimpl. + clear b Hb. intros b Hb IH Hc. + nzsimpl; trivial. + rewrite pow_add_r, IH, pow_mul_l; trivial. apply mul_comm. + now apply mul_nonneg_nonneg. +Qed. + +(** Positivity *) + +Lemma pow_nonneg_nonneg : forall a b, 0<=a -> 0<=b -> 0<=a^b. +Proof. + intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + nzsimpl; order'. + clear b Hb. intros b Hb IH. + nzsimpl; trivial. now apply mul_nonneg_nonneg. +Qed. + +Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b. +Proof. + intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + nzsimpl; order'. + clear b Hb. intros b Hb IH. + nzsimpl; trivial. now apply mul_pos_pos. +Qed. + +(** Monotonicity *) + +Lemma pow_lt_mono_l : forall a b c, 0<c -> 0<=a<b -> a^c < b^c. +Proof. + intros a b c Hc. apply lt_ind with (4:=Hc). solve_predicate_wd. + intros (Ha,H). nzsimpl; trivial; order. + clear c Hc. intros c Hc IH (Ha,H). + nzsimpl; try order. + apply mul_lt_mono_nonneg; trivial. + apply pow_nonneg_nonneg; try order. + apply IH. now split. +Qed. + +Lemma pow_le_mono_l : forall a b c, 0<=c -> 0<=a<=b -> a^c <= b^c. +Proof. + intros a b c Hc (Ha,H). + apply lt_eq_cases in Hc; destruct Hc as [Hc|Hc]; [|rewrite <- Hc]. + apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H]. + apply lt_le_incl, pow_lt_mono_l; now try split. + now nzsimpl. +Qed. + +Lemma pow_gt_1 : forall a b, 1<a -> 0<b -> 1<a^b. +Proof. + intros a b Ha Hb. rewrite <- (pow_1_l b) by order. + apply pow_lt_mono_l; try split; order'. +Qed. + +Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=b<c -> a^b < a^c. +Proof. + intros a b c Ha (Hb,H). + assert (H' : b<=c) by order. + destruct (le_exists_sub _ _ H') as (d & EQ & Hd). + rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1. + apply mul_lt_mono_pos_r. + apply pow_pos_nonneg; order'. + apply pow_gt_1; trivial. + apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial. + rewrite <- EQ' in *. rewrite add_0_l in EQ. 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 -> 0<=b<=c -> a^b <= a^c. +Proof. + intros a b c Ha (Hb,H). + apply le_succ_l in Ha. + apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. + apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H]. + apply lt_le_incl, pow_lt_mono_r; now try split. + nzsimpl; order. +Qed. + +Lemma pow_le_mono : forall a b c d, 0<a<=c -> 0<=b<=d -> + a^b <= c^d. +Proof. + intros. transitivity (a^d). + apply pow_le_mono_r; intuition order. + apply pow_le_mono_l; intuition order. +Qed. + +Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d -> + a^b < c^d. +Proof. + intros a b c d (Ha,Hac) (Hb,Hbd). + apply le_succ_l in Ha. + apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. + transitivity (a^d). + apply pow_lt_mono_r; intuition order. + apply pow_lt_mono_l; try split; order'. + nzsimpl; try order. apply pow_gt_1; order. +Qed. + +(** Injectivity *) + +Lemma pow_inj_l : forall a b c, 0<=a -> 0<=b -> 0<c -> + a^c == b^c -> a == b. +Proof. + intros a b c Ha Hb Hc EQ. + destruct (lt_trichotomy a b) as [LT|[EQ'|GT]]; trivial. + assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial). + order. + assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). + order. +Qed. + +Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c -> + a^b == a^c -> b == c. +Proof. + intros a b c Ha Hb Hc EQ. + destruct (lt_trichotomy b c) as [LT|[EQ'|GT]]; trivial. + assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial). + order. + assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial). + order. +Qed. + +(** Monotonicity results, both ways *) + +Lemma pow_lt_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> + (a<b <-> a^c < b^c). +Proof. + intros a b c Ha Hb Hc. + split; intro LT. + apply pow_lt_mono_l; try split; trivial. + destruct (le_gt_cases b a) as [LE|GT]; trivial. + assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order). + order. +Qed. + +Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> + (a<=b <-> a^c <= b^c). +Proof. + intros a b c Ha Hb Hc. + split; intro LE. + apply pow_le_mono_l; try split; trivial. order. + destruct (le_gt_cases a b) as [LE'|GT]; trivial. + assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). + order. +Qed. + +Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c -> + (b<c <-> a^b < a^c). +Proof. + intros a b c Ha Hb Hc. + split; intro LT. + apply pow_lt_mono_r; try split; trivial. + destruct (le_gt_cases c b) as [LE|GT]; trivial. + assert (a^c <= a^b) by (apply pow_le_mono_r; try split; order'). + order. +Qed. + +Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c -> + (b<=c <-> a^b <= a^c). +Proof. + intros a b c Ha Hb Hc. + split; intro LE. + apply pow_le_mono_r; try split; trivial. order'. + destruct (le_gt_cases b c) as [LE'|GT]; trivial. + assert (a^c < a^b) by (apply pow_lt_mono_r; try split; order'). + order. +Qed. + +(** For any a>1, the a^x function is above the identity function *) + +Lemma pow_gt_lin_r : forall a b, 1<a -> 0<=b -> b < a^b. +Proof. + intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + nzsimpl. order'. + clear b Hb. intros b Hb IH. nzsimpl; trivial. + rewrite <- !le_succ_l in *. + transitivity (2*(S b)). + nzsimpl. rewrite <- 2 succ_le_mono. + rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + apply mul_le_mono_nonneg; trivial. + order'. + now apply lt_le_incl, lt_succ_r. +Qed. + +(** Someday, we should say something about the full Newton formula. + In the meantime, we can at least provide some inequalities about + (a+b)^c. +*) + +Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c -> + a^c + b^c <= (a+b)^c. +Proof. + intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd. + nzsimpl; order. + clear c Hc. intros c Hc IH. + assert (0<=c) by order'. + nzsimpl; trivial. + transitivity ((a+b)*(a^c + b^c)). + rewrite mul_add_distr_r, !mul_add_distr_l. + apply add_le_mono. + rewrite <- add_0_r at 1. apply add_le_mono_l. + apply mul_nonneg_nonneg; trivial. + apply pow_nonneg_nonneg; trivial. + rewrite <- add_0_l at 1. apply add_le_mono_r. + apply mul_nonneg_nonneg; trivial. + apply pow_nonneg_nonneg; trivial. + apply mul_le_mono_nonneg_l; trivial. + now apply add_nonneg_nonneg. +Qed. + +(** This upper bound can also be seen as a convexity proof for x^c : + image of (a+b)/2 is below the middle of the images of a and b +*) + +Lemma pow_add_upper : forall a b c, 0<=a -> 0<=b -> 0<c -> + (a+b)^c <= 2^(pred c) * (a^c + b^c). +Proof. + assert (aux : forall a b c, 0<=a<=b -> 0<c -> + (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)). + (* begin *) + intros a b c (Ha,H) Hc. + rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl. + rewrite <- !add_assoc. apply add_le_mono_l. + rewrite !add_assoc. apply add_le_mono_r. + destruct (le_exists_sub _ _ H) as (d & EQ & Hd). + rewrite EQ. + rewrite 2 mul_add_distr_r. + rewrite !add_assoc. apply add_le_mono_r. + rewrite add_comm. apply add_le_mono_l. + apply mul_le_mono_nonneg_l; trivial. + apply pow_le_mono_l; try split; order. + (* end *) + intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd. + nzsimpl; order. + clear c Hc. intros c Hc IH. + assert (0<=c) by order. + nzsimpl; trivial. + transitivity ((a+b)*(2^(pred c) * (a^c + b^c))). + apply mul_le_mono_nonneg_l; trivial. + now apply add_nonneg_nonneg. + rewrite mul_assoc. rewrite (mul_comm (a+b)). + assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order'). + assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l). + assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl; order). + rewrite EQ', <- !mul_assoc. + apply mul_le_mono_nonneg_l. + apply pow_nonneg_nonneg; order'. + destruct (le_gt_cases a b). + apply aux; try split; order'. + rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)). + apply aux; try split; order'. +Qed. + +End NZPowProp. diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v index 5ef304606..13c262337 100644 --- a/theories/Numbers/NatInt/NZProperties.v +++ b/theories/Numbers/NatInt/NZProperties.v @@ -11,8 +11,8 @@ Require Export NZAxioms NZMulOrder. (** This functor summarizes all known facts about NZ. - For the moment it is only an alias to [NZMulOrderPropFunct], which + For the moment it is only an alias to [NZMulOrderProp], which subsumes all others. *) -Module Type NZPropFunct := NZMulOrderPropSig. +Module Type NZProp := NZMulOrderProp. diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index b2324d971..96d60c997 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -10,8 +10,8 @@ Require Export NBase. -Module NAddPropFunct (Import N : NAxiomsSig'). -Include NBasePropFunct N. +Module NAddProp (Import N : NAxiomsMiniSig'). +Include NBaseProp N. (** For theorems about [add] that are both valid for [N] and [Z], see [NZAdd] *) (** Now comes theorems valid for natural numbers but not for Z *) @@ -75,5 +75,5 @@ intros n m H; rewrite (add_comm n (P m)); rewrite (add_comm n m); now apply add_pred_l. Qed. -End NAddPropFunct. +End NAddProp. diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index fe7a491dd..da41886f0 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -10,8 +10,8 @@ Require Export NOrder. -Module NAddOrderPropFunct (Import N : NAxiomsSig'). -Include NOrderPropFunct N. +Module NAddOrderProp (Import N : NAxiomsMiniSig'). +Include NOrderProp N. (** Theorems true for natural numbers, not for integers *) @@ -43,4 +43,4 @@ Proof. intros; apply add_nonneg_pos. apply le_0_l. assumption. Qed. -End NAddOrderPropFunct. +End NAddOrderProp. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index fd5a35391..66ff2ded5 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -8,30 +8,67 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Export NZAxioms. +Require Export NZAxioms NZPow NZDiv. -Set Implicit Arguments. +(** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *) -Module Type NAxioms (Import NZ : NZDomainSig'). +Module Type NAxiom (Import NZ : NZDomainSig'). + Axiom pred_0 : P 0 == 0. +End NAxiom. -Axiom pred_0 : P 0 == 0. +Module Type NAxiomsMiniSig := NZOrdAxiomsSig <+ NAxiom. +Module Type NAxiomsMiniSig' := NZOrdAxiomsSig' <+ NAxiom. -Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A. -Implicit Arguments recursion [A]. -Declare Instance recursion_wd (A : Type) (Aeq : relation A) : - Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). +(** Let's now add some more functions and their specification *) + +(** Parity functions *) + +Module Type Parity (Import N : NAxiomsMiniSig'). + 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. + +(** Power function : NZPow is enough *) + +(** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon, + and add to that a N-specific constraint. *) + +Module Type NDivSpecific (Import N : NAxiomsMiniSig')(Import DM : DivMod' N). + Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. +End NDivSpecific. + + +(** We now group everything together. *) + +Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity + <+ NZPow.NZPow <+ DivMod <+ NZDivCommon <+ NDivSpecific. + +Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity + <+ NZPow.NZPow' <+ DivMod' <+ NZDivCommon <+ NDivSpecific. + + +(** It could also be interesting to have a constructive recursor function. *) + +Module Type NAxiomsRec (Import NZ : NZDomainSig'). + +Parameter Inline recursion : forall {A : Type}, A -> (t -> A -> A) -> t -> A. + +Declare Instance recursion_wd {A : Type} (Aeq : relation A) : + Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion. Axiom recursion_0 : - forall (A : Type) (a : A) (f : t -> A -> A), recursion a f 0 = a. + forall {A} (a : A) (f : t -> A -> A), recursion a f 0 = a. Axiom recursion_succ : - forall (A : Type) (Aeq : relation A) (a : A) (f : t -> A -> A), + forall {A} (Aeq : relation A) (a : A) (f : t -> A -> A), Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)). -End NAxioms. - -Module Type NAxiomsSig := NZOrdAxiomsSig <+ NAxioms. -Module Type NAxiomsSig' := NZOrdAxiomsSig' <+ NAxioms. +End NAxiomsRec. +Module Type NAxiomsFullSig := NAxiomsSig <+ NAxiomsRec. +Module Type NAxiomsFullSig' := NAxiomsSig' <+ NAxiomsRec. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 911be68b0..e9ec6a823 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -12,42 +12,19 @@ Require Export Decidable. Require Export NAxioms. Require Import NZProperties. -Module NBasePropFunct (Import N : NAxiomsSig'). +Module NBaseProp (Import N : NAxiomsMiniSig'). (** First, we import all known facts about both natural numbers and integers. *) -Include NZPropFunct N. +Include NZProp N. -(** We prove that the successor of a number is not zero by defining a -function (by recursion) that maps 0 to false and the successor to true *) - -Definition if_zero (A : Type) (a b : A) (n : N.t) : A := - recursion a (fun _ _ => b) n. - -Implicit Arguments if_zero [A]. - -Instance if_zero_wd (A : Type) : - Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A). -Proof. -intros; unfold if_zero. -repeat red; intros. apply recursion_wd; auto. repeat red; auto. -Qed. - -Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a. -Proof. -unfold if_zero; intros; now rewrite recursion_0. -Qed. - -Theorem if_zero_succ : - forall (A : Type) (a b : A) (n : N.t), if_zero a b (S n) = b. -Proof. -intros; unfold if_zero. -now rewrite recursion_succ. -Qed. +(** From [pred_0] and order facts, we can prove that 0 isn't a successor. *) Theorem neq_succ_0 : forall n, S n ~= 0. Proof. -intros n H. -generalize (Logic.eq_refl (if_zero false true 0)). -rewrite <- H at 1. rewrite if_zero_0, if_zero_succ; discriminate. + intros n EQ. + assert (EQ' := pred_succ n). + rewrite EQ, pred_0 in EQ'. + rewrite <- EQ' in EQ. + now apply (neq_succ_diag_l 0). Qed. Theorem neq_0_succ : forall n, 0 ~= S n. @@ -204,5 +181,5 @@ Ltac double_induct n m := pattern n, m; apply double_induction; clear n m; [solve_relation_wd | | | ]. -End NBasePropFunct. +End NBaseProp. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 308a24f79..c1bac7165 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -12,8 +12,37 @@ Require Import Bool. (* To get the orb and negb function *) Require Import RelationPairs. Require Export NStrongRec. -Module NdefOpsPropFunct (Import N : NAxiomsSig'). -Include NStrongRecPropFunct N. +(** In this module, we derive generic implementations of usual operators + just via the use of a [recursion] function. *) + +Module NdefOpsProp (Import N : NAxiomsFullSig'). +Include NStrongRecProp N. + +(** Nullity Test *) + +Definition if_zero (A : Type) (a b : A) (n : N.t) : A := + recursion a (fun _ _ => b) n. + +Implicit Arguments if_zero [A]. + +Instance if_zero_wd (A : Type) : + Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A). +Proof. +intros; unfold if_zero. +repeat red; intros. apply recursion_wd; auto. repeat red; auto. +Qed. + +Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a. +Proof. +unfold if_zero; intros; now rewrite recursion_0. +Qed. + +Theorem if_zero_succ : + forall (A : Type) (a b : A) (n : N.t), if_zero a b (S n) = b. +Proof. +intros; unfold if_zero. +now rewrite recursion_succ. +Qed. (*****************************************************) (** Addition *) @@ -473,5 +502,5 @@ Theorem log_pow2 : forall n, log (2^^n) = n. *) -End NdefOpsPropFunct. +End NdefOpsProp. diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 773b9ad61..be56c8b03 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -6,18 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Euclidean Division *) +(** Properties of Euclidean Division *) -Require Import NAxioms NProperties NZDiv. +Require Import NAxioms NSub NZDiv. -Module Type NDivSpecific (Import N : NAxiomsSig')(Import DM : DivMod' N). - Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. -End NDivSpecific. - -Module Type NDivSig := NAxiomsSig <+ DivMod <+ NZDivCommon <+ NDivSpecific. -Module Type NDivSig' := NAxiomsSig' <+ DivMod' <+ NZDivCommon <+ NDivSpecific. - -Module NDivPropFunct (Import N : NDivSig')(Import NP : NPropSig N). +Module NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N). (** We benefit from what already exists for NZ *) @@ -30,7 +23,7 @@ Module NDivPropFunct (Import N : NDivSig')(Import NP : NPropSig N). Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. Proof. split. apply le_0_l. apply mod_upper_bound. order. Qed. End ND. - Module Import NZDivP := NZDivPropFunct N NP ND. + Module Import NZDivP := NZDivProp N NP ND. Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l. @@ -235,5 +228,5 @@ Lemma mod_divides : forall a b, b~=0 -> (a mod b == 0 <-> exists c, a == b*c). Proof. intros. apply mod_divides; auto'. Qed. -End NDivPropFunct. +End NDivProp. diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 19e5a318a..3a48b7997 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -10,7 +10,7 @@ Require Import NBase. -Module Homomorphism (N1 N2 : NAxiomsSig). +Module Homomorphism (N1 N2 : NAxiomsFullSig). Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity). @@ -51,9 +51,9 @@ Qed. End Homomorphism. -Module Inverse (N1 N2 : NAxiomsSig). +Module Inverse (N1 N2 : NAxiomsFullSig). -Module Import NBasePropMod1 := NBasePropFunct N1. +Module Import NBasePropMod1 := NBaseProp N1. (* This makes the tactic induct available. Since it is taken from (NBasePropFunct NAxiomsMod1), it refers to induction on N1. *) @@ -74,7 +74,7 @@ Qed. End Inverse. -Module Isomorphism (N1 N2 : NAxiomsSig). +Module Isomorphism (N1 N2 : NAxiomsFullSig). Module Hom12 := Homomorphism N1 N2. Module Hom21 := Homomorphism N2 N1. diff --git a/theories/Numbers/Natural/Abstract/NMaxMin.v b/theories/Numbers/Natural/Abstract/NMaxMin.v index f8276c160..cdff6dbc8 100644 --- a/theories/Numbers/Natural/Abstract/NMaxMin.v +++ b/theories/Numbers/Natural/Abstract/NMaxMin.v @@ -10,8 +10,8 @@ Require Import NAxioms NSub GenericMinMax. (** * Properties of minimum and maximum specific to natural numbers *) -Module Type NMaxMinProp (Import N : NAxiomsSig'). -Include NSubPropFunct N. +Module Type NMaxMinProp (Import N : NAxiomsMiniSig'). +Include NSubProp N. (** Zero *) diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index 3eb6f3698..f6c6ad542 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -10,8 +10,8 @@ Require Export NAddOrder. -Module NMulOrderPropFunct (Import N : NAxiomsSig'). -Include NAddOrderPropFunct N. +Module NMulOrderProp (Import N : NAxiomsMiniSig'). +Include NAddOrderProp N. (** Theorems that are either not valid on Z or have different proofs on N and Z *) @@ -74,5 +74,5 @@ assert (H3 : 1 < n * m) by now apply (lt_1_l m). rewrite H in H3; false_hyp H3 lt_irrefl. Qed. -End NMulOrderPropFunct. +End NMulOrderProp. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index faa78b30c..fa855f210 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -10,8 +10,8 @@ Require Export NAdd. -Module NOrderPropFunct (Import N : NAxiomsSig'). -Include NAddPropFunct N. +Module NOrderProp (Import N : NAxiomsMiniSig'). +Include NAddProp N. (* Theorems that are true for natural numbers but not for integers *) @@ -238,5 +238,5 @@ rewrite pred_0. split; intro H; apply le_0_l. intro n. rewrite pred_succ. apply succ_le_mono. Qed. -End NOrderPropFunct. +End NOrderProp. diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v new file mode 100644 index 000000000..e815f9ee6 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -0,0 +1,206 @@ +(************************************************************************) +(* 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 NSub. + +(** 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 *) + +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. + +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. +Proof. + intros. rewrite <- (succ_pred n) at 2 by trivial. + symmetry. apply even_succ_odd. +Qed. + +Lemma even_pred_odd : 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). +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; + intros (m',Hm) (n',Hn). + exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm. + exists (n'-m'-1). + rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r. + rewrite <- (add_1_l 1) at 5. rewrite sub_add_distr. + symmetry. apply sub_add. + apply le_add_le_sub_l. + rewrite add_1_l, <- (mul_1_r 2) at 1. + rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l. + rewrite le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r. + destruct (le_gt_cases n' m') as [LE|GT]; trivial. + generalize (double_below _ _ LE). order. + apply lt_succ_r, le_0_1. + exists (n'-m'). rewrite mul_sub_distr_l, Hn, Hm. + apply add_sub_swap. + apply mul_le_mono_pos_l. + apply lt_succ_r, le_0_1. + destruct (le_gt_cases m' n') as [LE|GT]; trivial. + generalize (double_above _ _ GT). order. + exists (n'-m'). rewrite Hm,Hn, mul_sub_distr_l. + rewrite sub_add_distr. rewrite add_sub_swap. apply add_sub. + apply succ_le_mono. + rewrite add_1_r in Hm,Hn. order. +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. + now destruct (even n), (even m). +Qed. + +End NParityProp. diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v new file mode 100644 index 000000000..0039a1e2c --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NPow.v @@ -0,0 +1,147 @@ +(************************************************************************) +(* 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 NAxioms NSub NParity NZPow. + +(** Derived properties of power, specialized on natural numbers *) + +Module NPowProp + (Import N : NAxiomsSig')(Import NS : NSubProp N)(Import NP : NParityProp N NS). + + Module Import NZPowP := NZPowProp N NS N. + + Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l. + Ltac wrap l := intros; apply l; auto'. + +Lemma pow_succ_r' : forall a b, a^(S b) == a * a^b. +Proof. wrap pow_succ_r. Qed. + +(** Power and basic constants *) + +Lemma pow_0_l : forall a, a~=0 -> 0^a == 0. +Proof. wrap pow_0_l. Qed. + +Definition pow_1_r : forall a, a^1 == a + := pow_1_r. + +Lemma pow_1_l : forall a, 1^a == 1. +Proof. wrap pow_1_l. Qed. + +Definition pow_2_r : forall a, a^2 == a*a + := pow_2_r. + +(** Power and addition, multiplication *) + +Lemma pow_add_r : forall a b c, a^(b+c) == a^b * a^c. +Proof. wrap pow_add_r. Qed. + +Lemma pow_mul_l : forall a b c, (a*b)^c == a^c * b^c. +Proof. wrap pow_mul_l. Qed. + +Lemma pow_mul_r : forall a b c, a^(b*c) == (a^b)^c. +Proof. wrap pow_mul_r. Qed. + +(** Positivity *) + +Lemma pow_nonzero : forall a b, a~=0 -> a^b~=0. +Proof. intros. rewrite neq_0_lt_0. wrap pow_pos_nonneg. Qed. + +(** Monotonicity *) + +Lemma pow_lt_mono_l : forall a b c, c~=0 -> a<b -> a^c < b^c. +Proof. wrap pow_lt_mono_l. Qed. + +Lemma pow_le_mono_l : forall a b c, a<=b -> a^c <= b^c. +Proof. wrap pow_le_mono_l. Qed. + +Lemma pow_gt_1 : forall a b, 1<a -> b~=0 -> 1<a^b. +Proof. wrap pow_gt_1. Qed. + +Lemma pow_lt_mono_r : forall a b c, 1<a -> b<c -> a^b < a^c. +Proof. wrap pow_lt_mono_r. 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, a~=0 -> b<=c -> a^b <= a^c. +Proof. wrap pow_le_mono_r. Qed. + +Lemma pow_le_mono : forall a b c d, a~=0 -> a<=c -> b<=d -> + a^b <= c^d. +Proof. wrap pow_le_mono. Qed. + +Definition pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d -> + a^b < c^d + := pow_lt_mono. + +(** Injectivity *) + +Lemma pow_inj_l : forall a b c, c~=0 -> a^c == b^c -> a == b. +Proof. intros; eapply pow_inj_l; eauto; auto'. auto'. Qed. + +Lemma pow_inj_r : forall a b c, 1<a -> a^b == a^c -> b == c. +Proof. intros; eapply pow_inj_r; eauto; auto'. Qed. + +(** Monotonicity results, both ways *) + +Lemma pow_lt_mono_l_iff : forall a b c, c~=0 -> + (a<b <-> a^c < b^c). +Proof. wrap pow_lt_mono_l_iff. Qed. + +Lemma pow_le_mono_l_iff : forall a b c, c~=0 -> + (a<=b <-> a^c <= b^c). +Proof. wrap pow_le_mono_l_iff. Qed. + +Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> + (b<c <-> a^b < a^c). +Proof. wrap pow_lt_mono_r_iff. Qed. + +Lemma pow_le_mono_r_iff : forall a b c, 1<a -> + (b<=c <-> a^b <= a^c). +Proof. wrap pow_le_mono_r_iff. Qed. + +(** For any a>1, the a^x function is above the identity function *) + +Lemma pow_gt_lin_r : forall a b, 1<a -> b < a^b. +Proof. wrap pow_gt_lin_r. Qed. + +(** Someday, we should say something about the full Newton formula. + In the meantime, we can at least provide some inequalities about + (a+b)^c. +*) + +Lemma pow_add_lower : forall a b c, c~=0 -> + a^c + b^c <= (a+b)^c. +Proof. wrap pow_add_lower. Qed. + +(** This upper bound can also be seen as a convexity proof for x^c : + image of (a+b)/2 is below the middle of the images of a and b +*) + +Lemma pow_add_upper : forall a b c, c~=0 -> + (a+b)^c <= 2^(pred c) * (a^c + b^c). +Proof. wrap pow_add_upper. Qed. + +(** Power and parity *) + +Lemma even_pow : forall a b, b~=0 -> even (a^b) = even a. +Proof. + intros a b Hb. rewrite neq_0_lt_0 in Hb. + apply lt_ind with (4:=Hb). solve_predicate_wd. + now nzsimpl. + clear b Hb. intros b Hb IH. + rewrite pow_succ_r', even_mul, IH. now destruct (even a). +Qed. + +Lemma odd_pow : forall a b, b~=0 -> odd (a^b) = odd a. +Proof. + intros. now rewrite <- !negb_even_odd, even_pow. +Qed. + +End NPowProp. diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index 46117b25b..c1977f353 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -6,15 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Export NAxioms NMaxMin. +Require Export NAxioms. +Require Import NMaxMin NParity NPow NDiv. -(** This functor summarizes all known facts about N. - For the moment it is only an alias to the last functor which - subsumes all others. -*) +(** This functor summarizes all known facts about N. *) -Module Type NPropSig := NMaxMinProp. - -Module NPropFunct (N:NAxiomsSig) <: NPropSig N. - Include NPropSig N. -End NPropFunct. +Module Type NProp (N:NAxiomsSig) := + NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NDivProp N. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index f1ff87a8f..26cf2d64a 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -13,8 +13,8 @@ and proves its properties *) Require Export NSub. -Module NStrongRecPropFunct (Import N : NAxiomsSig'). -Include NSubPropFunct N. +Module NStrongRecProp (Import N : NAxiomsFullSig'). +Include NSubProp N. Section StrongRecursion. @@ -204,5 +204,5 @@ End StrongRecursion. Implicit Arguments strong_rec [A]. -End NStrongRecPropFunct. +End NStrongRecProp. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index 4cf8d62f1..4232ecbfa 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -10,8 +10,8 @@ Require Export NMulOrder. -Module Type NSubPropFunct (Import N : NAxiomsSig'). -Include NMulOrderPropFunct N. +Module Type NSubProp (Import N : NAxiomsMiniSig'). +Include NMulOrderProp N. Theorem sub_0_l : forall n, 0 - n == 0. Proof. @@ -316,5 +316,5 @@ Theorem add_dichotomy : forall n m, (exists p, p + n == m) \/ (exists p, p + m == n). Proof. exact le_alt_dichotomy. Qed. -End NSubPropFunct. +End NSubProp. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 2bb79280c..ef4ac7c45 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -29,7 +29,7 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake Module BigN <: NType <: OrderedTypeFull <: TotalOrder := NMake.Make Int31Cyclic <+ NTypeIsNAxioms - <+ !NPropSig <+ !NDivPropFunct <+ HasEqBool2Dec + <+ !NProp <+ HasEqBool2Dec <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. @@ -58,8 +58,9 @@ Arguments Scope BigN.compare [bigN_scope bigN_scope]. Arguments Scope BigN.min [bigN_scope bigN_scope]. Arguments Scope BigN.max [bigN_scope bigN_scope]. Arguments Scope BigN.eq_bool [bigN_scope bigN_scope]. -Arguments Scope BigN.power_pos [bigN_scope positive_scope]. -Arguments Scope BigN.power [bigN_scope N_scope]. +Arguments Scope BigN.pow_pos [bigN_scope positive_scope]. +Arguments Scope BigN.pow_N [bigN_scope N_scope]. +Arguments Scope BigN.pow [bigN_scope bigN_scope]. Arguments Scope BigN.sqrt [bigN_scope]. Arguments Scope BigN.div_eucl [bigN_scope bigN_scope]. Arguments Scope BigN.modulo [bigN_scope bigN_scope]. @@ -71,7 +72,7 @@ Infix "+" := BigN.add : bigN_scope. Infix "-" := BigN.sub : bigN_scope. Infix "*" := BigN.mul : bigN_scope. Infix "/" := BigN.div : bigN_scope. -Infix "^" := BigN.power : bigN_scope. +Infix "^" := BigN.pow : bigN_scope. Infix "?=" := BigN.compare : bigN_scope. Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. Notation "x != y" := (~x==y)%bigN (at level 70, no associativity) : bigN_scope. @@ -110,11 +111,11 @@ Qed. Lemma BigNeqb_correct : forall x y, BigN.eq_bool x y = true -> x==y. Proof. now apply BigN.eqb_eq. Qed. -Lemma BigNpower : power_theory 1 BigN.mul BigN.eq (@id N) BigN.power. +Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow. Proof. constructor. -intros. red. rewrite BigN.spec_power. unfold id. -destruct Zpower_theory as [EQ]. rewrite EQ. +intros. red. rewrite BigN.spec_pow, BigN.spec_of_N. +rewrite Zpower_theory.(rpow_pow_N). destruct n; simpl. reflexivity. induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto. Qed. @@ -172,6 +173,12 @@ Ltac BigNcst t := | false => constr:NotConstant end. +Ltac BigN_to_N t := + match isBigNcst t with + | true => eval vm_compute in (BigN.to_N t) + | false => constr:NotConstant + end. + Ltac Ncst t := match isNcst t with | true => constr:t @@ -183,11 +190,12 @@ Ltac Ncst t := Add Ring BigNr : BigNring (decidable BigNeqb_correct, constants [BigNcst], - power_tac BigNpower [Ncst], + power_tac BigNpower [BigN_to_N], div BigNdiv). Section TestRing. -Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x. +Local Notation "2" := (BigN.N0 2%int31) : bigN_scope. (* temporary notation *) +Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x. intros. ring_simplify. reflexivity. Qed. End TestRing. diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index cea2e3195..6697d59c3 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -16,7 +16,7 @@ representation. The representation-dependent (and macro-generated) part is now in [NMake_gen]. *) -Require Import BigNumPrelude ZArith CyclicAxioms DoubleType +Require Import Bool BigNumPrelude ZArith Nnat CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen. Module Make (W0:CyclicType) <: NType. @@ -69,6 +69,8 @@ Module Make (W0:CyclicType) <: NType. apply Zpower_le_monotone2; auto with zarith. Qed. + Definition to_N (x : t) := Zabs_N (to_Z x). + (** * Zero and One *) Definition zero := mk_t O ZnZ.zero. @@ -731,16 +733,16 @@ Module Make (W0:CyclicType) <: NType. (** * Power *) - Fixpoint power_pos (x:t)(p:positive) : t := + Fixpoint pow_pos (x:t)(p:positive) : t := match p with | xH => x - | xO p => square (power_pos x p) - | xI p => mul (square (power_pos x p)) x + | xO p => square (pow_pos x p) + | xI p => mul (square (pow_pos x p)) x end. - Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. + Theorem spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n. Proof. - intros x n; generalize x; elim n; clear n x; simpl power_pos. + intros x n; generalize x; elim n; clear n x; simpl pow_pos. intros; rewrite spec_mul; rewrite spec_square; rewrite H. rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith. rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith. @@ -752,15 +754,23 @@ Module Make (W0:CyclicType) <: NType. intros; rewrite Zpower_1_r; auto. Qed. - Definition power (x:t)(n:N) : t := match n with + Definition pow_N (x:t)(n:N) : t := match n with | BinNat.N0 => one - | BinNat.Npos p => power_pos x p + | BinNat.Npos p => pow_pos x p end. - Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. + Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n. Proof. destruct n; simpl. apply spec_1. - apply spec_power_pos. + apply spec_pow_pos. + Qed. + + Definition pow (x y:t) : t := pow_N x (to_N y). + + Theorem spec_pow : forall x y, [pow x y] = [x] ^ [y]. + Proof. + intros. unfold pow, to_N. + now rewrite spec_pow_N, Z_of_N_abs, Zabs_eq by apply spec_pos. Qed. @@ -1000,8 +1010,6 @@ Module Make (W0:CyclicType) <: NType. intros p; exact (spec_of_pos p). Qed. - Definition to_N (x : t) := Zabs_N (to_Z x). - (** * [head0] and [tail0] Number of zero at the beginning and at the end of @@ -1497,17 +1505,40 @@ Module Make (W0:CyclicType) <: NType. (** * Parity test *) - Definition is_even : t -> bool := Eval red_t in + Definition even : t -> bool := Eval red_t in iter_t (fun n x => ZnZ.is_even x). - Lemma is_even_fold : is_even = iter_t (fun n x => ZnZ.is_even x). + Definition odd x := negb (even x). + + Lemma even_fold : even = iter_t (fun n x => ZnZ.is_even x). Proof. red_t; reflexivity. Qed. - Theorem spec_is_even: forall x, - if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1. + Theorem spec_even_aux: forall x, + if even x then [x] mod 2 = 0 else [x] mod 2 = 1. Proof. - intros x. rewrite is_even_fold. destr_t x as (n,x). + intros x. rewrite even_fold. destr_t x as (n,x). exact (ZnZ.spec_is_even x). Qed. + Theorem spec_even: forall x, even x = Zeven_bool [x]. + Proof. + intros x. assert (H := spec_even_aux x). symmetry. + rewrite (Z_div_mod_eq_full [x] 2); auto with zarith. + destruct (even x); rewrite H, ?Zplus_0_r. + rewrite Zeven_bool_iff. apply Zeven_2p. + apply not_true_is_false. rewrite Zeven_bool_iff. + apply Zodd_not_Zeven. apply Zodd_2p_plus_1. + Qed. + + Theorem spec_odd: forall x, odd x = Zodd_bool [x]. + Proof. + intros x. unfold odd. + assert (H := spec_even_aux x). symmetry. + rewrite (Z_div_mod_eq_full [x] 2); auto with zarith. + destruct (even x); rewrite H, ?Zplus_0_r; simpl negb. + apply not_true_is_false. rewrite Zodd_bool_iff. + apply Zeven_not_Zodd. apply Zeven_2p. + apply Zodd_bool_iff. apply Zodd_2p_plus_1. + Qed. + End Make. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 0d6c379e0..65b166df6 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -10,14 +10,14 @@ Require Import BinPos Ndiv_def. Require Export BinNat. -Require Import NAxioms NProperties NDiv. +Require Import NAxioms NProperties. Local Open Scope N_scope. (** * Implementation of [NAxiomsSig] module type via [BinNat.N] *) Module Type N - <: NAxiomsSig <: UsualOrderedTypeFull <: TotalOrder <: DecidableTypeFull. + <: NAxiomsMiniSig <: UsualOrderedTypeFull <: TotalOrder <: DecidableTypeFull. (** Bi-directional induction. *) @@ -144,6 +144,19 @@ Program Instance mod_wd : Proper (eq==>eq==>eq) Nmod. Definition div_mod := fun x y (_:y<>0) => Ndiv_mod_eq x y. Definition mod_upper_bound := Nmod_lt. +(** Odd and Even *) + +Definition Even n := exists m, n = 2*m. +Definition Odd n := exists m, n = 2*m+1. +Definition even_spec := Neven_spec. +Definition odd_spec := Nodd_spec. + +(** Power *) + +Definition pow_0_r := Npow_0_r. +Definition pow_succ_r n p (H:0 <= p) := Npow_succ_r n p. +Program Instance pow_wd : Proper (eq==>eq==>eq) Npow. + (** The instantiation of operations. Placing them at the very end avoids having indirections in above lemmas. *) @@ -164,14 +177,13 @@ Definition min := Nmin. Definition max := Nmax. Definition div := Ndiv. Definition modulo := Nmod. +Definition pow := Npow. +Definition even := Neven. +Definition odd := Nodd. -Include NPropFunct +Include NProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. -(** Generic properties of [div] and [mod] *) - -Include NDivPropFunct. - End N. (* diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 182b9b8dd..5bb26d04f 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -8,25 +8,131 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Import Peano Peano_dec Compare_dec EqNat NAxioms NProperties NDiv. +Require Import + Bool Peano Peano_dec Compare_dec Plus Minus Le EqNat NAxioms NProperties. -(** Functions not already defined: div mod *) +(** Functions not already defined *) -Definition divF div x y := if leb y x then S (div (x-y) y) else 0. -Definition modF mod x y := if leb y x then mod (x-y) y else x. -Definition initF (_ _ : nat) := 0. +Fixpoint pow n m := + match m with + | O => 1 + | S m => n * (pow n m) + end. -Fixpoint loop {A} (F:A->A)(i:A) (n:nat) : A := - match n with - | 0 => i - | S n => F (loop F i n) - end. +Infix "^" := pow : nat_scope. + +Lemma pow_0_r : forall a, a^0 = 1. +Proof. reflexivity. Qed. + +Lemma pow_succ_r : forall a b, 0<=b -> a^(S b) = a * a^b. +Proof. reflexivity. Qed. + +Definition Even n := exists m, n = 2*m. +Definition Odd n := exists m, n = 2*m+1. + +Fixpoint even n := + match n with + | O => true + | 1 => false + | S (S n') => even n' + end. + +Definition odd n := negb (even n). + +Lemma even_spec : forall n, even n = true <-> Even n. +Proof. + fix 1. + destruct n as [|[|n]]; simpl; try rewrite even_spec; split. + now exists 0. + trivial. + discriminate. + intros (m,H). destruct m. discriminate. + simpl in H. rewrite <- plus_n_Sm in H. discriminate. + intros (m,H). exists (S m). rewrite H. simpl. now rewrite plus_n_Sm. + intros (m,H). destruct m. discriminate. exists m. + simpl in H. rewrite <- plus_n_Sm in H. inversion H. reflexivity. +Qed. + +Lemma odd_spec : forall n, odd n = true <-> Odd n. +Proof. + unfold odd. + fix 1. + destruct n as [|[|n]]; simpl; try rewrite odd_spec; split. + discriminate. + intros (m,H). rewrite <- plus_n_Sm in H; discriminate. + now exists 0. + trivial. + intros (m,H). exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m). + intros (m,H). destruct m. discriminate. exists m. + simpl in H. rewrite <- plus_n_Sm in H. inversion H. simpl. + now rewrite <- !plus_n_Sm, <- !plus_n_O. +Qed. + +(* A linear, tail-recursive, division for nat. + + In [divmod], [y] is the predecessor of the actual divisor, + and [u] is [y] minus the real remainder +*) + +Fixpoint divmod x y q u := + match x with + | 0 => (q,u) + | S x' => match u with + | 0 => divmod x' y (S q) y + | S u' => divmod x' y q u' + end + end. + +Definition div x y := + match y with + | 0 => 0 + | S y' => fst (divmod x y' 0 y') + end. + +Definition modulo x y := + match y with + | 0 => 0 + | S y' => y' - snd (divmod x y' 0 y') + end. -Definition div x y := loop divF initF x x y. -Definition modulo x y := loop modF initF x x y. Infix "/" := div : nat_scope. Infix "mod" := modulo (at level 40, no associativity) : nat_scope. +Lemma divmod_spec : forall x y q u, u <= y -> + let (q',u') := divmod x y q u in + x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y. +Proof. + induction x. simpl. intuition. + intros y q u H. destruct u; simpl divmod. + generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u'). + intros (EQ,LE); split; trivial. + rewrite <- EQ, <- minus_n_O, minus_diag, <- plus_n_O. + now rewrite !plus_Sn_m, plus_n_Sm, <- plus_assoc, mult_n_Sm. + generalize (IHx y q u (le_Sn_le _ _ H)). destruct divmod as (q',u'). + intros (EQ,LE); split; trivial. + rewrite <- EQ. + rewrite !plus_Sn_m, plus_n_Sm. f_equal. now apply minus_Sn_m. +Qed. + +Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y. +Proof. + intros x y Hy. + destruct y; [ now elim Hy | clear Hy ]. + unfold div, modulo. + generalize (divmod_spec x y 0 y (le_n y)). + destruct divmod as (q,u). + intros (U,V). + simpl in *. + now rewrite <- mult_n_O, minus_diag, <- !plus_n_O in U. +Qed. + +Lemma mod_upper_bound : forall x y, y<>0 -> x mod y < y. +Proof. + intros x y Hy. + destruct y; [ now elim Hy | clear Hy ]. + unfold modulo. + apply le_n_S, le_minus. +Qed. (** * Implementation of [NAxiomsSig] by [nat] *) @@ -119,25 +225,26 @@ Proof. reflexivity. Qed. -Definition recursion (A : Type) : A -> (nat -> A -> A) -> nat -> A := +(** Recursion fonction *) + +Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A := nat_rect (fun _ => A). -Implicit Arguments recursion [A]. -Instance recursion_wd (A : Type) (Aeq : relation A) : - Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). +Instance recursion_wd {A} (Aeq : relation A) : + Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion. Proof. intros a a' Ha f f' Hf n n' Hn. subst n'. induction n; simpl; auto. apply Hf; auto. Qed. Theorem recursion_0 : - forall (A : Type) (a : A) (f : nat -> A -> A), recursion a f 0 = a. + forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a. Proof. reflexivity. Qed. Theorem recursion_succ : - forall (A : Type) (Aeq : relation A) (a : A) (f : nat -> A -> A), + forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A), Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)). Proof. @@ -171,56 +278,29 @@ Definition eqb_eq := beq_nat_true_iff. Definition compare_spec := nat_compare_spec. Definition eq_dec := eq_nat_dec. -(** Generic Properties *) - -Include NPropFunct - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. - -(** Proofs of specification for [div] and [mod]. *) +Definition Even := Even. +Definition Odd := Odd. +Definition even := even. +Definition odd := odd. +Definition even_spec := even_spec. +Definition odd_spec := odd_spec. -Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y. -Proof. - cut (forall n x y, y<>0 -> x<=n -> - x = y*(loop divF initF n x y) + (loop modF initF n x y)). - intros H x y Hy. apply H; auto. - induction n. - simpl; unfold initF; simpl. intros. nzsimpl. auto with arith. - simpl; unfold divF at 1, modF at 1. - intros. - destruct (leb y x) as [ ]_eqn:L; - [apply leb_complete in L | apply leb_complete_conv in L; now nzsimpl]. - rewrite mul_succ_r, <- add_assoc, (add_comm y), add_assoc. - rewrite <- IHn; auto. - symmetry; apply sub_add; auto. - rewrite <- lt_succ_r. - apply lt_le_trans with x; auto. - apply sub_lt; auto. rewrite <- neq_0_lt_0; auto. -Qed. - -Lemma mod_upper_bound : forall x y, y<>0 -> x mod y < y. -Proof. - cut (forall n x y, y<>0 -> x<=n -> loop modF initF n x y < y). - intros H x y Hy. apply H; auto. - induction n. - simpl; unfold initF. intros. rewrite <- neq_0_lt_0; auto. - simpl; unfold modF at 1. - intros. - destruct (leb y x) as [ ]_eqn:L; - [apply leb_complete in L | apply leb_complete_conv in L]; auto. - apply IHn; auto. - rewrite <- lt_succ_r. - apply lt_le_trans with x; auto. - apply sub_lt; auto. rewrite <- neq_0_lt_0; auto. -Qed. +Definition pow := pow. +Program Instance pow_wd : Proper (eq==>eq==>eq) pow. +Definition pow_0_r := pow_0_r. +Definition pow_succ_r := pow_succ_r. Definition div := div. Definition modulo := modulo. Program Instance div_wd : Proper (eq==>eq==>eq) div. Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. +Definition div_mod := div_mod. +Definition mod_upper_bound := mod_upper_bound. -(** Generic properties of [div] and [mod] *) +(** Generic Properties *) -Include NDivPropFunct. +Include NProp + <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. End Nat. diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index ba2864760..3ff2ded62 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -46,8 +46,9 @@ Module Type NType. Parameter sub : t -> 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 log2 : t -> t. Parameter div_eucl : t -> t -> t * t. @@ -56,7 +57,8 @@ Module Type NType. Parameter gcd : t -> t -> t. Parameter shiftr : t -> t -> t. Parameter shiftl : t -> t -> t. - Parameter is_even : t -> bool. + 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 +72,9 @@ Module Type NType. Parameter spec_sub: forall x y, [sub x y] = Zmax 0 ([x] - [y]). 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, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. Parameter spec_log2_0: forall x, [x] = 0 -> [log2 x] = 0. Parameter spec_log2: forall x, [x]<>0 -> 2^[log2 x] <= [x] < 2^([log2 x]+1). @@ -82,8 +85,8 @@ Module Type NType. Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b]. Parameter spec_shiftr: forall p x, [shiftr p x] = [x] / 2^[p]. Parameter spec_shiftl: forall p x, [shiftl p x] = [x] * 2^[p]. - Parameter spec_is_even: forall x, - if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1. + Parameter spec_even: forall x, even x = Zeven_bool [x]. + Parameter spec_odd: forall x, odd x = Zodd_bool [x]. End NType. @@ -94,6 +97,7 @@ Module Type NType_Notation (Import N:NType). Infix "+" := add. Infix "-" := sub. Infix "*" := mul. + Infix "^" := pow. Infix "<=" := le. Infix "<" := lt. End NType_Notation. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 90dd16249..568ebeae8 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -13,13 +13,13 @@ Require Import ZArith Nnat NAxioms NDiv NSig. Module NTypeIsNAxioms (Import N : NType'). Hint Rewrite - spec_0 spec_succ spec_add spec_mul spec_pred spec_sub + spec_0 spec_1 spec_succ spec_add spec_mul spec_pred spec_sub spec_div spec_modulo spec_gcd spec_compare spec_eq_bool - spec_max spec_min spec_power_pos spec_power + spec_max spec_min spec_pow_pos spec_pow_N spec_pow spec_even spec_odd : nsimpl. Ltac nsimpl := autorewrite with nsimpl. -Ltac ncongruence := unfold eq; repeat red; intros; nsimpl; congruence. -Ltac zify := unfold eq, lt, le in *; nsimpl. +Ltac ncongruence := unfold eq, to_N; repeat red; intros; nsimpl; congruence. +Ltac zify := unfold eq, lt, le, to_N in *; nsimpl. Local Obligation Tactic := ncongruence. @@ -177,6 +177,70 @@ Proof. zify. auto. 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. intro Hb. + rewrite Zpower_exp; auto with zarith. + simpl. unfold Zpower_pos; simpl. ring. +Qed. + +Lemma pow_pow_N : forall a b, a^b == pow_N a (to_N b). +Proof. + intros. zify. f_equal. + now rewrite Z_of_N_abs, Zabs_eq by apply spec_pos. +Qed. + +Lemma pow_N_pow : forall a b, pow_N a b == a^(of_N b). +Proof. + intros. zify. f_equal. symmetry. apply spec_of_N. +Qed. + +Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p). +Proof. + intros. now zify. +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_N (Zabs_N m)). + zify. rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto. + generalize (spec_pos n); auto with zarith. + 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_N (Zabs_N m)). + zify. rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto. + generalize (spec_pos n); auto with zarith. + 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. @@ -192,6 +256,8 @@ destruct (Z_mod_lt [a] [b]); auto. generalize (spec_pos b); auto with zarith. Qed. +(** Recursion *) + Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) := Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n). Implicit Arguments recursion [A]. @@ -250,5 +316,5 @@ Qed. End NTypeIsNAxioms. Module NType_NAxioms (N : NType) - <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N <: HasMinMax N + <: NAxiomsSig <: HasCompare N <: HasEqBool N <: HasMinMax N := N <+ NTypeIsNAxioms. diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index d850f927a..6bb9c2ac4 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -937,8 +937,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Definition power_pos (x : t) p : t := match x with - | Qz zx => Qz (Z.power_pos zx p) - | Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p) + | Qz zx => Qz (Z.pow_pos zx p) + | Qq nx dx => Qq (Z.pow_pos nx p) (N.pow_pos dx p) end. Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p. @@ -946,25 +946,25 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. intros [ z | n d ] p; unfold power_pos. (* Qz *) simpl. - rewrite Z.spec_power_pos. + rewrite Z.spec_pow_pos. rewrite Qpower_decomp. red; simpl; f_equal. rewrite Zpower_pos_1_l; auto. (* Qq *) simpl. - rewrite Z.spec_power_pos. + rewrite Z.spec_pow_pos. destr_eqb; nzsimpl; intros. apply Qeq_sym; apply Qpower_positive_0. - rewrite N.spec_power_pos in *. + rewrite N.spec_pow_pos in *. assert (0 < N.to_Z d ^ ' p)%Z by (apply Zpower_gt_0; auto with zarith). romega. - rewrite N.spec_power_pos, H in *. + rewrite N.spec_pow_pos, H in *. rewrite Zpower_0_l in H0; [romega|discriminate]. rewrite Qpower_decomp. red; simpl; do 3 f_equal. rewrite Z2P_correct by (generalize (N.spec_pos d); romega). - rewrite N.spec_power_pos. auto. + rewrite N.spec_pow_pos. auto. Qed. Instance strong_spec_power_pos x p `(Reduced x) : Reduced (power_pos x p). @@ -979,10 +979,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. revert H. unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl. destr_eqb; nzsimpl; simpl; intros. - rewrite N.spec_power_pos in H0. + rewrite N.spec_pow_pos in H0. rewrite H, Zpower_0_l in *; [romega|discriminate]. rewrite Z2P_correct in *; auto. - rewrite N.spec_power_pos, Z.spec_power_pos; auto. + rewrite N.spec_pow_pos, Z.spec_pow_pos; auto. rewrite Zgcd_1_rel_prime in *. apply rel_prime_Zpower; auto with zarith. Qed. diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget index 787eee55c..a54e85872 100644 --- a/theories/Numbers/vo.itarget +++ b/theories/Numbers/vo.itarget @@ -28,6 +28,8 @@ Integer/Abstract/ZDivFloor.vo Integer/Abstract/ZDivTrunc.vo Integer/Abstract/ZDivEucl.vo Integer/Abstract/ZMaxMin.vo +Integer/Abstract/ZParity.vo +Integer/Abstract/ZPow.vo Integer/BigZ/BigZ.vo Integer/BigZ/ZMake.vo Integer/Binary/ZBinary.vo @@ -45,6 +47,7 @@ NatInt/NZOrder.vo NatInt/NZProperties.vo NatInt/NZDomain.vo NatInt/NZDiv.vo +NatInt/NZPow.vo Natural/Abstract/NAddOrder.vo Natural/Abstract/NAdd.vo Natural/Abstract/NAxioms.vo @@ -58,6 +61,8 @@ Natural/Abstract/NSub.vo Natural/Abstract/NProperties.vo Natural/Abstract/NDiv.vo Natural/Abstract/NMaxMin.vo +Natural/Abstract/NParity.vo +Natural/Abstract/NPow.vo Natural/BigN/BigN.vo Natural/BigN/Nbasic.vo Natural/BigN/NMake_gen.vo diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 53e71a53c..27393c265 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -6,11 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Rbase. -Require Import Rfunctions. -Require Import SeqSeries. -Require Import Rtrigo_fun. -Require Import Max. +Require Import Max Rbase Rfunctions SeqSeries Rtrigo_fun. Open Local Scope R_scope. (********************************) diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v index 83dbfa2fc..df81fa9a6 100644 --- a/theories/ZArith/ZOdiv.v +++ b/theories/ZArith/ZOdiv.v @@ -228,7 +228,7 @@ Module ZODivMod := ZBinary.Z <+ ZODiv. (** We hence benefit from generic results about this abstract division. *) -Module Z := ZDivTrunc.ZDivPropFunct ZODivMod ZBinary.Z. +Module Z := ZDivTrunc.ZDivProp ZODivMod ZBinary.Z. (** * Unicity results *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 409fac31a..83e3d8320 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -315,7 +315,7 @@ Module Z. Proof. intros; apply Z_mod_lt; auto with zarith. Qed. Definition mod_neg_bound := Z_mod_neg. - Include ZBinary.Z <+ ZDivFloor.ZDivPropFunct. + Include ZBinary.Z <+ ZDivFloor.ZDivProp. End Z. |