int.bend source
int.bend on the hub · documented module
# 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 Baseimport ./nat.bend as Ntype 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 Intlaw Int.add: for a: Int for b: Int Intlaw Int.mul: for a: Int for b: Int Intlaw Int.sub: for a: Int for b: Int Int# the absolute value, as a Natlaw Int.abs: for a: Int Nat# a <= b as a computed proposition (Unit or Empty), like N.Nat.Lelaw 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'slaw 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 negationlaw 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) = alaw 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 addlaw 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-negativelaw 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 negativelaw 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})