simpl
Require Import
Print
Inductive
Definition
Fixpoint
Lemma
Theorem
Proof
Qed
intro
intros
induction
unfold
fold
apply
simpl
rewrite
reflexivity
case
discriminate
trivial
assumption
（＊＊ Remark 今回はZArithモジュールを使うよ。 Require Import ZArith. をタイプしてね。 ＊） 導入 Coqでは、整数全体の型はZで表され、次のように定義されている。 Coq Z | Zneg : positive -> Z Z0はゼロで、Zposは正の数、Znegは負の数を表している。…
今日はCoqを使って大学院試験を解いてみよう。 題材は京都大学 理学研究科 数学専攻の数学の問題だ。 せっかくなので一番 新しい平成１９年度の問題に挑戦してみよう。 （＊＊ 注意！！今回Coqを使ってこの問題を解いたが、Coqが大学院試験を自動的に解いた…
