阿格达从怀疑？（引理的位置有不同的含义）

Question

我们有

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

并想证明

+-swap' : ∀(m n p : ℕ) → m + (n + p) ≡ n + (m + p)

这是我的第一次尝试：

+-swap' : ∀(m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap' m n p =
begin m + (n + p)
≡⟨ sym (+-assoc m n p) ⟩
    (m + n) + p
≡⟨ +-comm (m + n) p ⟩
    p + (m + n)
≡⟨ sym (+-assoc p m n) ⟩
    (p + m) + n 
≡⟨ +-comm (p + m)  n ⟩
    n + (p + m)
≡⟨ cong (n +_) (+-comm p m) ⟩
    n + (m + p)
∎

我想像这样简化它：

+-swap : ∀(m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p =
begin
m + (n + p)
≡⟨ sym (+-assoc m n p) ⟩ 
    (m + n) + p
≡⟨ cong ((+-comm m n) +_) p ⟩ -- the wrong line
    (n + m) + p
≡⟨ +-assoc n m p ⟩
    n + (m + p)
∎

然而这次我得到了：

m + n ≡ n + m !=< _A_224 → _B_226 of type Set
when checking that the expression +-comm m n has type
_A_224 → _B_226

那有什么区别呢？对我来说，我使用与好的模式相同的模式。因为我对这个话题很陌生。我也尝试了 ⟨ cong (+-comm m n) (p +_) ⟩，它喜欢 ⟨ cong (n +_) (+-comm p m) ⟩，但它不起作用。

Answer 1

在https://plfa.github.io/Induction。

A relation is said to be a congruence for a given function if it is preserved
by applying that function. If e is evidence that x ≡ y, then cong f e is 
evidence that f x ≡ f y, for any function f

经过我的理解。我改成这个

+-swap : ∀(m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p =
begin
m + (n + p)
≡⟨ sym (+-assoc m n p) ⟩ 
    (m + n) + p
≡⟨ cong (_+ p) (+-comm m n) ⟩   -- need to compute
    (n + m) + p
≡⟨ +-assoc n m p ⟩
n + (m + p)
∎

这里的引理是(+-comm m n)。该函数将是 (_+ p)。可能会有帮助。我只是把我的解决方案放在这里。

阿格达从怀疑？（引理的位置有不同的含义）

Agda cong doubut? (The position of lemma have different meaning)

agda

阿格达从怀疑？ （引理的位置有不同的含义）

Agda cong doubut? (The position of lemma have different meaning)

agda

阿格达从怀疑？（引理的位置有不同的含义）