{- Giuseppe Peano (1858 -- 1932) is credited with the inductive
representation of natural numbers we define below. Unlike the previous
exercises in Boolean logic, Peano arithmetic (natural numbers with +,
*, and equality) is not decidable. This means we cannot write an
algorithm which will tell us whether any statement in Peano arithmetic
is true or false.  Presburger proved that arithmetic with natural
numbers, +, and equality is decidable. However, he was not happy with
this result as he wanted to show that the system including * was
decidable (an impossible problem). Due to this he never submitted his
PhD thesis!

Please complete the exercises below. There are some optional exercises
which will not be graded at the end.

DEADLINE
=======
The deadline to submit is 8th March 2010. Please submit
BoolQuestions.agda and NatQuestion.agda by email to james@cs.ioc.ee.
-}

module NatQuestions where

data True : Set where
  triv : True

data False : Set where

data Nat : Set where
  z : Nat 
  s : Nat → Nat

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO    z   #-}
{-# BUILTIN SUC     s   #-}

_+_ : Nat → Nat → Nat
m + n = {!!}

_*_ : Nat → Nat → Nat
m * n = {!!}

_≡_ : Nat → Nat → Set
z   ≡ z    = True
z   ≡ s _  = False
s _ ≡ z    = False
s m ≡ s n  = m ≡ n

infix 10 _≡_

refl≡ : ∀ n → n ≡ n
refl≡ n = {!!}

symm≡ : ∀ m n → m ≡ n → n ≡ m 
symm≡ m n = {!!}

trans≡ : ∀ m n o → m ≡ n → n ≡ o → m ≡ o
trans≡ m n o = {!!}

-- Addition
-- --------
assoc+ : ∀ m n o → (m + n) + o ≡ m + (n + o)
assoc+ m n o = {!!}

lid+ : ∀ n → n ≡ 0 + n
lid+ n = {!!}

rid+ : ∀ n → n ≡ n + 0
rid+ n = {!!}

suc+ : ∀ m n → s m + n ≡ m + s n
suc+ m n = {!!}

comm+ : ∀ m n → m + n ≡ n + m
comm+ m n = {!!}

cong+ : ∀ m m' n n' → m ≡ m' → n ≡ n' → m + n ≡ m' + n'
cong+ m m' n n' p q = {!!}

-- Multiplication
-- -------------- 

-- Everything after this point is optional and ungraded.  PhD students
-- and Agda veterans are expected to, at least, attempt some of them

lid* : ∀ n → n ≡ 1 * n
lid* n = {!!}

rid* : ∀ n → n ≡ n * 1
rid* n = {!!}

lan* : ∀ n → 0 ≡ 0 * n
lan* n = {!!}

ran* : ∀ n → 0 ≡ n * 0
ran* n = {!!}

comm* : ∀ m n → m * n ≡ n * m
comm* m n = {!!}

assoc* : ∀ m n o → (m * n) * o ≡ m * (n * o)
assoc* m n o = {!!}

-- Below are two alternatives to the recursive equality defined above:
-- To use one of them replace the recursive equality above and retry
-- some of the exercises. Please save your file before doing this and
-- perform these equality experiments in a different file.

{-
data _≡_ : Nat → Nat → Set where
  zeq : z ≡ z
  seq : ∀{m n} → m ≡ n → s m ≡ s n

data _≡_ : Nat → Nat → Set where
  refl : ∀{n} → n ≡ n
-}

-- If you do try the equality experiments give a short explanation of
-- the advantages and disadvantages of the different representations.