这是我问题的一个最小示例。请考虑下列谓词，以及关于它们的引理：

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()

但我想写的证明在语法上是无效的：

old(AimpliesB());
oldBimpliesC();

因为Dafny的引理只是幽灵方法（ghost methods），它们不能在旧状态下被调用。但这个限制似乎阻止了Dafny证明某些显而易见的东西。

到目前为止，我唯一的变通办法是把 AimpliesB 重复一次，作为一个怪异、退化的两态引理，只引用旧状态。下面的代码可以验证：

twostate lemma {:axiom} oldAimpliesoldB()
    requires old(A())
    ensures old(B())

twostate lemma oldAimpliesC()
    requires old(A())
    ensures C()
{
    oldAimpliesoldB();
    oldBimpliesC();
}

但这感觉像是在重复编写代码，尤其当该引理并非公理且其主体需要被复制并混杂有 old 表达式时。有没有更好的办法？

解决方案

一种解决方案是创建一个具有 ()-值的函数，其契约与 AimpliesB 相同，可以在旧状态下被调用。这在调用点需要占位变量，代码仅略微显得混乱。

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

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

opaque ghost function fAimpliesB(): ()
    reads *
    requires A()
    ensures B()
{
    AimpliesB();
    ()
}

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

twostate lemma oldAimpliesC()
    requires old(A())
    ensures C()
{
    var _ := old(fAimpliesB());
    oldBimpliesC();
}