module Homework3-answers where

import Nat
import Equality
import Logic
import Ordering

-- In this homework, you may require additional lemmas. State and
-- prove all lemmas you might need.

-- ----------------------------------------------------------------------
module Subtraction where
 
  open Nat
  open Equality

  -- We define the truncated subtraction operation. It is like
  -- ordinary subtraction, except that n - m = 0 when n < m.
  _-_ : ℕ -> ℕ -> ℕ
  x - zero = x
  zero - succ y = zero
  succ x - succ y = x - y

  infixl 7 _-_

  -- Prove the following lemmas:

  lemma-0-minus-n : ∀ n -> 0 - n == 0
  lemma-0-minus-n zero = refl
  lemma-0-minus-n (succ n) = refl
  
  lemma-n-minus-1 : ∀ n m -> n == succ m -> n - 1 == m
  lemma-n-minus-1 (succ n) m h1 = context (\ n -> n - 1) h1
  
  lemma-n-minus-succ : ∀ n m -> n - m - 1 == n - succ m
  lemma-n-minus-succ zero m = context (\ n -> n - 1) (lemma-0-minus-n m)
  lemma-n-minus-succ (succ n) zero = refl
  lemma-n-minus-succ (succ n) (succ m) = lemma-n-minus-succ n m
  
  lemma-plus-minus : ∀ n m k -> k == n + m -> k - n == m
  lemma-plus-minus zero m k h = h
  lemma-plus-minus (succ n) m k h =
    trans (symm (lemma-n-minus-succ k n)) (context (\ n -> n - 1) (lemma-plus-minus n (succ m) k (trans h (lemma-add-succ n m))))
  
  lemma-n-minus-n : ∀ n -> n - n == zero
  lemma-n-minus-n zero = refl
  lemma-n-minus-n (succ n) = lemma-n-minus-n n
  
  lemma-succ-n-minus-n : ∀ n -> succ n - n == 1
  lemma-succ-n-minus-n zero = refl
  lemma-succ-n-minus-n (succ n) = lemma-succ-n-minus-n n
  
  lemma-sum-minus-sum : ∀ x y n -> x + n - (y + n) == x - y
  lemma-sum-minus-sum x y zero =
    equational x + zero - (y + zero)
       by context (\ u -> u - (y + 0)) (symm (lemma-add-m-zero x))
      equals x - (y + 0)
        by context (\ u -> x - u) (symm (lemma-add-m-zero y))
      equals x - y
  lemma-sum-minus-sum zero zero (succ n) = lemma-sum-minus-sum zero zero n
  lemma-sum-minus-sum zero (succ y) (succ n) = helper n y
    where helper : (n y : ℕ) -> n - (y + succ n) == zero
          helper zero y = lemma-0-minus-n (y + 1)
          helper (succ n) y =  equational succ n - (y + succ (succ n))
                                   by context (\ u -> succ n - u) (symm (lemma-add-succ y (succ n)))
                                  equals n - (y + succ n)
                                    by helper n y
                                  equals 0
  lemma-sum-minus-sum (succ x) zero (succ n) = helper x n
    where helper : (x n : ℕ) -> x + succ n - n == succ x
          helper zero n = lemma-succ-n-minus-n n
          helper (succ x) zero = context succ (helper x zero)
          helper (succ x) (succ n) = trans (context (\ u -> u - n) (symm (lemma-add-succ x (succ n)))) (helper (succ x) n)
  lemma-sum-minus-sum (succ x) (succ y) (succ n) = lemma-sum-minus-sum x y (succ n)
  
  lemma-minus-dist : ∀ x y n -> (x - y) * n == x * n - y * n
  lemma-minus-dist zero zero n = refl
  lemma-minus-dist zero (succ y) n = symm (lemma-0-minus-n (y * n + n))
  lemma-minus-dist (succ x) zero n = refl
  lemma-minus-dist (succ x) (succ y) n =
    trans (lemma-minus-dist x y n) (symm (lemma-sum-minus-sum (x * n) (y * n) n))
  
