module Nat

import Option
import Base
import NatDefs
import NatAdd
import NatMonus
import NatMult
import NatLess
import NatDiv

/*
 Properties of pow2
 */
 
lemma pow_positive: all n:Nat. zero < pow2(n)
proof
  induction Nat
  case zero {
    evaluate
  }
  case suc(n') suppose IH {
    suffices zero < suc(suc(zero)) * pow2(n')  by expand pow2.
    obtain pn' where pn_s: pow2(n') = suc(pn')
        from apply positive_suc[pow2(n')] to IH
    suffices zero < suc(suc(zero)) * suc(pn')  by replace pn_s.
    suffices zero < suc(pn') + (suc(pn') + zero)  by expand operator*.
    suffices zero < suc(pn') + suc(pn')  by .
    suffices zero < suc(pn' + suc(pn'))  by expand operator+.
    suffices zero < suc(suc(pn' + pn'))  by replace add_suc[pn'][pn'].
    evaluate
  }
end


/* 
  Properties of exponentiation
  https://rocq∸prover.org/doc/v8.9/stdlib/Coq.Numbers.NatInt.NZPow.html
  and
  https://coq.kwarc.info/Coq.Numbers.NatInt.NZPow.html
  */

lemma expt_one : all n : Nat.
  n ^ suc(zero) = n
proof
  arbitrary n : Nat
  suffices n * suc(zero) = n by evaluate
  mult_one
end

lemma one_expt : all n : Nat.
  suc(zero) ^ n = suc(zero)
proof
  induction Nat
  case zero {
    evaluate
  }
  case suc(n') assume IH {
    have IH' : expt(n', suc(zero)) = suc(zero) by expand operator^ in IH
    suffices suc(zero) * expt(n', suc(zero)) = suc(zero) by expand operator^ | expt.
    replace IH'.
  }
end

theorem pow_add_r : all n : Nat, m : Nat, o : Nat.
  m ^ (n + o) = m ^ n * m ^ o
proof
  induction Nat
  case zero {
    arbitrary m : Nat, o : Nat
    suffices expt(o, m) = expt(o, m) + zero by evaluate
    .
  }
  case suc(n') assume IH {
    arbitrary m : Nat, o : Nat
    have IH' : (all m':Nat, o':Nat. expt(n' + o', m') = expt(n', m') * expt(o', m')) 
      by expand operator^ in IH
    suffices  m * expt(n' + o, m) = m * expt(n', m) * expt(o, m) 
      by expand operator^ | operator+ | expt.
    replace IH'.
  }
end

theorem pow_mul_l : all o : Nat, m : Nat, n : Nat.
  (m * n) ^ o = m ^ o * n ^ o
proof
  induction Nat
  case zero {
    evaluate
  }
  case suc(o') assume IH {
    arbitrary m : Nat, n : Nat
    have IH' : (all m':Nat, n':Nat. expt(o', m' * n') = expt(o', m') * expt(o', n')) 
      by evaluate in IH
    suffices  m * n * expt(o', m * n) = m * expt(o', m) * n * expt(o', n) by evaluate
    replace IH' | mult_commute[n, expt(o', m)].
  }
end

theorem pow_mul_r : all o : Nat, m : Nat, n : Nat.
  (m ^ n) ^ o = m ^ (n * o)
proof
  induction Nat
  case zero {
    arbitrary m : Nat, n : Nat
    suffices (m ^ n) ^ zero = m ^ zero by .
    evaluate
  }
  case suc(o') assume IH {
    arbitrary m : Nat, n : Nat
    have IH' :  (all m':Nat, n':Nat. expt(o', expt(n', m')) = expt(n' * o', m')) 
      by expand operator^ in IH
    suffices expt(n, m) * expt(n * o', m) = expt(n + n * o', m) by {
      expand operator^ | expt
      replace mult_suc[n, o'] | IH'.
    }
    symmetric expand operator^ in pow_add_r[n, m, n * o']
  }
end

lemma pow_pos_nonneg : all b : Nat, a : Nat.
  if zero<a then zero<a^b
proof
  induction Nat
  case zero {
    evaluate
  }
  case suc(b') assume IH {
    arbitrary a : Nat
    assume prem
    suffices zero < a * expt(b', a) by expand operator^ | expt.
    have exp_nz : zero < expt(b', a) by expand operator^ in apply IH to prem
    apply mult_pos_nonneg to prem, exp_nz
  }
end


lemma pow_zero_l : all a : Nat. if zero<a then zero^a = zero
proof
  arbitrary a : Nat
  switch a {
    case zero {
      evaluate
    }
    case suc(n') {
      evaluate
    }
  }
end


lemma pow_eq_zero : all n : Nat, m : Nat.
  if m ^ n = zero then m = zero
proof
  induction Nat
  case zero {
    evaluate
  }
  case suc(n') assume IH {
    arbitrary m : Nat
    switch m {
      case zero assume eq_z_t {
        evaluate
      }
      case suc(m') assume eq_sn_t {
        assume contra
        have contra' : suc(m') * expt(n', suc(m')) = zero 
          by expand operator^ | expt in contra
        have e_n_sm_z : expt(n', suc(m')) = zero by apply mult_to_zero to contra'
        have IH' : all m'':Nat. if expt(n', m'') = zero then m'' = zero 
          by expand operator^ in IH
        conclude false by apply IH'[suc(m')] to e_n_sm_z
      }
    }
  }
