且和或

做完这一节，你能证明带“且”（∧）和“或”（∨）的命题。规律只有一条：它出现在目标里，还是出现在假设里，做法不同。

	在目标里（要证它）	在假设里（手里有它）
p ∧ q	constructor：分别证 p 和 q	h.left、h.right：取出其中一半
p ∨ q	left 或 right：选一边来证	rcases h with hp | hq：两种情况都要讨论

符号怎么打：在 VS Code 或在线版里输入 \and 得到 ∧，\or 得到 ∨，\to 得到 →。

学完你能做什么

• 证明一个“且”：两边都证
• 使用一个“且”：取出需要的一半
• 证明一个“或”：选对的一边
• 使用一个“或”：分情况讨论

第 1 步：且

要证 p ∧ q，就得 p 和 q 都证出来。constructor 把一个目标拆成两个：

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

行首的 · 表示“现在专心证这一个小目标”。输入 \. 得到它。

反过来，手里有 h : p ∧ q 时，h.left 是 p 的证明，h.right 是 q 的证明：

example (p q : Prop) (h : p ∧ q) : q := by
  exact h.right

课程入口页你证过的那个命题，现在每一步都能看懂了：

theorem and_swap' (p q : Prop) : p ∧ q → q ∧ p := by
  intro h
  constructor
  · exact h.right
  · exact h.left

• 我知道目标里的“且”用 constructor，假设里的“且”用 .left 和 .right

第 2 步：或

要证 p ∨ q，证出其中一边就够。用 left 或 right 说明你选哪边：

example (p q : Prop) (hp : p) : p ∨ q := by
  left
  exact hp

选错边就证不下去。手里只有 p，却选了右边：

example (p q : Prop) (hp : p) : p ∨ q := by
  right
  exact hp

Type mismatch
hp
has type
p
but is expected to have type
q

手里有 h : p ∨ q 时情况不同：你不知道成立的是哪一边，所以两种情况都要处理。rcases h with hp | hq 把证明分成两支，一支里有 hp : p，另一支里有 hq : q。

• 我知道目标里的“或”选一边，假设里的“或”两边都要讨论

动手：把“或”的两边换位置

已知“p 或 q”，证明“q 或 p”。留意分情况之后，两支选的边正好相反。

动手证把“或”的两边换个位置状态和报错由 Lean 4.35.0 生成

theorem or_swap' (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  rcases h with hp | hq
  right
  exact hp
  left
  exact hq

写成代码：

theorem or_swap' (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  rcases h with hp | hq
  · right
    exact hp
  · left
    exact hq

考考你手里有 h : p ∧ q，目标是 p ∨ q。下面哪种做法行得通？

检查点

• 我能默写本页开头那张两行两列的表
• 我在练习里证完了 or_swap'
• 我知道 · 是用来聚焦一个小目标的
• 我会输入 ∧、∨、→

没成功？

constructor 之后有两个目标，不知道现在在证哪个。 看目标状态最上面那一个，case left 或 case right 标明了它是哪一半。用 · 一个一个来。

rcases 那一行报语法错。 中间的竖线是键盘上的 |，两边的名字随你起。

下一节

到这里每一步都是你亲手推的。下一节学几个能替你干活的策略：改写、化简和自动算术。