fix: replace unary Nat.succ simp rules with simprocs #3808
Conversation
joehendrix
added
full-ci
awaiting-mathlib
|
This seems like it would be better addressed by finding a way for that expression not to count as having the form |
github-actions
bot
added
the
toolchain-available
|
I'll take a stab at a simproc that covers this case, but I don't think this should be a reason to touch discriminator tree patterns (e.g., the logic in |
joehendrix
changed the title
joehendrix
added
the
WIP
joehendrix
force-pushed
the
succ_sub_succ_eq
branch
from
8ab3bdf to
922ac57
Compare
This introduces a simproc for equality and another for subtraction so that we can remove simp attributes on Nat.succ_sub_succ_eq_sub and Nat.succ.injEq. Both of these have the potential to trigger stack overflows or performance problem when applied to terms with large Nat constants. The simproc operations bypass this through use of lemmas.
joehendrix
force-pushed
the
succ_sub_succ_eq
branch
from
94bec23 to
a956e88
Compare
joehendrix
removed
the
awaiting-mathlib
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
joehendrix
removed
the
WIP
@semorrison, this is misleading; the CI job "built", but the "build" step of the CI job failed. |
| if e.isAppOfArity ``HAdd.hAdd 6 then | ||
| let inst := e.appFn!.appFn!.appArg! | ||
| unless inst.isAppOfArity ``instHAdd 2 do return none | ||
| unless inst.appArg!.isAppOfArity ``instAddNat 0 do return none |
There was a problem hiding this comment.
This is going to fail if the instance is actually AddMonoid.toAdd from mathlib, which seems very likely to occur; which is to say, I think this needs to do (reducible) defeq matching, not syntactic matching.
There was a problem hiding this comment.
A small repro:
import Mathlib.Data.Nat.Basic
example : 1 + 2 = 3 := by
rewrite [add_comm]
-- goal is no longer about `instAddNat`
sorryThere was a problem hiding this comment.
Could you make an example showing this? Using import Mathlib is fine.
There was a problem hiding this comment.
@joehendrix: I just went back in time and posted one :)
There was a problem hiding this comment.
Note that this was fixed in mathlib in leanprover-community/mathlib3#18129
There was a problem hiding this comment.
For reference, the pattern of matching operators by name and typeclasses by defeq is called "keyed matching". (I learned this name from Reflexive tactics for algebra, revisited by Kazuhiko Sakaguchi, Section 3.2.)
Indeed, now that the linter runs even when the build fails, we need to change the logic. |
…ways runs (#12202) As reported [elsewhere](leanprover/lean4#3808 (comment)). Co-authored-by: Scott Morrison <[email protected]>
…ways runs (#12202) As reported [elsewhere](leanprover/lean4#3808 (comment)). Co-authored-by: Scott Morrison <[email protected]>
…ways runs (#12202) As reported [elsewhere](leanprover/lean4#3808 (comment)). Co-authored-by: Scott Morrison <[email protected]>
…ways runs (#12202) As reported [elsewhere](leanprover/lean4#3808 (comment)). Co-authored-by: Scott Morrison <[email protected]>
…ways runs (#12202) As reported [elsewhere](leanprover/lean4#3808 (comment)). Co-authored-by: Scott Morrison <[email protected]>
…ways runs (#12202) As reported [elsewhere](leanprover/lean4#3808 (comment)). Co-authored-by: Scott Morrison <[email protected]>
This removes simp attributes from
Nat.succ.injEqandNat.succ_sub_succ_eq_subto replace them with simprocs. This is because any reductions involvingNat.succhas a high risk of leading proof performance problems when dealing with even moderately large numbers.Here are a couple examples that will both report a maximum recursion depth error currently. These examples are fixed by this PR.