Tactics

Stream: lean4

[Calvin Lee]

I'm pretty new to tactics, so please excuse my ignorance.
What's the difference between rw and erw? Also does simp not work on lean4? I'm getting a sorry when I try to use it.

[Mario Carneiro]

simp doesn't exist in lean 4 yet

[Mario Carneiro]

the docstring for erw says

/--
A variant of `rewrite` that uses the unifier more aggressively, unfolding semireducible definitions.
-/

[Calvin Lee]

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]

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]

Mario Carneiro said:

simp doesn'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]

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]

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.