module Int

import UInt
import Base
import IntDefs
import IntAddSub
import IntMult
import IntDiv
import IntLess

/*
  Theorems about Int absolute value.

  Lifts the structural identities `abs(pos(n)) = n` and
  `abs(negsuc(n)) = 1 + n` to public theorems, gives the
  `abs(x) = 0 ⇔ x = +0` characterization, and shows that absolute value
  distributes over multiplication. The closing trio (no zero divisors,
  left/right cancellation by a nonzero factor) lives here because the
  proofs route through `int_abs_mult` and `int_abs_eq_zero_implies_zero`.
*/

// Structural identity: a nonnegative integer's absolute value is its UInt magnitude.
theorem int_abs_pos: all n:UInt. abs(pos(n)) = n
proof
  arbitrary n:UInt
  expand abs.
end

auto int_abs_pos

// Structural identity: |negsuc(n)| = 1 + n (since negsuc(n) represents -(1+n)).
theorem int_abs_negsuc: all n:UInt. abs(negsuc(n)) = 1 + n
proof
  arbitrary n:UInt
  expand abs.
end

auto int_abs_negsuc

// |+0| = 0.
theorem int_abs_zero: abs(+0) = 0
proof
  evaluate
end

auto int_abs_zero

// If |x| = 0 then x is the integer zero. The negsuc branch is vacuous
// since |negsuc(n)| = 1 + n > 0.
theorem int_abs_eq_zero_implies_zero: all x:Int.
  if abs(x) = 0 then x = +0
proof
  arbitrary x:Int
  switch x {
    case pos(n) {
      assume n_eq_0
      replace n_eq_0
      evaluate
    }
    case negsuc(n) {
      .
    }
  }
end

// Converse of `int_abs_eq_zero_implies_zero`: the zero integer has zero absolute value.
theorem int_zero_implies_abs_eq_zero: all x:Int.
  if x = +0 then abs(x) = 0
proof
  arbitrary x:Int
  assume prem
  replace prem
  int_abs_zero
end

// Combined characterization: |x| = 0 iff x is the integer zero.
theorem int_abs_eq_zero_iff_zero: all x:Int.
  abs(x) = 0 ⇔ x = +0
proof
  arbitrary x:Int
  int_abs_eq_zero_implies_zero[x], int_zero_implies_abs_eq_zero[x]
end

// Two integers share an absolute value exactly when they are equal or
// negatives of each other. Useful as a normalization step in proofs that
// would otherwise re-derive this by case-splitting on `pos`/`negsuc`.
theorem int_abs_eq_iff_eq_or_neg: all x:Int, y:Int.
  abs(x) = abs(y) ⇔ x = y or x = - y
proof
  arbitrary x:Int, y:Int
  have fwd: if abs(x) = abs(y) then x = y or x = - y by {
    assume ax_ay: abs(x) = abs(y)
    switch x {
      case pos(a) assume xa {
        switch y {
          case pos(b) assume yb {
            have ab: a = b by replace xa | yb in ax_ay
            conclude pos(a) = pos(b) or pos(a) = - pos(b) by replace ab.
          }
          case negsuc(b) assume yb {
            have ab: a = 1 + b by replace xa | yb in ax_ay
            have nyb: - negsuc(b) = pos(1 + b) by expand operator-.
            have eq2: pos(a) = - negsuc(b) by replace ab | nyb.
            conclude pos(a) = negsuc(b) or pos(a) = - negsuc(b) by eq2
          }
        }
      }
      case negsuc(a) assume xa {
        switch y {
          case pos(b) assume yb {
            have ab: 1 + a = b by replace xa | yb in ax_ay
            have nxa: - negsuc(a) = pos(1 + a) by expand operator-.
            have eq2: - negsuc(a) = pos(b) by replace ab in nxa
            have eq3: negsuc(a) = - pos(b) by {
              have h: - - negsuc(a) = - pos(b) by replace eq2.
              replace neg_involutive[negsuc(a)] in h
            }
            conclude negsuc(a) = pos(b) or negsuc(a) = - pos(b) by eq3
          }
          case negsuc(b) assume yb {
            have ab: 1 + a = 1 + b by replace xa | yb in ax_ay
            have ab2: a = b by apply uint_add_both_sides_of_equal[1, a, b] to ab
            conclude negsuc(a) = negsuc(b) or negsuc(a) = - negsuc(b)
              by replace ab2.
          }
        }
      }
    }
  }
  have bwd: if x = y or x = - y then abs(x) = abs(y) by {
    assume disj
    cases disj
    case xy { replace xy. }
    case xny { replace xny | abs_neg[y]. }
  }
  fwd, bwd
