初心者が陥りそうな罠 〜なんでもintrosすればいいってわけじゃない〜

introsタクティック

まず最初に覚えるタクティックがintrosだから、intros出来る形だとついついintrosしたくなりますよね。

forall b c : bool, P -> Q -> R

という形ならば、

intros b c p q.

としたくなるのが人の性。

では次の例はどうでしょう。

Theorem andb_eq_orb : 
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.

早速

  intros b c H.

とすると

1 subgoal
b : bool
c : bool
H : (b && c)%bool = (b || c)%bool
______________________________________(1/1)
b = c

なるほど。bとcはboolなのでtrueとfalseで場合分けして……

  destruct b.
  destruct c.

3 subgoals
H : (true && true)%bool = (true || true)%bool
______________________________________(1/3)
true = true


______________________________________(2/3)
true = false

______________________________________(3/3)
false = c

true = true は

  reflexivity.

で片付けて、

2 subgoals
H : (true && false)%bool = (true || false)%bool
______________________________________(1/2)
true = false


______________________________________(2/2)
false = c

Hの左辺はfalseで右辺はtrueだから、前提に矛盾が含まれるわけだから……

ちょっと待ってください。introsで前提に送ってしまったHの形、複雑過ぎませんか？ 簡約したくなりません？ simplタクティックを使いたくなってきません？

よし、じゃあsimplタクティックを使いましょう。最初のintrosタクティックを使ったところで

  intros b c.
  destruct b.
  destruct c.

としてみましょう。すると……

3 subgoals
______________________________________(1/3)
(true && true)%bool = (true || true)%bool -> true = true


______________________________________(2/3)
(true && false)%bool = (true || false)%bool -> true = false

______________________________________(3/3)
(false && c)%bool = (false || c)%bool -> false = c

お、simplタクティックがうまくいきそうなゴールの形になりましたね。

Theorem andb_eq_orb : 
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  intros b c.
  destruct b.
  destruct c.
    simpl.
    reflexivity.

    simpl.
    intros H.
    rewrite H.
    reflexivity.

    simpl.
    intros H.
    rewrite H.
    reflexivity.
Qed.

これで完成。なーんだ。最初の intros H は要らなかったんですね。

あとがき

このTheoremは、 Software Foundations の例題として載っていたものです。この例題が出る段階ではまだ習ったタクティックが非常に少ないため、仮定に矛盾が含まれている場合どうすればいいのかがわかりませんでした。intros出来る形だと何でもかんでもintrosしていた私は見事にハマりました。introsするときはその意味をよく考えるべしといういい教訓になりました。

参考