根据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)
Tesis:
p(k) ==> q(k)
但这证明了:
(p(k-1) ==> q(k-1) && p(k)) ==> q(k)
Q3。我的方法有意义吗?我们如何在dafny中进行这种归纳?
最佳答案
我不知道第一和第二季度的答案。但是,如果在归纳案例中添加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];
}
}