module Int

import UInt
import Base
import IntDefs
import IntAddSub
import IntMult
import IntLess
import IntAbs
import IntMod

/*
  Integer divisibility, gcd, and lcm.

  `divides(a, b)` is the existential `some k:Int. a*k = b`, the same
  shape as `UInt.divides`. The bridge `int_divides_iff_abs` lifts the
  Int question to the UInt one, which lets `gcd` and `lcm` be defined
  via the UInt versions on the absolute values:

      gcd(a, b) = pos(gcd(abs(a), abs(b)))
      lcm(a, b) = pos(lcm(abs(a), abs(b)))

  This is the divisor / common-multiple half of the Int division story
  (see issue #720). It is independent of the rounding convention chosen
  for `Int %`, since `divides` and `gcd`/`lcm` only care about the
  multiplicative structure.
*/

// Right distributivity of unary minus through multiplication.
// `dist_neg_mult` covers the left side; this lemma swaps via commutativity.
theorem int_neg_mult_right: all x:Int, y:Int.
  x * (- y) = - (x * y)
proof
  arbitrary x:Int, y:Int
  equations
    x * (- y) = (- y) * x  by int_mult_commute[x, - y]
          ... = - (y * x)  by symmetric dist_neg_mult[y, x]
          ... = - (x * y)  by replace int_mult_commute[y, x].
end

// `divides(a, b)` holds when some integer multiple of `a` equals `b`.
fun divides(a : Int, b : Int) {
  some k:Int. a * k = b
}

// Reflexivity: every integer divides itself.
theorem int_divides_refl: all n:Int. divides(n, n)
proof
  arbitrary n:Int
  expand divides
  choose +1
  int_mult_one[n]
end

// Every integer divides zero.
theorem int_divides_zero: all n:Int. divides(n, +0)
proof
  arbitrary n:Int
  expand divides
  choose +0
  int_mult_zero[n]
end

// `+1` divides every integer.
theorem int_one_divides: all n:Int. divides(+1, n)
proof
  arbitrary n:Int
  expand divides
  choose n
  int_one_mult[n]
end

// Negation on either side preserves divisibility.
theorem int_divides_neg_right: all d:Int, n:Int.
  if divides(d, n) then divides(d, - n)
proof
  arbitrary d:Int, n:Int
  assume dn
  obtain k where dk_n: d * k = n from expand divides in dn
  expand divides
  choose - k
  have eq: d * (- k) = - (d * k) by int_neg_mult_right[d, k]
  replace eq | dk_n.
end

// Negation on the divisor side preserves divisibility.
theorem int_divides_neg_left: all d:Int, n:Int.
  if divides(d, n) then divides(- d, n)
proof
  arbitrary d:Int, n:Int
  assume dn
  obtain k where dk_n: d * k = n from expand divides in dn
  expand divides
  choose - k
  have eq: (- d) * (- k) = d * k by {
    equations
      (- d) * (- k) = - (d * (- k))   by symmetric dist_neg_mult[d, - k]
                ... = - (- (d * k))   by replace int_neg_mult_right[d, k].
                ... = d * k           by neg_involutive[d * k]
  }
  replace eq
  dk_n
end

// Transitivity of divisibility.
theorem int_divides_trans: all a:Int, b:Int, c:Int.
  if divides(a, b) and divides(b, c) then divides(a, c)
proof
  arbitrary a:Int, b:Int, c:Int
  assume prem
  obtain k where ak_b: a * k = b from expand divides in conjunct 0 of prem
  obtain l where bl_c: b * l = c from expand divides in conjunct 1 of prem
  expand divides
  choose k * l
  have eq1: (a * k) * l = c by replace symmetric ak_b in bl_c
  eq1
end

// Closure under addition.
theorem int_divides_add: all d:Int, m:Int, n:Int.
  if divides(d, m) and divides(d, n) then divides(d, m + n)
proof
  arbitrary d:Int, m:Int, n:Int
  assume prem
  obtain k where dk_m: d * k = m from expand divides in conjunct 0 of prem
  obtain l where dl_n: d * l = n from expand divides in conjunct 1 of prem
  expand divides
  choose k + l
  replace int_dist_mult_add[d, k, l] | dk_m | dl_n.
end

// Closure under subtraction.
theorem int_divides_sub: all d:Int, m:Int, n:Int.
  if divides(d, m) and divides(d, n) then divides(d, m - n)
proof
  arbitrary d:Int, m:Int, n:Int
  assume prem
  obtain k where dk_m: d * k = m from expand divides in conjunct 0 of prem
  obtain l where dl_n: d * l = n from expand divides in conjunct 1 of prem
  expand divides
  choose k - l
  replace int_dist_mult_sub[d, k, l] | dk_m | dl_n.
