ポジティブ型とマイポジティブ型

（＊＊ Remark 今回はZArithモジュールを使うよ。 Require Import ZArith. をタイプしてね。＊）導入 Coqでは、整数全体の型はZで表され、次のように定義されている。 Coq Z | Zneg : positive -> Z Z0はゼロで、Zposは正の数、Znegは負の数を表している。…

2007-07-24

大阪人に関するうわさ

Section Variable Hypothesis Theorem Proof Qed tauto

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

2007-07-20

定義と、その展開

Coq入門 Definition Theorem Proof unfold reflexivity

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

2007-06-28

データベースを用いるWebアプリケーション

Fixpoint Lemma Theorem Proof Qed intro intros case unfold fold induction reflexivity rewrite elim inversion apply assumption

お客さんがWebブラウザを使って、入力項目をデータベースに登録したり、データベースからデータを取ってきたりする仕組みは、多くの場所に存在するだろう。このような仕組みは比較的簡単に提供することができ、かつ、利用する人の生活を便利にしてくれる。…

2007-06-27

Coqで大学院試験

Definition Proof Theorem Lemma Qed exists intro intros case unfold elim simpl reflexivity apply

今日はCoqを使って大学院試験を解いてみよう。題材は京都大学理学研究科数学専攻の数学の問題だ。せっかくなので一番新しい平成１９年度の問題に挑戦してみよう。（＊＊注意！！今回Coqを使ってこの問題を解いたが、Coqが大学院試験を自動的に解いた…

2007-06-26

さあ！証明しよう！

Coq入門 Proof

今日紹介するコマンドはProofコマンドだ。このコマンドは何もしない。 Proofというからには、自動証明をやってくれるだろう、とか、何かすごいCoqの力で証明が変形するのかな、とか思う人がいるかもしれないが、このコマンドは何もしない。このコマンドを…

2007-06-20

なぜか無い補題

雑談 Lemma Require Import Open Scope Proof Qed intros apply rewrite

Coqのライブラリにはなぜか無い補題というものがある。例えばZmult_le_reg_rというレンマはZArithのZorderライブラリにあるが、これの左バージョンは無いのだ。ちなみにZmult_le_reg_rとは次のような内容である。 Zmult_le_reg_r : forall n m p:Z, p > 0…