n Naturals 之和的 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)               ?