.. _transitioning_to_regular_lean:

过渡到主流 Lean
===============

如果你喜欢本书，也许会希望进一步使用 Lean，例如阅读
`Mathematics in Lean <https://leanprover-community.github.io/mathematics_in_lean/>`_，
或启动一个
`独立的形式化项目 <https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency>`_。

你会发现，本书使用的 Lean“方言”不同于 `mathlib <https://github.com/leanprover-community/mathlib4>`_
库及其相关文献（例如 *Mathematics in Lean*）中使用的主流数学 Lean。
为了帮助你适应，本附录概述主要差异。

本书中使用的一些策略，是 mathlib 中相应策略的有意弱化版本。我这样做，
是为了屏蔽 Lean 的某些能力，因为在本书层次的文字证明中，通常会把这些细节完整写出。
这些有意弱化的策略包括：

.. _tactic_comparison_table:

..  list-table::  本书策略及其 mathlib 原型
    :widths: 30 30 50
    :header-rows: 1

    * - mathlib 策略
      - 弱化的

        *证明的技艺*

        版本
      - 差异

    * - ``norm_num``
      - ``numbers``
      - ``norm_num`` 能完成本书要求读者手工完成的一些计算，

        包括模 :math:`n` 化简、

        处理逻辑，以及检查整除性和素性

    * - ``gcongr``
      - ``rel``
      - ``gcongr`` 不要求你说明正在代入哪些假设

    * - ``linarith``
      - ``addarith``
      - ``linarith`` 除了加减常数外，还可以取线性不等式的常数倍，

        可以组合许多线性不等式，且不要求你说明

        正在使用哪些假设

    * - ``duper``
      - ``exhaust``
      - ``duper`` 能处理包含量词的逻辑任务，而不只限于

        无量词的任务

本书中使用的一些策略在 mathlib 中没有直接对应物。它们通常是对一小组引理的封装；
在 mathlib 中，这些引理会按名称调用。

.. _tactic_lemma_wrapper_table:

..  list-table::  本书中没有 mathlib 对应物的策略
    :widths: 30 80
    :header-rows: 1

    * - *证明的技艺* 中的策略
      - 所封装的引理

    * - ``extra``
      - ``Int.modEq_fac_zero``、``le_add_of_nonneg_right``、

        ``lt_add_of_pos_right`` 等，以及策略

        ``positivity``

    * - ``cancel``
      - ``mul_left_cancel₀``、``lt_of_pow_lt_pow``、

        ``pos_of_mul_pos_left`` 等，以及策略

        ``positivity``

    * - ``simple_induction``

        ``induction_from_starting_point``

        ``two_step_induction``

        ``two_step_induction_from_starting_point``

      - ``Nat.le_induction``、``Nat.twoStepInduction`` 等，

        以及策略 ``induction`` 或 ``induction'``

本书中的许多问题若以 mathlib 风格的 Lean 来解，会高效得多，
因为某些步骤序列可以由超出本书数学范围的高级算法一步完成。应当了解的这类策略包括：

.. _decision_procedures:

..  list-table::  本书未使用的高级算法
    :widths: 30 30 50
    :header-rows: 1

    * - 算法
      - mathlib 策略
      - 该策略可以替代的步骤类型

    * - `Fourier-Motzkin 消元法 <https://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination>`_
      - ``linarith``
      - ``addarith``、``rel``、``ring``、``numbers``

    * - `Gröbner 基 <https://en.wikipedia.org/wiki/Gr%C3%B6bner_basis>`_
      - ``polyrith``
      - ``rw``、``ring``

    * - `叠加演算 <https://en.wikipedia.org/wiki/Superposition_calculus>`_
      - ``duper``
      - 证明或子证明末尾的逻辑策略

本书没有涉及的另一点，是如何与库交互。由于 mathlib 含有超过一百万行 Lean 代码，
要弄清库中是否已经有你想要的引理，并不总是容易的！在本书中，
我通过预先告诉你希望你使用的每个引理名称来避开这个问题。

与库交互时，需要了解以下几个基本点：

* `在线文档 <https://leanprover-community.github.io/mathlib4_docs/>`_ 通常比源代码更易读：
  它可搜索，并且含有内部超链接。
* 引理往往以极高的一般性陈述……:math:`(a - b) + c = a - (b - c)`
  `这个引理 <https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Basic.html#sub_sub>`_
  不是针对 :math:`\mathbb{R}` 陈述的，而是针对 ``SubtractionCommMonoid`` 陈述的。
  在修完抽象代数和点集拓扑的第一门课程之后，你可能会更容易与库交互。
* 如果你能猜出一个引理的精确陈述，策略 ``exact?`` 会在库中找到它。

以上只是触及皮毛：Lean 还有许多更多功能，可以帮助你进行数学探索。
*Mathematics in Lean*、`社区网站 <https://leanprover-community.github.io/>`_
和 `社区讨论区 <https://leanprover.zulipchat.com/>`_ 提供了进一步探索的指引。
祝你顺利探索！