diff options
| -rw-r--r-- | .depend.coq | 81 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_zdiv.v | 26 | ||||
| -rw-r--r-- | theories/Arith/Max.v | 2 | ||||
| -rw-r--r-- | theories/FSets/OrderedTypeEx.v | 21 | ||||
| -rw-r--r-- | theories/IntMap/Adalloc.v | 10 | ||||
| -rw-r--r-- | theories/NArith/BinNat.v | 54 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 12 | ||||
| -rw-r--r-- | theories/NArith/Ndec.v | 180 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 63 | ||||
| -rw-r--r-- | theories/NArith/Pnat.v | 2 |
10 files changed, 283 insertions, 168 deletions
diff --git a/.depend.coq b/.depend.coq index ac1fadf50..05031eba1 100644 --- a/.depend.coq +++ b/.depend.coq @@ -21,7 +21,7 @@ theories/FSets/FMapWeakFacts.vo: theories/FSets/FMapWeakFacts.v theories/Bool/Bo 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/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo theories/FSets/FMapWeakFacts.vo -theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/FMapInterface.vo +theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo 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/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 @@ -141,7 +141,7 @@ theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v theories/Logic/Decidable theories/Arith/Euclid.vo: theories/Arith/Euclid.v theories/Arith/Mult.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo -theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Arith.vo +theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Le.vo theories/Arith/Bool_nat.vo: theories/Arith/Bool_nat.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Bool/Sumbool.vo theories/Arith/Factorial.vo: theories/Arith/Factorial.v theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Lt.vo theories/Arith/Arith_base.vo: theories/Arith/Arith_base.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 @@ -156,7 +156,7 @@ theories/NArith/BinPos.vo: theories/NArith/BinPos.v theories/Logic/Eqdep_dec.vo theories/NArith/Pnat.vo: theories/NArith/Pnat.v theories/NArith/BinPos.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo theories/NArith/BinNat.vo: theories/NArith/BinNat.v theories/NArith/BinPos.vo theories/NArith/NArith.vo: theories/NArith/NArith.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/NArithRing.vo -theories/NArith/Nnat.vo: theories/NArith/Nnat.v theories/Arith/Arith_base.vo theories/Arith/Compare_dec.vo theories/Bool/Sumbool.vo theories/Arith/Div2.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo +theories/NArith/Nnat.vo: theories/NArith/Nnat.v theories/Arith/Arith_base.vo theories/Arith/Compare_dec.vo theories/Bool/Sumbool.vo theories/Arith/Div2.vo theories/Arith/Min.vo theories/Arith/Max.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo theories/NArith/Ndigits.vo: theories/NArith/Ndigits.v theories/Bool/Bool.vo theories/Bool/Bvector.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Ndec.vo: theories/NArith/Ndec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo theories/NArith/Nnat.vo theories/NArith/Ndigits.vo theories/NArith/Ndist.vo: theories/NArith/Ndist.v theories/Arith/Arith.vo theories/Arith/Min.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Ndigits.vo @@ -242,7 +242,7 @@ theories/FSets/FMapWeakFacts.vo: theories/FSets/FMapWeakFacts.v theories/Bool/Bo 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/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo theories/FSets/FMapWeakFacts.vo -theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/FMapInterface.vo +theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo 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/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 @@ -282,54 +282,6 @@ theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contri theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo theories/Reals/Rpow_def.vo: theories/Reals/Rpow_def.v theories/Reals/Rdefinitions.vo -theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo -theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo -theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo -theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo -theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo -theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/ArithRing.vo -theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo -theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo -theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo -theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo -theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplete.vo theories/Arith/Max.vo -theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo -theories/Reals/Binomial.vo: theories/Reals/Binomial.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo -theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo -theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binomial.vo -theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo -theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo -theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Arith/Max.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo -theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo -theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo -theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo -theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo -theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo -theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo -theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo -theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo -theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo -theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo -theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo -theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo -theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo -theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo -theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo -theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo -theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo -theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo -theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo -theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo -theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo -theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo -theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo -theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo -theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo -theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo -theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo -theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo -theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo -theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Arith/Arith.vo theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo @@ -341,6 +293,31 @@ theories/QArith/Qring.vo: theories/QArith/Qring.v contrib/setoid_ring/Ring.vo th theories/QArith/Qreals.vo: theories/QArith/Qreals.v theories/Reals/Rbase.vo theories/QArith/QArith_base.vo theories/QArith/QArith.vo: theories/QArith/QArith.v theories/QArith/QArith_base.vo theories/QArith/Qring.vo theories/QArith/Qreduction.vo theories/QArith/Qcanon.vo: theories/QArith/Qcanon.v contrib/setoid_ring/Field.vo theories/QArith/QArith.vo theories/ZArith/Znumtheory.vo theories/Logic/Eqdep_dec.vo +theories/Ints/Z/IntsZmisc.vo: theories/Ints/Z/IntsZmisc.v theories/ZArith/ZArith.vo +theories/Ints/Z/Pmod.vo: theories/Ints/Z/Pmod.v theories/Ints/Z/IntsZmisc.vo theories/ZArith/Zwf.vo theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo +theories/Ints/Tactic.vo: theories/Ints/Tactic.v +theories/Ints/Z/ZAux.vo: theories/Ints/Z/ZAux.v contrib/setoid_ring/ArithRing.vo theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo theories/Ints/Tactic.vo +theories/Ints/Z/ZPowerAux.vo: theories/Ints/Z/ZPowerAux.v theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo theories/Ints/Tactic.vo +theories/Ints/Z/ZDivModAux.vo: theories/Ints/Z/ZDivModAux.v theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo theories/Ints/Tactic.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZPowerAux.vo +theories/Ints/Z/Zmod.vo: theories/Ints/Z/Zmod.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo +theories/Ints/Basic_type.vo: theories/Ints/Basic_type.v theories/ZArith/ZArith.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo +theories/Ints/Int31.vo: theories/Ints/Int31.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo +theories/Ints/num/GenBase.vo: theories/Ints/num/GenBase.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Basic_type.vo theories/Logic/JMeq.vo +theories/Ints/num/ZnZ.vo: theories/Ints/num/ZnZ.v theories/Ints/Tactic.vo theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo +theories/Ints/num/GenAdd.vo: theories/Ints/num/GenAdd.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo +theories/Ints/num/GenSub.vo: theories/Ints/num/GenSub.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo +theories/Ints/num/GenMul.vo: theories/Ints/num/GenMul.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo +theories/Ints/num/GenDivn1.vo: theories/Ints/num/GenDivn1.v theories/ZArith/ZArith.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo +theories/Ints/num/GenDiv.vo: theories/Ints/num/GenDiv.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Z/Zmod.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo theories/Ints/num/GenDivn1.vo theories/Ints/num/GenAdd.vo theories/Ints/num/GenSub.vo +theories/Ints/num/GenSqrt.vo: theories/Ints/num/GenSqrt.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo +theories/Ints/num/GenLift.vo: theories/Ints/num/GenLift.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/Zmod.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo +theories/Ints/num/Zn2Z.vo: theories/Ints/num/Zn2Z.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo theories/Ints/num/GenAdd.vo theories/Ints/num/GenSub.vo theories/Ints/num/GenMul.vo theories/Ints/num/GenSqrt.vo theories/Ints/num/GenLift.vo theories/Ints/num/GenDivn1.vo theories/Ints/num/GenDiv.vo theories/Ints/num/ZnZ.vo +theories/Ints/num/Nbasic.vo: theories/Ints/num/Nbasic.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo +theories/Ints/num/NMake.vo: theories/Ints/num/NMake.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo theories/Ints/num/ZnZ.vo theories/Ints/num/Zn2Z.vo theories/Ints/num/Nbasic.vo theories/Ints/num/GenMul.vo theories/Ints/num/GenDivn1.vo +theories/Ints/BigN.vo: theories/Ints/BigN.v theories/Ints/Int31.vo theories/Ints/num/NMake.vo theories/Ints/num/ZnZ.vo +theories/Ints/num/ZMake.vo: theories/Ints/num/ZMake.v theories/ZArith/ZArith.vo +theories/Ints/BigZ.vo: theories/Ints/BigZ.v theories/Ints/BigN.vo theories/Ints/num/ZMake.vo +theories/Ints/num/QMake.vo: theories/Ints/num/QMake.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/Ints/BigN.vo theories/Ints/BigZ.vo contrib/omega/OmegaLemmas.vo: contrib/omega/OmegaLemmas.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/ZArith/Zhints.vo contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/List.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/Logic/Decidable.vo diff --git a/contrib/setoid_ring/Ring_zdiv.v b/contrib/setoid_ring/Ring_zdiv.v index 5b93d50b5..10141b6b4 100644 --- a/contrib/setoid_ring/Ring_zdiv.v +++ b/contrib/setoid_ring/Ring_zdiv.v @@ -11,21 +11,11 @@ Require Import BinPos. Require Import BinNat. Require Import ZArith_base. -Definition Nge a b := +Definition Ngeb a b := match a with N0 => false | Npos na => match Pcompare na b Eq with Lt => false | _ => true end end. -Definition Nminus a b := match a, b with - | N0, _ => N0 - | _ , N0 => a - | Npos na, Npos nb => - match (na - nb)%positive with - xH => match Pcompare na nb Eq with Eq => N0 | _ => Npos xH end - | t => Npos t - end - end. - Fixpoint pdiv_eucl (a b:positive) {struct a} : N * N := match a with | xH => @@ -33,24 +23,24 @@ Fixpoint pdiv_eucl (a b:positive) {struct a} : N * N := | xO a' => let (q, r) := pdiv_eucl a' b in let r' := (2 * r)%N in - if (Nge r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N + if (Ngeb r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N else (2 * q, r')%N | xI a' => let (q, r) := pdiv_eucl a' b in let r' := (2 * r + 1)%N in - if (Nge r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N + if (Ngeb r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N else (2 * q, r')%N end. -Theorem Nge_correct: forall a b, - if Nge a b then a = ((Nminus a (Npos b)) + Npos b)%N else True. +Theorem Ngeb_correct: forall a b, + if Ngeb a b then a = ((Nminus a (Npos b)) + Npos b)%N else True. destruct a; intros; simpl; auto. case_eq (Pcompare p b Eq); intros; auto. rewrite (Pcompare_Eq_eq _ _ H). assert (HH: forall p, Pminus p p = xH). intro p0; unfold Pminus; rewrite Pminus_mask_diag; auto. - rewrite HH; auto. + simpl; auto. generalize (Pplus_minus _ _ H). case (p - b)%positive; intros; subst; unfold Nplus; rewrite Pplus_comm; trivial. @@ -79,7 +69,7 @@ Theorem pdiv_eucl_correct: forall a b, induction a; unfold pdiv_eucl; fold pdiv_eucl. intros b; generalize (IHa b); case pdiv_eucl. intros q1 r1 Hq1. - generalize (Nge_correct (2 * r1 + 1) b); case Nge; intros H. + generalize (Ngeb_correct (2 * r1 + 1) b); case Ngeb; intros H. set (u := Nminus (2 * r1 + 1) (Npos b)) in * |- *. assert (HH: Z_of_N u = (Z_of_N (2 * r1 + 1) - Zpos b)%Z). rewrite H; z_of_n_tac; simpl. @@ -91,7 +81,7 @@ induction a; unfold pdiv_eucl; fold pdiv_eucl. rewrite Zpos_xI; rewrite Hq1; z_of_n_tac; ztac; auto. intros b; generalize (IHa b); case pdiv_eucl. intros q1 r1 Hq1. - generalize (Nge_correct (2 * r1) b); case Nge; intros H. + generalize (Ngeb_correct (2 * r1) b); case Ngeb; intros H. set (u := Nminus (2 * r1) (Npos b)) in * |- *. assert (HH: Z_of_N u = (Z_of_N (2 * r1) - Zpos b)%Z). rewrite H; z_of_n_tac; simpl. diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index a3d658d0c..75e1cdf0c 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require Import Arith. +Require Import Le. Open Local Scope nat_scope. diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index 8da19706e..0295133a6 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -154,16 +154,16 @@ Module N_as_OT <: UsualOrderedType. Definition eq_sym := @sym_eq t. Definition eq_trans := @trans_eq t. - Definition lt p q:= Nle q p = false. + Definition lt p q:= Nleb q p = false. - Definition lt_trans := Nlt_trans. + Definition lt_trans := Nltb_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof. intros; intro. rewrite H0 in H. unfold lt in H. - rewrite Nle_refl in H; discriminate. + rewrite Nleb_refl in H; discriminate. Qed. Definition compare : forall x y : t, Compare lt eq x y. @@ -172,16 +172,15 @@ Module N_as_OT <: UsualOrderedType. case_eq ((x ?= y)%N); intros. apply EQ; apply Ncompare_Eq_eq; auto. apply LT; unfold lt; auto. - generalize (Nle_Ncompare y x). - destruct (Nle y x); auto. - rewrite <- Ncompare_antisym. + generalize (Nleb_Nle y x). + unfold Nle; rewrite <- Ncompare_antisym. destruct (x ?= y)%N; simpl; try discriminate. - intros (H0,_); elim H0; auto. + clear H; intros H. + destruct (Nleb y x); intuition. apply GT; unfold lt. - generalize (Nle_Ncompare x y). - destruct (Nle x y); auto. - destruct (x ?= y)%N; simpl; try discriminate. - intros (H0,_); elim H0; auto. + generalize (Nleb_Nle x y). + unfold Nle; destruct (x ?= y)%N; simpl; try discriminate. + destruct (Nleb x y); intuition. Defined. End N_as_OT. diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v index d475bb54d..ef68b1e5c 100644 --- a/theories/IntMap/Adalloc.v +++ b/theories/IntMap/Adalloc.v @@ -64,20 +64,20 @@ Section AdAlloc. Lemma ad_alloc_opt_optimal_1 : forall (m:Map A) (a:ad), - Nle (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = Some y}. + Nleb (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = Some y}. Proof. induction m as [| a y| m0 H m1 H0]. simpl in |- *. unfold Nle in |- *. simpl in |- *. intros. discriminate H. simpl in |- *. intros b H. elim (sumbool_of_bool (Neqb a N0)). intro H0. rewrite H0 in H. - unfold Nle in H. cut (N0 = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity. + unfold Nleb in H. cut (N0 = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity. rewrite <- (N_of_nat_of_N b). rewrite <- (le_n_O_eq _ (le_S_n _ _ (leb_complete_conv _ _ H))). reflexivity. intro H0. rewrite H0 in H. discriminate H. intros. simpl in H1. elim (Ndouble_or_double_plus_un a). intro H2. elim H2. intros a0 H3. - rewrite H3 in H1. elim (H _ (Nlt_double_mono_conv _ _ (Nmin_lt_3 _ _ _ H1))). intros y H4. + rewrite H3 in H1. elim (H _ (Nltb_double_mono_conv _ _ (Nmin_lt_3 _ _ _ H1))). intros y H4. split with y. rewrite H3. rewrite MapGet_M2_bit_0_0. rewrite Ndouble_div2. assumption. apply Ndouble_bit0. intro H2. elim H2. intros a0 H3. rewrite H3 in H1. - elim (H0 _ (Nlt_double_plus_one_mono_conv _ _ (Nmin_lt_4 _ _ _ H1))). intros y H4. + elim (H0 _ (Nltb_double_plus_one_mono_conv _ _ (Nmin_lt_4 _ _ _ H1))). intros y H4. split with y. rewrite H3. rewrite MapGet_M2_bit_0_1. rewrite Ndouble_plus_one_div2. assumption. apply Ndouble_plus_one_bit0. @@ -85,7 +85,7 @@ Section AdAlloc. Lemma ad_alloc_opt_optimal : forall (m:Map A) (a:ad), - Nle (ad_alloc_opt m) a = false -> in_dom A a m = true. + Nleb (ad_alloc_opt m) a = false -> in_dom A a m = true. Proof. intros. unfold in_dom in |- *. elim (ad_alloc_opt_optimal_1 m a H). intros y H0. rewrite H0. reflexivity. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 0f2782bd9..b26a22c9e 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -70,6 +70,21 @@ Definition Nplus n m := Infix "+" := Nplus : N_scope. +(** Substraction *) + +Definition Nminus (x y:N) := + match x, y with + | N0, _ => N0 + | x, N0 => x + | Npos x', Npos y' => + match Pcompare x' y' Eq with + | Lt | Eq => N0 + | Gt => Npos (x' - y') + end + end. + +Infix "-" := Nminus : N_scope. + (** Multiplication *) Definition Nmult n m := @@ -93,6 +108,28 @@ Definition Ncompare n m := Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. +Definition Nlt (x y:N) := (x ?= y) = Lt. +Definition Ngt (x y:N) := (x ?= y) = Gt. +Definition Nle (x y:N) := (x ?= y) <> Gt. +Definition Nge (x y:N) := (x ?= y) <> Lt. + +Infix "<=" := Nle : N_scope. +Infix "<" := Nlt : N_scope. +Infix ">=" := Nge : N_scope. +Infix ">" := Ngt : N_scope. + +(** Min and max *) + +Definition Nmin (n n' : N) := match Ncompare n n' with + | Lt | Eq => n + | Gt => n' + end. + +Definition Nmax (n n' : N) := match Ncompare n n' with + | Lt | Eq => n' + | Gt => n + end. + (** convenient induction principles *) Lemma N_ind_double : @@ -217,6 +254,23 @@ intro n; pattern n in |- *; apply Nind; clear n; simpl in |- *. apply IHn; apply Nsucc_inj; assumption. Qed. +(** Properties of substraction. *) + +Lemma Nle_Nminus_N0 : forall n n':N, n <= n' -> n-n' = N0. +Proof. + destruct n; destruct n'; simpl; intros; auto. + elim H; auto. + red in H; simpl in *. + intros; destruct (Pcompare p p0 Eq); auto. + elim H; auto. +Qed. + +Lemma Nminus_N0_Nle : forall n n':N, n-n' = N0 -> n <= n'. +Proof. + destruct n; destruct n'; red; simpl; intros; try discriminate. + destruct (Pcompare p p0 Eq); discriminate. +Qed. + (** Properties of multiplication *) Theorem Nmult_0_l : forall n:N, N0 * n = N0. diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index c8c94f781..2e3c6a3a5 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -13,7 +13,7 @@ Unset Boxed Definitions. (**********************************************************************) (** Binary positive numbers *) -(** Original development by Pierre Crégut, CNET, Lannion, France *) +(** Original development by Pierre Crégut, CNET, Lannion, France *) Inductive positive : Set := | xI : positive -> positive @@ -220,6 +220,16 @@ Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison := Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope. +Definition Pmin (p p' : positive) := match Pcompare p p' Eq with + | Lt | Eq => p + | Gt => p' + end. + +Definition Pmax (p p' : positive) := match Pcompare p p' Eq with + | Lt | Eq => p' + | Gt => p + end. + (**********************************************************************) (** Miscellaneous properties of binary positive numbers *) diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index 29ac72d00..bbab81f4e 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -37,6 +37,13 @@ Proof. induction p; destruct p'; simpl; intros; try discriminate; auto. Qed. +Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'. +Proof. + intros. + apply Pcompare_Eq_eq. + apply Peqb_Pcompare; auto. +Qed. + Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true. Proof. intros; rewrite <- (Pcompare_Eq_eq _ _ H). @@ -208,205 +215,220 @@ Qed. (** A boolean order on [N] *) -Definition Nle (a b:N) := leb (nat_of_N a) (nat_of_N b). +Definition Nleb (a b:N) := leb (nat_of_N a) (nat_of_N b). -Lemma Nle_Ncompare : forall a b, Nle a b = true <-> Ncompare a b <> Gt. +Lemma Nleb_Nle : forall a b, Nleb a b = true <-> Nle a b. Proof. - intros; rewrite nat_of_Ncompare. - unfold Nle; apply leb_compare. + intros; unfold Nle; rewrite nat_of_Ncompare. + unfold Nleb; apply leb_compare. Qed. -Lemma Nle_refl : forall a, Nle a a = true. +Lemma Nleb_refl : forall a, Nleb a a = true. Proof. - intro. unfold Nle in |- *. apply leb_correct. apply le_n. + intro. unfold Nleb in |- *. apply leb_correct. apply le_n. Qed. -Lemma Nle_antisym : - forall a b, Nle a b = true -> Nle b a = true -> a = b. +Lemma Nleb_antisym : + forall a b, Nleb a b = true -> Nleb b a = true -> a = b. Proof. - unfold Nle in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b). + unfold Nleb in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b). rewrite (le_antisym _ _ (leb_complete _ _ H) (leb_complete _ _ H0)). reflexivity. Qed. -Lemma Nle_trans : - forall a b c, Nle a b = true -> Nle b c = true -> Nle a c = true. +Lemma Nleb_trans : + forall a b c, Nleb a b = true -> Nleb b c = true -> Nleb a c = true. Proof. - unfold Nle in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b). + unfold Nleb in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b). apply leb_complete. assumption. apply leb_complete. assumption. Qed. -Lemma Nle_lt_trans : +Lemma Nleb_ltb_trans : forall a b c, - Nle a b = true -> Nle c b = false -> Nle c a = false. + Nleb a b = true -> Nleb c b = false -> Nleb c a = false. Proof. - unfold Nle in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b). + unfold Nleb in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b). apply leb_complete. assumption. apply leb_complete_conv. assumption. Qed. -Lemma Nlt_le_trans : +Lemma Nltb_leb_trans : forall a b c, - Nle b a = false -> Nle b c = true -> Nle c a = false. + Nleb b a = false -> Nleb b c = true -> Nleb c a = false. Proof. - unfold Nle in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b). + unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b). apply leb_complete_conv. assumption. apply leb_complete. assumption. Qed. -Lemma Nlt_trans : +Lemma Nltb_trans : forall a b c, - Nle b a = false -> Nle c b = false -> Nle c a = false. + Nleb b a = false -> Nleb c b = false -> Nleb c a = false. Proof. - unfold Nle in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b). + unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b). apply leb_complete_conv. assumption. apply leb_complete_conv. assumption. Qed. -Lemma Nlt_le_weak : forall a b:N, Nle b a = false -> Nle a b = true. +Lemma Nltb_leb_weak : forall a b:N, Nleb b a = false -> Nleb a b = true. Proof. - unfold Nle in |- *. intros. apply leb_correct. apply lt_le_weak. + unfold Nleb in |- *. intros. apply leb_correct. apply lt_le_weak. apply leb_complete_conv. assumption. Qed. -Lemma Nle_double_mono : +Lemma Nleb_double_mono : forall a b, - Nle a b = true -> Nle (Ndouble a) (Ndouble b) = true. + Nleb a b = true -> Nleb (Ndouble a) (Ndouble b) = true. Proof. - unfold Nle in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct. + unfold Nleb in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct. simpl in |- *. apply plus_le_compat. apply leb_complete. assumption. apply plus_le_compat. apply leb_complete. assumption. apply le_n. Qed. -Lemma Nle_double_plus_one_mono : +Lemma Nleb_double_plus_one_mono : forall a b, - Nle a b = true -> - Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = true. + Nleb a b = true -> + Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true. Proof. - unfold Nle in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. + unfold Nleb in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. apply leb_correct. apply le_n_S. simpl in |- *. apply plus_le_compat. apply leb_complete. assumption. apply plus_le_compat. apply leb_complete. assumption. apply le_n. Qed. -Lemma Nle_double_mono_conv : +Lemma Nleb_double_mono_conv : forall a b, - Nle (Ndouble a) (Ndouble b) = true -> Nle a b = true. + Nleb (Ndouble a) (Ndouble b) = true -> Nleb a b = true. Proof. - unfold Nle in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro. + unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro. apply leb_correct. apply (mult_S_le_reg_l 1). apply leb_complete. assumption. Qed. -Lemma Nle_double_plus_one_mono_conv : +Lemma Nleb_double_plus_one_mono_conv : forall a b, - Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = true -> - Nle a b = true. + Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true -> + Nleb a b = true. Proof. - unfold Nle in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. + unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. intro. apply leb_correct. apply (mult_S_le_reg_l 1). apply le_S_n. apply leb_complete. assumption. Qed. -Lemma Nlt_double_mono : +Lemma Nltb_double_mono : forall a b, - Nle a b = false -> Nle (Ndouble a) (Ndouble b) = false. + Nleb a b = false -> Nleb (Ndouble a) (Ndouble b) = false. Proof. - intros. elim (sumbool_of_bool (Nle (Ndouble a) (Ndouble b))). intro H0. - rewrite (Nle_double_mono_conv _ _ H0) in H. discriminate H. + intros. elim (sumbool_of_bool (Nleb (Ndouble a) (Ndouble b))). intro H0. + rewrite (Nleb_double_mono_conv _ _ H0) in H. discriminate H. trivial. Qed. -Lemma Nlt_double_plus_one_mono : +Lemma Nltb_double_plus_one_mono : forall a b, - Nle a b = false -> - Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = false. + Nleb a b = false -> + Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false. Proof. - intros. elim (sumbool_of_bool (Nle (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0. - rewrite (Nle_double_plus_one_mono_conv _ _ H0) in H. discriminate H. + intros. elim (sumbool_of_bool (Nleb (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0. + rewrite (Nleb_double_plus_one_mono_conv _ _ H0) in H. discriminate H. trivial. Qed. -Lemma Nlt_double_mono_conv : +Lemma Nltb_double_mono_conv : forall a b, - Nle (Ndouble a) (Ndouble b) = false -> Nle a b = false. + Nleb (Ndouble a) (Ndouble b) = false -> Nleb a b = false. Proof. - intros. elim (sumbool_of_bool (Nle a b)). intro H0. rewrite (Nle_double_mono _ _ H0) in H. + intros. elim (sumbool_of_bool (Nleb a b)). intro H0. rewrite (Nleb_double_mono _ _ H0) in H. discriminate H. trivial. Qed. -Lemma Nlt_double_plus_one_mono_conv : +Lemma Nltb_double_plus_one_mono_conv : forall a b, - Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = false -> - Nle a b = false. + Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false -> + Nleb a b = false. Proof. - intros. elim (sumbool_of_bool (Nle a b)). intro H0. - rewrite (Nle_double_plus_one_mono _ _ H0) in H. discriminate H. + intros. elim (sumbool_of_bool (Nleb a b)). intro H0. + rewrite (Nleb_double_plus_one_mono _ _ H0) in H. discriminate H. trivial. Qed. -(* A [min] function over [N] *) +(* An alternate [min] function over [N] *) -Definition Nmin (a b:N) := if Nle a b then a else b. +Definition Nmin' (a b:N) := if Nleb a b then a else b. + +Lemma Nmin_Nmin' : forall a b, Nmin a b = Nmin' a b. +Proof. + unfold Nmin, Nmin', Nleb; intros. + rewrite nat_of_Ncompare. + generalize (leb_compare (nat_of_N a) (nat_of_N b)); + destruct (nat_compare (nat_of_N a) (nat_of_N b)); + destruct (leb (nat_of_N a) (nat_of_N b)); intuition. + lapply H1; intros; discriminate. + lapply H1; intros; discriminate. +Qed. Lemma Nmin_choice : forall a b, {Nmin a b = a} + {Nmin a b = b}. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. left. rewrite H. - reflexivity. - intro H. right. rewrite H. reflexivity. + unfold Nmin in *; intros; destruct (Ncompare a b); auto. Qed. -Lemma Nmin_le_1 : forall a b, Nle (Nmin a b) a = true. +Lemma Nmin_le_1 : forall a b, Nleb (Nmin a b) a = true. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. rewrite H. - apply Nle_refl. - intro H. rewrite H. apply Nlt_le_weak. assumption. + intros; rewrite Nmin_Nmin'. + unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H. + apply Nleb_refl. + intro H. rewrite H. apply Nltb_leb_weak. assumption. Qed. -Lemma Nmin_le_2 : forall a b, Nle (Nmin a b) b = true. +Lemma Nmin_le_2 : forall a b, Nleb (Nmin a b) b = true. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. rewrite H. assumption. - intro H. rewrite H. apply Nle_refl. + intros; rewrite Nmin_Nmin'. + unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H. assumption. + intro H. rewrite H. apply Nleb_refl. Qed. Lemma Nmin_le_3 : - forall a b c, Nle a (Nmin b c) = true -> Nle a b = true. + forall a b c, Nleb a (Nmin b c) = true -> Nleb a b = true. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. + intros; rewrite Nmin_Nmin' in *. + unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. assumption. - intro H0. rewrite H0 in H. apply Nlt_le_weak. apply Nle_lt_trans with (b := c); assumption. + intro H0. rewrite H0 in H. apply Nltb_leb_weak. apply Nleb_ltb_trans with (b := c); assumption. Qed. Lemma Nmin_le_4 : - forall a b c, Nle a (Nmin b c) = true -> Nle a c = true. + forall a b c, Nleb a (Nmin b c) = true -> Nleb a c = true. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. - apply Nle_trans with (b := b); assumption. + intros; rewrite Nmin_Nmin' in *. + unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. + apply Nleb_trans with (b := b); assumption. intro H0. rewrite H0 in H. assumption. Qed. Lemma Nmin_le_5 : forall a b c, - Nle a b = true -> Nle a c = true -> Nle a (Nmin b c) = true. + Nleb a b = true -> Nleb a c = true -> Nleb a (Nmin b c) = true. Proof. intros. elim (Nmin_choice b c). intro H1. rewrite H1. assumption. intro H1. rewrite H1. assumption. Qed. Lemma Nmin_lt_3 : - forall a b c, Nle (Nmin b c) a = false -> Nle b a = false. + forall a b c, Nleb (Nmin b c) a = false -> Nleb b a = false. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. + intros; rewrite Nmin_Nmin' in *. + unfold Nmin' in *. intros. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. assumption. - intro H0. rewrite H0 in H. apply Nlt_trans with (b := c); assumption. + intro H0. rewrite H0 in H. apply Nltb_trans with (b := c); assumption. Qed. Lemma Nmin_lt_4 : - forall a b c, Nle (Nmin b c) a = false -> Nle c a = false. + forall a b c, Nleb (Nmin b c) a = false -> Nleb c a = false. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. - apply Nlt_le_trans with (b := b); assumption. + intros; rewrite Nmin_Nmin' in *. + unfold Nmin' in *. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. + apply Nltb_leb_trans with (b := b); assumption. intro H0. rewrite H0 in H. assumption. Qed. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 5465bc692..e19989aed 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -12,6 +12,8 @@ Require Import Arith_base. Require Import Compare_dec. Require Import Sumbool. Require Import Div2. +Require Import Min. +Require Import Max. Require Import BinPos. Require Import BinNat. Require Import Pnat. @@ -108,6 +110,27 @@ Proof. apply N_of_nat_of_N. Qed. +Lemma nat_of_Nminus : + forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat. +Proof. + destruct a; destruct a'; simpl; auto with arith. + case_eq (Pcompare p p0 Eq); simpl; intros. + rewrite (Pcompare_Eq_eq _ _ H); auto with arith. + symmetry; apply not_le_minus_0. + generalize (nat_of_P_lt_Lt_compare_morphism _ _ H); auto with arith. + apply nat_of_P_minus_morphism; auto. +Qed. + +Lemma N_of_minus : + forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nminus. + apply N_of_nat_of_N. +Qed. + Lemma nat_of_Nmult : forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a'). Proof. @@ -175,3 +198,43 @@ Proof. pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). symmetry; apply nat_of_Ncompare. Qed. + +Lemma nat_of_Nmin : + forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). +Proof. + intros; unfold Nmin; rewrite nat_of_Ncompare. + unfold nat_compare. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + simpl; intros; symmetry; auto with arith. + apply min_l; rewrite e; auto with arith. +Qed. + +Lemma N_of_min : + forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nmin. + apply N_of_nat_of_N. +Qed. + +Lemma nat_of_Nmax : + forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a'). +Proof. + intros; unfold Nmax; rewrite nat_of_Ncompare. + unfold nat_compare. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + simpl; intros; symmetry; auto with arith. + apply max_r; rewrite e; auto with arith. +Qed. + +Lemma N_of_max : + forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nmax. + apply N_of_nat_of_N. +Qed. diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index f1c1d72fc..9bec3e994 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -14,7 +14,7 @@ Require Import BinPos. (** Properties of the injection from binary positive numbers to Peano natural numbers *) -(** Original development by Pierre Crégut, CNET, Lannion, France *) +(** Original development by Pierre Crégut, CNET, Lannion, France *) Require Import Le. Require Import Lt. |