Lean中eq.subst替换规则疑问：0+c替换为c为何失败？

你遇到的问题是eq.subst的参数逻辑搞反了。Lean里的eq.subst函数作用是：如果有等式a = b，它能把一个关于b的命题转换成关于a的命题。你的c0是0 + c = c，所以eq.subst c0需要接收一个形如P c的命题，但你传入的h是b + c = 0 + c，这是P (0 + c)的形式，类型不匹配，才会出现那个奇怪的错误提示。

要实现把0 + c替换成c的需求，有几种更直接的写法：

方法1：用等式传递（eq.trans） #

import data.int.basic

example : ∀ {b c : ℤ}, b + c = 0 + c → b + c = c :=
  assume b c : ℤ,
  assume h : b + c = 0 + c,
  have c0 : 0 + c = c, by rw zero_add,
  show b + c = c, from eq.trans h c0

方法2：直接在假设上替换（rw ... at h） #

import data.int.basic

example : ∀ {b c : ℤ}, b + c = 0 + c → b + c = c :=
  assume b c : ℤ,
  assume h : b + c = 0 + c,
  rw zero_add at h,
  show b + c = c, from h

方法3：更简洁的写法 #

import data.int.basic

example : ∀ {b c : ℤ}, b + c = 0 + c → b + c = c :=
λ b c h, by rw zero_add at h; exact h

本质上，你需要的是把h中的0 + c替换成c，而eq.subst的逻辑和这个需求相反，所以才会报错。用rw或者eq.trans更符合你的直观需求。

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