当 Coq 中使用自己的可判定性时，评估计算不完整

The 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 似乎已展开，但没有给出结果。

我必须改变什么才能获得答案1在最后Eval compute line ?

在 Coq 中，有两个用于证明脚本的终止符命令：Qed and Defined。它们之间的区别在于前者创建opaque术语，即使通过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}不太适合表达可判定的命题，正是因为证明和计算太纠缠在一起；特别是，证明会影响项的减少方式。我发现最好遵循反射风格，分离证明和计算，并通过特殊谓词将它们联系起来：

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

这提供了一种方便的方式来表示当且仅当某些属性为 true 时布尔计算返回 true。 Ssreflect 提供了在计算布尔视图和逻辑视图之间方便切换的支持。