[Merged by Bors] - feat: the 'hint' tactic #8363

semorrison · 2023-11-12T08:03:03Z

example (h : 1 < 0) : False := by hint
example {P Q : Prop} (p : P) (f : P → Q) : Q := by hint
example {P Q R: Prop} (x : P ∧ Q ∧ R ∧ R) : Q ∧ P ∧ R := by hint
example {a b : ℚ} (h : a < b) : ¬ b < a := by hint
example : 37^2 - 35^2 = 72 * 2 := by hint
example : Nat.Prime 37 := by hint

Tries out any tactics registered using register_hint tac, and reports which ones succeed using the new "Try these: " multiple suggestion widgets. Tactics that close the goal are highlighted in green. Tactics that succeed but don't close the goal display the new subgoals in the widget. If tac produces a "Try this: " message, use that instead of tac.

I haven't hooked up aesop yet, because of leanprover-community/aesop#85. Similarly for norm_num.

I would like to parallelize this, but I don't think that needs to happen right away.

timotree3 · 2023-11-13T06:37:29Z

How does this compare with #5363?

semorrison · 2023-11-13T07:42:04Z

How does this compare with #5363?

Oh! I had completely failed to notice that. Apologies in particular to @Komyyy.

I'm impressed how parallel parts of the implementation are. :-) My version uses the new "Try these:" widget for providing multiple suggestions (edit: oh, so does @Komyyy's), and also does some additional post-processing to stop if it finds a tactic that closes the goal, and also shows the remaining subgoals for each suggestion in the widget.

@Komyyy, how should we proceed? Can we combine these into something better than either?

semorrison · 2023-11-13T07:43:21Z

I will immediately steal the let tac : Syntax.Tactic := ⟨tac.raw.copyHeadTailInfoFrom .missing⟩ trick, which I presume solves the unreachable tactic warning.

Edit: nope. I wonder what it is for.

Komyyy · 2023-11-14T03:50:37Z

I integrated my changes:

Remove some placeholders for mathport
Remove some comments for add_hint_tactic
Align import
Add an new process for register_hint to remove following comments
Register the register_hint syntax as an exception of UnreachableTactic linter

semorrison · 2023-11-14T09:12:23Z

Thank you, @Komyyy, and apologies again for missing your earlier PR.

semorrison · 2023-11-14T12:37:49Z

Okay, I have a modification to this that runs all the hint tactics in parallel, and it's lovely. I still need to move some lemmas around to get the imports to work out, so we should merge this in the meantime.

Mathlib/Tactic/Common.lean

Mathlib/Tactic/Hint.lean

test/hint.lean

j-loreaux · 2023-11-15T23:04:45Z

Mathlib/Tactic/Common.lean

+section Hint
+
+register_hint split
+register_hint intro


Should tauto be included here?

At present there is no way to remove a register_hint (without PRing to Mathlib), but it is easy to add.

Can I suggest that intentionally undershoot on this PR, and then let people try it out and revise the list?

adomani · 2023-11-15T23:04:55Z

Mathlib/Tactic/Common.lean

+register_hint exact?
+


Suggested change

register_hint exact?

register_hint exact?

register_hint constructor

I think that Lean 3 had it and in Lean 4 is maybe more useful.
I wonder whether split_ifs is also an option.

At present there is no way to remove a register_hint (without PRing to Mathlib), but it is easy to add.

Can I suggest that intentionally undershoot on this PR, and then let people try it out and revise the list?

kmill · 2023-11-16T01:29:59Z

scripts/lint-style.py

@@ -254,7 +254,7 @@ def regular_check(lines, path):
        if copy_done and line == "\n":
            continue
        words = line.split()
-        if words[0] != "import" and words[0] != "/-!" and words[0] != "#align_import":
+        if words[0] != "import" and words[0] != "--" and words[0] != "/-!" and words[0] != "#align_import":


I'm not sure this should this be part of this PR, but if you think it's OK I'll let it slide.

I think this is a good first version of the tactic, and I'm happy if you merged it.

bors d+

mathlib-bors · 2023-11-16T01:30:01Z

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

semorrison · 2023-11-16T01:32:38Z

bors merge

``` example (h : 1 < 0) : False := by hint example {P Q : Prop} (p : P) (f : P → Q) : Q := by hint example {P Q R: Prop} (x : P ∧ Q ∧ R ∧ R) : Q ∧ P ∧ R := by hint example {a b : ℚ} (h : a < b) : ¬ b < a := by hint example : 37^2 - 35^2 = 72 * 2 := by hint example : Nat.Prime 37 := by hint ``` Tries out any tactics registered using `register_hint tac`, and reports which ones succeed using the new "Try these: " multiple suggestion widgets. Tactics that close the goal are highlighted in green. Tactics that succeed but don't close the goal display the new subgoals in the widget. If `tac` produces a "Try this: " message, use that instead of `tac`. I haven't hooked up `aesop` yet, because of leanprover-community/aesop#85. Similarly for `norm_num`. I would like to parallelize this, but I don't think that needs to happen right away. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>

