セッション型（一部）の双対の決定可能性を証明

Coq

すごくどうでもいい証明です．．Coqを触るのは2年ぶりくらいだろうか…
めちゃくちゃ非効率なことをやっていそうなので，皆さんのツッコミをお待ちしています．

前提

セッション型の双対とは，受信の双対が送信，送信の双対が受信という感じで決まっています．(他にセッションの委譲という機能もあるけどここでは扱わない．)
まずはセッション型(の一部)と，セッション型の双対をinductive predicateで定義します．

(* 値の型(とりあえずboolのみ) *)
Inductive valtyp : Set := vbool : valtyp.

(* 値の型は区別できる *)
Definition eq_valtyp_dec (t1 t2:valtyp) : {t1=t2}+{t1<>t2} :=
  match t1,t2 return {t1=t2}+{t1<>t2} with
  | vbool,vbool => left _ (refl_equal vbool)
  end.

(* boolバージョン *)
Definition eq_valtyp_bool (t1 t2:valtyp) : bool :=
  match t1, t2 with
  | vbool, vbool => true
  end.

(* セッション型．とりあえず送受信のみ *)
Inductive sesstyp : Set :=
  | SIn    : valtyp -> sesstyp -> sesstyp (* 入力 *)
  | SOut   : valtyp -> sesstyp -> sesstyp (* 出力 *)
  | SBot : sesstyp (* 所有されている *)
  | SEnd : sesstyp (* セッション終了 *)
.

(* セッション型の双対 *)
Inductive dual : sesstyp -> sesstyp -> Prop :=
  | DualInOut : forall (v:valtyp) (u1 u2:sesstyp),
                  dual u1 u2 -> dual (SIn v u1) (SOut v u2)
  | DualOutIn : forall (v:valtyp) (u1 u2:sesstyp),
                  dual u1 u2 -> dual (SOut v u1) (SIn v u2)
  | DualEnd   : dual SEnd SEnd.

(* たとえばこんな感じ *)
Lemma dual1 : dual (SIn vbool SEnd) (SOut vbool SEnd).
apply (DualInOut vbool SEnd SEnd DualEnd).
Qed.

でもここで決めたdualは述語なので，関数的には使えません．
場合によっては関数が必要なときもある…と思うので，関数的に書きます．

Fixpoint dual_bool (u1 u2:sesstyp) : bool :=
  match u1, u2 with
  | SIn v1 u1, SOut v2 u2 => if eq_valtyp_bool v1 v2 then dual_bool u1 u2 else false
  | SOut v1 u1, SIn v2 u2 => if eq_valtyp_bool v1 v2 then dual_bool u1 u2 else false
  | SEnd, SEnd => true
  | _, _ => false
  end .

でもbool型につぶすと情報が失われて証明で使いにくいのでsumbool型を使います．

(* sumbool型で書くと…？ *)
Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual u1 u2}+{~dual u1 u2}.

Coqは普通にやると停止する関数しか書けないので，この関数は，実質 「セッション型の双対は決定可能である」ということを述べています．(たぶん．)

証明

これを証明モードで書いてみます．
(関数をλ項で書き下すやり方もあると思いますがすぐにはわかりませんでした．match .. as .. in .. return .. with .. みたいな，dependentなパターンマッチが必要． )
(こちらに書きましたが，refineを使えば，プログラムとして書き下す方法と，証明モードを混在させることもできます．)
ゴールはこうなっています：

   forall u1 u2 : sesstyp, {dual u1 u2} + {~ dual u1 u2}

普通にu1とu2について帰納法を回せばできるはず．

dual_dec < intros. induction u1. induction u2.

...
7 subgoals
  
  v : valtyp
  u1 : sesstyp
  v0 : valtyp
  u2 : sesstyp
  IHu1 : {dual u1 (SIn v0 u2)} + {~ dual u1 (SIn v0 u2)}
  IHu2 : {dual u1 u2} + {~ dual u1 u2} ->
         {dual (SIn v u1) u2} + {~ dual (SIn v u1) u2}
  ============================
   {dual (SIn v u1) (SIn v0 u2)} + {~ dual (SIn v u1) (SIn v0 u2)}

(他7つのサブゴール)

SIn v u1 と SIn v0 u2 は，双対にはなりえない(両方とも入力だから)ので，false側に行きます．

dual_dec> right.

false側がrightというのは，ややわかりにくいですが。。

  v : valtyp
  u1 : sesstyp
  v0 : valtyp
  u2 : sesstyp
  IHu1 : {dual u1 (SIn v0 u2)} + {~ dual u1 (SIn v0 u2)}
  IHu2 : {dual u1 u2} + {~ dual u1 u2} ->
         {dual (SIn v u1) u2} + {~ dual (SIn v u1) u2}
  ============================
   ~ dual (SIn v u1) (SIn v0 u2)

私のCoq力が低いせいで，ここからはどうすればいいのかよくわかりません．とりあえず introします (~P == P -> False なので)．

