Getting evidence from a match statement

Stream: new members

[Mark Fischer]

So I noticed that List.findIdx?_of_eq_some returned proof of a match statement. It looks close to what I need, but I'm not sure whether it really is as I'm not sure how to think about interacting with a term like this.

My Proof state is as follows:

h : match List.get? (Finset.sort LE.le l.idxs) i with
| some a_1 => (l.l[a_1] == a) = true
| none => false = true
⊢ l.l[(Finset.sort LE.le l.idxs)[i]] = a

I could create a more minimal example, but I'm not sure if this even a helpful direction to explore in the first place.

[Timo Carlin-Burns]

This goal looks provable from h. There's a handy tactic for this sort of situation called split. split at h should get you pretty close.

[Mark Fischer]

:) thanks. That looks promising!

[Timo Carlin-Burns]

What split does under the hood is case analysis on the discriminant of the match (the value being inspected). You could do that manually too. If the discriminant was just a variable, it would be easy: just cases, but here since it's a more complicated expression you would need to use cases h2 : List.get? (Finset.sort LE.le l.idxs) i. That would give you hypotheses like h2 : List.get? (Finset.sort LE.le l.idxs) i = some x which you could use with simp [h2] at h

[Mark Fischer]

I didn't realize you could do that with cases, though I suppose that makes sense if I stare at it before a bit. It would be like

let h2 := List.get? (Finset.sort LE.le l.idxs) i
cases h2

[Timo Carlin-Burns]

Yeah although I think cases on h2 there would cause Lean to forget how h2 was defined, losing your desired equation. generalize is more appropriate

generalize h2 : List.get? (Finset.sort LE.le l.idxs) i = discr at h
cases discr

[Mark Fischer]

I see what you mean