diff options
Diffstat (limited to 'theories/Logic')
29 files changed, 389 insertions, 528 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 9eaef07a..5b2f5063 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 8122 2006-03-04 19:26:40Z herbelin $ i*) +(*i $Id$ i*) (** This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of @@ -67,10 +67,10 @@ Section Retracts. Variables A B : Prop. -Record retract : Prop := +Record retract : Prop := {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. -Record retract_cond : Prop := +Record retract_cond : Prop := {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. @@ -94,7 +94,7 @@ Proof. intros A B. destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. exists f0 g0; trivial. - exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; + 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 3d434b37..b2c4a049 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,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v 10756 2008-04-04 17:10:45Z herbelin $ i*) +(*i $Id: ChoiceFacts.v 12363 2009-09-28 15:04:07Z letouzey $ i*) (** Some facts and definitions concerning choice and description in intuitionistic logic. @@ -18,9 +19,11 @@ description principles (a "set-theoretic" axiom of choice) - AC_fun = functional form of the (non extensional) axiom of choice (a "type-theoretic" axiom of choice) +- DC_fun = functional form of the dependent axiom of choice +- ACw_fun = functional form of the countable axiom of choice - AC! = functional relation reification (known as axiom of unique choice in topos theory, - sometimes called principle of definite description in + 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 @@ -47,9 +50,9 @@ description principles We let also -IPL_2 = 2nd-order impredicative minimal predicate logic (with ex. quant.) -IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) -IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.) +- IPL_2 = 2nd-order impredicative minimal predicate logic (with ex. quant.) +- IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) +- IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.) with no prerequisite on the non-emptyness of domains @@ -73,6 +76,8 @@ Table of contents 7. Definite description transports classical logic to the computational world +8. Choice -> Dependent choice -> Countable choice + References: [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, @@ -81,7 +86,7 @@ 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 +[[Carlström05]] Jesper Carlström, Interpreting descriptions in intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. *) @@ -116,6 +121,20 @@ Definition FunctionalChoice_on := (forall x : A, exists y : B, R x y) -> (exists f : A->B, forall x : A, R x (f x)). +(** DC_fun *) + +Definition FunctionalDependentChoice_on := + forall (R:A->A->Prop), + (forall x, exists y, R x y) -> forall x0, + (exists f : nat -> A, f 0 = x0 /\ forall n, R (f n) (f (S n))). + +(** ACw_fun *) + +Definition FunctionalCountableChoice_on := + forall (R:nat->A->Prop), + (forall n, exists y, R n y) -> + (exists f : nat -> A, forall n, R n (f n)). + (** AC! or Functional Relation Reification (known as Axiom of Unique Choice in topos theory; also called principle of definite description *) @@ -126,7 +145,7 @@ Definition FunctionalRelReification_on := (** 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 + Carlström's type theory with a constructive indefinite description operator) *) Definition ConstructiveIndefiniteDescription_on := @@ -134,7 +153,7 @@ Definition ConstructiveIndefiniteDescription_on := (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 + with proof-irrelevance, it may be connected to Carlström's and Stenlund's type theory with a constructive definite description operator) *) @@ -146,16 +165,16 @@ Definition ConstructiveDefiniteDescription_on := (** GAC_rel *) -Definition GuardedRelationalChoice_on := +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, + (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, +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)). @@ -163,34 +182,34 @@ Definition GuardedFunctionalChoice_on := (** GFR_fun *) Definition GuardedFunctionalRelReification_on := - forall P : A->Prop, forall R : A->B->Prop, + 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 := +Definition OmniscientRelationalChoice_on := forall R : A->B->Prop, - exists 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, +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 EpsilonStatement_on := +Definition EpsilonStatement_on := forall P:A->Prop, inhabited A -> { x:A | (exists x, P x) -> P x }. (** D_iota *) -Definition IotaStatement_on := +Definition IotaStatement_on := forall P:A->Prop, inhabited A -> { x:A | (exists! x, P x) -> P x }. @@ -202,12 +221,16 @@ Notation RelationalChoice := (forall A B, RelationalChoice_on A B). Notation FunctionalChoice := (forall A B, FunctionalChoice_on A B). +Definition FunctionalDependentChoice := + (forall A, FunctionalDependentChoice_on A). +Definition FunctionalCountableChoice := + (forall A, FunctionalCountableChoice_on A). Notation FunctionalChoiceOnInhabitedSet := (forall A B, inhabited B -> FunctionalChoice_on A B). Notation FunctionalRelReification := (forall A B, FunctionalRelReification_on A B). -Notation GuardedRelationalChoice := +Notation GuardedRelationalChoice := (forall A B, GuardedRelationalChoice_on A B). Notation GuardedFunctionalChoice := (forall A B, GuardedFunctionalChoice_on A B). @@ -219,14 +242,14 @@ Notation OmniscientRelationalChoice := Notation OmniscientFunctionalChoice := (forall A B, OmniscientFunctionalChoice_on A B). -Notation ConstructiveDefiniteDescription := +Notation ConstructiveDefiniteDescription := (forall A, ConstructiveDefiniteDescription_on A). -Notation ConstructiveIndefiniteDescription := +Notation ConstructiveIndefiniteDescription := (forall A, ConstructiveIndefiniteDescription_on A). -Notation IotaStatement := +Notation IotaStatement := (forall A, IotaStatement_on A). -Notation EpsilonStatement := +Notation EpsilonStatement := (forall A, EpsilonStatement_on A). (** Subclassical schemes *) @@ -235,7 +258,7 @@ Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. Definition IndependenceOfGeneralPremises := - forall (A:Type) (P:A -> Prop) (Q:Prop), + forall (A:Type) (P:A -> Prop) (Q:Prop), inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x. @@ -270,7 +293,7 @@ Proof. apply HR'R; assumption. Qed. -Lemma funct_choice_imp_rel_choice : +Lemma funct_choice_imp_rel_choice : forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B. Proof. intros A B FunCh R H. @@ -283,7 +306,7 @@ Proof. trivial. Qed. -Lemma funct_choice_imp_description : +Lemma funct_choice_imp_description : forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B. Proof. intros A B FunCh R H. @@ -297,7 +320,7 @@ Proof. Qed. Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr : - forall A B, FunctionalChoice_on A B <-> + forall A B, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B. Proof. intros A B; split. @@ -312,7 +335,7 @@ Qed. (** We show that the guarded formulations of the axiom of choice are equivalent to their "omniscient" variant and comes from the non guarded - formulation in presence either of the independance of general premises + formulation in presence either of the independance of general premises or subset types (themselves derivable from subtypes thanks to proof- irrelevance) *) @@ -341,12 +364,12 @@ Proof. Qed. Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice : - forall A B, inhabited B -> RelationalChoice_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)). - intro x. apply IndPrem. exact Inh. intro Hx. + intro x. apply IndPrem. exact Inh. intro Hx. apply H; assumption. exists (fun x y => P x /\ R' x y). firstorder. @@ -385,7 +408,7 @@ 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. @@ -446,7 +469,7 @@ Proof. Qed. Lemma fun_choice_and_small_drinker_imp_omniscient_fun_choice : - FunctionalChoiceOnInhabitedSet -> SmallDrinker'sParadox + FunctionalChoiceOnInhabitedSet -> SmallDrinker'sParadox -> OmniscientFunctionalChoice. Proof. intros AC_fun Drinker A B R Inh. @@ -456,10 +479,10 @@ Proof. Qed. Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice : - FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox + FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox <-> OmniscientFunctionalChoice. Proof. - auto decomp using + auto decomp using omniscient_fun_choice_imp_small_drinker, omniscient_fun_choice_imp_fun_choice, fun_choice_and_small_drinker_imp_omniscient_fun_choice. @@ -510,7 +533,7 @@ Lemma constructive_indefinite_description_and_small_drinker_imp_epsilon : SmallDrinker'sParadox -> ConstructiveIndefiniteDescription -> EpsilonStatement. Proof. - intros Drinkers D_epsilon A P Inh; + intros Drinkers D_epsilon A P Inh; apply D_epsilon; apply Drinkers; assumption. Qed. @@ -542,7 +565,7 @@ Qed. 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 + relation with [nat] as codomain *) Require Import Wf_nat. @@ -552,10 +575,10 @@ 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, +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. @@ -563,7 +586,7 @@ Proof. 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 (dec_inh_nat_subset_has_unique_least_element (R x)). apply Rdec. apply (H x). exists f. @@ -582,12 +605,12 @@ Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) := (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 := +Notation DependentFunctionalChoice := (forall A (B:A->Type), DependentFunctionalChoice_on B). (** The easy part *) -Theorem dep_non_dep_functional_choice : +Theorem dep_non_dep_functional_choice : DependentFunctionalChoice -> FunctionalChoice. Proof. intros AC_depfun A B R H. @@ -606,12 +629,12 @@ 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 : +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)). + 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. @@ -633,7 +656,7 @@ Notation DependentFunctionalRelReification := (** The easy part *) -Theorem dep_non_dep_functional_rel_reification : +Theorem dep_non_dep_functional_rel_reification : DependentFunctionalRelReification -> FunctionalRelReification. Proof. intros DepFunReify A B R H. @@ -646,12 +669,12 @@ Qed. conjunction projections and dependent elimination of conjunction and equality *) -Theorem non_dep_dep_functional_rel_reification : +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)). + 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. @@ -665,7 +688,7 @@ Proof. destruct Heq using eq_indd; trivial. Qed. -Corollary dep_iff_non_dep_functional_rel_reification : +Corollary dep_iff_non_dep_functional_rel_reification : FunctionalRelReification <-> DependentFunctionalRelReification. Proof. auto decomp using @@ -764,7 +787,7 @@ be applied on the same Type universes on both sides of the first We adapt the proof to show that constructive definite description transports excluded-middle from [Prop] to [Set]. - [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos + [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag. *) @@ -786,14 +809,51 @@ Proof. intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction. left; trivial. right; trivial. -Qed. +Qed. Corollary fun_reification_descr_computational_excluded_middle_in_prop_context : FunctionalRelReification -> - (forall P:Prop, P \/ ~ P) -> + (forall P:Prop, P \/ ~ P) -> forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C. Proof. intros FunReify EM C; auto decomp using constructive_definite_descr_excluded_middle, (relative_non_contradiction_of_definite_descr (C:=C)). Qed. + +(**********************************************************************) +(** * Choice => Dependent choice => Countable choice *) + +(* The implications below are standard *) + +Require Import Arith. + +Theorem functional_choice_imp_functional_dependent_choice : + FunctionalChoice -> FunctionalDependentChoice. +Proof. + intros FunChoice A R HRfun x0. + apply FunChoice in HRfun as (g,Rg). + set (f:=fix f n := match n with 0 => x0 | S n' => g (f n') end). + exists f; firstorder. +Qed. + +Theorem functional_dependent_choice_imp_functional_countable_choice : + FunctionalDependentChoice -> FunctionalCountableChoice. +Proof. + intros H A R H0. + set (R' (p q:nat*A) := fst q = S (fst p) /\ R (fst p) (snd q)). + destruct (H0 0) as (y0,Hy0). + destruct H with (R:=R') (x0:=(0,y0)) as (f,(Hf0,HfS)). + intro x; destruct (H0 (fst x)) as (y,Hy). + exists (S (fst x),y). + red. auto. + assert (Heq:forall n, fst (f n) = n). + induction n. + rewrite Hf0; reflexivity. + specialize HfS with n; destruct HfS as (->,_); congruence. + exists (fun n => snd (f (S n))). + intro n'. specialize HfS with n'. + destruct HfS as (_,HR). + rewrite Heq in HR. + assumption. +Qed. diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 523c9245..1c2b97ce 100644 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id$ i*) (** Classical Logic *) diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index f9b59a6a..b0301994 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalChoice.v 10170 2007-10-03 14:41:25Z herbelin $ i*) +(*i $Id$ i*) (** This file provides classical logic and functional choice; this especially provides both indefinite descriptions and choice functions diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 31c41120..2b9df6d9 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalDescription.v 11481 2008-10-20 19:23:51Z herbelin $ i*) +(*i $Id$ i*) (** This file provides classical logic and definite description, which is equivalent to providing classical logic and Church's iota operator *) @@ -30,12 +30,12 @@ Axiom constructive_definite_description : Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}. Proof. -apply - (constructive_definite_descr_excluded_middle +apply + (constructive_definite_descr_excluded_middle constructive_definite_description classic). Qed. -Theorem classical_definite_description : +Theorem classical_definite_description : forall (A : Type) (P : A->Prop), inhabited A -> { x : A | (exists! x : A, P x) -> P x }. Proof. @@ -54,7 +54,7 @@ Qed. 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) : +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). diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 2a4de511..cee55dc8 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.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,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalEpsilon.v 10170 2007-10-03 14:41:25Z herbelin $ i*) +(*i $Id$ i*) (** This file provides classical logic and indefinite description under the form of Hilbert's epsilon operator *) @@ -22,11 +23,11 @@ Require Import ChoiceFacts. Set Implicit Arguments. Axiom constructive_indefinite_description : - forall (A : Type) (P : A->Prop), + forall (A : Type) (P : A->Prop), (exists x, P x) -> { x : A | P x }. Lemma constructive_definite_description : - forall (A : Type) (P : A->Prop), + forall (A : Type) (P : A->Prop), (exists! x, P x) -> { x : A | P x }. Proof. intros; apply constructive_indefinite_description; firstorder. @@ -34,18 +35,18 @@ Qed. Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}. Proof. - apply - (constructive_definite_descr_excluded_middle + apply + (constructive_definite_descr_excluded_middle constructive_definite_description classic). Qed. -Theorem classical_indefinite_description : +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 + apply constructive_indefinite_description with (P:= fun x => (exists x, P x) -> P x). destruct Hex as (x,Hx). exists x; intros _; exact Hx. @@ -60,7 +61,7 @@ Defined. 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) : +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). @@ -74,9 +75,9 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : (** 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) *) + (proof idea kindly provided by Pierre Castéran) *) -Lemma epsilon_inh_irrelevance : +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. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index db92696b..b22a3a87 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalFacts.v 11481 2008-10-20 19:23:51Z herbelin $ i*) +(*i $Id$ i*) (** Some facts and definitions about classical logic @@ -31,7 +31,7 @@ Table of contents: 3.1. Weak excluded middle -3.2. Gödel-Dummett axiom and right distributivity of implication over +3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction 3 3. Independence of general premises and drinker's paradox @@ -111,7 +111,7 @@ Qed. (** We successively show that: [prop_extensionality] - implies equality of [A] and [A->A] for inhabited [A], which + implies equality of [A] and [A->A] for inhabited [A], which implies the existence of a (trivial) retract from [A->A] to [A] (just take the identity), which implies the existence of a fixpoint operator in [A] @@ -128,7 +128,7 @@ Proof. apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ]. Qed. -Record retract (A B:Prop) : Prop := +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 : @@ -140,7 +140,7 @@ Proof. reflexivity. Qed. -Record has_fixpoint (A:Prop) : Prop := +Record has_fixpoint (A:Prop) : Prop := {F : (A -> A) -> A; Fix : forall f:A -> A, F f = f (F f)}. Lemma ext_prop_fixpoint : @@ -224,7 +224,7 @@ 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. @@ -233,10 +233,10 @@ Section Proof_irrelevance_Prop_Ext_CC. 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. @@ -248,7 +248,7 @@ End Proof_irrelevance_Prop_Ext_CC. (** Remark: [prop_extensionality] can be replaced in lemma [ext_prop_dep_proof_irrel_gen] by the weakest property - [provable_prop_extensionality]. + [provable_prop_extensionality]. *) (************************************************************************) @@ -260,7 +260,7 @@ End Proof_irrelevance_Prop_Ext_CC. *) Section Proof_irrelevance_CIC. - + Inductive boolP : Prop := | trueP : boolP | falseP : boolP. @@ -269,7 +269,7 @@ Section Proof_irrelevance_CIC. 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 => @@ -290,7 +290,7 @@ 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. *) @@ -316,7 +316,7 @@ 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. @@ -334,11 +334,11 @@ Section Proof_irrelevance_EM_CC. 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). @@ -392,13 +392,13 @@ 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) + + 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) + 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 @@ -417,7 +417,7 @@ End Proof_irrelevance_CCI. (** We show the following increasing in the strength of axioms: - weak excluded-middle - - right distributivity of implication over disjunction and Gödel-Dummett axiom + - right distributivity of implication over disjunction and Gödel-Dummett axiom - independence of general premises and drinker's paradox - excluded-middle *) @@ -436,20 +436,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 := +Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). -(** ** 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. *) @@ -473,7 +473,7 @@ Lemma Godel_Dummett_iff_right_distr_implication_over_disjunction : Proof. split. intros GD A B C HCAB. - destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC; + 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]. @@ -484,7 +484,7 @@ Qed. (** [(A->B) \/ (B->A)] is stronger than the weak excluded middle *) -Lemma Godel_Dummett_weak_excluded_middle : +Lemma Godel_Dummett_weak_excluded_middle : GodelDummett -> weak_excluded_middle. Proof. intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA]. @@ -500,13 +500,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 @@ -539,10 +539,10 @@ Qed. (** Independence of general premises is equivalent to the drinker's paradox *) Definition DrinkerParadox := - forall (A:Type) (P:A -> Prop), + forall (A:Type) (P:A -> Prop), inhabited A -> exists x, (exists x, P x) -> P x. -Lemma independence_general_premises_drinker : +Lemma independence_general_premises_drinker : IndependenceOfGeneralPremises <-> DrinkerParadox. Proof. split. @@ -551,14 +551,14 @@ Proof. exists x; intro HQ; apply (Hx (H HQ)). Qed. -(** Independence of general premises is weaker than (generalized) +(** Independence of general premises is weaker than (generalized) excluded middle Remark: generalized excluded middle is preferred here to avoid relying on the "ex falso quodlibet" property (i.e. [False -> forall A, A]) *) -Definition generalized_excluded_middle := +Definition generalized_excluded_middle := forall A B:Prop, A \/ (A -> B). Lemma excluded_middle_independence_general_premises : @@ -569,4 +569,4 @@ Proof. exists x; intro; exact Hx. exists x0; exact Hnot. Qed. - + diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index bb846aa6..f99d65eb 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.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,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalUniqueChoice.v 10170 2007-10-03 14:41:25Z herbelin $ i*) +(*i $Id$ i*) (** This file provides classical logic and unique choice; this is weaker than providing iota operator and classical logic as the @@ -15,11 +16,11 @@ be used to build functions outside the scope of a theorem proof) *) (** Classical logic and unique choice, as shown in - [ChicliPottierSimpson02], implies the double-negation of + [[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 + [[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. *) @@ -43,13 +44,14 @@ intros A B. apply (dependent_unique_choice A (fun _ => B)). Qed. -(** The following proof comes from [ChicliPottierSimpson02] *) +(** The following proof comes from [[ChicliPottierSimpson02]] *) Require Import Setoid. -Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False. +Theorem classic_set_in_prop_context : + forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C. Proof. -intro HnotEM. +intros C HnotEM. set (R := fun A b => A /\ true = b \/ ~ A /\ false = b). assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))). apply unique_choice. @@ -80,4 +82,12 @@ destruct (f P). discriminate. assumption. Qed. - + +Corollary not_not_classic_set : + ((forall P:Prop, {P} + {~ P}) -> False) -> False. +Proof. +apply classic_set_in_prop_context. +Qed. + +(* Compatibility *) +Notation classic_set := not_not_classic_set (only parsing). diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index 2a5f03ec..0b0c329b 100644 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Pred_Set.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id$ i*) (** This file is obsolete, use Classical_Pred_Type.v via Classical.v instead *) diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index 56ebf967..b30308af 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 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id$ i*) (** Classical Predicate Logic on Type *) @@ -44,7 +44,7 @@ Proof. (* Intuitionistic *) unfold not in |- *; intros P notex n abs. apply notex. exists n; trivial. -Qed. +Qed. Lemma not_ex_not_all : forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n. diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index ce3e84a7..df732959 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Prop.v 8892 2006-06-04 17:59:53Z herbelin $ i*) +(*i $Id$ i*) (** Classical Propositional Logic *) @@ -22,7 +22,7 @@ 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]. +(** 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 *) @@ -95,11 +95,11 @@ 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 +Ltac classical_right := match goal with | _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) end. -Ltac classical_left := match goal with +Ltac classical_left := match goal with | _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left]) end. @@ -107,7 +107,7 @@ Require Export EqdepFacts. Module Eq_rect_eq. -Lemma 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. diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index 9b1f4e19..3b91afd0 100644 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Type.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id$ i*) (** This file is obsolete, use Classical.v instead *) diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index ff70c9fb..6d22b1a9 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.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,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*) +(*i $Id$ i*) (** This module proves the constructive description schema, which infers the sigma-existence (i.e., [Set]-existence) of a witness to a diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 00d63252..c6d32d9b 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 11735 2009-01-02 17:22:31Z herbelin $ i*) +(*i $Id$ i*) (** Properties of decidable propositions *) @@ -13,7 +13,7 @@ Definition decidable (P:Prop) := P \/ ~ P. Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P. Proof. -unfold decidable; tauto. +unfold decidable; tauto. Qed. Theorem dec_True : decidable True. @@ -29,27 +29,27 @@ Qed. Theorem dec_or : forall A B:Prop, decidable A -> decidable B -> decidable (A \/ B). Proof. -unfold decidable; tauto. +unfold decidable; tauto. Qed. Theorem dec_and : forall A B:Prop, decidable A -> decidable B -> decidable (A /\ B). Proof. -unfold decidable; tauto. +unfold decidable; tauto. Qed. Theorem dec_not : forall A:Prop, decidable A -> decidable (~ A). Proof. -unfold decidable; tauto. +unfold decidable; tauto. Qed. Theorem dec_imp : forall A B:Prop, decidable A -> decidable B -> decidable (A -> B). Proof. -unfold decidable; tauto. +unfold decidable; tauto. Qed. -Theorem dec_iff : +Theorem dec_iff : forall A B:Prop, decidable A -> decidable B -> decidable (A<->B). Proof. unfold decidable; tauto. @@ -67,7 +67,7 @@ Qed. Theorem not_and : forall A B:Prop, decidable A -> ~ (A /\ B) -> ~ A \/ ~ B. Proof. -unfold decidable; tauto. +unfold decidable; tauto. Qed. Theorem not_imp : forall A B:Prop, decidable A -> ~ (A -> B) -> A /\ ~ B. @@ -80,16 +80,16 @@ Proof. unfold decidable; tauto. Qed. -Theorem not_iff : - forall A B:Prop, decidable A -> decidable B -> +Theorem not_iff : + forall A B:Prop, decidable A -> decidable B -> ~ (A <-> B) -> (A /\ ~ B) \/ (~ A /\ B). Proof. unfold decidable; tauto. Qed. -(** Results formulated with iff, used in FSetDecide. - Negation are expanded since it is unclear whether setoid rewrite - will always perform conversion. *) +(** Results formulated with iff, used in FSetDecide. + Negation are expanded since it is unclear whether setoid rewrite + will always perform conversion. *) (** We begin with lemmas that, when read from left to right, can be understood as ways to eliminate uses of [not]. *) diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v deleted file mode 100644 index a65e2c52..00000000 --- a/theories/Logic/DecidableType.v +++ /dev/null @@ -1,173 +0,0 @@ -(***********************************************************************) -(* 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 10616 2008-03-04 17:33:35Z letouzey $ *) - -Require Export SetoidList. -Set Implicit Arguments. -Unset Strict Implicit. - -(** * Types with Equalities, and nothing more (for subtyping purpose) *) - -Module Type EqualityType. - - Parameter Inline t : Type. - - Parameter Inline eq : t -> t -> Prop. - - Axiom eq_refl : forall x : t, eq x x. - Axiom eq_sym : forall x y : t, eq x y -> eq y x. - Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans. - -End EqualityType. - -(** * Types with decidable Equalities (but no ordering) *) - -Module Type DecidableType. - - Parameter Inline t : Type. - - Parameter Inline eq : t -> t -> Prop. - - Axiom eq_refl : forall x : t, eq x x. - Axiom eq_sym : forall x y : t, eq x y -> eq y x. - Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - - 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 : Type. - 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 deleted file mode 100644 index 9c59c519..00000000 --- a/theories/Logic/DecidableTypeEx.v +++ /dev/null @@ -1,109 +0,0 @@ -(***********************************************************************) -(* 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 11699 2008-12-18 11:49:08Z letouzey $ *) - -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 Inline t : Type. - 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 shortcut for easily building a UsualDecidableType *) - -Module Type MiniDecidableType. - Parameter Inline t : Type. - Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }. -End MiniDecidableType. - -Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. - Definition t:=M.t. - Definition eq := @eq t. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. - Definition eq_dec := M.eq_dec. -End Make_UDT. - -(** An OrderedType can now directly be seen as a DecidableType *) - -Module OT_as_DT (O:OrderedType) <: DecidableType := O. - -(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *) - -Module Nat_as_DT <: UsualDecidableType := Nat_as_OT. -Module Positive_as_DT <: UsualDecidableType := Positive_as_OT. -Module N_as_DT <: UsualDecidableType := N_as_OT. -Module Z_as_DT <: UsualDecidableType := Z_as_OT. - -(** From two decidable types, we can build a new DecidableType - over their cartesian product. *) - -Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. - - Definition t := prod D1.t D2.t. - - Definition eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y). - - Lemma eq_refl : forall x : t, eq x x. - Proof. - intros (x1,x2); red; simpl; auto. - Qed. - - Lemma eq_sym : forall x y : t, eq x y -> eq y x. - Proof. - intros (x1,x2) (y1,y2); unfold eq; simpl; intuition. - Qed. - - Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - Proof. - intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. - Qed. - - Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. - Proof. - intros (x1,x2) (y1,y2); unfold eq; simpl. - destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); intuition. - Defined. - -End PairDecidableType. - -(** Similarly for pairs of UsualDecidableType *) - -Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. - Definition t := prod D1.t D2.t. - Definition eq := @eq t. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. - Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. - Proof. - intros (x1,x2) (y1,y2); - destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); - unfold eq, D1.eq, D2.eq in *; simpl; - (left; f_equal; auto; fail) || - (right; intro H; injection H; auto). - Defined. - -End PairUsualDecidableType. diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v index 962f2a2a..a8a56ae7 100644 --- a/theories/Logic/Description.v +++ b/theories/Logic/Description.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Description.v 10170 2007-10-03 14:41:25Z herbelin $ i*) +(*i $Id$ i*) (** This file provides a constructive form of definite description; it allows to build functions from the proof of their existence in any @@ -17,5 +17,5 @@ Require Import ChoiceFacts. Set Implicit Arguments. Axiom constructive_definite_description : - forall (A : Type) (P : A->Prop), + forall (A : Type) (P : A->Prop), (exists! x, P x) -> { x : A | P x }. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index b935a676..18f3181b 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 11481 2008-10-20 19:23:51Z herbelin $ i*) +(*i $Id$ i*) (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show @@ -59,7 +59,7 @@ Definition PredicateExtensionality := Require Import ClassicalFacts. Variable pred_extensionality : PredicateExtensionality. - + Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B. Proof. intros A B H. @@ -99,11 +99,11 @@ Lemma AC_bool_subset_to_bool : (exists b : bool, P b) -> exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')). Proof. - destruct (guarded_rel_choice _ _ + 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. + exists R; intros P HP. destruct (HR P HP) as (y,(Hy,Huni)). exists y; firstorder. Qed. @@ -190,7 +190,7 @@ Lemma projT1_injective : a1=a2 -> a1'=a2'. Proof. intro Heq ; unfold a1', a2', A'. rewrite Heq. - replace (or_introl (a2=a2) (refl_equal a2)) + replace (or_introl (a2=a2) (refl_equal a2)) with (or_intror (a2=a2) (refl_equal a2)). reflexivity. apply proof_irrelevance. @@ -210,10 +210,10 @@ Qed. Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2. Proof. - destruct - (rel_choice A' bool + destruct + (rel_choice A' bool (fun x y => projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false)) - as (R,(HRsub,HR)). + as (R,(HRsub,HR)). apply decide. destruct (HR a1') as (b1,(Ha1'b1,_Huni1)). destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)]. @@ -235,18 +235,18 @@ 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 -> + 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 + assert (guarded_rel_choice := + rel_choice_and_proof_irrel_imp_guarded_rel_choice + rel_choice proof_irrelevance). - destruct - (guarded_rel_choice A bool + 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)). + as (R,(HRsub,HR)). apply decide. destruct (HR a1) as (b1,(Ha1b1,_Huni1)). left; reflexivity. destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)]. @@ -273,8 +273,8 @@ 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), +Hypothesis epsilon_spec : + forall (A:Type) (i:inhabited A) (P:A->Prop), (exists x, P x) -> P (epsilon A i P). Hypothesis epsilon_extensionality : @@ -288,9 +288,9 @@ Proof. intro P. pose (B := fun y => y=false \/ P). pose (C := fun y => y=true \/ P). - assert (B (eps B)) as [Hfalse|HP] + assert (B (eps B)) as [Hfalse|HP] by (apply epsilon_spec; exists false; left; reflexivity). - assert (C (eps C)) as [Htrue|HP] + 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). diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v index 65d4d853..d433be94 100644 --- a/theories/Logic/Epsilon.v +++ b/theories/Logic/Epsilon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Epsilon.v 10170 2007-10-03 14:41:25Z herbelin $ i*) +(*i $Id$ i*) (** This file provides indefinite description under the form of Hilbert's epsilon operator; it does not assume classical logic. *) @@ -17,12 +17,12 @@ Set Implicit Arguments. (** Hilbert's epsilon: operator and specification in one statement *) -Axiom epsilon_statement : +Axiom epsilon_statement : forall (A : Type) (P : A->Prop), inhabited A -> { x : A | (exists x, P x) -> P x }. Lemma constructive_indefinite_description : - forall (A : Type) (P : A->Prop), + forall (A : Type) (P : A->Prop), (exists x, P x) -> { x : A | P x }. Proof. apply epsilon_imp_constructive_indefinite_description. @@ -45,7 +45,7 @@ Proof. Qed. Lemma constructive_definite_description : - forall (A : Type) (P : A->Prop), + forall (A : Type) (P : A->Prop), (exists! x, P x) -> { x : A | P x }. Proof. apply iota_imp_constructive_definite_description. @@ -57,7 +57,7 @@ Qed. Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A := proj1_sig (epsilon_statement P i). -Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : +Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : (exists x, P x) -> P (epsilon i P) := proj2_sig (epsilon_statement P i). @@ -66,7 +66,7 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A := proj1_sig (iota_statement P i). -Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : +Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : (exists! x:A, P x) -> P (iota i P) := proj2_sig (iota_statement P i). diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 2fe9d1a6..5c6b4e89 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.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,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id$ i*) (** This file axiomatizes the invariance by substitution of reflexive equality proofs [[Streicher93]] and exports its consequences, such diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index d5738c82..4689fb46 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.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,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqdepFacts.v 11735 2009-01-02 17:22:31Z herbelin $ i*) +(*i $Id$ i*) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives @@ -25,7 +26,7 @@ References: [1] T. Streicher, Semantical Investigations into Intensional Type Theory, - Habilitationsschrift, LMU München, 1993. + 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 @@ -45,7 +46,7 @@ Table of contents: (** * Definition of dependent equality and equivalence with equality of dependent pairs *) Section Dependent_Equality. - + Variable U : Type. Variable P : U -> Type. @@ -119,7 +120,7 @@ Lemma equiv_eqex_eqdep : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), existT P p x = existT P q y <-> eq_dep p x q y. Proof. - split. + split. (* -> *) apply eq_sigT_eq_dep. (* <- *) @@ -142,27 +143,27 @@ Hint Immediate eq_dep_sym: core. (** * Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K *) Section Equivalences. - + Variable U:Type. - + (** Invariance by Substitution of Reflexive Equality Proofs *) - - Definition Eq_rect_eq := + + 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 := + + 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_ := + + Definition UIP_ := forall (x y:U) (p1 p2:x = y), p1 = p2. - + (** Uniqueness of Reflexive Identity Proofs *) - Definition UIP_refl_ := + Definition UIP_refl_ := forall (x:U) (p:x = x), p = refl_equal x. (** Streicher's axiom K *) @@ -198,7 +199,7 @@ Section Equivalences. 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_. @@ -216,7 +217,7 @@ Section Equivalences. (** 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. @@ -233,20 +234,20 @@ Section Equivalences. 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]. + 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. @@ -260,7 +261,7 @@ End Corollaries. Notation Inj_dep_pairS := Inj_dep_pair. Notation Inj_dep_pairT := Inj_dep_pair. Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2. - + (************************************************************************) (** * Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *) @@ -274,11 +275,11 @@ Module Type EqdepElimination. End EqdepElimination. Module EqdepTheory (M:EqdepElimination). - + 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 0281916e..fc1c4a97 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 10144 2007-09-26 15:12:17Z vsiles $ i*) +(*i $Id$ 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. @@ -38,7 +38,7 @@ 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. @@ -49,7 +49,7 @@ Section EqdepDec. Qed. Variable eq_dec : forall x y:A, x = y \/ x <> y. - + Variable x : A. Let nu (y:A) (u:x = y) : x = y := @@ -63,13 +63,13 @@ Section EqdepDec. 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. Proof. @@ -88,7 +88,7 @@ Section EqdepDec. reflexivity. Qed. - Theorem K_dec : + Theorem K_dec : forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p. Proof. intros. @@ -118,10 +118,10 @@ Section EqdepDec. case (eq_dec x x). intro e. elim e using K_dec; trivial. - + intros. case n; trivial. - + case H. reflexivity. Qed. @@ -165,6 +165,12 @@ Theorem eq_dep_eq_dec : forall (P:A->Type) (p:A) (x y:P p), eq_dep A P p x p y -> x = y. Proof (fun A eq_dec => eq_rect_eq__eq_dep_eq A (eq_rect_eq_dec eq_dec)). +Theorem UIP_dec : + forall (A:Type), + (forall x y:A, {x = y} + {x <> y}) -> + forall (x y:A) (p1 p2:x = y), p1 = p2. +Proof (fun A eq_dec => eq_dep_eq__UIP A (eq_dep_eq_dec eq_dec)). + Unset Implicit Arguments. (************************************************************************) @@ -173,13 +179,13 @@ Unset Implicit Arguments. (** 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 +(** The module [DecidableEqDep] collects equality properties for decidable set in [Type] *) Module DecidableEqDep (M:DecidableType). @@ -247,7 +253,7 @@ Module Type DecidableSet. End DecidableSet. -(** The module [DecidableEqDepSet] collects equality properties for decidable +(** The module [DecidableEqDepSet] collects equality properties for decidable set in [Set] *) Module DecidableEqDepSet (M:DecidableSet). @@ -307,11 +313,11 @@ End DecidableEqDepSet. (** From decidability to inj_pair2 **) Lemma inj_pair2_eq_dec : forall A:Type, (forall x y:A, {x=y}+{x<>y}) -> ( forall (P:A -> Type) (p:A) (x y:P p), existT P p x = existT P p y -> x = y ). -Proof. +Proof. intros A eq_dec. apply eq_dep_eq__inj_pair2. apply eq_rect_eq__eq_dep_eq. - unfold Eq_rect_eq. + unfold Eq_rect_eq. apply eq_rect_eq_dec. apply eq_dec. Qed. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 0dc82907..1678a287 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: FunctionalExtensionality.v 11686 2008-12-16 12:57:26Z msozeau $ i*) +(*i $Id$ i*) (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *) (** The converse of functional extensionality. *) -Lemma equal_f : forall {A B : Type} {f g : A -> B}, +Lemma equal_f : forall {A B : Type} {f g : A -> B}, f = g -> forall x, f x = g x. Proof. intros. @@ -23,11 +23,11 @@ Qed. (** Statements of functional extensionality for simple and dependent functions. *) -Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, - forall (f g : forall x : A, B x), +Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, + forall (f g : forall x : A, B x), (forall x, f x = g x) -> f = g. -Lemma functional_extensionality {A B} (f g : A -> B) : +Lemma functional_extensionality {A B} (f g : A -> B) : (forall x, f x = g x) -> f = g. Proof. intros ; eauto using @functional_extensionality_dep. @@ -37,8 +37,8 @@ Qed. Tactic Notation "extensionality" ident(x) := match goal with - [ |- ?X = ?Y ] => - (apply (@functional_extensionality _ _ X Y) || + [ |- ?X = ?Y ] => + (apply (@functional_extensionality _ _ X Y) || apply (@functional_extensionality_dep _ _ X Y)) ; intro x end. @@ -51,8 +51,8 @@ Proof. extensionality x. reflexivity. Qed. - + Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x. Proof. - intros A B f. apply (eta_expansion_dep f). + apply (eta_expansion_dep f). Qed. diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 46a57432..71c9af50 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -19,7 +19,7 @@ and Applications (TLCA'95), 1995. - [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001 - (see www.cs.kun.nl/~herman/note.ps.gz). + (see http://www.cs.kun.nl/~herman/note.ps.gz). *) Section Paradox. diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v index 740b889a..3651c1b2 100644 --- a/theories/Logic/IndefiniteDescription.v +++ b/theories/Logic/IndefiniteDescription.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: IndefiniteDescription.v 10170 2007-10-03 14:41:25Z herbelin $ i*) +(*i $Id$ i*) (** This file provides a constructive form of indefinite description that allows to build choice functions; this is weaker than Hilbert's @@ -19,11 +19,11 @@ Require Import ChoiceFacts. Set Implicit Arguments. Axiom constructive_indefinite_description : - forall (A : Type) (P : A->Prop), + forall (A : Type) (P : A->Prop), (exists x, P x) -> { x : A | P x }. Lemma constructive_definite_description : - forall (A : Type) (P : A->Prop), + forall (A : Type) (P : A->Prop), (exists! x, P x) -> { x : A | P x }. Proof. intros; apply constructive_indefinite_description; firstorder. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index c3573ac3..fc4555a4 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 9849 2007-05-22 20:40:04Z herbelin $ i*) +(*i $Id$ i*) (** John Major's Equality as proposed by Conor McBride @@ -28,44 +28,61 @@ Set Elimination Schemes. Hint Resolve JMeq_refl. -Lemma sym_JMeq : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. +Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. +Proof. destruct 1; trivial. Qed. -Hint Immediate sym_JMeq. +Hint Immediate JMeq_sym. -Lemma trans_JMeq : +Lemma JMeq_trans : forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z. -destruct 1; trivial. +Proof. +destruct 2; trivial. Qed. Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = 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. +Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq x y -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. Qed. -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. +Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set), + P x -> forall y, JMeq x y -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. Qed. -Lemma JMeq_rect : forall (A:Type) (x 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. +Lemma JMeq_rect : forall (A:Type) (x:A) (P:A->Type), + P x -> forall y, JMeq x y -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. +Qed. + +Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq y x -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial. Qed. -Lemma JMeq_ind_r : - 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. +Lemma JMeq_rec_r : forall (A:Type) (x:A) (P:A -> Set), + P x -> forall y, JMeq y x -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial. Qed. -Lemma JMeq_rec_r : - 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. +Lemma JMeq_rect_r : forall (A:Type) (x:A) (P:A -> Type), + P x -> forall y, JMeq y x -> P y. +Proof. +intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial. Qed. -Lemma JMeq_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. +Lemma JMeq_congr : + forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y. +Proof. +intros A x B f y H; case JMeq_eq with (1 := H); trivial. Qed. (** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *) @@ -107,3 +124,21 @@ intro H. assert (true=false) by (destruct H; reflexivity). discriminate. Qed. + +(** However, when the dependencies are equal, [JMeq (P p) x (P q) y] + is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *) + +Lemma JMeq_eq_dep : + forall U (P:U->Prop) p q (x:P p) (y:P q), + p = q -> JMeq x y -> eq_dep U P p x q y. +Proof. +intros. +destruct H. +apply JMeq_eq in H0 as ->. +reflexivity. +Qed. + + +(* Compatibility *) +Notation sym_JMeq := JMeq_sym (only parsing). +Notation trans_JMeq := JMeq_trans (only parsing). diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v index dd3178eb..4c48d95c 100644 --- a/theories/Logic/ProofIrrelevanceFacts.v +++ b/theories/Logic/ProofIrrelevanceFacts.v @@ -21,8 +21,8 @@ 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), + 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). diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index ec168f09..49fa1222 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RelationalChoice.v 8892 2006-06-04 17:59:53Z herbelin $ i*) +(*i $Id$ 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, + exists R' : A->B->Prop, subrelation R' R /\ forall x : A, exists! y : B, R' x y. diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget new file mode 100644 index 00000000..46046897 --- /dev/null +++ b/theories/Logic/vo.itarget @@ -0,0 +1,28 @@ +Berardi.vo +ChoiceFacts.vo +ClassicalChoice.vo +ClassicalDescription.vo +ClassicalEpsilon.vo +ClassicalFacts.vo +Classical_Pred_Set.vo +Classical_Pred_Type.vo +Classical_Prop.vo +Classical_Type.vo +ClassicalUniqueChoice.vo +Classical.vo +ConstructiveEpsilon.vo +Decidable.vo +Description.vo +Diaconescu.vo +Epsilon.vo +Eqdep_dec.vo +EqdepFacts.vo +Eqdep.vo +FunctionalExtensionality.vo +Hurkens.vo +IndefiniteDescription.vo +JMeq.vo +ProofIrrelevanceFacts.vo +ProofIrrelevance.vo +RelationalChoice.vo +SetIsType.vo |