More than 5 years have passed since last update.
introsタクティック
まず最初に覚えるタクティックがintrosだから、intros出来る形だとついついintrosしたくなりますよね。
forall b c : bool, P -> Q -> R
という形ならば、
introsbcpq.としたくなるのが人の性。
では次の例はどうでしょう。
Theoremandb_eq_orb:forall(bc:bool),(andbbc=orbbc)->b=c.早速
introsbcH.とすると
1 subgoal
b : bool
c : bool
H : (b && c)%bool = (b || c)%bool
______________________________________(1/1)
b = c
なるほど。bとcはboolなのでtrueとfalseで場合分けして……
destructb.destructc.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タクティックを使ったところで
introsbc.destructb.destructc.としてみましょう。すると……
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タクティックがうまくいきそうなゴールの形になりましたね。
Theoremandb_eq_orb:forall(bc:bool),(andbbc=orbbc)->b=c.Proof.introsbc.destructb.destructc.simpl.reflexivity.simpl.introsH.rewriteH.reflexivity.simpl.introsH.rewriteH.reflexivity.Qed.これで完成。なーんだ。最初の intros H は要らなかったんですね。
あとがき
このTheoremは、 Software Foundations の例題として載っていたものです。この例題が出る段階ではまだ習ったタクティックが非常に少ないため、仮定に矛盾が含まれている場合どうすればいいのかがわかりませんでした。intros出来る形だと何でもかんでもintrosしていた私は見事にハマりました。introsするときはその意味をよく考えるべしといういい教訓になりました。
参考
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme