2010-07-04

kururuさんがたらいまわしの証明をしていたのを見て

Coq

http://d.hatena.ne.jp/kururu_goedel/20100702

これを見て、とりあえず綺麗に書き直そうとしてみたら一日かかった。
しかし、これで一般たらいまわしへの道も見えてきたかも？

ここに置いた。http://github.com/kik/sandbox/blob/master/coq/tarai.v

多少、解説

Fixpoint ntarai3 (n : nat) (a b c : option Z) :=
match a with 
| None => None
| Some av =>
  match b with 
  | None => None
  | Some bv => 
      if Z_le_dec av bv then b else
      match n with 
      | 0%nat => None
      | S np => 
          match c with 
          | None => None
          | Some cv => 
              (ntarai3 np 
                (ntarai3 np (Some (av-1)) b c)
                (ntarai3 np (Some (bv-1)) c a)
                (ntarai3 np (Some (cv-1)) a b))
          end 
      end
  end
end.

くるるさんのからこぴってきたところ。call-by-nameなので必要になるまで option Z の中身はみない。
この定義のまま、証明を始めるとfixやらunfoldやらすさまじい項管理能力が必要で、まったく本質でないところで苦労する。というかした。

こういうときは、Inductive を使って、ntarai3 関数を特徴付けてやればよい

Inductive Tarai_value (n: nat) (a b c: option Z) (v: Z) : Prop :=
| Tarai_a_le_b (av bv: Z)
     (Hle: av <= bv) (Hv: bv = v) (Ha: a = Some av) (Hb: b = Some bv): Tarai_value n a b c v
