Доказательство 100 заключенных и лампочка с Дафни

Рассмотрим стандартную стратегию решения проблемы 100 заключенных и проблемы с лампочкой. Здесь моя попытка смоделировать его в Dafny:

method strategy<T>(P: set<T>, Special: T) returns (count: int)
  requires |P| > 1 && Special in P
  ensures count == (|P| - 1)
  decreases *
{
  count := 0;
  var I := {};
  var S := {};
  var switch := false;

  while (count < (|P|-1)) 
    invariant count <= (|P|-1) 
    invariant count > 0 ==> Special in I
    invariant Special !in S && S < P && S <= I && I <= P 
    decreases *
  { 
    var c :| c in P;
    I := I + {c};

    if c == Special {
      if switch == true {
        switch := false;
        count := count + 1;
      }
    } else {
      if c !in S && switch == false {
        S := S + {c};
        switch := true;
      }
    }
  }  

  assert(I == P);  
}

Однако это не позволяет доказать, что в конце I == P. Зачем? Мне, вероятно, нужно еще больше укрепить инвариант цикла, но не могу себе представить, с чего начать...

Ответ 1

Здесь - это один из способов сделать это.

Мне пришлось добавить один концептуальный ключевой инвариант цикла и одну не-концептуально-ключевую-но-полезную-в-Дафни лемму.

Вам нужен циклический инвариант, который каким-то образом соединяет count с различными наборами. В противном случае тот факт, что count == |P| - 1 после цикла не очень полезен. Я решил использовать

if switch then |S| == count + 1 else |S| == count

который соединяет count с мощностью S. (Я думаю о S как о наборе заключенных, подсчитанных счетчиком.) Когда свет выключен, count обновляется (т.е. |S| == count). Но когда свет горит, мы ждем, когда Счетчик заметит и обновит счет, поэтому он отстает (т.е. |S| == count + 1).

С этим инвариантом цикла мы можем теперь утверждать, что I == P после цикла. Одним из ваших других инвариантов цикла мы уже знаем I <= P. Поэтому достаточно доказать P <= I. Предположим вместо этого, что I < P. Тогда имеем S < I < P. Но по условию выхода цикла мы также имеем |S| == |P| - 1. Это невозможно.

Единственная морщина заключается в том, что Дафни не может напрямую связывать отношения подмножества с отношениями мощности, поэтому мы должны помочь им. Я доказал лемму CardinalitySubset, которая, учитывая множества A и B такие, что A < B, следует, что |A| < |B|. Доказательство проводится индукцией по B и относительно просто. Вызов его соответствующими наборами завершает основное доказательство.

В стороне, я немного посмотрел, почему Dafny напрямую не связывает отношения подмножества с отношениями мощности. В аксиомах Дафна о множествах я нашел прокомментировал аксиому, связывающую мощность с подмножествами. (По общему признанию, эта аксиома связана с нестрогим отношением подмножества, но, раскомментируя эту аксиому, я смог получить версию доказательства, чтобы пройти без дополнительных лемм, поэтому этого было бы достаточно.) Отслеживая ее до почему аксиома была прокомментирована, похоже, что решатель слишком сильно использовал ее, даже если это не имело значения, что замедлило ситуацию.

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