proof - n 自然之和的 Agda 证明

Question

我正在努力学习 Agda。任何人都可以完成此证明(如果它在正确的轨道上)或指出我现有的文章吗？我进行了广泛的搜索。

sum : ℕ → ℕ
sum 0 = 0
sum (suc a) = (suc a) + sum a

prove2*Sumn=n*sucn : (n : ℕ) → ((sum n) * 2) ≡ (n * (suc n))
prove2*Sumn=n*sucn zero = refl
prove2*Sumn=n*sucn (suc a) = {! !}

Answer 1

这需要比预期更多的工作。大多数辅助属性都可以在标准库中找到，但在这里我明确地提供了它们。我正在使用从 Agda 的标准库导入的内容。

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open ≡-Reasoning
open import Function

sum : ℕ → ℕ
sum 0 = 0
sum (suc a) = (suc a) + sum a

rightZero : ∀ a → a + 0 ≡ a
rightZero zero    = refl
rightZero (suc a) = cong suc (rightZero a)

times2 : ∀ a → a + a ≡ 2 * a
times2 zero    = refl
times2 (suc a) = sym (cong (suc ∘ (a +_) ∘ suc) (rightZero a))

+-asso : ∀ a b c → a + (b + c) ≡ (a + b) + c
+-asso zero b c = refl
+-asso (suc a) b c = cong suc (+-asso a b c)

+-rsucc : ∀ m n → m + suc n ≡ suc (m + n)
+-rsucc zero n = refl
+-rsucc (suc m) n = cong suc (+-rsucc m n)

+-comm : ∀ a b → a + b ≡ b + a
+-comm zero b = sym (rightZero b)
+-comm (suc a) b = trans (cong suc (+-comm a b)) (sym (+-rsucc b a))

distribl* : ∀ m n k → m * (n + k) ≡ m * n + m * k
distribl* zero n k = refl
distribl* (suc m) n k = begin
  n + k + m * (n + k)       ≡⟨ cong (_+_ (n + k)) (distribl* m n k) ⟩
  n + k + (m * n + m * k)   ≡⟨ sym (+-asso n k (m * n + m * k)) ⟩
  n + (k + (m * n + m * k)) ≡⟨ cong (_+_ n) (+-asso k (m * n) (m * k)) ⟩
  n + ((k + m * n) + m * k) ≡⟨ sym (cong (λ z → n + (z + m * k)) (+-comm (m * n) k)) ⟩
  n + ((m * n + k) + m * k) ≡⟨ sym (cong (_+_ n) (+-asso (m * n) k (m * k))) ⟩
  n + (m * n + (k + m * k)) ≡⟨ +-asso n (m * n) (k + m * k) ⟩
  n + m * n + (k + m * k  ) ∎

*rid : ∀ a → a * 1 ≡ a
*rid zero    = refl
*rid (suc a) = cong suc (*rid a)

*rz : ∀ a → a * 0 ≡ 0
*rz zero    = refl
*rz (suc a) = *rz a

*-distribr : ∀ a b c → (a + b) * c ≡ a * c + b * c
*-distribr zero b c = refl
*-distribr (suc a) b c = begin
  c + (a + b) * c     ≡⟨ cong (_+_ c) (*-distribr a b c) ⟩
  c + (a * c + b * c) ≡⟨ +-asso c (a * c) (b * c) ⟩
  c + a * c + b * c   ∎

*-rsucc : ∀ a b → a * suc b ≡ a + (a * b)
*-rsucc zero b = refl
*-rsucc (suc a) b = begin
  suc (b + a * suc b)   ≡⟨ cong (λ x → suc (b + x)) (*-rsucc a b) ⟩
  suc (b + (a + a * b)) ≡⟨ cong suc (+-asso b a (a * b)) ⟩
  suc ((b + a) + a * b) ≡⟨ sym (cong (λ z → suc (z + a * b)) (+-comm a b)) ⟩
  suc ((a + b) + a * b) ≡⟨ sym (cong suc (+-asso a b (a * b))) ⟩
  suc (a + (b + a * b)) ∎

*-comm : ∀ a b → a * b ≡ b * a
*-comm zero b = sym (*rz b)
*-comm (suc a) b = begin
                     b + a * b ≡⟨ cong (_+_ b) (*-comm a b) ⟩
                     b + b * a ≡⟨ sym (*-rsucc b a) ⟩ b * suc a ∎

prove2*Sumn=n*sucn : (n : ℕ) → (sum n * 2) ≡ (n * (1 + n))
prove2*Sumn=n*sucn zero = refl
prove2*Sumn=n*sucn (suc a) = cong (suc ∘ suc) $ begin
  (a + sum a) * 2               ≡⟨ *-comm (a + sum a) 2 ⟩
  2 * (a + sum a)               ≡⟨ sym (times2 (a + sum a)) ⟩
  (a + sum a) + (a + sum a)     ≡⟨ sym (+-asso a (sum a) (a + sum a)) ⟩
  a + (sum a + (a + sum a))     ≡⟨ cong (_+_ a) (+-asso (sum a) a (sum a)) ⟩
  a + ((sum a + a) + sum a)     ≡⟨ cong (a +_) (sym (cong (λ z → z + sum a) (+-comm a (sum a)))) ⟩
  a + ((a + sum a) + sum a)     ≡⟨ sym (cong (_+_ a) (+-asso a (sum a) (sum a))) ⟩
  a + (a + (sum a + sum a))     ≡⟨ +-asso a a (sum a + sum a) ⟩
  (a + a) + (sum a + sum a)     ≡⟨ cong ((a + a) +_) (times2 (sum a)) ⟩
  (a + a) + (2 * sum a)         ≡⟨ sym (cong (_+_ (a + a)) (*-comm (sum a) (suc (suc zero)))) ⟩
  (a + a) + (sum a * 2)         ≡⟨ cong (_+_ (a + a)) (prove2*Sumn=n*sucn a) ⟩ -- inductive hypothesis
  (a + a) + a * (1 + a)         ≡⟨ sym (+-asso a a (a * suc a)) ⟩
  a + (a + a * (1 + a))         ≡⟨ cong (a +_) (cong (a +_) (distribl* a 1 a)) ⟩
  a + (a + ((a * 1) + (a * a))) ≡⟨ cong (λ z → a + (a + (z + a * a))) (*rid a) ⟩
  a + (a + (a + (a * a)))       ≡⟨ cong (_+_ a) (+-asso a a (a * a)) ⟩
  a + (a + a + a * a)           ≡⟨ cong (λ z → a + (z + a * a)) (times2 a) ⟩
  a + (2 * a + a * a)           ≡⟨ sym (cong (λ z → a + (z + a * a)) (*-comm a (suc (suc zero)))) ⟩
  a + (a * 2 + a * a)           ≡⟨ sym (cong (_+_ a) (distribl* a (suc (suc zero)) a)) ⟩
  a + a * (2 + a)               ∎