Индуктивная лемма Дафни: не может вывести постусловие индукционной гипотезы

Question

Я пытаюсь определить семантику маленького шага очень простого языка с помощью арифметических выражений (исходный код доступен здесь). Для простоты мы предполагаем, что язык допускает только литералы и унарный минус (-exp).

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

Я определил отношение e1 --> e2 указание, как выполнить шаг вычисления из выражения e1 получить выражение e2, Давайте просто для простоты предположим, что это соотношение всегда выполняется:

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

(Любое другое нетривиальное отношение также приведет к проблеме, которую я здесь опишу).

Теперь я определяю отношение e1 -->* e2 указав, что e1 может быть уменьшено до e2 после нуля один или несколько шагов вычисления (как в статье Р. Лейно об экстремальных предикатах, стр. 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));
    }
}    

Дафни не может доказать последнее утверждение, хотя оно должно следовать из заявления о постусловии StepStarContext(exp2, exp3), Если я прокомментирую, что утверждение Дафни может успешно доказать лемму (фактически, Дафни все еще может доказать это, когда его тело пусто), но я все еще заинтригован фактом, что он не может доказать это утверждение. Я что-то пропустил?

Я также получил лемму префикса, как описано в статье Лейно (см. Исходный код). Как ни странно, Дафни доказывает это утверждение не только в префиксной лемме, но и в индуктивной лемме. StepStarContext, Зачем?

Любая помощь будет оценена.

Дафни версия: 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));

Дафни дает добро.