Zulip Chat Archive

Stream: general

Topic: inversion tactic

Jakob von Raumer (Jan 06 2021 at 21:36):

Is anybody aware of any implementations of an inversion tactic in Lean 3?

Jannis Limperg (Jan 06 2021 at 21:36):

cases is probably what you're looking for.

Wojciech Nawrocki (Jan 06 2021 at 21:51):

There is also a (possibly outdated) Coq-Lean cheatsheet.

Jakob von Raumer (Jan 06 2021 at 21:52):

Does cases create the equalities as in that contains0 example in the Coq Doc?

Jakob von Raumer (Jan 06 2021 at 22:04):

It seems not, unfortunately

Eric Wieser (Jan 06 2021 at 22:07):

Can you give a lean example showing what tactic state you actually want?

Eric Wieser (Jan 06 2021 at 22:07):

(and are you looking for cases h : x?)

Jannis Limperg (Jan 06 2021 at 22:12):

Jakob von Raumer said:

Does cases create the equalities as in that contains0 example in the Coq Doc?

cases substitutes the generated equations immediately, so you don't get to see them. This is like Coq's
inversion_clear.

Jakob von Raumer (Jan 06 2021 at 22:17):

Ah I guess, I can then easily write a wrapper around cases that gets me the equalities

Eric Wieser (Jan 06 2021 at 22:21):

cases with the colon generates the equations and also substitutes them, but without discarding them

Jakob von Raumer (Jan 06 2021 at 22:24):

Ah, completely missed the colon

Last updated: Dec 20 2023 at 11:08 UTC