| Tarai_a_gt_b_1 (av bv cv: Z) (n': nat) (Hgt: av > bv)
     (Ha: a = Some av) (Hb: b = Some bv) (Hc: c = Some cv)
     (Hn: n = S n')
     (v1: Z)
     (Hle2: v1 <= v)
     (Hrec1: Tarai_value n' (Some (av-1)) b c v1)
     (Hrec2: Tarai_value n' (Some (bv-1)) c a v)
| Tarai_a_gt_b_2 (av bv cv: Z) (n': nat) (Hgt: av > bv)
     (Ha: a = Some av) (Hb: b = Some bv) (Hc: c = Some cv)
     (Hn: n = S n')
     (v1 v2 v3: Z)
     (Hle2: ~v1 <= v2)
     (Hrec1: Tarai_value n' (Some (av-1)) b c v1)
     (Hrec2: Tarai_value n' (Some (bv-1)) c a v2)
     (Hrec3: Tarai_value n' (Some (cv-1)) a b v3)
     (Hrec4: Tarai_value n' (Some v1)
                                   (Some v2)
                                   (Some v3) v): Tarai_value n a b c v.

Tarai_value n a b c v という述語は、ntarai3 n a b c が停止して、結果が v になるという意味。
それは、結局３通りしかなくて、a <= b のときには停止して、b = v である(Tarai_a_le_b)。
a > b かつ n > 0 かつ Tarai_value (n-1) (a-1) b c v1 かつ Tarai_value (n-1) c a v かつ、v1 <= v のとき(Tarai_a_gt_b_1)。a > b かつ n > 0 かつ v1 > v2 たらい回しの結果が v になる場合(Tarai_a_gt_b_2)。

あと、こうやって名前をつけとくとdestructしたときにこの名前を使ってくれて読みやすい。

最初に、Tarai_value が正しく定義されてることを証明します。

Lemma lem_saficient:
  forall n a b c v, Tarai_value n a b c v -> ntarai3 n a b c = Some v.
Lemma lem_invert:
  forall n a b c v, ntarai3 n a b c = Some v -> Tarai_value n a b c v.

この二つを証明すれば、もう fix のことは忘れて、Tarai_value に専念できます。この証明は大変でした。特に下のやつ。

ここまで終われば、相当簡単になります(Coqに関しては、証明自体は複雑だけど)。

どれくらい簡単になるかというと

bv : Z
cv : Z
H : bv <= cv
______________________________________(1/2)
Tarai_value 1 (Some (bv + 1)) (Some bv) (Some cv) cv

を証明したいと思ったら、bv+1 > bv なので、Tarai_a_gt_b_1 か Tarai_a_gt_b_2 のどちらかで停止することになります。とりあえず、Tarai_a_gt_b_1 を apply してみると

apply Tarai_a_gt_b_1 with (bv + 1) bv cv 0%nat bv; auto; try omega.

これで、証明しないといけないことが２つになります。

bv : Z
cv : Z
H : bv <= cv
______________________________________(1/3)
Tarai_value 0 (Some (bv + 1 - 1)) (Some bv) (Some cv) bv


______________________________________(2/3)
Tarai_value 0 (Some (bv - 1)) (Some cv) (Some (bv + 1)) cv

上のほうは、bv + 1 - 1 <= bv なので、Tarai_a_le_b により停止します。下のほうも bv - 1 <= cv なので同様です。

apply Tarai_a_le_b with (bv + 1 - 1) bv; auto; omega.
apply Tarai_a_le_b with (bv - 1) cv; auto; omega.

これで、できあがりです。

結構こつをつかんだので、一般たらいまわしもいけるかなあ…

2010-06-29

証明してみた。

Coq

http://d.hatena.ne.jp/m-hiyama/20100629/1277774676 を証明してみた。

とりあえず、問題設定

Axiom A : Set.

Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }.

Axiom A_mul : A -> A -> A.
Axiom A_zero: A.
Axiom A_one: A.

Infix "*" := A_mul.
Notation "0" := A_zero.
Notation "1" := A_one.

Axiom A_mul_assoc: forall a b c, (a * b) * c = a * (b * c).
Axiom A_mul_comm: forall a b, a * b = b * a.
Axiom A_mul_1_r: forall a, a * 1 = a.
Axiom A_mul_inv_ex: forall a, a <> 0 -> { a': A | a * a' = 1 }.
Axiom A_mul_0_r: forall a, a * 0 = 0.

以下ねたばれ

2009-10-26

定理証明の会で実演した中間値の定理の証明

Coq

は

http://github.com/kik/sandbox/blob/f41bc1346d4491f937b3fb78da38a07c746acf1c/coq/ivt.v

にあります。試すにはcoqを適当にインストールしてcoqideを起動して、このファイルを開く。
あとはツールバーから適当に下に進むボタンを押してれば証明の様子が分かります。Ctrl+Alt+↓でもおけ。

ほとんど実数の公理から直接証明しています。ポイントは

$A := \{ t \in R : t \le y \wedge f(t) \le 0 \}$

という集合 $A$ を使うと、求める点は $z = \sup A$ となるので、あとは

$f(z) = 0$

を証明するだけになります。これを示すために実数が全順序であることから

$f(z) < 0 \vee f(z) = 0 \vee f(z) > 0$

であることがいえるので、

$z = \sup A \to f(z) < 0 \to f(z) = 0$
$z = \sup A \to f(z) = 0 \to f(z) = 0$
$z = \sup A \to f(z) > 0 \to f(z) = 0$

をそれぞれ証明すれば終わりです。まず真ん中は自明。残りの二つはそれぞれの二つの前提が矛盾しているので、矛盾からは何でも証明できることによって $f(z) = 0$ が示せます。

2009-09-27

ハノイの塔

Coq

久しぶりにCoqで遊ぼうかと思って、いい問題はないかと考えたところ、ハノイの塔あたりが面白いんじゃなかろうかということで証明してみた。

証明したいことはハノイの塔を完成させる最短手数は2^n-1であること…

と思って少し書いてみたんだけど、これはかなり大変だということになって、ハノイの塔の解等を計算する関数が正しく解になっていることを証明することを最初の目標としてみた。

問題設定は以下の通り

Inductive pos : Set := pos1 | pos2 | pos3.
Inductive move : Set :=
| from_to (from to: pos):  move.

Definition tower := list pos.
Definition moves := list move.

Fixpoint single_tower (t: tower) (p: pos) : Prop.

Definition legal_move (t: tower) (m: move) : Prop. 
Definition make_move (t:tower) (m:move) : tower.

Fixpoint legal_moves (m:moves) (t:tower) :=
match m with
| hd::tl => legal_move t hd /\ legal_moves tl (make_move t hd)
| nil => True
end.

Definition make_moves (m:moves) (t:tower) :=
  fold_left make_move m t.

Fixpoint answer (n: nat) (from to rest: pos) {struct n} :=
match n with
| O => nil
| S m =>  answer m from rest to ++ (from_to from to::nil) ++ answer m rest to from
end.

Theorem hanoi: forall (n:nat) (t: tower) (from to rest: pos),
  from <> to -> from <> rest -> to <> rest ->
  length t = n ->
  single_tower t from ->
  legal_moves (answer n from to rest) t
   /\ single_tower (make_moves (answer n from to rest) t) to.

塔をどのようにlist posで表現するかで泥沼がまっているぞ！

とりあえず、清書してない300行ある証明は http://github.com/kik/sandbox/blob/c1b16b684feb7482f0582480a43b2db4a9be3ce0/coq/Hanoi.v にあるけど、自分で証明したい人は見ないように。

Coq 8.1でやったから新しいのだと問題があるかも

2008-10-28

Seven Trees を…

Coq

Require Import ZArith.
Open Scope Z_scope.

Goal forall t:Z, t = 1 + t^2 -> t^7 = t.
intros.
ring [H].

終わらない…

2007-05-31

Coqのネタはwikiに移転した

Coq

http://as305.dyndns.org/wiki/index.php?Coq

2007-05-20

■

Coq

なんかいろんな言語で FizzBuzz が書かれているようなので、Coq でも書いてみる。

Coq の FizzBuzz は他のとは一味違う！なんとプログラムが正しく動くことが証明できるのだ！

とりあえず、書いたプログラム

Require Import Arith.
Require Import List.

(* FizzBuzz の結果を表すデータ型。FizzBuzz は list FizzBuzz_R を返す。 *)
Inductive FizzBuzz_R: Set :=
| R_nat (n: nat)
| R_Fizz
| R_Buzz
| R_FizzBuzz.

(* ループでまわす途中の値
 * r3: n を 3 で割った余り
 * r5: n を 5 で割った余り
 *)
Inductive FizzBuzz_D: Set :=
  FizzBuzz_d (n r3 r5: nat).

(* FizzBuzz_D を受け取って n+1 の FizzBuzz_D を返す。*)
Definition FizzBuzz_next (d: FizzBuzz_D) :=
  let (n, r3, r5) := d in
    let r3' := if eq_nat_dec r3 2 then 0 else r3+1 in
    let r5' := if eq_nat_dec r5 4 then 0 else r5+1 in
      FizzBuzz_d (n+1) r3' r5'.

(* FizzBuzz_D を受けとって FizzBuzz_R を返す。*)
Definition FizzBuzz_value (d: FizzBuzz_D) :=
  let (n, r3, r5) := d in
    (* n%3 と n%5 が 0 であるかで場合わけ *)
    match eq_nat_dec r3 0, eq_nat_dec r5 0 with
      | left  _, left  _ => R_FizzBuzz
      | left  _, right _ => R_Fizz
      | right _, left  _ => R_Buzz
      | right _, right _ => R_nat n
    end.

(* rep 回だけループする。*)
Fixpoint FizzBuzz_fold (rep: nat) (d: FizzBuzz_D) {struct rep} :=
  match rep with
    | O => nil  (* rep が 0 のときは空リスト *)
    | S k =>    (* rep が k の次の数の時は再帰する *)
      cons (FizzBuzz_value d) (FizzBuzz_fold k (FizzBuzz_next d))
  end.

(* 我々の FizzBuzz 関数 *)
Definition FizzBuzz (rep: nat) :=
  FizzBuzz_fold rep (FizzBuzz_d 1 1 1).

我々は割り算なんて複雑な関数は使わない。
だいたい、標準関数に n を m で割った余りが r かどうかを決定する関数が入ってないぞ！
（余りが r かどうかという命題はある。この二つは違うのだ！）

この FizzBuzz が正しい動作をすることを証明する前に、簡単な補題を証明する。

(* 簡単な補題
 * r=r' ならば r::L = r'::L
 *)
Lemma FizzBuzz_eq: forall (r r': FizzBuzz_R) L, r=r' -> r::L = r'::L.
Proof.
  intros.
  congruence.
Qed.

そして FizzBuzz の証明をするわけだが、残念なことにあまりに長いので途中を省略する。