プログラミング Coq 〜 絶対にバグのないプログラムの書き方 〜

coq1.v

(* 1.Coqを始めよう @see http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt1.html *)

(* Type: 型の型の一つ。あらゆる型のこと *)
(* Definition: 関数定義 *)
Definition id (A : Type)(x : A) : A := x.

(* 型が nat である引数 n と m を取り戻り値の型が nat である関数plus *)
Definition plus (n : nat)(m : nat) : nat := n + m.


(* prop0 idの証明
fun x => y: 無名関数
Prop : 命題を表す型、PropはTypeに含まれる
forall : 全称量化子 : ∀

命題	<->	型
証明	<->	プログラム

*)
Definition prop0: forall (A: Prop), A -> A :=
    fun A x => x.

(*∀A B C, (B ⇒ C) ⇒ (A ⇒ B) ⇒ (A ⇒ C)*)
(*prop1 A->B, B->Cならば A->Cの証明*)
Definition prop1 : forall (A B C : Prop), (B -> C) -> (A -> B) -> (A -> C) :=
   fun A B C f g x => f (g x).

(*
Definition prop2 : forall (A : Type) (l1 l2 l3 : list A), app l1 l3 = app l2 l3 -> l1 = l2
  := (* 定義が入る *)

Definition prop3 : forall(A B : Prop), A -> (A -> B) -> B
  := 

Definition prop4 : (A B C : Prop) : ((A->B)->C)-> (B->A->C)
  := 

*)