pattern match proof

Stream: new members

[Jem Bishop]

Hi I need to prove the termination of this function:

| [] n := (0, 0)
| [x] n := (0, 0)
| l n := let h := head l, t := lastn l in match cmp (h + t) n with
    | eq :=  (h, t)
    | gt := have (initial l).sizeof < l.sizeof,
            from sizeof_less_initial l (by sorry), find_sum_num (initial l) n
    | lt := have (tail l).sizeof < l.sizeof,
            from sizeof_less_tail l (by sorry), find_sum_num (tail l) n
    end

Within this where the by sorry is I need a proof that l is not nil . It obviously is as otherwise the function
would have matched at the first case. When I try to enter the proof here though this fact does not seem to be there. Any idea how I get the fact l is not nil here?

[Kevin Buzzard]

Why not match on a :: L instead of l?

[Kevin Buzzard]

then you get it for free

[Kevin Buzzard]

or even on a :: b :: L

[Jem Bishop]

yeah thats a good point, thanks for your help

[Kevin Buzzard]

PS you're right, the fact that l isn't nil really isn't there, the way you have it set up.