寻找适用于列表不同元素对的对称非自反归纳谓词

首先明确：Coq标准库中没有完全匹配你需求的现成归纳谓词。标准库的ForallPairs会包含(x,x)这类自反对，而ForallOrdPairs是为非对称关系设计的，都无法直接满足你要求的「列表中任意不同元素对(i1,j1)、(i2,j2)满足i1≠i2 ∧ j1≠j2」的约束。

不过你有两种可行方案：

方案1：基于标准库谓词改造 #

先定义你需要的核心关系：

Definition distinct_nat_pair (p1 p2 : nat * nat) : Prop :=
  let (i1, j1) := p1 in
  let (i2, j2) := p2 in
  i1 <> i2 /\ j1 <> j2.

然后利用ForallPairs，通过逻辑或排除自反情况（即允许x=x，要求所有x≠y的对满足上述关系）：

Definition all_distinct_nat_pairs (l : list (nat * nat)) : Prop :=
  ForallPairs (fun p1 p2 => p1 = p2 \/ distinct_nat_pair p1 p2) l.

这个定义的逻辑是：列表中所有元素对要么是同一个元素（自反情况），要么满足你要求的i、j都不相等的约束。

方案2：自定义归纳谓词 #

如果更追求直观性，直接自定义归纳谓词会更清晰，它天然保证只检查不同元素对：

Inductive all_distinct_nat_pairs : list (nat * nat) -> Prop :=
| adnp_nil : all_distinct_nat_pairs nil
| adnp_cons : forall p l,
    (forall q, q ∈ l -> distinct_nat_pair p q) ->
    all_distinct_nat_pairs l ->
    all_distinct_nat_pairs (p :: l).

验证示例 #

对于你提到的列表[(1,1),(1,1),(2,3)]：

• 当试图构造all_distinct_nat_pairs [(1,1),(1,1),(2,3)]时，第二个(1,1)加入列表[(1,1),(2,3)]时，无法满足「与列表中所有元素满足distinct_nat_pair」的条件（因为和第一个(1,1)的i、j都相等），因此该列表不满足谓词，符合你的预期。

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