如何在Dafny中证明正实数的a²≤b²c²蕴含a≤bc？

针对你提出的问题：验证非负实数下a² ≤ b²c²蕴含a ≤ bc的性质，Dafny无法自动证明实数版本，但可以通过反证法结合实数的有序域性质完成证明，且无需定义平方根函数。

可证明的引理实现（反证法版本） #

lemma powersVSsquares_reals(a: real, b: real, c: real)
  requires a >= 0.0 && b >= 0.0 && c >= 0.0
  ensures (a*a <= b*b*c*c) ==> (a <= b*c)
{
  // 先假设前提成立
  assume a*a <= b*b*c*c;
  // 反证：假设结论不成立，导出矛盾
  if !(a <= b*c) {
    // 非负实数的不等关系推导：a > bc（因为否定了a<=bc）
    assert a > b*c;
    // 非负数乘法保序：x > y ≥ 0 时，x² > y²
    assert a*a > (b*c)*(b*c);
    // 乘法交换律与结合律展开
    assert (b*c)*(b*c) == b*b*c*c;
    // 得到与前提矛盾的结论
    assert a*a > b*b*c*c;
    // 触发矛盾，证明原命题成立
    contradiction;
  }
}

思路说明 #

1. 利用反证法：假设前提a² ≤ b²c²成立，但结论a ≤ bc不成立（即a > bc）。
2. 依赖Dafny内置的实数公理：对于非负实数x和y，若x > y则x² > y²（乘法保序性）。
3. 通过展开(bc)²得到b²c²，推导出a² > b²c²，与前提直接矛盾，从而证明原命题的正确性。

另一种实现（直接推导版本） #

也可以用calc块明确展示等价推导关系，让Dafny自动验证每一步：

lemma powersVSsquares_reals_calc(a: real, b: real, c: real)
  requires a >= 0.0 && b >= 0.0 && c >= 0.0
  ensures (a*a <= b*b*c*c) ==> (a <= b*c)
{
  assume a*a <= b*b*c*c;
  let bc := b*c;
  // 非负实数下，x² ≤ y² 等价于 x ≤ y
  calc {
    a <= bc;
    ==> { a >= 0.0, bc >= 0.0 }
    a*a <= bc*bc;
    == { bc*bc == b*b*c*c }
    a*a <= b*b*c*c;
  }
}

这两个版本都完全依赖Dafny的内置实数理论，不需要额外定义平方根函数即可完成证明。

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