[Merged by Bors] - feat(tactic/field_simp): let field_simp use norm_num to prove numerals are nonzero #5418
Conversation
sgouezel
added
awaiting-review
| (cfg : simp_config_ext := {discharger := field_simp.ne_zero}) : tactic unit := | ||
| let attr_names := `field_simps :: attr_names, | ||
| hs := simp_arg_type.except `one_div :: simp_arg_type.except `mul_eq_zero :: hs in | ||
| propagate_tags (simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat) |
There was a problem hiding this comment.
Huh. field_simp isn't simp only using field_simps, it uses the full simp set. I didn't realize this. So technically nonterminal field_simp is a bad idea, although I guess it's less likely to be abused than regular simp.
There was a problem hiding this comment.
Yes, there are places in the library where it's used as: simp + the additional ability to simplify denominators. Just like simp, it shouldn't be used non-terminally, but in general it is just field_simp [...], ring.
| fact that a product is nonzero when all factors are, and that a power of a nonzero number is | ||
| nonzero, are included in the simpset, but more complicated assertions (especially dealing with sums) |
There was a problem hiding this comment.
Since you've changed the discharger from the default simp, this claim about products and powers is no longer true, right? The only preconditions you'll solve are those that are literally in the context and numeric ones.
There was a problem hiding this comment.
I don't get it. The default discharger for simp is failed, right? So it's only making things more powerful. Indeed, with the modification it solves everything it solved previously (at least all the mathlib examples and tests).
There was a problem hiding this comment.
Ah, sorry, I take it back. Seems like the discharger option is used in addition to recursively calling simp. I thought it was replacing that.
robertylewis
added
awaiting-author
sgouezel
added
awaiting-review
|
I don't see a commit for the change in bors d+ |
|
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
github-actions
bot
added
ready-to-merge
…s are nonzero (#5418) As suggested by @robertylewis in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Solving.20simple.20%28in%29equalities.20gets.20frustrating/near/220278546, change the discharger in `field_simp` to try `assumption` on goals `x ≠ 0` and `norm_num1` on these goals when `x` is a numeral.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
As suggested by @robertylewis in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Solving.20simple.20%28in%29equalities.20gets.20frustrating/near/220278546, change the discharger in
field_simpto tryassumptionon goalsx ≠ 0andnorm_num1on these goals whenxis a numeral.Since
field_simpnow depends onnorm_num, I have moved it to its own file instead oftactic.interactive.