1

我正在使用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

尝试输入英语：

  1. 实数 (R) 在mathlib的分析组件中定义。
  2. 我们需要将其推广到 k 维，所以我们想要 R 与其自身任意多次的笛卡尔积。
  3. repeated_prod允许一个人采用任意类型并多次应用笛卡尔积。
  4. euclidean_space是 R 情况的特化。
  5. 我们说，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，它花费了更长的时间，并且给出了相同的错误消息，导致我认为错误消息具有误导性。似乎找不到很多关于这种语言的信息，包括我收到的错误消息，任何解决此错误的帮助将不胜感激。

4

1 回答 1

2

您有两个编译错误，尽管其中一个是不可见的。首先，您不能以您尝试的方式创建欧几里得空间，使用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
于 2018-10-04T08:35:08.140 回答