Program コマンド - airoboの日記

こんにちは．未だに hatena に慣れない airobo です．

今日は Coq の Program コマンドの話です．Reference Manual にもある通り，まだ experimental らしいので，今後大幅に仕様が変わるかもしれません．

Program コマンドは，その名前の通り Coq 上でプログラムを定義するのに使うと便利なコマンドです．どういう風に便利かというと，型 T と型 {x:T | P(x)} とを（ある意味で）同一視してくれます．例えば次の例です．

Program Definition x : {v | v = 1} := 1.

このコードで，x の型は {v | v = 1} であると宣言しているのにも関わらず，定義は nat 型の値 1 になっています．このように，Program コマンドは型 T と型 {x:T | P(x)} とを同一視してくれます．

では Coq の内部では何が行われているのかというと，型が合うように coercion を自動で挿入しています．実際に，先ほど定義した x を Print してみると，

x = exist (fun v : nat => v = 1) 1 x_obligation_1
     : {v : nat | v = 1}

と表示され，exist が挿入されていることがわかります．
上の例とは逆に，型 {x:T | P(x)} から型 T への coercion が入る例としては次のようなものがあります．

Program Theorem nonsense_1_gt : forall x:{v:nat | v = 1}, {v:nat | v > x}.

ここで，x は {v:nat | v = 1} 型で宣言されていますが，nat 型として使われています．実際に Coq に入力すると，goal が "forall x : {v : nat | v = 1}, {v : nat | v > proj1_sig x}" となり，coercion として proj1_sig が挿入されていることが確認できます．

さて，T 型の値を {x:T | P(x)} 型の値に変換するためには当然 P(x) の証明が必要になります．実は先程の x の定義では，Coq が自動で証明をしてくれていて，x を定義したときにその旨が表示されていました．

x has type-checked, generating 1 obligation(s)
Solving obligations automatically...
x_obligation_1 is defined
No more obligations remaining
x is defined

"obligation(s)" というのが，示さないといけないもので，ここでは自動で解かれています．では，自動では解けない例を見てみましょう．

Program Definition zero : {v | forall n, n >= v} := 0.

これを実行すると，

zero has type-checked, generating 1 obligation(s)
Solving obligations automatically...
1 obligation remaining
Obligation 1 of zero:
forall n : nat, n >= 0.

と表示され，"forall n : nat, n >= 0." を証明しなければならないことがわかります．
実際に証明するには，"Next Obligation." または "Obligation 1." とすることで，証明が始まります．そして，すべての obligations の証明が終わったところで，定義が終了します．

ここまでの使い方では，あまり嬉しさを感じないかもしれません．私が便利だと思っているのは Program Fixpoint です．何が便利かというと，（coercion の自動挿入も嬉しいのですが，）induction の measure として，複数の引数が使えることです．例えば，nat -> nat -> nat 型の再帰関数を定義しようとしたときに，Function の measure関数は一引数関数しか許されていないので，uncurry化した nat * nat -> nat 型の関数を一度定義した後に curry化してやる必要があります．

例として，みんな大好きユークリッドの互差法を考えてみましょう．Program Fixpoint を使うと次のように書くことができます．

Definition divide n m := exists k, n = k * m.

Program Fixpoint gcd (m:nat) (n:{v:nat| m >= v}) {measure (m + n)}
  : {d:nat | divide m d /\ divide n d} :=
  match n with
  | O => m
  | _ =>
    match leb (m-n) n with
    | true => gcd n (m-n)
    | false => gcd (m-n) n
    end
  end.

ここで，measure を見ると，m と n に関するものになっています．Function で書こうとすると m と n を組にする必要がありますが，組の要素って依存できるんでしょうか？少なくとも私は方法を知りません．ということで，Function や fix で書こうと思うとつまります*1．

以上，Coq 上で関数を定義するときに Program Fixpoint 使うと便利だよ，という話でした．ここでいくつか気をつけないといけないことを書いておきます．

Function と違って，func_ind や func_rec みたいな便利な関数は定義されないので，関数の性質はプログラムを定義するときに全部書きましょう．
let じゃなくて，let ' を使うといいことがあります．詳しくは Reference Manual を参照のこと．
if dec というのを使うと分岐先で条件の情報が使えるよ，ということが Reference Manual に書いてあるのですが，自分の環境では dec が定義されていないと怒られます．とりあえずの解決策として if じゃなくて match を使いましょう．

最後に，今回でてきたコードとその証明を載せておきます．おまけとしてユークリッドの互助法も定義してあります．

Require Import Recdef.
Require Import ExtrOcamlNatBigInt.
Require Import Bool Arith NPeano Omega.
Require Import Coq.Arith.Wf_nat.
Require Import Coq.Program.Wf.

Program Definition x : {v | v = 1} := 1.

Program Theorem nonsense_1_gt : forall x:{v:nat | v = 1}, {v:nat | v > x}.
intro x.
exists (S (proj1_sig x)).
auto.
Qed.

Program Definition zero : {v | forall n, n >= v} := 0.
Next Obligation.
auto with arith.
Qed.

Definition divide n m := exists k, n = k * m.

Program Fixpoint gcd (m:nat) (n:{v:nat| m >= v}) {measure (m + n)}
  : {d:nat | divide m d /\ divide n d} :=
  match n with
  | O => m
  | _ =>
    match leb (m-n) n with
    | true => gcd n (m-n)
    | false => gcd (m-n) n
    end
  end.

