module UInt

import Base
import Nat
import UIntDefs
import UIntToFrom
import UIntLess
import UIntAdd

theorem toNat_mult: all x:UInt, y:UInt.
  toNat(x * y) = toNat(x) * toNat(y)
proof
  induction UInt
  case bzero {
    arbitrary y:UInt
    show toNat(bzero * y) = toNat(bzero) * toNat(y)
    expand operator* | toNat
    evaluate
  }
  case dub_inc(x') assume IH {
    arbitrary y:UInt
    show toNat(dub_inc(x') * y) = toNat(dub_inc(x')) * toNat(y)
    switch y {
      case bzero {
        expand operator* | toNat
        evaluate
      }
      case dub_inc(y') {
        expand operator* | toNat
        replace toNat_dub
        expand toNat
        replace toNat_add | toNat_add
        replace IH[y']
        replace nat_suc_one_add
        replace dist_mult_add[(ℕ2 + ℕ2 * toNat(x')), ℕ2, ℕ2*toNat(y')]
        replace mult_commute[toNat(x'), ℕ2]
        replace dist_mult_add_right[ℕ4, ℕ4*toNat(x'), toNat(y')].
      }
      case inc_dub(y') {
        expand operator* | toNat
        replace toNat_add | toNat_dub | toNat_add
        replace IH[y']
        replace nat_suc_one_add | dist_mult_add[(ℕ2 + ℕ2 * toNat(x')), ℕ1, ℕ2*toNat(y')]
        replace mult_commute[toNat(x'), ℕ2]
          | dist_mult_add_right[ℕ4, ℕ4*toNat(x'), toNat(y')].
      }
    }
  }
  case inc_dub(x') assume IH {
    arbitrary y:UInt
    show toNat(inc_dub(x') * y) = toNat(inc_dub(x')) * toNat(y)
    switch y {
      case bzero {
        expand operator* | toNat
        evaluate
      }
      case dub_inc(y') {
        expand operator* | toNat
        replace toNat_add | toNat_add | toNat_dub
        replace IH[y']
        replace dist_mult_add[ℕ2 * toNat(x'), ℕ2, ℕ2 * toNat(y')]
        replace mult_commute[toNat(x'), ℕ2]
        replace add_commute[ℕ4 * toNat(x'), ℕ2 * toNat(y')].
      }
      case inc_dub(y') {
        expand operator* | toNat
        replace toNat_add | toNat_add | toNat_dub
        replace IH[y']
        replace nat_suc_one_add | nat_suc_one_add
        replace dist_mult_add[ℕ2 * toNat(x'), ℕ1, ℕ2 * toNat(y')]
        replace mult_commute[toNat(x'), ℕ2]
        replace add_commute[ℕ2 * toNat(x'), ℕ2 * toNat(y')].
      }
    }
  }
end

theorem uint_mult_commute: all m:UInt, n:UInt.
  m * n = n * m
proof
  arbitrary m:UInt, n:UInt
  suffices toNat(m * n) = toNat(n * m)  by uint_toNat_injective
  replace toNat_mult
  mult_commute
end

theorem uint_mult_assoc: all m:UInt, n:UInt, o:UInt.
  (m * n) * o = m * (n * o)
proof
  arbitrary m:UInt, n:UInt, o:UInt
  suffices toNat((m * n) * o) = toNat(m * (n * o))  by uint_toNat_injective
  replace toNat_mult | toNat_mult.
end

associative operator* in UInt

postulate fromNat_mult: all x:Nat, y:Nat. (fromNat(x * y) = fromNat(x) * fromNat(y))
  
theorem lit_mult_fromNat: all x:Nat, y:Nat.
  fromNat(lit(x)) * fromNat(lit(y)) = fromNat(lit(x) * lit(y))
proof
  arbitrary x:Nat, y:Nat
  symmetric 
  fromNat_mult[lit(x), lit(y)]
end

auto lit_mult_fromNat

theorem uint_zero_mult: all n:UInt. 0 * n = 0
proof
  arbitrary n:UInt
  expand lit | fromNat | operator*.
end

auto uint_zero_mult

postulate uint_mult_zero: all n:UInt. n * 0 = 0

auto uint_mult_zero

theorem uint_one_mult: all n:UInt.
  1 * n = n
proof
  arbitrary n:UInt
  suffices toNat(1 * n) = toNat(n) by uint_toNat_injective
  replace toNat_mult
  evaluate
end

auto uint_one_mult

theorem uint_mult_one: all n:UInt.
  n * 1 = n
proof
  arbitrary n:UInt
  suffices toNat(n * 1) = toNat(n) by uint_toNat_injective
  replace toNat_mult
  evaluate
end

auto uint_mult_one

theorem uint_dist_mult_add:
  all a:UInt, x:UInt, y:UInt.
  a * (x + y) = a * x + a * y
proof
  arbitrary a:UInt, x:UInt, y:UInt
  suffices toNat(a * (x + y)) = toNat(a * x + a * y) by uint_toNat_injective
  replace toNat_mult | toNat_add | toNat_mult
  replace dist_mult_add.
end

postulate uint_dist_mult_add_right:
  all x:UInt, y:UInt, a:UInt.
  (x + y) * a = x * a + y * a

postulate uint_mult_to_zero: all n:UInt, m:UInt.
  (if n * m = 0 then n = 0 or m = 0)

postulate uint_two_mult: all n:UInt. 2 * n = n + n

postulate uint_mult_mono_le: (all n:UInt, x:UInt, y:UInt. (if x ≤ y then n * x ≤ n * y))

postulate uint_mult_mono_le2 : all n : UInt, x : UInt, m:UInt, y : UInt. (if n ≤ m and x ≤ y then n * x ≤ m * y)

lemma inc_dub_add_mult2: all n:UInt. inc_dub(n) = 1 + 2 * n
proof  
  arbitrary n:UInt
  suffices toNat(inc_dub(n)) = toNat(1 + 2 * n)  by uint_toNat_injective
  replace toNat_add | toNat_mult
  expand toNat
  replace uint_toNat_fromNat
  replace nat_suc_one_add.
end

lemma dub_inc_mult2_add: all n:UInt. dub_inc(n) = 2 * (1 + n)
proof
  arbitrary n:UInt
  suffices toNat(dub_inc(n)) = toNat(2 * (1 + n))  by uint_toNat_injective
  replace toNat_mult | toNat_add
  expand toNat
  replace uint_toNat_fromNat.
end

postulate uint_pos_mult_both_sides_of_less : all n : UInt, x : UInt, y : UInt.
  (if 0 < n and x < y then n * x < n * y)