Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
32 lines (22 sloc) 0.986 kb
module Commutative where
data Nat : Set where
zero : Nat
succ : Nat -> Nat
data _==_ {A : Set} : A -> A -> Set where
==-r : (a : A) -> a == a
==-s : (A : Set) -> (a a' : A) -> a == a' -> a' == a
==-s A .a .a (==-r a) = ==-r a
==-t : (A : Set) -> (a b c : A) -> a == b -> b == c -> a == c
==-t A .a .a .a (==-r a) (==-r .a) = ==-r a
_+_ : Nat -> Nat -> Nat
m + zero = m
m + succ n = succ (m + n)
succ-c : (x y : Nat) -> x == y -> succ x == succ y
succ-c .x .x (==-r x) = ==-r (succ x)
lemma : (m n : Nat) -> (m + (succ n)) == ((succ m) + n)
lemma m zero = ==-r (succ m)
lemma m (succ n) = succ-c (m + (succ n)) ((succ m) + n) (lemma m n)
commutative : (m n : Nat) -> (m + n) == (n + m)
commutative zero zero = ==-r zero
commutative zero (succ n) = succ-c (zero + n) n (commutative zero n)
commutative (succ m) n = ==-t Nat ((succ m) + n) (succ (m + n)) (n + (succ m)) (==-s Nat (m + (succ n)) ((succ m) + n) (lemma m n)) (succ-c (m + n) (n + m) (commutative m n))
Jump to Line
Something went wrong with that request. Please try again.