■

assert form

ゴールを直接の証明が簡単には書けないので、とりあえず簡単に証明できる中間結果を教えるtactic。
ringとかomegaで一発で証明するには複雑すぎるときに、問題を二つに分けるとよいことがある。

中間結果 form を指定すると、サブゴールにformが追加されて、元のゴールにはformが仮定として追加される。

< Goal forall x y: Z, x>=0 -> x*x>y*y -> x-y>0.
< intros.

1 subgoal

  x : Z
  y : Z
  H : x >= 0
  H0 : x * x > y * y
  ============================
   x - y > 0

ここで、定理 Zgt_square_simpl を使いたいわけだが、この定理は「x-y>0」ではなく「x>y」を導くものなので、直接は適用できない。そこで、assert を使って

Unnamed_thm < assert (x>y); auto with zarith.
1 subgoal

  x : Z
  y : Z
  H : x >= 0
  H0 : x * x > y * y
  ============================
   x > y

これで定理が使える形になったので、apply Zgt_square_simpl すれば証明が終わる。

assert (identifier:=term)

これは assert と exact を続けて実行したのと同じだが、論理式を書くのが億劫な場合に便利。
仮定に forall があって、それを例化した仮定を後でたくさん使いたいときに使うとよい。

  H : forall x : nat, P x -> Q x -> R x
  y : nat
  ============================

たとえば上のような場合で、「P y -> Q y -> R y」は導けるので

  H : forall x : nat, P x -> Q x -> R x
  y : nat
  Hy : P y -> Q y -> R y
  ============================

としておけば、後で Hy を何度も使う場合は便利である。この状態にもっていくのに普通の assert を使うと

< assert (Hy: P y -> Q y -> R y); auto.

と書かないといけないが、こっちの形式で書くと

< assert (Hy := H y).

と書くだけでよい。

cut form

これは基本的に assert と同じであるが、できあがるサブゴールの並び順が逆になる。

apply term in ident

assert のところに書いたことを、apply 一発で済ませられる tactic。
仮定に「H: T -> U」があって、定理「th: U->V->W」があったとすると、

apply th in H.

を実行すると、T と V を証明すれば W が仮定に追加できる状態になる。例えば、

  x : Z
  y : Z
  H : x >= 0
  H0 : y = 1 -> x * x > y * y
  ============================

で、

apply Zgt_squre_simpl in H0.

とすれば、「x >= 0」と「y = 1」を証明すれば「x > y」を使えるようになる。
Zgt_squre_simpl の前提は「n >= 0」と「n * n > m * m」なので、H に対して適用してもよいのだが

apply Zgt_squre_simpl in H.

では、「m」を何にして定理を適用するのか不明なのでだめで、

apply Zgt_squre_simpl with (m:=y) in H.

と書かないといけない。

この方法で適用できる定理を見つけるのは面倒なので、使えそうな定理を知ってるときにしか使えないと思う。