时间戳

首页 > 解决方案 > 为什么在这种情况下使用 `rewriting` 时需要使用 `sym`？

agda - 为什么在这种情况下使用 `rewriting` 时需要使用 `sym`？

问题描述

鉴于自然数的皮亚诺定义：

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

我们可以用不同的方法证明这个性质∀ (m : ℕ) → zero + m ≡ m + zero。

例如：

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) =
  begin
    zero + suc n
  ≡⟨⟩
    zero + suc (zero + n)
  ≡⟨⟩
    suc (zero + n)
  ≡⟨ cong suc (comm-+₀ n) ⟩
    suc (n + zero)
  ≡⟨⟩
    suc n + zero
  ∎

更简洁：

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) = cong suc (comm-+₀ n)

如果我们愿意，我们甚至可以使用rewrite和放弃cong：

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) rewrite comm-+₀ n = refl

可是等等！那是行不通的。Agda 会告诉我们该表达式是错误的，因为它无法证明以下内容：

suc (n + 0) ≡ suc (n + 0 + 0)

如果我们向 Agda 提供属性的对称重写 , sym (comm-+₀ n)，它将进行类型检查而不会出错。

所以，我的问题是：为什么我们需要sym在这种情况下？没有它与其他策略的证明工作得很好。重写是否同时在两侧工作，而不仅仅是左侧？

标签： agda

解决方案

在每种情况下，当m形式的目标suc n是：

suc n ≡ suc (n + 0)

要通过提供正确键入的术语来解决此目标，正确的方法是，正如您所注意到的：

cong suc (comm-+₀ n)

但是，当rewrite与等式一起使用时，a ≡ b您可以通过替换所有出现的aby来直接修改目标。b在您的情况下，使用类型为rewrite的数量会导致替换by的每个出现，从而将目标从comm-+₀ nn ≡ n + 0nn + 0

suc n ≡ suc (n + 0)

到

suc (n + 0) ≡ suc (n + 0 + 0)

这不是你想要做的。由于重写将左侧的所有出现替换为右侧，因此使用反转等式sym将代替唯一出现的n + 0byn从而将目标从

suc n ≡ suc (n + 0)

到

suc n ≡ suc n

这是您的预期行为，让您直接使用refl。这解释了为什么需要使用sym.

总结一下：

  • rewrite直接与目标的类型交互。
  • rewrite从左到右重写。
  • rewrite重写它在目标类型中找到的所有出现。

更多信息rewrite可以在这里找到：

https://agda.readthedocs.io/en/v2.6.0.1/language/with-abstraction.html#with-rewrite

推荐阅读