Dafny定义自然数代数类型运算及证明交换律结合律的验证问题

你需要先补全前置辅助引理，再修正现有引理的证明逻辑，具体修改如下：

前置依赖补全 #

你之前加法交换律中用到的Add1引理，以及加法结合律、乘法对加法的左分配律是证明乘法交换律、结合律的必要前提，先补全这部分代码：

// 加法单位元性质：0 + n = n
lemma Add1(n: Nat)
ensures add(Zero, n) == n
{} // 该性质可被Dafny自动验证，无需额外证明步骤

// 加法结合律：(a + b) + c = a + (b + c)
lemma AssocAdd(a: Nat, b: Nat, c: Nat)
ensures add(add(a,b), c) == add(a, add(b,c))
decreases a
{
    match a
    case Zero => {}
    case Succ(a') => AssocAdd(a', b, c);
}

// 乘法对加法的左分配律：a*(b + c) = a*b + a*c
lemma MultDistribLeft(a: Nat, b: Nat, c: Nat)
ensures multiply(a, add(b,c)) == add(multiply(a,b), multiply(a,c))
decreases c
{
    match c
    case Zero => {}
    case Succ(c') => {
        MultDistribLeft(a,b,c');
        AssocAdd(a, multiply(a,b), multiply(a,c'));
    }
}

修正单位元相关引理 #

你需要同时补全乘0的性质，作为交换律的基础分支case：

// 乘0性质：m * 0 = 0
lemma Multiply0(m: Nat)
ensures multiply(m, Zero) == Zero
{
    match m
    case Zero => {}
    case Succ(m') => Multiply0(m');
}

// 乘1性质：m * 1 = m
lemma Multiply1(m: Nat)
ensures multiply(m, Succ(Zero)) == m
decreases m
{
    match m
    case Zero => {}
    case Succ(m') => Multiply1(m');
}

修正乘法交换律证明 #

你之前的草稿只完成了case分支的结构，缺少归纳步骤的等式推导关联，需要显式调用前置引理打通逻辑：

lemma CommMult(m: Nat, n: Nat)
ensures multiply(m, n) == multiply(n, m)
decreases m
{
    match m
    case Zero => {
        Multiply0(n);
    }
    case Succ(Zero) => {
        Multiply1(n);
    }
    case Succ(m') => {
        CommMult(m', n);
        MultDistribLeft(n, m', Succ(Zero));
        CommAdd(n, multiply(m',n));
    }
}

乘法结合律实现 #

在上述引理的基础上，乘法结合律的证明代码如下：

lemma AssocMult(a: Nat, b: Nat, c: Nat)
ensures multiply(multiply(a,b), c) == multiply(a, multiply(b,c))
decreases c
{
    match c
    case Zero => {}
    case Succ(c') => {
        AssocMult(a,b,c');
        MultDistribLeft(a, multiply(b,c'), b);
        CommMult(multiply(a,b), c');
    }
}

内容的提问来源于stack exchange，提问作者Cezar Cobuz