LEAN 简介

GlimpseOfLean 项目的非官方文档，旨在为初学者提供一个快速入门指南。

这个仓库是为想快速了解 LEAN 的人提供一个入门介绍。目标是在2到3个小时内了解在 LEAN 中进行证明的样子。阅读 Introduction.lean 文件后，您应该阅读 Basics 文件夹中的解释和练习，并选择从 Topics 文件夹中的一个文件开始工作。当然，如果您有更多时间，您可以尝试该文件夹中的所有文件。

要使用 LEAN 进行工作，您可以在本地安装 LEAN，使用 Codespaces 或使用 Gitpod。

要使用 Codespaces，请确保已登录 Github，点击下面的按钮，选择 4-core，然后按下 Create codespace。几分钟后，一个带有 LEAN 的编辑器将在您的浏览器中打开。

Gitpod与 Codespaces 非常相似，请点击下面的按钮，按下 Continue 并等待几分钟。

要在本地安装 LEAN，请按照这里的说明进行操作。

如果您有更多时间，您还应阅读《LEAN中的数学》一书（链接）。

import GlimpseOfLean.Library.Basic

namespace Introduction

LEAN 教程简介

如果您使用的是小屏幕，可以按下 alt-Z（或option-Z）键来启用自动换行。

欢迎来到这个旨在在几个小时内让您对 LEAN 有所了解的教程。

首先让我们看一下一个 LEAN 证明的样子，暂时不需要理解其中的语法细节。您不需要在此文件中输入任何内容。

如果一切正常，您当前应该看到本文右侧一个名为“Lean Infoview”的面板，上面显示着“No info found.”之类的消息。这个面板将开始显示证明中的有趣内容。

首先让我们回顾两个微积分定义。

如果一个实数序列 u 收敛到 l ，则对于任意 ε > 0 ，存在一个 N ，使得对于所有 n ≥ N ，都满足 |uₙ - l| ≤ ε。我们将这个条件写作 seq_limit u l。

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

在上面的定义中，注意到序列 u 的第 n 项简单地表示为 u n。

类似地，在下一个定义中，f x 可以写作在纸上我们会写作 f(x)。还要注意，蕴含关系使用单箭头表示（稍后我们会解释原因）。

如果一个函数 f: ℝ → ℝ 在 x₀ 处连续，则对于任意 ε > 0 ，存在一个 δ > 0 ，使得对于所有 x ，只要 |x - x₀| ≤ δ ，就有 |f(x) - f(x₀)| ≤ ε。我们将这个条件写作 continuous_at f x₀。

def continuous_at (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε

现在我们声称，如果 f 在 x₀ 处连续，则它在 x₀ 处是顺序连续的：对于任意收敛到 x₀ 的序列 u ，序列 f ∘ u 收敛

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ) (hu : seq_limit u x₀) (hf : continuous_at f x₀) :
  seq_limit (f ∘ u) (f x₀) := by { -- 这里的 `by` 关键字标志着开始证明的地方
  -- 将光标放在这里，观察右侧的 Lean InfoView 面板。
  -- 在证明的过程中，根据需要将光标从一行移动到另一行，同时监视 InfoView 面板。

  -- 我们的目标是证明，对于任意正的 `ε` ，存在一个自然数 `N` ，使得对于任意自然数 `n` ，如果 `n ≥ N` ，则 `|f(u_n) - f(x₀)|` 至多为 `ε`。
  unfold seq_limit
  -- 取一个正的数 `ε`。
  intros ε hε
  -- 根据 `f` 在这个正的 `ε` 上的假设，我们得到一个正的 `δ` ，使得对于所有实数 `x` ，如果 `|x - x₀| ≤ δ` ，则 `|f(x) - f(x₀)| ≤ ε` (1)。
  obtain ⟨δ, δ_pos, Hf⟩ : ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε := hf ε hε
  -- 根据 `u` 在这个 `δ` 上的假设，我们得到一个自然数 `N` ，使得对于每个自然数 `n` ，如果 `n ≥ N` ，则 `|u_n - x₀| ≤ δ` (2)。
  obtain ⟨N, Hu⟩ : ∃ N, ∀ n ≥ N, |u n - x₀| ≤ δ := hu δ δ_pos
  -- 我们证明 `N` 是合适的。
  use N
  -- 取一个大于等于 `N` 的 `n` 。我们证明 `|f(u_n) - f(x₀)| ≤ ε`。
  intros n hn
  -- 根据 (1) 对 `u_n` 的应用，我们只需证明 `|u_n - x₀| ≤ δ`。
  apply Hf
  -- 这可以通过 (2) 的性质以及我们对 `n` 的假设得到。
  exact Hu n hn
  -- 证明结束！
  }

现在此证明已经结束，您可以使用面板左侧的文件浏览器打开文件Exercises > 01Rewriting.lean。

练习题

import GlimpseOfLean.Library.Basic
import Mathlib.Data.Complex.Exponential
open Real

计算

环算策略

在学习数学的过程中，我们遇到的最早的一种证明是通过计算来证明。这可能听起来不像是一种证明，但实际上这是在使用表达数字运算性质的引理。当然，我们通常不想显式地调用这些，所以 mathlib 有一个 ring 策略，专门处理通过应用所有交换环的性质而得出的等式证明。

example (a b c : ℝ) : (a * b) * c = b * (a * c) := by {
  ring
}

现在轮到你了，将下面的 "sorry" 替换为一个证据。在这个例子中，证明只是 ring。在你证明一些事情之后，你会看到一个小的 "No goals" 消息，这是你的证明已经完成的标志。

example (a b : ℝ) : (a+b)^2 = a^2 + 2*a*b + b^2 := by {
  sorry
}

在上述的第一个例子中，仔细看看 Lean 在哪里显示括号。 ring 策略当然知道乘法的结合律，但有时候理解二元操作真的是二元的以及类似 a*b*c 的表达式被 Lean 读作 (a*b)*c 是有用的，事实上这等于 a*(b*c) 是一个引理当需要的时候会被 ring 策略使用。

重写策略

让我们现在看看如何利用涉及数字的假设进行计算。这利用了等式的基本属性：如果两个数学对象 A 和 B 是相等的，那么在任何涉及 A 的陈述中，都可以用 B 来代替 A。这个操作被称为重写，而 Lean 的策略对应的命名为 rw。请仔细逐步理解下面的证明，并尝试理解正在发生的事情。

example (a b c d e : ℝ) (h : a = b + c) (h' : b = d - e) : a + e = d + c := by {
  rw [h]
  rw [h']
  ring
}

注意 rw 策略是用来改变当前目标的。在上述证明的第一行之后，新的目标是 b + c + e = d + c。因此，你可以把这第一步证明理解为："我想要证明，a + e = d + c，但是，由于假设 h 告诉我 a = b + c，我只需要证明 b + c + e = d + c 就足够了。"

实际上，我们可以在一条命令中做几个重写。

example (a b c d : ℝ) (h : a = b + c) (h' : b = d - e) : a + e = d + c := by {
  rw [h, h']
  ring
}

注意，将光标置于 h 和 h' 之间会显示中间的证明状态。

还需要注意的是，策略状态背景色的细微变化，绿色部分表示新的内容，红色部分表示即将改变的部分。

现在请你自己试试。注意 ring 依然可以进行计算，但它并不使用假设 h 和 h'。

example (a b c d : ℝ) (h : b = d + d) (h' : a = b + c) : a + b = c + 4 * d := by {
  sorry
}

使用引理进行重写

在前面的示例中，我们使用本地假设重写了目标。但我们也可以使用引理。例如，让我们证明一个关于指数的引理。由于 ring 只知道如何从环的公理中证明事物，它不知道如何处理指数。对于以下的引理，我们将两次使用引理 exp_add x y 进行重写，该引理证明了 exp(x+y) = exp(x) * exp(y)。

example (a b c : ℝ) : exp (a + b + c) = exp a * exp b * exp c := by {
  rw [exp_add (a + b) c]
  rw [exp_add a b]
}

请注意，在第二次 rw 之后，目标变为 exp a * exp b * exp c = exp a * exp b * exp c，Lean 会立即声明证明已经完成。

如果我们不提供引理的参数，Lean 将重写第一个匹配的子表达式。在我们的示例中，这已经足够好。有时需要更多的控制。

example (a b c : ℝ) : exp (a + b + c) = exp a * exp b * exp c := by {
  rw [exp_add, exp_add]
}

让我们做一个练习，你也需要使用 exp_sub x y : exp(x-y) = exp(x) / exp(y) 和 exp_zero : exp 0 = 1。

记住，a + b - c 代表的是 (a + b) - c。

你可以使用 ring 或者通过重写 mul_one x : x * 1 = x 来简化等式右侧的分母。

example (a b c : ℝ) : exp (a + b - c) = (exp a * exp b) / (exp c * exp 0) := by {
  sorry
}

从右至左进行重写

由于等式是对称的，我们也可以使用 ← ，将等式的右边替换为左边，如下例所示。

example (a b c : ℝ) (h : a = b + c) (h' : a + e = d + c) : b + c + e = d + c := by {
  rw [← h, h']
}

无论何时，只要你在 Lean 文件中看到你键盘上没有的符号，比如 ←，你都可以将鼠标光标放在其上方，通过工具提示学习如何输入它。对于 ← 这个符号，你可以通过输入 "\l "，也就是反斜杠-l-空格来输入。

注意，这种从右到左的重写都是关心你想要使用的等式的两边，而不是你想要证明的东西的两边。rw [← h] 将会用左边替换右边，因此它会在当前目标中寻找 b + c 并将其替换为 a。

example (a b c d : ℝ) (h : a = b + b) (h' : b = c) (h'' : a = d) : b + c = d := by {
  sorry
}

在局部假设中重写

我们也可以在局部上下文的假设中进行重写，例如使用 rw [exp_add x y] at h 来替换假设 h 中的 exp(x + y) 为 exp(x) * exp(y)。

exact 策略允许你给出显式的证明项来证明当前的目标。

example (a b c d : ℝ) (h : c = d*a - b) (h' : b = a*d) : c = 0 := by {
  rw [h'] at h
  ring at h
  -- Our assumption `h` is now exactly what we have to prove
  exact h
}

使用 calc 进行计算布局

上述例子所写的内容与我们在纸上写的内容相去甚远。让我们看看如何获得更自然的布局（同时也恢复使用 ring 而不是显式的引理调用）。
在下面的每个 := 之后，目标是证明与前面一行（或第一行的左边）相等。
通过将鼠标指针置于每个 by 后面并查看策略状态，仔细检查你是否理解了这一点。

example (a b c d : ℝ) (h : c = b*a - d) (h' : d = a*b) : c = 0 := by {
  calc
    c = b*a - d   := by rw [h]
    _ = b*a - a*b := by rw [h']
    _ = 0         := by ring
}

我们来使用 calc 做一些练习。

example (a b c : ℝ) (h : a = b + c) : exp (2 * a) = (exp b) ^ 2 * (exp c) ^ 2 := by {
  calc
    exp (2 * a) = exp (2 * (b + c))                 := by sorry
              _ = exp ((b + b) + (c + c))           := by sorry
              _ = exp (b + b) * exp (c + c)         := by sorry
              _ = (exp b * exp b) * (exp c * exp c) := by sorry
              _ = (exp b) ^ 2 * (exp c)^2           := by sorry
}

从实际角度来看，在编写这样的证明时，有时候采取以下操作会很方便：

通过在 Lean 信息视图面板的右上角点击暂停图标按钮，暂停 VScode 中的策略状态视图更新。
编写完整的计算过程，每行结束时用“:= ?_”。
通过点击播放图标按钮恢复策略状态更新，并填充证明。

下划线应放在 calc 下面的第一行的左手边的部分下面。将等号和 := 对齐并不是必要的，但会显得整洁。

example (a b c d : ℝ) (h : c = d*a + b) (h' : b = a*d) : c = 2*a*d := by {
  sorry
}

恭喜你，这是你的第一个练习文件的结束！你已经看到了 Lean 证明的格式以及学习了以下策略：

ring
rw
exact
calc

import GlimpseOfLean.Library.Basic

含义

使用含义

Lean通过符号 → 表示含义，而非 ⇒ ，因为它将 P → Q 的证明视为一个函数，它可以将任何 P 的证明发送给 Q 的证明（如果你看不清→和⇒的区别，请增大字体大小）。

例如，给定一个实数 a ，引理 sq_pos_of_pos 声称 0 < a → 0 < a^2 所以下面的证明应用了 "函数" sq_pos_of_pos 到假设 ha。

example (a : ℝ) (ha : 0 < a) : 0 < a^2 := by {
  exact sq_pos_of_pos ha
}

上述证明是一个直接证明：我们已知 0 < a 并将这个事实用于推理。我们也可以使用 apply 策略进行反向推理。

example (a : ℝ) (ha : 0 < a) : 0 < (a^2)^2 := by {
  apply sq_pos_of_pos -- Thanks to `sq_pos_of_pos`, it suffices to prove `0 < a^2`
  apply sq_pos_of_pos -- Thanks to `sq_pos_of_pos`, it suffices to prove `0 < a`
  exact ha -- this is exactly our assumption `ha`.
}

尝试使用引理 add_pos : 0 < x → 0 < y → 0 < x + y 来完成下一个练习。注意，在你 apply add_pos 之后，你将会产生两个目标，你需要一个个去证明。

example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : 0 < a^2 + b^2 := by {
  sorry
}

你也可以使用向前推理的方式，使用 have 策略来进行证明。为了声明一个中间语句，我们使用：

have my_name : my_statement

此操作会引发一个新目标的出现：证明该语句。证明需要以一个中心点 ·（使用 \.输入）开始，且应对其进行缩进。在证明完成后，该语句将以 my_name 的名字变得可用。

example (a : ℝ) (ha : 0 < a) : 0 < (a^2)^2 := by {
  have h2 : 0 < a^2      -- we declare `0 < a^2` as a subgoal
  · apply sq_pos_of_pos  -- we start proving the subgoal
    exact ha             -- this line is indented, so part of the proof of the subgoal
  exact sq_pos_of_pos h2 -- we finished the subgoal, and now we prove the main goal using it.
}

现在使用前向推理证明之前的引理。

example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : 0 < a^2 + b^2 := by {
  sorry
}

证明推论

为了证明一个推论，我们需要假设前提并证明结论。这是使用 intro 策略完成的。秘密地，上述练习是证明推论 a > 0 → (a^2)^2 > 0 ，但是前提已经为我们介绍了。

example (a : ℝ) : a > 0 → b > 0 → a + b > 0 := by {
  intro ha hb -- You can choose any names here
  exact add_pos ha hb
}

现在，我们证明以下的命题逻辑简单陈述。请注意，p → q → r 意味着 p → (q → r)。

example (p q r : Prop) : (p → q) → (p → q → r) → p → r := by {
  sorry
}

等价

使用等价关系重写陈述

在上一个文件中，我们看到了如何使用等式进行重写。用数学语句进行的类似操作是使用等价关系进行重写。这也是使用 rw 策略完成的。 Lean 使用 ↔ 代替 ⇔ 来表示等价（如果看不清区别，请增大字体大小）。

在以下练习中，我们将使用以下引理：

sub_nonneg : 0 ≤ y - x ↔ x ≤ y

example {a b c : ℝ} : c + a ≤ c + b ↔ a ≤ b := by {
  rw [← sub_nonneg]
  have key : (c + b) - (c + a) = b - a -- Here we introduce an intermediate statement named key
  · ring   -- and prove it after a `·`
  rw [key] -- we can now use `key`. This `rw` uses an equality result, not an equivalence
  rw [sub_nonneg] -- and switch back to reach the tautology a ≤ b ↔ a ≤ b
}

我们来证明一个变种

example {a b : ℝ} (c : ℝ) : a + c ≤ b + c ↔ a ≤ b := by {
  sorry
}

上述引理已经存在于数学库中，名为 add_le_add_iff_right ：

add_le_add_iff_right (c : ℝ) : a + c ≤ b + c ↔ a ≤ b

这可以理解为：“ add_le_add_iff_right 是一个函数，它以一个实数 c 作为输入，并将输出 a + c ≤ b + c ↔ a ≤ b 的证明”。这里有一个使用这个引理的例子。

example {a b : ℝ}  (ha : 0 ≤ a) : b ≤ a + b := by {
  calc
    b = 0 + b := by ring
    _ ≤ a + b := by { rw [add_le_add_iff_right b] ; exact ha  }
}

将等价关系作为一对蕴含关系使用

在以上证明的第二行里，我们有点傻：我们使用命题重写来将目标简化为我们的假设 ha，但更自然的做法是将等价关系看作双向蕴含关系。我们可以访问等价关系 h : P ↔ Q 的两个蕴含 h.1 : P → Q 和 h.2 : Q → P。这允许我们将上述证明重写为：

example {a b : ℝ}  (ha : 0 ≤ a) : b ≤ a + b := by {
  calc
    b = 0 + b := by ring
    _ ≤ a + b := by exact (add_le_add_iff_right b).2 ha
}

让我们用 add_le_add_iff_left a : a + b ≤ a + c ↔ b ≤ c 进行一种变体。

Let's try it.

proof

import data.int.basic

theorem add_left_cancel {a b c : ℕ} :
  a + b = a + c ↔ b = c :=
begin
  rw nat.add_comm a b,
  rw nat.add_comm a c,
  apply add_right_cancel,
end

... And the result:

Lean check passed!

然后试试看。

证明

import data.int.basic

theorem add_left_cancel {a b c : ℕ} :
  a + b = a + c ↔ b = c :=
begin
  rw nat.add_comm a b,
  rw nat.add_comm a c,
  apply add_right_cancel,
end

... 结果如下：

Lean check 通过！

example (a b : ℝ) (hb : 0 ≤ b) : a ≤ a + b := by {
  sorry
}

证明等价

为了证明一个等价，你可以像处理等式一样，使用 rw 直到目标变成恒等式 P ↔ P。

你也可以分别证明这两个含义，使用 constructor 策略。

以下是一个例子。

example (a b : ℝ) : (a-b)*(a+b) = 0 ↔ a^2 = b^2 := by {
  constructor
  · intro h
    calc
      a ^ 2 = b^2 + (a - b) * (a + b)  := by ring
          _ = b^2 + 0                  := by rw [h]
          _ = b^2                      := by ring
  · intro h
    calc
      (a-b)*(a+b) = a^2 - b^2  := by ring
                _ = b^2 - b^2  := by rw [h]
                _ = 0          := by ring
  }

你可以在这个练习中自己试试。

example (a b : ℝ) : a = b ↔ b - a = 0 := by {
  sorry
}

这是本文件的结尾，你学习了如何处理蕴含关系和等价关系。你学习了以下策略：

intro
apply
have
constructor

import GlimpseOfLean.Library.Basic
import Mathlib.Topology.Algebra.Order.IntermediateValue
import Mathlib.Topology.Instances.Real

open Function

namespace Forall

通用量词

在这个文件中，我们将了解∀量词。

设P是一种类型X的谓词。这意味着对于每一个类型为X的数学对象x，我们得到一个数学语句P x。在 Lean 中，P x的类型为Prop。

Lean 将证明h为∀ x, P x视为一个函数，将任意的x : X送入证明h x中，证实P x。这已经解释了使用假设或引理的主要方法，该假设或引理开始于∀。

为了证明∀ x, P x，我们使用intro x来固定一个具有类型X的任意对象，并称之为x（intro代表 "介绍"）。

同时请注意，只要 Lean 能明白P的类型，我们在表达式∀ x, P x中不需要给出x的类型，因为它可以推断出x的类型。

让我们定义一个谓词来试验∀。

def even_fun (f : ℝ → ℝ) := ∀ x, f (-x) = f x

在下一个证明中，我们也利用机会介绍 unfold 策略，它只是展开定义。这里完全出于教学原因，Lean 并不需要那些 unfold 的调用。我们还将使用 rfl 策略，它证明了根据定义就为真的等式（在很强的意义上），代表 "反射性"。

example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by {
  -- Our assumption on that f is even means ∀ x, f (-x) = f x
  unfold even_fun at hf
  -- and the same for g
  unfold even_fun at hg
  -- We need to prove ∀ x, (f+g)(-x) = (f+g)(x)
  unfold even_fun
  -- Let x be any real number
  intro x
  -- and let's compute
  calc
    (f + g) (-x) = f (-x) + g (-x)  := by rfl
               _ = f x + g (-x)     := by rw [hf x]
               _ = f x + g x        := by rw [hg x]
               _ = (f + g) x        := by rfl
}

像 unfold，apply，exact，rfl 和 calc 这样的策略将会自动展开定义。你可以通过在上述示例中删除 unfold 行来测试它。

像 rw，ring 和 linarith 这样的策略通常不会展开目标中出现的定义。这就是为什么必须要有第一行计算行，尽管它的证明就是 rfl。在那行之前，rw hf x 找不到任何类似 f (-x) 的东西，因此会放弃。但最后一行并不必要，因为它只证明了一个根据定义就是真实的事情，并且没有后面的 rw。

此外，Lean 不需要被告知在重写之前应该将 hf 专用于 x，就像在第一个文件中一样。

还要记住，rw 可以采用一个表达式列表来用于重写。例如 rw [h₁, h₂, h₃] 等效于三行 rw [h₁]，rw [h₂] 和 rw [h₃]。请注意，当你使用这种语法阅读一个证明时，你可以在这些重写之间查看策略状态。你只需要将光标移到列表内部就可以。

因此，我们可以将上述证明压缩为：

example (f g : ℝ → ℝ) : even_fun f → even_fun g → even_fun (f + g) := by {
  intro hf hg x
  calc
    (f + g) (-x) = f (-x) + g (-x)  := by rfl
               _ = f x + g x        := by rw [hf, hg]
}

现在让我们开始练习。请记住，如果你需要学习如何输入一个 unicode 符号，你可以把你的鼠标光标放在符号上面并等待一秒钟。

example (f g : ℝ → ℝ) (hf : even_fun f) : even_fun (g ∘ f) := by {
  sorry
}

让我们使用更多的量词，并且尝试使用前向和后向推理。

在下面的定义中，注意如何将∀ x₁, ∀ x₂, ...缩写为∀ x₁ x₂, ...。

def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂

def non_increasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≥ f x₂

让我们首先非常明确地使用前向推理。

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) :
    non_decreasing (g ∘ f) := by {
  -- Let x₁ and x₂ be real numbers such that x₁ ≤ x₂
  intro x₁ x₂ h
  -- Since f is non-decreasing, f x₁ ≤ f x₂.
  have step₁ : f x₁ ≤ f x₂
  · exact hf x₁ x₂ h
  -- Since g is non-decreasing, we then get g (f x₁) ≤ g (f x₂).
  exact hg (f x₁) (f x₂) step₁
}

在上述证明中，注意到指定 hf x₁ x₂ h 中的 x₁ 和 x₂ 是多么不方便，因为它们可以从 hf 的类型中推断出来。我们本来可以写成 hf _ _ h ，Lean 就会自动填充由 _ 表示的空缺。对于最后一行，也有同样的问题。

对上述证明的一种可能的变种是使用 specialize 策略来替换 hf 为其对相关值的特化。

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) :
    non_decreasing (g ∘ f) := by {
  intro x₁ x₂ h
  specialize hf x₁ x₂ h
  exact hg (f x₁) (f x₂) hf
}

这种 specialize 策略主要用于探索，或者为在假设中进行重写做准备。人们通常可以通过使用直接涉及原始假设的更复杂的表达式来替换其使用，如下一种变体：

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) :
    non_decreasing (g ∘ f) := by {
  intro x₁ x₂ h
  exact hg (f x₁) (f x₂) (hf x₁ x₂ h)
}

让我们来看看这里的反向推理是什么样子的。像往常一样，我们使用 apply 并且享受 Lean 使用所谓的统一方法为我们专门化假设。

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) :
    non_decreasing (g ∘ f) := by {
  -- Let x₁ and x₂ be real numbers such that x₁ ≤ x₂
  intro x₁ x₂ h
  -- We need to prove (g ∘ f) x₁ ≤ (g ∘ f) x₂.
  -- Since g is non-decreasing, it suffices to prove f x₁ ≤ f x₂
  apply hg
  -- which follows from our assumption on f
  apply hf
  -- and on x₁ and x₂
  exact h
}

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_increasing g) :
    non_increasing (g ∘ f) := by {
  sorry
}

