Coq

状態のところを読む。

Definition mystate : state := 
  fun i => 
   match i with 
   | Id n => n // id nに対応するなんらかのnatを返すことが出来る。
   end.
Definition myid5 := Id 5.
Eval simpl in update mystate myid5 10. (* Id 5に対応する値を 10にするという意味かな？ *)

返るのが新しい状態を表す関数である。dictionaryの時もそうだったっけ。updateはoverrideと似てるというか同じか。
SICPで言うところの環境なのかな？stateというと、stateパターンとか単一の変数を思いうかべてしまう。

Theorem update_neq : forall V2 V1 n st,
  beq_id V2 V1 = false -> (update st V2 n) V1 = (st V1).
Proof .
  intros. unfold update. 
  (* subst. が効かないのはなぜ? *)
  rewrite -> H. reflexivity.
Qed.

substも効いたり効かなかったりだな。このへんがよくわからん。

update_exampleにて、

タクティックを使って遊び始める前に、 定理が言っていることを正確に理解していることを確認しなさい! 

ごもっとも。でもやっぱりタクティック使って証明するのって感覚的にゲームに近いよなあ。