■

Imp_J.v プログラム正当性 (Optional)
長いうえに何やってんのか分がんね。

apply with の使いかたは何となく分かった気がしないでもない。

現在のコンテキストは H(仮定orなんかの定理)そのものである場合

  apply H.

現在のコンテキスト((サブ)ゴールにある命題)は、全称修飾のパラメータつき命題 (関数)H にあるパラメータ xを適用したものである場合は

apply H with x.

あるいは、

 apply (H x).

とも書ける。

Theorem ceval_step_more: forall i1 i2 st st' c,
  i1 <= i2 ->
  ceval_step st c i1 = Some st' ->
  ceval_step st c i2 = Some st'.

という定理を

  st : state
  st' : state
  c1 : com
  x1 : nat
  x2 : nat 
  H1 : ceval_step st c1 x1 = Some st'

という仮定H1にi2を(x1+x2)で適用したい場合、
正式にはこう書く。

  apply (ceval_step_more x1 (x1+x2) st st' c1) in H1.

適用にかんして、Coqが中途半端によきにはからってくれるので、私のような初心者は混乱する。
実際

   apply  ceval_step_more (i2:=x1+x2)  in H1. 

とも書ける。
そしてやる気を失ないかける。でもまあ、実行出来るかどうかは、実際に動くので一目瞭然なところが、他の教科書と違ってありがたい。