In pattern match fallthrough cases prove ¬ matched cases?

Stream: new members

[aron]

Is it possible in a match expression to prove for the fallthrough pattern that the value you're matching on is none of the previously matched patterns?

I feel like this should be possible since Lean should be able to see that you have already matched on the other cases and therefore this fallthrough is none of those cases

inductive T
  | a
  | b
  | c
  | d
  | e

inductive R : (t : T) → Type
  | fromA : R .a
  | fromB : R .b
  | other : (t : T) → (prf : t ≠ .a ∧ t ≠ .b) → R t

def m (t : T) : R t :=
  match h : t with
  | .a => .fromA
  | .b => .fromB
  | _ => by
    refine .other _ ?_
    -- I want to be able to use `h` here to prove that `t` is neither `.a` or `.b`
    sorry

[aron]

Without this, the only alternative is to stick a potentially very large number of patterns in your match expression. Depending on the number of variants you have and how many values you're matching on in the same pattern this could result in an enormous number of patterns to match. Whereas if you could access the proof that the value is none of the constructors you're interested in, you could handle them all in parallel using tactics

[aron]

Here's a real life example for the number of patterns I need to add to eliminate false cases – and this is just a small sample of all the patterns I'm going to have to add :cry: the unhappy paths outnumber the happy ones by 5 to 1. There must be a better way to do this

Screenshot 2025-06-08 at 13.21.22.png

[Aaron Liu]

Would if-then-else expressions work?

[aron]

Alas no. For two reasons: 1 if/else expressions are more tedious especially for large numbers of checks, plus 2. you can only check boolean equalities with them, you can't use them to pattern match. So there's no way to do something like .prim _

[Aaron Liu]

I know the cases tactic can handle this kind of stuff, but for match I don't know of any way to do it.

[aron]

Can cases be used in the same way as match can? For types also or just props?

[aron]

Like is there a difference between them other than some minor ergonomics?

[Aaron Liu]

You can, though I think there's a chance you might need to mark the result noncomputable since the compiler doesn't yet support raw recursors, and also you have little control over the term it produces.

[aron]

Ah ok that would be a problem because I want to match on real values, not just props

[Aaron Liu]

What do you mean "match on real values"?

[aron]

Well this is for code to actually run in a program, so doesn't that mean it needs to be computable?

[Aaron Liu]

You can of course compile_inductive to force computability, but if your inductives are recursive this will not be performant

[Aaron Liu]

Actually, since cases uses the .casesOn which does not expose the induction hypothesis, you might just be fine

[Aaron Liu]

The problem is induction which uses the .rec

[Mario Carneiro]

This is done automatically, but for splitter theorems, not match statements directly. So for example if you have a match statement in your goal and want to prove something about it, you can use the split tactic and it will introduce hypotheses for the wildcard cases

[Aaron Liu]

You could make it return a Bool and then prove the theorem after

[Aaron Liu]

Like how prelude sets up docs#Nat.beq before using it to get docs#Nat.decEq

[Mario Carneiro]

Here's a way to exploit the fact that split is basically match but with these extra hypotheses to perform the case split you want, by splitting a match with the right structure but nothing else of interest:

def m (t : T) : R t := by
  let x := match t with | .a | .b | _ => ()
  revert x; split
  · exact .fromA
  · exact .fromB
  · exact .other _ ⟨‹_›, ‹_›⟩

[aron]

@Mario Carneiro mmmm very interesting! although this feels a bit like magic to me atm.

So basically by constructing an otherwise useless value x whose definition involves a match expression according to the cases that you want, the split tactic will give you the hypotheses that the fallback case is none of the previously matched patterns?

[aron]

putting this here as a note for myself for how to extend this pattern when your constructors take some data:

inductive T
  | a
  | b (str : String)
  | c
  | d
  | e

inductive R : (t : T) → Type
  | fromA : R .a
  | fromB str : R (.b str)
  | other : (t : T) → (prf : t ≠ .a ∧ ∀ str, t ≠ .b str) → R t

def m (t : T) : R t := by
  let x := match t with | .a | .b _ | _ => ()
  revert x
  split
  · exact .fromA
  · refine .fromB ?_
  · exact .other _ ⟨‹_›, ‹_›⟩