{- 
  Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Thorsten Altenkirch

  Exercise 5: Arithmetic
  Deadline: 5/3/2010, 12:00

  Use the coursework submission (id: 271)) system to submit the coursework
  after demonstrating it in the lab to me or Darin.
  
  Prove the following propositions of propositional logic by
  completing the sheds { .. }.

  Note that not all propositions may be provable. If you think that a
  proposition is unprovable clearly mark this one by adding a line:
  -- impossible.

-}

module ex05 where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary -- Dec
open ≡-Reasoning
open import Data.Product
open import Data.Sum
{- we use ⊎ (\uplus) for ∨ -}
open import Algebra
module ℕ = CommutativeSemiring Data.Nat.Properties.commutativeSemiring

{- This structure shows that ℕ is a commutative semiring, e.g.
   ℕ.+-comm : m + n ≡ n + m
   ℕ.+-assoc : (m + n) + l ≡ m + (n + l)
   ℕ.*-comm : m * n ≡ n * m
   ℕ.*-assoc : (m * n) * l ≡ m * (n * l)
   ℕ.distribʳ : (y + z) * x ≡ y * x + z * x
-}

{- Warm up: I define doubling: -}

2*_ : ℕ → ℕ
2* zero = 0
2* suc n = 2 + 2* n

{- prove it is the same as adding a number to itself: -}

2*Lem : ∀ {m} → 2* m ≡ m + m
2*Lem {zero} = refl
2*Lem {suc m} = begin 
  2* (suc m)    ≡⟨ refl ⟩
  2 + 2* m      ≡⟨ cong (_+_ 2) (2*Lem {m}) ⟩
  2 + (m + m)   ≡⟨ cong suc (ℕ.+-comm (suc m) m) ⟩
  suc m + suc m
  ∎

{- Define functions,
   mod₂ : remainder of division by 2
   div₂ : division by two 
-}
mod₂ : ℕ → ℕ 
mod₂ zero = 0
mod₂ (suc zero) = 1
mod₂ (suc (suc n)) = mod₂ n

div₂ : ℕ → ℕ
div₂ zero = zero
div₂ (suc zero) = zero
div₂ (suc (suc n)) = suc (div₂ n)

{- And prove the following properties: -}

mod₂Lem : (n : ℕ) → mod₂ n ≡ 0 ⊎ mod₂ n ≡ 1
mod₂Lem zero = inj₁ refl
mod₂Lem (suc zero) = inj₂ refl
mod₂Lem (suc (suc n)) = mod₂Lem n

s2* : ∀{n} → 2 * (suc n) ≡ 2 + 2 * n
s2* {n} =  begin 
  2 * (suc n) ≡⟨ ℕ.*-comm 2 (suc n) ⟩
  (suc n) * 2 ≡⟨ refl ⟩
  2 + n * 2 ≡⟨ cong (_+_ 2) (ℕ.*-comm n 2) ⟩
  2 + 2 * n
  ∎

div₂Lem : ∀ {n} → 2 * (div₂ n) + mod₂ n ≡ n
div₂Lem {zero} = refl
div₂Lem {suc zero} = refl
div₂Lem {suc (suc n)} = begin 
  2 * div₂ (suc (suc n)) + mod₂ (suc (suc n))    ≡⟨ refl ⟩
  2 * suc (div₂ n) + mod₂ n    ≡⟨ cong (λ x → x + mod₂ n) (s2* {div₂ n}) ⟩
  2 + (2 * div₂ n + mod₂ n)    ≡⟨ cong (_+_ 2) div₂Lem ⟩
  suc (suc n)
  ∎

{- Show that equality modulo 2 is decidable. -}

_≡₂_ : ℕ → ℕ → Set
m ≡₂ n = mod₂ m ≡ mod₂ n

_≡₂?_ : (m n : ℕ) → Dec (m ≡₂ n)
zero ≡₂? zero = yes refl
zero ≡₂? suc zero = no (λ ())
zero ≡₂? suc (suc n) = zero ≡₂? n
suc zero ≡₂? zero = no (λ ())
suc zero ≡₂? suc zero = yes refl
suc zero ≡₂? suc (suc n) = suc zero ≡₂? n
suc (suc n) ≡₂? n' = n ≡₂? n'