end

// Closure under multiplication on the right.
theorem int_divides_mult_right: all d:Int, n:Int, m:Int.
  if divides(d, n) then divides(d, n * m)
proof
  arbitrary d:Int, n:Int, m:Int
  assume dn
  obtain k where dk_n: d * k = n from expand divides in dn
  expand divides
  choose k * m
  have eq: (d * k) * m = n * m by replace dk_n.
  eq
end

// Closure under multiplication on the left.
theorem int_divides_mult_left: all d:Int, n:Int, m:Int.
  if divides(d, n) then divides(d, m * n)
proof
  arbitrary d:Int, n:Int, m:Int
  assume dn
  replace int_mult_commute[m, n]
  apply int_divides_mult_right[d, n, m] to dn
end

// Bridge: `Int.divides` is equivalent to `UInt.divides` on absolute
// values. Lets gcd/lcm theorems lift from the UInt versions.
theorem int_divides_iff_abs: all a:Int, b:Int.
  divides(a, b) ⇔ divides(abs(a), abs(b))
proof
  arbitrary a:Int, b:Int
  have fwd: if divides(a, b) then divides(abs(a), abs(b)) by {
    assume ab
    obtain k where ak_b: a * k = b from expand divides in ab
    expand divides
    choose abs(k)
    have eq: abs(a) * abs(k) = abs(b) by {
      replace symmetric int_abs_mult[a, k]
      replace ak_b.
    }
    eq
  }
  have bwd: if divides(abs(a), abs(b)) then divides(a, b) by {
    assume ab
    obtain k0 where ak0: abs(a) * k0 = abs(b) from expand divides in ab
    have abs_eq: abs(a * pos(k0)) = abs(b) by {
      replace int_abs_mult[a, pos(k0)]
      ak0
    }
    have ak_eq_or: a * pos(k0) = b or a * pos(k0) = - b
      by apply (conjunct 0 of int_abs_eq_iff_eq_or_neg[a * pos(k0), b]) to abs_eq
    expand divides
    cases ak_eq_or
    case ak_b_eq {
      choose pos(k0)
      ak_b_eq
    }
    case ak_negb {
      choose - pos(k0)
      have eq: a * (- pos(k0)) = b by {
        replace int_neg_mult_right[a, pos(k0)] | ak_negb | neg_involutive[b].
      }
      eq
    }
  }
  fwd, bwd
end

// Divisibility is antisymmetric up to absolute value: mutual divisibility
// pins down the magnitude, but not the sign (e.g. `+3` and `-3` divide each
// other). Lifts `uint_divides_antisymmetric` through `int_divides_iff_abs`.
theorem int_divides_antisymmetric: all a:Int, b:Int.
  if divides(a, b) and divides(b, a) then abs(a) = abs(b)
proof
  arbitrary a:Int, b:Int
  assume prem
  have ab: divides(abs(a), abs(b))
    by apply (conjunct 0 of int_divides_iff_abs[a, b]) to conjunct 0 of prem
  have ba: divides(abs(b), abs(a))
    by apply (conjunct 0 of int_divides_iff_abs[b, a]) to conjunct 1 of prem
  apply uint_divides_antisymmetric[abs(a), abs(b)] to ab, ba
end

// Divisibility bridges to the remainder: for a nonzero divisor, `m` divides
// `n` exactly when the truncated remainder `n % m` vanishes. The forward
// direction routes `abs(n % m)` through `int_abs_mod` /
// `uint_mult_mod_left_zero`; the backward direction reconstructs `n` from the
// division identity `int_div_mod` once the remainder is `+0`.
theorem int_divides_iff_mod_zero: all m:Int, n:Int.
  if not (m = +0) then (divides(m, n) ⇔ n % m = +0)
proof
  arbitrary m:Int, n:Int
  assume prem: not (m = +0)
  have mpos: 0 < abs(m) by {
    have nz: not (abs(m) = 0) by {
      assume az: abs(m) = 0
      conclude false
        by apply prem to (apply int_abs_eq_zero_implies_zero[m] to az)
    }
    apply uint_not_zero_pos to nz
  }
  have fwd: if divides(m, n) then n % m = +0 by {
    assume dvd
    obtain k where mk: m * k = n from expand divides in dvd
    have absmod0: abs(n % m) = 0 by {
      replace int_abs_mod[n, m] | symmetric mk | int_abs_mult[m, k]
      apply uint_mult_mod_left_zero[abs(k), abs(m)] to mpos
    }
    apply int_abs_eq_zero_implies_zero[n % m] to absmod0
  }
  have bwd: if n % m = +0 then divides(m, n) by {
    assume modz: n % m = +0
    have dm: (n / m) * m + (n % m) = n by apply int_div_mod[n, m] to prem
    have eq: (n / m) * m = n by replace modz in dm
    expand divides
    choose n / m
    replace int_mult_commute[m, n / m]
    eq
  }
  fwd, bwd
