如何证明数对(2,4)不在succ_rel归纳关系中？

你的succ_rel是归纳定义的，只有唯一构造子pair a，意思是仅当第二个数是第一个数的直接后继（即Nat.succ a）时，两个数才属于该关系。要证明¬succ_rel 2 4，核心是推导矛盾——2的直接后继是3而非4，不存在符合条件的构造子能生成succ_rel 2 4。

具体Lean实现方法 #

先修正你代码里的小错误：open succ_relation应该改成open succ_rel（因为你定义的归纳类型是succ_rel）。下面提供两种实现方式：

方式1：用cases策略快速推导

inductive succ_rel : Nat → Nat → Prop
    | pair (a : Nat) : succ_rel a (Nat.succ a)

open succ_rel

example : ¬succ_rel 2 4 := by
  cases H : succ_rel 2 4 <;> contradiction

• cases H会把假设H: succ_rel 2 4分解为唯一的构造子pair a，Lean自动生成两个等式：a = 2和Nat.succ a = 4。
• <;> contradiction检查分支矛盾：代入a=2后，Nat.succ a等于3，和4矛盾，直接完成证明。

方式2：手动展开match过程（更直观）

inductive succ_rel : Nat → Nat → Prop
    | pair (a : Nat) : succ_rel a (Nat.succ a)

open succ_rel

example : ¬succ_rel 2 4 :=
fun H : succ_rel 2 4 =>
match H with
| pair a =>
  -- 从构造子推导出a必须等于2
  have h1 : a = 2 := by simp [H]
  -- 同时Nat.succ a必须等于4
  have h2 : Nat.succ a = 4 := by simp [H]
  -- 代入a=2后得到3=4的矛盾
  rw [h1] at h2
  contradiction

这种方式把矛盾推导过程拆解开，更适合理解归纳类型的否定证明逻辑——枚举所有可能的构造子，证明每个构造子都无法满足目标命题的条件。

内容的提问来源于stack exchange，提问作者Boba Tea