Stream: new members

Topic: pattern match proof

Jem Bishop (Dec 01 2020 at 22:13):

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 (Dec 01 2020 at 22:13):

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

Kevin Buzzard (Dec 01 2020 at 22:14):

then you get it for free

Kevin Buzzard (Dec 01 2020 at 22:14):

or even on a :: b :: L

Jem Bishop (Dec 01 2020 at 22:18):

yeah thats a good point, thanks for your help

Kevin Buzzard (Dec 01 2020 at 22:19):

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

Last updated: May 16 2021 at 20:13 UTC