LoginSignup
3

More than 5 years have passed since last update.

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

Posted at

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するときはその意味をよく考えるべしといういい教訓になりました。

参考

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
3