refineタクティックでらくらく依存型プログラミング(?)

下の記事では，

Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual u1 u2}+{~dual u1 u2}.

という関数を，Coqの証明モードで作りました．ところが証明モードで作ったプログラムは極めて複雑でイマイチ効率のほどがよくわかりません (Coqで Print dual_dec. するとわかります)．
ソートSetの部分だけを見ればdual_decは非常に簡単な関数で，dual_boolで見たように高々項の深さ回数*2のパターンマッチで書けるはずです．

というわけで，dual_dec を 直接 λ項で書き下してみましょう．ただし，せっかくCoqを使うので，証明が必要な部分は極力 証明モードを使います．
そういう用途には refineタクティックを使います．どうやって証明していいかわからない部分を _ にしておくと，そこを証明するモードが始まるという超・便利なタクティックです．
これで依存型も怖くありませんね．

refineを試してみる

refine タクティックに，dual_dec の関数本体を与えます． 関数は再帰するので fix を使っています．

Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual (u1,u2)}+{~dual (u1,u2)}.
refine (fix dual_dec (u1:sesstyp) (u2:sesstyp) : {dual (u1,u2)}+{~dual (u1,u2)} := 
  match (u1,u2) with
  | (SIn v1 u1', SOut v2 u2') =>
    if eq_valtyp_dec v1 v2 
      then if dual_dec u1' u2' 
              then left (~dual (SIn v1 u1',SOut v2 u2')) (_:dual (SIn v1 u1',SOut v2 u2')) 
              else right (dual (SIn v1 u1',SOut v2 u2')) (_:~dual (SIn v1 u1',SOut v2 u2')) 
      else right (dual (SIn v1 u1',SOut v2 u2')) (_:~dual (SIn v1 u1',SOut v2 u2')) 
  | (SOut v1 u1', SIn v2 u2') =>
    if eq_valtyp_dec v1 v2 
      then if dual_dec u1' u2' 
              then left (~dual (SOut v1 u1',SIn v2 u2')) (_:dual (SOut v1 u1',SIn v2 u2'))
              else right (dual (SOut v1 u1',SIn v2 u2')) (_:~dual (SOut v1 u1',SIn v2 u2'))
      else right (dual (SOut v1 u1',SIn v2 u2')) (_:~dual (SOut v1 u1',SIn v2 u2'))
  | (SEnd, SEnd) => left (~dual (SEnd,SEnd)) _
  | x => right (dual x) (_:~dual x)
  end).

さきほど，sumbool 型は if文で使えると id:yoshihiro503 さんから聞いたので，それを使っています．
やや複雑に見えますが，left は true に，right は false に相当することを考えれば簡単です．ここで left や right の 第1引数は他方の(leftならrightの,rightならleftの)命題を書きます．第2引数にはその命題の証明を書きます．証明は証明モードでやってしまいたいので、leftやrightの証明引数にはアンダースコアを置いています．

ところがこんなエラーが出ます：

>   | x => right (dual x) (_:~dual x)
>          ^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
In environment
dual_dec : forall u1 u2 : sesstyp, {dual (u1, u2)} + {~ dual (u1, u2)}
u1 : sesstyp
u2 : sesstyp
s : sesstyp
s0 : sesstyp
v : valtyp
s1 : sesstyp
v0 : valtyp
s2 : sesstyp
x := (SIn v s1, SIn v0 s2) : sesstyp * sesstyp
The term "right (dual x) (?1558:~ dual x)" has type 
"{dual x} + {~ dual x}" while it is expected to have type
 "{dual ?1553} + {~ dual ?1554}".

no free lunch! / match ... return ... 構文

そう，そんなウマい話はありませんでした…
sumboolは型に式レベルの項が現れる依存型です．sumboolのパターンマッチは，分枝によって全く異なる型をとるので，Coqはこのままだと型の整合性を検査できないのです．

match 式 return 型 with 分枝1 | ... | 分枝n end. という構文で，matchの各分枝が返しうる型をCoqに教えてやることができます．
早速，上の match を

  match (u1,u2) return {dual (u1,u2)}+{~dual (u1,u2)} with

で置き換えてみましょう．

しかしダメです．

>   | x => right (dual x) (_:~dual x)
>          ^^^^^^^^^^^^^^^^^^^^^^^^^^
...
The term "right (dual x) (?1570:~ dual x)" has type 
"{dual x} + {~ dual x}" while it is expected to have type
 "{dual (u1, u2)} + {~ dual (u1, u2)}".

Coqは型dual (u1,u2) と 型dual x を同一視してくれません．おそらく他の分枝でも同様 (型dual (SIn v1 u1',SOut v2 u2')と型dual (u1,u2) を同一視してくれない)．

match ... as ... return ... 構文

match の各分枝の型が，match でパターンマッチする式に依存する場合，そのパラメータをCoqに教えてあげなければなりません．
ここで match 式 as 識別子 return 型 with ... という構文を使います．
先ほどのmatchを，

  match (u1,u2) as x return {dual x}+{~dual x} with

と書き換えましょう…

refine成功！ そして証明へ…

refineすると，17個のサブゴールが現れます．全てのサブゴールは先のエントリの通りで証明できるはず．やりました，成功です！

Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual (u1,u2)}+{~dual (u1,u2)}.
refine (fix dual_dec (u1:sesstyp) (u2:sesstyp) : {dual (u1,u2)}+{~dual (u1,u2)} := 
  match (u1,u2) as x return {dual x}+{~dual x} with
  | (SIn v1 u1', SOut v2 u2') =>
    if eq_valtyp_dec v1 v2 
      then if dual_dec u1' u2' 
              then left (~dual (SIn v1 u1',SOut v2 u2')) (_:dual (SIn v1 u1',SOut v2 u2')) 
              else right (dual (SIn v1 u1',SOut v2 u2')) (_:~dual (SIn v1 u1',SOut v2 u2')) 
      else right (dual (SIn v1 u1',SOut v2 u2')) (_:~dual (SIn v1 u1',SOut v2 u2')) 
  | (SOut v1 u1', SIn v2 u2') =>
    if eq_valtyp_dec v1 v2 
      then if dual_dec u1' u2' 
              then left (~dual (SOut v1 u1',SIn v2 u2')) (_:dual (SOut v1 u1',SIn v2 u2'))
              else right (dual (SOut v1 u1',SIn v2 u2')) (_:~dual (SOut v1 u1',SIn v2 u2'))
      else right (dual (SOut v1 u1',SIn v2 u2')) (_:~dual (SOut v1 u1',SIn v2 u2'))
  | (SEnd, SEnd) => left (~dual (SEnd,SEnd)) _
  | x => right (dual x) (_:~dual x)
  end).

 intro.
 inversion H.
 
 rewrite _H in |- *.
 apply (DualInOut v2 u1' u2' _H0).
 
 intro.
 inversion H.
 apply (_H0 H1).
 
 intro H.
 inversion H.
 apply (_H H3).
 
 intro H.
 inversion H.
 
 intro H.
 inversion H.
 
 rewrite _H in |- *.
 apply (DualOutIn v2 u1' u2' _H0).
 
 intro H.
 inversion H.
 apply (_H0 H1).
 
 intro H.
 inversion H.
 apply (_H H3).
 
 intro H.
 inversion H.
 
 intro H.
 inversion H.
 
 intro H.
 inversion H.
 
 intro H.
 inversion H.
 
 intro H.
 inversion H.
 
 intro H.
 inversion H.
 
 intro H.
 inversion H.
 
 apply DualEnd.
 Qed.