diff options
author | 2010-10-14 11:37:33 +0000 | |
---|---|---|
committer | 2010-10-14 11:37:33 +0000 | |
commit | 888c41d2bf95bb84fee28a8737515c9ff66aa94e (patch) | |
tree | 80c67a7a2aa22cabc94335bc14dcd33bed981417 /theories/Numbers/Natural/Abstract | |
parent | d7a3d9b4fbfdd0df8ab4d0475fc7afa1ed5f5bcb (diff) |
Numbers: new functions pow, even, odd + many reorganisations
- Simplification of functor names, e.g. ZFooProp instead of ZFooPropFunct
- The axiomatisations of the different fonctions are now in {N,Z}Axioms.v
apart for Z division (three separate flavours in there own files).
Content of {N,Z}AxiomsSig is extended, old version is {N,Z}AxiomsMiniSig.
- In NAxioms, the recursion field isn't that useful, since we axiomatize
other functions and not define them (apart in the toy NDefOps.v).
We leave recursion there, but in a separate NAxiomsFullSig.
- On Z, the pow function is specified to behave as Zpower : a^(-1)=0
- In BigN/BigZ, (power:t->N->t) is now pow_N, while pow is t->t->t
These pow could be more clever (we convert 2nd arg to N and use pow_N).
Default "^" is now (pow:t->t->t). BigN/BigZ ring is adapted accordingly
- In BigN, is_even is now even, its spec is changed to use Zeven_bool.
We add an odd. In BigZ, we add even and odd.
- In ZBinary (implem of ZAxioms by ZArith), we create an efficient Zpow
to implement pow. This Zpow should replace the current linear Zpower
someday.
- In NPeano (implem of NAxioms by Arith), we create pow, even, odd functions,
and we modify the div and mod functions for them to be linear, structural,
tail-recursive.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
-rw-r--r-- | theories/Numbers/Natural/Abstract/NAdd.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NAddOrder.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 65 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 41 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 35 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NDiv.v | 17 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NIso.v | 8 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NMaxMin.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NMulOrder.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NParity.v | 206 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NPow.v | 147 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NProperties.v | 15 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NStrongRec.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NSub.v | 6 |
15 files changed, 479 insertions, 95 deletions
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. |