intro
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は負の数を表している。…
Fixpoint
Lemma
Theorem
Proof
Qed
intro
intros
case
unfold
fold
induction
reflexivity
rewrite
elim
inversion
apply
assumption
お客さんがWebブラウザを使って、入力項目をデータベースに登録したり、データベースからデータを取ってきたりする仕組みは、多くの場所に存在するだろう。 このような仕組みは比較的簡単に提供することができ、かつ、利用する人の生活を便利にしてくれる。…
今日はCoqを使って大学院試験を解いてみよう。 題材は京都大学 理学研究科 数学専攻の数学の問題だ。 せっかくなので一番 新しい平成19年度の問題に挑戦してみよう。 (** 注意!!今回Coqを使ってこの問題を解いたが、Coqが大学院試験を自動的に解いた…
証明モードのときは今までのCoqコマンドに加えて、タクティックというものを使うことができる。 タクティックは必ず小文字で始まり、ドットで終わる。 s intro. A : Prop ======================================= forall B C:Prop, (A->B->C) -> (A->B) -> …