coq - 具有多个字段的类型类与 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。我似乎无法简化这个表达式，也不确定哪里出了问题。我怎样才能用额外的假设定义上面的类型类，并且仍然能够使用我定义的实例(即得到与以前相同的消息)？

非常感谢!

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