## Stream: Coq users

### Topic: newbie question

#### 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: Jun 25 2024 at 14:01 UTC