From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Logic/Berardi.v | 6 +- theories/Logic/ChoiceFacts.v | 94 +++++++++++++++---------------- theories/Logic/ClassicalDescription.v | 8 +-- theories/Logic/ClassicalEpsilon.v | 16 +++--- theories/Logic/ClassicalFacts.v | 48 ++++++++-------- theories/Logic/ClassicalUniqueChoice.v | 2 +- theories/Logic/Classical_Pred_Type.v | 2 +- theories/Logic/Classical_Prop.v | 8 +-- theories/Logic/Decidable.v | 24 ++++---- theories/Logic/DecidableType.v | 26 ++++----- theories/Logic/DecidableTypeEx.v | 24 ++++---- theories/Logic/Description.v | 2 +- theories/Logic/Diaconescu.v | 36 ++++++------ theories/Logic/Epsilon.v | 10 ++-- theories/Logic/EqdepFacts.v | 50 ++++++++-------- theories/Logic/Eqdep_dec.v | 24 ++++---- theories/Logic/FunctionalExtensionality.v | 14 ++--- theories/Logic/IndefiniteDescription.v | 4 +- theories/Logic/JMeq.v | 6 +- theories/Logic/ProofIrrelevanceFacts.v | 4 +- theories/Logic/RelationalChoice.v | 2 +- 21 files changed, 205 insertions(+), 205 deletions(-) (limited to 'theories/Logic') diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 27e375f62..5b2f5063b 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -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 3f4c4354b..32880b2f7 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -20,7 +20,7 @@ description principles (a "type-theoretic" axiom of choice) - AC! = functional relation reification (known as axiom of unique choice in topos theory, - sometimes called principle of definite description in + 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 @@ -146,16 +146,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 +163,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 }. @@ -207,7 +207,7 @@ Notation FunctionalChoiceOnInhabitedSet := 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 +219,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 +235,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 +270,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 +283,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 +297,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 +312,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 +341,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 +385,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 +446,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 +456,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 +510,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 +542,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 +552,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 +563,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 +582,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 +606,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 +633,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 +646,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 +665,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 @@ -786,11 +786,11 @@ 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 diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index dad60fb77..2b9df6d97 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -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 c45aeb6f9..0d65a89ba 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -22,11 +22,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 +34,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 +60,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). @@ -76,7 +76,7 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : the actual proof that the domain of [P] is inhabited (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 d4ba4a3a7..9ec916a7d 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -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 => @@ -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 @@ -438,7 +438,7 @@ Definition weak_excluded_middle := [weak_generalized_excluded_middle] is that it holds even in logic without a primitive [False] connective (like Gödel-Dummett axiom) *) -Definition weak_generalized_excluded_middle := +Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). (** ** Gödel-Dummett axiom *) @@ -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]. @@ -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 2e739dd51..c1f9881fa 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -80,4 +80,4 @@ destruct (f P). discriminate. assumption. Qed. - + diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index ce94bec14..b30308af5 100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -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 8d2e946de..df732959f 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -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/Decidable.v b/theories/Logic/Decidable.v index 6129128de..c6d32d9be 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -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 index fed25ad74..625f776bf 100644 --- a/theories/Logic/DecidableType.v +++ b/theories/Logic/DecidableType.v @@ -14,7 +14,7 @@ Unset Strict Implicit. (** * Types with Equalities, and nothing more (for subtyping purpose) *) -Module Type EqualityType. +Module Type EqualityType. Parameter Inline t : Type. @@ -27,11 +27,11 @@ Module Type EqualityType. Hint Immediate eq_sym. Hint Resolve eq_refl eq_trans. -End EqualityType. +End EqualityType. (** * Types with decidable Equalities (but no ordering) *) -Module Type DecidableType. +Module Type DecidableType. Parameter Inline t : Type. @@ -46,7 +46,7 @@ Module Type DecidableType. Hint Immediate eq_sym. Hint Resolve eq_refl eq_trans. -End DecidableType. +End DecidableType. (** * Additional notions about keys and datas used in FMap *) @@ -58,21 +58,21 @@ Module KeyDecidableType(D:DecidableType). Notation key:=t. Definition eqk (p p':key*elt) := eq (fst p) (fst p'). - Definition eqke (p p':key*elt) := + 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. @@ -96,7 +96,7 @@ Module KeyDecidableType(D:DecidableType). Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. Hint Immediate eqk_sym eqke_sym. - Lemma InA_eqke_eqk : + Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. unfold eqke; induction 1; intuition. @@ -134,22 +134,22 @@ Module KeyDecidableType(D:DecidableType). 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. + 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. + Qed. - Lemma In_inv_2 : forall k k' e e' l, + 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. + Proof. inversion_clear 1; compute in H0; intuition. Qed. - Lemma In_inv_3 : forall x x' l, + 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. diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v index 57a2248b3..022102f70 100644 --- a/theories/Logic/DecidableTypeEx.v +++ b/theories/Logic/DecidableTypeEx.v @@ -14,7 +14,7 @@ Unset Strict Implicit. (** * Examples of Decidable Type structures. *) -(** A particular case of [DecidableType] where +(** A particular case of [DecidableType] where the equality is the usual one of Coq. *) Module Type UsualDecidableType. @@ -32,13 +32,13 @@ Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. (** an shortcut for easily building a UsualDecidableType *) -Module Type MiniDecidableType. +Module Type MiniDecidableType. Parameter Inline t : Type. Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }. -End MiniDecidableType. +End MiniDecidableType. Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. - Definition t:=M.t. + Definition t:=M.t. Definition eq := @eq t. Definition eq_refl := @refl_equal t. Definition eq_sym := @sym_eq t. @@ -57,7 +57,7 @@ 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 +(** From two decidable types, we can build a new DecidableType over their cartesian product. *) Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. @@ -67,17 +67,17 @@ Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. 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. + Proof. intros (x1,x2); red; simpl; auto. Qed. Lemma eq_sym : forall x y : t, eq x y -> eq y x. - Proof. + 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. + Proof. intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. Qed. @@ -99,10 +99,10 @@ Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. 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) || + 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. diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v index 41cde8aa5..a8a56ae74 100644 --- a/theories/Logic/Description.v +++ b/theories/Logic/Description.v @@ -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 95a07f2f3..18f3181b6 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -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 ead91c9ec..d433be944 100644 --- a/theories/Logic/Epsilon.v +++ b/theories/Logic/Epsilon.v @@ -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/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 74d9726a6..a4b4b5b4a 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -45,7 +45,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 +119,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 +142,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 +198,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 +216,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 +233,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 +260,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 +274,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 1943c1629..c7cb9b0d4 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -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. @@ -173,13 +173,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 +247,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 +307,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 31b633c25..bf29c63dd 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -13,7 +13,7 @@ (** 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,7 +51,7 @@ 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). diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v index ce9405f85..3651c1b2f 100644 --- a/theories/Logic/IndefiniteDescription.v +++ b/theories/Logic/IndefiniteDescription.v @@ -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 7d9e11296..127be1134 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -43,13 +43,13 @@ Qed. Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. -Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), +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:A) (P:A -> Set), +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. @@ -61,7 +61,7 @@ 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), +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. diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v index dd3178ebe..4c48d95cd 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 9ad6b7220..49fa12224 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -13,5 +13,5 @@ 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. -- cgit v1.2.3