4

命題と述語の微積分で数十の補題を証明した後 (他よりも難しいものもありますが、一般的にintro-apply-destructオートパイロットで証明可能です)、w/ から始めて 1 つヒットし、~forallすぐに引っ掛かりました。明らかに、私の Coq に対する理解と知識は不足していました。そこで、一般的な形式のステートメントを証明するための低レベルの Coq テクニックを求めています。

~forall A [B].., C -> D.  
exists A [B].., ~(C -> D).

言い換えれば、反例を設定して起動するための一般的な Coq レシピを期待しています。(上記の関数を量化する主な理由は、それが Coq の原始接続詞 (または) であるためです。) 例が必要な場合は、たとえば次のように提案します。

~forall P Q: Prop, P -> Q.
~forall P: Prop, P -> ~P.

私の提案も回答もしていない関連する質問があるので、重複していないと思います。

4

1 に答える 1

5

~ Pとして定義されていることを思い出してくださいP -> False。つまり、そのような言明を示すためにPは、矛盾を仮定して導出すれば十分です。重要な点はP、仮説としてどのように使用してもよいということです。普遍的に数量化されたステートメントの特定のケースでは、このspecialize戦術が役立つ場合があります。この戦術により、特定の値を持つ普遍的に量化された変数をインスタンス化できます。例えば、

Goal ~ forall P Q, P -> Q.
Proof.
  intros contra.
  specialize (contra True False). (* replace the hypothesis 
                                     by [True -> False] *)
  apply contra. (* At this point the goal becomes [True] *)
  trivial.
Qed.
于 2016-03-01T15:29:48.833 に答える