0

从软件基础通过 Quick Chick 课程我陷入了以下定理：

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

在这里我们得到：

1 subgoal (ID 164)

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

证明true = true -> (eqb f1 f2) = true似乎是不可能的，因为(eqb f1 f2)可能是错误的，在这种情况下，我们进入false = true了空的上下文，这是无法证明的。

这个定理是不正确的还是我遗漏了什么？

4

1 回答 1

1

该定理无效。

任何命题P <-> true = true都等价于，并且对于所有函数都P无效（至少当有两个或更多居民时）。eqb f1 f2 = truef1, f2 : bool -> AA

于 2020-10-10T15:26:31.233 回答