■

仕事でPlay2を少し調べた。割と簡単そうかなと思う。nodejsなみに扱いやすそうかもしらん。
少しはscalaもやるかな。

今日のCoq

Imp_J.vに入る。四則演算も満足に出来ないミニ言語のくせに、証明がいきなり長い。それに応じてTacticも大量に出て来た。それぞれが何やってんのかすらよく分からない。

• tryタクティカル
• ;タクティカル
• Tactic Notation

• clear H: 仮定Hをコンテキストから消去します。

• subst x: コンテキストから仮定 x = e または e = x を発見し、 xをコンテキストおよび現在のゴールのすべての場所でeに置き換え、 この仮定を消去します。

• subst: x = e および e = x の形のすべての仮定を置換します。

• rename... into...: 証明コンテキストの仮定の名前を変更します。 例えば、コンテキストがxという名前の変数を含んでいるとき、 rename x into y は、すべてのxの出現をyに変えます。

• assumption: ゴールにちょうどマッチする仮定Hをコンテキストから探そうとします。 発見されたときは apply H と同様に振る舞います。

• contradiction: Falseと同値の仮定Hをコンテキストから探そうとします。 発見されたときはゴールを解きます。

• constructor: 現在のゴールを解くのに使えるコンストラクタcを (現在の環境のInductiveによる定義から)探そうとします。 発見されたときは apply c と同様に振る舞います。

そして究極の omega。FF5か。

関係を記述するbevalR問題で苦闘。定義が間違ってんのか証明が下手糞なのか区別がつかない。
というところで、omegaタクティクを思い出す。

Theorem beval_iff_bevalR : forall (be : bexp) (b : bool),
  (be || b) <-> beval be = b.
Proof.
  intros. omega.

で、ドン

Toplevel input, characters 15-20:
Error: Omega: Can't solve a goal with equality on bool

あー定義まちがってるようだわ。おかしーな。