From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Jun 2016 19:12:49 -0400 Subject: Add transparent_abstract tactic --- theories/Init/Prelude.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories') diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index c58d23dad0..e71a8774ed 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -23,4 +23,4 @@ Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". Declare ML Module "recdef_plugin". (* Default substrings not considered by queries like SearchAbout *) -Add Search Blacklist "_subproof" "Private_". +Add Search Blacklist "_subproof" "_subterm" "Private_". -- cgit v1.2.3 From fdd5a8452bd2da22ffd1cab3b1888f2261f193b9 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Sun, 30 Apr 2017 13:10:48 +0200 Subject: Functional choice <-> [inhabited] and [forall] commute --- theories/Init/Logic.v | 5 +++++ theories/Init/Specif.v | 11 +++++++++++ theories/Logic/ChoiceFacts.v | 33 +++++++++++++++++++++++++++++++++ 3 files changed, 49 insertions(+) (limited to 'theories') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9ae9dde28d..3eefe9a849 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -609,6 +609,11 @@ Proof. destruct 1; auto. Qed. +Lemma inhabited_covariant (A B : Type) : (A -> B) -> inhabited A -> inhabited B. +Proof. + intros f [x];exact (inhabits (f x)). +Qed. + (** Declaration of stepl and stepr for eq and iff *) Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2cc2ecbc20..43a441fc51 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -207,6 +207,17 @@ Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). Proof. destruct p; reflexivity. Defined. +(** [exists x : A, B] is equivalent to [inhabited {x : A | B}] *) +Lemma exists_to_inhabited_sig {A P} : (exists x : A, P x) -> inhabited {x : A | P x}. +Proof. + intros [x y]. exact (inhabits (exist _ x y)). +Qed. + +Lemma inhabited_sig_to_exists {A P} : inhabited {x : A | P x} -> exists x : A, P x. +Proof. + intros [[x y]];exists x;exact y. +Qed. + (** [sumbool] is a boolean type equipped with the justification of their value *) diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 07e8b6ef8d..f1f20606b1 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -760,6 +760,39 @@ Proof. destruct Heq using eq_indd; trivial. Qed. +(** Functional choice can be reformulated as a property on [inhabited] *) + +Definition InhabitedForallCommute_on (A : Type) (B : A -> Type) := + (forall x, inhabited (B x)) -> inhabited (forall x, B x). + +Notation InhabitedForallCommute := + (forall A (B : A -> Type), InhabitedForallCommute_on B). + +Theorem functional_choice_to_inhabited_forall_commute : + FunctionalChoice -> InhabitedForallCommute. +Proof. + intros choose0 A B Hinhab. + pose proof (non_dep_dep_functional_choice choose0) as choose;clear choose0. + assert (Hexists : forall x, exists _ : B x, True). + { intros x;apply inhabited_sig_to_exists. + refine (inhabited_covariant _ (Hinhab x)). + intros y;exists y;exact I. } + apply choose in Hexists. + destruct Hexists as [f _]. + exact (inhabits f). +Qed. + +Theorem inhabited_forall_commute_to_functional_choice : + InhabitedForallCommute -> FunctionalChoice. +Proof. + intros choose A B R Hexists. + assert (Hinhab : forall x, inhabited {y : B | R x y}). + { intros x;apply exists_to_inhabited_sig;trivial. } + apply choose in Hinhab. destruct Hinhab as [f]. + exists (fun x => proj1_sig (f x)). + exact (fun x => proj2_sig (f x)). +Qed. + (** ** Reification of dependent and non dependent functional relation are equivalent *) Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := -- cgit v1.2.3 From 8adfa0e5290056b7683a3a8b778ca16182a1eb3d Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Tue, 2 May 2017 14:43:32 +0200 Subject: Reorganize comment documentation of ChoiceFacts.v Shortnames and natural language descriptions of principles are moved next to each principle. The table of contents is moved to after the principle definitions. Extra definitions are moved to the definition section (eg DependentFunctionalChoice) Compatibility notations have been moved to the end of the file. Details: The following used to be announced but were neither defined or used, and have been removed: - OAC! - Ext_pred = extensionality of predicates - Ext_fun_prop_repr = choice of a representative among extensional functions to Prop GuardedFunctionalRelReification was announced with shortname GAC! but shortname GFR_fun was used next to it. Only the former has been retained. Shortnames and descriptions have been invented for InhabitedForallCommute DependentFunctionalRelReification ExtensionalPropositionRepresentative ExtensionalFunctionRepresentative Some modification of headlines --- theories/Logic/ChoiceFacts.v | 283 ++++++++++++++++++++----------------------- 1 file changed, 131 insertions(+), 152 deletions(-) (limited to 'theories') diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index f1f20606b1..116897f4ce 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -8,94 +8,9 @@ (************************************************************************) (** Some facts and definitions concerning choice and description in - intuitionistic logic. - -We investigate the relations between the following choice and -description principles - -- AC_rel = relational form of the (non extensional) axiom of choice - (a "set-theoretic" axiom of choice) -- AC_fun = functional form of the (non extensional) axiom of choice - (a "type-theoretic" axiom of choice) -- DC_fun = functional form of the dependent axiom of choice -- ACw_fun = functional form of the countable axiom of choice -- AC! = functional relation reification - (known as axiom of unique choice in topos theory, - sometimes called principle of definite description in - the context of constructive type theory, sometimes - called axiom of no choice) - -- AC_fun_repr = functional choice of a representative in an equivalence class -- AC_fun_setoid_gen = functional form of the general form of the (so-called - extensional) axiom of choice over setoids -- AC_fun_setoid = functional form of the (so-called extensional) axiom of - choice from setoids -- AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of - choice from setoids on locally compatible relations - -- GAC_rel = guarded relational form of the (non extensional) axiom of choice -- GAC_fun = guarded functional form of the (non extensional) axiom of choice -- GAC! = guarded functional relation reification - -- OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice -- OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice - (called AC* in Bell [[Bell]]) -- OAC! - -- ID_iota = intuitionistic definite description -- ID_epsilon = intuitionistic indefinite description - -- D_iota = (weakly classical) definite description principle -- D_epsilon = (weakly classical) indefinite description principle - -- PI = proof irrelevance -- IGP = independence of general premises - (an unconstrained generalisation of the constructive principle of - independence of premises) -- Drinker = drinker's paradox (small form) - (called Ex in Bell [[Bell]]) -- EM = excluded-middle - -- Ext_pred_repr = choice of a representative among extensional predicates -- Ext_pred = extensionality of predicates -- Ext_fun_prop_repr = choice of a representative among extensional functions to Prop - -We let also - -- IPL_2 = 2nd-order impredicative minimal predicate logic (with ex. quant.) -- IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) -- IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.) - -with no prerequisite on the non-emptiness of domains - -Table of contents - -1. Definitions - -2. IPL_2^2 |- AC_rel + AC! = AC_fun - -3.1. typed IPL_2 + Sigma-types + PI |- AC_rel = GAC_rel and IPL_2 |- AC_rel + IGP -> GAC_rel and IPL_2 |- GAC_rel = OAC_rel - -3.2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker - -3.3. D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker - -4. Derivability of choice for decidable relations with well-ordered codomain - -5. Equivalence of choices on dependent or non dependent functional types - -6. Non contradiction of constructive descriptions wrt functional choices - -7. Definite description transports classical logic to the computational world - -8. Choice -> Dependent choice -> Countable choice - -9.1. AC_fun_ext = AC_fun + Ext_fun_repr + EM - -9.2. AC_fun_ext = AC_fun + Ext_prop_fun_repr + PI - -References: - + intuitionistic logic. *) +(** * References: *) +(** [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, unpublished. @@ -133,47 +48,75 @@ Variable P:A->Prop. (** ** Constructive choice and description *) -(** AC_rel *) +(** AC_rel = relational form of the (non extensional) axiom of choice + (a "set-theoretic" axiom of choice) *) Definition RelationalChoice_on := forall R:A->B->Prop, (forall x : A, exists y : B, R x y) -> (exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y). -(** AC_fun *) +(** AC_fun = functional form of the (non extensional) axiom of choice + (a "type-theoretic" axiom of choice) *) (* Note: This is called Type-Theoretic Description Axiom (TTDA) in [[Werner97]] (using a non-standard meaning of "description"). This is called intensional axiom of choice (AC_int) in [[Carlström04]] *) +Definition FunctionalChoice_on_rel (R:A->B->Prop) := + (forall x:A, exists y : B, R x y) -> + exists f : A -> B, (forall x:A, R x (f x)). + Definition FunctionalChoice_on := forall R:A->B->Prop, (forall x : A, exists y : B, R x y) -> (exists f : A->B, forall x : A, R x (f x)). -(** DC_fun *) +(** AC_fun_dep = functional form of the (non extensional) axiom of + choice, with dependent functions *) +Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) := + forall R:forall x:A, B x -> Prop, + (forall x:A, exists y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). + +(** AC_trunc = axiom of choice for propositional truncations + (truncation and quantification commute) *) +Definition InhabitedForallCommute_on (A : Type) (B : A -> Type) := + (forall x, inhabited (B x)) -> inhabited (forall x, B x). + +(** DC_fun = functional form of the dependent axiom of choice *) Definition FunctionalDependentChoice_on := forall (R:A->A->Prop), (forall x, exists y, R x y) -> forall x0, (exists f : nat -> A, f 0 = x0 /\ forall n, R (f n) (f (S n))). -(** ACw_fun *) +(** ACw_fun = functional form of the countable axiom of choice *) Definition FunctionalCountableChoice_on := forall (R:nat->A->Prop), (forall n, exists y, R n y) -> (exists f : nat -> A, forall n, R n (f n)). -(** AC! or Functional Relation Reification (known as Axiom of Unique Choice - in topos theory; also called principle of definite description *) +(** AC! = functional relation reification + (known as axiom of unique choice in topos theory, + sometimes called principle of definite description in + the context of constructive type theory, sometimes + called axiom of no choice) *) Definition FunctionalRelReification_on := forall R:A->B->Prop, (forall x : A, exists! y : B, R x y) -> (exists f : A->B, forall x : A, R x (f x)). -(** AC_fun_repr *) +(** AC_dep! = functional relation reification, with dependent functions + see AC! *) +Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := + forall (R:forall x:A, B x -> Prop), + (forall x:A, exists! y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). + +(** AC_fun_repr = functional choice of a representative in an equivalence class *) (* Note: This is called Type-Theoretic Choice Axiom (TTCA) in [[Werner97]] (by reference to the extensional set-theoretic @@ -187,7 +130,8 @@ Definition RepresentativeFunctionalChoice_on := (Equivalence R) -> (exists f : A->A, forall x : A, (R x (f x)) /\ forall x', R x x' -> f x = f x'). -(** AC_fun_setoid *) +(** AC_fun_setoid = functional form of the (so-called extensional) axiom of + choice from setoids *) Definition SetoidFunctionalChoice_on := forall R : A -> A -> Prop, @@ -197,7 +141,8 @@ Definition SetoidFunctionalChoice_on := (forall x, exists y, T x y) -> exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). -(** AC_fun_setoid_gen *) +(** AC_fun_setoid_gen = functional form of the general form of the (so-called + extensional) axiom of choice over setoids *) (* Note: This is called extensional axiom of choice (AC_ext) in [[Carlström04]]. *) @@ -213,7 +158,8 @@ Definition GeneralizedSetoidFunctionalChoice_on := exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> S (f x) (f x')). -(** AC_fun_setoid_simple *) +(** AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of + choice from setoids on locally compatible relations *) Definition SimpleSetoidFunctionalChoice_on A B := forall R : A -> A -> Prop, @@ -222,19 +168,19 @@ Definition SimpleSetoidFunctionalChoice_on A B := (forall x, exists y, forall x', R x x' -> T x' y) -> exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). -(** ID_epsilon (constructive version of indefinite description; - combined with proof-irrelevance, it may be connected to - Carlström's type theory with a constructive indefinite description - operator) *) +(** ID_epsilon = constructive version of indefinite description; + combined with proof-irrelevance, it may be connected to + Carlström's type theory with a constructive indefinite description + operator *) Definition ConstructiveIndefiniteDescription_on := forall P:A->Prop, (exists x, P x) -> { x:A | P x }. -(** ID_iota (constructive version of definite description; combined - with proof-irrelevance, it may be connected to Carlström's and - Stenlund's type theory with a constructive definite description - operator) *) +(** ID_iota = constructive version of definite description; + combined with proof-irrelevance, it may be connected to + Carlström's and Stenlund's type theory with a + constructive definite description operator) *) Definition ConstructiveDefiniteDescription_on := forall P:A->Prop, @@ -242,7 +188,7 @@ Definition ConstructiveDefiniteDescription_on := (** ** Weakly classical choice and description *) -(** GAC_rel *) +(** GAC_rel = guarded relational form of the (non extensional) axiom of choice *) Definition GuardedRelationalChoice_on := forall P : A->Prop, forall R : A->B->Prop, @@ -250,7 +196,7 @@ Definition GuardedRelationalChoice_on := (exists R' : A->B->Prop, subrelation R' R /\ forall x, P x -> exists! y, R' x y). -(** GAC_fun *) +(** GAC_fun = guarded functional form of the (non extensional) axiom of choice *) Definition GuardedFunctionalChoice_on := forall P : A->Prop, forall R : A->B->Prop, @@ -258,7 +204,7 @@ Definition GuardedFunctionalChoice_on := (forall x : A, P x -> exists y : B, R x y) -> (exists f : A->B, forall x, P x -> R x (f x)). -(** GFR_fun *) +(** GAC! = guarded functional relation reification *) Definition GuardedFunctionalRelReification_on := forall P : A->Prop, forall R : A->B->Prop, @@ -266,27 +212,28 @@ Definition GuardedFunctionalRelReification_on := (forall x : A, P x -> exists! y : B, R x y) -> (exists f : A->B, forall x : A, P x -> R x (f x)). -(** OAC_rel *) +(** OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice *) Definition OmniscientRelationalChoice_on := forall R : A->B->Prop, exists R' : A->B->Prop, subrelation R' R /\ forall x : A, (exists y : B, R x y) -> exists! y, R' x y. -(** OAC_fun *) +(** OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice + (called AC* in Bell [[Bell]]) *) Definition OmniscientFunctionalChoice_on := forall R : A->B->Prop, inhabited B -> exists f : A->B, forall x : A, (exists y : B, R x y) -> R x (f x). -(** D_epsilon *) +(** D_epsilon = (weakly classical) indefinite description principle *) Definition EpsilonStatement_on := forall P:A->Prop, inhabited A -> { x:A | (exists x, P x) -> P x }. -(** D_iota *) +(** D_iota = (weakly classical) definite description principle *) Definition IotaStatement_on := forall P:A->Prop, @@ -300,14 +247,20 @@ Notation RelationalChoice := (forall A B : Type, RelationalChoice_on A B). Notation FunctionalChoice := (forall A B : Type, FunctionalChoice_on A B). -Definition FunctionalDependentChoice := +Notation DependentFunctionalChoice := + (forall A (B:A->Type), DependentFunctionalChoice_on B). +Notation InhabitedForallCommute := + (forall A (B : A -> Type), InhabitedForallCommute_on B). +Notation FunctionalDependentChoice := (forall A : Type, FunctionalDependentChoice_on A). -Definition FunctionalCountableChoice := +Notation FunctionalCountableChoice := (forall A : Type, FunctionalCountableChoice_on A). Notation FunctionalChoiceOnInhabitedSet := (forall A B : Type, inhabited B -> FunctionalChoice_on A B). Notation FunctionalRelReification := (forall A B : Type, FunctionalRelReification_on A B). +Notation DependentFunctionalRelReification := + (forall A (B:A->Type), DependentFunctionalRelReification_on B). Notation RepresentativeFunctionalChoice := (forall A : Type, RepresentativeFunctionalChoice_on A). Notation SetoidFunctionalChoice := @@ -341,38 +294,87 @@ Notation EpsilonStatement := (** Subclassical schemes *) +(** PI = proof irrelevance *) Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. +(** IGP = independence of general premises + (an unconstrained generalisation of the constructive principle of + independence of premises) *) Definition IndependenceOfGeneralPremises := forall (A:Type) (P:A -> Prop) (Q:Prop), inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x. +(** Drinker = drinker's paradox (small form) + (called Ex in Bell [[Bell]]) *) Definition SmallDrinker'sParadox := forall (A:Type) (P:A -> Prop), inhabited A -> exists x, (exists x, P x) -> P x. +(** EM = excluded-middle *) Definition ExcludedMiddle := forall P:Prop, P \/ ~ P. (** Extensional schemes *) +(** Ext_prop_repr = choice of a representative among extensional propositions *) Local Notation ExtensionalPropositionRepresentative := (forall (A:Type), exists h : Prop -> Prop, forall P : Prop, (P <-> h P) /\ forall Q, (P <-> Q) -> h P = h Q). +(** Ext_pred_repr = choice of a representative among extensional predicates *) Local Notation ExtensionalPredicateRepresentative := (forall (A:Type), exists h : (A->Prop) -> (A->Prop), forall (P : A -> Prop), (forall x, P x <-> h P x) /\ forall Q, (forall x, P x <-> Q x) -> h P = h Q). +(** Ext_fun_repr = choice of a representative among extensional functions *) Local Notation ExtensionalFunctionRepresentative := (forall (A B:Type), exists h : (A->B) -> (A->B), forall (f : A -> B), (forall x, f x = h f x) /\ forall g, (forall x, f x = g x) -> h f = h g). +(** We let also + +- IPL_2 = 2nd-order impredicative minimal predicate logic (with ex. quant.) +- IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) +- IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.) + +with no prerequisite on the non-emptiness of domains +*) + +(**********************************************************************) +(** * Table of contents *) + +(* This is very fragile. *) +(** +1. Definitions + +2. IPL_2^2 |- AC_rel + AC! = AC_fun + +3.1. typed IPL_2 + Sigma-types + PI |- AC_rel = GAC_rel and IPL_2 |- AC_rel + IGP -> GAC_rel and IPL_2 |- GAC_rel = OAC_rel + +3.2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker + +3.3. D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker + +4. Derivability of choice for decidable relations with well-ordered codomain + +5. AC_fun = AC_fun_dep = AC_trunc + +6. Non contradiction of constructive descriptions wrt functional choices + +7. Definite description transports classical logic to the computational world + +8. Choice -> Dependent choice -> Countable choice + +9.1. AC_fun_setoid = AC_fun + Ext_fun_repr + EM + +9.2. AC_fun_setoid = AC_fun + Ext_pred_repr + PI + *) + (**********************************************************************) (** * AC_rel + AC! = AC_fun @@ -400,9 +402,6 @@ Proof. apply HR'R; assumption. Qed. -Notation description_rel_choice_imp_funct_choice := - functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6"). - Lemma fun_choice_imp_rel_choice : forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B. Proof. @@ -416,8 +415,6 @@ Proof. trivial. Qed. -Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6"). - Lemma fun_choice_imp_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B. Proof. @@ -431,8 +428,6 @@ Proof. exists f; exact H0. Qed. -Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6"). - Corollary fun_choice_iff_rel_choice_and_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B. @@ -444,8 +439,6 @@ Proof. intros [H H0]; exact (functional_rel_reification_and_rel_choice_imp_fun_choice H0 H). Qed. -Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := - fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6"). (**********************************************************************) (** * Connection between the guarded, non guarded and omniscient choices *) @@ -687,10 +680,6 @@ Qed. Require Import Wf_nat. Require Import Decidable. -Definition FunctionalChoice_on_rel (A B:Type) (R:A->B->Prop) := - (forall x:A, exists y : B, R x y) -> - exists f : A -> B, (forall x:A, R x (f x)). - Lemma classical_denumerable_description_imp_fun_choice : forall A:Type, FunctionalRelReification_on A nat -> @@ -712,18 +701,10 @@ Proof. Qed. (**********************************************************************) -(** * Choice on dependent and non dependent function types are equivalent *) +(** * AC_fun = AC_fun_dep = AC_trunc *) (** ** Choice on dependent and non dependent function types are equivalent *) -Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) := - forall R:forall x:A, B x -> Prop, - (forall x:A, exists y : B x, R x y) -> - (exists f : (forall x:A, B x), forall x:A, R x (f x)). - -Notation DependentFunctionalChoice := - (forall A (B:A->Type), DependentFunctionalChoice_on B). - (** The easy part *) Theorem dep_non_dep_functional_choice : @@ -760,13 +741,7 @@ Proof. destruct Heq using eq_indd; trivial. Qed. -(** Functional choice can be reformulated as a property on [inhabited] *) - -Definition InhabitedForallCommute_on (A : Type) (B : A -> Type) := - (forall x, inhabited (B x)) -> inhabited (forall x, B x). - -Notation InhabitedForallCommute := - (forall A (B : A -> Type), InhabitedForallCommute_on B). +(** ** Functional choice and truncation choice are equivalent *) Theorem functional_choice_to_inhabited_forall_commute : FunctionalChoice -> InhabitedForallCommute. @@ -795,14 +770,6 @@ Qed. (** ** Reification of dependent and non dependent functional relation are equivalent *) -Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := - forall (R:forall x:A, B x -> Prop), - (forall x:A, exists! y : B x, R x y) -> - (exists f : (forall x:A, B x), forall x:A, R x (f x)). - -Notation DependentFunctionalRelReification := - (forall A (B:A->Type), DependentFunctionalRelReification_on B). - (** The easy part *) Theorem dep_non_dep_functional_rel_reification : @@ -1337,3 +1304,15 @@ Proof. apply repr_fun_choice_imp_excluded_middle. now apply setoid_fun_choice_imp_repr_fun_choice. Qed. + +(**********************************************************************) +(** * Compatibility notations *) +Notation description_rel_choice_imp_funct_choice := + functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6"). + +Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6"). + +Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := + fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6"). + +Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6"). -- cgit v1.2.3 From ca4aee0fcf1b54363a6a1eb837cd05cd7ffcc0d9 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Wed, 3 May 2017 07:47:51 -0400 Subject: Report a useful error for dependent induction The dependent induction tactic notation is in the standard library but not loaded by default, leading to a parser error message that is confusing and unhelpful. This commit adds a notation for dependent induction to Init that fails and reports [Require Import Coq.Program.Equality.] is required to use [dependent induction]. --- theories/Init/Tactics.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'theories') diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 5d1e87ae0c..7a846cd1b3 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -236,3 +236,10 @@ Tactic Notation "clear" "dependent" hyp(h) := Tactic Notation "revert" "dependent" hyp(h) := generalize dependent h. + +(** Provide an error message for dependent induction that reports an import is +required to use it. Importing Coq.Program.Equality will shadow this notation +with the actual [dependent induction] tactic. *) + +Tactic Notation "dependent" "induction" ident(H) := + fail "To use dependent induction, first [Require Import Coq.Program.Equality.]". -- cgit v1.2.3 From 530ce019b7bdcc2603027082f6b3f6841d5990e1 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 16 May 2017 18:28:41 +0200 Subject: Stop using auto with * in two proofs. auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db. --- theories/Structures/DecidableType.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories') diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index f85222dfb4..d811f04ef6 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -86,7 +86,7 @@ Module KeyDecidableType(D:DecidableType). 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 with *. + intros; apply InA_eqA with p; auto using eqk_equiv. Qed. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). @@ -109,7 +109,7 @@ Module KeyDecidableType(D:DecidableType). 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 with *. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. -- cgit v1.2.3