-
Notifications
You must be signed in to change notification settings - Fork 310
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: the 'hint' tactic #8363
Conversation
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? |
I will immediately steal the Edit: nope. I wonder what it is for. |
I integrated my changes:
|
Thank you, @Komyyy, and apologies again for missing your earlier PR. |
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. |
section Hint | ||
|
||
register_hint split | ||
register_hint intro |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should tauto
be included here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
register_hint exact? | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
@@ -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": |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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+
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
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>
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>
``` 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>
``` 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>
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. Iftac
produces a "Try this: " message, use that instead oftac
.I haven't hooked up
aesop
yet, because of leanprover-community/aesop#85. Similarly fornorm_num
.I would like to parallelize this, but I don't think that needs to happen right away.