How to prove a match is exhaustive (or similar)

Stream: new members

[Ryan Greenblatt]

I want to be able to use a proposition to show that a match case is impossible.
Something like:

def non_empty_list := {l : list ℕ // l ≠ []}

def extract_first (l : non_empty_list) : ℕ :=
match l.val with
| [] := sorry -- prove impossible
| a::_ := a
end

Anyone know how to do this?

[Kyle Miller]

If you match on l.val, Lean won't specialize h.property to the different cases.

You can match on l itself:

def extract_first (l : non_empty_list) : ℕ :=
match l with
| ⟨[], h⟩ := (h rfl).elim
| ⟨a::_, h⟩ := a
end

I'm using the angle bracket notation, which can be used for any inductive type with only one constructor (like subtype).

[Kyle Miller]

This is also a place where you can merge the match into the def syntax:

def extract_first : non_empty_list → ℕ
| ⟨[], h⟩ := (h rfl).elim
| ⟨a::_, h⟩ := a

[Kyle Miller]

(This actually has some consequences to how Lean generates the "equation lemmas". When you fold in the match syntax, you get

extract_first.equations._eqn_1 : ∀ (h : list.nil ≠ list.nil), extract_first ⟨list.nil ℕ, h⟩ = _.elim
extract_first.equations._eqn_2 : ∀ (a : ℕ) (_x : list ℕ) (h : a :: _x ≠ list.nil), extract_first ⟨a :: _x, h⟩ = a

but if you keep the match separate you get

extract_first.equations._eqn_1 : ∀ (l : non_empty_list), extract_first l = extract_first._match_1 l
extract_first._match_1.equations._eqn_1 : ∀ (h : list.nil ≠ list.nil), extract_first._match_1 ⟨list.nil ℕ, h⟩ = _.elim
extract_first._match_1.equations._eqn_2 : ∀ (a : ℕ) (_x : list ℕ) (h : a :: _x ≠ list.nil), extract_first._match_1 ⟨a :: _x, h⟩ = a

As I understand it, the difference is in what happens when you unfold definitions in a proof. The second one will unfold into extract_first._match_1, but if you unfold this, too, they're otherwise identical.)