int.bend open laws/TODOs

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/int.bend as Int

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.

2 imports

import Base
import ./nat.bend as N

Laws

law Int.neg provedin fermat4.bendsource · line 28 · raw

@a:Int -> Int

law Int.add provedin fermat4.bendsource · line 32 · raw

@a:Int -> @b:Int -> Int

law Int.mul provedin fermat4.bendsource · line 37 · raw

@a:Int -> @b:Int -> Int

law Int.sub provedin fermat4.bendsource · line 42 · raw

@a:Int -> @b:Int -> Int

law Int.abs provedin fermat4.bendsource · line 48 · raw

@a:Int -> Nat

the absolute value, as a Nat

law Int.Le provedin fermat4.bendsource · line 53 · raw

@a:Int -> @b:Int -> Type

a <= b as a computed proposition (Unit or Empty), like N.Nat.Le

law t_add_1 provedin fermat4.bendsource · line 60 · raw

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

law t_add_2 provedin fermat4.bendsource · line 63 · raw

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

law t_mul_1 provedin fermat4.bendsource · line 66 · raw

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

law t_mul_2 provedin fermat4.bendsource · line 69 · raw

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

law t_sub_1 provedin fermat4.bendsource · line 72 · raw

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

law t_abs_1 provedin fermat4.bendsource · line 75 · raw

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

law of_add provedin fermat4.bendsource · line 81 · raw

@+a:Nat -> @+b:Nat -> {Int.add(Pos{a}, Pos{b}) == Pos{Nat.add(a, b)} : Int}

1. Int.of embeds Nat: addition and multiplication agree with Nat's

law of_mul provedin fermat4.bendsource · line 86 · raw

@+a:Nat -> @+b:Nat -> {Int.mul(Pos{a}, Pos{b}) == Pos{Nat.mul(a, b)} : Int}

law sub_def provedin fermat4.bendsource · line 92 · raw

@+a:Int -> @+b:Int -> {Int.sub(a, b) == Int.add(a, Int.neg(b)) : Int}

2. sub is add of the negation

law add_neg provedin fermat4.bendsource · line 98 · raw

@+a:Int -> {Int.add(a, Int.neg(a)) == Pos{0n} : Int}

3. a + (-a) = 0, and -(-a) = a

law neg_neg provedin fermat4.bendsource · line 102 · raw

@a:Int -> {Int.neg(Int.neg(a)) == a : Int}

law add_zero provedin fermat4.bendsource · line 108 · raw

@a:Int -> {Int.add(a, Pos{0n}) == a : Int}

4. (Int, add, 0) is a commutative group; (Int, mul, 1) a commutative monoid; mul distributes over add

law add_comm provedin fermat4.bendsource · line 112 · raw

@+a:Int -> @+b:Int -> {Int.add(a, b) == Int.add(b, a) : Int}

law add_assoc provedin fermat4.bendsource · line 117 · raw

@+a:Int -> @+b:Int -> @+c:Int -> {Int.add(a, Int.add(b, c)) == Int.add(Int.add(a, b), c) : Int}

law mul_one provedin fermat4.bendsource · line 123 · raw

@a:Int -> {Int.mul(a, Pos{1n}) == a : Int}

law mul_zero provedin fermat4.bendsource · line 127 · raw

@a:Int -> {Int.mul(a, Pos{0n}) == Pos{0n} : Int}

law mul_comm provedin fermat4.bendsource · line 131 · raw

@+a:Int -> @+b:Int -> {Int.mul(a, b) == Int.mul(b, a) : Int}

law mul_assoc provedin fermat4.bendsource · line 136 · raw

@+a:Int -> @+b:Int -> @+c:Int -> {Int.mul(a, Int.mul(b, c)) == Int.mul(Int.mul(a, b), c) : Int}

law mul_add provedin fermat4.bendsource · line 142 · raw

@+a:Int -> @+b:Int -> @+c:Int -> {Int.mul(a, Int.add(b, c)) == Int.add(Int.mul(a, b), Int.mul(a, c)) : Int}

law mul_eq_zero provedin fermat4.bendsource · line 149 · raw

@+a:Int -> @+b:Int -> @e:{Int.mul(a, b) == Pos{0n} : Int} -> @na:(@_:{a == Pos{0n} : Int} -> Empty) -> {b == Pos{0n} : Int}

5. no zero divisors (what the rationals will need)

law le_refl provedin fermat4.bendsource · line 158 · raw

@a:Int -> Int.Le(a, a)

6. the order: total, antisymmetric, compatible with add and with mul by a non-negative

law le_antisym provedin fermat4.bendsource · line 162 · raw

@+a:Int -> @+b:Int -> @h1:Int.Le(a, b) -> @h2:Int.Le(b, a) -> {a == b : Int}

law le_trans provedin fermat4.bendsource · line 169 · raw

@+a:Int -> @+b:Int -> @+c:Int -> @h1:Int.Le(a, b) -> @h2:Int.Le(b, c) -> Int.Le(a, c)

law le_add provedin fermat4.bendsource · line 177 · raw

@+a:Int -> @+b:Int -> @+c:Int -> @h:Int.Le(a, b) -> Int.Le(Int.add(a, c), Int.add(b, c))

law le_mul_nonneg provedin fermat4.bendsource · line 184 · raw

@+a:Int -> @+b:Int -> @+n:Nat -> @h:Int.Le(a, b) -> Int.Le(Int.mul(a, Pos{n}), Int.mul(b, Pos{n}))

law le_neg provedin fermat4.bendsource · line 192 · raw

@+a:Int -> @+b:Int -> @h:Int.Le(a, b) -> Int.Le(Int.neg(b), Int.neg(a))

7. neg reverses the order, and Pos{n} is never negative

law pos_nonneg provedin fermat4.bendsource · line 198 · raw

@n:Nat -> Int.Le(Pos{0n}, Pos{n})

Types

type Int source · line 13 · raw

Data

Pos
```
@n:Nat -> Int
```
NegS
```
@n:Nat -> Int
```

Definitions

def Int.of source · line 17 · raw

@n:Nat -> Int

def Int.zero source · line 20 · raw

Int

def Int.one source · line 23 · raw

Int