diff options
Diffstat (limited to 'theories/Logic')
35 files changed, 7117 insertions, 0 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v new file mode 100644 index 0000000000..ed4d69ab02 --- /dev/null +++ b/theories/Logic/Berardi.v @@ -0,0 +1,154 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This file formalizes Berardi's paradox which says that in + the calculus of constructions, excluded middle (EM) and axiom of + choice (AC) imply proof irrelevance (PI). + Here, the axiom of choice is not necessary because of the use + of inductive types. +<< +@article{Barbanera-Berardi:JFP96, + author = {F. Barbanera and S. Berardi}, + title = {Proof-irrelevance out of Excluded-middle and Choice + in the Calculus of Constructions}, + journal = {Journal of Functional Programming}, + year = {1996}, + volume = {6}, + number = {3}, + pages = {519-525} +} +>> *) + +Set Implicit Arguments. + +Section Berardis_paradox. + +(** Excluded middle *) +Hypothesis EM : forall P:Prop, P \/ ~ P. + +(** Conditional on any proposition. *) +Definition IFProp (P B:Prop) (e1 e2:P) := + match EM B with + | or_introl _ => e1 + | or_intror _ => e2 + end. + +(** Axiom of choice applied to disjunction. + Provable in Coq because of dependent elimination. *) +Lemma AC_IF : + forall (P B:Prop) (e1 e2:P) (Q:P -> Prop), + (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2). +Proof. +intros P B e1 e2 Q p1 p2. +unfold IFProp. +case (EM B); assumption. +Qed. + + +(** We assume a type with two elements. They play the role of booleans. + The main theorem under the current assumptions is that [T=F] *) +Variable Bool : Prop. +Variable T : Bool. +Variable F : Bool. + +(** The powerset operator *) +Definition pow (P:Prop) := P -> Bool. + + +(** A piece of theory about retracts *) +Section Retracts. + +Variables A B : Prop. + +Record retract : Prop := + {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. +Record retract_cond : Prop := + {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. + +(** The dependent elimination above implies the axiom of choice: *) + +Lemma AC : forall r:retract_cond, retract -> forall a:A, r.(j2) (r.(i2) a) = a. +Proof. intros r. exact r.(inv2). Qed. + +End Retracts. + +(** This lemma is basically a commutation of implication and existential + quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) + which is provable in classical logic ( => is already provable in + intuitionistic logic). *) + +Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). +Proof. +intros A B. +destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. + exists f0 g0; trivial. + exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; + destruct hf; auto. +Qed. + + +(** The paradoxical set *) +Definition U := forall P:Prop, pow P. + +(** Bijection between [U] and [(pow U)] *) +Definition f (u:U) : pow U := u U. + +Definition g (h:pow U) : U := + fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h). + +(** We deduce that the powerset of [U] is a retract of [U]. + This lemma is stated in Berardi's article, but is not used + afterwards. *) +Lemma retract_pow_U_U : retract (pow U) U. +Proof. +exists g f. +intro a. +unfold f, g; simpl. +apply AC. +exists (fun x:pow U => x) (fun x:pow U => x). +trivial. +Qed. + +(** Encoding of Russel's paradox *) + +(** The boolean negation. *) +Definition Not_b (b:Bool) := IFProp (b = T) F T. + +(** the set of elements not belonging to itself *) +Definition R : U := g (fun u:U => Not_b (u U u)). + + +Lemma not_has_fixpoint : R R = Not_b (R R). +Proof. +unfold R at 1. +unfold g. +rewrite AC. +trivial. +exists (fun x:pow U => x) (fun x:pow U => x). +trivial. +Qed. + + +Theorem classical_proof_irrelevance : T = F. +Proof. +generalize not_has_fixpoint. +unfold Not_b. +apply AC_IF. +intros is_true is_false. +elim is_true; elim is_false; trivial. + +intros not_true is_true. +elim not_true; trivial. +Qed. + + +Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8"). + +End Berardis_paradox. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v new file mode 100644 index 0000000000..238ac7df0b --- /dev/null +++ b/theories/Logic/ChoiceFacts.v @@ -0,0 +1,1320 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(************************************************************************) + +(** Some facts and definitions concerning choice and description in + intuitionistic logic. *) +(** * 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öm04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to +AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + +[[Carlström05]] Jesper Carlström, Interpreting descriptions in +intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. + +[[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997. +*) + +Require Import RelationClasses Logic. + +Set Implicit Arguments. +Local Unset Intuition Negation Unfolding. + +(**********************************************************************) +(** * Definitions *) + +(** Choice, reification and description schemes *) + +(** We make them all polymorphic. Most of them have existentials as conclusion + so they require polymorphism otherwise their first application (e.g. to an + existential in [Set]) will fix the level of [A]. +*) +(* Set Universe Polymorphism. *) + +Section ChoiceSchemes. + +Variables A B :Type. + +Variable P:A->Prop. + +(** ** Constructive choice and description *) + +(** AC_rel = relational form of the (non extensional) axiom of choice + (a "set-theoretic" axiom of choice) *) + +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 = functional form of the (non extensional) axiom of choice + (a "type-theoretic" axiom of choice) *) + +(* Note: This is called Type-Theoretic Description Axiom (TTDA) in + [[Werner97]] (using a non-standard meaning of "description"). This + is called intensional axiom of choice (AC_int) in [[Carlström04]] *) + +Definition FunctionalChoice_on_rel (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 := + 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_fun_dep = functional form of the (non extensional) axiom of + choice, with dependent functions *) +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)). + +(** AC_trunc = axiom of choice for propositional truncations + (truncation and quantification commute) *) +Definition InhabitedForallCommute_on (A : Type) (B : A -> Type) := + (forall x, inhabited (B x)) -> inhabited (forall x, B x). + +(** DC_fun = functional form of the dependent axiom of choice *) + +Definition FunctionalDependentChoice_on := + forall (R:A->A->Prop), + (forall x, exists y, R x y) -> forall x0, + (exists f : nat -> A, f 0 = x0 /\ forall n, R (f n) (f (S n))). + +(** ACw_fun = functional form of the countable axiom of choice *) + +Definition FunctionalCountableChoice_on := + forall (R:nat->A->Prop), + (forall n, exists y, R n y) -> + (exists f : nat -> A, forall n, R n (f n)). + +(** AC! = functional relation reification + (known as axiom of unique choice in topos theory, + sometimes called principle of definite description in + the context of constructive type theory, sometimes + called axiom of no choice) *) + +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)). + +(** AC_dep! = functional relation reification, with dependent functions + see AC! *) +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)). + +(** AC_fun_repr = functional choice of a representative in an equivalence class *) + +(* Note: This is called Type-Theoretic Choice Axiom (TTCA) in + [[Werner97]] (by reference to the extensional set-theoretic + formulation of choice); Note also a typo in its intended + formulation in [[Werner97]]. *) + +Definition RepresentativeFunctionalChoice_on := + forall R:A->A->Prop, + (Equivalence R) -> + (exists f : A->A, forall x : A, (R x (f x)) /\ forall x', R x x' -> f x = f x'). + +(** AC_fun_setoid = functional form of the (so-called extensional) axiom of + choice from setoids *) + +Definition SetoidFunctionalChoice_on := + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x x' y, R x x' -> T x y -> T x' y) -> + (forall x, exists y, T x y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). + +(** AC_fun_setoid_gen = functional form of the general form of the (so-called + extensional) axiom of choice over setoids *) + +(* Note: This is called extensional axiom of choice (AC_ext) in + [[Carlström04]]. *) + +Definition GeneralizedSetoidFunctionalChoice_on := + forall R : A -> A -> Prop, + forall S : B -> B -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + Equivalence S -> + (forall x x' y y', R x x' -> S y y' -> T x y -> T x' y') -> + (forall x, exists y, T x y) -> + exists f : A -> B, + forall x : A, T x (f x) /\ (forall x' : A, R x x' -> S (f x) (f x')). + +(** AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of + choice from setoids on locally compatible relations *) + +Definition SimpleSetoidFunctionalChoice_on A B := + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x, exists y, forall x', R x x' -> T x' y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f 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 *) + +(** GAC_rel = guarded relational form of the (non extensional) axiom of choice *) + +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 = guarded functional form of the (non extensional) axiom of choice *) + +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)). + +(** GAC! = guarded functional relation reification *) + +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 = "omniscient" relational form of the (non extensional) axiom of choice *) + +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 = "omniscient" functional form of the (non extensional) axiom of choice + (called AC* in Bell [[Bell]]) *) + +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 = (weakly classical) indefinite description principle *) + +Definition EpsilonStatement_on := + forall P:A->Prop, + inhabited A -> { x:A | (exists x, P x) -> P x }. + +(** D_iota = (weakly classical) definite description principle *) + +Definition IotaStatement_on := + forall P:A->Prop, + inhabited A -> { x:A | (exists! x, P x) -> P x }. + +End ChoiceSchemes. + +(** Generalized schemes *) + +Notation RelationalChoice := + (forall A B : Type, RelationalChoice_on A B). +Notation FunctionalChoice := + (forall A B : Type, FunctionalChoice_on A B). +Notation DependentFunctionalChoice := + (forall A (B:A->Type), DependentFunctionalChoice_on B). +Notation InhabitedForallCommute := + (forall A (B : A -> Type), InhabitedForallCommute_on B). +Notation FunctionalDependentChoice := + (forall A : Type, FunctionalDependentChoice_on A). +Notation FunctionalCountableChoice := + (forall A : Type, FunctionalCountableChoice_on A). +Notation FunctionalChoiceOnInhabitedSet := + (forall A B : Type, inhabited B -> FunctionalChoice_on A B). +Notation FunctionalRelReification := + (forall A B : Type, FunctionalRelReification_on A B). +Notation DependentFunctionalRelReification := + (forall A (B:A->Type), DependentFunctionalRelReification_on B). +Notation RepresentativeFunctionalChoice := + (forall A : Type, RepresentativeFunctionalChoice_on A). +Notation SetoidFunctionalChoice := + (forall A B: Type, SetoidFunctionalChoice_on A B). +Notation GeneralizedSetoidFunctionalChoice := + (forall A B : Type, GeneralizedSetoidFunctionalChoice_on A B). +Notation SimpleSetoidFunctionalChoice := + (forall A B : Type, SimpleSetoidFunctionalChoice_on A B). + +Notation GuardedRelationalChoice := + (forall A B : Type, GuardedRelationalChoice_on A B). +Notation GuardedFunctionalChoice := + (forall A B : Type, GuardedFunctionalChoice_on A B). +Notation GuardedFunctionalRelReification := + (forall A B : Type, GuardedFunctionalRelReification_on A B). + +Notation OmniscientRelationalChoice := + (forall A B : Type, OmniscientRelationalChoice_on A B). +Notation OmniscientFunctionalChoice := + (forall A B : Type, OmniscientFunctionalChoice_on A B). + +Notation ConstructiveDefiniteDescription := + (forall A : Type, ConstructiveDefiniteDescription_on A). +Notation ConstructiveIndefiniteDescription := + (forall A : Type, ConstructiveIndefiniteDescription_on A). + +Notation IotaStatement := + (forall A : Type, IotaStatement_on A). +Notation EpsilonStatement := + (forall A : Type, EpsilonStatement_on A). + +(** Subclassical schemes *) + +(** PI = proof irrelevance *) +Definition ProofIrrelevance := + forall (A:Prop) (a1 a2:A), a1 = a2. + +(** IGP = independence of general premises + (an unconstrained generalisation of the constructive principle of + independence of premises) *) +Definition IndependenceOfGeneralPremises := + forall (A:Type) (P:A -> Prop) (Q:Prop), + inhabited A -> + (Q -> exists x, P x) -> exists x, Q -> P x. + +(** Drinker = drinker's paradox (small form) + (called Ex in Bell [[Bell]]) *) +Definition SmallDrinker'sParadox := + forall (A:Type) (P:A -> Prop), inhabited A -> + exists x, (exists x, P x) -> P x. + +(** EM = excluded-middle *) +Definition ExcludedMiddle := + forall P:Prop, P \/ ~ P. + +(** Extensional schemes *) + +(** Ext_prop_repr = choice of a representative among extensional propositions *) +Local Notation ExtensionalPropositionRepresentative := + (forall (A:Type), + exists h : Prop -> Prop, + forall P : Prop, (P <-> h P) /\ forall Q, (P <-> Q) -> h P = h Q). + +(** Ext_pred_repr = choice of a representative among extensional predicates *) +Local Notation ExtensionalPredicateRepresentative := + (forall (A:Type), + exists h : (A->Prop) -> (A->Prop), + forall (P : A -> Prop), (forall x, P x <-> h P x) /\ forall Q, (forall x, P x <-> Q x) -> h P = h Q). + +(** Ext_fun_repr = choice of a representative among extensional functions *) +Local Notation ExtensionalFunctionRepresentative := + (forall (A B:Type), + exists h : (A->B) -> (A->B), + forall (f : A -> B), (forall x, f x = h f x) /\ forall g, (forall x, f x = g x) -> h f = h g). + +(** We let also + +- 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-emptiness of domains +*) + +(**********************************************************************) +(** * Table of contents *) + +(* This is very fragile. *) +(** +1. Definitions + +2. IPL_2^2 |- AC_rel + AC! = AC_fun + +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 + +3.3. D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker + +4. Derivability of choice for decidable relations with well-ordered codomain + +5. AC_fun = AC_fun_dep = AC_trunc + +6. Non contradiction of constructive descriptions wrt functional choices + +7. Definite description transports classical logic to the computational world + +8. Choice -> Dependent choice -> Countable choice + +9.1. AC_fun_setoid = AC_fun + Ext_fun_repr + EM + +9.2. AC_fun_setoid = AC_fun + Ext_pred_repr + PI + *) + +(**********************************************************************) +(** * 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) + 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 functional relation reification conflicts with classical logic *) + +Lemma functional_rel_reification_and_rel_choice_imp_fun_choice : + 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. + destruct (H0 x) as (y,(HR'xy,Huniq)). + rewrite <- (Huniq (f x) (Hf x)). + apply HR'R; assumption. +Qed. + +Lemma fun_choice_imp_rel_choice : + forall A B : Type, 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 fun_choice_imp_functional_rel_reification : + forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B. +Proof. + intros A B FunCh R H. + destruct (FunCh R) as [f H0]. + (* 1 *) + intro x. + destruct (H x) as (y,(HRxy,_)). + exists y; exact HRxy. + (* 2 *) + exists f; exact H0. +Qed. + +Corollary fun_choice_iff_rel_choice_and_functional_rel_reification : + forall A B : Type, FunctionalChoice_on A B <-> + RelationalChoice_on A B /\ FunctionalRelReification_on A B. +Proof. + intros A B. split. + intro H; split; + [ exact (fun_choice_imp_rel_choice H) + | exact (fun_choice_imp_functional_rel_reification H) ]. + intros [H H0]; exact (functional_rel_reification_and_rel_choice_imp_fun_choice H0 H). +Qed. + +(**********************************************************************) +(** * Connection between the guarded, non guarded and omniscient choices *) + +(** 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 independence 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 *) + +Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : + RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice. +Proof. + intros rel_choice proof_irrel. + red; intros A B P R H. + 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''; 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. + rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'. +Qed. + +Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice : + forall A B : Type, 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 : Type, 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. + +Lemma subset_types_imp_guarded_rel_choice_iff_rel_choice : + ProofIrrelevance -> (GuardedRelationalChoice <-> RelationalChoice). +Proof. + intuition auto using + guarded_rel_choice_imp_rel_choice, + rel_choice_and_proof_irrel_imp_guarded_rel_choice. +Qed. + +(** OAC_rel = GAC_rel *) + +Corollary 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. + +(**********************************************************************) +(** ** 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. + +Corollary fun_choice_and_indep_general_prem_iff_guarded_fun_choice : + FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises + <-> GuardedFunctionalChoice. +Proof. + intuition auto 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]] *) + +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. + +Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice : + FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox + <-> OmniscientFunctionalChoice. +Proof. + intuition auto 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 *) + +Theorem 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_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. + intuition auto 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 + 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 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. +Require Import Decidable. + +Lemma classical_denumerable_description_imp_fun_choice : + forall A:Type, + 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; 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). + 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,_). + assumption. +Qed. + +(**********************************************************************) +(** * AC_fun = AC_fun_dep = AC_trunc *) + +(** ** Choice on dependent and non dependent function types are equivalent *) + +(** 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. + +(** ** Functional choice and truncation choice are equivalent *) + +Theorem functional_choice_to_inhabited_forall_commute : + FunctionalChoice -> InhabitedForallCommute. +Proof. + intros choose0 A B Hinhab. + pose proof (non_dep_dep_functional_choice choose0) as choose;clear choose0. + assert (Hexists : forall x, exists _ : B x, True). + { intros x;apply inhabited_sig_to_exists. + refine (inhabited_covariant _ (Hinhab x)). + intros y;exists y;exact I. } + apply choose in Hexists. + destruct Hexists as [f _]. + exact (inhabits f). +Qed. + +Theorem inhabited_forall_commute_to_functional_choice : + InhabitedForallCommute -> FunctionalChoice. +Proof. + intros choose A B R Hexists. + assert (Hinhab : forall x, inhabited {y : B | R x y}). + { intros x;apply exists_to_inhabited_sig;trivial. } + apply choose in Hinhab. destruct Hinhab as [f]. + exists (fun x => proj1_sig (f x)). + exact (fun x => proj2_sig (f x)). +Qed. + +(** ** Reification of dependent and non dependent functional relation are equivalent *) + +(** 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. + +Corollary dep_iff_non_dep_functional_rel_reification : + FunctionalRelReification <-> DependentFunctionalRelReification. +Proof. + intuition auto 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_descr : + forall C:Prop, (ConstructiveIndefiniteDescription -> C) + -> (FunctionalChoice -> C). +Proof. + 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). + 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 _ A (existT _ P H'))). + pose (Hf' := Hf (existT _ A (existT _ 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. + +(** ** Non contradiction of definite description *) + +Lemma relative_non_contradiction_of_definite_descr : + forall C:Prop, (ConstructiveDefiniteDescription -> C) + -> (FunctionalRelReification -> C). +Proof. + 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). + 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 _ A (existT _ P H'))). + pose (Hf' := Hf (existT _ A (existT _ 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. + +(** 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]] *) + +(** 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 : + (forall A : Type, ConstructiveDefiniteDescription_on A) -> + (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). + red in Descr. + 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. + +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 H. intuition auto using + constructive_definite_descr_excluded_middle, + (relative_non_contradiction_of_definite_descr (C:=C)). +Qed. + +(**********************************************************************) +(** * Choice => Dependent choice => Countable choice *) +(* The implications below are standard *) + +Require Import Arith. + +Theorem functional_choice_imp_functional_dependent_choice : + FunctionalChoice -> FunctionalDependentChoice. +Proof. + intros FunChoice A R HRfun x0. + apply FunChoice in HRfun as (g,Rg). + set (f:=fix f n := match n with 0 => x0 | S n' => g (f n') end). + exists f; firstorder. +Qed. + +Theorem functional_dependent_choice_imp_functional_countable_choice : + FunctionalDependentChoice -> FunctionalCountableChoice. +Proof. + intros H A R H0. + set (R' (p q:nat*A) := fst q = S (fst p) /\ R (fst p) (snd q)). + destruct (H0 0) as (y0,Hy0). + destruct H with (R:=R') (x0:=(0,y0)) as (f,(Hf0,HfS)). + intro x; destruct (H0 (fst x)) as (y,Hy). + exists (S (fst x),y). + red. auto. + assert (Heq:forall n, fst (f n) = n). + induction n. + rewrite Hf0; reflexivity. + specialize HfS with n; destruct HfS as (->,_); congruence. + exists (fun n => snd (f (S n))). + intro n'. specialize HfS with n'. + destruct HfS as (_,HR). + rewrite Heq in HR. + assumption. +Qed. + +(**********************************************************************) +(** * About the axiom of choice over setoids *) + +Require Import ClassicalFacts PropExtensionalityFacts. + +(**********************************************************************) +(** ** Consequences of the choice of a representative in an equivalence class *) + +Theorem repr_fun_choice_imp_ext_prop_repr : + RepresentativeFunctionalChoice -> ExtensionalPropositionRepresentative. +Proof. + intros ReprFunChoice A. + pose (R P Q := P <-> Q). + assert (Hequiv:Equivalence R) by (split; firstorder). + apply (ReprFunChoice _ R Hequiv). +Qed. + +Theorem repr_fun_choice_imp_ext_pred_repr : + RepresentativeFunctionalChoice -> ExtensionalPredicateRepresentative. +Proof. + intros ReprFunChoice A. + pose (R P Q := forall x : A, P x <-> Q x). + assert (Hequiv:Equivalence R) by (split; firstorder). + apply (ReprFunChoice _ R Hequiv). +Qed. + +Theorem repr_fun_choice_imp_ext_function_repr : + RepresentativeFunctionalChoice -> ExtensionalFunctionRepresentative. +Proof. + intros ReprFunChoice A B. + pose (R (f g : A -> B) := forall x : A, f x = g x). + assert (Hequiv:Equivalence R). + { split; try easy. firstorder using eq_trans. } + apply (ReprFunChoice _ R Hequiv). +Qed. + +(** *** This is a variant of Diaconescu and Goodman-Myhill theorems *) + +Theorem repr_fun_choice_imp_excluded_middle : + RepresentativeFunctionalChoice -> ExcludedMiddle. +Proof. + intros ReprFunChoice. + apply representative_boolean_partition_imp_excluded_middle, ReprFunChoice. +Qed. + +Theorem repr_fun_choice_imp_relational_choice : + RepresentativeFunctionalChoice -> RelationalChoice. +Proof. + intros ReprFunChoice A B T Hexists. + pose (D := (A*B)%type). + pose (R (z z':D) := + let x := fst z in + let x' := fst z' in + let y := snd z in + let y' := snd z' in + x = x' /\ (T x y -> y = y' \/ T x y') /\ (T x y' -> y = y' \/ T x y)). + assert (Hequiv : Equivalence R). + { split. + - split. easy. firstorder. + - intros (x,y) (x',y') (H1,(H2,H2')). split. easy. simpl fst in *. simpl snd in *. + subst x'. split; intro H. + + destruct (H2' H); firstorder. + + destruct (H2 H); firstorder. + - intros (x,y) (x',y') (x'',y'') (H1,(H2,H2')) (H3,(H4,H4')). + simpl fst in *. simpl snd in *. subst x'' x'. split. easy. split; intro H. + + simpl fst in *. simpl snd in *. destruct (H2 H) as [<-|H0]. + * destruct (H4 H); firstorder. + * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. + + simpl fst in *. simpl snd in *. destruct (H4' H) as [<-|H0]. + * destruct (H2' H); firstorder. + * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. } + destruct (ReprFunChoice D R Hequiv) as (g,Hg). + set (T' x y := T x y /\ exists y', T x y' /\ g (x,y') = (x,y)). + exists T'. split. + - intros x y (H,_); easy. + - intro x. destruct (Hexists x) as (y,Hy). + exists (snd (g (x,y))). + destruct (Hg (x,y)) as ((Heq1,(H',H'')),Hgxyuniq); clear Hg. + destruct (H' Hy) as [Heq2|Hgy]; clear H'. + + split. split. + * rewrite <- Heq2. assumption. + * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1, Heq2. subst; easy. + * intros y' (Hy',(y'',(Hy'',Heq))). + rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy. + split; right; easy. + + split. split. + * assumption. + * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1. subst x'; easy. + * intros y' (Hy',(y'',(Hy'',Heq))). + rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy. + split; right; easy. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC_fun_setoid_gen = AC_fun_setoid_simple *) + +Theorem gen_setoid_fun_choice_imp_setoid_fun_choice : + forall A B, GeneralizedSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B. +Proof. + intros A B GenSetoidFunChoice R T Hequiv Hcompat Hex. + apply GenSetoidFunChoice; try easy. + apply eq_equivalence. + intros * H <-. firstorder. +Qed. + +Theorem setoid_fun_choice_imp_gen_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> GeneralizedSetoidFunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice R S T HequivR HequivS Hcompat Hex. + destruct SetoidFunChoice with (R:=R) (T:=T) as (f,Hf); try easy. + { intros; apply (Hcompat x x' y y); try easy. } + exists f. intros x; specialize Hf with x as (Hf,Huniq). intuition. now erewrite Huniq. +Qed. + +Corollary setoid_fun_choice_iff_gen_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B <-> GeneralizedSetoidFunctionalChoice_on A B. +Proof. + split; auto using gen_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_gen_setoid_fun_choice. +Qed. + +Theorem setoid_fun_choice_imp_simple_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> SimpleSetoidFunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice R T Hequiv Hexists. + pose (T' x y := forall x', R x x' -> T x' y). + assert (Hcompat : forall (x x' : A) (y : B), R x x' -> T' x y -> T' x' y) by firstorder. + destruct (SetoidFunChoice R T' Hequiv Hcompat Hexists) as (f,Hf). + exists f. firstorder. +Qed. + +Theorem simple_setoid_fun_choice_imp_setoid_fun_choice : + forall A B, SimpleSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B. +Proof. + intros A B SimpleSetoidFunChoice R T Hequiv Hcompat Hexists. + destruct (SimpleSetoidFunChoice R T Hequiv) as (f,Hf); firstorder. +Qed. + +Corollary setoid_fun_choice_iff_simple_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B <-> SimpleSetoidFunctionalChoice_on A B. +Proof. + split; auto using simple_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_simple_setoid_fun_choice. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC! + AC_fun_repr *) + +Theorem setoid_fun_choice_imp_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> FunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice T Hexists. + destruct SetoidFunChoice with (R:=@eq A) (T:=T) as (f,Hf). + - apply eq_equivalence. + - now intros * ->. + - assumption. + - exists f. firstorder. +Qed. + +Corollary setoid_fun_choice_imp_functional_rel_reification : + forall A B, SetoidFunctionalChoice_on A B -> FunctionalRelReification_on A B. +Proof. + intros A B SetoidFunChoice. + apply fun_choice_imp_functional_rel_reification. + now apply setoid_fun_choice_imp_fun_choice. +Qed. + +Theorem setoid_fun_choice_imp_repr_fun_choice : + SetoidFunctionalChoice -> RepresentativeFunctionalChoice . +Proof. + intros SetoidFunChoice A R Hequiv. + apply SetoidFunChoice; firstorder. +Qed. + +Theorem functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice : + FunctionalRelReification -> RepresentativeFunctionalChoice -> SetoidFunctionalChoice. +Proof. + intros FunRelReify ReprFunChoice A B R T Hequiv Hcompat Hexists. + assert (FunChoice : FunctionalChoice). + { intros A' B'. apply functional_rel_reification_and_rel_choice_imp_fun_choice. + - apply FunRelReify. + - now apply repr_fun_choice_imp_relational_choice. } + destruct (FunChoice _ _ T Hexists) as (f,Hf). + destruct (ReprFunChoice A R Hequiv) as (g,Hg). + exists (fun a => f (g a)). + intro x. destruct (Hg x) as (Hgx,HRuniq). + split. + - eapply Hcompat. symmetry. apply Hgx. apply Hf. + - intros y Hxy. f_equal. auto. +Qed. + +Theorem functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice : + FunctionalRelReification /\ RepresentativeFunctionalChoice <-> SetoidFunctionalChoice. +Proof. + split; intros. + - now apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + - split. + + now intros A B; apply setoid_fun_choice_imp_functional_rel_reification. + + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. + +(** Note: What characterization to give of +RepresentativeFunctionalChoice? A formulation of it as a functional +relation would certainly be equivalent to the formulation of +SetoidFunctionalChoice as a functional relation, but in their +functional forms, SetoidFunctionalChoice seems strictly stronger *) + +(**********************************************************************) +(** * AC_fun_setoid = AC_fun + Ext_fun_repr + EM *) + +Import EqNotations. + +(** ** This is the main theorem in [[Carlström04]] *) + +(** Note: all ingredients have a computational meaning when taken in + separation. However, to compute with the functional choice, + existential quantification has to be thought as a strong + existential, which is incompatible with the computational content of + excluded-middle *) + +Theorem fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice : + FunctionalChoice -> ExtensionalFunctionRepresentative -> ExcludedMiddle -> RepresentativeFunctionalChoice. +Proof. + intros FunChoice SetoidFunRepr EM A R (Hrefl,Hsym,Htrans). + assert (H:forall P:Prop, exists b, b = true <-> P). + { intros P. destruct (EM P). + - exists true; firstorder. + - exists false; easy. } + destruct (FunChoice _ _ _ H) as (c,Hc). + pose (class_of a y := c (R a y)). + pose (isclass f := exists x:A, f x = true). + pose (class := {f:A -> bool | isclass f}). + pose (contains (c:class) (a:A) := proj1_sig c a = true). + destruct (FunChoice class A contains) as (f,Hf). + - intros f. destruct (proj2_sig f) as (x,Hx). + exists x. easy. + - destruct (SetoidFunRepr A bool) as (h,Hh). + assert (Hisclass:forall a, isclass (h (class_of a))). + { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). + rewrite <- Ha. apply Hc. apply Hrefl. } + pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). + exists (fun a => f (f' a)). + intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + + specialize Hf with (f' x). unfold contains in Hf. simpl in Hf. rewrite <- Hx in Hf. apply Hc. assumption. + + intros y Hxy. + f_equal. + assert (Heq1: h (class_of x) = h (class_of y)). + { apply Huniqx. intro z. unfold class_of. + destruct (c (R x z)) eqn:Hxz. + - symmetry. apply Hc. apply -> Hc in Hxz. firstorder. + - destruct (c (R y z)) eqn:Hyz. + + apply -> Hc in Hyz. rewrite <- Hxz. apply Hc. firstorder. + + easy. } + assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). + { apply proof_irrelevance_cci, EM. } + unfold f'. + rewrite <- Heq2. + rewrite <- Heq1. + reflexivity. +Qed. + +Theorem setoid_functional_choice_first_characterization : + FunctionalChoice /\ ExtensionalFunctionRepresentative /\ ExcludedMiddle <-> SetoidFunctionalChoice. +Proof. + split. + - intros (FunChoice & SetoidFunRepr & EM). + apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + + intros A B. apply fun_choice_imp_functional_rel_reification, FunChoice. + + now apply fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice. + - intro SetoidFunChoice. repeat split. + + now intros A B; apply setoid_fun_choice_imp_fun_choice. + + apply repr_fun_choice_imp_ext_function_repr. + now apply setoid_fun_choice_imp_repr_fun_choice. + + apply repr_fun_choice_imp_excluded_middle. + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC_fun + Ext_pred_repr + PI *) + +(** Note: all ingredients have a computational meaning when taken in + separation. However, to compute with the functional choice, + existential quantification has to be thought as a strong + existential, which is incompatible with proof-irrelevance which + requires existential quantification to be truncated *) + +Theorem fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice : + FunctionalChoice -> ExtensionalPredicateRepresentative -> ProofIrrelevance -> RepresentativeFunctionalChoice. +Proof. + intros FunChoice PredExtRepr PI A R (Hrefl,Hsym,Htrans). + pose (isclass P := exists x:A, P x). + pose (class := {P:A -> Prop | isclass P}). + pose (contains (c:class) (a:A) := proj1_sig c a). + pose (class_of a := R a). + destruct (FunChoice class A contains) as (f,Hf). + - intros c. apply proj2_sig. + - destruct (PredExtRepr A) as (h,Hh). + assert (Hisclass:forall a, isclass (h (class_of a))). + { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). + rewrite <- Ha; apply Hrefl. } + pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). + exists (fun a => f (f' a)). + intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + + specialize Hf with (f' x). simpl in Hf. rewrite <- Hx in Hf. assumption. + + intros y Hxy. + f_equal. + assert (Heq1: h (class_of x) = h (class_of y)). + { apply Huniqx. intro z. unfold class_of. firstorder. } + assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). + { apply PI. } + unfold f'. + rewrite <- Heq2. + rewrite <- Heq1. + reflexivity. +Qed. + +Theorem setoid_functional_choice_second_characterization : + FunctionalChoice /\ ExtensionalPredicateRepresentative /\ ProofIrrelevance <-> SetoidFunctionalChoice. +Proof. + split. + - intros (FunChoice & ExtPredRepr & PI). + apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + + intros A B. now apply fun_choice_imp_functional_rel_reification. + + now apply fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice. + - intro SetoidFunChoice. repeat split. + + now intros A B; apply setoid_fun_choice_imp_fun_choice. + + apply repr_fun_choice_imp_ext_pred_repr. + now apply setoid_fun_choice_imp_repr_fun_choice. + + red. apply proof_irrelevance_cci. + apply repr_fun_choice_imp_excluded_middle. + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. + +(**********************************************************************) +(** * Compatibility notations *) +Notation description_rel_choice_imp_funct_choice := + functional_rel_reification_and_rel_choice_imp_fun_choice (only parsing). + +Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (only parsing). + +Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := + fun_choice_iff_rel_choice_and_functional_rel_reification (only parsing). + +Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (only parsing). diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v new file mode 100644 index 0000000000..72f53a46e1 --- /dev/null +++ b/theories/Logic/Classical.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* File created for Coq V5.10.14b, Oct 1995 *) + +(** Classical Logic *) + +Require Export Classical_Prop. +Require Export Classical_Pred_Type. + diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v new file mode 100644 index 0000000000..016fa72f9b --- /dev/null +++ b/theories/Logic/ClassicalChoice.v @@ -0,0 +1,51 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** 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 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 + impredicativity of [Set], knowing that [true<>false] in [Set]. *) + +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)). +Proof. +intros A B. +apply description_rel_choice_imp_funct_choice. +exact (unique_choice A B). +exact (relational_choice A B). +Qed. diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v new file mode 100644 index 0000000000..6867c76e21 --- /dev/null +++ b/theories/Logic/ClassicalDescription.v @@ -0,0 +1,87 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This file provides classical logic and definite description, which is + equivalent to providing classical logic and Church's iota operator *) + +(** 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. + +Require Export Classical. (* Axiomatize classical reasoning *) +Require Export Description. (* Axiomatize constructive form of Church's iota *) +Require Import ChoiceFacts. + +Local Notation inhabited A := A (only parsing). + +(** 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 *) + +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). + +(** Axiom of unique "choice" (functional reification of functional relations) *) +Theorem dependent_unique_choice : + 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 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. +intros A B. +apply dependent_unique_choice with (B:=fun _:A => B). +Qed. + +(** Compatibility lemmas *) + +Unset Implicit Arguments. + +Definition dependent_description := dependent_unique_choice. +Definition description := unique_choice. diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v new file mode 100644 index 0000000000..77af904812 --- /dev/null +++ b/theories/Logic/ClassicalEpsilon.v @@ -0,0 +1,103 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(************************************************************************) + +(** This file provides classical logic and indefinite description under + the form of Hilbert's epsilon operator *) + +(** 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] *) + +Require Export Classical. +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. + +Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}. +Proof. + apply + (constructive_definite_descr_excluded_middle + constructive_definite_description classic). +Qed. + +Theorem classical_indefinite_description : + forall (A : Type) (P : A->Prop), inhabited A -> + { x : A | (exists x, P x) -> P x }. +Proof. + intros A P i. + destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP]. + apply constructive_indefinite_description + with (P:= fun x => (exists x, P x) -> P x). + destruct Hex as (x,Hx). + exists x; intros _; exact Hx. + assert {x : A | True} as (a,_). + apply constructive_indefinite_description with (P := fun _ : A => True). + destruct i as (a); firstorder. + firstorder. +Defined. + +(** Hilbert's epsilon operator *) + +Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A + := proj1_sig (classical_indefinite_description P i). + +Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : + (exists x, P x) -> P (epsilon i P) + := proj2_sig (classical_indefinite_description P i). + +(** Open question: is classical_indefinite_description constructively + provable from [relational_choice] and + [constructive_definite_description] (at least, using the fact that + [functional_choice] is provable from [relational_choice] and + [unique_choice], we know that the double negation of + [classical_indefinite_description] is provable (see + [relative_non_contradiction_of_indefinite_desc]). *) + +(** A proof that if [P] is inhabited, [epsilon a P] does not depend on + the actual proof that the domain of [P] is inhabited + (proof idea kindly provided by Pierre Castéran) *) + +Lemma epsilon_inh_irrelevance : + forall (A:Type) (i j : inhabited A) (P:A->Prop), + (exists x, P x) -> epsilon i P = epsilon j P. +Proof. + intros. + unfold epsilon, classical_indefinite_description. + destruct (excluded_middle_informative (exists x : A, P x)) as [|[]]; trivial. +Qed. + +Opaque epsilon. + +(** *** Weaker lemmas (compatibility lemmas) *) + +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)). +Proof. + intros A B R H. + exists (fun x => proj1_sig (constructive_indefinite_description _ (H x))). + intro x. + apply (proj2_sig (constructive_indefinite_description _ (H x))). +Qed. + diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v new file mode 100644 index 0000000000..b06384e992 --- /dev/null +++ b/theories/Logic/ClassicalFacts.v @@ -0,0 +1,800 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Some facts and definitions about classical logic + +Table of contents: + +1. Propositional degeneracy = excluded-middle + propositional extensionality + +2. Classical logic and proof-irrelevance + +2.1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint + +2.2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance + +2.3. CIC |- prop. ext. -> proof-irrelevance + +2.4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance + +2.5. CIC |- excluded-middle -> proof-irrelevance + +3. Weak classical axioms + +3.1. Weak excluded middle + +3.2. Gödel-Dummett axiom and right distributivity of implication over + disjunction + +3 3. Independence of general premises and drinker's paradox + +4. Principles equivalent to classical logic + +4.1 Classical logic = principle of unrestricted minimization + +4.2 Classical logic = choice of representatives in a partition of bool +*) + +(************************************************************************) +(** * Prop degeneracy = excluded-middle + prop extensionality *) +(** + i.e. [(forall A, A=True \/ A=False) + <-> + (forall A, A\/~A) /\ (forall A B, (A<->B) -> A=B)] +*) + +(** [prop_degeneracy] (also referred to as propositional completeness) + asserts (up to consistency) that there are only two distinct formulas *) +Definition prop_degeneracy := forall A:Prop, A = True \/ A = False. + +(** [prop_extensionality] asserts that equivalent formulas are equal *) +Definition prop_extensionality := forall A B:Prop, (A <-> B) -> A = B. + +(** [excluded_middle] asserts that we can reason by case on the truth + or falsity of any formula *) +Definition excluded_middle := forall A:Prop, A \/ ~ A. + +(** We show [prop_degeneracy <-> (prop_extensionality /\ excluded_middle)] *) + +Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality. +Proof. + intros H A B [Hab Hba]. + destruct (H A); destruct (H B). + rewrite H1; exact H0. + absurd B. + rewrite H1; exact (fun H => H). + apply Hab; rewrite H0; exact I. + absurd A. + rewrite H0; exact (fun H => H). + apply Hba; rewrite H1; exact I. + rewrite H1; exact H0. +Qed. + +Lemma prop_degen_em : prop_degeneracy -> excluded_middle. +Proof. + intros H A. + destruct (H A). + left; rewrite H0; exact I. + right; rewrite H0; exact (fun x => x). +Qed. + +Lemma prop_ext_em_degen : + prop_extensionality -> excluded_middle -> prop_degeneracy. +Proof. + intros Ext EM A. + destruct (EM A). + left; apply (Ext A True); split; + [ exact (fun _ => I) | exact (fun _ => H) ]. + right; apply (Ext A False); split; [ exact H | apply False_ind ]. +Qed. + +(** A weakest form of propositional extensionality: extensionality for + provable propositions only *) + +Require Import PropExtensionalityFacts. + +Definition provable_prop_extensionality := forall A:Prop, A -> A = True. + +Lemma provable_prop_ext : + prop_extensionality -> provable_prop_extensionality. +Proof. + exact PropExt_imp_ProvPropExt. +Qed. + +(************************************************************************) +(** * Classical logic and proof-irrelevance *) + +(************************************************************************) +(** ** CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *) + +(** We successively show that: + + [prop_extensionality] + implies equality of [A] and [A->A] for inhabited [A], which + implies the existence of a (trivial) retract from [A->A] to [A] + (just take the identity), which + implies the existence of a fixpoint operator in [A] + (e.g. take the Y combinator of lambda-calculus) + +*) + +Local Notation inhabited A := A (only parsing). + +Lemma prop_ext_A_eq_A_imp_A : + prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. +Proof. + intros Ext A a. + apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ]. +Qed. + +Record retract (A B:Prop) : Prop := + {f1 : A -> B; f2 : B -> A; f1_o_f2 : forall x:B, f1 (f2 x) = x}. + +Lemma prop_ext_retract_A_A_imp_A : + prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A). +Proof. + intros Ext A a. + rewrite (prop_ext_A_eq_A_imp_A Ext A a). + exists (fun x:A => x) (fun x:A => x). + reflexivity. +Qed. + +Record has_fixpoint (A:Prop) : Prop := + {F : (A -> A) -> A; Fix : forall f:A -> A, F f = f (F f)}. + +Lemma ext_prop_fixpoint : + prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A. +Proof. + intros Ext A a. + case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2. + exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))). + intro f. + pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1. + rewrite (g1_o_g2 (fun x:A => f (g1 x x))). + 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 *) + +(** [proof_irrelevance] asserts equality of all proofs of a given formula *) +Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. + +(** Assume that we have booleans with the property that there is at most 2 + booleans (which is equivalent to dependent case analysis). Consider + the fixpoint of the negation function: it is either true or false by + dependent case analysis, but also the opposite by fixpoint. Hence + proof-irrelevance. + + We then map equality of boolean proofs to proof irrelevance in all + propositions. +*) + +Section Proof_irrelevance_gen. + + Variable bool : Prop. + Variable true : bool. + Variable false : bool. + Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C. + Hypothesis + bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true. + Hypothesis + bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false. + Let bool_dep_induction := + forall P:bool -> Prop, P true -> P false -> forall b:bool, P b. + + Lemma aux : prop_extensionality -> bool_dep_induction -> true = false. + Proof. + intros Ext Ind. + case (ext_prop_fixpoint Ext bool true); intros G Gfix. + set (neg := fun b:bool => bool_elim bool false true b). + generalize (eq_refl (G neg)). + pattern (G neg) at 1. + apply Ind with (b := G neg); intro Heq. + rewrite (bool_elim_redl bool false true). + change (true = neg true); rewrite Heq; apply Gfix. + rewrite (bool_elim_redr bool false true). + change (neg false = false); rewrite Heq; symmetry ; + apply Gfix. + Qed. + + Lemma ext_prop_dep_proof_irrel_gen : + prop_extensionality -> bool_dep_induction -> proof_irrelevance. + Proof. + intros Ext Ind A a1 a2. + set (f := fun b:bool => bool_elim A a1 a2 b). + rewrite (bool_elim_redl A a1 a2). + change (f true = a2). + rewrite (bool_elim_redr A a1 a2). + change (f true = f false). + rewrite (aux Ext Ind). + reflexivity. + Qed. + +End Proof_irrelevance_gen. + +(** In the pure Calculus of Constructions, we can define the boolean + proposition bool = (C:Prop)C->C->C but we cannot prove that it has at + most 2 elements. +*) + +Section Proof_irrelevance_Prop_Ext_CC. + + Definition BoolP := forall C:Prop, C -> C -> C. + Definition TrueP : BoolP := fun C c1 c2 => c1. + Definition FalseP : BoolP := fun C c1 c2 => c2. + Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2. + Definition BoolP_elim_redl (C:Prop) (c1 c2:C) : + c1 = BoolP_elim C c1 c2 TrueP := eq_refl c1. + Definition BoolP_elim_redr (C:Prop) (c1 c2:C) : + c2 = BoolP_elim C c1 c2 FalseP := eq_refl c2. + + Definition BoolP_dep_induction := + forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b. + + Lemma ext_prop_dep_proof_irrel_cc : + prop_extensionality -> BoolP_dep_induction -> proof_irrelevance. + Proof. + exact (ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl + BoolP_elim_redr). + Qed. + +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 *) + +(** In the Calculus of Inductive Constructions, inductively defined booleans + enjoy dependent case analysis, hence directly proof-irrelevance from + propositional extensionality. +*) + +Section Proof_irrelevance_CIC. + + Inductive boolP : Prop := + | trueP : boolP + | falseP : boolP. + Definition boolP_elim_redl (C:Prop) (c1 c2:C) : + c1 = boolP_ind C c1 c2 trueP := eq_refl c1. + Definition boolP_elim_redr (C:Prop) (c1 c2:C) : + c2 = boolP_ind C c1 c2 falseP := eq_refl c2. + Scheme boolP_indd := Induction for boolP Sort Prop. + + Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. + Proof. + exact (fun pe => + ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl + boolP_elim_redr pe boolP_indd). + Qed. + +End Proof_irrelevance_CIC. + +(** Can we state proof irrelevance from propositional degeneracy + (i.e. propositional extensionality + excluded middle) without + dependent case analysis ? + + Berardi [[Berardi90]] built a model of CC interpreting inhabited + types by the set of all untyped lambda-terms. This model satisfies + propositional degeneracy without satisfying proof-irrelevance (nor + dependent case analysis). This implies that the previous results + cannot be refined. + + [[Berardi90]] Stefano Berardi, "Type dependence and constructive + mathematics", Ph. D. thesis, Dipartimento Matematica, Università di + Torino, 1990. +*) + +(************************************************************************) +(** ** CC |- excluded-middle + dep elim on bool -> proof-irrelevance *) + +(** This is a proof in the pure Calculus of Construction that + classical logic in [Prop] + dependent elimination of disjunction entails + proof-irrelevance. + + Reference: + + [[Coquand90]] T. Coquand, "Metamathematical Investigations of a + Calculus of Constructions", Proceedings of Logic in Computer Science + (LICS'90), 1990. + + Proof skeleton: classical logic + dependent elimination of + disjunction + discrimination of proofs implies the existence of a + retract from [Prop] into [bool], hence inconsistency by encoding any + paradox of system U- (e.g. Hurkens' paradox). +*) + +Require Import Hurkens. + +Section Proof_irrelevance_EM_CC. + + Variable or : Prop -> Prop -> Prop. + Variable or_introl : forall A B:Prop, A -> or A B. + Variable or_intror : forall A B:Prop, B -> or A B. + Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C. + Hypothesis + or_elim_redl : + forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A), + f a = or_elim A B C f g (or_introl A B a). + Hypothesis + or_elim_redr : + forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B), + g b = or_elim A B C f g (or_intror A B b). + Hypothesis + or_dep_elim : + forall (A B:Prop) (P:or A B -> Prop), + (forall a:A, P (or_introl A B a)) -> + (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b. + + Hypothesis em : forall A:Prop, or A (~ A). + Variable B : Prop. + Variables b1 b2 : B. + + (** [p2b] and [b2p] form a retract if [~b1=b2] *) + + Let p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A). + Let b2p b := b1 = b. + + Lemma p2p1 : forall A:Prop, A -> b2p (p2b A). + Proof. + unfold p2b; intro A; apply or_dep_elim with (b := em A); + unfold b2p; intros. + apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)). + destruct (b H). + Qed. + + Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A. + Proof. + intro not_eq_b1_b2. + unfold p2b; intro A; apply or_dep_elim with (b := em A); + unfold b2p; intros. + assumption. + destruct not_eq_b1_b2. + rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H. + assumption. + Qed. + + (** Using excluded-middle a second time, we get proof-irrelevance *) + + Theorem proof_irrelevance_cc : b1 = b2. + Proof. + refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H. + trivial. + apply (NoRetractFromSmallPropositionToProp.paradox B p2b b2p (p2p2 H) p2p1). + Qed. + +End Proof_irrelevance_EM_CC. + +(** Hurkens' paradox still holds with a retract from the _negative_ + fragment of [Prop] into [bool], hence weak classical logic, + i.e. [forall A, ~A\/~~A], is enough for deriving a weak version of + proof-irrelevance. This is enough to derive a contradiction from a + [Set]-bound weak excluded middle wih an impredicative [Set] + universe. *) + +Section Proof_irrelevance_WEM_CC. + + Variable or : Prop -> Prop -> Prop. + Variable or_introl : forall A B:Prop, A -> or A B. + Variable or_intror : forall A B:Prop, B -> or A B. + Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C. + Hypothesis + or_elim_redl : + forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A), + f a = or_elim A B C f g (or_introl A B a). + Hypothesis + or_elim_redr : + forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B), + g b = or_elim A B C f g (or_intror A B b). + Hypothesis + or_dep_elim : + forall (A B:Prop) (P:or A B -> Prop), + (forall a:A, P (or_introl A B a)) -> + (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b. + + Hypothesis wem : forall A:Prop, or (~~A) (~ A). + + Local Notation NProp := NoRetractToNegativeProp.NProp. + Local Notation El := NoRetractToNegativeProp.El. + + Variable B : Prop. + Variables b1 b2 : B. + + (** [p2b] and [b2p] form a retract if [~b1=b2] *) + + Let p2b (A:NProp) := or_elim (~~El A) (~El A) B (fun _ => b1) (fun _ => b2) (wem (El A)). + Let b2p b : NProp := exist (fun P=>~~P -> P) (~~(b1 = b)) (fun h x => h (fun k => k x)). + + Lemma wp2p1 : forall A:NProp, El A -> El (b2p (p2b A)). + Proof. + intros A. unfold p2b. + apply or_dep_elim with (b := wem (El A)). + + intros nna a. + rewrite <- or_elim_redl. + cbn. auto. + + intros n x. + destruct (n x). + Qed. + + Lemma wp2p2 : b1 <> b2 -> forall A:NProp, El (b2p (p2b A)) -> El A. + Proof. + intro not_eq_b1_b2. + intros A. unfold p2b. + apply or_dep_elim with (b := wem (El A)). + + cbn. + intros x _. + destruct A. cbn in x |- *. + auto. + + intros na. + rewrite <- or_elim_redr. cbn. + intros h. destruct (h not_eq_b1_b2). + Qed. + + (** By Hurkens's paradox, we get a weak form of proof irrelevance. *) + + Theorem wproof_irrelevance_cc : ~~(b1 = b2). + Proof. + intros h. + unshelve (refine (let NB := exist (fun P=>~~P -> P) B _ in _)). + { exact (fun _ => b1). } + pose proof (NoRetractToNegativeProp.paradox NB p2b b2p (wp2p2 h) wp2p1) as paradox. + unshelve (refine (let F := exist (fun P=>~~P->P) False _ in _)). + { auto. } + exact (paradox F). + Qed. + +End Proof_irrelevance_WEM_CC. + +(************************************************************************) +(** ** CIC |- excluded-middle -> proof-irrelevance *) + +(** + Since, dependent elimination is derivable in the Calculus of + Inductive Constructions (CCI), we get proof-irrelevance from classical + logic in the CCI. +*) + +Section Proof_irrelevance_CCI. + + Hypothesis em : forall A:Prop, A \/ ~ A. + + Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) + (a:A) : f a = or_ind f g (or_introl B a) := eq_refl (f a). + Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) + (b:B) : g b = or_ind f g (or_intror A b) := eq_refl (g b). + Scheme or_indd := Induction for or Sort Prop. + + Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2. + Proof. + exact (proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl + or_elim_redr or_indd em). + Qed. + +End Proof_irrelevance_CCI. + +(** The same holds with weak excluded middle. The proof is a little + more involved, however. *) + + + +Section Weak_proof_irrelevance_CCI. + + Hypothesis wem : forall A:Prop, ~~A \/ ~ A. + + Theorem wem_proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), ~~b1 = b2. + Proof. + exact (wproof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl + or_elim_redr or_indd wem). + Qed. + +End Weak_proof_irrelevance_CCI. + +(** Remark: in the Set-impredicative CCI, Hurkens' paradox still holds with + [bool] in [Set] and since [~true=false] for [true] and [false] + in [bool] from [Set], we get the inconsistency of + [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI. +*) + +(** * Weak classical axioms *) + +(** We show the following increasing in the strength of axioms: + - weak excluded-middle + - right distributivity of implication over disjunction and Gödel-Dummett axiom + - independence of general premises and drinker's paradox + - excluded-middle +*) + +(** ** Weak excluded-middle *) + +(** The weak classical logic based on [~~A \/ ~A] is referred to with + name KC in [[ChagrovZakharyaschev97]] + + [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael + Zakharyaschev, "Modal Logic", Clarendon Press, 1997. +*) + +Definition weak_excluded_middle := + forall A:Prop, ~~A \/ ~A. + +(** The interest in the equivalent variant + [weak_generalized_excluded_middle] is that it holds even in logic + without a primitive [False] connective (like Gödel-Dummett axiom) *) + +Definition weak_generalized_excluded_middle := + forall A B:Prop, ((A -> B) -> B) \/ (A -> B). + +(** ** Gödel-Dummett axiom *) + +(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. + + [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus + with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol + 24 No. 2(1959), pp 97-103. + + [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", + Ergeb. Math. Koll. 4 (1933), pp. 34-38. + *) + +Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A). + +Lemma excluded_middle_Godel_Dummett : excluded_middle -> GodelDummett. +Proof. + intros EM A B. destruct (EM B) as [HB|HnotB]. + left; intros _; exact HB. + right; intros HB; destruct (HnotB HB). +Qed. + +(** [(A->B) \/ (B->A)] is equivalent to [(C -> A\/B) -> (C->A) \/ (C->B)] + (proof from [[Dummett59]]) *) + +Definition RightDistributivityImplicationOverDisjunction := + forall A B C:Prop, (C -> A\/B) -> (C->A) \/ (C->B). + +Lemma Godel_Dummett_iff_right_distr_implication_over_disjunction : + GodelDummett <-> RightDistributivityImplicationOverDisjunction. +Proof. + split. + intros GD A B C HCAB. + destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC; + destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption. + intros Distr A B. + destruct (Distr A B (A\/B)) as [HABA|HABB]. + intro HAB; exact HAB. + right; intro HB; apply HABA; right; assumption. + left; intro HA; apply HABB; left; assumption. +Qed. + +(** [(A->B) \/ (B->A)] is stronger than the weak excluded middle *) + +Lemma Godel_Dummett_weak_excluded_middle : + GodelDummett -> weak_excluded_middle. +Proof. + intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA]. + left; intro HnotA; apply (HnotA (HnotAA HnotA)). + right; intro HA; apply (HAnotA HA HA). +Qed. + +(** ** Independence of general premises and drinker's paradox *) + +(** Independence of general premises is the unconstrained, non + constructive, version of the Independence of Premises as + considered in [[Troelstra73]]. + + It is a generalization to predicate logic of the right + distributivity of implication over disjunction (hence of + Gödel-Dummett axiom) whose own constructive form (obtained by a + restricting the third formula to be negative) is called + Kreisel-Putnam principle [[KreiselPutnam57]]. + + [[KreiselPutnam57]], Georg Kreisel and Hilary Putnam. "Eine + Unableitsbarkeitsbeweismethode für den intuitionistischen + Aussagenkalkül". Archiv für Mathematische Logik und + Graundlagenforschung, 3:74- 78, 1957. + + [[Troelstra73]], Anne Troelstra, editor. Metamathematical + Investigation of Intuitionistic Arithmetic and Analysis, volume + 344 of Lecture Notes in Mathematics, Springer-Verlag, 1973. +*) + +Definition IndependenceOfGeneralPremises := + forall (A:Type) (P:A -> Prop) (Q:Prop), + inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x. + +Lemma + independence_general_premises_right_distr_implication_over_disjunction : + IndependenceOfGeneralPremises -> RightDistributivityImplicationOverDisjunction. +Proof. + intros IP A B C HCAB. + destruct (IP bool (fun b => if b then A else B) C true) as ([|],H). + intro HC; destruct (HCAB HC); [exists true|exists false]; assumption. + left; assumption. + right; assumption. +Qed. + +Lemma independence_general_premises_Godel_Dummett : + IndependenceOfGeneralPremises -> GodelDummett. +Proof. + destruct Godel_Dummett_iff_right_distr_implication_over_disjunction. + auto using independence_general_premises_right_distr_implication_over_disjunction. +Qed. + +(** Independence of general premises is equivalent to the drinker's paradox *) + +Definition DrinkerParadox := + forall (A:Type) (P:A -> Prop), + inhabited A -> exists x, (exists x, P x) -> P x. + +Lemma independence_general_premises_drinker : + IndependenceOfGeneralPremises <-> DrinkerParadox. +Proof. + split. + intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx. + intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx). + exists x; intro HQ; apply (Hx (H HQ)). +Qed. + +(** Independence of general premises is weaker than (generalized) + 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). + +Lemma excluded_middle_independence_general_premises : + generalized_excluded_middle -> DrinkerParadox. +Proof. + intros GEM A P x0. + destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot]. + exists x; intro; exact Hx. + exists x0; exact Hnot. +Qed. + +(** * Axioms equivalent to classical logic *) + +(** ** Principle of unrestricted minimization *) + +Require Import Coq.Arith.PeanoNat. + +Definition Minimal (P:nat -> Prop) (n:nat) : Prop := + P n /\ forall k, P k -> n<=k. + +Definition Minimization_Property (P : nat -> Prop) : Prop := + forall n, P n -> exists m, Minimal P m. + +Section Unrestricted_minimization_entails_excluded_middle. + + Hypothesis unrestricted_minimization: forall P, Minimization_Property P. + + Theorem unrestricted_minimization_entails_excluded_middle : forall A, A\/~A. + Proof. + intros A. + pose (P := fun n:nat => n=0/\A \/ n=1). + assert (P 1) as h. + { unfold P. intuition. } + assert (P 0 <-> A) as p₀. + { split. + + intros [[_ h₀]|[=]]. assumption. + + unfold P. tauto. } + apply unrestricted_minimization in h as ([|[|m]] & hm & hmm). + + intuition. + + right. + intros HA. apply p₀, hmm, PeanoNat.Nat.nle_succ_0 in HA. assumption. + + destruct hm as [([=],_) | [=] ]. + Qed. + +End Unrestricted_minimization_entails_excluded_middle. + +Require Import Wf_nat. + +Section Excluded_middle_entails_unrestricted_minimization. + + Hypothesis em : forall A, A\/~A. + + Theorem excluded_middle_entails_unrestricted_minimization : + forall P, Minimization_Property P. + Proof. + intros P n HPn. + assert (dec : forall n, P n \/ ~ P n) by auto using em. + assert (ex : exists n, P n) by (exists n; assumption). + destruct (dec_inh_nat_subset_has_unique_least_element P dec ex) as (n' & HPn' & _). + exists n'. assumption. + Qed. + +End Excluded_middle_entails_unrestricted_minimization. + +(** However, minimization for a given predicate does not necessarily imply + decidability of this predicate *) + +Section Example_of_undecidable_predicate_with_the_minimization_property. + + Variable s : nat -> bool. + + Let P n := exists k, n<=k /\ s k = true. + + Example undecidable_predicate_with_the_minimization_property : + Minimization_Property P. + Proof. + unfold Minimization_Property. + intros h hn. + exists 0. split. + + unfold P in *. destruct hn as (k&hk₁&hk₂). + exists k. split. + * rewrite <- hk₁. + apply PeanoNat.Nat.le_0_l. + * assumption. + + intros **. apply PeanoNat.Nat.le_0_l. + Qed. + +End Example_of_undecidable_predicate_with_the_minimization_property. + +(** ** Choice of representatives in a partition of bool *) + +(** This is similar to Bell's "weak extensional selection principle" in [[Bell]] + + [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, unpublished. +*) + +Require Import RelationClasses. + +Local Notation representative_boolean_partition := + (forall R:bool->bool->Prop, + Equivalence R -> exists f, forall x, R x (f x) /\ forall y, R x y -> f x = f y). + +Theorem representative_boolean_partition_imp_excluded_middle : + representative_boolean_partition -> excluded_middle. +Proof. + intros ReprFunChoice P. + pose (R (b1 b2 : bool) := b1 = b2 \/ P). + assert (Equivalence R). + { split. + - now left. + - destruct 1. now left. now right. + - destruct 1, 1; try now right. left; now transitivity y. } + destruct (ReprFunChoice R H) as (f,Hf). clear H. + destruct (Bool.bool_dec (f true) (f false)) as [Heq|Hneq]. + + left. + destruct (Hf false) as ([Hfalse|HP],_); try easy. + destruct (Hf true) as ([Htrue|HP],_); try easy. + congruence. + + right. intro HP. + destruct (Hf true) as (_,H). apply Hneq, H. now right. +Qed. + +Theorem excluded_middle_imp_representative_boolean_partition : + excluded_middle -> representative_boolean_partition. +Proof. + intros EM R H. + destruct (EM (R true false)). + - exists (fun _ => true). + intros []; firstorder. + - exists (fun b => b). + intro b. split. + + reflexivity. + + destruct b, y; intros HR; easy || now symmetry in HR. +Qed. + +Theorem excluded_middle_iff_representative_boolean_partition : + excluded_middle <-> representative_boolean_partition. +Proof. + split; auto using excluded_middle_imp_representative_boolean_partition, + representative_boolean_partition_imp_excluded_middle. +Qed. diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v new file mode 100644 index 0000000000..841bd1bede --- /dev/null +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -0,0 +1,93 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** 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 + excluded-middle in [Set], hence it implies a strongly classical + world. Especially it conflicts with the impredicativity of [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 Export Classical. + +Axiom + dependent_unique_choice : + 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)). + +(** Unique choice reifies functional relations into functions *) + +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. +intros A B. +apply (dependent_unique_choice A (fun _ => B)). +Qed. + + +(** The following proof comes from [[ChicliPottierSimpson02]] *) +Require Import Setoid. + +Theorem classic_set_in_prop_context : + forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C. +Proof. +intros C 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 unique_choice. +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. +Qed. + +Corollary not_not_classic_set : + ((forall P:Prop, {P} + {~ P}) -> False) -> False. +Proof. +apply classic_set_in_prop_context. +Qed. + +(* Compatibility *) +Notation classic_set := not_not_classic_set (only parsing). diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v new file mode 100644 index 0000000000..18820d3ba3 --- /dev/null +++ b/theories/Logic/Classical_Pred_Type.v @@ -0,0 +1,74 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* This file is a renaming for V5.10.14b, Oct 1995, of file Classical.v + introduced in Coq V5.8.3, June 1993 *) + +(** Classical Predicate Logic on Type *) + +Require Import Classical_Prop. + +Section Generic. +Variable U : Type. + +(** de Morgan laws for quantifiers *) + +Lemma not_all_not_ex : + forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. +Proof. +intros P notall. +apply NNPP. +intro abs. +apply notall. +intros n H. +apply abs; exists n; exact H. +Qed. + +Lemma not_all_ex_not : + forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. +Proof. +intros P notall. +apply not_all_not_ex with (P:=fun x => ~ P x). +intro all; apply notall. +intro n; apply NNPP. +apply all. +Qed. + +Lemma not_ex_all_not : + forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. +Proof. (* Intuitionistic *) +unfold not; intros P notex n abs. +apply notex. +exists n; trivial. +Qed. + +Lemma not_ex_not_all : + forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n. +Proof. +intros P H n. +apply NNPP. +red; intro K; apply H; exists n; trivial. +Qed. + +Lemma ex_not_not_all : + forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). +Proof. (* Intuitionistic *) +unfold not; intros P exnot allP. +elim exnot; auto. +Qed. + +Lemma all_not_not_ex : + forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). +Proof. (* Intuitionistic *) +unfold not; intros P allnot exP; elim exP; intros n p. +apply allnot with n; auto. +Qed. + +End Generic. diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v new file mode 100644 index 0000000000..9f5a299371 --- /dev/null +++ b/theories/Logic/Classical_Prop.v @@ -0,0 +1,123 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* File created for Coq V5.10.14b, Oct 1995 *) +(* Classical tactics for proving disjunctions by Julien Narboux, Jul 2005 *) +(* Inferred proof-irrelevance and eq_rect_eq added by Hugo Herbelin, Mar 2006 *) + +(** Classical Propositional Logic *) + +Require Import ClassicalFacts. + +Hint Unfold not: core. + +Axiom classic : forall P:Prop, P \/ ~ P. + +Lemma NNPP : forall p:Prop, ~ ~ p -> p. +Proof. +unfold not; intros; elim (classic p); auto. +intro NP; elim (H NP). +Qed. + +(** Peirce's law states [forall P Q:Prop, ((P -> 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. +intro; apply H; intro; absurd P; trivial. +Qed. + +Lemma not_imply_elim2 : forall P Q:Prop, ~ (P -> Q) -> ~ Q. +Proof. (* Intuitionistic *) +tauto. +Qed. + +Lemma imply_to_or : forall P Q:Prop, (P -> Q) -> ~ P \/ Q. +Proof. +intros; elim (classic P); auto. +Qed. + +Lemma imply_to_and : forall P Q:Prop, ~ (P -> Q) -> P /\ ~ Q. +Proof. +intros; split. +apply not_imply_elim with Q; trivial. +apply not_imply_elim2 with P; trivial. +Qed. + +Lemma or_to_imply : forall P Q:Prop, ~ P \/ Q -> P -> Q. +Proof. (* Intuitionistic *) +tauto. +Qed. + +Lemma not_and_or : forall P Q:Prop, ~ (P /\ Q) -> ~ P \/ ~ Q. +Proof. +intros; elim (classic P); auto. +Qed. + +Lemma or_not_and : forall P Q:Prop, ~ P \/ ~ Q -> ~ (P /\ Q). +Proof. +simple induction 1; red; simple induction 2; auto. +Qed. + +Lemma not_or_and : forall P Q:Prop, ~ (P \/ Q) -> ~ P /\ ~ Q. +Proof. (* Intuitionistic *) +tauto. +Qed. + +Lemma and_not_or : forall P Q:Prop, ~ P /\ ~ Q -> ~ (P \/ Q). +Proof. (* Intuitionistic *) +tauto. +Qed. + +Lemma imply_and_or : forall P Q:Prop, (P -> Q) -> P \/ Q -> Q. +Proof. (* Intuitionistic *) +tauto. +Qed. + +Lemma imply_and_or2 : forall P Q R:Prop, (P -> Q) -> P \/ R -> Q \/ R. +Proof. (* Intuitionistic *) +tauto. +Qed. + +Lemma proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. +Proof proof_irrelevance_cci classic. + +(* classical_left transforms |- A \/ B into ~B |- A *) +(* classical_right transforms |- A \/ B into ~A |- B *) + +Ltac classical_right := match goal with +|- ?X \/ _ => (elim (classic X);intro;[left;trivial|right]) +end. + +Ltac classical_left := match goal with +|- _ \/ ?X => (elim (classic X);intro;[right;trivial|left]) +end. + +Require Export EqdepFacts. + +Module Eq_rect_eq. + +Lemma eq_rect_eq : + forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. +Proof. +intros; rewrite proof_irrelevance with (p1:=h) (p2:=eq_refl p); reflexivity. +Qed. + +End Eq_rect_eq. + +Module EqdepTheory := EqdepTheory(Eq_rect_eq). +Export EqdepTheory. diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v new file mode 100644 index 0000000000..04e3981001 --- /dev/null +++ b/theories/Logic/ConstructiveEpsilon.v @@ -0,0 +1,270 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*) + +(** This provides with a proof of the constructive form of definite +and indefinite descriptions for Sigma^0_1-formulas (hereafter called +"small" formulas), which infers the sigma-existence (i.e., +[Type]-existence) of a witness to a decidable predicate over a +countable domain from the regular existence (i.e., +[Prop]-existence). *) + +(** Coq does not allow case analysis on sort [Prop] when the goal is in +not in [Prop]. Therefore, one cannot eliminate [exists n, P n] in order to +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 [Type]. 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 +[Fix_F] in the module Coq.Init.Wf. There, recursion is done on an +inductive predicate [Acc] and the resulting type is in [Type]. + +To find a witness of [P] constructively, we program the well-known +linear search algorithm that tries P on all natural numbers starting +from 0 and going up. Such an algorithm needs a suitable termination +certificate. We offer two ways for providing this termination +certificate: a direct one, based on an ad-hoc predicate called +[before_witness], and another one based on the predicate [Acc]. +For the first one we provide explicit and short proof terms. *) + +(** Based on ideas from Benjamin Werner and Jean-François Monin *) + +(** Contributed by Yevgeniy Makarov and Jean-François Monin *) + +(* -------------------------------------------------------------------- *) + +(* Direct version *) + +Require Import Arith. + +Section ConstructiveIndefiniteGroundDescription_Direct. + +Variable P : nat -> Prop. + +Hypothesis P_dec : forall n, {P n}+{~(P n)}. + + +(** The termination argument is [before_witness n], which says that +any number before any witness (not necessarily the [x] of [exists x :A, P x]) +makes the search eventually stops. *) + +Inductive before_witness (n:nat) : Prop := + | stop : P n -> before_witness n + | next : before_witness (S n) -> before_witness n. + +(* Computation of the initial termination certificate *) +Fixpoint O_witness (n : nat) : before_witness n -> before_witness 0 := + match n return (before_witness n -> before_witness 0) with + | 0 => fun b => b + | S n => fun b => O_witness n (next n b) + end. + +(* Inversion of [inv_before_witness n] in a way such that the result +is structurally smaller even in the [stop] case. *) +Definition inv_before_witness : + forall n, before_witness n -> ~(P n) -> before_witness (S n) := + fun n b => + match b return ~ P n -> before_witness (S n) with + | stop _ p => fun not_p => match (not_p p) with end + | next _ b => fun _ => b + end. + +Fixpoint linear_search m (b : before_witness m) : {n : nat | P n} := + match P_dec m with + | left yes => exist (fun n => P n) m yes + | right no => linear_search (S m) (inv_before_witness m b no) + end. + +Definition constructive_indefinite_ground_description_nat : + (exists n, P n) -> {n:nat | P n} := + fun e => linear_search O (let (n, p) := e in O_witness n (stop n p)). + +Fixpoint linear_search_smallest (start : nat) (pr : before_witness start) : + forall k : nat, start <= k < proj1_sig (linear_search start pr) -> ~P k. +Proof. + (* Recursion on pr, which is the distance between start and linear_search *) + intros. destruct (P_dec start) eqn:Pstart. + - (* P start, k cannot exist *) + intros. assert (proj1_sig (linear_search start pr) = start). + { unfold linear_search. destruct pr; rewrite -> Pstart; reflexivity. } + rewrite -> H0 in H. destruct H. apply (le_lt_trans start k) in H1. + apply lt_irrefl in H1. contradiction. assumption. + - (* ~P start, step once in the search and use induction hypothesis *) + destruct pr. contradiction. destruct H. apply le_lt_or_eq in H. destruct H. + apply (linear_search_smallest (S start) pr). split. assumption. + simpl in H0. rewrite -> Pstart in H0. assumption. subst. assumption. +Defined. + +Definition epsilon_smallest : + (exists n : nat, P n) + -> { n : nat | P n /\ forall k : nat, k < n -> ~P k }. +Proof. + intros. pose (wit := (let (n, p) := H in O_witness n (stop n p))). + destruct (linear_search 0 wit) as [n pr] eqn:ls. exists n. split. assumption. intros. + apply (linear_search_smallest 0 wit). split. apply le_0_n. + rewrite -> ls. assumption. +Qed. + +End ConstructiveIndefiniteGroundDescription_Direct. + +(************************************************************************) + +(* Version using the predicate [Acc] *) + +Section ConstructiveIndefiniteGroundDescription_Acc. + +Variable P : nat -> Prop. + +Hypothesis P_decidable : forall n : nat, {P n} + {~ P n}. + +(** 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 [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}]. + +The relation [R] describes the connection between the two successive +numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after +[x], i.e., [y = S x] and [P x] is false. Then the absence of an +infinite [R]-descending chain from 0 is equivalent to the termination +of our searching algorithm. *) + +Let R (x y : nat) : Prop := x = S y /\ ~ P y. + +Local Notation acc x := (Acc R x). + +Lemma P_implies_acc : forall x : nat, P x -> acc x. +Proof. +intros x H. constructor. +intros y [_ not_Px]. absurd (P x); assumption. +Qed. + +Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x. +Proof. +intros x n; generalize x; clear x; induction n as [|n IH]; simpl. +apply P_implies_acc. +intros x H. constructor. intros y [fxy _]. +apply IH. rewrite fxy. +replace (n + S x) with (S (n + x)); auto with arith. +Defined. + +Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0. +Proof. +intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x). +replace (x + 0) with x; auto with arith. +Defined. + +(** In the following statement, we use the trick with recursion on +[Acc]. This is also where decidability of [P] is used. *) + +Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}. +Proof. +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. +set (y := S x). +assert (Ryx : R y x). unfold R; split; auto. +destruct (IH y Ryx) as [n Hn]. +exists n; assumption. +Defined. + +Theorem constructive_indefinite_ground_description_nat_Acc : + (exists n : nat, P n) -> {n : nat | P n}. +Proof. +intros H; apply acc_implies_P_eventually. +apply P_eventually_implies_acc_ex; assumption. +Defined. + +End ConstructiveIndefiniteGroundDescription_Acc. + +(************************************************************************) + +Section ConstructiveGroundEpsilon_nat. + +Variable P : nat -> Prop. + +Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}. + +Definition constructive_ground_epsilon_nat (E : exists n : nat, P n) : nat + := proj1_sig (constructive_indefinite_ground_description_nat P P_decidable E). + +Definition constructive_ground_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_ground_epsilon_nat E) + := proj2_sig (constructive_indefinite_ground_description_nat P P_decidable E). + +End ConstructiveGroundEpsilon_nat. + +(************************************************************************) + +Section ConstructiveGroundEpsilon. + +(** For the current purpose, we say that a set [A] is countable if +there are functions [f : A -> nat] and [g : nat -> A] such that [g] is +a left inverse of [f]. *) + +Variable A : Type. +Variable f : A -> nat. +Variable g : nat -> A. + +Hypothesis gof_eq_id : forall x : A, g (f x) = x. + +Variable P : A -> Prop. + +Hypothesis P_decidable : forall x : A, {P x} + {~ P x}. + +Definition P' (x : nat) : Prop := P (g x). + +Lemma P'_decidable : forall n : nat, {P' n} + {~ P' n}. +Proof. +intro n; unfold P'; destruct (P_decidable (g n)); auto. +Defined. + +Lemma constructive_indefinite_ground_description : (exists x : A, P x) -> {x : A | P x}. +Proof. +intro H. assert (H1 : exists n : nat, P' n). +destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption. +apply (constructive_indefinite_ground_description_nat P' P'_decidable) in H1. +destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption. +Defined. + +Lemma constructive_definite_ground_description : (exists! x : A, P x) -> {x : A | P x}. +Proof. + intros; apply constructive_indefinite_ground_description; firstorder. +Defined. + +Definition constructive_ground_epsilon (E : exists x : A, P x) : A + := proj1_sig (constructive_indefinite_ground_description E). + +Definition constructive_ground_epsilon_spec (E : (exists x, P x)) : P (constructive_ground_epsilon E) + := proj2_sig (constructive_indefinite_ground_description E). + +End ConstructiveGroundEpsilon. + +(* begin hide *) +(* Compatibility: the qualificative "ground" was absent from the initial +names of the results in this file but this had introduced confusion +with the similarly named statement in Description.v *) +Notation constructive_indefinite_description_nat := + constructive_indefinite_ground_description_nat (only parsing). +Notation constructive_epsilon_spec_nat := + constructive_ground_epsilon_spec_nat (only parsing). +Notation constructive_epsilon_nat := + constructive_ground_epsilon_nat (only parsing). +Notation constructive_indefinite_description := + constructive_indefinite_ground_description (only parsing). +Notation constructive_definite_description := + constructive_definite_ground_description (only parsing). +Notation constructive_epsilon_spec := + constructive_ground_epsilon_spec (only parsing). +Notation constructive_epsilon := + constructive_ground_epsilon (only parsing). +(* end hide *) diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v new file mode 100644 index 0000000000..49276f904f --- /dev/null +++ b/theories/Logic/Decidable.v @@ -0,0 +1,226 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(** Properties of decidable propositions *) + +Definition decidable (P:Prop) := P \/ ~ P. + +Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P. +Proof. +unfold decidable; tauto. +Qed. + +Theorem dec_True : decidable True. +Proof. +unfold decidable; auto. +Qed. + +Theorem dec_False : decidable False. +Proof. +unfold decidable, not; auto. +Qed. + +Theorem dec_or : + forall A B:Prop, decidable A -> decidable B -> decidable (A \/ B). +Proof. +unfold decidable; tauto. +Qed. + +Theorem dec_and : + forall A B:Prop, decidable A -> decidable B -> decidable (A /\ B). +Proof. +unfold decidable; tauto. +Qed. + +Theorem dec_not : forall A:Prop, decidable A -> decidable (~ A). +Proof. +unfold decidable; tauto. +Qed. + +Theorem dec_imp : + forall A B:Prop, decidable A -> decidable B -> decidable (A -> B). +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. +Proof. +unfold decidable; tauto. +Qed. + +Theorem not_or : forall A B:Prop, ~ (A \/ B) -> ~ A /\ ~ B. +Proof. +tauto. +Qed. + +Theorem not_and : forall A B:Prop, decidable A -> ~ (A /\ B) -> ~ A \/ ~ B. +Proof. +unfold decidable; tauto. +Qed. + +Theorem not_imp : forall A B:Prop, decidable A -> ~ (A -> B) -> A /\ ~ B. +Proof. +unfold decidable; tauto. +Qed. + +Theorem imp_simp : forall A B:Prop, decidable A -> (A -> B) -> ~ A \/ B. +Proof. +unfold decidable; tauto. +Qed. + +Theorem not_iff : + forall A B:Prop, decidable A -> decidable B -> + ~ (A <-> B) -> (A /\ ~ B) \/ (~ A /\ B). +Proof. +unfold decidable; tauto. +Qed. + +Register dec_True as core.dec.True. +Register dec_False as core.dec.False. +Register dec_or as core.dec.or. +Register dec_and as core.dec.and. +Register dec_not as core.dec.not. +Register dec_imp as core.dec.imp. +Register dec_iff as core.dec.iff. +Register dec_not_not as core.dec.not_not. +Register not_not as core.dec.dec_not_not. +Register not_or as core.dec.not_or. +Register not_and as core.dec.not_and. +Register not_imp as core.dec.not_imp. +Register imp_simp as core.dec.imp_simp. +Register not_iff as core.dec.not_iff. + +(** 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. + +(* Functional relations on decidable co-domains are decidable *) + +Theorem dec_functional_relation : + forall (X Y : Type) (A:X->Y->Prop), (forall y y' : Y, decidable (y=y')) -> + (forall x, exists! y, A x y) -> forall x y, decidable (A x y). +Proof. +intros X Y A Hdec H x y. +destruct (H x) as (y',(Hex,Huniq)). +destruct (Hdec y y') as [->|Hnot]; firstorder. +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/Description.v b/theories/Logic/Description.v new file mode 100644 index 0000000000..5c4f1960fb --- /dev/null +++ b/theories/Logic/Description.v @@ -0,0 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This file provides a constructive form of definite description; it + allows building 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/Diaconescu.v b/theories/Logic/Diaconescu.v new file mode 100644 index 0000000000..66e82ddbf4 --- /dev/null +++ b/theories/Logic/Diaconescu.v @@ -0,0 +1,305 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Diaconescu showed that the Axiom of Choice entails Excluded-Middle + in topoi [[Diaconescu75]]. Lacas and Werner adapted the proof to show + that the axiom of choice in equivalence classes entails + Excluded-Middle in Type Theory [[LacasWerner99]]. + + Three variants of Diaconescu's result in type theory are shown below. + + A. A proof that the relational form of the Axiom of Choice + + Extensionality for Predicates entails Excluded-Middle (by Hugo + Herbelin) + + B. A proof that the relational form of the Axiom of Choice + Proof + Irrelevance entails Excluded-Middle for Equality Statements (by + Benjamin Werner) + + C. A proof that extensional Hilbert epsilon's description operator + entails excluded-middle (taken from Bell [[Bell93]]) + + See also [[Carlström04]] for a discussion of the connection between the + Extensional Axiom of Choice and Excluded-Middle + + [[Diaconescu75]] Radu Diaconescu, Axiom of Choice and Complementation, + in Proceedings of AMS, vol 51, pp 176-178, 1975. + + [[LacasWerner99]] Samuel Lacas, Benjamin Werner, Which Choices imply + the excluded middle?, preprint, 1999. + + [[Bell93]] John L. Bell, Hilbert's epsilon operator and classical + logic, Journal of Philosophical Logic, 22: 1-18, 1993 + + [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent + to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. +*) +Require ClassicalFacts ChoiceFacts. + +(**********************************************************************) +(** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) + +Section PredExt_RelChoice_imp_EM. + +(** The axiom of extensionality for predicates *) + +Definition PredicateExtensionality := + forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q. + +(** From predicate extensionality we get propositional extensionality + hence proof-irrelevance *) + +Import ClassicalFacts. + +Variable pred_extensionality : PredicateExtensionality. + +Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B. +Proof. + intros A B H. + change ((fun _ => A) true = (fun _ => B) true). + rewrite + pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B). + reflexivity. + intros _; exact H. +Qed. + +Lemma proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2. +Proof. + apply (ext_prop_dep_proof_irrel_cic prop_ext). +Qed. + +(** From proof-irrelevance and relational choice, we get guarded + relational choice *) + +Import ChoiceFacts. + +Variable rel_choice : RelationalChoice. + +Lemma guarded_rel_choice : GuardedRelationalChoice. +Proof. + apply + (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel). +Qed. + +(** The form of choice we need: there is a functional relation which chooses + an element in any non empty subset of bool *) + +Import Bool. + +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. + 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 *) +(** Remark: P could have been in Set or Type *) + +Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P. +Proof. +intro P. + +(* first we exhibit the choice functional relation R *) +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). + +(* the actual "decision": is (R class_of_true) = true or false? *) +destruct (H class_of_true) as [b0 [H0 [H0' H0'']]]. +exists true; left; reflexivity. +destruct H0. + +(* the actual "decision": is (R class_of_false) = true or false? *) +destruct (H class_of_false) as [b1 [H1 [H1' H1'']]]. +exists false; left; reflexivity. +destruct H1. + +(* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *) +right. +intro HP. +assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b). +intro b; split. +unfold class_of_false; right; assumption. +unfold class_of_true; right; assumption. +assert (Heq : class_of_true = class_of_false). +apply pred_extensionality with (1 := Hequiv). +apply diff_true_false. +rewrite <- H0. +rewrite <- H1. +rewrite <- H0''. reflexivity. +rewrite Heq. +assumption. + +(* cases where P is true *) +left; assumption. +left; assumption. + +Qed. + +End PredExt_RelChoice_imp_EM. + +(**********************************************************************) +(** * Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *) + +(** This is an adaptation of Diaconescu's theorem, exploiting the + form of extensionality provided by proof-irrelevance *) + +Section ProofIrrel_RelChoice_imp_EqEM. + +Import ChoiceFacts. + +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 A (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) (eq_refl a2)) + with (or_intror (a2=a2) (eq_refl 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 *) + +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. + +(**********************************************************************) +(** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *) + +(** Proof sketch from Bell [[Bell93]] (with thanks to P. Castéran) *) + +Local Notation inhabited A := A (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. + +Local Notation 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/Epsilon.v b/theories/Logic/Epsilon.v new file mode 100644 index 0000000000..d8c527c612 --- /dev/null +++ b/theories/Logic/Epsilon.v @@ -0,0 +1,72 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** 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/Eqdep.v b/theories/Logic/Eqdep.v new file mode 100644 index 0000000000..35bc422597 --- /dev/null +++ b/theories/Logic/Eqdep.v @@ -0,0 +1,39 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *) +(* Abstraction with respect to the eq_rect_eq axiom and creation of + EqdepFacts.v by Hugo Herbelin, Mar 2006 *) + +(** This file axiomatizes the invariance by substitution of reflexive + equality proofs [[Streicher93]] and exports its consequences, such + as the injectivity of the projection of the dependent pair. + + [[Streicher93]] T. Streicher, Semantical Investigations into + Intensional Type Theory, Habilitationsschrift, LMU München, 1993. +*) + +Require Export EqdepFacts. + +Module Eq_rect_eq. + +Axiom eq_rect_eq : + forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + +End Eq_rect_eq. + +Module EqdepTheory := EqdepTheory(Eq_rect_eq). +Export EqdepTheory. + +(** Exported hints *) + +Hint Resolve eq_dep_eq: eqdep. +Hint Resolve inj_pair2 inj_pairT2: eqdep. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v new file mode 100644 index 0000000000..8e59941f37 --- /dev/null +++ b/theories/Logic/EqdepFacts.v @@ -0,0 +1,507 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *) +(* Further documentation and variants of eq_rect_eq by Hugo Herbelin, + Apr 2003 *) +(* Abstraction with respect to the eq_rect_eq axiom and renaming to + EqdepFacts.v by Hugo Herbelin, Mar 2006 *) + +(** This file defines dependent equality and shows its equivalence with + equality on dependent pairs (inhabiting sigma-types). It derives + the consequence of axiomatizing the invariance by substitution of + reflexive equality proofs and shows the equivalence between the 4 + following statements + + - Invariance by Substitution of Reflexive Equality Proofs. + - Injectivity of Dependent Equality + - Uniqueness of Identity Proofs + - Uniqueness of Reflexive Identity Proofs + - Streicher's Axiom K + + These statements are independent of the calculus of constructions [2]. + + References: + + [1] T. Streicher, Semantical Investigations into Intensional Type Theory, + Habilitationsschrift, LMU München, 1993. + [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory, + Proceedings of the meeting Twenty-five years of constructive + type theory, Venice, Oxford University Press, 1998 + +Table of contents: + +1. Definition of dependent equality and equivalence with equality of + dependent pairs and with dependent pair of equalities + +2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K + +3. Definition of the functor that builds properties of dependent + equalities assuming axiom eq_rect_eq + +*) + +(************************************************************************) +(** * Definition of dependent equality and equivalence with equality of dependent pairs *) + +Import EqNotations. + +(* Set Universe Polymorphism. *) + +Section Dependent_Equality. + + Variable U : Type. + Variable P : U -> Type. + + (** Dependent equality *) + + Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop := + eq_dep_intro : eq_dep p x p x. + Hint Constructors eq_dep: core. + + Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x. + Proof eq_dep_intro. + + Lemma eq_dep_sym : + forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x. + Proof. + destruct 1; auto. + Qed. + Hint Immediate eq_dep_sym: core. + + Lemma eq_dep_trans : + forall (p q r:U) (x:P p) (y:P q) (z:P r), + eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z. + Proof. + destruct 1; auto. + Qed. + + Scheme eq_indd := Induction for eq Sort Prop. + + (** Equivalent definition of dependent equality as a dependent pair of + equalities *) + + Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop := + eq_dep1_intro : forall h:q = p, x = rew h in y -> eq_dep1 p x q y. + + Lemma eq_dep1_dep : + forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y. + Proof. + destruct 1 as (eq_qp, H). + destruct eq_qp using eq_indd. + rewrite H. + apply eq_dep_intro. + Qed. + + Lemma eq_dep_dep1 : + forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y. + Proof. + destruct 1. + apply eq_dep1_intro with (eq_refl p). + simpl; trivial. + Qed. + +End Dependent_Equality. + +Arguments eq_dep [U P] p x q _. +Arguments eq_dep1 [U P] p x q y. + +(** Dependent equality is equivalent to equality on dependent pairs *) + +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. + +Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.7"). (* Compatibility *) + +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. +Proof. + destruct 1; reflexivity. +Qed. + +Lemma eq_sigT_iff_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. + split; auto using eq_sigT_eq_dep, eq_dep_eq_sigT. +Qed. + +Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing). (* Compat *) + +Lemma eq_sig_eq_dep : + forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + exist P p x = exist P q y -> eq_dep p x q y. +Proof. + intros. + dependent rewrite H. + apply eq_dep_intro. +Qed. + +Lemma eq_dep_eq_sig : + forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + eq_dep p x q y -> exist P p x = exist P q y. +Proof. + destruct 1; reflexivity. +Qed. + +Lemma eq_sig_iff_eq_dep : + forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + exist P p x = exist P q y <-> eq_dep p x q y. +Proof. + split; auto using eq_sig_eq_dep, eq_dep_eq_sig. +Qed. + +(** Dependent equality is equivalent to a dependent pair of equalities *) + +Set Implicit Arguments. + +Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> + {H:x1=x2 | rew H in H1 = H2}. +Proof. + intros; split; intro H. + - change x2 with (projT1 (existT P x2 H2)). + change H2 with (projT2 (existT P x2 H2)) at 5. + destruct H. simpl. + exists eq_refl. + reflexivity. + - destruct H as (->,<-). + reflexivity. +Defined. + +Lemma eq_sigT_fst : + forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), x1 = x2. +Proof. + intros. + change x2 with (projT1 (existT P x2 H2)). + destruct H. + reflexivity. +Defined. + +Lemma eq_sigT_snd : + forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2. +Proof. + intros. + unfold eq_sigT_fst. + change x2 with (projT1 (existT P x2 H2)). + change H2 with (projT2 (existT P x2 H2)) at 3. + destruct H. + reflexivity. +Defined. + +Lemma eq_sig_fst : + forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), x1 = x2. +Proof. + intros. + change x2 with (proj1_sig (exist P x2 H2)). + destruct H. + reflexivity. +Defined. + +Lemma eq_sig_snd : + forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), rew (eq_sig_fst H) in H1 = H2. +Proof. + intros. + unfold eq_sig_fst, eq_ind. + change x2 with (proj1_sig (exist P x2 H2)). + change H2 with (proj2_sig (exist P x2 H2)) at 3. + destruct H. + reflexivity. +Defined. + +Unset Implicit Arguments. + +(** Exported hints *) + +Hint Resolve eq_dep_intro: core. +Hint Immediate eq_dep_sym: core. + +(************************************************************************) +(** * Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K *) + +Section Equivalences. + + Variable U:Type. + + (** Invariance by Substitution of Reflexive Equality Proofs *) + + Definition Eq_rect_eq_on (p : U) (Q : U -> Type) (x : Q p) := + forall (h : p = p), x = eq_rect p Q x p h. + Definition Eq_rect_eq := forall p Q x, Eq_rect_eq_on p Q x. + + (** Injectivity of Dependent Equality *) + + Definition Eq_dep_eq_on (P : U -> Type) (p : U) (x : P p) := + forall (y : P p), eq_dep p x p y -> x = y. + Definition Eq_dep_eq := forall P p x, Eq_dep_eq_on P p x. + + (** Uniqueness of Identity Proofs (UIP) *) + + Definition UIP_on_ (x y : U) (p1 : x = y) := + forall (p2 : x = y), p1 = p2. + Definition UIP_ := forall x y p1, UIP_on_ x y p1. + + (** Uniqueness of Reflexive Identity Proofs *) + + Definition UIP_refl_on_ (x : U) := + forall (p : x = x), p = eq_refl x. + Definition UIP_refl_ := forall x, UIP_refl_on_ x. + + (** Streicher's axiom K *) + + Definition Streicher_K_on_ (x : U) (P : x = x -> Prop) := + P (eq_refl x) -> forall p : x = x, P p. + Definition Streicher_K_ := forall x P, Streicher_K_on_ x P. + + (** Injectivity of Dependent Equality is a consequence of *) + (** Invariance by Substitution of Reflexive Equality Proof *) + + Lemma eq_rect_eq_on__eq_dep1_eq_on (p : U) (P : U -> Type) (y : P p) : + Eq_rect_eq_on p P y -> forall (x : P p), eq_dep1 p x p y -> x = y. + Proof. + intro eq_rect_eq. + simple destruct 1; intro. + rewrite <- eq_rect_eq; auto. + Qed. + Lemma eq_rect_eq__eq_dep1_eq : + Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y. + Proof (fun eq_rect_eq P p y x => + @eq_rect_eq_on__eq_dep1_eq_on p P x (eq_rect_eq p P x) y). + + Lemma eq_rect_eq_on__eq_dep_eq_on (p : U) (P : U -> Type) (x : P p) : + Eq_rect_eq_on p P x -> Eq_dep_eq_on P p x. + Proof. + intros eq_rect_eq; red; intros. + symmetry; apply (eq_rect_eq_on__eq_dep1_eq_on _ _ _ eq_rect_eq). + apply eq_dep_sym in H; apply eq_dep_dep1; trivial. + Qed. + Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq. + Proof (fun eq_rect_eq P p x y => + @eq_rect_eq_on__eq_dep_eq_on p P x (eq_rect_eq p P x) y). + + (** Uniqueness of Identity Proofs (UIP) is a consequence of *) + (** Injectivity of Dependent Equality *) + + Lemma eq_dep_eq_on__UIP_on (x y : U) (p1 : x = y) : + Eq_dep_eq_on (fun y => x = y) x eq_refl -> UIP_on_ x y p1. + Proof. + intro eq_dep_eq; red. + elim p1 using eq_indd. + intros; apply eq_dep_eq. + elim p2 using eq_indd. + apply eq_dep_intro. + Qed. + Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_. + Proof (fun eq_dep_eq x y p1 => + @eq_dep_eq_on__UIP_on x y p1 (eq_dep_eq _ _ _)). + + (** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *) + + Lemma UIP_on__UIP_refl_on (x : U) : + UIP_on_ x x eq_refl -> UIP_refl_on_ x. + Proof. + intro UIP; red; intros; symmetry; apply UIP. + Qed. + Lemma UIP__UIP_refl : UIP_ -> UIP_refl_. + Proof (fun UIP x p => + @UIP_on__UIP_refl_on x (UIP x x eq_refl) p). + + (** Streicher's axiom K is a direct consequence of Uniqueness of + Reflexive Identity Proofs *) + + Lemma UIP_refl_on__Streicher_K_on (x : U) (P : x = x -> Prop) : + UIP_refl_on_ x -> Streicher_K_on_ x P. + Proof. + intro UIP_refl; red; intros; rewrite UIP_refl; assumption. + Qed. + Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_. + Proof (fun UIP_refl x P => + @UIP_refl_on__Streicher_K_on x P (UIP_refl x)). + + (** We finally recover from K the Invariance by Substitution of + Reflexive Equality Proofs *) + + Lemma Streicher_K_on__eq_rect_eq_on (p : U) (P : U -> Type) (x : P p) : + Streicher_K_on_ p (fun h => x = rew -> [P] h in x) + -> Eq_rect_eq_on p P x. + Proof. + intro Streicher_K; red; intros. + apply Streicher_K. + reflexivity. + Qed. + Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq. + Proof (fun Streicher_K p P x => + @Streicher_K_on__eq_rect_eq_on p P x (Streicher_K p _)). + +(** Remark: It is reasonable to think that [eq_rect_eq] is strictly + stronger than [eq_rec_eq] (which is [eq_rect_eq] restricted on [Set]): + + [Definition Eq_rec_eq := + forall (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.] + + Typically, [eq_rect_eq] allows proving UIP and Streicher's K what + does not seem possible with [eq_rec_eq]. In particular, the proof of [UIP] + requires to use [eq_rect_eq] on [fun y -> x=y] which is in [Type] but not + in [Set]. +*) + +End Equivalences. + +(** UIP_refl is downward closed (a short proof of the key lemma of Voevodsky's + proof of inclusion of h-level n into h-level n+1; see hlevelntosn + in https://github.com/vladimirias/Foundations.git). *) + +Theorem UIP_shift_on (X : Type) (x : X) : + UIP_refl_on_ X x -> forall y : x = x, UIP_refl_on_ (x = x) y. +Proof. + intros UIP_refl y. + rewrite (UIP_refl y). + intros z. + assert (UIP:forall y' y'' : x = x, y' = y''). + { intros. apply eq_trans with (eq_refl x). apply UIP_refl. + symmetry. apply UIP_refl. } + transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) + (eq_sym (UIP (eq_refl x) (eq_refl x)))). + - destruct z. destruct (UIP _ _). reflexivity. + - change + (match eq_refl x as y' in _ = x' return y' = y' -> Prop with + | eq_refl => fun z => z = (eq_refl (eq_refl x)) + end (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) + (eq_sym (UIP (eq_refl x) (eq_refl x))))). + destruct z. destruct (UIP _ _). reflexivity. +Qed. +Theorem UIP_shift : forall U, UIP_refl_ U -> forall x:U, UIP_refl_ (x = x). +Proof (fun U UIP_refl x => + @UIP_shift_on U x (UIP_refl x)). + +Section Corollaries. + + Variable U:Type. + + (** UIP implies the injectivity of equality on dependent pairs in Type *) + + + Definition Inj_dep_pair_on (P : U -> Type) (p : U) (x : P p) := + forall (y : P p), existT P p x = existT P p y -> x = y. + Definition Inj_dep_pair := forall P p x, Inj_dep_pair_on P p x. + + Lemma eq_dep_eq_on__inj_pair2_on (P : U -> Type) (p : U) (x : P p) : + Eq_dep_eq_on U P p x -> Inj_dep_pair_on P p x. + Proof. + intro eq_dep_eq; red; intros. + apply eq_dep_eq. + apply eq_sigT_eq_dep. + assumption. + Qed. + Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair. + Proof (fun eq_dep_eq P p x => + @eq_dep_eq_on__inj_pair2_on P p x (eq_dep_eq P p x)). + +End Corollaries. + +Notation Inj_dep_pairS := Inj_dep_pair. +Notation Inj_dep_pairT := Inj_dep_pair. +Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2. + + +(************************************************************************) +(** * Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *) + +Module Type EqdepElimination. + + Axiom eq_rect_eq : + forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), + x = eq_rect p Q x p h. + +End EqdepElimination. + +Module EqdepTheory (M:EqdepElimination). + + Section Axioms. + + Variable U:Type. + +(** Invariance by Substitution of Reflexive Equality Proofs *) + +Lemma eq_rect_eq : + forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. +Proof M.eq_rect_eq U. + +Lemma eq_rec_eq : + forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h. +Proof (fun p Q => M.eq_rect_eq U p Q). + +(** Injectivity of Dependent Equality *) + +Lemma eq_dep_eq : forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y. +Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq). + +(** Uniqueness of Identity Proofs (UIP) is a consequence of *) +(** Injectivity of Dependent Equality *) + +Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2. +Proof (eq_dep_eq__UIP U eq_dep_eq). + +(** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *) + +Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x. +Proof (UIP__UIP_refl U UIP). + +(** Streicher's axiom K is a direct consequence of Uniqueness of + Reflexive Identity Proofs *) + +Lemma Streicher_K : + forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. +Proof (UIP_refl__Streicher_K U UIP_refl). + +End Axioms. + +(** UIP implies the injectivity of equality on dependent pairs in Type *) + +Lemma inj_pair2 : + forall (U:Type) (P:U -> Type) (p:U) (x y:P p), + existT P p x = existT P p y -> x = y. +Proof (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)). + +Notation inj_pairT2 := inj_pair2. + +End EqdepTheory. + +(** Basic facts about eq_dep *) + +Lemma f_eq_dep : + forall U (P:U->Type) R p q x y (f:forall p, P p -> R p), + eq_dep p x q y -> eq_dep p (f p x) q (f q y). +Proof. +intros * []. reflexivity. +Qed. + +Lemma eq_dep_non_dep : + forall U P p q x y, @eq_dep U (fun _ => P) p x q y -> x = y. +Proof. +intros * []. reflexivity. +Qed. + +Lemma f_eq_dep_non_dep : + forall U (P:U->Type) R p q x y (f:forall p, P p -> R), + eq_dep p x q y -> f p x = f q y. +Proof. +intros * []. reflexivity. +Qed. + +Arguments eq_dep U P p x q _ : clear implicits. +Arguments eq_dep1 U P p x q y : clear implicits. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v new file mode 100644 index 0000000000..4e8b48af9f --- /dev/null +++ b/theories/Logic/Eqdep_dec.v @@ -0,0 +1,396 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Created by Bruno Barras, Jan 1998 *) +(* Made a module instance for EqdepFacts by Hugo Herbelin, Mar 2006 *) + +(** We prove that there is only one proof of [x=x], i.e [eq_refl x]. + This holds if the equality upon the set of [x] is decidable. + A corollary of this theorem is the equality of the right projections + of two equal dependent pairs. + + Author: Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego + adapted to Coq by B. Barras + + Credit: Proofs up to [K_dec] follow an outline by Michael Hedberg + +Table of contents: + +1. Streicher's K and injectivity of dependent pair hold on decidable types + +1.1. Definition of the functor that builds properties of dependent equalities + from a proof of decidability of equality for a set in Type + +1.2. Definition of the functor that builds properties of dependent equalities + from a proof of decidability of equality for a set in Set + +*) + +(************************************************************************) +(** * Streicher's K and injectivity of dependent pair hold on decidable types *) + +Set Implicit Arguments. +(* Set Universe Polymorphism. *) + +Section EqdepDec. + + Variable A : Type. + + Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' := + eq_ind _ (fun a => a = y') eq2 _ eq1. + + Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = eq_refl y. + Proof. + intros. + case u; trivial. + Qed. + + Variable x : A. + + Variable eq_dec : forall y:A, x = y \/ x <> y. + + Let nu (y:A) (u:x = y) : x = y := + match eq_dec y with + | or_introl eqxy => eqxy + | or_intror neqxy => False_ind _ (neqxy u) + end. + + Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v. + intros. + unfold nu. + destruct (eq_dec y) as [Heq|Hneq]. + reflexivity. + + case Hneq; trivial. + Qed. + + + Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (eq_refl x)) v. + + + Remark nu_left_inv_on : forall (y:A) (u:x = y), nu_inv (nu u) = u. + Proof. + intros. + case u; unfold nu_inv. + apply trans_sym_eq. + Qed. + + + Theorem eq_proofs_unicity_on : forall (y:A) (p1 p2:x = y), p1 = p2. + Proof. + intros. + elim nu_left_inv_on with (u := p1). + elim nu_left_inv_on with (u := p2). + elim nu_constant with y p1 p2. + reflexivity. + Qed. + + Theorem K_dec_on : + forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p. + Proof. + intros. + elim eq_proofs_unicity_on with x (eq_refl x) p. + trivial. + Qed. + + (** The corollary *) + + Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x := + match exP with + | ex_intro _ x' prf => + match eq_dec x' with + | or_introl eqprf => eq_ind x' P prf x (eq_sym eqprf) + | _ => def + end + end. + + + Theorem inj_right_pair_on : + forall (P:A -> Prop) (y y':P x), + ex_intro P x y = ex_intro P x y' -> y = y'. + Proof. + intros. + cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y). + simpl. + destruct (eq_dec x) as [Heq|Hneq]. + elim Heq using K_dec_on; trivial. + + intros. + case Hneq; trivial. + + case H. + reflexivity. + Qed. + +End EqdepDec. + +(** Now we prove the versions that require decidable equality for the entire type + rather than just on the given element. The rest of the file uses this total + decidable equality. We could do everything using decidable equality at a point + (because the induction rule for [eq] is really an induction rule for + [{ y : A | x = y }]), but we don't currently, because changing everything + would break backward compatibility and no-one has yet taken the time to define + the pointed versions, and then re-define the non-pointed versions in terms of + those. *) + +Theorem eq_proofs_unicity A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) +: forall (y:A) (p1 p2:x = y), p1 = p2. +Proof (@eq_proofs_unicity_on A x (eq_dec x)). + +Theorem K_dec A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) +: forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p. +Proof (@K_dec_on A x (eq_dec x)). + +Theorem inj_right_pair A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) +: forall (P:A -> Prop) (y y':P x), + ex_intro P x y = ex_intro P x y' -> y = y'. +Proof (@inj_right_pair_on A x (eq_dec x)). + +Require Import EqdepFacts. + +(** We deduce axiom [K] for (decidable) types *) +Theorem K_dec_type : + forall A:Type, + (forall x y:A, {x = y} + {x <> y}) -> + forall (x:A) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. +Proof. + intros A eq_dec x P H p. + elim p using K_dec; intros. + case (eq_dec x0 y); [left|right]; assumption. + trivial. +Qed. + +Theorem K_dec_set : + forall A:Set, + (forall x y:A, {x = y} + {x <> y}) -> + forall (x:A) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. +Proof fun A => K_dec_type (A:=A). + +(** We deduce the [eq_rect_eq] axiom for (decidable) types *) +Theorem eq_rect_eq_dec : + forall A:Type, + (forall x y:A, {x = y} + {x <> y}) -> + forall (p:A) (Q:A -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. +Proof. + intros A eq_dec. + 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)). + +Theorem UIP_dec : + forall (A:Type), + (forall x y:A, {x = y} + {x <> y}) -> + forall (x y:A) (p1 p2:x = y), p1 = p2. +Proof (fun A eq_dec => eq_dep_eq__UIP A (eq_dep_eq_dec eq_dec)). + +Unset Implicit Arguments. + +(************************************************************************) +(** ** Definition of the functor that builds properties of dependent equalities on decidable sets in Type *) + +(** The signature of decidable sets in [Type] *) + +Module Type DecidableType. + + Monomorphic Parameter U:Type. + Axiom eq_dec : forall x y:U, {x = y} + {x <> y}. + +End DecidableType. + +(** The module [DecidableEqDep] collects equality properties for decidable + set in [Type] *) + +Module DecidableEqDep (M:DecidableType). + + Import M. + + (** Invariance by Substitution of Reflexive Equality Proofs *) + + Lemma eq_rect_eq : + forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + Proof eq_rect_eq_dec eq_dec. + + (** Injectivity of Dependent Equality *) + + Theorem eq_dep_eq : + forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y. + Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq). + + (** Uniqueness of Identity Proofs (UIP) *) + + Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2. + Proof (eq_dep_eq__UIP U eq_dep_eq). + + (** Uniqueness of Reflexive Identity Proofs *) + + Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x. + Proof (UIP__UIP_refl U UIP). + + (** Streicher's axiom K *) + + Lemma Streicher_K : + forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. + Proof (K_dec_type eq_dec). + + (** Injectivity of equality on dependent pairs in [Type] *) + + Lemma inj_pairT2 : + forall (P:U -> Type) (p:U) (x y:P p), + existT P p x = existT P p y -> x = y. + Proof eq_dep_eq__inj_pairT2 U eq_dep_eq. + + (** Proof-irrelevance on subsets of decidable sets *) + + Lemma inj_pairP2 : + forall (P:U -> Prop) (x:U) (p q:P x), + ex_intro P x p = ex_intro P x q -> p = q. + Proof. + intros. + apply inj_right_pair with (A:=U). + intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. + assumption. + Qed. + +End DecidableEqDep. + +(************************************************************************) +(** ** Definition of the functor that builds properties of dependent equalities on decidable sets in Set *) + +(** The signature of decidable sets in [Set] *) + +Module Type DecidableSet. + + Parameter U:Set. + Axiom eq_dec : forall x y:U, {x = y} + {x <> y}. + +End DecidableSet. + +(** The module [DecidableEqDepSet] collects equality properties for decidable + set in [Set] *) + +Module DecidableEqDepSet (M:DecidableSet). + + Import M. + Module N:=DecidableEqDep(M). + + (** Invariance by Substitution of Reflexive Equality Proofs *) + + Lemma eq_rect_eq : + forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + Proof eq_rect_eq_dec eq_dec. + + (** Injectivity of Dependent Equality *) + + Theorem eq_dep_eq : + forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y. + Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq). + + (** Uniqueness of Identity Proofs (UIP) *) + + Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2. + Proof (eq_dep_eq__UIP U eq_dep_eq). + + (** Uniqueness of Reflexive Identity Proofs *) + + Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x. + Proof (UIP__UIP_refl U UIP). + + (** Streicher's axiom K *) + + Lemma Streicher_K : + forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. + Proof (K_dec_type eq_dec). + + (** Proof-irrelevance on subsets of decidable sets *) + + Lemma inj_pairP2 : + forall (P:U -> Prop) (x:U) (p q:P x), + ex_intro P x p = ex_intro P x q -> p = q. + Proof N.inj_pairP2. + + (** Injectivity of equality on dependent pairs in [Type] *) + + Lemma inj_pair2 : + forall (P:U -> Type) (p:U) (x y:P p), + existT P p x = existT P p y -> x = y. + Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq. + + (** Injectivity of equality on dependent pairs with second component + in [Type] *) + + 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, Eq_rect_eq_on. + intros; apply eq_rect_eq_dec. + apply eq_dec. +Qed. + +Register inj_pair2_eq_dec as core.eqdep_dec.inj_pair2. + + (** Examples of short direct proofs of unicity of reflexivity proofs + on specific domains *) + +Lemma UIP_refl_unit (x : tt = tt) : x = eq_refl tt. +Proof. + change (match tt as b return tt = b -> Prop with + | tt => fun x => x = eq_refl tt + end x). + destruct x; reflexivity. +Defined. + +Lemma UIP_refl_bool (b:bool) (x : b = b) : x = eq_refl. +Proof. + destruct b. + - change (match true as b return true=b -> Prop with + | true => fun x => x = eq_refl + | _ => fun _ => True + end x). + destruct x; reflexivity. + - change (match false as b return false=b -> Prop with + | false => fun x => x = eq_refl + | _ => fun _ => True + end x). + destruct x; reflexivity. +Defined. + +Lemma UIP_refl_nat (n:nat) (x : n = n) : x = eq_refl. +Proof. + induction n. + - change (match 0 as n return 0=n -> Prop with + | 0 => fun x => x = eq_refl + | _ => fun _ => True + end x). + destruct x; reflexivity. + - specialize IHn with (f_equal pred x). + change eq_refl with (f_equal S (@eq_refl _ n)). + rewrite <- IHn; clear IHn. + change (match S n as n' return S n = n' -> Prop with + | 0 => fun _ => True + | S n' => fun x => + x = f_equal S (f_equal pred x) + end x). + pattern (S n) at 2 3, x. + destruct x; reflexivity. +Defined. diff --git a/theories/Logic/ExtensionalFunctionRepresentative.v b/theories/Logic/ExtensionalFunctionRepresentative.v new file mode 100644 index 0000000000..0aac56bbcc --- /dev/null +++ b/theories/Logic/ExtensionalFunctionRepresentative.v @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module states a limited form axiom of functional + extensionality which selects a canonical representative in each + class of extensional functions *) + +(** Its main interest is that it is the needed ingredient to provide + axiom of choice on setoids (a.k.a. axiom of extensional choice) + when combined with classical logic and axiom of (intensonal) + choice *) + +(** It provides extensionality of functions while still supporting (a + priori) an intensional interpretation of equality *) + +Axiom extensional_function_representative : + forall A B, exists repr, forall (f : A -> B), + (forall x, f x = repr f x) /\ + (forall g, (forall x, f x = g x) -> repr f = repr g). diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v new file mode 100644 index 0000000000..a70bd92329 --- /dev/null +++ b/theories/Logic/ExtensionalityFacts.v @@ -0,0 +1,139 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Some facts and definitions about extensionality + +We investigate the relations between the following extensionality principles + +- Functional extensionality +- Equality of projections from diagonal +- Unicity of inverse bijections +- Bijectivity of bijective composition + +Table of contents + +1. Definitions + +2. Functional extensionality <-> Equality of projections from diagonal + +3. Functional extensionality <-> Unicity of inverse bijections + +4. Functional extensionality <-> Bijectivity of bijective composition + +*) + +Set Implicit Arguments. + +(**********************************************************************) +(** * Definitions *) + +(** Being an inverse *) + +Definition is_inverse A B f g := (forall a:A, g (f a) = a) /\ (forall b:B, f (g b) = b). + +(** The diagonal over A and the one-one correspondence with A *) + +#[universes(template)] +Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }. + +Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}. + +Arguments pi1 {A} _. +Arguments pi2 {A} _. + +Lemma diagonal_projs_same_behavior : forall A (x:Delta A), pi1 x = pi2 x. +Proof. + destruct x as (a1,a2,Heq); assumption. +Qed. + +Lemma diagonal_inverse1 : forall A, is_inverse (A:=A) delta pi1. +Proof. + split; [trivial|]; destruct b as (a1,a2,[]); reflexivity. +Qed. + +Lemma diagonal_inverse2 : forall A, is_inverse (A:=A) delta pi2. +Proof. + split; [trivial|]; destruct b as (a1,a2,[]); reflexivity. +Qed. + +(** Functional extensionality *) + +Local Notation FunctionalExtensionality := + (forall A B (f g : A -> B), (forall x, f x = g x) -> f = g). + +(** Equality of projections from diagonal *) + +Local Notation EqDeltaProjs := (forall A, pi1 = pi2 :> (Delta A -> A)). + +(** Unicity of bijection inverse *) + +Local Notation UniqueInverse := (forall A B (f:A->B) g1 g2, is_inverse f g1 -> is_inverse f g2 -> g1 = g2). + +(** Bijectivity of bijective composition *) + +Definition action A B C (f:A->B) := (fun h:B->C => fun x => h (f x)). + +Local Notation BijectivityBijectiveComp := (forall A B C (f:A->B) g, + is_inverse f g -> is_inverse (A:=B->C) (action f) (action g)). + +(**********************************************************************) +(** * Functional extensionality <-> Equality of projections from diagonal *) + +Theorem FunctExt_iff_EqDeltaProjs : FunctionalExtensionality <-> EqDeltaProjs. +Proof. + split. + - intros FunExt *; apply FunExt, diagonal_projs_same_behavior. + - intros EqProjs **; change f with (fun x => pi1 {|pi1:=f x; pi2:=g x; eq:=H x|}). + rewrite EqProjs; reflexivity. +Qed. + +(**********************************************************************) +(** * Functional extensionality <-> Unicity of bijection inverse *) + +Lemma FunctExt_UniqInverse : FunctionalExtensionality -> UniqueInverse. +Proof. + intros FunExt * (Hg1f,Hfg1) (Hg2f,Hfg2). + apply FunExt. intros; congruence. +Qed. + +Lemma UniqInverse_EqDeltaProjs : UniqueInverse -> EqDeltaProjs. +Proof. + intros UniqInv *. + apply UniqInv with delta; [apply diagonal_inverse1 | apply diagonal_inverse2]. +Qed. + +Theorem FunctExt_iff_UniqInverse : FunctionalExtensionality <-> UniqueInverse. +Proof. + split. + - apply FunctExt_UniqInverse. + - intro; apply FunctExt_iff_EqDeltaProjs, UniqInverse_EqDeltaProjs; trivial. +Qed. + +(**********************************************************************) +(** * Functional extensionality <-> Bijectivity of bijective composition *) + +Lemma FunctExt_BijComp : FunctionalExtensionality -> BijectivityBijectiveComp. +Proof. + intros FunExt * (Hgf,Hfg). split; unfold action. + - intros h; apply FunExt; intro b; rewrite Hfg; reflexivity. + - intros h; apply FunExt; intro a; rewrite Hgf; reflexivity. +Qed. + +Lemma BijComp_FunctExt : BijectivityBijectiveComp -> FunctionalExtensionality. +Proof. + intros BijComp. + apply FunctExt_iff_UniqInverse. intros * H1 H2. + destruct BijComp with (C:=A) (1:=H2) as (Hg2f,_). + destruct BijComp with (C:=A) (1:=H1) as (_,Hfg1). + rewrite <- (Hg2f g1). + change g1 with (action g1 (fun x => x)). + rewrite -> (Hfg1 (fun x => x)). + reflexivity. +Qed. diff --git a/theories/Logic/FinFun.v b/theories/Logic/FinFun.v new file mode 100644 index 0000000000..89f5a82a82 --- /dev/null +++ b/theories/Logic/FinFun.v @@ -0,0 +1,402 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Functions on finite domains *) + +(** Main result : for functions [f:A->A] with finite [A], + f injective <-> f bijective <-> f surjective. *) + +Require Import List Compare_dec EqNat Decidable ListDec. Require Fin. +Set Implicit Arguments. + +(** General definitions *) + +Definition Injective {A B} (f : A->B) := + forall x y, f x = f y -> x = y. + +Definition Surjective {A B} (f : A->B) := + forall y, exists x, f x = y. + +Definition Bijective {A B} (f : A->B) := + exists g:B->A, (forall x, g (f x) = x) /\ (forall y, f (g y) = y). + +(** Finiteness is defined here via exhaustive list enumeration *) + +Definition Full {A:Type} (l:list A) := forall a:A, In a l. +Definition Finite (A:Type) := exists (l:list A), Full l. + +(** In many following proofs, it will be convenient to have + list enumerations without duplicates. As soon as we have + decidability of equality (in Prop), this is equivalent + to the previous notion. *) + +Definition Listing {A:Type} (l:list A) := NoDup l /\ Full l. +Definition Finite' (A:Type) := exists (l:list A), Listing l. + +Lemma Finite_alt A (d:decidable_eq A) : Finite A <-> Finite' A. +Proof. + split. + - intros (l,F). destruct (uniquify d l) as (l' & N & I). + exists l'. split; trivial. + intros x. apply I, F. + - intros (l & _ & F). now exists l. +Qed. + +(** Injections characterized in term of lists *) + +Lemma Injective_map_NoDup A B (f:A->B) (l:list A) : + Injective f -> NoDup l -> NoDup (map f l). +Proof. + intros Ij. induction 1 as [|x l X N IH]; simpl; constructor; trivial. + rewrite in_map_iff. intros (y & E & Y). apply Ij in E. now subst. +Qed. + +Lemma Injective_list_carac A B (d:decidable_eq A)(f:A->B) : + Injective f <-> (forall l, NoDup l -> NoDup (map f l)). +Proof. + split. + - intros. now apply Injective_map_NoDup. + - intros H x y E. + destruct (d x y); trivial. + assert (N : NoDup (x::y::nil)). + { repeat constructor; simpl; intuition. } + specialize (H _ N). simpl in H. rewrite E in H. + inversion_clear H; simpl in *; intuition. +Qed. + +Lemma Injective_carac A B (l:list A) : Listing l -> + forall (f:A->B), Injective f <-> NoDup (map f l). +Proof. + intros L f. split. + - intros Ij. apply Injective_map_NoDup; trivial. apply L. + - intros N x y E. + assert (X : In x l) by apply L. + assert (Y : In y l) by apply L. + apply In_nth_error in X. destruct X as (i,X). + apply In_nth_error in Y. destruct Y as (j,Y). + assert (X' := map_nth_error f _ _ X). + assert (Y' := map_nth_error f _ _ Y). + assert (i = j). + { rewrite NoDup_nth_error in N. apply N. + - rewrite <- nth_error_Some. now rewrite X'. + - rewrite X', Y'. now f_equal. } + subst j. rewrite Y in X. now injection X. +Qed. + +(** Surjection characterized in term of lists *) + +Lemma Surjective_list_carac A B (f:A->B): + Surjective f <-> (forall lB, exists lA, incl lB (map f lA)). +Proof. + split. + - intros Su. + induction lB as [|b lB IH]. + + now exists nil. + + destruct (Su b) as (a,E). + destruct IH as (lA,IC). + exists (a::lA). simpl. rewrite E. + intros x [X|X]; simpl; intuition. + - intros H y. + destruct (H (y::nil)) as (lA,IC). + assert (IN : In y (map f lA)) by (apply (IC y); now left). + rewrite in_map_iff in IN. destruct IN as (x & E & _). + now exists x. +Qed. + +Lemma Surjective_carac A B : Finite B -> decidable_eq B -> + forall f:A->B, Surjective f <-> (exists lA, Listing (map f lA)). +Proof. + intros (lB,FB) d. split. + - rewrite Surjective_list_carac. + intros Su. destruct (Su lB) as (lA,IC). + destruct (uniquify_map d f lA) as (lA' & N & IC'). + exists lA'. split; trivial. + intro x. apply IC', IC, FB. + - intros (lA & N & FA) y. + generalize (FA y). rewrite in_map_iff. intros (x & E & _). + now exists x. +Qed. + +(** Main result : *) + +Lemma Endo_Injective_Surjective : + forall A, Finite A -> decidable_eq A -> + forall f:A->A, Injective f <-> Surjective f. +Proof. + intros A F d f. rewrite (Surjective_carac F d). split. + - apply (Finite_alt d) in F. destruct F as (l,L). + rewrite (Injective_carac L); intros. + exists l; split; trivial. + destruct L as (N,F). + assert (I : incl l (map f l)). + { apply NoDup_length_incl; trivial. + - now rewrite map_length. + - intros x _. apply F. } + intros x. apply I, F. + - clear F d. intros (l,L). + assert (N : NoDup l). { apply (NoDup_map_inv f), L. } + assert (I : incl (map f l) l). + { apply NoDup_length_incl; trivial. + - now rewrite map_length. + - intros x _. apply L. } + assert (L' : Listing l). + { split; trivial. + intro x. apply I, L. } + apply (Injective_carac L'), L. +Qed. + +(** An injective and surjective function is bijective. + We need here stronger hypothesis : decidability of equality in Type. *) + +Definition EqDec (A:Type) := forall x y:A, {x=y}+{x<>y}. + +(** First, we show that a surjective f has an inverse function g such that + f.g = id. *) + +(* NB: instead of (Finite A), we could ask for (RecEnum A) with: +Definition RecEnum A := exists h:nat->A, surjective h. +*) + +Lemma Finite_Empty_or_not A : + Finite A -> (A->False) \/ exists a:A,True. +Proof. + intros (l,F). + destruct l. + - left; exact F. + - right; now exists a. +Qed. + +Lemma Surjective_inverse : + forall A B, Finite A -> EqDec B -> + forall f:A->B, Surjective f -> + exists g:B->A, forall x, f (g x) = x. +Proof. + intros A B F d f Su. + destruct (Finite_Empty_or_not F) as [noA | (a,_)]. + - (* A is empty : g is obtained via False_rect *) + assert (noB : B -> False). { intros y. now destruct (Su y). } + exists (fun y => False_rect _ (noB y)). + intro y. destruct (noB y). + - (* A is inhabited by a : we use it in Option.get *) + destruct F as (l,F). + set (h := fun x k => if d (f k) x then true else false). + set (get := fun o => match o with Some y => y | None => a end). + exists (fun x => get (List.find (h x) l)). + intros x. + case_eq (find (h x) l); simpl; clear get; [intros y H|intros H]. + * apply find_some in H. destruct H as (_,H). unfold h in H. + now destruct (d (f y) x) in H. + * exfalso. + destruct (Su x) as (y & Y). + generalize (find_none _ l H y (F y)). + unfold h. now destruct (d (f y) x). +Qed. + +(** Same, with more knowledge on the inverse function: g.f = f.g = id *) + +Lemma Injective_Surjective_Bijective : + forall A B, Finite A -> EqDec B -> + forall f:A->B, Injective f -> Surjective f -> Bijective f. +Proof. + intros A B F d f Ij Su. + destruct (Surjective_inverse F d Su) as (g, E). + exists g. split; trivial. + intros y. apply Ij. now rewrite E. +Qed. + + +(** An example of finite type : [Fin.t] *) + +Lemma Fin_Finite n : Finite (Fin.t n). +Proof. + induction n. + - exists nil. + red;inversion a. + - destruct IHn as (l,Hl). + exists (Fin.F1 :: map Fin.FS l). + intros a. revert n a l Hl. + refine (@Fin.caseS _ _ _); intros. + + now left. + + right. now apply in_map. +Qed. + +(** Instead of working on a finite subset of nat, another + solution is to use restricted [nat->nat] functions, and + to consider them only below a certain bound [n]. *) + +Definition bFun n (f:nat->nat) := forall x, x < n -> f x < n. + +Definition bInjective n (f:nat->nat) := + forall x y, x < n -> y < n -> f x = f y -> x = y. + +Definition bSurjective n (f:nat->nat) := + forall y, y < n -> exists x, x < n /\ f x = y. + +(** We show that this is equivalent to the use of [Fin.t n]. *) + +Module Fin2Restrict. + +Notation n2f := Fin.of_nat_lt. +Definition f2n {n} (x:Fin.t n) := proj1_sig (Fin.to_nat x). +Definition f2n_ok n (x:Fin.t n) : f2n x < n := proj2_sig (Fin.to_nat x). +Definition n2f_f2n : forall n x, n2f (f2n_ok x) = x := @Fin.of_nat_to_nat_inv. +Definition f2n_n2f x n h : f2n (n2f h) = x := f_equal (@proj1_sig _ _) (@Fin.to_nat_of_nat x n h). +Definition n2f_ext : forall x n h h', n2f h = n2f h' := @Fin.of_nat_ext. +Definition f2n_inj : forall n x y, f2n x = f2n y -> x = y := @Fin.to_nat_inj. + +Definition extend n (f:Fin.t n -> Fin.t n) : (nat->nat) := + fun x => + match le_lt_dec n x with + | left _ => 0 + | right h => f2n (f (n2f h)) + end. + +Definition restrict n (f:nat->nat)(hf : bFun n f) : (Fin.t n -> Fin.t n) := + fun x => let (x',h) := Fin.to_nat x in n2f (hf _ h). + +Ltac break_dec H := + let H' := fresh "H" in + destruct le_lt_dec as [H'|H']; + [elim (Lt.le_not_lt _ _ H' H) + |try rewrite (n2f_ext H' H) in *; try clear H']. + +Lemma extend_ok n f : bFun n (@extend n f). +Proof. + intros x h. unfold extend. break_dec h. apply f2n_ok. +Qed. + +Lemma extend_f2n n f (x:Fin.t n) : extend f (f2n x) = f2n (f x). +Proof. + generalize (n2f_f2n x). unfold extend, f2n, f2n_ok. + destruct (Fin.to_nat x) as (x',h); simpl. + break_dec h. + now intros ->. +Qed. + +Lemma extend_n2f n f x (h:x<n) : n2f (extend_ok f h) = f (n2f h). +Proof. + generalize (extend_ok f h). unfold extend in *. break_dec h. intros h'. + rewrite <- n2f_f2n. now apply n2f_ext. +Qed. + +Lemma restrict_f2n n f hf (x:Fin.t n) : + f2n (@restrict n f hf x) = f (f2n x). +Proof. + unfold restrict, f2n. destruct (Fin.to_nat x) as (x',h); simpl. + apply f2n_n2f. +Qed. + +Lemma restrict_n2f n f hf x (h:x<n) : + @restrict n f hf (n2f h) = n2f (hf _ h). +Proof. + unfold restrict. generalize (f2n_n2f h). unfold f2n. + destruct (Fin.to_nat (n2f h)) as (x',h'); simpl. intros ->. + now apply n2f_ext. +Qed. + +Lemma extend_surjective n f : + bSurjective n (@extend n f) <-> Surjective f. +Proof. + split. + - intros hf y. + destruct (hf _ (f2n_ok y)) as (x & h & Eq). + exists (n2f h). + apply f2n_inj. now rewrite <- Eq, <- extend_f2n, f2n_n2f. + - intros hf y hy. + destruct (hf (n2f hy)) as (x,Eq). + exists (f2n x). + split. + + apply f2n_ok. + + rewrite extend_f2n, Eq. apply f2n_n2f. +Qed. + +Lemma extend_injective n f : + bInjective n (@extend n f) <-> Injective f. +Proof. + split. + - intros hf x y Eq. + apply f2n_inj. apply hf; try apply f2n_ok. + now rewrite 2 extend_f2n, Eq. + - intros hf x y hx hy Eq. + rewrite <- (f2n_n2f hx), <- (f2n_n2f hy). f_equal. + apply hf. + rewrite <- 2 extend_n2f. + generalize (extend_ok f hx) (extend_ok f hy). + rewrite Eq. apply n2f_ext. +Qed. + +Lemma restrict_surjective n f h : + Surjective (@restrict n f h) <-> bSurjective n f. +Proof. + split. + - intros hf y hy. + destruct (hf (n2f hy)) as (x,Eq). + exists (f2n x). + split. + + apply f2n_ok. + + rewrite <- (restrict_f2n h), Eq. apply f2n_n2f. + - intros hf y. + destruct (hf _ (f2n_ok y)) as (x & hx & Eq). + exists (n2f hx). + apply f2n_inj. now rewrite restrict_f2n, f2n_n2f. +Qed. + +Lemma restrict_injective n f h : + Injective (@restrict n f h) <-> bInjective n f. +Proof. + split. + - intros hf x y hx hy Eq. + rewrite <- (f2n_n2f hx), <- (f2n_n2f hy). f_equal. + apply hf. + rewrite 2 restrict_n2f. + generalize (h x hx) (h y hy). + rewrite Eq. apply n2f_ext. + - intros hf x y Eq. + apply f2n_inj. apply hf; try apply f2n_ok. + now rewrite <- 2 (restrict_f2n h), Eq. +Qed. + +End Fin2Restrict. +Import Fin2Restrict. + +(** We can now use Proof via the equivalence ... *) + +Lemma bInjective_bSurjective n (f:nat->nat) : + bFun n f -> (bInjective n f <-> bSurjective n f). +Proof. + intros h. + rewrite <- (restrict_injective h), <- (restrict_surjective h). + apply Endo_Injective_Surjective. + - apply Fin_Finite. + - intros x y. destruct (Fin.eq_dec x y); [left|right]; trivial. +Qed. + +Lemma bSurjective_bBijective n (f:nat->nat) : + bFun n f -> bSurjective n f -> + exists g, bFun n g /\ forall x, x < n -> g (f x) = x /\ f (g x) = x. +Proof. + intro hf. + rewrite <- (restrict_surjective hf). intros Su. + assert (Ij : Injective (restrict hf)). + { apply Endo_Injective_Surjective; trivial. + - apply Fin_Finite. + - intros x y. destruct (Fin.eq_dec x y); [left|right]; trivial. } + assert (Bi : Bijective (restrict hf)). + { apply Injective_Surjective_Bijective; trivial. + - apply Fin_Finite. + - exact Fin.eq_dec. } + destruct Bi as (g & Hg & Hg'). + exists (extend g). + split. + - apply extend_ok. + - intros x Hx. split. + + now rewrite <- (f2n_n2f Hx), <- (restrict_f2n hf), extend_f2n, Hg. + + now rewrite <- (f2n_n2f Hx), extend_f2n, <- (restrict_f2n hf), Hg'. +Qed. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v new file mode 100644 index 0000000000..95e1af2ead --- /dev/null +++ b/theories/Logic/FunctionalExtensionality.v @@ -0,0 +1,238 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. + It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *) + +(** The converse of functional extensionality. *) + +Lemma equal_f : forall {A B : Type} {f g : A -> B}, + f = g -> forall x, f x = g x. +Proof. + intros. + rewrite H. + auto. +Qed. + +Lemma equal_f_dep : forall {A B} {f g : forall (x : A), B x}, + f = g -> forall x, f x = g x. +Proof. +intros A B f g <- H; reflexivity. +Qed. + +(** Statements of functional extensionality for simple and dependent functions. *) + +Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, + forall (f g : forall x : A, B x), + (forall x, f x = g x) -> f = g. + +Lemma functional_extensionality {A B} (f g : A -> B) : + (forall x, f x = g x) -> f = g. +Proof. + intros ; eauto using @functional_extensionality_dep. +Qed. + +(** Extensionality of [forall]s follows from functional extensionality. *) +Lemma forall_extensionality {A} {B C : A -> Type} (H : forall x : A, B x = C x) +: (forall x, B x) = (forall x, C x). +Proof. + apply functional_extensionality in H. destruct H. reflexivity. +Defined. + +Lemma forall_extensionalityP {A} {B C : A -> Prop} (H : forall x : A, B x = C x) +: (forall x, B x) = (forall x, C x). +Proof. + apply functional_extensionality in H. destruct H. reflexivity. +Defined. + +Lemma forall_extensionalityS {A} {B C : A -> Set} (H : forall x : A, B x = C x) +: (forall x, B x) = (forall x, C x). +Proof. + apply functional_extensionality in H. destruct H. reflexivity. +Defined. + +(** A version of [functional_extensionality_dep] which is provably + equal to [eq_refl] on [fun _ => eq_refl] *) +Definition functional_extensionality_dep_good + {A} {B : A -> Type} + (f g : forall x : A, B x) + (H : forall x, f x = g x) + : f = g + := eq_trans (eq_sym (functional_extensionality_dep f f (fun _ => eq_refl))) + (functional_extensionality_dep f g H). + +Lemma functional_extensionality_dep_good_refl {A B} f + : @functional_extensionality_dep_good A B f f (fun _ => eq_refl) = eq_refl. +Proof. + unfold functional_extensionality_dep_good; edestruct functional_extensionality_dep; reflexivity. +Defined. + +Opaque functional_extensionality_dep_good. + +Lemma forall_sig_eq_rect + {A B} (f : forall a : A, B a) + (P : { g : _ | (forall a, f a = g a) } -> Type) + (k : P (exist (fun g => forall a, f a = g a) f (fun a => eq_refl))) + g +: P g. +Proof. + destruct g as [g1 g2]. + set (g' := fun x => (exist _ (g1 x) (g2 x))). + change g2 with (fun x => proj2_sig (g' x)). + change g1 with (fun x => proj1_sig (g' x)). + clearbody g'; clear g1 g2. + cut (forall x, (exist _ (f x) eq_refl) = g' x). + { intro H'. + apply functional_extensionality_dep_good in H'. + destruct H'. + exact k. } + { intro x. + destruct (g' x) as [g'x1 g'x2]. + destruct g'x2. + reflexivity. } +Defined. + +Definition forall_eq_rect + {A B} (f : forall a : A, B a) + (P : forall g, (forall a, f a = g a) -> Type) + (k : P f (fun a => eq_refl)) + g H + : P g H + := @forall_sig_eq_rect A B f (fun g => P (proj1_sig g) (proj2_sig g)) k (exist _ g H). + +Definition forall_eq_rect_comp {A B} f P k + : @forall_eq_rect A B f P k f (fun _ => eq_refl) = k. +Proof. + unfold forall_eq_rect, forall_sig_eq_rect; simpl. + rewrite functional_extensionality_dep_good_refl; reflexivity. +Qed. + +Definition f_equal__functional_extensionality_dep_good + {A B f g} H a + : f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H) = H a. +Proof. + apply forall_eq_rect with (H := H); clear H g. + change (eq_refl (f a)) with (f_equal (fun h => h a) (eq_refl f)). + apply f_equal, functional_extensionality_dep_good_refl. +Defined. + +Definition f_equal__functional_extensionality_dep_good__fun + {A B f g} H + : (fun a => f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H)) = H. +Proof. + apply functional_extensionality_dep_good; intro a; apply f_equal__functional_extensionality_dep_good. +Defined. + +(** Apply [functional_extensionality], introducing variable x. *) + +Tactic Notation "extensionality" ident(x) := + match goal with + [ |- ?X = ?Y ] => + (apply (@functional_extensionality _ _ X Y) || + apply (@functional_extensionality_dep _ _ X Y) || + apply forall_extensionalityP || + apply forall_extensionalityS || + apply forall_extensionality) ; intro x + end. + +(** Iteratively apply [functional_extensionality] on an hypothesis + until finding an equality statement *) +(* Note that you can write [Ltac extensionality_in_checker tac ::= tac tt.] to get a more informative error message. *) +Ltac extensionality_in_checker tac := + first [ tac tt | fail 1 "Anomaly: Unexpected error in extensionality tactic. Please report." ]. +Tactic Notation "extensionality" "in" hyp(H) := + let rec check_is_extensional_equality H := + lazymatch type of H with + | _ = _ => constr:(Prop) + | forall a : ?A, ?T + => let Ha := fresh in + constr:(forall a : A, match H a with Ha => ltac:(let v := check_is_extensional_equality Ha in exact v) end) + end in + let assert_is_extensional_equality H := + first [ let dummy := check_is_extensional_equality H in idtac + | fail 1 "Not an extensional equality" ] in + let assert_not_intensional_equality H := + lazymatch type of H with + | _ = _ => fail "Already an intensional equality" + | _ => idtac + end in + let enforce_no_body H := + (tryif (let dummy := (eval unfold H in H) in idtac) + then clearbody H + else idtac) in + let rec extensionality_step_make_type H := + lazymatch type of H with + | forall a : ?A, ?f = ?g + => constr:({ H' | (fun a => f_equal (fun h => h a) H') = H }) + | forall a : ?A, _ + => let H' := fresh in + constr:(forall a : A, match H a with H' => ltac:(let ret := extensionality_step_make_type H' in exact ret) end) + end in + let rec eta_contract T := + lazymatch (eval cbv beta in T) with + | context T'[fun a : ?A => ?f a] + => let T'' := context T'[f] in + eta_contract T'' + | ?T => T + end in + let rec lift_sig_extensionality H := + lazymatch type of H with + | sig _ => H + | forall a : ?A, _ + => let Ha := fresh in + let ret := constr:(fun a : A => match H a with Ha => ltac:(let v := lift_sig_extensionality Ha in exact v) end) in + lazymatch type of ret with + | forall a : ?A, sig (fun b : ?B => @?f a b = @?g a b) + => eta_contract (exist (fun b : (forall a : A, B) => (fun a : A => f a (b a)) = (fun a : A => g a (b a))) + (fun a : A => proj1_sig (ret a)) + (@functional_extensionality_dep_good _ _ _ _ (fun a : A => proj2_sig (ret a)))) + end + end in + let extensionality_pre_step H H_out Heq := + let T := extensionality_step_make_type H in + let H' := fresh in + assert (H' : T) by (intros; eexists; apply f_equal__functional_extensionality_dep_good__fun); + let H''b := lift_sig_extensionality H' in + case H''b; clear H'; + intros H_out Heq in + let rec extensionality_rec H H_out Heq := + lazymatch type of H with + | forall a, _ = _ + => extensionality_pre_step H H_out Heq + | _ + => let pre_H_out' := fresh H_out in + let H_out' := fresh pre_H_out' in + extensionality_pre_step H H_out' Heq; + let Heq' := fresh Heq in + extensionality_rec H_out' H_out Heq'; + subst H_out' + end in + first [ assert_is_extensional_equality H | fail 1 "Not an extensional equality" ]; + first [ assert_not_intensional_equality H | fail 1 "Already an intensional equality" ]; + (tryif enforce_no_body H then idtac else clearbody H); + let H_out := fresh in + let Heq := fresh "Heq" in + extensionality_in_checker ltac:(fun tt => extensionality_rec H H_out Heq); + (* If we [subst H], things break if we already have another equation of the form [_ = H] *) + destruct Heq; rename H_out into H. + +(** Eta expansion is built into Coq. *) + +Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) : + f = fun x => f x. +Proof. + intros. + reflexivity. +Qed. + +Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x. +Proof. + apply (eta_expansion_dep f). +Qed. diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v new file mode 100644 index 0000000000..6c4a8533a1 --- /dev/null +++ b/theories/Logic/Hurkens.v @@ -0,0 +1,719 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(* Hurkens.v *) +(************************************************************************) + +(** Exploiting Hurkens's paradox [[Hurkens95]] for system U- so as to + derive various contradictory contexts. + + The file is divided into various sub-modules which all follow the + same structure: a section introduces the contradictory hypotheses + and a theorem named [paradox] concludes the module with a proof of + [False]. + + - The [Generic] module contains the actual Hurkens's paradox for a + postulated shallow encoding of system U- in Coq. This is an + adaptation by Arnaud Spiwack of a previous, more restricted + implementation by Herman Geuvers. It is used to derive every + other special cases of the paradox in this file. + + - The [NoRetractToImpredicativeUniverse] module contains a simple + and effective formulation by Herman Geuvers [[Geuvers01]] of a + result by Thierry Coquand [[Coquand90]]. It states that no + impredicative sort can contain a type of which it is a + retract. This result implies that Coq with classical logic + stated in impredicative Set is inconsistent and that classical + logic stated in Prop implies proof-irrelevance (see + [ClassicalFacts.v]) + + - The [NoRetractFromSmallPropositionToProp] module is a + specialisation of the [NoRetractToImpredicativeUniverse] module + to the case where the impredicative sort is [Prop]. + + - The [NoRetractToModalProposition] module is a strengthening of + the [NoRetractFromSmallPropositionToProp] module. It shows that + given a monadic modality (aka closure operator) [M], the type of + modal propositions (i.e. such that [M A -> A]) cannot be a + retract of a modal proposition. It is an example of use of the + paradox where the universes of system U- are not mapped to + universes of Coq. + + - The [NoRetractToNegativeProp] module is the specialisation of + the [NoRetractFromSmallPropositionToProp] module where the + modality is double-negation. This result implies that the + principle of weak excluded middle ([forall A, ~~A\/~A]) implies + a weak variant of proof irrelevance. + + - The [NoRetractFromTypeToProp] module proves that [Prop] cannot + be a retract of a larger type. + + - The [TypeNeqSmallType] module proves that [Type] is different + from any smaller type. + + - The [PropNeqType] module proves that [Prop] is different from + any larger [Type]. It is an instance of the previous result. + + References: + + - [[Coquand90]] T. Coquand, "Metamathematical Investigations of a + Calculus of Constructions", Proceedings of Logic in Computer + Science (LICS'90), 1990. + + - [[Hurkens95]] A. J. Hurkens, "A simplification of Girard's paradox", + Proceedings of the 2nd international conference Typed Lambda-Calculi + and Applications (TLCA'95), 1995. + + - [[Geuvers01]] H. Geuvers, "Inconsistency of Classical Logic in Type + Theory", 2001, revised 2007 + (see {{http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz}}). +*) + + +Set Universe Polymorphism. + +(* begin show *) + +(** * A modular proof of Hurkens's paradox. *) + +(** It relies on an axiomatisation of a shallow embedding of system U- + (i.e. types of U- are interpreted by types of Coq). The + universes are encoded in a style, due to Martin-Löf, where they + are given by a set of names and a family [El:Name->Type] which + interprets each name into a type. This allows the encoding of + universe to be decoupled from Coq's universes. Dependent products + and abstractions are similarly postulated rather than encoded as + Coq's dependent products and abstractions. *) + +Module Generic. + +(* begin hide *) +(* Notations used in the proof. Hidden in coqdoc. *) + +Reserved Notation "'∀₁' x : A , B" (at level 200, x ident, A at level 200,right associativity). +Reserved Notation "A '⟶₁' B" (at level 99, right associativity, B at level 200). +Reserved Notation "'λ₁' x , u" (at level 200, x ident, right associativity). +Reserved Notation "f '·₁' x" (at level 5, left associativity). +Reserved Notation "'∀₂' A , F" (at level 200, A ident, right associativity). +Reserved Notation "'λ₂' x , u" (at level 200, x ident, right associativity). +Reserved Notation "f '·₁' [ A ]" (at level 5, left associativity). +Reserved Notation "'∀₀' x : A , B" (at level 200, x ident, A at level 200,right associativity). +Reserved Notation "A '⟶₀' B" (at level 99, right associativity, B at level 200). +Reserved Notation "'λ₀' x , u" (at level 200, x ident, right associativity). +Reserved Notation "f '·₀' x" (at level 5, left associativity). +Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associativity). +Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity). +Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity). + +(* end hide *) + +Section Paradox. + +(** ** Axiomatisation of impredicative universes in a Martin-Löf style *) + +(** System U- has two impredicative universes. In the proof of the + paradox they are slightly asymmetric (in particular the reduction + rules of the small universe are not needed). Therefore, the + axioms are duplicated allowing for a weaker requirement than the + actual system U-. *) + + +(** *** Large universe *) +Variable U1 : Type. +Variable El1 : U1 -> Type. +(** **** Closure by small product *) +Variable Forall1 : forall u:U1, (El1 u -> U1) -> U1. + Notation "'∀₁' x : A , B" := (Forall1 A (fun x => B)). + Notation "A '⟶₁' B" := (Forall1 A (fun _ => B)). +Variable lam1 : forall u B, (forall x:El1 u, El1 (B x)) -> El1 (∀₁ x:u, B x). + Notation "'λ₁' x , u" := (lam1 _ _ (fun x => u)). +Variable app1 : forall u B (f:El1 (Forall1 u B)) (x:El1 u), El1 (B x). + Notation "f '·₁' x" := (app1 _ _ f x). +Variable beta1 : forall u B (f:forall x:El1 u, El1 (B x)) x, + (λ₁ y, f y) ·₁ x = f x. +(** **** Closure by large products *) +(** [U1] only needs to quantify over itself. *) +Variable ForallU1 : (U1->U1) -> U1. + Notation "'∀₂' A , F" := (ForallU1 (fun A => F)). +Variable lamU1 : forall F, (forall A:U1, El1 (F A)) -> El1 (∀₂ A, F A). + Notation "'λ₂' x , u" := (lamU1 _ (fun x => u)). +Variable appU1 : forall F (f:El1(∀₂ A,F A)) (A:U1), El1 (F A). + Notation "f '·₁' [ A ]" := (appU1 _ f A). +Variable betaU1 : forall F (f:forall A:U1, El1 (F A)) A, + (λ₂ x, f x) ·₁ [ A ] = f A. + +(** *** Small universe *) +(** The small universe is an element of the large one. *) +Variable u0 : U1. +Notation U0 := (El1 u0). +Variable El0 : U0 -> Type. +(** **** Closure by small product *) +(** [U0] does not need reduction rules *) +Variable Forall0 : forall u:U0, (El0 u -> U0) -> U0. + Notation "'∀₀' x : A , B" := (Forall0 A (fun x => B)). + Notation "A '⟶₀' B" := (Forall0 A (fun _ => B)). +Variable lam0 : forall u B, (forall x:El0 u, El0 (B x)) -> El0 (∀₀ x:u, B x). + Notation "'λ₀' x , u" := (lam0 _ _ (fun x => u)). +Variable app0 : forall u B (f:El0 (Forall0 u B)) (x:El0 u), El0 (B x). + Notation "f '·₀' x" := (app0 _ _ f x). +(** **** Closure by large products *) +Variable ForallU0 : forall u:U1, (El1 u->U0) -> U0. + Notation "'∀₀¹' A : U , F" := (ForallU0 U (fun A => F)). +Variable lamU0 : forall U F, (forall A:El1 U, El0 (F A)) -> El0 (∀₀¹ A:U, F A). + Notation "'λ₀¹' x , u" := (lamU0 _ _ (fun x => u)). +Variable appU0 : forall U F (f:El0(∀₀¹ A:U,F A)) (A:El1 U), El0 (F A). + Notation "f '·₀' [ A ]" := (appU0 _ _ f A). + +(** ** Automating the rewrite rules of our encoding. *) +Local Ltac simplify := + (* spiwack: ideally we could use [rewrite_strategy] here, but I am a tad + scared of the idea of depending on setoid rewrite in such a simple + file. *) + (repeat rewrite ?beta1, ?betaU1); + lazy beta. + +Local Ltac simplify_in h := + (repeat rewrite ?beta1, ?betaU1 in h); + lazy beta in h. + + +(** ** Hurkens's paradox. *) + +(** An inhabitant of [U0] standing for [False]. *) +Variable F:U0. + +(** *** Preliminary definitions *) + +Definition V : U1 := ∀₂ A, ((A ⟶₁ u0) ⟶₁ A ⟶₁ u0) ⟶₁ A ⟶₁ u0. +Definition U : U1 := V ⟶₁ u0. + +Definition sb (z:El1 V) : El1 V := λ₂ A, λ₁ r, λ₁ a, r ·₁ (z·₁[A]·₁r) ·₁ a. + +Definition le (i:El1 (U⟶₁u0)) (x:El1 U) : U0 := + x ·₁ (λ₂ A, λ₁ r, λ₁ a, i ·₁ (λ₁ v, (sb v) ·₁ [A] ·₁ r ·₁ a)). +Definition le' : El1 ((U⟶₁u0) ⟶₁ U ⟶₁ u0) := λ₁ i, λ₁ x, le i x. +Definition induct (i:El1 (U⟶₁u0)) : U0 := + ∀₀¹ x:U, le i x ⟶₀ i ·₁ x. + +Definition WF : El1 U := λ₁ z, (induct (z·₁[U] ·₁ le')). +Definition I (x:El1 U) : U0 := + (∀₀¹ i:U⟶₁u0, le i x ⟶₀ i ·₁ (λ₁ v, (sb v) ·₁ [U] ·₁ le' ·₁ x)) ⟶₀ F +. + +(** *** Proof *) + +Lemma Omega : El0 (∀₀¹ i:U⟶₁u0, induct i ⟶₀ i ·₁ WF). +Proof. + refine (λ₀¹ i, λ₀ y, _). + refine (y·₀[_]·₀_). + unfold le,WF,induct. simplify. + refine (λ₀¹ x, λ₀ h0, _). simplify. + refine (y·₀[_]·₀_). + unfold le. simplify. + unfold sb at 1. simplify. + unfold le' at 1. simplify. + exact h0. +Qed. + +Lemma lemma1 : El0 (induct (λ₁ u, I u)). +Proof. + unfold induct. + refine (λ₀¹ x, λ₀ p, _). simplify. + refine (λ₀ q,_). + assert (El0 (I (λ₁ v, (sb v)·₁[U]·₁le'·₁x))) as h. + { generalize (q·₀[λ₁ u, I u]·₀p). simplify. + intros q'. + exact q'. } + refine (h·₀_). + refine (λ₀¹ i,_). + refine (λ₀ h', _). + generalize (q·₀[λ₁ y, i ·₁ (λ₁ v, (sb v)·₁[U] ·₁ le' ·₁ y)]). simplify. + intros q'. + refine (q'·₀_). clear q'. + unfold le at 1 in h'. simplify_in h'. + unfold sb at 1 in h'. simplify_in h'. + unfold le' at 1 in h'. simplify_in h'. + exact h'. +Qed. + +Lemma lemma2 : El0 ((∀₀¹i:U⟶₁u0, induct i ⟶₀ i·₁WF) ⟶₀ F). +Proof. + refine (λ₀ x, _). + assert (El0 (I WF)) as h. + { generalize (x·₀[λ₁ u, I u]·₀lemma1). simplify. + intros q. + exact q. } + refine (h·₀_). clear h. + refine (λ₀¹ i, λ₀ h0, _). + generalize (x·₀[λ₁ y, i·₁(λ₁ v, (sb v)·₁[U]·₁le'·₁y)]). simplify. + intros q. + refine (q·₀_). clear q. + unfold le in h0. simplify_in h0. + unfold WF in h0. simplify_in h0. + exact h0. +Qed. + +Theorem paradox : El0 F. +Proof. + exact (lemma2·₀Omega). +Qed. + +End Paradox. + +(** The [paradox] tactic can be called as a shortcut to use the paradox. *) +Ltac paradox h := + unshelve (refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ))). + +End Generic. + +(** * Impredicative universes are not retracts. *) + +(** There can be no retract to an impredicative Coq universe from a + smaller type. In this version of the proof, the impredicativity of + the universe is postulated with a pair of functions from the + universe to its type and back which commute with dependent product + in an appropriate way. *) + +Module NoRetractToImpredicativeUniverse. + +Section Paradox. + +Let U2 := Type. +Let U1:U2 := Type. +Variable U0:U1. + +(** *** [U1] is impredicative *) +Variable u22u1 : U2 -> U1. +Hypothesis u22u1_unit : forall (c:U2), c -> u22u1 c. +(** [u22u1_counit] and [u22u1_coherent] only apply to dependent + product so that the equations happen in the smaller [U1] rather + than [U2]. Indeed, it is not generally the case that one can + project from a large universe to an impredicative universe and + then get back the original type again. It would be too strong a + hypothesis to require (in particular, it is not true of + [Prop]). The formulation is reminiscent of the monadic + characteristic of the projection from a large type to [Prop].*) +Hypothesis u22u1_counit : forall (F:U1->U1), u22u1 (forall A,F A) -> (forall A,F A). +Hypothesis u22u1_coherent : forall (F:U1 -> U1) (f:forall x:U1, F x) (x:U1), + u22u1_counit _ (u22u1_unit _ f) x = f x. + +(** *** [U0] is a retract of [U1] *) +Variable u02u1 : U0 -> U1. +Variable u12u0 : U1 -> U0. +Hypothesis u12u0_unit : forall (b:U1), b -> u02u1 (u12u0 b). +Hypothesis u12u0_counit : forall (b:U1), u02u1 (u12u0 b) -> b. + +(** ** Paradox *) + +Theorem paradox : forall F:U1, F. +Proof. + intros F. + Generic.paradox h. + (** Large universe *) + + exact U1. + + exact (fun X => X). + + cbn. exact (fun u F => forall x:u, F x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + + cbn. exact (fun F => u22u1 (forall x, F x)). + + cbn. exact (fun _ x => u22u1_unit _ x). + + cbn. exact (fun _ x => u22u1_counit _ x). + (** Small universe *) + + exact U0. + (** The interpretation of the small universe is the image of + [U0] in [U1]. *) + + cbn. exact (fun X => u02u1 X). + + cbn. exact (fun u F => u12u0 (forall x:(u02u1 u), u02u1 (F x))). + + cbn. exact (fun u F => u12u0 (forall x:u, u02u1 (F x))). + + cbn. exact (u12u0 F). + + cbn in h. + exact (u12u0_counit _ h). + + cbn. easy. + + cbn. intros **. now rewrite u22u1_coherent. + + cbn. intros * x. exact (u12u0_unit _ x). + + cbn. intros * x. exact (u12u0_counit _ x). + + cbn. intros * x. exact (u12u0_unit _ x). + + cbn. intros * x. exact (u12u0_counit _ x). +Qed. + +End Paradox. + +End NoRetractToImpredicativeUniverse. + +(** * Modal fragments of [Prop] are not retracts *) + +(** In presence of a a monadic modality on [Prop], we can define a + subset of [Prop] of modal propositions which is also a complete + Heyting algebra. These cannot be a retract of a modal + proposition. This is a case where the universe in system U- are + not encoded as Coq universes. *) + +Module NoRetractToModalProposition. + +(** ** Monadic modality *) + +Section Paradox. + +Variable M : Prop -> Prop. +Hypothesis incr : forall A B:Prop, (A->B) -> M A -> M B. + +Lemma strength: forall A (P:A->Prop), M(forall x:A,P x) -> forall x:A,M(P x). +Proof. + intros A P h x. + eapply incr in h; eauto. +Qed. + +(** ** The universe of modal propositions *) + +Definition MProp := { P:Prop | M P -> P }. +Definition El : MProp -> Prop := @proj1_sig _ _. + +Lemma modal : forall P:MProp, M(El P) -> El P. +Proof. + intros [P m]. cbn. + exact m. +Qed. + +Definition Forall {A:Type} (P:A->MProp) : MProp. +Proof. + unshelve (refine (exist _ _ _)). + + exact (forall x:A, El (P x)). + + intros h x. + eapply strength in h. + eauto using modal. +Defined. + +(** ** Retract of the modal fragment of [Prop] in a small type *) + +(** The retract is axiomatized using logical equivalence as the + equality on propositions. *) + +Variable bool : MProp. +Variable p2b : MProp -> El bool. +Variable b2p : El bool -> MProp. +Hypothesis p2p1 : forall A:MProp, El (b2p (p2b A)) -> El A. +Hypothesis p2p2 : forall A:MProp, El A -> El (b2p (p2b A)). + +(** ** Paradox *) + +Theorem paradox : forall B:MProp, El B. +Proof. + intros B. + Generic.paradox h. + (** Large universe *) + + exact MProp. + + exact El. + + exact (fun _ => Forall). + + cbn. exact (fun _ _ f => f). + + cbn. exact (fun _ _ f => f). + + exact Forall. + + cbn. exact (fun _ f => f). + + cbn. exact (fun _ f => f). + (** Small universe *) + + exact bool. + + exact (fun b => El (b2p b)). + + cbn. exact (fun _ F => p2b (Forall (fun x => b2p (F x)))). + + exact (fun _ F => p2b (Forall (fun x => b2p (F x)))). + + apply p2b. + exact B. + + cbn in h. auto. + + cbn. easy. + + cbn. easy. + + cbn. auto. + + cbn. intros * f. + apply p2p1 in f. cbn in f. + exact f. + + cbn. auto. + + cbn. intros * f. + apply p2p1 in f. cbn in f. + exact f. +Qed. + +End Paradox. + +End NoRetractToModalProposition. + +(** * The negative fragment of [Prop] is not a retract *) + +(** The existence in the pure Calculus of Constructions of a retract + from the negative fragment of [Prop] into a negative proposition + is inconsistent. This is an instance of the previous result. *) + +Module NoRetractToNegativeProp. + +(** ** The universe of negative propositions. *) + +Definition NProp := { P:Prop | ~~P -> P }. +Definition El : NProp -> Prop := @proj1_sig _ _. + +Section Paradox. + +(** ** Retract of the negative fragment of [Prop] in a small type *) + +(** The retract is axiomatized using logical equivalence as the + equality on propositions. *) + +Variable bool : NProp. +Variable p2b : NProp -> El bool. +Variable b2p : El bool -> NProp. +Hypothesis p2p1 : forall A:NProp, El (b2p (p2b A)) -> El A. +Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). + +(** ** Paradox *) + +Theorem paradox : forall B:NProp, El B. +Proof. + intros B. + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + + exact (fun P => ~~P). + + exact bool. + + exact p2b. + + exact b2p. + + exact B. + + exact h. + + cbn. auto. + + cbn. auto. + + cbn. auto. +Qed. + +End Paradox. + +End NoRetractToNegativeProp. + +(** * Prop is not a retract *) + +(** The existence in the pure Calculus of Constructions of a retract + from [Prop] into a small type of [Prop] is inconsistent. This is a + special case of the previous result. *) + +Module NoRetractFromSmallPropositionToProp. + +(** ** The universe of propositions. *) + +Definition NProp := { P:Prop | P -> P}. +Definition El : NProp -> Prop := @proj1_sig _ _. + +Section MParadox. + +(** ** Retract of [Prop] in a small type, using the identity modality. *) + +Variable bool : NProp. +Variable p2b : NProp -> El bool. +Variable b2p : El bool -> NProp. +Hypothesis p2p1 : forall A:NProp, El (b2p (p2b A)) -> El A. +Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). + +(** ** Paradox *) + +Theorem mparadox : forall B:NProp, El B. +Proof. + intros B. + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + + exact (fun P => P). + + exact bool. + + exact p2b. + + exact b2p. + + exact B. + + exact h. + + cbn. auto. + + cbn. auto. + + cbn. auto. +Qed. + +End MParadox. + +Section Paradox. + +(** ** Retract of [Prop] in a small type *) + +(** The retract is axiomatized using logical equivalence as the + equality on propositions. *) +Variable bool : Prop. +Variable p2b : Prop -> bool. +Variable b2p : bool -> Prop. +Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A. +Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A). + +(** ** Paradox *) + +Theorem paradox : forall B:Prop, B. +Proof. + intros B. + unshelve (refine (mparadox (exist _ bool (fun x => x)) _ _ _ _ + (exist _ B (fun x => x)))). + + intros p. red. red. exact (p2b (El p)). + + cbn. intros b. red. exists (b2p b). exact (fun x => x). + + cbn. intros [A H]. cbn. apply p2p1. + + cbn. intros [A H]. cbn. apply p2p2. +Qed. + +End Paradox. + +End NoRetractFromSmallPropositionToProp. + + +(** * Large universes are not retracts of [Prop]. *) + +(** The existence in the Calculus of Constructions with universes of a + retract from some [Type] universe into [Prop] is inconsistent. *) + +(* Note: Assuming the context [down:Type->Prop; up:Prop->Type; forth: + forall (A:Type), A -> up (down A); back: forall (A:Type), up + (down A) -> A; H: forall (A:Type) (P:A->Type) (a:A), + P (back A (forth A a)) -> P a] is probably enough. *) + +Module NoRetractFromTypeToProp. + +Definition Type2 := Type. +Definition Type1 := Type : Type2. + +Section Paradox. + +(** ** Assumption of a retract from Type into Prop *) + +Variable down : Type1 -> Prop. +Variable up : Prop -> Type1. +Hypothesis up_down : forall (A:Type1), up (down A) = A :> Type1. + +(** ** Paradox *) + +Theorem paradox : forall P:Prop, P. +Proof. + intros P. + Generic.paradox h. + (** Large universe. *) + + exact Type1. + + exact (fun X => X). + + cbn. exact (fun u F => forall x, F x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + exact (fun F => forall A:Prop, F(up A)). + + cbn. exact (fun F f A => f (up A)). + + cbn. + intros F f A. + specialize (f (down A)). + rewrite up_down in f. + exact f. + + exact Prop. + + cbn. exact (fun X => X). + + cbn. exact (fun A P => forall x:A, P x). + + cbn. exact (fun A P => forall x:A, P x). + + cbn. exact P. + + exact h. + + cbn. easy. + + cbn. + intros F f A. + destruct (up_down A). cbn. + reflexivity. + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). +Qed. + +End Paradox. + +End NoRetractFromTypeToProp. + +(** * [A<>Type] *) + +(** No Coq universe can be equal to one of its elements. *) + +Module TypeNeqSmallType. + +Unset Universe Polymorphism. + +Section Paradox. + +(** ** Universe [U] is equal to one of its elements. *) + +Let U := Type. +Variable A:U. +Hypothesis h : U=A. + +(** ** Universe [U] is a retract of [A] *) + +(** The following context is actually sufficient for the paradox to + hold. The hypothesis [h:U=A] is only used to define [down], [up] + and [up_down]. *) + +Let down (X:U) : A := @eq_rect _ _ (fun X => X) X _ h. +Let up (X:A) : U := @eq_rect_r _ _ (fun X => X) X _ h. + +Lemma up_down : forall (X:U), up (down X) = X. +Proof. + unfold up,down. + rewrite <- h. + reflexivity. +Qed. + +Theorem paradox : False. +Proof. + Generic.paradox p. + (** Large universe *) + + exact U. + + exact (fun X=>X). + + cbn. exact (fun X F => forall x:X, F x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + exact (fun F => forall x:A, F (up x)). + + cbn. exact (fun _ f => fun x:A => f (up x)). + + cbn. intros * f X. + specialize (f (down X)). + rewrite up_down in f. + exact f. + (** Small universe *) + + exact A. + (** The interpretation of [A] as a universe is [U]. *) + + cbn. exact up. + + cbn. exact (fun _ F => down (forall x, up (F x))). + + cbn. exact (fun _ F => down (forall x, up (F x))). + + cbn. exact (down False). + + rewrite up_down in p. + exact p. + + cbn. easy. + + cbn. intros ? f X. + destruct (up_down X). cbn. + reflexivity. + + cbn. intros ? ? f. + rewrite up_down. + exact f. + + cbn. intros ? ? f. + rewrite up_down in f. + exact f. + + cbn. intros ? ? f. + rewrite up_down. + exact f. + + cbn. intros ? ? f. + rewrite up_down in f. + exact f. +Qed. + +End Paradox. + +End TypeNeqSmallType. + +(** * [Prop<>Type]. *) + +(** Special case of [TypeNeqSmallType]. *) + +Module PropNeqType. + +Theorem paradox : Prop <> Type. +Proof. + intros h. + unshelve (refine (TypeNeqSmallType.paradox _ _)). + + exact Prop. + + easy. +Qed. + +End PropNeqType. + +(* end show *) diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v new file mode 100644 index 0000000000..86e81529dc --- /dev/null +++ b/theories/Logic/IndefiniteDescription.v @@ -0,0 +1,39 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This file provides a constructive form of indefinite description that + allows building 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 new file mode 100644 index 0000000000..3914f44a2c --- /dev/null +++ b/theories/Logic/JMeq.v @@ -0,0 +1,160 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** John Major's Equality as proposed by Conor McBride + + Reference: + + [McBride] Elimination with a Motive, Proceedings of TYPES 2000, + LNCS 2277, pp 197-216, 2002. + +*) + +Set Implicit Arguments. + +Unset Elimination Schemes. + +Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop := + JMeq_refl : JMeq x x. + +Set Elimination Schemes. + +Arguments JMeq_refl {A x} , [A] x. + +Register JMeq as core.JMeq.type. +Register JMeq_refl as core.JMeq.refl. + +Hint Resolve JMeq_refl : core. + +Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. + +Register JMeq_hom as core.JMeq.hom. + +Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. +Proof. +intros; destruct H; trivial. +Qed. + +Hint Immediate JMeq_sym : core. + +Register JMeq_sym as core.JMeq.sym. + +Lemma JMeq_trans : + forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z. +Proof. +destruct 2; trivial. +Qed. + +Register JMeq_trans as core.JMeq.trans. + +Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. + +Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq x y -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. +Qed. + +Register JMeq_ind as core.JMeq.ind. + +Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set), + P x -> forall y, JMeq x y -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. +Qed. + +Lemma JMeq_rect : forall (A:Type) (x:A) (P:A->Type), + P x -> forall y, JMeq x y -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. +Qed. + +Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq y x -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial. +Qed. + +Lemma JMeq_rec_r : forall (A:Type) (x:A) (P:A -> Set), + P x -> forall y, JMeq y x -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial. +Qed. + +Lemma JMeq_rect_r : forall (A:Type) (x:A) (P:A -> Type), + P x -> forall y, JMeq y x -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial. +Qed. + +Lemma JMeq_congr : + forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y. +Proof. +intros A x B f y H; case JMeq_eq with (1 := H); trivial. +Qed. + +Register JMeq_congr as core.JMeq.congr. + +(** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *) + +Require Import Eqdep. + +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_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. +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 P p q x 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. + +(** However, when the dependencies are equal, [JMeq (P p) x (P q) y] + is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *) + +Lemma JMeq_eq_dep : + forall U (P:U->Type) p q (x:P p) (y:P q), + p = q -> JMeq x y -> eq_dep U P p x q y. +Proof. +intros. +destruct H. +apply JMeq_eq in H0 as ->. +reflexivity. +Qed. + + +(* Compatibility *) +Notation sym_JMeq := JMeq_sym (only parsing). +Notation trans_JMeq := JMeq_trans (only parsing). diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v new file mode 100644 index 0000000000..134bf649dc --- /dev/null +++ b/theories/Logic/ProofIrrelevance.v @@ -0,0 +1,20 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This file axiomatizes proof-irrelevance and derives some consequences *) + +Require Import ProofIrrelevanceFacts. + +Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. + +Module PI. Definition proof_irrelevance := proof_irrelevance. End PI. + +Module ProofIrrelevanceTheory := ProofIrrelevanceTheory(PI). +Export ProofIrrelevanceTheory. diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v new file mode 100644 index 0000000000..10d9dbcdaf --- /dev/null +++ b/theories/Logic/ProofIrrelevanceFacts.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This defines the functor that build consequences of proof-irrelevance *) + +Require Export EqdepFacts. + +Module Type ProofIrrelevance. + + Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. + +End ProofIrrelevance. + +Module ProofIrrelevanceTheory (M:ProofIrrelevance). + + (** Proof-irrelevance implies uniqueness of reflexivity proofs *) + + Module Eq_rect_eq. + Lemma eq_rect_eq : + forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), + x = eq_rect p Q x p h. + Proof. + intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=eq_refl p). + reflexivity. + Qed. + End Eq_rect_eq. + + (** Export the theory of injective dependent elimination *) + + Module EqdepTheory := EqdepTheory(Eq_rect_eq). + Export EqdepTheory. + + Scheme eq_indd := Induction for eq Sort Prop. + + (** We derive the irrelevance of the membership property for subsets *) + + Lemma subset_eq_compat : + forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), + x = y -> exist P x p = exist P y q. + Proof. + intros. + rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + elim H using eq_indd. + reflexivity. + Qed. + + Lemma subsetT_eq_compat : + forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), + x = y -> existT P x p = existT P y q. + Proof. + intros. + rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + elim H using eq_indd. + reflexivity. + Qed. + +End ProofIrrelevanceTheory. diff --git a/theories/Logic/PropExtensionality.v b/theories/Logic/PropExtensionality.v new file mode 100644 index 0000000000..80dd4e850e --- /dev/null +++ b/theories/Logic/PropExtensionality.v @@ -0,0 +1,24 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module states propositional extensionality and draws + consequences of it *) + +Axiom propositional_extensionality : + forall (P Q : Prop), (P <-> Q) -> P = Q. + +Require Import ClassicalFacts. + +Theorem proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. +Proof. + apply ext_prop_dep_proof_irrel_cic. + exact propositional_extensionality. +Qed. + diff --git a/theories/Logic/PropExtensionalityFacts.v b/theories/Logic/PropExtensionalityFacts.v new file mode 100644 index 0000000000..2b30351738 --- /dev/null +++ b/theories/Logic/PropExtensionalityFacts.v @@ -0,0 +1,111 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Some facts and definitions about propositional and predicate extensionality + +We investigate the relations between the following extensionality principles + +- Proposition extensionality +- Predicate extensionality +- Propositional functional extensionality +- Provable-proposition extensionality +- Refutable-proposition extensionality +- Extensional proposition representatives +- Extensional predicate representatives +- Extensional propositional function representatives + +Table of contents + +1. Definitions + +2.1 Predicate extensionality <-> Proposition extensionality + Propositional functional extensionality + +2.2 Propositional extensionality -> Provable propositional extensionality + +2.3 Propositional extensionality -> Refutable propositional extensionality + +*) + +Set Implicit Arguments. + +(**********************************************************************) +(** * Definitions *) + +(** Propositional extensionality *) + +Local Notation PropositionalExtensionality := + (forall A B : Prop, (A <-> B) -> A = B). + +(** Provable-proposition extensionality *) + +Local Notation ProvablePropositionExtensionality := + (forall A:Prop, A -> A = True). + +(** Refutable-proposition extensionality *) + +Local Notation RefutablePropositionExtensionality := + (forall A:Prop, ~A -> A = False). + +(** Predicate extensionality *) + +Local Notation PredicateExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q). + +(** Propositional functional extensionality *) + +Local Notation PropositionalFunctionalExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x = Q x) -> P = Q). + +(**********************************************************************) +(** * Propositional and predicate extensionality *) + +(**********************************************************************) +(** ** Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality *) + +Lemma PredExt_imp_PropExt : PredicateExtensionality -> PropositionalExtensionality. +Proof. + intros Ext A B Equiv. + change A with ((fun _ => A) I). + now rewrite Ext with (P := fun _ : True =>A) (Q := fun _ => B). +Qed. + +Lemma PredExt_imp_PropFunExt : PredicateExtensionality -> PropositionalFunctionalExtensionality. +Proof. + intros Ext A P Q Eq. apply Ext. intros x. now rewrite (Eq x). +Qed. + +Lemma PropExt_and_PropFunExt_imp_PredExt : + PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality. +Proof. + intros Ext FunExt A P Q Equiv. + apply FunExt. intros x. now apply Ext. +Qed. + +Theorem PropExt_and_PropFunExt_iff_PredExt : + PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality. +Proof. + firstorder using PredExt_imp_PropExt, PredExt_imp_PropFunExt, PropExt_and_PropFunExt_imp_PredExt. +Qed. + +(**********************************************************************) +(** ** Propositional extensionality and provable proposition extensionality *) + +Lemma PropExt_imp_ProvPropExt : PropositionalExtensionality -> ProvablePropositionExtensionality. +Proof. + intros Ext A Ha; apply Ext; split; trivial. +Qed. + +(**********************************************************************) +(** ** Propositional extensionality and refutable proposition extensionality *) + +Lemma PropExt_imp_RefutPropExt : PropositionalExtensionality -> RefutablePropositionExtensionality. +Proof. + intros Ext A Ha; apply Ext; split; easy. +Qed. diff --git a/theories/Logic/PropFacts.v b/theories/Logic/PropFacts.v new file mode 100644 index 0000000000..067870356a --- /dev/null +++ b/theories/Logic/PropFacts.v @@ -0,0 +1,52 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Basic facts about Prop as a type *) + +(** An intuitionistic theorem from topos theory [[LambekScott]] + +References: + +[[LambekScott]] Jim Lambek, Phil J. Scott, Introduction to higher +order categorical logic, Cambridge Studies in Advanced Mathematics +(Book 7), 1988. + +*) + +Theorem injection_is_involution_in_Prop + (f : Prop -> Prop) + (inj : forall A B, (f A <-> f B) -> (A <-> B)) + (ext : forall A B, A <-> B -> f A <-> f B) + : forall A, f (f A) <-> A. +Proof. +intros. +enough (f (f (f A)) <-> f A) by (apply inj; assumption). +split; intro H. +- now_show (f A). + enough (f A <-> True) by firstorder. + enough (f (f A) <-> f True) by (apply inj; assumption). + split; intro H'. + + now_show (f True). + enough (f (f (f A)) <-> f True) by firstorder. + apply ext; firstorder. + + now_show (f (f A)). + enough (f (f A) <-> True) by firstorder. + apply inj; firstorder. +- now_show (f (f (f A))). + enough (f A <-> f (f (f A))) by firstorder. + apply ext. + split; intro H'. + + now_show (f (f A)). + enough (f A <-> f (f A)) by firstorder. + apply ext; firstorder. + + now_show A. + enough (f A <-> A) by firstorder. + apply inj; firstorder. +Defined. diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v new file mode 100644 index 0000000000..994f07856d --- /dev/null +++ b/theories/Logic/RelationalChoice.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** 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, + subrelation R' R /\ forall x : A, exists! y : B, R' x y. diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v new file mode 100644 index 0000000000..afa85514eb --- /dev/null +++ b/theories/Logic/SetIsType.v @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * The Set universe seen as a synonym for Type *) + +(** After loading this file, Set becomes just another name for Type. + This allows easily performing 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). diff --git a/theories/Logic/SetoidChoice.v b/theories/Logic/SetoidChoice.v new file mode 100644 index 0000000000..21bf73356f --- /dev/null +++ b/theories/Logic/SetoidChoice.v @@ -0,0 +1,62 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module states the functional form of the axiom of choice over + setoids, commonly called extensional axiom of choice [[Carlström04]], + [[Martin-Löf05]]. This is obtained by a decomposition of the axiom + into the following components: + + - classical logic + - relational axiom of choice + - axiom of unique choice + - a limited form of functional extensionality + + Among other results, it entails: + - proof irrelevance + - choice of a representative in equivalence classes + + [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to + AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + + [[Martin-Löf05] Per Martin-Löf, 100 years of Zermelo’s axiom of + choice: what was the problem with it?, lecture notes for KTH/SU + colloquium, 2005. + +*) + +Require Export ClassicalChoice. (* classical logic, relational choice, unique choice *) +Require Export ExtensionalFunctionRepresentative. + +Require Import ChoiceFacts. +Require Import ClassicalFacts. +Require Import RelationClasses. + +Theorem setoid_choice : + forall A B, + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x x' y, R x x' -> T x y -> T x' y) -> + (forall x, exists y, T x y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). +Proof. + apply setoid_functional_choice_first_characterization. split; [|split]. + - exact choice. + - exact extensional_function_representative. + - exact classic. +Qed. + +Theorem representative_choice : + forall A (R:A->A->Prop), (Equivalence R) -> + exists f : A->A, forall x : A, R x (f x) /\ forall x', R x x' -> f x = f x'. +Proof. + apply setoid_fun_choice_imp_repr_fun_choice. + exact setoid_choice. +Qed. diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v new file mode 100644 index 0000000000..579800b802 --- /dev/null +++ b/theories/Logic/WKL.v @@ -0,0 +1,263 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** A constructive proof of a version of Weak König's Lemma over a + decidable predicate in the formulation of which infinite paths are + treated as predicates. The representation of paths as relations + avoid the need for classical logic and unique choice. The + decidability condition is sufficient to ensure that some required + instance of double negation for disjunction of finite paths holds. + + The idea of the proof comes from the proof of the weak König's + lemma from separation in second-order arithmetic. + + Notice that we do not start from a tree but just from an arbitrary + predicate. Original Weak Konig's Lemma is the instantiation of + the lemma to a tree *) + +Require Import WeakFan List. +Import ListNotations. + +Require Import Omega. + +(** [is_path_from P n l] means that there exists a path of length [n] + from [l] on which [P] does not hold *) + +Inductive is_path_from (P:list bool -> Prop) : nat -> list bool -> Prop := +| here l : ~ P l -> is_path_from P 0 l +| next_left l n : ~ P l -> is_path_from P n (true::l) -> is_path_from P (S n) l +| next_right l n : ~ P l -> is_path_from P n (false::l) -> is_path_from P (S n) l. + +(** We give the characterization of is_path_from in terms of a more common arithmetical formula *) + +Proposition is_path_from_characterization P n l : + is_path_from P n l <-> exists l', length l' = n /\ forall n', n'<=n -> ~ P (rev (firstn n' l') ++ l). +Proof. +intros. split. +- induction 1 as [|* HP _ (l'&Hl'&HPl')|* HP _ (l'&Hl'&HPl')]. + + exists []. split. reflexivity. intros n <-%le_n_0_eq. assumption. + + exists (true :: l'). split. apply eq_S, Hl'. intros [|] H. + * assumption. + * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H. + + exists (false :: l'). split. apply eq_S, Hl'. intros [|] H. + * assumption. + * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H. +- intros (l'& <- &HPl'). induction l' as [|[|]] in l, HPl' |- *. + + constructor. apply (HPl' 0). apply le_0_n. + + eapply next_left. + * apply (HPl' 0), le_0_n. + * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. + + apply next_right. + * apply (HPl' 0), le_0_n. + * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. +Qed. + +(** [infinite_from P l] means that we can find arbitrary long paths + along which [P] does not hold above [l] *) + +Definition infinite_from (P:list bool -> Prop) l := forall n, is_path_from P n l. + +(** [has_infinite_path P] means that there is an infinite path + (represented as a predicate) along which [P] does not hold at all *) + +Definition has_infinite_path (P:list bool -> Prop) := + exists (X:nat -> Prop), forall l, approx X l -> ~ P l. + +(** [inductively_barred_at P n l] means that [P] eventually holds above + [l] after at most [n] steps upwards *) + +Inductive inductively_barred_at (P:list bool -> Prop) : nat -> list bool -> Prop := +| now_at l n : P l -> inductively_barred_at P n l +| propagate_at l n : + inductively_barred_at P n (true::l) -> + inductively_barred_at P n (false::l) -> + inductively_barred_at P (S n) l. + +(** The proof proceeds by building a set [Y] of finite paths + approximating either the smallest unbarred infinite path in [P], if + there is one (taking [true]>[false]), or the path + true::true::... if [P] happens to be inductively_barred *) + +Fixpoint Y P (l:list bool) := + match l with + | [] => True + | b::l => + Y P l /\ + if b then exists n, inductively_barred_at P n (false::l) else infinite_from P (false::l) + end. + +Require Import Compare_dec Le Lt. + +Lemma is_path_from_restrict : forall P n n' l, n <= n' -> + is_path_from P n' l -> is_path_from P n l. +Proof. +intros * Hle H; induction H in n, Hle, H |- * ; intros. +- apply le_n_0_eq in Hle as <-. apply here. assumption. +- destruct n. + + apply here. assumption. + + apply next_left; auto using le_S_n. +- destruct n. + + apply here. assumption. + + apply next_right; auto using le_S_n. +Qed. + +Lemma inductively_barred_at_monotone : forall P l n n', n' <= n -> + inductively_barred_at P n' l -> inductively_barred_at P n l. +Proof. +intros * Hle Hbar. +induction Hbar in n, l, Hle, Hbar |- *. +- apply now_at; auto. +- destruct n; [apply le_Sn_0 in Hle; contradiction|]. + apply le_S_n in Hle. + apply propagate_at; auto. +Qed. + +Definition demorgan_or (P:list bool -> Prop) l l' := ~ (P l /\ P l') -> ~ P l \/ ~ P l'. + +Definition demorgan_inductively_barred_at P := + forall n l, demorgan_or (inductively_barred_at P n) (true::l) (false::l). + +Lemma inductively_barred_at_imp_is_path_from : + forall P, demorgan_inductively_barred_at P -> forall n l, + ~ inductively_barred_at P n l -> is_path_from P n l. +Proof. +intros P Hdemorgan; induction n; intros l H. +- apply here. + intro. apply H. + apply now_at. auto. +- assert (H0:~ (inductively_barred_at P n (true::l) /\ inductively_barred_at P n (false::l))) + by firstorder using inductively_barred_at. + assert (HnP:~ P l) by firstorder using inductively_barred_at. + apply Hdemorgan in H0 as [H0|H0]; apply IHn in H0; auto using is_path_from. +Qed. + +Lemma is_path_from_imp_inductively_barred_at : forall P n l, + is_path_from P n l -> inductively_barred_at P n l -> False. +Proof. +intros P; induction n; intros l H1 H2. +- inversion_clear H1. inversion_clear H2. auto. +- inversion_clear H1. + + inversion_clear H2. + * auto. + * apply IHn with (true::l); auto. + + inversion_clear H2. + * auto. + * apply IHn with (false::l); auto. +Qed. + +Lemma find_left_path : forall P l n, + is_path_from P (S n) l -> inductively_barred_at P n (false :: l) -> is_path_from P n (true :: l). +Proof. +inversion 1; subst; intros. +- auto. +- exfalso. eauto using is_path_from_imp_inductively_barred_at. +Qed. + +Lemma Y_unique : forall P, demorgan_inductively_barred_at P -> + forall l1 l2, length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2. +Proof. +intros * DeMorgan. induction l1, l2. +- trivial. +- discriminate. +- discriminate. +- intros [= H] (HY1,H1) (HY2,H2). + pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1. + subst l1. + f_equal. + destruct a, b; try reflexivity. + + destruct H1 as (n,Hbar). + destruct (is_path_from_imp_inductively_barred_at _ _ _ (H2 n) Hbar). + + destruct H2 as (n,Hbar). + destruct (is_path_from_imp_inductively_barred_at _ _ _ (H1 n) Hbar). +Qed. + +(** [X] is the translation of [Y] as a predicate *) + +Definition X P n := exists l, length l = n /\ Y P (true::l). + +Lemma Y_approx : forall P, demorgan_inductively_barred_at P -> + forall l, approx (X P) l -> Y P l. +Proof. +intros P DeMorgan. induction l. +- trivial. +- intros (H,Hb). split. + + auto. + + unfold X in Hb. + destruct a. + * destruct Hb as (l',(Hl',(HYl',HY))). + rewrite <- (Y_unique P DeMorgan l' l Hl'); auto. + * intro n. apply inductively_barred_at_imp_is_path_from. assumption. + firstorder. +Qed. + +(** Main theorem *) + +Theorem PreWeakKonigsLemma : forall P, + demorgan_inductively_barred_at P -> infinite_from P [] -> has_infinite_path P. +Proof. +intros P DeMorgan Hinf. +exists (X P). intros l Hl. +assert (infinite_from P l). +{ induction l. + - assumption. + - destruct Hl as (Hl,Ha). + intros n. + pose proof (IHl Hl) as IHl'. clear IHl. + apply Y_approx in Hl; [|assumption]. + destruct a. + + destruct Ha as (l'&Hl'&HY'&n'&Hbar). + rewrite (Y_unique _ DeMorgan _ _ Hl' HY' Hl) in Hbar. + destruct (le_lt_dec n n') as [Hle|Hlt]. + * specialize (IHl' (S n')). + apply is_path_from_restrict with n'; [assumption|]. + apply find_left_path; trivial. + * specialize (IHl' (S n)). + apply inductively_barred_at_monotone with (n:=n) in Hbar; [|apply lt_le_weak, Hlt]. + apply find_left_path; trivial. + + apply inductively_barred_at_imp_is_path_from; firstorder. } +specialize (H 0). inversion H. assumption. +Qed. + +Lemma inductively_barred_at_decidable : + forall P, (forall l, P l \/ ~ P l) -> forall n l, inductively_barred_at P n l \/ ~ inductively_barred_at P n l. +Proof. +intros P HP. induction n; intros. +- destruct (HP l). + + left. apply now_at, H. + + right. inversion 1. auto. +- destruct (HP l). + + left. apply now_at, H. + + destruct (IHn (true::l)). + * destruct (IHn (false::l)). + { left. apply propagate_at; assumption. } + { right. inversion_clear 1; auto. } + * right. inversion_clear 1; auto. +Qed. + +Lemma inductively_barred_at_is_path_from_decidable : + forall P, (forall l, P l \/ ~ P l) -> demorgan_inductively_barred_at P. +Proof. +intros P Hdec n l H. +destruct (inductively_barred_at_decidable P Hdec n (true::l)). +- destruct (inductively_barred_at_decidable P Hdec n (false::l)). + + auto. + + auto. +- auto. +Qed. + +(** Main corollary *) + +Corollary WeakKonigsLemma : forall P, (forall l, P l \/ ~ P l) -> + infinite_from P [] -> has_infinite_path P. +Proof. +intros P Hdec Hinf. +apply inductively_barred_at_is_path_from_decidable in Hdec. +apply PreWeakKonigsLemma; assumption. +Qed. diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v new file mode 100644 index 0000000000..c9822f47dc --- /dev/null +++ b/theories/Logic/WeakFan.v @@ -0,0 +1,104 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** A constructive proof of a non-standard version of the weak Fan Theorem + in the formulation of which infinite paths are treated as + predicates. The representation of paths as relations avoid the + need for classical logic and unique choice. The idea of the proof + comes from the proof of the weak König's lemma from separation in + second-order arithmetic [[Simpson99]]. + + [[Simpson99]] Stephen G. Simpson. Subsystems of second order + arithmetic, Cambridge University Press, 1999 *) + +Require Import List. +Import ListNotations. + +(** [inductively_barred P l] means that P eventually holds above l *) + +Inductive inductively_barred P : list bool -> Prop := +| now l : P l -> inductively_barred P l +| propagate l : + inductively_barred P (true::l) -> + inductively_barred P (false::l) -> + inductively_barred P l. + +(** [approx X l] says that [l] is a boolean representation of a prefix of [X] *) + +Fixpoint approx X (l:list bool) := + match l with + | [] => True + | b::l => approx X l /\ (if b then X (length l) else ~ X (length l)) + end. + +(** [barred P] means that for any infinite path represented as a predicate, + the property [P] holds for some prefix of the path *) + +Definition barred P := + forall (X:nat -> Prop), exists l, approx X l /\ P l. + +(** The proof proceeds by building a set [Y] of finite paths + approximating either the smallest unbarred infinite path in [P], if + there is one (taking [true]>[false]), or the path [true::true::...] + if [P] happens to be inductively_barred *) + +Fixpoint Y P (l:list bool) := + match l with + | [] => True + | b::l => + Y P l /\ + if b then inductively_barred P (false::l) else ~ inductively_barred P (false::l) + end. + +Lemma Y_unique : forall P l1 l2, length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2. +Proof. +induction l1, l2. +- trivial. +- discriminate. +- discriminate. +- intros H (HY1,H1) (HY2,H2). + injection H as H. + pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1. + subst l1. + f_equal. + destruct a, b; firstorder. +Qed. + +(** [X] is the translation of [Y] as a predicate *) + +Definition X P n := exists l, length l = n /\ Y P (true::l). + +Lemma Y_approx : forall P l, approx (X P) l -> Y P l. +Proof. +induction l. +- trivial. +- intros (H,Hb). split. + + auto. + + unfold X in Hb. + destruct a. + * destruct Hb as (l',(Hl',(HYl',HY))). + rewrite <- (Y_unique P l' l Hl'); auto. + * firstorder. +Qed. + +Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P []. +Proof. +intros P Hbar. +destruct Hbar with (X P) as (l,(Hd%Y_approx,HP)). +assert (inductively_barred P l) by (apply (now P l), HP). +clear Hbar HP. +induction l as [|a l]. +- assumption. +- destruct Hd as (Hd,HX). + apply (IHl Hd). clear IHl. + destruct a; unfold X in HX; simpl in HX. + + apply propagate; assumption. + + exfalso; destruct (HX H). +Qed. |