关于equal .subst替换规则的基本问题

Question

我正在努力学习精益。我不明白为什么最后一个等式替换不起作用(我只是试图"逐字逐句"地";用简单的c代替0+c):

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.subst c0 h

我得到了错误:

"eliminator"术语:精雕细琢者类型不匹配h有类型B + c = 0 + c但预计会有类型B + (0 + c) = 0 + c

在我看来，Lean假设c的所有出现都必须以0+c的形式出现，这有点奇怪。

Answer 1

Lean使用show的预期类型来确定h应该是什么，因此它假设h应该来自于在目标中进行反向替换。这就是为什么使用rewrite这样的策略在实践中使用起来更方便的原因之一。

让它工作的一种方法是这样做:

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.substr h c0