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

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

0 голосов
/ 08 июня 2018

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

1 Ответ

0 голосов
/ 17 июля 2018

Я понял, что индуктивная лемма обесценивается следующим образом: 

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

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

...