Things in Rocq I want in Lean

Stream: LFTCM 2024

[Riccardo Brasca]

This is a random list of things I am seeing the Rocq tutorial and I would like to have in Lean (maybe the're already there and I don't know it):

• the abort command

[Riccardo Brasca]

• have ->

[Riccardo Brasca]

• rewrite seems easier to combine with other tactics

[Riccardo Brasca]

• rw [in ...]

[Johan Commelin]

• search in the middle of a tactic script

[Johan Commelin]

• have -> : some_prop := by proof as alternative to rw [show some_prop by proof]

[Floris van Doorn]

Re: have ->: I think it makes sense to add ← and → as rcases patterns, to rewrite with the term immediately (forwards and backwards) and then clear it. Then you can write obtain → : ... := ...

[Johan Commelin]

Yeah, I don't mind whether it is have or obtain. I can also imagine that those two tactics get merged anyways.

[Cyril Cohen]

What is the difference between have and obtain btw?

[Anne Baanen]

have x : P := Q requires that x is a single variable, while obtain accepts any destructuring pattern.

[Anne Baanen]

So obtain is strictly more powerful than have. And obtain and rcases are the same, apart from syntax.

[Eric Rodriguez]

Have does some destructuring now, I think

[Richard Osborn]

I believe you can write obtain rfl : a = b := ... in current lean.

[Edward van de Meent]

there is some difference though... i believe obtain a := b removes b from the context, while have a := b doesn't...

[Edward van de Meent]

so it's not exactly strictly more expressive