Some proofs of basic properties of addition and equality in Agda. Update: Now lists and multiplication!

Nats.agda

module Nats where

open import Agda.Primitive

data Equal {a : Level} {X : Set a} : X → X → Set a where
  equal : {x : X} → Equal x x
{-# BUILTIN EQUALITY Equal #-}

_==_ : _
_==_ = Equal

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN REFL equal #-}

_+_ : ℕ → ℕ → ℕ
zero + y = y
suc x + y = suc (x + y)

{- Proof of transitivity of equality -}
transitive : (a b c : ℕ) → a == b → b == c → a == c
transitive zero zero zero p1 p2 = equal
transitive zero zero (suc c) equal ()
transitive zero (suc b) c () p2
transitive (suc a) .(suc a) .(suc a) equal equal = equal

symmetry : (a b : ℕ) → a == b → b == a
symmetry a .a equal = equal

reflex : (a : ℕ) → a == a
reflex a = equal

{- Proof of commutativity of addition -}
x+0 : (a : ℕ) → (a + 0) == a
x+0 zero = equal
x+0 (suc a) rewrite x+0 a = equal

commute' : (a b : ℕ) → (a + suc b) == suc (a + b) 
commute' zero b = equal
commute' (suc a) b rewrite commute' a b = equal

commute : (a b : ℕ) → (a + b) == (b + a)
commute zero b rewrite x+0 b = equal
commute (suc a) b rewrite commute' b a | commute a b = equal

{- Applying the commutativity proof: x + 1 == 1 + x -}
x+1 : (x : ℕ) → (x + 1) == (1 + x)
x+1 x = commute x 1

{- Proof of associativity of addition -}
assoc : (a b c : ℕ) → ((a + b) + c) == (a + (b + c))
assoc zero b c = equal
assoc (suc a) b c rewrite assoc a b c = equal

_*_ : ℕ → ℕ → ℕ
zero * _ = zero
suc a * b = b + (b * a)

a*0 : (a : ℕ) → (a * 0) == 0
a*0 zero = equal
a*0 (suc a) rewrite a*0 a = equal

{- Proof that 1 is identity element of multiply over nats -}
a*1 : (a : ℕ) → (a * 1) == a
a*1 zero = equal
a*1 (suc a) rewrite a*1 a | a*0 a | x+0 a = equal

{-
commute* : (a b : ℕ) → (a * b) == (b * a)
commute* zero b rewrite a*0 b = equal
commute* (suc a) b rewrite commute* a b = {!!}
-}

infixr 40 _::_
data List (A : Set) : Set where
  nil : List A
  _::_ : A → List A → List A

id : {ℓ : Level} → {A : Set ℓ} → A → A
id a = a

map : {A B : Set} → (A → B) → List A → List B
map f nil = nil
map f (x :: l) = f x :: map f l

_++_ : {A : Set} → List A → List A → List A
nil ++ r = r
x :: l ++ r = x :: (l ++ r)

{- Proof of list append associativity -}
listAssoc : {A : Set} → (a b c : List A) → (a ++ (b ++ c)) == ((a ++ b) ++ c)
listAssoc nil b c = equal
listAssoc (x :: a) b c rewrite listAssoc (a) b c = equal

{- Proof of the first functor law: map id == id -}
mapIdFunctorLaw : {A : Set} → (a : List A) → (map id a) == (id a)
mapIdFunctorLaw nil = equal
mapIdFunctorLaw (x :: l) rewrite mapIdFunctorLaw l = equal

_∘_ : {A B C : Set} → (B -> C) → (A -> B) -> A -> C
_∘_ g f a = g (f a)

{- Proof of the second functor law: map g ∘ f == map g ∘ map f -}
mapComposeLaw : {A B C : Set} → (a : List A) → (f : A → B) → (g : B → C) → map (g ∘ f) a == (map g ∘ map f) a
mapComposeLaw nil f g = equal
mapComposeLaw (x :: l) f g rewrite mapComposeLaw l f g = equal

In transitive, if you case split p1 and p2 you will get a one-liner: transitive a .a .a equal equal = equal. You get transitivity of equality for "free"!

@scott-fleischman: Ah good point! To be honest I just mashed C-c C-c and C-c C-r until it type checked :) But now I'm starting to get more a feel for how to work toward a solution.

@scott-fleischman: Also, any recommendations on next steps once I finish your exercises?

Hmm… think of something to prove and prove it? The Agda Wiki has lots of references to publications, other introductions, tons of papers: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation

One fun thing to do is to write purely functional data structures (say, from Okasaki) and to prove the invariants about the code and/or find ways "bake in" the invariants into the structures themselves.

@scott-fleischman

Hmm… think of something to prove and prove it?

Haha fair enough. I love the Okasaki idea. I've had that book on my shelf for a while and have been looking for an excuse to spend some time with it.

Hi, I noticed that is no long possible to use {-# BUILTIN REFL equal #-}.
Agda says:

Builtin REFL no longer exists. It is now bound by BUILTIN EQUALITY
when checking the pragma BUILTIN REFL equal

To fix it, is just remove the line xD