# int.bend -- the integers, as a bounty: a canonical
# representation is FIXED here (so that == is real equality), the
# operations are open (laws with no def), and the laws and test cases
# are open claims about them. Fill the operations first, in a new file
# that imports this one with an alias; every test case is then {==}.
#
# Int.Pos{n} is n, Int.NegS{n} is -(1+n). Nothing else represents an
# integer, so there is exactly one term per integer.

import Base
import ./nat.bend as N

type Int is Data:
  Pos{n: Nat}
  NegS{n: Nat}

def Int.of(n: Nat) -> Int:
  Pos{n}

def Int.zero() -> Int:
  Pos{0n}

def Int.one() -> Int:
  Pos{1n}

# ---- operations (open) --------------------------------------------------

law Int.neg:
  for a: Int
  Int

law Int.add:
  for a: Int
  for b: Int
  Int

law Int.mul:
  for a: Int
  for b: Int
  Int

law Int.sub:
  for a: Int
  for b: Int
  Int

# the absolute value, as a Nat
law Int.abs:
  for a: Int
  Nat

# a <= b as a computed proposition (Unit or Empty), like N.Nat.Le
law Int.Le:
  for a: Int
  for b: Int
  Type

# ---- test cases (each is {==} once the operations compute) -------------

law t_add_1:
  {Int.add(Pos{3n}, NegS{4n}) == NegS{1n} : Int}

law t_add_2:
  {Int.add(NegS{0n}, Pos{1n}) == Pos{0n} : Int}

law t_mul_1:
  {Int.mul(NegS{1n}, NegS{2n}) == Pos{6n} : Int}

law t_mul_2:
  {Int.mul(Pos{3n}, NegS{0n}) == NegS{2n} : Int}

law t_sub_1:
  {Int.sub(Pos{0n}, Pos{5n}) == NegS{4n} : Int}

law t_abs_1:
  {Int.abs(NegS{6n}) == 7n : Nat}

# ---- laws (open) --------------------------------------------------------

# 1. Int.of embeds Nat: addition and multiplication agree with Nat's
law of_add:
  for +a: Nat
  for +b: Nat
  {Int.add(Pos{a}, Pos{b}) == Pos{Nat.add(a, b)} : Int}

law of_mul:
  for +a: Nat
  for +b: Nat
  {Int.mul(Pos{a}, Pos{b}) == Pos{Nat.mul(a, b)} : Int}

# 2. sub is add of the negation
law sub_def:
  for +a: Int
  for +b: Int
  {Int.sub(a, b) == Int.add(a, Int.neg(b)) : Int}

# 3. a + (-a) = 0, and -(-a) = a
law add_neg:
  for +a: Int
  {Int.add(a, Int.neg(a)) == Pos{0n} : Int}

law neg_neg:
  for a: Int
  {Int.neg(Int.neg(a)) == a : Int}

# 4. (Int, add, 0) is a commutative group; (Int, mul, 1) a commutative
#    monoid; mul distributes over add
law add_zero:
  for a: Int
  {Int.add(a, Pos{0n}) == a : Int}

law add_comm:
  for +a: Int
  for +b: Int
  {Int.add(a, b) == Int.add(b, a) : Int}

law add_assoc:
  for +a: Int
  for +b: Int
  for +c: Int
  {Int.add(a, Int.add(b, c)) == Int.add(Int.add(a, b), c) : Int}

law mul_one:
  for a: Int
  {Int.mul(a, Pos{1n}) == a : Int}

law mul_zero:
  for a: Int
  {Int.mul(a, Pos{0n}) == Pos{0n} : Int}

law mul_comm:
  for +a: Int
  for +b: Int
  {Int.mul(a, b) == Int.mul(b, a) : Int}

law mul_assoc:
  for +a: Int
  for +b: Int
  for +c: Int
  {Int.mul(a, Int.mul(b, c)) == Int.mul(Int.mul(a, b), c) : Int}

law mul_add:
  for +a: Int
  for +b: Int
  for +c: Int
  {Int.mul(a, Int.add(b, c)) == Int.add(Int.mul(a, b), Int.mul(a, c)) : Int}

# 5. no zero divisors (what the rationals will need)
law mul_eq_zero:
  for +a: Int
  for +b: Int
  for e: {Int.mul(a, b) == Pos{0n} : Int}
  for na: {a == Pos{0n} : Int} -> Empty
  {b == Pos{0n} : Int}

# 6. the order: total, antisymmetric, compatible with add and with mul by
#    a non-negative
law le_refl:
  for a: Int
  Int.Le(a, a)

law le_antisym:
  for +a: Int
  for +b: Int
  for h1: Int.Le(a, b)
  for h2: Int.Le(b, a)
  {a == b : Int}

law le_trans:
  for +a: Int
  for +b: Int
  for +c: Int
  for h1: Int.Le(a, b)
  for h2: Int.Le(b, c)
  Int.Le(a, c)

law le_add:
  for +a: Int
  for +b: Int
  for +c: Int
  for h: Int.Le(a, b)
  Int.Le(Int.add(a, c), Int.add(b, c))

law le_mul_nonneg:
  for +a: Int
  for +b: Int
  for +n: Nat
  for h: Int.Le(a, b)
  Int.Le(Int.mul(a, Pos{n}), Int.mul(b, Pos{n}))

# 7. neg reverses the order, and Pos{n} is never negative
law le_neg:
  for +a: Int
  for +b: Int
  for h: Int.Le(a, b)
  Int.Le(Int.neg(b), Int.neg(a))

law pos_nonneg:
  for n: Nat
  Int.Le(Pos{0n}, Pos{n})