自然数的基本运算(+/*)，并证明它们的交换性和结合性- Dafny

Question

学习Dafny我想在自然数(作为代数数据类型)上定义自然数的和和乘法，并证明它们的交换性和结合性。

我成功地做到了：

加法

datatype Nat = Zero | Succ(Pred: Nat)

function add(m: Nat, n: Nat) : Nat
decreases m
{
    match m
    case Zero => n
    case Succ(m') => Succ(add(m', n))
}

乘法

function multiply(m: Nat, n: Nat) : Nat
decreases n
{
    match n
    case Zero => Zero
    case Succ(Zero) => m
    case Succ(p) => add(m, multiply(m, p))
}

加法交换性

lemma CommAdd(m: Nat, n: Nat)
ensures add(m,n) == add(n, m)
{
    match m
    case Zero => Add1(n);
    case Succ(m') => CommAdd(m', n);
}

我被卡住的地方：

乘法交换性，结合性，这是我尝试过的，但没有得到“验证”。

// Neutral element
lemma Multiply1(m: Nat)
decreases m
// ensures multiply(m, Zero) == Zero
ensures multiply(m, Succ(Zero)) == m
{
//
}


// Commutativity of Multiplication - DRAFT, NOT VERIFIED
lemma CommMult(m: Nat, n: Nat)
ensures multiply(m, n) == multiply(n, m)
{
    match m
    case Zero => Zero
    case Succ(Zero) => Multiply1(n)
    case Succ(m') => CommMult(m', n)
}

Answer 1

注意，您对multiply模式的定义与第二个参数相匹配，而作为证明，CommMult模式与第一个参数相匹配。虽然可以使用任何一种方法来证明，但如果双方都同意，就会容易得多。

function multiply(m: Nat, n: Nat): Nat
  decreases m
{
  match m
    case Zero => Zero
    case Succ(Zero) => n
    case Succ(p) => add(n, multiply(p, n))
}
lemma CommMult(m: Nat, n: Nat)
  ensures multiply(m, n) == multiply(n, m)
{
  match m
    case Zero => {}
    case Succ(Zero) => Multiply1(n);
    case Succ(m') => CommMult(m', n);
}

现在Succ(Zero)分支不会抛出验证错误。进一步注意，它是与匹配表达式不同的匹配语句。在Zero情况下，dafny能够自动验证，原因语句为空。在Succ(Zero)情况下，引理Multiply1(n)足以证明后置条件。Succ(m')分支需要进一步的引理/语句来证明。CommMult(m', n)给出了multiply(m', n) == multiply(n, m')，但它也需要乘法对加法的分配性质来完成证明。

   m * n 
== S m' * n
== n + m' * n
{ using CommMulti property}
== n + n * m'
{ using distributive property }
== n * (1 + m')
== n * m

dafny以calc的形式支持这种计算风格的证明

lemma CommMult(m: Nat, n: Nat)
  ensures multiply(m, n) == multiply(n, m)
{
  match m
    case Zero => {}
    case Succ(Zero) => Multiply1(n);
    case Succ(m') => {
      calc {
        multiply(Succ(m'), n);
        // defintion of multiply
        add(n, multiply(m', n));
        { CommMult(m', n); }
        add(n, multiply(n, m'));
        { Multiply1(n); }
        add(multiply(n, Succ(Zero)), multiply(n, m'));
        // TODO use distributive law
      }
    }
}