查找引理

Lean 的数学库包含许多有用的事实，记住所有这些事实是不切实际的。以下练习将教你两种此类技巧。

simp 将简化复杂的表达式。
apply? 将从库中找到引理。

使用 simp 来证明以下内容。注意 X : Set ℝ 表示 X 是一个只包含实数的集合。

example (x : ℝ) (X Y : Set ℝ) (hx : x ∈ X) : x ∈ (X ∩ Y) ∪ (X \ Y) := by {
  sorry
}

使用 apply? 来找出这个引理，即每个具有紧致支持的连续函数都具有全局最小值。

example (f : ℝ → ℝ) (hf : Continuous f) (h2f : HasCompactSupport f) : ∃ x, ∀ y, f x ≤ f y := by {
  sorry
}

这是这个文件的结束，你学习了如何处理通用量词。你学习了以下策略：

unfold
specialize
simp
apply?

你现在可以选择下一步要做什么。还有一个基本文件 04Exists 关于存在量词和连接词。你可以现在就处理，或者直接深入专业文件中。在后者的情况下，如果你在 ∃/∧ 遇到任何问题，你应该回到 04Exists 。

你可以从 Topics 文件夹中的专业文件开始。你可以选择

ClassicalPropositionalLogic（更简单，逻辑）如果你想学习如何在 Lean 中进行经典命题逻辑。
IntuitionisticPropositionalLogic（更难，逻辑）如果你想挑战更大并进行直觉主义命题逻辑。
SequenceLimit （更简单，数学）如果你想做一些初级微积分。对于这个文件，建议先处理 04Exists 。
GaloisAjunctions（更难，数学）如果你想有更多的抽象化并学习如何证明完全格之间的伴随性的事情。它以产品拓扑的构造及其普遍属性结束尽可能少地操作开放集。

import GlimpseOfLean.Library.Basic

open Function

合取

在此文件中，我们将学习如何处理合取（"逻辑与"）运算符和存在量词。

在 Lean 中，两个陈述 P 和 Q 的合取表示为 P ∧ Q，读作 "P and Q"。

我们可以类似于 ↔ 来使用合取：

如果 h : P ∧ Q 那么 h.1 : P 和 h.2 : Q。
为了证明 P ∧ Q，使用 constructor 策略。

此外，我们可以分解合取和等价。

如果 h : P ∧ Q，策略 rcases h with ⟨hP, hQ⟩ 会给出两个新的假设 hP : P 和 hQ : Q。
如果 h : P ↔ Q，策略 rcases h with ⟨hPQ, hQP⟩ 会给出两个新的假设 hPQ : P → Q 和 hQP : Q → P。

example (p q r s : Prop) (h : p → r) (h' : q → s) : p ∧ q → r ∧ s := by {
  intro hpq
  rcases hpq with ⟨hp, hq⟩
  constructor
  · exact h hp
  · exact h' hq
}

我们也可以在不使用构造函数策略的情况下证明一个并列关系，通过使用 ⟨/⟩ 括号收集两侧内容，所以上述的证明可以被重写为。

example (p q r s : Prop) (h : p → r) (h' : q → s) : p ∧ q → r ∧ s := by {
  intro hpq
  exact ⟨h hpq.1, h' hpq.2⟩
}

你可以在下一个练习中选择你自己的风格。

example (p q r : Prop) : (p → (q → r)) ↔ p ∧ q → r := by {
  sorry
}

当然，Lean 在证明这类逻辑恒等式方面并不需要任何帮助。这是 tauto 策略的工作，它能在命题逻辑中证明真实的陈述。

example (p q r : Prop) : (p → (q → r)) ↔ p ∧ q → r := by {
  tauto
}

存在量词

为了证明 ∃ x, P x ，我们提供某些 x₀ ，使用策略 use x₀ ，然后证明 P x₀ 。这个 x₀ 可以是来自局部环境的对象或者更复杂的表达式。在下面的例子中， use 后要检查的属性按照定义是正确的，所以证明到此结束。

example : ∃ n : ℕ, 8 = 2*n := by {
  use 4
}

为了使用 h : ∃ x, P x，我们使用 rcases 策略来固定一个有效的 x₀。

同样，h 可以直接来自本地上下文，也可以是更复杂的表达式。

example (n : ℕ) (h : ∃ k : ℕ, n = k + 1) : n > 0 := by {
  -- Let's fix k₀ such that n = k₀ + 1.
  rcases h with ⟨k₀, hk₀⟩
  -- It now suffices to prove k₀ + 1 > 0.
  rw [hk₀]
  -- and we have a lemma about this
  exact Nat.succ_pos k₀
}

接下来的习题将使用ℤ中的整除（注意 ∣ 符号，它不是 ASCII）。

根据定义，a ∣ b ↔ ∃ k, b = a*k，所以你可以使用 use 策略来证明 a ∣ b。

