## Stream: new members

### Topic: Getting equation from match

#### Anton Lorenzen (Feb 16 2020 at 09:05):

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

#### Chris B (Feb 16 2020 at 13:18):

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

#### Anton Lorenzen (Feb 16 2020 at 13:59):

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 (Feb 16 2020 at 17:45):

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 (Feb 17 2020 at 21:29):

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 (Feb 17 2020 at 21:31):

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 (Feb 18 2020 at 03:26):

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 (Feb 18 2020 at 08:24):

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 (Feb 18 2020 at 11:05):

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 (Feb 18 2020 at 11:06):

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 (Feb 18 2020 at 11:13):

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.

Last updated: May 06 2021 at 22:13 UTC