From ca13fb40562c9d664aa4f363755eab6e5f2eeaa5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 9 Jun 2006 14:08:38 +0000 Subject: Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend.coq | 77 +++++-- Makefile | 9 +- theories/FSets/DecidableType.v | 156 -------------- theories/FSets/DecidableTypeEx.v | 50 ----- theories/FSets/Int.v | 421 -------------------------------------- theories/Logic/ClassicalEpsilon.v | 24 ++- theories/Logic/DecidableType.v | 156 ++++++++++++++ theories/Logic/DecidableTypeEx.v | 50 +++++ theories/ZArith/Int.v | 421 ++++++++++++++++++++++++++++++++++++++ 9 files changed, 707 insertions(+), 657 deletions(-) delete mode 100644 theories/FSets/DecidableType.v delete mode 100644 theories/FSets/DecidableTypeEx.v delete mode 100644 theories/FSets/Int.v create mode 100644 theories/Logic/DecidableType.v create mode 100644 theories/Logic/DecidableTypeEx.v create mode 100644 theories/ZArith/Int.v diff --git a/.depend.coq b/.depend.coq index 658d38a6fc..949cc501cb 100644 --- a/.depend.coq +++ b/.depend.coq @@ -1,5 +1,3 @@ -theories/FSets/DecidableType.vo: theories/FSets/DecidableType.v theories/Lists/SetoidList.vo -theories/FSets/DecidableTypeEx.vo: theories/FSets/DecidableTypeEx.v theories/FSets/DecidableType.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedType.vo: theories/FSets/OrderedType.v theories/Lists/SetoidList.vo theories/FSets/OrderedTypeEx.vo: theories/FSets/OrderedTypeEx.v theories/FSets/OrderedType.vo theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/NArith/NArith.vo theories/NArith/Ndec.vo theories/Arith/Compare_dec.vo theories/FSets/OrderedTypeAlt.vo: theories/FSets/OrderedTypeAlt.v theories/FSets/OrderedType.vo @@ -11,10 +9,10 @@ theories/FSets/FSetProperties.vo: theories/FSets/FSetProperties.v theories/FSets theories/FSets/FSetEqProperties.vo: theories/FSets/FSetEqProperties.v theories/FSets/FSetProperties.vo theories/Bool/Zerob.vo theories/Bool/Sumbool.vo contrib/omega/Omega.vo theories/FSets/FSets.vo: theories/FSets/FSets.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FSetInterface.vo theories/FSets/FSetBridge.vo theories/FSets/FSetProperties.vo theories/FSets/FSetEqProperties.vo theories/FSets/FSetList.vo theories/FSets/FSetWeakProperties.vo: theories/FSets/FSetWeakProperties.v theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakFacts.vo -theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories/Bool/Bool.vo theories/FSets/DecidableType.vo +theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories/Bool/Bool.vo theories/Logic/DecidableType.vo 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/FSets/DecidableType.vo theories/FSets/DecidableTypeEx.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetProperties.vo theories/FSets/FSetWeakList.vo +theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetProperties.vo theories/FSets/FSetWeakList.vo theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/FSets/FSetInterface.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 @@ -22,13 +20,12 @@ theories/FSets/FMapFacts.vo: theories/FSets/FMapFacts.v theories/Bool/Bool.vo th 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/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/FSets/DecidableType.vo theories/FSets/DecidableTypeEx.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo theories/FSets/FMapWeakFacts.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/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/FMapInterface.vo theories/FSets/FMapIntMap.vo: theories/FSets/FMapIntMap.v theories/Bool/Bool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Allmaps.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FSetToFiniteSet.vo: theories/FSets/FSetToFiniteSet.v theories/Sets/Ensembles.vo theories/Sets/Finite_sets.vo theories/FSets/FSetInterface.vo theories/FSets/FSetProperties.vo theories/FSets/OrderedTypeEx.vo -theories/FSets/Int.vo: theories/FSets/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo -theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo -theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo +theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/ZArith/Int.vo +theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/ZArith/Int.vo theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rdefinitions.vo theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo @@ -122,6 +119,8 @@ theories/Logic/EqdepFacts.vo: theories/Logic/EqdepFacts.v theories/Logic/ProofIrrelevanceFacts.vo: theories/Logic/ProofIrrelevanceFacts.v theories/Logic/EqdepFacts.vo theories/Logic/ClassicalEpsilon.vo: theories/Logic/ClassicalEpsilon.v theories/Logic/Classical.vo theories/Logic/ChoiceFacts.vo theories/Logic/ClassicalUniqueChoice.vo: theories/Logic/ClassicalUniqueChoice.v theories/Logic/Classical.vo theories/Setoids/Setoid.vo +theories/Logic/DecidableType.vo: theories/Logic/DecidableType.v theories/Lists/SetoidList.vo +theories/Logic/DecidableTypeEx.vo: theories/Logic/DecidableTypeEx.v theories/Logic/DecidableType.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Factorial.vo theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo @@ -182,6 +181,7 @@ theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v theories/NArith/Bi theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/BinInt.vo theories/ZArith/Zeven.vo theories/ZArith/Zorder.vo theories/ZArith/Zcompare.vo theories/ZArith/ZArith_dec.vo theories/Bool/Sumbool.vo theories/ZArith/Zbinary.vo: theories/ZArith/Zbinary.v theories/Bool/Bvector.vo theories/ZArith/ZArith.vo theories/ZArith/Zpower.vo contrib/omega/Omega.vo theories/ZArith/Znumtheory.vo: theories/ZArith/Znumtheory.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zdiv.vo +theories/ZArith/Int.vo: theories/ZArith/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v theories/Relations/Relation_Definitions.vo theories/Lists/MonoList.vo: theories/Lists/MonoList.v theories/Arith/Le.vo theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/List.vo @@ -213,8 +213,6 @@ theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theo theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo -theories/FSets/DecidableType.vo: theories/FSets/DecidableType.v theories/Lists/SetoidList.vo -theories/FSets/DecidableTypeEx.vo: theories/FSets/DecidableTypeEx.v theories/FSets/DecidableType.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedType.vo: theories/FSets/OrderedType.v theories/Lists/SetoidList.vo theories/FSets/OrderedTypeEx.vo: theories/FSets/OrderedTypeEx.v theories/FSets/OrderedType.vo theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/NArith/NArith.vo theories/NArith/Ndec.vo theories/Arith/Compare_dec.vo theories/FSets/OrderedTypeAlt.vo: theories/FSets/OrderedTypeAlt.v theories/FSets/OrderedType.vo @@ -226,10 +224,10 @@ theories/FSets/FSetProperties.vo: theories/FSets/FSetProperties.v theories/FSets theories/FSets/FSetEqProperties.vo: theories/FSets/FSetEqProperties.v theories/FSets/FSetProperties.vo theories/Bool/Zerob.vo theories/Bool/Sumbool.vo contrib/omega/Omega.vo theories/FSets/FSets.vo: theories/FSets/FSets.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FSetInterface.vo theories/FSets/FSetBridge.vo theories/FSets/FSetProperties.vo theories/FSets/FSetEqProperties.vo theories/FSets/FSetList.vo theories/FSets/FSetWeakProperties.vo: theories/FSets/FSetWeakProperties.v theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakFacts.vo -theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories/Bool/Bool.vo theories/FSets/DecidableType.vo +theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories/Bool/Bool.vo theories/Logic/DecidableType.vo 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/FSets/DecidableType.vo theories/FSets/DecidableTypeEx.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetProperties.vo theories/FSets/FSetWeakList.vo +theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetProperties.vo theories/FSets/FSetWeakList.vo theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/FSets/FSetInterface.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 @@ -237,13 +235,12 @@ theories/FSets/FMapFacts.vo: theories/FSets/FMapFacts.v theories/Bool/Bool.vo th 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/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/FSets/DecidableType.vo theories/FSets/DecidableTypeEx.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo theories/FSets/FMapWeakFacts.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/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/FMapInterface.vo theories/FSets/FMapIntMap.vo: theories/FSets/FMapIntMap.v theories/Bool/Bool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Allmaps.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FSetToFiniteSet.vo: theories/FSets/FSetToFiniteSet.v theories/Sets/Ensembles.vo theories/Sets/Finite_sets.vo theories/FSets/FSetInterface.vo theories/FSets/FSetProperties.vo theories/FSets/OrderedTypeEx.vo -theories/FSets/Int.vo: theories/FSets/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo -theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo -theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo +theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/ZArith/Int.vo +theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/ZArith/Int.vo theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/List.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/List.vo @@ -277,6 +274,54 @@ theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base. theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo 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/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 +theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rbase.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 diff --git a/Makefile b/Makefile index 01038273f9..0d8c0745ac 100644 --- a/Makefile +++ b/Makefile @@ -823,7 +823,8 @@ LOGICVO=\ theories/Logic/ClassicalChoice.vo theories/Logic/ClassicalDescription.vo \ theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo \ theories/Logic/EqdepFacts.vo theories/Logic/ProofIrrelevanceFacts.vo \ - theories/Logic/ClassicalEpsilon.vo theories/Logic/ClassicalUniqueChoice.vo + theories/Logic/ClassicalEpsilon.vo theories/Logic/ClassicalUniqueChoice.vo \ + theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo ARITHVO=\ theories/Arith/Arith.vo theories/Arith/Gt.vo \ @@ -868,7 +869,7 @@ ZARITHVO=\ theories/ZArith/Zdiv.vo theories/ZArith/Zsqrt.vo \ theories/ZArith/Zwf.vo theories/ZArith/ZArith_base.vo \ theories/ZArith/Zbool.vo theories/ZArith/Zbinary.vo \ - theories/ZArith/Znumtheory.vo + theories/ZArith/Znumtheory.vo theories/ZArith/Int.vo QARITHVO=\ theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \ @@ -898,7 +899,6 @@ SETSVO=\ theories/Sets/Partial_Order.vo theories/Sets/Uniset.vo FSETSBASEVO=\ - theories/FSets/DecidableType.vo theories/FSets/DecidableTypeEx.vo \ theories/FSets/OrderedType.vo \ theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo \ theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo \ @@ -912,8 +912,7 @@ FSETSBASEVO=\ theories/FSets/FMapWeakFacts.vo \ theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo \ theories/FSets/FMapWeak.vo theories/FSets/FMapPositive.vo \ - theories/FSets/FMapIntMap.vo theories/FSets/FSetToFiniteSet.vo \ - theories/FSets/Int.vo \ + theories/FSets/FMapIntMap.vo theories/FSets/FSetToFiniteSet.vo FSETS_basic= diff --git a/theories/FSets/DecidableType.v b/theories/FSets/DecidableType.v deleted file mode 100644 index a4de6ca7fe..0000000000 --- a/theories/FSets/DecidableType.v +++ /dev/null @@ -1,156 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t -> Prop. - - Axiom eq_refl : forall x : t, eq x x. - Axiom eq_sym : forall x y : t, eq x y -> eq y x. - Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - - Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. - - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans. - -End DecidableType. - -(** * Additional notions about keys and datas used in FMap *) - -Module KeyDecidableType(D:DecidableType). - Import D. - - Section Elt. - Variable elt : Set. - Notation key:=t. - - Definition eqk (p p':key*elt) := eq (fst p) (fst p'). - Definition eqke (p p':key*elt) := - eq (fst p) (fst p') /\ (snd p) = (snd p'). - - Hint Unfold eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. - - (* eqke is stricter than eqk *) - - Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'. - Proof. - unfold eqk, eqke; intuition. - Qed. - - (* eqk, eqke are equalities *) - - Lemma eqk_refl : forall e, eqk e e. - Proof. auto. Qed. - - Lemma eqke_refl : forall e, eqke e e. - Proof. auto. Qed. - - Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. - Proof. auto. Qed. - - Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. - Proof. unfold eqke; intuition. Qed. - - Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. - Proof. eauto. Qed. - - Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. - Proof. - unfold eqke; intuition; [ eauto | congruence ]. - Qed. - - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Immediate eqk_sym eqke_sym. - - Lemma InA_eqke_eqk : - forall x m, InA eqke x m -> InA eqk x m. - Proof. - unfold eqke; induction 1; intuition. - Qed. - Hint Resolve InA_eqke_eqk. - - Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. - Proof. - intros; apply InA_eqA with p; auto; apply eqk_trans; auto. - Qed. - - Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). - Definition In k m := exists e:elt, MapsTo k e m. - - Hint Unfold MapsTo In. - - (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) - - Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. - Proof. - firstorder. - exists x; auto. - induction H. - destruct y. - exists e; auto. - destruct IHInA as [e H0]. - exists e; auto. - Qed. - - Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. - Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto. - Qed. - - Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. - Proof. - destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto. - Qed. - - Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. - Proof. - inversion 1. - inversion_clear H0; eauto. - destruct H1; simpl in *; intuition. - Qed. - - Lemma In_inv_2 : forall k k' e e' l, - InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. - Proof. - inversion_clear 1; compute in H0; intuition. - Qed. - - Lemma In_inv_3 : forall x x' l, - InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. - Proof. - inversion_clear 1; compute in H0; intuition. - Qed. - - End Elt. - - Hint Unfold eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Immediate eqk_sym eqke_sym. - Hint Resolve InA_eqke_eqk. - Hint Unfold MapsTo In. - Hint Resolve In_inv_2 In_inv_3. - -End KeyDecidableType. - - - - - diff --git a/theories/FSets/DecidableTypeEx.v b/theories/FSets/DecidableTypeEx.v deleted file mode 100644 index dcca370953..0000000000 --- a/theories/FSets/DecidableTypeEx.v +++ /dev/null @@ -1,50 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Z. - Arguments Scope i2z [ Int_scope ]. - - Parameter _0 : int. - Parameter _1 : int. - Parameter _2 : int. - Parameter _3 : int. - Parameter plus : int -> int -> int. - Parameter opp : int -> int. - Parameter minus : int -> int -> int. - Parameter mult : int -> int -> int. - Parameter max : int -> int -> int. - - Notation "0" := _0 : Int_scope. - Notation "1" := _1 : Int_scope. - Notation "2" := _2 : Int_scope. - Notation "3" := _3 : Int_scope. - Infix "+" := plus : Int_scope. - Infix "-" := minus : Int_scope. - Infix "*" := mult : Int_scope. - Notation "- x" := (opp x) : Int_scope. - -(** For logical relations, we can rely on their counterparts in Z, - since they don't appear after extraction. Moreover, using tactics - like omega is easier this way. *) - - Notation "x == y" := (i2z x = i2z y) - (at level 70, y at next level, no associativity) : Int_scope. - Notation "x <= y" := (Zle (i2z x) (i2z y)): Int_scope. - Notation "x < y" := (Zlt (i2z x) (i2z y)) : Int_scope. - Notation "x >= y" := (Zge (i2z x) (i2z y)) : Int_scope. - Notation "x > y" := (Zgt (i2z x) (i2z y)): Int_scope. - Notation "x <= y <= z" := (x <= y /\ y <= z) : Int_scope. - Notation "x <= y < z" := (x <= y /\ y < z) : Int_scope. - Notation "x < y < z" := (x < y /\ y < z) : Int_scope. - Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope. - - (** Some decidability fonctions (informative). *) - - Axiom gt_le_dec : forall x y: int, {x > y} + {x <= y}. - Axiom ge_lt_dec : forall x y : int, {x >= y} + {x < y}. - Axiom eq_dec : forall x y : int, { x == y } + {~ x==y }. - - (** Specifications *) - - (** First, we ask [i2z] to be injective. Said otherwise, our ad-hoc equality - [==] and the generic [=] are in fact equivalent. We define [==] - nonetheless since the translation to [Z] for using automatic tactic is easier. *) - - Axiom i2z_eq : forall n p : int, n == p -> n = p. - - (** Then, we express the specifications of the above parameters using their - Z counterparts. *) - - Open Scope Z_scope. - Axiom i2z_0 : i2z _0 = 0. - Axiom i2z_1 : i2z _1 = 1. - Axiom i2z_2 : i2z _2 = 2. - Axiom i2z_3 : i2z _3 = 3. - Axiom i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. - Axiom i2z_opp : forall n, i2z (-n) = -i2z n. - Axiom i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. - Axiom i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. - Axiom i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). - -End Int. - -Module MoreInt (I:Int). - Import I. - - Open Scope Int_scope. - - (** A magic (but costly) tactic that goes from [int] back to the [Z] - friendly world ... *) - - Hint Rewrite -> - i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z. - - Ltac i2z := match goal with - | H : (eq (A:=int) ?a ?b) |- _ => - generalize (f_equal i2z H); - try autorewrite with i2z; clear H; intro H; i2z - | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); try autorewrite with i2z; i2z - | H : _ |- _ => progress autorewrite with i2z in H; i2z - | _ => try autorewrite with i2z - end. - - (** A reflexive version of the [i2z] tactic *) - - (** this [i2z_refl] is actually weaker than [i2z]. For instance, if a - [i2z] is buried deep inside a subterm, [i2z_refl] may miss it. - See also the limitation about [Set] or [Type] part below. - Anyhow, [i2z_refl] is enough for applying [romega]. *) - - Ltac i2z_gen := match goal with - | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen - | H : (eq (A:=int) ?a ?b) |- _ => - generalize (f_equal i2z H); clear H; i2z_gen - | H : (eq (A:=Z) ?a ?b) |- _ => generalize H; clear H; i2z_gen - | H : (Zlt ?a ?b) |- _ => generalize H; clear H; i2z_gen - | H : (Zle ?a ?b) |- _ => generalize H; clear H; i2z_gen - | H : (Zgt ?a ?b) |- _ => generalize H; clear H; i2z_gen - | H : (Zge ?a ?b) |- _ => generalize H; clear H; i2z_gen - | H : _ -> ?X |- _ => - (* A [Set] or [Type] part cannot be dealt with easily - using the [ExprP] datatype. So we forget it, leaving - a goal that can be weaker than the original. *) - match type of X with - | Type => clear H; i2z_gen - | Prop => generalize H; clear H; i2z_gen - end - | H : _ <-> _ |- _ => generalize H; clear H; i2z_gen - | H : _ /\ _ |- _ => generalize H; clear H; i2z_gen - | H : _ \/ _ |- _ => generalize H; clear H; i2z_gen - | H : ~ _ |- _ => generalize H; clear H; i2z_gen - | _ => idtac - end. - - Inductive ExprI : Set := - | EI0 : ExprI - | EI1 : ExprI - | EI2 : ExprI - | EI3 : ExprI - | EIplus : ExprI -> ExprI -> ExprI - | EIopp : ExprI -> ExprI - | EIminus : ExprI -> ExprI -> ExprI - | EImult : ExprI -> ExprI -> ExprI - | EImax : ExprI -> ExprI -> ExprI - | EIraw : int -> ExprI. - - Inductive ExprZ : Set := - | EZplus : ExprZ -> ExprZ -> ExprZ - | EZopp : ExprZ -> ExprZ - | EZminus : ExprZ -> ExprZ -> ExprZ - | EZmult : ExprZ -> ExprZ -> ExprZ - | EZmax : ExprZ -> ExprZ -> ExprZ - | EZofI : ExprI -> ExprZ - | EZraw : Z -> ExprZ. - - Inductive ExprP : Type := - | EPeq : ExprZ -> ExprZ -> ExprP - | EPlt : ExprZ -> ExprZ -> ExprP - | EPle : ExprZ -> ExprZ -> ExprP - | EPgt : ExprZ -> ExprZ -> ExprP - | EPge : ExprZ -> ExprZ -> ExprP - | EPimpl : ExprP -> ExprP -> ExprP - | EPequiv : ExprP -> ExprP -> ExprP - | EPand : ExprP -> ExprP -> ExprP - | EPor : ExprP -> ExprP -> ExprP - | EPneg : ExprP -> ExprP - | EPraw : Prop -> ExprP. - - (** [int] to [ExprI] *) - - Ltac i2ei trm := - match constr:trm with - | 0 => constr:EI0 - | 1 => constr:EI1 - | 2 => constr:EI2 - | 3 => constr:EI3 - | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIplus ex ey) - | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIminus ex ey) - | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImult ex ey) - | max ?x ?y => let ex := i2ei x with ey := i2ei y in constr:(EImax ex ey) - | - ?x => let ex := i2ei x in constr:(EIopp ex) - | ?x => constr:(EIraw x) - end - - (** [Z] to [ExprZ] *) - - with z2ez trm := - match constr:trm with - | (?x+?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey) - | (?x-?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey) - | (?x*?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey) - | (Zmax ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey) - | (-?x)%Z => let ex := z2ez x in constr:(EZopp ex) - | i2z ?x => let ex := i2ei x in constr:(EZofI ex) - | ?x => constr:(EZraw x) - end. - - (** [Prop] to [ExprP] *) - - Ltac p2ep trm := - match constr:trm with - | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey) - | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey) - | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey) - | (?x \/ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPor ex ey) - | (~ ?x) => let ex := p2ep x in constr:(EPneg ex) - | (eq (A:=Z) ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EPeq ex ey) - | (?x let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey) - | (?x<=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey) - | (?x>?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey) - | (?x>=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey) - | ?x => constr:(EPraw x) - end. - - (** [ExprI] to [int] *) - - Fixpoint ei2i (e:ExprI) : int := - match e with - | EI0 => 0 - | EI1 => 1 - | EI2 => 2 - | EI3 => 3 - | EIplus e1 e2 => (ei2i e1)+(ei2i e2) - | EIminus e1 e2 => (ei2i e1)-(ei2i e2) - | EImult e1 e2 => (ei2i e1)*(ei2i e2) - | EImax e1 e2 => max (ei2i e1) (ei2i e2) - | EIopp e => -(ei2i e) - | EIraw i => i - end. - - (** [ExprZ] to [Z] *) - - Fixpoint ez2z (e:ExprZ) : Z := - match e with - | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z - | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z - | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z - | EZmax e1 e2 => Zmax (ez2z e1) (ez2z e2) - | EZopp e => (-(ez2z e))%Z - | EZofI e => i2z (ei2i e) - | EZraw z => z - end. - - (** [ExprP] to [Prop] *) - - Fixpoint ep2p (e:ExprP) : Prop := - match e with - | EPeq e1 e2 => (ez2z e1) = (ez2z e2) - | EPlt e1 e2 => ((ez2z e1)<(ez2z e2))%Z - | EPle e1 e2 => ((ez2z e1)<=(ez2z e2))%Z - | EPgt e1 e2 => ((ez2z e1)>(ez2z e2))%Z - | EPge e1 e2 => ((ez2z e1)>=(ez2z e2))%Z - | EPimpl e1 e2 => (ep2p e1) -> (ep2p e2) - | EPequiv e1 e2 => (ep2p e1) <-> (ep2p e2) - | EPand e1 e2 => (ep2p e1) /\ (ep2p e2) - | EPor e1 e2 => (ep2p e1) \/ (ep2p e2) - | EPneg e => ~ (ep2p e) - | EPraw p => p - end. - - (** [ExprI] (supposed under a [i2z]) to a simplified [ExprZ] *) - - Fixpoint norm_ei (e:ExprI) : ExprZ := - match e with - | EI0 => EZraw (0%Z) - | EI1 => EZraw (1%Z) - | EI2 => EZraw (2%Z) - | EI3 => EZraw (3%Z) - | EIplus e1 e2 => EZplus (norm_ei e1) (norm_ei e2) - | EIminus e1 e2 => EZminus (norm_ei e1) (norm_ei e2) - | EImult e1 e2 => EZmult (norm_ei e1) (norm_ei e2) - | EImax e1 e2 => EZmax (norm_ei e1) (norm_ei e2) - | EIopp e => EZopp (norm_ei e) - | EIraw i => EZofI (EIraw i) - end. - - (** [ExprZ] to a simplified [ExprZ] *) - - Fixpoint norm_ez (e:ExprZ) : ExprZ := - match e with - | EZplus e1 e2 => EZplus (norm_ez e1) (norm_ez e2) - | EZminus e1 e2 => EZminus (norm_ez e1) (norm_ez e2) - | EZmult e1 e2 => EZmult (norm_ez e1) (norm_ez e2) - | EZmax e1 e2 => EZmax (norm_ez e1) (norm_ez e2) - | EZopp e => EZopp (norm_ez e) - | EZofI e => norm_ei e - | EZraw z => EZraw z - end. - - (** [ExprP] to a simplified [ExprP] *) - - Fixpoint norm_ep (e:ExprP) : ExprP := - match e with - | EPeq e1 e2 => EPeq (norm_ez e1) (norm_ez e2) - | EPlt e1 e2 => EPlt (norm_ez e1) (norm_ez e2) - | EPle e1 e2 => EPle (norm_ez e1) (norm_ez e2) - | EPgt e1 e2 => EPgt (norm_ez e1) (norm_ez e2) - | EPge e1 e2 => EPge (norm_ez e1) (norm_ez e2) - | EPimpl e1 e2 => EPimpl (norm_ep e1) (norm_ep e2) - | EPequiv e1 e2 => EPequiv (norm_ep e1) (norm_ep e2) - | EPand e1 e2 => EPand (norm_ep e1) (norm_ep e2) - | EPor e1 e2 => EPor (norm_ep e1) (norm_ep e2) - | EPneg e => EPneg (norm_ep e) - | EPraw p => EPraw p - end. - - Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e). - Proof. - induction e; simpl; intros; i2z; auto; try congruence. - Qed. - - Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e. - Proof. - induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct. - Qed. - - Lemma norm_ep_correct : - forall e:ExprP, ep2p (norm_ep e) <-> ep2p e. - Proof. - induction e; simpl; repeat (rewrite norm_ez_correct); intuition. - Qed. - - Lemma norm_ep_correct2 : - forall e:ExprP, ep2p (norm_ep e) -> ep2p e. - Proof. - intros; destruct (norm_ep_correct e); auto. - Qed. - - Ltac i2z_refl := - i2z_gen; - match goal with |- ?t => - let e := p2ep t - in - (change (ep2p e); - apply norm_ep_correct2; - simpl) - end. - - Ltac iauto := i2z_refl; auto. - Ltac iomega := i2z_refl; intros; romega. - - Open Scope Z_scope. - - Lemma max_spec : forall (x y:Z), - x >= y /\ Zmax x y = x \/ - x < y /\ Zmax x y = y. - Proof. - intros; unfold Zmax, Zlt, Zge. - destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate. - Qed. - - Ltac omega_max_genspec x y := - generalize (max_spec x y); - let z := fresh "z" in let Hz := fresh "Hz" in - (set (z:=Zmax x y); clearbody z). - - Ltac omega_max_loop := - match goal with - (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *) - | |- context [ i2z (?f ?x) ] => - let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop - | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop - | _ => intros - end. - - Ltac omega_max := i2z_refl; omega_max_loop; try romega. - - Ltac false_omega := i2z_refl; intros; romega. - Ltac false_omega_max := elimtype False; omega_max. - - Open Scope Int_scope. -End MoreInt. - - -(** It's always nice to know that our [Int] interface is realizable :-) *) - -Module Z_as_Int <: Int. - Open Scope Z_scope. - Definition int := Z. - Definition _0 := 0. - Definition _1 := 1. - Definition _2 := 2. - Definition _3 := 3. - Definition plus := Zplus. - Definition opp := Zopp. - Definition minus := Zminus. - Definition mult := Zmult. - Definition max := Zmax. - Definition gt_le_dec := Z_gt_le_dec. - Definition ge_lt_dec := Z_ge_lt_dec. - Definition eq_dec := Z_eq_dec. - Definition i2z : int -> Z := fun n => n. - Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed. - Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed. - Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed. - Lemma i2z_2 : i2z _2 = 2. Proof. auto. Qed. - Lemma i2z_3 : i2z _3 = 3. Proof. auto. Qed. - Lemma i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. Proof. auto. Qed. - Lemma i2z_opp : forall n, i2z (- n) = - i2z n. Proof. auto. Qed. - Lemma i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. Proof. auto. Qed. - Lemma i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. Proof. auto. Qed. - Lemma i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed. -End Z_as_Int. - diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index b3efa5fadd..79c1e56d21 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) -(** This file provides classical logic and indefinite description +(** *** This file provides classical logic and indefinite description (Hilbert's epsilon operator) *) (** Classical epsilon's operator (i.e. indefinite description) implies @@ -25,7 +25,7 @@ Notation Local "'inhabited' A" := A (at level 200, only parsing). Axiom constructive_indefinite_description : forall (A : Type) (P : A->Prop), - (exists x : A, P x) -> { x : A | P x }. + (ex P) -> { x : A | P x }. Lemma constructive_definite_description : forall (A : Type) (P : A->Prop), @@ -43,11 +43,11 @@ Qed. Theorem classical_indefinite_description : forall (A : Type) (P : A->Prop), inhabited A -> - { x : A | (exists x : A, P x) -> P x }. + { x : A | ex P -> P x }. Proof. intros A P i. destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP]. - apply constructive_indefinite_description with (P:= fun x => (exists x, P x) -> P x). + apply constructive_indefinite_description with (P:= fun x => ex P -> P x). destruct Hex as (x,Hx). exists x; intros _; exact Hx. firstorder. @@ -59,9 +59,11 @@ Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A := proj1_sig (classical_indefinite_description P i). Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : - (exists x:A, P x) -> P (epsilon i P) + (ex P) -> P (epsilon i P) := proj2_sig (classical_indefinite_description P i). +Opaque epsilon. + (** Open question: is classical_indefinite_description constructively provable from [relational_choice] and [constructive_definite_description] (at least, using the fact that @@ -70,7 +72,10 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : [classical_indefinite_description] is provable (see [relative_non_contradiction_of_indefinite_desc]). *) -(** Weaker lemmas (compatibility lemmas) *) +(** Remark: we use [ex P] rather than [exists x, P x] (which is [ex + (fun x => P x)] to ease unification *) + +(** *** Weaker lemmas (compatibility lemmas) *) Theorem choice : forall (A B : Type) (R : A->B->Prop), @@ -78,7 +83,8 @@ Theorem choice : (exists f : A->B, forall x : A, R x (f x)). Proof. intros A B R H. -exists (fun x => proj1_sig (constructive_indefinite_description (R x) (H x))). +exists (fun x => proj1_sig (constructive_indefinite_description (H x))). intro x. -apply (proj2_sig (constructive_indefinite_description (R x) (H x))). +apply (proj2_sig (constructive_indefinite_description (H x))). Qed. + diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v new file mode 100644 index 0000000000..a4de6ca7fe --- /dev/null +++ b/theories/Logic/DecidableType.v @@ -0,0 +1,156 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> Prop. + + Axiom eq_refl : forall x : t, eq x x. + Axiom eq_sym : forall x y : t, eq x y -> eq y x. + Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + + Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. + + Hint Immediate eq_sym. + Hint Resolve eq_refl eq_trans. + +End DecidableType. + +(** * Additional notions about keys and datas used in FMap *) + +Module KeyDecidableType(D:DecidableType). + Import D. + + Section Elt. + Variable elt : Set. + Notation key:=t. + + Definition eqk (p p':key*elt) := eq (fst p) (fst p'). + Definition eqke (p p':key*elt) := + eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Hint Unfold eqk eqke. + Hint Extern 2 (eqke ?a ?b) => split. + + (* eqke is stricter than eqk *) + + Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'. + Proof. + unfold eqk, eqke; intuition. + Qed. + + (* eqk, eqke are equalities *) + + Lemma eqk_refl : forall e, eqk e e. + Proof. auto. Qed. + + Lemma eqke_refl : forall e, eqke e e. + Proof. auto. Qed. + + Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. + Proof. auto. Qed. + + Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. + Proof. unfold eqke; intuition. Qed. + + Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. + Proof. eauto. Qed. + + Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. + Proof. + unfold eqke; intuition; [ eauto | congruence ]. + Qed. + + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. + Hint Immediate eqk_sym eqke_sym. + + Lemma InA_eqke_eqk : + forall x m, InA eqke x m -> InA eqk x m. + Proof. + unfold eqke; induction 1; intuition. + Qed. + Hint Resolve InA_eqke_eqk. + + Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. + Proof. + intros; apply InA_eqA with p; auto; apply eqk_trans; auto. + Qed. + + Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). + Definition In k m := exists e:elt, MapsTo k e m. + + Hint Unfold MapsTo In. + + (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) + + Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. + Proof. + firstorder. + exists x; auto. + induction H. + destruct y. + exists e; auto. + destruct IHInA as [e H0]. + exists e; auto. + Qed. + + Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. + Proof. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto. + Qed. + + Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. + Proof. + destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto. + Qed. + + Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. + Proof. + inversion 1. + inversion_clear H0; eauto. + destruct H1; simpl in *; intuition. + Qed. + + Lemma In_inv_2 : forall k k' e e' l, + InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. + Proof. + inversion_clear 1; compute in H0; intuition. + Qed. + + Lemma In_inv_3 : forall x x' l, + InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. + Proof. + inversion_clear 1; compute in H0; intuition. + Qed. + + End Elt. + + Hint Unfold eqk eqke. + Hint Extern 2 (eqke ?a ?b) => split. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. + Hint Immediate eqk_sym eqke_sym. + Hint Resolve InA_eqke_eqk. + Hint Unfold MapsTo In. + Hint Resolve In_inv_2 In_inv_3. + +End KeyDecidableType. + + + + + diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v new file mode 100644 index 0000000000..dcca370953 --- /dev/null +++ b/theories/Logic/DecidableTypeEx.v @@ -0,0 +1,50 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Z. + Arguments Scope i2z [ Int_scope ]. + + Parameter _0 : int. + Parameter _1 : int. + Parameter _2 : int. + Parameter _3 : int. + Parameter plus : int -> int -> int. + Parameter opp : int -> int. + Parameter minus : int -> int -> int. + Parameter mult : int -> int -> int. + Parameter max : int -> int -> int. + + Notation "0" := _0 : Int_scope. + Notation "1" := _1 : Int_scope. + Notation "2" := _2 : Int_scope. + Notation "3" := _3 : Int_scope. + Infix "+" := plus : Int_scope. + Infix "-" := minus : Int_scope. + Infix "*" := mult : Int_scope. + Notation "- x" := (opp x) : Int_scope. + +(** For logical relations, we can rely on their counterparts in Z, + since they don't appear after extraction. Moreover, using tactics + like omega is easier this way. *) + + Notation "x == y" := (i2z x = i2z y) + (at level 70, y at next level, no associativity) : Int_scope. + Notation "x <= y" := (Zle (i2z x) (i2z y)): Int_scope. + Notation "x < y" := (Zlt (i2z x) (i2z y)) : Int_scope. + Notation "x >= y" := (Zge (i2z x) (i2z y)) : Int_scope. + Notation "x > y" := (Zgt (i2z x) (i2z y)): Int_scope. + Notation "x <= y <= z" := (x <= y /\ y <= z) : Int_scope. + Notation "x <= y < z" := (x <= y /\ y < z) : Int_scope. + Notation "x < y < z" := (x < y /\ y < z) : Int_scope. + Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope. + + (** Some decidability fonctions (informative). *) + + Axiom gt_le_dec : forall x y: int, {x > y} + {x <= y}. + Axiom ge_lt_dec : forall x y : int, {x >= y} + {x < y}. + Axiom eq_dec : forall x y : int, { x == y } + {~ x==y }. + + (** Specifications *) + + (** First, we ask [i2z] to be injective. Said otherwise, our ad-hoc equality + [==] and the generic [=] are in fact equivalent. We define [==] + nonetheless since the translation to [Z] for using automatic tactic is easier. *) + + Axiom i2z_eq : forall n p : int, n == p -> n = p. + + (** Then, we express the specifications of the above parameters using their + Z counterparts. *) + + Open Scope Z_scope. + Axiom i2z_0 : i2z _0 = 0. + Axiom i2z_1 : i2z _1 = 1. + Axiom i2z_2 : i2z _2 = 2. + Axiom i2z_3 : i2z _3 = 3. + Axiom i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. + Axiom i2z_opp : forall n, i2z (-n) = -i2z n. + Axiom i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. + Axiom i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. + Axiom i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). + +End Int. + +Module MoreInt (I:Int). + Import I. + + Open Scope Int_scope. + + (** A magic (but costly) tactic that goes from [int] back to the [Z] + friendly world ... *) + + Hint Rewrite -> + i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z. + + Ltac i2z := match goal with + | H : (eq (A:=int) ?a ?b) |- _ => + generalize (f_equal i2z H); + try autorewrite with i2z; clear H; intro H; i2z + | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); try autorewrite with i2z; i2z + | H : _ |- _ => progress autorewrite with i2z in H; i2z + | _ => try autorewrite with i2z + end. + + (** A reflexive version of the [i2z] tactic *) + + (** this [i2z_refl] is actually weaker than [i2z]. For instance, if a + [i2z] is buried deep inside a subterm, [i2z_refl] may miss it. + See also the limitation about [Set] or [Type] part below. + Anyhow, [i2z_refl] is enough for applying [romega]. *) + + Ltac i2z_gen := match goal with + | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen + | H : (eq (A:=int) ?a ?b) |- _ => + generalize (f_equal i2z H); clear H; i2z_gen + | H : (eq (A:=Z) ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zlt ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zle ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zgt ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zge ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : _ -> ?X |- _ => + (* A [Set] or [Type] part cannot be dealt with easily + using the [ExprP] datatype. So we forget it, leaving + a goal that can be weaker than the original. *) + match type of X with + | Type => clear H; i2z_gen + | Prop => generalize H; clear H; i2z_gen + end + | H : _ <-> _ |- _ => generalize H; clear H; i2z_gen + | H : _ /\ _ |- _ => generalize H; clear H; i2z_gen + | H : _ \/ _ |- _ => generalize H; clear H; i2z_gen + | H : ~ _ |- _ => generalize H; clear H; i2z_gen + | _ => idtac + end. + + Inductive ExprI : Set := + | EI0 : ExprI + | EI1 : ExprI + | EI2 : ExprI + | EI3 : ExprI + | EIplus : ExprI -> ExprI -> ExprI + | EIopp : ExprI -> ExprI + | EIminus : ExprI -> ExprI -> ExprI + | EImult : ExprI -> ExprI -> ExprI + | EImax : ExprI -> ExprI -> ExprI + | EIraw : int -> ExprI. + + Inductive ExprZ : Set := + | EZplus : ExprZ -> ExprZ -> ExprZ + | EZopp : ExprZ -> ExprZ + | EZminus : ExprZ -> ExprZ -> ExprZ + | EZmult : ExprZ -> ExprZ -> ExprZ + | EZmax : ExprZ -> ExprZ -> ExprZ + | EZofI : ExprI -> ExprZ + | EZraw : Z -> ExprZ. + + Inductive ExprP : Type := + | EPeq : ExprZ -> ExprZ -> ExprP + | EPlt : ExprZ -> ExprZ -> ExprP + | EPle : ExprZ -> ExprZ -> ExprP + | EPgt : ExprZ -> ExprZ -> ExprP + | EPge : ExprZ -> ExprZ -> ExprP + | EPimpl : ExprP -> ExprP -> ExprP + | EPequiv : ExprP -> ExprP -> ExprP + | EPand : ExprP -> ExprP -> ExprP + | EPor : ExprP -> ExprP -> ExprP + | EPneg : ExprP -> ExprP + | EPraw : Prop -> ExprP. + + (** [int] to [ExprI] *) + + Ltac i2ei trm := + match constr:trm with + | 0 => constr:EI0 + | 1 => constr:EI1 + | 2 => constr:EI2 + | 3 => constr:EI3 + | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIplus ex ey) + | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIminus ex ey) + | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImult ex ey) + | max ?x ?y => let ex := i2ei x with ey := i2ei y in constr:(EImax ex ey) + | - ?x => let ex := i2ei x in constr:(EIopp ex) + | ?x => constr:(EIraw x) + end + + (** [Z] to [ExprZ] *) + + with z2ez trm := + match constr:trm with + | (?x+?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey) + | (?x-?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey) + | (?x*?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey) + | (Zmax ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey) + | (-?x)%Z => let ex := z2ez x in constr:(EZopp ex) + | i2z ?x => let ex := i2ei x in constr:(EZofI ex) + | ?x => constr:(EZraw x) + end. + + (** [Prop] to [ExprP] *) + + Ltac p2ep trm := + match constr:trm with + | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey) + | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey) + | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey) + | (?x \/ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPor ex ey) + | (~ ?x) => let ex := p2ep x in constr:(EPneg ex) + | (eq (A:=Z) ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EPeq ex ey) + | (?x let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey) + | (?x<=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey) + | (?x>?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey) + | (?x>=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey) + | ?x => constr:(EPraw x) + end. + + (** [ExprI] to [int] *) + + Fixpoint ei2i (e:ExprI) : int := + match e with + | EI0 => 0 + | EI1 => 1 + | EI2 => 2 + | EI3 => 3 + | EIplus e1 e2 => (ei2i e1)+(ei2i e2) + | EIminus e1 e2 => (ei2i e1)-(ei2i e2) + | EImult e1 e2 => (ei2i e1)*(ei2i e2) + | EImax e1 e2 => max (ei2i e1) (ei2i e2) + | EIopp e => -(ei2i e) + | EIraw i => i + end. + + (** [ExprZ] to [Z] *) + + Fixpoint ez2z (e:ExprZ) : Z := + match e with + | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z + | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z + | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z + | EZmax e1 e2 => Zmax (ez2z e1) (ez2z e2) + | EZopp e => (-(ez2z e))%Z + | EZofI e => i2z (ei2i e) + | EZraw z => z + end. + + (** [ExprP] to [Prop] *) + + Fixpoint ep2p (e:ExprP) : Prop := + match e with + | EPeq e1 e2 => (ez2z e1) = (ez2z e2) + | EPlt e1 e2 => ((ez2z e1)<(ez2z e2))%Z + | EPle e1 e2 => ((ez2z e1)<=(ez2z e2))%Z + | EPgt e1 e2 => ((ez2z e1)>(ez2z e2))%Z + | EPge e1 e2 => ((ez2z e1)>=(ez2z e2))%Z + | EPimpl e1 e2 => (ep2p e1) -> (ep2p e2) + | EPequiv e1 e2 => (ep2p e1) <-> (ep2p e2) + | EPand e1 e2 => (ep2p e1) /\ (ep2p e2) + | EPor e1 e2 => (ep2p e1) \/ (ep2p e2) + | EPneg e => ~ (ep2p e) + | EPraw p => p + end. + + (** [ExprI] (supposed under a [i2z]) to a simplified [ExprZ] *) + + Fixpoint norm_ei (e:ExprI) : ExprZ := + match e with + | EI0 => EZraw (0%Z) + | EI1 => EZraw (1%Z) + | EI2 => EZraw (2%Z) + | EI3 => EZraw (3%Z) + | EIplus e1 e2 => EZplus (norm_ei e1) (norm_ei e2) + | EIminus e1 e2 => EZminus (norm_ei e1) (norm_ei e2) + | EImult e1 e2 => EZmult (norm_ei e1) (norm_ei e2) + | EImax e1 e2 => EZmax (norm_ei e1) (norm_ei e2) + | EIopp e => EZopp (norm_ei e) + | EIraw i => EZofI (EIraw i) + end. + + (** [ExprZ] to a simplified [ExprZ] *) + + Fixpoint norm_ez (e:ExprZ) : ExprZ := + match e with + | EZplus e1 e2 => EZplus (norm_ez e1) (norm_ez e2) + | EZminus e1 e2 => EZminus (norm_ez e1) (norm_ez e2) + | EZmult e1 e2 => EZmult (norm_ez e1) (norm_ez e2) + | EZmax e1 e2 => EZmax (norm_ez e1) (norm_ez e2) + | EZopp e => EZopp (norm_ez e) + | EZofI e => norm_ei e + | EZraw z => EZraw z + end. + + (** [ExprP] to a simplified [ExprP] *) + + Fixpoint norm_ep (e:ExprP) : ExprP := + match e with + | EPeq e1 e2 => EPeq (norm_ez e1) (norm_ez e2) + | EPlt e1 e2 => EPlt (norm_ez e1) (norm_ez e2) + | EPle e1 e2 => EPle (norm_ez e1) (norm_ez e2) + | EPgt e1 e2 => EPgt (norm_ez e1) (norm_ez e2) + | EPge e1 e2 => EPge (norm_ez e1) (norm_ez e2) + | EPimpl e1 e2 => EPimpl (norm_ep e1) (norm_ep e2) + | EPequiv e1 e2 => EPequiv (norm_ep e1) (norm_ep e2) + | EPand e1 e2 => EPand (norm_ep e1) (norm_ep e2) + | EPor e1 e2 => EPor (norm_ep e1) (norm_ep e2) + | EPneg e => EPneg (norm_ep e) + | EPraw p => EPraw p + end. + + Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e). + Proof. + induction e; simpl; intros; i2z; auto; try congruence. + Qed. + + Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e. + Proof. + induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct. + Qed. + + Lemma norm_ep_correct : + forall e:ExprP, ep2p (norm_ep e) <-> ep2p e. + Proof. + induction e; simpl; repeat (rewrite norm_ez_correct); intuition. + Qed. + + Lemma norm_ep_correct2 : + forall e:ExprP, ep2p (norm_ep e) -> ep2p e. + Proof. + intros; destruct (norm_ep_correct e); auto. + Qed. + + Ltac i2z_refl := + i2z_gen; + match goal with |- ?t => + let e := p2ep t + in + (change (ep2p e); + apply norm_ep_correct2; + simpl) + end. + + Ltac iauto := i2z_refl; auto. + Ltac iomega := i2z_refl; intros; romega. + + Open Scope Z_scope. + + Lemma max_spec : forall (x y:Z), + x >= y /\ Zmax x y = x \/ + x < y /\ Zmax x y = y. + Proof. + intros; unfold Zmax, Zlt, Zge. + destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate. + Qed. + + Ltac omega_max_genspec x y := + generalize (max_spec x y); + let z := fresh "z" in let Hz := fresh "Hz" in + (set (z:=Zmax x y); clearbody z). + + Ltac omega_max_loop := + match goal with + (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *) + | |- context [ i2z (?f ?x) ] => + let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop + | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop + | _ => intros + end. + + Ltac omega_max := i2z_refl; omega_max_loop; try romega. + + Ltac false_omega := i2z_refl; intros; romega. + Ltac false_omega_max := elimtype False; omega_max. + + Open Scope Int_scope. +End MoreInt. + + +(** It's always nice to know that our [Int] interface is realizable :-) *) + +Module Z_as_Int <: Int. + Open Scope Z_scope. + Definition int := Z. + Definition _0 := 0. + Definition _1 := 1. + Definition _2 := 2. + Definition _3 := 3. + Definition plus := Zplus. + Definition opp := Zopp. + Definition minus := Zminus. + Definition mult := Zmult. + Definition max := Zmax. + Definition gt_le_dec := Z_gt_le_dec. + Definition ge_lt_dec := Z_ge_lt_dec. + Definition eq_dec := Z_eq_dec. + Definition i2z : int -> Z := fun n => n. + Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed. + Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed. + Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed. + Lemma i2z_2 : i2z _2 = 2. Proof. auto. Qed. + Lemma i2z_3 : i2z _3 = 3. Proof. auto. Qed. + Lemma i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. Proof. auto. Qed. + Lemma i2z_opp : forall n, i2z (- n) = - i2z n. Proof. auto. Qed. + Lemma i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. Proof. auto. Qed. + Lemma i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. Proof. auto. Qed. + Lemma i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed. +End Z_as_Int. + -- cgit v1.2.3