Coq使用Program定义时Obligation信息丢失的原因与解决办法

• Program处理{x : T | P x}形式的子集类型时，默认仅提取类型对应的载体值（你示例中就是两个自然数），不会自动将子集关联的性质假设加入Obligation的证明上下文。
• 你定义中传入的两个参数k1、k2本身都携带j + j = n的约束性质，但Program生成证明目标时直接丢弃了这部分约束，仅保留了投影得到的自然数变量，自然缺少必要的证明前提。

这里提供两种常用的可行方案：

方案1：显式解构子集类型参数 #

在写定义时手动解构子集类型的载体和对应性质，解构得到的性质会自动保留在Obligation的上下文里：

Program Definition f {n : nat} (k1 k2 : {j : nat | j + j = n}) : {j : nat | j = n} :=
  let (j1, H1) := k1 in
  let (j2, H2) := k2 in
  j1 + j2.
Next Obligation.
(* 此时上下文已自动包含 H1: j1 + j1 = n、H2: j2 + j2 = n，目标为 j1 + j2 = n *)
lia. (* 用算术自动证明即可完成目标 *)
Defined.

方案2：开启Program保留相等性的开关 #

如果不想每次手动解构，可以开启Set Program Keep Equalities选项，让Program生成Obligation时自动保留所有子集类型的性质假设：

Set Program Keep Equalities.
Program Definition f {n : nat} (k1 k2 : {j : nat | j + j = n}) : {j : nat | j = n} := k1 + k2.
Next Obligation.
(* 此时上下文已自动携带两个参数对应的约束性质，直接证明即可 *)
lia.
Defined.

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