module Int

import Nat
import UInt
import Base

/*
  Signed integers represented as nonnegative values `pos(n)` and
  negative successors `negsuc(n)`, where `negsuc(0)` is -1.

  This module gathers the definitions, addition/subtraction,
  multiplication, literals, and order facts for Int.
*/

public import IntDefs
public import IntAddSub
public import IntMult
public import IntDiv
public import IntLess
public import IntEvenOdd
public import IntAbs

// The following exports are needed for integer literals: the
// `lit`/`zero`/`suc` triple supplies the underlying numeric
// constructors and `fromNat` lifts a literal Nat into a UInt magnitude.

export lit
export zero
export suc
export fromNat

/*
  Auto-rules for Int literal addition.

  These let `auto` simplify sums whose operands are integer literals
  (i.e. `pos(fromNat(lit(...)))` or `negsuc(fromNat(lit(...)))`) into
  the corresponding combined-literal form. They cover the mixed
  pos/negsuc shapes the user sees in source.
*/

// Sum of two literal nonnegative integers reduces to the literal of their UInt sum.
theorem lit_add_pos_pos: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+.
end

auto lit_add_pos_pos

// Mixed-form sum: `pos(literal) + literal` collapses like `pos(literal) + pos(literal)`.
theorem lit_add_pos_lit: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) + fromNat(lit(y)) = pos(fromNat(lit(x) + lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+.
end

auto lit_add_pos_lit

// Mixed-form sum: `literal + pos(literal)` collapses to the literal of the sum.
theorem lit_add_lit_pos: all x:Nat, y:Nat.
  fromNat(lit(x)) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+.
end

auto lit_add_lit_pos

// Cancellation step when adding a positive literal and a negative literal,
// both with a successor magnitude: peel one unit off each side.
theorem lit_add_pos_negsuc_suc: all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + negsuc(fromNat(lit(suc(x)))) = pos(fromNat(lit(y))) + negsuc(fromNat(lit(x)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+
  suc_uint_monuso[fromNat(lit(y)), fromNat(lit(suc(x)))]
end

auto lit_add_pos_negsuc_suc

// Symmetric cancellation: same as `lit_add_pos_negsuc_suc` with operands swapped.
theorem lit_add_negsuc_pos_suc: all x:Nat, y:Nat. negsuc(fromNat(lit(suc(x)))) + pos(fromNat(lit(suc(y)))) = negsuc(fromNat(lit(x))) + pos(fromNat(lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+
  suc_uint_monuso[fromNat(lit(y)), fromNat(lit(suc(x)))]
end

auto lit_add_negsuc_pos_suc

// Base case of the cancellation: `pos(suc(y)) + negsuc(zero) = pos(y)`
// (adding -1 to a positive successor literal decrements).
theorem lit_add_pos_suc_negsuc_zero: all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + negsuc(fromNat(lit(zero))) = pos(fromNat(lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+
  transitive suc_uint_monuso[fromNat(lit(y)), 0] int_monuso_zero[fromNat(lit(y))]
end

auto lit_add_pos_suc_negsuc_zero

// Symmetric base case: `negsuc(zero) + pos(suc(y)) = pos(y)`.
theorem lit_add_negsuc_zero_pos_suc: all x:Nat, y:Nat. negsuc(fromNat(lit(zero))) + pos(fromNat(lit(suc(y)))) = pos(fromNat(lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+
  transitive suc_uint_monuso[fromNat(lit(y)), 0] int_monuso_zero[fromNat(lit(y))]
end

auto lit_add_negsuc_zero_pos_suc

/*
  Auto-rules for Int literal negation.

  Push unary minus through literal integer constructors so that, for
  example, `- pos(suc(x))` rewrites to `negsuc(x)` and `- negsuc(x)`
  rewrites to `pos(suc(x))`.
*/

// `-(+0) = +0`.
theorem neg_lit_zero: - pos(fromNat(lit(zero))) = pos(fromNat(lit(zero)))
proof
  expand operator-.
end

auto neg_lit_zero

// `-0 = +0` for the bare UInt-literal form.
theorem neg_uint_zero: - fromNat(lit(zero)) = pos(fromNat(lit(zero)))
proof
  expand operator-.
end

auto neg_uint_zero

// `-(pos(suc(x))) = negsuc(x)`: negating a positive successor gives the negative successor.
theorem neg_pos_lit_suc: all x:Nat.
  - pos(fromNat(lit(suc(x)))) = negsuc(fromNat(lit(x)))
proof
  arbitrary x:Nat
  expand operator-.
end

auto neg_pos_lit_suc

// Bare-literal form: `-suc(x) = negsuc(x)`.
theorem neg_lit_suc: all x:Nat.
  - fromNat(lit(suc(x))) = negsuc(fromNat(lit(x)))
proof
  arbitrary x:Nat
  expand operator-.
end

auto neg_lit_suc

// `-(negsuc(x)) = pos(suc(x))`: negation of a negative successor is the corresponding positive.
theorem neg_negsuc_lit: all x:Nat.
  - negsuc(fromNat(lit(x))) = pos(fromNat(lit(suc(x))))
proof
  arbitrary x:Nat
  expand operator-.
end

auto neg_negsuc_lit

/*
  Auto-rules for absolute value and sign on Int literals.
*/

// `abs(pos(literal))` is the literal itself.
theorem abs_lit: all x:Nat. abs(pos(fromNat(lit(x)))) = fromNat(lit(x))
proof
  arbitrary x:Nat
  evaluate
end

auto abs_lit

// Sign of a nonnegative literal is `positive`.
theorem sign_pos_lit: all x:Nat. sign(pos(fromNat(lit(x)))) = positive
proof
  arbitrary x:Nat
  evaluate
end

auto sign_pos_lit

// Sign of a negative-successor literal is `negative`.
theorem sign_neg_lit: all x:Nat. sign(negsuc(fromNat(lit(x)))) = negative
proof
  arbitrary x:Nat
  evaluate
end

auto sign_neg_lit

/*
  Auto-rules for Int literal multiplication.

  Cover the four sign combinations of literal operands, plus the
  mixed-form variants where one side is bare `fromNat(lit(...))`.
*/

// `pos(literal) * pos(literal)` reduces to the literal of the product.
theorem mult_pos_lit_pos_lit: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y)))
proof
  arbitrary x:Nat, y:Nat
  replace mult_pos_pos.
end

auto mult_pos_lit_pos_lit

// Mixed form: `literal * pos(literal)`.
theorem mult_lit_pos_lit: all x:Nat, y:Nat.
  fromNat(lit(x)) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator*.
end

auto mult_lit_pos_lit

// Mixed form: `pos(literal) * literal`.
theorem mult_pos_lit_lit: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) * fromNat(lit(y)) = pos(fromNat(lit(x) * lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator*.
end

auto mult_pos_lit_lit

// `pos(x) * negsuc(y) = -(x + x*y)`: the product is negative with magnitude x*(1+y).
theorem mult_pos_lit_neg_lit: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) * negsuc(fromNat(lit(y)))
  = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y)))
proof
  arbitrary x:Nat, y:Nat
  replace mult_pos_negsuc.
end

auto mult_pos_lit_neg_lit

// Mixed form of `mult_pos_lit_neg_lit`: bare literal on the left.
theorem mult_lit_neg_lit: all x:Nat, y:Nat.
  fromNat(lit(x)) * negsuc(fromNat(lit(y)))
  = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator*.
end

auto mult_lit_neg_lit

// `negsuc(x) * pos(y) = -(y + y*x)`: commute then reuse `mult_pos_negsuc`.
theorem mult_neg_lit_pos: all x:Nat, y:Nat.
  negsuc(fromNat(lit(x))) * pos(fromNat(lit(y)))
  = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x)))
proof
  arbitrary x:Nat, y:Nat
  replace int_mult_commute[negsuc(fromNat(lit(x))), pos(fromNat(lit(y)))].
end

auto mult_neg_lit_pos

// Mixed form of `mult_neg_lit_pos`: bare literal on the right.
theorem mult_neg_lit_lit: all x:Nat, y:Nat.
  negsuc(fromNat(lit(x))) * fromNat(lit(y))
  = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x)))
proof
  arbitrary x:Nat, y:Nat
  expand operator*.
end

auto mult_neg_lit_lit