[SOLVED] Quick Chick eqBoolArrowA

Quick Chick eqBoolArrowA_correct theorem

Passing Quick Chick course from Software foundations I am stuck at the following theorem:

Class Eq A :=
{
    eqb: A -> A -> bool;
}.


Instance eqBoolArrowA {A : Type} `{Eq A} : Eq (bool -> A) :=
{
  eqb f1 f2 :=
           (andb (eqb (f1 false) (f2 false)) (eqb (f1 true) (f2 true)))
}.

Theorem eqBoolArrowA_correct : forall (f1 f2 : bool -> bool -> nat),
                                      (eqb f1 f2) = true <-> true = true.
Proof.
  intros. split.
  - destruct (f1 =? f2).
    + intro. assumption.
    + intros H. discriminate H.
  - intros _. destruct (f1 =? f2).
    + reflexivity.
    +

Here we get:

1 subgoal (ID 164)

  f1, f2 : bool -> bool -> nat
  ============================
  false = true

Proving true = true -> (eqb f1 f2) = true seems impossible, because (eqb f1 f2) can be false, and in this case we get false = true in empty context, which is unprovable.

Is this theorem incorrect or am I missing something?

Solution

That theorem is not valid.

Any proposition P <-> true = true is equivalent to P, and it is not valid that eqb f1 f2 = true for all functions f1, f2 : bool -> A (at least when A has two or more inhabitants).