初心者が陥りそうな罠 〜なんでもintrosすればいいってわけじゃない〜 ref: http://qiita.com/kimitaka@github/items/7879ea3133fe378b178c

file0.txt

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

file1.txt

intros b c p q.

file10.txt

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

file11.txt

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.

file2.txt

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

file3.txt

  intros b c H.

file4.txt

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

file5.txt

  destruct b.
  destruct c.

file6.txt

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


______________________________________(2/3)
true = false

______________________________________(3/3)
false = c

file7.txt

  reflexivity.

file8.txt

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


______________________________________(2/2)
false = c

file9.txt

  intros b c.
  destruct b.
  destruct c.