module Int

import UInt
import Base
import IntDefs
import IntAddSub

/*
  Theorems about Int order.

  Less-than-or-equal (`≤`) and strict less-than (`<`) on Int are defined
  in `IntDefs.pf` by structural recursion on the `pos`/`negsuc`
  representation. This file develops the basic order laws (reflexive,
  transitive, antisymmetric, irreflexive, trichotomy, dichotomy), the
  connections between `<` and `≤` (reducing to the corresponding UInt
  facts in `UIntLess.pf`), min/max algebraic laws, and the addition
  monotonicity / cancellation theorems that mix `+` with `≤` and `<`.
*/

// Properties of less-than-or-equal.

theorem int_less_equal_refl: all n:Int. n ≤ n
proof
  arbitrary n:Int
  switch n {
    case pos(n') {
      expand operator≤
      uint_less_equal_refl
    }
    case negsuc(n') {
      expand operator≤
      uint_less_equal_refl
    }
  }
end

theorem int_less_equal_trans: all m:Int, n:Int, o:Int.
  if m ≤ n and n ≤ o then m ≤ o
proof
  arbitrary m:Int, n:Int, o:Int
  switch m {
    case pos(m') {
      switch n {
        case pos(n') {
          switch o {
            case pos(o') {
              expand operator≤
              uint_less_equal_trans
            }
            case negsuc(o') { expand operator≤. }
          }
        }
        case negsuc(n') { expand operator≤. }
      }
    }
    case negsuc(m') {
      switch n {
        case pos(n') {
          switch o {
            case pos(o') { expand operator≤. }
            case negsuc(o') { expand operator≤. }
          }
        }
        case negsuc(n') {
          switch o {
            case pos(o') { expand operator≤. }
            case negsuc(o') {
              expand operator≤
              assume nm_n_on
              apply uint_less_equal_trans[o',n',m'] to nm_n_on
            }
          }
        }
      }
    }
  }
end

theorem int_less_equal_antisymmetric:
  all x:Int, y:Int.
  if x ≤ y and y ≤ x
  then x = y
proof
  arbitrary x:Int, y:Int
  assume xy_n_yx
  switch x {
    case pos(x') assume x_pos {
      switch y {
        case pos(y') assume y_pos {
          have: x' ≤ y' and y' ≤ x' by expand operator≤ in replace x_pos | y_pos in xy_n_yx
          have: x' = y' by apply uint_less_equal_antisymmetric to (recall x' ≤ y' and y' ≤ x')
          conclude pos(x') = pos(y')  by replace (recall x' = y').
        }
        case negsuc(y') assume y_neg {
          conclude false by expand operator≤ in replace x_pos | y_neg in xy_n_yx
        }
      }
    }
    case negsuc(x') assume x_neg {
      switch y {
        case pos(y') assume y_pos {
          conclude false by expand operator≤ in replace x_neg | y_pos in xy_n_yx
        }
        case negsuc(y') assume y_neg {
          have: x' ≤ y' and y' ≤ x' by expand operator≤ in replace x_neg | y_neg in xy_n_yx
          have: x' = y' by apply uint_less_equal_antisymmetric to (recall x' ≤ y' and y' ≤ x')
          conclude negsuc(x') = negsuc(y')  by replace (recall x' = y').
        }
      }
    }
  }
end

// Properties of strict less-than.

theorem int_less_irreflexive: all x:Int. not (x < x)
proof
  arbitrary x:Int
  switch x {
    case pos(n) { expand operator<. }
    case negsuc(n) { expand operator<. }
  }
end

theorem int_less_implies_not_equal: all x:Int, y:Int.
  if x < y then not (x = y)
proof
  arbitrary x:Int, y:Int
  assume x_y: x < y
  assume xy_eq: x = y
  have y_y: y < y by replace xy_eq in x_y
  apply int_less_irreflexive[y] to y_y
end

theorem int_less_implies_less_equal: all x:Int, y:Int.
  if x < y then x ≤ y
proof
  arbitrary x:Int, y:Int
  switch x {
    case pos(x') {
      switch y {
        case pos(y') {
          expand operator< | operator≤
          uint_less_implies_less_equal
        }
        case negsuc(y') { expand operator<. }
      }
    }
    case negsuc(x') {
      switch y {
        case pos(y') { expand operator≤. }
        case negsuc(y') {
          expand operator< | operator≤
          uint_less_implies_less_equal
        }
      }
    }
  }
end

theorem int_less_trans: all x:Int, y:Int, z:Int.
  if x < y and y < z then x < z
proof
  arbitrary x:Int, y:Int, z:Int
  switch x {
    case pos(x') {
      switch y {
        case pos(y') {
          switch z {
            case pos(z') {
              expand operator<
              assume prem
              apply uint_less_trans[x', y', z'] to prem
            }
            case negsuc(z') { expand operator<. }
          }
        }
        case negsuc(y') { expand operator<. }
      }
    }
    case negsuc(x') {
      switch y {
        case pos(y') {
          switch z {
            case pos(z') { expand operator<. }
            case negsuc(z') { expand operator<. }
          }
        }
        case negsuc(y') {
          switch z {
            case pos(z') { expand operator<. }
            case negsuc(z') {
              expand operator<
              assume prem
              apply uint_less_trans[z', y', x'] to prem
            }
          }
        }
      }
    }
  }
end

theorem int_less_equal_implies_less_or_equal: all x:Int, y:Int.
  if x ≤ y then x < y or x = y
proof
  arbitrary x:Int, y:Int
  switch x {
    case pos(x') {
      switch y {
        case pos(y') {
          assume xy
          have A: x' ≤ y' by expand operator≤ in xy
          have B: x' < y' or x' = y' by expand operator≤ in A
          cases B
          case x_l_y: x' < y' {
            conclude pos(x') < pos(y') or pos(x') = pos(y') by {
              have h: pos(x') < pos(y') by expand operator< x_l_y
              h
            }
          }
          case x_eq_y: x' = y' {
            conclude pos(x') < pos(y') or pos(x') = pos(y') by {
              have h: pos(x') = pos(y') by replace x_eq_y.
              h
            }
          }
        }
        case negsuc(y') {
          assume xy
          conclude false by expand operator≤ in xy
        }
      }
    }
    case negsuc(x') {
      switch y {
        case pos(y') {
          assume xy
          conclude negsuc(x') < pos(y') or negsuc(x') = pos(y') by {
            have h: negsuc(x') < pos(y') by expand operator<.
            h
          }
        }
        case negsuc(y') {
          assume xy
          have A: y' ≤ x' by expand operator≤ in xy
          have B: y' < x' or y' = x' by expand operator≤ in A
          cases B
          case y_l_x: y' < x' {
            conclude negsuc(x') < negsuc(y') or negsuc(x') = negsuc(y') by {
              have h: negsuc(x') < negsuc(y') by expand operator< y_l_x
              h
            }
          }
          case y_eq_x: y' = x' {
            conclude negsuc(x') < negsuc(y') or negsuc(x') = negsuc(y') by {
              have h: negsuc(x') = negsuc(y') by replace y_eq_x.
              h
            }
          }
        }
      }
    }
  }
end

theorem int_less_or_equal_implies_less_equal: all x:Int, y:Int.
  if x < y or x = y then x ≤ y
proof
  arbitrary x:Int, y:Int
  assume disj
  cases disj
  case x_l_y: x < y {
    apply int_less_implies_less_equal to x_l_y
  }
  case x_eq_y: x = y {
    replace x_eq_y
    int_less_equal_refl[y]
  }
end

theorem int_less_equal_iff_less_or_equal: all x:Int, y:Int.
  x ≤ y ⇔ (x < y or x = y)
proof
  arbitrary x:Int, y:Int
  int_less_equal_implies_less_or_equal[x, y],
  int_less_or_equal_implies_less_equal[x, y]
end

theorem int_trichotomy: all x:Int, y:Int.
  x < y or x = y or y < x
proof
  arbitrary x:Int, y:Int
  switch x {
    case pos(x') {
      switch y {
        case pos(y') {
          have tri: x' < y' or x' = y' or y' < x' by uint_trichotomy[x', y']
          cases tri
          case x_l_y: x' < y' {
            have h: pos(x') < pos(y') by expand operator< x_l_y
            h
          }
          case x_eq_y: x' = y' {
            have h: pos(x') = pos(y') by replace x_eq_y.
            h
          }
          case y_l_x: y' < x' {
            have h: pos(y') < pos(x') by expand operator< y_l_x
            h
          }
        }
        case negsuc(y') {
          have h: negsuc(y') < pos(x') by expand operator<.
          h
        }
      }
    }
    case negsuc(x') {
      switch y {
        case pos(y') {
          have h: negsuc(x') < pos(y') by expand operator<.
          h
        }
        case negsuc(y') {
          have tri: x' < y' or x' = y' or y' < x' by uint_trichotomy[x', y']
          cases tri
          case x_l_y: x' < y' {
            have h: negsuc(y') < negsuc(x') by expand operator< x_l_y
            h
          }
          case x_eq_y: x' = y' {
            have h: negsuc(x') = negsuc(y') by replace x_eq_y.
            h
          }
          case y_l_x: y' < x' {
            have h: negsuc(x') < negsuc(y') by expand operator< y_l_x
            h
          }
        }
      }
    }
  }
end

theorem int_dichotomy: all x:Int, y:Int. x ≤ y or y < x
proof
  arbitrary x:Int, y:Int
  have tri: x < y or x = y or y < x by int_trichotomy[x, y]
  cases tri
  case x_l_y: x < y {
    have x_le_y: x ≤ y by apply int_less_implies_less_equal to x_l_y
    x_le_y
  }
  case x_eq_y: x = y {
    have x_le_y: x ≤ y by {
      replace x_eq_y
      int_less_equal_refl[y]
    }
    x_le_y
  }
  case y_l_x: y < x { y_l_x }
end

theorem int_less_implies_not_greater: all x:Int, y:Int.
  if x < y then not (y < x)
proof
  arbitrary x:Int, y:Int
  assume x_l_y
  assume y_l_x
  have x_l_x: x < x by apply int_less_trans[x, y, x] to x_l_y, y_l_x
  apply int_less_irreflexive[x] to x_l_x
end

theorem int_not_less_implies_less_equal: all x:Int, y:Int.
  if not (x < y) then y ≤ x
proof
  arbitrary x:Int, y:Int
  assume not_x_l_y
  have tri: x < y or x = y or y < x by int_trichotomy[x, y]
  cases tri
  case x_l_y: x < y {
    conclude false by apply not_x_l_y to x_l_y
  }
  case x_eq_y: x = y {
    replace symmetric x_eq_y
    int_less_equal_refl[x]
  }
  case y_l_x: y < x {
    apply int_less_implies_less_equal to y_l_x
  }
end

theorem int_not_less_equal_iff_greater: all x:Int, y:Int.
  not (x ≤ y) ⇔ y < x
proof
  arbitrary x:Int, y:Int
  have fwd: if not (x ≤ y) then y < x by {
    assume not_xy
    have tri: x < y or x = y or y < x by int_trichotomy[x, y]
    cases tri
    case x_l_y: x < y {
      have x_le_y: x ≤ y by apply int_less_implies_less_equal to x_l_y
      conclude false by apply not_xy to x_le_y
    }
    case x_eq_y: x = y {
      have x_le_y: x ≤ y by {
        replace x_eq_y
        int_less_equal_refl[y]
      }
      conclude false by apply not_xy to x_le_y
    }
    case y_l_x: y < x { y_l_x }
  }
  have bkwd: if y < x then not (x ≤ y) by {
    assume y_l_x
    assume x_le_y
    have x_l_y_or_eq: x < y or x = y
      by apply int_less_equal_iff_less_or_equal[x, y] to x_le_y
    cases x_l_y_or_eq
    case x_l_y: x < y {
      have x_l_x: x < x by apply int_less_trans[x, y, x] to x_l_y, y_l_x
      apply int_less_irreflexive[x] to x_l_x
    }
    case x_eq_y: x = y {
      have y_l_y: y < y by replace x_eq_y in y_l_x
      apply int_less_irreflexive[y] to y_l_y
    }
  }
  fwd, bkwd
end

theorem int_greater_implies_not_equal: all x:Int, y:Int.
  if x > y then not (x = y)
proof
  arbitrary x:Int, y:Int
  assume x_g_y: x > y
  have y_l_x: y < x by expand operator> in x_g_y
  assume xy_eq: x = y
  have y_l_y: y < y by replace xy_eq in y_l_x
  apply int_less_irreflexive[y] to y_l_y
end

theorem int_less_equal_iff_not_greater: all x:Int, y:Int.
  x ≤ y ⇔ not (y < x)
proof
  arbitrary x:Int, y:Int
  have fwd: if x ≤ y then not (y < x) by {
    assume x_le_y
    assume y_l_x
    have x_l_y_or_eq: x < y or x = y
      by apply int_less_equal_iff_less_or_equal[x, y] to x_le_y
    cases x_l_y_or_eq
    case x_l_y: x < y {
      have x_l_x: x < x by apply int_less_trans[x, y, x] to x_l_y, y_l_x
      apply int_less_irreflexive[x] to x_l_x
    }
    case x_eq_y: x = y {
      have y_l_y: y < y by replace x_eq_y in y_l_x
      apply int_less_irreflexive[y] to y_l_y
    }
  }
  have bkwd: if not (y < x) then x ≤ y by {
    assume not_y_l_x
    have A: y ≤ x or x < y by {
      have tri: x < y or x = y or y < x by int_trichotomy[x, y]
      cases tri
      case x_l_y: x < y { x_l_y }
      case x_eq_y: x = y {
        have y_le_x: y ≤ x by {
          replace symmetric x_eq_y
          int_less_equal_refl[x]
        }
        y_le_x
      }
      case y_l_x: y < x {
        conclude false by apply not_y_l_x to y_l_x
      }
    }
    cases A
    case y_le_x: y ≤ x {
      have x_l_y_or_eq: y < x or y = x
        by apply int_less_equal_iff_less_or_equal[y, x] to y_le_x
      cases x_l_y_or_eq
      case y_l_x: y < x {
        conclude false by apply not_y_l_x to y_l_x
      }
      case y_eq_x: y = x {
        replace y_eq_x
        int_less_equal_refl[x]
      }
    }
    case x_l_y: x < y {
      apply int_less_implies_less_equal to x_l_y
    }
  }
  fwd, bkwd
end

theorem int_less_trans_less_equal_right: all x:Int, y:Int, z:Int.
  if x < y and y ≤ z then x < z
proof
  arbitrary x:Int, y:Int, z:Int
  assume prem
  have x_l_y: x < y by prem
  have y_le_z: y ≤ z by prem
  have y_l_z_or_eq: y < z or y = z
    by apply int_less_equal_iff_less_or_equal[y, z] to y_le_z
  cases y_l_z_or_eq
  case y_l_z: y < z {
    apply int_less_trans[x, y, z] to x_l_y, y_l_z
  }
  case y_eq_z: y = z {
    replace symmetric y_eq_z
    x_l_y
  }
end

theorem int_less_trans_less_equal_left: all x:Int, y:Int, z:Int.
  if x ≤ y and y < z then x < z
proof
  arbitrary x:Int, y:Int, z:Int
  assume prem
  have x_le_y: x ≤ y by prem
  have y_l_z: y < z by prem
  have x_l_y_or_eq: x < y or x = y
    by apply int_less_equal_iff_less_or_equal[x, y] to x_le_y
  cases x_l_y_or_eq
  case x_l_y: x < y {
    apply int_less_trans[x, y, z] to x_l_y, y_l_z
  }
  case x_eq_y: x = y {
    replace x_eq_y
    y_l_z
  }
end

// Properties of maximum and minimum.

theorem int_max_symmetric: all x:Int, y:Int. max(x, y) = max(y, x)
proof
  arbitrary x:Int, y:Int
  expand max
  have tri: x < y or x = y or y < x by int_trichotomy[x, y]
  cases tri
  case x_l_y: x < y {
    have not_y_l_x: not (y < x) by apply int_less_implies_not_greater to x_l_y
    simplify with x_l_y | not_y_l_x.
  }
  case x_eq_y: x = y {
    replace x_eq_y.
  }
  case y_l_x: y < x {
    have not_x_l_y: not (x < y) by apply int_less_implies_not_greater to y_l_x
    simplify with y_l_x | not_x_l_y.
  }
end

theorem int_max_equal_greater_right: all x:Int, y:Int.
  if x ≤ y then max(x, y) = y
proof
  arbitrary x:Int, y:Int
  assume prem
  expand max
  have x_l_y_or_eq: x < y or x = y
    by apply int_less_equal_iff_less_or_equal[x, y] to prem
  cases x_l_y_or_eq
  case x_l_y: x < y {
    simplify with x_l_y.
  }
  case x_eq_y: x = y {
    have not_x_l_y: not (x < y) by {
      replace x_eq_y
      int_less_irreflexive[y]
    }
    simplify with not_x_l_y
    x_eq_y
  }
end

theorem int_max_equal_greater_left: all x:Int, y:Int.
  if y ≤ x then max(x, y) = x
proof
  arbitrary x:Int, y:Int
  assume prem
  expand max
  have y_l_x_or_eq: y < x or y = x
    by apply int_less_equal_iff_less_or_equal[y, x] to prem
  cases y_l_x_or_eq
  case y_l_x: y < x {
    have not_x_l_y: not (x < y) by apply int_less_implies_not_greater to y_l_x
    simplify with not_x_l_y.
  }
  case y_eq_x: y = x {
    have not_x_l_y: not (x < y) by {
      replace y_eq_x
      int_less_irreflexive[x]
    }
    simplify with not_x_l_y.
  }
end

theorem int_max_less_equal: all x:Int, y:Int, z:Int.
  if x ≤ z and y ≤ z then max(x, y) ≤ z
proof
  arbitrary x:Int, y:Int, z:Int
  assume prem
  expand max
  have xy: x < y or not (x < y) by ex_mid[x < y]
  cases xy
  case x_l_y: x < y {
    simplify with x_l_y
    show y ≤ z
    prem
  }
  case not_x_l_y: not (x < y) {
    simplify with not_x_l_y
    show x ≤ z
    prem
  }
end

theorem int_max_greater_left: all x:Int, y:Int.
  x ≤ max(x, y)
proof
  arbitrary x:Int, y:Int
  expand max
  have xy: x < y or not (x < y) by ex_mid[x < y]
  cases xy
  case x_l_y: x < y {
    simplify with x_l_y
    apply int_less_implies_less_equal to x_l_y
  }
  case not_x_l_y: not (x < y) {
    simplify with not_x_l_y
    int_less_equal_refl[x]
  }
end

theorem int_max_greater_right: all x:Int, y:Int.
  y ≤ max(x, y)
proof
  arbitrary x:Int, y:Int
  expand max
  have xy: x < y or not (x < y) by ex_mid[x < y]
  cases xy
  case x_l_y: x < y {
    simplify with x_l_y
    int_less_equal_refl[y]
  }
  case not_x_l_y: not (x < y) {
    simplify with not_x_l_y
    apply int_not_less_implies_less_equal to not_x_l_y
  }
end

theorem int_max_is_left_or_right: all x:Int, y:Int.
  max(x, y) = x or max(x, y) = y
proof
  arbitrary x:Int, y:Int
  expand max
  have xy: x < y or not (x < y) by ex_mid[x < y]
  cases xy
  case x_l_y: x < y {
    simplify with x_l_y.
  }
  case not_x_l_y: not (x < y) {
    simplify with not_x_l_y.
  }
end

theorem int_max_idempotent: all x:Int.
  max(x, x) = x
proof
  arbitrary x:Int
  expand max
  simplify with int_less_irreflexive[x].
end

theorem int_max_assoc: all x:Int, y:Int, z:Int.
  max(max(x, y), z) = max(x, max(y, z))
proof
  arbitrary x:Int, y:Int, z:Int
  have xy: x < y or not (x < y) by ex_mid[x < y]
  have yz: y < z or not (y < z) by ex_mid[y < z]
  cases xy
  case x_l_y: x < y {
    cases yz
    case y_l_z: y < z {
      have x_l_z: x < z by apply int_less_trans to x_l_y, y_l_z
      expand max
      simplify with x_l_y
      simplify with y_l_z
      simplify with x_l_z.
    }
    case not_y_l_z: not (y < z) {
      expand max
      simplify with x_l_y
      simplify with not_y_l_z
      simplify with x_l_y.
    }
  }
  case not_x_l_y: not (x < y) {
    cases yz
    case y_l_z: y < z {
      expand max
      simplify with not_x_l_y
      simplify with y_l_z.
    }
    case not_y_l_z: not (y < z) {
      have y_le_x: y ≤ x by apply int_not_less_implies_less_equal to not_x_l_y
      have z_le_y: z ≤ y by apply int_not_less_implies_less_equal to not_y_l_z
      have z_le_x: z ≤ x by apply int_less_equal_trans to z_le_y, y_le_x
      have not_x_l_z: not (x < z) by {
        assume x_l_z
        have z_l_x_or_eq: z < x or z = x
          by apply int_less_equal_iff_less_or_equal[z, x] to z_le_x
        cases z_l_x_or_eq
        case z_l_x: z < x {
          have x_l_x: x < x by apply int_less_trans to x_l_z, z_l_x
          apply int_less_irreflexive to x_l_x
        }
        case z_eq_x: z = x {
          have x_l_x: x < x by replace z_eq_x in x_l_z
          apply int_less_irreflexive to x_l_x
        }
      }
      expand max
      simplify with not_x_l_y
      simplify with not_y_l_z
      simplify with not_x_l_z
      simplify with not_x_l_y.
    }
  }
end

theorem int_min_less_equal_left: all x:Int, y:Int.
  min(x, y) ≤ x
proof
  arbitrary x:Int, y:Int
  expand min
  have xy: x < y or not (x < y) by ex_mid[x < y]
  cases xy
  case x_l_y: x < y {
    simplify with x_l_y
    int_less_equal_refl[x]
  }
  case not_x_l_y: not (x < y) {
    simplify with not_x_l_y
    apply int_not_less_implies_less_equal to not_x_l_y
  }
end

theorem int_min_less_equal_right: all x:Int, y:Int.
  min(x, y) ≤ y
proof
  arbitrary x:Int, y:Int
  expand min
  have xy: x < y or not (x < y) by ex_mid[x < y]
  cases xy
  case x_l_y: x < y {
    simplify with x_l_y
    apply int_less_implies_less_equal to x_l_y
  }
  case not_x_l_y: not (x < y) {
    simplify with not_x_l_y
    int_less_equal_refl[y]
  }
end

theorem int_min_equal_less_left: all x:Int, y:Int.
  if x ≤ y then min(x, y) = x
proof
  arbitrary x:Int, y:Int
  assume prem
  expand min
  have x_l_y_or_eq: x < y or x = y
    by apply int_less_equal_iff_less_or_equal[x, y] to prem
  cases x_l_y_or_eq
  case x_l_y: x < y {
    simplify with x_l_y.
  }
  case x_eq_y: x = y {
    have not_x_l_y: not (x < y) by {
      replace x_eq_y
      int_less_irreflexive[y]
    }
    simplify with not_x_l_y
    symmetric x_eq_y
  }
end

theorem int_min_equal_less_right: all x:Int, y:Int.
  if y ≤ x then min(x, y) = y
proof
  arbitrary x:Int, y:Int
  assume prem
  expand min
  have not_x_l_y: not (x < y) by {
    assume x_l_y
    have y_l_x_or_eq: y < x or y = x
      by apply int_less_equal_iff_less_or_equal[y, x] to prem
    cases y_l_x_or_eq
    case y_l_x: y < x {
      have x_l_x: x < x by apply int_less_trans[x, y, x] to x_l_y, y_l_x
      apply int_less_irreflexive[x] to x_l_x
    }
    case y_eq_x: y = x {
      have x_l_x: x < x by replace y_eq_x in x_l_y
      apply int_less_irreflexive[x] to x_l_x
    }
  }
  simplify with not_x_l_y.
end

theorem int_min_is_left_or_right: all x:Int, y:Int.
  min(x, y) = x or min(x, y) = y
proof
  arbitrary x:Int, y:Int
  expand min
  have xy: x < y or not (x < y) by ex_mid[x < y]
  cases xy
  case x_l_y: x < y {
    simplify with x_l_y.
  }
  case not_x_l_y: not (x < y) {
    simplify with not_x_l_y.
  }
end

theorem int_min_idempotent: all x:Int.
  min(x, x) = x
proof
  arbitrary x:Int
  expand min
  simplify with int_less_irreflexive[x].
end

theorem int_min_assoc: all x:Int, y:Int, z:Int.
  min(min(x, y), z) = min(x, min(y, z))
proof
  arbitrary x:Int, y:Int, z:Int
  have xy: x < y or not (x < y) by ex_mid[x < y]
  have yz: y < z or not (y < z) by ex_mid[y < z]
  cases xy
  case x_l_y: x < y {
    cases yz
    case y_l_z: y < z {
      have x_l_z: x < z by apply int_less_trans to x_l_y, y_l_z
      expand min
      simplify with x_l_y
      simplify with y_l_z
      simplify with x_l_z
      simplify with x_l_y.
    }
    case not_y_l_z: not (y < z) {
      expand min
      simplify with x_l_y
      simplify with not_y_l_z.
    }
  }
  case not_x_l_y: not (x < y) {
    cases yz
    case y_l_z: y < z {
      expand min
      simplify with not_x_l_y
      simplify with y_l_z
      simplify with not_x_l_y.
    }
    case not_y_l_z: not (y < z) {
      have y_le_x: y ≤ x by apply int_not_less_implies_less_equal to not_x_l_y
      have z_le_y: z ≤ y by apply int_not_less_implies_less_equal to not_y_l_z
      have z_le_x: z ≤ x by apply int_less_equal_trans to z_le_y, y_le_x
      have not_x_l_z: not (x < z) by {
        assume x_l_z
        have z_l_x_or_eq: z < x or z = x
          by apply int_less_equal_iff_less_or_equal[z, x] to z_le_x
        cases z_l_x_or_eq
        case z_l_x: z < x {
          have x_l_x: x < x by apply int_less_trans to x_l_z, z_l_x
          apply int_less_irreflexive to x_l_x
        }
        case z_eq_x: z = x {
          have x_l_x: x < x by replace z_eq_x in x_l_z
          apply int_less_irreflexive to x_l_x
        }
      }
      expand min
      simplify with not_x_l_y
      simplify with not_y_l_z
      simplify with not_x_l_z.
    }
  }
end

theorem int_min_symmetric: all x:Int, y:Int.
  min(x, y) = min(y, x)
proof
  arbitrary x:Int, y:Int
  expand min
  have tri: x < y or x = y or y < x by int_trichotomy[x, y]
  cases tri
  case x_l_y: x < y {
    have not_y_l_x: not (y < x) by apply int_less_implies_not_greater to x_l_y
    simplify with x_l_y | not_y_l_x.
  }
  case x_eq_y: x = y {
    replace x_eq_y.
  }
  case y_l_x: y < x {
    have not_x_l_y: not (x < y) by apply int_less_implies_not_greater to y_l_x
    simplify with y_l_x | not_x_l_y.
  }
end

theorem int_min_greatest_less_equal: all x:Int, y:Int, z:Int.
  if z ≤ x and z ≤ y then z ≤ min(x, y)
proof
  arbitrary x:Int, y:Int, z:Int
  assume prem
  expand min
  have xy: x < y or not (x < y) by ex_mid[x < y]
  cases xy
  case x_l_y: x < y {
    simplify with x_l_y
    show z ≤ x
    prem
  }
  case not_x_l_y: not (x < y) {
    simplify with not_x_l_y
    show z ≤ y
    prem
  }
end

theorem int_min_max_absorb_left: all x:Int, y:Int.
  min(x, max(x, y)) = x
proof
  arbitrary x:Int, y:Int
  apply int_min_equal_less_left[x, max(x, y)] to int_max_greater_left[x, y]
end

theorem int_max_min_absorb_left: all x:Int, y:Int.
  max(x, min(x, y)) = x
proof
  arbitrary x:Int, y:Int
  apply int_max_equal_greater_left[x, min(x, y)] to int_min_less_equal_left[x, y]
end

theorem int_min_max_absorb_right: all x:Int, y:Int.
  min(max(x, y), x) = x
proof
  arbitrary x:Int, y:Int
  replace int_min_symmetric[max(x, y), x]
  int_min_max_absorb_left[x, y]
end

theorem int_max_min_absorb_right: all x:Int, y:Int.
  max(min(x, y), x) = x
proof
  arbitrary x:Int, y:Int
  replace int_max_symmetric[min(x, y), x]
  int_max_min_absorb_left[x, y]
end

// Structural spec theorems for `≤` and `<` on Int.
//
// Each constructor-pair case reduces to the corresponding UInt comparison
// (or to a constant `true`/`false` for the cross-sign cases). These are
// the Int-side analogue of `uint_lit_less_equal` / `uint_lit_less` and
// the `≤`/`<` part of the conversion-and-specification story described
// in the `lib/UIntToFrom.pf` source comment.

theorem int_pos_le_pos: all au:UInt, bu:UInt.
  (pos(au) ≤ pos(bu)) = (au ≤ bu)
proof
  arbitrary au:UInt, bu:UInt
  expand operator≤ | operator≤.
end

auto int_pos_le_pos

theorem int_pos_le_negsuc: all au:UInt, bu:UInt.
  (pos(au) ≤ negsuc(bu)) = false
proof
  arbitrary au:UInt, bu:UInt
  expand operator≤.
end

auto int_pos_le_negsuc

theorem int_negsuc_le_pos: all au:UInt, bu:UInt.
  (negsuc(au) ≤ pos(bu)) = true
proof
  arbitrary au:UInt, bu:UInt
  expand operator≤.
end

auto int_negsuc_le_pos

theorem int_negsuc_le_negsuc: all au:UInt, bu:UInt.
  (negsuc(au) ≤ negsuc(bu)) = (bu ≤ au)
proof
  arbitrary au:UInt, bu:UInt
  expand operator≤ | operator≤.
end

auto int_negsuc_le_negsuc

theorem int_pos_less_pos: all au:UInt, bu:UInt.
  (pos(au) < pos(bu)) = (au < bu)
proof
  arbitrary au:UInt, bu:UInt
  expand operator<.
end

auto int_pos_less_pos

theorem int_pos_less_negsuc: all au:UInt, bu:UInt.
  (pos(au) < negsuc(bu)) = false
proof
  arbitrary au:UInt, bu:UInt
  expand operator<.
end

auto int_pos_less_negsuc

theorem int_negsuc_less_pos: all au:UInt, bu:UInt.
  (negsuc(au) < pos(bu)) = true
proof
  arbitrary au:UInt, bu:UInt
  expand operator<.
end

auto int_negsuc_less_pos

theorem int_negsuc_less_negsuc: all au:UInt, bu:UInt.
  (negsuc(au) < negsuc(bu)) = (bu < au)
proof
  arbitrary au:UInt, bu:UInt
  expand operator<.
end

auto int_negsuc_less_negsuc

// Addition monotonicity and cancellation for ≤ and <.
//
// The strategy is to characterize `a ≤ b` as `+0 ≤ b - a` (via `a ⊝ b`
// being non-negative iff `b ≤ a`), prove the algebraic identity
// `(x + z) - (x + y) = z - y`, and then read off both directions of
// `x + y ≤ x + z ⇔ y ≤ z`.

lemma pos_zero_le_monuso: all a:UInt, b:UInt.
  +0 ≤ (a ⊝ b) ⇔ b ≤ a
proof
  arbitrary a:UInt, b:UInt
  have fwd: if +0 ≤ (a ⊝ b) then b ≤ a by {
    assume prem
    cases ex_mid[b ≤ a]
    case bla: b ≤ a { bla }
    case not_bla: not (b ≤ a) {
      have alb: a < b
        by apply (conjunct 0 of uint_not_less_equal_iff_greater[b, a]) to not_bla
      have pos_ba: 0 < b ∸ a by {
        have ba_nz: not (b ∸ a = 0) by {
          assume ba_z
          have bla_again: b ≤ a
            by apply (conjunct 1 of uint_monus_zero_iff_less_eq[b, a]) to ba_z
          apply not_bla to bla_again
        }
        apply uint_not_zero_pos to ba_nz
      }
      obtain w where w_eq: b ∸ a = 1 + w
        from apply uint_positive_add_one to pos_ba
      have lhs_neg: (a ⊝ b) = negsuc(w) by {
        expand operator⊝
        simplify with alb
        replace w_eq
        neg_suc[w]
      }
      have absurd: +0 ≤ negsuc(w) by replace lhs_neg in prem
      absurd
    }
  }
  have bkwd: if b ≤ a then +0 ≤ (a ⊝ b) by {
    assume bla
    have not_alb: not (a < b) by {
      assume alb
      have not_bla: not (b ≤ a)
        by apply (conjunct 1 of uint_not_less_equal_iff_greater[b, a]) to alb
      apply not_bla to bla
    }
    have form: (a ⊝ b) = pos(a ∸ b) by {
      expand operator⊝
      simplify with not_alb.
    }
    replace form
    suffices 0 ≤ a ∸ b by .
    uint_zero_le[a ∸ b]
  }
  fwd, bkwd
end

lemma neg_pos_eq_zero_monuso: all au:UInt. -pos(au) = (0 ⊝ au)
proof
  arbitrary au:UInt
  cases uint_zero_or_positive[au]
  case auz: au = 0 {
    replace auz
    expand operator-
    expand operator⊝.
  }
  case au_pos: 0 < au {
    obtain au' where au_s: au = 1 + au'
      from apply uint_positive_add_one to au_pos
    replace au_s
    have form: -pos(1 + au') = negsuc(au') by neg_pos[au']
    have rhs: (0 ⊝ (1 + au')) = negsuc(au') by zero_monuso_neg[au']
    equations
          -pos(1 + au')
        = negsuc(au')       by form
    ... = (0 ⊝ (1 + au'))   by symmetric rhs
  }
end

theorem int_le_iff_diff_nonneg: all a:Int, b:Int.
  a ≤ b ⇔ +0 ≤ b - a
proof
  arbitrary a:Int, b:Int
  switch a {
    case pos(au) {
      switch b {
        case pos(bu) {
          have diff: pos(bu) - pos(au) = (bu ⊝ au) by symmetric subo_monus[bu, au]
          replace diff
          apply iff_symm to pos_zero_le_monuso[bu, au]
        }
        case negsuc(bu) {
          have diff_form: (negsuc(bu) - pos(au)) = (0 ⊝ (1 + bu + au)) by {
            equations
                  negsuc(bu) - pos(au)
                = negsuc(bu) + (-pos(au))      by expand operator-.
            ... = negsuc(bu) + (0 ⊝ au)        by replace neg_pos_eq_zero_monuso.
            ... = (0 ⊝ (1 + bu + au))          by distrib_right_monus_add_neg[bu, 0, au]
          }
          replace diff_form
          have rhs_iff: +0 ≤ (0 ⊝ (1 + bu + au)) ⇔ (1 + bu + au) ≤ 0
            by pos_zero_le_monuso[0, 1 + bu + au]
          have rhs_false: ((1 + bu + au) ≤ 0) = false by {
            apply eq_false to {
              assume bad: (1 + bu + au) ≤ 0
              apply uint_less_equal_zero to bad
            }
          }
          replace apply iff_equal to rhs_iff
          replace rhs_false.
        }
      }
    }
    case negsuc(au) {
      switch b {
        case pos(bu) {
          have diff_form: (pos(bu) - negsuc(au)) = pos(bu + 1 + au) by {
            equations
                  pos(bu) - negsuc(au)
                = pos(bu) + (-negsuc(au))     by expand operator-.
            ... = pos(bu) + pos(1 + au)       by expand operator-.
            ... = pos(bu + 1 + au)            by add_pos_pos
          }
          replace diff_form.
        }
        case negsuc(bu) {
          have diff_form: (negsuc(bu) - negsuc(au)) = (au ⊝ bu) by {
            equations
                  negsuc(bu) - negsuc(au)
                = negsuc(bu) + (-negsuc(au))   by expand operator-.
            ... = negsuc(bu) + pos(1 + au)     by expand operator-.
            ... = (1 + au) ⊝ (1 + bu)          by add_negsuc_pos[bu, 1 + au]
            ... = au ⊝ bu                       by suc_uint_monuso[au, bu]
          }
          replace diff_form
          apply iff_symm to pos_zero_le_monuso[au, bu]
        }
      }
    }
  }
end

// Cancelling a common left summand under subtraction.
lemma int_add_sub_cancel_left: all x:Int, y:Int, z:Int.
  (x + z) - (x + y) = z - y
proof
  arbitrary x:Int, y:Int, z:Int
  expand operator-
  show (x + z) + (-(x + y)) = z + (-y)
  equations
        (x + z) + (-(x + y))
      = (x + z) + ((-x) + (-y))  by replace neg_distr_add[x, y].
  ... = z + x + (-x) + (-y)      by replace int_add_commute[x, z].
  ... = z + (-y)                 by replace int_add_inverse[x].
end

theorem int_add_both_sides_of_less_equal: all x:Int, y:Int, z:Int.
  x + y ≤ x + z ⇔ y ≤ z
proof
  arbitrary x:Int, y:Int, z:Int
  have lhs_iff: x + y ≤ x + z ⇔ +0 ≤ (x + z) - (x + y)
    by int_le_iff_diff_nonneg[x + y, x + z]
  have cancel_eq: +0 ≤ (x + z) - (x + y) ⇔ +0 ≤ z - y by {
    have eq: (x + z) - (x + y) = z - y by int_add_sub_cancel_left[x, y, z]
    replace eq.
  }
  have rhs_iff: +0 ≤ z - y ⇔ y ≤ z
    by apply iff_symm to int_le_iff_diff_nonneg[y, z]
  apply iff_trans[x + y ≤ x + z, +0 ≤ (x + z) - (x + y), y ≤ z]
    to lhs_iff,
       apply iff_trans[+0 ≤ (x + z) - (x + y), +0 ≤ z - y, y ≤ z]
         to cancel_eq, rhs_iff
end

theorem int_add_le_left_mono: all x:Int, y:Int, z:Int.
  if y ≤ z then x + y ≤ x + z
proof
  arbitrary x:Int, y:Int, z:Int
  conjunct 1 of int_add_both_sides_of_less_equal[x, y, z]
end

theorem int_add_le_right_mono: all x:Int, y:Int, z:Int.
  if y ≤ z then y + x ≤ z + x
proof
  arbitrary x:Int, y:Int, z:Int
  assume yz
  have step: x + y ≤ x + z by apply int_add_le_left_mono[x, y, z] to yz
  replace int_add_commute[x, y] | int_add_commute[x, z] in step
end

theorem int_add_both_sides_of_less_equal_right: all x:Int, y:Int, z:Int.
  y + x ≤ z + x ⇔ y ≤ z
proof
  arbitrary x:Int, y:Int, z:Int
  have eq1: y + x = x + y by int_add_commute[y, x]
  have eq2: z + x = x + z by int_add_commute[z, x]
  replace eq1 | eq2
  int_add_both_sides_of_less_equal[x, y, z]
end

theorem int_add_mono_less_equal: all a:Int, b:Int, c:Int, d:Int.
  if a ≤ c and b ≤ d then a + b ≤ c + d
proof
  arbitrary a:Int, b:Int, c:Int, d:Int
  assume prem
  have ac: a ≤ c by prem
  have bd: b ≤ d by prem
  have step1: a + b ≤ a + d by apply int_add_le_left_mono[a, b, d] to bd
  have step2: a + d ≤ c + d by apply int_add_le_right_mono[d, a, c] to ac
  apply int_less_equal_trans[a + b, a + d, c + d] to step1, step2
end

theorem int_add_both_sides_of_less: all x:Int, y:Int, z:Int.
  x + y < x + z ⇔ y < z
proof
  arbitrary x:Int, y:Int, z:Int
  have fwd: if x + y < x + z then y < z by {
    assume prem
    have nle: not (x + z ≤ x + y)
      by apply (conjunct 1 of int_not_less_equal_iff_greater[x + z, x + y]) to prem
    have iff_yz: x + z ≤ x + y ⇔ z ≤ y
      by int_add_both_sides_of_less_equal[x, z, y]
    have not_zy: not (z ≤ y) by {
      assume zy
      have zy_le: x + z ≤ x + y by apply (conjunct 1 of iff_yz) to zy
      apply nle to zy_le
    }
    apply (conjunct 0 of int_not_less_equal_iff_greater[z, y]) to not_zy
  }
  have bkwd: if y < z then x + y < x + z by {
    assume prem
    have nle: not (z ≤ y)
      by apply (conjunct 1 of int_not_less_equal_iff_greater[z, y]) to prem
    have iff_yz: x + z ≤ x + y ⇔ z ≤ y
      by int_add_both_sides_of_less_equal[x, z, y]
    have not_xzxy: not (x + z ≤ x + y) by {
      assume xzxy
      have zy_le: z ≤ y by apply (conjunct 0 of iff_yz) to xzxy
      apply nle to zy_le
    }
    apply (conjunct 0 of int_not_less_equal_iff_greater[x + z, x + y]) to not_xzxy
  }
  fwd, bkwd
end

theorem int_add_both_sides_of_less_right: all x:Int, y:Int, z:Int.
  y + x < z + x ⇔ y < z
proof
  arbitrary x:Int, y:Int, z:Int
  have eq1: y + x = x + y by int_add_commute[y, x]
  have eq2: z + x = x + z by int_add_commute[z, x]
  replace eq1 | eq2
  int_add_both_sides_of_less[x, y, z]
end

theorem int_add_less_mono_left: all x:Int, y:Int, z:Int.
  if y < z then x + y < x + z
proof
  arbitrary x:Int, y:Int, z:Int
  conjunct 1 of int_add_both_sides_of_less[x, y, z]
end

theorem int_add_less_mono_right: all x:Int, y:Int, z:Int.
  if y < z then y + x < z + x
proof
  arbitrary x:Int, y:Int, z:Int
  conjunct 1 of int_add_both_sides_of_less_right[x, y, z]
end

theorem int_add_mono_less: all a:Int, b:Int, c:Int, d:Int.
  if a < c and b < d then a + b < c + d
proof
  arbitrary a:Int, b:Int, c:Int, d:Int
  assume prem
  have ac: a < c by prem
  have bd: b < d by prem
  have step1: a + b < a + d by apply int_add_less_mono_left[a, b, d] to bd
  have step2: a + d < c + d by apply int_add_less_mono_right[d, a, c] to ac
  apply int_less_trans[a + b, a + d, c + d] to step1, step2
end

theorem int_neg_le_mono: all x:Int, y:Int.
  if x ≤ y then -y ≤ -x
proof
  arbitrary x:Int, y:Int
  assume xy
  have step: x + ((-x) + (-y)) ≤ y + ((-x) + (-y))
    by apply int_add_le_right_mono[(-x) + (-y), x, y] to xy
  have lhs_eq: x + ((-x) + (-y)) = -y by {
    equations
          x + ((-x) + (-y))
        = (x + (-x)) + (-y)   by symmetric int_add_assoc[x, -x, -y]
    ... = +0 + (-y)           by replace int_add_inverse[x].
    ... = -y                  by int_zero_add[-y]
  }
  have rhs_eq: y + ((-x) + (-y)) = -x by {
    equations
          y + ((-x) + (-y))
        = y + ((-y) + (-x))   by replace int_add_commute[-x, -y].
    ... = (y + (-y)) + (-x)   by symmetric int_add_assoc[y, -y, -x]
    ... = +0 + (-x)           by replace int_add_inverse[y].
    ... = -x                  by int_zero_add[-x]
  }
  replace lhs_eq | rhs_eq in step
end

theorem int_neg_le_iff: all x:Int, y:Int.
  x ≤ y ⇔ -y ≤ -x
proof
  arbitrary x:Int, y:Int
  have fwd: if x ≤ y then -y ≤ -x by int_neg_le_mono[x, y]
  have bkwd: if -y ≤ -x then x ≤ y by {
    assume neg_le
    have step: -(-x) ≤ -(-y) by apply int_neg_le_mono[-y, -x] to neg_le
    replace neg_involutive[x] | neg_involutive[y] in step
  }
  fwd, bkwd
end

theorem int_neg_less_mono: all x:Int, y:Int.
  if x < y then -y < -x
proof
  arbitrary x:Int, y:Int
  assume xy
  have step: x + ((-x) + (-y)) < y + ((-x) + (-y))
    by apply int_add_less_mono_right[(-x) + (-y), x, y] to xy
  have lhs_eq: x + ((-x) + (-y)) = -y by {
    equations
          x + ((-x) + (-y))
        = (x + (-x)) + (-y)   by symmetric int_add_assoc[x, -x, -y]
    ... = +0 + (-y)           by replace int_add_inverse[x].
    ... = -y                  by int_zero_add[-y]
  }
  have rhs_eq: y + ((-x) + (-y)) = -x by {
    equations
          y + ((-x) + (-y))
        = y + ((-y) + (-x))   by replace int_add_commute[-x, -y].
    ... = (y + (-y)) + (-x)   by symmetric int_add_assoc[y, -y, -x]
    ... = +0 + (-x)           by replace int_add_inverse[y].
    ... = -x                  by int_zero_add[-x]
  }
  replace lhs_eq | rhs_eq in step
end

theorem int_neg_less_iff: all x:Int, y:Int.
  x < y ⇔ -y < -x
proof
  arbitrary x:Int, y:Int
  have fwd: if x < y then -y < -x by int_neg_less_mono[x, y]
  have bkwd: if -y < -x then x < y by {
    assume neg_less
    have step: -(-x) < -(-y) by apply int_neg_less_mono[-y, -x] to neg_less
    replace neg_involutive[x] | neg_involutive[y] in step
  }
  fwd, bkwd
end