proving list nonempty by pattern match

Stream: lean4

[James Sully]

if I have list : List Int, and

match list with
| [] => ...
| List.cons _ _ => ...

What's the syntax for obtaining a proof of list ≠ [] in the second branch?

[Shreyas Srinivas]

match h : list with
| [] => ...
| List.cons _ _ => ...

[Shreyas Srinivas]

You should have the hypothesis h : list = List.cons ..... inside the cons arm. Then you can introduce a local have declaration in the cons arm. With a little bit of simp on h, you should be able to get the proof of list ≠ []

[James Sully]

neat it works, thank you! I'm trying to understand what this means... h is given the type of the value of the list?? Where can I read about what's going on here?

[Shreyas Srinivas]

I am not sure there is a deeper explanation. Every inductive type comes with a casesOn recursor. This is produced by lean along with rec.

[Shreyas Srinivas]

If I remember this correctly, match uses the cases recursor.

[James Sully]

I will read through this chapter: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html

[Shreyas Srinivas]

If you are referring to the name h, its type is a value of Prop. It is an equality.

[James Sully]

h for hypothesis?

[Shreyas Srinivas]

h is a name I picked. You can give it whatever name you like

[James Sully]

sure, I'm asking about the convention

[Shreyas Srinivas]

James Sully said:

h for hypothesis?

That's my best guess. I have never bothered to ask (maybe I should have).

[Kyle Miller]

James Sully said:

h is given the type of the value of the list??

h is given a proof that list equals the given pattern for the given match arm

[Kyle Miller]

(and yeah, I think h is "hypothesis". it's often used as a prefix for proof variables, like hpos : 0 < x for the fact that x is positive)

[James Sully]

ah, I see

[James Sully]

thanks both!

[Kyle Miller]

This notation by the way appears in a few other constructs, like if h : x = 0 then ... else ..., which gives you h : x = 0 in the true case and x : Not (x = 0) in the false case, or for h : x in lst do ... to get a proof that x is in lst in the loop body.

[James Sully]

Oh nice, that's good to know.

[James Sully]

Would the by simp [h] bottom out in a List.noConfusion?

[James Sully]

if written out explicitly?

[Kyle Miller]

I assume you mean if you have something like have : list ≠ [] := by simp [h] in the second branch? Yeah, that sounds right.

[James Sully]

yep. ok cool

[Kyle Miller]

You could also do by intro h'; cases h.symm.trans h' (untested!), which would also use List.noConfusion. The h.symm.trans h' should be something :: something = []

[James Sully]

that also works. I'm not familiar with the cases tactic yet, I've only used cases' from the Lean Game Server, which I think is a simplified version

[Kyle Miller]

cases' is like cases but it has different syntax for how you name hypotheses (it's the Lean 3 style cases tactic)

[James Sully]

Oh is the h.symm.trans just function application? Like trans (symm h)

[Kyle Miller]

It takes a bit of a leap into dependent type theory to see why cases on an equality makes sense, but all you need to know is that it tries to make both sides of an equality exactly the same. That might mean substituting variables automatically, or, in this case, realizing we're in an impossible situation and close the goal using List.noConfusion.

[Kyle Miller]

Oh, yeah, h.symm.trans h' is Eq.trans (Eq.symm h) h'.

[James Sully]

what's the type of h.symm.trans?

[James Sully]

i'm trying to extract it into a have to understand better

[James Sully]

If i'm understanding right:

h.symm : x :: xs = list
h.symm.trans : (list = c) -> x :: xs = c

[James Sully]

I wrote it out in excruciating detail and I'm starting to understand haha

      match h : digits with
        | [] => none
        | x :: xs =>
            have digits_ne_nil : digits ≠ [] := by
              -- simp [h]
              -- or
              -- rw [h]
              -- exact λ h2 => List.noConfusion h2
              -- or
              intro (h1 : digits = [])
              have h2 {c} : (digits = c) → x :: xs = c := h.symm.trans
              have h3 : x :: xs = [] := h2 h1
              cases h3