destruct them all

[dmytrish]

Є, значить, тут теоремка із першого розділу Software Foundations:

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


В принципі, ясно, що твердження покладається на семантику операцій andb та orb, і тому доводити його треба через аналіз можливих випадків b і c. Тактику destruct в книжці уже показували, тому, здавалось би, залишилось проаналізувати випадки:

1 subgoal

============================
forall b c : bool, (b && c)%bool = (b || c)%bool -> b = c

andb_eq_orb < intros b c.
1 subgoal

b : bool
c : bool
============================
(b && c)%bool = (b || c)%bool -> b = c

andb_eq_orb < destruct b.
2 subgoals

c : bool
============================
(true && c)%bool = (true || c)%bool -> true = c

subgoal 2 is:
(false && c)%bool = (false || c)%bool -> false = c

andb_eq_orb < destruct c.
3 subgoals

============================
andb true true = orb true true -> true = true

subgoal 2 is:
andb true false = orb true false -> true = false
subgoal 3 is:
forall c : bool, andb false c = orb false c -> false = c

andb_eq_orb < reflexivity.
2 subgoals

============================
andb true false = orb true false -> true = false

subgoal 2 is:
forall c : bool, andb false c = orb false c -> false = c

andb_eq_orb < reflexivity.
Toplevel input, characters 0-11:
> reflexivity.
> ^^^^^^^^^^^
Error: Impossible to unify "false" with "true".

А от тут я перестаю розумію, чому Coq не може обчислити, що andb true false = orb true false -> true = false це правда. Здавалось би, простий reflexivity:

andb true false = orb true false -> true = false;
false = orb true false -> true = false;
false = true -> true = false;
false -> false;
true.

Підкажіть новачку, що тут не так.

P.S. simpl допоміг, цікаво, перечитаю про різницю між ним і reflexivity.
P.P.S. Довелось ще поборотись із зведенням false = true -> true = false, неочевидний трюк: intro H. rewrite H.. В результаті таки довів (хоч і почуваюсь індусом, який пише на Coq):


Proof.
destruct b.
destruct c.
simpl. reflexivity.
simpl. intro H. rewrite H. reflexivity.
destruct c.
simpl. intro H. rewrite H. reflexivity.
simpl. reflexivity.
Qed.