diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 18:39:14 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 18:39:14 +0000 |
commit | 70eb4b8dd94ef17cb246a25eb7525626e0f30296 (patch) | |
tree | a33bbbfe85a13b2f1071c8559da6825abc14b768 | |
parent | 5ca33dcd307ce331964a2e9867e03218c6de621b (diff) |
Numbers abstract layer: more Module Type, used especially for divisions.
Properties are now rather passed as functor arg instead of via Include or
some inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12629 85f007b7-540e-0410-9357-904b9bb8a0f7
22 files changed, 59 insertions, 67 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 3429a4fa3..64a122c71 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -15,7 +15,7 @@ Require Export ZAxioms. Require Import NZProperties. Module ZBasePropFunct (Import Z : ZAxiomsSig). -Include NZPropFunct Z. +Include Type NZPropFunct Z. Local Open Scope NumScope. (* Theorems that are true for integers but not for natural numbers *) diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index ad8e24cfb..a853395a6 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -33,9 +33,7 @@ End ZDiv. Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module ZDivPropFunct (Import Z : ZDivSig). - (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *) - Module Import ZP := ZPropFunct Z. +Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z). (** We benefit from what already exists for NZ *) @@ -48,7 +46,7 @@ Module ZDivPropFunct (Import Z : ZDivSig). apply le_trans with 0; [ rewrite opp_nonpos_nonneg |]; order. Qed. End Z'. - Module Import NZDivP := NZDivPropFunct Z'. + Module Import NZDivP := NZDivPropFunct Z' ZP. (** Another formulation of the main equation *) diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index fe695907d..551ce6b41 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -36,9 +36,7 @@ End ZDiv. Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module ZDivPropFunct (Import Z : ZDivSig). - (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *) - Module Import ZP := ZPropFunct Z. +Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z). (** We benefit from what already exists for NZ *) @@ -47,7 +45,7 @@ Module ZDivPropFunct (Import Z : ZDivSig). Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. Proof. intros. now apply mod_pos_bound. Qed. End Z'. - Module Import NZDivP := NZDivPropFunct Z'. + Module Import NZDivP := NZDivPropFunct Z' ZP. (** Another formulation of the main equation *) diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index b57f8e27f..c60bf7c6a 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -37,13 +37,11 @@ End ZDiv. Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module ZDivPropFunct (Import Z : ZDivSig). - (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *) - Module Import ZP := ZPropFunct Z. +Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z). (** We benefit from what already exists for NZ *) - Module Import NZDivP := NZDivPropFunct Z. + Module Import NZDivP := NZDivPropFunct Z ZP. Ltac pos_or_neg a := let LT := fresh "LT" in diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index a9cf0dc4d..bd9a85714 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -12,7 +12,7 @@ Require Export ZAddOrder. -Module ZMulOrderPropFunct (Import Z : ZAxiomsSig). +Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig). Include ZAddOrderPropFunct Z. Local Open Scope NumScope. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index eee5b0273..7f2253205 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -15,4 +15,9 @@ Require Export ZAxioms ZMulOrder. subsumes all others. *) -Module ZPropFunct := ZMulOrderPropFunct. +Module Type ZPropSig := ZMulOrderPropFunct. + +Module ZPropFunct (Z:ZAxiomsSig) <: ZPropSig Z. + Include Type ZPropSig Z. +End ZPropFunct. + diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 785abb5c7..bca7c3682 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -13,7 +13,8 @@ Require Import NZAxioms. Require Import NZBase. -Module NZAddProp (Import NZ : NZAxiomsSig)(Import NZBase : NZBaseProp NZ). +Module Type NZAddPropSig + (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ). Local Open Scope NumScope. Hint Rewrite @@ -88,6 +89,4 @@ Proof. intro n; now nzsimpl. Qed. -End NZAddProp. - -Module NZAddPropFunct (NZ : NZAxiomsSig) := NZBasePropFunct NZ <+ NZAddProp NZ. +End NZAddPropSig. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index b51216fd2..56982c616 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -12,10 +12,8 @@ Require Import NZAxioms NZBase NZMul NZOrder. -Module NZAddOrderProp - (Import NZ : NZOrdAxiomsSig)(Import NZBase : NZBaseProp NZ). -Include NZMulProp NZ NZBase. -Include NZOrderProp NZ NZBase. +Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig). +Include Type NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ. Local Open Scope NumScope. Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m. @@ -152,8 +150,5 @@ Proof. intros n m H; apply add_le_cases; now nzsimpl. Qed. -End NZAddOrderProp. - -Module NZAddOrderPropFunct (NZ:NZOrdAxiomsSig) := - NZBasePropFunct NZ <+ NZAddOrderProp NZ. +End NZAddOrderPropSig. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 1215bfba2..04955b3b3 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -12,7 +12,7 @@ Require Import NZAxioms. -Module Type NZBaseProp (Import NZ : NZDomainSig). +Module Type NZBasePropSig (Import NZ : NZDomainSig). Local Open Scope NumScope. Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *) @@ -86,9 +86,5 @@ Tactic Notation "nzinduct" ident(n) := Tactic Notation "nzinduct" ident(n) constr(u) := induction_maker n ltac:(apply central_induction with (z := u)). -End NZBaseProp. - -Module NZBasePropFunct (NZ : NZDomainSig). - Include Type NZBaseProp NZ. -End NZBasePropFunct. +End NZBasePropSig. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 5b81cadd2..db64a7963 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -38,9 +38,8 @@ End NZDiv. Module Type NZDivSig := NZOrdAxiomsSig <+ NZDiv. -Module NZDivPropFunct (Import NZ : NZDivSig). - (* TODO: a transformer un jour en arg funct puis include *) - Module Import P := NZMulOrderPropFunct NZ. +Module NZDivPropFunct + (Import NZ : NZDivSig)(Import NZP : NZMulOrderPropSig NZ). (** Uniqueness theorems *) diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 0daca2b87..e7c9b05e0 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -12,8 +12,9 @@ Require Import NZAxioms NZBase NZAdd. -Module NZMulProp (Import NZ : NZAxiomsSig)(Import NZBase : NZBaseProp NZ). -Include NZAddProp NZ NZBase. +Module Type NZMulPropSig + (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ). +Include Type NZAddPropSig NZ NZBase. Local Open Scope NumScope. Theorem mul_0_r : forall n, n * 0 == 0. @@ -67,6 +68,4 @@ Proof. intro n. now nzsimpl. Qed. -End NZMulProp. - -Module NZMulPropFunct (NZ : NZAxiomsSig) := NZBasePropFunct NZ <+ NZMulProp NZ. +End NZMulPropSig. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index b6e4849f5..a4d8a3972 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -13,8 +13,8 @@ Require Import NZAxioms. Require Import NZAddOrder. -Module NZMulOrderPropFunct (Import NZ : NZOrdAxiomsSig). -Include NZAddOrderPropFunct NZ. +Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig). +Include Type NZAddOrderPropSig NZ. Local Open Scope NumScope. Theorem mul_lt_pred : @@ -305,4 +305,4 @@ rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l. apply add_pos_pos; now apply lt_0_1. Qed. -End NZMulOrderPropFunct. +End NZMulOrderPropSig. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index c6815ebf5..a95de8df7 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -12,7 +12,8 @@ Require Import NZAxioms NZBase Decidable OrderTac. -Module NZOrderProp (Import NZ : NZOrdSig)(Import NZBase : NZBaseProp NZ). +Module Type NZOrderPropSig + (Import NZ : NZOrdSig)(Import NZBase : NZBasePropSig NZ). Local Open Scope NumScope. Instance le_wd : Proper (eq==>eq==>iff) le. @@ -613,9 +614,11 @@ Qed. End WF. -End NZOrderProp. +End NZOrderPropSig. -Module NZOrderPropFunct (NZ : NZOrdSig) := NZBasePropFunct NZ <+ NZOrderProp NZ. +Module NZOrderPropFunct (Import NZ : NZOrdSig). + Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ. +End NZOrderPropFunct. (** To Merge with GenericMinMax ... *) diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v index 781d06594..125b4f62c 100644 --- a/theories/Numbers/NatInt/NZProperties.v +++ b/theories/Numbers/NatInt/NZProperties.v @@ -17,4 +17,4 @@ Require Export NZAxioms NZMulOrder. subsumes all others. *) -Module NZPropFunct := NZMulOrderPropFunct. +Module Type NZPropFunct := NZMulOrderPropSig. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 6bf12ee5e..4095fbb50 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -16,7 +16,7 @@ Require Import NZProperties. Module NBasePropFunct (Import N : NAxiomsSig). (** First, we import all known facts about both natural numbers and integers. *) -Include NZPropFunct N. +Include Type NZPropFunct N. Local Open Scope NumScope. (** We prove that the successor of a number is not zero by defining a diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 6c417868a..9e446dc69 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -19,8 +19,7 @@ End NDiv. Module Type NDivSig := NAxiomsSig <+ NDiv. -Module NDivPropFunct (Import N : NDivSig). - Module Import NP := NPropFunct N. +Module NDivPropFunct (Import N : NDivSig)(Import NP : NPropSig N). (** We benefit from what already exists for NZ *) @@ -29,7 +28,7 @@ Module NDivPropFunct (Import N : NDivSig). 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 N'. - Module Import NZDivP := NZDivPropFunct N'. + Module Import NZDivP := NZDivPropFunct N' NP. Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l. diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index 29bda136a..f59d5b1e7 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -15,4 +15,8 @@ Require Export NAxioms NSub. subsumes all others. *) -Module NPropFunct := NSubPropFunct. +Module Type NPropSig := NSubPropFunct. + +Module NPropFunct (N:NAxiomsSig). (* <: NPropSig N. BUG !! *) + Include Type NPropSig N. +End NPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index fee9b4372..7629aa11b 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -16,7 +16,7 @@ and proves its properties *) Require Export NSub. Module NStrongRecPropFunct (Import N : NAxiomsSig). -Include NSubPropFunct N. +Include Type NSubPropFunct N. Local Open Scope NumScope. Section StrongRecursion. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index 62d1c731c..e027c0be2 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -12,7 +12,7 @@ Require Export NMulOrder. -Module NSubPropFunct (Import N : NAxiomsSig). +Module Type NSubPropFunct (Import N : NAxiomsSig). Include NMulOrderPropFunct N. Local Open Scope NumScope. @@ -220,7 +220,7 @@ Qed. Theorem add_dichotomy : forall n m, (exists p, p + n == m) \/ (exists p, p + m == n). -Proof le_alt_dichotomy. +Proof. exact le_alt_dichotomy. Qed. End NSubPropFunct. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 97ac9f872..73affd90d 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -232,4 +232,4 @@ Module NDivMod <: NDivSig. Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. End NDivMod. -Module Export NDivPropMod := NDivPropFunct NDivMod. +Module Export NDivPropMod := NDivPropFunct NDivMod NPeanoPropMod. diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v index 473e25ffb..a7dcb63de 100644 --- a/theories/ZArith/ZOdiv.v +++ b/theories/ZArith/ZOdiv.v @@ -7,10 +7,9 @@ (************************************************************************) -Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing - ZBinary ZDivTrunc Morphisms. +Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms. Require Export ZOdiv_def. -Require Zdiv. +Require Zdiv ZBinary ZDivTrunc. Open Scope Z_scope. @@ -247,7 +246,7 @@ Qed. (** We know enough to prove that [ZOdiv] and [ZOmod] are instances of one of the abstract Euclidean divisions of Numbers. *) -Module ZODiv <: ZDiv ZBinAxiomsMod. +Module ZODiv <: ZDivTrunc.ZDiv ZBinary.ZBinAxiomsMod. Definition div := ZOdiv. Definition modulo := ZOmod. Program Instance div_wd : Proper (eq==>eq==>eq) div. @@ -259,12 +258,12 @@ Module ZODiv <: ZDiv ZBinAxiomsMod. Definition mod_opp_r := fun a b (_:b<>0) => ZOmod_opp_r a b. End ZODiv. -Module ZODivMod := ZBinAxiomsMod <+ ZODiv. +Module ZODivMod := ZBinary.ZBinAxiomsMod <+ ZODiv. (** We hence benefit from generic results about this abstract division. *) Module Z. - Include ZDivPropFunct ZODivMod. + Include ZDivTrunc.ZDivPropFunct ZODivMod ZBinary.ZBinPropMod. End Z. (** * Unicity results *) @@ -434,15 +433,15 @@ Proof. intros. zero_or_not b. apply Z.mod_le; auto with zarith. Qed. Theorem ZOdiv_le_upper_bound: forall a b q, 0 < b -> a <= q*b -> a/b <= q. -Proof. intros a b q; rewrite mul_comm; apply Z.div_le_upper_bound. Qed. +Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_upper_bound. Qed. Theorem ZOdiv_lt_upper_bound: forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q. -Proof. intros a b q; rewrite mul_comm; apply Z.div_lt_upper_bound. Qed. +Proof. intros a b q; rewrite Zmult_comm; apply Z.div_lt_upper_bound. Qed. Theorem ZOdiv_le_lower_bound: forall a b q, 0 < b -> q*b <= a -> q <= a/b. -Proof. intros a b q; rewrite mul_comm; apply Z.div_le_lower_bound. Qed. +Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_lower_bound. Qed. Theorem ZOdiv_sgn: forall a b, 0 <= Zsgn (a/b) * Zsgn a * Zsgn b. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 06aa2b660..a07b6d038 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -319,7 +319,7 @@ Module ZDivMod := ZBinary.ZBinAxiomsMod <+ ZDiv. (** We hence benefit from generic results about this abstract division. *) -Module Z := ZDivFloor.ZDivPropFunct ZDivMod. +Module Z := ZDivFloor.ZDivPropFunct ZDivMod ZBinary.ZBinPropMod. (** Existence theorem *) |