当在 Coq 中使用自己的可判定性时，Eval 计算是不完整的

Question

Eval compute 命令的计算结果并不总是简单的表达式。考虑代码：

Require Import Coq.Lists.List.
Require Import Coq.Arith.Peano_dec.
Import ListNotations.

Inductive I : Set := a : nat -> I | b : nat -> nat -> I.

Lemma I_eq_dec : forall x y : I, {x = y}+{x <> y}.
Proof.
  repeat decide equality.
Qed.

并且，如果我执行以下命令：

Eval compute in (if (In_dec eq_nat_dec 10 [3;4;5]) then 1 else 2).

Coq 告诉我结果是 2。但是，当我执行以下表达式时：

Eval compute in (if (In_dec I_eq_dec (a 2) [(a 1);(a 2)]) then 1 else 2).

我得到一个很长的表达式，其中 In-predicate 似乎展开了，但没有给出结果。

我必须更改什么才能在最后 Eval compute 行中获得答案 1？

Answer 1

如果你想评估你的证明，你需要让它们透明。您可以使用 Defined 命令完成它们。 Qed 命令使它们不透明，这意味着它丢弃了它们的计算内容。

Answer 2

在 Coq 中，有两个用于证明脚本的终止符命令：Qed 和 Defined。它们之间的区别在于前者创建 不透明 项，即使 Eval compute 也无法展开。后者创建透明的条款，然后可以像往常一样展开。因此，您只需将 Defined 放在 Qed.:

的位置

Require Import Coq.Lists.List.
Require Import Coq.Arith.Peano_dec.
Import ListNotations.

Inductive I : Set := a : nat -> I | b : nat -> nat -> I.

Lemma I_eq_dec : forall x y : I, {x = y}+{x <> y}.
Proof.
  repeat decide equality.
Defined.

Eval compute in (if (In_dec I_eq_dec (a 2) [(a 1);(a 2)]) then 1 else 2).

我个人觉得 sumbool 类型 {A} + {B} 不太适合表达可判定的命题，正是因为证明和计算太纠缠在一起了；特别是，证据会影响术语的减少方式。我发现最好遵循 Ssreflect 风格，将证明和计算分开并通过特殊谓词将它们联系起来：

Inductive reflect (P : Prop) : bool -> Set :=
  | ReflectT of P : reflect P true
  | ReflectF of ~ P : reflect P false.

这提供了一种方便的方式来说明布尔计算 returns 为真当且仅当某些属性为真。 ssreflect 支持方便地在计算布尔视图和逻辑视图之间切换。

当在 Coq 中使用自己的可判定性时，Eval 计算是不完整的

Eval compute is incomplete when own decidability is used in Coq

coq