Finish proof with false hypothesis in Coq

Question

So I have a false hypothesis in a subgoal. It's an equality between different constructors. How do I finish the subgoal?

H: List.Not_Empty Bit.Bit Bit.Zero (List.Empty Bit.Bit) = List.Empty Bit.Bit

Answer 1

This doesn't look like the Coq List I'm used to from the standard library, so it will be hard to help you without knowing the definitions of List.Not_Empty and List.Empty. If I guess correctly that List.Empty stands for nil and List.Not_empty stands for cons, then it's just a matter of showing that the two constructors are not equal. You can for instance do:

congruence.

or simply:

inversion H.

However, if it's something more involved, these two might fail. So you'd want to either:

SearchAbout List.Not_Empty.

to see if lemmas exist about it, or to:

unfold List.Not_Empty, List.Empty in H.

to unfold definitions and work out the details (possibly saving this subproof as a lemma if it does not exist, as it seems useful).