[Merged by Bors] - feat: port field_simp tactic #1824
Conversation
| | .ok (some _) => return m!"{checkEmoji} discharge {prop}" | ||
|
|
||
| /-- Discharge strategy for the field_simp tactic. -/ | ||
| partial def discharge (prop : Expr) : SimpM (Option Expr) := |
There was a problem hiding this comment.
I used the default discharger implementation as a model for this function. https://github.com/leanprover/lean4/blob/1f41b912064e49979bfefa5874ea53cb25934a06/src/Lean/Meta/Tactic/Simp/Main.lean#L815-L835
There was a problem hiding this comment.
Since there seem to be quite some differences between the mathlib3 and mathlib4 implementations of field_simps, it might be good to test this on more examples, if it is reasonably easy to add more examples...
I saw three commented out cases in test/ring. If I add
import Mathlib.Tactic.FieldSimp
import Mathlib.Data.Real.Basic
the first two work, but are incredibly slow, and I think the third one is supposed to further simplify 2 * x ^ 3 * 2 / (24 * x) and fails.
Mathlib/Tactic/FieldSimp.lean
Outdated
| let r ← elabSimpArgs (sa.getD ⟨.missing⟩) ctx (eraseLocal := false) .simp | ||
|
|
||
| let _ ← simpLocation r.ctx dis loc | ||
| pure () |
fpvandoorn
added
awaiting-author
|
Re-added a call to |
|
|
||
| let prop : Q(Prop) ← (do pure prop) | ||
| let pf? ← match prop with | ||
| | ~q(($e : $α) ≠ $b) => |
There was a problem hiding this comment.
The mathlib3 version instead matches on $e ≠ 0. I couldn't figure out a way to make that work with Qq. (I could get it to typecheck here, but then it failed to actually match the expressions that we need it to.) This more general match should be fine. The cost is that we might call NormNum.derive slightly more often than is strictly necessary.
|
I'm guessing that the slowness of the first two examples in test/ring.lean has to do with leanprover/lean4#2055. |
dwrensha
added
awaiting-review
and removed
awaiting-author
|
After #2188, the examples in test/ring seem to be going a lot faster. |
|
Ok, let's get this merged bors merge |
github-actions
bot
added
ready-to-merge
* Ports the `field_simp` tactic and tests from mathlib3. * Adds a new test taken from minif2f (but with rats instead of reals, for simplicity): https://github.com/openai/miniF2F/blob/4e433ff5cadff23f9911a2bb5bbab2d351ce5554/lean/src/valid.lean#L524-L530. * Uses `field_simp` in two already-ported files, as directed by port notes. * Adds an explicit priority to a few `field_simps` lemmas. This is necessary to make all of the examples work.
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
* Ports the `field_simp` tactic and tests from mathlib3. * Adds a new test taken from minif2f (but with rats instead of reals, for simplicity): https://github.com/openai/miniF2F/blob/4e433ff5cadff23f9911a2bb5bbab2d351ce5554/lean/src/valid.lean#L524-L530. * Uses `field_simp` in two already-ported files, as directed by port notes. * Adds an explicit priority to a few `field_simps` lemmas. This is necessary to make all of the examples work.
* Ports the `field_simp` tactic and tests from mathlib3. * Adds a new test taken from minif2f (but with rats instead of reals, for simplicity): https://github.com/openai/miniF2F/blob/4e433ff5cadff23f9911a2bb5bbab2d351ce5554/lean/src/valid.lean#L524-L530. * Uses `field_simp` in two already-ported files, as directed by port notes. * Adds an explicit priority to a few `field_simps` lemmas. This is necessary to make all of the examples work.
field_simptactic and tests from mathlib3.field_simpin two already-ported files, as directed by port notes.field_simpslemmas. This is necessary to make all of the examples work.