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。在你证明某些东西后，你会看到一个小的 "No goals" 消息，这表明你的证明已经完成。

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就足够了。"

rw 策略需要被告知每个重写步骤。稍后我们将看到更强大的策略，可以为你自动化这些繁琐的步骤。

实际上可以在一个命令中进行多次重写。

example (a b c d e : ℝ) (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 d e : ℝ) (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 = d) : c = d*a + d := by
  rw [h'] at h
  -- 我们的假设 `h` 现在正好是我们需要证明的
  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

inline sorry

rw [h]/- inline sorry -/

              _ = exp ((b + b) + (c + c))           := by

inline sorry

ring/- inline sorry -/

              _ = exp (b + b) * exp (c + c)         := by

inline sorry

rw [exp_add]/- inline sorry -/

              _ = (exp b * exp b) * (exp c * exp c) := by

inline sorry

rw [exp_add, exp_add]/- inline sorry -/

              _ = (exp b) ^ 2 * (exp c)^2           := by

inline sorry

ring/- inline sorry -/

从实用的角度来看，编写这样的证明时，有时很方便： * 通过点击Lean Infoview面板右上角的暂停图标按钮暂停VScode中的策略状态视图更新。 * 写出完整的计算，每行以":= ?_"结尾 * 通过点击播放图标按钮恢复策略状态更新并填入证明。

下划线应该放在 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