Consider this theorem:
Theorem f3x: forall (f: bool -> bool) b, f (f (f b)) = f b.
(It is an exercise from a popular book, but I would like not to make it easily searchable, as per the request of the authors, so the name is altered. What follows is my own work.)
It can be proven with the tactic of brutality:
Proof. intros. destruct (f true) eqn: T, (f false) eqn: F, b. * rewrite T, T, T. reflexivity. * rewrite F, T, T. reflexivity. * rewrite T, T, T. reflexivity. * rewrite F, F, F. reflexivity. * rewrite T, F, T. reflexivity. * rewrite F, T, F. reflexivity. * rewrite T, F, F. reflexivity. * rewrite F, F, F. reflexivity. Qed.
— So it must be true. Giving it some informal thought, there are 2 kinds of subsets in the domain of a function: attractors and cycles. With
bool, it is trivial: there is one function with a 2-cycle (
negb), one function with 2 attractors (
id) and two functions with one attractor (
const true and
It is therefore plausible to believe that these two lemmas describe the situation with fidelity:
Lemma bool_attractor: forall f (b: bool), f (f b) = f b -> f (f (f b)) = f b. Lemma bool_cycle: forall f (b: bool), f (f b) <> f b -> f (f (f b)) = f b.
For the first one, the proof is immediate:
Proof. intros. rewrite H, H. reflexivity. Qed.
— But I was unable to prove the latter. (Other than by reference to
f3x.) Once I
intro the boolean value, the hypothesis specializes to it, and I can never prove both
f true = false and
f false = true. The inequality sign does not help, since I do not really know how to either transform it to equality or utilize directly, so I resort to converting it with a lemma like
b <> b' -> b = negb b' /\ negb b = b', or otherwise rephrase the problem in terms of
Please explain this situation to me. Should I think that the kind of reasoning I am trying to apply here is too «classical» for Coq? Or am I missing some sharp move?