diff options
-rw-r--r-- | .depend.coq | 64 | ||||
-rw-r--r-- | Makefile | 3 | ||||
-rw-r--r-- | theories/FSets/FMapFacts.v | 541 | ||||
-rw-r--r-- | theories/FSets/FMapWeak.v | 1 | ||||
-rw-r--r-- | theories/FSets/FMapWeakFacts.v | 583 | ||||
-rw-r--r-- | theories/FSets/FMaps.v | 1 | ||||
-rw-r--r-- | theories/Lists/SetoidList.v | 49 |
7 files changed, 1187 insertions, 55 deletions
diff --git a/.depend.coq b/.depend.coq index 822602cd6..d6babae10 100644 --- a/.depend.coq +++ b/.depend.coq @@ -1,7 +1,7 @@ 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 theories/NArith/NArith.vo theories/NArith/Ndec.vo theories/Arith/Compare_dec.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 theories/FSets/FSetInterface.vo: theories/FSets/FSetInterface.v theories/Bool/Bool.vo theories/FSets/OrderedType.vo theories/FSets/FSetList.vo: theories/FSets/FSetList.v theories/FSets/FSetInterface.vo @@ -17,10 +17,12 @@ theories/FSets/FSetWeakFacts.vo: theories/FSets/FSetWeakFacts.v theories/FSets/F 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/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/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/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/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/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 @@ -212,7 +214,7 @@ theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/S 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 theories/NArith/NArith.vo theories/NArith/Ndec.vo theories/Arith/Compare_dec.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 theories/FSets/FSetInterface.vo: theories/FSets/FSetInterface.v theories/Bool/Bool.vo theories/FSets/OrderedType.vo theories/FSets/FSetList.vo: theories/FSets/FSetList.v theories/FSets/FSetInterface.vo @@ -228,10 +230,12 @@ theories/FSets/FSetWeakFacts.vo: theories/FSets/FSetWeakFacts.v theories/FSets/F 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/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/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/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/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/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 @@ -271,54 +275,6 @@ 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 @@ -877,7 +877,8 @@ FSETSBASEVO=\ theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakList.vo \ theories/FSets/FSetWeakFacts.vo theories/FSets/FSetWeak.vo \ theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo \ - theories/FSets/FMaps.vo \ + theories/FSets/FMaps.vo theories/FSets/FMapFacts.vo \ + 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 \ diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v new file mode 100644 index 000000000..6217a7037 --- /dev/null +++ b/theories/FSets/FMapFacts.v @@ -0,0 +1,541 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(** * Finite maps library *) + +(** This functor derives additional facts from [FMapInterface.S]. These + facts are mainly the specifications of [FMapInterface.S] written using + different styles: equivalence and boolean equalities. +*) + +Require Import Bool. +Require Import OrderedType. +Require Export FMapInterface. +Set Implicit Arguments. +Unset Strict Implicit. + +Module Facts (M: S). +Module ME := OrderedTypeFacts M.E. +Import ME. +Import M. +Import Logic. (* to unmask [eq] *) +Import Peano. (* to unmask [lt] *) + +Lemma MapsTo_fun : forall (elt:Set) m x (e e':elt), + MapsTo x e m -> MapsTo x e' m -> e=e'. +Proof. +intros. +generalize (find_1 H) (find_1 H0); clear H H0. +intros; rewrite H in H0; injection H0; auto. +Qed. + +(** * Specifications written using equivalences *) + +Section IffSpec. +Variable elt elt' elt'': Set. +Implicit Type m: t elt. +Implicit Type x y z: key. +Implicit Type e: elt. + +Lemma MapsTo_iff : forall m x y e, E.eq x y -> (MapsTo x e m <-> MapsTo y e m). +Proof. +split; apply MapsTo_1; auto. +Qed. + +Lemma In_iff : forall m x y, E.eq x y -> (In x m <-> In y m). +Proof. +unfold In. +split; intros (e0,H0); exists e0. +apply (MapsTo_1 H H0); auto. +apply (MapsTo_1 (E.eq_sym H) H0); auto. +Qed. + +Lemma find_mapsto_iff : forall m x e, MapsTo x e m <-> find x m = Some e. +Proof. +split; [apply find_1|apply find_2]. +Qed. + +Lemma not_find_mapsto_iff : forall m x, ~In x m <-> find x m = None. +Proof. +intros. +generalize (find_mapsto_iff m x); destruct (find x m). +split; intros; try discriminate. +destruct H0. +exists e; rewrite H; auto. +split; auto. +intros; intros (e,H1). +rewrite H in H1; discriminate. +Qed. + +Lemma mem_in_iff : forall m x, In x m <-> mem x m = true. +Proof. +split; [apply mem_1|apply mem_2]. +Qed. + +Lemma not_mem_in_iff : forall m x, ~In x m <-> mem x m = false. +Proof. +intros; rewrite mem_in_iff; destruct (mem x m); intuition. +Qed. + +Lemma equal_iff : forall m m' cmp, Equal cmp m m' <-> equal cmp m m' = true. +Proof. +split; [apply equal_1|apply equal_2]. +Qed. + +Lemma empty_mapsto_iff : forall x e, MapsTo x e (empty elt) <-> False. +Proof. +intuition; apply (empty_1 H). +Qed. + +Lemma empty_in_iff : forall x, In x (empty elt) <-> False. +Proof. +unfold In. +split; [intros (e,H); rewrite empty_mapsto_iff in H|]; intuition. +Qed. + +Lemma is_empty_iff : forall m, Empty m <-> is_empty m = true. +Proof. +split; [apply is_empty_1|apply is_empty_2]. +Qed. + +Lemma add_mapsto_iff : forall m x y e e', + MapsTo y e' (add x e m) <-> + (E.eq x y /\ e=e') \/ + (~E.eq x y /\ MapsTo y e' m). +Proof. +intros. +intuition. +destruct (eq_dec x y); [left|right]. +split; auto. +symmetry; apply (MapsTo_fun (e':=e) H); auto. +split; auto; apply add_3 with x e; auto. +subst; auto. +Qed. + +Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m. +Proof. +unfold In; split. +intros (e',H). +destruct (eq_dec x y) as [E|E]; auto. +right; exists e'; auto. +apply (add_3 E H). +destruct (eq_dec x y) as [E|E]; auto. +intros. +exists e; apply add_1; auto. +intros [H|(e',H)]. +destruct E; auto. +exists e'; apply add_2; auto. +Qed. + +Lemma add_neq_mapsto_iff : forall m x y e e', + ~ E.eq x y -> (MapsTo y e' (add x e m) <-> MapsTo y e' m). +Proof. +split; [apply add_3|apply add_2]; auto. +Qed. + +Lemma add_neq_in_iff : forall m x y e, + ~ E.eq x y -> (In y (add x e m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +apply (add_3 H H0). +apply add_2; auto. +Qed. + +Lemma remove_mapsto_iff : forall m x y e, + MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m. +Proof. +intros. +split; intros. +split. +assert (In y (remove x m)) by (exists e; auto). +intro H1; apply (remove_1 H1 H0). +apply remove_3 with x; auto. +apply remove_2; intuition. +Qed. + +Lemma remove_in_iff : forall m x y, In y (remove x m) <-> ~E.eq x y /\ In y m. +Proof. +unfold In; split. +intros (e,H). +split. +assert (In y (remove x m)) by (exists e; auto). +intro H1; apply (remove_1 H1 H0). +exists e; apply remove_3 with x; auto. +intros (H,(e,H0)); exists e; apply remove_2; auto. +Qed. + +Lemma remove_neq_mapsto_iff : forall m x y e, + ~ E.eq x y -> (MapsTo y e (remove x m) <-> MapsTo y e m). +Proof. +split; [apply remove_3|apply remove_2]; auto. +Qed. + +Lemma remove_neq_in_iff : forall m x y, + ~ E.eq x y -> (In y (remove x m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +apply (remove_3 H0). +apply remove_2; auto. +Qed. + +Lemma elements_mapsto_iff : forall m x e, + MapsTo x e m <-> InA (@eq_key_elt _) (x,e) (elements m). +Proof. +split; [apply elements_1 | apply elements_2]. +Qed. + +Lemma elements_in_iff : forall m x, + In x m <-> exists e, InA (@eq_key_elt _) (x,e) (elements m). +Proof. +unfold In; split; intros (e,H); exists e; [apply elements_1 | apply elements_2]; auto. +Qed. + +Lemma map_mapsto_iff : forall m x b (f : elt -> elt'), + MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m. +Proof. +split. +case_eq (find x m); intros. +exists e. +split. +apply (MapsTo_fun (m:=map f m) (x:=x)); auto. +apply find_2; auto. +assert (In x (map f m)) by (exists b; auto). +destruct (map_2 H1) as (a,H2). +rewrite (find_1 H2) in H; discriminate. +intros (a,(H,H0)). +subst b; auto. +Qed. + +Lemma map_in_iff : forall m x (f : elt -> elt'), + In x (map f m) <-> In x m. +Proof. +split; intros; eauto. +destruct H as (a,H). +exists (f a); auto. +Qed. + +Lemma mapi_in_iff : forall m x (f:key->elt->elt'), + In x (mapi f m) <-> In x m. +Proof. +split; intros; eauto. +destruct H as (a,H). +destruct (mapi_1 f H) as (y,(H0,H1)). +exists (f y a); auto. +Qed. + +(* Unfortunately, we don't have simple equivalences for [mapi] + and [MapsTo]. The only correct one needs compatibility of [f]. *) + +Lemma mapi_inv : forall m x b (f : key -> elt -> elt'), + MapsTo x b (mapi f m) -> + exists a, exists y, E.eq y x /\ b = f y a /\ MapsTo x a m. +Proof. +intros; case_eq (find x m); intros. +exists e. +destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)). +apply find_2; auto. +exists y; repeat split; auto. +apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto. +assert (In x (mapi f m)) by (exists b; auto). +destruct (mapi_2 H1) as (a,H2). +rewrite (find_1 H2) in H0; discriminate. +Qed. + +Lemma mapi_1bis : forall m x e (f:key->elt->elt'), + (forall x y e, E.eq x y -> f x e = f y e) -> + MapsTo x e m -> MapsTo x (f x e) (mapi f m). +Proof. +intros. +destruct (mapi_1 f H0) as (y,(H1,H2)). +replace (f x e) with (f y e) by auto. +auto. +Qed. + +Lemma mapi_mapsto_iff : forall m x b (f:key->elt->elt'), + (forall x y e, E.eq x y -> f x e = f y e) -> + (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m). +Proof. +split. +intros. +destruct (mapi_inv H0) as (a,(y,(H1,(H2,H3)))). +exists a; split; auto. +subst b; auto. +intros (a,(H0,H1)). +subst b. +apply mapi_1bis; auto. +Qed. + +(** Things are even worse for [map2] : we don't try to state any + equivalence, see instead boolean results below. *) + +End IffSpec. + +(** Useful tactic for simplifying expressions like [In y (add x e (remove z m))] *) + +Ltac map_iff := + repeat (progress ( + rewrite add_mapsto_iff || rewrite add_in_iff || + rewrite remove_mapsto_iff || rewrite remove_in_iff || + rewrite empty_mapsto_iff || rewrite empty_in_iff || + rewrite map_mapsto_iff || rewrite map_in_iff || + rewrite mapi_in_iff)). + +(** * Specifications written using boolean predicates *) + +Section BoolSpec. + +Lemma mem_find_b : forall (elt:Set)(m:t elt)(x:key), mem x m = if find x m then true else false. +Proof. +intros. +generalize (find_mapsto_iff m x)(mem_in_iff m x); unfold In. +destruct (find x m); destruct (mem x m); auto. +intros. +rewrite <- H0; exists e; rewrite H; auto. +intuition. +destruct H0 as (e,H0). +destruct (H e); intuition discriminate. +Qed. + +Variable elt elt' elt'' : Set. +Implicit Types m : t elt. +Implicit Types x y z : key. +Implicit Types e : elt. + +Lemma mem_b : forall m x y, E.eq x y -> mem x m = mem y m. +Proof. +intros. +generalize (mem_in_iff m x) (mem_in_iff m y)(In_iff m H). +destruct (mem x m); destruct (mem y m); intuition. +Qed. + +Lemma find_o : forall m x y, E.eq x y -> find x m = find y m. +Proof. +intros. +generalize (find_mapsto_iff m x) (find_mapsto_iff m y) (fun e => MapsTo_iff m e H). +destruct (find x m); destruct (find y m); intros. +rewrite <- H0; rewrite H2; rewrite H1; auto. +symmetry; rewrite <- H1; rewrite <- H2; rewrite H0; auto. +rewrite <- H0; rewrite H2; rewrite H1; auto. +auto. +Qed. + +Lemma add_eq_o : forall m x y e, + E.eq x y -> find y (add x e m) = Some e. +Proof. +auto. +Qed. + +Lemma add_neq_o : forall m x y e, + ~ E.eq x y -> find y (add x e m) = find y m. +Proof. +intros. +case_eq (find y m); intros; auto. +case_eq (find y (add x e m)); intros; auto. +rewrite <- H0; symmetry. +apply find_1; apply add_3 with x e; auto. +Qed. +Hint Resolve add_neq_o. + +Lemma add_o : forall m x y e, + find y (add x e m) = if eq_dec x y then Some e else find y m. +Proof. +intros; destruct (eq_dec x y); auto. +Qed. + +Lemma add_eq_b : forall m x y e, + E.eq x y -> mem y (add x e m) = true. +Proof. +intros; rewrite mem_find_b; rewrite add_eq_o; auto. +Qed. + +Lemma add_neq_b : forall m x y e, + ~E.eq x y -> mem y (add x e m) = mem y m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite add_neq_o; auto. +Qed. + +Lemma add_b : forall m x y e, + mem y (add x e m) = eqb x y || mem y m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite add_o; unfold eqb. +destruct (eq_dec x y); simpl; auto. +Qed. + +Lemma remove_eq_o : forall m x y, + E.eq x y -> find y (remove x m) = None. +Proof. +intros. +generalize (remove_1 (m:=m) H). +generalize (find_mapsto_iff (remove x m) y). +destruct (find y (remove x m)); auto. +destruct 2. +exists e; rewrite H0; auto. +Qed. +Hint Resolve remove_eq_o. + +Lemma remove_neq_o : forall m x y, + ~ E.eq x y -> find y (remove x m) = find y m. +Proof. +intros. +case_eq (find y m); intros; auto. +case_eq (find y (remove x m)); intros; auto. +rewrite <- H0; symmetry. +apply find_1; apply remove_3 with x; auto. +Qed. +Hint Resolve remove_neq_o. + +Lemma remove_o : forall m x y, + find y (remove x m) = if eq_dec x y then None else find y m. +Proof. +intros; destruct (eq_dec x y); auto. +Qed. + +Lemma remove_eq_b : forall m x y, + E.eq x y -> mem y (remove x m) = false. +Proof. +intros; rewrite mem_find_b; rewrite remove_eq_o; auto. +Qed. + +Lemma remove_neq_b : forall m x y, + ~ E.eq x y -> mem y (remove x m) = mem y m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite remove_neq_o; auto. +Qed. + +Lemma remove_b : forall m x y, + mem y (remove x m) = negb (eqb x y) && mem y m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. +destruct (eq_dec x y); auto. +Qed. + +Definition option_map (A:Set)(B:Set)(f:A->B)(o:option A) : option B := + match o with + | Some a => Some (f a) + | None => None + end. + +Lemma map_o : forall m x (f:elt->elt'), + find x (map f m) = option_map f (find x m). +Proof. +intros. +generalize (find_mapsto_iff (map f m) x) (find_mapsto_iff m x) + (fun b => map_mapsto_iff m x b f). +destruct (find x (map f m)); destruct (find x m); simpl; auto; intros. +rewrite <- H; rewrite H1; exists e0; rewrite H0; auto. +destruct (H e) as [_ H2]. +rewrite H1 in H2. +destruct H2 as (a,(_,H2)); auto. +rewrite H0 in H2; discriminate. +rewrite <- H; rewrite H1; exists e; rewrite H0; auto. +Qed. + +Lemma map_b : forall m x (f:elt->elt'), + mem x (map f m) = mem x m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite map_o. +destruct (find x m); simpl; auto. +Qed. + +Lemma mapi_b : forall m x (f:key->elt->elt'), + mem x (mapi f m) = mem x m. +Proof. +intros. +generalize (mem_in_iff (mapi f m) x) (mem_in_iff m x) (mapi_in_iff m x f). +destruct (mem x (mapi f m)); destruct (mem x m); simpl; auto; intros. +symmetry; rewrite <- H0; rewrite <- H1; rewrite H; auto. +rewrite <- H; rewrite H1; rewrite H0; auto. +Qed. + +Lemma mapi_o : forall m x (f:key->elt->elt'), + (forall x y e, E.eq x y -> f x e = f y e) -> + find x (mapi f m) = option_map (f x) (find x m). +Proof. +intros. +generalize (find_mapsto_iff (mapi f m) x) (find_mapsto_iff m x) + (fun b => mapi_mapsto_iff m x b H). +destruct (find x (mapi f m)); destruct (find x m); simpl; auto; intros. +rewrite <- H0; rewrite H2; exists e0; rewrite H1; auto. +destruct (H0 e) as [_ H3]. +rewrite H2 in H3. +destruct H3 as (a,(_,H3)); auto. +rewrite H1 in H3; discriminate. +rewrite <- H0; rewrite H2; exists e; rewrite H1; auto. +Qed. + +Lemma map2_1bis : forall (m: t elt)(m': t elt') x + (f:option elt->option elt'->option elt''), + f None None = None -> + find x (map2 f m m') = f (find x m) (find x m'). +Proof. +intros. +case_eq (find x m); intros. +rewrite <- H0. +apply map2_1; auto. +left; exists e; auto. +case_eq (find x m'); intros. +rewrite <- H0; rewrite <- H1. +apply map2_1; auto. +right; exists e; auto. +rewrite H. +case_eq (find x (map2 f m m')); intros; auto. +assert (In x (map2 f m m')) by (exists e; auto). +destruct (map2_2 H3) as [(e0,H4)|(e0,H4)]. +rewrite (find_1 H4) in H0; discriminate. +rewrite (find_1 H4) in H1; discriminate. +Qed. + +Lemma elements_o : forall m x, + find x m = findA (eqb x) (elements m). +Proof. +intros. +assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)). + intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff. +assert (NoDupA (eq_key (elt:=elt)) (elements m)). + apply SortA_NoDupA with (lt_key (elt:=elt)); unfold eq_key, lt_key; intuition eauto. + destruct y; simpl in *. + apply (E.lt_not_eq H0 H1). + exact (elements_3 m). +generalize (fun e => @findA_NoDupA _ _ _ E.eq_sym E.eq_trans eq_dec (elements m) x e H0). +unfold eqb. +destruct (find x m); destruct (findA (fun y : E.t => if eq_dec x y then true else false) (elements m)); + simpl; auto; intros. +symmetry; rewrite <- H1; rewrite <- H; auto. +symmetry; rewrite <- H1; rewrite <- H; auto. +rewrite H; rewrite H1; auto. +Qed. + +Lemma elements_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (elements m). +Proof. +intros. +generalize (mem_in_iff m x)(elements_in_iff m x) + (existsb_exists (fun p => eqb x (fst p)) (elements m)). +destruct (mem x m); destruct (existsb (fun p => eqb x (fst p)) (elements m)); auto; intros. +symmetry; rewrite H1. +destruct H0 as (H0,_). +destruct H0 as (e,He); [ intuition |]. +rewrite InA_alt in He. +destruct He as ((y,e'),(Ha1,Ha2)). +compute in Ha1; destruct Ha1; subst e'. +exists (y,e); split; simpl; auto. +unfold eqb; destruct (eq_dec x y); intuition. +rewrite <- H; rewrite H0. +destruct H1 as (H1,_). +destruct H1 as ((y,e),(Ha1,Ha2)); [intuition|]. +simpl in Ha2. +unfold eqb in *; destruct (eq_dec x y); auto; try discriminate. +exists e; rewrite InA_alt. +exists (y,e); intuition. +compute; auto. +Qed. + +End BoolSpec. + +End Facts. diff --git a/theories/FSets/FMapWeak.v b/theories/FSets/FMapWeak.v index 7bdee004e..a04ace03c 100644 --- a/theories/FSets/FMapWeak.v +++ b/theories/FSets/FMapWeak.v @@ -12,3 +12,4 @@ Require Export DecidableType. Require Export DecidableTypeEx. Require Export FMapWeakInterface. Require Export FMapWeakList. +Require Export FMapWeakFacts.
\ No newline at end of file diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v new file mode 100644 index 000000000..f53e1d2b5 --- /dev/null +++ b/theories/FSets/FMapWeakFacts.v @@ -0,0 +1,583 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(** * Finite maps library *) + +(** This functor derives additional facts from [FMapWeakInterface.S]. These + facts are mainly the specifications of [FMapWeakInterface.S] written using + different styles: equivalence and boolean equalities. +*) + +Require Import Bool. +Require Import OrderedType. +Require Export FMapWeakInterface. +Set Implicit Arguments. +Unset Strict Implicit. + +Module Facts (M: S). +Import M. +Import Logic. (* to unmask [eq] *) +Import Peano. (* to unmask [lt] *) + +Lemma MapsTo_fun : forall (elt:Set) m x (e e':elt), + MapsTo x e m -> MapsTo x e' m -> e=e'. +Proof. +intros. +generalize (find_1 H) (find_1 H0); clear H H0. +intros; rewrite H in H0; injection H0; auto. +Qed. + +(** * Specifications written using equivalences *) + +Section IffSpec. +Variable elt elt' elt'': Set. +Implicit Type m: t elt. +Implicit Type x y z: key. +Implicit Type e: elt. + +Lemma MapsTo_iff : forall m x y e, E.eq x y -> (MapsTo x e m <-> MapsTo y e m). +Proof. +split; apply MapsTo_1; auto. +Qed. + +Lemma In_iff : forall m x y, E.eq x y -> (In x m <-> In y m). +Proof. +unfold In. +split; intros (e0,H0); exists e0. +apply (MapsTo_1 H H0); auto. +apply (MapsTo_1 (E.eq_sym H) H0); auto. +Qed. + +Lemma find_mapsto_iff : forall m x e, MapsTo x e m <-> find x m = Some e. +Proof. +split; [apply find_1|apply find_2]. +Qed. + +Lemma not_find_mapsto_iff : forall m x, ~In x m <-> find x m = None. +Proof. +intros. +generalize (find_mapsto_iff m x); destruct (find x m). +split; intros; try discriminate. +destruct H0. +exists e; rewrite H; auto. +split; auto. +intros; intros (e,H1). +rewrite H in H1; discriminate. +Qed. + +Lemma mem_in_iff : forall m x, In x m <-> mem x m = true. +Proof. +split; [apply mem_1|apply mem_2]. +Qed. + +Lemma not_mem_in_iff : forall m x, ~In x m <-> mem x m = false. +Proof. +intros; rewrite mem_in_iff; destruct (mem x m); intuition. +Qed. + +Lemma equal_iff : forall m m' cmp, Equal cmp m m' <-> equal cmp m m' = true. +Proof. +split; [apply equal_1|apply equal_2]. +Qed. + +Lemma empty_mapsto_iff : forall x e, MapsTo x e (empty elt) <-> False. +Proof. +intuition; apply (empty_1 H). +Qed. + +Lemma empty_in_iff : forall x, In x (empty elt) <-> False. +Proof. +unfold In. +split; [intros (e,H); rewrite empty_mapsto_iff in H|]; intuition. +Qed. + +Lemma is_empty_iff : forall m, Empty m <-> is_empty m = true. +Proof. +split; [apply is_empty_1|apply is_empty_2]. +Qed. + +Lemma add_mapsto_iff : forall m x y e e', + MapsTo y e' (add x e m) <-> + (E.eq x y /\ e=e') \/ + (~E.eq x y /\ MapsTo y e' m). +Proof. +intros. +intuition. +destruct (E.eq_dec x y); [left|right]. +split; auto. +symmetry; apply (MapsTo_fun (e':=e) H); auto. +split; auto; apply add_3 with x e; auto. +subst; auto. +Qed. + +Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m. +Proof. +unfold In; split. +intros (e',H). +destruct (E.eq_dec x y) as [E|E]; auto. +right; exists e'; auto. +apply (add_3 E H). +destruct (E.eq_dec x y) as [E|E]; auto. +intros. +exists e; apply add_1; auto. +intros [H|(e',H)]. +destruct E; auto. +exists e'; apply add_2; auto. +Qed. + +Lemma add_neq_mapsto_iff : forall m x y e e', + ~ E.eq x y -> (MapsTo y e' (add x e m) <-> MapsTo y e' m). +Proof. +split; [apply add_3|apply add_2]; auto. +Qed. + +Lemma add_neq_in_iff : forall m x y e, + ~ E.eq x y -> (In y (add x e m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +apply (add_3 H H0). +apply add_2; auto. +Qed. + +Lemma remove_mapsto_iff : forall m x y e, + MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m. +Proof. +intros. +split; intros. +split. +assert (In y (remove x m)) by (exists e; auto). +intro H1; apply (remove_1 H1 H0). +apply remove_3 with x; auto. +apply remove_2; intuition. +Qed. + +Lemma remove_in_iff : forall m x y, In y (remove x m) <-> ~E.eq x y /\ In y m. +Proof. +unfold In; split. +intros (e,H). +split. +assert (In y (remove x m)) by (exists e; auto). +intro H1; apply (remove_1 H1 H0). +exists e; apply remove_3 with x; auto. +intros (H,(e,H0)); exists e; apply remove_2; auto. +Qed. + +Lemma remove_neq_mapsto_iff : forall m x y e, + ~ E.eq x y -> (MapsTo y e (remove x m) <-> MapsTo y e m). +Proof. +split; [apply remove_3|apply remove_2]; auto. +Qed. + +Lemma remove_neq_in_iff : forall m x y, + ~ E.eq x y -> (In y (remove x m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +apply (remove_3 H0). +apply remove_2; auto. +Qed. + +Lemma elements_mapsto_iff : forall m x e, + MapsTo x e m <-> InA (@eq_key_elt _) (x,e) (elements m). +Proof. +split; [apply elements_1 | apply elements_2]. +Qed. + +Lemma elements_in_iff : forall m x, + In x m <-> exists e, InA (@eq_key_elt _) (x,e) (elements m). +Proof. +unfold In; split; intros (e,H); exists e; [apply elements_1 | apply elements_2]; auto. +Qed. + +Lemma map_mapsto_iff : forall m x b (f : elt -> elt'), + MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m. +Proof. +split. +case_eq (find x m); intros. +exists e. +split. +apply (MapsTo_fun (m:=map f m) (x:=x)); auto. +apply find_2; auto. +assert (In x (map f m)) by (exists b; auto). +destruct (map_2 H1) as (a,H2). +rewrite (find_1 H2) in H; discriminate. +intros (a,(H,H0)). +subst b; auto. +Qed. + +Lemma map_in_iff : forall m x (f : elt -> elt'), + In x (map f m) <-> In x m. +Proof. +split; intros; eauto. +destruct H as (a,H). +exists (f a); auto. +Qed. + +Lemma mapi_in_iff : forall m x (f:key->elt->elt'), + In x (mapi f m) <-> In x m. +Proof. +split; intros; eauto. +destruct H as (a,H). +destruct (mapi_1 f H) as (y,(H0,H1)). +exists (f y a); auto. +Qed. + +(* Unfortunately, we don't have simple equivalences for [mapi] + and [MapsTo]. The only correct one needs compatibility of [f]. *) + +Lemma mapi_inv : forall m x b (f : key -> elt -> elt'), + MapsTo x b (mapi f m) -> + exists a, exists y, E.eq y x /\ b = f y a /\ MapsTo x a m. +Proof. +intros; case_eq (find x m); intros. +exists e. +destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)). +apply find_2; auto. +exists y; repeat split; auto. +apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto. +assert (In x (mapi f m)) by (exists b; auto). +destruct (mapi_2 H1) as (a,H2). +rewrite (find_1 H2) in H0; discriminate. +Qed. + +Lemma mapi_1bis : forall m x e (f:key->elt->elt'), + (forall x y e, E.eq x y -> f x e = f y e) -> + MapsTo x e m -> MapsTo x (f x e) (mapi f m). +Proof. +intros. +destruct (mapi_1 f H0) as (y,(H1,H2)). +replace (f x e) with (f y e) by auto. +auto. +Qed. + +Lemma mapi_mapsto_iff : forall m x b (f:key->elt->elt'), + (forall x y e, E.eq x y -> f x e = f y e) -> + (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m). +Proof. +split. +intros. +destruct (mapi_inv H0) as (a,(y,(H1,(H2,H3)))). +exists a; split; auto. +subst b; auto. +intros (a,(H0,H1)). +subst b. +apply mapi_1bis; auto. +Qed. + +(** Things are even worse for [map2] : we don't try to state any + equivalence, see instead boolean results below. *) + +End IffSpec. + +(** Useful tactic for simplifying expressions like [In y (add x e (remove z m))] *) + +Ltac map_iff := + repeat (progress ( + rewrite add_mapsto_iff || rewrite add_in_iff || + rewrite remove_mapsto_iff || rewrite remove_in_iff || + rewrite empty_mapsto_iff || rewrite empty_in_iff || + rewrite map_mapsto_iff || rewrite map_in_iff || + rewrite mapi_in_iff)). + +(** * Specifications written using boolean predicates *) + +Section BoolSpec. + +Definition eqb x y := if E.eq_dec x y then true else false. + +Lemma mem_find_b : forall (elt:Set)(m:t elt)(x:key), mem x m = if find x m then true else false. +Proof. +intros. +generalize (find_mapsto_iff m x)(mem_in_iff m x); unfold In. +destruct (find x m); destruct (mem x m); auto. +intros. +rewrite <- H0; exists e; rewrite H; auto. +intuition. +destruct H0 as (e,H0). +destruct (H e); intuition discriminate. +Qed. + +Variable elt elt' elt'' : Set. +Implicit Types m : t elt. +Implicit Types x y z : key. +Implicit Types e : elt. + +Lemma mem_b : forall m x y, E.eq x y -> mem x m = mem y m. +Proof. +intros. +generalize (mem_in_iff m x) (mem_in_iff m y)(In_iff m H). +destruct (mem x m); destruct (mem y m); intuition. +Qed. + +Lemma find_o : forall m x y, E.eq x y -> find x m = find y m. +Proof. +intros. +generalize (find_mapsto_iff m x) (find_mapsto_iff m y) (fun e => MapsTo_iff m e H). +destruct (find x m); destruct (find y m); intros. +rewrite <- H0; rewrite H2; rewrite H1; auto. +symmetry; rewrite <- H1; rewrite <- H2; rewrite H0; auto. +rewrite <- H0; rewrite H2; rewrite H1; auto. +auto. +Qed. + +Lemma add_eq_o : forall m x y e, + E.eq x y -> find y (add x e m) = Some e. +Proof. +auto. +Qed. + +Lemma add_neq_o : forall m x y e, + ~ E.eq x y -> find y (add x e m) = find y m. +Proof. +intros. +case_eq (find y m); intros; auto. +case_eq (find y (add x e m)); intros; auto. +rewrite <- H0; symmetry. +apply find_1; apply add_3 with x e; auto. +Qed. +Hint Resolve add_neq_o. + +Lemma add_o : forall m x y e, + find y (add x e m) = if E.eq_dec x y then Some e else find y m. +Proof. +intros; destruct (E.eq_dec x y); auto. +Qed. + +Lemma add_eq_b : forall m x y e, + E.eq x y -> mem y (add x e m) = true. +Proof. +intros; rewrite mem_find_b; rewrite add_eq_o; auto. +Qed. + +Lemma add_neq_b : forall m x y e, + ~E.eq x y -> mem y (add x e m) = mem y m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite add_neq_o; auto. +Qed. + +Lemma add_b : forall m x y e, + mem y (add x e m) = eqb x y || mem y m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite add_o; unfold eqb. +destruct (E.eq_dec x y); simpl; auto. +Qed. + +Lemma remove_eq_o : forall m x y, + E.eq x y -> find y (remove x m) = None. +Proof. +intros. +generalize (remove_1 (m:=m) H). +generalize (find_mapsto_iff (remove x m) y). +destruct (find y (remove x m)); auto. +destruct 2. +exists e; rewrite H0; auto. +Qed. +Hint Resolve remove_eq_o. + +Lemma remove_neq_o : forall m x y, + ~ E.eq x y -> find y (remove x m) = find y m. +Proof. +intros. +case_eq (find y m); intros; auto. +case_eq (find y (remove x m)); intros; auto. +rewrite <- H0; symmetry. +apply find_1; apply remove_3 with x; auto. +Qed. +Hint Resolve remove_neq_o. + +Lemma remove_o : forall m x y, + find y (remove x m) = if E.eq_dec x y then None else find y m. +Proof. +intros; destruct (E.eq_dec x y); auto. +Qed. + +Lemma remove_eq_b : forall m x y, + E.eq x y -> mem y (remove x m) = false. +Proof. +intros; rewrite mem_find_b; rewrite remove_eq_o; auto. +Qed. + +Lemma remove_neq_b : forall m x y, + ~ E.eq x y -> mem y (remove x m) = mem y m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite remove_neq_o; auto. +Qed. + +Lemma remove_b : forall m x y, + mem y (remove x m) = negb (eqb x y) && mem y m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. +destruct (E.eq_dec x y); auto. +Qed. + +Definition option_map (A:Set)(B:Set)(f:A->B)(o:option A) : option B := + match o with + | Some a => Some (f a) + | None => None + end. + +Lemma map_o : forall m x (f:elt->elt'), + find x (map f m) = option_map f (find x m). +Proof. +intros. +generalize (find_mapsto_iff (map f m) x) (find_mapsto_iff m x) + (fun b => map_mapsto_iff m x b f). +destruct (find x (map f m)); destruct (find x m); simpl; auto; intros. +rewrite <- H; rewrite H1; exists e0; rewrite H0; auto. +destruct (H e) as [_ H2]. +rewrite H1 in H2. +destruct H2 as (a,(_,H2)); auto. +rewrite H0 in H2; discriminate. +rewrite <- H; rewrite H1; exists e; rewrite H0; auto. +Qed. + +Lemma map_b : forall m x (f:elt->elt'), + mem x (map f m) = mem x m. +Proof. +intros; do 2 rewrite mem_find_b; rewrite map_o. +destruct (find x m); simpl; auto. +Qed. + +Lemma mapi_b : forall m x (f:key->elt->elt'), + mem x (mapi f m) = mem x m. +Proof. +intros. +generalize (mem_in_iff (mapi f m) x) (mem_in_iff m x) (mapi_in_iff m x f). +destruct (mem x (mapi f m)); destruct (mem x m); simpl; auto; intros. +symmetry; rewrite <- H0; rewrite <- H1; rewrite H; auto. +rewrite <- H; rewrite H1; rewrite H0; auto. +Qed. + +Lemma mapi_o : forall m x (f:key->elt->elt'), + (forall x y e, E.eq x y -> f x e = f y e) -> + find x (mapi f m) = option_map (f x) (find x m). +Proof. +intros. +generalize (find_mapsto_iff (mapi f m) x) (find_mapsto_iff m x) + (fun b => mapi_mapsto_iff m x b H). +destruct (find x (mapi f m)); destruct (find x m); simpl; auto; intros. +rewrite <- H0; rewrite H2; exists e0; rewrite H1; auto. +destruct (H0 e) as [_ H3]. +rewrite H2 in H3. +destruct H3 as (a,(_,H3)); auto. +rewrite H1 in H3; discriminate. +rewrite <- H0; rewrite H2; exists e; rewrite H1; auto. +Qed. + +Lemma map2_1bis : forall (m: t elt)(m': t elt') x + (f:option elt->option elt'->option elt''), + f None None = None -> + find x (map2 f m m') = f (find x m) (find x m'). +Proof. +intros. +case_eq (find x m); intros. +rewrite <- H0. +apply map2_1; auto. +left; exists e; auto. +case_eq (find x m'); intros. +rewrite <- H0; rewrite <- H1. +apply map2_1; auto. +right; exists e; auto. +rewrite H. +case_eq (find x (map2 f m m')); intros; auto. +assert (In x (map2 f m m')) by (exists e; auto). +destruct (map2_2 H3) as [(e0,H4)|(e0,H4)]. +rewrite (find_1 H4) in H0; discriminate. +rewrite (find_1 H4) in H1; discriminate. +Qed. + +Fixpoint findA (A B:Set)(f : A -> bool) (l:list (A*B)) : option B := + match l with + | nil => None + | (a,b)::l => if f a then Some b else findA f l + end. + +Lemma findA_NoDupA : + forall (A B:Set) + (eqA:A->A->Prop) + (eqA_sym: forall a b, eqA a b -> eqA b a) + (eqA_trans: forall a b c, eqA a b -> eqA b c -> eqA a c) + (eqA_dec : forall a a', { eqA a a' }+{~eqA a a' }) + (l:list (A*B))(x:A)(e:B), + NoDupA (fun p p' => eqA (fst p) (fst p')) l -> + (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (x,e) l <-> + findA (fun y:A => if eqA_dec x y then true else false) l = Some e). +Proof. +induction l; simpl; intros. +split; intros; try discriminate. +inversion H0. +destruct a as (y,e'). +inversion_clear H. +split; intros. +inversion_clear H. +simpl in *; destruct H2; subst e'. +destruct (eqA_dec x y); intuition. +destruct (eqA_dec x y); simpl. +destruct H0. +generalize e0 H2 eqA_trans eqA_sym; clear. +induction l. +inversion 2. +inversion_clear 2; intros; auto. +destruct a. +compute in H; destruct H. +subst b. +constructor 1; auto. +simpl. +apply eqA_trans with x; auto. +rewrite <- IHl; auto. +destruct (eqA_dec x y); simpl in *. +inversion H; clear H; intros; subst e'; auto. +constructor 2. +rewrite IHl; auto. +Qed. + +Lemma elements_o : forall m x, + find x m = findA (eqb x) (elements m). +Proof. +intros. +assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)). + intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff. +assert (NoDupA (eq_key (elt:=elt)) (elements m)). + exact (elements_3 m). +generalize (fun e => @findA_NoDupA _ _ _ E.eq_sym E.eq_trans E.eq_dec (elements m) x e H0). +unfold eqb. +destruct (find x m); destruct (findA (fun y : E.t => if E.eq_dec x y then true else false) (elements m)); + simpl; auto; intros. +symmetry; rewrite <- H1; rewrite <- H; auto. +symmetry; rewrite <- H1; rewrite <- H; auto. +rewrite H; rewrite H1; auto. +Qed. + +Lemma elements_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (elements m). +Proof. +intros. +generalize (mem_in_iff m x)(elements_in_iff m x) + (existsb_exists (fun p => eqb x (fst p)) (elements m)). +destruct (mem x m); destruct (existsb (fun p => eqb x (fst p)) (elements m)); auto; intros. +symmetry; rewrite H1. +destruct H0 as (H0,_). +destruct H0 as (e,He); [ intuition |]. +rewrite InA_alt in He. +destruct He as ((y,e'),(Ha1,Ha2)). +compute in Ha1; destruct Ha1; subst e'. +exists (y,e); split; simpl; auto. +unfold eqb; destruct (E.eq_dec x y); intuition. +rewrite <- H; rewrite H0. +destruct H1 as (H1,_). +destruct H1 as ((y,e),(Ha1,Ha2)); [intuition|]. +simpl in Ha2. +unfold eqb in *; destruct (E.eq_dec x y); auto; try discriminate. +exists e; rewrite InA_alt. +exists (y,e); intuition. +compute; auto. +Qed. + +End BoolSpec. + +End Facts. diff --git a/theories/FSets/FMaps.v b/theories/FSets/FMaps.v index d7b29547a..f812e56e8 100644 --- a/theories/FSets/FMaps.v +++ b/theories/FSets/FMaps.v @@ -15,3 +15,4 @@ Require Export FMapInterface. Require Export FMapList. Require Export FMapPositive. Require Export FMapIntMap. +Require Export FMapFacts.
\ No newline at end of file diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index dc9856bc0..f9b28be3a 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -464,3 +464,52 @@ Hint Constructors InA. Hint Constructors NoDupA. Hint Constructors sort. Hint Constructors lelistA. + +Section Find. +Variable A B : Set. +Variable eqA : A -> A -> Prop. +Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x. +Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z. +Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. + +Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B := + match l with + | nil => None + | (a,b)::l => if f a then Some b else findA f l + end. + +Lemma findA_NoDupA : + forall l a b, + NoDupA (fun p p' => eqA (fst p) (fst p')) l -> + (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (a,b) l <-> + findA (fun a' => if eqA_dec a a' then true else false) l = Some b). +Proof. +induction l; simpl; intros. +split; intros; try discriminate. +inversion H0. +destruct a as (a',b'); rename a0 into a. +inversion_clear H. +split; intros. +inversion_clear H. +simpl in *; destruct H2; subst b'. +destruct (eqA_dec a a'); intuition. +destruct (eqA_dec a a'); simpl. +destruct H0. +generalize e H2 eqA_trans eqA_sym; clear. +induction l. +inversion 2. +inversion_clear 2; intros; auto. +destruct a0. +compute in H; destruct H. +subst b. +constructor 1; auto. +simpl. +apply eqA_trans with a; auto. +rewrite <- IHl; auto. +destruct (eqA_dec a a'); simpl in *. +inversion H; clear H; intros; subst b'; auto. +constructor 2. +rewrite IHl; auto. +Qed. + +End Find. |