Prove forall f (b: bool), f (f b) <> f b -> f (f (f b)) = f b?

Using Coq
1

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 const false).

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 negb.

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?

2

I am not sure I perfectly understand the shape of the proof you are looking for, but concerning Lemma bool_cycle, the property f b <> b looks like a natural thing to deduce from f (f b) <> f b.
A second point is that in order to “use” inequalities like f b <> true, you can rely on properties like not_true_is_false from the standard library.

3

Here is a completely over-engineered proof.

Definition extensional {A B} (P : (forall x : A, B x) -> Prop) :=
  forall (f g : forall x : A, B x), (forall x, f x = g x) -> P f -> P g.

Lemma rect :
  forall (P : (bool -> bool) -> Prop), extensional P ->
    P (fun _ => true) ->
    P (fun _ => false) ->
    P (fun x => x) ->
    P negb -> forall f, P f.
Proof.
intros P HP pt pf pid pneg f.
remember (f true) as b0.
remember (f false) as b1.
destruct b0, b1.
+ eapply HP, pt; intros [|]; assumption.
+ eapply HP, pid; intros [|]; assumption.
+ eapply HP, pneg; intros [|]; assumption.
+ eapply HP, pf; intros [|]; assumption.
Qed.

Lemma bool_cycle:
    forall f (b: bool),
        f (f b) <> f b -> f (f (f b)) = f b.
Proof.
intros f b; pattern f.
apply rect; try congruence.
+ clear; intros f g Hfg.
  rewrite <-! Hfg; tauto.
+ destruct b; reflexivity.
Qed.
4

With @ppedrot 's approach, it is even more natural to go directly to Theorem f3x rather than through Lemma bool_cycle:

Theorem f3x: forall (f: bool -> bool) b, f (f (f b)) = f b.
Proof.
intros f b; pattern f.
apply rect; try congruence.
destruct b; reflexivity.
Qed.
1 Like