elim
Fixpoint
Lemma
Theorem
Proof
Qed
intro
intros
case
unfold
fold
induction
reflexivity
rewrite
elim
inversion
apply
assumption
お客さんがWebブラウザを使って、入力項目をデータベースに登録したり、データベースからデータを取ってきたりする仕組みは、多くの場所に存在するだろう。 このような仕組みは比較的簡単に提供することができ、かつ、利用する人の生活を便利にしてくれる。…
今日はCoqを使って大学院試験を解いてみよう。 題材は京都大学 理学研究科 数学専攻の数学の問題だ。 せっかくなので一番 新しい平成19年度の問題に挑戦してみよう。 (** 注意!!今回Coqを使ってこの問題を解いたが、Coqが大学院試験を自動的に解いた…