From f8e565adb8ab395eac97caf40eecc66a9c4ee81e Mon Sep 17 00:00:00 2001 From: jalex-stark Date: Tue, 26 May 2020 21:51:39 -0400 Subject: [PATCH 1/5] feat(library/init/meta)\nadd assumption? tactic --- library/init/meta/interactive.lean | 9 ++++++--- library/init/meta/tactic.lean | 13 ++++++++++++- 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 7ca4dd82f6..abe64b9b56 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -244,10 +244,13 @@ meta def refine (q : parse texpr) : tactic unit := tactic.refine q /-- -This tactic looks in the local context for a hypothesis whose type is equal to the goal target. If it finds one, it uses it to prove the goal, and otherwise it fails. +This tactic looks in the local context for a hypothesis whose type is equal to the goal target. +If it finds one, it uses it to prove the goal, and otherwise it fails. +`assumption?` will print the name of the goal that it found. -/ -meta def assumption : tactic unit := -tactic.assumption + +meta def assumption (trace_result : parse $ optional (tk "?")) := +tactic.assumption trace_result.is_some /-- Try to apply `assumption` to all goals. -/ meta def assumption' : tactic unit := diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 072e197c33..49338f020a 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -948,10 +948,21 @@ meta def find_same_type : expr → list expr → tactic expr meta def find_assumption (e : expr) : tactic expr := do ctx ← local_context, find_same_type e ctx -meta def assumption : tactic unit := +meta def is_implicit : expr → bool +| (expr.pi _ binder_info.implicit _ _) := tt +| _ := ff + +/-- Find a hypothesis matching the goal. `assumption tt` will print the goal that it found. + If the goal type starts with an implicit binder, prints an "@" in front. -/ +meta def assumption (trace_result : bool := ff) : tactic unit := do { ctx ← local_context, t ← target, H ← find_same_type t ctx, + when trace_result $ + do { pp_H ← pp H, + H_type ← tactic.infer_type H, + let H_format := if is_implicit H_type then ↑"@" ++ pp_H else pp_H, + trace ( ("Try this: exact " : format) ++ H_format) }, exact H } <|> fail "assumption tactic failed" From 1877db4f408e7f13fb82736b6a74af0c4f20fefd Mon Sep 17 00:00:00 2001 From: jalex-stark Date: Tue, 26 May 2020 22:24:51 -0400 Subject: [PATCH 2/5] chore(tests/lean)\n add tests for --- tests/lean/assumption.lean | 9 +++++++++ tests/lean/assumption.lean.expected.out | 3 +++ tests/lean/interactive/assumption.lean | 9 +++++++++ tests/lean/interactive/assumption.lean.expected.out | 3 +++ 4 files changed, 24 insertions(+) create mode 100644 tests/lean/assumption.lean create mode 100644 tests/lean/assumption.lean.expected.out create mode 100644 tests/lean/interactive/assumption.lean create mode 100644 tests/lean/interactive/assumption.lean.expected.out diff --git a/tests/lean/assumption.lean b/tests/lean/assumption.lean new file mode 100644 index 0000000000..79668a10c4 --- /dev/null +++ b/tests/lean/assumption.lean @@ -0,0 +1,9 @@ +example (p : Prop) (h1 : p) : p := +begin + assumption?, +end + +example (p : Prop) (h2 : ∀ {x : ℕ}, p) : ∀ x : ℕ, p := +begin + assumption?, +end diff --git a/tests/lean/assumption.lean.expected.out b/tests/lean/assumption.lean.expected.out new file mode 100644 index 0000000000..026b5b5869 --- /dev/null +++ b/tests/lean/assumption.lean.expected.out @@ -0,0 +1,3 @@ +{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":"Try this: h1\n"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":""Try this: @h1\n"},"response":"all_messages"] +{"message":"file invalidated","response":"ok","seq_num":0} diff --git a/tests/lean/interactive/assumption.lean b/tests/lean/interactive/assumption.lean new file mode 100644 index 0000000000..79668a10c4 --- /dev/null +++ b/tests/lean/interactive/assumption.lean @@ -0,0 +1,9 @@ +example (p : Prop) (h1 : p) : p := +begin + assumption?, +end + +example (p : Prop) (h2 : ∀ {x : ℕ}, p) : ∀ x : ℕ, p := +begin + assumption?, +end diff --git a/tests/lean/interactive/assumption.lean.expected.out b/tests/lean/interactive/assumption.lean.expected.out new file mode 100644 index 0000000000..026b5b5869 --- /dev/null +++ b/tests/lean/interactive/assumption.lean.expected.out @@ -0,0 +1,3 @@ +{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":"Try this: h1\n"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":""Try this: @h1\n"},"response":"all_messages"] +{"message":"file invalidated","response":"ok","seq_num":0} From 78059335bf697652ba2d840df011cee891777843 Mon Sep 17 00:00:00 2001 From: jalex-stark Date: Tue, 26 May 2020 22:25:14 -0400 Subject: [PATCH 3/5] chore(tests/lean)\n add tests for --- tests/lean/interactive/assumption.lean | 9 --------- tests/lean/interactive/assumption.lean.expected.out | 3 --- 2 files changed, 12 deletions(-) delete mode 100644 tests/lean/interactive/assumption.lean delete mode 100644 tests/lean/interactive/assumption.lean.expected.out diff --git a/tests/lean/interactive/assumption.lean b/tests/lean/interactive/assumption.lean deleted file mode 100644 index 79668a10c4..0000000000 --- a/tests/lean/interactive/assumption.lean +++ /dev/null @@ -1,9 +0,0 @@ -example (p : Prop) (h1 : p) : p := -begin - assumption?, -end - -example (p : Prop) (h2 : ∀ {x : ℕ}, p) : ∀ x : ℕ, p := -begin - assumption?, -end diff --git a/tests/lean/interactive/assumption.lean.expected.out b/tests/lean/interactive/assumption.lean.expected.out deleted file mode 100644 index 026b5b5869..0000000000 --- a/tests/lean/interactive/assumption.lean.expected.out +++ /dev/null @@ -1,3 +0,0 @@ -{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":"Try this: h1\n"}],"response":"all_messages"} -{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":""Try this: @h1\n"},"response":"all_messages"] -{"message":"file invalidated","response":"ok","seq_num":0} From 6e4f0f3590448e45e934919058b67ea553904366 Mon Sep 17 00:00:00 2001 From: Jalex Stark Date: Wed, 3 Jun 2020 18:56:55 -0400 Subject: [PATCH 4/5] Update library/init/meta/tactic.lean Co-authored-by: Yury G. Kudryashov --- library/init/meta/tactic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 49338f020a..917da0dab8 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -960,9 +960,9 @@ do { ctx ← local_context, H ← find_same_type t ctx, when trace_result $ do { pp_H ← pp H, - H_type ← tactic.infer_type H, - let H_format := if is_implicit H_type then ↑"@" ++ pp_H else pp_H, - trace ( ("Try this: exact " : format) ++ H_format) }, + H_type ← tactic.infer_type H, + let H_format := if is_implicit H_type then ↑"@" ++ pp_H else pp_H, + trace ( ("Try this: exact " : format) ++ H_format) }, exact H } <|> fail "assumption tactic failed" From 0b9219fd863d810cd17d60cb5a7cb8218b60cbde Mon Sep 17 00:00:00 2001 From: jalex-stark Date: Wed, 3 Jun 2020 19:00:35 -0400 Subject: [PATCH 5/5] added expected output for test --- tests/lean/assumption.lean.expected.out | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/assumption.lean.expected.out b/tests/lean/assumption.lean.expected.out index 026b5b5869..85f42b2a3d 100644 --- a/tests/lean/assumption.lean.expected.out +++ b/tests/lean/assumption.lean.expected.out @@ -1,3 +1,3 @@ -{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":"Try this: h1\n"}],"response":"all_messages"} -{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":""Try this: @h1\n"},"response":"all_messages"] -{"message":"file invalidated","response":"ok","seq_num":0} +-{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":"Try this: h1\n"}],"response":"all_messages"} +-{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":""Try this: @h1\n"},"response":"all_messages"] +-{"message":"file invalidated","response":"ok","seq_num":0} \ No newline at end of file