From 03c392f24a204be29093166b9c42fa5c485e627c Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 4 Jun 2006 17:59:53 +0000 Subject: Ajout exists! et restructuration/extension des fichiers sur la description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8892 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend.coq | 60 ++- Makefile | 21 +- theories/Init/Logic.v | 32 +- theories/Logic/ChoiceFacts.v | 710 +++++++++++++++++++++++++++++----- theories/Logic/ClassicalChoice.v | 36 +- theories/Logic/ClassicalDescription.v | 122 +++--- theories/Logic/ClassicalFacts.v | 1 + theories/Logic/Classical_Prop.v | 9 + theories/Logic/Diaconescu.v | 220 +++++++++-- theories/Logic/RelationalChoice.v | 13 +- 10 files changed, 999 insertions(+), 225 deletions(-) diff --git a/.depend.coq b/.depend.coq index caa85a2c6..46a2af571 100644 --- a/.depend.coq +++ b/.depend.coq @@ -106,20 +106,22 @@ theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Pred_Type.vo theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v theories/Logic/EqdepFacts.vo -theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v theories/Logic/ClassicalFacts.vo theories/Logic/EqdepFacts.vo +theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo theories/Logic/ClassicalFacts.vo: theories/Logic/ClassicalFacts.v theories/Logic/Hurkens.vo -theories/Logic/ChoiceFacts.vo: theories/Logic/ChoiceFacts.v theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Logic/Decidable.vo theories/Arith/Arith.vo +theories/Logic/ChoiceFacts.vo: theories/Logic/ChoiceFacts.v theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Logic/Decidable.vo theories/Arith/Arith.vo theories/Setoids/Setoid.vo theories/Logic/Berardi.vo: theories/Logic/Berardi.v theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v theories/Logic/EqdepFacts.vo theories/Logic/Decidable.vo: theories/Logic/Decidable.v theories/Logic/JMeq.vo: theories/Logic/JMeq.v theories/Logic/Eqdep.vo -theories/Logic/ClassicalDescription.vo: theories/Logic/ClassicalDescription.v theories/Logic/Classical.vo -theories/Logic/ClassicalChoice.vo: theories/Logic/ClassicalChoice.v theories/Logic/ClassicalDescription.vo theories/Logic/RelationalChoice.vo theories/Logic/ChoiceFacts.vo +theories/Logic/ClassicalChoice.vo: theories/Logic/ClassicalChoice.v theories/Logic/ClassicalUniqueChoice.vo theories/Logic/RelationalChoice.vo theories/Logic/ChoiceFacts.vo +theories/Logic/ClassicalDescription.vo: theories/Logic/ClassicalDescription.v theories/Logic/Classical.vo theories/Logic/ChoiceFacts.vo theories/Setoids/Setoid.vo theories/Logic/RelationalChoice.vo: theories/Logic/RelationalChoice.v theories/Logic/Diaconescu.vo: theories/Logic/Diaconescu.v theories/Logic/ClassicalFacts.vo theories/Logic/ChoiceFacts.vo theories/Bool/Bool.vo theories/Logic/EqdepFacts.vo: theories/Logic/EqdepFacts.v theories/Logic/ProofIrrelevanceFacts.vo: theories/Logic/ProofIrrelevanceFacts.v theories/Logic/EqdepFacts.vo +theories/Logic/ClassicalEpsilon.vo: theories/Logic/ClassicalEpsilon.v theories/Logic/Classical.vo theories/Logic/ChoiceFacts.vo +theories/Logic/ClassicalUniqueChoice.vo: theories/Logic/ClassicalUniqueChoice.v theories/Logic/Classical.vo theories/Setoids/Setoid.vo theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Factorial.vo theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo @@ -240,8 +242,6 @@ theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/ZArith/ZA theories/FSets/FMapIntMap.vo: theories/FSets/FMapIntMap.v theories/Bool/Bool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Allmaps.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FSetToFiniteSet.vo: theories/FSets/FSetToFiniteSet.v theories/Sets/Ensembles.vo theories/Sets/Finite_sets.vo theories/FSets/FSetInterface.vo theories/FSets/FSetProperties.vo theories/FSets/OrderedTypeEx.vo theories/FSets/Int.vo: theories/FSets/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo -theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo -theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/List.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/List.vo @@ -275,6 +275,54 @@ theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base. theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo +theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo +theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo +theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo +theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo +theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo +theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo +theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo +theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo +theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo +theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo +theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplete.vo theories/Arith/Max.vo +theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/Binomial.vo: theories/Reals/Binomial.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo +theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binomial.vo +theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Arith/Max.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo +theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo +theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo +theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo +theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo +theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo +theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo +theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo +theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo +theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo +theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo +theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo +theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo +theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo +theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo +theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo +theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo +theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo +theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo +theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo +theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo +theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo +theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo +theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo +theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Arith/Arith.vo theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo diff --git a/Makefile b/Makefile index 526fdf1e5..d446d5f7f 100644 --- a/Makefile +++ b/Makefile @@ -813,16 +813,17 @@ INITVO=\ init: $(INITVO) LOGICVO=\ - theories/Logic/Hurkens.vo theories/Logic/ProofIrrelevance.vo\ - theories/Logic/Classical.vo theories/Logic/Classical_Type.vo \ - theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo \ - theories/Logic/Classical_Pred_Type.vo theories/Logic/Classical_Prop.vo \ - theories/Logic/ClassicalFacts.vo theories/Logic/ChoiceFacts.vo \ - theories/Logic/Berardi.vo theories/Logic/Eqdep_dec.vo \ - theories/Logic/Decidable.vo theories/Logic/JMeq.vo \ - theories/Logic/ClassicalDescription.vo theories/Logic/ClassicalChoice.vo \ - theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo \ - theories/Logic/EqdepFacts.vo theories/Logic/ProofIrrelevanceFacts.vo + theories/Logic/Hurkens.vo theories/Logic/ProofIrrelevance.vo\ + theories/Logic/Classical.vo theories/Logic/Classical_Type.vo \ + theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo \ + theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo \ + theories/Logic/ClassicalFacts.vo theories/Logic/ChoiceFacts.vo \ + theories/Logic/Berardi.vo theories/Logic/Eqdep_dec.vo \ + theories/Logic/Decidable.vo theories/Logic/JMeq.vo \ + theories/Logic/ClassicalChoice.vo theories/Logic/ClassicalDescription.vo \ + theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo \ + theories/Logic/EqdepFacts.vo theories/Logic/ProofIrrelevanceFacts.vo \ + theories/Logic/ClassicalEpsilon.vo theories/Logic/ClassicalUniqueChoice.vo ARITHVO=\ theories/Arith/Arith.vo theories/Arith/Gt.vo \ diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 4907c93a4..53a526895 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -280,13 +280,35 @@ Qed. Hint Immediate sym_eq sym_not_eq: core v62. -(** Other notations *) +(** Basic definitions about relations and properties *) -Notation "'exists' ! x , P" := - (exists x', (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'') +Definition subrelation (A B : Type) (R R' : A->B->Prop) := + forall x y, R x y -> R' x y. + +Definition singleton (A : Type) (P : A->Prop) (x:A) := + P x /\ forall (x':A), P x' -> x=x'. + +Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y. + +(** Unique existence *) + +Notation "'exists' ! x , P" := (exists x', singleton (fun x => P) x') (at level 200, x ident, right associativity, format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope. -Notation "'exists' ! x : A , P" := - (exists x' : A, (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'') +Notation "'exists' ! x : A , P" := (exists x':A, singleton (fun x:A => P) x') (at level 200, x ident, right associativity, format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope. + +Lemma unique_existence : forall (A:Type) (P:A->Prop), + ((exists x, P x) /\ uniqueness P) <-> (exists! x, P x). +Proof. +intros A P; split. + intros ((x,Hx),Huni); exists x; red; auto. + intros (x,(Hx,Huni)); split. + exists x; assumption. + intros x' x'' Hx' Hx''; transitivity x. + symmetry; auto. + auto. +Qed. + + diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 5180bf5b2..71db456e9 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* GAC_rel and PL_2 |- AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel + +C. 2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker + +D. Derivability of choice for decidable relations with well-ordered codomain + +E. Equivalence of choices on dependent or non dependent functional types + +F. Non contradiction of constructive descriptions wrt functional choices + +G. Definite description transports classical logic to the computational world -Section ChoiceEquivalences. +References: + +[Bell] John L. Bell, Choice principles in intuitionistic set theory, +unpublished. + +[Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic +Type Theories, Mathematical Logic Quarterly, volume 39, 1993. + +[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in +intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. +*) + +Set Implicit Arguments. + +Notation Local "'inhabited' A" := A (at level 10, only parsing). + +(**********************************************************************) +(** *** A. Definitions *) + +(** Choice, reification and description schemes *) + +Section ChoiceSchemes. Variables A B :Type. -Definition RelationalChoice := - forall (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). +Variables P:A->Prop. + +Variables R:A->B->Prop. + +(** **** Constructive choice and description *) + +(** AC_rel *) + +Definition RelationalChoice_on := + forall R:A->B->Prop, + (forall x : A, exists y : B, R x y) -> + (exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y). + +(** AC_fun *) + +Definition FunctionalChoice_on := + forall R:A->B->Prop, + (forall x : A, exists y : B, R x y) -> + (exists f : A->B, forall x : A, R x (f x)). + +(** AC! or Functional Relation Reification (known as Axiom of Unique Choice + in topos theory; also called principle of definite description *) + +Definition FunctionalRelReification_on := + forall R:A->B->Prop, + (forall x : A, exists! y : B, R x y) -> + (exists f : A->B, forall x : A, R x (f x)). + +(** ID_epsilon (constructive version of indefinite description; + combined with proof-irrelevance, it may be connected to + Carlstrøm's type theory with a constructive indefinite description + operator) *) + +Definition ConstructiveIndefiniteDescription_on := + forall P:A->Prop, + (exists x, P x) -> { x:A | P x }. + +(** ID_iota (constructive version of definite description; combined + with proof-irrelevance, it may be connected to Carlstrøm's and + Stenlund's type theory with a constructive definite description + operator) *) + +Definition ConstructiveDefiniteDescription_on := + forall P:A->Prop, + (exists! x, P x) -> { x:A | P x }. + +(** **** Weakly classical choice and description *) -Definition FunctionalChoice := - forall (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y) -> - exists f : A -> B, (forall x:A, R x (f x)). +(** GAC_rel *) -Definition ParamDefiniteDescription := - forall (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) -> - exists f : A -> B, (forall x:A, R x (f x)). +Definition GuardedRelationalChoice_on := + forall P : A->Prop, forall R : A->B->Prop, + (forall x : A, P x -> exists y : B, R x y) -> + (exists R' : A->B->Prop, + subrelation R' R /\ forall x, P x -> exists! y, R' x y). + +(** GAC_fun *) + +Definition GuardedFunctionalChoice_on := + forall P : A->Prop, forall R : A->B->Prop, + inhabited B -> + (forall x : A, P x -> exists y : B, R x y) -> + (exists f : A->B, forall x, P x -> R x (f x)). + +(** GFR_fun *) + +Definition GuardedFunctionalRelReification_on := + forall P : A->Prop, forall R : A->B->Prop, + inhabited B -> + (forall x : A, P x -> exists! y : B, R x y) -> + (exists f : A->B, forall x : A, P x -> R x (f x)). + +(** OAC_rel *) + +Definition OmniscientRelationalChoice_on := + forall R : A->B->Prop, + exists R' : A->B->Prop, + subrelation R' R /\ forall x : A, (exists y : B, R x y) -> exists! y, R' x y. + +(** OAC_fun *) + +Definition OmniscientFunctionalChoice_on := + forall R : A->B->Prop, + inhabited B -> + exists f : A->B, forall x : A, (exists y : B, R x y) -> R x (f x). + +(** D_epsilon *) + +Definition ClassicalIndefiniteDescription := + forall P:A->Prop, + A -> { x:A | (exists x, P x) -> P x }. + +(** D_iota *) + +Definition ClassicalDefiniteDescription := + forall P:A->Prop, + A -> { x:A | (exists! x, P x) -> P x }. + +End ChoiceSchemes. + +(** Generalized schemes *) + +Notation RelationalChoice := + (forall A B, RelationalChoice_on A B). +Notation FunctionalChoice := + (forall A B, FunctionalChoice_on A B). +Notation FunctionalChoiceOnInhabitedSet := + (forall A B, inhabited B -> FunctionalChoice_on A B). +Notation FunctionalRelReification := + (forall A B, FunctionalRelReification_on A B). + +Notation GuardedRelationalChoice := + (forall A B, GuardedRelationalChoice_on A B). +Notation GuardedFunctionalChoice := + (forall A B, GuardedFunctionalChoice_on A B). +Notation GuardedFunctionalRelReification := + (forall A B, GuardedFunctionalRelReification_on A B). + +Notation OmniscientRelationalChoice := + (forall A B, OmniscientRelationalChoice_on A B). +Notation OmniscientFunctionalChoice := + (forall A B, OmniscientFunctionalChoice_on A B). + +Notation ConstructiveDefiniteDescription := + (forall A, ConstructiveDefiniteDescription_on A). +Notation ConstructiveIndefiniteDescription := + (forall A, ConstructiveIndefiniteDescription_on A). + +(** Subclassical schemes *) + +Definition ProofIrrelevance := + forall (A:Prop) (a1 a2:A), a1 = a2. + +Definition IndependenceOfGeneralPremises := + forall (A:Type) (P:A -> Prop) (Q:Prop), + inhabited A -> + (Q -> exists x, P x) -> exists x, Q -> P x. + +Definition SmallDrinker'sParadox := + forall (A:Type) (P:A -> Prop), inhabited A -> + exists x, (exists x, P x) -> P x. + +(**********************************************************************) +(** *** B. AC_rel + PDP = AC_fun + + We show that the functional formulation of the axiom of Choice + (usual formulation in type theory) is equivalent to its relational + formulation (only formulation of set theory) + the axiom of + (parametric) definite description (aka axiom of unique choice) *) + +(** This shows that the axiom of choice can be assumed (under its + relational formulation) without known inconsistency with classical logic, + though definite description conflicts with classical logic *) Lemma description_rel_choice_imp_funct_choice : - ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice. -intros Descr RelCh. -red in |- *; intros R H. -destruct (RelCh R H) as [R' H0]. -destruct (Descr R') as [f H1]. -intro x. -elim (H0 x); intros y [H2 [H3 H4]]; exists y; split; [ exact H3 | exact H4 ]. + forall A B : Type, + FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B. +Proof. +intros A B Descr RelCh R H. +destruct (RelCh R H) as (R',(HR'R,H0)). +destruct (Descr R') as (f,Hf). +firstorder. exists f; intro x. -elim (H0 x); intros y [H2 [H3 H4]]. -rewrite <- (H4 (f x) (H1 x)). -exact H2. +destruct (H0 x) as (y,(HR'xy,Huniq)). +rewrite <- (Huniq (f x) (Hf x)). +apply HR'R; assumption. Qed. -Lemma funct_choice_imp_rel_choice : FunctionalChoice -> RelationalChoice. -intros FunCh. -red in |- *; intros R H. -destruct (FunCh R H) as [f H0]. -exists (fun x y => y = f x). -intro x; exists (f x); split; - [ apply H0 - | split; [ reflexivity | intros y H1; symmetry in |- *; exact H1 ] ]. +Lemma funct_choice_imp_rel_choice : + forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B. +Proof. +intros A B FunCh R H. +destruct (FunCh R H) as (f,H0). +exists (fun x y => f x = y). +split. + intros x y Heq; rewrite <- Heq; trivial. + intro x; exists (f x); split. + reflexivity. + trivial. Qed. -Lemma funct_choice_imp_description : - FunctionalChoice -> ParamDefiniteDescription. -intros FunCh. -red in |- *; intros R H. +Lemma funct_choice_imp_description : + forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B. +Proof. +intros A B FunCh R H. destruct (FunCh R) as [f H0]. (* 1 *) intro x. -elim (H x); intros y [H0 H1]. -exists y; exact H0. +destruct (H x) as (y,(HRxy,_)). +exists y; exact HRxy. (* 2 *) exists f; exact H0. Qed. Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr : - FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription. -split. + forall A B, FunctionalChoice_on A B <-> + RelationalChoice_on A B /\ FunctionalRelReification_on A B. +Proof. +intros A B; split. intro H; split; [ exact (funct_choice_imp_rel_choice H) | exact (funct_choice_imp_description H) ]. intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H). Qed. -End ChoiceEquivalences. +(**********************************************************************) +(** *** C. Connection between the guarded, non guarded and descriptive choices and *) (** We show that the guarded relational formulation of the axiom of Choice comes from the non guarded formulation in presence either of the independance of premises or proof-irrelevance *) -Definition GuardedRelationalChoice (A B:Type) := - forall (P:A -> Prop) (R:A -> B -> Prop), - (forall x:A, P x -> exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - P x -> - exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). - -Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. +(**********************************************************************) +(** **** C. 1. AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *) Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : - (forall A B, RelationalChoice A B) - -> ProofIrrelevance -> (forall A B, GuardedRelationalChoice A B). + RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice. Proof. intros rel_choice proof_irrel. red in |- *; intros A B P R H. -destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0]. -intros [x HPx]. -destruct (H x HPx) as [y HRxy]. +destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)). +intros (x,HPx). +destruct (H x HPx) as (y,HRxy). exists y; exact HRxy. set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). -exists R''; intros x HPx. -destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]]. -exists y. split. - exact HRxy. - split. - red in |- *; exists HPx; exact HR'xy. - intros y' HR''xy'. +exists R''; split. + intros x y (HPx,HR'xy). + change x with (projT1 (existT P x HPx)); apply HR'R; exact HR'xy. + intros x HPx. + destruct (H0 (existT P x HPx)) as (y,(HR'xy,Huniq)). + exists y; split. exists HPx; exact HR'xy. + intros y' (H'Px,HR'xy'). apply Huniq. - unfold R'' in HR''xy'. - destruct HR''xy' as [H'Px HR'xy']. - rewrite proof_irrel with (a1 := HPx) (a2 := H'Px). - exact HR'xy'. + rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'. Qed. -Definition IndependenceOfGeneralPremises := - forall (A:Type) (P:A -> Prop) (Q:Prop), - (Q -> exists x, P x) -> exists x, Q -> P x. - Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice : - forall A B, RelationalChoice A B -> - IndependenceOfGeneralPremises -> GuardedRelationalChoice A B. -Proof. -intros A B RelCh IndPrem. -red in |- *; intros P R H. -destruct (RelCh (fun x y => P x -> R x y)) as [R' H0]. - intro x. apply IndPrem. - apply H. - exists R'. - intros x HPx. - destruct (H0 x) as [y [H1 H2]]. - exists y. split. - apply (H1 HPx). - exact H2. + forall A B, inhabited B -> RelationalChoice_on A B -> + IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B. +Proof. +intros A B Inh AC_rel IndPrem P R H. +destruct (AC_rel (fun x y => P x -> R x y)) as (R',(HR'R,H0)). + intro x. apply IndPrem. exact Inh. intro Hx. + apply H; assumption. + exists (fun x y => P x /\ R' x y). + firstorder. +Qed. + +Lemma guarded_rel_choice_imp_rel_choice : + forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B. +Proof. +intros A B GAC_rel R H. +destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)). + firstorder. +exists R'; firstorder. Qed. +(** OAC_rel = GAC_rel *) + +Lemma guarded_iff_omniscient_rel_choice : + GuardedRelationalChoice <-> OmniscientRelationalChoice. +Proof. +split. + intros GAC_rel A B R. + apply (GAC_rel A B (fun x => exists y, R x y) R); auto. + intros OAC_rel A B P R H. + destruct (OAC_rel A B R) as (f,Hf); exists f; firstorder. +Qed. + +(**********************************************************************) +(** **** C. 2. AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker *) + +(** AC_fun + IGP = GAC_fun *) + +Lemma guarded_fun_choice_imp_indep_of_general_premises : + GuardedFunctionalChoice -> IndependenceOfGeneralPremises. +Proof. +intros GAC_fun A P Q Inh H. +destruct (GAC_fun unit A (fun _ => Q) (fun _ => P) Inh) as (f,Hf). +tauto. +exists (f tt); auto. +Qed. + +Lemma guarded_fun_choice_imp_fun_choice : + GuardedFunctionalChoice -> FunctionalChoiceOnInhabitedSet. +Proof. +intros GAC_fun A B Inh R H. +destruct (GAC_fun A B (fun _ => True) R Inh) as (f,Hf). +firstorder. +exists f; auto. +Qed. + +Lemma fun_choice_and_indep_general_prem_imp_guarded_fun_choice : + FunctionalChoiceOnInhabitedSet -> IndependenceOfGeneralPremises + -> GuardedFunctionalChoice. +Proof. +intros AC_fun IndPrem A B P R Inh H. +apply (AC_fun A B Inh (fun x y => P x -> R x y)). +intro x; apply IndPrem; eauto. +Qed. + +(** AC_fun + Drinker = OAC_fun *) + +(** This was already observed by Bell [Bell] *) + +Lemma omniscient_fun_choice_imp_small_drinker : + OmniscientFunctionalChoice -> SmallDrinker'sParadox. +Proof. +intros OAC_fun A P Inh. +destruct (OAC_fun unit A (fun _ => P)) as (f,Hf). +auto. +exists (f tt); firstorder. +Qed. + +Lemma omniscient_fun_choice_imp_fun_choice : + OmniscientFunctionalChoice -> FunctionalChoiceOnInhabitedSet. +Proof. +intros OAC_fun A B Inh R H. +destruct (OAC_fun A B R Inh) as (f,Hf). +exists f; firstorder. +Qed. + +Lemma fun_choice_and_small_drinker_imp_omniscient_fun_choice : + FunctionalChoiceOnInhabitedSet -> SmallDrinker'sParadox + -> OmniscientFunctionalChoice. +Proof. +intros AC_fun Drinker A B R Inh. +destruct (AC_fun A B Inh (fun x y => (exists y, R x y) -> R x y)) as (f,Hf). + intro x; apply (Drinker B (R x) Inh). + exists f; assumption. +Qed. + +(** OAC_fun = GAC_fun *) + +(** This is derivable from the intuitionistic equivalence between IGP and Drinker +but we give a direct proof *) + +Lemma guarded_iff_omniscient_fun_choice : + GuardedFunctionalChoice <-> OmniscientFunctionalChoice. +Proof. +split. + intros GAC_fun A B R Inh. + apply (GAC_fun A B (fun x => exists y, R x y) R); auto. + intros OAC_fun A B P R Inh H. + destruct (OAC_fun A B R Inh) as (f,Hf). + exists f; firstorder. +Qed. + +(**********************************************************************) +(** *** D. Derivability of choice for decidable relations with well-ordered codomain *) (** Countable codomains, such as [nat], can be equipped with a well-order, which implies the existence of a least element on inhabited decidable subsets. As a consequence, the relational form of the axiom of choice is derivable on [nat] for decidable relations. - We show instead that definite description and the functional form - of the axiom of choice are equivalent on decidable relation with [nat] - as codomain + We show instead that functional relation reification and the + functional form of the axiom of choice are equivalent on decidable + relation with [nat] as codomain *) Require Import Wf_nat. @@ -163,12 +462,11 @@ Require Import Decidable. Require Import Arith. Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) := - (exists x, (P x /\ forall x', P x' -> R x x') - /\ forall x', P x' /\ (forall x'', P x'' -> R x' x'') -> x=x'). + exists! x, P x /\ forall x', P x' -> R x x'. Lemma dec_inh_nat_subset_has_unique_least_element : forall P:nat->Prop, (forall n, P n \/ ~ P n) -> - (exists n, P n) -> has_unique_least_element nat le P. + (exists n, P n) -> has_unique_least_element le P. Proof. intros P Pdec (n0,HPn0). assert @@ -194,30 +492,228 @@ assert assumption. destruct H0. rewrite Heqn; assumption. -destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0]; - repeat split; + destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0]; + repeat split; assumption || intros n' (HPn',Hminn'); apply le_antisym; auto. Qed. -Definition FunctionalChoice_on (A B:Type) (R:A->B->Prop) := - (forall x:A, exists y : B, R x y) -> - exists f : A -> B, (forall x:A, R x (f x)). +Definition FunctionalChoice_on_rel (A B:Type) (R:A->B->Prop) := + (forall x:A, exists y : B, R x y) -> + exists f : A -> B, (forall x:A, R x (f x)). Lemma classical_denumerable_description_imp_fun_choice : forall A:Type, - ParamDefiniteDescription A nat -> - forall R, (forall x y, decidable (R x y)) -> FunctionalChoice_on A nat R. + FunctionalRelReification_on A nat -> + forall R:A->nat->Prop, + (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R. Proof. intros A Descr. red in |- *; intros R Rdec H. set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y'). -destruct (Descr R') as [f Hf]. +destruct (Descr R') as (f,Hf). intro x. apply (dec_inh_nat_subset_has_unique_least_element (R x)). apply Rdec. apply (H x). exists f. intros x. -destruct (Hf x) as [Hfx _]. +destruct (Hf x) as (Hfx,_). +assumption. +Qed. + +(**********************************************************************) +(** *** E. Choice on dependent and non dependent function types are equivalent *) + +(** **** E. 1. Choice on dependent and non dependent function types are equivalent *) + +Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) := + forall R:forall x:A, B x -> Prop, + (forall x:A, exists y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). + +Notation DependentFunctionalChoice := + (forall A (B:A->Type), DependentFunctionalChoice_on B). + +(** The easy part *) + +Theorem dep_non_dep_functional_choice : + DependentFunctionalChoice -> FunctionalChoice. +Proof. +intros AC_depfun A B R H. + destruct (AC_depfun A (fun _ => B) R H) as (f,Hf). + exists f; trivial. +Qed. + +(** Deriving choice on product types requires some computation on + singleton propositional types, so we need computational + conjunction projections and dependent elimination of conjunction + and equality *) + +Scheme and_indd := Induction for and Sort Prop. +Scheme eq_indd := Induction for eq Sort Prop. + +Definition proj1_inf (A B:Prop) (p : A/\B) := + let (a,b) := p in a. + +Theorem non_dep_dep_functional_choice : + FunctionalChoice -> DependentFunctionalChoice. +Proof. +intros AC_fun A B R H. +pose (B' := { x:A & B x }). +pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). +destruct (AC_fun A B' R') as (f,Hf). +intros x. destruct (H x) as (y,Hy). +exists (existT (fun x => B x) x y). split; trivial. +exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))). +intro x; destruct (Hf x) as (Heq,HR) using and_indd. +destruct (f x); simpl in *. +destruct Heq using eq_indd; trivial. +Qed. + +(** **** E. 2. Reification of dependent and non dependent functional relation are equivalent *) + +Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := + forall (R:forall x:A, B x -> Prop), + (forall x:A, exists! y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). + +Notation DependentFunctionalRelReification := + (forall A (B:A->Type), DependentFunctionalRelReification_on B). + +(** The easy part *) + +Theorem dep_non_dep_functional_rel_reification : + DependentFunctionalRelReification -> FunctionalRelReification. +Proof. +intros DepFunReify A B R H. + destruct (DepFunReify A (fun _ => B) R H) as (f,Hf). + exists f; trivial. +Qed. + +(** Deriving choice on product types requires some computation on + singleton propositional types, so we need computational + conjunction projections and dependent elimination of conjunction + and equality *) + +Theorem non_dep_dep_functional_rel_reification : + FunctionalRelReification -> DependentFunctionalRelReification. +Proof. +intros AC_fun A B R H. +pose (B' := { x:A & B x }). +pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). +destruct (AC_fun A B' R') as (f,Hf). +intros x. destruct (H x) as (y,(Hy,Huni)). + exists (existT (fun x => B x) x y). repeat split; trivial. + intros (x',y') (Heqx',Hy'). + simpl in *. + destruct Heqx'. + rewrite (Huni y'); trivial. +exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))). +intro x; destruct (Hf x) as (Heq,HR) using and_indd. +destruct (f x); simpl in *. +destruct Heq using eq_indd; trivial. +Qed. + +(**********************************************************************) +(** *** F. Non contradiction of constructive descriptions wrt functional axioms of choice *) + +(** **** F. 1. Non contradiction of indefinite description *) + +Lemma relative_non_contradiction_of_indefinite_desc : + (ConstructiveIndefiniteDescription -> False) + -> (FunctionalChoice -> False). +Proof. +intros H AC_fun. +assert (AC_depfun := non_dep_dep_functional_choice AC_fun). +pose (A0 := { A:Type & { P:A->Prop & exists x, P x }}). +pose (B0 := fun x:A0 => projT1 x). +pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y). +pose (H0 := fun x:A0 => projT2 (projT2 x)). +destruct (AC_depfun A0 B0 R0 H0) as (f, Hf). +apply H. +intros A P H'. +exists (f (existT (fun _ => sigT _) A + (existT (fun P => exists x, P x) P H'))). +pose (Hf' := + Hf (existT (fun _ => sigT _) A + (existT (fun P => exists x, P x) P H'))). assumption. Qed. + +Lemma constructive_indefinite_descr_fun_choice : + ConstructiveIndefiniteDescription -> FunctionalChoice. +Proof. +intros IndefDescr A B R H. +exists (fun x => proj1_sig (IndefDescr B (R x) (H x))). +intro x. +apply (proj2_sig (IndefDescr B (R x) (H x))). +Qed. + +(** **** F. 2. Non contradiction of definite description *) + +Lemma relative_non_contradiction_of_definite_descr : + (ConstructiveDefiniteDescription -> False) + -> (FunctionalRelReification -> False). +Proof. +intros H FunReify. +assert (DepFunReify := non_dep_dep_functional_rel_reification FunReify). +pose (A0 := { A:Type & { P:A->Prop & exists! x, P x }}). +pose (B0 := fun x:A0 => projT1 x). +pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y). +pose (H0 := fun x:A0 => projT2 (projT2 x)). +destruct (DepFunReify A0 B0 R0 H0) as (f, Hf). +apply H. +intros A P H'. +exists (f (existT (fun _ => sigT _) A + (existT (fun P => exists! x, P x) P H'))). +pose (Hf' := + Hf (existT (fun _ => sigT _) A + (existT (fun P => exists! x, P x) P H'))). +assumption. +Qed. + +Lemma constructive_definite_descr_fun_reification : + ConstructiveDefiniteDescription -> FunctionalRelReification. +Proof. +intros DefDescr A B R H. +exists (fun x => proj1_sig (DefDescr B (R x) (H x))). +intro x. +apply (proj2_sig (DefDescr B (R x) (H x))). +Qed. + +(**********************************************************************) +(** *** G. Excluded-middle + definite description => computational excluded-middle *) + +(** The idea for the following proof comes from [ChicliPottierSimpson02] *) + +(** Classical logic and axiom of unique choice (i.e. functional + relation reification), as shown in [ChicliPottierSimpson02], + implies the double-negation of excluded-middle in [Set] (which is + incompatible with the impredicativity of [Set]). + + We adapt the proof to show that constructive definite description + transports excluded-middle from [Prop] to [Set]. + + [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos + Simpson, Mathematical Quotients and Quotient Types in Coq, + Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, + Springer Verlag. *) + +Require Import Setoid. + +Theorem constructive_definite_descr_excluded_middle : + ConstructiveDefiniteDescription -> + (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}). +Proof. +intros Descr EM P. +pose (select := fun b:bool => if b then P else ~P). +assert { b:bool | select b } as ([|],HP). + apply Descr. + rewrite <- unique_existence; split. + destruct (EM P). + exists true; trivial. + exists false; trivial. + intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction. +left; trivial. +right; trivial. +Qed. diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 5b347b1be..51f1b3eff 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -8,26 +8,38 @@ (*i $Id$ i*) -(** This file provides classical logic and functional choice *) +(** This file provides classical logic, and functional choice *) -(** This file extends ClassicalDescription.v with the axiom of choice. - As ClassicalDescription.v, it implies the double-negation of - excluded-middle in Set and implies a strongly classical - world. Especially it conflicts with impredicativity of Set, knowing - that [true<>false] in Set. -*) +(** This file extends ClassicalUniqueChoice.v with the axiom of choice. + As ClassicalUniqueChoice.v, it implies the double-negation of + excluded-middle in [Set] and leads to a classical world populated + with non computable functions. Especially it conflicts with the + impredicativity of [Set], knowing that [true<>false] in [Set]. *) -Require Export ClassicalDescription. +Require Export ClassicalUniqueChoice. Require Export RelationalChoice. Require Import ChoiceFacts. +Set Implicit Arguments. + +Definition subset (U:Type) (P Q:U->Prop) : Prop := forall x, P x -> Q x. + +Theorem singleton_choice : + forall (A : Type) (P : A->Prop), + (exists x : A, P x) -> exists P' : A->Prop, subset P' P /\ exists! x, P' x. +Proof. +intros A P H. +destruct (relational_choice unit A (fun _ => P) (fun _ => H)) as (R',(Hsub,HR')). +exists (R' tt); firstorder. +Qed. + Theorem choice : - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y) -> - exists f : A -> B, (forall x:A, R x (f x)). + forall (A B : Type) (R : A->B->Prop), + (forall x : A, exists y : B, R x y) -> + exists f : A->B, (forall x : A, R x (f x)). Proof. intros A B. apply description_rel_choice_imp_funct_choice. -exact (description A B). +exact (unique_choice A B). exact (relational_choice A B). Qed. diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 2f175981f..2e15732ef 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -10,69 +10,91 @@ (** This file provides classical logic and definite description *) -(** Classical logic and definite description, as shown in [1], - implies the double-negation of excluded-middle in Set, hence it - implies a strongly classical world. Especially it conflicts with - impredicativity of Set, knowing that true<>false in Set. +(** Classical definite description operator (i.e. iota) implies + excluded-middle in [Set] and leads to a classical world populated + with non computable functions. It conflicts with the + impredicativity of [Set] *) - [1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical - Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, - Lecture Notes in Computer Science 2646, Springer Verlag. -*) +Set Implicit Arguments. Require Export Classical. +Require Import ChoiceFacts. -Axiom - dependent_description : - forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), - (forall x:A, - exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) -> - exists f : forall x:A, B x, (forall x:A, R x (f x)). +Notation Local "'inhabited' A" := A (at level 200, only parsing). + +Axiom constructive_definite_description : + forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }. + +(** The idea for the following proof comes from [ChicliPottierSimpson02] *) + +Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}. +Proof. +apply + (constructive_definite_descr_excluded_middle + constructive_definite_description classic). +Qed. + +Theorem classical_definite_description : + forall (A : Type) (P : A->Prop), inhabited A -> + { x : A | (exists! x : A, P x) -> P x }. +Proof. +intros A P i. +destruct (excluded_middle_informative (exists! x, P x)) as [Hex|HnonP]. + apply constructive_definite_description with (P:= fun x => (exists! x : A, P x) -> P x). + destruct Hex as (x,(Hx,Huni)). + exists x; split. + intros _; exact Hx. + firstorder. +exists i; tauto. +Qed. + +(** Church's iota operator *) -(** Principle of definite descriptions (aka axiom of unique choice) *) +Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A + := proj1_sig (classical_definite_description P i). + +Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : + (exists! x:A, P x) -> P (iota i P) + := proj2_sig (classical_definite_description P i). + +(** Weaker lemmas (compatibility lemmas) *) + +Unset Implicit Arguments. + +Lemma dependent_description : + forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), + (forall x:A, exists! y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). +Proof. +intros A B R H. +assert (Hexuni:forall x, exists! y, R x y). + intro x. apply H. +exists (fun x => proj1_sig (constructive_definite_description (R x) (Hexuni x))). +intro x. +apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))). +Qed. Theorem description : forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) -> - exists f : A -> B, (forall x:A, R x (f x)). + (forall x : A, exists! y : B, R x y) -> + (exists f : A->B, forall x:A, R x (f x)). Proof. intros A B. apply (dependent_description A (fun _ => B)). Qed. -(** The followig proof comes from [1] *) +(** Axiom of unique "choice" (functional reification of functional relations) *) + +Set Implicit Arguments. -Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False. +Require Import Setoid. + +Theorem unique_choice : + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists! y : B, R x y) -> + (exists f : A -> B, forall x:A, R x (f x)). Proof. -intro HnotEM. -set (R := fun A b => A /\ true = b \/ ~ A /\ false = b). -assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))). -apply description. -intro A. -destruct (classic A) as [Ha| Hnota]. - exists true; split. - left; split; [ assumption | reflexivity ]. - intros y [[_ Hy]| [Hna _]]. - assumption. - contradiction. - exists false; split. - right; split; [ assumption | reflexivity ]. - intros y [[Ha _]| [_ Hy]]. - contradiction. - assumption. -destruct H as [f Hf]. -apply HnotEM. -intro P. -assert (HfP := Hf P). -(* Elimination from Hf to Set is not allowed but from f to Set yes ! *) -destruct (f P). - left. - destruct HfP as [[Ha _]| [_ Hfalse]]. - assumption. - discriminate. - right. - destruct HfP as [[_ Hfalse]| [Hna _]]. - discriminate. - assumption. +intros A B R H. +apply (description A B). +intro x. apply H. Qed. - diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 7edd66708..e3307d53f 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* Q) -> P) -> P]. + Thanks to [forall P, False -> P], it is equivalent to the + following form *) + +Lemma Peirce : forall P:Prop, ((P -> False) -> P) -> P. +Proof. +intros P H; destruct (classic P); auto. +Qed. + Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P. Proof. intros; apply NNPP; red in |- *. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 5f7112fd7..6b825d47a 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* AC_ext, + Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) -Section PredExt_GuardRelChoice_imp_EM. +(**********************************************************************) +(** *** A. Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) + +Section PredExt_RelChoice_imp_EM. (** The axiom of extensionality for predicates *) @@ -59,15 +80,9 @@ Qed. Require Import ChoiceFacts. -Variable rel_choice : forall A B:Type, RelationalChoice A B. +Variable rel_choice : RelationalChoice. -Lemma guarded_rel_choice : - forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop), - (forall x:A, P x -> exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - P x -> - exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). +Lemma guarded_rel_choice : GuardedRelationalChoice. Proof. apply (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel). @@ -78,16 +93,19 @@ Qed. Require Import Bool. -Lemma AC : +Lemma AC_bool_subset_to_bool : exists R : (bool -> Prop) -> bool -> Prop, (forall P:bool -> Prop, (exists b : bool, P b) -> exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')). Proof. - apply guarded_rel_choice with - (P := fun Q:bool -> Prop => exists y : _, Q y) - (R := fun (Q:bool -> Prop) (y:bool) => Q y). - exact (fun _ H => H). + destruct (guarded_rel_choice _ _ + (fun Q:bool -> Prop => exists y : _, Q y) + (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)). + exact (fun _ H => H). + exists R; intros P HP. + destruct (HR P HP) as (y,(Hy,Huni)). + exists y; firstorder. Qed. (** The proof of the excluded middle *) @@ -98,7 +116,7 @@ Proof. intro P. (** first we exhibit the choice functional relation R *) -destruct AC as [R H]. +destruct AC_bool_subset_to_bool as [R H]. set (class_of_true := fun b => b = true \/ P). set (class_of_false := fun b => b = false \/ P). @@ -135,4 +153,152 @@ left; assumption. Qed. -End PredExt_GuardRelChoice_imp_EM. +End PredExt_RelChoice_imp_EM. + +(**********************************************************************) +(** *** B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *) + +(** This is an adaptation of Diaconescu's paradox exploiting that + proof-irrelevance is some form of extensionality *) + +Section ProofIrrel_RelChoice_imp_EqEM. + +Variable rel_choice : RelationalChoice. + +Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y. + +(** Let [a1] and [a2] be two elements in some type [A] *) + +Variable A :Type. +Variables a1 a2 : A. + +(** We build the subset [A'] of [A] made of [a1] and [a2] *) + +Definition A' := sigT (fun x => x=a1 \/ x=a2). + +Definition a1':A'. +exists a1 ; auto. +Defined. + +Definition a2':A'. +exists a2 ; auto. +Defined. + +(** By proof-irrelevance, projection is a retraction *) + +Lemma projT1_injective : a1=a2 -> a1'=a2'. +Proof. + intro Heq ; unfold a1', a2', A'. + rewrite Heq. + replace (or_introl (a2=a2) (refl_equal a2)) + with (or_intror (a2=a2) (refl_equal a2)). + reflexivity. + apply proof_irrelevance. +Qed. + +(** But from the actual proofs of being in [A'], we can assert in the + proof-irrelevant world the existence of relevant boolean witnesses *) + +Lemma decide : forall x:A', exists y:bool , + (projT1 x = a1 /\ y = true ) \/ (projT1 x = a2 /\ y = false). +Proof. + intros [a [Ha1|Ha2]]; [exists true | exists false]; auto. +Qed. + +(** Thanks to the axiom of choice, the boolean witnesses move from the + propositional world to the relevant world *) + +Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2. +Proof. + destruct + (rel_choice A' bool + (fun x y => projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false)) + as (R,(HRsub,HR)). + apply decide. + destruct (HR a1') as (b1,(Ha1'b1,_Huni1)). + destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)]. + destruct (HR a2') as (b2,(Ha2'b2,Huni2)). + destruct (HRsub a2' b2 Ha2'b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)]. + left; symmetry; assumption. + right; intro H. + subst b1; subst b2. + rewrite (projT1_injective H) in Ha1'b1. + assert (false = true) by auto using Huni2. + discriminate. + left; assumption. +Qed. + +(** An alternative more concise proof can be done by directly using + the guarded relational choice *) + +Declare Implicit Tactic auto. + +Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2. +Proof. + assert (decide: forall x:A, x=a1 \/ x=a2 -> + exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false). + intros a [Ha1|Ha2]; [exists true | exists false]; auto. + assert (guarded_rel_choice := + rel_choice_and_proof_irrel_imp_guarded_rel_choice + rel_choice + proof_irrelevance). + destruct + (guarded_rel_choice A bool + (fun x => x=a1 \/ x=a2) + (fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false)) + as (R,(HRsub,HR)). + apply decide. + destruct (HR a1) as (b1,(Ha1b1,_Huni1)). left; reflexivity. + destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)]. + destruct (HR a2) as (b2,(Ha2b2,Huni2)). right; reflexivity. + destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)]. + left; symmetry; assumption. + right; intro H. + subst b1; subst b2; subst a1. + assert (false = true) by auto using Huni2, Ha1b1. + discriminate. + left; assumption. +Qed. + +End ProofIrrel_RelChoice_imp_EqEM. + +(**********************************************************************) +(** *** B. Extensional Hilbert's epsilon description operator -> Excluded-Middle *) + +(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) + +Notation Local "'inhabited' A" := A (at level 10, only parsing). + +Section ExtensionalEpsilon_imp_EM. + +Variable epsilon : forall A : Type, inhabited A -> (A -> Prop) -> A. + +Hypothesis epsilon_spec : + forall (A:Type) (i:inhabited A) (P:A->Prop), + (exists x, P x) -> P (epsilon A i P). + +Hypothesis epsilon_extensionality : + forall (A:Type) (i:inhabited A) (P Q:A->Prop), + (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q. + +Notation Local eps := (epsilon bool true) (only parsing). + +Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P. +Proof. +intro P. +pose (B := fun y => y=false \/ P). +pose (C := fun y => y=true \/ P). +assert (B (eps B)) as [Hfalse|HP] + by (apply epsilon_spec; exists false; left; reflexivity). +assert (C (eps C)) as [Htrue|HP] + by (apply epsilon_spec; exists true; left; reflexivity). + right; intro HP. + assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption). + rewrite epsilon_extensionality with (1:=H) in Hfalse. + rewrite Htrue in Hfalse. + discriminate. +auto. +auto. +Qed. + +End ExtensionalEpsilon_imp_EM. diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index feb11b827..9ad6b7220 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -10,11 +10,8 @@ (** This file axiomatizes the relational form of the axiom of choice *) -Axiom - relational_choice : - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - exists y : B, - R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). +Axiom relational_choice : + forall (A B : Type) (R : A->B->Prop), + (forall x : A, exists y : B, R x y) -> + exists R' : A->B->Prop, + subrelation R' R /\ forall x : A, exists! y : B, R' x y. -- cgit v1.2.3