Getting equation from match

Stream: new members

[Anton Lorenzen]

Is it possible to get an equation from a match statement similar to cases h : e or if h : p?

[Chris B]

Can you give an example of what you want to get?

[Anton Lorenzen]

Sure! In the minimal example below I want to fill in sorry:

inductive AB | A | B

def useAB (ab : AB) : unit := match ab with
| AB.A := let h : ab = AB.A := sorry in ⟨⟩
| AB.B := let h : ab = AB.B := sorry in ⟨⟩
end

[Anton Lorenzen]

Also, isn't this what set_option eqn_compiler.lemmas true is supposed to be doing? Or am I confusing something here?

[Floris van Doorn]

The short answer is "no": in the body of a match statement like that, you should not use the variable ab anymore.
There is probably some match-trickery you can do to mimic the behavior you want, though...

[Floris van Doorn]

Here is you match trickery:

inductive AB | A | B

def useAB (ab : AB) : unit := match (⟨ab, rfl⟩ : {x : AB // ab = x}) with
| ⟨AB.A, h⟩ := let h : ab = AB.A := h in ⟨⟩
| ⟨AB.B, h⟩ := let h : ab = AB.B := h in ⟨⟩
end

[Mario Carneiro]

You can also do it without the tupling if you make use of the "match-return" clause:

inductive AB | A | B

def useAB (ab : AB) : unit :=
match ab, rfl : ∀ x : AB, ab = x → unit with
| AB.A, h := let h : ab = AB.A := h in ⟨⟩
| AB.B, h := let h : ab = AB.B := h in ⟨⟩
end

[Kevin Buzzard]

This is not the first time that this really cunning match trick has come up! Maybe it should be documented somewhere? TPIL might be the natural place for it?

[Anton Lorenzen]

I wanted to write up a small document with Lean tips and tricks not covered in TPiL anyway; I am going to include this trick there.

[Anton Lorenzen]

I don't understand though why Lean doesn't have special syntax for this, when it is so natural to get the same effect in tactics mode with cases h : ab

[Kevin Buzzard]

If it's in core then it's hard to change. Mathlib is not just a mahs library -- it has got an extensive set of tactics and other workarounds which have been an attempt to make the frozen Lean 3.4.2 better. It has taken the community a year or so to decide that it is now worth letting mathlib master track Lean 3.5c, and this only happened a few weeks ago. Changes to core are hard, often needing C++ skills which not everyone here has, as well as a good understanding of the core code. Writing another tactic to do something can often be done in Lean itself.