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

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.

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

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