Software Foundations

Imp.v

初めて読むところが多くなってきたので読むスピードが落ちる。
スピードが0になったら終わり。

一度手動で全部書いてからでないと、「便利なタクティカル」とやらをちっともどうやって使ったらいいのか分からない。いずれ慣れるのだろうか。

プログラミング言語の基礎概念のオンライン演習をやってるので、この章でやってることのイメージは明確に分かる。よかったよかった。

やはり、副作用は悪。というより変わり続ける環境を常に把握出来るほどの自分の頭のスタック領域は広くありません。

Theorem pup_to_2_ceval :
  pup_to_n / (update empty_state X 2) ||
    update (update (update (update (update (update empty_state
      X 2) Y 0) Y 2) X 1) Y 3) X 0.
Proof.
  unfold pup_to_n.
  apply E_Seq with (st':=(update (update empty_state X 2) Y 0)).
  apply E_Ass. reflexivity.
  apply E_WhileLoop with (st':=(update (update (update (update empty_state X 2) Y 0) Y 2) X 1)).
  Case "while condition". reflexivity.
  Case "while_body".  
    apply E_Seq with (st':=(update (update (update empty_state X 2) Y 0) Y 2)).
    apply E_Ass. compute. reflexivity.
    apply E_Ass. compute. reflexivity.
  apply E_WhileLoop with (st':= update (update (update (update (update (update empty_state X 2) Y 0) Y 2) X 1)
        Y 3) X 0).
  Case "while condition". simpl. reflexivity.
  Case "while body". 
    apply E_Seq with (st':=
     (update (update (update (update (update empty_state X 2) Y 0) Y 2) X 1)
        Y 3)).
    apply E_Ass. simpl. reflexivity.
    apply E_Ass.  simpl.  reflexivity.
  apply E_WhileEnd. simpl. reflexivity.
Qed.

環境のupdateだらけ。

whileのないプログラムの停止性証明って、

Theorem no_while_always_stop : forall c,
  no_whilesR c -> exists st,  exists st', c / st || st'.

んな感じでいいんだろか。
場合分けが死ぬほど面倒臭い。