.. raw:: latex

    \appendix

.. _tactic_index:

Lean 策略索引
=============

标有 \* 的策略是本书专用的策略，因此你无法通过搜索引擎、网络论坛等渠道获得关于它们的帮助。请重读书中指出的相关部分，或询问你的教师。

.. rubric:: \* ``addarith``（首次使用：:numref:`第 %s 节 <shortcut>`）

试图通过把项从等式或不等式的一边移到另一边来证明该等式或不等式。

.. rubric:: ``apply``（首次使用：:numref:`第 %s 节 <lemmas>`；用于 :math:`\forall` 和 :math:`\to` 假设：:numref:`第 %s 节 <forall_implies>`）

调用指定的引理或假设来改变目标。

.. rubric:: ``by_cases``（首次使用：:numref:`第 %s 节 <lem>`）

按给定命题为真或为假进行分类讨论。

.. rubric:: \* ``cancel``（首次使用：:numref:`第 %s 节 <tactic_mode>`）

消去等式或不等式两边的公因子，消去两边共同出现的幂，等等。

.. rubric:: ``constructor``（首次使用：:numref:`第 %s 节 <and>`；用于 ``↔`` 目标：:numref:`第 %s 节 <iff>`）

把一个“且”目标（:math:`\land`）拆成分别对应左右两部分的子目标。

.. rubric:: ``contradiction``（首次使用：:numref:`第 %s 节 <contradiction_hyp>`）

若当前已有两个相互矛盾的假设，则结束证明。

.. rubric:: ``dsimp``（首次使用：:numref:`第 %s 节 <parity>`）

展开一个定义。它通常用于证明探索阶段，而不是用于最终版本；它有助于更仔细地查看目标或假设，但在多数情况下，删除一行 ``dsimp`` 后证明仍能成立。

.. rubric:: \* ``extra``（首次使用：:numref:`第 %s 节 <proving_inequalities>`；用于同余：:numref:`第 %s 节 <using_modular>`）

用于不等式或同余等其他关系的比较策略：它可以检查两边相差一个正量的不等式、两边相差 3 的倍数的模 3 同余，等等。

.. rubric:: ``interval_cases``（首次使用：:numref:`第 %s 节 <forall_implies>`）

给定一个自然数变量或整数变量 :math:`n`，并且已有关于 :math:`n` 的数值上下界时，对 :math:`n` 的每一种可能数值分别产生一个情形。

.. rubric:: ``intro``（首次使用：:numref:`第 %s 节 <forall_implies>`；用于 :math:`\lnot` 目标：:numref:`第 %s 节 <contradiction>`）

从目标中引入一个全称量化变量（:math:`\forall`）或一个蕴含（:math:`\to`）的前件；或者在证明否定（:math:`\lnot`）目标时，为了导出矛盾而假设其正向版本。

.. rubric:: ``left``（首次使用：:numref:`第 %s 节 <or>`）

选择“或”目标（:math:`\lor`）的左侧选项。

.. rubric:: ``have``（首次使用：:numref:`第 %s 节 <tactic_mode>`；配合引理使用：:numref:`第 %s 节 <or>`；引入新目标：:numref:`第 %s 节 <and>`）

记录一个事实（随后给出该事实的证明），然后这个事实会作为额外假设可供使用。

.. rubric:: ``mod_cases``（首次使用：:numref:`第 %s 节 <using_modular>`）

按照变量模指定数的余数来引入分类讨论。

.. rubric:: \* ``numbers``（首次使用：:numref:`第 %s 节 <proving_inequalities>`；配合 ``at`` 处理矛盾：:numref:`第 %s 节 <contradiction_hyp>`）

证明数值事实，例如 :math:`3\cdot 12 < 13 + 25` 或 :math:`3\cdot 5+1=4\cdot 4`。

.. rubric:: ``obtain``（首次用于 :math:`\lor`：:numref:`第 %s 节 <or>`；用于 :math:`\land`：:numref:`第 %s 节 <and>`；用于 :math:`\exists`：:numref:`第 %s 节 <exists>`）

拆解形如“或”（:math:`\lor`）、“且”（:math:`\land`）或“存在”（:math:`\exists`）的假设。

.. rubric:: ``push_neg``（首次使用：:numref:`第 %s 节 <negation_normalize>`）

把一个假设或目标转换为逻辑等价的形式，其中否定号被尽可能向内推进。

.. rubric:: ``rel``（首次使用：:numref:`第 %s 节 <proving_inequalities>`；用于同余：:numref:`第 %s 节 <using_modular>`；用于逻辑等价：:numref:`第 %s 节 <negation_normalize>`）

一个用于不等式或同余等其他关系的“类似代换”的策略：它会在目标中寻找某个指定不等式（或同余等）事实的左边，并在这种替换“显然”给出一个有效的不等式（或模算术等）推理时，把它替换为该事实的右边。可与 ``rw`` 比较。

.. rubric:: ``right``（首次使用：:numref:`第 %s 节 <or>`）

选择“或”目标（:math:`\lor`）的右侧选项。

.. rubric:: ``ring``（首次使用：:numref:`第 %s 节 <proving_equalities_in_lean>`）

解决代数等式目标，例如 :math:`(x + y) ^ 2 = x ^ 2 + 2xy + y ^ 2`，前提是证明实质上只是“展开两边并重新整理”。

.. rubric:: ``rw``（首次使用：:numref:`第 %s 节 <proving_equalities_in_lean>`；用于 ``↔`` 假设或引理：:numref:`第 %s 节 <iff>`）

代换：在目标中寻找某个指定等式事实的左边，并把它替换为该事实的右边。

对于 ``↔`` 假设或引理，把指定 ``↔`` 事实的左边替换为其右边。

.. rubric:: ``use``（首次使用：:numref:`第 %s 节 <exists>`）

为存在性目标（:math:`\exists`）提供一个见证。