Lean 4（元）编程 Cookbook

例子：拆分 `∧` 中的目标🔗

作为一个例子，我们可能想把形如 P ∧ Q 的目标迭代地分解为独立的目标 P 和 Q。为此，我们可以用 Expr.app2? 函数检查主目标是否为 P ∧ Q 的形式，该函数检查一个表达式是否是给定常量带两个参数的应用，如果是，就返回该应用的参数。递归地这样做，就能把形如 P1 ∧ P2 ∧ P3 的目标拆分成三个独立的目标 P1、P2 和 P3。我们在下面的函数中这样做。

partial def splitAnds (e: Expr) : List Expr :=
  match e.app2? ``And with
  | some (P, Q) => splitAnds P ++ splitAnds Q
  | none => [e]

为了看到这个函数的实际效果，我们写一个精译器，它在证明过程中获取主目标并把它传给 splitAnds（关于如何用精译器编写策略见查看与关闭目标，关于如何在信息视图中显示信息见在信息视图中显示）。

elab "splitAnds" : tactic => do
  withMainContext do
  let goal ← getMainTarget
  let subgoals := splitAnds goal
  if subgoals.length = 1 then
    logInfo m!"The goal is not a conjunction: {goal}"
  else
    logInfo m!"The goal is a conjunction"
    logInfo m!" Subgoals ({subgoals.length} subgoals) are:"
    for subgoal in subgoals do
      logInfo m!"Subgoal: {subgoal}"

example: 123 ≤ 234 := by⊢ 123 ≤ 234
  The goal is not a conjunction: 123 ≤ 234splitAnds⊢ 123 ≤ 234
  simpAll goals completed! 🐙

example: (123 ≤ 234) ∧ (234 ≤ 345) ∧
    (345 ≤ 456 ∧ 2 ≤ 3) := by⊢ 123 ≤ 234 ∧ 234 ≤ 345 ∧ 345 ≤ 456 ∧ 2 ≤ 3
  Subgoal: 2 ≤ 3The goal is a conjunction Subgoals (4 subgoals) are:Subgoal: 123 ≤ 234Subgoal: 234 ≤ 345Subgoal: 345 ≤ 456splitAnds⊢ 123 ≤ 234 ∧ 234 ≤ 345 ∧ 345 ≤ 456 ∧ 2 ≤ 3
  simpAll goals completed! 🐙

其他识别器🔗

如上所述，还有若干其他识别器，可用来检查一个表达式是否匹配某个模式并提取相关的子表达式。也有相关的布尔函数，它们检查一个表达式是否匹配某个模式，但不提取子表达式。

例如，函数 Expr.isLambda 检查一个表达式是否是 λ 抽象并提取该 λ 抽象的主体。函数 Expr.isForall 检查一个表达式是否是全称量化并提取该量化的主体。函数 Expr.isAppOfArity 检查一个表达式是否是某个函数带一定数量参数的应用并提取该应用的参数。我们还有匹配器 Expr.eq?、Expr.const?、Expr.prod? 等，它们检查一个表达式是否为某种形式并提取相关的子表达式。

你可以在 Lean 4 文档中找到识别器的完整列表。