如何对有限类型间的函数进行分情况证明？（Lean新手求助）

数据老陈

2026-8-19

证明Bool→Bool函数的迭代性质

在Lean中，无法直接对函数f : Bool → Bool使用cases，因为cases仅适用于归纳类型的值，而函数本身是依赖于输入的映射，不属于归纳构造子。不过Bool是有限类型（仅包含false和true两个值），我们可以通过枚举f在所有输入上的输出，来覆盖所有可能的函数情况。

方法1：用`<;>`串联多轮`cases`

利用<;>将分支策略批量应用到所有子目标，一步到位覆盖所有情况：

example (f : Bool -> Bool) : (∀ x : Bool, f (f (f x)) = f x) := by
  intro x
  -- 先拆分x的两种情况，再枚举f false和f true的所有组合，最后用rfl验证
  cases x <;> cases f false <;> cases f true <;> rfl

cases x：拆分x为false和true两个分支
<;> cases f false：对每个x的分支，再拆分f false的两种可能
<;> cases f true：对每个子分支，继续拆分f true的两种可能
<;> rfl：在所有最底层分支中，Lean会自动计算f(f(f x))和f x的结果，确认两者相等，rfl直接完成证明

方法2：用`match`枚举所有组合

更直观地列出所有可能的x、f false、f true组合，逐个验证：

example (f : Bool -> Bool) : (∀ x : Bool, f (f (f x)) = f x) := by
  intro x
  match x, f false, f true with
  | false, false, false => rfl
  | false, false, true => rfl
  | false, true, false => rfl
  | false, true, true => rfl
  | true, false, false => rfl
  | true, false, true => rfl
  | true, true, false => rfl
  | true, true, true => rfl

这种写法清晰展示了所有8种可能的场景（2种x × 2种f(false) × 2种f(true)），每个场景下函数的行为完全确定，rfl可直接验证等式成立。