diff options
Diffstat (limited to 'theories/Logic')
36 files changed, 1230 insertions, 311 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 1e0bd0fe..c6836a1c 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 1420a000..238ac7df 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1,93 +1,35 @@ -(* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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. - -We investigate the relations between the following choice and -description principles - -- AC_rel = relational form of the (non extensional) axiom of choice - (a "set-theoretic" axiom of choice) -- AC_fun = functional form of the (non extensional) axiom of choice - (a "type-theoretic" axiom of choice) -- DC_fun = functional form of the dependent axiom of choice -- ACw_fun = functional form of the countable axiom of choice -- 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) - -- GAC_rel = guarded relational form of the (non extensional) axiom of choice -- GAC_fun = guarded functional form of the (non extensional) axiom of choice -- GAC! = guarded functional relation reification - -- OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice -- OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice - (called AC* in Bell [[Bell]]) -- OAC! - -- ID_iota = intuitionistic definite description -- ID_epsilon = intuitionistic indefinite description - -- D_iota = (weakly classical) definite description principle -- D_epsilon = (weakly classical) indefinite description principle - -- PI = proof irrelevance -- IGP = independence of general premises - (an unconstrained generalisation of the constructive principle of - independence of premises) -- Drinker = drinker's paradox (small form) - (called Ex in Bell [[Bell]]) - -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 - -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. Equivalence of choices on dependent or non dependent functional types - -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 - -References: - + 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. @@ -108,59 +50,139 @@ Variables A B :Type. Variable P:A->Prop. -Variable R:A->B->Prop. - (** ** Constructive choice and description *) -(** AC_rel *) +(** 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 *) +(** 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)). -(** DC_fun *) +(** 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 *) +(** 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! or Functional Relation Reification (known as Axiom of Unique Choice - in topos theory; also called principle of definite description *) +(** 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)). -(** 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) *) +(** 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) *) +(** 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, @@ -168,7 +190,7 @@ Definition ConstructiveDefiniteDescription_on := (** ** Weakly classical choice and description *) -(** GAC_rel *) +(** GAC_rel = guarded relational form of the (non extensional) axiom of choice *) Definition GuardedRelationalChoice_on := forall P : A->Prop, forall R : A->B->Prop, @@ -176,7 +198,7 @@ Definition GuardedRelationalChoice_on := (exists R' : A->B->Prop, subrelation R' R /\ forall x, P x -> exists! y, R' x y). -(** GAC_fun *) +(** GAC_fun = guarded functional form of the (non extensional) axiom of choice *) Definition GuardedFunctionalChoice_on := forall P : A->Prop, forall R : A->B->Prop, @@ -184,7 +206,7 @@ Definition GuardedFunctionalChoice_on := (forall x : A, P x -> exists y : B, R x y) -> (exists f : A->B, forall x, P x -> R x (f x)). -(** GFR_fun *) +(** GAC! = guarded functional relation reification *) Definition GuardedFunctionalRelReification_on := forall P : A->Prop, forall R : A->B->Prop, @@ -192,27 +214,28 @@ Definition GuardedFunctionalRelReification_on := (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 *) +(** 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 *) +(** 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 *) +(** 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 *) +(** D_iota = (weakly classical) definite description principle *) Definition IotaStatement_on := forall P:A->Prop, @@ -226,14 +249,28 @@ Notation RelationalChoice := (forall A B : Type, RelationalChoice_on A B). Notation FunctionalChoice := (forall A B : Type, FunctionalChoice_on A B). -Definition FunctionalDependentChoice := +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). -Definition FunctionalCountableChoice := +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). @@ -259,18 +296,87 @@ Notation EpsilonStatement := (** 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 @@ -284,7 +390,7 @@ Definition SmallDrinker'sParadox := relational formulation) without known inconsistency with classical logic, though functional relation reification conflicts with classical logic *) -Lemma description_rel_choice_imp_funct_choice : +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. @@ -298,7 +404,7 @@ Proof. apply HR'R; assumption. Qed. -Lemma funct_choice_imp_rel_choice : +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. @@ -311,7 +417,7 @@ Proof. trivial. Qed. -Lemma funct_choice_imp_description : +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. @@ -324,15 +430,15 @@ Proof. exists f; exact H0. Qed. -Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr : +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 (funct_choice_imp_rel_choice H) - | exact (funct_choice_imp_description H) ]. - intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H). + [ 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. (**********************************************************************) @@ -576,10 +682,6 @@ Qed. Require Import Wf_nat. Require Import Decidable. -Definition FunctionalChoice_on_rel (A B:Type) (R:A->B->Prop) := - (forall x:A, exists y : B, R x y) -> - exists f : A -> B, (forall x:A, R x (f x)). - Lemma classical_denumerable_description_imp_fun_choice : forall A:Type, FunctionalRelReification_on A nat -> @@ -601,18 +703,10 @@ Proof. Qed. (**********************************************************************) -(** * Choice on dependent and non dependent function types are equivalent *) +(** * AC_fun = AC_fun_dep = AC_trunc *) (** ** Choice on dependent and non dependent function types are equivalent *) -Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) := - forall R:forall x:A, B x -> Prop, - (forall x:A, exists y : B x, R x y) -> - (exists f : (forall x:A, B x), forall x:A, R x (f x)). - -Notation DependentFunctionalChoice := - (forall A (B:A->Type), DependentFunctionalChoice_on B). - (** The easy part *) Theorem dep_non_dep_functional_choice : @@ -649,15 +743,34 @@ Proof. destruct Heq using eq_indd; trivial. Qed. -(** ** Reification of dependent and non dependent functional relation are equivalent *) +(** ** Functional choice and truncation choice are equivalent *) -Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := - forall (R:forall x:A, B x -> Prop), - (forall x:A, exists! y : B x, R x y) -> - (exists f : (forall x:A, B x), forall x:A, R x (f x)). +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. -Notation DependentFunctionalRelReification := - (forall A (B:A->Type), DependentFunctionalRelReification_on B). +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 *) @@ -862,3 +975,346 @@ Proof. 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 index 14d83501..72f53a46 100644 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 7041ee40..016fa72f 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 9e6d07b2..6867c76e 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 0e91613d..77af9048 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -1,10 +1,12 @@ -(* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index afd64efd..b06384e9 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -1,10 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 @@ -34,8 +36,11 @@ Table of contents: 3 3. Independence of general premises and drinker's paradox -4. Classical logic and principle of unrestricted minimization +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 *) (************************************************************************) @@ -94,12 +99,14 @@ 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. - intros Ext A Ha; apply Ext; split; trivial. + exact PropExt_imp_ProvPropExt. Qed. (************************************************************************) @@ -516,7 +523,7 @@ End Weak_proof_irrelevance_CCI. (** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with - name KC in {[ChagrovZakharyaschev97]] + name KC in [[ChagrovZakharyaschev97]] [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997. @@ -661,6 +668,8 @@ Proof. exists x0; exact Hnot. Qed. +(** * Axioms equivalent to classical logic *) + (** ** Principle of unrestricted minimization *) Require Import Coq.Arith.PeanoNat. @@ -736,3 +745,56 @@ Section Example_of_undecidable_predicate_with_the_minimization_property. 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 index 57f367e5..841bd1be 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -1,10 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index 6665798d..18820d3b 100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index 2c69d4f0..9f5a2993 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) @@ -97,12 +99,12 @@ 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 - | _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) +Ltac classical_right := match goal with +|- ?X \/ _ => (elim (classic X);intro;[left;trivial|right]) end. Ltac classical_left := match goal with -| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left]) +|- _ \/ ?X => (elim (classic X);intro;[right;trivial|left]) end. Require Export EqdepFacts. diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index a304dd24..6e3da423 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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*) diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 8b6054f9..35920d91 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v index 0239222e..5c4f1960 100644 --- a/theories/Logic/Description.v +++ b/theories/Logic/Description.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 23af5afc..3317766c 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -1,16 +1,18 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 + 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]. + Excluded-Middle in Type Theory [[LacasWerner99]]. Three variants of Diaconescu's result in type theory are shown below. @@ -23,23 +25,24 @@ Benjamin Werner) C. A proof that extensional Hilbert epsilon's description operator - entails excluded-middle (taken from Bell [Bell93]) + entails excluded-middle (taken from Bell [[Bell93]]) - See also [Carlström] for a discussion of the connection between the + 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, + [[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 + [[LacasWerner99]] Samuel Lacas, Benjamin Werner, Which Choices imply the excluded middle?, preprint, 1999. - [Bell93] John L. Bell, Hilbert's epsilon operator and classical + [[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 <-> AC_ext, - Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + [[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 *) @@ -54,7 +57,7 @@ Definition PredicateExtensionality := (** From predicate extensionality we get propositional extensionality hence proof-irrelevance *) -Require Import ClassicalFacts. +Import ClassicalFacts. Variable pred_extensionality : PredicateExtensionality. @@ -76,7 +79,7 @@ Qed. (** From proof-irrelevance and relational choice, we get guarded relational choice *) -Require Import ChoiceFacts. +Import ChoiceFacts. Variable rel_choice : RelationalChoice. @@ -89,7 +92,7 @@ Qed. (** The form of choice we need: there is a functional relation which chooses an element in any non empty subset of bool *) -Require Import Bool. +Import Bool. Lemma AC_bool_subset_to_bool : exists R : (bool -> Prop) -> bool -> Prop, @@ -161,6 +164,8 @@ End PredExt_RelChoice_imp_EM. Section ProofIrrel_RelChoice_imp_EqEM. +Import ChoiceFacts. + Variable rel_choice : RelationalChoice. Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y. @@ -263,7 +268,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (**********************************************************************) (** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *) -(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) +(** Proof sketch from Bell [[Bell93]] (with thanks to P. Castéran) *) Local Notation inhabited A := A (only parsing). diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v index ffbb5758..d8c527c6 100644 --- a/theories/Logic/Epsilon.v +++ b/theories/Logic/Epsilon.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 5ef86b8e..35bc4225 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -1,10 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index bd59159b..d938b315 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -1,10 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) @@ -123,7 +125,7 @@ Proof. apply eq_dep_intro. Qed. -Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.2"). (* Compatibility *) +Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.6"). (* Compatibility *) Lemma eq_dep_eq_sigT : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index b7b4dec2..0560d9ed 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/ExtensionalFunctionRepresentative.v b/theories/Logic/ExtensionalFunctionRepresentative.v new file mode 100644 index 00000000..0aac56bb --- /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 index 0e34e7e9..02c8998a 100644 --- a/theories/Logic/ExtensionalityFacts.v +++ b/theories/Logic/ExtensionalityFacts.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/FinFun.v b/theories/Logic/FinFun.v index 06466801..89f5a82a 100644 --- a/theories/Logic/FinFun.v +++ b/theories/Logic/FinFun.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 04d9a670..95e1af2e 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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. @@ -56,6 +58,78 @@ 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) := @@ -68,13 +142,93 @@ Tactic Notation "extensionality" ident(x) := apply forall_extensionality) ; intro x end. -(** Eta expansion follows from extensionality. *) +(** 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. - extensionality x. reflexivity. Qed. diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 841f843c..6c4a8533 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) (************************************************************************) @@ -360,13 +362,12 @@ Module NoRetractToModalProposition. Section Paradox. Variable M : Prop -> Prop. -Hypothesis unit : forall A:Prop, A -> M A. -Hypothesis join : forall A:Prop, M (M A) -> M A. 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. - eauto. + intros A P h x. + eapply incr in h; eauto. Qed. (** ** The universe of modal propositions *) @@ -470,7 +471,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem paradox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => ~~P). + exact bool. + exact p2b. @@ -480,8 +481,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End Paradox. @@ -516,7 +515,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem mparadox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => P). + exact bool. + exact p2b. @@ -526,8 +525,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End MParadox. @@ -562,7 +559,7 @@ End Paradox. End NoRetractFromSmallPropositionToProp. -(** * Large universes are no retracts of [Prop]. *) +(** * 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. *) diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v index 21be5032..86e81529 100644 --- a/theories/Logic/IndefiniteDescription.v +++ b/theories/Logic/IndefiniteDescription.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 2f95856b..9c56b60a 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 @@ -130,7 +132,7 @@ Qed. is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *) Lemma JMeq_eq_dep : - forall U (P:U->Prop) p q (x:P p) (y:P q), + 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. diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v index 305839cd..134bf649 100644 --- a/theories/Logic/ProofIrrelevance.v +++ b/theories/Logic/ProofIrrelevance.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v index 19b3e9e6..10d9dbcd 100644 --- a/theories/Logic/ProofIrrelevanceFacts.v +++ b/theories/Logic/ProofIrrelevanceFacts.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/PropExtensionality.v b/theories/Logic/PropExtensionality.v new file mode 100644 index 00000000..80dd4e85 --- /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 00000000..2b303517 --- /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 index 309539e5..06787035 100644 --- a/theories/Logic/PropFacts.v +++ b/theories/Logic/PropFacts.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index d16835f8..994f0785 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v index 33fce6cc..afa85514 100644 --- a/theories/Logic/SetIsType.v +++ b/theories/Logic/SetIsType.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 *) diff --git a/theories/Logic/SetoidChoice.v b/theories/Logic/SetoidChoice.v new file mode 100644 index 00000000..21bf7335 --- /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 index 95f3e83f..579800b8 100644 --- a/theories/Logic/WKL.v +++ b/theories/Logic/WKL.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v index 4416d38d..c9822f47 100644 --- a/theories/Logic/WeakFan.v +++ b/theories/Logic/WeakFan.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget deleted file mode 100644 index 32359739..00000000 --- a/theories/Logic/vo.itarget +++ /dev/null @@ -1,30 +0,0 @@ -Berardi.vo -ChoiceFacts.vo -ClassicalChoice.vo -ClassicalDescription.vo -ClassicalEpsilon.vo -ClassicalFacts.vo -Classical_Pred_Type.vo -Classical_Prop.vo -ClassicalUniqueChoice.vo -Classical.vo -ConstructiveEpsilon.vo -Decidable.vo -Description.vo -Diaconescu.vo -Epsilon.vo -Eqdep_dec.vo -EqdepFacts.vo -Eqdep.vo -WeakFan.vo -WKL.vo -FunctionalExtensionality.vo -ExtensionalityFacts.vo -Hurkens.vo -IndefiniteDescription.vo -JMeq.vo -ProofIrrelevanceFacts.vo -ProofIrrelevance.vo -RelationalChoice.vo -SetIsType.vo -FinFun.vo
\ No newline at end of file |