Next Obligation.
split; [exists 1 | exists 0]; auto with arith.
Qed.

Next Obligation.
symmetry in Heq_anonymous.
apply leb_iff in Heq_anonymous.
omega.
Qed.

Next Obligation.
symmetry in Heq_anonymous.
apply leb_iff in Heq_anonymous.
omega.
Qed.

Lemma divide_sub : forall m n d, m >= n -> divide n d -> divide (m - n) d -> divide m d.
intros m n d Hmn Hdiv_nd Hdiv_mnd.
destruct (le_lt_eq_dec n m Hmn).
 inversion Hdiv_nd as (k1, Hdiv_nd').
 inversion Hdiv_mnd as (k2, Hdiv_mnd').
 subst n.
 exists (k2 + k1).
 remember (m - k1 * d) as m'.
 symmetry  in Heqm'.
 apply add_sub_eq_nz in Heqm'.
  subst.
  ring.

  omega.

 subst n; assumption.
Qed.

Next Obligation.
destruct (gcd n
           (exist (fun v : nat => n >= v) (m - n)
              (gcd_func_obligation_2 m (exist (fun v : nat => m >= v) n H0)
                 gcd n H (Logic.eq_refl n) Heq_anonymous))
           (gcd_func_obligation_3 m (exist (fun v : nat => m >= v) n H0) gcd
              n H (Logic.eq_refl n) Heq_anonymous)) as [k Hdiv]; simpl.
simpl in Hdiv.
inversion Hdiv as (Hdiv1, Hdiv2).
split.
 apply divide_sub with n; assumption.

 assumption.
Qed.

Next Obligation.
symmetry in Heq_anonymous.
apply leb_iff_conv in Heq_anonymous.
omega.
Qed.

Next Obligation.
symmetry in Heq_anonymous.
apply leb_iff_conv in Heq_anonymous.
omega.
Qed.

Next Obligation.
destruct (gcd (m - n)
           (exist (fun v : nat => m - n >= v) n
              (gcd_func_obligation_5 m (exist (fun v : nat => m >= v) n H0)
                 gcd n H (Logic.eq_refl n) Heq_anonymous))
           (gcd_func_obligation_6 m (exist (fun v : nat => m >= v) n H0) gcd
              n H (Logic.eq_refl n) Heq_anonymous)) as [k Hdiv]; simpl.
simpl in Hdiv.
inversion Hdiv as (Hdiv1, Hdiv2).
split.
 apply divide_sub with n; assumption.

 assumption.
Qed.

Program Fixpoint gcd' (m:nat) (n:{v:nat| m >= v}) {measure n}
  : {d:nat | divide m d /\ divide n d} :=
  match n with
  | O => m
  | _ => gcd' n (m mod n)
  end.

Next Obligation.
split; [exists 1 | exists 0]; auto with arith.
Qed.

Next Obligation.
apply lt_le_weak.
apply mod_upper_bound.
auto.
Qed.

Next Obligation.
apply mod_upper_bound.
auto.
Qed.

Theorem mod_divides_res : forall a b r: nat, b <> 0 -> a mod b = r ->
  exists c : nat, a = b * c + r.
intros a b r Hb Hmod.
assert (b > r) as Hbr.
 subst r.
 apply mod_upper_bound.
 assumption.

 assert ((a + (b - r)) mod b = 0) as Hmod0.
  rewrite add_mod.
   rewrite Hmod.
   destruct (eq_nat_dec r 0) as [Hr | Hr].
    rewrite Hr.
    simpl.
    rewrite <- minus_n_O.
    rewrite mod_same.
     reflexivity.

     assumption.

    replace ((b - r) mod b) with (b - r) .
     rewrite le_plus_minus_r.
      apply mod_same.
      assumption.

      omega.

     symmetry .
     apply mod_small.
     omega.

   assumption.

  apply mod_divides in Hmod0.
   inversion Hmod0 as (c,Hmod0').
   destruct c as [| c'].
    exists 0.
    omega.

    exists c'.
    remember (b - r) as br.
    assert (r + br = b) as Hadd_sub.
     apply add_sub_eq_nz.
      omega.

      symmetry; assumption.

     subst b.
     rewrite mult_comm in Hmod0'.
     simpl in Hmod0'.
     rewrite mult_comm.
     omega.

   assumption.
Qed.

Next Obligation.
destruct (gcd' n
           (exist (fun v : nat => n >= v) (m mod n)
              (gcd'_func_obligation_2 m (exist (fun v : nat => m >= v) n H0)
                 gcd' n H (Logic.eq_refl n)))
           (gcd'_func_obligation_3 m (exist (fun v : nat => m >= v) n H0) gcd'
              n H (Logic.eq_refl n))) as [d Hdiv]; simpl.
simpl in Hdiv; inversion Hdiv as [H1 H2].
split.
 inversion H1 as (k1, H1').
 inversion H2 as (k2, H2').
 apply mod_divides_res in H2'.
  inversion H2' as (k3, H2'').
  subst.
  exists (k1 * k3 + k2).
  ring.

  auto.

 assumption.
Qed.

*1:いろいろがんばってみましたが，結局定義できませんでした．もちろん，well_founded_induction を使えば書けますが，書く気が起きないので書いてません．