Dafny 归纳引理：无法推断归纳假设的后置条件

Question

我正在尝试用算术表达式定义一种非常简单的语言的小步语义（源代码可用 here）。为了简单起见，我们假设该语言只允许字面量和一元减号 (-exp).

datatype expression = Literal(int) | Minus(expression)

我定义了一个关系 e1 --> e2 指定如何从表达式 e1 执行计算步骤以获得表达式 e2。为简单起见，我们假设此关系始终成立：

predicate Step(exp: expression, exp': expression) { true }

（任何其他不平凡的关系也会导致我在这里描述的问题）。

现在我定义一个关系 e1 -->* e2 指定 e1 在零、一个或多个计算步骤后可以简化为 e2（如 R. Leino's paper on extreme predicates，第 11 页）：

inductive predicate StepStar(exp: expression, exp': expression) {
    (exp == exp')
    || (exists exp'': expression :: Step(exp, exp'') && StepStar(exp'', exp'))
}

我想证明 -->* 在上下文中是封闭的。也就是说，e -->* e' 意味着 Minus(e) -->* Minus(e')。这可以通过对 -->*:

的推导进行归纳证明

inductive lemma StepStarContext(exp1: expression, exp3: expression)
    requires StepStar(exp1, exp3)
    ensures StepStar(Minus(exp1), Minus(exp3)) 
{
    if (exp1 == exp3) {
        // Base case: zero steps.
    } else {
        // Inductive step.

        // We unfold the exp1 -->* exp3 relation into: exp1 --> exp2 -->* exp3.
        var exp2 :| Step(exp1, exp2) && StepStar(exp2, exp3);

        // Apply induction hypothesis on exp2 -->* exp3.
        StepStarContext(exp2, exp3);

        // ASSERTION VIOLATION: 
        // Why Minus(exp2) -->* Minus(exp3) cannot be proved?
        assert StepStar(Minus(exp2), Minus(exp3));
    }
}

Dafny 无法证明最后一个断言，尽管它应该来自后置条件应用 StepStarContext(exp2, exp3)。如果我注释掉 Dafny 可以成功证明引理的断言（事实上，当它的主体为空时，Dafny 仍然可以证明它），但我仍然对它无法证明这个断言这一事实感到好奇。我错过了什么吗？

我还推导出了 Leino 论文中描述的前缀引理（参见 source code）。奇怪的是，Dafny 不仅在前缀引理中证明了这个断言，而且在归纳引理 StepStarContext 中也证明了这一断言。为什么？

如有任何帮助，我们将不胜感激。

Dafny 版本: 2.1.1

Answer 1

我已经意识到归纳引理被脱糖如下：

lemma StepStarContext#[_k: ORDINAL](exp1: expression, exp3: expression)
  requires StepStar#[_k](exp1, exp3)
  ensures StepStar(Minus(exp1), Minus(exp3)) 
{
  if (exp1 == exp3) {
     ...
  } else {
    ...
    // Apply induction hypothesis on exp2 -->* exp3.
    StepStarContext(exp2, exp3);

    // ASSERTION VIOLATION: 
    assert StepStar#[_k - 1](Minus(exp2), Minus(exp3));
  }
}

基本上，未满足的断言要求 exp2 -->* exp3 的长度为 _k - 1，但这不符合归纳假设，因为引理的结论是 Minus(exp1) --> Minus(exp3) 对于 一些推导长度 。因此，在归纳假设中，我们不能期望 exp2 -->* exp3 的长度为 _k - 1.

修正断言后，

assert exists k' :: StepStar#[k'](Minus(exp2), Minus(exp3));

Dafny 同意了。

Dafny 归纳引理：无法推断归纳假设的后置条件

Dafny inductive lemma: cannot infer postcondition of induction hypothesis

induction

dafny