lean - 难以定义欧几里得空间的子集
问题描述
我正在使用Lean来尝试形式化欧几里得空间 (R^n) 子集的概念。
我尝试了以下方法:
import analysis.real
def repeated_prod : ℕ → Type → Type
| 0 s := empty
| 1 s := s
| (n + 1) s := prod s (repeated_prod n s)
structure euclidean_space (n : ℕ) : Type :=
(space : set (repeated_prod n ℝ))
def euclidean_subset (M : Type) := ∃ n : ℕ, (set M) ⊆ (euclidean_space.mk n).space
尝试输入英语:
- 实数 (R) 在mathlib的分析组件中定义。
- 我们需要将其推广到 k 维,所以我们想要 R 与其自身任意多次的笛卡尔积。
repeated_prod
允许一个人采用任意类型并多次应用笛卡尔积。euclidean_space
是 R 情况的特化。- 我们说,
euclidean_subset
如果存在某个欧几里得空间(注意:我试图避免提及维度,所以它是某个R^n。),它是集合 (M
) 的子集。
然而,这给出了错误:
euclidean.lean:11:52: error: failed to synthesize type class instance for
M : Type,
n : ℕ
⊢ has_subset Type
euclidean.lean:11:74: error: maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
虽然,我承认我不知道默认值trace.class_instances
是什么,但我将其设置为10000
,它花费了更长的时间,并且给出了相同的错误消息,导致我认为错误消息具有误导性。似乎找不到很多关于这种语言的信息,包括我收到的错误消息,任何解决此错误的帮助将不胜感激。
解决方案
您有两个编译错误,尽管其中一个是不可见的。首先,您不能以您尝试的方式创建欧几里得空间,使用mk
. 我建议暂时从结构更改为 def,因为您的结构只有一个字段:
def euclidean_space (n : ℕ) : Type := set (repeated_prod n ℝ)
那么维数 n 的欧几里得空间就是euclidean_space n
。
其次,类型与集合不同,这就是 Lean 找不到has_subset Type
. 在结构演算中,精益所基于的类型理论,在面向对象的编程意义上,类型实际上不能是其他类型的子类型——尽管您可以使用“子类型”和/或强制来模拟这一点。所以这就是我改变你的代码要做的事情 - 而不是euclidean_subset
谓词试图检查某物是否是一个子集,而是检查它是否是 a 的一个子euclidean space n
类型n
:
def euclidean_subset (M : Type) := ∃ (n : ℕ) (P : euclidean_space n → Prop), M = subtype P
推荐阅读
- python - 无法使用 rmtree 擦除目录,因为它正在被另一个进程使用
- julia - 如何使用多个数组图制作 GIF?
- php - 如何建立 Pervasive PDO PHP 连接
- python - 发送 CAN J1939 消息
- c# - 当应用程序是 32 位时构建自定义控件,现在我正在移动到 64 位,只有自定义控件不能放置
- java - Flutter:我正在使用从 git hub 克隆它的 Flutter 应用程序,当我尝试运行它时构建失败
- c# - 使用动态键将 json 反序列化为 C#
- r - 根据基数 R 中另一个向量的值生成一个包含重复值的向量
- php - 为什么我的表单没有提交数据来更新我的数据库?
- javascript - 使用 Slicknav 时,链接在移动菜单上不起作用