Dafny.Докажите, что все значения из интервала появляются в seq - PullRequest
Новая
       36

Dafny.Докажите, что все значения из интервала появляются в seq

1 голос
/ 05 июня 2019

Я пытаюсь доказать следующую лемму.Это кажется тривиальным, но я не могу доказать это.Заранее спасибо! 

lemma test(x : seq<int>)
  // if the values from x are margined by an interval
  // the values are different
  // and the number of values equals the size of the interval
  // then all values from the interval appear in x

  requires forall i :: 0 <= i < |x| ==> 
    0 <= x[i] < |x|;

  requires forall i :: 0 <= i < |x| ==>
   forall i' :: 0 <= i' < |x| && i != i' ==>
     x[i] != x[i'];

  ensures forall v :: 0 <= v < |x| ==>
    exists i :: 0 <= i < |x| && x[i] == v;
{

}

https://rise4fun.com/Dafny/d8VK

1 Ответ

1 голос
/ 05 июня 2019

Вот один из способов сделать это, используя некоторые факты о множестве множеств. 

lemma test(x : seq<int>)
  // if the values from x are margined by an interval
  // the values are different
  // and the number of values equals the size of the interval
  // then all values from the interval appear in x

  requires forall i :: 0 <= i < |x| ==> 
    0 <= x[i] < |x|;

  requires forall i :: 0 <= i < |x| ==>
   forall i' :: 0 <= i' < |x| && i != i' ==>
     x[i] != x[i'];

  ensures forall v :: 0 <= v < |x| ==> v in x
{
    var L: set<int>, R: set<int> := {}, RangeSet(0, |x|);
    var i := 0;
    CardinalityRangeSet(0, |x|);
    while i < |x|
        invariant 0 <= i <= |x|
        invariant L == set j | 0 <= j < i :: x[j]
        invariant forall v | v in L :: v in x
        invariant forall v | 0 <= v < |x| :: v in L || v in R
        invariant |R| == |x| - i

    {
        L, R := L + {x[i]}, R - {x[i]};
        i := i + 1;
    }
}

predicate InRange(lo: int, hi: int, i: int)
{
    lo <= i < hi
}

function RangeSet(lo: int, hi: int): set<int>
{
    set i | lo <= i < hi && InRange(lo, hi, i)
}

lemma CardinalityRangeSet(lo: int, hi: int)
    decreases hi - lo
    ensures |RangeSet(lo, hi)| == if lo >= hi then 0 else hi - lo
{
    if lo < hi {
        assert RangeSet(lo, hi) == {lo} + RangeSet(lo + 1, hi);
        CardinalityRangeSet(lo + 1, hi);
    }
}

Я немного изменил вашу спецификацию, чтобы использовать синтаксис Дафни v in x, который эквивалентен тому, что вы написали, иДафни немного легче рассуждать.

Основная идея доказательства состоит в том, чтобы начать с диапазона R элементов 0..|x|, а затем итеративно удалить элементы x[i] из R и добавить ихдо L.Это сохраняет инвариант, что каждое число в диапазоне 0..|x| находится в L или R, в то время как количество элементов R уменьшается на каждой итерации.Таким образом, в конце цикла R пуст, поэтому каждое число в диапазоне должно быть в L, и, следовательно, в x.

я также использовал одну вспомогательную лемму, доказанную индукцией кпокажите, что RangeSet имеет ожидаемый размер.

(Отредактировано, чтобы избавиться от предупреждения "Не найдено терминов, запускающих" в RangeSet. Введение предиката InRange дает ему возможность срабатывать, новам все еще нужно включить явный диапазон в RangeSet, потому что иначе он не может понять, что множество конечно.)

...