懲りずにCoq

Logic_J.vまで一応読了。分からん問題は答え見てもさっぱり分からん。
殊にappears_inがらみがまるで歯が立たなかった。

途中 一つQed.を書き忘れて、

Error: There are pending proofs

とかエラーが出てcoqcが失敗して難儀した。括弧の対応が取れてないような初心者はすっこんでろということなんだろうが、せめてどこの証明が終了してないかくらいエラーで出してくれてもバチは当たらんと思う。

Coqで証明出来ない(理由はようわからん)論理式一覧。

Definition peirce := forall P Q : Prop,
  ((P->Q) -> P)->P.
Definition classic := forall P : Prop,
 ~~P -> P.
Definition excluded_middle := forall P:Prop,
  P \/ ~P.
Definition implies_to_or := forall P Q:Prop,
  (P->Q) -> (~P\/Q).