具有多个字段的类型类与 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).

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

Typeclasses with multiple fields vs. single field in Coq / Unexpected behaviour of Compute command

typeclass

coq