end

// Greatest common divisor on Int, defined through `UInt.gcd` on
// absolute values. The result is wrapped as `pos` so the gcd is always
// nonnegative.
fun gcd(a : Int, b : Int) {
  pos(gcd(abs(a), abs(b)))
}

// `gcd(a, b)` divides `a`.
theorem int_gcd_divides_left: all a:Int, b:Int. divides(gcd(a, b), a)
proof
  arbitrary a:Int, b:Int
  expand gcd
  have ug: divides(gcd(abs(a), abs(b)), abs(a))
    by uint_gcd_divides_left[abs(a), abs(b)]
  have unfold: abs(pos(gcd(abs(a), abs(b)))) = gcd(abs(a), abs(b))
    by int_abs_pos[gcd(abs(a), abs(b))]
  have ug2: divides(abs(pos(gcd(abs(a), abs(b)))), abs(a))
    by replace symmetric unfold in ug
  apply (conjunct 1 of int_divides_iff_abs[pos(gcd(abs(a), abs(b))), a]) to ug2
end

// `gcd(a, b)` divides `b`.
theorem int_gcd_divides_right: all a:Int, b:Int. divides(gcd(a, b), b)
proof
  arbitrary a:Int, b:Int
  expand gcd
  have ug: divides(gcd(abs(a), abs(b)), abs(b))
    by uint_gcd_divides_right[abs(a), abs(b)]
  have unfold: abs(pos(gcd(abs(a), abs(b)))) = gcd(abs(a), abs(b))
    by int_abs_pos[gcd(abs(a), abs(b))]
  have ug2: divides(abs(pos(gcd(abs(a), abs(b)))), abs(b))
    by replace symmetric unfold in ug
  apply (conjunct 1 of int_divides_iff_abs[pos(gcd(abs(a), abs(b))), b]) to ug2
end

// Greatest property: any common divisor `d` of `a` and `b` divides
// `gcd(a, b)`.
theorem int_gcd_greatest: all d:Int, a:Int, b:Int.
  if divides(d, a) and divides(d, b) then divides(d, gcd(a, b))
proof
  arbitrary d:Int, a:Int, b:Int
  assume prem
  have d_a: divides(d, a) by conjunct 0 of prem
  have d_b: divides(d, b) by conjunct 1 of prem
  have abs_d_a: divides(abs(d), abs(a))
    by apply (conjunct 0 of int_divides_iff_abs[d, a]) to d_a
  have abs_d_b: divides(abs(d), abs(b))
    by apply (conjunct 0 of int_divides_iff_abs[d, b]) to d_b
  have ug: divides(abs(d), gcd(abs(a), abs(b)))
    by apply uint_gcd_greatest[abs(d), abs(a), abs(b)] to abs_d_a, abs_d_b
  expand gcd
  have unfold: abs(pos(gcd(abs(a), abs(b)))) = gcd(abs(a), abs(b))
    by int_abs_pos[gcd(abs(a), abs(b))]
  have ug2: divides(abs(d), abs(pos(gcd(abs(a), abs(b)))))
    by replace symmetric unfold in ug
  apply (conjunct 1 of int_divides_iff_abs[d, pos(gcd(abs(a), abs(b)))]) to ug2
end

// Least common multiple on Int, wrapped in `pos` to be nonnegative.
fun lcm(a : Int, b : Int) {
  pos(lcm(abs(a), abs(b)))
}

// `lcm(+0, b) = +0`.
theorem int_lcm_zero_left: all b:Int. lcm(+0, b) = +0
proof
  arbitrary b:Int
  expand lcm.
end

// `lcm(a, +0) = +0`.
theorem int_lcm_zero_right: all a:Int. lcm(a, +0) = +0
proof
  arbitrary a:Int
  expand lcm.
end

