我对Coq非常陌生。我正在尝试使用Coq的依赖类型。我想做的就是简单地将偶数提供给函数。例如，使用伪代码：
def add_two_even(n: {n: Integer | n is even}) :=
{
add n 2
}
然后，我想使用具有不同参数的函数，例如（以伪代码）：
add_two_even(1) // Coq should show an error
add_two_even(4) // Coq should compute 6
所以，在Coq中，我想执行以下操作：
Compute (add_two_even 1).
Compute (add_two_even 4).
我如何构造它？
这里是您在Coq中功能的直接翻译：
From Coq Require Import Arith.
Definition add_two_even (n : {n : nat | Nat.even n = true}) : nat :=
proj1_sig n + 1.
注意，您需要proj1_sig函数才能从子集类型n中提取{n : nat | Nat.even n = true}。要使用add_two_even，您还需要采取另一种方法：从数字转到{n | Nat.even n = true}的元素。在Coq中，这需要手动证明。对于n的具体值，这很容易：
(* The next command fails with a type checking error *)
Fail Compute add_two_even (exist _ 1 eq_refl).
(* The next command succeeds *)
Compute add_two_even (exist _ 4 eq_refl).
exist构造函数包装带有x证明的值P x，从而产生子集类型{x | P x}的元素。对于任何eq_refl的值，x = x项都是x的证明。当n是具体数字时，Coq可以评估Nat.even n并确定eq_refl是否是Nat.even n = true的有效证明。当n为1时，Nat.even n = false，并且检查失败，导致出现第一条错误消息。 n为4时，检查成功。
n不是常数而是任意表达式时，情况变得更加复杂。证明Nat.even n = true可能需要详细的推理，且必须由用户指导。例如，我们知道Nat.even (n + n) = true对于n的任何值，但Coq却不知道。因此，要以add_two_even形式调用n + n，我们需要显示引理。
Lemma add_n_n_even n : Nat.even (n + n) = true.
Proof.
induction n as [|n IH]; trivial.
now simpl; rewrite <- plus_n_Sm, IH.
Qed.
Definition foo (n : nat) :=
add_two_even (exist _ (n + n) (add_n_n_even n)).
[有一些工具可以促进这种编程风格，例如equations plugin，但是Coq社区的普遍智慧是，对于诸如add_two_even之类的函数，应避免使用子集类型，因为这些约束不会显着简化有关该函数的属性。
您可以在Mathematical Components库中找到许多很好地使用子集类型的示例。例如，库使用子集类型来定义长度为n.-tuple T的列表的类型n和以'I_n为界的整数的类型n。这使我们可以定义一个总访问器函数tnth (t : n.-tuple T) (i : 'I_n) : T，该函数提取列表i的第t个元素。如果我们为任意列表和整数定义此访问器，则需要将默认值传递给函数以在索引超出范围时返回，或者更改函数的签名以使其返回类型为option T的值，从而指示该函数可能无法返回值。此更改使访问器功能的属性更难以陈述。例如，考虑eq_from_tnth引理，该引理说如果两个列表的所有元素都相等，则两个列表相等：
eq_from_tnth:
forall (n : nat) (T : Type) (t1 t2 : n.-tuple T),
(forall i : 'I_n, tnth t1 i = tnth t2 i) -> t1 = t2
关于任意列表的此引理的陈述变得更加复杂，因为我们需要额外的假设，即两个列表的大小相同。 （这里x0是默认值。）
eq_from_nth:
forall (T : Type) (x0 : T) (s1 s2 : list T),
size s1 = size s2 ->
(forall i : nat, i < size s1 -> nth x0 s1 i = nth x0 s2 i) -> s1 = s2