如何解决如何在 Isabelle/HOL 中表达数组?
我正在尝试表达数组,但不知道具体如何表达。例如,在以下玩具引理中,断言一系列数字的总和等于某些事物:
lemma " ∑ {x |x. x ∈ {0..(n::nat)} } = n*(n+1) div 2"
,对于给定的数组 A[i] = i,i = 0..n
,我该如何表达?
我尝试使用向量 (vec
) 来说明它失败
imports Complex_Main "~~/src/HOL/Analysis/Finite_Cartesian_Product"
如下:
lemma test_array:
fixes n::nat and A::"(nat,3) vec"
shows "∑ {A $ x |x. x ∈ {0..(3::nat)} } = 3*4 div 2"
首先,我不知道如何让 vec
接受关于其大小的参数 n
。其次,结论部分 "∑ {A $ x |x. x ∈ {0..(3::nat)} }
有一些类型错误。也许 vec
不是正确的解决方案。因此,这里的问题。
在 Isabelle 中,是否有任何(最好是标准的)方法来表示一个范围内的 A[i]
的数组 i
?
(澄清一下,我不需要像在编程中那样可以修改的命令式数组;我只需要大小事先已知但不固定为 3
之类的数学数组)。
解决方法
在不了解具体应用的情况下,很难在这里给出好的建议。
我认为最标准的方法是使用函数而不是数组。如果需要,您可以表示紧缩域外的值为零。但是,Isabelle 中无限对象的总和始终为零。
如果你真的需要有长度的东西:在你说的评论中,你想使用int
,但也许你的索引无论如何都是正数,你可以将它们转换为nat
,使其成为可能无论如何都要使用列表?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。