Zulip Chat Archive

Stream: lean4

Topic: How to indicate empty matches in Lean 4


view this post on Zulip François G. Dorais (Jan 05 2021 at 11:22):

In Lean 3, a period can be used to indicate an empty match:

inductive test : bool  Type | of_tt : test tt

def test_ff_is_empty : test ff  empty .

Is there a similar thing in Lean 4? I can make it work using tactic mode:

inductive Test : Bool  Type | ofTrue : Test true

def testFalseIsEmpty : Test false  Empty := by {intro x; cases x}

Since Test has a parameter, using recursors directly is a major pain. Nothing else I tried seems to work.

view this post on Zulip François G. Dorais (Jan 05 2021 at 12:01):

Perhaps I should have waited a few minutes and posted to #lean4

view this post on Zulip Notification Bot (Jan 05 2021 at 12:02):

This topic was moved here from #general > How to indicate empty matches in Lean 4 by Rob Lewis

view this post on Zulip Mario Carneiro (Jan 05 2021 at 12:04):

I started trying to port logic.basic and got stuck on the very first proof for this reason :)

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 12:07):

def testFalseIsEmpty (t : Test false) : Empty := nomatch t

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 12:07):

Zero-case match doesn't exactly work after we removed the end token from it, so a new keyword it is

view this post on Zulip Mario Carneiro (Jan 05 2021 at 12:08):

We use . in lean3

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 12:11):

Which really is a workaround using a feature no-one uses in any other case. I much prefer this very explicit form.

view this post on Zulip Mario Carneiro (Jan 05 2021 at 12:12):

Does it still create equation lemmas? In lean 3 there is a difference between match and def match in the equation lemmas you get out

view this post on Zulip Jannis Limperg (Jan 05 2021 at 12:13):

Is this equivalent to Agda's solution? They have a separate pattern for impossible matches; in Lean it would look like this:

def testFalseIsEmpty (t : Test false) : Empty
| ()

The paper about Agda's method argued, afair, that having a separate form for this is crucial, particularly when the impossibility only becomes apparent after you've matched on some other things.

view this post on Zulip Mario Carneiro (Jan 05 2021 at 12:14):

Obviously we've got by in lean 3 without having to explicitly indicate this, although occasionally lean will miss an impossible case in a dependent pattern match situation like matching on fin 3

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 12:25):

Mario Carneiro said:

Does it still create equation lemmas? In lean 3 there is a difference between match and def match in the equation lemmas you get out

Equation lemmas are TBD AFAIK. But syntactic equations are expanded to match, so there should not be any difference: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Binders.lean#L415-L442

view this post on Zulip Jacques Carette (Jan 05 2021 at 20:15):

Yes, @Jannis Limperg , that is equivalent to Agda's solution.

view this post on Zulip Leonardo de Moura (Jan 05 2021 at 20:36):

The paper about Agda's method argued, afair, that having a separate form for this is crucial, particularly when the impossibility only becomes apparent after you've matched on some other things.

It is not crucial for Lean since we can have nested (dependent) match-expressions. We also have tactics (i.e., we can always use by cases x).
I consider this feature as a very low priority.

view this post on Zulip Jannis Limperg (Jan 05 2021 at 20:51):

That's fair -- I guess in Lean we can always give the case tree that Agda compiles to. Thanks for the responses!


Last updated: May 18 2021 at 22:15 UTC