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/Init') 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/Init') 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/Init') 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/Init/_CoqProject | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 theories/Init/_CoqProject (limited to 'theories/Init') 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 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 +++++++++++ 2 files changed, 16 insertions(+) (limited to 'theories/Init') 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 *) -- 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/Init') 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