Zulip Chat Archive

Stream: new members

Topic: pattern match proof


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Dec 01 2020 at 22:13):

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

view this post on Zulip Kevin Buzzard (Dec 01 2020 at 22:14):

then you get it for free

view this post on Zulip Kevin Buzzard (Dec 01 2020 at 22:14):

or even on a :: b :: L

view this post on Zulip Jem Bishop (Dec 01 2020 at 22:18):

yeah thats a good point, thanks for your help

view this post on Zulip 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