如何用`replace`完成这种交换性证明？

Question

在this文档中，提到了如何使用replace来完成证明，但它最终使用rewrite，这似乎是为你编写replace的语法糖。我有兴趣了解如何明确地使用它。

如果我理解正确，它可以用来重写S k = S (plus k 0)作为S (plus k 0) = S (plus k 0)，给出k = plus k 0的证明，然后可以通过反身性来证明。但如果我们将它作为replace {P = \x => S x = S (plus k 0)} {x = k} {y = plus k 0} rec实例，我们现在需要一个S k = S (plus k 0)的证明，这是我们想要开始证明的。简而言之，我不确定P到底应该是什么。

Answer 1

啊，回想起来相当明显。如果我们让：

P = \x => S x = S (plus k 0)

然后，我们可以证明它为x = (plus k 0)（通过反身性）。现在，如果我们让y = k，那么，通过使用replace，我们获得了S k = S (plus k 0)的证明，这是我们需要的。或者，换句话说：

plusCommZ : (m : Nat) -> m = plus m 0
plusCommZ Z = Refl
plusCommZ (S k) = replace 
  {P = \x => S x = S (plus k 0)}
  {x = plus k 0}
  {y = k}
  (sym (plusCommZ k))
  Refl

完成证明。我们可以用P = \x => S x = S k反过来做。