问题标签 [isabelle]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票
1 回答
199 浏览

isabelle - 以应用样式将产品/元组/对类型的变量拆分为其成员

假设我们正在使用一对类型('a × 'a)并为它定义一个fun模式匹配。

如果我现在有一个a_btype 变量,('a × 'a)我如何(a,b)在应用样式证明中将其替换为它的对表示。例如,显示以下引理的最佳方式是什么?我该如何test a_b c替换test (a,b) c

这是否也适用于假设中的对?

0 投票
2 回答
366 浏览

isabelle - 将部分定义提升为商类型

disj_union我想提升到商类型 ( ) 的集合上有一个部分定义的运算符 (下面natq)。从道德上讲,我认为这应该没问题,因为总是可以在等价类中找到定义了运算符 [*] 的一些代表。但是,我无法完成提升定义保留等价性的证明,因为disj_union只是部分定义。在下面的理论文件中,我提出了一种我找到的定义disj_union运算符的方法,但我不喜欢它,因为它具有很多功能,abs而且Rep我认为它很难使用(对吗?)。

使用 Isabelle 中的商来定义这种事情的好方法是什么?

[*] 这有点像如何只在绑定变量不冲突的条件下定义避免捕获替换;始终可以通过重命名为 alpha 等价类中的另一个代表来满足的条件。

0 投票
3 回答
106 浏览

theorem-proving - 有限有界量词的消除规则

我有以下目标:

我想将此目标分解为六个子目标P 0P 1P 2P 3和。这很容易做到。但是用于执行此操作的相关规则是什么?我问是因为我的实际目标看起来更像这样:P 4P 5apply autoauto

并且apply auto不会以同样的方式打破这个目标(它给了我

反而)。

0 投票
3 回答
546 浏览

rename - 为什么要重命名元通用量化变量以及如何防止它?

考虑以下愚蠢的例子

接下来我想使用strict_subset引理并替换A两者AB它会这样做,但是它将现有的重命名AAa,完全违背了引入引理的目的。

如果我使用派生引理strict_subset2,一切都会很好,所以我相信我的推理是合理的。

关键是大多数标准引理都是形式strict_subset而不是形式strict_subset2,伊莎贝尔的制造者不可能让我strict_subset2先自己制作,所以,我一定做错了什么。

我想明白为什么A要改名?我认为这与打字系统有关,因为我认为我还看到了只要类型完全正确,元通用量化就不是问题的例子。

另一个问题是我是否可以以A某种方式阻止重命名?

当然,很可能这两个问题实际上都与真正正确的答案无关,因为我对伊莎贝尔还是很陌生。

PS。是否也可以从 Isabelle 那里获得漂亮的符号?

0 投票
1 回答
426 浏览

isabelle - 部分函数与未指定的总函数

假设我有一套A ⊆ nat. 我想在 Isabelle 中建模一个函数f : A ⇒ Y。我可以使用任何一个:

  1. 偏函数,即 type 之一nat ⇒ Y option,或
  2. 一个总函数,即nat ⇒ Y未指定输入的类型之一不在A.

我想知道哪个是“更好”的选择。我看到几个因素:

  • “偏函数”方法更好,因为它更容易比较偏函数的相等性。也就是说,如果我想看看是否f等于另一个函数g : A ⇒ Y,那么我就说f = g。要比较未指定的总函数fg,我不得不说∀x ∈ A. f x = g x

  • “未指定的总函数”方法更好,因为我不必一直关心构造/解构option类型。例如,如果f是一个未指定的总函数,并且x ∈ A,那么我只能说f x,但如果f是一个部分函数,​​我不得不说(the ∘ f) x。再举一个例子,对部分函数进行函数组合比对总函数进行函数组合更棘手。

对于与此问题相关的具体实例,请考虑以下形式化简单图形的尝试。

图由一组节点、它们之间的边关系以及label每个节点的边关系组成。我们只关心位于 中的节点的标签V。那么,应该label是带有 的部分函数node ⇒ 'a optiondom label = V​​还是应该只是在 之外未指定的总函数V

0 投票
3 回答
984 浏览

isabelle - 如何查看 Isabelle 证明目标中的隐藏类型变量?

在 Isabelle 中,人们经常可以达到证明目标,其中中间类型的术语对证明的正确性至关重要。例如,考虑以下引理将nat42 转换为'a wordthen 再返回:

现在这个陈述的真假取决于 的类型of_nat 42:如果是32 word,那么这个陈述是真的,如果它是一个2 word,那么这个陈述是假的。

不幸的是,我似乎无法让 Isabelle 向我展示这种中间类型。

我尝试了以下方法:

  • declare [[show_types]]
  • declare [[show_sorts]]
  • local_setup {* Config.put show_all_types true *}

所有这些都只显示:

在紧要关头,可以这样做:

确实得到了原始转储term,但我希望有更好的方法。

有没有一种在证明目标中显示中间项类型的好方法?

0 投票
1 回答
240 浏览

code-generation - 如何用“未定义”常量证明代码正确性引理

鉴于我对代码生成有一个非常简单的定义。它仅针对某些情况定义,否则会引发运行时异常。

现在我想显示blubb正确。应该忽略抛出异常的情况(从我的角度来看,而不是从数学的角度来看)。但是,我最终得到了一个假设某个任意值Xundefined. 以下引理或多或少等同于子目标。我想显示False,因为我想忽略抛出异常(即undefined返回)的情况。

这是无法证明的。

显示可能引发异常或处理的函数正确性的最佳方法是什么undefined?这与这个问题有关。

0 投票
1 回答
216 浏览

scala - 列表上“不同”的更快代码

这个问题是指使用 Isabelle/HOL 定理证明器生成代码。

当我distinct在列表中导出函数的代码时

我得到以下代码

此代码具有二次运行时。有更快的版本吗?我想"~~/src/HOL/Library/Code_Char"在我的理论开始时导入字符串,并为列表设置有效的代码生成。一个更好的实现distinct是在 O(n log n) 中对列表进行排序并遍历列表一次。但我想一个人可以做得更好吗?

无论如何,是否有更快的实现distinct,也许还有其他Main可用的功能?

0 投票
3 回答
427 浏览

isabelle - “应用(规则)”或“证明”使用什么规则?

当我apply (rule)在应用脚本中使用时,通常会选择适当的规则。这同样适用proof于结构化证明。我在哪里可以了解/查找使用的规则的名称?

0 投票
1 回答
238 浏览

scala - 从程序和数据类型细化开始的教程

从 Isabelle/HOL 理论手册中阅读了代码生成。不过,我还是觉得有点失落。我在哪里需要类似的东西linorder?我如何使用例如红黑树来加快速度?locale在程序细化的上下文中如何使用?...

是否有一些教程可以开始细化?如果没有,是否有一些简短的、独立的、正确的示例?


我们可以开发一个例子吗?

让我们假设我们有A :: 'a set并且我们知道finite A。我们如何继续生成例如有效的代码a ∈ A

我们如何表达我们对finite A. 我们如何才能将数学理论(a ∈ A)与代码生成和优化分开?