end

// Absolute value distributes over multiplication: |x*y| = |x|*|y|.
theorem int_abs_mult: all x:Int, y:Int.
  abs(x * y) = abs(x) * abs(y)
proof
  arbitrary x:Int, y:Int
  switch x {
    case pos(x') {
      switch y {
        case pos(y') {
          replace mult_pos_pos.
        }
        case negsuc(y') {
          replace mult_pos_negsuc
          replace abs_neg
          replace uint_dist_mult_add.
        }
      }
    }
    case negsuc(x') {
      switch y {
        case pos(y') {
          replace int_mult_commute[negsuc(x'), pos(y')]
          replace mult_pos_negsuc
          replace abs_neg
          replace uint_dist_mult_add_right
          replace uint_mult_commute[y', x'].
        }
        case negsuc(y') {
          expand operator*
          replace sign_negsuc | mult_neg_neg | mult_pos_uint.
        }
      }
    }
  }
end

// Division analogue of `int_abs_mult`: absolute value distributes over
// integer division. Truncating division on `Int` is defined sign-then-
// magnitude, so once the four `pos`/`negsuc` cases of `x` and `y` are
// fixed the `div_pos_pos` / `div_pos_negsuc` / etc. auto rules collapse
// the LHS to a (possibly negated) `pos`-wrapped UInt quotient, and
// `abs_neg` peels any outer `-`.
theorem int_abs_div: all x:Int, y:Int. abs(x / y) = abs(x) / abs(y)
proof
  arbitrary x:Int, y:Int
  switch x {
    case pos(au) {
      switch y {
        case pos(bu) { . }
        case negsuc(bu) { replace abs_neg. }
      }
    }
    case negsuc(au) {
      switch y {
        case pos(bu) { replace abs_neg. }
        case negsuc(bu) { . }
      }
    }
  }
end

// Int has no zero divisors: a product is zero only if a factor is.
theorem int_mult_to_zero: all x:Int, y:Int.
  if x * y = +0 then x = +0 or y = +0
proof
  arbitrary x:Int, y:Int
  assume prem
  have abs_prod_zero: abs(x) * abs(y) = 0 by {
    equations
          abs(x) * abs(y)
        = abs(x * y)             by symmetric int_abs_mult[x, y]
    ... = abs(+0)                by replace prem.
    ... = 0                      by int_abs_zero
  }
  cases apply uint_mult_to_zero[abs(x), abs(y)] to abs_prod_zero
  case ax_zero {
    conclude x = +0 or y = +0
      by apply int_abs_eq_zero_implies_zero[x] to ax_zero
  }
  case ay_zero {
    conclude x = +0 or y = +0
      by apply int_abs_eq_zero_implies_zero[y] to ay_zero
  }
end

