diff options
Diffstat (limited to 'theories/Logic')
-rw-r--r-- | theories/Logic/ChoiceFacts.v | 440 | ||||
-rw-r--r-- | theories/Logic/ClassicalEpsilon.v | 68 | ||||
-rw-r--r-- | theories/Logic/ClassicalFacts.v | 452 | ||||
-rw-r--r-- | theories/Logic/Diaconescu.v | 36 | ||||
-rw-r--r-- | theories/Logic/EqdepFacts.v | 332 | ||||
-rw-r--r-- | theories/Logic/Eqdep_dec.v | 177 | ||||
-rw-r--r-- | theories/Logic/JMeq.v | 35 |
7 files changed, 785 insertions, 755 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index d2b7db04..3b066cfc 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -7,9 +7,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v 8999 2006-07-04 12:46:04Z notin $ i*) +(*i $Id: ChoiceFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** ** Some facts and definitions concerning choice and description in +(** Some facts and definitions concerning choice and description in intuitionistic logic. We investigate the relations between the following choice and @@ -54,21 +54,21 @@ IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) Table of contents -A. Definitions +1. Definitions -B. IPL_2^2 |- AC_rel + AC! = AC_fun +2. IPL_2^2 |- AC_rel + AC! = AC_fun -C. 1. AC_rel + PI -> GAC_rel and PL_2 |- AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel +3. 1. AC_rel + PI -> GAC_rel and PL_2 |- AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel -C. 2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker +4. 2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker -D. Derivability of choice for decidable relations with well-ordered codomain +5. Derivability of choice for decidable relations with well-ordered codomain -E. Equivalence of choices on dependent or non dependent functional types +6. Equivalence of choices on dependent or non dependent functional types -F. Non contradiction of constructive descriptions wrt functional choices +7. Non contradiction of constructive descriptions wrt functional choices -G. Definite description transports classical logic to the computational world +8. Definite description transports classical logic to the computational world References: @@ -87,7 +87,7 @@ Set Implicit Arguments. Notation Local "'inhabited' A" := A (at level 10, only parsing). (**********************************************************************) -(** *** A. Definitions *) +(** * Definitions *) (** Choice, reification and description schemes *) @@ -99,29 +99,29 @@ Variables P:A->Prop. Variables R:A->B->Prop. -(** **** Constructive choice and description *) +(** ** 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). + (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)). + (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)). + (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 @@ -130,7 +130,7 @@ Definition FunctionalRelReification_on := Definition ConstructiveIndefiniteDescription_on := forall P:A->Prop, - (exists x, P x) -> { x:A | P x }. + (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 @@ -139,59 +139,59 @@ Definition ConstructiveIndefiniteDescription_on := Definition ConstructiveDefiniteDescription_on := forall P:A->Prop, - (exists! x, P x) -> { x:A | P x }. + (exists! x, P x) -> { x:A | P x }. -(** **** Weakly classical choice and description *) +(** ** 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). + (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)). + 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)). + 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. + 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). + 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 }. + 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 }. + A -> { x:A | (exists! x, P x) -> P x }. End ChoiceSchemes. @@ -235,10 +235,10 @@ Definition IndependenceOfGeneralPremises := Definition SmallDrinker'sParadox := forall (A:Type) (P:A -> Prop), inhabited A -> - exists x, (exists x, P x) -> P x. + exists x, (exists x, P x) -> P x. (**********************************************************************) -(** *** B. AC_rel + PDP = AC_fun +(** * 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 @@ -251,25 +251,25 @@ Definition SmallDrinker'sParadox := Lemma description_rel_choice_imp_funct_choice : forall A B : Type, - FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B. + 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. + intros A B Descr RelCh R H. + destruct (RelCh R H) as (R',(HR'R,H0)). + destruct (Descr R') as (f,Hf). + firstorder. + exists f; intro x. + destruct (H0 x) as (y,(HR'xy,Huniq)). + rewrite <- (Huniq (f x) (Hf x)). + apply HR'R; assumption. Qed. Lemma 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 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. @@ -279,77 +279,77 @@ Qed. 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. + 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 : 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). + 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. (**********************************************************************) -(** *** C. Connection between the guarded, non guarded and descriptive choices and *) +(** * 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 *) (**********************************************************************) -(** **** C. 1. AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *) +(** ** 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',(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 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 (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'. + 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. + 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)). + 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. + 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. + 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)). + intros A B GAC_rel R H. + destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)). firstorder. -exists R'; firstorder. + exists R'; firstorder. Qed. (** OAC_rel = GAC_rel *) @@ -357,43 +357,43 @@ Qed. Lemma guarded_iff_omniscient_rel_choice : GuardedRelationalChoice <-> OmniscientRelationalChoice. Proof. -split. + split. intros GAC_rel A B R. - apply (GAC_rel A B (fun x => exists y, R x y) R); auto. + 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. + destruct (OAC_rel A B R) as (f,Hf); exists f; firstorder. Qed. (**********************************************************************) -(** **** C. 2. AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker *) +(** ** AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker *) (** AC_fun + IGP = GAC_fun *) Lemma guarded_fun_choice_imp_indep_of_general_premises : - GuardedFunctionalChoice -> IndependenceOfGeneralPremises. + 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. + 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. + 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. + 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. + 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 *) @@ -403,26 +403,26 @@ Qed. 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. + 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. + 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). + 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. @@ -435,16 +435,16 @@ but we give a direct proof *) Lemma guarded_iff_omniscient_fun_choice : GuardedFunctionalChoice <-> OmniscientFunctionalChoice. Proof. -split. + split. intros GAC_fun A B R Inh. - apply (GAC_fun A B (fun x => exists y, R x y) R); auto. + 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. + destruct (OAC_fun A B R Inh) as (f,Hf). + exists f; firstorder. Qed. (**********************************************************************) -(** *** D. Derivability of choice for decidable relations with well-ordered codomain *) +(** * 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 @@ -468,10 +468,10 @@ 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')). + 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'. @@ -493,43 +493,43 @@ assert 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. + 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)). + 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. + 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). + 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. + exists f. + intros x. + destruct (Hf x) as (Hfx,_). + assumption. Qed. (**********************************************************************) -(** *** E. Choice on dependent and non dependent function types are equivalent *) +(** * Choice on dependent and non dependent function types are equivalent *) -(** **** E. 1. 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)). + (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). @@ -539,7 +539,7 @@ Notation DependentFunctionalChoice := Theorem dep_non_dep_functional_choice : DependentFunctionalChoice -> FunctionalChoice. Proof. -intros AC_depfun A B R H. + intros AC_depfun A B R H. destruct (AC_depfun A (fun _ => B) R H) as (f,Hf). exists f; trivial. Qed. @@ -558,24 +558,24 @@ Definition proj1_inf (A B:Prop) (p : A/\B) := 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. + intros AC_fun A B R H. + pose (B' := { x:A & B x }). + pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). + destruct (AC_fun A B' R') as (f,Hf). + intros x. destruct (H x) as (y,Hy). + exists (existT (fun x => B x) x y). split; trivial. + exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))). + intro x; destruct (Hf x) as (Heq,HR) using and_indd. + destruct (f x); simpl in *. + destruct Heq using eq_indd; trivial. Qed. -(** **** E. 2. Reification of dependent and non dependent functional relation are equivalent *) +(** ** 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)). + (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). @@ -585,7 +585,7 @@ Notation DependentFunctionalRelReification := Theorem dep_non_dep_functional_rel_reification : DependentFunctionalRelReification -> FunctionalRelReification. Proof. -intros DepFunReify A B R H. + intros DepFunReify A B R H. destruct (DepFunReify A (fun _ => B) R H) as (f,Hf). exists f; trivial. Qed. @@ -598,91 +598,91 @@ Qed. 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)). + 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. + exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))). + intro x; destruct (Hf x) as (Heq,HR) using and_indd. + destruct (f x); simpl in *. + destruct Heq using eq_indd; trivial. Qed. (**********************************************************************) -(** *** F. Non contradiction of constructive descriptions wrt functional axioms of choice *) +(** * Non contradiction of constructive descriptions wrt functional axioms of choice *) -(** **** F. 1. Non contradiction of indefinite description *) +(** ** Non contradiction of indefinite description *) Lemma relative_non_contradiction_of_indefinite_desc : - (ConstructiveIndefiniteDescription -> False) - -> (FunctionalChoice -> False). + (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. + 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. + 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))). + intros IndefDescr A B R H. + exists (fun x => proj1_sig (IndefDescr B (R x) (H x))). + intro x. + apply (proj2_sig (IndefDescr B (R x) (H x))). Qed. -(** **** F. 2. Non contradiction of definite description *) +(** ** Non contradiction of definite description *) Lemma relative_non_contradiction_of_definite_descr : - (ConstructiveDefiniteDescription -> False) - -> (FunctionalRelReification -> False). + (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. + 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. + 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))). + intros DefDescr A B R H. + exists (fun x => proj1_sig (DefDescr B (R x) (H x))). + intro x. + apply (proj2_sig (DefDescr B (R x) (H x))). Qed. (**********************************************************************) -(** *** G. Excluded-middle + definite description => computational excluded-middle *) +(** * Excluded-middle + definite description => computational excluded-middle *) (** The idea for the following proof comes from [ChicliPottierSimpson02] *) @@ -705,15 +705,15 @@ 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). + 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. + exists true; trivial. + exists false; trivial. + intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction. + left; trivial. + right; trivial. Qed. diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index b7293bec..6d0a9c77 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalEpsilon.v 8933 2006-06-09 14:08:38Z herbelin $ i*) +(*i $Id: ClassicalEpsilon.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** *** This file provides classical logic and indefinite description +(** This file provides classical logic and indefinite description (Hilbert's epsilon operator) *) (** Classical epsilon's operator (i.e. indefinite description) implies @@ -21,37 +21,39 @@ Require Import ChoiceFacts. Set Implicit Arguments. -Notation Local "'inhabited' A" := A (at level 200, only parsing). - Axiom constructive_indefinite_description : forall (A : Type) (P : A->Prop), - (ex P) -> { x : A | P x }. + (exists x, P x) -> { x : A | P x }. Lemma constructive_definite_description : forall (A : Type) (P : A->Prop), - (exists! x : A, P x) -> { x : A | P x }. + (exists! x, P x) -> { x : A | P x }. Proof. -intros; apply constructive_indefinite_description; firstorder. + 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). + 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 | ex P -> P x }. + { 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 => ex P -> P x). + 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. - firstorder. -Qed. + 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 *) @@ -59,11 +61,9 @@ 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) : - (ex P) -> P (epsilon i P) + (exists x, P x) -> P (epsilon i P) := proj2_sig (classical_indefinite_description P i). -Opaque epsilon. - (** Open question: is classical_indefinite_description constructively provable from [relational_choice] and [constructive_definite_description] (at least, using the fact that @@ -72,19 +72,31 @@ Opaque epsilon. [classical_indefinite_description] is provable (see [relative_non_contradiction_of_indefinite_desc]). *) -(** Remark: we use [ex P] rather than [exists x, P x] (which is [ex - (fun x => P x)] to ease unification *) +(** 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)). + 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))). + 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 70da74d3..dd911db6 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -7,39 +7,39 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalFacts.v 8892 2006-06-04 17:59:53Z herbelin $ 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 Table of contents: -A. Propositional degeneracy = excluded-middle + propositional extensionality +1. Propositional degeneracy = excluded-middle + propositional extensionality -B. Classical logic and proof-irrelevance +2. Classical logic and proof-irrelevance -B. 1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint +2.1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint -B. 2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance +2.2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance -B. 3. CIC |- prop. ext. -> proof-irrelevance +2.3. CIC |- prop. ext. -> proof-irrelevance -B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance +2.4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance -B. 5. CIC |- excluded-middle -> proof-irrelevance +2.5. CIC |- excluded-middle -> proof-irrelevance -C. Weak classical axioms +3. Weak classical axioms -C. 1. Weak excluded middle +3.1. Weak excluded middle -C. 2. Gödel-Dummet axiom and right distributivity of implication over +3.2. Gödel-Dummet axiom and right distributivity of implication over disjunction -C. 3. Independence of general premises and drinker's paradox +3 3. Independence of general premises and drinker's paradox *) (************************************************************************) -(** *** A. Prop degeneracy = excluded-middle + prop extensionality *) +(** * Prop degeneracy = excluded-middle + prop extensionality *) (** i.e. [(forall A, A=True \/ A=False) <-> @@ -61,41 +61,41 @@ Definition excluded_middle := forall A:Prop, A \/ ~ A. 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. (************************************************************************) -(** *** B. Classical logic and proof-irrelevance *) +(** * Classical logic and proof-irrelevance *) (************************************************************************) -(** **** B. 1. CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *) +(** ** CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *) (** We successively show that: @@ -110,41 +110,41 @@ 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. (************************************************************************) -(** **** B. 2. CC |- prop_ext /\ dep elim on bool -> proof-irrelevance *) +(** ** 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. @@ -161,44 +161,44 @@ Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. 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. @@ -208,29 +208,30 @@ End Proof_irrelevance_gen. *) 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 - ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl - BoolP_elim_redr. + + 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. (************************************************************************) -(** **** B. 3. CIC |- prop. ext. -> proof-irrelevance *) +(** ** CIC |- prop. ext. -> proof-irrelevance *) (** In the Calculus of Inductive Constructions, inductively defined booleans enjoy dependent case analysis, hence directly proof-irrelevance from @@ -238,21 +239,22 @@ End Proof_irrelevance_Prop_Ext_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. @@ -267,12 +269,12 @@ End Proof_irrelevance_CIC. cannot be refined. [[Berardi90]] Stefano Berardi, "Type dependence and constructive - mathematics", Ph. D. thesis, Dipartimento Matematica, Università di + mathematics", Ph. D. thesis, Dipartimento Matematica, Università di Torino, 1990. *) (************************************************************************) -(** **** B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance *) +(** ** 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 @@ -293,60 +295,61 @@ End Proof_irrelevance_CIC. 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 : + + 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 : + 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 : + 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. + + 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. + apply (paradox B p2b b2p (p2p2 H) p2p1). + Qed. End Proof_irrelevance_EM_CC. @@ -357,7 +360,7 @@ End Proof_irrelevance_EM_CC. *) (************************************************************************) -(** **** B. 5. CIC |- excluded-middle -> proof-irrelevance *) +(** ** CIC |- excluded-middle -> proof-irrelevance *) (** Since, dependent elimination is derivable in the Calculus of @@ -367,18 +370,19 @@ End Proof_irrelevance_EM_CC. 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. + 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. @@ -388,16 +392,16 @@ End Proof_irrelevance_CCI. [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI. *) -(** *** C. Weak classical axioms *) +(** * 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 + - right distributivity of implication over disjunction and Gödel-Dummet axiom - independence of general premises and drinker's paradox - excluded-middle *) -(** **** C. 1. Weak excluded-middle *) +(** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with name KC in {[ChagrovZakharyaschev97]] @@ -411,20 +415,20 @@ Definition weak_excluded_middle := (** 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) *) + without a primitive [False] connective (like Gödel-Dummett axiom) *) Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). -(** **** C. 2. Gödel-Dummett axiom *) +(** ** Gödel-Dummett axiom *) -(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. +(** [(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", + [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", Ergeb. Math. Koll. 4 (1933), pp. 34-38. *) @@ -432,7 +436,7 @@ 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]. + intros EM A B. destruct (EM B) as [HB|HnotB]. left; intros _; exact HB. right; intros HB; destruct (HnotB HB). Qed. @@ -446,15 +450,15 @@ Definition RightDistributivityImplicationOverDisjunction := 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. + 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 *) @@ -462,12 +466,12 @@ Qed. 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). + 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. -(** **** C. 3. Independence of general premises and drinker's paradox *) +(** ** Independence of general premises and drinker's paradox *) (** Independence of general premises is the unconstrained, non constructive, version of the Independence of Premises as @@ -475,13 +479,13 @@ Qed. 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 + 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 + Unableitsbarkeitsbeweismethode für den intuitionistischen + Aussagenkalkül". Archiv für Mathematische Logik und Graundlagenforschung, 3:74- 78, 1957. [[Troelstra73]], Anne Troelstra, editor. Metamathematical @@ -499,33 +503,33 @@ 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. + 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. + 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. + 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)). + 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) @@ -537,9 +541,9 @@ Definition generalized_excluded_middle := 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. + 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/Diaconescu.v b/theories/Logic/Diaconescu.v index 19d5d7ec..5f139f35 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Diaconescu.v 8892 2006-06-04 17:59:53Z herbelin $ i*) +(*i $Id: Diaconescu.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show @@ -44,7 +44,7 @@ *) (**********************************************************************) -(** *** A. Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) +(** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) Section PredExt_RelChoice_imp_EM. @@ -156,7 +156,7 @@ Qed. End PredExt_RelChoice_imp_EM. (**********************************************************************) -(** *** B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *) +(** * 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 *) @@ -263,7 +263,7 @@ Qed. End ProofIrrel_RelChoice_imp_EqEM. (**********************************************************************) -(** *** B. Extensional Hilbert's epsilon description operator -> Excluded-Middle *) +(** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *) (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) @@ -285,20 +285,20 @@ 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. + 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/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 7963555a..a257ef55 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqdepFacts.v 8674 2006-03-30 06:56:50Z herbelin $ i*) +(*i $Id: EqdepFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives @@ -32,70 +32,70 @@ Table of contents: -A. Definition of dependent equality and equivalence with equality +1. Definition of dependent equality and equivalence with equality -B. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K +2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K -C. Definition of the functor that builds properties of dependent +3. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *) (************************************************************************) -(** *** A. Definition of dependent equality and equivalence with equality of dependent pairs *) +(** * Definition of dependent equality and equivalence with equality of dependent pairs *) Section Dependent_Equality. + + Variable U : Type. + Variable P : U -> Type. -Variable U : Type. -Variable P : U -> Type. + (** Dependent equality *) -(** Dependent equality *) - -Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop := + 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. + 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_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_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. + 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. + Scheme eq_indd := Induction for eq Sort Prop. -(** Equivalent definition of dependent equality expressed as a non - dependent inductive type *) + (** 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 := + 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. + 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. @@ -105,8 +105,8 @@ Implicit Arguments eq_dep1 [U P]. (** Dependent equality is equivalent to equality on dependent pairs *) Lemma eq_sigS_eq_dep : - 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 p x q y. + 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 p x q y. Proof. intros. dependent rewrite H. @@ -114,10 +114,10 @@ Proof. Qed. Lemma equiv_eqex_eqdep : - forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q), + 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 p x q y. Proof. -split. + split. (* -> *) apply eq_sigS_eq_dep. (* <- *) @@ -125,8 +125,8 @@ split. 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. + 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. @@ -134,8 +134,8 @@ Proof. 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. + 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. @@ -146,90 +146,90 @@ Hint Resolve eq_dep_intro: core v62. Hint Immediate eq_dep_sym: core v62. (************************************************************************) -(** *** B. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K *) +(** * 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. + + 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]): @@ -246,37 +246,37 @@ Qed. End Equivalences. Section Corollaries. - -Variable U:Type. -Variable V:Set. - -(** UIP implies the injectivity of equality on dependent pairs in Type *) - -Definition Inj_dep_pairT := - 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_pairT2 : Eq_dep_eq U -> Inj_dep_pairT. + + Variable U:Type. + Variable V:Set. + + (** UIP implies the injectivity of equality on dependent pairs in Type *) + + Definition Inj_dep_pairT := + 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_pairT2 : Eq_dep_eq U -> Inj_dep_pairT. + Proof. + intro eq_dep_eq; red; intros. + apply eq_dep_eq. + apply eq_sigT_eq_dep. + assumption. + Qed. + + (** UIP implies the injectivity of equality on dependent pairs in Set *) + + Definition Inj_dep_pairS := + forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y. + + Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS. Proof. intro eq_dep_eq; red; intros. apply eq_dep_eq. - apply eq_sigT_eq_dep. + apply eq_sigS_eq_dep. assumption. Qed. -(** UIP implies the injectivity of equality on dependent pairs in Set *) - -Definition Inj_dep_pairS := - forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y. - -Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS. -Proof. - intro eq_dep_eq; red; intros. - apply eq_dep_eq. - apply eq_sigS_eq_dep. - assumption. -Qed. - End Corollaries. (************************************************************************) @@ -286,16 +286,16 @@ 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. + x = eq_rect p Q x p h. End EqdepElimination. Module EqdepTheory (M:EqdepElimination). - -Section Axioms. - -Variable U:Type. - + + Section Axioms. + + Variable U:Type. + (** Invariance by Substitution of Reflexive Equality Proofs *) Lemma eq_rect_eq : diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 7d71a1a6..740fcfcf 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep_dec.v 8136 2006-03-05 21:57:47Z herbelin $ i*) +(*i $Id: Eqdep_dec.v 9245 2006-10-17 12:53:34Z notin $ 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. @@ -20,149 +20,153 @@ Table of contents: -A. Streicher's K and injectivity of dependent pair hold on decidable types +1. Streicher's K and injectivity of dependent pair hold on decidable types -B.1. Definition of the functor that builds properties of dependent equalities +1.1. Definition of the functor that builds properties of dependent equalities from a proof of decidability of equality for a set in Type -B.2. Definition of the functor that builds properties of dependent equalities +1.2. Definition of the functor that builds properties of dependent equalities from a proof of decidability of equality for a set in Set *) (************************************************************************) -(** *** A. Streicher's K and injectivity of dependent pair hold on decidable types *) +(** * Streicher's K and injectivity of dependent pair hold on decidable types *) Set Implicit Arguments. Section EqdepDec. Variable A : Type. - + Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' := eq_ind _ (fun a => a = y') eq2 _ eq1. Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = refl_equal y. -intros. -case u; trivial. -Qed. - - + 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_eq. -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. + 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. -intros. -elim eq_proofs_unicity with x (refl_equal x) p. -trivial. -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. -Qed. + 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. -intros A eq_dec x P H p. -elim p using K_dec; intros. -case (eq_dec x0 y); [left|right]; assumption. -trivial. +(** 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. -intros A eq_dec. -apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)). +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. (************************************************************************) -(** *** B.1. Definition of the functor that builds properties of dependent equalities on decidable sets in Type *) +(** ** 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}. @@ -215,16 +219,17 @@ Module DecidableEqDep (M:DecidableType). 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. - intros. - apply inj_right_pair with (A:=U). - intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. - assumption. + Proof. + intros. + apply inj_right_pair with (A:=U). + intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. + assumption. Qed. End DecidableEqDep. (************************************************************************) -(** *** B.2 Definition of the functor that builds properties of dependent equalities on decidable sets in Set *) +(** ** B Definition of the functor that builds properties of dependent equalities on decidable sets in Set *) (** The signature of decidable sets in [Set] *) diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 4d365e32..6a723e43 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: JMeq.v 6009 2004-08-03 17:42:55Z herbelin $ i*) +(*i $Id: JMeq.v 9077 2006-08-24 08:44:32Z herbelin $ i*) (** John Major's Equality as proposed by Conor McBride @@ -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. |