■

暫くCoqを弄ってみようかと。Coqは、Calculus of (Co)Inductive Constructionsという謎の体系を背景にしているらしい。実装はOcaml(多分)。CoqをSchemeで書けるようになるくらいまで頑張ろう

今日のまとめ
・IDEは全く使い方が分からないので、コマンドラインで
・終了コマンドはQuit
・0(ゼロ)とO(オー)が紛らわしいので、注意
・式の末尾はピリオドで

まず、Check。型(?)を返すっぽい。

Coq<Check 3.
3
     : nat
Coq < Check nat.
nat
     : Set
Coq < Check Set.
Set
     : Type
Coq < Check Type.
Type
     : Type
Coq < Check True.
True
     : Prop
Coq < Check (3=3).
3 = 3
     : Prop
Coq < Check Prop.
Prop
     : Type
Coq < Check (3+2).
3 + 2
     : nat
Coq < Check plus.
plus
     : nat -> nat -> nat
Coq < Check (3,4).
(3, 4)
     : (nat * nat)%type
Coq < Check S.
S
     : nat -> nat
Coq < Check nat_ind.
nat_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

nat_indは自然数に対する数学的帰納法。natはどっかで、

Inductive nat : Set := | O : nat | S : nat -> nat.

と定義されているらしい。Inductiveを使って、定義してやると、自動的に、帰納法が生成されるらしい。Oはゼロではなく、オー。

Coq < Inductive even : nat -> Prop := 
Coq < | even0 : even 0 | evenS : forall x:nat, even x -> even (S (S x)). 

みたいにやると、evenとeven_indが定義される。ちなみに、CoIndutiveもある。

次が、Evalと関数定義(Definiton,Fixpoint)

Coq < Eval compute in (S (S (S O))).
     = 3
     : nat
Coq < Definition F x:nat := 2*x+1.
Coq < Eval compute in (F 3).
     = 7
     : nat
Coq < Definition H := fun x:nat => fun y:nat => 2*x+y.
Coq < Eval compute in (H 3).
     = fun y : nat => S (S (S (S (S (S y)))))
     : nat -> nat
Coq < Fixpoint fact (x:nat) {struct x} :nat  :=
Coq < match x with
Coq < | O => (S O)
Coq < | (S p) => (mult (S p) (fact p))
Coq < end.
Coq < Eval compute in (fact 3).
     = 6
     : nat

Evalは中では、愚直に、SとOを使って計算してるんじゃないかと思うので、多分効率は悪い。

証明。「AならばA」という命題の証明。Goalで証明モード(?)に入る。

Coq < Variable A:Prop.
Coq < Goal A->A.
1 subgoal

  ============================
   A -> A

Unnamed_thm < trivial.
Proof completed.

Unnamed_thm < Qed.
trivial.
Unnamed_thm is defined

自明らしい。trivialがいつ使えるのか謎。Variableは変数の宣言。途中で証明を諦める場合は、Abort。もうちょっとちゃんと証明。

Coq < Goal A->A.
1 subgoal

  ============================
   A -> A

Unnamed_thm0 < intro.
1 subgoal

  H0 : A
  ============================
   A

Unnamed_thm0 < exact H0.
Proof completed.

Unnamed_thm0 < Qed.
intro.
exact H0.
Unnamed_thm0 is defined

縦に書くと長いので、H0 ,... |- Goal0 ,... みたいに書くことにする。
証明したいのは、

- A->A

なんだけど、introコマンドで、
H0:A |- A
に書き換える。exact H0で、仮定H0から、ゴールAを導ける。introとか、exactというのは、tacticとか呼ばれてる。多分、Coq用語

もう少し複雑な例。

Coq < Variable B C:Prop.
Coq < Goal (A->B->C)->(A->B)->(A->C).
1 subgoal

  ============================
   (A -> B -> C) -> (A -> B) -> A

Unnamed_thm1 < intro.
1 subgoal

  H0 : A -> B -> C
  ============================
   (A -> B) -> A -> C

Unnamed_thm1 < intro.
1 subgoal

  H0 : A -> B -> C
  H1 : A -> B
  ============================
   A -> C

Unnamed_thm1 < intro.
1 subgoal

  H0 : A -> B -> C
  H1 : A -> B
  H2 : A
  ============================
   C

Unnamed_thm1 < apply H0.
2 subgoals

  H0 : A -> B -> C
  H1 : A -> B
  H2 : A
  ============================
   A

subgoal 2 is:
 B

Unnamed_thm1 < exact H2.
1 subgoal

  H0 : A -> B -> C
  H1 : A -> B
  H2 : A
  ============================
   B

Unnamed_thm1 < apply H1.
1 subgoal

  H0 : A -> B -> C
  H1 : A -> B
  H2 : A
  ============================
   A

Unnamed_thm1 < exact H2.
Proof completed.

Unnamed_thm1 < Qed.
intro.
intro.
intro.
apply H0.
 exact H2.
 apply H1.
   exact H2.
Unnamed_thm1 is defined

新しいtacticは、applyのみ。よく分からないけど、雰囲気で。

- (A->B->C)->(A->B)->(A->C)

• • > (A->B->C) |- (A->B)->(A->C)
  • > (A->B->C) , (A->B) |- A->C
  • > (A->B->C) , (A->B) , A |- C
  • > (A->B->C) , (A->B) , A |- A,B
  • > (A->B->C) , (A->B) , A |- B
  • > (A->B->C) , (A->B) , A |- A
  • > (A->B->C) , (A->B) , A |-

tacticは、;で区切って複数一気に書いてもいい。他のtacticはtutorial読めば、なんか載ってる。論理記号は、/\でandだったり、\/でorだったり。

帰納法。n=n+0を証明。

Coq <  Goal forall n:nat , n=n+0.
1 subgoal

  ============================
   forall n : nat, n = n + 0

Unnamed_thm7 < induction n.
2 subgoals

  ============================
   0 = 0 + 0

subgoal 2 is:
 S n = S n + 0

Unnamed_thm7 < simpl.
2 subgoals

  ============================
   0 = 0

subgoal 2 is:
 S n = S n + 0

Unnamed_thm7 < auto.
1 subgoal

  n : nat
  IHn : n = n + 0
  ============================
   S n = S n + 0

Unnamed_thm7 < simpl.
1 subgoal

  n : nat
  IHn : n = n + 0
  ============================
   S n = S (n + 0)

Unnamed_thm7 < Lemma thm7_lemma1 : forall x y:nat , x=y->(S x)=(S y)
1 subgoal

  ============================
   forall x y : nat, x = y -> S x = S y

thm7_lemma1 < auto.
Proof completed.

thm7_lemma1 < Qed.
auto.
thm7_lemma1 is defined

Unnamed_thm7 < apply thm7_lemma1.
1 subgoal

  n : nat
  IHn : n = n + 0
  ============================
   n = n + 0

Unnamed_thm7 < exact IHn.
Proof completed.

この程度なら、ここまで詳細に指定しなくても解いてくれるけど。inductionでnに関する帰納法を使うことを指定。simplは式を定義に従って簡約してくれる。途中で、補題"forall x y:nat , x=y->(S x)=(S y)"を証明している。applyで補題を適用

1+...+n=n*(n+1)/2を証明しようとしたけど、挫折。う〜ん、ただ計算するだけだろうがー。simplがバカすぎるんだよ