// Left cancellation by a nonzero factor in an Int equation.
theorem int_mult_left_cancel: all n:Int, x:Int, y:Int.
  if not (n = +0) and n * x = n * y then x = y
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have nnz: not (n = +0) by conjunct 0 of prem
  have nxy: n * x = n * y by conjunct 1 of prem
  // From n * x = n * y, derive n * (y - x) = +0.
  have prod_zero: n * (y - x) = +0 by {
    equations
          n * (y - x)
        = n * (y + -x)            by expand operator-.
    ... = n * y + n * (-x)        by int_dist_mult_add[n, y, -x]
    ... = n * y + -(n * x)        by {
            have neg_mult: n * (-x) = -(n * x) by {
              equations
                    n * (-x)
                  = (-x) * n          by int_mult_commute[n, -x]
              ... = -(x * n)          by symmetric dist_neg_mult[x, n]
              ... = -(n * x)          by replace int_mult_commute[x, n].
            }
            replace neg_mult.
          }
    ... = n * y + -(n * y)        by replace nxy.
    ... = +0                      by int_add_inverse[n * y]
  }
  cases apply int_mult_to_zero[n, y - x] to prod_zero
  case n_zero {
    conclude false by apply nnz to n_zero
  }
  case yx_zero {
    // y - x = +0 implies x = y.
    have y_neg_x: y + -x = +0 by expand operator- in yx_zero
    have x_neg_x: x + -x = +0 by int_add_inverse[x]
    have step: y + -x = x + -x by transitive y_neg_x (symmetric x_neg_x)
    symmetric apply int_add_both_sides_of_equal_right[-x, y, x] to step
  }
end

// Right cancellation by a nonzero factor in an Int equation.
theorem int_mult_right_cancel: all n:Int, x:Int, y:Int.
  if not (n = +0) and x * n = y * n then x = y
proof
  arbitrary n:Int, x:Int, y:Int
  assume prem
  have nnz: not (n = +0) by conjunct 0 of prem
  have xn_yn: x * n = y * n by conjunct 1 of prem
  have nxy: n * x = n * y by {
    replace int_mult_commute[n, x] | int_mult_commute[n, y]
    xn_yn
  }
  apply int_mult_left_cancel[n, x, y] to nnz, nxy
end

// Every integer is bounded above by the positive embedding of its
// absolute value: `x ≤ pos(abs(x))`. Together with `int_neg_abs_le`,
// this is the standard `-|x| ≤ x ≤ |x|` sandwich.
theorem int_le_abs: all x:Int. x ≤ pos(abs(x))
proof
  arbitrary x:Int
  switch x {
    case pos(n) {
      int_less_equal_refl[pos(n)]
    }
    case negsuc(n) { . }
  }
end

// The negation of the positive embedding of `abs(x)` is bounded above
// by `x`: `-pos(abs(x)) ≤ x`.
theorem int_neg_abs_le: all x:Int. -pos(abs(x)) ≤ x
proof
  arbitrary x:Int
  have h1: -x ≤ pos(abs(-x)) by int_le_abs[-x]
  have h2: -x ≤ pos(abs(x)) by replace abs_neg[x] in h1
  have h3: -pos(abs(x)) ≤ -(-x)
    by apply (conjunct 0 of int_neg_le_iff[-x, pos(abs(x))]) to h2
  replace neg_involutive[x] in h3
end

// Characterize `abs(x) ≤ y` (as UInt-to-UInt comparison) as a sandwich
// `-pos(y) ≤ x ≤ pos(y)` lifted into Int comparisons.
theorem int_abs_le_iff: all x:Int, y:UInt.
  abs(x) ≤ y ⇔ -pos(y) ≤ x and x ≤ pos(y)
proof
  arbitrary x:Int, y:UInt
  have fwd: if abs(x) ≤ y then -pos(y) ≤ x and x ≤ pos(y) by {
    assume prem
    have ax_le_y: pos(abs(x)) ≤ pos(y) by prem
    have x_le_ax: x ≤ pos(abs(x)) by int_le_abs[x]
    have x_le_y: x ≤ pos(y)
      by apply int_less_equal_trans[x, pos(abs(x)), pos(y)] to x_le_ax, ax_le_y
    have neg_ax_le_x: -pos(abs(x)) ≤ x by int_neg_abs_le[x]
    have neg_y_le_neg_ax: -pos(y) ≤ -pos(abs(x))
      by apply int_neg_le_mono[pos(abs(x)), pos(y)] to ax_le_y
    have neg_y_le_x: -pos(y) ≤ x
      by apply int_less_equal_trans[-pos(y), -pos(abs(x)), x] to neg_y_le_neg_ax, neg_ax_le_x
    neg_y_le_x, x_le_y
  }
  have bkwd: if -pos(y) ≤ x and x ≤ pos(y) then abs(x) ≤ y by {
    assume prem
    have lb: -pos(y) ≤ x by conjunct 0 of prem
    have ub: x ≤ pos(y) by conjunct 1 of prem
    have neg_x_le: -x ≤ pos(y) by {
      have temp: -pos(y) ≤ -(-x) by replace symmetric neg_involutive[x] in lb
      apply (conjunct 1 of int_neg_le_iff[-x, pos(y)]) to temp
    }
    switch x {
      case pos(n) assume xp {
        replace xp in ub
      }
      case negsuc(n) assume xn {
        have neg_x_eq: -x = pos(1 + n) by replace xn expand operator-.
        replace neg_x_eq in neg_x_le
      }
    }
  }
  fwd, bkwd
