упрощение в dafny, доказать (a + b) / c == (a / c) + (b / c)

Question

Я пытаюсь доказать (a + b) / c == (a / c) + (b / c) в dafny.

Я пытался использовать вещественное для c, в основном 1 / c.Да, у Дафни были проблемы с действительными числами.

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.
    }

Я ожидал, что Дафни автоматически получит это, потому что это довольно просто, но, похоже, не понимает.

Answer 1

Лемма неверна.Действительно, предполагая, что это правда, Дафни сможет доказать ложность.

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

Возможно, вы хотите работать с действительными числами вместо натуральных чисел?