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

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

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

Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
1
0
134
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

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

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, потому что в противном случае он не может понять, что набор конечен.)

Спасибо за быстрый и комплексный ответ!

Andrici Cezar 05.06.2019 09:41

Есть идеи, как убрать /!\ No terms found to trigger on. для RangeSet?

Andrici Cezar 06.06.2019 13:28

@AndriciCezar Я отредактировал свой ответ, чтобы исправить предупреждение (и последующую ошибку).

James Wilcox 06.06.2019 19:37

Другие вопросы по теме