как доказать, что превращение множества в последовательность и обратно тождество в дафни

Хорошо, здесь много чего происходит. Прежде всего, я не уверен, собирались ли вы что-либо делать с помощью методов seq2Set и set2Seq, но они, похоже, не имеют отношения к вашей ошибке, поэтому я просто проигнорирую их и сосредоточусь на функциях.

Говоря о функциях, Danfy сообщает об ошибке в вашем определении fset2Seq, потому что s может быть пустым. В этом случае мы должны вернуть пустую последовательность, поэтому я изменил ваше определение на:

function fset2Seq(s:set<int>):seq<int> 
  decreases s
{
  if s == {} then []
  else 
    var y := Pick(s);
    [y] + fset2Seq(s - {y})
}

function Pick(s: set<int>): int
  requires s != {}
{
  var x :| x in s; x
}

который исправляет эту ошибку. Обратите внимание, что я также обернул оператор let-some-that :| в функцию с именем Pick. Это важно, но трудно объяснить. Просто доверься мне сейчас.

Теперь к лемме. Ваша лемма сформулирована немного странно, потому что она принимает параметр s, но тогда в предложении ensures не упоминается s. (Вместо этого там упоминается совершенно другая переменная, также называемая s, которая связана квантификатором forall!) Поэтому я изменил ее, чтобы избавиться от квантификатора, следующим образом:

lemma cycle(s:set<int>)
  ensures fseq2Set(fset2Seq(s)) == s

Затем я следую Моей Любимой Эвристике™ в верификации программы, которая состоит в том, что структура доказательства соответствует структуре программы. В данном случае речь идет о программе fseq2Set(fset2Seq(s)). Начиная с нашего ввода s, он сначала рекурсивно обрабатывается fset2Seq, а затем через понимание множества в fseq2Set. Итак, я ожидаю доказательства по индукции по s, которое следует структуре fset2Seq. Эта структура должна разветвляться в зависимости от того, пусто ли s, поэтому давайте сделаем это и в лемме:

lemma cycle(s:set<int>)
  ensures fseq2Set(fset2Seq(s)) == s
{
  if s == {} {
  } else {
  }
...

Dafny сообщает об ошибке в ветке else, но не в ветке if. Другими словами, Дафни доказал базовый случай, но ему нужна помощь с индуктивным случаем. Следующее, что делает fset2Seq(s), это звонит Pick(s). Давайте сделаем это тоже.

lemma cycle(s:set<int>)
  ensures fseq2Set(fset2Seq(s)) == s
{
  if s == {} {
  } else {
    var y := Pick(s);
...

Теперь мы знаем из его определения, что fset2Seq(s) вернет [y] + fset2Seq(s - {y}), поэтому мы можем скопировать и вставить наше предложение ensures и вручную подставить это выражение.

lemma cycle(s:set<int>)
  ensures fseq2Set(fset2Seq(s)) == s
{
  if s == {} {
  } else {
    var y := Pick(s);
    assert fseq2Set([y] + fset2Seq(s - {y})) == s;
...

Дафни сообщает об ошибке в этом утверждении, что неудивительно, поскольку это всего лишь слегка отредактированная версия пункта ensures, которую мы пытаемся доказать. Но важно то, что Dafny больше не сообщает об ошибке в самом предложении ensures. Другими словами, если мы сможем доказать это утверждение, мы закончим.

Глядя на это утверждение, мы видим, что fseq2Set применяется к двум спискам, добавленным вместе. И мы ожидаем, что это будет эквивалентно отдельному преобразованию двух списков в наборы, а затем их объединению. Мы могли бы доказать лемму на этот счет, или мы могли бы просто спросить Дафни, знает ли она уже этот факт, например:

lemma cycle(s:set<int>)
  ensures fseq2Set(fset2Seq(s)) == s
{
  if s == {} {
  } else {
    var y := Pick(s);
    assert fseq2Set([y] + fset2Seq(s - {y})) == fseq2Set([y]) + fseq2Set(fset2Seq(s - {y}));
    assert fseq2Set([y] + fset2Seq(s - {y})) == s;
...

(Обратите внимание, что новое добавленное утверждение перед последним.)

Теперь Дафни принимает нашу лемму. Мы можем немного подчистить, удалив базовый случай и финальное утверждение, которое было просто копией и вставкой версии нашего предложения обеспечить. Вот полированное доказательство.

lemma cycle(s:set<int>)
  ensures fseq2Set(fset2Seq(s)) == s
{
  if s != {} {
    var y := Pick(s);
    assert fseq2Set([y] + fset2Seq(s - {y})) == fseq2Set([y]) + fseq2Set(fset2Seq(s - {y}));
  }
}

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

Я не объяснил Pick. По сути, как правило, вы всегда должны заключать :| в функцию всякий раз, когда вы ее используете. Чтобы понять почему, см. сообщения опытного пользователя Dafny на перебор коллекции и функции над элементами множества. Также см. статью Растана Компиляция оператора эпсилон Гильберта.