example (a b c : ℤ) (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c := by {
  sorry
}

我们现在可以开始结合量词，使用定义

Surjective (f : X → Y) := ∀ y, ∃ x, f x = y

这是 "映射的反向" 的定义。意思是对于所有的 y，都存在某个 x，使得 f 函数作用于 x 之后得到 y。

example (f g : ℝ → ℝ) (h : Surjective (g ∘ f)) : Surjective g := by {
  sorry
}

这是关于 ∃ 和 ∧ 的文件的结尾。你已经学到了以下技巧：

rcases
tauto
use

这是 基础 文件夹的结束。我们故意没有包括逻辑或运算符和所有关于否定的内容，以便你能尽快进入实际的数学内容。你现在可以从 主题 中选择一个文件。

请查看 03Forall 底部对可选项的描述。

抽象无意义 101：Galois 伴随

在这个文件中，我们将尝试最简单的伴随示例：完全格之间的 Galois 连接。尽管在 mathlib 中有很多关于这个主题的内容，但是在这里，我们会创建自己的版本进行练习。这篇文件构建了这些对象的基础理论，每个你在其中证明的引理都有名字，可以用来证明下一个引理。

namespace Tutorial

section InfSup
variable [PartialOrder X]

在本节中，X 是一个配备了偏序关系的类型。所以你可以访问以下引理：

le_rfl {a : X} : a ≤ a
le_trans {a b c : X} (h : a ≤ b) (h' : b ≤ c) : a ≤ c
le_antisymm {a b : X} (h : a ≤ b) (h' : b ≤ a) : a = b

大括号围绕的参数意味着这些参数是隐式的，Lean 将从上下文中推断出这些参数。

一个元素 x₀ 是集合 s 在 X 中的下确界，当且仅当 X 中的每个元素都是 s 的下界，并且它们都小于 x₀。

def isInf (s : Set X) (x₀ : X) :=
  ∀ x, x ∈ lowerBounds s ↔ x ≤ x₀

lemma isInf.lowerBound {s : Set X} {x₀ : X} (h : isInf s x₀) : x₀ ∈ lowerBounds s := by {
  sorry
}

一个集合最多只有一个下确界。

def isInf.eq {s : Set X} {x₀ x₁ : X} (hx₀ : isInf s x₀) (hx₁ : isInf s x₁) : x₀ = x₁ := by {
  sorry
}

一个元素 x₀ 是集合 s 在 X 中的上确界，当且仅当 X 中的每个元素都是 s 的下界，并且它们都小于 x₀。

def isSup (s : Set X) (x₀ : X) :=
  ∀ x, x ∈ upperBounds s ↔ x₀ ≤ x

下一条引理的证明是通过将 isInf.lowerBound 应用于配备了相反的顺序关系的 X 来完成的。你不需要精确地理解这是如何实现的，因为使用这个技巧的所有证明都将会提供。

lemma isSup.upperBound {s : Set X} {x₀ : X} (h : isSup s x₀) : x₀ ∈ upperBounds s :=
  isInf.lowerBound (X := OrderDual X) h

一个集合最多有一个上确界。

lemma isSup.eq {s : Set X} {x₀ x₁ : X} (hx₀ : isSup s x₀) (hx₁ : isSup s x₁) : x₀ = x₁ :=
  isInf.eq (X := OrderDual X) hx₀ hx₁

如果一个函数从 Set X 到 X ，并且它将每个集合映射到该集合的下确界，那么这个函数就被称为下确界函数。

def isInfFun (I : Set X → X) :=
  ∀ s : Set X, isInf s (I s)

一个从 Set X 到 X 的函数是一个 supremum 函数，如果它将每一个集合都映射到这个集合的 supremum。

def isSupFun (S : Set X → X) :=
  ∀ s : Set X, isSup s (S s)

下面的引理是这个文件中的第一个关键结果。如果 X 有一个下确界函数，那么它自动会有一个上确界函数。

lemma isSup_of_isInf {I : Set X → X} (h : isInfFun I) : isSupFun (fun s ↦ I (upperBounds s)) := by {
  sorry
}

当然，我们也有一种双重结果，可以从一个取最大值的功能中构造出一个取最小值的功能。

lemma isInf_of_isSup {S : Set X → X} (h : isSupFun S) : isInfFun (fun s ↦ S (lowerBounds s)) :=
  isSup_of_isInf (X := OrderDual X) h

我们现在准备好了这个文件的第一个主要定义：完全格。

Markdown 格式请保持，特殊格式前后带空格。

一个完全格是一种装备了偏序关系、最小值函数和最大值函数的类型。例如，用包含顺序、交集函数和并集函数装备的 X = Set Y 是一个完全格。

class CompleteLattice (X : Type) [PartialOrder X] where
  I : Set X → X
  I_isInf : isInfFun I
  S : Set X → X
  S_isSup : isSupFun S

将完全格 X 转换为对偶格。当使用上述的 OrderDual 技巧时， Lean 会自动采用这种构造。

注：完全格、对偶格和OrderDual都是数学上的专业术语。

instance (X : Type) [PartialOrder X] [CompleteLattice X] : CompleteLattice (OrderDual X) where
  I := CompleteLattice.S (X := X)
  I_isInf := CompleteLattice.S_isSup (X := X)
  S := CompleteLattice.I (X := X)
  S_isSup := CompleteLattice.I_isInf (X := X)

我们现在可以使用上述的第一个主要结果，基于一个部分有序类型上的下确界或上确界函数，来构建一个完全格。

从部分有序类型的下确界函数构建一个完全格结构。

本文描述了如何使用 Lean 定理证明器，通过下确界函数来构建在部分有序类型上的完全格结构。

我们从部分有序类型 (Partially Ordered Type) 开始，这是一个集合类型 Type，集合的元素具有反身性、传递性和反对称性。有一些操作符 ≤ 表示“小于或等于”，满足以下条件：

反身性：对于所有的 x，x ≤ x；
传递性：如果 x ≤ y 并且 y ≤ z，那么 x ≤ z；
反对称性：如果 x ≤ y 并且 y ≤ x，那么 x = y。

接下来，我们定义一个 inf 函数，它接收两个参数并返回一个结果，这个结果是参数集合的 下确界 （也称为 最小界 或下界）。

我们的目标是从 inf 函数出发，构建一个 完全格 结构。完全格是一个格结构，其中任何集合都有一个上确界和下确界。这意味着，我们需要定义两个函数 Sup 和 Inf，分别代表上确界和下确界。

Lean 定理证明的主要目标之一就是确保构建的完全格结构满足一些基本属性，如：

如果 x ≤ Sup S 对于集合 S 中的所有 x 都成立，那么 Sup S 是 S 的上确界；
如果 Inf S ≤ x 对于集合 S 中的所有 x 都成立，那么 Inf S 是 S 的下确界；

我们还需要证明一些其他属性，以确保 Sup 和 Inf 函数的行为与我们期望的行为一致。通过证明这些属性，我们可以确信我们的完全格结构是有效的，并且可以用于进一步的数理逻辑研究。

def CompleteLattice.mk_of_Inf {I : Set X → X} (h : isInfFun I) : CompleteLattice X where
 I := I
 I_isInf := h
 S := fun s ↦ I (upperBounds s)
 S_isSup := isSup_of_isInf h

从部分排序类型的上确界函数建立完全格构造。

定理声明

我们考虑一个部分排序类型 P ，并且给定一个函数 Sup : set P -> P，这个函数满足以下性质：

对于任何集合s， Sup s是s的一个上界。
对于任何集合s和任何x，如果 x是s的上界，那么Sup s <= x。

我们希望从这个 Sup 函数构造一个完全格complete lattice。

一种完全格应满足以下性质：

它是一个部分排序集。
对于每个集合，该集合的最小元素和最大元素存在（即完全格上的上确界和下确界函数是存在的）。

A lattice is a set L of elements that is ordered that, for any two elements x and y in L, the two elements have a unique supremum (also called the least upper bound) and a unique infimum (also called the greatest lower bound). In the Set we know as Boolean algebra, the supremum is the union of two sets and the infimum is their intersection.

一个格是一个元素集合 L ，该集合的元素排列有序，对于 L 中的任何两个元素 x 和 y ，存在一个唯一的上确界（也称为最小上界）和一个唯一的下确界（也称为最大下界）。在我们所知的作为布尔代数的 Set 中，上确界是两个集合的 并集 ，下确界是它们的 交集。

A complete lattice is a lattice that, additionally, has a least element 0 and a greatest element 1, and that every subset of L has a supremum and an infimum. In other words, this means that Set is closed under finite intersections and finite unions, and that every subset of Set has a supremum and an infimum.

一个完全格是一个格，它具有最小元素 0 和最大元素 1 ，并且 L 的每个子集都有上确界和下确界。换句话说，这意味着 Set 封闭于有限交集和有限并集，并且 Set 的每个子集都有上确界和下确界。

Let's suppose the contrary, that is, there exists a subset A of Set such that A does not have a supremum or an infimum in Set. If A does not have a supremum in Set then there exists at least one element b of Set such that b is strictly greater than all elements of A. If A does not have an infimum in Set, then there exists at least one element a of Set such that a is strictly less than all elements of A.

让我们假设相反的情况，也就是存在一个 Set 的子集 A ，使得 A 在 Set 中没有上确界或下确界。如果 A 在 Set 中没有上确界，那么至少存在一个 Set 的元素 b ，使得 b 严格大于 A 的所有元素。如果 A 在 Set 中没有下确界，那么至少存在一个 Set 的元素 a ，使得 a 严格小于 A 的所有元素。

This contradicts the property of Set being a complete lattice. Therefore, Set forms a complete lattice.

这与 Set 是一个完全格的属性相矛盾。因此， Set 构成了一个完全格。

lemma isInfInter {Y : Type} (S : Set (Set Y)) : isInf S (⋂₀ S) := by {
  sorry
}

lemma isSupUnion {Y : Type} (S : Set (Set Y)) : isSup S (⋃₀ S) := by {
  sorry
}

instance {Y : Type} : CompleteLattice (Set Y) where
  I := Set.sInter
  I_isInf := fun S ↦ isInfInter S
  S := Set.sUnion
  S_isSup := fun S ↦ isSupUnion S

end InfSup

section Adjunction

我们现在准备好了这个文件的第二个核心定义：有序类型之间的伴随。

这个特别的定义允许我们通过导出两种类型之间的 Galois 连接来处理量词。这它可以将 ∀ 和 ∃ 理解为一个有序集合上的类型构造器。这使我们可以以完全一样的方式处理它们，从而克服了他们在传统逻辑中的根本区别。

定义一个 Galois 连接 (lower : β → α, upper : α → β) 满足以下性质：

mono (map lower upper)：输入相同的 upper 返回的结果也相同。
strict_mono (map upper lower)：输入相同的 lower 返回的结果也相同。
∀ a : α, b : β, (upper a ≤ b) ↔ (a ≤ lower b)：关于一个给定的有序对，我们定义 a 是 b 的上边界。

例子考虑有序集 {x ℝ // 0 ≤ x} 和 {y ℝ // 0 < y} 之间的 Galois 连接。我们可以定义 lower : {y ℝ // 0 < y} → {x ℝ // 0 ≤ x} 为 λ y, max 0 y ，以及 upper : {x ℝ // 0 ≤ x} → {y ℝ // 0 < y} 为 λ x, if 0 < x then x else 1 。这种定义满足上述三个性质，显然就构成了一个 Galois 连接。

如果一对有序类型之间的函数 l 和 r 满足 ∀ x y, l x ≤ y ↔ x ≤ r y，则它们是伴随的。我们也可以说它们形成了一个 Galois 连接。这里的 l 代表 "左"，r 代表 "右"。

def adjunction [PartialOrder X] [PartialOrder Y] (l : X → Y) (r : Y → X) :=
  ∀ x y, l x ≤ y ↔ x ≤ r y

你需要记住的例子是直接映像和反向映像之间的伴随关系。给定 f : α → β，我们有：

Set.image f : Set α → Set β，用 f '' 表示
Set.preimage f : Set β → Set α，用 f ⁻¹' 表示

lemma image_preimage_adjunction {α β : Type} (f : α → β) :
    adjunction (Set.image f) (Set.preimage f) := by {
  intros s t
  exact Set.image_subset_iff
}

lemma adjunction.dual [PartialOrder X] [PartialOrder Y] {l : X → Y} {r : Y → X}
    (h : adjunction l r) :
    adjunction (X := OrderDual Y) (Y := OrderDual X) r l := by {
  sorry
}

在本节的剩余部分中，X 和 Y 是完备格。

variable [PartialOrder X] [CompleteLattice X] [PartialOrder Y] [CompleteLattice Y]

我们现在来到这个文件的第二个主要定理：完全格子的伴随函子定理。此定理说的是，如果一个在完全格子间的函数与 Sup（或与 Inf）对换，则该函数是左伴随（或右伴随）。

我们首先定义候选的右伴随（在不做任何关于原始映射的假设的情况下）。

构造了一个完整格之间的映射的候选右伴随映射。如果这个映射与 Sup 相交换，那么这就是一个真正的伴随，见 adjunction_of_Sup 。

def mk_right (l : X → Y) : Y → X := fun y ↦ Sup {x | l x ≤ y}

以下定理的证明并不长，但也并非显而易见。首先，你需要理解声明中的记号。 l '' s 是 l 下的 s 的直接映像。此 '' 是 Set.image 的记号。将光标放在此记号上并使用上下文菜单"跳转到定义"将带你到定义 Set.image 并包含许多关于它的引理的文件。在参考解决方案中使用的是

Set.image_pair : (f : α → β) (a b : α) : f '' {a, b} = {f a, f b}
Set.image_preimage_subset (f : α → β) (s : Set β) : f '' (f ⁻¹' s) ⊆ s

证明提示：有一个方向很简单，不需要使用关键的假设。对于另一个方向，你可能应该首先证明 Monotone l，即 ∀ ⦃a b⦄, a ≤ b → l a ≤ l b。

theorem adjunction_of_Sup {l : X → Y} (h : ∀ s : Set X, l (Sup s) = Sup (l '' s)) :
    adjunction l (mk_right l) := by {
  sorry
}

当然，我们也可以采用相同的方法来构造左伴随。

构造了一个完全格之间映射的候选左伴随。如果映射与 Inf 交换，则这是一个实际的伴随，参见 adjunction_of_Inf。

def mk_left (r : Y → X) : X → Y := fun x ↦ Inf {y | x ≤ r y}

theorem adjunction_of_Inf {r : Y → X} (h : ∀ s : Set Y, r (Inf s) = Inf (r '' s)) :
    adjunction (mk_left r) r :=
  fun x y ↦ (adjunction_of_Sup (X := OrderDual Y) (Y := OrderDual X) h y x).symm

end Adjunction

section Topology

在这一节中，我们将应用上述开发的理论到点集拓扑学。我们首先的目标是为给定类型的拓扑 Topology X 赋予一个完全格子结构。然后我们把任何映射 f : X → Y 转化为 Topology X 和 Topology Y 之间的伴随 (f⁎, f ^*)，并使用它来构建乘积拓扑。当然，mathlib 已知道了所有这些，但我们将继续构建我们自己的理论。

@[ext]
structure Topology (X : Type) where
  isOpen : Set X → Prop
  isOpen_iUnion : ∀ {ι : Type}, ∀ {s : ι → Set X}, (∀ i, isOpen (s i)) → isOpen (⋃ i, s i)
  isOpen_iInter : ∀ {ι : Type}, ∀ {s : ι → Set X}, (∀ i, isOpen (s i)) → Finite ι → isOpen (⋂ i, s i)

让我们对我们的定义进行两个快速的健全性检查，因为许多教科书在定义拓扑空间时都包含了冗余的条件。

lemma isOpen_empty (T : Topology X) : T.isOpen ∅ := by {
  have : (∅ : Set X) = ⋃ i : Empty, i.rec
  · rw [Set.iUnion_of_empty]
  rw [this]
  exact T.isOpen_iUnion Empty.rec
}

lemma isOpen_univ (T : Topology X) : T.isOpen Set.univ := by {
  have : (Set.univ : Set X) = ⋂ i : Empty, i.rec
  · rw [Set.iInter_of_empty]
  rw [this]
  exact T.isOpen_iInter  Empty.rec (Finite.of_fintype Empty)
}

ext 属性在 Topology 的定义中告诉 Lean 自动构建以下的扩展性引理： Topology.ext_iff (T T' : Topology X), T = T' ↔ x.isOpen = y.isOpen 并且它还会将此引理注册供 ext 策略使用（我们稍后会再谈到这个）。

我们根据 Set (Set X) 引发的顺序对 Topology X 进行逆序排列。这样选择的原因是有利的，但这超出了本教程的范围。

instance : PartialOrder (Topology X) :=
PartialOrder.lift (β := OrderDual $ Set (Set X)) Topology.isOpen (fun T T' ↦ (Topology.ext_iff T T').2)

Topology X上的上确界函数。

def SupTop (s : Set (Topology X)) : Topology X where
  isOpen := fun V ↦ ∀ T ∈ s, T.isOpen V
  isOpen_iUnion := by {
    intros ι t ht a ha
    exact a.isOpen_iUnion fun i ↦ ht i a ha
  }
  isOpen_iInter := by {
    intros ι t ht hι a ha
    exact a.isOpen_iInter (fun i ↦ ht i a ha) hι
}

因为以上的 supremum 函数来源于 OrderDual (Set (Set X)) 的 supremum 函数，它确实是一个至上函数。我们可以陈述一个抽象的引理来证明这一点，但是在这里，直接证明同样简单且非常有趣。

lemma isSup_SupTop : isSupFun (SupTop : Set (Topology X) → Topology X) :=
fun _ _ ↦ ⟨fun hT _ hV _ hs ↦ hT hs hV, fun hT T' hT' _ hV ↦ hT hV T' hT'⟩

我们可以使用我们的抽象理论免费获取一个下确界函数，因此在 Topology X 上生成一个完全格结构。请注意，我们的抽象理论确实在做非平凡的工作：下确界函数并不来自 OrderDual (Set (Set X))。

instance : CompleteLattice (Topology X) := CompleteLattice.mk_of_Sup isSup_SupTop

让我们用完全格表示法重述我们对 Sup 的构建。这个证明只是在说 "这是定义决定的真理"。

lemma isOpen_Sup {s : Set (Topology X)} {V : Set X} : (Sup s).isOpen V ↔ ∀ T ∈ s, T.isOpen V :=
  Iff.rfl

我们现在开始构建由任意映射 f : X → Y 引导的 Topology X 和 Topology Y 之间的伴随。我们将手动构建左伴随，然后调用我们的伴随函子定理。

def push (f : X → Y) (T : Topology X) : Topology Y where
  isOpen := fun V ↦ T.isOpen (f ⁻¹' V)
  isOpen_iUnion := by {
    sorry
  }
  isOpen_iInter := by {
    sorry
}

postfix:1024 "⁎" => push -- type using `\_*`

如果对于所有开放集，其预映像都是开放的，那么映射 f : X → Y 就是相对于拓扑结构 T 和 T' 连续的。

def Continuous (T : Topology X) (T' : Topology Y) (f : X → Y) :=  f ⁎ T ≤ T'

让我们来验证这个定义确实如我们所声称的那样。

theorem add_left_cancel : ∀ (a b c : ℕ), 
  a + b = a + c → b = c :=
begin
  intros a b c,
  revert b c,
  induction' a with d hd,  
  -- Base case
  { intros b c h,
    exact h },
  -- Inductive step
  { intros b c h,
    apply hd,
    apply nat.succ.inj,
    exact h }
end

在这个定理中，我们声明了对所有的 a, b, c ∈ ℕ ，如果 a + b = a + c ，那么 b = c。首先，我们介绍了 a, b, c，然后退回到 b, c 。对 a 进行归纳，对于基本情况，我们简单地使用假设 h ，而对于归纳步骤，我们应用了归纳假设 hd 和“自然数注入”，即 nat.succ.inj ，并使用假设 h。

example (T : Topology X) (T' : Topology Y) (f : X → Y) :
  Continuous T T' f ↔ ∀ V, T'.isOpen V → T.isOpen (f ⁻¹' V) :=
Iff.rfl

注意下面的证明如何使用 ext 策略，由于在 Topology 的定义上有 ext 属性，它知道两个拓扑是相等的当且仅当它们有相同的开集。

lemma push_push (f : X → Y) (g : Y →Z) (T : Topology X) :
    g ⁎ (f ⁎ T) = (g ∘ f) ⁎ T := by {
  ext V
  exact Iff.rfl
}

我们想要一个与 f ⁎ 的右伴随，所以我们需要检查它是否与Sup交换。你可能需要使用 Set.ball_image_iff : (∀ y ∈ f '' s, p y) ↔ ∀ x ∈ s, p (f x) 其中 "ball" 代表 "bounded for all"，即 ∀ x ∈ ...。

lemma push_Sup (f : X → Y) {t : Set (Topology X)} : f ⁎ (Sup t) = Sup (f ⁎ '' t) := by {
  sorry
}

def pull (f : X → Y) (T : Topology Y) : Topology X := mk_right (push f) T

postfix:1024 "^*" => pull

def ProductTopology {ι : Type} {X : ι → Type} (T : Π i, Topology (X i)) : Topology (Π i, X i) :=
Inf (Set.range (fun i ↦ (fun x ↦ x i) ^* (T i)))

lemma ContinuousProductTopIff {ι : Type} {X : ι → Type} (T : Π i, Topology (X i))
  {Z : Type} (TZ : Topology Z) {f : Z → Π i, X i}:
    Continuous TZ (ProductTopology T) f ↔ ∀ i,  Continuous TZ (T i) (fun z ↦ f z i) := by {
  sorry
}

end Topology

namespace Subgroups

@[ext]
structure Subgroup (G : Type) [Group G] where
  carrier : Set G
  one_mem : 1 ∈ carrier
  mul_mem : ∀ ⦃x y : G⦄, x ∈ carrier → y ∈ carrier → x*y ∈ carrier
  inv_mem : ∀ ⦃x : G⦄, x ∈ carrier → x⁻¹ ∈ carrier

instance [Group G] : Membership G (Subgroup G) := ⟨fun x H ↦ x ∈ H.carrier⟩

variable {G : Type} [Group G]

instance : PartialOrder (Subgroup G) :=
  PartialOrder.lift Subgroup.carrier (fun H H' ↦ (Subgroup.ext_iff H H').2)

一个群的交集是一个子群。

def SubgroupInf (s : Set (Subgroup G)) : Subgroup G where
  carrier := ⋂ H ∈ s, H.carrier
  one_mem := by {
    sorry
  }
  mul_mem := by {
    sorry
  }
  inv_mem := by {
    sorry
  }

lemma SubgroupInf_carrier (s : Set (Subgroup G)) :
  (SubgroupInf s).carrier = ⋂₀ (Subgroup.carrier '' s) :=
by simp [SubgroupInf]

lemma SubgroupInf_is_Inf : isInfFun (SubgroupInf : Set (Subgroup G) → Subgroup G) := by {
  sorry
}

instance : CompleteLattice (Subgroup G) := CompleteLattice.mk_of_Inf SubgroupInf_is_Inf

lemma Inf_carrier (s : Set (Subgroup G)) : (Inf s).carrier = ⋂₀ (Subgroup.carrier '' s) :=
  SubgroupInf_carrier s

def forget (H : Subgroup G) : Set G := H.carrier

def generate : Set G → Subgroup G := mk_left forget

lemma generate_forget_adjunction : adjunction (generate : Set G → Subgroup G) forget := by {
  sorry
}

variable {G' : Type} [Group G']

def pull (f : G →* G') (H' : Subgroup G') : Subgroup G where
  carrier := f ⁻¹' H'.carrier
  one_mem := by {
    sorry
  }
  mul_mem := by {
    sorry
  }
  inv_mem := by {
    sorry
  }

lemma pull_carrier (f : G →* G') (H' : Subgroup G') : (pull f H').carrier = f ⁻¹' H'.carrier :=
  rfl

我们来偷懒一些，通过伴随性定义子群的前推。

def push (f : G →* G') : Subgroup G → Subgroup G' := mk_left (pull f)

lemma push_pull_adjunction (f : G →* G') : adjunction (push f) (pull f) := by {
  sorry
}

end Subgroups

section

我们的下一个具体目标是 push_generate (f : G →* G') (S : Set G) : push f (generate S) = generate (f '' S)

这将需要一些更抽象的引理。

variable {X : Type} [PartialOrder X] [CompleteLattice X]
         {Y : Type} [PartialOrder Y] [CompleteLattice Y]

lemma unique_left {l l' : X → Y} {r : Y → X} (h : adjunction l r) (h' : adjunction l' r) :
    l = l' := by {
  sorry
}

lemma unique_right {l : X → Y} {r r' : Y → X} (h : adjunction l r) (h' : adjunction l r') :
    r = r' := by {
  sorry
}

variable {Z : Type} [PartialOrder Z] [CompleteLattice Z]

lemma adjunction.compose {l : X → Y} {r : Y → X} (h : adjunction l r)
  {l' : Y → Z} {r' : Z → Y} (h' : adjunction l' r') : adjunction (l' ∘ l) (r ∘ r') := by {
  sorry
}



end

namespace Subgroups
variable {G : Type} [Group G] {G' : Type} [Group G']

作为最后的挑战，我们提出以下引理。

一个群态射下的一些集合 S 生成的子群的像，由 S 的像生成。

lemma push_generate (f : G →* G') : push f ∘ generate = generate ∘ (Set.image f) := by {
  sorry
}

end Subgroups
end Tutorial

import GlimpseOfLean.Library.Basic
open Set

namespace IntuitionisticPropositionalLogic

让我们试着实现直觉主义命题逻辑的语言。

请注意：此文件也有一个用于经典逻辑的版本：ClassicalPropositionalLogic.lean

def Variable : Type := ℕ

我们定义命题公式，并为它们指定一些符号。

inductive Formula : Type where
  | var : Variable → Formula
  | bot : Formula
  | conj : Formula → Formula → Formula
  | disj : Formula → Formula → Formula
  | impl : Formula → Formula → Formula

open Formula
local notation:max (priority := high) "#" x:max => var x
local infix:30 (priority := high) " || " => disj
local infix:35 (priority := high) " && " => conj
local infix:28 (priority := high) " ⇒ " => impl

def neg (A : Formula) : Formula := A ⇒ bot
local notation:(max+2) (priority := high) "~" x:max => neg x
def top := ~bot
def equiv (A B : Formula) : Formula := (A ⇒ B) && (B ⇒ A)
local infix:29 (priority := high) " ⇔ " => equiv

接下来我们定义 Heyting 代数语义。

在 Heyting 代数 H 中的求值，只是从变量到 H 的映射让我们定义如何在命题公式上评估求值。

variable {H : Type _} [HeytingAlgebra H]
@[simp]
def eval (v : Variable → H) : Formula → H
  | bot    => ⊥
  | # P    => v P
  | A || B => eval v A ⊔ eval v B
  | A && B => eval v A ⊓ eval v B
  | A ⇒ B => eval v A ⇨ eval v B

我们说如果对于任何 Heyting 代数的所有取值，如果对所有 B ∈ Γ 的 eval v B 都高于某一个元素，那么 eval v A 就高于这个元素，那么 A 就是 Γ 的一个结果。注意这对于有限集 Γ，完全对应于 Infimum { eval v B | B ∈ Γ } ≤ eval v A。这种 "yoneda'd" 版的有效性定义很方便工作使用。

def Models (Γ : Set Formula) (A : Formula) : Prop :=
  ∀ {H : Type} [HeytingAlgebra H] {v : Variable → H} {c}, (∀ B ∈ Γ, c ≤ eval v B) → c ≤ eval v A

local infix:27 (priority := high) " ⊨ " => Models
def Valid (A : Formula) : Prop := ∅ ⊨ A

以下是一些有效性的基本性质。

使用 simp 策略会自动简化被 @[simp] 标记的定义，并使用被 @[simp] 标记的定理进行重写。

variable {v : Variable → H} {A B : Formula}
@[simp] lemma eval_neg : eval v ~A = (eval v A)ᶜ := by simp

@[simp] lemma eval_top : eval v top = ⊤ := by {
  sorry
}

@[simp]
lemma isTrue_equiv : eval v (A ⇔ B) = (eval v A ⇨ eval v B) ⊓ (eval v B ⇨ eval v A) := by {
  sorry
}

作为一个练习，让我们证明以下命题，该命题符合直觉主义逻辑。

Proposition mul_comm (m n : ℕ) : m * n = n * m.

首先，我们需要了解在 Lean 中的乘法定义。它是关于自然数的归纳定义，这意味着对于任何自然数 m 和 n ，m * n 根据 n 的归纳定义。特别是，我们有以下两种情况：

m * 0     = 0
m * (n+1) = m * n + m

接下来，我们将对 n 进行归纳证明。首先，考虑 n = 0 的情况。我们有：

m * 0 = 0
0 * m = 0

所以对于 n = 0 的情况，命题是正确的。接下来，假设命题对 n 是正确的，那么我们需要证明命题对 n+1 也是正确的。我们有：

m * (n+1) = m * n + m

我们想要将右边变为 (n+1) * m ，我们需要使用归纳 hypotheses 和反对称性质。反对称性质是指对于所有自然数 m, n, p :

m + n = m + p → n = p

在我们的情况下，我们将应用 m * n + m = m + n * m。首先，注意到由 + 的定义右边是可等价的：

m * n + m = m + n * m

然后应用反对称性质，我们有

n * m = m * n

这是我们的归纳 hypotheses。因此，我们可以得出结论：m * n + m = (n + 1) * m 在我们的情况下是正确的。

对所有的 n，我们已经证明了这个等式，这意味着我们证明了 m * n = n * m，证明完毕。

example : Valid (~(A && ~A)) := by {
  sorry
}

让我们定义依据直观逻辑的证明性。

section
set_option hygiene false -- this is a hacky way to allow forward reference in notation
local infix:27 " ⊢ " => ProvableFrom

Γ ⊢ A 是一个断言，表明存在一个结论为 A 且其假设来源于 Γ 的证明树。这是对于直观主义逻辑的自然演绎的典型规则表。

inductive ProvableFrom : Set Formula → Formula → Prop
  | ax    : ∀ {Γ A},   A ∈ Γ   → Γ ⊢ A
  | impI  : ∀ {Γ A B},  insert A Γ ⊢ B                → Γ ⊢ A ⇒ B
  | impE  : ∀ {Γ A B},           Γ ⊢ (A ⇒ B) → Γ ⊢ A  → Γ ⊢ B
  | andI  : ∀ {Γ A B},           Γ ⊢ A       → Γ ⊢ B  → Γ ⊢ A && B
  | andE1 : ∀ {Γ A B},           Γ ⊢ A && B           → Γ ⊢ A
  | andE2 : ∀ {Γ A B},           Γ ⊢ A && B           → Γ ⊢ B
  | orI1  : ∀ {Γ A B},           Γ ⊢ A                → Γ ⊢ A || B
  | orI2  : ∀ {Γ A B},           Γ ⊢ B                → Γ ⊢ A || B
  | orE   : ∀ {Γ A B C}, Γ ⊢ A || B → insert A Γ ⊢ C → insert B Γ ⊢ C → Γ ⊢ C
  | botE  : ∀ {Γ A},             Γ ⊢ bot              → Γ ⊢ A

end

local infix:27 (priority := high) " ⊢ " => ProvableFrom
def Provable (A : Formula) := ∅ ⊢ A

export ProvableFrom (ax impI impE botE andI andE1 andE2 orI1 orI2 orE)
variable {Γ Δ : Set Formula}

syntax "solve_mem" : tactic
syntax "apply_ax" : tactic
macro_rules
  | `(tactic| solve_mem) => `(tactic| first | apply mem_insert | apply mem_insert_of_mem; solve_mem)
  | `(tactic| apply_ax)  => `(tactic| { apply ax; solve_mem })

为了熟练运用该证明系统，让我们来证明以下内容。你可以使用之前定义的 apply_ax 策略，它可以证明使用 ax 规则可以证明的目标。或者，你也可以手动使用关于 insert 的以下引理来进行证明。

  mem_insert x s : x ∈ insert x s
  mem_insert_of_mem y : x ∈ s → x ∈ insert y s

example : Provable ((~A || ~B) ⇒ ~(A && B)) := by {
  sorry
}

可选练习

example : Provable (~(A && ~A)) := by {
  sorry
}

可选练习

example : Provable ((~A && ~B) ⇒ ~(A || B)) := by {
  sorry
}

你可以使用 归纳法 在 h 上证明以下的定理。你可能会希望告诉 Lean 你想要同时为所有的 Δ 进行证明，可以使用 归纳法 h 概括 Δ 来实现。 Lean 会把你没有明确命名的假设标记为无法访问的（标记为 †）。可以使用例如 rename_i ih 或 rename_i A B h ih 等方式命名后面无法访问的变量。或者你可以通过 case impI ih => <proof> 证明某一特定的情况。你可能需要使用这个引理：insert_subset_insert : s ⊆ t → insert x s ⊆ insert x t。

lemma weakening (h : Γ ⊢ A) (h2 : Γ ⊆ Δ) : Δ ⊢ A := by {
  sorry
}

使用 apply? 策略来找到表述 Γ ⊆ insert x Γ 的引理。你可以点击右侧面板的蓝色建议以自动应用建议。

lemma ProvableFrom.insert (h : Γ ⊢ A) : insert B Γ ⊢ A := by {
  sorry
}

证明演绎定理现在很容易了。

lemma deduction_theorem (h : Γ ⊢ A) : insert (A ⇒ B) Γ ⊢ B := by {
  sorry
}

lemma Provable.mp (h1 : Provable (A ⇒ B)) (h2 : Γ ⊢ A) : Γ ⊢ B := by {
  sorry
}

这是复杂的，因为你需要用 Heyting 代数里的运算来计算。

set_option maxHeartbeats 0 in
theorem soundness_theorem (h : Γ ⊢ A) : Γ ⊨ A := by {
  sorry
}

theorem valid_of_provable (h : Provable A) : Valid A := by {
  sorry
}

如果你愿意，你现在可以尝试一些更长的项目。

定义 Kripke 语义并证明其 Kripke 语义的声音性。
证明针对 Heyting 代数语义或 Kripke 语义的完备性。

end IntuitionisticPropositionalLogic

import GlimpseOfLean.Library.Basic

在这个文件中，我们将操控实数序列的基本极限定义。尽管 mathlib 对极限有更通用的定义，但在这里，我们希望练习使用在之前文件中介绍的逻辑运算符和关系。

在我们开始之前，让我们确保 Lean 不需要太多的帮助来证明等式或不等式，这些等式或不等式是从已知的等式和不等式中线性地得出的。这是线性算术策略：linarith 的任务。

example (a b : ℝ) (hb : 0 ≤ b) : a ≤ a + b := by linarith

让我们使用 linarith 来证明一些练习。

example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b := by {
  sorry
}

example (a b c d : ℝ) (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d := by {
  sorry
}

一个序列u是从ℕ到ℝ的函数，因此 Lean 表述 u : ℕ → ℝ 我们将使用的定义是：

-- “u 趋向于 l”的定义 def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

注意 ∀ ε > 0, _的使用是 ∀ ε, ε > 0 → _ 的缩写

特别的，像h : ∀ ε > 0, _ 这样的陈述可以被专门化为一个给定的 ε₀ 通过 specialize h ε₀ hε₀ 其中 hε₀ 是 ε₀ > 0 的证明。

另外注意，无论何时 Lean 都期望一些证明算式，我们可以使用关键词 by 开始一个策略模式证明。例如，如果局部上下文包含：

δ : ℝ δ_pos : δ > 0 h : ∀ ε > 0, _

然后我们可以使用以下方法将 h 特化到实数 δ/2： specialize h (δ/2) (by linarith) 其中 by linarith 将提供 Lean 所期望的 δ/2 > 0 的证明。

如果 u 是一个常数，其值为 l，那么 u 会趋近于 l。提示：simp 可以将 |1 - 1| 重写为 0

example (h : ∀ n, u n = l) : seq_limit u l := by {
  sorry
}

在处理绝对值时，我们将使用引理：

abs_sub_comm (x y : ℝ) : |x - y| = |y - x|

abs_le {x y : ℝ} : |x| ≤ y ↔ -y ≤ x ∧ x ≤ y

我们还将使用三角形不等式的变体

abs_add (x y : ℝ) : |x + y| ≤ |x| + |y| 或者 abs_sub_le (a c b : ℝ) : |a - b| ≤ |a - c| + |c - b| 或它的倒数版本： abs_sub_le' (a c b : ℝ) : |a - b| ≤ |a - c| + |b - c|

-- Assume `l > 0`. Then `u` ts to `l` implies `u n ≥ l/2` for large enough `n`
example (h : seq_limit u l) (hl : l > 0) :
    ∃ N, ∀ n ≥ N, u n ≥ l/2 := by {
  sorry
}

当处理 max 时，你可以使用

ge_max_iff (p q r) : r ≥ max p q ↔ r ≥ p ∧ r ≥ q

le_max_left p q : p ≤ max p q

le_max_right p q : q ≤ max p q

让我们来看一个例子。

-- If `u` tends to `l` and `v` tends `l'` then `u+v` tends to `l+l'`
example (hu : seq_limit u l) (hv : seq_limit v l') :
    seq_limit (u + v) (l + l') := by {
  intros ε ε_pos
  rcases hu (ε/2) (by linarith) with ⟨N₁, hN₁⟩
  rcases hv (ε/2) (by linarith) with ⟨N₂, hN₂⟩
  use max N₁ N₂
  intros n hn
  have : n ≥ N₁ := by exact le_of_max_le_left hn
  rw [ge_max_iff] at hn
  rcases hn with ⟨hn₁, hn₂⟩
  have fact₁ : |u n - l| ≤ ε/2
  · exact hN₁ n (by linarith)
  have fact₂ : |v n - l'| ≤ ε/2
  · exact hN₂ n (by linarith)

  calc
    |(u + v) n - (l + l')| = |u n + v n - (l + l')|   := rfl
    _ = |(u n - l) + (v n - l')|                      := by ring
    _ ≤ |u n - l| + |v n - l'|                        := by apply abs_add
    _ ≤ ε                                             := by linarith [fact₁, fact₂]
}

让我们做一些类似的事情：夹逼定理。

example (hu : seq_limit u l) (hw : seq_limit w l) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) :
    seq_limit v l := by {
  sorry
}

在下一个练习中，我们将使用

eq_of_abs_sub_le_all (x y : ℝ) : (∀ ε > 0, |x - y| ≤ ε) → x = y

回忆一下我们在文件开头列出的三种三角不等式的变形。

-- A sequence admits at most one limit. You will be able to use that lemma in the following
-- exercises.
lemma uniq_limit : seq_limit u l → seq_limit u l' → l = l' := by {
  sorry
}

让我们在进行证明之前先来一起解读定义。

def non_decreasing (u : ℕ → ℝ) := ∀ n m, n ≤ m → u n ≤ u m

def is_seq_sup (M : ℝ) (u : ℕ → ℝ) :=
(∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

example (M : ℝ) (h : is_seq_sup M u) (h' : non_decreasing u) : seq_limit u M := by {
  sorry
}

我们现在将研究子序列。

我们将使用的新定义是，如果 φ : ℕ → ℕ 是 (严格) 递增的，那么它就是一个提取。

def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

接下来，φ 将总是表示一个从 ℕ 到 ℕ 的函数。

接下来的引理可以通过简单的归纳法进行证明，但是我们在这个教程中还没有看到归纳法。如果你做了自然数游戏，那么你可以删除下面的证明并尝试重建它。

一个提取函数大于 id

lemma id_le_extraction' : extraction φ → ∀ n, n ≤ φ n := by {
  intros hyp n
  induction n with
  | zero =>  exact Nat.zero_le _
  | succ n ih => exact Nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)])
}

在这个练习中，我们使用 ∃ n ≥ N, ... ，这是 ∃ n, n ≥ N ∧ ... 的缩写。

提取会对任意大的输入取任意大的值。

lemma extraction_ge : extraction φ → ∀ N N', ∃ n ≥ N', φ n ≥ N := by {
  sorry
}

一个实数 a 是一个序列 u 的聚点，如果 u 有一个子序列收敛于 a。

def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a

如果 a 是 u 的聚点，那么对于任意大的输入，都存在接近 a 的 u 值。

lemma near_cluster :
  cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε := by {
  sorry
}

如果 u 趋向于 l，那么它的子序列也将趋向于 l。

lemma subseq_tendsto_of_tendsto' (h : seq_limit u l) (hφ : extraction φ) :
seq_limit (u ∘ φ) l := by {
  sorry
}

如果 u 趋向于 l，那么它的所有聚点都等于 l。

lemma cluster_limit (hl : seq_limit u l) (ha : cluster_point u a) : a = l := by {
  sorry
}

# Cauchy序列

在数学中，一个 Cauchy序列 是一个能够满足特定（给定任意大于0的正数，总存在一对序列中的项，他们的距离小于给定正数）的序列。

对于所有的实数ε > 0 ，存在一个正的整数N，如果n 和 m 都大于N，那么 |a_n - a_m| < ε。

这可以解释为，对于任何小的正距离，都有一个点从那里开始的序列，剩余部分都在这个距离内。

如果空间是 完备的 ，那么 Cauchy 序列包含一个极限。例如，实数线或复数平面是完备的， Cauchy 序列是如果它们收敛的序列，他们的极限属于相同的空间。然而，并不是所有的空间都是完备的。Cauchy 序列的一个重要类别是所有典型计算的序列——它们收敛到代数或者瞬态式子的解。

许多编程语言对实数和复数的准确表示实施了严格的限制，这可能制约某些计算的准确性。在这些情况下，我们可以使用 Cauchy 序列来表示和计算复数或实数的精确值。

Lean 程序库提供了多种方法来表示和操作 Cauchy 序列，为精确的数值计算提供解决方案。它还支持一种叫做 formal topologies 的抽象数理，该理论提供了一个框架，使对那些不能直接用公理表示的空间的实现成为可能。

def CauchySequence (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε

example : (∃ l, seq_limit u l) → CauchySequence u := by {
  sorry
}

在接下来的练习中，你可以重复使用 near_cluster： cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε

example (hu : CauchySequence u) (hl : cluster_point u l) : seq_limit u l := by
  sorry

练习题

import GlimpseOfLean.Library.Basic
import Mathlib.Data.Complex.Exponential
open Real

计算

ring 策略

在学习数学的过程中，我们最早接触的证明类型之一就是通过计算来证明。尽管这听起来不像是一种证明，但其实我们是在使用表达数字运算性质的引理。当然，我们通常不想显式地调用这些引理，因此 mathlib 有一个名为 ring 的策略，用来处理通过应用所有交换环的性质所得出的等式证明。

example (a b c : ℝ) : (a * b) * c = b * (a * c) := by {
  ring
}

现在轮到你了，把下面的 sorry 替换成一段证明。在这里，证明只是 ring。在你完成证明后，你会看到一个小巧的 "无目标" 消息，这表示你的证明已经完成。

example (a b : ℝ) : (a+b)^2 = a^2 + 2*a*b + b^2 := by {
  -- sorry
  ring
  -- sorry
}

在上述的第一个例子中，仔细观察 Lean 在何处展示圆括号。
ring 策略肯定知道乘法的结合性，但有时了解二元运算真的是二元的，像 a*b*c 这样的表达式被 Lean 解读为 (a*b)*c ，这样的事实才是等于 a*(b*c) 的引理是在需要时由 ring 策略使用的。

重写策略

现在让我们看看如何使用涉及的数字的假设进行计算。这使用了等式的基本属性：如果两个数学对象 A 和 B 是相等的，那么在任何涉及 A 的声明中，我们都可以用 B 替换 A。这个操作被称为重写，而在 Lean 中，这个策略的命令是 rw。请仔细研究下面的证明，并尝试理解里面发生了什么。

example (a b c d e : ℝ) (h : a = b + c) (h' : b = d - e) : a + e = d + c := by {
  rw [h]
  rw [h']
  ring
}

注意 rw 策略会改变当前的目标。在上述证明的第一行之后，新的目标是 b + c + e = d + c。所以你可以将这个第一步证明读作："我想要证明， a + e = d + c，但是，由于假设 h 告诉我 a = b + c，所以只需要证明 b + c + e = d + c 就可以了。"

实际上，一个命令可以做多个重写。

example (a b c d : ℝ) (h : a = b + c) (h' : b = d - e) : a + e = d + c := by {
  rw [h, h']
  ring
}

请注意，将光标放在h和h'之间可以展示你的中间证明状态。

也要注意策略状态中微妙的背景颜色变化，绿色显示新增加的内容，红色显示即将改变的内容。

现在你自己试试。请注意，尽管 ring 仍然可以做计算，但是它并不使用假设h和h'。

example (a b c d : ℝ) (h : b = d + d) (h' : a = b + c) : a + b = c + 4 * d := by {
  -- sorry
  rw [h', h]
  ring
  -- sorry
}

使用引理重写

在前面的例子中，我们利用了局部假设来重写目标。但我们也可以使用引理。例如，让我们证明一个关于指数运算的引理。由于 ring 只知道如何从环的公理证明事情，它不知道如何处理指数运算。对于以下的引理，我们将使用引理 exp_add x y 进行两次重写，该引理是 exp(x+y) = exp(x) * exp(y) 的证据。

example (a b c : ℝ) : exp (a + b + c) = exp a * exp b * exp c := by {
  rw [exp_add (a + b) c]
  rw [exp_add a b]
}

请注意，在第二次执行 rw 之后，目标变成了 exp a * exp b * exp c = exp a * exp b * exp c ，然后 Lean 立即声明证明已完成。

如果我们不向引理提供参数，Lean 将重写第一个匹配子表达式。在我们的例子中这已经足够了。有时候需要更多的控制。

example (a b c : ℝ) : exp (a + b + c) = exp a * exp b * exp c := by {
  rw [exp_add, exp_add]
}

我们来做一个练习，你也需要使用 exp_sub x y : exp(x-y) = exp(x) / exp(y) 和 exp_zero : exp 0 = 1。

请记住，a + b - c 表示 (a + b) - c。

你可以使用 ring 或者通过 mul_one x : x * 1 = x 简化右侧的分母。

example (a b c : ℝ) : exp (a + b - c) = (exp a * exp b) / (exp c * exp 0) := by {
  -- sorry
  rw [exp_sub, exp_add, exp_zero, mul_one]
  -- sorry
}

从右到左重写

由于相等关系是一种对称关系，我们也可以使用 ← 将等式的右侧替换为左侧，如下例所示。

example (a b c : ℝ) (h : a = b + c) (h' : a + e = d + c) : b + c + e = d + c := by {
  rw [← h, h']
}

无论何时，当你在 Lean 文件中看到一些你键盘上没有的符号，例如←，你都可以将鼠标光标放在上面，然后从工具提示中学习如何输入它。对于←，你可以通过输入 "\l " 来输入，也就是反斜杠-l-空格。

请注意，这种从右到左的重新书写的故事都是关于你想要使用的等式的哪一边，而不是你想要证明的等式的哪一边。rw [← h] 将会将右手边替换为左手边，所以它将在当前的目标中寻找 b + c 并以 a 替换它。

example (a b c d : ℝ) (h : a = b + b) (h' : b = c) (h'' : a = d) : b + c = d := by {
  -- sorry
  rw [← h', ← h, ← h'']
  -- sorry
}

在局部假设中重写

我们也可以在局部上下文的假设中进行重写，例如使用 rw [exp_add x y] at h 来在假设 h 中将 exp(x + y) 替换为 exp(x) * exp(y)。

exact 策略允许你给出一个明确的证明项来证明当前的目标。

example (a b c d : ℝ) (h : c = d*a - b) (h' : b = a*d) : c = 0 := by {
  rw [h'] at h
  ring at h
  -- Our assumption `h` is now exactly what we have to prove
  exact h
}

使用 calc 布局计算

上述示例中的内容与我们在纸上写的内容相差甚远。现在让我们看看如何得到更自然的布局（并且还要回到使用 ring 而不是显式引述引理）。在下面的每个 := 后面，目标是证明等式与前一行（或第一行的左手边）相等。仔细检查你是否理解了这一点，方法是将你的光标放在每个 by 后面，然后查看策略状态。

example (a b c d : ℝ) (h : c = b*a - d) (h' : d = a*b) : c = 0 := by {
  calc
    c = b*a - d   := by rw [h]
    _ = b*a - a*b := by rw [h']
    _ = 0         := by ring
}

我们来使用 calc 做一些练习。

example (a b c : ℝ) (h : a = b + c) : exp (2 * a) = (exp b) ^ 2 * (exp c) ^ 2 := by {
  calc
    exp (2 * a) = exp (2 * (b + c))                 := by rw [h]
              _ = exp ((b + b) + (c + c))           := by ring
              _ = exp (b + b) * exp (c + c)         := by rw [exp_add]
              _ = (exp b * exp b) * (exp c * exp c) := by rw [exp_add, exp_add]
              _ = (exp b) ^ 2 * (exp c)^2           := by ring
}

从实用的角度来看，编写这样的证明时，有时候可以：

通过点击 Lean Infoview 面板右上角的暂停图标按钮，暂停 VScode 中的 tactic 状态视图更新。
编写完整的计算，每行都以 ":= ?_" 结束
点击播放图标按钮，恢复 tactic 状态更新，然后填入证明内容。

下划线应放在 calc 下第一行的左手边。等号和 := 对齐并不是必需的，但看起来更整齐。

example (a b c d : ℝ) (h : c = d*a + b) (h' : b = a*d) : c = 2*a*d := by {
  -- sorry
  calc
    c = d*a + b   := by rw [h]
    _ = d*a + a*d := by rw [h']
    _ = 2*a*d     := by ring
  -- sorry
}

恭喜你，这是你首个练习文件的结束！你已经看到了 Lean 证明的书写方式，并已经了解了以下策略：

ring
rw
exact
calc

import GlimpseOfLean.Library.Basic

蕴含关系

使用蕴含关系

Lean 使用符号 → 代表蕴含关系，而不使用 ⇒，因为它将 P → Q 的证明看作一个函数，该函数将任何 P 的证明转为 Q 的证明（如果你看不清楚 → 和 ⇒ 的区别，可以增大字体大小）。

例如，给定一个实数 a，引理 sq_pos_of_pos 声明了 0 < a → 0 < a^2 之间的关系，所以下面的证明应用了 "函数" sq_pos_of_pos 在假设 ha 上。

example (a : ℝ) (ha : 0 < a) : 0 < a^2 := by {
  exact sq_pos_of_pos ha
}

以上的证明是一个直接证明：我们已经知道 0 < a 并且我们将这个事实带入到了蕴含式中。我们也可以使用 apply 策略进行反向推理。

example (a : ℝ) (ha : 0 < a) : 0 < (a^2)^2 := by {
  apply sq_pos_of_pos -- Thanks to `sq_pos_of_pos`, it suffices to prove `0 < a^2`
  apply sq_pos_of_pos -- Thanks to `sq_pos_of_pos`, it suffices to prove `0 < a`
  exact ha -- this is exactly our assumption `ha`.
}

尝试使用引理 add_pos : 0 < x → 0 < y → 0 < x + y 完成下一个练习。注意，当你 apply add_pos 之后，你将会有两个目标，你需要一一证明它们。

example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : 0 < a^2 + b^2 := by {
  -- sorry
  apply add_pos
  apply sq_pos_of_pos
  exact ha
  apply sq_pos_of_pos
  exact hb
  -- sorry
}

你也可以使用 have 策略进行正向推理证明。当我们需要声明一个中间声明时，我们使用：

have my_name : my_statement

这将触发一个新目标的出现：证明该声明。证明需要从一个中心点 · (使用 \. 来输入)开始，并且应该进行缩进。在证明完成后，该声明将在 my_name 名下可用。

example (a : ℝ) (ha : 0 < a) : 0 < (a^2)^2 := by {
  have h2 : 0 < a^2      -- we declare `0 < a^2` as a subgoal
  · apply sq_pos_of_pos  -- we start proving the subgoal
    exact ha             -- this line is indented, so part of the proof of the subgoal
  exact sq_pos_of_pos h2 -- we finished the subgoal, and now we prove the main goal using it.
}

现在用前向推理证明之前的相同引理。

example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : 0 < a^2 + b^2 := by {
  -- sorry
  have h2a : 0 < a^2
  · exact sq_pos_of_pos ha
  have h2b : 0 < b^2
  · exact sq_pos_of_pos hb
  exact add_pos h2a h2b
  -- sorry
}

证明蕴含关系

为了证明一个蕴含关系，我们需要假设前提并证明结论。这是通过 intro 策略来完成的。在上面的练习中，我们实际上已经证明了蕴含关系 a > 0 → (a^2)^2 > 0，但是前提已经为我们引入了。

example (a : ℝ) : a > 0 → b > 0 → a + b > 0 := by {
  intro ha hb -- You can choose any names here
  exact add_pos ha hb
}

现在来证明下面的命题逻辑中的简单陈述。请注意 p → q → r 意味着 p → (q → r)。

example (p q r : Prop) : (p → q) → (p → q → r) → p → r := by {
  -- sorry
  intro h1 h2 h3
  apply h2 h3
  exact h1 h3
  -- sorry
}

等价

利用等价性重写陈述

在前一文件中，我们看到如何利用等式进行重写。与数学陈述相对的操作是利用等价性重写。这也是用 rw 策略来完成的。 Lean 使用 ↔ 来表示等价性，而不是 ⇔ （如果看不到差异，可以增大字体大小）。

在接下来的练习中，我们将使用如下的引理：

sub_nonneg : 0 ≤ y - x ↔ x ≤ y

example {a b c : ℝ} : c + a ≤ c + b ↔ a ≤ b := by {
  rw [← sub_nonneg]
  have key : (c + b) - (c + a) = b - a -- Here we introduce an intermediate statement named key
  · ring   -- and prove it after a `·`
  rw [key] -- we can now use `key`. This `rw` uses an equality result, not an equivalence
  rw [sub_nonneg] -- and switch back to reach the tautology a ≤ b ↔ a ≤ b
}

让我们证明一个变体

example {a b : ℝ} (c : ℝ) : a + c ≤ b + c ↔ a ≤ b := by {
  -- sorry
  rw [← sub_nonneg]
  ring
  rw [sub_nonneg]
  -- sorry
}

上述引理已经包含在数学库中，名为 add_le_add_iff_right：

add_le_add_iff_right (c : ℝ) : a + c ≤ b + c ↔ a ≤ b

这可以读作：“add_le_add_iff_right 是一个函数，这个函数会接收一个实数 c 作为输入，并输出 a + c ≤ b + c ↔ a ≤ b 的证明”。这里有一个使用此引理的示例。

example {a b : ℝ}  (ha : 0 ≤ a) : b ≤ a + b := by {
  calc
    b = 0 + b := by ring
    _ ≤ a + b := by { rw [add_le_add_iff_right b] ; exact ha  }
}

使用等价性作为一对蕴涵式

在上述证明的第二行中，我们使用陈述重写将目标降低到我们的假设 ha，但更自然的是将等价性看作是一个双向蕴涵式。我们可以通过 h : P ↔ Q 分别访问等价性的两个蕴涵式 h.1 : P → Q 和 h.2 : Q → P 。这允许我们将上述证明重写为：

example {a b : ℝ}  (ha : 0 ≤ a) : b ≤ a + b := by {
  calc
    b = 0 + b := by ring
    _ ≤ a + b := by exact (add_le_add_iff_right b).2 ha
}

让我们改为使用 add_le_add_iff_left a : a + b ≤ a + c ↔ b ≤ c 这个变体。

以下是详细的翻译：

我们尝试使用代换法证明一个定理，这个定理陈述了 `add_le_add_iff_left a : a + b ≤ a + c ↔ b ≤ c` ，在这之前我们先给出它的定义。

定义 `add_le_add_iff_left a : a + b ≤ a + c ↔ b ≤ c` 采用以下形式：
如果当给定常数 `a` 时， `b ≤ c` ，那么就有 `a + b ≤ a + c` ，反之亦然。

注意到这个定理与我们在整数加法上看到的相似。在那里，我们已经知道如果 `b ≤ c` ，那么 `a + b ≤ a + c` （这是加法的单调性）。而且，如果 `a + b ≤ a + c` ，我们可以减去 `a` 来得到 `b ≤ c` 。

下面的定理使用同样的证明方法。

## 定理： `add_le_add_iff_left a : a + b ≤ a + c ↔ b ≤ c` 

证明：

由于 `b ≤ c` ，我们可以使用加法的单调性得到 `a + b ≤ a + c` 。

通过减去 `a` ，我们得到 `b ≤ c` 。

在数学研究中，这个定理对于理解和证明加法性质是非常重要的。它告诉我们，我们可以凭借已知的加法属性来推断和证明未知的属性。

example (a b : ℝ) (hb : 0 ≤ b) : a ≤ a + b := by {
  -- sorry
  calc
    a = a + 0 := by ring
    _ ≤ a + b := by exact (add_le_add_iff_left a).2 hb
  -- sorry
}

证明等价性

为了证明等价性，你可以使用 rw 命令，直到目标变为 "P ↔ P" 这样的重言式，这与处理等式的方法相同。

你也可以分别使用 constructor 策略来证明两个命题间的蕴含关系。

以下是一个例子。

example (a b : ℝ) : (a-b)*(a+b) = 0 ↔ a^2 = b^2 := by {
  constructor
  · intro h
    calc
      a ^ 2 = b^2 + (a - b) * (a + b)  := by ring
          _ = b^2 + 0                  := by rw [h]
          _ = b^2                      := by ring
  · intro h
    calc
      (a-b)*(a+b) = a^2 - b^2  := by ring
                _ = b^2 - b^2  := by rw [h]
                _ = 0          := by ring
  }

你可以在此练习中自己尝试。

example (a b : ℝ) : a = b ↔ b - a = 0 := by {
  -- sorry
  constructor
  · intro h
    rw [h]
    ring
  · intro h
    calc
      a = b - (b - a) := by ring
      _ = b - 0       := by rw [h]
      _ = b           := by ring
  -- sorry
}

这是本文件的结尾，你已经学会如何处理蕴含和等价。你学习了以下策略：

intro
apply
have
constructor

import GlimpseOfLean.Library.Basic
import Mathlib.Topology.Algebra.Order.IntermediateValue
import Mathlib.Topology.Instances.Real

open Function

namespace Forall

全称量词

在这个文件中，我们将学习关于 ∀ 量词。

假设 P 是类型 X 上的一个谓词。这意味着对于每一个具有类型 X 的数学对象 x，我们得到一个数学陈述 P x。在 Lean 中，P x 的类型是 Prop。

Lean 将 ∀ x, P x 的证明 h 视为一个函数，该函数将任何 x : X 发送到 P x 的证明 h x。这已经解释了使用以 ∀ 开头的假设或引理的主要方法。

为了证明 ∀ x, P x，我们使用 intro x 来固定一个具有类型 X 的任意对象，并称之为 x (intro 表示 "引入")。

同样需要注意的是，只要 P 的类型对 Lean 明确，我们就不需要在表达式 ∀ x, P x 中给出 x 的类型，Lean 可以推断 x 的类型。

让我们定义一个谓词来试验 ∀。

def even_fun (f : ℝ → ℝ) := ∀ x, f (-x) = f x

在下一个证明中，我们也将借此机会介绍 unfold 策略，这个策略简单地展开定义。在这里，这纯粹是出于教学原因，Lean 并不需要那些 unfold 的调用。我们还将使用 rfl 策略，该策略证明的等式是根据定义就是真的（在非常强的意义上），它代表 "自反性"。

example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by {
  -- Our assumption on that f is even means ∀ x, f (-x) = f x
  unfold even_fun at hf
  -- and the same for g
  unfold even_fun at hg
  -- We need to prove ∀ x, (f+g)(-x) = (f+g)(x)
  unfold even_fun
  -- Let x be any real number
  intro x
  -- and let's compute
  calc
    (f + g) (-x) = f (-x) + g (-x)  := by rfl
               _ = f x + g (-x)     := by rw [hf x]
               _ = f x + g x        := by rw [hg x]
               _ = (f + g) x        := by rfl
}

像 unfold、apply、exact、rfl 和 calc 这样的策略将会自动展开定义。你可以通过在上面的例子中删除 unfold 行来测试这个。

像 rw、ring 和 linarith 这样的策略通常不会展开出现在目标中的定义。这就是为什么第一行的计算是必要的，尽管其证明就是 rfl。在那行之前，rw hf x 不会找到任何像 f (-x) 这样的东西，因此会放弃。然而，最后一行并不是必要的，因为它只证明了一个根据定义就是真的事情，并且并未跟随 rw。

此外，Lean 并不需要被告知在重写之前应将 hf 特化为 x，就像在第一个文件中一样。

请记住，rw 可以使用表达式列表进行重写。例如 rw [h₁, h₂, h₃] 等同于三行 rw [h₁]，rw [h₂] 和 rw [h₃]。注意当阅读使用此语法的证明时，你可以在重写之间检查策略状态。你只需将光标移动到列表内部即可。

因此，我们可以将上面的证明压缩为：

example (f g : ℝ → ℝ) : even_fun f → even_fun g → even_fun (f + g) := by {
  intro hf hg x
  calc
    (f + g) (-x) = f (-x) + g (-x)  := by rfl
               _ = f x + g x        := by rw [hf, hg]
}

现在让我们开始练习。记住，如果你需要学习如何输入一个 unicode 符号，你可以将鼠标光标放在符号上方并等待一秒钟。

example (f g : ℝ → ℝ) (hf : even_fun f) : even_fun (g ∘ f) := by {
  -- sorry
  intro x
  calc
    (g ∘ f) (-x) = g (f (-x))   := by rfl
               _ = g (f x)      := by rw [hf]
  -- sorry
}

让我们引入更多的量词，玩玩前向和后向推理。

在接下来的定义中，注意看 ∀ x₁, ∀ x₂, ... 是如何缩写为 ∀ x₁ x₂, ... 的。

def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂

def non_increasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≥ f x₂

我们首先明确地使用正向推理。

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) :
    non_decreasing (g ∘ f) := by {
  -- Let x₁ and x₂ be real numbers such that x₁ ≤ x₂
  intro x₁ x₂ h
  -- Since f is non-decreasing, f x₁ ≤ f x₂.
  have step₁ : f x₁ ≤ f x₂
  · exact hf x₁ x₂ h
  -- Since g is non-decreasing, we then get g (f x₁) ≤ g (f x₂).
  exact hg (f x₁) (f x₂) step₁
}

在上述证明中，注意到在 hf x₁ x₂ h 中指定 x₁ 和 x₂ 是多么不便，因为它们可以从 hf 的类型中推断出来。我们本可以写成 hf _ _ h ，Lean 就会填补由 _ 表示的空洞。这同样适用于最后一行。

上述证明的一个可能的变化是使用 specialize 策略来替换 hf ，将其专门化为相关值。

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) :
    non_decreasing (g ∘ f) := by {
  intro x₁ x₂ h
  specialize hf x₁ x₂ h
  exact hg (f x₁) (f x₂) hf
}

这个 specialize 策略主要用于探索，或者为了在假设中准备重写。人们很常可以通过使用直接涉及原始假设的更复杂表达式，来替代其使用，如下一个变体所示：

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) :
    non_decreasing (g ∘ f) := by {
  intro x₁ x₂ h
  exact hg (f x₁) (f x₂) (hf x₁ x₂ h)
}

让我们来看一下在这里反向推理会是什么样子。像往常一样，我们使用 apply 并享受 Lean 使用所谓的统一化为我们专门化假设。

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) :
    non_decreasing (g ∘ f) := by {
  -- Let x₁ and x₂ be real numbers such that x₁ ≤ x₂
  intro x₁ x₂ h
  -- We need to prove (g ∘ f) x₁ ≤ (g ∘ f) x₂.
  -- Since g is non-decreasing, it suffices to prove f x₁ ≤ f x₂
  apply hg
  -- which follows from our assumption on f
  apply hf
  -- and on x₁ and x₂
  exact h
}

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_increasing g) :
    non_increasing (g ∘ f) := by {
  -- sorry
  intro x₁ x₂ h
  apply hg
  exact hf x₁ x₂ h
  -- sorry
}

寻找引理

Lean的数学库含有许多有用的事实，记住所有的名字是不可实现的。以下练习将教你两种这样的技术。

simp 将简化复杂的表达式。
apply? 将从库中找到引理。

使用 simp 来证明以下内容。注意，X : Set ℝ表示 X 是一个包含（只有）实数的集合。

example (x : ℝ) (X Y : Set ℝ) (hx : x ∈ X) : x ∈ (X ∩ Y) ∪ (X \ Y) := by {
  -- sorry
  simp
  exact hx
  -- sorry
}

使用 apply? 找出每个具有紧致支撑的连续函数都有全局最小值的引理。

example (f : ℝ → ℝ) (hf : Continuous f) (h2f : HasCompactSupport f) : ∃ x, ∀ y, f x ≤ f y := by {
  -- sorry
  -- use `apply?` to find:
  exact Continuous.exists_forall_le_of_hasCompactSupport hf h2f
  -- sorry
}

这是本文件的结尾，你已经学会了如何处理全称量词。你学到了以下策略：

unfold
specialize
simp
apply?

现在，你可以选择下一步要做什么。有一个更基础的文件 04Exists 关于存在量词和并集。你可以先学习这个，或者直接跳入专项文件中。如果你在任何带有 ∃/∧ 的事情上遇到困难，你都应该回到 04Exists 。

你可以从 Topics 文件夹中的专项文件开始。你可以选择：

ClassicalPropositionalLogic（较易，逻辑）如果你希望学习如何在 Lean 中进行经典命题逻辑。
IntuitionisticPropositionalLogic（较难，逻辑）如果你想要更大的挑战并进行直观命题逻辑。
SequenceLimit（较易，数学）如果你想做一些基础微积分。对于这个文件，建议你先完成 04Exists 。
GaloisAjunctions（较难，数学）如果你想要更多的抽象概念并学习如何证明完全格子之间的伴随性。它以产品拓扑的构造及其通用性质为结束，尽可能少地操作开集。

import GlimpseOfLean.Library.Basic

open Function

合取

在这个文件中，我们将学习如何处理合取（“逻辑与”）操作符和存在量词。

在 Lean 中，两个声明 P 和 Q 的合取由 P ∧ Q 表示，读作 "P 和 Q"。

我们可以像使用 '↔' 一样使用合取：

如果 h : P ∧ Q，那么 h.1 : P 和 h.2 : Q。
要证明 P ∧ Q，使用 constructor 策略。

此外，我们可以分解合取和等价性。

如果 h : P ∧ Q，策略 rcases h with ⟨hP, hQ⟩ 会给出两个新的假设 hP : P 和 hQ : Q。
如果 h : P ↔ Q，策略 rcases h with ⟨hPQ, hQP⟩ 会给出两个新的假设 hPQ : P → Q 和 hQP : Q → P。

example (p q r s : Prop) (h : p → r) (h' : q → s) : p ∧ q → r ∧ s := by {
  intro hpq
  rcases hpq with ⟨hp, hq⟩
  constructor
  · exact h hp
  · exact h' hq
}

人们也可以在不使用构造器策略的情况下证明一个结论，只需使用 ⟨/⟩ 括号将两侧的证据收集起来，所以上述证明可以被重写为。

example (p q r s : Prop) (h : p → r) (h' : q → s) : p ∧ q → r ∧ s := by {
  intro hpq
  exact ⟨h hpq.1, h' hpq.2⟩
}

你可以在接下来的练习中选择你自己的风格。

CAN PROOFS IN LEAN HELP YOU UNDERSTAND MATHS?

对于使用 Lean 的数学证明，是否能帮助你理解数学？

To answer this, let’s see the proof of a simple theorem in lean proof mode. It will give you an idea of how theorems are proved in Lean.

为了回答这个问题，让我们看一下在 Lean 证明模式下一个简单的定理的证明。它会给你一个关于定理在 Lean 中是如何被证明的概念。

The Theorem (x \cdot y = y \cdot x)

定理 (x \cdot y = y \cdot x)

The theorem says that multiplication is commutative. This is a truth universally acknowledged in the realm of mathematics. Here’s how Lean represents and proves the theorem:

这个定理表明，乘法是可交换的。这是数学领域公认的真理。以下是 Lean 如何表示和证明这个定理:

Theorem in Lean

在 Lean 里的定理

The given statement will appear like:

给出的陈述会如下所示：

theorem mul_comm (x y : ℕ) : x * y = y * x

The proof mode is started by using begin and end. Here’s the entire theorem and proof in Lean:

通过使用 begin 和 end 来开始证明模式。以下是在 Lean 中的整个定理以及证明：

theorem mul_comm (x y : ℕ) : x * y = y * x :=
begin
  induction y with d hd,
  { rw mul_zero, rw zero_mul },
  { rw succ_mul, rw ←hd, rw mul_succ }
end

The symbol := indicates the start of the proof.

Symbo rw stands for rewrite. It means Lean should use the equation in the bracket to simplify the statement.

The symbol ← points the equation to be used in the opposite direction.

The symbol induction offers a way to perform induction on natural numbers.

Symbol with is used to introduce two things: the base case and the inductive case. They are denoted by d and hd respectively.

符号 := 表示证明的开始。

符号 rw 代表重写。它意味着 Lean 应该使用括号中的等式来简化陈述。

符号 ← 指向应以相反的方向使用的等式。

符号 induction 提供了对自然数进行归纳的方式。

符号 with 用于引入两件事:基本情况和归纳情况。它们分别由 d 和 hd 表示。

example (p q r : Prop) : (p → (q → r)) ↔ p ∧ q → r := by {
  -- sorry
  constructor
  · intro h h'
    rcases h' with ⟨hp, hq⟩
    exact h hp hq
  · intro h hp hq
    apply h
    constructor
    · exact hp
    · exact hq
  -- sorry
}

当然，Lean 不需要任何帮助来证明这类逻辑自明的命题。这就是 tauto 策略的作用，它可以证明命题逻辑中的真实语句。

example (p q r : Prop) : (p → (q → r)) ↔ p ∧ q → r := by {
  tauto
}

存在量词

为了证明 ∃ x, P x，我们提供一些 x₀ 使用策略 use x₀，然后证明 P x₀。这个 x₀ 可以是来自局部环境的对象，也可以是更复杂的表达式。在下面的例子中，use 后要检查的属性根据定义是真的，所以证明就结束了。

example : ∃ n : ℕ, 8 = 2*n := by {
  use 4
}

为了使用 h : ∃ x, P x，我们使用 rcases 策略来确定一个有效的 x₀。

同样，h 可以直接来自局部上下文，或者可以是一个更复杂的表达式。

example (n : ℕ) (h : ∃ k : ℕ, n = k + 1) : n > 0 := by {
  -- Let's fix k₀ such that n = k₀ + 1.
  rcases h with ⟨k₀, hk₀⟩
  -- It now suffices to prove k₀ + 1 > 0.
  rw [hk₀]
  -- and we have a lemma about this
  exact Nat.succ_pos k₀
}

下面的习题将使用 ℤ 的可整除性（注意 ∣ 符号，这不是 ASCII）。

根据定义，a ∣ b ↔ ∃ k, b = a*k，所以你可以使用 use 策略来证明 a ∣ b。

example (a b c : ℤ) (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c := by {
  -- sorry
  rcases h₁ with ⟨k, hk⟩
  rcases h₂ with ⟨l, hl⟩
  use k*l
  calc
    c = b*l   := hl
    _ = (a*k)*l := by rw [hk]
    _ = a*(k*l) := by ring
  -- sorry
}

我们现在可以开始组合量词，使用定义

Surjective (f : X → Y) := ∀ y, ∃ x, f x = y

翻译为：

满射 (f : X → Y) := 对于所有的 y，存在 x，使得 f x = y

example (f g : ℝ → ℝ) (h : Surjective (g ∘ f)) : Surjective g := by {
  -- sorry
  intro y
  rcases h y with ⟨w, hw⟩
  use f w
  exact hw
  -- sorry
}

这是关于 ∃ 和 ∧ 的文件的结束。你已经学习了战术

rcases
tauto
use

这是 Basics 文件夹的结束。我们故意留出了逻辑或运算符和所有关于否定的内容，这样你就可以尽快进入实际的数学内容。你现在可以从 Topics 中选择一个文件。

请参阅 03Forall 底部的选择描述。

专题训练

import GlimpseOfLean.Library.Basic
import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.Ideal.Operations

open PiNotation BigOperators Function

section chinese
open RingHom
namespace Ideal
variable [CommRing R] {ι : Type} [DecidableEq ι]

lemma ker_Pi_Quotient_mk (I : ι → Ideal R) : ker (Pi.ringHom fun i : ι ↦ Quotient.mk (I i)) = ⨅ i, I i := by {
  simp [Pi.ker_ringHom, Ideal.ker_mk]
}

def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
  Quotient.lift (⨅ i, I i) (Pi.ringHom fun i : ι ↦ Quotient.mk (I i))
    (by simp [← RingHom.mem_ker, ker_Pi_Quotient_mk])

lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
  chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Quotient.mk (I i) x :=
rfl

lemma chineseMap_mk' (I : ι → Ideal R) (x : R) (i : ι) :
  chineseMap I (Quotient.mk _ x) i = Quotient.mk (I i) x :=
rfl

lemma chineseMap_injective (I : ι → Ideal R) : Injective (chineseMap I) := by {
  rw [chineseMap, injective_lift_iff, ker_Pi_Quotient_mk]
}

lemma coprime_iInf_of_coprime {I : Ideal R} {J : ι → Ideal R} {s : Finset ι} (hf : ∀ j ∈ s, I + J j = 1) :
    I + (⨅ j ∈ s, J j) = 1 := by {
  revert hf
  induction s using Finset.induction with
  | empty =>
      simp
  | @insert i s _ hs =>
      intro h
      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
      set K := ⨅ j ∈ s, J j
      calc
        1 = I + K            := (hs fun j hj ↦ h j (Finset.mem_insert_of_mem hj)).symm
        _ = I + K*(I + J i)  := by rw [h i (Finset.mem_insert_self i s), mul_one]
        _ = (1+K)*I + K*J i  := by ring
        _ ≤ I + K ⊓ J i      := add_le_add mul_le_left mul_le_inf
}

lemma chineseMap_surjective [Fintype ι] {I : ι → Ideal R} (hI : ∀ i j, i ≠ j → I i + I j = 1) :
    Function.Surjective (chineseMap I) := by {
  intro g
  choose f hf using fun i ↦ Quotient.mk_surjective (g i)
  have key : ∀ i, ∃ e : R, Quotient.mk (I i) e = 1 ∧ ∀ j, j ≠ i → Quotient.mk (I j) e = 0 := by {
    intro i
    have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, I i + I j = 1 := by {
      intros j hj
      apply hI
      simpa [ne_comm] using hj
    }
    rcases Ideal.add_eq_one_iff.mp (coprime_iInf_of_coprime hI') with ⟨u, hu, e, he, hue⟩
    refine ⟨e, ?_, ?_⟩
    · simp [eq_sub_of_add_eq' hue, map_sub, Ideal.Quotient.eq_zero_iff_mem.mpr hu]
      rfl
    · intros j hj
      apply Ideal.Quotient.eq_zero_iff_mem.mpr
      simp at he
      tauto
  }
  choose e he using key
  use Quotient.mk _ (∑ i, f i*e i)
  ext i
  rw [chineseMap_mk', map_sum, Finset.sum_univ_eq_single i]
  · simp [(he i).1, hf]
  · intros j hj
    simp [(he j).2 i hj.symm]
}

noncomputable def chineseIso [Fintype ι] (I : ι → Ideal R) (hI : ∀ i j, i ≠ j → I i + I j = 1) :
   (R ⧸ ⨅ i, I i) ≃+* Π i, R ⧸ I i :=
{ Equiv.ofBijective _ ⟨chineseMap_injective I, chineseMap_surjective hI⟩, chineseMap I with }

end Ideal
end chinese

import GlimpseOfLean.Library.Basic
open Set

namespace ClassicalPropositionalLogic

让我们尝试实现一个经典命题逻辑的语言。

注意，这个文件也有一个直观逻辑版本： IntuitionisticPropositionalLogic.lean

def Variable : Type := ℕ

我们定义了命题公式，并为它们制定了一些符号表示。

inductive Formula : Type where
  | var : Variable → Formula
  | bot : Formula
  | conj : Formula → Formula → Formula
  | disj : Formula → Formula → Formula
  | impl : Formula → Formula → Formula

open Formula
local notation:max (priority := high) "#" x:max => var x
local infix:30 (priority := high) " || " => disj
local infix:35 (priority := high) " && " => conj
local infix:28 (priority := high) " ⇒ " => impl
local notation (priority := high) "⊥" => bot

def neg (A : Formula) : Formula := A ⇒ ⊥
local notation:(max+2) (priority := high) "~" x:max => neg x
def top : Formula := ~⊥
local notation (priority := high) "⊤" => top
def equiv (A B : Formula) : Formula := (A ⇒ B) && (B ⇒ A)
local infix:29 (priority := high) " ⇔ " => equiv

我们来定义一个相对于估值的真理，即古典有效性。

@[simp]
def IsTrue (v : Variable → Prop) : Formula → Prop
  | ⊥      => False
  | # P    => v P
  | A || B => IsTrue v A ∨ IsTrue v B
  | A && B => IsTrue v A ∧ IsTrue v B
  | A ⇒ B => IsTrue v A → IsTrue v B

def Satisfies (v : Variable → Prop) (Γ : Set Formula) : Prop := ∀ {A}, A ∈ Γ → IsTrue v A
def Models (Γ : Set Formula) (A : Formula) : Prop := ∀ {v}, Satisfies v Γ → IsTrue v A
local infix:27 (priority := high) " ⊨ " => Models
def Valid (A : Formula) : Prop := ∅ ⊨ A

这里是一些关于有效性的基本属性。

策略 simp 将自动简化标记为 @[simp] 的定义并使用标记为 @[simp] 的定理进行重写。

variable {v : Variable → Prop} {A B : Formula}
@[simp] lemma isTrue_neg : IsTrue v ~A ↔ ¬ IsTrue v A := by simp

@[simp] lemma isTrue_top : IsTrue v ⊤ := by {
  -- sorry
  simp
  -- sorry
}

@[simp] lemma isTrue_equiv : IsTrue v (A ⇔ B) ↔ (IsTrue v A ↔ IsTrue v B) := by {
  -- sorry
  simp
  tauto
  -- sorry
}

作为一个练习，让我们证明（使用经典逻辑）双重否定消除原则。 by_contra h 可能对证明悖论有所帮助。

example : Valid (~~A ⇔ A) := by {
  -- sorry
  intros v _
  simp
  tauto
  -- sorry
}

@[simp] lemma satisfies_insert_iff : Satisfies v (insert A Γ) ↔ IsTrue v A ∧ Satisfies v Γ := by {
  simp [Satisfies]
}

我们首先定义经典逻辑下的可证性。

section
set_option hygiene false -- this is a hacky way to allow forward reference in notation
local infix:27 " ⊢ " => ProvableFrom

Γ ⊢ A 是一个谓词，表示有一个假设来自 Γ，结论为 A 的证明树。这是经典逻辑中自然推理的典型规则列表。

inductive ProvableFrom : Set Formula → Formula → Prop
  | ax    : ∀ {Γ A},   A ∈ Γ   → Γ ⊢ A
  | impI  : ∀ {Γ A B},  insert A Γ ⊢ B                → Γ ⊢ A ⇒ B
  | impE  : ∀ {Γ A B},           Γ ⊢ (A ⇒ B) → Γ ⊢ A  → Γ ⊢ B
  | andI  : ∀ {Γ A B},           Γ ⊢ A       → Γ ⊢ B  → Γ ⊢ A && B
  | andE1 : ∀ {Γ A B},           Γ ⊢ A && B           → Γ ⊢ A
  | andE2 : ∀ {Γ A B},           Γ ⊢ A && B           → Γ ⊢ B
  | orI1  : ∀ {Γ A B},           Γ ⊢ A                → Γ ⊢ A || B
  | orI2  : ∀ {Γ A B},           Γ ⊢ B                → Γ ⊢ A || B
  | orE   : ∀ {Γ A B C}, Γ ⊢ A || B → insert A Γ ⊢ C → insert B Γ ⊢ C → Γ ⊢ C
  | botC  : ∀ {Γ A},   insert ~A Γ ⊢ ⊥                → Γ ⊢ A

end

local infix:27 (priority := high) " ⊢ " => ProvableFrom

一种公式被证明是正确的，如果存在一个

proof tree

证明树

such that

使得

The leaves of the proof tree correspond to axioms
The internal nodes of the proof tree correspond to inference rules
证明树的叶子对应着公理
证明树的内部节点对应于推理规则

This proof tree can be represented as a mudule where each internal node corresponds to an instance, like Prop α, and each leaf corresponds to a definition, like axioms_1 : Prop α.

这个证明树可以被表示为一个模块，其中每个内部节点对应一个实例，例如 Prop α，每个树叶对应一个定义，比如 axioms_1 : Prop α。

instance inference_rules_1 : Prop α :=
begin apply axioms_1 end

实例 inference_rules_1 : Prop α :=
开始 应用 axioms_1 结束

Note that the proof tree can be likened to the definition of a programming function: a concise description of a very large and potentially unbounded computation. The computational content of the proof tree, known as the Curry-Howard correspondence, is what makes interactive theorem proving in Lean so powerful.

注意，该证明树可以类比于编程函数的定义：简洁地描述了非常大且可能无界的计算。证明树的计算内容，被称为 Curry-Howard correspondence ，这是使得在 Lean 中的交互式定理证明如此强大的原因。

def inference_rules_2 : Prop β → Prop γ :=
begin apply inference_rules_1 end

定义 inference_rules_2 : Prop β → Prop γ :=
开始 应用 inference_rules_1 结束

def Provable (A : Formula) := ∅ ⊢ A

export ProvableFrom (ax impI impE botC andI andE1 andE2 orI1 orI2 orE)
variable {Γ Δ : Set Formula}

我们定义了一个简单的策略 apply_ax 来使用 ax 规则证明一些东西。

syntax "solve_mem" : tactic
syntax "apply_ax" : tactic
macro_rules
  | `(tactic| solve_mem) =>
    `(tactic| first | apply mem_insert | apply mem_insert_of_mem; solve_mem
                    | fail "tactic \'apply_ax\' failed")
  | `(tactic| apply_ax)  => `(tactic| { apply ax; solve_mem })

为了熟悉证明系统，让我们来证明以下定理。你可以使用之前定义的 apply_ax 策略，可以证明一个可以用 ax 规则证明的目标。或者你可以手动使用关于 insert 的以下引理。

  mem_insert x s : x ∈ insert x s
  mem_insert_of_mem y : x ∈ s → x ∈ insert y s

example : insert A (insert B ∅) ⊢ A && B := by
  exact andI (ax (mem_insert _ _)) (ax (mem_insert_of_mem _ (mem_insert _ _)))

example : insert A (insert B ∅) ⊢ A && B := by
  exact andI (by apply_ax) (by apply_ax)

example : Provable (~~A ⇔ A) := by {
  -- sorry
  apply andI
  · apply impI
    apply botC
    apply impE _ (by apply_ax)
    apply_ax
  · apply impI
    apply impI
    apply impE (by apply_ax)
    apply_ax
  -- sorry
}

可选练习：证明排除中介的法则。

首先，我们需要在 Lean 中输入的代码：

open classical

variables p : Prop

theorem lem : p ∨ ¬p :=
by_cases
  (assume h : p, or.inl h)
  (assume h : ¬p, or.inr h)

这段代码在 Lean 中表示 "排除中介的法则" 的证明。现在，让我们将它转化成中文理解。

我们先声明一个逻辑命题 p。然后，证明定理 lem，即 p ∨ ¬p，也就是 "p 或者非 p"，这就是所谓的 "排除中介的法则"。

我们使用 by_cases 策略，这是一个基于反证法的策略，允许我们考虑两种可能，一种是 p 成立，一种是 p 不成立。

如果 p 成立，那么我们可以使用 or.inl 来表示 p ∨ ¬p 是因为 p 成立而成立。
另一种情况，假设 p 不成立（即 ¬p），那么我们可以使用 or.inr 来表示 p ∨ ¬p 是因为 ¬p 成立而成立。

上述代码完成了 "排除中介的法则" 的证明。

example : Provable (A || ~A) := by {
  -- sorry
  apply botC
  apply impE (by apply_ax)
  apply orI2
  apply impI
  apply impE (by apply_ax)
  apply orI1 (by apply_ax)
  -- sorry
}

可选练习：证明其中一个德摩根定律。如果你希望称 impE 公理的参数 A 为 X && Y，你可以使用 impE (A := X && Y) 来实现。

example : Provable (~(A && B) ⇔ ~A || ~B) := by {
  -- sorry
  apply andI
  · apply impI
    apply botC
    apply impE (A := A && B) (by apply_ax)
    apply andI
    · apply botC
      apply impE (A := _ || _) (by apply_ax)
      apply orI1 (by apply_ax)
    · apply botC
      apply impE (A := _ || _) (by apply_ax)
      apply orI2 (by apply_ax)
  · apply impI
    apply impI
    apply orE (by apply_ax)
    · apply impE (by apply_ax)
      apply andE1 (by apply_ax)
    · apply impE (by apply_ax)
      apply andE2 (by apply_ax)
  -- sorry
}

你可以使用 归纳法 在 h 上进行以下证明。你可能需要告诉 Lean，你希望一次性证明所有的 Δ，通过使用 对 h 进行归纳，同时泛化 Δ。如果你不显式地命名它们，Lean 会将创建的假设标记为无法访问（标记为 †）。您可以使用例如 rename_i ih 或 rename_i A B h ih来命名最后的不可访问变量。或者你可以使用 case impI ih => <proof> 来证明特定的例子。你可能需要使用引理 insert_subset_insert : s ⊆ t → insert x s ⊆ insert x t。

lemma weakening (h : Γ ⊢ A) (h2 : Γ ⊆ Δ) : Δ ⊢ A := by {
  -- sorry
  induction h generalizing Δ
  case ax => apply ax; solve_by_elim
  case impI ih => apply impI; solve_by_elim [insert_subset_insert]
  case impE ih₁ ih₂ => apply impE <;> solve_by_elim
  case andI ih₁ ih₂ => apply andI <;> solve_by_elim
  case andE1 ih => apply andE1 <;> solve_by_elim
  case andE2 ih => apply andE2 <;> solve_by_elim
  case orI1 ih => apply orI1; solve_by_elim
  case orI2 ih => apply orI2; solve_by_elim
  case orE ih₁ ih₂ ih₃ => apply orE <;> solve_by_elim [insert_subset_insert]
  case botC ih => apply botC; solve_by_elim [insert_subset_insert]
  -- sorry
}

使用 apply? 策略来找到声明 Γ ⊆ insert x Γ 的引理。你可以在右边的面板中点击蓝色的建议，以自动应用这个建议。

lemma ProvableFrom.insert (h : Γ ⊢ A) : insert B Γ ⊢ A := by {
  -- sorry
  apply weakening h
  -- use `apply?` here
  exact subset_insert B Γ
  -- sorry
}

证明演绎定理现在变得容易了。

lemma deduction_theorem (h : Γ ⊢ A) : insert (A ⇒ B) Γ ⊢ B := by {
  -- sorry
  intros
  apply impE (ax $ mem_insert _ _)
  exact h.insert
  -- sorry
}


lemma Provable.mp (h1 : Provable (A ⇒ B)) (h2 : Γ ⊢ A) : Γ ⊢ B := by {
  -- sorry
  apply impE _ h2
  apply weakening h1
  -- apply?
  exact empty_subset Γ
  -- sorry
}

你需要使用策略 left 和 right 来证明一个析取式，并且如果 h 是一个析取式，你需要使用策略 cases h 来做情冱分析。

theorem soundness_theorem (h : Γ ⊢ A) : Γ ⊨ A := by {
  -- sorry
  induction h <;> intros v hv
  solve_by_elim
  case impI ih => intro hA; apply ih; simp [*]
  case impE ih₁ ih₂ => exact ih₁ hv (ih₂ hv)
  case botC ih => by_contra hA; apply ih (satisfies_insert_iff.mpr ⟨by exact hA, hv⟩)
  case andI ih₁ ih₂ => exact ⟨ih₁ hv, ih₂ hv⟩
  case andE1 ih => exact (ih hv).1
  case andE2 ih => exact (ih hv).2
  case orI1 ih => exact .inl (ih hv)
  case orI2 ih => exact .inr (ih hv)
  case orE ih₁ ih₂ ih₃ => refine (ih₁ hv).elim (fun hA => ih₂ ?_) (fun hB => ih₃ ?_) <;> simp [*]
  -- sorry
}

theorem valid_of_provable (h : Provable A) : Valid A := by {
  -- sorry
  exact soundness_theorem h
  -- sorry
}

如果你愿意，现在可以尝试这些更长的项目。

证明完整性：如果一个公式是有效的，那么它是可证明的这是这个证明的一种可能策略：

如果一个公式是有效的，那么它的否定规范形式（NNF）也是有效的；
如果一个处于 NNF 的公式是有效的，那么它的合取范式（CNF）也是有效的；
如果一个处于 CNF 的公式是有效的，那么它就是语法上的有效：所有的子句都包含 A 和 ¬ A，对某个 A 来说（或者包含 ⊤）；
如果一个处于 CNF 的公式在语法上是有效的，那么它是可证明的；
如果一个处于 NNF 的公式的 CNF 是可证明的，那么该公式本身也是可证明的；
如果一个公式的 NNF 是可证明的，那么该公式本身也是可证明的。

定义 Gentzen's 的顺序演算法，用于命题逻辑，并证明这导致了相同的可证明性。

end ClassicalPropositionalLogic

import GlimpseOfLean.Library.Basic

open PiNotation

抽象非理性 101：伽罗瓦伴随

在这个文件中，我们将探讨最简单的伴随之例子：完全格之间的伽罗瓦连接。mathlib中有很多关于这个话题的内容，但在这里，我们将自己动手实践。这个文件构建了这些对象的基础理论，你在那里证明的每一个引理都有名字，并且可以重复使用，以证明下一个引理。

namespace Tutorial

section InfSup
variable [PartialOrder X]

在这一部分，X 是一个装备有偏序关系的类型。因此，你可以访问下列引理：

le_rfl {a : X} : a ≤ a
le_trans {a b c : X} (h : a ≤ b) (h' : b ≤ c) : a ≤ c
le_antisymm {a b : X} (h : a ≤ b) (h' : b ≤ a) : a = b

花括号（）中的参数表示这些参数是隐式的，Lean 将从上下文中推断出这些参数。

一个元素 x₀ 是集合 s 在 X中的下确界，当且仅当，X 中的每一个元素作为 s 的下界，都必须小于或等于 x₀。

def isInf (s : Set X) (x₀ : X) :=
  ∀ x, x ∈ lowerBounds s ↔ x ≤ x₀

lemma isInf.lowerBound {s : Set X} {x₀ : X} (h : isInf s x₀) : x₀ ∈ lowerBounds s := by {
  -- sorry
  rw [h]
  -- sorry
}

一个集合最多只有一个下确界。

def isInf.eq {s : Set X} {x₀ x₁ : X} (hx₀ : isInf s x₀) (hx₁ : isInf s x₁) : x₀ = x₁ := by {
  -- sorry
  apply le_antisymm
  · exact (hx₁ _).1 ((hx₀ _).2 le_rfl)
  · exact (hx₀ _).1 ((hx₁ _).2 le_rfl)
  -- sorry
}

一个元素 x₀ 是集合 s 在 X 中的上确界，当且仅当它低于 x₀ 的每一个 X 的元素都是 s 的下界。

def isSup (s : Set X) (x₀ : X) :=
  ∀ x, x ∈ upperBounds s ↔ x₀ ≤ x

下一个引理的证明是通过将 isInf.lowerBound 应用于配备了相反顺序关系的 X 来完成的。你不需要精确理解如何实现这一点，因为所有使用这个技巧的证明都会提供给你。

lemma isSup.upperBound {s : Set X} {x₀ : X} (h : isSup s x₀) : x₀ ∈ upperBounds s :=
  isInf.lowerBound (X := OrderDual X) h

一个集合最多只有一个上确界。

lemma isSup.eq {s : Set X} {x₀ x₁ : X} (hx₀ : isSup s x₀) (hx₁ : isSup s x₁) : x₀ = x₁ :=
  isInf.eq (X := OrderDual X) hx₀ hx₁

一个从 Set X 到 X 的函数是一个下确界函数，如果它将每个集合映射到这个集合的下确界。

def isInfFun (I : Set X → X) :=
  ∀ s : Set X, isInf s (I s)

一个从 集合 X 到 X 的函数是极大值函数，如果它把每个集合映射到该集合的极大值。

def isSupFun (S : Set X → X) :=
  ∀ s : Set X, isSup s (S s)

下个引理是本文件的第一个关键结果。如果 X 承认一个下确界函数，那么它自动承认一个上确界函数。

lemma isSup_of_isInf {I : Set X → X} (h : isInfFun I) : isSupFun (fun s ↦ I (upperBounds s)) := by {
  -- sorry
  intro s x
  constructor
  · intro hx
    exact (h _).lowerBound hx
  · intros hx y hy
    calc
      y ≤ I (upperBounds s) := (h _ y).mp (fun z hz ↦ hz hy)
      _ ≤ x                 := hx
  -- sorry
}

当然，我们也有对偶结果，可以从一个最大函数构建一个下确界函数。

lemma isInf_of_isSup {S : Set X → X} (h : isSupFun S) : isInfFun (fun s ↦ S (lowerBounds s)) :=
  isSup_of_isInf (X := OrderDual X) h

我们现在准备好进行本文件的第一个主要定义：完全格。

Markdown 格式：We are now ready for the first main definition of this file: complete lattices.

完全格是一种配备有偏序、下确界函数和上确界函数的类型。例如，配备有包含顺序、交集函数和并集函数的 X = Set Y 就是一个完全格。

class CompleteLattice (X : Type) [PartialOrder X] where
  I : Set X → X
  I_isInf : isInfFun I
  S : Set X → X
  S_isSup : isSupFun S

将完全格 X 转化为对偶格。当使用上述的 OrderDual 技巧时，Lean 将自动采用此构造方式。

instance (X : Type) [PartialOrder X] [CompleteLattice X] : CompleteLattice (OrderDual X) where
  I := CompleteLattice.S (X := X)
  I_isInf := CompleteLattice.S_isSup (X := X)
  S := CompleteLattice.I (X := X)
  S_isSup := CompleteLattice.I_isInf (X := X)

我们现在可以使用上述的第一个主要结果，从一个部分排序类型的最小值功能或最大值功能构建一个完整的格结构。

从部分有序类型的下确界函数构建完全格构造。

这篇笔记解释如何从给定的部分有序类型 型 上的一个下确界函数，如何构建一个完全格的结构。

前提

我们从一个部分有序集开始 α ，并给出一个 α 上的函数 inf ，它对每个 α 的集合给出一个元素，这个元素应满足下确界的条件。我们将此函数应用到非空有界集上。

α 上的偏序定义了一个二元关系 ≤ ，其具有反身性（每个元素都对自身有序）、反对称性（如果 a ≤ b 并且 b ≤ a ，那么 a = b ）和传递性（如果 a ≤ b 并且 b ≤ c ，那么 a ≤ c ）。

一个元素 a 是集合 s 的下确界，如果它满足两个条件：

a 是 s 中所有元素的下界。这就是说，对于所有的 x ∈ s ，我们有 a ≤ x 。
如果 b 是 s 的任何下界，那么 a 不小于 b 。也就是说，如果对于所有的 x ∈ s ，我们有 b ≤ x ，那么 a ≤ b 。

我们的目标是使用 inf 函数来构建一个完全格。一个完全格是一个满足以下条件的格：

任意两个元素都有公共下界和公共上界
非空有界子集都有确界和下确界。

构造方法

为了实现我们的目标，我们定义了新的上限 sup 和完全格结构。

我们可以定义 sup s 为所有 s 的上界的下确界。由于之前的偏序关系和 inf 函数很容易验证：如果一个元素 a 是集合中所有元素的上界，那么它就是这些元素的上确界。

结合下确界和上确界，我们可以为 α 定义一个完全格结构。我们可以使用 lean 的助手函数 lattice.complete_lattice_of_Inf 来实现这个构造。

这个构造的正确性依赖于下确界的定义和上确界的存在性。这个定义保证了对于任何集合 s ，都存在一个元素 a 是 s 的下确界。而上确界的存在性确保了任何非空有界的 s 都有一个上确界。结合这两点，可以确保我们可以为 α 构建一个完全格的结构。

def CompleteLattice.mk_of_Inf {I : Set X → X} (h : isInfFun I) : CompleteLattice X where
 I := I
 I_isInf := h
 S := fun s ↦ I (upperBounds s)
 S_isSup := isSup_of_isInf h

在部分排序类型上从一个最大上界函数构建一个完全格结构。

Markdown格式：

在部分排序类型上从一个最大上界函数构建一个完全格结构。

def CompleteLattice.mk_of_Sup {S : Set X → X} (h : isSupFun S) : CompleteLattice X where
 I := fun s ↦ S (lowerBounds s)
 I_isInf := isInf_of_isSup h
 S := S
 S_isSup := h

在本节结束之前，X 将是一个完全格。

variable [CompleteLattice X]

在一个完全格上的下确界函数。

在一个完全格 (complete lattice) 上，对任意的集合都存在一个下确界 (infimum) 和上确界 (supremum)。

定理

在完全格 L 上，下确界函数 inf 实际是一个格同态。

证明：

为了证明 inf 函数是一个格同态，我们需要展示以下两点：

inf(a, b) = a ∧ b
inf(a ∨ b) = inf(a) ∨ inf(b)

对于第一点，由于 a, b 是 L 中的任意元素，a ∧ b 就是 a, b 的下确界，因此 inf(a, b) = a ∧ b。

对于第二点，我们要展示 inf(a ∨ b) = inf(a) ∨ inf(b)。为此，我们需要引用到完全格的定义，按照定义，对于任意的子集 S，如果 S 的所有元素都小于等于某个元素 x，则 x 就是 S 的上确界。

如果 c 是 a ∨ b 的下确界，那么我们有 c ≤ a 和 c ≤ b。因此，c 也是 a, b 的下确界，也就是说 c ≤ inf(a, b)。另一方面，既然 inf(a, b) 是 a 和 b 的下确界，我们有 inf(a, b) ≤ a 和 inf(a, b) ≤ b 。由于 a ∨ b 是 a 和 b 的上确界，我们可以推断出 inf(a, b) ≤ a ∨ b ，也就是 inf(a, b) 是 a ∨ b 的下确界，即 inf(a ∨ b) = inf(a) ∨ inf(b)。

至此，我们证明了在完全格上，下确界函数 inf 是一个格同态。

notation "Inf" => CompleteLattice.I

在一个完整的格子上的最大上界函数。

notation "Sup" => CompleteLattice.S

我们现在以完全格言来重新陈述一些上述已证明的引理。

lemma lowerBound_Inf (s : Set X) : Inf s ∈ lowerBounds s :=
  (CompleteLattice.I_isInf _).lowerBound

lemma upperBound_Sup (s : Set X) : Sup s ∈ upperBounds s :=
  (CompleteLattice.S_isSup _).upperBound

我们现在证明一系列的引理，断言 Inf （然后通过对偶性 Sup）符合你的直觉。如果你觉得你能够证明它们，想看更有趣的东西，你可以随意跳过这些，直接跳到伴随部分。

在下面的第一个引理中，你可能会想使用 lowerBounds_mono_set ⦃s t : Set α⦄ (hst : s ⊆ t) : lowerBounds t ⊆ lowerBounds s 或者再次证明它作为你的证明的一部分。

lemma Inf_subset {s t : Set X} (h : s ⊆ t): Inf t ≤ Inf s := by {
  -- sorry
  apply (CompleteLattice.I_isInf s _).1
  apply lowerBounds_mono_set h
  exact lowerBound_Inf t
  -- sorry
}

lemma Sup_subset {s t : Set X} (h : s ⊆ t): Sup s ≤ Sup t :=
  Inf_subset (X := OrderDual X) h

lemma Inf_pair {x x' : X} : x ≤ x' ↔ Inf {x, x'} = x := by {
  -- sorry
  constructor
  · intro h
    apply (CompleteLattice.I_isInf _).eq
    intro z
    constructor
    · intro hz
      apply hz
      simp
    · intro hz
      simp [hz, hz.trans h]
  · intro h
    rw [← h]
    apply lowerBound_Inf
    simp
  -- sorry
}

lemma Sup_pair {x x' : X} : x ≤ x' ↔ Sup {x, x'} = x' := by {
  rw [Set.pair_comm x x']
  exact Inf_pair (X := OrderDual X)
}

lemma Inf_self_le (x : X) : Inf {x' | x ≤ x'} = x := by {
  -- sorry
  apply (CompleteLattice.I_isInf _).eq
  intro x'
  constructor
  · intro h
    exact h le_rfl
  · intro h x'' hx''
    exact h.trans hx''
  -- sorry
}

lemma Sup_le_self (x : X) : Sup {x' | x' ≤ x} = x :=
  Inf_self_le (X := OrderDual X) x

让我们证明 Set 构成一个完全格。

完全格中的`Set`证明

定义

在秩序理论中，一个集合形成一个 完全格 ，如果对于该集合中任何子集，该子集的上有界集和下有界集都存在。

证明

我们需要证明对于任何给定的 Set，其最小边界（inf）和最大边界（sup）都存在。

对于一个空 Set ，最小边界是全体集合（所有的元素），最大边界是空集（没有元素）。
对于一个非空 Set ，最小边界是 Set 中所有元素的交集，最大边界是 Set 中所有元素的并集。

因此，以这种方式定义的 Set ，它的上下边界始终存在，所以 Set 构成一个完全格。

请注意，这只是一个证明的简述，实际的数学证明可能需要更详尽和严谨的论述。

lemma isInfInter {Y : Type} (S : Set (Set Y)) : isInf S (⋂₀ S) := by {
  -- sorry
  intro t
  constructor
  · intro ht x hx u hu
    exact ht hu hx
  · intro ht u hu x hx
    exact ht hx _ hu
  -- sorry
}

lemma isSupUnion {Y : Type} (S : Set (Set Y)) : isSup S (⋃₀ S) := by {
  -- sorry
  intro t
  constructor
  · intro ht x hx
    rcases hx with ⟨s, hs, hx⟩
    exact ht hs hx
  · intro ht u hu x hx
    apply ht
    use u
    tauto
  -- sorry
}

instance {Y : Type} : CompleteLattice (Set Y) where
  I := Set.sInter
  I_isInf := fun S ↦ isInfInter S
  S := Set.sUnion
  S_isSup := fun S ↦ isSupUnion S

end InfSup

section Adjunction

我们现在准备好进行这个文件的第二个核心定义：有序类型之间的伴随。

如果在有序类型之间的一对函数 l 和 r 满足 ∀ x y, l x ≤ y ↔ x ≤ r y，那么它们就是伴随的。也就是说，它们形成了一个伽罗瓦连接。其中，l 代表 "左"，r 代表 "右"。

def adjunction [PartialOrder X] [PartialOrder Y] (l : X → Y) (r : Y → X) :=
  ∀ x y, l x ≤ y ↔ x ≤ r y

你需要记住的例子是直接映射和反向映射之间的伴随。给定 f : α → β，我们有：

Set.image f : Set α → Set β，记作 f ''
Set.preimage f : Set β → Set α，记作 f ⁻¹'

lemma image_preimage_adjunction {α β : Type} (f : α → β) :
    adjunction (Set.image f) (Set.preimage f) := by {
  intros s t
  exact Set.image_subset_iff
}

lemma adjunction.dual [PartialOrder X] [PartialOrder Y] {l : X → Y} {r : Y → X}
    (h : adjunction l r) :
    adjunction (X := OrderDual Y) (Y := OrderDual X) r l := by {
  -- sorry
  intros y x
  exact (h x y).symm
  -- sorry
}

在本节的剩余部分中，X 和 Y 是完全格。

variable [PartialOrder X] [CompleteLattice X] [PartialOrder Y] [CompleteLattice Y]

我们现在来到本文件的第二个主要定理：完全格的伴随函子定理。这个定理指出，完全格之间的函数只有在与 Sup（或者 Inf）交换时才是左伴随（或者右伴随）。

我们首先定义候选的右伴随（在不对原始映射做任何假设的情况下）。

构造一个在完全格子间的映射的候选右伴随。如果映射与 Sup 交换，这就是一个实际的伴随，参见 adjunction_of_Sup 。

def mk_right (l : X → Y) : Y → X := fun y ↦ Sup {x | l x ≤ y}

以下定理的证明并不长，但也不完全显而易见。首先你需要理解声明中的符号。l '' s 是 s 在 l 下的直接映射。这个 '' 是 Set.image 的符号。将你的光标放在这个符号上并使用上下文菜单点击 "跳转到定义"，将会带你到定义 Set.image 并包含许多相关引理的文件。在参考解决方案中使用的引理有：

Set.image_pair : (f : α → β) (a b : α) : f '' {a, b} = {f a, f b}
Set.image_preimage_subset (f : α → β) (s : Set β) : f '' (f ⁻¹' s) ⊆ s

证明提示：有一方向很简单并且不使用关键假设。对于另一方向，你可能应该首先证明 Monotone l，即 ∀ ⦃a b⦄, a ≤ b → l a ≤ l b。

theorem adjunction_of_Sup {l : X → Y} (h : ∀ s : Set X, l (Sup s) = Sup (l '' s)) :
    adjunction l (mk_right l) := by {
  -- sorry
  intro x y
  constructor
  · intro h'
    exact (CompleteLattice.S_isSup {x | l x ≤ y}).upperBound h'
  · intro h'
    have l_mono : Monotone l := by {
      intro a b hab
      have := h {a, b}
      rw [Sup_pair.1 hab, Set.image_pair] at this
      exact Sup_pair.2 this.symm
    }
    calc
      l x ≤ l (mk_right l y) := l_mono h'
      _   = Sup (l '' { x | l x ≤ y }) := h {x | l x ≤ y}
      _   ≤ Sup { y' | y' ≤ y } := Sup_subset (Set.image_preimage_subset l { y' | y' ≤ y })
      _   = y := Sup_le_self y
  -- sorry
}

当然，我们也可以以同样的方式构造左伴随。

Of course we can also provide a "reverse" constructor, mk_opposite.

def mk_opposite (α : Type*) := α

Of notice is the prefix notation, op, which you may guess stands for "opposite".

prefix `op`:max := mk_opposite

Now, we can make op α an instance of has_mul iff α has division.

instance [div : has_div α] : has_mul (op α) :=
{ mul := λ x y, ⟨div x.1 y.1⟩ }

We also need to provide an inv instance if α has multiplication.

instance [mul : has_mul α] : has_inv (op α) :=
{ inv := λ x, ⟨mul x.1 x.1⟩ }

But we can do even better if α has both division and multiplication.

instance [mul_div : has_mul_div α] : has_div_mul (op α) :=
{ ..mul_div.to_has_mul, ..mul_div.to_has_div }

Having done that, we also need to define the instances for addition, subtraction and so on.

不仅如此，我们还可以提供一个“反向”构造函数，mk_opposite。

def mk_opposite (α : Type*) := α

值得注意的是前缀表示法，op，你可能已经猜到，它代表的是“反向”。

prefix `op`:max := mk_opposite

现在，如果 α 有除法，我们可以使 op α 成为 has_mul 的实例。

instance [div : has_div α] : has_mul (op α) :=
{ mul := λ x y, ⟨div x.1 y.1⟩ }

如果 α 有乘法，我们还需要提供一个 inv 实例。

instance [mul : has_mul α] : has_inv (op α) :=
{ inv := λ x, ⟨mul x.1 x.1⟩ }

但是，如果 α 同时有除法和乘法，我们可以做得更好。

instance [mul_div : has_mul_div α] : has_div_mul (op α) :=
{ ..mul_div.to_has_mul, ..mul_div.to_has_div }

做完这些，我们还需要为加法、减法等定义实例。

构建一个完全格之间映射的候选左伴随。如果该映射与 Inf 交换，这就是一个实际的伴随，参见 adjunction_of_Inf。

def mk_left (r : Y → X) : X → Y := fun x ↦ Inf {y | x ≤ r y}

theorem adjunction_of_Inf {r : Y → X} (h : ∀ s : Set Y, r (Inf s) = Inf (r '' s)) :
    adjunction (mk_left r) r :=
  fun x y ↦ (adjunction_of_Sup (X := OrderDual Y) (Y := OrderDual X) h y x).symm

end Adjunction

section Topology

在这一部分，我们将把上述发展的理论应用到点集拓扑学上。我们的首要目标是在给定类型上的拓扑类型 Topology X 上赋予一个完全格结构。然后我们把任何映射 f : X → Y 变成 Topology X 和 Topology Y 之间的伴随 (f⁎, f ^*)，并用它构建乘积拓扑。当然，数学库知道所有这些，但我们将继续构建我们自己的理论。

@[ext]
structure Topology (X : Type) where
  isOpen : Set X → Prop
  isOpen_iUnion : ∀ {ι : Type}, ∀ {s : ι → Set X}, (∀ i, isOpen (s i)) → isOpen (⋃ i, s i)
  isOpen_iInter : ∀ {ι : Type}, ∀ {s : ι → Set X}, (∀ i, isOpen (s i)) → Finite ι → isOpen (⋂ i, s i)

让我们对我们的定义快速进行两次完整性检查，因为许多教科书在定义拓扑空间时都包含了冗余的条件。

lemma isOpen_empty (T : Topology X) : T.isOpen ∅ := by {
  have : (∅ : Set X) = ⋃ i : Empty, i.rec
  · rw [Set.iUnion_of_empty]
  rw [this]
  exact T.isOpen_iUnion Empty.rec
}

lemma isOpen_univ (T : Topology X) : T.isOpen Set.univ := by {
  have : (Set.univ : Set X) = ⋂ i : Empty, i.rec
  · rw [Set.iInter_of_empty]
  rw [this]
  exact T.isOpen_iInter  Empty.rec (Finite.of_fintype Empty)
}

在 Topology 的定义中的 ext 属性告诉 Lean 自动构建以下的延展性引理： Topology.ext_iff (T T' : Topology X), T = T' ↔ x.isOpen = y.isOpen 并且它也为 ext 策略注册了这个引理（我们将在下文中回到这个话题）。

我们使用由 Set (Set X) 引导的顺序的对偶来排序 Topology X。尽管有充分的理由选择这种方式，但它们超出了本教程的范围。

instance : PartialOrder (Topology X) :=
PartialOrder.lift (β := OrderDual $ Set (Set X)) Topology.isOpen (fun T T' ↦ (Topology.ext_iff T T').2)

拓扑 X 上的上确界函数。

def SupTop (s : Set (Topology X)) : Topology X where
  isOpen := fun V ↦ ∀ T ∈ s, T.isOpen V
  isOpen_iUnion := by {
    intros ι t ht a ha
    exact a.isOpen_iUnion fun i ↦ ht i a ha
  }
  isOpen_iInter := by {
    intros ι t ht hι a ha
    exact a.isOpen_iInter (fun i ↦ ht i a ha) hι
}

因为上述的 supremum 函数来源于 OrderDual (Set (Set X)) 的 supremum 函数，它确实是一个 supremum 函数。我们可以陈述一个抽象的引理，但在这里直接证明就很容易，也很有趣。

OrderDual (Set (Set X)) 是把 Set X 视作偏序集然后取对偶得到的新偏序集，其 supremum 函数是原偏序集的 infimum 函数。
一个集合的 supremum 是所有小于等于它的元素集合（闭锁）的最大元素（如果存在的话）。
因此，OrderDual (Set (Set X)) 的 supremum 函数给出了每个集合的下界集合的最大元素，也就是闭锁的最小元素，这符合我们对集合的序基本了解。因此，直接证明该函数是一个 supremum 函数十分直观且有趣。

lemma isSup_SupTop : isSupFun (SupTop : Set (Topology X) → Topology X) :=
fun _ _ ↦ ⟨fun hT _ hV _ hs ↦ hT hs hV, fun hT T' hT' _ hV ↦ hT hV T' hT'⟩

我们可以使用我们的抽象理论来免费获得一个下确界函数，因此在 Topology X 上有一个完备格结构。需要注意的是，我们的抽象理论的确在做非平凡的工作：下确界函数并不来自于 OrderDual (Set (Set X))。

instance : CompleteLattice (Topology X) := CompleteLattice.mk_of_Sup isSup_SupTop

让我们用完全格记法重新阐述我们对 Sup 的构造是什么。这个证明就是简单的说 "这是按定义为真的"。

lemma isOpen_Sup {s : Set (Topology X)} {V : Set X} : (Sup s).isOpen V ↔ ∀ T ∈ s, T.isOpen V :=
  Iff.rfl

我们现在开始通过任意映射 f : X → Y 来构建 Topology X 和 Topology Y 之间的伴随关系。我们会手动构建左伴随，然后调用我们的伴随函子定理。

def push (f : X → Y) (T : Topology X) : Topology Y where
  isOpen := fun V ↦ T.isOpen (f ⁻¹' V)
  isOpen_iUnion := by {
    -- sorry
    intros ι s hs
    rw [Set.preimage_iUnion]
    exact T.isOpen_iUnion hs
    -- sorry
  }
  isOpen_iInter := by {
    -- sorry
    intros ι s hs hι
    rw [Set.preimage_iInter]
    exact T.isOpen_iInter hs hι
    -- sorry
}

postfix:1024 "⁎" => push -- type using `\_*`

一个映射 f : X → Y 相对于拓扑 T 和 T' 是连续的，如果每个开集的原像是开放的。

def Continuous (T : Topology X) (T' : Topology Y) (f : X → Y) :=  f ⁎ T ≤ T'

让我们来确认一下这个定义是否确实表达了我们所声称的内容。

example (T : Topology X) (T' : Topology Y) (f : X → Y) :
  Continuous T T' f ↔ ∀ V, T'.isOpen V → T.isOpen (f ⁻¹' V) :=
Iff.rfl

注意到以下证明使用了 ext 策略，这是由于它知道如果两个拓扑具有相同的开集，那么它们就是相等的，这得益于对 Topology 定义的 ext 属性的应用。

lemma push_push (f : X → Y) (g : Y →Z) (T : Topology X) :
    g ⁎ (f ⁎ T) = (g ∘ f) ⁎ T := by {
  ext V
  exact Iff.rfl
}

我们需要一个与 f ⁎ 相对应的右伴随，因此我们需要检查它与 Sup 是否相交。你可能想使用 Set.ball_image_iff : (∀ y ∈ f '' s, p y) ↔ ∀ x ∈ s, p (f x) 其中 "ball" 代表的是 "bounded for all"，即 ∀ x ∈ ...。

lemma push_Sup (f : X → Y) {t : Set (Topology X)} : f ⁎ (Sup t) = Sup (f ⁎ '' t) := by {
  -- sorry
  ext V
  rw [isOpen_Sup, Set.ball_image_iff]
  exact Iff.rfl
  -- sorry
}

def pull (f : X → Y) (T : Topology Y) : Topology X := mk_right (push f) T

postfix:1024 "^*" => pull

def ProductTopology {ι : Type} {X : ι → Type} (T : Π i, Topology (X i)) : Topology (Π i, X i) :=
Inf (Set.range (fun i ↦ (fun x ↦ x i) ^* (T i)))

lemma ContinuousProductTopIff {ι : Type} {X : ι → Type} (T : Π i, Topology (X i))
  {Z : Type} (TZ : Topology Z) {f : Z → Π i, X i}:
    Continuous TZ (ProductTopology T) f ↔ ∀ i,  Continuous TZ (T i) (fun z ↦ f z i) := by {
  -- sorry
  calc
    Continuous TZ (ProductTopology T) f
    _ ↔ f ⁎ TZ ∈ lowerBounds (Set.range (fun i ↦ (fun x ↦ x i) ^* (T i))) := by {
          rw [CompleteLattice.I_isInf]
          exact Iff.rfl
          }
    _ ↔ ∀ i, f ⁎ TZ ≤ (fun x ↦ x i) ^* (T i)        := by rw [lowerBounds_range]
    _ ↔ ∀ i, (fun x ↦ x i) ⁎ (f ⁎ TZ) ≤ T i        := by {
          apply forall_congr'
          intro i
          rw [pull, ← adjunction_of_Sup (fun s ↦ push_Sup _), push_push]
          }
    _ ↔ ∀ i,  Continuous TZ (T i) (fun z ↦ f z i)  := Iff.rfl

展开 Continuous ProductTopology rw [← CompleteLattice.I_isInf, lowerBounds_range] 应用 forall_congr' 引入 i 展开 pull rw [← adjunction_of_Sup (fun s ↦ push_Sup _), push_push] rfl

-- sorry
}

end Topology

namespace Subgroups

@[ext]
structure Subgroup (G : Type) [Group G] where
  carrier : Set G
  one_mem : 1 ∈ carrier
  mul_mem : ∀ ⦃x y : G⦄, x ∈ carrier → y ∈ carrier → x*y ∈ carrier
  inv_mem : ∀ ⦃x : G⦄, x ∈ carrier → x⁻¹ ∈ carrier

instance [Group G] : Membership G (Subgroup G) := ⟨fun x H ↦ x ∈ H.carrier⟩

variable {G : Type} [Group G]

instance : PartialOrder (Subgroup G) :=
  PartialOrder.lift Subgroup.carrier (fun H H' ↦ (Subgroup.ext_iff H H').2)

一个群的交集是一个子群。

def SubgroupInf (s : Set (Subgroup G)) : Subgroup G where
  carrier := ⋂ H ∈ s, H.carrier
  one_mem := by {
    -- sorry
    rw [Set.mem_iInter₂]
    intro H _
    exact H.one_mem
    -- sorry
  }
  mul_mem := by {
    -- sorry
    intro x y hx hy
    rw [Set.mem_iInter₂] at hx hy ⊢
    intro H hH
    exact H.mul_mem (hx H hH) (hy H hH)
    -- sorry
  }
  inv_mem := by {
    -- sorry
    intro x hx
    rw [Set.mem_iInter₂] at hx ⊢
    intro H hH
    exact H.inv_mem (hx H hH)
    -- sorry
  }

lemma SubgroupInf_carrier (s : Set (Subgroup G)) :
  (SubgroupInf s).carrier = ⋂₀ (Subgroup.carrier '' s) :=
by simp [SubgroupInf]
-- omit

lemma isInf.lift [PartialOrder X] {f : Y → X} (hf : Function.Injective f) {s : Set Y} {y : Y}
  (hy : isInf (f '' s) (f y)) : @isInf Y (PartialOrder.lift f hf) s y := by {
  intro y'
  erw [← hy (f y')]
  constructor
  · intro hy' x hx
    rcases hx with ⟨y'', hy'', H⟩
    rw [← H]
    exact hy' hy''
  · intro hy' y'' hy''
    apply hy'
    exact Set.mem_image_of_mem f hy''
}

-- omit
lemma SubgroupInf_is_Inf : isInfFun (SubgroupInf : Set (Subgroup G) → Subgroup G) := by {
  -- sorry
  intro s H
  apply isInf.lift (fun H H' ↦ (Subgroup.ext_iff H H').2)
  rw [SubgroupInf_carrier]
  apply isInfInter
  -- sorry
}

instance : CompleteLattice (Subgroup G) := CompleteLattice.mk_of_Inf SubgroupInf_is_Inf

lemma Inf_carrier (s : Set (Subgroup G)) : (Inf s).carrier = ⋂₀ (Subgroup.carrier '' s) :=
  SubgroupInf_carrier s

def forget (H : Subgroup G) : Set G := H.carrier

def generate : Set G → Subgroup G := mk_left forget

lemma generate_forget_adjunction : adjunction (generate : Set G → Subgroup G) forget := by {
  -- sorry
  exact adjunction_of_Inf SubgroupInf_carrier
  -- sorry
}

variable {G' : Type} [Group G']

def pull (f : G →* G') (H' : Subgroup G') : Subgroup G where
  carrier := f ⁻¹' H'.carrier
  one_mem := by {
    -- sorry
    show f 1 ∈ H'
    rw [f.map_one]
    exact H'.one_mem
    -- sorry
  }
  mul_mem := by {
    -- sorry
    intro x y hx hy
    show f (x*y) ∈ H'
    rw [f.map_mul]
    exact H'.mul_mem hx hy
    -- sorry
  }
  inv_mem := by {
    -- sorry
    intro x hx
    show f x⁻¹ ∈ H'
    rw [f.map_inv]
    exact H'.inv_mem hx
    -- sorry
  }

lemma pull_carrier (f : G →* G') (H' : Subgroup G') : (pull f H').carrier = f ⁻¹' H'.carrier :=
  rfl

让我们真正偷懒，通过伴随性定义子群的正向推导。

def push (f : G →* G') : Subgroup G → Subgroup G' := mk_left (pull f)

lemma push_pull_adjunction (f : G →* G') : adjunction (push f) (pull f) := by {
  -- sorry
  apply adjunction_of_Inf
  intro S
  ext x
  simp [Inf_carrier, Set.image_image, pull, Set.preimage_iInter]
  -- sorry
}

end Subgroups

section

我们的下一个具体目标是 push_generate (f : G →* G') (S : Set G) : push f (generate S) = generate (f '' S)

这将需要几个更抽象的引理。

variable {X : Type} [PartialOrder X] [CompleteLattice X]
         {Y : Type} [PartialOrder Y] [CompleteLattice Y]

lemma unique_left {l l' : X → Y} {r : Y → X} (h : adjunction l r) (h' : adjunction l' r) :
    l = l' := by {
  -- sorry
  ext x
  apply le_antisymm
  · rw [h, ← h']
  · rw [h', ← h]
  -- sorry
}

lemma unique_right {l : X → Y} {r r' : Y → X} (h : adjunction l r) (h' : adjunction l r') :
    r = r' := by {
  -- sorry
  exact (unique_left h'.dual h.dual).symm
  -- sorry
}

variable {Z : Type} [PartialOrder Z] [CompleteLattice Z]

lemma adjunction.compose {l : X → Y} {r : Y → X} (h : adjunction l r)
  {l' : Y → Z} {r' : Z → Y} (h' : adjunction l' r') : adjunction (l' ∘ l) (r ∘ r') := by {
  -- sorry
  intro x z
  rw [Function.comp_apply, h', h]
  rfl
  -- sorry
}

-- omit
lemma left_comm_of_right_comm {W : Type} [PartialOrder W] {Z : Type} [PartialOrder Z]
    {lYX : X → Y} {uXY : Y → X} (hXY : adjunction lYX uXY)
    {lWZ : Z → W} {uZW : W → Z} (hZW : adjunction lWZ uZW)
    {lWY : Y → W} {uYW : W → Y} (hWY : adjunction lWY uYW)
    {lZX : X → Z} {uXZ : Z → X} (hXZ : adjunction lZX uXZ)
    (h : uXZ ∘ uZW = uXY ∘ uYW) : lWZ ∘ lZX = lWY ∘ lYX := by {
  have A₁
  · exact hXZ.compose hZW
  rw [h] at A₁
  exact unique_left A₁ (hXY.compose hWY)
}
-- omit

end

namespace Subgroups
variable {G : Type} [Group G] {G' : Type} [Group G']

作为最后的挑战，我们提出以下引理。

群态射下，由某些集合 S 生成的子群的像，由 S 的像生成。

lemma push_generate (f : G →* G') : push f ∘ generate = generate ∘ (Set.image f) := by {
  -- sorry
  apply left_comm_of_right_comm
  apply image_preimage_adjunction
  apply push_pull_adjunction
  apply generate_forget_adjunction
  apply generate_forget_adjunction
  ext H
  exact Iff.rfl
  -- sorry
}

end Subgroups
end Tutorial

import GlimpseOfLean.Library.Basic
open Set

namespace IntuitionisticPropositionalLogic

我们试图实现直觉主义命题逻辑的语言。

注意，这个文件也有一个经典逻辑版本：ClassicalPropositionalLogic.lean

def Variable : Type := ℕ

我们定义了命题公式，并为它们制定了一些符号表示法。

inductive Formula : Type where
  | var : Variable → Formula
  | bot : Formula
  | conj : Formula → Formula → Formula
  | disj : Formula → Formula → Formula
  | impl : Formula → Formula → Formula

open Formula
local notation:max (priority := high) "#" x:max => var x
local infix:30 (priority := high) " || " => disj
local infix:35 (priority := high) " && " => conj
local infix:28 (priority := high) " ⇒ " => impl

def neg (A : Formula) : Formula := A ⇒ bot
local notation:(max+2) (priority := high) "~" x:max => neg x
def top := ~bot
def equiv (A B : Formula) : Formula := (A ⇒ B) && (B ⇒ A)
local infix:29 (priority := high) " ⇔ " => equiv

接下来我们定义海廷代数语义学。

在海廷代数H中的估值只是一个从变量到H的映射我们来定义如何对命题公式进行估值评估。

variable {H : Type _} [HeytingAlgebra H]
@[simp]
def eval (v : Variable → H) : Formula → H
  | bot    => ⊥
  | # P    => v P
  | A || B => eval v A ⊔ eval v B
  | A && B => eval v A ⊓ eval v B
  | A ⇒ B => eval v A ⇨ eval v B

我们称 A 是 Γ 的一个推断，如果对于任何 Heyting 代数中的所有取值，如果 eval v B 对于所有 B ∈ Γ 都高于某个元素，那么 eval v A 也高于这个元素。注意，对于有限集 Γ，这正好对应于 Infimum { eval v B | B ∈ Γ } ≤ eval v A。这个 "yoneda'd" 版本的有效性定义非常方便我们使用。

def Models (Γ : Set Formula) (A : Formula) : Prop :=
  ∀ {H : Type} [HeytingAlgebra H] {v : Variable → H} {c}, (∀ B ∈ Γ, c ≤ eval v B) → c ≤ eval v A

local infix:27 (priority := high) " ⊨ " => Models
def Valid (A : Formula) : Prop := ∅ ⊨ A

下面是一些有效性的基本属性。

simp 策略会自动简化标记为 @[simp] 的定义，并使用标记为 @[simp] 的定理进行重写。

variable {v : Variable → H} {A B : Formula}
@[simp] lemma eval_neg : eval v ~A = (eval v A)ᶜ := by simp

@[simp] lemma eval_top : eval v top = ⊤ := by {
  -- sorry
  simp
  -- sorry
}

@[simp]
lemma isTrue_equiv : eval v (A ⇔ B) = (eval v A ⇨ eval v B) ⊓ (eval v B ⇨ eval v A) := by {
  -- sorry
  simp
  -- sorry
}

作为一个练习，我们来证明以下命题，这在直观逻辑中是成立的。

example : Valid (~(A && ~A)) := by {
  -- sorry
  simp [Valid, Models]
  -- sorry
}

让我们以直觉逻辑来定义可证明性。

section
set_option hygiene false -- this is a hacky way to allow forward reference in notation
local infix:27 " ⊢ " => ProvableFrom

Γ ⊢ A 是一个谓词，表示有一个以 A 作为结论的证明树，其假设来自于 Γ。这是直觉主义逻辑自然演绎的典型规则列表。

inductive ProvableFrom : Set Formula → Formula → Prop
  | ax    : ∀ {Γ A},   A ∈ Γ   → Γ ⊢ A
  | impI  : ∀ {Γ A B},  insert A Γ ⊢ B                → Γ ⊢ A ⇒ B
  | impE  : ∀ {Γ A B},           Γ ⊢ (A ⇒ B) → Γ ⊢ A  → Γ ⊢ B
  | andI  : ∀ {Γ A B},           Γ ⊢ A       → Γ ⊢ B  → Γ ⊢ A && B
  | andE1 : ∀ {Γ A B},           Γ ⊢ A && B           → Γ ⊢ A
  | andE2 : ∀ {Γ A B},           Γ ⊢ A && B           → Γ ⊢ B
  | orI1  : ∀ {Γ A B},           Γ ⊢ A                → Γ ⊢ A || B
  | orI2  : ∀ {Γ A B},           Γ ⊢ B                → Γ ⊢ A || B
  | orE   : ∀ {Γ A B C}, Γ ⊢ A || B → insert A Γ ⊢ C → insert B Γ ⊢ C → Γ ⊢ C
  | botE  : ∀ {Γ A},             Γ ⊢ bot              → Γ ⊢ A

end

local infix:27 (priority := high) " ⊢ " => ProvableFrom
def Provable (A : Formula) := ∅ ⊢ A

export ProvableFrom (ax impI impE botE andI andE1 andE2 orI1 orI2 orE)
variable {Γ Δ : Set Formula}

syntax "solve_mem" : tactic
syntax "apply_ax" : tactic
macro_rules
  | `(tactic| solve_mem) => `(tactic| first | apply mem_insert | apply mem_insert_of_mem; solve_mem)
  | `(tactic| apply_ax)  => `(tactic| { apply ax; solve_mem })

为了熟悉证明系统，让我们证明以下内容。你可以使用前面定义的 apply_ax 策略，该策略可以证明一个可以通过 ax 规则证明的目标。或者你可以手动操作，使用以下关于插入的引理。

  mem_insert x s : x ∈ insert x s
  mem_insert_of_mem y : x ∈ s → x ∈ insert y s

example : Provable ((~A || ~B) ⇒ ~(A && B)) := by {
  -- sorry
  apply impI
  apply impI
  apply orE (by apply_ax)
  · apply impE (by apply_ax)
    apply andE1 (by apply_ax)
  · apply impE (by apply_ax)
    apply andE2 (by apply_ax)
  -- sorry
}

可选练习

example : Provable (~(A && ~A)) := by {
  -- sorry
  apply impI
  exact impE (andE2 (by apply_ax)) (andE1 (by apply_ax))
  -- sorry
}

可选练习

example : Provable ((~A && ~B) ⇒ ~(A || B)) := by {
  -- sorry
  apply impI
  apply impI
  apply orE (by apply_ax)
  · exact impE (andE1 (by apply_ax)) (by apply_ax)
  · exact impE (andE2 (by apply_ax)) (by apply_ax)
  -- sorry
}

你可以使用 归纳法 在 h 上进行以下证明。你可能会希望告诉 Lean ，你希望同时为所有的 Δ 进行证明，可以使用 induction h generalizing Δ 来实现。 Lean 会将你没有明确命名的假设标记为不可访问（用 † 标记）。例如你可以使用 rename_i ih 或 rename_i A B h ih 来为最后的不可访问变量命名。或者你可以使用 case impI ih => <proof> 来证明特定的情况。你可能需要使用这个引理 insert_subset_insert : s ⊆ t → insert x s ⊆ insert x t。

lemma weakening (h : Γ ⊢ A) (h2 : Γ ⊆ Δ) : Δ ⊢ A := by {
  -- sorry
  induction h generalizing Δ
  case ax => apply ax; solve_by_elim
  case impI ih => apply impI; solve_by_elim [insert_subset_insert]
  case impE ih₁ ih₂ => apply impE <;> solve_by_elim
  case andI ih₁ ih₂ => apply andI <;> solve_by_elim
  case andE1 ih => apply andE1 <;> solve_by_elim
  case andE2 ih => apply andE2 <;> solve_by_elim
  case orI1 ih => apply orI1; solve_by_elim
  case orI2 ih => apply orI2; solve_by_elim
  case orE ih₁ ih₂ ih₃ => apply orE <;> solve_by_elim [insert_subset_insert]
  case botE ih => apply botE; solve_by_elim [insert_subset_insert]
  -- sorry
}

使用 apply? 策略来找到陈述 Γ ⊆ insert x Γ 的引理。你可以点击右侧面板中的蓝色建议，来自动应用这个建议。

lemma ProvableFrom.insert (h : Γ ⊢ A) : insert B Γ ⊢ A := by {
  -- sorry
  apply weakening h
  -- use `apply?` here
  exact subset_insert B Γ
  -- sorry
}

现在，证明演绎定理变得十分简单。

lemma deduction_theorem (h : Γ ⊢ A) : insert (A ⇒ B) Γ ⊢ B := by {
  -- sorry
  intros
  apply impE (ax $ mem_insert _ _)
  exact h.insert
  -- sorry
}

lemma Provable.mp (h1 : Provable (A ⇒ B)) (h2 : Γ ⊢ A) : Γ ⊢ B := by {
  -- sorry
  apply impE _ h2
  apply weakening h1
  -- apply?
  exact empty_subset Γ
  -- sorry
}

这个问题有些棘手，因为你需要使用 Heyting 代数中的运算进行计算。

set_option maxHeartbeats 0 in
theorem soundness_theorem (h : Γ ⊢ A) : Γ ⊨ A := by {
  -- sorry
  induction h <;> intros H hH v c hv
  solve_by_elim
  case impI ih =>
    simp
    apply ih
    simp
    intros B hB
    -- apply?
    exact inf_le_of_left_le (hv B hB)
  case impE ih₁ ih₂ =>
    specialize ih₁ hv
    simp at ih₁
    rwa [inf_eq_left.mpr (ih₂ hv)] at ih₁
  case andI ih₁ ih₂ => simp [ih₁ hv, ih₂ hv]
  case andE1 ih =>
    specialize ih hv
    simp at ih
    exact ih.1
  case andE2 ih =>
    specialize ih hv
    simp at ih
    exact ih.2
  case orI1 ih =>
    simp
    exact le_trans (ih hv) le_sup_left
  case orI2 ih =>
    simp
    exact le_trans (ih hv) le_sup_right
  case orE Γ A B C _h1 _h2 _h3 ih₁ ih₂ ih₃ =>
    specialize ih₁ hv
    have h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
    · simp; intros D hD; exact inf_le_of_left_le (hv D hD) -- apply? found this
    have h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
    · simp; intros D hD; exact inf_le_of_left_le (hv D hD) -- apply? found this
    simp at ih₁
    rw [← inf_eq_left.mpr ih₁, inf_sup_left]
    rw [← sup_idem (a := eval v C)]
    exact sup_le_sup (ih₂ h2v) (ih₃ h3v)
  case botE ih =>
    specialize ih hv
    simp at ih
    simp [ih]
  -- sorry
}

theorem valid_of_provable (h : Provable A) : Valid A := by {
  -- sorry
  exact soundness_theorem h
  -- sorry
}

如果你愿意，现在可以尝试一些更长的项目。

定义 Kripke 语义并证明相对于 Kripke 语义的正确性。
对 Heyting 代数语义或 Kripke 语义证明完备性。

end IntuitionisticPropositionalLogic

import GlimpseOfLean.Library.Basic

在这个文件中，我们处理的是实数序列极限的基础定义。
mathlib 提供了一种更加通用的极限定义，但是在这里，我们想要利用前面文件中涉及的逻辑运算符和关系来进行实践。

在我们开始之前，让我们确保 Lean 在证明线性地从已知的等式和不等式中得出的等式和不等式时，不需要太多的帮助。这就是线性算术策略：linarith。

example (a b : ℝ) (hb : 0 ≤ b) : a ≤ a + b := by linarith

让我们使用 linarith 来证明一些练习。

example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b := by {
  -- sorry
  linarith
  -- sorry
}

example (a b c d : ℝ) (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d := by {
  -- sorry
  linarith
  -- sorry
}

一序列 u 是从 ℕ 到 ℝ 的函数，因此 Lean 表示为 u : ℕ → ℝ 我们将使用的定义是：

-- "u 趋向于 l" 的定义 def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

注意 ∀ ε > 0, _ 的使用，这是 ∀ ε, ε > 0 → _ 的简写。

特别的，像 h : ∀ ε > 0, _ 这样的陈述可以特殊化到给定的 ε₀，以 specialize h ε₀ hε₀ 的形式，其中 hε₀ 是 ε₀ > 0 的证明。

同样请注意，任何 Lean 期望得到一些证明项的地方，我们都可以使用关键词 by 开启策略模式证明。例如，如果局部上下文含有：

δ : ℝ δ_pos : δ > 0 h : ∀ ε > 0, _

那么我们可以使用 specialize h (δ/2) (by linarith) 将 h 特殊化为实数 δ/2，其中 by linarith 将提供 Lean 所期望的 δ/2 > 0 的证明。

如果 u 是常数，值为 l，那么 u 趋向于 l。提示：simp 可以将 |1 - 1| 重写为 0

example (h : ∀ n, u n = l) : seq_limit u l := by {
  -- sorry
  intros ε ε_pos
  use 0
  intros n _
  rw [h]
  simp
  linarith
  -- sorry
}

在处理绝对值时，我们会使用以下引理：

abs_sub_comm (x y : ℝ) : |x - y| = |y - x|

abs_le {x y : ℝ} : |x| ≤ y ↔ -y ≤ x ∧ x ≤ y

我们还会用到三角不等式的变形：

abs_add (x y : ℝ) : |x + y| ≤ |x| + |y| 或者： abs_sub_le (a c b : ℝ) : |a - b| ≤ |a - c| + |c - b| 再或者其带引号的版本： abs_sub_le' (a c b : ℝ) : |a - b| ≤ |a - c| + |b - c|

-- Assume `l > 0`. Then `u` ts to `l` implies `u n ≥ l/2` for large enough `n`
example (h : seq_limit u l) (hl : l > 0) :
    ∃ N, ∀ n ≥ N, u n ≥ l/2 := by {
  -- sorry
  rcases h (l/2) (by linarith) with ⟨N, hN⟩
  use N
  intros n hn
  specialize hN n hn
  rw [abs_le] at hN
  linarith [hN]
  -- sorry
}

当处理 max 时，你可以使用

ge_max_iff (p q r) : r ≥ max p q ↔ r ≥ p ∧ r ≥ q

le_max_left p q : p ≤ max p q

le_max_right p q : q ≤ max p q

让我们看一个例子。

-- If `u` tends to `l` and `v` tends `l'` then `u+v` tends to `l+l'`
example (hu : seq_limit u l) (hv : seq_limit v l') :
    seq_limit (u + v) (l + l') := by {
  intros ε ε_pos
  rcases hu (ε/2) (by linarith) with ⟨N₁, hN₁⟩
  rcases hv (ε/2) (by linarith) with ⟨N₂, hN₂⟩
  use max N₁ N₂
  intros n hn
  have : n ≥ N₁ := by exact le_of_max_le_left hn
  rw [ge_max_iff] at hn
  rcases hn with ⟨hn₁, hn₂⟩
  have fact₁ : |u n - l| ≤ ε/2
  · exact hN₁ n (by linarith)
  have fact₂ : |v n - l'| ≤ ε/2
  · exact hN₂ n (by linarith)
  -- omit

-- 不使用 calc 的另一种证明 simp have : |u n + v n - (l + l')| = |(u n - l) + (v n - l')| · ring rw [this] trans |u n - l| + |v n - l'| apply abs_add linarith [fact₁, fact₂]

-- omit
  calc
    |(u + v) n - (l + l')| = |u n + v n - (l + l')|   := rfl
    _ = |(u n - l) + (v n - l')|                      := by ring
    _ ≤ |u n - l| + |v n - l'|                        := by apply abs_add
    _ ≤ ε                                             := by linarith [fact₁, fact₂]
}

我们来做一些类似的事情：挤压定理。

example (hu : seq_limit u l) (hw : seq_limit w l) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) :
    seq_limit v l := by {
  -- sorry
  intros ε ε_pos
  rcases hu ε ε_pos with ⟨N, hN⟩
  rcases hw ε ε_pos with ⟨N', hN'⟩
  use max N N'
  intros n hn
  rw [ge_max_iff] at hn
  specialize hN n (by linarith)
  specialize hN' n (by linarith)
  specialize h n
  specialize h' n
  rw [abs_le] at *
  constructor
  -- Here `linarith` can finish, but on paper we would write
  calc
    -ε ≤ u n - l := by linarith
     _ ≤ v n - l := by linarith
  calc
    v n - l ≤ w n - l := by linarith
          _ ≤ ε := by linarith
  -- sorry
}

在下一个练习中，我们将使用

eq_of_abs_sub_le_all (x y : ℝ) : (∀ ε > 0, |x - y| ≤ ε) → x = y

回忆一下，我们在文件开始时列出了三种三角形不等式。

-- A sequence admits at most one limit. You will be able to use that lemma in the following
-- exercises.
lemma uniq_limit : seq_limit u l → seq_limit u l' → l = l' := by {
  -- sorry
  intros hl hl'
  apply eq_of_abs_sub_le_all
  intros ε ε_pos
  rcases hl (ε/2) (by linarith) with ⟨N, hN⟩
  rcases hl' (ε/2) (by linarith) with ⟨N', hN'⟩
  calc
    |l - l'| ≤ |l - u (max N N')| + |u (max N N') - l'| := by apply abs_sub_le
           _ = |u (max N N') - l| + |u (max N N') - l'| := by rw [abs_sub_comm]
           _ ≤ ε := by linarith [hN _ (le_max_left N N'), hN' _ (le_max_right N N')]
  -- sorry
}

让我们在进行定理证明前先练习解读定义。

def non_decreasing (u : ℕ → ℝ) := ∀ n m, n ≤ m → u n ≤ u m

def is_seq_sup (M : ℝ) (u : ℕ → ℝ) :=
(∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

example (M : ℝ) (h : is_seq_sup M u) (h' : non_decreasing u) : seq_limit u M := by {
  -- sorry
  intros ε ε_pos
  rcases h with ⟨inf_M, sup_M_ep⟩
  rcases sup_M_ep ε ε_pos with ⟨n₀, hn₀⟩
  use n₀
  intros n hn
  rw [abs_le]
  constructor <;> linarith [inf_M n, h' n₀ n hn]
  -- sorry
}

我们现在将探索子序列。

我们将要使用的新定义是，如果 φ : ℕ → ℕ 是（严格）递增的，那么它就是一个提取。

def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

以下的 φ 将总是表示一个从 ℕ 到 ℕ 的函数。

下一个引理通过简单的归纳证明，但是我们在这个教程中还没有看到归纳。如果你玩过自然数游戏，那么你可以删除下面的证明并尝试重新构建它。

一个提取操作大于 id

lemma id_le_extraction' : extraction φ → ∀ n, n ≤ φ n := by {
  intros hyp n
  induction n with
  | zero =>  exact Nat.zero_le _
  | succ n ih => exact Nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)])
}

在这个练习中，我们使用了 ∃ n ≥ N, ... ，这是 ∃ n, n ≥ N ∧ ... 的缩写形式。

提取将对任意大的输入取任意大的值。

lemma extraction_ge : extraction φ → ∀ N N', ∃ n ≥ N', φ n ≥ N := by {
  -- sorry
  intro h N N'
  use max N N'
  constructor
  apply le_max_right
  calc
    N ≤ max N N' := by apply le_max_left
    _ ≤ φ (max N N') := by apply id_le_extraction' h
  -- sorry
}

一个实数 a 是序列 u 的聚点，如果 u 有一个子序列收敛于 a。

def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a

如果 a 是 u 的聚点，那么对于任意大的输入，u 的值可以任意接近 a。

lemma near_cluster :
  cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε := by {
  -- sorry
  intro hyp ε ε_pos N
  rcases hyp with ⟨φ, φ_extr, hφ⟩
  cases' hφ ε ε_pos with N' hN'
  rcases extraction_ge φ_extr N N' with ⟨q, hq, hq'⟩
  exact ⟨φ q, hq', hN' _ hq⟩
  -- sorry
}

如果 u 趋向于 l，那么其子序列也趋向于 l。

lemma subseq_tendsto_of_tendsto' (h : seq_limit u l) (hφ : extraction φ) :
seq_limit (u ∘ φ) l := by {
  -- sorry
  intro ε ε_pos
  cases' h ε ε_pos with N hN
  use N
  intro n hn
  apply hN
  calc
    N ≤ n := hn
    _ ≤ φ n := id_le_extraction' hφ n
  -- sorry
}

如果 u 趋于 l，那么它的所有聚点都等于 l。

lemma cluster_limit (hl : seq_limit u l) (ha : cluster_point u a) : a = l := by {
  -- sorry
  rcases ha with ⟨φ, φ_extr, lim_u_φ⟩
  have lim_u_φ' : seq_limit (u ∘ φ) l := subseq_tendsto_of_tendsto' hl φ_extr
  exact unique_limit lim_u_φ lim_u_φ'
  -- sorry
}

Cauchy序列

一个序列 {a_n} 被称为 Cauchy 序列，如果对于任意一个小于 0 且大于限制性数字epsilon存在一个带有足够大基数的 N ，使得：∀m,n>N, |a_m-a_n|<ε。

为了更形象的描述 Cauchy 序列的定义，我们可以想象，随着 N 的增大，a_n 序列的元素越来越接近，这些元素组成的距离会无限接近等于 0。

在真实数的集合中，一个序列 {a_n} 是 Cauchy 序列的充分必要条件是该序列有限。

定理

在实数面板中，每一个 Cauchy 序列 {a_n} 都有极限。

证明：

年考虑 {a_n} 是一个 Cauchy 序列。通过序列 {a_n} 的有限性，我们可以证明 {a_n} 是一个有界序列。

• 确定 N1 使 |a_m - a_n| < 1 对于所有 m,n > N1。

• 选择 N=max{N1, a_1, a_2, ..., a_N1} 。

因此，以下的不等式成立：

-N ≤ a_n ≤ N 对于所有 n ，这意味着 {a_n} 是一个有界序列。

通过 Bolzano-Weierstrass 定理，每一个有界序列都有收敛的子序列。因此，我们可以找出 {a_n} 的收敛子序列 {a_nk} ，这个子序列收敛到 l。

我们想要证明最初的序列 {a_n} 也收敛到 l。

• 确定 N2 使 |a_nk - a_nl| < ε/2 对于所有 k,l > N2。

• 确定 N3 使 |a_n - l| < ε/2 ，对于所有 n > N3。

• 选择 N = max{N2, N3}。这对于所有的 n > N 和 m > N ，以下的不等式都成立：

|a_n - a_m| ≤ |a_n - l| + |l - a_m| < ε/2 + ε/2 = ε。

通过三角不等式，我们得出结论，{a_n} 是收敛到 l 的。证明结束。

def CauchySequence (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε

example : (∃ l, seq_limit u l) → CauchySequence u := by {
  -- sorry
  intro hyp
  cases' hyp with l hl
  intro ε ε_pos
  cases' hl (ε / 2) (by positivity) with N hN
  use N
  intro p q hp hq
  calc
    |u p - u q| = |u p - l + (l - u q)| := by ring_nf
    _ ≤ |u p - l| + |l - u q| := by apply abs_add
    _ = |u p - l| + |u q - l| := by rw [abs_sub_comm (u q) l]
    _ ≤ ε := by linarith [hN p hp, hN q hq]
  -- sorry
}

在下一个练习中，你可以重复使用 near_cluster : cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε

example (hu : CauchySequence u) (hl : cluster_point u l) : seq_limit u l := by
  -- sorry
  intro ε ε_pos
  cases' hu (ε / 2) (by positivity) with N hN
  use N
  have clef : ∃ N' ≥ N, |u N' - l| ≤ ε / 2
  apply near_cluster hl (ε / 2) (by positivity)
  cases' clef with N' h
  cases' h with hNN' hN'
  intro n hn
  calc
    |u n - l| = |u n - u N' + (u N' - l)| := by ring_nf
    _ ≤ |u n - u N'| + |u N' - l| := by apply abs_add
    _ ≤ ε := by linarith [hN n N' hn hNN', hN']
  -- sorry

初探 LEAN