不同的“排序”谓词在 Dafny 中应该是等价的

Question

根据Automating Induction with an 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];
{ }

但 Dafny 拒绝它（至少在我的桌面和 Dafny 在线中）。也许有些东西改变了。

问题：

Q1。为什么？

Q2. 真的需要对 j 或 i 和 j 进行归纳吗？我认为对 seq 长度的归纳应该足够了。

无论如何，我对以下内容更感兴趣：我想通过手动归纳来证明这一点，以供学习。在纸上，我认为对 seq 长度的归纳就足够了。现在我试图在 Dafny 上这样做：

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 中进行这种归纳？

Answer 1

我不知道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 子句。否则，Dafny 会抱怨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];
  }
}