Zulip Chat Archive

Stream: lean4

Topic: Detecting match case unreachability


Raghuram (May 20 2022 at 07:59):

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 (May 20 2022 at 13:11):

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 (May 20 2022 at 15:50):

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 (May 20 2022 at 16:00):

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.)


Last updated: Dec 20 2023 at 11:08 UTC