How to indicate empty matches in Lean 4

Stream: lean4

[François G. Dorais]

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.

[François G. Dorais]

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

[Notification Bot]

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

[Mario Carneiro]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

We use . in lean3

[Sebastian Ullrich]

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

[Mario Carneiro]

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

[Jannis Limperg]

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.

[Mario Carneiro]

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

[Sebastian Ullrich]

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

[Jacques Carette]

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

[Leonardo de Moura]

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.

[Jannis Limperg]

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