diff options
author | roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-21 11:46:13 +0000 |
---|---|---|
committer | roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-21 11:46:13 +0000 |
commit | bd5b2a45c2ef00d63fc84f5f1bc577fcb3a3d0d9 (patch) | |
tree | 635e016228fd284c8f4165465b728f0c8cc48aa3 | |
parent | f4586d1e8b1116340574d9660117f93e7a1e4e3b (diff) |
Adding: Field instance for Q.
: Power function from Q -> Z -> Q.
: Absolute value function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9901 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend.coq | 64 | ||||
-rw-r--r-- | Makefile | 4 | ||||
-rw-r--r-- | theories/QArith/QArith_base.v | 79 | ||||
-rw-r--r-- | theories/QArith/Qabs.v | 103 | ||||
-rw-r--r-- | theories/QArith/Qfield.v | 131 | ||||
-rw-r--r-- | theories/QArith/Qpower.v | 139 | ||||
-rw-r--r-- | theories/QArith/Qreduction.v | 10 | ||||
-rw-r--r-- | theories/QArith/Qring.v | 95 |
8 files changed, 488 insertions, 137 deletions
diff --git a/.depend.coq b/.depend.coq index 05031eba1..887cd4f73 100644 --- a/.depend.coq +++ b/.depend.coq @@ -13,12 +13,12 @@ theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories theories/FSets/FSetWeakList.vo: theories/FSets/FSetWeakList.v theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakFacts.vo: theories/FSets/FSetWeakFacts.v theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakFacts.vo theories/FSets/FSetWeakProperties.vo theories/FSets/FSetWeakList.vo -theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/FSets/FSetInterface.vo +theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/Bool/Bool.vo theories/FSets/OrderedType.vo theories/FSets/FMapList.vo: theories/FSets/FMapList.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMaps.vo: theories/FSets/FMaps.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FMapPositive.vo theories/FSets/FMapIntMap.vo theories/FSets/FMapFacts.vo theories/FSets/FMapFacts.vo: theories/FSets/FMapFacts.v theories/Bool/Bool.vo theories/FSets/OrderedType.vo theories/FSets/FMapInterface.vo theories/FSets/FMapWeakFacts.vo: theories/FSets/FMapWeakFacts.v theories/Bool/Bool.vo theories/FSets/OrderedType.vo theories/FSets/FMapWeakInterface.vo -theories/FSets/FMapWeakInterface.vo: theories/FSets/FMapWeakInterface.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo +theories/FSets/FMapWeakInterface.vo: theories/FSets/FMapWeakInterface.v theories/Bool/Bool.vo theories/Logic/DecidableType.vo theories/FSets/FMapWeakList.vo: theories/FSets/FMapWeakList.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeak.vo: theories/FSets/FMapWeak.v theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo theories/FSets/FMapWeakFacts.vo theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo @@ -234,12 +234,12 @@ theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories theories/FSets/FSetWeakList.vo: theories/FSets/FSetWeakList.v theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakFacts.vo: theories/FSets/FSetWeakFacts.v theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakFacts.vo theories/FSets/FSetWeakProperties.vo theories/FSets/FSetWeakList.vo -theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/FSets/FSetInterface.vo +theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/Bool/Bool.vo theories/FSets/OrderedType.vo theories/FSets/FMapList.vo: theories/FSets/FMapList.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMaps.vo: theories/FSets/FMaps.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FMapPositive.vo theories/FSets/FMapIntMap.vo theories/FSets/FMapFacts.vo theories/FSets/FMapFacts.vo: theories/FSets/FMapFacts.v theories/Bool/Bool.vo theories/FSets/OrderedType.vo theories/FSets/FMapInterface.vo theories/FSets/FMapWeakFacts.vo: theories/FSets/FMapWeakFacts.v theories/Bool/Bool.vo theories/FSets/OrderedType.vo theories/FSets/FMapWeakInterface.vo -theories/FSets/FMapWeakInterface.vo: theories/FSets/FMapWeakInterface.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo +theories/FSets/FMapWeakInterface.vo: theories/FSets/FMapWeakInterface.v theories/Bool/Bool.vo theories/Logic/DecidableType.vo theories/FSets/FMapWeakList.vo: theories/FSets/FMapWeakList.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeak.vo: theories/FSets/FMapWeak.v theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo theories/FSets/FMapWeakFacts.vo theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo @@ -282,6 +282,54 @@ theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contri theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo theories/Reals/Rpow_def.vo: theories/Reals/Rpow_def.v theories/Reals/Rdefinitions.vo +theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo +theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo +theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo +theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo +theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo +theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/ArithRing.vo +theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo +theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo +theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo +theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo +theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplete.vo theories/Arith/Max.vo +theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/Binomial.vo: theories/Reals/Binomial.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo +theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binomial.vo +theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Arith/Max.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo +theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo +theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo +theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo +theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo +theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo +theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo +theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo +theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo +theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo +theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo +theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo +theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo +theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo +theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo +theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo +theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo +theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo +theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo +theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo +theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo +theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo +theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo +theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo +theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Arith/Arith.vo theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo @@ -289,10 +337,13 @@ theories/Sorting/PermutSetoid.vo: theories/Sorting/PermutSetoid.v contrib/omega/ theories/Sorting/PermutEq.vo: theories/Sorting/PermutEq.v contrib/omega/Omega.vo theories/Relations/Relations.vo theories/Setoids/Setoid.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/QArith/QArith_base.vo: theories/QArith/QArith_base.v theories/ZArith/ZArith.vo contrib/setoid_ring/ZArithRing.vo theories/Setoids/Setoid.vo theories/QArith/Qreduction.vo: theories/QArith/Qreduction.v theories/QArith/QArith_base.vo theories/ZArith/Znumtheory.vo -theories/QArith/Qring.vo: theories/QArith/Qring.v contrib/setoid_ring/Ring.vo theories/QArith/QArith_base.vo +theories/QArith/Qring.vo: theories/QArith/Qring.v theories/QArith/Qfield.vo theories/QArith/Qreals.vo: theories/QArith/Qreals.v theories/Reals/Rbase.vo theories/QArith/QArith_base.vo theories/QArith/QArith.vo: theories/QArith/QArith.v theories/QArith/QArith_base.vo theories/QArith/Qring.vo theories/QArith/Qreduction.vo theories/QArith/Qcanon.vo: theories/QArith/Qcanon.v contrib/setoid_ring/Field.vo theories/QArith/QArith.vo theories/ZArith/Znumtheory.vo theories/Logic/Eqdep_dec.vo +theories/QArith/Qfield.vo: theories/QArith/Qfield.v contrib/setoid_ring/Field.vo theories/QArith/QArith_base.vo contrib/setoid_ring/NArithRing.vo +theories/QArith/Qpower.vo: theories/QArith/Qpower.v theories/QArith/Qfield.vo +theories/QArith/Qabs.vo: theories/QArith/Qabs.v theories/QArith/QArith.vo theories/QArith/Qreduction.vo theories/Ints/Z/IntsZmisc.vo: theories/Ints/Z/IntsZmisc.v theories/ZArith/ZArith.vo theories/Ints/Z/Pmod.vo: theories/Ints/Z/Pmod.v theories/Ints/Z/IntsZmisc.vo theories/ZArith/Zwf.vo theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo theories/Ints/Tactic.vo: theories/Ints/Tactic.v @@ -340,7 +391,8 @@ contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/LegacyFi contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo contrib/subtac/SubtacTactics.vo: contrib/subtac/SubtacTactics.v theories/Logic/Eqdep.vo -contrib/subtac/Utils.vo: contrib/subtac/Utils.v contrib/subtac/SubtacTactics.vo theories/Bool/Sumbool.vo theories/Logic/ProofIrrelevance.vo +contrib/subtac/Heq.vo: contrib/subtac/Heq.v theories/Logic/JMeq.vo +contrib/subtac/Utils.vo: contrib/subtac/Utils.v contrib/subtac/SubtacTactics.vo theories/Bool/Sumbool.vo theories/Logic/ProofIrrelevance.vo contrib/subtac/Heq.vo contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo contrib/subtac/Utils.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo contrib/subtac/Subtac.vo: contrib/subtac/Subtac.v contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/FunctionalExtensionality.vo: contrib/subtac/FunctionalExtensionality.v contrib/subtac/Utils.vo contrib/subtac/FixSub.vo @@ -930,7 +930,9 @@ INTSVO=\ QARITHVO=\ theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \ theories/QArith/Qring.vo theories/QArith/Qreals.vo \ - theories/QArith/QArith.vo theories/QArith/Qcanon.vo + theories/QArith/QArith.vo theories/QArith/Qcanon.vo \ + theories/QArith/Qfield.vo theories/QArith/Qpower.vo \ + theories/QArith/Qabs.vo LISTSVO=\ theories/Lists/MonoList.vo \ diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index f919398f0..198fedd55 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -165,6 +165,13 @@ Infix "/" := Qdiv : Q_scope. Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope. +Lemma Qmake_Qdiv : forall a b, a#b==inject_Z a/inject_Z ('b). +Proof. +intros a b. +unfold Qeq. +simpl. +ring. +Qed. (** * Setoid compatibility results *) @@ -416,6 +423,11 @@ Qed. (** * Inverse and division. *) +Lemma Qinv_involutive : forall q, (/ / q) == q. +Proof. +intros [[|n|n] d]; red; simpl; reflexivity. +Qed. + Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1. Proof. intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl; @@ -641,50 +653,45 @@ Proof. Close Scope Z_scope. Qed. -(** * Rational to the n-th power *) - -Fixpoint Qpower (q:Q)(n:nat) { struct n } : Q := - match n with - | O => 1 - | S n => q * (Qpower q n) - end. - -Notation " q ^ n " := (Qpower q n) : Q_scope. - -Lemma Qpower_1 : forall n, 1^n == 1. +Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b. Proof. - induction n; simpl; auto with qarith. - rewrite IHn; auto with qarith. +intros a b Ha Hb. +unfold Qle in *. +simpl in *. +auto with *. Qed. -Lemma Qpower_0 : forall n, n<>O -> 0^n == 0. +Lemma Qinv_le_0_compat : forall a, 0 <= a -> 0 <= /a. Proof. - destruct n; simpl. - destruct 1; auto. - intros. - compute; auto. +intros [[|n|n] d] Ha; assumption. Qed. -Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n. -Proof. - induction n; simpl; auto with qarith. - intros; compute; intro; discriminate. - intros. - apply Qle_trans with (0*(p^n)). - compute; intro; discriminate. - apply Qmult_le_compat_r; auto. -Qed. +(** * Rational to the n-th power *) + +Definition Qpower_positive (q:Q)(p:positive) : Q := + pow_pos Qmult q p. -Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n. +Add Morphism Qpower_positive with signature Qeq ==> eq ==> Qeq as Qpower_positive_comp. Proof. - induction n. - compute; auto. - simpl. - intros; rewrite IHn; clear IHn. - unfold Qdiv; rewrite Qinv_mult_distr. - setoid_replace (1#p) with (/ inject_Z ('p)). - apply Qeq_refl. - compute; auto. +intros x1 x2 Hx y. +unfold Qpower_positive. +induction y; simpl; +try rewrite IHy; +try rewrite Hx; +reflexivity. Qed. +Definition Qpower (q:Q) (z:Z) := + match z with + | Zpos p => Qpower_positive q p + | Z0 => 1 + | Zneg p => /Qpower_positive q p + end. + +Notation " q ^ z " := (Qpower q z) : Q_scope. +Add Morphism Qpower with signature Qeq ==> eq ==> Qeq as Qpower_comp. +Proof. +intros x1 x2 Hx [|y|y]; try reflexivity; +simpl; rewrite Hx; reflexivity. +Qed. diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v new file mode 100644 index 000000000..511463ee7 --- /dev/null +++ b/theories/QArith/Qabs.v @@ -0,0 +1,103 @@ +Require Export QArith. +Require Export Qreduction. + +Hint Resolve Qlt_le_weak : qarith. + +Definition Qabs (x:Q) := let (n,d):=x in (Zabs n#d). + +Lemma Qabs_case : forall (x:Q) (P : Q -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x). +Proof. +intros x P H1 H2. +destruct x as [[|xn|xn] xd]; +[apply H1|apply H1|apply H2]; +abstract (compute; discriminate). +Defined. + +Add Morphism Qabs with signature Qeq ==> Qeq as Qabs_wd. +intros [xn xd] [yn yd] H. +simpl. +unfold Qeq in *. +simpl in *. +change (' yd)%Z with (Zabs (' yd)). +change (' xd)%Z with (Zabs (' xd)). +repeat rewrite <- Zabs_Zmult. +congruence. +Qed. + +Lemma Qabs_pos : forall x, 0 <= x -> Qabs x == x. +Proof. +intros x H. +apply Qabs_case. +reflexivity. +intros H0. +setoid_replace x with 0. +reflexivity. +apply Qle_antisym; assumption. +Qed. + +Lemma Qabs_neg : forall x, x <= 0 -> Qabs x == - x. +Proof. +intros x H. +apply Qabs_case. +intros H0. +setoid_replace x with 0. +reflexivity. +apply Qle_antisym; assumption. +reflexivity. +Qed. + +Lemma Qabs_nonneg : forall x, 0 <= (Qabs x). +intros x. +apply Qabs_case. +auto. +apply (Qopp_le_compat x 0). +Qed. + +Lemma Zabs_Qabs : forall n d, (Zabs n#d)==Qabs (n#d). +Proof. +intros [|n|n]; reflexivity. +Qed. + +Lemma Qabs_opp : forall x, Qabs (-x) == Qabs x. +Proof. +intros x. +do 2 apply Qabs_case; try (intros; ring); +(intros H0 H1; +setoid_replace x with 0;[reflexivity|]; +apply Qle_antisym);try assumption; +rewrite Qle_minus_iff in *; +ring_simplify; +ring_simplify in H1; +assumption. +Qed. + +Lemma Qabs_triangle : forall x y, Qabs (x+y) <= Qabs x + Qabs y. +Proof. +intros [xn xd] [yn yd]. +unfold Qplus. +unfold Qle. +simpl. +apply Zmult_le_compat_r;auto with *. +change (' yd)%Z with (Zabs (' yd)). +change (' xd)%Z with (Zabs (' xd)). +repeat rewrite <- Zabs_Zmult. +apply Zabs_triangle. +Qed. + +Lemma Qabs_triangle_reverse : forall x y, Qabs x - Qabs y <= Qabs (x - y). +Proof. +intros x y. +rewrite Qle_minus_iff. +setoid_replace (Qabs (x - y) + - (Qabs x - Qabs y)) with ((Qabs (x - y) + Qabs y) + - Qabs x) by ring. +rewrite <- Qle_minus_iff. +setoid_replace (Qabs x) with (Qabs (x-y+y)). +apply Qabs_triangle. +apply Qabs_wd. +ring. +Qed. + +Definition Qminus' x y := Qred (Qminus x y). +Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q). +Proof. + intros; unfold Qminus' in |- *; apply Qred_correct; auto. +Qed. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v new file mode 100644 index 000000000..3b14a47ce --- /dev/null +++ b/theories/QArith/Qfield.v @@ -0,0 +1,131 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Qring.v 9427 2006-12-11 18:46:35Z bgregoir $ i*) + +Require Export Field. +Require Export QArith_base. +Require Import NArithRing. + +(** * A ring tactic for rational numbers *) + +Definition Qeq_bool (x y : Q) := + if Qeq_dec x y then true else false. + +Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y. +Proof. + intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto. + intros _ H; inversion H. +Qed. + +Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq. +Proof. + constructor. + constructor. + exact Qplus_0_l. + exact Qplus_comm. + exact Qplus_assoc. + exact Qmult_1_l. + exact Qmult_comm. + exact Qmult_assoc. + exact Qmult_plus_distr_l. + reflexivity. + exact Qplus_opp_r. + discriminate. + reflexivity. + intros p Hp. + rewrite Qmult_comm. + apply Qmult_inv_r. + exact Hp. +Qed. + +Lemma Qpower_theory : power_theory 1 Qmult Qeq Z_of_N Qpower. +Proof. +constructor. +intros r [|n]; +reflexivity. +Qed. + +Ltac isQcst t := + match t with + | inject_Z ?z => isZcst z + | Qmake ?n ?d => + match isZcst n with + true => isPcst d + | _ => false + end + | _ => false + end. + +Ltac Qcst t := + match isQcst t with + true => t + | _ => NotConstant + end. + +Ltac Qpow_tac t := + match t with + | Z_of_N ?n => Ncst n + | NtoZ ?n => Ncst n + | _ => NotConstant + end. + +Add Field Qfield : Qsft(decidable Qeq_bool_correct, constants [Qcst], power_tac Qpower_theory [Qpow_tac]). +(** Exemple of use: *) + +Section Examples. + +Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). + intros. + ring. +Qed. + +Let ex2 : forall x y : Q, x+y == y+x. + intros. + ring. +Qed. + +Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z). + intros. + ring. +Qed. + +Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2). + ring. +Qed. + +Let ex5 : 1+1 == 2#1. + ring. +Qed. + +Let ex6 : (1#1)+(1#1) == 2#1. + ring. +Qed. + +Let ex7 : forall x : Q, x-x== 0#1. + intro. + ring. +Qed. + +Example test_field : forall x y : Q, ~(y==0) -> (x/y)*y == x. +intros. +field. +auto. +Qed. + +End Examples. + +Lemma Qopp_plus : forall a b, -(a+b) == -a + -b. +Proof. + intros; ring. +Qed. + +Lemma Qopp_opp : forall q, - -q==q. +Proof. + intros; ring. +Qed. diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v new file mode 100644 index 000000000..d50443498 --- /dev/null +++ b/theories/QArith/Qpower.v @@ -0,0 +1,139 @@ +Require Import Qfield. + +Lemma Qpower_positive_1 : forall n, Qpower_positive 1 n == 1. +Proof. +induction n; +simpl; try rewrite IHn; reflexivity. +Qed. + +Lemma Qpower_1 : forall n, 1^n == 1. +Proof. + intros [|n|n]; simpl; try rewrite Qpower_positive_1; reflexivity. +Qed. + +Lemma Qpower_positive_0 : forall n, Qpower_positive 0 n == 0. +Proof. +induction n; +simpl; try rewrite IHn; reflexivity. +Qed. + +Lemma Qpower_0 : forall n, (n<>0)%Z -> 0^n == 0. +Proof. + intros [|n|n] Hn; try (elim Hn; reflexivity); simpl; + rewrite Qpower_positive_0; reflexivity. +Qed. + +Lemma Qpower_not_0_positive : forall a n, ~a==0 -> ~Qpower_positive a n == 0. +Proof. +intros a n X H. +apply X; clear X. +induction n; simpl in *; try assumption; +destruct (Qmult_integral _ _ H); +try destruct (Qmult_integral _ _ H0); auto. +Qed. + +Lemma Qpower_pos_positive : forall p n, 0 <= p -> 0 <= Qpower_positive p n. +intros p n Hp. +induction n; simpl; repeat apply Qmult_le_0_compat;assumption. +Qed. + +Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n. +Proof. + intros p [|n|n] Hp; simpl; try discriminate; + try apply Qinv_le_0_compat; apply Qpower_pos_positive; assumption. +Qed. + +Lemma Qmult_power_positive : forall a b n, Qpower_positive (a*b) n == (Qpower_positive a n)*(Qpower_positive b n). +Proof. +induction n; +simpl; repeat rewrite IHn; ring. +Qed. + +Lemma Qmult_power : forall a b n, (a*b)^n == a^n*b^n. +Proof. + intros a b [|n|n]; simpl; + try rewrite Qmult_power_positive; + try rewrite Qinv_mult_distr; + reflexivity. +Qed. + +Lemma Qinv_power_positive : forall a n, Qpower_positive (/a) n == /(Qpower_positive a n). +Proof. +induction n; +simpl; repeat (rewrite IHn || rewrite Qinv_mult_distr); reflexivity. +Qed. + +Lemma Qinv_power : forall a n, (/a)^n == /a^n. +Proof. + intros a [|n|n]; simpl; + try rewrite Qinv_power_positive; + reflexivity. +Qed. + +Lemma Qdiv_power : forall a b n, (a/b)^n == (a^n/b^n). +Proof. +unfold Qdiv. +intros a b n. +rewrite Qmult_power. +rewrite Qinv_power. +reflexivity. +Qed. + +Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n. +Proof. +intros n p. +rewrite Qmake_Qdiv. +rewrite Qdiv_power. +rewrite Qpower_1. +unfold Qdiv. +ring. +Qed. + +Lemma Qpower_plus_positive : forall a n m, Qpower_positive a (n+m) == (Qpower_positive a n)*(Qpower_positive a m). +Proof. +intros a n m. +unfold Qpower_positive. +apply pow_pos_Pplus. +apply Q_Setoid. +apply Qmult_comp. +apply Qmult_comm. +apply Qmult_assoc. +Qed. + +Lemma Qpower_opp : forall a n, a^(-n) == /a^n. +Proof. +intros a [|n|n]; simpl; try reflexivity. +symmetry; apply Qinv_involutive. +Qed. + +Lemma Qpower_minus_positive : forall a (n m:positive), (Pcompare n m Eq=Gt)%positive -> Qpower_positive a (n-m)%positive == (Qpower_positive a n)/(Qpower_positive a m). +Proof. +intros a n m H. +destruct (Qeq_dec a 0). + rewrite q. + repeat rewrite Qpower_positive_0. + reflexivity. +rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)). + apply Qpower_not_0_positive; assumption. +apply Qdiv_comp;[|reflexivity]. +rewrite Qmult_comm. +rewrite <- Qpower_plus_positive. +rewrite Pplus_minus. +reflexivity. +assumption. +Qed. + +Lemma Qpower_plus : forall a n m, ~a==0 -> a^(n+m) == a^n*a^m. +Proof. +intros a [|n|n] [|m|m] H; simpl; try ring; +try rewrite Qpower_plus_positive; +try apply Qinv_mult_distr; try reflexivity; +case_eq ((n ?= m)%positive Eq); intros H0; simpl; + try rewrite Qpower_minus_positive; + try rewrite (Pcompare_Eq_eq _ _ H0); + try (field; try split; apply Qpower_not_0_positive); + try assumption; + apply ZC2; + assumption. +Qed. + diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 7ca07f841..ddd9b0a26 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -145,6 +145,7 @@ Qed. Definition Qplus' (p q : Q) := Qred (Qplus p q). Definition Qmult' (p q : Q) := Qred (Qmult p q). +Definition Qminus' x y := Qred (Qminus x y). Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q). Proof. @@ -156,6 +157,11 @@ Proof. intros; unfold Qmult' in |- *; apply Qred_correct; auto. Qed. +Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q). +Proof. + intros; unfold Qminus' in |- *; apply Qred_correct; auto. +Qed. + Add Morphism Qplus' : Qplus'_comp. Proof. intros; unfold Qplus' in |- *. @@ -167,3 +173,7 @@ Add Morphism Qmult' : Qmult'_comp. rewrite H; rewrite H0; auto with qarith. Qed. +Add Morphism Qminus' : Qminus'_comp. + intros; unfold Qminus' in |- *. + rewrite H; rewrite H0; auto with qarith. +Qed. diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v index 609e82b07..8c9e2dfa3 100644 --- a/theories/QArith/Qring.v +++ b/theories/QArith/Qring.v @@ -8,97 +8,4 @@ (*i $Id$ i*) -Require Export Ring. -Require Export QArith_base. - -(** * A ring tactic for rational numbers *) - -Definition Qeq_bool (x y : Q) := - if Qeq_dec x y then true else false. - -Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y. -Proof. - intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto. - intros _ H; inversion H. -Qed. - -Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq. -Proof. - constructor. - exact Qplus_0_l. - exact Qplus_comm. - exact Qplus_assoc. - exact Qmult_1_l. - exact Qmult_comm. - exact Qmult_assoc. - exact Qmult_plus_distr_l. - reflexivity. - exact Qplus_opp_r. -Qed. - -Ltac isQcst t := - match t with - | inject_Z ?z => isZcst z - | Qmake ?n ?d => - match isZcst n with - true => isPcst d - | _ => false - end - | _ => false - end. - -Ltac Qcst t := - match isQcst t with - true => t - | _ => NotConstant - end. - -Add Ring Qring : Qsrt (decidable Qeq_bool_correct, constants [Qcst]). -(** Exemple of use: *) - -Section Examples. - -Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). - intros. - ring. -Qed. - -Let ex2 : forall x y : Q, x+y == y+x. - intros. - ring. -Qed. - -Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z). - intros. - ring. -Qed. - -Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2). - ring. -Qed. - -Let ex5 : 1+1 == 2#1. - ring. -Qed. - -Let ex6 : (1#1)+(1#1) == 2#1. - ring. -Qed. - -Let ex7 : forall x : Q, x-x== 0#1. - intro. - ring. -Qed. - -End Examples. - -Lemma Qopp_plus : forall a b, -(a+b) == -a + -b. -Proof. - intros; ring. -Qed. - -Lemma Qopp_opp : forall q, - -q==q. -Proof. - intros; ring. -Qed. - +Require Export Qfield. |