问题标签 [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.
isabelle - 以应用样式将产品/元组/对类型的变量拆分为其成员
假设我们正在使用一对类型('a × 'a)
并为它定义一个fun
模式匹配。
如果我现在有一个a_b
type 变量,('a × 'a)
我如何(a,b)
在应用样式证明中将其替换为它的对表示。例如,显示以下引理的最佳方式是什么?我该如何test a_b c
替换test (a,b) c
?
这是否也适用于假设中的对?
isabelle - 将部分定义提升为商类型
disj_union
我想提升到商类型 ( ) 的集合上有一个部分定义的运算符 (下面natq
)。从道德上讲,我认为这应该没问题,因为总是可以在等价类中找到定义了运算符 [*] 的一些代表。但是,我无法完成提升定义保留等价性的证明,因为disj_union
只是部分定义。在下面的理论文件中,我提出了一种我找到的定义disj_union
运算符的方法,但我不喜欢它,因为它具有很多功能,abs
而且Rep
我认为它很难使用(对吗?)。
使用 Isabelle 中的商来定义这种事情的好方法是什么?
[*] 这有点像如何只在绑定变量不冲突的条件下定义避免捕获替换;始终可以通过重命名为 alpha 等价类中的另一个代表来满足的条件。
theorem-proving - 有限有界量词的消除规则
我有以下目标:
我想将此目标分解为六个子目标P 0
,P 1
,P 2
,P 3
和。这很容易做到。但是用于执行此操作的相关规则是什么?我问是因为我的实际目标看起来更像这样:P 4
P 5
apply auto
auto
并且apply auto
不会以同样的方式打破这个目标(它给了我
反而)。
rename - 为什么要重命名元通用量化变量以及如何防止它?
考虑以下愚蠢的例子
接下来我想使用strict_subset
引理并替换A
两者A
,B
它会这样做,但是它将现有的重命名A
为Aa
,完全违背了引入引理的目的。
如果我使用派生引理strict_subset2
,一切都会很好,所以我相信我的推理是合理的。
关键是大多数标准引理都是形式strict_subset
而不是形式strict_subset2
,伊莎贝尔的制造者不可能让我strict_subset2
先自己制作,所以,我一定做错了什么。
我想明白为什么A
要改名?我认为这与打字系统有关,因为我认为我还看到了只要类型完全正确,元通用量化就不是问题的例子。
另一个问题是我是否可以以A
某种方式阻止重命名?
当然,很可能这两个问题实际上都与真正正确的答案无关,因为我对伊莎贝尔还是很陌生。
PS。是否也可以从 Isabelle 那里获得漂亮的符号?
isabelle - 部分函数与未指定的总函数
假设我有一套A ⊆ nat
. 我想在 Isabelle 中建模一个函数f : A ⇒ Y
。我可以使用任何一个:
- 偏函数,即 type 之一
nat ⇒ Y option
,或 - 一个总函数,即
nat ⇒ Y
未指定输入的类型之一不在A
.
我想知道哪个是“更好”的选择。我看到几个因素:
“偏函数”方法更好,因为它更容易比较偏函数的相等性。也就是说,如果我想看看是否
f
等于另一个函数g : A ⇒ Y
,那么我就说f = g
。要比较未指定的总函数f
和g
,我不得不说∀x ∈ A. f x = g x
。“未指定的总函数”方法更好,因为我不必一直关心构造/解构
option
类型。例如,如果f
是一个未指定的总函数,并且x ∈ A
,那么我只能说f x
,但如果f
是一个部分函数,我不得不说(the ∘ f) x
。再举一个例子,对部分函数进行函数组合比对总函数进行函数组合更棘手。
对于与此问题相关的具体实例,请考虑以下形式化简单图形的尝试。
图由一组节点、它们之间的边关系以及label
每个节点的边关系组成。我们只关心位于 中的节点的标签V
。那么,应该label
是带有 的部分函数node ⇒ 'a option
,dom label = V
还是应该只是在 之外未指定的总函数V
?
isabelle - 如何查看 Isabelle 证明目标中的隐藏类型变量?
在 Isabelle 中,人们经常可以达到证明目标,其中中间类型的术语对证明的正确性至关重要。例如,考虑以下引理将nat
42 转换为'a word
then 再返回:
现在这个陈述的真假取决于 的类型of_nat 42
:如果是32 word
,那么这个陈述是真的,如果它是一个2 word
,那么这个陈述是假的。
不幸的是,我似乎无法让 Isabelle 向我展示这种中间类型。
我尝试了以下方法:
declare [[show_types]]
declare [[show_sorts]]
local_setup {* Config.put show_all_types true *}
所有这些都只显示:
在紧要关头,可以这样做:
确实得到了原始转储term
,但我希望有更好的方法。
有没有一种在证明目标中显示中间项类型的好方法?
code-generation - 如何用“未定义”常量证明代码正确性引理
鉴于我对代码生成有一个非常简单的定义。它仅针对某些情况定义,否则会引发运行时异常。
现在我想显示blubb
正确。应该忽略抛出异常的情况(从我的角度来看,而不是从数学的角度来看)。但是,我最终得到了一个假设某个任意值X
是undefined
. 以下引理或多或少等同于子目标。我想显示False
,因为我想忽略抛出异常(即undefined
返回)的情况。
这是无法证明的。
显示可能引发异常或处理的函数正确性的最佳方法是什么undefined
?这与这个问题有关。
scala - 列表上“不同”的更快代码
这个问题是指使用 Isabelle/HOL 定理证明器生成代码。
当我distinct
在列表中导出函数的代码时
我得到以下代码
此代码具有二次运行时。有更快的版本吗?我想"~~/src/HOL/Library/Code_Char"
在我的理论开始时导入字符串,并为列表设置有效的代码生成。一个更好的实现distinct
是在 O(n log n) 中对列表进行排序并遍历列表一次。但我想一个人可以做得更好吗?
无论如何,是否有更快的实现distinct
,也许还有其他Main
可用的功能?
isabelle - “应用(规则)”或“证明”使用什么规则?
当我apply (rule)
在应用脚本中使用时,通常会选择适当的规则。这同样适用proof
于结构化证明。我在哪里可以了解/查找使用的规则的名称?
scala - 从程序和数据类型细化开始的教程
我从 Isabelle/HOL 理论手册中阅读了代码生成。不过,我还是觉得有点失落。我在哪里需要类似的东西linorder
?我如何使用例如红黑树来加快速度?locale
在程序细化的上下文中如何使用?...
是否有一些教程可以开始细化?如果没有,是否有一些简短的、独立的、正确的示例?
我们可以开发一个例子吗?
让我们假设我们有A :: 'a set
并且我们知道finite A
。我们如何继续生成例如有效的代码a ∈ A
?
我们如何表达我们对finite A
. 我们如何才能将数学理论(a ∈ A
)与代码生成和优化分开?