tactic 基础

tactic 是什么、intro/exact/apply/refine 的精确差别、目标管理与 rcases 模式语言。

tactic 是构造项的程序

by 之后的每条 tactic，都在帮你写那个证明项。

theorem manual (p q : Prop) (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩

theorem tactical (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp
  · exact hq

两者产生的最终项完全相同。tactic 只是构造过程的自动化——用 #print tactical 能看到它生成的项。

理解这点很重要：tactic 失败不是「证明错了」，是「没能造出那个项」。

目标与上下文

theorem example_state (a b : Nat) (h : a = b) : b = a := by
  -- a b : Nat        ← 局部上下文
  -- h : a = b
  -- ⊢ b = a          ← 目标
  exact h.symm

tactic 做的事只有两类：改变上下文（加/改假设）或改变目标。

核心 tactic

exact

theorem use_exact (p : Prop) (hp : p) : p := by exact hp

「目标就是这个项」。要求类型完全匹配（允许定义展开）。

exact? 会搜索库里能直接闭合目标的定理——非常有用：

example (a b : Nat) : a + b = b + a := by exact?
-- 提示：exact Nat.add_comm a b

apply

theorem use_apply (p q : Prop) (hpq : p → q) (hp : p) : q := by
  apply hpq
  exact hp

「用这个定理，缺的参数留作新目标」。

apply f 会把 f 的结论与目标匹配，把 f 还缺的参数变成新目标。

exact 与 apply 的区别：

exact h —— h 必须完全是目标。
apply h —— h 的结论是目标，前提变成新目标。

exact hpq hp 与 apply hpq; exact hp 等价。apply 适合分步推进。

intro

theorem use_intro (p q : Prop) : p → q → p := by
  intro hp hq
  exact hp

「把目标里的箭头/量词移到上下文」。

对应逻辑里的蕴含引入与全称引入——本质是写 fun：

theorem use_intro' (p q : Prop) : p → q → p := fun hp _ => hp

intro 可以一次引入多个，也可以直接模式匹配：

example (p q : Prop) : p ∧ q → q := by
  intro ⟨_, hq⟩
  exact hq

refine

theorem use_refine (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  refine ⟨?_, ?_⟩
  · exact hp
  · exact hq

「给出部分项，用 ?_ 标出待填的洞」。

refine 是 exact 与 apply 的一般化——你控制项的骨架，把不想现在填的地方留成目标。

命名洞便于引用：

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  refine ⟨?left, ?right⟩
  case left => exact hp
  case right => exact hq

rfl / trivial / assumption

example : 2 + 2 = 4 := by rfl              -- 按定义相等
example : True := by trivial               -- 平凡目标
example (p : Prop) (hp : p) : p := by assumption   -- 从上下文里找

tactic	何时用
`rfl`	两边计算后相同
`trivial`	`True`、`rfl`、`assumption` 的组合尝试
`assumption`	上下文里已经有一模一样的假设

assumption 在自动化中常用——不必记住假设叫什么名字。

目标管理

focus dot

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp        -- 只处理第一个目标
  · exact hq

·（\.）聚焦当前第一个目标，块内必须把它完全解决。

强烈建议总是用 ·：不用它的话所有 tactic 作用在「当前所有目标」上，证明会变得难读且脆弱。

case

example (n : Nat) : n = n := by
  cases n with
  | zero => rfl
  | succ k => rfl

按名字处理分支，比位置更稳健。

组合子

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor <;> assumption

组合子	含义
`t1 <;> t2`	先跑 t1，再对它产生的所有目标跑 t2
`t1 ; t2`	顺序执行（换行等价）
`first \| t1 \| t2`	试 t1，失败就试 t2
`try t`	试 t，失败也不报错
`repeat t`	反复跑 t 直到失败
`all_goals t`	对所有目标跑 t
`any_goals t`	对任意目标跑 t（至少一个成功）

<;> 是最常用的——constructor <;> assumption 一行解决对称的分支。

rcases 模式语言

rcases / obtain 用一套小语言描述「怎么拆」：

example (h : (p ∧ q) ∨ (r ∧ s)) : True := by
  rcases h with ⟨hp, hq⟩ | ⟨hr, hs⟩
  · trivial
  · trivial

模式	含义
`⟨a, b⟩`	拆结构体/合取/存在
`a \| b`	分情况（析取/多构造子）
`⟨a, b\|c⟩`	嵌套
`-`	丢弃
`rfl`	若是等式，直接代入
`_`	自动命名

rfl 模式特别有用：

example (a b : Nat) (h : ∃ c, a = b + c) : b ≤ a := by
  obtain ⟨c, rfl⟩ := h      -- 直接把 a 替换成 b + c
  omega

obtain 与 rcases 基本同义，习惯上 obtain 用于「我知道结构」，rcases 用于「分情况」。

常用辅助

example (a b : Nat) (h : a = b) : b = a := by
  have h2 : b = a := h.symm      -- 引入中间结论
  exact h2

example (n : Nat) : n + 0 = n := by
  show n + 0 = n                  -- 显式声明目标（可改写成定义等价形式）
  simp

tactic	作用
`have h : T := e`	加一个已证的中间结论
`suffices h : T by ...`	「只需证 T」——先用后证
`show T`	把目标改写成定义等价的形式
`change T`	同 `show`，更严格
`clear h`	从上下文删掉 h
`rename_i x`	给自动生成的名字改名
`specialize h a`	把全称假设特化到具体值

have 是结构化证明的基础，下面会专门讲。

排查 tactic 失败

看清当前状态

把光标放在失败的 tactic 之前，Infoview 显示的就是它面对的状态。大多数失败是因为状态与你以为的不同。

trace 与 sorry

example (n : Nat) : n + 0 = n := by
  trace_state          -- 打印当前状态
  sorry

用 sorry 临时闭合，先确认前面的步骤对不对。

拆开自动化

example (a b : Nat) : a + b = b + a := by
  -- simp 失败时，看它到底做了什么
  simp?

simp? 会显示 simp 实际用了哪些引理，可以据此改成显式的 simp only [...]。

常见错误信息

信息	含义
`unsolved goals`	tactic 跑完了目标还在——信息里会列出剩余目标
`type mismatch`	`exact` 给的项类型不对
`failed to unify`	`apply` 的结论与目标对不上
`no goals`	目标已经没了还在写 tactic
`tactic 'rfl' failed`	两边计算后不相同

apply 失败常见于隐式参数推断不出来。 试试用 @ 显式给出，或者用 refine 手工留洞：

refine my_thm ?_ ?_      -- 明确留两个洞，避免 apply 的启发式

一个从零构造的证明

theorem and_or_distrib (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  constructor
  · intro ⟨hp, hqr⟩
    rcases hqr with hq | hr
    · left;  exact ⟨hp, hq⟩
    · right; exact ⟨hp, hr⟩
  · intro h
    rcases h with ⟨hp, hq⟩ | ⟨hp, hr⟩
    · exact ⟨hp, Or.inl hq⟩
    · exact ⟨hp, Or.inr hr⟩

每一步都对应上一章那张引入/消去表——没有任何需要「灵感」的地方。基础逻辑证明基本都是这样机械推进的。

下一篇：重写与化简。

本页目录