Различные отсортированные предикаты должны быть эквивалентны в Dafny.

Согласно Автоматизация индукции с помощью SMT Solver на Dafny должно работать следующее:

ghost method AdjacentImpliesTransitive(s: seq<int>)
requires ∀ i • 1 ≤ i < |s| ==> s[i-1] ≤ s[i];
ensures ∀ i,j {:induction j} • 0 ≤ i < j < |s| ==> s[i] ≤ s[j];
{ }

Но Дафни его отвергает (по крайней мере, у меня на рабочем столе и в Дафни онлайн). Может быть, что-то изменилось.

Вопросы:

Q1. Почему?

Q2. Действительно ли необходима индукция по j или по i и j? Я думаю, что индукции по длине seq должно быть достаточно.

Во всяком случае, меня больше интересует следующее: я хочу доказать это с помощью ручной индукции для обучения. На бумаге я думаю, что индукции по длине последовательности достаточно. Теперь я пытаюсь сделать это на Дафни:

lemma {:induction false} AdjacentImpliesTransitive(s: seq<int>)
   ensures forall i :: 0 <= i <= |s|-2 ==> s[i] <= s[i+1] ==> forall l, r :: 0 <= l < r <= |s|-1 ==> s[l] <= s[r]
   decreases s
{
   if |s| == 0
   { 
     //explicit calc proof, not neccesary
     calc {
        (forall i :: 0 <= i <= 0-2 ==> s[i] <= s[i+1]) ==> (forall l, r :: 0 <= l < r <= 0-1 ==> s[l] <= s[r]);
     ==
        (forall i :: false ==> s[i] <= s[i+1])  ==>  (forall l, r :: false ==> s[l] <= s[r]);
     ==
        true ==> true;
     == 
        true;
     }
   } 
   else if |s| == 1
   { 
     //trivial for dafny
   }  
   else {

     AdjacentImpliesTransitive(s[..|s|-1]);
     assert (forall i :: 0 <= i <= |s|-3 ==> s[i] <= s[i+1]) ==> (forall l, r :: 0 <= l < r <= |s|-2 ==> s[l] <= s[r]);
    //What??

   }
}

Я застрял на последнем случае. Я не знаю, как совместить расчетный стиль доказательства (как в базовом случае) с индуктивной аферой.

Может быть, это следствие, которое сложно. На бумаге («неформальное» доказательство), когда нам нужно доказать импликацию p(n) ==> q(n) по индукции, у нас было что-то вроде:

Хип: p(k-1) ==> q(k-1)

Тесис: p(k) ==> q(k)

Но тогда это доказывает:

(p(k-1) ==> q(k-1) && p(k)) ==> q(k)

Q3. Имеет ли смысл мой подход? Как мы можем сделать такую ​​индукцию в dafny?


theorem-proving induction dafny
person fulem    schedule 18.01.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я не знаю ответа на вопросы Q1 и Q2. Однако ваше доказательство индукции пройдет, если вы добавите assert s[|s|-2] <= s[|s|-1] в случае индукции (вам не нужно другое утверждение). Вот полное доказательство:

lemma {:induction false} AdjacentImpliesTransitive(s: seq<int>)
   requires forall i :: 0 <= i <= |s|-2 ==> s[i] <= s[i+1]
   ensures forall l, r :: 0 <= l < r <= |s|-1 ==> s[l] <= s[r]
   decreases s
{
   if |s| == 0
   { 
     //explicit calc proof, not neccesary
     calc {
        (forall i :: 0 <= i <= 0-2 ==> s[i] <= s[i+1]) ==> (forall l, r :: 0 <= l < r <= 0-1 ==> s[l] <= s[r]);
     ==
        (forall i :: false ==> s[i] <= s[i+1])  ==>  (forall l, r :: false ==> s[l] <= s[r]);
     ==
        true ==> true;
     == 
        true;
     }
   } 
   else if |s| == 1
   { 
     //trivial for dafny
   }  
   else {

     AdjacentImpliesTransitive(s[..|s|-1]);
     assert s[|s|-2] <= s[|s|-1];

   }
}

По какой-то причине мне пришлось разделить ваше предложение ensures на предложения requires и ensures. В противном случае Дафни жаловался на undeclared identifier: _t#0#0. Я понятия не имею, что это значит.

И, если это интересно, вот более короткое доказательство:

lemma AdjacentImpliesTransitive(s: seq<int>)
requires forall i | 1 <= i < |s| :: s[i-1] <= s[i]
ensures forall i,j | 0 <= i < j < |s| :: s[i] <= s[j]
decreases s
{
  if |s| < 2
  {
    assert forall i,j | 0 <= i < j < |s| :: s[i] <= s[j];
  } else {
    AdjacentImpliesTransitive(s[..|s|-1]);
    assert s[|s|-2] <= s[|s|-1];
  }
}
person Daniel Ricketts    schedule 03.10.2019