написание индуктивных лемм в dafny - PullRequest
Новая
       19

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

0 голосов
/ 05 февраля 2019

Я бы хотел доказать следующее в 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?
  }
}

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

1 Ответ

0 голосов
/ 02 мая 2019

Вы сделаете индукцию по длине последовательности (как x, так и 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]);
  }
}
...