■

Coq。証明中、Undo機能が欲しいなーと思ってたら、ちゃんとあった。前回の補足のような。Variableで大域変数を宣言したけど、

Coq < forall A B C:Prop , (A->B->C)->(A->B)->(A->C).

みたく、forallでローカルに束縛しちゃっていいらしい。Propが型というのは多少変な感じだけど、Propを返り値にした関数もつくれる。例えば、集合AとA上の二項演算opが半群である(つまり、opが結合律を満たす)ことを意味する命題を返す関数。

Definition Semigroup := 
 fun (A:Set) => fun (op:A->A->A) => forall x y z:A , op x (op y z) = op (op x y) z.

Coq < Goal (Semigroup nat plus).
Unnamed_thm2 < compute.

やたら長い式が出力されるけど、以下、普通に、結合律の証明をやっていけば証明できる。

それから、関数定義で、if文ないと不便すぎる("match ... with ..."ではinductiveでないデータ型には使えないし)と思っていたら、一応あるらしいけど、

Coq < Definition bool_to_int := fun (x:Bool) => if x then 0 else 1.

で。then elseのタイプがめんどい。しかし、(x<3)とかの型は、Boolではなく、Propなので、どうすればいいんだ。gcd関数を普通に定義できない気が。

前回挫折した1+...+n=n*(n+1)/2の証明

Fixpoint sum (n:nat) {struct n} : nat :=
 match n with
  | O => O
  | (S p) => (S p)+(sum p)
 end.

Coq < Theorem sum_of_1_to_n: forall x:nat , 2*(sum x)=x*(x+1).
sum_of_1_to_n < induction x;auto.
1 subgoal

  x : nat
  IHx : 2 * sum x = x * (x + 1)
  ============================
   2 * sum (S x) = S x * (S x + 1)

sum_of_1_to_n < Lemma sub:forall n:nat,sum (S n)=(S n)+(sum n).
sub < auto.
sub < Qed.
sum_of_1_to_n < rewrite sub.
sum_of_1_to_n < Require Import Arith.
sum_of_1_to_n < rewrite mult_plus_distr_l.
sum_of_1_to_n < rewrite IHx.
sum_of_1_to_n < Require Import ArithRing.
sum_of_1_to_n < ring_nat.
sum_of_1_to_n < Qed.

subはsum (S n)=(S n)+(sum n)という定義から自明な補題で、これを使って、2*(sum (S x))を2*( (sum x)+(S x) )に置き換える。mult_plus_distr_lは、x*(y+z)=x*y+x*zというLemmaで、2*( (sum n)+(S n) )を展開するこの補題はArithというライブラリで証明されている。"rewrite IHx"は、仮定IHxを使って下式の左辺の2*(sum x)をx*(x+1)に書き換える。この時点で、下式は、xの多項式の比較になってるので、両辺を正規形に変形してやれば、等しいことを自動的に証明できるはず。多項式を正規形に変形するのが、Ring tacticというもの。けど、下式は、Sを含むので、(S x)をx+1に置き換えてやる必要がある。これも含めて自動的にやってくれるのが、ring_natというtacticマクロで、"rewrite S_to_plus_one; ring. "を繰り返すらしい。これはArithRingで定義されている。最後のring_natなしで、手でやろうとすると、結構大変なことになる

色々分からないけど、算術は飽きたので、リスト。標準ライブラリで色々定義されているようなので、それを使う

Coq < Require Import List.
Coq < Check cons.
cons
     : forall A : Set, A -> list A -> list A
Coq < Check list.
list
     : Set -> Set
Coq < Eval compute in (cons 3 (cons 2 nil)).
     = 3 :: 2 :: nil
     : list nat
Coq < Eval compute in (length (cons 3 (cons 2 nil))).
     = 2
     : nat

とりあえず、練習。

Coq < Goal forall (S:Set) (x y:list S) , (length (app x y)) = (length x) + (length y).
(中略)
Unnamed_thm0 < Qed.
intros.
induction x.
 simpl in |- *; trivial.
 simpl in |- *.
   rewrite IHx.
   trivial.
Unnamed_thm2 is defined

Coq < Goal forall (S T:Set) (f:S->T) (x y:list S) ,
Coq <   (map f (app x y)) = (app (map f x) (map f y)).
(中略)
Unnamed_thm1 < Qed.
intros.
induction x.
 simpl in |- *.
   trivial.
 simpl in |- *.
   rewrite IHx.
   trivial.
Unnamed_thm1 is defined

練習なので、autoで済むところも、敢えて手でやっている。基本的に帰納法。

まあ、Coqは何となく分かってきた。とりあえず、(定理|補題)名が分かりづらい。これ覚えれる気はしない。最初の方に書いたような命題をパラメータ化するような手法がほしいね。結合律だったら、Associative(nat,plus)とか、Associative(list,app)みたいに書けるといい。あと、推論エンジンが馬鹿っぽいというか、例えばappの結合律は、app_assとass_appと二種類あるとか。

やってることといえば、H0,... |- G0,...という図をどんどん変換していく関数みたいなんがtacticで、|- Goalから始めて、H0,...|-という形に変形できれば終わりみたいな、そんな感じ。多分。いや、それだと型理論とかはどこいったって話なんだけど。あと、CoqはTuring-completeではないという話が。むう。けど、それだとTuring completeな言語のformal semantics書いたりできないような。いや、書けるけど、計算できないのか。よく分かんないな