I've recently decided to pick up Agda again in preparation for SPLV, and after reading several chapters of Programming Language Foundations in Agda decided to just fiddle with some random proofs instead of trying to follow some exercise set.
Having remembered that I once have implemented a verified merge sort (I'm not good at keeping my files and all evidence of that has been lost, so you have to trust me on this one), verifying insertion sort seemed like an obvious starter task. Unfortunately, I've quickly found out that it seems to require some intuition about how to properly design predicates in order to be able to actually prove something, so I quickly switched to something simpler, which is obviously proving some properties of arithmetic functions.
One small project came to mind is to prove that sum of integers from 1 to n equals to n * (n + 1) / 2. I haven't managed to get it done on the first try, but after remembering that I don't need to prove stupid ring equations and can use a solver available in standard library, it turned out to be quite a simple task. Here is how the finished proof looks like:
sum : ℕ → ℕ
sum zero = zero
sum (suc n) = suc n + sum n
gauss : (n : ℕ) → sum n + sum n ≡ n * (suc n)
gauss zero = refl
gauss (suc n) =
begin
suc (n + sum n + suc (n + sum n))
≡⟨ cong suc
(solve 3 (λ x y z → x :+ y :+ z := x :+ (z :+ y))
(λ {x} {x = x₁} {x = x₂} → refl) n (sum n) (suc (n + sum n))) ⟩
suc (n + (suc (n + sum n) + sum n))
≡⟨⟩
suc (n + (suc (n + sum n + sum n)))
≡⟨ cong (λ z → suc (n + suc z)) (+-assoc n (sum n) (sum n)) ⟩
suc (n + (suc (n + (sum n + sum n))))
≡⟨ cong (λ z → suc (n + suc (n + z))) (gauss n) ⟩
suc (n + (suc (n + n * (suc n))))
≡⟨ cong (λ x → suc (n + suc x))
(solve 3 (λ x y z → x :+ y :* z := z :* y :+ x)
(λ {x} {x = x₁} {x = x₂} → refl) n n (suc n)) ⟩
suc (n + (suc (suc n * n + n)))
≡⟨⟩
suc (n + suc (n + n * n + n))
≡⟨ cong suc (+-comm n (suc (n + n * n + n))) ⟩
suc (suc ((n + n * n + n) + n))
≡⟨ cong (λ n → suc (suc n))
(solve 2
(λ x y → x :+ y :+ x :+ x := x :+ (x :+ (x :+ y))) (λ {x} {x = x₁} → refl) n (n * n)) ⟩
suc (suc (n + suc (suc n) * n))
≡⟨ sym (cong (λ z → suc (suc (n + z))) (*-comm n (suc (suc n)))) ⟩
suc (suc (n + n * suc (suc n)))
∎
Which was satisfying, but I wanted to do another proof, attributed to Gauss, which goes like this: notice that we can reverse a list of integers from 1 to n, and add it to original copy. That would lead to list of n integers, with every one of them being n + 1, which is obviously n * (n + 1). Dividing that by half (because we took two copies of the list) gives the result.
Turns out that while this proof is way easier when presented informally, doing it formally is way more complicated when done formally. I've ended up having 13K file (which also happens to have more warm-up exercises as well, such as properties of addition and multiplication, but they don't take that much space), which I'm not going to bore you with, but would just show the main lemma for comparison:
prefix-reverse
: (n : ℕ)
→ sum (add-lists (prefix n) (reverse (prefix n))) ≡ sum (replicate (suc n) n)
prefix-reverse zero = refl
prefix-reverse (suc n) =
begin
sum (add-lists (suc n :: prefix n) (reverse-helper (prefix n) (suc n :: [])))
≡⟨ cong (λ x → sum (add-lists (suc n :: prefix n) x))
(reverse-++-helper (prefix n) [] (suc n :: [])) ⟩
sum (add-lists (suc n :: prefix n) (reverse-helper (prefix n) [] ++ (suc n :: [])))
≡⟨ add-lists-sum (suc n :: prefix n) (reverse-helper (prefix n) [] ++ (suc n :: []))
(same-same (suc n :: prefix n) (reverse-helper (prefix n) [] ++ (suc n :: [])) lemma) ⟩
sum (suc n :: prefix n) + sum (reverse-helper (prefix n) [] ++ (suc n :: []))
≡⟨⟩
suc (n + sum (prefix n) + sum (reverse-helper (prefix n) [] ++ (suc n :: [])))
≡⟨ cong (λ x → suc (n + sum (prefix n) + x))
(sum-append (reverse-helper (prefix n) []) (suc n :: [])) ⟩
suc (n + sum (prefix n) + (sum (reverse-helper (prefix n) []) + sum (suc n :: [])))
≡⟨ cong
(λ x →
suc
(n + sum (prefix n) + (sum (reverse-helper (prefix n) []) + suc x)))
(+-comm n zero) ⟩
suc (n + sum (prefix n) + (sum (reverse-helper (prefix n) []) + suc n))
≡⟨ cong suc
(solve 4
(λ a b c d → a :+ b :+ (c :+ d) := b :+ c :+ a :+ d)
(λ {x} {x = x₁} {x = x₂} {x = x₃} → refl) n (sum (prefix n))
(sum (reverse-helper (prefix n) [])) (suc n)) ⟩
suc (sum (prefix n) + sum (reverse-helper (prefix n) []) + n + suc n)
≡⟨ cong
(λ x → suc (x + n + suc n))
(sym
(add-lists-sum (prefix n) (reverse-helper (prefix n) [])
(same-same (prefix n) (reverse-helper (prefix n) []) (sym (reverse-length (prefix n)))))) ⟩
suc (sum (add-lists (prefix n) (reverse-helper (prefix n) [])) + n + suc n)
≡⟨ cong (λ z → suc (z + n + suc n)) (prefix-reverse n) ⟩
suc (sum (replicate (suc n) n) + n + suc n)
≡⟨ cong (λ z → suc (z + n + suc n)) (replicate-lemma (suc n) n) ⟩
suc (n * suc n + n + suc n)
≡⟨ cong (λ z → suc (z + n + suc n)) (*-comm n (suc n)) ⟩
suc (suc n * n + n + suc n)
≡⟨⟩
suc (n + (n * n) + n + suc n)
≡⟨ sym (cong suc (+-assoc (n + (n * n)) n (suc n))) ⟩
suc (n + (n * n) + (n + suc n))
≡⟨ cong (λ z → suc (n + (n * n) + z)) (+-comm n (suc n)) ⟩
suc (n + (n * n) + (suc (n + n)))
≡⟨ cong suc (solve 3 (λ a b c → a :+ b :+ c := c :+ a :+ b) (λ {x} {x = x₁} {x = x₂} → refl) n (n * n) (suc (n + n))) ⟩
suc (suc (n + n) + n + n * n)
≡⟨ cong (λ x → suc (suc x)) (solve 4 (λ a b c d → a :+ b :+ c :+ d := a :+ (b :+ (c :+ d))) (λ {x} {x = x₁} {x = x₂} {x = x₃} → refl) n n n (n * n)) ⟩
suc (suc n + (n + (n + n * n)))
≡⟨⟩
suc (suc (n + suc (suc n) * n))
≡⟨ cong (λ x → suc (suc (n + x))) (sym (*-comm n (suc (suc n)))) ⟩
suc (suc (n + n * suc (suc n)))
≡⟨ sym (cong (λ z → suc (suc (n + z))) (replicate-lemma (suc (suc n)) n)) ⟩
suc (suc (n + sum (replicate (suc (suc n)) n)))
∎
where
lemma : suc (length (prefix n)) ≡ length (reverse-helper (prefix n) [] ++ (suc n :: []))
lemma =
begin
suc (length (prefix n))
≡⟨ sym (+-comm (length (prefix n)) 1) ⟩
length (prefix n) + 1
≡⟨ sym (cong (λ z → z + 1) (reverse-length (prefix n))) ⟩
length (reverse-helper (prefix n) []) + 1
≡⟨ sym (length-++ (reverse-helper (prefix n) []) (suc n :: [])) ⟩
length (reverse-helper (prefix n) [] ++ (suc n :: []))
∎
Yeah, and that's only the main thing. I also needed to prove a ton of dumb properties, such as list length and sum being homomorphisms, reversing a list not changing sum or length and so on.
It was fun though! I also learned a bunch of things and some ideas, which are:
suc n ≡ suc m → n ≡ m by induction. I ultimately managed to do that by proving suc n - 1 ≡ n for saturated subtraction on naturals, but it turned out to be completely unnecessary.where language construct exists! I haven't used it before for some reason, but it's way more convenient to just write a bunch of lemmas using identifiers already in scope instead of defining a new top-level thing having to write down all the necessary arguments as parameters.