Coq中SumPairs归纳谓词的定理正确性验证与定义修正问题

问题诊断 #

你遇到的问题分为两个层面：

1. 语法层面：Coq完全支持多值的子集类型（Sigma类型），只是你提到的{n0 n1: nat | ...}写法不符合语法规范，并非Coq不支持这类需求。
2. 逻辑层面：你当前写的定理命题本身不符合你定义的SumPairs的语义：该命题要求对于任意二元组列表，都存在单个自然数n使得列表所有元素的左项总和等于右项总和，这显然是不成立的。比如你举的例子[(1,2),(3,4)]，左项总和为4、右项总和为6，不存在n满足SumPairs (n,n) l，因此这个命题本身是不可证明的。

修正方案 #

1. 正确的强规范写法 #

要返回左右总和两个值，有两种常用的合法写法：

• 直接用二元组作为子集类型的承载元素，和SumPairs的参数形式完全匹配，写法最简洁：

Theorem sumPairs_correct : forall (l:list (nat*nat)), { p : nat * nat | SumPairs p l }.

• 嵌套Sigma类型的写法，适合需要分开使用两个返回值的场景：

Theorem sumPairs_correct : forall (l:list (nat*nat)), { n0 : nat & { n1 : nat | SumPairs (n0, n1) l } }.

2. 对应证明实现 #

修正后的定理可以直接通过列表归纳完成证明，逻辑完全对齐SumPairs的归纳定义：

Proof.
  intros l. induction l as [| y l IH].
  - exists (0,0). apply sp_base.
  - destruct IH as [p IH_p]. exists (fst p + fst y, snd p + snd y). apply sp_step. exact IH_p.
Qed.

累加顺序说明 #

你给出的示例输入[(1,2),(3,4)]按当前SumPairs的定义，计算结果为(4,6)。如果你预期得到的是(3,7)，只需要调整sp_step构造子中的累加顺序即可，不需要修改定理结构。

内容的提问来源于stack exchange，提问作者Cris Teller