如何在Coq中基于归纳谓词递归定义返回Set类型的函数？

这个问题的核心是Coq和Agda在Prop/Set区分以及证明消除规则上的关键差异：Agda默认允许从证明（即使是Prop级别的）递归构造Set类型的对象，但Coq出于证明无关性和一致性的考虑，禁止直接从Prop类型的证明中提取结构信息来构造Set/Type级别的计算对象。下面是几种实用的解决方案：

1. 将归纳谓词从Prop移到Type/Set #

如果你的归纳谓词本身带有计算意义（比如像Agda里那样，证明的结构对应某种计算步骤），最直接的办法是把它定义在Type而非Prop中。这样Coq就允许你对其进行模式匹配和结构递归，完全复刻Agda的风格。

举个例子：

-- 把Even定义在Type里，而非默认的Prop
Inductive Even : nat -> Type :=
| even_zero : Even 0
| even_suc : forall n, Even n -> Even (S (S n)).

-- 现在可以直接基于Even的结构递归定义返回Set类型的函数
Definition even_to_half (n : nat) (p : Even n) : nat :=
  match p with
  | even_zero => 0
  | even_suc _ p' => S (even_to_half _ p')
  end.

这种方式完全贴合你在Agda中的习惯，因为Type级别的归纳类型自带计算内容，Coq不会限制对它的消除。

2. 利用谓词的可判定性（Decidable） #

如果你的谓词确实是纯证明性质的（必须放在Prop里），但它是可判定的——也就是你能证明forall x, {P x} + {¬P x}（Coq的sumbool类型，属于Set），那可以先证明这个可判定性定理，再基于它来分支定义函数，而非直接匹配Prop中的证明结构。

示例：

-- 纯Prop级别的Even谓词
Inductive Even : nat -> Prop :=
| even_zero : Even 0
| even_suc : forall n, Even n -> Even (S (S n)).

-- 先证明Even的可判定性
Theorem even_dec : forall n, {Even n} + {¬ Even n}.
Proof.
  induction n as [|n IH].
  - left; apply even_zero.
  - destruct n as [|n].
    + right; intros [].
    + destruct IH as [p|np].
      * left; apply even_suc; assumption.
      * right; intros (even_suc p); apply np; assumption.
Qed.

-- 基于可判定性定义返回bool的函数
Definition is_even (n : nat) : bool :=
  match even_dec n with
  | left _ => true
  | right _ => false
  end.

这里我们不需要关心Prop中证明的具体结构，只需要利用“谓词是否成立”的结果来构造Set类型的对象。

3. 使用Equations插件处理复杂依赖消除 #

如果你确实需要基于Prop中证明的结构来构造Set对象（且无法将谓词移到Type），可以使用Coq的Equations插件——它提供了更灵活的依赖模式匹配规则，能绕过部分Coq默认的消除限制，同时保证一致性。

示例：

Require Import Equations.Equations.

Inductive Even : nat -> Prop :=
| even_zero : Even 0
| even_suc : forall n, Even n -> Even (S (S n)).

-- 使用Equations定义依赖Prop证明的函数
Equations even_to_nat (n : nat) (p : Even n) : nat :=
even_to_nat 0 even_zero := 0;
even_to_nat (S (S m)) (even_suc p) := S (even_to_nat m p).

Equations会自动处理消除的合法性检查，只要你的函数满足证明无关性（即不同的证明对应相同的输出结果），就能顺利通过验证。

关键注意点 #

Coq的Prop/Set区分是为了保证证明无关性：Prop中的证明被视为“无计算内容”的，不同的证明应该被等价对待。如果你的函数必须依赖证明的结构，那本质上这个谓词就不应该属于Prop——它带有计算意义，应该放在Type里。

内容的提问来源于stack exchange，提问作者Rodrigo Ribeiro