coq - Coqで誤った仮説を立てて証明を終了する

Question

したがって、サブゴールに誤った仮説があります。これは、異なるコンストラクター間の同等性です。サブゴールを終了するにはどうすればよいですか？

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

Answer 1

これは私が標準ライブラリから慣れているCoqリストのようには見えないので、List.Not_EmptyとList.Emptyの定義を知らなければあなたを助けるのは難しいでしょう。List.Emptyを表すとをnil正しくList.Not_empty推測するconsと、2つのコンストラクターが等しくないことを示すだけです。たとえば、次のことができます。

congruence.

または単に：

inversion H.

ただし、もっと複雑な場合は、これら2つが失敗する可能性があります。したがって、次のいずれかを実行する必要があります。

SearchAbout List.Not_Empty.

それについて見出語が存在するかどうかを確認するため、または次のことを行います。

unfold List.Not_Empty, List.Empty in H.

定義を展開し、詳細を理解するため（このサブプルーフが存在しない場合は、有用と思われるため、補題として保存する可能性があります）。