-- ----------------------------------------------------------------------
module Divisibility where

  open Nat
  open Logic
  open Equality
  open Ordering
  open Subtraction

  -- We define the divisibility relation.
  _divides_ : ℕ -> ℕ -> Set
  n divides m = ∃ \(k : ℕ) -> k * n == m

  infix 5 _divides_

  -- Prove the following properties:xs
  
  dividesRefl : ∀ n -> n divides n
  dividesRefl n = (1 , refl)

  dividesTrans : ∀ n m l -> n divides m -> m divides l -> n divides l
  dividesTrans n m l (a , x) (b , y) = ((b * a) , pf)
    where pf : b * a * n == l
          pf = equational b * a * n
                 by theorem-mult-associative b a n 
                equals b * (a * n) 
                  by context (\ u -> b * u) x 
                equals b * m
                  by y
                equals l
  
  addEq : ∀ x y u v -> x == y -> u == v -> x + u == y + v
  addEq x y u v h1 h2 =
    equational x + u
      by context (\ x -> x + u) h1
      equals y + u
      by context (\ x -> y + x) h2
      equals y + v
  
  dividesAdd : ∀ n m l -> n divides m -> n divides l -> n divides (m + l)
  dividesAdd n m l (a , x) (a₁ , x₁) =
    ((a + a₁) ,
      trans (theorem-right-distributive a a₁ n) (addEq (a * n) m (a₁ * n) l x x₁))
      
  addDivides : ∀ n m l -> n divides (m + l) -> n divides m -> n divides l
  addDivides n m l (k1 , x) (k2 , x₁) =
    ((k1 - k2) , trans (lemma-minus-dist k1 k2 n) (trans (context (\ u -> k1 * n - u) x₁) (lemma-plus-minus m l (k1 * n) x) ))

  one-divides : ∀ n -> 1 divides n
  one-divides n = (n , lemma-mult-one n)
  
  divides-zero : ∀ n -> n divides 0
  divides-zero n = (zero , refl)
  
  succ-not-1 : ∀ {A : Set} -> (a n : ℕ) -> a * succ (succ n) == 1 -> A
  succ-not-1 zero n ()
  succ-not-1 (succ a) n h = helper (a * succ (succ n)) n h
    where
      helper : {A : Set} -> (a n : ℕ) -> a + succ (succ n) == 1 -> A
      helper (succ a) n h =  helper a (succ n) (trans (symm (lemma-add-succ a (succ (succ n)))) h)

  one-not-divisible : ∀ n -> 1 < n -> ¬ (n divides 1)
  one-not-divisible .(succ (succ _)) (less-succ (less-zero {n})) (a , x) =
    succ-not-1 a n x

  mult-divides : ∀ n m l -> n divides m -> n divides l * m
  mult-divides n m l (a , hyp) = (l * a , claim)
      where
        claim : (l * a) * n == l * m
        claim =
          equational (l * a) * n
                  by theorem-mult-associative l a n
              equals l * (a * n)
                  by context (λ x → l * x) hyp
              equals l * m

-- ----------------------------------------------------------------------
module Factorial where

  open Nat
  open Divisibility
  open Logic
  open Equality
  open Ordering

  -- Define the factorial function.
  _! : ℕ -> ℕ
  0 ! = 1
  succ n ! = succ n * n !

  infix 13 _!

  -- Prove the following properties.
  divFact : ∀ n m -> 1 ≤ m -> m ≤ n -> m divides n !
  divFact zero .(succ m) (s≤s .0 m h1) ()
  divFact (succ n) m h1 h2 with theorem-≤-invert m n h2
  divFact (succ n) m h1 h2 | right x = (n ! , eq)
      where eq : (n !) * m == n * (n !) + (n !)
            eq = equational (n !) * m
                         by context (\ u -> (n !) * u) x
                     equals (n !) * (succ n)
                         by context (\ u -> (n !) * u) (symm (lemma-add-one n))
                     equals (n !) * (n + 1)
                         by theorem-left-distributive (n !) n 1
                     equals (n !) * n + (n !) * 1
                         by context (\ u -> (n !) * n + u) (lemma-mult-one (n !))
                     equals (n !) * n + (n !)
                         by context (\ u -> u + (n !)) (theorem-mult-commutative (n !) n) 
                     equals  n * (n !) + (n !)
  divFact (succ n) m h1 h2 | left x = dividesAdd m (n * (n !)) (n !) (mult-divides m (n !) n (divFact n m h1 x)) (divFact n m h1 x)
  
  not-divides-n!+1 : ∀ n m -> 1 < m -> m ≤ n -> ¬ (m divides ((n !) + 1))
  not-divides-n!+1 n m h1 h2 =
      λ x → one-not-divisible m h1 (addDivides m (n !) 1 x (divFact n m (theorem-<-to-≤ 1 m h1) h2))