// `a` divides `lcm(a, b)`. Lifts `uint_divides_lcm_left` through
// `int_divides_iff_abs`, since `lcm` is defined on absolute values.
theorem int_divides_lcm_left: all a:Int, b:Int. divides(a, lcm(a, b))
proof
  arbitrary a:Int, b:Int
  expand lcm
  have ul: divides(abs(a), lcm(abs(a), abs(b)))
    by uint_divides_lcm_left[abs(a), abs(b)]
  have unfold: abs(pos(lcm(abs(a), abs(b)))) = lcm(abs(a), abs(b))
    by int_abs_pos[lcm(abs(a), abs(b))]
  have ul2: divides(abs(a), abs(pos(lcm(abs(a), abs(b)))))
    by replace symmetric unfold in ul
  apply (conjunct 1 of int_divides_iff_abs[a, pos(lcm(abs(a), abs(b)))]) to ul2
end

// `b` divides `lcm(a, b)`. Mirrors `int_divides_lcm_left` through
// `uint_divides_lcm_right`.
theorem int_divides_lcm_right: all a:Int, b:Int. divides(b, lcm(a, b))
proof
  arbitrary a:Int, b:Int
  expand lcm
  have ul: divides(abs(b), lcm(abs(a), abs(b)))
    by uint_divides_lcm_right[abs(a), abs(b)]
  have unfold: abs(pos(lcm(abs(a), abs(b)))) = lcm(abs(a), abs(b))
    by int_abs_pos[lcm(abs(a), abs(b))]
  have ul2: divides(abs(b), abs(pos(lcm(abs(a), abs(b)))))
    by replace symmetric unfold in ul
  apply (conjunct 1 of int_divides_iff_abs[b, pos(lcm(abs(a), abs(b)))]) to ul2
end

// Universal property of the least common multiple on `Int`: every common
// multiple of `a` and `b` is a multiple of `lcm(a, b)`. Together with
// `int_divides_lcm_left`/`int_divides_lcm_right`, this characterizes
// `lcm(a, b)` as the least common multiple up to divisibility. Lifts
// `uint_lcm_least` through `int_divides_iff_abs`, since `lcm` is defined on
// absolute values.
theorem int_lcm_least: all a:Int, b:Int, m:Int.
  if divides(a, m) and divides(b, m) then divides(lcm(a, b), m)
proof
  arbitrary a:Int, b:Int, m:Int
  assume prem
  have ua: divides(abs(a), abs(m))
    by apply (conjunct 0 of int_divides_iff_abs[a, m]) to conjunct 0 of prem
  have ub: divides(abs(b), abs(m))
    by apply (conjunct 0 of int_divides_iff_abs[b, m]) to conjunct 1 of prem
  have ul: divides(lcm(abs(a), abs(b)), abs(m))
    by apply uint_lcm_least[abs(a), abs(b), abs(m)] to ua, ub
  expand lcm
  have unfold: abs(pos(lcm(abs(a), abs(b)))) = lcm(abs(a), abs(b))
    by int_abs_pos[lcm(abs(a), abs(b))]
  have ul2: divides(abs(pos(lcm(abs(a), abs(b)))), abs(m))
    by replace symmetric unfold in ul
  apply (conjunct 1 of int_divides_iff_abs[pos(lcm(abs(a), abs(b))), m]) to ul2
end

// Commutativity of `gcd` on `Int`, lifted from `uint_gcd_commutative`
// through the `abs`-based definition.
theorem int_gcd_commutative: all a:Int, b:Int. gcd(a, b) = gcd(b, a)
proof
  arbitrary a:Int, b:Int
  expand gcd
  replace uint_gcd_commutative[abs(a), abs(b)].
end

// Commutativity of `lcm` on `Int`, lifted from `uint_lcm_commutative`.
theorem int_lcm_commutative: all a:Int, b:Int. lcm(a, b) = lcm(b, a)
proof
  arbitrary a:Int, b:Int
  expand lcm
  replace uint_lcm_commutative[abs(a), abs(b)].
end

// The product of the gcd and lcm recovers the (absolute) product of the
// arguments: `gcd(a, b) * lcm(a, b) = pos(abs(a * b))`. Both `gcd` and
// `lcm` are nonnegative on `Int` (defined via `pos`/`abs`), so the product
// equals `|a * b|`; it lifts the `UInt` identity `uint_gcd_lcm_product`
// through `mult_pos_pos` and `int_abs_mult`.
theorem int_gcd_lcm_product: all a:Int, b:Int.
  gcd(a, b) * lcm(a, b) = pos(abs(a * b))
proof
  arbitrary a:Int, b:Int
  expand gcd | lcm
  replace mult_pos_pos[gcd(abs(a), abs(b)), lcm(abs(a), abs(b))]
  replace uint_gcd_lcm_product[abs(a), abs(b)]
  replace int_abs_mult[a, b].
end