Software Foundations

Software Foundations Imp.v

全開前回挫折したとこまで再び到達。前よりは若干分かってる感じもする。

http://d.hatena.ne.jp/morita_non/20130928/1380366939
で書いた、関係 bevalR のどこが間違ってるとか。

関係なのに、関数aevalと混ぜたらあかんやろ。

Reserved Notation "e '||' b" (at level 50, left associativity).

Inductive bevalR : bexp -> bool -> Prop :=
  | E_BTrue  : BTrue || true
  | E_BFalse : BFalse || false
  | E_Eq     : forall (a1 a2 : aexp) (n1 n2: nat), aevalR a1 n1 -> aevalR a2 n2 -> BEq a1 a2 || beq_nat n1 n2
  | E_Le     : forall (a1 a2 : aexp) (n1 n2: nat), aevalR a1 n1 -> aevalR a2 n2 -> BLe a1 a2 || ble_nat n1 n2 
  | E_Not    : forall (e : bexp) (b : bool) , e || b -> BNot e || negb b 
  | E_And    : forall (e1 e2 : bexp) (b1 b2 : bool), e1 || b1 -> e2 || b2 -> BAnd e1 e2 || andb b1 b2
  where "e '||' b" := (bevalR e b) : type_scope.

こうやって、aexpの関係を記述するところで||を使用せずにaevalRと書けば、aevalRとbevalRで、評価のために同じ記号 '||'が使えるようになるっぽいな。

generalize dependent

generalize dependentの意味がやっと分かった。
introsで 変数をコンテキストに上げるとは、「関数の引数にする。」ということ。そして、「値が引数として与えられた、関数の中で考える」ということ。

Theorem double_injective : forall n m,
     double n = double m -> n = m.
Proof.

ここで、intros n m.としてしまうことは、
fun (n : nat) (m : nat) => ...
と、mがnとは無関係に与えられるものとして考えを進めることになる。
しかし、nとmはこの場合、無関係ではありえない。nが与えられたら、mはそれに応じて決まるものであり、n = 1と与えたときに、m = 100と好きに与えて考えるような命題ではない。

こーゆーちょっと頭のいい小学生でも分かるようなことが、今の今まで分かってないんだから、確かにこの本読むのは無謀だと自分でも思う。