diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAdd.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAddOrder.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 66 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 14 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivFloor.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivTrunc.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZLt.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMaxMin.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMul.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZParity.v | 196 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPow.v | 151 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZProperties.v | 14 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZSgnAbs.v | 48 |
15 files changed, 469 insertions, 80 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. |