[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.
Should tauto be included here?
There was a problem hiding this comment.
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.
| 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.
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?
| 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.
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. Iftacproduces a "Try this: " message, use that instead oftac.I haven't hooked up
aesopyet, 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.