An exercise in dependent types (解答編) - 論理とか計算機とか数学とか

http://lkozima.hatenablog.com/entry/2014/09/15/013735 の続き。ホーア論理の健全性の証明をやろうとしていたのでした。

一箇所ちょっと難しいところがあるような気がしたのでそれについて書こうとしていたのですが，あれこれ調べているうちに簡単な解決策があることに気付いたうえに，それで解決してしまうとあんまり an exercise in dependent types になりませんでした。困った。

でも簡単な方法があることがわかっているのにわざわざややこしい証明を書きたくもないので，簡単な方の解答を書きます。でもその前に依存型が出てくる話をします。

何がややこしい（と思った）か

証明することはこれ。

Theorem hoare_sound : forall ht, hoare_provable ht -> hoare_valid ht.

ホーア論理の健全性って，帰納法でできるし別に難しくないんじゃないの，という気がするわけですが，実際にやってみると一箇所詰まりました。とりあえず帰納法をやろうとすると，規則が 5 つあるから 5 つの subgoal が出てくるわけですが，一つめ（代入文の場合）がこんな形になります。

5 subgoals, subgoal 1 (ID 673)

  c : context
  ht : hoare_triple c
  ============================
   forall (m : member c) (e : expression c (type_of_var m))
     (post : environment c -> Prop) (env env' : environment c),
   post (update_env env m (eval_expression env e)) ->
   exec_program (PAssign m e) env env' -> post env'

普通の証明だと，4 行目の exec_program ... に対して inversion lemma を使って env' の形が決まって，それは確かに仮定から post を満たす，という流れになります。まあ今回もそういう方針なのですが。

というわけでとりあえず

inversion 2.

としてみると，こうなります。

5 subgoals, subgoal 1 (ID 730)

  c : context
  ht : hoare_triple c
  m : member c
  e : expression c (type_of_var m)
  post : environment c -> Prop
  env : environment c
  env' : environment c
  H : post (update_env env m (eval_expression env e))
  H0 : exec_program (PAssign m e) env env'
  m0 : member c
  env0 : environment c
  H2 : m0 = m
  e1 : expression c (type_of_var m)
  H3 : existT (fun m1 : member c => expression c (type_of_var m1)) m e1 =
       existT (fun m1 : member c => expression c (type_of_var m1)) m e
  H1 : env0 = env
  H4 : update_env env m (eval_expression env e1) = env'
  ============================
   post (update_env env m (eval_expression env e1))

H は元々のゴールの仮定にあったやつが inversion したときに上に移動したもので，これがそのまま結論になることが期待されるのですが，なんかちょっと違います。H の中で e になってる部分が結論では e1 になっています。

inversion を使ったときはだいたいいくつか等式が生成されるので，普通は e1 = e が前提のどこかにあるんですが，どうもそれらしいものがありません。

よく見ると H3 が等式で，左辺に e1 が，右辺に e が出てきています。他にそれらしいものもないので，これが e1 = e の代わりに出てきたらしいと推測できます。一見 existT というコンストラクタに渡されているのだから injection で e1 = e が出てきそうですが，直ちには導けません。これがややこしいところ。

なんで existT が出てくるのか

短く言えば，PAssign の第二引数の型が第一引数に依存しているためにこういうことになるのでしょう（inversion の中身をよく知りませんが）。

プログラムの構文をどう定義したか思い出すと，こんなふうになってました。

Inductive program c : Set :=

    
     PAssign : forall m : member c, expression (type_of_var m) -> program
    
(* 以下略 *)

代入文の右辺の型は左辺の型に一致しなければならないという制約があるため，第二引数（本当は第三引数と言うべきかも）の型が依存型になっています。

forall m, expression (type_of_var m) -> program が PAssign の型ですが，こいつは sigT (fun m => expression (type_of_var m)) -> program とだいたい同じであることを考えると，PAssign は existT _ m e みたいなものを受け取っているとも考えられるわけで，そうすると前出の H3 みたいなものが出てきてもおかしくはない気がします。

解決方法

そういうわけなので，H3 から何とかして e1 = e を出せるかどうか，というあたりが問題になりそう……と思ってあれこれやっていたのですが，別にそんなことはないことがわかりました。dependent rewrite を使うと e1 が e に書き換えられます。

それだけ。ちなみに e1 = e を証明する方法も下のほうにちょっと書きます。

証明

というわけでこうなりました。

  Theorem hoare_sound : forall ht, hoare_provable ht -> hoare_valid ht.
    move => ht; elim => /=.
    - inversion 2.
      match goal with [H : _ |- _] => by dependent rewrite H end.
    - by inversion 2; subst.
    - by inversion 6; firstorder.
    - by inversion 6; firstorder.
    - move => e p inv HPinv HVinv env env' inv_env.
      move pweq : (PWhile e p) => p'.
      move => H; move : H HPinv HVinv inv_env pweq; elim => //.
      + move => e0 p0 env1 env2 env3 env1_e p0_env1_env2 IH1
                  pw_env2_env3 IH2 HPinv HVinv inv_env1 [? ?].
        by subst; eauto.
      + move => e0 p0 env0 n_e0 HPinv HVinv inv_env0 [? ?].
        by subst.
  Qed.

ついでに e1 = e2 の証明

ちなみに今の場合は e1 = e も証明できるので簡単に書いてみます。

inj_pair2_eq_dec という補題があるので，このあたりを使うとよさそうです。

あるいは ssreflect の場合 eqType に対して成り立つ eq_axiomK という補題（Corollary って宣言されてるけど）があるので，これを使うとよい気がします。

いずれにしても member が decidable equality を持つことを証明しないといけませんが，頑張ればできます。

以下頑張ったコード。

Scheme Equality for vtype.
Canonical vtype_eqMixin := comparableClass vtype_eq_dec.
Canonical vtype_eqType := Eval hnf in EqType vtype vtype_eqMixin.

Lemma member_eq_dec' c c' (p : c = c') (m : member c) (m' : member c') :           
  {eq_rect _ _ m _ p = m'} + {eq_rect _ _ m _ p <> m'}.                            
  move: c' m' p; elim : m => {c} [t c | t c m IHm];                                
    move => c'; elim => {c'} [t' c' | t' c' m' IHm'] p => /=;                      
    pose proof p as p'; move : p'; case => ? ?; subst;                             
    rewrite eq_axiomK; [by left | by right | by right |].                          
  case: (IHm c' m' Logic.eq_refl) => /=; [left; congruence | right].               
  by case => H; move : (EqdepFacts.eq_sigT_snd H); rewrite eq_axiomK.              
Qed.

Definition member_eq_dec c m m' := @member_eq_dec' c c Logic.eq_refl m m'.
Canonical member_eqMixin c := comparableClass (@member_eq_dec c).
Canonical member_eqType c := Eval hnf in EqType (member c) (member_eqMixin c).