- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
根据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 在线中)。也许有些事情发生了变化。
问题:
问题1。为什么?
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)
时,我们有这样的东西:
Hyp:p(k-1) ==> q(k-1)
Tesis:p(k) ==> q(k)
但这证明了:
(p(k-1) ==> q(k-1) && p(k)) ==> q(k)
Q3.我的方法有意义吗?我们如何在 dafny 中进行这种归纳?
最佳答案
我不知道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];
}
}
关于theorem-proving - 不同的 "sorted"谓词在 Dafny 中应该是等效的,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/48331442/
考虑以下片段: import Data.List %default total x : Elem 1 [1, 2] x = Here type : Type type = Elem 1 [1, 2]
我有以下目标: ∀x ∈ {0,1,2,3,4,5}. P x 我想将这个目标分解为六个子目标 P 0、P 1、P 2、P 3、P 4 和 P 5。这可以通过 apply auto 轻松完成。但是 a
我有以下目标: ∀x ∈ {0,1,2,3,4,5}. P x 我想将这个目标分解为六个子目标 P 0、P 1、P 2、P 3、P 4 和 P 5。这可以通过 apply auto 轻松完成。但是 a
我是一个绝对的初学者,不是程序员,正在尝试使用 Logic and Proof 学习形式验证.我无法在精益中导入任何东西。 我将二进制文件的 tar 文件提取到 /tmp 然后执行 /tmp/lean
如果我理解正确(主要来自 applyTactic 函数的存在),则可以为 Idris 中的定理证明器编写自定义策略。我可以用什么(或哪里)的例子来学习如何做到这一点? 最佳答案 在 Idris 中有两
我正在尝试使用 Kowalski 图算法来求解定理证明。算法的描述位于 http://www.doc.ic.ac.uk/~rak/对于如何处理大事件却保持沉默它生成的重复子句的数量。我想知道是否有处理
Z3有一个prove()方法,可以证明两个公式的等价性。 但是,我找不到此prove() 方法的技术文档。 prove() 在幕后使用的“等价”的定义是什么?那是“部分等价”(在“回归验证”论文中提出
关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。 想改善这个问题吗?更新问题,使其成为 on-topic对于堆栈溢出。 7年前关闭。 Improve thi
任务。 假设我们给 Coq 如下定义: Inductive R2 : nat -> list nat -> Prop := | c1 : R2 0 [] | c2 : forall n l, R2 n
我(错误地)学习了关于验证并发程序的类(class),到目前为止我们已经介绍了这种称为“Owicki-Gries 方法”的方法。显然,可以通过将断言与每个语句相关联来证明有关程序的各种结果,并表明这些
我有 2 个公式 F1 和 F2。这两个公式共享大多数变量,除了一些具有不同名称的“临时”(或我称它们为“免费”)变量,这是出于某些原因。 现在我想证明 F1 == F2,但是 Z3 的 prove(
在 3D 渲染(或几何图形)中,在光栅化算法中,当您将三角形的顶点投影到屏幕上,然后查找像素是否与 2D 三角形重叠时,您通常需要查找深度或像素重叠的三角形的 z 坐标。一般来说,该方法包括计算三角形
我有 2 个公式 F1 和 F2。这两个公式共享大多数变量,除了一些具有不同名称的“临时”(或我称它们为“免费”)变量,这是出于某些原因。 现在我想证明 F1 == F2,但是 Z3 的 prove(
我有一个Map可能有相同类型的嵌套映射。每个嵌套映射都有一个指向外部映射的引用。 我定义了 findValue方法查看当前映射,如果没有找到任何内容,则转到其父级,依此类推,直到到达 null这是最外
我正在试验 CoNat 的定义取自 this paper作者:Jesper Cockx 和 Andreas Abel: open import Data.Bool open import Relati
我们的客户要求我们针对我们的 Web 应用程序(ASP.NET 4.5.2、Webforms)运行 OWASP ZAP 工具,我们不能在报告中有任何高优先级的发现。 我们已经完成分析,OWASP ZA
我有几个 .t文件夹中的文件。每个测试脚本都会启动自己的 Selenium 实例,因此会打开自己的浏览器。然后它们将它们的指令传递给单独模块中的页面对象。唉,页面对象是大多数测试断言发生的地方。 我使
我的部分测试套件依赖于 API URL。有时我想使用另一个 URL 运行我的测试。有没有办法将此参数传递给 prove,或者我是否需要编辑定义 API URL 的文件? 最佳答案 可以在测试程序中设置
如何证明 Cubical Agda 中的两件事不相等? (v2.6.1, Cubical repo 版本 acabbd9 ) 具体来说,这里是作为更高归纳类型的整数: {-# OPTIONS --sa
我正在尝试证明在Agda中的简单引理,我认为这是对的。 If a vector has more than two elements, taking its head following taking
我是一名优秀的程序员,十分优秀!