Terminer la preuve avec une fausse hypothèse dans Coq

Question

J'ai donc une fausse hypothèse dans un sous-objectif. C'est une égalité entre différents constructeurs. Comment puis-je terminer le sous-objectif?

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

Answer 1

Cela ne ressemble pas à la liste Coq je suis habitué de la bibliothèque standard, il sera difficile de vous aider sans connaître les définitions de List.Not_Empty et List.Empty. Si je devine correctement que List.Empty signifie nil et List.Not_empty signifie cons, alors il s'agit juste de montrer que les deux constructeurs ne sont pas égaux. Vous pouvez par exemple faire:

congruence. 

ou simplement:

inversion H. 

Cependant, si elle est quelque chose de plus impliqué, ces deux risque d'échouer. Donc, vous voudriez soit:

SearchAbout List.Not_Empty. 

pour voir si lemmes existent à ce sujet, ou à:

unfold List.Not_Empty, List.Empty in H. 

à se dérouler définitions et les travaux les détails (peut-être sauver ce subproof comme si lemme cela n'existe pas, car cela semble utile).