Stream: Coq users

Topic: newbie question


view this post on Zulip Valéry Croizier (Jul 16 2020 at 09:59):

Hi, newbie here, struggling to prove (a :: l)%list = (a :: nil)%list from h: length (a :: l) = 1. How to do it?

view this post on Zulip Kenji Maillard (Jul 16 2020 at 10:05):

You want to do a case analysis on l (using destruct, case...) in order to obtain that l can be either a nil or a cons _ _ and then discard the second case by simplifying/computing your hypothesis h (with cbn in h or simpl in h) to h : S (S (length ...)) = 1 which is contradictory (you can tell that to coq with discriminate h).

view this post on Zulip Valéry Croizier (Jul 16 2020 at 10:13):

Thanks. Actually I did exactly the same thing a bit earlier in the proof and discarded the absurd case with exfalso. inversion h., but I didn't think I needed to destruct again. Will have to look into those cbn and discriminate.

view this post on Zulip Valéry Croizier (Jul 16 2020 at 10:15):

Just tried discriminate and it's easier this way for sure.


Last updated: Feb 01 2023 at 11:04 UTC