Dafny无法证明旧状态相关真命题，求无冗余解决方案

在Dafny中，单状态引理无法直接通过old()修饰调用，导致需要重复编写双状态版本引理，造成代码冗余。以下是几种更优的解决方法：

方法一：状态参数化（推荐） #

将谓词和引理抽象为接受显式State参数的通用版本，同时支持单状态和双状态场景，彻底避免冗余。

// 用State参数显式指定谓词所属的状态
predicate A(s: State)
predicate B(s: State)
predicate C()

// 通用引理，适用于任意状态
lemma {:axiom} AimpliesB(s: State)
    requires A(s)
    ensures B(s)

twostate lemma {:axiom} oldBimpliesC()
    requires old(B(State))
    ensures C()

twostate lemma oldAimpliesC()
    requires old(A(State))
    ensures C()
{
    // 直接传入旧状态实例调用通用引理
    AimpliesB(old(State));
    oldBimpliesC();
}

单状态场景下使用时，直接传当前状态State即可，和原单状态引理效果一致：

lemma SingleStateExample()
    requires A(State)
    ensures B(State)
{
    AimpliesB(State);
}

方法二：幽灵变量捕获旧状态 #

对于非公理引理，可以通过幽灵变量和假设模拟旧状态下的引理调用，避免重复编写双状态版本：

predicate A() reads *
predicate B() reads *
predicate C()

lemma {:axiom} AimpliesB()
    requires A()
    ensures B()

twostate lemma {:axiom} oldBimpliesC()
    requires old(B())
    ensures C()

twostate lemma oldAimpliesC()
    requires old(A())
    ensures C()
{
    ghost var oldA := old(A());
    ghost var derivedOldB;

    // 在幽灵块中模拟旧状态环境
    ghost {
        assume oldA;          // 假设旧状态下A成立
        AimpliesB();          // 调用单状态引理，推导该环境下B成立
        derivedOldB := B();   // 捕获该环境下的B结果
    }

    assume old(derivedOldB);  // 将捕获的结果关联到实际旧状态
    oldBimpliesC();
}

方法三：直接逻辑推导 #

如果引理是公理性质的，可直接利用逻辑蕴涵让Dafny自动推导，无需显式调用引理：

twostate lemma oldAimpliesC()
    requires old(A())
    ensures C()
{
    // 借助AimpliesB公理，自动推导旧状态下B成立
    assert old(B()) {:by AimpliesB()};
    oldBimpliesC();
}

若Dafny无法自动触发推导，可通过{:by}注解指定依赖的公理引理，引导证明器完成推导。

内容的提问来源于stack exchange，提问作者Frank Seidl