Hi, newbie here, struggling to prove `(a :: l)%list = (a :: nil)%list`

from `h: length (a :: l) = 1`

. How to do it?

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`

).

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`

.

Just tried `discriminate`

and it's easier this way for sure.

Last updated: Feb 01 2023 at 11:04 UTC