加法的交换性和结合性的综合证明

Question

我试图证明下面的引理

 infixr 5 _~_
 _~_ = trans

lemma-+swap : ∀ a b c → a + (b + c) ≡ b + (a + c)
lemma-+swap zero b c = refl
lemma-+swap (suc a) b c = (+-assoc a b c) ~ (comm-+ a (b + c)) ~ (+-assoc b c a)

注意:我导入了这个文件

open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; sym; trans; cong; cong₂)

而在纸面上，我是这样尝试的：

(a + b) + c equivalent a + (b + c) -- associativity
 a + (b + c) equivalent to (b + c) + a -- commutativity
(b + c) + a equi to b + (c + a) -- associativity

我在goal中写了这段代码，但得到了错误。我有结合性和交换性的证明。请帮帮忙。

Answer 1

你基本上是在做不必要的案例拆分。在第一个例子中，我们得到：

lemma-+swap zero b c = ?

-- goal: b + c ≡ b + c

这是通过简单的refl来满足的。然而，第二个是：

lemma-+swap (suc a) b c = ?

-- goal: suc (a + (b + c)) ≡ b + suc (a + c)

因此您有两种选择:首选的一种是避免大小写拆分，直接使用属性。另一种方法是使用带有suc a而不是a的属性。

在这里，我假设您的属性与上面提到的模块中的属性具有相同的类型(这是一个合理的假设，因为对于其他变体，子表达式+-assoc a b c ~ comm-+ a (b + c) ~ +-assoc b c a不会检查类型)。

+-assoc a b c    : a + b + c   ≡ a + (b + c)
+-comm a (b + c) : a + (b + c) ≡ b + c + a
+-assoc b c a    : b + c + a   ≡ b + (c + a)

+-assoc a b c ~ comm-+ a (b + c) ~ +-assoc b c a : a + b + c ≡ b + (c + a)       (*)

所以，子表达式的类型是(*)，但是您的目标是a + (b + c) ≡ b + (a + c)。

Answer 2

将你已经有的证明抄写在纸上

像这样编写校样的一种非常好的方法是使用Relation.Binary.PropositionalEquality.≡-Reasoning模块，因为它使您能够准确地将您的校样写在纸上：

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
open import Data.Nat
open import Data.Nat.Properties.Simple using (+-assoc; +-comm)

lemma-+swap : ∀ a b c → a + (b + c) ≡ b + (a + c)
lemma-+swap a b c = begin
  a + (b + c) ≡⟨ {!!} ⟩
  (a + b) + c ≡⟨ {!!} ⟩
  (b + a) + c ≡⟨ {!!} ⟩
  b + (a + c) ∎
  where
    open PropEq.≡-Reasoning

现在，您需要填写的是与证明的三个步骤相对应的三个洞。

使用半环求解器

最省事的方法是让semiring solver来处理您的相等，因为自然数的加法和乘法形成了一个半环。但是，我不建议您现在这样做，因为您似乎需要更多的基础知识经验，以确保您不会落入认为半环求解器是不应该理解的黑盒魔法的陷阱。因此，下面的答案对其他读者来说更有意义，而不是太多的操作：

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)
open import Data.Nat

lemma-+swap : ∀ a b c → a + (b + c) ≡ b + (a + c)
lemma-+swap = solve 3 (λ a b c → a :+ (b :+ c) := b :+ (a :+ c)) refl
  where
    open import Data.Nat.Properties as Nat
    open Nat.SemiringSolver