mathlib-bors · 2023-11-16T02:42:47Z

Pull request successfully merged into master.

Build succeeded:

``` example (h : 1 < 0) : False := by hint example {P Q : Prop} (p : P) (f : P → Q) : Q := by hint example {P Q R: Prop} (x : P ∧ Q ∧ R ∧ R) : Q ∧ P ∧ R := by hint example {a b : ℚ} (h : a < b) : ¬ b < a := by hint example : 37^2 - 35^2 = 72 * 2 := by hint example : Nat.Prime 37 := by hint ``` Tries out any tactics registered using `register_hint tac`, and reports which ones succeed using the new "Try these: " multiple suggestion widgets. Tactics that close the goal are highlighted in green. Tactics that succeed but don't close the goal display the new subgoals in the widget. If `tac` produces a "Try this: " message, use that instead of `tac`. I haven't hooked up `aesop` yet, because of leanprover-community/aesop#85. Similarly for `norm_num`. I would like to parallelize this, but I don't think that needs to happen right away. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>

semorrison added 2 commits November 12, 2023 18:58

feat: the 'hint' tactic

32e7f90

imports

b00f84d

semorrison added awaiting-review The author would like community review of the PR awaiting-CI labels Nov 12, 2023

semorrison added 3 commits November 12, 2023 19:05

linting

446f173

linting

a4c98a4

linter: relax, dude

f23ebb5

github-actions bot removed the awaiting-CI label Nov 12, 2023

Komyyy added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Nov 14, 2023

Komyyy added 2 commits November 14, 2023 10:39

Merge branch 'master' into hint_tactic

3fa0c62

integrate

8f09de2

Komyyy mentioned this pull request Nov 14, 2023

feat: port tactic hint #5363

Closed

2 tasks

Komyyy added awaiting-review The author would like community review of the PR awaiting-CI and removed WIP Work in progress labels Nov 14, 2023

github-actions bot removed the awaiting-CI label Nov 14, 2023

merge; enable aesop

90c6dfe

kmill reviewed Nov 15, 2023

View reviewed changes

Mathlib/Tactic/Common.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/Hint.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/Hint.lean Show resolved Hide resolved

test/hint.lean Show resolved Hide resolved

semorrison added 3 commits November 15, 2023 11:30

restore module doc

6dfdb9d

remove #align_import

ec48fd0

use guard_msgs

d6a2989

j-loreaux reviewed Nov 15, 2023

View reviewed changes

adomani reviewed Nov 15, 2023

View reviewed changes

kmill reviewed Nov 16, 2023

View reviewed changes

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Nov 16, 2023

mathlib-bors bot changed the title ~~feat: the 'hint' tactic~~ [Merged by Bors] - feat: the 'hint' tactic Nov 16, 2023

mathlib-bors bot closed this Nov 16, 2023

mathlib-bors bot deleted the hint_tactic branch November 16, 2023 02:42

Komyyy mentioned this pull request Nov 17, 2023

tactic porting tracking issue #430

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: the 'hint' tactic #8363

[Merged by Bors] - feat: the 'hint' tactic #8363

semorrison commented Nov 12, 2023

timotree3 commented Nov 13, 2023

semorrison commented Nov 13, 2023 •

edited

Loading

semorrison commented Nov 13, 2023 •

edited

Loading

Komyyy commented Nov 14, 2023

semorrison commented Nov 14, 2023

semorrison commented Nov 14, 2023

j-loreaux Nov 15, 2023

semorrison Nov 16, 2023

adomani Nov 15, 2023

semorrison Nov 16, 2023

kmill Nov 16, 2023

mathlib-bors bot commented Nov 16, 2023

semorrison commented Nov 16, 2023

mathlib-bors bot commented Nov 16, 2023

[Merged by Bors] - feat: the 'hint' tactic #8363

[Merged by Bors] - feat: the 'hint' tactic #8363

Conversation

semorrison commented Nov 12, 2023

timotree3 commented Nov 13, 2023

semorrison commented Nov 13, 2023 • edited Loading

semorrison commented Nov 13, 2023 • edited Loading

Komyyy commented Nov 14, 2023

semorrison commented Nov 14, 2023

semorrison commented Nov 14, 2023

j-loreaux Nov 15, 2023

Choose a reason for hiding this comment

semorrison Nov 16, 2023

Choose a reason for hiding this comment

adomani Nov 15, 2023

Choose a reason for hiding this comment

semorrison Nov 16, 2023

Choose a reason for hiding this comment

kmill Nov 16, 2023

Choose a reason for hiding this comment

mathlib-bors bot commented Nov 16, 2023

semorrison commented Nov 16, 2023

mathlib-bors bot commented Nov 16, 2023

semorrison commented Nov 13, 2023 •

edited

Loading

semorrison commented Nov 13, 2023 •

edited

Loading