dafny 中的化简，证明 (a+b) / c == (a/c) + (b/c)

Question

我试图用 dafny 证明 (a+b) / c == (a/c) + (b/c)。

我尝试对 c 使用实数，基本上是 1/c。不过，dafny 在实数方面遇到了麻烦。

lemma s(a:nat, b:nat, d:nat)
    requires d>0
    ensures (a+b) / d == (a/d) + (b/d)
    {
        //Nothing in here works I tried using a calc == block, but I'm not really sure where to go with it because it really seems basic.
    }

我希望 Dafny 会自动得到这个，因为它非常基础，但似乎无法理解。

Answer 1

引理不正确。事实上，假设它是真的，Dafny 就能证明它是假的。

lemma no()
ensures false
{
    s(1,1,2);
}

也许您想使用实数而不是自然数？