Matching wildcards

Stream: new members

[Henry Towsner]

Working in lean 4, I have a term defined by a match involving two terms with some specific cases I pull out and then a wildcard case covering everything else.

For a somewhat simplified example, something like this:

def diag (a:ℕ) (b:ℕ) : Prop :=
match a, b with
| 0, 0 => true
| 1,1 => true
| _, _ => false

I'm running into trouble proving anything about the wildcard case, though (e.g. lemma x (a:ℕ) (b:ℕ) : diag a b → (a=0∨ a=1) ). When I try to use the same match set up in the proof, the wildcard case doesn't seem to have any hypothesis recognizing that it's not in one of the overlapping cases, so I can't prove it that way, and I haven't been able to make other tactics (e.g. cases) work either, though perhaps there's a subtlety I haven't caught.

(In this case handling the cases manually with by_cases or the like wouldn't be so bad, but the actual example involves more cases and I need to prove several lemmas that all parallel the match structure of the definition, so it would be nice to have a structured way to do this.)

[Mario Carneiro]

the easiest way to reason about this function is to use the split tactic after it appears in the goal

[Henry Towsner]

How does one use the split tactic? When I use it unmodified, it says "tactic 'split' failed", and when I try something like "split diag" it says "'split' tactic, term to split is not supported yet", and I can't seem to figure out the right way to use it.

[Henry Towsner]

Aha, found it. The answer, for anyone else with the same problem, is that you have to unfold or expand the definition into a big match expression before using split.