Dafny中一元数上<关系的性质证明问题

要证明这个命题，核心是给Dafny明确一元数上<关系的定义/约束——因为Dafny不会默认推导出自定义类型上序关系的逆保序性质，你需要通过归纳谓词或公理明确<的行为。

方案1：用归纳谓词定义< #

直接通过归纳定义<，让Dafny能自动展开推理：

// 定义一元数类型
datatype Nat = Z | S(pred: Nat)

// 归纳定义小于关系
predicate Less(x: Nat, y: Nat) {
  match x, y {
    // 0小于任何后继数
    case Z, S(_) => true
    // 后继数的小于关系等价于前驱的小于关系
    case S(x'), S(y') => Less(x', y')
    // 其他情况都不满足小于
    case _, _ => false
  }
}

// 启用中缀符号，方便书写
notation x < y := Less(x, y)

// 目标定理证明
theorem SuccLessImpliesLess(x: Nat, y: Nat)
  requires S(x) < S(y)
  ensures x < y
{
  // 展开S(x)<S(y)的定义，直接得到Less(x', y')即x<y
  unfold Less(S(x), S(y));
}

这个方案里，Less(S(x), S(y))的定义直接等价于Less(x, y)，展开后就能直接满足结论。

方案2：用公理约束<的性质 #

如果你的<是opaque谓词（比如不想暴露具体实现），可以通过公理明确逆保序的性质：

datatype Nat = Z | S(pred: Nat)

// 定义opaque的小于谓词
predicate {:opaque} Less(x: Nat, y: Nat)
notation x < y := Less(x, y)

// 公理1：0小于任何后继数
axiom LessZeroSucc(n: Nat): Z < S(n)
// 公理2：后继数的小于关系双向等价于前驱的小于关系
axiom LessSuccSucc(x: Nat, y: Nat): (S(x) < S(y)) <==> (x < y)
// 可选：补充其他必要公理（如反自反、传递性）
axiom LessNotRefl(n: Nat): !(n < n)
axiom LessTrans(x: Nat, y: Nat, z: Nat): x < y && y < z ==> x < z

// 目标定理证明
theorem SuccLessImpliesLess(x: Nat, y: Nat)
  requires S(x) < S(y)
  ensures x < y
{
  // 直接应用双向等价公理，从前提推导出结论
  apply LessSuccSucc(x, y);
}

问题根源 #

你之前卡壳的核心原因是：Dafny对自定义类型上的<没有默认语义，如果你只是泛泛声明了<但没约束它和构造函数S的关联，Dafny无法自动推导S(x)<S(y)和x<y的关系——必须明确告诉它这种逆保序的规则。

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