这是一份 Coq 战术速查表，包含了在 Coq 中证明定理时可用的各种战术及其用法。

• 求解简单目标的战术：

  • assumption：如果目标已在上下文中假设，则可立即证明目标。
  • reflexivity：如果目标是一个简单的等式且显然成立，可使用此战术完成证明。
  • trivial：可以解决各种简单目标，能引入变量和假设并尝试使用其他战术证明目标，即使不能证明也不会失败。
  • auto：是更高级的trivial，进行递归证明搜索，即使不能做任何事情也不会失败。
  • discriminate：证明归纳类型的不同构造函数不能相等，若上下文包含假等式也可用于证明任何目标。
  • exact：如果知道确切的证明项可直接使用此战术证明目标，否则会失败。
  • contradiction：如果上下文中有等价于False的假设或矛盾假设，可用于证明任何目标。

• 转换目标的战术：

  • intros / intro：引入全称量化变量或蕴含的前提到上下文中，intros可引入所有可引入的内容，intro只引入一个。
  • simpl：将复杂项简化为更简单的形式，对目标或上下文中的假设都可用，即使不能简化也不会失败。
  • unfold：用定义替换目标或上下文中的项，若项没有定义则会失败。
  • apply：用于根据已知的蕴含关系转换目标或假设，可用于证明定理等，若无法匹配则会失败。
  • rewrite：根据已知的等式在目标或假设中进行替换，有rewrite -> <equality>和rewrite <- <equality>两种形式，对假设使用时语法为rewrite..in..。
  • inversion：根据等式推导相等的信息，并尝试用这些信息重写目标。
  • left / right：如果目标是一个析取式A \\/ B，left将目标替换为左边A，right将目标替换为右边B，目标不是析取式时会失败。
  • replace：用一个项替换目标中的另一个项，并生成一个子目标证明这两个项相等。

• 分解目标和假设的战术：

  • split：如果目标是一个合取式A /\\ B，将目标分解为两个子目标A和B，目标不是合取式时会失败。
  • destruct (and/or)：对于上下文中的合取式A /\\ B，将其分解为两个新的假设A和B；对于析取式A \\/ B，生成两个子目标，分别在A和B成立的情况下证明目标。
  • destruct (case analysis)：对类型为归纳类型的项或变量进行更一般的情况分析，根据不同的构造函数生成子目标。
  • induction：与destruct类似，但会引入适当的归纳假设，可用于归纳证明。

• 求解特定类型目标的战术：

  • ring：可解决只包含加法和乘法运算的目标，使用前需导入Require Import Arith.。
  • tauto：可解决任何在构造逻辑中是重言式的目标。
  • field：可解决包含加法、减法、乘法和除法运算的目标，使用前需导入Require Import Field.，注意不能用于自然数或整数。

• 战术组合（作用于其他战术的战术）：

  • ; (semicolon)：将分号右边的战术应用于左边战术生成的所有子目标。
  • try：尝试使用一个战术，即使该战术失败也允许继续执行。
  • || (or)：先尝试左边的战术，如果失败则尝试右边的战术。
  • all:：将给定的战术应用于所有剩余的子目标。
  • repeat：重复应用给定的战术，直到该战术失败，即使应用零次也不会失败。

此速查表受Coq Tactic Index启发。