我试图用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自动获得它,因为它很基本,但似乎不了解。
引理不是正确的。确实,假设这是真的,Dafny就能证明是错误的。
lemma no()
ensures false
{
s(1,1,2);
}
也许您想使用实数而不是自然数?