dual_dec> intro.
  v : valtyp
  u1 : sesstyp
  v0 : valtyp
  u2 : sesstyp
  IHu1 : {dual u1 (SIn v0 u2)} + {~ dual u1 (SIn v0 u2)}
  IHu2 : {dual u1 u2} + {~ dual u1 u2} ->
         {dual (SIn v u1) u2} + {~ dual (SIn v u1) u2}
  H : dual (SIn v u1) (SIn v0 u2)
  ============================
   False

試行錯誤の結果，ここから inversionタクティックを H に使うと，矛盾となってくれることがわかりました．目出度い．

dual_dec < inversion H.
6 subgoals
  
  v : valtyp
  u1 : sesstyp
  v0 : valtyp
  u2 : sesstyp
  IHu1 : {dual u1 (SOut v0 u2)} + {~ dual u1 (SOut v0 u2)}
  IHu2 : {dual u1 u2} + {~ dual u1 u2} ->
         {dual (SIn v u1) u2} + {~ dual (SIn v u1) u2}
  ============================
   {dual (SIn v u1) (SOut v0 u2)} + {~ dual (SIn v u1) (SOut v0 u2)}

やったね．

次のサブゴールは 受信と送信の場合なので，双対になるかもしれません．まずは v=v0 とそうでない場合とで場合分けします． v=v0=vboolは明らかですが，型が増えた時のために eq_valtyp_dec を使います．

dual_dec < elim (eq_valtyp_dec v v0).
7 subgoals
  
  v : valtyp
  u1 : sesstyp
  v0 : valtyp
  u2 : sesstyp
  IHu1 : {dual u1 (SOut v0 u2)} + {~ dual u1 (SOut v0 u2)}
  IHu2 : {dual u1 u2} + {~ dual u1 u2} ->
         {dual (SIn v u1) u2} + {~ dual (SIn v u1) u2}
  ============================
   v = v0 ->
   {dual (SIn v u1) (SOut v0 u2)} + {~ dual (SIn v u1) (SOut v0 u2)}

subgoal 2 is:
 v <> v0 -> {dual (SIn v u1) (SOut v0 u2)} + {~ dual (SIn v u1) (SOut v0 u2)}
...(他5個のサブゴール)

このサブゴールはv=v0なので，introしてrewriteしてゴールのvをv0に書き換えてやります．

dual_dec < intro eqv. rewrite eqv.

7 subgoals
  
  v : valtyp
  u1 : sesstyp
  v0 : valtyp
  u2 : sesstyp
  IHu1 : {dual u1 (SOut v0 u2)} + {~ dual u1 (SOut v0 u2)}
  IHu2 : {dual u1 u2} + {~ dual u1 u2} ->
         {dual (SIn v u1) u2} + {~ dual (SIn v u1) u2}
  eqv : v = v0
  ============================
   {dual (SIn v0 u1) (SOut v0 u2)} + {~ dual (SIn v0 u1) (SOut v0 u2)}

続きのセッションu1 とu2が双対かどうかで場合分けします．
と…あれ？帰納法の仮定が何か変です！ よくわからないので Undo ．
最初にrefineとfixを使ってゴニョゴニョしておくことにします． fixタクティックを使ってもできそうなのですがよくわからないのでパス．

dual_dec < refine (fix f(u1 u2:sesstyp) : {dual u1 u2}+{~dual u1 u2} := _).
1 subgoal
  
  f : forall u1 u2 : sesstyp, {dual u1 u2} + {~ dual u1 u2}
  u1 : sesstyp
  u2 : sesstyp
  ============================
   {dual u1 u2} + {~ dual u1 u2}

こんな感じで．注意点として，fを何かに適用するときはu1,u2のどちらかより小さな項が必要です．

さっきの所に戻ってきましょう．もうinductionは必要ないので caseタクティックで場合分けします．適度にintrosを挟むと…

dual_dec < induction u1. induction u2. right. intro. inversion H. elim (eq_valtyp_dec v v0). intro eqv. rewrite eqv.
7 subgoals
  
  f : forall u1 u2 : sesstyp, {dual u1 u2} + {~ dual u1 u2}
  u1 : sesstyp
  u2 : sesstyp
  v : valtyp
  u1' : sesstyp
  v0 : valtyp
  u2' : sesstyp
  eqv : v = v0
  ============================
   {dual (SIn v0 u1') (SOut v0 u2')} + {~ dual (SIn v0 u1') (SOut v0 u2')}

ここに戻ってきます．今度は u1, u2 より小さい u1', u2' について帰納法の仮定fを使えます．
elimタクティックを使って…

dual_dec < 
8 subgoals
  dual_dec < elim (f u1' u2').
  f : forall u1 u2 : sesstyp, {dual u1 u2} + {~ dual u1 u2}
  u1 : sesstyp
  u2 : sesstyp
  v : valtyp
  u2' : sesstyp
  v0 : valtyp
  u1' : sesstyp
  eqv : v = v0
  ============================
   dual u1' u2' ->
   {dual (SIn v0 u1') (SOut v0 u2')} + {~ dual (SIn v0 u1') (SOut v0 u2')}

