2

说我的证明目标包括nat.succ (nat.succ 0)，我想快速重写它说2；我可以定义一个全新的定理：

theorem succ_succ_zero_eq_two : nat.succ (nat.succ 0) = 2 := rfl

然后将该定理与 一起使用rw，但这似乎很笨拙。在我的证明中，有没有办法在一行中做到这一点？

4

2 回答 2

1

一个更简单的解决方案将使用以下change策略：

change 2

另请参阅ac_change，它也可以重新排列总和和产品。

于 2020-05-01T01:36:46.577 回答
0

利用rw (show nat.succ (nat.succ 0) = 2, by refl),

于 2020-04-01T03:56:42.133 回答