I'm trying to learn Agda. Can anyone complete this proof (if it is on the right track) or point me to an existing writeup? I've searched extensively.
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) = {! !}
This requires more work than one would expect. Most of the side properties can be found in the standard library but here I have them explicitly. i am using imports from Agda's standard library.
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) ∎
You can simplify white_wolf's answer a lot by just letting the ring solver do all the heavy lifting before/after getting to the inductive step:
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open ≡-Reasoning
open import Function
sum : ℕ → ℕ
sum 0 = 0
sum (suc n) = (suc n) + sum n
thm : ∀ n → sum n * 2 ≡ n * (suc n)
thm zero = refl
thm (suc n) = cong (suc ∘ suc) $ begin
(n + sum n) * 2 ≡⟨ solve 2 (λ n s → (n :+ s) :* con 2 := n :* con 2 :+ s :* con 2) refl n (sum n) ⟩
n * 2 + sum n * 2 ≡⟨ cong (n * 2 +_) (thm n) ⟩
n * 2 + n * suc n ≡⟨ solve 1 (λ n → n :* con 2 :+ n :* (con 1 :+ n) := n :+ n :* (con 2 :+ n)) refl n ⟩
n + n * suc (suc n) ∎
where import Data.Nat.Properties; open Data.Nat.Properties.SemiringSolver
The redundancy in the polynomial equation passed to solve can probably be removed with some metaprogramming (by traversing a quotation of the goal), I remember seeing someone doing that but can't remember the reference.