subgoal 2 is:
 ~ dual u1' u2' ->
 {dual (SIn v0 u1') (SOut v0 u2')} + {~ dual (SIn v0 u1') (SOut v0 u2')}
(他6つのサブゴール)

またサブゴールが増えました…． dual u1' u2' の場合と ~dual u1' u2' の場合が必要です．まずは dual u1' u2' の場合．
これはtrue側ですので leftを選びます． 

dual_dec < intro. left.  
8 subgoals
  
  f : forall u1 u2 : sesstyp, {dual u1 u2} + {~ dual u1 u2}
  u1 : sesstyp
  u2 : sesstyp
  v : valtyp
  u2' : sesstyp
  v0 : valtyp
  u1' : sesstyp
  eqv : v = v0
  a : dual u1' u2'
  ============================
   dual (SIn v0 u1') (SOut v0 u2')
(他7)

ここで inductive predicate の 帰納段階 DualInOut を使うと…

dual_dec < apply (DualInOut v0 u1' u2' a).
7 subgoals
  
  f : forall u1 u2 : sesstyp, {dual u1 u2} + {~ dual u1 u2}
  u1 : sesstyp
  u2 : sesstyp
  v : valtyp
  u2' : sesstyp
  v0 : valtyp
  u1' : sesstyp
  eqv : v = v0
  ============================
   ~ dual u1' u2' ->
   {dual (SIn v0 u1') (SOut v0 u2')} + {~ dual (SIn v0 u1') (SOut v0 u2')}
(他6)

めでたく サブゴールをつぶせました．最後にこのサブゴールもやってみましょう．
前提をintroして，false側を選んで(right)，~ほげほげ を intro すると

dual_dec < intro. right. intro H. 
7 subgoals
  
  f : forall u1 u2 : sesstyp, {dual u1 u2} + {~ dual u1 u2}
  u1 : sesstyp
  u2 : sesstyp
  v : valtyp
  u2' : sesstyp
  v0 : valtyp
  u1' : sesstyp
  eqv : v = v0
  b : ~ dual u1' u2'
  H : dual (SIn v0 u1') (SOut v0 u2')
  ============================
   False
(他6)

ここで inversion H すると，inductive predicateのDualInOutの場合の仮定 dual u1' u2' が現れるので，False を導けます．

dual_dec < inversion H.
7 subgoals
  
  f : forall u1 u2 : sesstyp, {dual u1 u2} + {~ dual u1 u2}
  u1 : sesstyp
  u2 : sesstyp
  v : valtyp
  u2' : sesstyp
  v0 : valtyp
  u1' : sesstyp
  eqv : v = v0
  b : ~ dual u1' u2'
  H : dual (SIn v0 u1') (SOut v0 u2')
  v1 : valtyp
  u0 : sesstyp
  u3 : sesstyp
  H1 : dual u1' u2'
  H0 : v1 = v0
  H2 : u0 = u1'
  H3 : u3 = u2'
  ============================
   False
(他6)

dual_dec < apply (b H1).
6 subgoals
...

矛盾する仮定がある場合にどうやってFalseを導いたものかよくわからなかったので， ~ P == P -> False を使って， apply (b H1) で False を導いてます．

勉強になったこと

証明技法については残念ながら素人な私ですが，これだけやってみると勉強になりました．

  • 仮定に現れたinductive predicateがありえない場合は inversion で活路を開く
  • 場合分けの時にelimは超便利．
  • inductionで帰納法がうまく回らない場合は fixを使う
  • fixを使うときも inductionで場合分けする

完全な証明

Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual u1 u2}+{~dual u1 u2}.
refine (fix f (u1 u2 : sesstyp) : {dual u1 u2} + {~ dual u1 u2} := _).
induction u1.
 induction u2.
  right.
  intro.
  inversion H.
  
  elim (eq_valtyp_dec v v0).
   intro eqv.
   rewrite eqv in |- *.
   elim (f u1 u2).
    intro.
    left.
    apply (DualInOut v0 u1 u2 a).
    
    intro.
    right.
    intro H.
    inversion H.
    apply (b H1).
    
   intro.
   right.
   intro H.
   inversion H.
   apply (b H3).
   
  right.
  intro H.
  inversion H.
  
  right.
  intro H.
  inversion H.
  
 induction u2.
  elim (eq_valtyp_dec v v0).
   intro.
   rewrite a in |- *.
   elim (f u1 u2).
    intro.
    left.
    apply (DualOutIn v0 u1 u2 a0).
    
    intro.
    right.
    intro H.
    inversion H.
    apply (b H1).
    
   intro.
   right.
   intro H.
   inversion H.
   apply (b H3).
   
  right.
  intro H.
  inversion H.
  
  right.
  intro H.
  inversion H.
  
  right.
  intro H.
  inversion H.
  
 right.
 intro H.
 inversion H.
 
 induction u2.
  right.
  intro H.
  inversion H.
  
  right.
  intro H.
  inversion H.
  
  right.
  intro H.
  inversion H.
  
  left.
  apply DualEnd.

Qed.

right. intro H. inversion H. ばかりが目立ちます…