diff options
Diffstat (limited to 'theories/Logic')
24 files changed, 2754 insertions, 808 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 0fe8a87d..9eaef07a 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Berardi.v,v 1.5.2.2 2004/08/03 17:42:43 herbelin Exp $ i*) +(*i $Id: Berardi.v 8122 2006-03-04 19:26:40Z herbelin $ i*) (** This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of @@ -92,14 +92,10 @@ End Retracts. Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). Proof. intros A B. -elim (EM (retract (pow A) (pow B))). -intros [f0 g0 e]. -exists f0 g0. -trivial. - -intros hf. -exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F). -intros; elim hf; auto. +destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. + exists f0 g0; trivial. + exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; + destruct hf; auto. Qed. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 87d8a70e..3b066cfc 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,9 +7,240 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v,v 1.7.2.2 2004/08/01 09:29:59 herbelin Exp $ i*) +(*i $Id: ChoiceFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** We show that the functional formulation of the axiom of Choice +(** 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) +- 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^2 = 2nd-order impredicative, 2nd-order functional minimal predicate logic +IPL_2 = 2nd-order impredicative minimal predicate logic +IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) + +Table of contents + +1. Definitions + +2. IPL_2^2 |- AC_rel + AC! = AC_fun + +3. 1. AC_rel + PI -> GAC_rel and PL_2 |- AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel + +4. 2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker + +5. Derivability of choice for decidable relations with well-ordered codomain + +6. Equivalence of choices on dependent or non dependent functional types + +7. Non contradiction of constructive descriptions wrt functional choices + +8. Definite description transports classical logic to the computational world + +References: + +[Bell] John L. Bell, Choice principles in intuitionistic set theory, +unpublished. + +[Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic +Type Theories, Mathematical Logic Quarterly, volume 39, 1993. + +[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in +intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. +*) + +Set Implicit Arguments. + +Notation Local "'inhabited' A" := A (at level 10, only parsing). + +(**********************************************************************) +(** * Definitions *) + +(** Choice, reification and description schemes *) + +Section ChoiceSchemes. + +Variables A B :Type. + +Variables P:A->Prop. + +Variables R:A->B->Prop. + +(** ** Constructive choice and description *) + +(** AC_rel *) + +Definition RelationalChoice_on := + forall R:A->B->Prop, + (forall x : A, exists y : B, R x y) -> + (exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y). + +(** AC_fun *) + +Definition FunctionalChoice_on := + forall R:A->B->Prop, + (forall x : A, exists y : B, R x y) -> + (exists f : A->B, forall x : A, R x (f x)). + +(** AC! or Functional Relation Reification (known as Axiom of Unique Choice + in topos theory; also called principle of definite description *) + +Definition FunctionalRelReification_on := + forall R:A->B->Prop, + (forall x : A, exists! y : B, R x y) -> + (exists f : A->B, forall x : A, R x (f x)). + +(** ID_epsilon (constructive version of indefinite description; + combined with proof-irrelevance, it may be connected to + Carlstrøm's type theory with a constructive indefinite description + operator) *) + +Definition ConstructiveIndefiniteDescription_on := + forall P:A->Prop, + (exists x, P x) -> { x:A | P x }. + +(** ID_iota (constructive version of definite description; combined + with proof-irrelevance, it may be connected to Carlstrøm's and + Stenlund's type theory with a constructive definite description + operator) *) + +Definition ConstructiveDefiniteDescription_on := + forall P:A->Prop, + (exists! x, P x) -> { x:A | P x }. + +(** ** Weakly classical choice and description *) + +(** GAC_rel *) + +Definition GuardedRelationalChoice_on := + forall P : A->Prop, forall R : A->B->Prop, + (forall x : A, P x -> exists y : B, R x y) -> + (exists R' : A->B->Prop, + subrelation R' R /\ forall x, P x -> exists! y, R' x y). + +(** GAC_fun *) + +Definition GuardedFunctionalChoice_on := + forall P : A->Prop, forall R : A->B->Prop, + inhabited B -> + (forall x : A, P x -> exists y : B, R x y) -> + (exists f : A->B, forall x, P x -> R x (f x)). + +(** GFR_fun *) + +Definition GuardedFunctionalRelReification_on := + forall P : A->Prop, forall R : A->B->Prop, + inhabited B -> + (forall x : A, P x -> exists! y : B, R x y) -> + (exists f : A->B, forall x : A, P x -> R x (f x)). + +(** OAC_rel *) + +Definition OmniscientRelationalChoice_on := + forall R : A->B->Prop, + exists R' : A->B->Prop, + subrelation R' R /\ forall x : A, (exists y : B, R x y) -> exists! y, R' x y. + +(** OAC_fun *) + +Definition OmniscientFunctionalChoice_on := + forall R : A->B->Prop, + inhabited B -> + exists f : A->B, forall x : A, (exists y : B, R x y) -> R x (f x). + +(** D_epsilon *) + +Definition ClassicalIndefiniteDescription := + forall P:A->Prop, + A -> { x:A | (exists x, P x) -> P x }. + +(** D_iota *) + +Definition ClassicalDefiniteDescription := + forall P:A->Prop, + A -> { x:A | (exists! x, P x) -> P x }. + +End ChoiceSchemes. + +(** Generalized schemes *) + +Notation RelationalChoice := + (forall A B, RelationalChoice_on A B). +Notation FunctionalChoice := + (forall A B, FunctionalChoice_on A B). +Notation FunctionalChoiceOnInhabitedSet := + (forall A B, inhabited B -> FunctionalChoice_on A B). +Notation FunctionalRelReification := + (forall A B, FunctionalRelReification_on A B). + +Notation GuardedRelationalChoice := + (forall A B, GuardedRelationalChoice_on A B). +Notation GuardedFunctionalChoice := + (forall A B, GuardedFunctionalChoice_on A B). +Notation GuardedFunctionalRelReification := + (forall A B, GuardedFunctionalRelReification_on A B). + +Notation OmniscientRelationalChoice := + (forall A B, OmniscientRelationalChoice_on A B). +Notation OmniscientFunctionalChoice := + (forall A B, OmniscientFunctionalChoice_on A B). + +Notation ConstructiveDefiniteDescription := + (forall A, ConstructiveDefiniteDescription_on A). +Notation ConstructiveIndefiniteDescription := + (forall A, ConstructiveIndefiniteDescription_on A). + +(** Subclassical schemes *) + +Definition ProofIrrelevance := + forall (A:Prop) (a1 a2:A), a1 = a2. + +Definition IndependenceOfGeneralPremises := + forall (A:Type) (P:A -> Prop) (Q:Prop), + inhabited A -> + (Q -> exists x, P x) -> exists x, Q -> P x. + +Definition SmallDrinker'sParadox := + forall (A:Type) (P:A -> Prop), inhabited A -> + exists x, (exists x, P x) -> P x. + +(**********************************************************************) +(** * AC_rel + PDP = AC_fun + + We show that the functional formulation of the axiom of Choice (usual formulation in type theory) is equivalent to its relational formulation (only formulation of set theory) + the axiom of (parametric) definite description (aka axiom of unique choice) *) @@ -17,123 +249,471 @@ relational formulation) without known inconsistency with classical logic, though definite description conflicts with classical logic *) -Definition RelationalChoice := - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). - -Definition FunctionalChoice := - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y) -> - exists f : A -> B, (forall x:A, R x (f x)). +Lemma description_rel_choice_imp_funct_choice : + forall A B : Type, + FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B. +Proof. + intros A B Descr RelCh R H. + destruct (RelCh R H) as (R',(HR'R,H0)). + destruct (Descr R') as (f,Hf). + firstorder. + exists f; intro x. + destruct (H0 x) as (y,(HR'xy,Huniq)). + rewrite <- (Huniq (f x) (Hf x)). + apply HR'R; assumption. +Qed. -Definition ParamDefiniteDescription := - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) -> - exists f : A -> B, (forall x:A, R x (f x)). +Lemma funct_choice_imp_rel_choice : + forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B. +Proof. + intros A B FunCh R H. + destruct (FunCh R H) as (f,H0). + exists (fun x y => f x = y). + split. + intros x y Heq; rewrite <- Heq; trivial. + intro x; exists (f x); split. + reflexivity. + trivial. +Qed. -Lemma description_rel_choice_imp_funct_choice : - ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice. -intros Descr RelCh. -red in |- *; intros A B R H. -destruct (RelCh A B R H) as [R' H0]. -destruct (Descr A B R') as [f H1]. -intro x. -elim (H0 x); intros y [H2 [H3 H4]]; exists y; split; [ exact H3 | exact H4 ]. -exists f; intro x. -elim (H0 x); intros y [H2 [H3 H4]]. -rewrite <- (H4 (f x) (H1 x)). -exact H2. -Qed. - -Lemma funct_choice_imp_rel_choice : FunctionalChoice -> RelationalChoice. -intros FunCh. -red in |- *; intros A B R H. -destruct (FunCh A B R H) as [f H0]. -exists (fun x y => y = f x). -intro x; exists (f x); split; - [ apply H0 - | split; [ reflexivity | intros y H1; symmetry in |- *; exact H1 ] ]. -Qed. - -Lemma funct_choice_imp_description : - FunctionalChoice -> ParamDefiniteDescription. -intros FunCh. -red in |- *; intros A B R H. -destruct (FunCh A B R) as [f H0]. -(* 1 *) -intro x. -elim (H x); intros y [H0 H1]. -exists y; exact H0. -(* 2 *) -exists f; exact H0. +Lemma funct_choice_imp_description : + forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B. +Proof. + intros A B FunCh R H. + destruct (FunCh R) as [f H0]. + (* 1 *) + intro x. + destruct (H x) as (y,(HRxy,_)). + exists y; exact HRxy. + (* 2 *) + exists f; exact H0. Qed. Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr : - FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription. -split. -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). + forall A B, FunctionalChoice_on A B <-> + RelationalChoice_on A B /\ FunctionalRelReification_on A B. +Proof. + intros A B; split. + intro H; split; + [ exact (funct_choice_imp_rel_choice H) + | exact (funct_choice_imp_description H) ]. + intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H). Qed. +(**********************************************************************) +(** * Connection between the guarded, non guarded and descriptive choices and *) + (** We show that the guarded relational formulation of the axiom of Choice comes from the non guarded formulation in presence either of the independance of premises or proof-irrelevance *) -Definition GuardedRelationalChoice := - forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop), - (forall x:A, P x -> exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - P x -> - exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). - -Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. +(**********************************************************************) +(** ** AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *) Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : - RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice. -Proof. -intros rel_choice proof_irrel. -red in |- *; intros A B P R H. -destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0]. -intros [x HPx]. -destruct (H x HPx) as [y HRxy]. -exists y; exact HRxy. -set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). -exists R''; intros x HPx. -destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]]. -exists y. split. - exact HRxy. - split. - red in |- *; exists HPx; exact HR'xy. - intros y' HR''xy'. - apply Huniq. - unfold R'' in HR''xy'. - destruct HR''xy' as [H'Px HR'xy']. - rewrite proof_irrel with (a1 := HPx) (a2 := H'Px). - exact HR'xy'. -Qed. - -Definition IndependenceOfPremises := - forall (A:Type) (P:A -> Prop) (Q:Prop), - (Q -> exists x : _, P x) -> exists x : _, Q -> P x. - -Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice : - RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice. -Proof. -intros RelCh IndPrem. -red in |- *; intros A B P R H. -destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0]. - intro x. apply IndPrem. - apply H. - exists R'. + RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice. +Proof. + intros rel_choice proof_irrel. + red in |- *; intros A B P R H. + destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)). + intros (x,HPx). + destruct (H x HPx) as (y,HRxy). + exists y; exact HRxy. + set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). + exists R''; split. + intros x y (HPx,HR'xy). + change x with (projT1 (existT P x HPx)); apply HR'R; exact HR'xy. intros x HPx. - destruct (H0 x) as [y [H1 H2]]. - exists y. split. - apply (H1 HPx). - exact H2. + destruct (H0 (existT P x HPx)) as (y,(HR'xy,Huniq)). + exists y; split. exists HPx; exact HR'xy. + intros y' (H'Px,HR'xy'). + apply Huniq. + rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'. +Qed. + +Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice : + forall A B, inhabited B -> RelationalChoice_on A B -> + IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B. +Proof. + intros A B Inh AC_rel IndPrem P R H. + destruct (AC_rel (fun x y => P x -> R x y)) as (R',(HR'R,H0)). + intro x. apply IndPrem. exact Inh. intro Hx. + apply H; assumption. + exists (fun x y => P x /\ R' x y). + firstorder. +Qed. + +Lemma guarded_rel_choice_imp_rel_choice : + forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B. +Proof. + intros A B GAC_rel R H. + destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)). + firstorder. + exists R'; firstorder. +Qed. + +(** OAC_rel = GAC_rel *) + +Lemma guarded_iff_omniscient_rel_choice : + GuardedRelationalChoice <-> OmniscientRelationalChoice. +Proof. + split. + intros GAC_rel A B R. + apply (GAC_rel A B (fun x => exists y, R x y) R); auto. + intros OAC_rel A B P R H. + destruct (OAC_rel A B R) as (f,Hf); exists f; firstorder. +Qed. + +(**********************************************************************) +(** ** AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker *) + +(** AC_fun + IGP = GAC_fun *) + +Lemma guarded_fun_choice_imp_indep_of_general_premises : + GuardedFunctionalChoice -> IndependenceOfGeneralPremises. +Proof. + intros GAC_fun A P Q Inh H. + destruct (GAC_fun unit A (fun _ => Q) (fun _ => P) Inh) as (f,Hf). + tauto. + exists (f tt); auto. +Qed. + +Lemma guarded_fun_choice_imp_fun_choice : + GuardedFunctionalChoice -> FunctionalChoiceOnInhabitedSet. +Proof. + intros GAC_fun A B Inh R H. + destruct (GAC_fun A B (fun _ => True) R Inh) as (f,Hf). + firstorder. + exists f; auto. +Qed. + +Lemma fun_choice_and_indep_general_prem_imp_guarded_fun_choice : + FunctionalChoiceOnInhabitedSet -> IndependenceOfGeneralPremises + -> GuardedFunctionalChoice. +Proof. + intros AC_fun IndPrem A B P R Inh H. + apply (AC_fun A B Inh (fun x y => P x -> R x y)). + intro x; apply IndPrem; eauto. +Qed. + +(** AC_fun + Drinker = OAC_fun *) + +(** This was already observed by Bell [Bell] *) + +Lemma omniscient_fun_choice_imp_small_drinker : + OmniscientFunctionalChoice -> SmallDrinker'sParadox. +Proof. + intros OAC_fun A P Inh. + destruct (OAC_fun unit A (fun _ => P)) as (f,Hf). + auto. + exists (f tt); firstorder. +Qed. + +Lemma omniscient_fun_choice_imp_fun_choice : + OmniscientFunctionalChoice -> FunctionalChoiceOnInhabitedSet. +Proof. + intros OAC_fun A B Inh R H. + destruct (OAC_fun A B R Inh) as (f,Hf). + exists f; firstorder. +Qed. + +Lemma fun_choice_and_small_drinker_imp_omniscient_fun_choice : + FunctionalChoiceOnInhabitedSet -> SmallDrinker'sParadox + -> OmniscientFunctionalChoice. +Proof. + intros AC_fun Drinker A B R Inh. + destruct (AC_fun A B Inh (fun x y => (exists y, R x y) -> R x y)) as (f,Hf). + intro x; apply (Drinker B (R x) Inh). + exists f; assumption. +Qed. + +(** OAC_fun = GAC_fun *) + +(** This is derivable from the intuitionistic equivalence between IGP and Drinker +but we give a direct proof *) + +Lemma guarded_iff_omniscient_fun_choice : + GuardedFunctionalChoice <-> OmniscientFunctionalChoice. +Proof. + split. + intros GAC_fun A B R Inh. + apply (GAC_fun A B (fun x => exists y, R x y) R); auto. + intros OAC_fun A B P R Inh H. + destruct (OAC_fun A B R Inh) as (f,Hf). + exists f; firstorder. +Qed. + +(**********************************************************************) +(** * Derivability of choice for decidable relations with well-ordered codomain *) + +(** Countable codomains, such as [nat], can be equipped with a + well-order, which implies the existence of a least element on + inhabited decidable subsets. As a consequence, the relational form of + the axiom of choice is derivable on [nat] for decidable relations. + + We show instead that functional relation reification and the + functional form of the axiom of choice are equivalent on decidable + relation with [nat] as codomain +*) + +Require Import Wf_nat. +Require Import Compare_dec. +Require Import Decidable. +Require Import Arith. + +Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) := + exists! x, P x /\ forall x', P x' -> R x x'. + +Lemma dec_inh_nat_subset_has_unique_least_element : + forall P:nat->Prop, (forall n, P n \/ ~ P n) -> + (exists n, P n) -> has_unique_least_element le P. +Proof. + intros P Pdec (n0,HPn0). + assert + (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') + \/(forall n', P n' -> n<=n')). + induction n. + right. + intros n' Hn'. + apply le_O_n. + destruct IHn. + left; destruct H as (n', (Hlt', HPn')). + exists n'; split. + apply lt_S; assumption. + assumption. + destruct (Pdec n). + left; exists n; split. + apply lt_n_Sn. + split; assumption. + right. + intros n' Hltn'. + destruct (le_lt_eq_dec n n') as [Hltn|Heqn]. + apply H; assumption. + assumption. + destruct H0. + rewrite Heqn; assumption. + destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0]; + repeat split; + assumption || intros n' (HPn',Hminn'); apply le_antisym; auto. +Qed. + +Definition FunctionalChoice_on_rel (A B:Type) (R:A->B->Prop) := + (forall x:A, exists y : B, R x y) -> + 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 -> + forall R:A->nat->Prop, + (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R. +Proof. + intros A Descr. + red in |- *; intros R Rdec H. + set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y'). + destruct (Descr R') as (f,Hf). + intro x. + apply (dec_inh_nat_subset_has_unique_least_element (R x)). + apply Rdec. + apply (H x). + exists f. + intros x. + destruct (Hf x) as (Hfx,_). + assumption. +Qed. + +(**********************************************************************) +(** * Choice on dependent and non dependent function types are equivalent *) + +(** ** Choice on dependent and non dependent function types are equivalent *) + +Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) := + forall R:forall x:A, B x -> Prop, + (forall x:A, exists y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). + +Notation DependentFunctionalChoice := + (forall A (B:A->Type), DependentFunctionalChoice_on B). + +(** The easy part *) + +Theorem dep_non_dep_functional_choice : + DependentFunctionalChoice -> FunctionalChoice. +Proof. + intros AC_depfun A B R H. + destruct (AC_depfun A (fun _ => B) R H) as (f,Hf). + exists f; trivial. +Qed. + +(** Deriving choice on product types requires some computation on + singleton propositional types, so we need computational + conjunction projections and dependent elimination of conjunction + and equality *) + +Scheme and_indd := Induction for and Sort Prop. +Scheme eq_indd := Induction for eq Sort Prop. + +Definition proj1_inf (A B:Prop) (p : A/\B) := + let (a,b) := p in a. + +Theorem non_dep_dep_functional_choice : + FunctionalChoice -> DependentFunctionalChoice. +Proof. + intros AC_fun A B R H. + pose (B' := { x:A & B x }). + pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). + destruct (AC_fun A B' R') as (f,Hf). + intros x. destruct (H x) as (y,Hy). + exists (existT (fun x => B x) x y). split; trivial. + exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))). + intro x; destruct (Hf x) as (Heq,HR) using and_indd. + destruct (f x); simpl in *. + destruct Heq using eq_indd; trivial. Qed. + +(** ** Reification of dependent and non dependent functional relation are equivalent *) + +Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := + forall (R:forall x:A, B x -> Prop), + (forall x:A, exists! y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). + +Notation DependentFunctionalRelReification := + (forall A (B:A->Type), DependentFunctionalRelReification_on B). + +(** The easy part *) + +Theorem dep_non_dep_functional_rel_reification : + DependentFunctionalRelReification -> FunctionalRelReification. +Proof. + intros DepFunReify A B R H. + destruct (DepFunReify A (fun _ => B) R H) as (f,Hf). + exists f; trivial. +Qed. + +(** Deriving choice on product types requires some computation on + singleton propositional types, so we need computational + conjunction projections and dependent elimination of conjunction + and equality *) + +Theorem non_dep_dep_functional_rel_reification : + FunctionalRelReification -> DependentFunctionalRelReification. +Proof. + intros AC_fun A B R H. + pose (B' := { x:A & B x }). + pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). + destruct (AC_fun A B' R') as (f,Hf). + intros x. destruct (H x) as (y,(Hy,Huni)). + exists (existT (fun x => B x) x y). repeat split; trivial. + intros (x',y') (Heqx',Hy'). + simpl in *. + destruct Heqx'. + rewrite (Huni y'); trivial. + exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))). + intro x; destruct (Hf x) as (Heq,HR) using and_indd. + destruct (f x); simpl in *. + destruct Heq using eq_indd; trivial. +Qed. + +(**********************************************************************) +(** * Non contradiction of constructive descriptions wrt functional axioms of choice *) + +(** ** Non contradiction of indefinite description *) + +Lemma relative_non_contradiction_of_indefinite_desc : + (ConstructiveIndefiniteDescription -> False) + -> (FunctionalChoice -> False). +Proof. + intros H AC_fun. + assert (AC_depfun := non_dep_dep_functional_choice AC_fun). + pose (A0 := { A:Type & { P:A->Prop & exists x, P x }}). + pose (B0 := fun x:A0 => projT1 x). + pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y). + pose (H0 := fun x:A0 => projT2 (projT2 x)). + destruct (AC_depfun A0 B0 R0 H0) as (f, Hf). + apply H. + intros A P H'. + exists (f (existT (fun _ => sigT _) A + (existT (fun P => exists x, P x) P H'))). + pose (Hf' := + Hf (existT (fun _ => sigT _) A + (existT (fun P => exists x, P x) P H'))). + assumption. +Qed. + +Lemma constructive_indefinite_descr_fun_choice : + ConstructiveIndefiniteDescription -> FunctionalChoice. +Proof. + intros IndefDescr A B R H. + exists (fun x => proj1_sig (IndefDescr B (R x) (H x))). + intro x. + apply (proj2_sig (IndefDescr B (R x) (H x))). +Qed. + +(** ** Non contradiction of definite description *) + +Lemma relative_non_contradiction_of_definite_descr : + (ConstructiveDefiniteDescription -> False) + -> (FunctionalRelReification -> False). +Proof. + intros H FunReify. + assert (DepFunReify := non_dep_dep_functional_rel_reification FunReify). + pose (A0 := { A:Type & { P:A->Prop & exists! x, P x }}). + pose (B0 := fun x:A0 => projT1 x). + pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y). + pose (H0 := fun x:A0 => projT2 (projT2 x)). + destruct (DepFunReify A0 B0 R0 H0) as (f, Hf). + apply H. + intros A P H'. + exists (f (existT (fun _ => sigT _) A + (existT (fun P => exists! x, P x) P H'))). + pose (Hf' := + Hf (existT (fun _ => sigT _) A + (existT (fun P => exists! x, P x) P H'))). + assumption. +Qed. + +Lemma constructive_definite_descr_fun_reification : + ConstructiveDefiniteDescription -> FunctionalRelReification. +Proof. + intros DefDescr A B R H. + exists (fun x => proj1_sig (DefDescr B (R x) (H x))). + intro x. + apply (proj2_sig (DefDescr B (R x) (H x))). +Qed. + +(**********************************************************************) +(** * Excluded-middle + definite description => computational excluded-middle *) + +(** The idea for the following proof comes from [ChicliPottierSimpson02] *) + +(** Classical logic and axiom of unique choice (i.e. functional + relation reification), as shown in [ChicliPottierSimpson02], + implies the double-negation of excluded-middle in [Set] (which is + incompatible with the impredicativity of [Set]). + + We adapt the proof to show that constructive definite description + transports excluded-middle from [Prop] to [Set]. + + [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos + Simpson, Mathematical Quotients and Quotient Types in Coq, + Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, + Springer Verlag. *) + +Require Import Setoid. + +Theorem constructive_definite_descr_excluded_middle : + ConstructiveDefiniteDescription -> + (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}). +Proof. + intros Descr EM P. + pose (select := fun b:bool => if b then P else ~P). + assert { b:bool | select b } as ([|],HP). + apply Descr. + rewrite <- unique_existence; split. + destruct (EM P). + exists true; trivial. + exists false; trivial. + intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction. + left; trivial. + right; trivial. +Qed. diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 044cee17..523c9245 100755..100644 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Classical.v 8642 2006-03-17 10:09:02Z notin $ i*) (** Classical Logic *) Require Export Classical_Prop. -Require Export Classical_Pred_Type.
\ No newline at end of file +Require Export Classical_Pred_Type. + diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 51f758e2..bb8186ae 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -6,27 +6,40 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalChoice.v,v 1.4.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: ClassicalChoice.v 8892 2006-06-04 17:59:53Z herbelin $ i*) -(** This file provides classical logic and functional choice *) +(** This file provides classical logic, and functional choice *) -(** This file extends ClassicalDescription.v with the axiom of choice. - As ClassicalDescription.v, it implies the double-negation of - excluded-middle in Set and implies a strongly classical - world. Especially it conflicts with impredicativity of Set, knowing - that true<>false in Set. -*) +(** This file extends ClassicalUniqueChoice.v with the axiom of choice. + As ClassicalUniqueChoice.v, it implies the double-negation of + excluded-middle in [Set] and leads to a classical world populated + with non computable functions. Especially it conflicts with the + impredicativity of [Set], knowing that [true<>false] in [Set]. *) -Require Export ClassicalDescription. +Require Export ClassicalUniqueChoice. Require Export RelationalChoice. Require Import ChoiceFacts. +Set Implicit Arguments. + +Definition subset (U:Type) (P Q:U->Prop) : Prop := forall x, P x -> Q x. + +Theorem singleton_choice : + forall (A : Type) (P : A->Prop), + (exists x : A, P x) -> exists P' : A->Prop, subset P' P /\ exists! x, P' x. +Proof. +intros A P H. +destruct (relational_choice unit A (fun _ => P) (fun _ => H)) as (R',(Hsub,HR')). +exists (R' tt); firstorder. +Qed. + Theorem choice : - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y) -> - exists f : A -> B, (forall x:A, R x (f x)). + forall (A B : Type) (R : A->B->Prop), + (forall x : A, exists y : B, R x y) -> + exists f : A->B, (forall x : A, R x (f x)). Proof. +intros A B. apply description_rel_choice_imp_funct_choice. -exact description. -exact relational_choice. -Qed.
\ No newline at end of file +exact (unique_choice A B). +exact (relational_choice A B). +Qed. diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 6602cd73..1f1c34bf 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -6,73 +6,83 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalDescription.v,v 1.7.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: ClassicalDescription.v 9514 2007-01-22 14:58:50Z herbelin $ i*) (** This file provides classical logic and definite description *) -(** Classical logic and definite description, as shown in [1], - implies the double-negation of excluded-middle in Set, hence it - implies a strongly classical world. Especially it conflicts with - impredicativity of Set, knowing that true<>false in Set. +(** Classical definite description operator (i.e. iota) implies + excluded-middle in [Set] and leads to a classical world populated + with non computable functions. It conflicts with the + impredicativity of [Set] *) - [1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical - Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, - Lecture Notes in Computer Science 2646, Springer Verlag. -*) +Set Implicit Arguments. Require Export Classical. +Require Import ChoiceFacts. -Axiom - dependent_description : - forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), - (forall x:A, - exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) -> - exists f : forall x:A, B x, (forall x:A, R x (f x)). +Notation Local "'inhabited' A" := A (at level 200, only parsing). -(** Principle of definite descriptions (aka axiom of unique choice) *) +Axiom constructive_definite_description : + forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }. -Theorem description : - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) -> - exists f : A -> B, (forall x:A, R x (f x)). +(** The idea for the following proof comes from [ChicliPottierSimpson02] *) + +Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}. Proof. -intros A B. -apply (dependent_description A (fun _ => B)). +apply + (constructive_definite_descr_excluded_middle + constructive_definite_description classic). Qed. -(** The followig proof comes from [1] *) +Theorem classical_definite_description : + forall (A : Type) (P : A->Prop), inhabited A -> + { x : A | (exists! x : A, P x) -> P x }. +Proof. +intros A P i. +destruct (excluded_middle_informative (exists! x, P x)) as [Hex|HnonP]. + apply constructive_definite_description with (P:= fun x => (exists! x : A, P x) -> P x). + destruct Hex as (x,(Hx,Huni)). + exists x; split. + intros _; exact Hx. + firstorder. +exists i; tauto. +Qed. + +(** Church's iota operator *) + +Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A + := proj1_sig (classical_definite_description P i). + +Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : + (exists! x:A, P x) -> P (iota i P) + := proj2_sig (classical_definite_description P i). -Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False. +(** Axiom of unique "choice" (functional reification of functional relations) *) +Theorem dependent_unique_choice : + forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), + (forall x:A, exists! y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). Proof. -intro HnotEM. -set (R := fun A b => A /\ true = b \/ ~ A /\ false = b). -assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))). -apply description. -intro A. -destruct (classic A) as [Ha| Hnota]. - exists true; split. - left; split; [ assumption | reflexivity ]. - intros y [[_ Hy]| [Hna _]]. - assumption. - contradiction. - exists false; split. - right; split; [ assumption | reflexivity ]. - intros y [[Ha _]| [_ Hy]]. - contradiction. - assumption. -destruct H as [f Hf]. -apply HnotEM. -intro P. -assert (HfP := Hf P). -(* Elimination from Hf to Set is not allowed but from f to Set yes ! *) -destruct (f P). - left. - destruct HfP as [[Ha _]| [_ Hfalse]]. - assumption. - discriminate. - right. - destruct HfP as [[_ Hfalse]| [Hna _]]. - discriminate. - assumption. +intros A B R H. +assert (Hexuni:forall x, exists! y, R x y). + intro x. apply H. +exists (fun x => proj1_sig (constructive_definite_description (R x) (Hexuni x))). +intro x. +apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))). Qed. - + +Theorem unique_choice : + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists! y : B, R x y) -> + (exists f : A -> B, forall x:A, R x (f x)). +Proof. +intros A B. +apply dependent_unique_choice with (B:=fun _:A => B). +Qed. + +(** Compatibility lemmas *) + +Unset Implicit Arguments. + +Definition dependent_description := dependent_unique_choice. +Definition description := unique_choice. diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v new file mode 100644 index 00000000..6d0a9c77 --- /dev/null +++ b/theories/Logic/ClassicalEpsilon.v @@ -0,0 +1,102 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ClassicalEpsilon.v 9245 2006-10-17 12:53:34Z notin $ i*) + +(** This file provides classical logic and indefinite description + (Hilbert's epsilon operator) *) + +(** Classical epsilon's operator (i.e. indefinite description) implies + excluded-middle in [Set] and leads to a classical world populated + with non computable functions. It conflicts with the + impredicativity of [Set] *) + +Require Export Classical. +Require Import ChoiceFacts. + +Set Implicit Arguments. + +Axiom constructive_indefinite_description : + forall (A : Type) (P : A->Prop), + (exists x, P x) -> { x : A | P x }. + +Lemma constructive_definite_description : + forall (A : Type) (P : A->Prop), + (exists! x, P x) -> { x : A | P x }. +Proof. + intros; apply constructive_indefinite_description; firstorder. +Qed. + +Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}. +Proof. + apply + (constructive_definite_descr_excluded_middle + constructive_definite_description classic). +Qed. + +Theorem classical_indefinite_description : + forall (A : Type) (P : A->Prop), inhabited A -> + { x : A | (exists x, P x) -> P x }. +Proof. + intros A P i. + destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP]. + apply constructive_indefinite_description + with (P:= fun x => (exists x, P x) -> P x). + destruct Hex as (x,Hx). + exists x; intros _; exact Hx. + assert {x : A | True} as (a,_). + apply constructive_indefinite_description with (P := fun _ : A => True). + destruct i as (a); firstorder. + firstorder. +Defined. + +(** Hilbert's epsilon operator *) + +Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A + := proj1_sig (classical_indefinite_description P i). + +Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : + (exists x, P x) -> P (epsilon i P) + := proj2_sig (classical_indefinite_description P i). + +(** Open question: is classical_indefinite_description constructively + provable from [relational_choice] and + [constructive_definite_description] (at least, using the fact that + [functional_choice] is provable from [relational_choice] and + [unique_choice], we know that the double negation of + [classical_indefinite_description] is provable (see + [relative_non_contradiction_of_indefinite_desc]). *) + +(** A proof that if [P] is inhabited, [epsilon a P] does not depend on + the actual proof that the domain of [P] is inhabited + (proof idea kindly provided by Pierre Castéran) *) + +Lemma epsilon_inh_irrelevance : + forall (A:Type) (i j : inhabited A) (P:A->Prop), + (exists x, P x) -> epsilon i P = epsilon j P. +Proof. + intros. + unfold epsilon, classical_indefinite_description. + destruct (excluded_middle_informative (exists x : A, P x)) as [|[]]; trivial. +Qed. + +Opaque epsilon. + +(** *** Weaker lemmas (compatibility lemmas) *) + +Theorem choice : + forall (A B : Type) (R : A->B->Prop), + (forall x : A, exists y : B, R x y) -> + (exists f : A->B, forall x : A, R x (f x)). +Proof. + intros A B R H. + exists (fun x => proj1_sig (constructive_indefinite_description _ (H x))). + intro x. + apply (proj2_sig (constructive_indefinite_description _ (H x))). +Qed. + diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index cb14fb0e..dd911db6 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,58 +7,96 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalFacts.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: ClassicalFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** Some facts and definitions about classical logic *) +(** Some facts and definitions about classical logic -(** [prop_degeneracy] (also referred as propositional completeness) *) -(* asserts (up to consistency) that there are only two distinct formulas *) +Table of contents: + +1. Propositional degeneracy = excluded-middle + propositional extensionality + +2. Classical logic and proof-irrelevance + +2.1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint + +2.2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance + +2.3. CIC |- prop. ext. -> proof-irrelevance + +2.4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance + +2.5. CIC |- excluded-middle -> proof-irrelevance + +3. Weak classical axioms + +3.1. Weak excluded middle + +3.2. Gödel-Dummet axiom and right distributivity of implication over + disjunction + +3 3. Independence of general premises and drinker's paradox + +*) + +(************************************************************************) +(** * Prop degeneracy = excluded-middle + prop extensionality *) +(** + i.e. [(forall A, A=True \/ A=False) + <-> + (forall A, A\/~A) /\ (forall A B, (A<->B) -> A=B)] +*) + +(** [prop_degeneracy] (also referred to as propositional completeness) + asserts (up to consistency) that there are only two distinct formulas *) Definition prop_degeneracy := forall A:Prop, A = True \/ A = False. -(** [prop_extensionality] asserts equivalent formulas are equal *) +(** [prop_extensionality] asserts that equivalent formulas are equal *) Definition prop_extensionality := forall A B:Prop, (A <-> B) -> A = B. -(** [excluded_middle] asserts we can reason by case on the truth *) -(* or falsity of any formula *) +(** [excluded_middle] asserts that we can reason by case on the truth + or falsity of any formula *) Definition excluded_middle := forall A:Prop, A \/ ~ A. -(** [proof_irrelevance] asserts equality of all proofs of a given formula *) -Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. - (** We show [prop_degeneracy <-> (prop_extensionality /\ excluded_middle)] *) Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality. Proof. -intros H A B [Hab Hba]. -destruct (H A); destruct (H B). - rewrite H1; exact H0. - absurd B. - rewrite H1; exact (fun H => H). - apply Hab; rewrite H0; exact I. - absurd A. - rewrite H0; exact (fun H => H). - apply Hba; rewrite H1; exact I. - rewrite H1; exact H0. + intros H A B [Hab Hba]. + destruct (H A); destruct (H B). + rewrite H1; exact H0. + absurd B. + rewrite H1; exact (fun H => H). + apply Hab; rewrite H0; exact I. + absurd A. + rewrite H0; exact (fun H => H). + apply Hba; rewrite H1; exact I. + rewrite H1; exact H0. Qed. Lemma prop_degen_em : prop_degeneracy -> excluded_middle. Proof. -intros H A. -destruct (H A). - left; rewrite H0; exact I. - right; rewrite H0; exact (fun x => x). + intros H A. + destruct (H A). + left; rewrite H0; exact I. + right; rewrite H0; exact (fun x => x). Qed. Lemma prop_ext_em_degen : - prop_extensionality -> excluded_middle -> prop_degeneracy. + prop_extensionality -> excluded_middle -> prop_degeneracy. Proof. -intros Ext EM A. -destruct (EM A). - left; apply (Ext A True); split; - [ exact (fun _ => I) | exact (fun _ => H) ]. - right; apply (Ext A False); split; [ exact H | apply False_ind ]. + intros Ext EM A. + destruct (EM A). + left; apply (Ext A True); split; + [ exact (fun _ => I) | exact (fun _ => H) ]. + right; apply (Ext A False); split; [ exact H | apply False_ind ]. Qed. +(************************************************************************) +(** * Classical logic and proof-irrelevance *) + +(************************************************************************) +(** ** CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *) + (** We successively show that: [prop_extensionality] @@ -71,88 +110,95 @@ Qed. Definition inhabited (A:Prop) := A. Lemma prop_ext_A_eq_A_imp_A : - prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. + prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. Proof. -intros Ext A a. -apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ]. + intros Ext A a. + apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ]. Qed. Record retract (A B:Prop) : Prop := {f1 : A -> B; f2 : B -> A; f1_o_f2 : forall x:B, f1 (f2 x) = x}. Lemma prop_ext_retract_A_A_imp_A : - prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A). + prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A). Proof. -intros Ext A a. -rewrite (prop_ext_A_eq_A_imp_A Ext A a). -exists (fun x:A => x) (fun x:A => x). -reflexivity. + intros Ext A a. + rewrite (prop_ext_A_eq_A_imp_A Ext A a). + exists (fun x:A => x) (fun x:A => x). + reflexivity. Qed. Record has_fixpoint (A:Prop) : Prop := {F : (A -> A) -> A; Fix : forall f:A -> A, F f = f (F f)}. Lemma ext_prop_fixpoint : - prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A. + prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A. Proof. -intros Ext A a. -case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2. -exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))). -intro f. -pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *. -rewrite (g1_o_g2 (fun x:A => f (g1 x x))). -reflexivity. + intros Ext A a. + case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2. + exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))). + intro f. + pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *. + rewrite (g1_o_g2 (fun x:A => f (g1 x x))). + reflexivity. Qed. -(** Assume we have booleans with the property that there is at most 2 +(************************************************************************) +(** ** CC |- prop_ext /\ dep elim on bool -> proof-irrelevance *) + +(** [proof_irrelevance] asserts equality of all proofs of a given formula *) +Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. + +(** Assume that we have booleans with the property that there is at most 2 booleans (which is equivalent to dependent case analysis). Consider the fixpoint of the negation function: it is either true or false by dependent case analysis, but also the opposite by fixpoint. Hence proof-irrelevance. - We then map bool proof-irrelevance to all propositions. + We then map equality of boolean proofs to proof irrelevance in all + propositions. *) Section Proof_irrelevance_gen. -Variable bool : Prop. -Variable true : bool. -Variable false : bool. -Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C. -Hypothesis - bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true. -Hypothesis - bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false. -Let bool_dep_induction := + Variable bool : Prop. + Variable true : bool. + Variable false : bool. + Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C. + Hypothesis + bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true. + Hypothesis + bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false. + Let bool_dep_induction := forall P:bool -> Prop, P true -> P false -> forall b:bool, P b. -Lemma aux : prop_extensionality -> bool_dep_induction -> true = false. -Proof. -intros Ext Ind. -case (ext_prop_fixpoint Ext bool true); intros G Gfix. -set (neg := fun b:bool => bool_elim bool false true b). -generalize (refl_equal (G neg)). -pattern (G neg) at 1 in |- *. -apply Ind with (b := G neg); intro Heq. -rewrite (bool_elim_redl bool false true). -change (true = neg true) in |- *; rewrite Heq; apply Gfix. -rewrite (bool_elim_redr bool false true). -change (neg false = false) in |- *; rewrite Heq; symmetry in |- *; - apply Gfix. -Qed. - -Lemma ext_prop_dep_proof_irrel_gen : - prop_extensionality -> bool_dep_induction -> proof_irrelevance. -Proof. -intros Ext Ind A a1 a2. -set (f := fun b:bool => bool_elim A a1 a2 b). -rewrite (bool_elim_redl A a1 a2). -change (f true = a2) in |- *. -rewrite (bool_elim_redr A a1 a2). -change (f true = f false) in |- *. -rewrite (aux Ext Ind). -reflexivity. -Qed. + Lemma aux : prop_extensionality -> bool_dep_induction -> true = false. + Proof. + intros Ext Ind. + case (ext_prop_fixpoint Ext bool true); intros G Gfix. + set (neg := fun b:bool => bool_elim bool false true b). + generalize (refl_equal (G neg)). + pattern (G neg) at 1 in |- *. + apply Ind with (b := G neg); intro Heq. + rewrite (bool_elim_redl bool false true). + change (true = neg true) in |- *; rewrite Heq; apply Gfix. + rewrite (bool_elim_redr bool false true). + change (neg false = false) in |- *; rewrite Heq; symmetry in |- *; + apply Gfix. + Qed. + + Lemma ext_prop_dep_proof_irrel_gen : + prop_extensionality -> bool_dep_induction -> proof_irrelevance. + Proof. + intros Ext Ind A a1 a2. + set (f := fun b:bool => bool_elim A a1 a2 b). + rewrite (bool_elim_redl A a1 a2). + change (f true = a2) in |- *. + rewrite (bool_elim_redr A a1 a2). + change (f true = f false) in |- *. + rewrite (aux Ext Ind). + reflexivity. + Qed. End Proof_irrelevance_gen. @@ -161,27 +207,31 @@ End Proof_irrelevance_gen. most 2 elements. *) -Section Proof_irrelevance_CC. +Section Proof_irrelevance_Prop_Ext_CC. + + Definition BoolP := forall C:Prop, C -> C -> C. + Definition TrueP : BoolP := fun C c1 c2 => c1. + Definition FalseP : BoolP := fun C c1 c2 => c2. + Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2. + Definition BoolP_elim_redl (C:Prop) (c1 c2:C) : + c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1. + Definition BoolP_elim_redr (C:Prop) (c1 c2:C) : + c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2. + + Definition BoolP_dep_induction := + forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b. + + Lemma ext_prop_dep_proof_irrel_cc : + prop_extensionality -> BoolP_dep_induction -> proof_irrelevance. + Proof. + exact (ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl + BoolP_elim_redr). + Qed. + +End Proof_irrelevance_Prop_Ext_CC. -Definition BoolP := forall C:Prop, C -> C -> C. -Definition TrueP : BoolP := fun C c1 c2 => c1. -Definition FalseP : BoolP := fun C c1 c2 => c2. -Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2. -Definition BoolP_elim_redl (C:Prop) (c1 c2:C) : - c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1. -Definition BoolP_elim_redr (C:Prop) (c1 c2:C) : - c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2. - -Definition BoolP_dep_induction := - forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b. - -Lemma ext_prop_dep_proof_irrel_cc : - prop_extensionality -> BoolP_dep_induction -> proof_irrelevance. -Proof - ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl - BoolP_elim_redr. - -End Proof_irrelevance_CC. +(************************************************************************) +(** ** CIC |- prop. ext. -> proof-irrelevance *) (** In the Calculus of Inductive Constructions, inductively defined booleans enjoy dependent case analysis, hence directly proof-irrelevance from @@ -189,21 +239,22 @@ End Proof_irrelevance_CC. *) Section Proof_irrelevance_CIC. - -Inductive boolP : Prop := - | trueP : boolP - | falseP : boolP. -Definition boolP_elim_redl (C:Prop) (c1 c2:C) : - c1 = boolP_ind C c1 c2 trueP := refl_equal c1. -Definition boolP_elim_redr (C:Prop) (c1 c2:C) : - c2 = boolP_ind C c1 c2 falseP := refl_equal c2. -Scheme boolP_indd := Induction for boolP Sort Prop. - -Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. -Proof - fun pe => - ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl - boolP_elim_redr pe boolP_indd. + + Inductive boolP : Prop := + | trueP : boolP + | falseP : boolP. + Definition boolP_elim_redl (C:Prop) (c1 c2:C) : + c1 = boolP_ind C c1 c2 trueP := refl_equal c1. + Definition boolP_elim_redr (C:Prop) (c1 c2:C) : + c2 = boolP_ind C c1 c2 falseP := refl_equal c2. + Scheme boolP_indd := Induction for boolP Sort Prop. + + Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. + Proof. + exact (fun pe => + ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl + boolP_elim_redr pe boolP_indd). + Qed. End Proof_irrelevance_CIC. @@ -211,9 +262,288 @@ End Proof_irrelevance_CIC. (i.e. propositional extensionality + excluded middle) without dependent case analysis ? - Conjecture: it seems possible to build a model of CC interpreting - all non-empty types by the set of all lambda-terms. Such a model would - satisfy propositional degeneracy without satisfying proof-irrelevance - (nor dependent case analysis). This would imply that the previous - results cannot be refined. + Berardi [[Berardi90]] built a model of CC interpreting inhabited + types by the set of all untyped lambda-terms. This model satisfies + propositional degeneracy without satisfying proof-irrelevance (nor + dependent case analysis). This implies that the previous results + cannot be refined. + + [[Berardi90]] Stefano Berardi, "Type dependence and constructive + mathematics", Ph. D. thesis, Dipartimento Matematica, Università di + Torino, 1990. +*) + +(************************************************************************) +(** ** CC |- excluded-middle + dep elim on bool -> proof-irrelevance *) + +(** This is a proof in the pure Calculus of Construction that + classical logic in [Prop] + dependent elimination of disjunction entails + proof-irrelevance. + + Reference: + + [[Coquand90]] T. Coquand, "Metamathematical Investigations of a + Calculus of Constructions", Proceedings of Logic in Computer Science + (LICS'90), 1990. + + Proof skeleton: classical logic + dependent elimination of + disjunction + discrimination of proofs implies the existence of a + retract from [Prop] into [bool], hence inconsistency by encoding any + paradox of system U- (e.g. Hurkens' paradox). +*) + +Require Import Hurkens. + +Section Proof_irrelevance_EM_CC. + + Variable or : Prop -> Prop -> Prop. + Variable or_introl : forall A B:Prop, A -> or A B. + Variable or_intror : forall A B:Prop, B -> or A B. + Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C. + Hypothesis + or_elim_redl : + forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A), + f a = or_elim A B C f g (or_introl A B a). + Hypothesis + or_elim_redr : + forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B), + g b = or_elim A B C f g (or_intror A B b). + Hypothesis + or_dep_elim : + forall (A B:Prop) (P:or A B -> Prop), + (forall a:A, P (or_introl A B a)) -> + (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b. + + Hypothesis em : forall A:Prop, or A (~ A). + Variable B : Prop. + Variables b1 b2 : B. + + (** [p2b] and [b2p] form a retract if [~b1=b2] *) + + Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A). + Definition b2p b := b1 = b. + + Lemma p2p1 : forall A:Prop, A -> b2p (p2b A). + Proof. + unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); + unfold b2p in |- *; intros. + apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)). + destruct (b H). + Qed. + + Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A. + Proof. + intro not_eq_b1_b2. + unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); + unfold b2p in |- *; intros. + assumption. + destruct not_eq_b1_b2. + rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H. + assumption. + Qed. + + (** Using excluded-middle a second time, we get proof-irrelevance *) + + Theorem proof_irrelevance_cc : b1 = b2. + Proof. + refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H. + trivial. + apply (paradox B p2b b2p (p2p2 H) p2p1). + Qed. + +End Proof_irrelevance_EM_CC. + +(** Remark: Hurkens' paradox still holds with a retract from the + _negative_ fragment of [Prop] into [bool], hence weak classical + logic, i.e. [forall A, ~A\/~~A], is enough for deriving + proof-irrelevance. +*) + +(************************************************************************) +(** ** CIC |- excluded-middle -> proof-irrelevance *) + +(** + Since, dependent elimination is derivable in the Calculus of + Inductive Constructions (CCI), we get proof-irrelevance from classical + logic in the CCI. +*) + +Section Proof_irrelevance_CCI. + + Hypothesis em : forall A:Prop, A \/ ~ A. + + Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) + (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a). + Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) + (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b). + Scheme or_indd := Induction for or Sort Prop. + + Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2. + Proof. + exact (proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl + or_elim_redr or_indd em). + Qed. + +End Proof_irrelevance_CCI. + +(** Remark: in the Set-impredicative CCI, Hurkens' paradox still holds with + [bool] in [Set] and since [~true=false] for [true] and [false] + in [bool] from [Set], we get the inconsistency of + [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI. +*) + +(** * Weak classical axioms *) + +(** We show the following increasing in the strength of axioms: + - weak excluded-middle + - right distributivity of implication over disjunction and Gödel-Dummet axiom + - independence of general premises and drinker's paradox + - excluded-middle +*) + +(** ** Weak excluded-middle *) + +(** The weak classical logic based on [~~A \/ ~A] is referred to with + name KC in {[ChagrovZakharyaschev97]] + + [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael + Zakharyaschev, "Modal Logic", Clarendon Press, 1997. +*) + +Definition weak_excluded_middle := + forall A:Prop, ~~A \/ ~A. + +(** The interest in the equivalent variant + [weak_generalized_excluded_middle] is that it holds even in logic + without a primitive [False] connective (like Gödel-Dummett axiom) *) + +Definition weak_generalized_excluded_middle := + forall A B:Prop, ((A -> B) -> B) \/ (A -> B). + +(** ** Gödel-Dummett axiom *) + +(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. + + [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus + with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol + 24 No. 2(1959), pp 97-103. + + [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", + Ergeb. Math. Koll. 4 (1933), pp. 34-38. + *) + +Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A). + +Lemma excluded_middle_Godel_Dummett : excluded_middle -> GodelDummett. +Proof. + intros EM A B. destruct (EM B) as [HB|HnotB]. + left; intros _; exact HB. + right; intros HB; destruct (HnotB HB). +Qed. + +(** [(A->B) \/ (B->A)] is equivalent to [(C -> A\/B) -> (C->A) \/ (C->B)] + (proof from [[Dummett59]]) *) + +Definition RightDistributivityImplicationOverDisjunction := + forall A B C:Prop, (C -> A\/B) -> (C->A) \/ (C->B). + +Lemma Godel_Dummett_iff_right_distr_implication_over_disjunction : + GodelDummett <-> RightDistributivityImplicationOverDisjunction. +Proof. + split. + intros GD A B C HCAB. + destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC; + destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption. + intros Distr A B. + destruct (Distr A B (A\/B)) as [HABA|HABB]. + intro HAB; exact HAB. + right; intro HB; apply HABA; right; assumption. + left; intro HA; apply HABB; left; assumption. +Qed. + +(** [(A->B) \/ (B->A)] is stronger than the weak excluded middle *) + +Lemma Godel_Dummett_weak_excluded_middle : + GodelDummett -> weak_excluded_middle. +Proof. + intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA]. + left; intro HnotA; apply (HnotA (HnotAA HnotA)). + right; intro HA; apply (HAnotA HA HA). +Qed. + +(** ** Independence of general premises and drinker's paradox *) + +(** Independence of general premises is the unconstrained, non + constructive, version of the Independence of Premises as + considered in [[Troelstra73]]. + + It is a generalization to predicate logic of the right + distributivity of implication over disjunction (hence of + Gödel-Dummett axiom) whose own constructive form (obtained by a + restricting the third formula to be negative) is called + Kreisel-Putnam principle [[KreiselPutnam57]]. + + [[KreiselPutnam57]], Georg Kreisel and Hilary Putnam. "Eine + Unableitsbarkeitsbeweismethode für den intuitionistischen + Aussagenkalkül". Archiv für Mathematische Logik und + Graundlagenforschung, 3:74- 78, 1957. + + [[Troelstra73]], Anne Troelstra, editor. Metamathematical + Investigation of Intuitionistic Arithmetic and Analysis, volume + 344 of Lecture Notes in Mathematics, Springer-Verlag, 1973. *) + +Notation Local "'inhabited' A" := A (at level 10, only parsing). + +Definition IndependenceOfGeneralPremises := + forall (A:Type) (P:A -> Prop) (Q:Prop), + inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x. + +Lemma + independence_general_premises_right_distr_implication_over_disjunction : + IndependenceOfGeneralPremises -> RightDistributivityImplicationOverDisjunction. +Proof. + intros IP A B C HCAB. + destruct (IP bool (fun b => if b then A else B) C true) as ([|],H). + intro HC; destruct (HCAB HC); [exists true|exists false]; assumption. + left; assumption. + right; assumption. +Qed. + +Lemma independence_general_premises_Godel_Dummett : + IndependenceOfGeneralPremises -> GodelDummett. +Proof. + destruct Godel_Dummett_iff_right_distr_implication_over_disjunction. + auto using independence_general_premises_right_distr_implication_over_disjunction. +Qed. + +(** Independence of general premises is equivalent to the drinker's paradox *) + +Definition DrinkerParadox := + forall (A:Type) (P:A -> Prop), + inhabited A -> exists x, (exists x, P x) -> P x. + +Lemma independence_general_premises_drinker : + IndependenceOfGeneralPremises <-> DrinkerParadox. +Proof. + split. + intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx. + intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx). + exists x; intro HQ; apply (Hx (H HQ)). +Qed. + +(** Independence of general premises is weaker than (generalized) + excluded middle *) + +Definition generalized_excluded_middle := + forall A B:Prop, A \/ (A -> B). + +Lemma excluded_middle_independence_general_premises : + generalized_excluded_middle -> DrinkerParadox. +Proof. + intros GEM A P x0. + destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot]. + exists x; intro; exact Hx. + exists x0; exact Hnot. +Qed. + diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v new file mode 100644 index 00000000..28d32fcc --- /dev/null +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -0,0 +1,79 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ClassicalUniqueChoice.v 9026 2006-07-06 15:16:20Z herbelin $ i*) + +(** This file provides classical logic and unique choice *) + +(** Classical logic and unique choice, as shown in + [ChicliPottierSimpson02], implies the double-negation of + excluded-middle in [Set], hence it implies a strongly classical + world. Especially it conflicts with the impredicativity of [Set]. + + [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos + Simpson, Mathematical Quotients and Quotient Types in Coq, + Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, + Springer Verlag. *) + +Require Export Classical. + +Axiom + dependent_unique_choice : + forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), + (forall x : A, exists! y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). + +(** Unique choice reifies functional relations into functions *) + +Theorem unique_choice : + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists! y : B, R x y) -> + (exists f:A->B, forall x:A, R x (f x)). +Proof. +intros A B. +apply (dependent_unique_choice A (fun _ => B)). +Qed. + +(** The following proof comes from [ChicliPottierSimpson02] *) + +Require Import Setoid. + +Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False. +Proof. +intro HnotEM. +set (R := fun A b => A /\ true = b \/ ~ A /\ false = b). +assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))). +apply unique_choice. +intro A. +destruct (classic A) as [Ha| Hnota]. + exists true; split. + left; split; [ assumption | reflexivity ]. + intros y [[_ Hy]| [Hna _]]. + assumption. + contradiction. + exists false; split. + right; split; [ assumption | reflexivity ]. + intros y [[Ha _]| [_ Hy]]. + contradiction. + assumption. +destruct H as [f Hf]. +apply HnotEM. +intro P. +assert (HfP := Hf P). +(* Elimination from Hf to Set is not allowed but from f to Set yes ! *) +destruct (f P). + left. + destruct HfP as [[Ha _]| [_ Hfalse]]. + assumption. + discriminate. + right. + destruct HfP as [[_ Hfalse]| [Hna _]]. + discriminate. + assumption. +Qed. + diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index c8f87fe8..2a5f03ec 100755..100644 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -6,11 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Pred_Set.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Classical_Pred_Set.v 8642 2006-03-17 10:09:02Z notin $ i*) + +(** This file is obsolete, use Classical_Pred_Type.v via Classical.v +instead *) (** Classical Predicate Logic on Set*) -Require Import Classical_Prop. +Require Import Classical_Pred_Type. Section Generic. Variable U : Set. @@ -19,52 +22,26 @@ Variable U : Set. Lemma not_all_ex_not : forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. -Proof. -unfold not in |- *; intros P notall. -apply NNPP; unfold not in |- *. -intro abs. -cut (forall n:U, P n); auto. -intro n; apply NNPP. -unfold not in |- *; intros. -apply abs; exists n; trivial. -Qed. +Proof (Classical_Pred_Type.not_all_ex_not U). Lemma not_all_not_ex : forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. -Proof. -intros P H. -elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n. -apply NNPP; trivial. -Qed. +Proof (Classical_Pred_Type.not_all_not_ex U). Lemma not_ex_all_not : forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. -Proof. -unfold not in |- *; intros P notex n abs. -apply notex. -exists n; trivial. -Qed. +Proof (Classical_Pred_Type.not_ex_all_not U). Lemma not_ex_not_all : forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n. -Proof. -intros P H n. -apply NNPP. -red in |- *; intro K; apply H; exists n; trivial. -Qed. +Proof (Classical_Pred_Type.not_ex_not_all U). Lemma ex_not_not_all : forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). -Proof. -unfold not in |- *; intros P exnot allP. -elim exnot; auto. -Qed. +Proof (Classical_Pred_Type.ex_not_not_all U). Lemma all_not_not_ex : forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). -Proof. -unfold not in |- *; intros P allnot exP; elim exP; intros n p. -apply allnot with n; auto. -Qed. +Proof (Classical_Pred_Type.all_not_not_ex U). -End Generic.
\ No newline at end of file +End Generic. diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index 804ff32d..56ebf967 100755..100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Pred_Type.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Classical_Pred_Type.v 8642 2006-03-17 10:09:02Z notin $ i*) (** Classical Predicate Logic on Type *) @@ -17,29 +17,30 @@ Variable U : Type. (** de Morgan laws for quantifiers *) -Lemma not_all_ex_not : - forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. +Lemma not_all_not_ex : + forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. Proof. -unfold not in |- *; intros P notall. -apply NNPP; unfold not in |- *. +intros P notall. +apply NNPP. intro abs. -cut (forall n:U, P n); auto. -intro n; apply NNPP. -unfold not in |- *; intros. -apply abs; exists n; trivial. +apply notall. +intros n H. +apply abs; exists n; exact H. Qed. -Lemma not_all_not_ex : - forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. +Lemma not_all_ex_not : + forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. Proof. -intros P H. -elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n. -apply NNPP; trivial. +intros P notall. +apply not_all_not_ex with (P:=fun x => ~ P x). +intro all; apply notall. +intro n; apply NNPP. +apply all. Qed. Lemma not_ex_all_not : forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. -Proof. +Proof. (* Intuitionistic *) unfold not in |- *; intros P notex n abs. apply notex. exists n; trivial. @@ -55,16 +56,16 @@ Qed. Lemma ex_not_not_all : forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). -Proof. +Proof. (* Intuitionistic *) unfold not in |- *; intros P exnot allP. elim exnot; auto. Qed. Lemma all_not_not_ex : forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). -Proof. +Proof. (* Intuitionistic *) unfold not in |- *; intros P allnot exP; elim exP; intros n p. apply allnot with n; auto. Qed. -End Generic.
\ No newline at end of file +End Generic. diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index ccc26df1..ce3e84a7 100755..100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Prop.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Classical_Prop.v 8892 2006-06-04 17:59:53Z herbelin $ i*) (** Classical Propositional Logic *) -Require Import ProofIrrelevance. +Require Import ClassicalFacts. Hint Unfold not: core. @@ -22,6 +22,15 @@ unfold not in |- *; intros; elim (classic p); auto. intro NP; elim (H NP). Qed. +(** Peirce's law states [forall P Q:Prop, ((P -> Q) -> P) -> P]. + Thanks to [forall P, False -> P], it is equivalent to the + following form *) + +Lemma Peirce : forall P:Prop, ((P -> False) -> P) -> P. +Proof. +intros P H; destruct (classic P); auto. +Qed. + Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P. Proof. intros; apply NNPP; red in |- *. @@ -29,8 +38,8 @@ intro; apply H; intro; absurd P; trivial. Qed. Lemma not_imply_elim2 : forall P Q:Prop, ~ (P -> Q) -> ~ Q. -Proof. -intros; elim (classic Q); auto. +Proof. (* Intuitionistic *) +tauto. Qed. Lemma imply_to_or : forall P Q:Prop, (P -> Q) -> ~ P \/ Q. @@ -46,9 +55,8 @@ apply not_imply_elim2 with P; trivial. Qed. Lemma or_to_imply : forall P Q:Prop, ~ P \/ Q -> P -> Q. -Proof. -simple induction 1; auto. -intros H1 H2; elim (H1 H2). +Proof. (* Intuitionistic *) +tauto. Qed. Lemma not_and_or : forall P Q:Prop, ~ (P /\ Q) -> ~ P \/ ~ Q. @@ -62,24 +70,50 @@ simple induction 1; red in |- *; simple induction 2; auto. Qed. Lemma not_or_and : forall P Q:Prop, ~ (P \/ Q) -> ~ P /\ ~ Q. -Proof. -intros; elim (classic P); auto. +Proof. (* Intuitionistic *) +tauto. Qed. Lemma and_not_or : forall P Q:Prop, ~ P /\ ~ Q -> ~ (P \/ Q). -Proof. -simple induction 1; red in |- *; simple induction 3; trivial. +Proof. (* Intuitionistic *) +tauto. Qed. Lemma imply_and_or : forall P Q:Prop, (P -> Q) -> P \/ Q -> Q. -Proof. -simple induction 2; trivial. +Proof. (* Intuitionistic *) +tauto. Qed. Lemma imply_and_or2 : forall P Q R:Prop, (P -> Q) -> P \/ R -> Q \/ R. -Proof. -simple induction 2; auto. +Proof. (* Intuitionistic *) +tauto. Qed. Lemma proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. -Proof proof_irrelevance_cci classic.
\ No newline at end of file +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]) +end. + +Ltac classical_left := match goal with +| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left]) +end. + +Require Export EqdepFacts. + +Module Eq_rect_eq. + +Lemma eq_rect_eq : + forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. +Proof. +intros; rewrite proof_irrelevance with (p1:=h) (p2:=refl_equal p); reflexivity. +Qed. + +End Eq_rect_eq. + +Module EqdepTheory := EqdepTheory(Eq_rect_eq). +Export EqdepTheory. diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index 753b8590..9b1f4e19 100755..100644 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v @@ -6,9 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Type.v,v 1.5.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Classical_Type.v 8642 2006-03-17 10:09:02Z notin $ i*) + +(** This file is obsolete, use Classical.v instead *) (** Classical Logic for Type *) Require Export Classical_Prop. -Require Export Classical_Pred_Type.
\ No newline at end of file +Require Export Classical_Pred_Type. diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v new file mode 100644 index 00000000..61e377ea --- /dev/null +++ b/theories/Logic/ConstructiveEpsilon.v @@ -0,0 +1,155 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id:$ i*) + +(** This module proves the constructive description schema, which +infers the sigma-existence (i.e., [Set]-existence) of a witness to a +predicate from the regular existence (i.e., [Prop]-existence). One +requires that the underlying set is countable and that the predicate +is decidable. *) + +(** Coq does not allow case analysis on sort [Set] when the goal is in +[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to +show [{n : nat | P n}]. However, one can perform a recursion on an +inductive predicate in sort [Prop] so that the returning type of the +recursion is in [Set]. This trick is described in Coq'Art book, Sect. +14.2.3 and 15.4. In particular, this trick is used in the proof of +[Acc_iter] in the module Coq.Init.Wf. There, recursion is done on an +inductive predicate [Acc] and the resulting type is in [Type]. + +The predicate [Acc] delineates elements that are accessible via a +given relation [R]. An element is accessible if there are no infinite +[R]-descending chains starting from it. + +To use [Acc_iter], we define a relation R and prove that if [exists n, +P n] then 0 is accessible with respect to R. Then, by induction on the +definition of [Acc R 0], we show [{n : nat | P n}]. *) + +(** Contributed by Yevgeniy Makarov *) + +Require Import Arith. + +Section ConstructiveIndefiniteDescription. + +Variable P : nat -> Prop. + +Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}. + +(** To find a witness of [P] constructively, we define an algorithm +that tries P on all natural numbers starting from 0 and going up. The +relation [R] describes the connection between the two successive +numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after +[x], i.e., [y = S x] and [P x] is false. Then the absence of an +infinite [R]-descending chain from 0 is equivalent to the termination +of our searching algorithm. *) + +Let R (x y : nat) := (x = S y /\ ~ P y). +Notation Local "'acc' x" := (Acc R x) (at level 10). + +Lemma P_implies_acc : forall x : nat, P x -> acc x. +Proof. +intros x H. constructor. +intros y [_ not_Px]. absurd (P x); assumption. +Qed. + +Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x. +Proof. +intros x n; generalize x; clear x; induction n as [|n IH]; simpl. +apply P_implies_acc. +intros x H. constructor. intros y [fxy _]. +apply IH. rewrite fxy. +replace (n + S x) with (S (n + x)); auto with arith. +Defined. + +Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0. +Proof. +intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x). +replace (x + 0) with x; auto with arith. +Defined. + +(** In the following statement, we use the trick with recursion on +[Acc]. This is also where decidability of [P] is used. *) + +Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}. +Proof. +intros Acc_0. pattern 0. apply Acc_iter with (R := R); [| assumption]. +clear Acc_0; intros x IH. +destruct (P_decidable x) as [Px | not_Px]. +exists x; simpl; assumption. +set (y := S x). +assert (Ryx : R y x). unfold R; split; auto. +destruct (IH y Ryx) as [n Hn]. +exists n; assumption. +Defined. + +Theorem constructive_indefinite_description_nat : (exists n : nat, P n) -> {n : nat | P n}. +Proof. +intros H; apply acc_implies_P_eventually. +apply P_eventually_implies_acc_ex; assumption. +Defined. + +End ConstructiveIndefiniteDescription. + +Section ConstructiveEpsilon. + +(** For the current purpose, we say that a set [A] is countable if +there are functions [f : A -> nat] and [g : nat -> A] such that [g] is +a left inverse of [f]. *) + +Variable A : Type. +Variable f : A -> nat. +Variable g : nat -> A. + +Hypothesis gof_eq_id : forall x : A, g (f x) = x. + +Variable P : A -> Prop. + +Hypothesis P_decidable : forall x : A, {P x} + {~ P x}. + +Definition P' (x : nat) : Prop := P (g x). + +Lemma P'_decidable : forall n : nat, {P' n} + {~ P' n}. +Proof. +intro n; unfold P'; destruct (P_decidable (g n)); auto. +Defined. + +Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}. +Proof. +intro H. assert (H1 : exists n : nat, P' n). +destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption. +apply (constructive_indefinite_description_nat P' P'_decidable) in H1. +destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption. +Defined. + +Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}. +Proof. + intros; apply constructive_indefinite_description; firstorder. +Defined. + +Definition epsilon (E : exists x : A, P x) : A + := proj1_sig (constructive_indefinite_description E). + +Definition epsilon_spec (E : (exists x, P x)) : P (epsilon E) + := proj2_sig (constructive_indefinite_description E). + +End ConstructiveEpsilon. + +Theorem choice : + forall (A B : Type) (f : B -> nat) (g : nat -> B), + (forall x : B, g (f x) = x) -> + forall (R : A -> B -> Prop), + (forall (x : A) (y : B), {R x y} + {~ R x y}) -> + (forall x : A, exists y : B, R x y) -> + (exists f : A -> B, forall x : A, R x (f x)). +Proof. +intros A B f g gof_eq_id R R_dec H. +exists (fun x : A => epsilon B f g gof_eq_id (R x) (R_dec x) (H x)). +intro x. +apply (epsilon_spec B f g gof_eq_id (R x) (R_dec x) (H x)). +Qed. diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 08babda9..8317f6bb 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Decidable.v,v 1.5.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Decidable.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (** Properties of decidable propositions *) diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v new file mode 100644 index 00000000..a38b111f --- /dev/null +++ b/theories/Logic/DecidableType.v @@ -0,0 +1,156 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id: DecidableType.v 8933 2006-06-09 14:08:38Z herbelin $ *) + +Require Export SetoidList. +Set Implicit Arguments. +Unset Strict Implicit. + +(** * Types with decidable Equalities (but no ordering) *) + +Module Type DecidableType. + + Parameter t : Set. + + Parameter eq : t -> t -> Prop. + + Axiom eq_refl : forall x : t, eq x x. + Axiom eq_sym : forall x y : t, eq x y -> eq y x. + Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + + Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. + + Hint Immediate eq_sym. + Hint Resolve eq_refl eq_trans. + +End DecidableType. + +(** * Additional notions about keys and datas used in FMap *) + +Module KeyDecidableType(D:DecidableType). + Import D. + + Section Elt. + Variable elt : Set. + Notation key:=t. + + Definition eqk (p p':key*elt) := eq (fst p) (fst p'). + Definition eqke (p p':key*elt) := + eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Hint Unfold eqk eqke. + Hint Extern 2 (eqke ?a ?b) => split. + + (* eqke is stricter than eqk *) + + Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'. + Proof. + unfold eqk, eqke; intuition. + Qed. + + (* eqk, eqke are equalities *) + + Lemma eqk_refl : forall e, eqk e e. + Proof. auto. Qed. + + Lemma eqke_refl : forall e, eqke e e. + Proof. auto. Qed. + + Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. + Proof. auto. Qed. + + Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. + Proof. unfold eqke; intuition. Qed. + + Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. + Proof. eauto. Qed. + + Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. + Proof. + unfold eqke; intuition; [ eauto | congruence ]. + Qed. + + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. + Hint Immediate eqk_sym eqke_sym. + + Lemma InA_eqke_eqk : + forall x m, InA eqke x m -> InA eqk x m. + Proof. + unfold eqke; induction 1; intuition. + Qed. + Hint Resolve InA_eqke_eqk. + + Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. + Proof. + intros; apply InA_eqA with p; auto; apply eqk_trans; auto. + Qed. + + Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). + Definition In k m := exists e:elt, MapsTo k e m. + + Hint Unfold MapsTo In. + + (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) + + Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. + Proof. + firstorder. + exists x; auto. + induction H. + destruct y. + exists e; auto. + destruct IHInA as [e H0]. + exists e; auto. + Qed. + + Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. + Proof. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto. + Qed. + + Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. + Proof. + destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto. + Qed. + + Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. + Proof. + inversion 1. + inversion_clear H0; eauto. + destruct H1; simpl in *; intuition. + Qed. + + Lemma In_inv_2 : forall k k' e e' l, + InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. + Proof. + inversion_clear 1; compute in H0; intuition. + Qed. + + Lemma In_inv_3 : forall x x' l, + InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. + Proof. + inversion_clear 1; compute in H0; intuition. + Qed. + + End Elt. + + Hint Unfold eqk eqke. + Hint Extern 2 (eqke ?a ?b) => split. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. + Hint Immediate eqk_sym eqke_sym. + Hint Resolve InA_eqke_eqk. + Hint Unfold MapsTo In. + Hint Resolve In_inv_2 In_inv_3. + +End KeyDecidableType. + + + + + diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v new file mode 100644 index 00000000..a4f99de2 --- /dev/null +++ b/theories/Logic/DecidableTypeEx.v @@ -0,0 +1,50 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id: DecidableTypeEx.v 8933 2006-06-09 14:08:38Z herbelin $ *) + +Require Import DecidableType OrderedType OrderedTypeEx. +Set Implicit Arguments. +Unset Strict Implicit. + +(** * Examples of Decidable Type structures. *) + +(** A particular case of [DecidableType] where + the equality is the usual one of Coq. *) + +Module Type UsualDecidableType. + Parameter t : Set. + Definition eq := @eq t. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Parameter eq_dec : forall x y, { eq x y }+{~eq x y }. +End UsualDecidableType. + +(** a [UsualDecidableType] is in particular an [DecidableType]. *) + +Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. + +(** An OrderedType can be seen as a DecidableType *) + +Module OT_as_DT (O:OrderedType) <: DecidableType. + Module OF := OrderedTypeFacts O. + Definition t := O.t. + Definition eq := O.eq. + Definition eq_refl := O.eq_refl. + Definition eq_sym := O.eq_sym. + Definition eq_trans := O.eq_trans. + Definition eq_dec := OF.eq_dec. +End OT_as_DT. + +(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *) + +Module Nat_as_DT <: UsualDecidableType := OT_as_DT (Nat_as_OT). +Module Positive_as_DT <: UsualDecidableType := OT_as_DT (Positive_as_OT). +Module N_as_DT <: UsualDecidableType := OT_as_DT (N_as_OT). +Module Z_as_DT <: UsualDecidableType := OT_as_DT (Z_as_OT). diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 2b982963..5f139f35 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,26 +7,46 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Diaconescu.v,v 1.5.2.3 2004/08/01 09:36:44 herbelin Exp $ i*) +(*i $Id: Diaconescu.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory - entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner] - adapted the proof to show that the axiom of choice in equivalence - classes entails Excluded-Middle in Type Theory. +(** Diaconescu showed that the Axiom of Choice entails Excluded-Middle + in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show + that the axiom of choice in equivalence classes entails + Excluded-Middle in Type Theory [LacasWerner99]. - This is an adaptatation of the proof by Hugo Herbelin to show that - the relational form of the Axiom of Choice + Extensionality for - predicates entails Excluded-Middle + Three variants of Diaconescu's result in type theory are shown below. - [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in - Proceedings of AMS, vol 51, pp 176-178, 1975. + A. A proof that the relational form of the Axiom of Choice + + Extensionality for Predicates entails Excluded-Middle (by Hugo + Herbelin) - [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?, - preprint, 1999. + B. A proof that the relational form of the Axiom of Choice + Proof + Irrelevance entails Excluded-Middle for Equality Statements (by + Benjamin Werner) + C. A proof that extensional Hilbert epsilon's description operator + entails excluded-middle (taken from Bell [Bell93]) + + See also [Carlström] for a discussion of the connection between the + Extensional Axiom of Choice and Excluded-Middle + + [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation, + in Proceedings of AMS, vol 51, pp 176-178, 1975. + + [LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply + the excluded middle?, preprint, 1999. + + [Bell93] John L. Bell, Hilbert's epsilon operator and classical + logic, Journal of Philosophical Logic, 22: 1-18, 1993 + + [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext, + Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) -Section PredExt_GuardRelChoice_imp_EM. +(**********************************************************************) +(** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) + +Section PredExt_RelChoice_imp_EM. (** The axiom of extensionality for predicates *) @@ -61,16 +82,10 @@ Require Import ChoiceFacts. Variable rel_choice : RelationalChoice. -Lemma guarded_rel_choice : - forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop), - (forall x:A, P x -> exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - P x -> - exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). +Lemma guarded_rel_choice : GuardedRelationalChoice. Proof. - exact - (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel). + apply + (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel). Qed. (** The form of choice we need: there is a functional relation which chooses @@ -78,16 +93,19 @@ Qed. Require Import Bool. -Lemma AC : +Lemma AC_bool_subset_to_bool : exists R : (bool -> Prop) -> bool -> Prop, (forall P:bool -> Prop, (exists b : bool, P b) -> exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')). Proof. - apply guarded_rel_choice with - (P := fun Q:bool -> Prop => exists y : _, Q y) - (R := fun (Q:bool -> Prop) (y:bool) => Q y). - exact (fun _ H => H). + destruct (guarded_rel_choice _ _ + (fun Q:bool -> Prop => exists y : _, Q y) + (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)). + exact (fun _ H => H). + exists R; intros P HP. + destruct (HR P HP) as (y,(Hy,Huni)). + exists y; firstorder. Qed. (** The proof of the excluded middle *) @@ -98,7 +116,7 @@ Proof. intro P. (** first we exhibit the choice functional relation R *) -destruct AC as [R H]. +destruct AC_bool_subset_to_bool as [R H]. set (class_of_true := fun b => b = true \/ P). set (class_of_false := fun b => b = false \/ P). @@ -135,4 +153,152 @@ left; assumption. Qed. -End PredExt_GuardRelChoice_imp_EM. +End PredExt_RelChoice_imp_EM. + +(**********************************************************************) +(** * B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *) + +(** This is an adaptation of Diaconescu's paradox exploiting that + proof-irrelevance is some form of extensionality *) + +Section ProofIrrel_RelChoice_imp_EqEM. + +Variable rel_choice : RelationalChoice. + +Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y. + +(** Let [a1] and [a2] be two elements in some type [A] *) + +Variable A :Type. +Variables a1 a2 : A. + +(** We build the subset [A'] of [A] made of [a1] and [a2] *) + +Definition A' := sigT (fun x => x=a1 \/ x=a2). + +Definition a1':A'. +exists a1 ; auto. +Defined. + +Definition a2':A'. +exists a2 ; auto. +Defined. + +(** By proof-irrelevance, projection is a retraction *) + +Lemma projT1_injective : a1=a2 -> a1'=a2'. +Proof. + intro Heq ; unfold a1', a2', A'. + rewrite Heq. + replace (or_introl (a2=a2) (refl_equal a2)) + with (or_intror (a2=a2) (refl_equal a2)). + reflexivity. + apply proof_irrelevance. +Qed. + +(** But from the actual proofs of being in [A'], we can assert in the + proof-irrelevant world the existence of relevant boolean witnesses *) + +Lemma decide : forall x:A', exists y:bool , + (projT1 x = a1 /\ y = true ) \/ (projT1 x = a2 /\ y = false). +Proof. + intros [a [Ha1|Ha2]]; [exists true | exists false]; auto. +Qed. + +(** Thanks to the axiom of choice, the boolean witnesses move from the + propositional world to the relevant world *) + +Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2. +Proof. + destruct + (rel_choice A' bool + (fun x y => projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false)) + as (R,(HRsub,HR)). + apply decide. + destruct (HR a1') as (b1,(Ha1'b1,_Huni1)). + destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)]. + destruct (HR a2') as (b2,(Ha2'b2,Huni2)). + destruct (HRsub a2' b2 Ha2'b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)]. + left; symmetry; assumption. + right; intro H. + subst b1; subst b2. + rewrite (projT1_injective H) in Ha1'b1. + assert (false = true) by auto using Huni2. + discriminate. + left; assumption. +Qed. + +(** An alternative more concise proof can be done by directly using + the guarded relational choice *) + +Declare Implicit Tactic auto. + +Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2. +Proof. + assert (decide: forall x:A, x=a1 \/ x=a2 -> + exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false). + intros a [Ha1|Ha2]; [exists true | exists false]; auto. + assert (guarded_rel_choice := + rel_choice_and_proof_irrel_imp_guarded_rel_choice + rel_choice + proof_irrelevance). + destruct + (guarded_rel_choice A bool + (fun x => x=a1 \/ x=a2) + (fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false)) + as (R,(HRsub,HR)). + apply decide. + destruct (HR a1) as (b1,(Ha1b1,_Huni1)). left; reflexivity. + destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)]. + destruct (HR a2) as (b2,(Ha2b2,Huni2)). right; reflexivity. + destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)]. + left; symmetry; assumption. + right; intro H. + subst b1; subst b2; subst a1. + assert (false = true) by auto using Huni2, Ha1b1. + discriminate. + left; assumption. +Qed. + +End ProofIrrel_RelChoice_imp_EqEM. + +(**********************************************************************) +(** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *) + +(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) + +Notation Local "'inhabited' A" := A (at level 10, only parsing). + +Section ExtensionalEpsilon_imp_EM. + +Variable epsilon : forall A : Type, inhabited A -> (A -> Prop) -> A. + +Hypothesis epsilon_spec : + forall (A:Type) (i:inhabited A) (P:A->Prop), + (exists x, P x) -> P (epsilon A i P). + +Hypothesis epsilon_extensionality : + forall (A:Type) (i:inhabited A) (P Q:A->Prop), + (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q. + +Notation Local eps := (epsilon bool true) (only parsing). + +Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P. +Proof. + intro P. + pose (B := fun y => y=false \/ P). + pose (C := fun y => y=true \/ P). + assert (B (eps B)) as [Hfalse|HP] + by (apply epsilon_spec; exists false; left; reflexivity). + assert (C (eps C)) as [Htrue|HP] + by (apply epsilon_spec; exists true; left; reflexivity). + right; intro HP. + assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption). + rewrite epsilon_extensionality with (1:=H) in Hfalse. + rewrite Htrue in Hfalse. + discriminate. + auto. + auto. +Qed. + +End ExtensionalEpsilon_imp_EM. diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 24905039..2fe9d1a6 100755..100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -6,183 +6,29 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep.v,v 1.10.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Eqdep.v 8642 2006-03-17 10:09:02Z notin $ i*) -(** This file defines dependent equality and shows its equivalence with - equality on dependent pairs (inhabiting sigma-types). It axiomatizes - the invariance by substitution of reflexive equality proofs and - shows the equivalence between the 4 following statements +(** This file axiomatizes the invariance by substitution of reflexive + equality proofs [[Streicher93]] and exports its consequences, such + as the injectivity of the projection of the dependent pair. - - Invariance by Substitution of Reflexive Equality Proofs. - - Injectivity of Dependent Equality - - Uniqueness of Identity Proofs - - Uniqueness of Reflexive Identity Proofs - - Streicher's Axiom K - - These statements are independent of the calculus of constructions [2]. - - References: - - [1] T. Streicher, Semantical Investigations into Intensional Type Theory, - Habilitationsschrift, LMU München, 1993. - [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory, - Proceedings of the meeting Twenty-five years of constructive - type theory, Venice, Oxford University Press, 1998 + [[Streicher93]] T. Streicher, Semantical Investigations into + Intensional Type Theory, Habilitationsschrift, LMU München, 1993. *) -Section Dependent_Equality. - -Variable U : Type. -Variable P : U -> Type. - -(** Dependent equality *) - -Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop := - eq_dep_intro : eq_dep p x p x. -Hint Constructors eq_dep: core v62. - -Lemma eq_dep_sym : - forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x. -Proof. -destruct 1; auto. -Qed. -Hint Immediate eq_dep_sym: core v62. +Require Export EqdepFacts. -Lemma eq_dep_trans : - forall (p q r:U) (x:P p) (y:P q) (z:P r), - eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z. -Proof. -destruct 1; auto. -Qed. - -Scheme eq_indd := Induction for eq Sort Prop. - -Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop := - eq_dep1_intro : forall h:q = p, x = eq_rect q P y p h -> eq_dep1 p x q y. - -Lemma eq_dep1_dep : - forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y. -Proof. -destruct 1 as (eq_qp, H). -destruct eq_qp using eq_indd. -rewrite H. -apply eq_dep_intro. -Qed. - -Lemma eq_dep_dep1 : - forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y. -Proof. -destruct 1. -apply eq_dep1_intro with (refl_equal p). -simpl in |- *; trivial. -Qed. - -(** Invariance by Substitution of Reflexive Equality Proofs *) +Module Eq_rect_eq. Axiom eq_rect_eq : - forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. - -(** Injectivity of Dependent Equality is a consequence of *) -(** Invariance by Substitution of Reflexive Equality Proof *) - -Lemma eq_dep1_eq : forall (p:U) (x y:P p), eq_dep1 p x p y -> x = y. -Proof. -simple destruct 1; intro. -rewrite <- eq_rect_eq; auto. -Qed. - -Lemma eq_dep_eq : forall (p:U) (x y:P p), eq_dep p x p y -> x = y. -Proof. -intros; apply eq_dep1_eq; apply eq_dep_dep1; trivial. -Qed. - -End Dependent_Equality. - -(** Uniqueness of Identity Proofs (UIP) is a consequence of *) -(** Injectivity of Dependent Equality *) - -Lemma UIP : forall (U:Type) (x y:U) (p1 p2:x = y), p1 = p2. -Proof. -intros; apply eq_dep_eq with (P := fun y => x = y). -elim p2 using eq_indd. -elim p1 using eq_indd. -apply eq_dep_intro. -Qed. - -(** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *) - -Lemma UIP_refl : forall (U:Type) (x:U) (p:x = x), p = refl_equal x. -Proof. -intros; apply UIP. -Qed. - -(** Streicher axiom K is a direct consequence of Uniqueness of - Reflexive Identity Proofs *) - -Lemma Streicher_K : - forall (U:Type) (x:U) (P:x = x -> Prop), - P (refl_equal x) -> forall p:x = x, P p. -Proof. -intros; rewrite UIP_refl; assumption. -Qed. - -(** We finally recover eq_rec_eq (alternatively eq_rect_eq) from K *) - -Lemma eq_rec_eq : - forall (U:Type) (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h. -Proof. -intros. -apply Streicher_K with (p := h). -reflexivity. -Qed. - -(** Dependent equality is equivalent to equality on dependent pairs *) - -Lemma equiv_eqex_eqdep : - forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q), - existS P p x = existS P q y <-> eq_dep U P p x q y. -Proof. -split. -(* -> *) -intro H. -change p with (projS1 (existS P p x)) in |- *. -change x at 2 with (projS2 (existS P p x)) in |- *. -rewrite H. -apply eq_dep_intro. -(* <- *) -destruct 1; reflexivity. -Qed. - -(** UIP implies the injectivity of equality on dependent pairs *) - -Lemma inj_pair2 : - forall (U:Set) (P:U -> Set) (p:U) (x y:P p), - existS P p x = existS P p y -> x = y. -Proof. -intros. -apply (eq_dep_eq U P). -generalize (equiv_eqex_eqdep U P p p x y). -simple induction 1. -intros. -auto. -Qed. + forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. -(** UIP implies the injectivity of equality on dependent pairs *) +End Eq_rect_eq. -Lemma inj_pairT2 : - forall (U:Type) (P:U -> Type) (p:U) (x y:P p), - existT P p x = existT P p y -> x = y. -Proof. -intros. -apply (eq_dep_eq U P). -change p at 1 with (projT1 (existT P p x)) in |- *. -change x at 2 with (projT2 (existT P p x)) in |- *. -rewrite H. -apply eq_dep_intro. -Qed. +Module EqdepTheory := EqdepTheory(Eq_rect_eq). +Export EqdepTheory. -(** The main results to be exported *) +(** Exported hints *) -Hint Resolve eq_dep_intro eq_dep_eq: core v62. -Hint Immediate eq_dep_sym: core v62. +Hint Resolve eq_dep_eq: core v62. Hint Resolve inj_pair2 inj_pairT2: core. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v new file mode 100644 index 00000000..94a577ca --- /dev/null +++ b/theories/Logic/EqdepFacts.v @@ -0,0 +1,336 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: EqdepFacts.v 9597 2007-02-06 19:44:05Z herbelin $ i*) + +(** This file defines dependent equality and shows its equivalence with + equality on dependent pairs (inhabiting sigma-types). It derives + the consequence of axiomatizing the invariance by substitution of + reflexive equality proofs and shows the equivalence between the 4 + following statements + + - Invariance by Substitution of Reflexive Equality Proofs. + - Injectivity of Dependent Equality + - Uniqueness of Identity Proofs + - Uniqueness of Reflexive Identity Proofs + - Streicher's Axiom K + + These statements are independent of the calculus of constructions [2]. + + References: + + [1] T. Streicher, Semantical Investigations into Intensional Type Theory, + Habilitationsschrift, LMU München, 1993. + [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory, + Proceedings of the meeting Twenty-five years of constructive + type theory, Venice, Oxford University Press, 1998 + +Table of contents: + +1. Definition of dependent equality and equivalence with equality + +2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K + +3. Definition of the functor that builds properties of dependent + equalities assuming axiom eq_rect_eq + +*) + +(************************************************************************) +(** * Definition of dependent equality and equivalence with equality of dependent pairs *) + +Section Dependent_Equality. + + Variable U : Type. + Variable P : U -> Type. + + (** Dependent equality *) + + Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop := + eq_dep_intro : eq_dep p x p x. + Hint Constructors eq_dep: core v62. + + Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x. + Proof eq_dep_intro. + + Lemma eq_dep_sym : + forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x. + Proof. + destruct 1; auto. + Qed. + Hint Immediate eq_dep_sym: core v62. + + Lemma eq_dep_trans : + forall (p q r:U) (x:P p) (y:P q) (z:P r), + eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z. + Proof. + destruct 1; auto. + Qed. + + Scheme eq_indd := Induction for eq Sort Prop. + + (** Equivalent definition of dependent equality expressed as a non + dependent inductive type *) + + Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop := + eq_dep1_intro : forall h:q = p, x = eq_rect q P y p h -> eq_dep1 p x q y. + + Lemma eq_dep1_dep : + forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y. + Proof. + destruct 1 as (eq_qp, H). + destruct eq_qp using eq_indd. + rewrite H. + apply eq_dep_intro. + Qed. + + Lemma eq_dep_dep1 : + forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y. + Proof. + destruct 1. + apply eq_dep1_intro with (refl_equal p). + simpl in |- *; trivial. + Qed. + +End Dependent_Equality. + +Implicit Arguments eq_dep [U P]. +Implicit Arguments eq_dep1 [U P]. + +(** Dependent equality is equivalent to equality on dependent pairs *) + +Lemma eq_sigS_eq_dep : + forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), + existT P p x = existT P q y -> eq_dep p x q y. +Proof. + intros. + dependent rewrite H. + apply eq_dep_intro. +Qed. + +Lemma equiv_eqex_eqdep : + forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), + existS P p x = existS P q y <-> eq_dep p x q y. +Proof. + split. + (* -> *) + apply eq_sigS_eq_dep. + (* <- *) + destruct 1; reflexivity. +Qed. + +Lemma eq_sigT_eq_dep : + forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), + existT P p x = existT P q y -> eq_dep p x q y. +Proof. + intros. + dependent rewrite H. + apply eq_dep_intro. +Qed. + +Lemma eq_dep_eq_sigT : + forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), + eq_dep p x q y -> existT P p x = existT P q y. +Proof. + destruct 1; reflexivity. +Qed. + +(** Exported hints *) + +Hint Resolve eq_dep_intro: core v62. +Hint Immediate eq_dep_sym: core v62. + +(************************************************************************) +(** * Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K *) + +Section Equivalences. + + Variable U:Type. + + (** Invariance by Substitution of Reflexive Equality Proofs *) + + Definition Eq_rect_eq := + forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + + (** Injectivity of Dependent Equality *) + + Definition Eq_dep_eq := + forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y. + + (** Uniqueness of Identity Proofs (UIP) *) + + Definition UIP_ := + forall (x y:U) (p1 p2:x = y), p1 = p2. + + (** Uniqueness of Reflexive Identity Proofs *) + + Definition UIP_refl_ := + forall (x:U) (p:x = x), p = refl_equal x. + + (** Streicher's axiom K *) + + Definition Streicher_K_ := + forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + + (** Injectivity of Dependent Equality is a consequence of *) + (** Invariance by Substitution of Reflexive Equality Proof *) + + Lemma eq_rect_eq__eq_dep1_eq : + Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y. + Proof. + intro eq_rect_eq. + simple destruct 1; intro. + rewrite <- eq_rect_eq; auto. + Qed. + + Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq. + Proof. + intros eq_rect_eq; red; intros. + apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial. + Qed. + + (** Uniqueness of Identity Proofs (UIP) is a consequence of *) + (** Injectivity of Dependent Equality *) + + Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_. + Proof. + intro eq_dep_eq; red. + intros; apply eq_dep_eq with (P := fun y => x = y). + elim p2 using eq_indd. + elim p1 using eq_indd. + apply eq_dep_intro. + Qed. + + (** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *) + + Lemma UIP__UIP_refl : UIP_ -> UIP_refl_. + Proof. + intro UIP; red; intros; apply UIP. + Qed. + + (** Streicher's axiom K is a direct consequence of Uniqueness of + Reflexive Identity Proofs *) + + Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_. + Proof. + intro UIP_refl; red; intros; rewrite UIP_refl; assumption. + Qed. + + (** We finally recover from K the Invariance by Substitution of + Reflexive Equality Proofs *) + + Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq. + Proof. + intro Streicher_K; red; intros. + apply Streicher_K with (p := h). + reflexivity. + Qed. + +(** Remark: It is reasonable to think that [eq_rect_eq] is strictly + stronger than [eq_rec_eq] (which is [eq_rect_eq] restricted on [Set]): + + [Definition Eq_rec_eq := + forall (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.] + + Typically, [eq_rect_eq] allows to prove UIP and Streicher's K what + does not seem possible with [eq_rec_eq]. In particular, the proof of [UIP] + requires to use [eq_rect_eq] on [fun y -> x=y] which is in [Type] but not + in [Set]. +*) + +End Equivalences. + +Section Corollaries. + + Variable U:Type. + + (** UIP implies the injectivity of equality on dependent pairs in Type *) + + Definition Inj_dep_pair := + forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y. + + Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair. + Proof. + intro eq_dep_eq; red; intros. + apply eq_dep_eq. + apply eq_sigS_eq_dep. + assumption. + Qed. + +End Corollaries. + +Notation Inj_dep_pairS := Inj_dep_pair. +Notation Inj_dep_pairT := Inj_dep_pair. +Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2. + + +(************************************************************************) +(** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *) + +Module Type EqdepElimination. + + Axiom eq_rect_eq : + forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), + x = eq_rect p Q x p h. + +End EqdepElimination. + +Module EqdepTheory (M:EqdepElimination). + + Section Axioms. + + Variable U:Type. + +(** Invariance by Substitution of Reflexive Equality Proofs *) + +Lemma eq_rect_eq : + forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. +Proof M.eq_rect_eq U. + +Lemma eq_rec_eq : + forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h. +Proof (fun p Q => M.eq_rect_eq U p Q). + +(** Injectivity of Dependent Equality *) + +Lemma eq_dep_eq : forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y. +Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq). + +(** Uniqueness of Identity Proofs (UIP) is a consequence of *) +(** Injectivity of Dependent Equality *) + +Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2. +Proof (eq_dep_eq__UIP U eq_dep_eq). + +(** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *) + +Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x. +Proof (UIP__UIP_refl U UIP). + +(** Streicher's axiom K is a direct consequence of Uniqueness of + Reflexive Identity Proofs *) + +Lemma Streicher_K : + forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. +Proof (UIP_refl__Streicher_K U UIP_refl). + +End Axioms. + +(** UIP implies the injectivity of equality on dependent pairs in Type *) + +Lemma inj_pair2 : + forall (U:Type) (P:U -> Type) (p:U) (x y:P p), + existT P p x = existT P p y -> x = y. +Proof (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)). + +Notation inj_pairT2 := inj_pair2. + +End EqdepTheory. + +Implicit Arguments eq_dep []. +Implicit Arguments eq_dep1 []. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 7caf403c..103efd22 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -6,153 +6,293 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep_dec.v,v 1.14.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Eqdep_dec.v 9597 2007-02-06 19:44:05Z herbelin $ i*) -(** We prove that there is only one proof of [x=x], i.e [(refl_equal ? x)]. - This holds if the equality upon the set of [x] is decidable. - A corollary of this theorem is the equality of the right projections - of two equal dependent pairs. +(** We prove that there is only one proof of [x=x], i.e [refl_equal x]. + This holds if the equality upon the set of [x] is decidable. + A corollary of this theorem is the equality of the right projections + of two equal dependent pairs. - Author: Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego - adapted to Coq by B. Barras + Author: Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego + adapted to Coq by B. Barras - Credit: Proofs up to [K_dec] follows an outline by Michael Hedberg -*) + Credit: Proofs up to [K_dec] follow an outline by Michael Hedberg +Table of contents: -(** We need some dependent elimination schemes *) +1. Streicher's K and injectivity of dependent pair hold on decidable types -Set Implicit Arguments. +1.1. Definition of the functor that builds properties of dependent equalities + from a proof of decidability of equality for a set in Type - (** Bijection between [eq] and [eqT] *) - Definition eq2eqT (A:Set) (x y:A) (eqxy:x = y) : - x = y := - match eqxy in (_ = y) return x = y with - | refl_equal => refl_equal x - end. - - Definition eqT2eq (A:Set) (x y:A) (eqTxy:x = y) : - x = y := - match eqTxy in (_ = y) return x = y with - | refl_equal => refl_equal x - end. +1.2. Definition of the functor that builds properties of dependent equalities + from a proof of decidability of equality for a set in Set - Lemma eq_eqT_bij : forall (A:Set) (x y:A) (p:x = y), p = eqT2eq (eq2eqT p). -intros. -case p; reflexivity. -Qed. +*) - Lemma eqT_eq_bij : forall (A:Set) (x y:A) (p:x = y), p = eq2eqT (eqT2eq p). -intros. -case p; reflexivity. -Qed. +(************************************************************************) +(** * Streicher's K and injectivity of dependent pair hold on decidable types *) +Set Implicit Arguments. -Section DecidableEqDep. +Section EqdepDec. Variable A : Type. - + Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' := eq_ind _ (fun a => a = y') eq2 _ eq1. - Remark trans_sym_eqT : forall (x y:A) (u:x = y), comp u u = refl_equal y. -intros. -case u; trivial. -Qed. - - + Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = refl_equal y. + Proof. + intros. + case u; trivial. + Qed. Variable eq_dec : forall x y:A, x = y \/ x <> y. - + Variable x : A. - Let nu (y:A) (u:x = y) : x = y := match eq_dec x y with - | or_introl eqxy => eqxy - | or_intror neqxy => False_ind _ (neqxy u) + | or_introl eqxy => eqxy + | or_intror neqxy => False_ind _ (neqxy u) end. Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v. -intros. -unfold nu in |- *. -case (eq_dec x y); intros. -reflexivity. - -case n; trivial. -Qed. + intros. + unfold nu in |- *. + case (eq_dec x y); intros. + reflexivity. + + case n; trivial. + Qed. Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (refl_equal x)) v. - + Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u. -intros. -case u; unfold nu_inv in |- *. -apply trans_sym_eqT. -Qed. + Proof. + intros. + case u; unfold nu_inv in |- *. + apply trans_sym_eq. + Qed. Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2. -intros. -elim nu_left_inv with (u := p1). -elim nu_left_inv with (u := p2). -elim nu_constant with y p1 p2. -reflexivity. -Qed. - - Theorem K_dec : - forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p. -intros. -elim eq_proofs_unicity with x (refl_equal x) p. -trivial. -Qed. - + Proof. + intros. + elim nu_left_inv with (u := p1). + elim nu_left_inv with (u := p2). + elim nu_constant with y p1 p2. + reflexivity. + Qed. + + Theorem K_dec : + forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p. + Proof. + intros. + elim eq_proofs_unicity with x (refl_equal x) p. + trivial. + Qed. (** The corollary *) Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x := match exP with - | ex_intro x' prf => + | ex_intro x' prf => match eq_dec x' x with - | or_introl eqprf => eq_ind x' P prf x eqprf - | _ => def + | or_introl eqprf => eq_ind x' P prf x eqprf + | _ => def end end. Theorem inj_right_pair : - forall (P:A -> Prop) (y y':P x), - ex_intro P x y = ex_intro P x y' -> y = y'. -intros. -cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y). -simpl in |- *. -case (eq_dec x x). -intro e. -elim e using K_dec; trivial. - -intros. -case n; trivial. - -case H. -reflexivity. + forall (P:A -> Prop) (y y':P x), + ex_intro P x y = ex_intro P x y' -> y = y'. + Proof. + intros. + cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y). + simpl in |- *. + case (eq_dec x x). + intro e. + elim e using K_dec; trivial. + + intros. + case n; trivial. + + case H. + reflexivity. + Qed. + +End EqdepDec. + +Require Import EqdepFacts. + +(** We deduce axiom [K] for (decidable) types *) +Theorem K_dec_type : + forall A:Type, + (forall x y:A, {x = y} + {x <> y}) -> + forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. +Proof. + intros A eq_dec x P H p. + elim p using K_dec; intros. + case (eq_dec x0 y); [left|right]; assumption. + trivial. Qed. +Theorem K_dec_set : + forall A:Set, + (forall x y:A, {x = y} + {x <> y}) -> + forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. +Proof fun A => K_dec_type (A:=A). + +(** We deduce the [eq_rect_eq] axiom for (decidable) types *) +Theorem eq_rect_eq_dec : + forall A:Type, + (forall x y:A, {x = y} + {x <> y}) -> + forall (p:A) (Q:A -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. +Proof. + intros A eq_dec. + apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)). +Qed. + +Unset Implicit Arguments. + +(************************************************************************) +(** ** Definition of the functor that builds properties of dependent equalities on decidable sets in Type *) + +(** The signature of decidable sets in [Type] *) + +Module Type DecidableType. + + Parameter U:Type. + Axiom eq_dec : forall x y:U, {x = y} + {x <> y}. + +End DecidableType. + +(** The module [DecidableEqDep] collects equality properties for decidable + set in [Type] *) + +Module DecidableEqDep (M:DecidableType). + + Import M. + + (** Invariance by Substitution of Reflexive Equality Proofs *) + + Lemma eq_rect_eq : + forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + Proof eq_rect_eq_dec eq_dec. + + (** Injectivity of Dependent Equality *) + + Theorem eq_dep_eq : + forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y. + Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq). + + (** Uniqueness of Identity Proofs (UIP) *) + + Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2. + Proof (eq_dep_eq__UIP U eq_dep_eq). + + (** Uniqueness of Reflexive Identity Proofs *) + + Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x. + Proof (UIP__UIP_refl U UIP). + + (** Streicher's axiom K *) + + Lemma Streicher_K : + forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + Proof (K_dec_type eq_dec). + + (** Injectivity of equality on dependent pairs in [Type] *) + + Lemma inj_pairT2 : + forall (P:U -> Type) (p:U) (x y:P p), + existT P p x = existT P p y -> x = y. + Proof eq_dep_eq__inj_pairT2 U eq_dep_eq. + + (** Proof-irrelevance on subsets of decidable sets *) + + Lemma inj_pairP2 : + forall (P:U -> Prop) (x:U) (p q:P x), + ex_intro P x p = ex_intro P x q -> p = q. + Proof. + intros. + apply inj_right_pair with (A:=U). + intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. + assumption. + Qed. + End DecidableEqDep. - (** We deduce the [K] axiom for (decidable) Set *) - Theorem K_dec_set : - forall A:Set, - (forall x y:A, {x = y} + {x <> y}) -> - forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. -intros. -rewrite eq_eqT_bij. -elim (eq2eqT p) using K_dec. -intros. -case (H x0 y); intros. -elim e; left; reflexivity. - -right; red in |- *; intro neq; apply n; elim neq; reflexivity. - -trivial. -Qed.
\ No newline at end of file +(************************************************************************) +(** ** B Definition of the functor that builds properties of dependent equalities on decidable sets in Set *) + +(** The signature of decidable sets in [Set] *) + +Module Type DecidableSet. + + Parameter U:Type. + Axiom eq_dec : forall x y:U, {x = y} + {x <> y}. + +End DecidableSet. + +(** The module [DecidableEqDepSet] collects equality properties for decidable + set in [Set] *) + +Module DecidableEqDepSet (M:DecidableSet). + + Import M. + Module N:=DecidableEqDep(M). + + (** Invariance by Substitution of Reflexive Equality Proofs *) + + Lemma eq_rect_eq : + forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + Proof eq_rect_eq_dec eq_dec. + + (** Injectivity of Dependent Equality *) + + Theorem eq_dep_eq : + forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y. + Proof N.eq_dep_eq. + + (** Uniqueness of Identity Proofs (UIP) *) + + Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2. + Proof N.UIP. + + (** Uniqueness of Reflexive Identity Proofs *) + + Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x. + Proof N.UIP_refl. + + (** Streicher's axiom K *) + + Lemma Streicher_K : + forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + Proof N.Streicher_K. + + (** Proof-irrelevance on subsets of decidable sets *) + + Lemma inj_pairP2 : + forall (P:U -> Prop) (x:U) (p q:P x), + ex_intro P x p = ex_intro P x q -> p = q. + Proof N.inj_pairP2. + + (** Injectivity of equality on dependent pairs in [Type] *) + + Lemma inj_pair2 : + forall (P:U -> Type) (p:U) (x y:P p), + existS P p x = existS P p y -> x = y. + Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq. + + (** Injectivity of equality on dependent pairs with second component + in [Type] *) + + Notation inj_pairT2 := inj_pair2. + +End DecidableEqDepSet. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 4666d9b4..6a723e43 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: JMeq.v,v 1.8.2.2 2004/08/03 17:42:32 herbelin Exp $ i*) +(*i $Id: JMeq.v 9077 2006-08-24 08:44:32Z herbelin $ i*) -(** John Major's Equality as proposed by C. Mc Bride +(** John Major's Equality as proposed by Conor McBride Reference: @@ -19,56 +19,65 @@ Set Implicit Arguments. -Inductive JMeq (A:Set) (x:A) : forall B:Set, B -> Prop := +Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop := JMeq_refl : JMeq x x. -Reset JMeq_ind. +Reset JMeq_rect. Hint Resolve JMeq_refl. -Lemma sym_JMeq : forall (A B:Set) (x:A) (y:B), JMeq x y -> JMeq y x. +Lemma sym_JMeq : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. destruct 1; trivial. Qed. Hint Immediate sym_JMeq. Lemma trans_JMeq : - forall (A B C:Set) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z. + forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z. destruct 1; trivial. Qed. -Axiom JMeq_eq : forall (A:Set) (x y:A), JMeq x y -> x = y. +Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. -Lemma JMeq_ind : forall (A:Set) (x y:A) (P:A -> Prop), P x -> JMeq x y -> P y. +Lemma JMeq_ind : forall (A:Type) (x y:A) (P:A -> Prop), P x -> JMeq x y -> P y. intros A x y P H H'; case JMeq_eq with (1 := H'); trivial. Qed. -Lemma JMeq_rec : forall (A:Set) (x y:A) (P:A -> Set), P x -> JMeq x y -> P y. +Lemma JMeq_rec : forall (A:Type) (x y:A) (P:A -> Set), P x -> JMeq x y -> P y. +intros A x y P H H'; case JMeq_eq with (1 := H'); trivial. +Qed. + +Lemma JMeq_rect : forall (A:Type) (x y:A) (P:A->Type), P x -> JMeq x y -> P y. intros A x y P H H'; case JMeq_eq with (1 := H'); trivial. Qed. Lemma JMeq_ind_r : - forall (A:Set) (x y:A) (P:A -> Prop), P y -> JMeq x y -> P x. + forall (A:Type) (x y:A) (P:A -> Prop), P y -> JMeq x y -> P x. intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial. Qed. Lemma JMeq_rec_r : - forall (A:Set) (x y:A) (P:A -> Set), P y -> JMeq x y -> P x. + forall (A:Type) (x y:A) (P:A -> Set), P y -> JMeq x y -> P x. +intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial. +Qed. + +Lemma JMeq_rect_r : + forall (A:Type) (x y:A) (P:A -> Type), P y -> JMeq x y -> P x. intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial. Qed. -(** [JMeq] is equivalent to [(eq_dep Set [X]X)] *) +(** [JMeq] is equivalent to [(eq_dep Type [X]X)] *) Require Import Eqdep. Lemma JMeq_eq_dep : - forall (A B:Set) (x:A) (y:B), JMeq x y -> eq_dep Set (fun X => X) A x B y. + forall (A B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X => X) A x B y. Proof. destruct 1. apply eq_dep_intro. Qed. Lemma eq_dep_JMeq : - forall (A B:Set) (x:A) (y:B), eq_dep Set (fun X => X) A x B y -> JMeq x y. + forall (A B:Type) (x:A) (y:B), eq_dep Type (fun X => X) A x B y -> JMeq x y. Proof. destruct 1. apply JMeq_refl. diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v index afdc0ffe..44ab9a2e 100644 --- a/theories/Logic/ProofIrrelevance.v +++ b/theories/Logic/ProofIrrelevance.v @@ -6,109 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** This is a proof in the pure Calculus of Construction that - classical logic in Prop + dependent elimination of disjunction entails - proof-irrelevance. +(** This file axiomatizes proof-irrelevance and derives some consequences *) - Since, dependent elimination is derivable in the Calculus of - Inductive Constructions (CCI), we get proof-irrelevance from classical - logic in the CCI. +Require Import ProofIrrelevanceFacts. - Reference: +Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. - - [Coquand] T. Coquand, "Metamathematical Investigations of a - Calculus of Constructions", Proceedings of Logic in Computer Science - (LICS'90), 1990. +Module PI. Definition proof_irrelevance := proof_irrelevance. End PI. - Proof skeleton: classical logic + dependent elimination of - disjunction + discrimination of proofs implies the existence of a - retract from [Prop] into [bool], hence inconsistency by encoding any - paradox of system U- (e.g. Hurkens' paradox). -*) - -Require Import Hurkens. - -Section Proof_irrelevance_CC. - -Variable or : Prop -> Prop -> Prop. -Variable or_introl : forall A B:Prop, A -> or A B. -Variable or_intror : forall A B:Prop, B -> or A B. -Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C. -Hypothesis - or_elim_redl : - forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A), - f a = or_elim A B C f g (or_introl A B a). -Hypothesis - or_elim_redr : - forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B), - g b = or_elim A B C f g (or_intror A B b). -Hypothesis - or_dep_elim : - forall (A B:Prop) (P:or A B -> Prop), - (forall a:A, P (or_introl A B a)) -> - (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b. - -Hypothesis em : forall A:Prop, or A (~ A). -Variable B : Prop. -Variables b1 b2 : B. - -(** [p2b] and [b2p] form a retract if [~b1=b2] *) - -Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A). -Definition b2p b := b1 = b. - -Lemma p2p1 : forall A:Prop, A -> b2p (p2b A). -Proof. - unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); - unfold b2p in |- *; intros. - apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)). - destruct (b H). -Qed. -Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A. -Proof. - intro not_eq_b1_b2. - unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); - unfold b2p in |- *; intros. - assumption. - destruct not_eq_b1_b2. - rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H. - assumption. -Qed. - -(** Using excluded-middle a second time, we get proof-irrelevance *) - -Theorem proof_irrelevance_cc : b1 = b2. -Proof. - refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H. - trivial. - apply (paradox B p2b b2p (p2p2 H) p2p1). -Qed. - -End Proof_irrelevance_CC. - - -(** The Calculus of Inductive Constructions (CCI) enjoys dependent - elimination, hence classical logic in CCI entails proof-irrelevance. -*) - -Section Proof_irrelevance_CCI. - -Hypothesis em : forall A:Prop, A \/ ~ A. - -Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) - (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a). -Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) - (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b). -Scheme or_indd := Induction for or Sort Prop. - -Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2. -Proof - proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl - or_elim_redr or_indd em. - -End Proof_irrelevance_CCI. - -(** Remark: in CCI, [bool] can be taken in [Set] as well in the - paradox and since [~true=false] for [true] and [false] in - [bool], we get the inconsistency of [em : forall A:Prop, {A}+{~A}] in CCI -*) +Module ProofIrrelevanceTheory := ProofIrrelevanceTheory(PI). +Export ProofIrrelevanceTheory. diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v new file mode 100644 index 00000000..dd3178eb --- /dev/null +++ b/theories/Logic/ProofIrrelevanceFacts.v @@ -0,0 +1,62 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This defines the functor that build consequences of proof-irrelevance *) + +Require Export EqdepFacts. + +Module Type ProofIrrelevance. + + Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. + +End ProofIrrelevance. + +Module ProofIrrelevanceTheory (M:ProofIrrelevance). + + (** Proof-irrelevance implies uniqueness of reflexivity proofs *) + + Module Eq_rect_eq. + Lemma eq_rect_eq : + forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), + x = eq_rect p Q x p h. + Proof. + intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=refl_equal p). + reflexivity. + Qed. + End Eq_rect_eq. + + (** Export the theory of injective dependent elimination *) + + Module EqdepTheory := EqdepTheory(Eq_rect_eq). + Export EqdepTheory. + + Scheme eq_indd := Induction for eq Sort Prop. + + (** We derive the irrelevance of the membership property for subsets *) + + Lemma subset_eq_compat : + forall (U:Set) (P:U->Prop) (x y:U) (p:P x) (q:P y), + x = y -> exist P x p = exist P y q. + Proof. + intros. + rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + elim H using eq_indd. + reflexivity. + Qed. + + Lemma subsetT_eq_compat : + forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), + x = y -> existT P x p = existT P y q. + Proof. + intros. + rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + elim H using eq_indd. + reflexivity. + Qed. + +End ProofIrrelevanceTheory. diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index 08873aa5..ec168f09 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -6,15 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RelationalChoice.v,v 1.3.2.2 2004/08/01 09:29:59 herbelin Exp $ i*) +(*i $Id: RelationalChoice.v 8892 2006-06-04 17:59:53Z herbelin $ i*) (** This file axiomatizes the relational form of the axiom of choice *) -Axiom - relational_choice : - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - exists y : B, - R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). +Axiom relational_choice : + forall (A B : Type) (R : A->B->Prop), + (forall x : A, exists y : B, R x y) -> + exists R' : A->B->Prop, + subrelation R' R /\ forall x : A, exists! y : B, R' x y. |