module Homework3 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 = {!!}

  lemma-n-minus-1 : ∀ n m -> n == succ m -> n - 1 == m
  lemma-n-minus-1 = {!!}
  
  lemma-plus-minus : ∀ n m k -> k == n + m -> k - n == m
  lemma-plus-minus = {!!}
  
  lemma-n-minus-n : ∀ n -> n - n == zero
  lemma-n-minus-n = {!!}
  
  lemma-succ-n-minus-n : ∀ n -> succ n - n == 1
  lemma-succ-n-minus-n = {!!}
  
  lemma-sum-minus-sum : ∀ x y n -> x + n - (y + n) == x - y
  lemma-sum-minus-sum = {!!}
  
  lemma-minus-dist : ∀ x y n -> (x - y) * n == x * n - y * n
  lemma-minus-dist = {!!}
  
-- ----------------------------------------------------------------------
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 = {!!}

  dividesTrans : ∀ n m l -> n divides m -> m divides l -> n divides l
  dividesTrans = {!!}
  
  dividesAdd : ∀ n m l -> n divides m -> n divides l -> n divides (m + l)
  dividesAdd = {!!}
                                                              
  addDivides : ∀ n m l -> n divides (m + l) -> n divides m -> n divides l
  addDivides = {!!}

  one-divides : ∀ n -> 1 divides n
  one-divides = {!!}
  
  divides-zero : ∀ n -> n divides 0
  divides-zero = {!!}
  
  one-not-divisible : ∀ n -> 1 < n -> ¬ (n divides 1)
  one-not-divisible = {!!}

  mult-divides : ∀ n m l -> n divides m -> n divides l * m
  mult-divides = {!!}

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

  open Nat
  open Divisibility
  open Logic
  open Equality
  open Ordering

  -- Define the factorial function.
  _! : ℕ -> ℕ
  n ! = {!!}

  infix 13 _!

  -- Prove the following properties.
  divFact : ∀ n m -> 1 ≤ m -> m ≤ n -> m divides n !
  divFact = {!!}
  
  not-divides-n!+1 : ∀ n m -> 1 < m -> m ≤ n -> ¬ (m divides ((n !) + 1))
  not-divides-n!+1 = {!!}