Coq中具有多个字段的类型类与单个字段的类型类 / Compute命令的意外行为

Question

我正在使用《软件基础》这本书学习Coq中的类型类。

运行以下代码：

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

Notation "x =? y" := (eqb x y) (at level 70).

Instance eqBool : Eq bool :=
{
eqb := fun (b c : bool) => 
   match b, c with
     | true, true => true
     | true, false => false
     | false, true => false
     | false, false => true
   end
}.

Compute (true =? false).

我收到了消息 = false : bool，正如预期的那样。 但如果我做以下操作，

Class Eq A :=
{
eqb: A -> A -> bool;
eqb_refl: forall (x : A), eqb x x = true;
}.

Notation "x =? y" := (eqb x y) (at level 70).

Instance eqBool : Eq bool :=
{
eqb := fun (b c : bool) => 
   match b, c with
     | true, true => true
     | true, false => false
     | false, true => false
     | false, false => true
   end
}.
Proof.
  intros []; reflexivity.
Qed.

Compute (true =? false).

我收到了这条消息：= (let (eqb, _) := eqBool in eqb) true false : bool。我似乎无法简化这个表达式，并且不确定出了什么问题以及在哪里。如何使用额外的假设定义上述类型类，并仍然能够使用我定义的实例（即获得与之前相同的消息）？

非常感谢！

- David

Answer 1

Qed 命令创建不透明的定义，这些定义不会被像 Compute 这样的命令展开。你可以使用 Program Instance 命令告诉 Coq 仅使证明义务不透明：

Require Import Coq.Program.Tactics.

Class Eq A :=
{
eqb: A -> A -> bool;
eqb_refl: forall (x : A), eqb x x = true;
}.

Notation "x =? y" := (eqb x y) (at level 70).

Program Instance eqBool : Eq bool :=
{
eqb := fun (b c : bool) =>
   match b, c with
     | true, true => true
     | true, false => false
     | false, true => false
     | false, false => true
   end
}.
Next Obligation. now destruct x. Qed.

Compute (true =? false).

- Arthur Azevedo De Amorim

---

另一种方法是重用现有的函数和它们的证明：From Coq Require Import Bool. Instance eqBool : Eq bool := { eqb := eqb; eqb_refl := eqb_reflx }. - Anton Trunov