Lean4中证明`(xs=ys)=(reverse xs=reverse ys)`的可行性探讨

问题描述 #

直观上，列表xs与ys相等等价于它们的反转列表reverse xs与reverse ys相等。尝试证明如下定理：

theorem rev_eq (xs ys : List α) : (xs = ys) = (reverse xs = reverse ys)

目前仅能在xs = ys的假设下完成部分证明：

theorem rev_eq' (xs ys : List α) :
  xs = ys -> (xs = ys) = (reverse xs = reverse ys) := by
  intros h
  rw [h]
  simp

卡在xs ≠ ys的情况，需要解决思路。

解决思路 #

核心关键：反转函数的单射性 #

要证明原定理，核心是利用**reverse是单射函数**——即若reverse xs = reverse ys，则必有xs = ys。Lean4中已内置该性质的证明：List.reverse_injective，可直接调用。

分情况完成完整证明 #

通过by_cases分两种场景讨论：

1. xs = ys的情况：你已完成这部分，rw [h]后simp即可得证。
2. xs ≠ ys的情况：需证明reverse xs ≠ reverse ys，这是reverse_injective的逆否命题（单射的逆否逻辑：原像不等则像不等），Lean的simp策略可自动处理这类逻辑转换。

完整证明代码 #

theorem rev_eq (xs ys : List α) : (xs = ys) = (reverse xs = reverse ys) := by
  by_cases h : xs = ys
  -- 场景1：xs = ys
  · rw [h]
    simp
  -- 场景2：xs ≠ ys
  · simp [h, List.reverse_injective]

更简洁的写法可直接利用等价关系转等式：

theorem rev_eq (xs ys : List α) : (xs = ys) = (reverse xs = reverse ys) := by
  rw [← Iff.to_eq (List.reverse_injective.eq_iff)]
  simp

这里List.reverse_injective.eq_iff直接给出xs = ys ↔ reverse xs = reverse ys，再通过Iff.to_eq把等价关系转为等式，最后simp清理即可。

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