LEAN 之 Cauchy 序列（Cauchy Sequence）

直观感受（Intuition） 

        Cauchy 序列（Cauchy Sequence）是指，当一个序列 (x₀, x₁, ...) 在它一直往后延伸时，它的元素越靠越近，那么，该序列是 Cauchy 序列（Cauchy Sequence）。

        Cauchy 序列（Cauchy Sequence）有可能最终收敛（Converges）于一个值，也有可能一直缩小下去，而收敛值不存在。

        那么，可以通过使用Cauchy序列的概念，去判断一个度量空间（Metric space）是否完备的（Complete），即没有漏洞（no holes）。

        度量空间（Metric space）是指一个集合，其中任意两元素都可以计算它们的距离。因此，度量空间也记为，（M，d: M × M → ℝ），S指的是其集合，d指的是集合里任二元素的距离计算函数。

        在一个度量空间（M，d: M × M → ℝ）中，其所有的Cauchy 序列（Cauchy Sequence）都收敛于该空间中的一个值，那么该度量空间是完备的（Complete）。

在LEAN中的形式化（Formalization in LEAN）

        如下图：

        其中，

        1. f : ℕ → β，指的是序列。即，通过 f : ℕ → β，可以生成一系列的值，即，序列中的每一个元素。

        2. 要求了 类型 β 具备 代数结构 Ring，以支持减法操作。

        3. abv : β → α 函数，用于计算类型 β的值的绝对值的，即 absolute value。

        4. 要求了，类型 α 具备 线性有序域的结构，以支持大小的比较，及相关算术运算。

        5. Type*，意思是，类型宇宙中，除最底层Prop外的任意层次。

        那么，回到，命题： ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - f i) < ε 。

        即，给定任意大于0的 ε，存在一个自然数 i，（i, j for index），对于所有大于等于 i 的索引 j，有，索引值 f j 与 索引值 f i 的差的绝对值，即 两索引值的距离，小于 ε 。

        也就是说，无论给定的距离多小，都存在一个索引，使得在那索引之后的索引值间的距离，小于给定的距离。以此，来表达当序列在往后申延时，其元素越靠越近，也就是 Cauchy 序列（Cauchy Sequence）的要求。

        因此，IsCauSeq，是对于序列  f : ℕ → β，是否为 Cauchy 序列（Cauchy Sequence）的判断。

        基于 IsCauSeq 的判断，可以定义 Cauchy 序列，如下图：

        这里，需要注意的是，CauSeq 是一个子类型，其原类型是 f : ℕ → β。

        也就是说，CauSeq 的元素，是类型  f : ℕ → β 中，满足 IsCauSeq abv f 的元素。

        而，类型  f : ℕ → β 是表达一个序列，即 〈 fᵢ: i < ℕ 〉，因此，CauSeq 类型指代着Cauchy 序列（Cauchy Sequence）。

        更准确来说，CauSeq 是一个类型函数，给入对应的参数，返回一个类型。此处，Type _，指的是，有编译器根据 α 与 β 的类型，给出 返回类型的类型宇宙层次。

        也就是说， CauSeq abv: Type _ ，才是类型。

        既然CauSeq abv: Type _是类型，那么其元素间可定义等价关系（Equivalence），有了等价关系就可以作为类集合（Setoid）的存在。由此，在LEAN 中定义有

        其中，Cauchy 序列中，两Cauchy序列 f g : CauSeq β abv 相等，意味这 两Cauchy序列的差值趋向 0，即 LimZero。

         另，两 Cauchy序列 的差值是一个新的Cauchy序列，每个元素为对应两元素的差值，如下：

        那么，此时，就有了，Cauchy序列 是 类集合（Setoid）了。也就是，当一类型具备了元素间的等价关系。因此，可以定义 Cauchy序列 作为一个集合的存在，即定义了其元素及元素间的等价关系，如下图：

         实际上， Cauchy 也是类型函数，需要给入其参数，返回对应的类型。