■

change term

ゴールとtermが変換可能なときに、ゴールをtermで置き換える tacic。

simpl とかを適当に使った結果、やりすぎていらんとこまで置き換えてしまった場合とか、逆に何をどう使えばもっと簡単に置き換えることができるのか分からない場合に使うとよいかも。

例えば、simpl の結果

  ============================
   x =
   match y with
   | 0 => 0
   | Zpos y' => Zpos (xO y')
   | Zneg y' => Zneg (xO y')
   end + x

というわけのわからない式になっちまったが、よく考えると「x = 2 * y + x」じゃねーかってときに

< change (x = 2 * y + x).

とすればよい。

absurd term

仮定に矛盾がありそうなときはこれを使う。termと~termを証明すれば、ゴールを証明したことになる。

普通はtermか~termのどちらかが仮定にそのまま入ってる。すでに両方とも入ってる場合は contradiction を使うとよい。

contradiction

これは tauto でも証明できる。

cbv系

さっぱりわからん。あとで書く。