当在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似乎展开,但没有给出结果.

为了1在最后Eval compute一行获得答案,我需要更改什么？

Answer 1

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

这给了一个方便的方法来说明如果某个属性为true,则布尔计算返回true.Ssreflect支持在计算布尔视图和逻辑视图之间方便地切换.