end

// Triangle inequality: `abs(x + y) ≤ abs(x) + abs(y)`. Routes through
// `int_abs_le_iff` to reduce the goal to the `-(abs(x)+abs(y)) ≤ x+y ≤
// abs(x)+abs(y)` sandwich, then adds `int_le_abs` and `int_neg_abs_le`
// componentwise.
theorem int_abs_add: all x:Int, y:Int. abs(x + y) ≤ abs(x) + abs(y)
proof
  arbitrary x:Int, y:Int
  have x_le: x ≤ pos(abs(x)) by int_le_abs[x]
  have y_le: y ≤ pos(abs(y)) by int_le_abs[y]
  have ub1: x + y ≤ pos(abs(x)) + pos(abs(y))
    by apply int_add_mono_less_equal[x, y, pos(abs(x)), pos(abs(y))] to x_le, y_le
  have ub: x + y ≤ pos(abs(x) + abs(y))
    by replace add_pos_pos[abs(x), abs(y)] in ub1
  have neg_x_le: -pos(abs(x)) ≤ x by int_neg_abs_le[x]
  have neg_y_le: -pos(abs(y)) ≤ y by int_neg_abs_le[y]
  have lb1: -pos(abs(x)) + -pos(abs(y)) ≤ x + y
    by apply int_add_mono_less_equal[-pos(abs(x)), -pos(abs(y)), x, y]
       to neg_x_le, neg_y_le
  have neg_eq: -pos(abs(x) + abs(y)) = -pos(abs(x)) + -pos(abs(y)) by {
    replace symmetric add_pos_pos[abs(x), abs(y)]
    neg_distr_add[pos(abs(x)), pos(abs(y))]
  }
  have lb: -pos(abs(x) + abs(y)) ≤ x + y by replace neg_eq lb1
  apply (conjunct 1 of int_abs_le_iff[x + y, abs(x) + abs(y)]) to lb, ub
end

