というわけで、Coq入門編その一、forall と -> だけ使った定理の証明、をお届けしました。気が向いたら「and, or, not を使った定理の証明」「exists を使った定理の証明」「帰納法」「forallと->と依存型について本気出して考えてみた」… の順番で続きます…

ここまでに紹介した apply と intro(s) は、どちらも、証明のゴールを変形する tactic でした。なのですが、これってあまり直感的ではない気がするのですよね。私見ですが。 「A と B と C を仮定して Z を証明して下さい！」 って言われたときに 「Cが使え…

別の例をやってみたいと思います。Sコンビネータと呼ばれる定理です。 Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R.いきなりexactで書いてもいいんですが、順を追ってやっていきましょう。 intros.「ゴールにforallや->があったら、と…

ところで、HaskellやOCamlなどの関数型言語をご存じの方なら100倍高速にCoqを理解できる！というショートカットのご紹介です。以下、この節限定で、説明にHaskellが混じります。Haskellわからんという人はこの節は飛ばしても以降に差し支えはない…はず…たぶ…

いくつか細かい捕捉。introintrosと同じひっぺがし作業を１回だけやる単数形にすると「1回だけやる」意味になります。introsだとやれるまでやってしまうので、今回の例だと4個全部はがしちゃいますが Theorem Modus_ponens: forall (P: Prop), forall (Q: Pr…

Modus Ponens 一番最初の例として Anarchy Proof 第1問: http://as305.dyndns.org/aps/problem/view/1 を証明してみよう。古代ギリシャから伝わる "Modus Ponens" とよばれる定理「"PならばQ" であり、しかも "P" ならば、それすなわち "Q" である」です。こ…

証明支援系Coqの遊び方の入門を書いてみるよ。すでに世の中に何個も入門記事ありますけど、増えて困ることはなかろう…ということで。まず、インストール方法については、id:yoshihiro503 による紹介記事 http://d.hatena.ne.jp/yoshihiro503/20070706#p1 最…