Valéry Croizier (Jul 16 2020 at 09:59): 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?
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).
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.
Valéry Croizier (Jul 16 2020 at 10:15):Just tried discriminate and it's easier this way for sure.
Last updated: Oct 05 2023 at 02:01 UTC