// `abs(x - y) = abs(y - x)`: subtraction is symmetric inside absolute
// value. Use case analysis on the `pos`/`negsuc` representation: the
// `pos`/`pos` and `negsuc`/`negsuc` cases reduce to a `⊝` swap via
// `neg_monuso`; the cross-sign cases reduce after commuting addends.
theorem int_abs_sub_symm: all x:Int, y:Int. abs(x - y) = abs(y - x)
proof
  arbitrary x:Int, y:Int
  switch x {
    case pos(xu) {
      switch y {
        case pos(yu) {
          have lhs: pos(xu) - pos(yu) = (xu ⊝ yu) by symmetric subo_monus[xu, yu]
          have rhs: pos(yu) - pos(xu) = (yu ⊝ xu) by symmetric subo_monus[yu, xu]
          replace lhs | rhs
          have neg_swap: (yu ⊝ xu) = -(xu ⊝ yu) by symmetric neg_monuso[xu, yu]
          replace neg_swap | abs_neg[xu ⊝ yu].
        }
        case negsuc(yu) {
          // pos - negsuc: x + (1 + yu) on one side, abs of negsuc(yu + xu)
          // on the other. Reduce to a UInt equality by computing both
          // sides through `int_abs_pos` / `int_abs_negsuc`.
          have ya_eq: abs(pos(xu) - negsuc(yu)) = xu + (1 + yu) by {
            expand 2* operator-
            show abs(pos(xu) + pos(1 + yu)) = xu + (1 + yu)
            replace add_pos_pos[xu, 1 + yu]
            int_abs_pos[xu + (1 + yu)]
          }
          have yb_eq: abs(negsuc(yu) - pos(xu)) = 1 + (yu + xu) by {
            cases uint_zero_or_positive[xu]
            case xz: xu = 0 {
              replace xz
              show abs(negsuc(yu) - +0) = 1 + (yu + 0)
              have step: negsuc(yu) - +0 = negsuc(yu) by {
                expand 2* operator-.
              }
              replace step.
            }
            case xpos: 0 < xu {
              obtain xu' where xu_eq: xu = 1 + xu'
                from apply uint_positive_add_one to xpos
              replace xu_eq
              expand 2* operator-
              show abs(negsuc(yu) + negsuc(xu')) = 1 + (yu + (1 + xu'))
              replace add_negsuc_negsuc[yu, xu']
              // Goal: `2 + yu + xu' = 1 + yu + 1 + xu'` — same up to commute.
              show 2 + yu + xu' = 1 + yu + 1 + xu'
              have e: 1 + yu + 1 + xu' = 2 + yu + xu' by {
                replace uint_add_commute[yu, 1].
              }
              symmetric e
            }
          }
          replace ya_eq | yb_eq
          // Goal: xu + 1 + yu = 1 + yu + xu.
          replace uint_add_commute[xu, 1]
                | uint_add_commute[xu, yu].
        }
      }
    }
    case negsuc(xu) {
      switch y {
        case pos(yu) {
          have ya_eq: abs(negsuc(xu) - pos(yu)) = 1 + (xu + yu) by {
            cases uint_zero_or_positive[yu]
            case yz: yu = 0 {
              replace yz
              have step: negsuc(xu) - +0 = negsuc(xu) by {
                expand 2* operator-.
              }
              replace step.
            }
            case ypos: 0 < yu {
              obtain yu' where yu_eq: yu = 1 + yu'
                from apply uint_positive_add_one to ypos
              replace yu_eq
              expand 2* operator-
              show abs(negsuc(xu) + negsuc(yu')) = 1 + (xu + (1 + yu'))
              replace add_negsuc_negsuc[xu, yu']
              show 2 + xu + yu' = 1 + xu + 1 + yu'
              have e: 1 + xu + 1 + yu' = 2 + xu + yu' by {
                replace uint_add_commute[xu, 1].
              }
              symmetric e
            }
          }
          have yb_eq: abs(pos(yu) - negsuc(xu)) = yu + (1 + xu) by {
            expand 2* operator-
            show abs(pos(yu) + pos(1 + xu)) = yu + (1 + xu)
            replace add_pos_pos[yu, 1 + xu]
            int_abs_pos[yu + (1 + xu)]
          }
          replace ya_eq | yb_eq
          // Goal (after auto): 1 + xu + yu = yu + 1 + xu.
          show 1 + (xu + yu) = yu + (1 + xu)
          replace uint_add_commute[1 + xu, yu].
        }
        case negsuc(yu) {
          have lhs: negsuc(xu) - negsuc(yu) = ((1 + yu) ⊝ (1 + xu))
            by expand 2* operator- | operator+.
          have rhs: negsuc(yu) - negsuc(xu) = ((1 + xu) ⊝ (1 + yu))
            by expand 2* operator- | operator+.
          replace lhs | rhs
          have neg_swap: ((1 + xu) ⊝ (1 + yu)) = -((1 + yu) ⊝ (1 + xu))
            by symmetric neg_monuso[1 + yu, 1 + xu]
          replace neg_swap | abs_neg[(1 + yu) ⊝ (1 + xu)].
        }
      }
    }
  }
end

// Reverse triangle inequality: `abs(x) ∸ abs(y) ≤ abs(x - y)`. Standard
// consequence of `int_abs_add` applied to the identity `x = (x - y) + y`:
// `abs(x) ≤ abs(x - y) + abs(y)`, then read off the monus form.
theorem int_rev_triangle: all x:Int, y:Int. abs(x) ∸ abs(y) ≤ abs(x - y)
proof
  arbitrary x:Int, y:Int
  have h0: abs((x - y) + y) ≤ abs(x - y) + abs(y) by int_abs_add[x - y, y]
  have h1: abs(x) ≤ abs(x - y) + abs(y)
    by replace int_sub_add_cancel[x, y] in h0
  cases uint_dichotomy[abs(y), abs(x)]
  case ay_le_ax: abs(y) ≤ abs(x) {
    // `abs(y) ≤ abs(x)` means the monus does not truncate:
    // `(abs(x) ∸ abs(y)) + abs(y) = abs(x)`. Combine with `h1` and cancel.
    have monus_eq0: abs(y) + (abs(x) ∸ abs(y)) = abs(x)
      by apply uint_monus_add_identity[abs(x), abs(y)] to ay_le_ax
    have monus_eq: (abs(x) ∸ abs(y)) + abs(y) = abs(x)
      by replace uint_add_commute[abs(y), abs(x) ∸ abs(y)] in monus_eq0
    have combined: (abs(x) ∸ abs(y)) + abs(y) ≤ abs(x - y) + abs(y)
      by replace monus_eq h1
    have commuted: abs(y) + (abs(x) ∸ abs(y)) ≤ abs(y) + abs(x - y)
      by replace uint_add_commute[abs(x) ∸ abs(y), abs(y)]
              | uint_add_commute[abs(x - y), abs(y)] in combined
    apply (conjunct 0 of uint_add_both_sides_of_less_equal[abs(y), abs(x) ∸ abs(y), abs(x - y)])
      to commuted
  }
  case ax_l_ay: abs(x) < abs(y) {
    have axay: abs(x) ≤ abs(y) by apply uint_less_implies_less_equal to ax_l_ay
    have rw: abs(x) ∸ abs(y) = 0
      by apply (conjunct 0 of uint_monus_zero_iff_less_eq[abs(x), abs(y)]) to axay
    replace rw
    uint_zero_le
  }
end

// Symmetric form: `abs(y) ∸ abs(x) ≤ abs(x - y)`. Follows from
// `int_rev_triangle` after swapping operands inside `abs(- -)`.
theorem int_rev_triangle_right: all x:Int, y:Int. abs(y) ∸ abs(x) ≤ abs(x - y)
proof
  arbitrary x:Int, y:Int
  have step: abs(y) ∸ abs(x) ≤ abs(y - x) by int_rev_triangle[y, x]
  replace symmetric int_abs_sub_symm[x, y] in step
end

// Round-trip via `abs`: `pos(abs(x)) = x` exactly when `x` is nonnegative.
// This is the abs-routed analogue of `uint_fromNat_toNat` — the side
// where round-trip is total. The negative side is exactly excluded.
theorem int_pos_abs_eq_iff_nonneg: all x:Int.
  pos(abs(x)) = x  ⇔  +0 ≤ x
proof
  arbitrary x:Int
  switch x {
    case pos(n) {
      have fwd: if pos(abs(pos(n))) = pos(n) then +0 ≤ pos(n) by {
        assume _
        // `+0 ≤ pos(n)` reduces to `0 ≤ n` (auto via `int_pos_le_pos`).
        .
      }
      have bkwd: if +0 ≤ pos(n) then pos(abs(pos(n))) = pos(n) by {
        assume _.
      }
      fwd, bkwd
    }
    case negsuc(n) {
      have fwd: if pos(abs(negsuc(n))) = negsuc(n) then +0 ≤ negsuc(n) by {
        assume bad: pos(abs(negsuc(n))) = negsuc(n)
        conclude false by expand abs in bad
      }
      have bkwd: if +0 ≤ negsuc(n) then pos(abs(negsuc(n))) = negsuc(n) by {
        // `+0 ≤ negsuc(n)` is already `false` after auto.
        assume bad
        bad
      }
      fwd, bkwd
    }
  }
end