Написание индуктивных лемм в dafny

Question

Я хотел бы доказать следующее в dafny:

function append(xs: seq<int>) : seq<int> {  
  if |xs| == 0 then []  
  else [xs[0]] + append(xs[1..])
}

method test(o:seq<int>, xs: seq<int>, i:int)
requires 0 <= i < |xs|
{  
  if o == append(xs[..i])
  {
    assert o + [xs[i]] == append(xs[..(i+1)]);
  }
}

Я считаю, что это требует написания индуктивного доказательства с использованием лемм, но я не уверен, как написать лемму. Он- лайн документ приводил примеры использования структурной индукции для содержимого последовательности, но я думаю, что в этом случае я думаю, что шаг индукции должен быть включен i? Я попытался написать один следующим образом:

lemma appendLemma (xs:seq<int>, o:seq<int>, i:int)
requires 0 <= i < |xs|
requires o == append(xs[..i])
ensures o + [xs[i]] == append(xs[..(i+1)])
{
  if i == 0
  {
    assert o + [xs[0]] == append(xs[..1]);
  }
  else
  {    
    appendLemma(xs, o, i);
    // what to do here?
  }
}

но он продолжает просить предложение о сокращении, которое в этом случае я не уверен, есть ли оно?

Answer 1

Вы сделаете индукцию по длине последовательности (как xs, так и o), а затем мне также придется уменьшиться, как вы можете видеть в моем доказательстве ниже. Таким образом, вы могли бы сказать, что вы делаете индукцию на я. Но что бы вы ни делали, внутренний вызов appendLemma должен быть связан с меньшими аргументами. Это представляет гипотезу индукции, см. Вот почему Дафни жалуется на прекращение.

Поскольку все, что мы знаем о функции append, это ее индуктивное определение, в виде головы / хвоста, мы должны следовать этому принципу при доказательстве appendLemma и применять индукцию к хвосту xs.

Мне нужна была дополнительная лемма (appendIsCopyLemma Это замечание Левента Эркока, приведенное выше, на самом деле является простой копией. Обратите внимание, что Dafny проверяет эту лемму без дополнительной помощи, но вы должны вызывать ее явно в доказательстве appendLemma (два раза).

Обратите внимание, что условие уменьшения, которое Дафни пропустил в исходном коде, теперь будет выводиться самим Дафни; аргументы рекурсивного вызова уже достаточно помогают.

// Verified by Dafny 2.2.0
// definition of append and test in the question above
lemma appendIsCopyLemma(xs: seq<int>)
  ensures xs == append(xs);
{ }

lemma appendLemma (xs:seq<int>, o:seq<int>, i:int)
  // decreases i; // Dafny can infer a decrease clause by itself
  requires 0 <= i < |xs|
  requires o == append(xs[..i])
  ensures o + [xs[i]] == append(xs[..(i+1)])
{
  if |xs| == 1 || i == 0
  {
    assert o + [xs[0]] == append(xs[..1]); //redundant
  }
  else
  {
    appendIsCopyLemma(xs[..i]);
    assert o[1..] == xs[1..][..i-1];
    appendLemma(xs[1..], o[1..], i-1);
    appendIsCopyLemma(xs[..i+1]);
    assert xs[..i+1] == append(xs[..i+1]);
  }
}