end

lemma exp_one_implies_zero_or_one : all m : Nat, n : Nat.
  if m ^ n = suc(zero) then n = zero or m = suc(zero)
proof 
  arbitrary m : Nat, n : Nat
  switch n {
    case zero  {
      .
    }
    case suc(n') {
      suffices  (if m * expt(n', m) = suc(zero) then m = suc(zero)) by evaluate
      assume prem
      apply one_mult_one to prem
    }
  }
end

lemma pow_lt_mono_l : all  c : Nat, a : Nat, b : Nat.
  if zero < c then if a < b then a ^ c < b ^ c
proof
  induction Nat
  case zero {
    evaluate
  }
  case suc(n') assume IH {
    arbitrary a : Nat, b : Nat
    assume z_l_sc
    assume alb
    switch zero < n' {
      case true assume prop_t {
        suffices a * expt(n', a) < b * expt(n', b) 
          by expand operator^ | expt.
        have ena_l_enb : expt(n', a) < expt(n', b) 
          by expand operator^ in apply (replace prop_t in IH) to alb
        have enb_nz :  expt(n', b) > zero by {
          expand operator >
          apply greater_any_zero to ena_l_enb
        }
        have bnz : zero < b 
          by apply greater_any_zero to alb
        have step1 : a * expt(n', a) <= a * expt(n', b)
          by apply mult_mono_le[a, expt(n', a), expt(n', b)] to 
            (apply less_implies_less_equal to ena_l_enb)
        have step2 : a * (expt(n',b)) < b * expt(n', b) 
          by apply (apply mult_lt_mono_l[expt(n', b), a, b] to enb_nz) to alb

        cases (apply less_equal_implies_less_or_equal to step1) 
        case step1':  a * expt(n', a) < a * expt(n', b) {
          apply less_trans[a * expt(n', a), a * expt(n', b)] to step1', step2
        }
        case step1'':  a * expt(n', a) = a * expt(n', b) {
          replace symmetric step1'' in step2
        }
      }
      case false assume prop_f {
        have nz : n' = zero by replace prop_f in zero_or_positive[n']
        suffices a < b by replace nz | expt_one.
        alb
      }
    }
  }
end

lemma pow_gt_1 : all n : Nat, m : Nat.
  if suc(zero) < n then (zero < m <=> suc(zero) < n ^ m)
proof
  arbitrary n : Nat, m : Nat
  assume prem
  have l : if zero < m then suc(zero) < n ^ m by {
    assume zlm
    replace symmetric one_expt[m]
    show suc(zero)^m < n^m
    suffices suc(zero) < n by apply pow_lt_mono_l[m, suc(zero), n] to zlm
    prem
  }
  have r : if suc(zero) < n ^ m then zero < m by {
    assume nm_g1
    cases zero_or_positive[m]
    case zm : m = zero {
      evaluate in replace zm in nm_g1 
    }
    case : zero < m { recall zero < m }
  }
  r, l
end

theorem pow_le_mono_l : all c : Nat, a : Nat, b : Nat.
  if a <= b then a ^ c <= b ^ c
proof 
  induction Nat
  case zero {
    evaluate
  }
  case suc(n') assume IH {
    arbitrary a : Nat, b : Nat
    assume a_le_b
    suffices  a * expt(n', a) ≤ b * expt(n', b) 
      by expand operator^ | expt.
    have step : expt(n', a) <= expt(n', b)
      by expand operator^ in (apply IH to a_le_b)
    have step1 : a * expt(n', a) <= a * expt(n', b)
      by apply mult_mono_le[a, expt(n', a), expt(n', b)] to step
    have step2 : a * expt(n', b) <= b * expt(n', b)
      by apply mult_mono_le_r[expt(n', b), a, b] to a_le_b
    apply less_equal_trans[a * expt(n', a), a * expt(n', b)] to step1, step2
  }
end

lemma pow_lt_mono_r : all c : Nat, a : Nat, b : Nat.
  if suc(zero) < a then if b < c then a^b < a^c
proof
  arbitrary c : Nat, a : Nat, b : Nat
  assume prem
  assume blc
  have blec : b <= c by apply less_implies_less_equal to blc
  obtain x where step from apply le_exists_monus to blec
  replace step | pow_add_r | mult_commute[a^b, a^x]
  show suc(zero) * a ^ b < a ^ x * suc(zero) * a ^ b
  have zla : zero < a by {
    have zl1 : zero < suc(zero) by evaluate
    apply less_trans[zero, suc(zero), a] to zl1, prem
  }
  have : a ^ b > zero by {
    expand operator>
    apply pow_pos_nonneg[b, a] to zla
  }
  suffices suc(zero) < a^x * suc(zero)
    by (apply mult_lt_mono_l[a^b, suc(zero), a^x * suc(zero)] to recall a^b > zero)
  have zlx : zero < x by {
    cases zero_or_positive[x]
    case xz : x = zero {
      have cb : c = b by replace xz in step
      apply less_irreflexive to replace cb in blc 
    }
    case : zero < x { recall zero < x }
  }
  replace symmetric mult_one[a^x] in apply (apply pow_gt_1[a, x] to prem) to zlx
end

lemma pow_inj_l : all a : Nat, b : Nat, c : Nat.
  if zero < c then (if a^c = b^c then a = b)
proof
  arbitrary a : Nat, b : Nat, c : Nat
  assume zlc
  assume ac_eq_bc
  cases trichotomy[a, b]
  case : a < b {
    have contra : a^c < b^c by apply (apply pow_lt_mono_l[c, a, b] to zlc) to (recall a < b)
    apply less_irreflexive to replace ac_eq_bc in contra
  }
  case : a = b { recall a = b }
  case : b < a {
    have contra : b^c < a^c by apply (apply pow_lt_mono_l[c, b, a] to zlc) to (recall b < a)
    apply less_irreflexive to replace ac_eq_bc in contra
  }
end

lemma pow_inj_r : all a : Nat, b : Nat, c : Nat.
  if suc(zero) < a then if a^b = a ^ c then b = c
proof
  arbitrary a : Nat, b : Nat, c : Nat
  assume ola
  assume ab_eq_ac
  cases trichotomy[b, c]
  case : b < c {
    apply less_irreflexive to
      replace ab_eq_ac in
      apply apply pow_lt_mono_r[c,a,b] to ola to recall b < c
  }
  case : b = c { recall b = c }
  case : c < b {
    apply less_irreflexive to
      replace ab_eq_ac in
      apply apply pow_lt_mono_r[b,a,c] to ola to recall c < b
  }
end

/*
  Properties of log
  */

lemma add_less_equal_pow_find_log: all m:Nat. all n:Nat, l:Nat.
  if n ≤ pow2(l)
  then m + n ≤ pow2(find_log(m, n, l))
proof
  induction Nat
  case zero {
    arbitrary n:Nat, l:Nat
    suppose n_le_pl: n ≤ pow2(l)
    suffices n ≤ pow2(l)
        by expand find_log.
    n_le_pl
  }
  case suc(m') suppose IH {
    arbitrary n:Nat, l:Nat
    suppose prem
    switch pow2(l) < suc(n) for find_log {
      case true {
        have sn_le_spl: suc(n) ≤ suc(pow2(l)) by {
          suffices n ≤ pow2(l) by expand operator ≤.
          prem
        }
        obtain p where pl_sp: pow2(l) = suc(p) from
          (apply positive_suc[pow2(l)] to pow_positive[l])
        have sn_le_psl: suc(n) ≤ pow2(suc(l)) by {
          suffices suc(n) ≤ suc(p) + suc(p) by {
            expand pow2 | operator*
            replace pl_sp.
          }
          suffices n ≤ pow2(l) + p by {
            expand operator+ | operator≤
            replace symmetric pl_sp | add_commute[p][pow2(l)].
          }
          apply less_equal_trans[n][pow2(l), pow2(l) + p] 
          to prem, less_equal_add[pow2(l)][p]
        }
        have IH': m' + suc(n) ≤ pow2(find_log(m',suc(n),suc(l)))
          by apply IH[suc(n),suc(l)] to sn_le_psl
        conclude suc(m') + n ≤ pow2(find_log(m',suc(n),suc(l))) by {
          suffices suc(m' + n) ≤ pow2(find_log(m', suc(n), suc(l)))
            by expand operator+.
          replace add_suc[m'][n] in IH'
        }
      }
      case false suppose pl_l_sn_false {
        have not_pl_l_sn: not (pow2(l) < suc(n)) by {
          suppose pl_l_sn
          conclude false by replace pl_l_sn_false in pl_l_sn
        }
        have sn_le_pl: suc(n) ≤ pow2(l)
          by apply not_less_implies_less_equal[pow2(l)][suc(n)] to not_pl_l_sn
        have IH': m' + suc(n) ≤ pow2(find_log(m',suc(n),l))
          by apply IH[suc(n), l] to sn_le_pl
        conclude suc(m') + n ≤ pow2(find_log(m',suc(n),l)) by {
          suffices suc(m' + n) ≤ pow2(find_log(m', suc(n), l))
            by expand operator +.
          replace add_suc[m'][n] in IH'
        }
      }
    }
  }
end

theorem less_equal_pow_log: all n:Nat.
  n ≤ pow2(log(n))
proof
  arbitrary n:Nat
  suffices n ≤ pow2(find_log(n, zero, zero)) by expand log.
  have f1: n + zero ≤ pow2(find_log(n, zero, zero))
    by apply add_less_equal_pow_find_log[n][zero,zero] to
       apply less_implies_less_equal[ zero ][pow2(zero)] to pow_positive[ zero ]
  conclude n ≤ pow2(find_log(n,zero,zero))
    by { evaluate in f1 }
end