Detecting match case unreachability

Stream: lean4

[Raghuram]

namespace Temp

open Option (none some)

variable [LE α] [DecidableRel (α := α) (· ≤ ·)]

def min : List α → Option α
| []    => none
| a::as => some <| match min as with
  | none    => a
  | some a' => if a ≤ a' then a else a'

def min' (l : List α) (h : l ≠ []) : α := match l, h' : min l with
| [],   none   => absurd rfl h
| _::_, some a => a

end Temp

In the above (using the stable channel of Lean 4 i.e. 4th milestone release), removing the h' : from min l results in match complaining about the missing case cons, none. Why does this make a difference?
Also, using the nightly version, match complains about the missing case regardless of whether I include h' : .

[Leonardo de Moura]

The match compiler uses the contradiction tactic before reporting a missing case. When we add the annotation h' : min l, we are instructing the match compiler to add a new hypothesis saying that h' : min l = <pattern> in each case. The contradiction tactic uses this information when trying to discharge the missing case. In the m4 milestone, in the cases _::_, none, we have h' : min (_::_) = none, which can be detected by the contradiction tactic as contradictory. Example:

example (a : α) (as : List α) (h : min (a :: as) = none) : False := by
  contradiction

Since the m4 release, we have modified how the annotation h' : min l is compiled to address issues raised by users. In the new encoding, in the missing branch, the hypothesis is h' : min l = none. Unfortunately, the contradiction tactic cannot detect the contradiction anymore. Here is a way to handle that using the nightly build.

def min' (l : List α) (h : l ≠ []) : α :=
  match h₁ : l, h₂ : min l with
  | [],   none   => absurd rfl h
  | _::_, none   => by subst h₁; contradiction
  | _::_, some a => a

Note that I annotated both discriminants, and the goal for the _::_, none is

...
h₁ : l = head✝ :: tail✝
h₂ : min l = none
⊢ α

subst h₁ transforms the goal into

...
h₂ : min (head✝ :: tail✝) = none
⊢ α

which can now be discharged by the contradiction tactic.
BTW, in the future, we want to allow users to specify their own tactics for detecting "unreachable" cases.

[Raghuram]

Leonardo de Moura said:

When we add the annotation h' : min l, we are instructing the match compiler to add a new hypothesis saying that h' : min l = <pattern> in each case. The contradiction tactic uses this information when trying to discharge the missing case.

Ah, I see. I thought that the purpose of that syntax was only to make that fact user-accessible and that match 'knew' it regardless.

Now that I know this, I thought to check, and the [], none case can actually be omitted too, even without h1 or h2 (both stable and nightly).

[Raghuram]

BTW is subst documented anywhere other than the docstring? I can't seem to find it in Theorem Proving in Lean 4 or the manual, and I didn't know it existed until now. (Although in this case rw [h1] at h2; works just as well.)