如何在 Isabelle/HOL 中表达数组？

编程问答 2022-05-29

问题描述

我正在尝试表达数组，但不知道具体如何表达。例如，在以下玩具引理中，断言一系列数字的总和等于某些事物：

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，使其成为可能无论如何都要使用列表？

isabelle