diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 264 | ||||
| -rw-r--r-- | theories/Logic/ClassicalChoice.v | 12 | ||||
| -rw-r--r-- | theories/Logic/ClassicalDescription.v | 13 | ||||
| -rw-r--r-- | theories/Logic/ClassicalEpsilon.v | 8 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 35 | ||||
| -rw-r--r-- | theories/Logic/ClassicalUniqueChoice.v | 8 | ||||
| -rw-r--r-- | theories/Logic/ConstructiveEpsilon.v | 32 | ||||
| -rw-r--r-- | theories/Logic/Decidable.v | 161 | ||||
| -rw-r--r-- | theories/Logic/DecidableType.v | 25 | ||||
| -rw-r--r-- | theories/Logic/DecidableTypeEx.v | 71 | ||||
| -rw-r--r-- | theories/Logic/Description.v | 21 | ||||
| -rw-r--r-- | theories/Logic/Epsilon.v | 72 | ||||
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 23 | ||||
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 23 | ||||
| -rw-r--r-- | theories/Logic/IndefiniteDescription.v | 39 | ||||
| -rw-r--r-- | theories/Logic/JMeq.v | 37 | ||||
| -rw-r--r-- | theories/Logic/SetIsType.v | 17 |
17 files changed, 686 insertions, 175 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 3b066cfc..3d434b37 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1,4 +1,3 @@ -(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: ChoiceFacts.v 10756 2008-04-04 17:10:45Z herbelin $ i*) (** Some facts and definitions concerning choice and description in intuitionistic logic. @@ -30,7 +29,7 @@ description principles - OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice - OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice - (called AC* in Bell [Bell]) + (called AC* in Bell [[Bell]]) - OAC! - ID_iota = intuitionistic definite description @@ -44,13 +43,15 @@ description principles (an unconstrained generalisation of the constructive principle of independence of premises) - Drinker = drinker's paradox (small form) - (called Ex in Bell [Bell]) + (called Ex in Bell [[Bell]]) We let also -IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal predicate logic -IPL_2 = 2nd-order impredicative minimal predicate logic +IPL_2 = 2nd-order impredicative minimal predicate logic (with ex. quant.) IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) +IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.) + +with no prerequisite on the non-emptyness of domains Table of contents @@ -58,24 +59,26 @@ Table of contents 2. IPL_2^2 |- AC_rel + AC! = AC_fun -3. 1. AC_rel + PI -> GAC_rel and PL_2 |- AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel +3.1. typed IPL_2 + Sigma-types + PI |- AC_rel = GAC_rel and IPL_2 |- AC_rel + IGP -> GAC_rel and IPL_2 |- GAC_rel = OAC_rel + +3.2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker -4. 2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker +3.3. D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker -5. Derivability of choice for decidable relations with well-ordered codomain +4. Derivability of choice for decidable relations with well-ordered codomain -6. Equivalence of choices on dependent or non dependent functional types +5. Equivalence of choices on dependent or non dependent functional types -7. Non contradiction of constructive descriptions wrt functional choices +6. Non contradiction of constructive descriptions wrt functional choices -8. Definite description transports classical logic to the computational world +7. Definite description transports classical logic to the computational world References: -[Bell] John L. Bell, Choice principles in intuitionistic set theory, +[[Bell]] John L. Bell, Choice principles in intuitionistic set theory, unpublished. -[Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic +[[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 @@ -84,8 +87,6 @@ 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). - (**********************************************************************) (** * Definitions *) @@ -95,9 +96,9 @@ Section ChoiceSchemes. Variables A B :Type. -Variables P:A->Prop. +Variable P:A->Prop. -Variables R:A->B->Prop. +Variable R:A->B->Prop. (** ** Constructive choice and description *) @@ -183,15 +184,15 @@ Definition OmniscientFunctionalChoice_on := (** D_epsilon *) -Definition ClassicalIndefiniteDescription := +Definition EpsilonStatement_on := forall P:A->Prop, - A -> { x:A | (exists x, P x) -> P x }. + inhabited A -> { x:A | (exists x, P x) -> P x }. (** D_iota *) -Definition ClassicalDefiniteDescription := +Definition IotaStatement_on := forall P:A->Prop, - A -> { x:A | (exists! x, P x) -> P x }. + inhabited A -> { x:A | (exists! x, P x) -> P x }. End ChoiceSchemes. @@ -223,6 +224,11 @@ Notation ConstructiveDefiniteDescription := Notation ConstructiveIndefiniteDescription := (forall A, ConstructiveIndefiniteDescription_on A). +Notation IotaStatement := + (forall A, IotaStatement_on A). +Notation EpsilonStatement := + (forall A, EpsilonStatement_on A). + (** Subclassical schemes *) Definition ProofIrrelevance := @@ -238,16 +244,17 @@ Definition SmallDrinker'sParadox := exists x, (exists x, P x) -> P x. (**********************************************************************) -(** * AC_rel + PDP = AC_fun +(** * AC_rel + AC! = 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) *) + formulation (only formulation of set theory) + functional relation + reification (aka axiom of unique choice, or, principle of (parametric) + definite descriptions) *) (** 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 *) + though functional relation reification conflicts with classical logic *) Lemma description_rel_choice_imp_funct_choice : forall A B : Type, @@ -289,7 +296,7 @@ Proof. exists f; exact H0. Qed. -Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr : +Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr : forall A B, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B. Proof. @@ -301,11 +308,13 @@ Proof. Qed. (**********************************************************************) -(** * Connection between the guarded, non guarded and descriptive choices and *) +(** * Connection between the guarded, non guarded and omniscient choices *) -(** 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 *) +(** We show that the guarded formulations of the axiom of choice + are equivalent to their "omniscient" variant and comes from the non guarded + formulation in presence either of the independance of general premises + or subset types (themselves derivable from subtypes thanks to proof- + irrelevance) *) (**********************************************************************) (** ** AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *) @@ -352,9 +361,17 @@ Proof. exists R'; firstorder. Qed. +Lemma subset_types_imp_guarded_rel_choice_iff_rel_choice : + ProofIrrelevance -> (GuardedRelationalChoice <-> RelationalChoice). +Proof. + auto decomp using + guarded_rel_choice_imp_rel_choice, + rel_choice_and_proof_irrel_imp_guarded_rel_choice. +Qed. + (** OAC_rel = GAC_rel *) -Lemma guarded_iff_omniscient_rel_choice : +Corollary guarded_iff_omniscient_rel_choice : GuardedRelationalChoice <-> OmniscientRelationalChoice. Proof. split. @@ -378,6 +395,7 @@ Proof. exists (f tt); auto. Qed. + Lemma guarded_fun_choice_imp_fun_choice : GuardedFunctionalChoice -> FunctionalChoiceOnInhabitedSet. Proof. @@ -396,9 +414,19 @@ Proof. intro x; apply IndPrem; eauto. Qed. +Corollary fun_choice_and_indep_general_prem_iff_guarded_fun_choice : + FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises + <-> GuardedFunctionalChoice. +Proof. + auto decomp using + guarded_fun_choice_imp_indep_of_general_premises, + guarded_fun_choice_imp_fun_choice, + fun_choice_and_indep_general_prem_imp_guarded_fun_choice. +Qed. + (** AC_fun + Drinker = OAC_fun *) -(** This was already observed by Bell [Bell] *) +(** This was already observed by Bell [[Bell]] *) Lemma omniscient_fun_choice_imp_small_drinker : OmniscientFunctionalChoice -> SmallDrinker'sParadox. @@ -427,12 +455,22 @@ Proof. exists f; assumption. Qed. +Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice : + FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox + <-> OmniscientFunctionalChoice. +Proof. + auto decomp using + omniscient_fun_choice_imp_small_drinker, + omniscient_fun_choice_imp_fun_choice, + fun_choice_and_small_drinker_imp_omniscient_fun_choice. +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 : +Theorem guarded_iff_omniscient_fun_choice : GuardedFunctionalChoice <-> OmniscientFunctionalChoice. Proof. split. @@ -444,6 +482,57 @@ Proof. Qed. (**********************************************************************) +(** ** D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker *) + +(** D_iota -> ID_iota *) + +Lemma iota_imp_constructive_definite_description : + IotaStatement -> ConstructiveDefiniteDescription. +Proof. + intros D_iota A P H. + destruct D_iota with (P:=P) as (x,H1). + destruct H; red in H; auto. + exists x; apply H1; assumption. +Qed. + +(** ID_epsilon + Drinker <-> D_epsilon *) + +Lemma epsilon_imp_constructive_indefinite_description: + EpsilonStatement -> ConstructiveIndefiniteDescription. +Proof. + intros D_epsilon A P H. + destruct D_epsilon with (P:=P) as (x,H1). + destruct H; auto. + exists x; apply H1; assumption. +Qed. + +Lemma constructive_indefinite_description_and_small_drinker_imp_epsilon : + SmallDrinker'sParadox -> ConstructiveIndefiniteDescription -> + EpsilonStatement. +Proof. + intros Drinkers D_epsilon A P Inh; + apply D_epsilon; apply Drinkers; assumption. +Qed. + +Lemma epsilon_imp_small_drinker : + EpsilonStatement -> SmallDrinker'sParadox. +Proof. + intros D_epsilon A P Inh; edestruct D_epsilon; eauto. +Qed. + +Theorem constructive_indefinite_description_and_small_drinker_iff_epsilon : + (SmallDrinker'sParadox * ConstructiveIndefiniteDescription -> + EpsilonStatement) * + (EpsilonStatement -> + SmallDrinker'sParadox * ConstructiveIndefiniteDescription). +Proof. + auto decomp using + epsilon_imp_constructive_indefinite_description, + constructive_indefinite_description_and_small_drinker_imp_epsilon, + epsilon_imp_small_drinker. +Qed. + +(**********************************************************************) (** * Derivability of choice for decidable relations with well-ordered codomain *) (** Countable codomains, such as [nat], can be equipped with a @@ -457,45 +546,7 @@ Qed. *) Require Import Wf_nat. -Require Import Compare_dec. 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'. - -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 le P. -Proof. - intros P Pdec (n0,HPn0). - assert - (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') - \/(forall n', P n' -> n<=n')). - induction n. - right. - intros n' Hn'. - apply le_O_n. - destruct IHn. - left; destruct H as (n', (Hlt', HPn')). - exists n'; split. - apply lt_S; assumption. - assumption. - destruct (Pdec n). - left; exists n; split. - apply lt_n_Sn. - split; assumption. - right. - intros n' Hltn'. - destruct (le_lt_eq_dec n n') as [Hltn|Heqn]. - apply H; assumption. - assumption. - destruct H0. - rewrite Heqn; assumption. - 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_rel (A B:Type) (R:A->B->Prop) := (forall x:A, exists y : B, R x y) -> @@ -614,16 +665,24 @@ Proof. destruct Heq using eq_indd; trivial. Qed. +Corollary dep_iff_non_dep_functional_rel_reification : + FunctionalRelReification <-> DependentFunctionalRelReification. +Proof. + auto decomp using + non_dep_dep_functional_rel_reification, + dep_non_dep_functional_rel_reification. +Qed. + (**********************************************************************) (** * Non contradiction of constructive descriptions wrt functional axioms of choice *) (** ** Non contradiction of indefinite description *) -Lemma relative_non_contradiction_of_indefinite_desc : - (ConstructiveIndefiniteDescription -> False) - -> (FunctionalChoice -> False). +Lemma relative_non_contradiction_of_indefinite_descr : + forall C:Prop, (ConstructiveIndefiniteDescription -> C) + -> (FunctionalChoice -> C). Proof. - intros H AC_fun. + intros C 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). @@ -632,11 +691,8 @@ Proof. 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'))). + exists (f (existT _ A (existT _ P H'))). + pose (Hf' := Hf (existT _ A (existT _ P H'))). assumption. Qed. @@ -652,10 +708,10 @@ Qed. (** ** Non contradiction of definite description *) Lemma relative_non_contradiction_of_definite_descr : - (ConstructiveDefiniteDescription -> False) - -> (FunctionalRelReification -> False). + forall C:Prop, (ConstructiveDefiniteDescription -> C) + -> (FunctionalRelReification -> C). Proof. - intros H FunReify. + intros C 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). @@ -664,11 +720,8 @@ Proof. 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'))). + exists (f (existT _ A (existT _ P H'))). + pose (Hf' := Hf (existT _ A (existT _ P H'))). assumption. Qed. @@ -681,20 +734,37 @@ Proof. apply (proj2_sig (DefDescr B (R x) (H x))). Qed. +(** Remark, the following corollaries morally hold: + +Definition In_propositional_context (A:Type) := forall C:Prop, (A -> C) -> C. + +Corollary constructive_definite_descr_in_prop_context_iff_fun_reification : + In_propositional_context ConstructiveIndefiniteDescription + <-> FunctionalChoice. + +Corollary constructive_definite_descr_in_prop_context_iff_fun_reification : + In_propositional_context ConstructiveDefiniteDescription + <-> FunctionalRelReification. + +but expecting [FunctionalChoice] (resp. [FunctionalRelReification]) to +be applied on the same Type universes on both sides of the first +(resp. second) equivalence breaks the stratification of universes. +*) + (**********************************************************************) (** * Excluded-middle + definite description => computational excluded-middle *) -(** The idea for the following proof comes from [ChicliPottierSimpson02] *) +(** 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], + 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 + [[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. *) @@ -717,3 +787,13 @@ Proof. left; trivial. right; trivial. Qed. + +Corollary fun_reification_descr_computational_excluded_middle_in_prop_context : + FunctionalRelReification -> + (forall P:Prop, P \/ ~ P) -> + forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C. +Proof. + intros FunReify EM C; auto decomp using + constructive_definite_descr_excluded_middle, + (relative_non_contradiction_of_definite_descr (C:=C)). +Qed. diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index bb8186ae..f9b59a6a 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -6,11 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalChoice.v 8892 2006-06-04 17:59:53Z herbelin $ i*) +(*i $Id: ClassicalChoice.v 10170 2007-10-03 14:41:25Z herbelin $ i*) -(** This file provides classical logic, and functional choice *) +(** This file provides classical logic and functional choice; this + especially provides both indefinite descriptions and choice functions + but this is weaker than providing epsilon operator and classical logic + as the indefinite descriptions provided by the axiom of choice can + be used only in a propositional context (especially, they cannot + be used to build choice functions outside the scope of a theorem + proof) *) -(** This file extends ClassicalUniqueChoice.v with the axiom of choice. +(** This file extends ClassicalUniqueChoice.v with full 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 diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 1f1c34bf..3737abf6 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -6,14 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalDescription.v 9514 2007-01-22 14:58:50Z herbelin $ i*) +(*i $Id: ClassicalDescription.v 10170 2007-10-03 14:41:25Z herbelin $ i*) -(** This file provides classical logic and definite description *) +(** This file provides classical logic and definite description, which is + equivalent to providing classical logic and Church's iota operator *) -(** 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] *) +(** Classical logic and definite descriptions implies excluded-middle + in [Set] and leads to a classical world populated with non + computable functions. It conflicts with the impredicativity of + [Set] *) Set Implicit Arguments. diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 6d0a9c77..2a4de511 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalEpsilon.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: ClassicalEpsilon.v 10170 2007-10-03 14:41:25Z herbelin $ i*) -(** This file provides classical logic and indefinite description - (Hilbert's epsilon operator) *) +(** This file provides classical logic and indefinite description under + the form of Hilbert's epsilon operator *) -(** Classical epsilon's operator (i.e. indefinite description) implies +(** Hilbert's epsilon operator and classical logic implies excluded-middle in [Set] and leads to a classical world populated with non computable functions. It conflicts with the impredicativity of [Set] *) diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index dd911db6..734de52d 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: ClassicalFacts.v 10156 2007-09-30 19:02:14Z herbelin $ i*) (** Some facts and definitions about classical logic @@ -31,8 +31,8 @@ Table of contents: 3.1. Weak excluded middle -3.2. Gödel-Dummet axiom and right distributivity of implication over - disjunction +3.2. Gödel-Dummett axiom and right distributivity of implication over + disjunction 3 3. Independence of general premises and drinker's paradox @@ -91,6 +91,17 @@ Proof. right; apply (Ext A False); split; [ exact H | apply False_ind ]. Qed. +(** A weakest form of propositional extensionality: extensionality for + provable propositions only *) + +Definition provable_prop_extensionality := forall A:Prop, A -> A = True. + +Lemma provable_prop_ext : + prop_extensionality -> provable_prop_extensionality. +Proof. + intros Ext A Ha; apply Ext; split; trivial. +Qed. + (************************************************************************) (** * Classical logic and proof-irrelevance *) @@ -105,6 +116,7 @@ Qed. (just take the identity), which implies the existence of a fixpoint operator in [A] (e.g. take the Y combinator of lambda-calculus) + *) Definition inhabited (A:Prop) := A. @@ -143,6 +155,10 @@ Proof. reflexivity. Qed. +(** Remark: [prop_extensionality] can be replaced in lemma [ext_prop_fixpoint] + by the weakest property [provable_prop_extensionality]. +*) + (************************************************************************) (** ** CC |- prop_ext /\ dep elim on bool -> proof-irrelevance *) @@ -230,6 +246,11 @@ Section Proof_irrelevance_Prop_Ext_CC. End Proof_irrelevance_Prop_Ext_CC. +(** Remark: [prop_extensionality] can be replaced in lemma + [ext_prop_dep_proof_irrel_gen] by the weakest property + [provable_prop_extensionality]. +*) + (************************************************************************) (** ** CIC |- prop. ext. -> proof-irrelevance *) @@ -396,7 +417,7 @@ End Proof_irrelevance_CCI. (** We show the following increasing in the strength of axioms: - weak excluded-middle - - right distributivity of implication over disjunction and Gödel-Dummet axiom + - right distributivity of implication over disjunction and Gödel-Dummett axiom - independence of general premises and drinker's paradox - excluded-middle *) @@ -533,7 +554,11 @@ Proof. Qed. (** Independence of general premises is weaker than (generalized) - excluded middle *) + excluded middle + +Remark: generalized excluded middle is preferred here to avoid relying on +the "ex falso quodlibet" property (i.e. [False -> forall A, A]) +*) Definition generalized_excluded_middle := forall A B:Prop, A \/ (A -> B). diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index 28d32fcc..bb846aa6 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -6,9 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalUniqueChoice.v 9026 2006-07-06 15:16:20Z herbelin $ i*) +(*i $Id: ClassicalUniqueChoice.v 10170 2007-10-03 14:41:25Z herbelin $ i*) -(** This file provides classical logic and unique choice *) +(** This file provides classical logic and unique choice; this is + weaker than providing iota operator and classical logic as the + definite descriptions provided by the axiom of unique choice can + be used only in a propositional context (especially, they cannot + be used to build functions outside the scope of a theorem proof) *) (** Classical logic and unique choice, as shown in [ChicliPottierSimpson02], implies the double-negation of diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 61e377ea..f1503d24 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) +(*i $Id: ConstructiveEpsilon.v 10739 2008-04-01 14:45:20Z herbelin $ i*) (** This module proves the constructive description schema, which infers the sigma-existence (i.e., [Set]-existence) of a witness to a @@ -20,17 +20,19 @@ show [{n : nat | P n}]. However, one can perform a recursion on an inductive predicate in sort [Prop] so that the returning type of the recursion is in [Set]. This trick is described in Coq'Art book, Sect. 14.2.3 and 15.4. In particular, this trick is used in the proof of -[Acc_iter] in the module Coq.Init.Wf. There, recursion is done on an +[Fix_F] in the module Coq.Init.Wf. There, recursion is done on an inductive predicate [Acc] and the resulting type is in [Type]. The predicate [Acc] delineates elements that are accessible via a given relation [R]. An element is accessible if there are no infinite [R]-descending chains starting from it. -To use [Acc_iter], we define a relation R and prove that if [exists n, +To use [Fix_F], we define a relation R and prove that if [exists n, P n] then 0 is accessible with respect to R. Then, by induction on the definition of [Acc R 0], we show [{n : nat | P n}]. *) +(** Based on ideas from Benjamin Werner and Jean-François Monin *) + (** Contributed by Yevgeniy Makarov *) Require Import Arith. @@ -49,7 +51,8 @@ numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after infinite [R]-descending chain from 0 is equivalent to the termination of our searching algorithm. *) -Let R (x y : nat) := (x = S y /\ ~ P y). +Let R (x y : nat) : Prop := x = S y /\ ~ P y. + Notation Local "'acc' x" := (Acc R x) (at level 10). Lemma P_implies_acc : forall x : nat, P x -> acc x. @@ -78,7 +81,7 @@ Defined. Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}. Proof. -intros Acc_0. pattern 0. apply Acc_iter with (R := R); [| assumption]. +intros Acc_0. pattern 0. apply Fix_F with (R := R); [| assumption]. clear Acc_0; intros x IH. destruct (P_decidable x) as [Px | not_Px]. exists x; simpl; assumption. @@ -102,7 +105,7 @@ Section ConstructiveEpsilon. there are functions [f : A -> nat] and [g : nat -> A] such that [g] is a left inverse of [f]. *) -Variable A : Type. +Variable A : Set. Variable f : A -> nat. Variable g : nat -> A. @@ -132,24 +135,11 @@ Proof. intros; apply constructive_indefinite_description; firstorder. Defined. -Definition epsilon (E : exists x : A, P x) : A +Definition constructive_epsilon (E : exists x : A, P x) : A := proj1_sig (constructive_indefinite_description E). -Definition epsilon_spec (E : (exists x, P x)) : P (epsilon E) +Definition constructive_epsilon_spec (E : (exists x, P x)) : P (constructive_epsilon E) := proj2_sig (constructive_indefinite_description E). End ConstructiveEpsilon. -Theorem choice : - forall (A B : Type) (f : B -> nat) (g : nat -> B), - (forall x : B, g (f x) = x) -> - forall (R : A -> B -> Prop), - (forall (x : A) (y : B), {R x y} + {~ R x y}) -> - (forall x : A, exists y : B, R x y) -> - (exists f : A -> B, forall x : A, R x (f x)). -Proof. -intros A B f g gof_eq_id R R_dec H. -exists (fun x : A => epsilon B f g gof_eq_id (R x) (R_dec x) (H x)). -intro x. -apply (epsilon_spec B f g gof_eq_id (R x) (R_dec x) (H x)). -Qed. diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 8317f6bb..a7c098e8 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -5,56 +5,191 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Decidable.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Decidable.v 10500 2008-02-02 15:51:00Z letouzey $ i*) (** Properties of decidable propositions *) Definition decidable (P:Prop) := P \/ ~ P. Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P. -unfold decidable in |- *; tauto. +Proof. +unfold decidable; tauto. Qed. Theorem dec_True : decidable True. -unfold decidable in |- *; auto. +Proof. +unfold decidable; auto. Qed. Theorem dec_False : decidable False. -unfold decidable, not in |- *; auto. +Proof. +unfold decidable, not; auto. Qed. Theorem dec_or : forall A B:Prop, decidable A -> decidable B -> decidable (A \/ B). -unfold decidable in |- *; tauto. +Proof. +unfold decidable; tauto. Qed. Theorem dec_and : forall A B:Prop, decidable A -> decidable B -> decidable (A /\ B). -unfold decidable in |- *; tauto. +Proof. +unfold decidable; tauto. Qed. Theorem dec_not : forall A:Prop, decidable A -> decidable (~ A). -unfold decidable in |- *; tauto. +Proof. +unfold decidable; tauto. Qed. Theorem dec_imp : forall A B:Prop, decidable A -> decidable B -> decidable (A -> B). -unfold decidable in |- *; tauto. +Proof. +unfold decidable; tauto. +Qed. + +Theorem dec_iff : + forall A B:Prop, decidable A -> decidable B -> decidable (A<->B). +Proof. +unfold decidable; tauto. Qed. Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P. -unfold decidable in |- *; tauto. Qed. +Proof. +unfold decidable; tauto. +Qed. Theorem not_or : forall A B:Prop, ~ (A \/ B) -> ~ A /\ ~ B. -tauto. Qed. +Proof. +tauto. +Qed. Theorem not_and : forall A B:Prop, decidable A -> ~ (A /\ B) -> ~ A \/ ~ B. -unfold decidable in |- *; tauto. Qed. +Proof. +unfold decidable; tauto. +Qed. Theorem not_imp : forall A B:Prop, decidable A -> ~ (A -> B) -> A /\ ~ B. -unfold decidable in |- *; tauto. +Proof. +unfold decidable; tauto. Qed. Theorem imp_simp : forall A B:Prop, decidable A -> (A -> B) -> ~ A \/ B. -unfold decidable in |- *; tauto. +Proof. +unfold decidable; tauto. +Qed. + +(** Results formulated with iff, used in FSetDecide. + Negation are expanded since it is unclear whether setoid rewrite + will always perform conversion. *) + +(** We begin with lemmas that, when read from left to right, + can be understood as ways to eliminate uses of [not]. *) + +Theorem not_true_iff : (True -> False) <-> False. +Proof. +tauto. +Qed. + +Theorem not_false_iff : (False -> False) <-> True. +Proof. +tauto. +Qed. + +Theorem not_not_iff : forall A:Prop, decidable A -> + (((A -> False) -> False) <-> A). +Proof. +unfold decidable; tauto. +Qed. + +Theorem contrapositive : forall A B:Prop, decidable A -> + (((A -> False) -> (B -> False)) <-> (B -> A)). +Proof. +unfold decidable; tauto. +Qed. + +Lemma or_not_l_iff_1 : forall A B: Prop, decidable A -> + ((A -> False) \/ B <-> (A -> B)). +Proof. +unfold decidable. tauto. +Qed. + +Lemma or_not_l_iff_2 : forall A B: Prop, decidable B -> + ((A -> False) \/ B <-> (A -> B)). +Proof. +unfold decidable. tauto. +Qed. + +Lemma or_not_r_iff_1 : forall A B: Prop, decidable A -> + (A \/ (B -> False) <-> (B -> A)). +Proof. +unfold decidable. tauto. Qed. + +Lemma or_not_r_iff_2 : forall A B: Prop, decidable B -> + (A \/ (B -> False) <-> (B -> A)). +Proof. +unfold decidable. tauto. +Qed. + +Lemma imp_not_l : forall A B: Prop, decidable A -> + (((A -> False) -> B) <-> (A \/ B)). +Proof. +unfold decidable. tauto. +Qed. + + +(** Moving Negations Around: + We have four lemmas that, when read from left to right, + describe how to push negations toward the leaves of a + proposition and, when read from right to left, describe + how to pull negations toward the top of a proposition. *) + +Theorem not_or_iff : forall A B:Prop, + (A \/ B -> False) <-> (A -> False) /\ (B -> False). +Proof. +tauto. +Qed. + +Lemma not_and_iff : forall A B:Prop, + (A /\ B -> False) <-> (A -> B -> False). +Proof. +tauto. +Qed. + +Lemma not_imp_iff : forall A B:Prop, decidable A -> + (((A -> B) -> False) <-> A /\ (B -> False)). +Proof. +unfold decidable. tauto. +Qed. + +Lemma not_imp_rev_iff : forall A B : Prop, decidable A -> + (((A -> B) -> False) <-> (B -> False) /\ A). +Proof. +unfold decidable. tauto. +Qed. + + + +(** With the following hint database, we can leverage [auto] to check + decidability of propositions. *) + +Hint Resolve dec_True dec_False dec_or dec_and dec_imp dec_not dec_iff + : decidable_prop. + +(** [solve_decidable using lib] will solve goals about the + decidability of a proposition, assisted by an auxiliary + database of lemmas. The database is intended to contain + lemmas stating the decidability of base propositions, + (e.g., the decidability of equality on a particular + inductive type). *) + +Tactic Notation "solve_decidable" "using" ident(db) := + match goal with + | |- decidable _ => + solve [ auto 100 with decidable_prop db ] + end. + +Tactic Notation "solve_decidable" := + solve_decidable using core. diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v index a38b111f..a65e2c52 100644 --- a/theories/Logic/DecidableType.v +++ b/theories/Logic/DecidableType.v @@ -6,19 +6,36 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: DecidableType.v 8933 2006-06-09 14:08:38Z herbelin $ *) +(* $Id: DecidableType.v 10616 2008-03-04 17:33:35Z letouzey $ *) Require Export SetoidList. Set Implicit Arguments. Unset Strict Implicit. +(** * Types with Equalities, and nothing more (for subtyping purpose) *) + +Module Type EqualityType. + + Parameter Inline t : Type. + + Parameter Inline eq : t -> t -> Prop. + + Axiom eq_refl : forall x : t, eq x x. + Axiom eq_sym : forall x y : t, eq x y -> eq y x. + Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + + Hint Immediate eq_sym. + Hint Resolve eq_refl eq_trans. + +End EqualityType. + (** * Types with decidable Equalities (but no ordering) *) Module Type DecidableType. - Parameter t : Set. + Parameter Inline t : Type. - Parameter eq : t -> t -> Prop. + Parameter Inline eq : t -> t -> Prop. Axiom eq_refl : forall x : t, eq x x. Axiom eq_sym : forall x y : t, eq x y -> eq y x. @@ -37,7 +54,7 @@ Module KeyDecidableType(D:DecidableType). Import D. Section Elt. - Variable elt : Set. + Variable elt : Type. Notation key:=t. Definition eqk (p p':key*elt) := eq (fst p) (fst p'). diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v index a4f99de2..9c928598 100644 --- a/theories/Logic/DecidableTypeEx.v +++ b/theories/Logic/DecidableTypeEx.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: DecidableTypeEx.v 8933 2006-06-09 14:08:38Z herbelin $ *) +(* $Id: DecidableTypeEx.v 10739 2008-04-01 14:45:20Z herbelin $ *) Require Import DecidableType OrderedType OrderedTypeEx. Set Implicit Arguments. @@ -18,7 +18,7 @@ Unset Strict Implicit. the equality is the usual one of Coq. *) Module Type UsualDecidableType. - Parameter t : Set. + Parameter Inline t : Type. Definition eq := @eq t. Definition eq_refl := @refl_equal t. Definition eq_sym := @sym_eq t. @@ -30,6 +30,22 @@ End UsualDecidableType. Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. +(** an shortcut for easily building a UsualDecidableType *) + +Module Type MiniDecidableType. + Parameter Inline t : Type. + Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }. +End MiniDecidableType. + +Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. + Definition t:=M.t. + Definition eq := @eq t. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Definition eq_dec := M.eq_dec. +End Make_UDT. + (** An OrderedType can be seen as a DecidableType *) Module OT_as_DT (O:OrderedType) <: DecidableType. @@ -48,3 +64,54 @@ Module Nat_as_DT <: UsualDecidableType := OT_as_DT (Nat_as_OT). Module Positive_as_DT <: UsualDecidableType := OT_as_DT (Positive_as_OT). Module N_as_DT <: UsualDecidableType := OT_as_DT (N_as_OT). Module Z_as_DT <: UsualDecidableType := OT_as_DT (Z_as_OT). + +(** From two decidable types, we can build a new DecidableType + over their cartesian product. *) + +Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. + + Definition t := prod D1.t D2.t. + + Definition eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y). + + Lemma eq_refl : forall x : t, eq x x. + Proof. + intros (x1,x2); red; simpl; auto. + Qed. + + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Proof. + intros (x1,x2) (y1,y2); unfold eq; simpl; intuition. + Qed. + + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Proof. + intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. + Qed. + + Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. + Proof. + intros (x1,x2) (y1,y2); unfold eq; simpl. + destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); intuition. + Defined. + +End PairDecidableType. + +(** Similarly for pairs of UsualDecidableType *) + +Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: DecidableType. + Definition t := prod D1.t D2.t. + Definition eq := @eq t. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. + Proof. + intros (x1,x2) (y1,y2); + destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); + unfold eq, D1.eq, D2.eq in *; simpl; + (left; f_equal; auto; fail) || + (right; intro H; injection H; auto). + Defined. + +End PairUsualDecidableType. diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v new file mode 100644 index 00000000..962f2a2a --- /dev/null +++ b/theories/Logic/Description.v @@ -0,0 +1,21 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Description.v 10170 2007-10-03 14:41:25Z herbelin $ i*) + +(** This file provides a constructive form of definite description; it + allows to build functions from the proof of their existence in any + context; this is weaker than Church's iota operator *) + +Require Import ChoiceFacts. + +Set Implicit Arguments. + +Axiom constructive_definite_description : + forall (A : Type) (P : A->Prop), + (exists! x, P x) -> { x : A | P x }. diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v new file mode 100644 index 00000000..65d4d853 --- /dev/null +++ b/theories/Logic/Epsilon.v @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Epsilon.v 10170 2007-10-03 14:41:25Z herbelin $ i*) + +(** This file provides indefinite description under the form of + Hilbert's epsilon operator; it does not assume classical logic. *) + +Require Import ChoiceFacts. + +Set Implicit Arguments. + +(** Hilbert's epsilon: operator and specification in one statement *) + +Axiom epsilon_statement : + forall (A : Type) (P : A->Prop), inhabited A -> + { x : A | (exists x, P x) -> P x }. + +Lemma constructive_indefinite_description : + forall (A : Type) (P : A->Prop), + (exists x, P x) -> { x : A | P x }. +Proof. + apply epsilon_imp_constructive_indefinite_description. + exact epsilon_statement. +Qed. + +Lemma small_drinkers'_paradox : + forall (A:Type) (P:A -> Prop), inhabited A -> + exists x, (exists x, P x) -> P x. +Proof. + apply epsilon_imp_small_drinker. + exact epsilon_statement. +Qed. + +Theorem iota_statement : + forall (A : Type) (P : A->Prop), inhabited A -> + { x : A | (exists! x : A, P x) -> P x }. +Proof. + intros; destruct epsilon_statement with (P:=P); firstorder. +Qed. + +Lemma constructive_definite_description : + forall (A : Type) (P : A->Prop), + (exists! x, P x) -> { x : A | P x }. +Proof. + apply iota_imp_constructive_definite_description. + exact iota_statement. +Qed. + +(** Hilbert's epsilon operator and its specification *) + +Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A + := proj1_sig (epsilon_statement P i). + +Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : + (exists x, P x) -> P (epsilon i P) + := proj2_sig (epsilon_statement P i). + +(** Church's iota operator and its specification *) + +Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A + := proj1_sig (iota_statement P i). + +Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : + (exists! x:A, P x) -> P (iota i P) + := proj2_sig (iota_statement P i). + diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 94a577ca..844bff88 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqdepFacts.v 9597 2007-02-06 19:44:05Z herbelin $ i*) +(*i $Id: EqdepFacts.v 11095 2008-06-10 19:36:10Z herbelin $ i*) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives @@ -104,7 +104,7 @@ Implicit Arguments eq_dep1 [U P]. (** Dependent equality is equivalent to equality on dependent pairs *) -Lemma eq_sigS_eq_dep : +Lemma eq_sigT_eq_dep : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), existT P p x = existT P q y -> eq_dep p x q y. Proof. @@ -113,26 +113,19 @@ Proof. apply eq_dep_intro. Qed. +Notation eq_sigS_eq_dep := eq_sigT_eq_dep (only parsing). (* Compatibility *) + Lemma equiv_eqex_eqdep : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), - existS P p x = existS P q y <-> eq_dep p x q y. + existT P p x = existT P q y <-> eq_dep p x q y. Proof. split. (* -> *) - apply eq_sigS_eq_dep. + apply eq_sigT_eq_dep. (* <- *) destruct 1; reflexivity. Qed. -Lemma eq_sigT_eq_dep : - forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), - existT P p x = existT P q y -> eq_dep p x q y. -Proof. - intros. - dependent rewrite H. - apply eq_dep_intro. -Qed. - Lemma eq_dep_eq_sigT : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), eq_dep p x q y -> existT P p x = existT P q y. @@ -258,7 +251,7 @@ Section Corollaries. Proof. intro eq_dep_eq; red; intros. apply eq_dep_eq. - apply eq_sigS_eq_dep. + apply eq_sigT_eq_dep. assumption. Qed. @@ -270,7 +263,7 @@ Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2. (************************************************************************) -(** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *) +(** * Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *) Module Type EqdepElimination. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 103efd22..0281916e 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep_dec.v 9597 2007-02-06 19:44:05Z herbelin $ i*) +(*i $Id: Eqdep_dec.v 10144 2007-09-26 15:12:17Z vsiles $ i*) (** We prove that there is only one proof of [x=x], i.e [refl_equal x]. This holds if the equality upon the set of [x] is decidable. @@ -158,6 +158,13 @@ Proof. apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)). Qed. +(** We deduce the injectivity of dependent equality for decidable types *) +Theorem eq_dep_eq_dec : + forall A:Type, + (forall x y:A, {x = y} + {x <> y}) -> + forall (P:A->Type) (p:A) (x y:P p), eq_dep A P p x p y -> x = y. +Proof (fun A eq_dec => eq_rect_eq__eq_dep_eq A (eq_rect_eq_dec eq_dec)). + Unset Implicit Arguments. (************************************************************************) @@ -229,7 +236,7 @@ Module DecidableEqDep (M:DecidableType). End DecidableEqDep. (************************************************************************) -(** ** B Definition of the functor that builds properties of dependent equalities on decidable sets in Set *) +(** ** Definition of the functor that builds properties of dependent equalities on decidable sets in Set *) (** The signature of decidable sets in [Set] *) @@ -296,3 +303,15 @@ Module DecidableEqDepSet (M:DecidableSet). Notation inj_pairT2 := inj_pair2. End DecidableEqDepSet. + + (** From decidability to inj_pair2 **) +Lemma inj_pair2_eq_dec : forall A:Type, (forall x y:A, {x=y}+{x<>y}) -> + ( forall (P:A -> Type) (p:A) (x y:P p), existT P p x = existT P p y -> x = y ). +Proof. + intros A eq_dec. + apply eq_dep_eq__inj_pair2. + apply eq_rect_eq__eq_dep_eq. + unfold Eq_rect_eq. + apply eq_rect_eq_dec. + apply eq_dec. +Qed. diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v new file mode 100644 index 00000000..740b889a --- /dev/null +++ b/theories/Logic/IndefiniteDescription.v @@ -0,0 +1,39 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: IndefiniteDescription.v 10170 2007-10-03 14:41:25Z herbelin $ i*) + +(** This file provides a constructive form of indefinite description that + allows to build choice functions; this is weaker than Hilbert's + epsilon operator (which implies weakly classical properties) but + stronger than the axiom of choice (which cannot be used outside + the context of a theorem proof). *) + +Require Import ChoiceFacts. + +Set Implicit Arguments. + +Axiom constructive_indefinite_description : + forall (A : Type) (P : A->Prop), + (exists x, P x) -> { x : A | P x }. + +Lemma constructive_definite_description : + forall (A : Type) (P : A->Prop), + (exists! x, P x) -> { x : A | P x }. +Proof. + intros; apply constructive_indefinite_description; firstorder. +Qed. + +Lemma functional_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. + apply constructive_indefinite_descr_fun_choice. + exact constructive_indefinite_description. +Qed. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 6a723e43..c3573ac3 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: JMeq.v 9077 2006-08-24 08:44:32Z herbelin $ i*) +(*i $Id: JMeq.v 9849 2007-05-22 20:40:04Z herbelin $ i*) (** John Major's Equality as proposed by Conor McBride @@ -19,9 +19,12 @@ Set Implicit Arguments. +Unset Elimination Schemes. + Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop := JMeq_refl : JMeq x x. -Reset JMeq_rect. + +Set Elimination Schemes. Hint Resolve JMeq_refl. @@ -65,20 +68,42 @@ Lemma JMeq_rect_r : intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial. Qed. -(** [JMeq] is equivalent to [(eq_dep Type [X]X)] *) +(** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *) Require Import Eqdep. -Lemma JMeq_eq_dep : +Lemma JMeq_eq_dep_id : forall (A B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X => X) A x B y. Proof. destruct 1. apply eq_dep_intro. Qed. -Lemma eq_dep_JMeq : +Lemma eq_dep_id_JMeq : forall (A B:Type) (x:A) (y:B), eq_dep Type (fun X => X) A x B y -> JMeq x y. Proof. destruct 1. -apply JMeq_refl. +apply JMeq_refl. +Qed. + +(** [eq_dep U P p x q y] is strictly finer than [JMeq (P p) x (P q) y] *) + +Lemma eq_dep_JMeq : + forall U P p x q y, eq_dep U P p x q y -> JMeq x y. +Proof. +destruct 1. +apply JMeq_refl. +Qed. + +Lemma eq_dep_strictly_stronger_JMeq : + exists U, exists P, exists p, exists q, exists x, exists y, + JMeq x y /\ ~ eq_dep U P p x q y. +Proof. +exists bool. exists (fun _ => True). exists true. exists false. +exists I. exists I. +split. +trivial. +intro H. +assert (true=false) by (destruct H; reflexivity). +discriminate. Qed. diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v new file mode 100644 index 00000000..3286beb4 --- /dev/null +++ b/theories/Logic/SetIsType.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * The Set universe seen as a synonym for Type *) + +(** After loading this file, Set becomes just another name for Type. + This allows to easily perform a Set-to-Type migration, or at least + test whether a development relies or not on specific features of + Set: simply insert some Require Export of this file at starting + points of the development and try to recompile... *) + +Notation "'Set'" := Type (only parsing).
\ No newline at end of file |