module EvenPlus where

open import Nat
open import PropositionalLogic
open import PredicateLogic
open import Identity

{-

The game of turning propositions into types does not end once we've mapped all
the logical connectives to types. For any new proposition and predicate you want
to reason about there's a choice of how to represent it as a type. In the same
way that you have to decide on a data representation when programming, you have
to decide on a proof object representation when proving theorems.

For example, let us reason about even numbers. For this we need a predicate
Even : Nat → Set. The most obvious(?) thing to do is to look up the definition
of even numbers on Wikipedia:

  An integer is even if it is evenly divisible by two

and clicking "divisible" gets us

  a divisor of an integer n, also called a factor of n, is an integer m that may
  be multiplied by some integer to produce n

Reading this a few times until it makes sense, leads us to the following
definition of Even:
-}

WikipediaEven : Nat → Set
WikipediaEven n = ∃ Nat (λ k → k * 2 ≡ n)

{-
Another option is to exploit the fact that predicates are just functions. We
don't need a fancy proof object for a number being even. We can easily verify
that a number is even by looking at it.
-}

ComputeEven : Nat → Set
ComputeEven 0 = ⊤
ComputeEven 1 = ⊥
ComputeEven (succ (succ n)) = ComputeEven n

{-
The third option is to use our nice recipe for turning propositions into
types: just look at the introduction rules. The natural deduction style rules
for a number being even are

                Even n
   ------    ------------
   Even 0    Even (n + 2)

This turns into the data type
-}

data Even : Nat → Set where
  even0  : Even 0
  evenss : ∀ n → Even n → Even (succ (succ n))

{-
The nice thing about defining predicates inductively (i.e. as a recursive data
type) is that it lets us use pattern matching when proving theorems (writing
programs) about them. For instance, proving that the sum of two even numbers is
even proceeds by straightforward recursion on the first proof object:
-}

even-sum : ∀ m n → Even m → Even n → Even (m + n)
even-sum m .0 em even0 = em
even-sum m .(succ (succ n)) em (evenss n en) = evenss {!m + n!} (even-sum m n em en)





--even-sum m .0 em even0 = em
--even-sum m .(succ (succ n)) em (evenss n en) = evenss (m + n) (even-sum m n em en)
--even-sum m zero em en = em
--even-sum m (succ zero) em ()
--even-sum m (succ (succ n)) em (evenss .n en) = evenss (m + n) (even-sum m n em en)

compute-even-sum : ∀ m n → ComputeEven m → ComputeEven n → ComputeEven (m + n)
compute-even-sum m zero em en = em
compute-even-sum m (succ zero) em ()
compute-even-sum m (succ (succ n)) em en = compute-even-sum m n em en

-- mutual definitions

mutual
  data Evenm : Nat → Set where
    evenm0 : Evenm 0
    evenms : ∀ n → Oddm n → Evenm (succ n)

  data Oddm : Nat → Set where
    oddms : ∀ n → Evenm n → Oddm (succ n)

-- we can also have mutual definitions of functions, use the keyword mutual.