From f5c81ac1bcae7c40d5e89229647c06c97b5ddc85 Mon Sep 17 00:00:00 2001 From: Thomas Sibut-Pinote Date: Wed, 1 Feb 2017 17:58:32 +0100 Subject: Added some theory on powerRZ. For this, I used a new inductive type Z_spec to reason on Z. --- theories/Reals/Rfunctions.v | 98 +++++++++++++++++++++++++++++++++++++++++++++ theories/Reals/Rpower.v | 14 +++++++ 2 files changed, 112 insertions(+) (limited to 'theories') diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 0a49d49831..80dc36e876 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -531,6 +531,36 @@ Qed. (*******************************) (*i Due to L.Thery i*) +Section PowerRZ. + +Local Coercion Z_of_nat : nat >-> Z. + +(* the following section should probably be somewhere else, but not sure where *) +Section Z_compl. + +Local Open Scope Z_scope. + +(* Provides a way to reason directly on Z in terms of nats instead of positive *) +Inductive Z_spec (x : Z) : Z -> Type := +| ZintNull : x = 0 -> Z_spec x 0 +| ZintPos (n : nat) : x = n -> Z_spec x n +| ZintNeg (n : nat) : x = - n -> Z_spec x (- n). + +Lemma intP (x : Z) : Z_spec x x. +Proof. + destruct x as [|p|p]. + - now apply ZintNull. + - rewrite <-positive_nat_Z at 2. + apply ZintPos. + now rewrite positive_nat_Z. + - rewrite <-Pos2Z.opp_pos. + rewrite <-positive_nat_Z at 2. + apply ZintNeg. + now rewrite positive_nat_Z. +Qed. + +End Z_compl. + Definition powerRZ (x:R) (n:Z) := match n with | Z0 => 1 @@ -657,6 +687,74 @@ Proof. auto with real. Qed. +Local Open Scope Z_scope. + +Lemma pow_powerRZ (r : R) (n : nat) : + (r ^ n)%R = powerRZ r (Z_of_nat n). +Proof. + induction n; [easy|simpl]. + now rewrite SuccNat2Pos.id_succ. +Qed. + +Lemma powerRZ_ind (P : Z -> R -> R -> Prop) : + (forall x, P 0 x 1%R) -> + (forall x n, P (Z.of_nat n) x (x ^ n)%R) -> + (forall x n, P ((-(Z.of_nat n))%Z) x (Rinv (x ^ n))) -> + forall x (m : Z), P m x (powerRZ x m)%R. +Proof. + intros ? ? ? x m. + destruct (intP m) as [n Hm| n Hm|n Hm]. + - easy. + - now rewrite <- pow_powerRZ. + - unfold powerRZ. + destruct n as [|n]; [ easy |]. + rewrite Nat2Z.inj_succ, <- Zpos_P_of_succ_nat, Pos2Z.opp_pos. + now rewrite <- Pos2Z.opp_pos, <- positive_nat_Z. +Qed. + +Lemma powerRZ_inv x alpha : (x <> 0)%R -> powerRZ (/ x) alpha = Rinv (powerRZ x alpha). +Proof. + intros; destruct (intP alpha). + - now simpl; rewrite Rinv_1. + - now rewrite <-!pow_powerRZ, ?Rinv_pow, ?pow_powerRZ. + - unfold powerRZ. + destruct (- n). + + now rewrite Rinv_1. + + now rewrite Rinv_pow. + + now rewrite <-Rinv_pow. +Qed. + +Lemma powerRZ_neg x : forall alpha, x <> R0 -> powerRZ x (- alpha) = powerRZ (/ x) alpha. +Proof. + intros [|n|n] H ; simpl. + - easy. + - now rewrite Rinv_pow. + - rewrite Rinv_pow by now apply Rinv_neq_0_compat. + now rewrite Rinv_involutive. +Qed. + +Lemma powerRZ_mult_distr : + forall m x y, ((0 <= m)%Z \/ (x * y <> 0)%R) -> + (powerRZ (x*y) m = powerRZ x m * powerRZ y m)%R. +Proof. + intros m x0 y0 Hmxy. + destruct (intP m) as [ | | n Hm ]. + - now simpl; rewrite Rmult_1_l. + - now rewrite <- !pow_powerRZ, Rpow_mult_distr. + - destruct Hmxy as [H|H]. + + assert(m = 0) as -> by now omega. + now rewrite <- Hm, Rmult_1_l. + + assert(x0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_l. + assert(y0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_r. + rewrite !powerRZ_neg by assumption. + rewrite Rinv_mult_distr by assumption. + now rewrite <- !pow_powerRZ, Rpow_mult_distr. +Qed. + +End PowerRZ. + +Local Infix "^Z" := powerRZ (at level 30, right associativity) : R_scope. + (*******************************) (* For easy interface *) (*******************************) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index b3ce6fa338..93462a1fc3 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -490,6 +490,20 @@ Proof. apply exp_Ropp. Qed. +Lemma powerRZ_Rpower x z : (0 < x)%R -> powerRZ x z = Rpower x (IZR z). +Proof. + intros Hx. + assert (x <> 0)%R + by now intros Habs; rewrite Habs in Hx; apply (Rlt_irrefl 0). + destruct (intP z). + - now rewrite Rpower_O. + - rewrite <- pow_powerRZ, <- Rpower_pow by assumption. + now rewrite INR_IZR_INZ. + - rewrite opp_IZR, Rpower_Ropp. + rewrite powerRZ_neg, powerRZ_inv by assumption. + now rewrite <- pow_powerRZ, <- INR_IZR_INZ, Rpower_pow. +Qed. + Theorem Rle_Rpower : forall e n m:R, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m. Proof. -- cgit v1.2.3 From 16b8ed513cb4a0e68456fc968a9a0107d02acf5a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 25 Apr 2017 13:50:54 -0400 Subject: Give andb_prop a simpler proof No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.--- theories/Init/Datatypes.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories') diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 11d80dbc33..41e1fea61d 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -65,7 +65,7 @@ Infix "&&" := andb : bool_scope. Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true. Proof. - destruct a; destruct b; intros; split; try (reflexivity || discriminate). + destruct a, b; repeat split; assumption. Qed. Hint Resolve andb_prop: bool. -- cgit v1.2.3 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 2fc235b0e00c028d2e91c696926ad339232d51e3 Mon Sep 17 00:00:00 2001 From: Vadim Zaliva Date: Wed, 26 Apr 2017 11:21:10 -0700 Subject: Small typo in comment --- theories/Init/Logic.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index f659c31f95..9ae9dde28d 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -223,7 +223,7 @@ Proof. Qed. (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes - either [P] and [Q], or [~P] and [Q] *) + either [P] and [Q], or [~P] and [R] *) Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R. -- cgit v1.2.3 From e1fc5c4dae82acd2eb6618724599aca368c200b7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 4 Dec 2016 14:09:24 -0500 Subject: Add .dir-locals.el and _CoqProject files for emacs stdlib editing These set up PG to use the local coqtop, and the local coqlib, when editing files in the stdlib. As per https://github.com/coq/coq/pull/386#issuecomment-279012238, we can use `_CoqProject` for `theories/Init`, and this allows CoqIDE to edit those files. However, we cannot use it for `theories/`, because a `_CoqProject` file will override a `.dir-locals.el` in the same directory, and there is no way to get PG to pick up a valid `-coqlib` from `_CoqProject` (because it'll take the path relative to the current directory, not relative to the directory of `_CoqProject`). --- theories/.dir-locals.el | 4 ++++ theories/Init/_CoqProject | 2 ++ 2 files changed, 6 insertions(+) create mode 100644 theories/.dir-locals.el create mode 100644 theories/Init/_CoqProject (limited to 'theories') diff --git a/theories/.dir-locals.el b/theories/.dir-locals.el new file mode 100644 index 0000000000..4e8830f6c1 --- /dev/null +++ b/theories/.dir-locals.el @@ -0,0 +1,4 @@ +((coq-mode . ((eval . (let ((default-directory (locate-dominating-file + buffer-file-name ".dir-locals.el"))) + (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) + (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) diff --git a/theories/Init/_CoqProject b/theories/Init/_CoqProject new file mode 100644 index 0000000000..bff79d34bf --- /dev/null +++ b/theories/Init/_CoqProject @@ -0,0 +1,2 @@ +-R .. Coq +-arg -noinit -- cgit v1.2.3 From 6deddd3e0c6cc1d7cbf8414f7553c5d7752a0801 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 28 Apr 2017 14:02:00 -0400 Subject: Allow interactive editing of {C,}Morphisms in PG --- theories/Classes/CMorphisms.v | 2 +- theories/Classes/Morphisms.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'theories') diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 1cfca41692..74ca5d4c8a 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -1,4 +1,4 @@ -(* -*- coding: utf-8 -*- *) +(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.CMorphisms") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* R -> R -> Prop) : forall x (m : Z), P m x (powerRZ x m)%R. Proof. intros ? ? ? x m. - destruct (intP m) as [n Hm| n Hm|n Hm]. + destruct (intP m) as [Hm|n Hm|n Hm]. - easy. - now rewrite <- pow_powerRZ. - unfold powerRZ. -- 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