Calvin Lee (Jan 28 2021 at 23:15):
I'm pretty new to tactics, so please excuse my ignorance.
What's the difference between
erw? Also does
simp not work on lean4? I'm getting a
sorry when I try to use it.
Mario Carneiro (Jan 28 2021 at 23:18):
simp doesn't exist in lean 4 yet
Mario Carneiro (Jan 28 2021 at 23:19):
the docstring for
/-- A variant of `rewrite` that uses the unifier more aggressively, unfolding semireducible definitions. -/
Calvin Lee (Jan 28 2021 at 23:21):
Ok, so is there no way to, say, try a tactic in several places until it succeeds then?
e.g. if I wanted to apply
rw [Nat.mulComm] but on the second or third term where it would be valid?
Mario Carneiro (Jan 28 2021 at 23:22):
this is not really a lean 4 question, but you can use
rw [Nat.mulComm a] or
rw [Nat.mulComm a b] to limit the matches to the one you want
Daniel Selsam (Jan 28 2021 at 23:23):
Mario Carneiro said:
simpdoesn't exist in lean 4 yet
FYI it is still missing some features but much of the functionality is already there, e.g. https://github.com/leanprover/lean4/blob/master/tests/lean/run/simp4.lean
Calvin Lee (Jan 28 2021 at 23:26):
Ok, I'll try to post in #new members about tactic proofs. I wasn't sure if I would run into lean4 specific behavior that would send me back here :smile:
Kyle Miller (Jan 28 2021 at 23:30):
A new Lean 4 thing you can do is
rw [Nat.mulComm (m := a)] rather than
rw [Nat.mulComm _ a], supposing you knew
m was the name of the second argument. This is more useful for lemmas with multiple arguments, especially implicit ones.
Last updated: May 18 2021 at 22:15 UTC