Zulip Chat Archive

Stream: new members

Topic: Getting equation from match


view this post on Zulip 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?

view this post on Zulip Chris B (Feb 16 2020 at 13:18):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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