世の中には大阪人に関する間違った認識があふれているように思う。 例えば、大阪人は縦縞のユニフォームを着ている、とか嫁さんが強くてカカア天下である、とかである。今回はそのような間違った俗説を払拭するべくCoqで証明してみた。 Coq Section なにわ. …

Definitionコマンドを使って型や、関数を定義することができるが、証明の中で、定義に戻って展開したくなる時がある。例えば次のような２足す関数を定義して、それを二回適用すると4になるような定理を証明したい場合を考える。 Welcome to Coq 8.1 (Feb. 20…

最近パソコンを買ったんだけど、使い方がよく解らない。という人のために、今日はCoqのインストールの方法を紹介しよう。 対象となる OS はWindows Vistaだ!Coqはだいたい次の３ステップで、使うことが出来る。恐れずに挑戦してみよう。 1。CoqのサイトからC…

なぜかCoqのサイトやOCamlのサイトなどが見れない。 困った。同じようなページが↓にあるようだ。とりあえず、ここを参考にしよう。 http://pauillac.inria.fr/coq/coq-eng.html