int_filled.bend source
int_filled.bend on the hub · documented module
import Baseimport ./nat.bend as Nimport ./int.bend as C# lib/claims/int_filled.bend -- fills for lib/claims/int.bend.## The representation is fixed by the claim file: Pos{n} is n and NegS{n}# is -(1+n). Every operation below is written so that it computes on# constructors, which is what makes the test cases and the embedding laws# close with {==}.# ---- helpers ------------------------------------------------------------# -n, as an Int (the only place the two zeros have to be reconciled)def Int.neg_nat(n: Nat) -> C.Int: match n: case 0n: C.Pos{0n} case 1n+p: C.NegS{p}# a - b for Nats, as an Intdef Int.sub_nat(a: Nat, b: Nat) -> C.Int: match a b: case 0n 0n: C.Pos{0n} case 0n 1n+bp: C.NegS{bp} case 1n+ap 0n: C.Pos{1n+ap} case 1n+ap 1n+bp: Int.sub_nat(ap, bp)# ---- operations ---------------------------------------------------------def C.Int.neg(a): match a: case C.Pos{n}: Int.neg_nat(n) case C.NegS{n}: C.Pos{1n+n}def C.Int.add(a, b): match a b: case C.Pos{x} C.Pos{y}: C.Pos{Nat.add(x, y)} case C.Pos{x} C.NegS{y}: Int.sub_nat(x, 1n+y) case C.NegS{x} C.Pos{y}: Int.sub_nat(y, 1n+x) case C.NegS{x} C.NegS{y}: C.NegS{1n+Nat.add(x, y)}def C.Int.mul(a, b): match a b: case C.Pos{x} C.Pos{y}: C.Pos{Nat.mul(x, y)} case C.Pos{x} C.NegS{y}: Int.neg_nat(Nat.mul(x, 1n+y)) case C.NegS{x} C.Pos{y}: Int.neg_nat(Nat.mul(1n+x, y)) case C.NegS{x} C.NegS{y}: C.Pos{Nat.mul(1n+x, 1n+y)}def C.Int.sub(a, b): C.Int.add(a, C.Int.neg(b))def C.Int.abs(a): match a: case C.Pos{n}: n case C.NegS{n}: 1n+ndef C.Int.Le(a, b): match a b: case C.Pos{x} C.Pos{y}: N.Nat.Le(x, y) case C.Pos{x} C.NegS{y}: Empty case C.NegS{x} C.Pos{y}: Unit case C.NegS{x} C.NegS{y}: N.Nat.Le(y, x)# ---- test cases ---------------------------------------------------------def C.t_add_1(): {==}def C.t_add_2(): {==}def C.t_mul_1(): {==}def C.t_mul_2(): {==}def C.t_sub_1(): {==}def C.t_abs_1(): {==}# ---- laws ---------------------------------------------------------------def C.of_add(a, b): {==}def C.of_mul(a, b): {==}def C.sub_def(a, b): {==}# n - n = 0def Int.sub_nat_self(n: Nat) -> {Int.sub_nat(n, n) == C.Pos{0n} : C.Int}: match n: case 0n: {==} case 1n+p: Int.sub_nat_self(p)def C.add_neg(a): match a: case C.Pos{n}: match n: case 0n: {==} case 1n+p: Int.sub_nat_self(p) case C.NegS{n}: Int.sub_nat_self(n)def C.neg_neg(a): match a: case C.Pos{n}: match n: case 0n: {==} case 1n+p: {==} case C.NegS{n}: {==}def C.add_zero(a): match a: case C.Pos{n}: %N.Nat.add_zero(n) : {C.Pos{Nat.add(n, 0n)} == C.Pos{_} : C.Int} {==} case C.NegS{n}: {==}def C.add_comm(a, b): match a b: case C.Pos{x} C.Pos{y}: %N.Nat.add_comm(x, y) : {C.Pos{Nat.add(x, y)} == C.Pos{_} : C.Int} {==} case C.Pos{x} C.NegS{y}: {==} case C.NegS{x} C.Pos{y}: {==} case C.NegS{x} C.NegS{y}: %N.Nat.add_comm(x, y) : {C.NegS{1n+Nat.add(x, y)} == C.NegS{1n+_} : C.Int} {==}def C.mul_one(a): match a: case C.Pos{n}: %N.Nat.mul_one(n) : {C.Pos{Nat.mul(n, 1n)} == C.Pos{_} : C.Int} {==} case C.NegS{n}: %N.Nat.mul_one(n) : {C.NegS{Nat.mul(n, 1n)} == C.NegS{_} : C.Int} {==}def C.mul_zero(a): match a: case C.Pos{n}: %N.Nat.mul_zero(n) : {C.Pos{Nat.mul(n, 0n)} == C.Pos{_} : C.Int} {==} case C.NegS{n}: %Equal.sym(Nat, Nat.mul(n, 0n), 0n, N.Nat.mul_zero(n)) : {Int.neg_nat(_) == C.Pos{0n} : C.Int} {==}def C.mul_comm(a, b): match a b: case C.Pos{x} C.Pos{y}: %N.Nat.mul_comm(x, y) : {C.Pos{Nat.mul(x, y)} == C.Pos{_} : C.Int} {==} case C.Pos{x} C.NegS{y}: %N.Nat.mul_comm(x, 1n+y) : {Int.neg_nat(Nat.mul(x, 1n+y)) == Int.neg_nat(_) : C.Int} {==} case C.NegS{x} C.Pos{y}: %N.Nat.mul_comm(1n+x, y) : {Int.neg_nat(Nat.mul(1n+x, y)) == Int.neg_nat(_) : C.Int} {==} case C.NegS{x} C.NegS{y}: %N.Nat.mul_comm(1n+x, 1n+y) : {C.Pos{Nat.mul(1n+x, 1n+y)} == C.Pos{_} : C.Int} {==}def C.le_refl(a): match a: case C.Pos{n}: N.Nat.le_refl(n) case C.NegS{n}: N.Nat.le_refl(n)def C.le_antisym(a, b, h1, h2): match a b: case C.Pos{x} C.Pos{y}: %N.Nat.le_antisym(x, y, h1, h2) : {C.Pos{x} == C.Pos{_} : C.Int} {==} case C.Pos{x} C.NegS{y}: match h1: case C.NegS{x} C.Pos{y}: match h2: case C.NegS{x} C.NegS{y}: %N.Nat.le_antisym(x, y, h2, h1) : {C.NegS{x} == C.NegS{_} : C.Int} {==}def C.le_trans(a, b, c, h1, h2): match a b c: case C.Pos{x} C.Pos{y} C.Pos{z}: N.Nat.le_trans(x, y, z, h1, h2) case C.Pos{x} C.Pos{y} C.NegS{z}: match h2: case C.Pos{x} C.NegS{y} C.Pos{z}: match h1: case C.Pos{x} C.NegS{y} C.NegS{z}: match h1: case C.NegS{x} C.Pos{y} C.Pos{z}: Unit{} case C.NegS{x} C.Pos{y} C.NegS{z}: match h2: case C.NegS{x} C.NegS{y} C.Pos{z}: Unit{} case C.NegS{x} C.NegS{y} C.NegS{z}: N.Nat.le_trans(z, y, x, h2, h1)def C.pos_nonneg(n): Unit{}# ---- the difference view -------------------------------------------------## Every Int is Int.sub_nat(p, m) for a pair of Nats, and the operations# act on such pairs the way school arithmetic says. Proving that once# turns the ring laws into Nat lemmas.def Int.toP(a: C.Int) -> Nat: match a: case C.Pos{n}: n case C.NegS{n}: 0ndef Int.toM(a: C.Int) -> Nat: match a: case C.Pos{n}: 0n case C.NegS{n}: 1n+ndef Int.sub_nat_zero(x: Nat) -> {Int.sub_nat(x, 0n) == C.Pos{x} : C.Int}: match x: case 0n: {==} case 1n+xp: {==}def Int.sub_nat_zero_l(x: Nat) -> {Int.sub_nat(0n, x) == Int.neg_nat(x) : C.Int}: match x: case 0n: {==} case 1n+xp: {==}def Int.split(a: C.Int) -> {Int.sub_nat(Int.toP(a), Int.toM(a)) == a : C.Int}: match a: case C.Pos{n}: Int.sub_nat_zero(n) case C.NegS{n}: {==}def Int.by1(-P: C.Int -> Type, +a: C.Int, w: P(Int.sub_nat(Int.toP(a), Int.toM(a)))) -> P(a): %Int.split(a) : P(_) wdef Int.by2(-P: C.Int -> C.Int -> Type, +a: C.Int, +b: C.Int, w: P(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b)))) -> P(a, b): %Int.split(a) : P(_, b) %Int.split(b) : P(Int.sub_nat(Int.toP(a), Int.toM(a)), _) wdef Int.by3(-P: C.Int -> C.Int -> C.Int -> Type, +a: C.Int, +b: C.Int, +c: C.Int, w: P(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b)), Int.sub_nat(Int.toP(c), Int.toM(c)))) -> P(a, b, c): %Int.split(a) : P(_, b, c) %Int.split(b) : P(Int.sub_nat(Int.toP(a), Int.toM(a)), _, c) %Int.split(c) : P(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b)), _) w# p + (q - n) = (p + q) - ndef Int.add_pos(+x: Nat, q: Nat, n: Nat) -> {C.Int.add(C.Pos{x}, Int.sub_nat(q, n)) == Int.sub_nat(Nat.add(x, q), n) : C.Int}: match q n: case 0n 0n: Equal.sym(C.Int, Int.sub_nat(Nat.add(x, 0n), 0n), C.Pos{Nat.add(x, 0n)}, Int.sub_nat_zero(Nat.add(x, 0n))) case 0n 1n+np: %N.Nat.add_zero(x) : {Int.sub_nat(_, 1n+np) == Int.sub_nat(Nat.add(x, 0n), 1n+np) : C.Int} {==} case 1n+qp 0n: Equal.sym(C.Int, Int.sub_nat(Nat.add(x, 1n+qp), 0n), C.Pos{Nat.add(x, 1n+qp)}, Int.sub_nat_zero(Nat.add(x, 1n+qp))) case 1n+qp 1n+np: %Equal.sym(Nat, Nat.add(x, 1n+qp), 1n+Nat.add(x, qp), N.Nat.add_succ(x, qp)) : {C.Int.add(C.Pos{x}, Int.sub_nat(qp, np)) == Int.sub_nat(_, 1n+np) : C.Int} Int.add_pos(x, qp, np)# -(1+m) + (q - n) = q - (1 + m + n)def Int.add_negs(+m: Nat, q: Nat, n: Nat) -> {C.Int.add(C.NegS{m}, Int.sub_nat(q, n)) == Int.sub_nat(q, 1n+Nat.add(m, n)) : C.Int}: match q n: case 0n 0n: %Equal.sym(Nat, Nat.add(m, 0n), m, N.Nat.add_zero(m)) : {C.NegS{m} == C.NegS{_} : C.Int} {==} case 0n 1n+np: %N.Nat.add_succ(m, np) : {C.NegS{_} == C.NegS{Nat.add(m, 1n+np)} : C.Int} {==} case 1n+qp 0n: %Equal.sym(Nat, Nat.add(m, 0n), m, N.Nat.add_zero(m)) : {Int.sub_nat(qp, m) == Int.sub_nat(qp, _) : C.Int} {==} case 1n+qp 1n+np: %Equal.sym(Nat, Nat.add(m, 1n+np), 1n+Nat.add(m, np), N.Nat.add_succ(m, np)) : {C.Int.add(C.NegS{m}, Int.sub_nat(qp, np)) == Int.sub_nat(qp, _) : C.Int} Int.add_negs(m, qp, np)# (p - m) + (q - n) = (p + q) - (m + n)def Int.add_sub(p: Nat, m: Nat, +q: Nat, +n: Nat) -> {C.Int.add(Int.sub_nat(p, m), Int.sub_nat(q, n)) == Int.sub_nat(Nat.add(p, q), Nat.add(m, n)) : C.Int}: match p m: case 0n 0n: Int.add_pos(0n, q, n) case 0n 1n+mp: Int.add_negs(mp, q, n) case 1n+pp 0n: Int.add_pos(1n+pp, q, n) case 1n+pp 1n+mp: Int.add_sub(pp, mp, q, n)def Int.add_assoc.core(+p1: Nat, +m1: Nat, +p2: Nat, +m2: Nat, +p3: Nat, +m3: Nat) -> {C.Int.add(Int.sub_nat(p1, m1), C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3))) == C.Int.add(C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(p2, m2)), Int.sub_nat(p3, m3)) : C.Int}: %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3)), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3)), Int.add_sub(p2, m2, p3, m3)) : {C.Int.add(Int.sub_nat(p1, m1), _) == C.Int.add(C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(p2, m2)), Int.sub_nat(p3, m3)) : C.Int} %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(p2, m2)), Int.sub_nat(Nat.add(p1, p2), Nat.add(m1, m2)), Int.add_sub(p1, m1, p2, m2)) : {C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(_, Int.sub_nat(p3, m3)) : C.Int} %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))), Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), Nat.add(m1, Nat.add(m2, m3))), Int.add_sub(p1, m1, Nat.add(p2, p3), Nat.add(m2, m3))) : {_ == C.Int.add(Int.sub_nat(Nat.add(p1, p2), Nat.add(m1, m2)), Int.sub_nat(p3, m3)) : C.Int} %Equal.sym(C.Int, C.Int.add(Int.sub_nat(Nat.add(p1, p2), Nat.add(m1, m2)), Int.sub_nat(p3, m3)), Int.sub_nat(Nat.add(Nat.add(p1, p2), p3), Nat.add(Nat.add(m1, m2), m3)), Int.add_sub(Nat.add(p1, p2), Nat.add(m1, m2), p3, m3)) : {Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), Nat.add(m1, Nat.add(m2, m3))) == _ : C.Int} %N.Nat.add_assoc(p1, p2, p3) : {Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), Nat.add(m1, Nat.add(m2, m3))) == Int.sub_nat(_, Nat.add(Nat.add(m1, m2), m3)) : C.Int} %N.Nat.add_assoc(m1, m2, m3) : {Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), Nat.add(m1, Nat.add(m2, m3))) == Int.sub_nat(Nat.add(p1, Nat.add(p2, p3)), _) : C.Int} {==}def C.add_assoc(a, b, c): Int.by3(x => y => z => {C.Int.add(x, C.Int.add(y, z)) == C.Int.add(C.Int.add(x, y), z) : C.Int}, a, b, c, Int.add_assoc.core(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.toP(c), Int.toM(c)))# (k+u) - (k+v) = u - vdef Int.sub_nat_cancel(k: Nat, -u: Nat, -v: Nat) -> {Int.sub_nat(Nat.add(k, u), Nat.add(k, v)) == Int.sub_nat(u, v) : C.Int}: match k: case 0n: {==} case 1n+kp: Int.sub_nat_cancel(kp, u, v)# x * (q - n) = xq - xndef Int.mul_pos(+x: Nat, q: Nat, n: Nat) -> {C.Int.mul(C.Pos{x}, Int.sub_nat(q, n)) == Int.sub_nat(Nat.mul(x, q), Nat.mul(x, n)) : C.Int}: match q n: case 0n 0n: %Equal.sym(Nat, Nat.mul(x, 0n), 0n, N.Nat.mul_zero(x)) : {C.Pos{_} == Int.sub_nat(_, _) : C.Int} {==} case 0n 1n+np: %Equal.sym(Nat, Nat.mul(x, 0n), 0n, N.Nat.mul_zero(x)) : {Int.neg_nat(Nat.mul(x, 1n+np)) == Int.sub_nat(_, Nat.mul(x, 1n+np)) : C.Int} Equal.sym(C.Int, Int.sub_nat(0n, Nat.mul(x, 1n+np)), Int.neg_nat(Nat.mul(x, 1n+np)), Int.sub_nat_zero_l(Nat.mul(x, 1n+np))) case 1n+qp 0n: %Equal.sym(Nat, Nat.mul(x, 0n), 0n, N.Nat.mul_zero(x)) : {C.Pos{Nat.mul(x, 1n+qp)} == Int.sub_nat(Nat.mul(x, 1n+qp), _) : C.Int} Equal.sym(C.Int, Int.sub_nat(Nat.mul(x, 1n+qp), 0n), C.Pos{Nat.mul(x, 1n+qp)}, Int.sub_nat_zero(Nat.mul(x, 1n+qp))) case 1n+qp 1n+np: +qp2 = qp +np2 = np %Equal.sym(Nat, Nat.mul(x, 1n+qp2), Nat.add(x, Nat.mul(x, qp2)), N.Nat.mul_succ(x, qp2)) : {C.Int.mul(C.Pos{x}, Int.sub_nat(qp2, np2)) == Int.sub_nat(_, Nat.mul(x, 1n+np2)) : C.Int} %Equal.sym(Nat, Nat.mul(x, 1n+np2), Nat.add(x, Nat.mul(x, np2)), N.Nat.mul_succ(x, np2)) : {C.Int.mul(C.Pos{x}, Int.sub_nat(qp2, np2)) == Int.sub_nat(Nat.add(x, Nat.mul(x, qp2)), _) : C.Int} Equal.trans(C.Int, C.Int.mul(C.Pos{x}, Int.sub_nat(qp2, np2)), Int.sub_nat(Nat.mul(x, qp2), Nat.mul(x, np2)), Int.sub_nat(Nat.add(x, Nat.mul(x, qp2)), Nat.add(x, Nat.mul(x, np2))), Int.mul_pos(x, qp2, np2), Equal.sym(C.Int, Int.sub_nat(Nat.add(x, Nat.mul(x, qp2)), Nat.add(x, Nat.mul(x, np2))), Int.sub_nat(Nat.mul(x, qp2), Nat.mul(x, np2)), Int.sub_nat_cancel(x, Nat.mul(x, qp2), Nat.mul(x, np2))))# -(1+m) * (q - n) = (1+m)n - (1+m)qdef Int.mul_negs(+m: Nat, q: Nat, n: Nat) -> {C.Int.mul(C.NegS{m}, Int.sub_nat(q, n)) == Int.sub_nat(Nat.mul(1n+m, n), Nat.mul(1n+m, q)) : C.Int}: match q n: case 0n 0n: %Equal.sym(Nat, Nat.mul(1n+m, 0n), 0n, N.Nat.mul_zero(1n+m)) : {Int.neg_nat(_) == Int.sub_nat(_, _) : C.Int} {==} case 0n 1n+np: %Equal.sym(Nat, Nat.mul(1n+m, 0n), 0n, N.Nat.mul_zero(1n+m)) : {C.Pos{Nat.mul(1n+m, 1n+np)} == Int.sub_nat(Nat.mul(1n+m, 1n+np), _) : C.Int} Equal.sym(C.Int, Int.sub_nat(Nat.mul(1n+m, 1n+np), 0n), C.Pos{Nat.mul(1n+m, 1n+np)}, Int.sub_nat_zero(Nat.mul(1n+m, 1n+np))) case 1n+qp 0n: %Equal.sym(Nat, Nat.mul(1n+m, 0n), 0n, N.Nat.mul_zero(1n+m)) : {Int.neg_nat(Nat.mul(1n+m, 1n+qp)) == Int.sub_nat(_, Nat.mul(1n+m, 1n+qp)) : C.Int} Equal.sym(C.Int, Int.sub_nat(0n, Nat.mul(1n+m, 1n+qp)), Int.neg_nat(Nat.mul(1n+m, 1n+qp)), Int.sub_nat_zero_l(Nat.mul(1n+m, 1n+qp))) case 1n+qp 1n+np: +qp2 = qp +np2 = np %Equal.sym(Nat, Nat.mul(1n+m, 1n+np2), Nat.add(1n+m, Nat.mul(1n+m, np2)), N.Nat.mul_succ(1n+m, np2)) : {C.Int.mul(C.NegS{m}, Int.sub_nat(qp2, np2)) == Int.sub_nat(_, Nat.mul(1n+m, 1n+qp2)) : C.Int} %Equal.sym(Nat, Nat.mul(1n+m, 1n+qp2), Nat.add(1n+m, Nat.mul(1n+m, qp2)), N.Nat.mul_succ(1n+m, qp2)) : {C.Int.mul(C.NegS{m}, Int.sub_nat(qp2, np2)) == Int.sub_nat(Nat.add(1n+m, Nat.mul(1n+m, np2)), _) : C.Int} Equal.trans(C.Int, C.Int.mul(C.NegS{m}, Int.sub_nat(qp2, np2)), Int.sub_nat(Nat.mul(1n+m, np2), Nat.mul(1n+m, qp2)), Int.sub_nat(Nat.add(1n+m, Nat.mul(1n+m, np2)), Nat.add(1n+m, Nat.mul(1n+m, qp2))), Int.mul_negs(m, qp2, np2), Equal.sym(C.Int, Int.sub_nat(Nat.add(1n+m, Nat.mul(1n+m, np2)), Nat.add(1n+m, Nat.mul(1n+m, qp2))), Int.sub_nat(Nat.mul(1n+m, np2), Nat.mul(1n+m, qp2)), Int.sub_nat_cancel(1n+m, Nat.mul(1n+m, np2), Nat.mul(1n+m, qp2))))def Int.mul_add.core(a: C.Int, +p2: Nat, +m2: Nat, +p3: Nat, +m3: Nat) -> {C.Int.mul(a, C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3))) == C.Int.add(C.Int.mul(a, Int.sub_nat(p2, m2)), C.Int.mul(a, Int.sub_nat(p3, m3))) : C.Int}: match a: case C.Pos{x}: +x2 = x %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3)), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3)), Int.add_sub(p2, m2, p3, m3)) : {C.Int.mul(C.Pos{x2}, _) == C.Int.add(C.Int.mul(C.Pos{x2}, Int.sub_nat(p2, m2)), C.Int.mul(C.Pos{x2}, Int.sub_nat(p3, m3))) : C.Int} %Equal.sym(C.Int, C.Int.mul(C.Pos{x2}, Int.sub_nat(p2, m2)), Int.sub_nat(Nat.mul(x2, p2), Nat.mul(x2, m2)), Int.mul_pos(x2, p2, m2)) : {C.Int.mul(C.Pos{x2}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(_, C.Int.mul(C.Pos{x2}, Int.sub_nat(p3, m3))) : C.Int} %Equal.sym(C.Int, C.Int.mul(C.Pos{x2}, Int.sub_nat(p3, m3)), Int.sub_nat(Nat.mul(x2, p3), Nat.mul(x2, m3)), Int.mul_pos(x2, p3, m3)) : {C.Int.mul(C.Pos{x2}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(Int.sub_nat(Nat.mul(x2, p2), Nat.mul(x2, m2)), _) : C.Int} %Equal.sym(C.Int, C.Int.mul(C.Pos{x2}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))), Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), Nat.mul(x2, Nat.add(m2, m3))), Int.mul_pos(x2, Nat.add(p2, p3), Nat.add(m2, m3))) : {_ == C.Int.add(Int.sub_nat(Nat.mul(x2, p2), Nat.mul(x2, m2)), Int.sub_nat(Nat.mul(x2, p3), Nat.mul(x2, m3))) : C.Int} %Equal.sym(C.Int, C.Int.add(Int.sub_nat(Nat.mul(x2, p2), Nat.mul(x2, m2)), Int.sub_nat(Nat.mul(x2, p3), Nat.mul(x2, m3))), Int.sub_nat(Nat.add(Nat.mul(x2, p2), Nat.mul(x2, p3)), Nat.add(Nat.mul(x2, m2), Nat.mul(x2, m3))), Int.add_sub(Nat.mul(x2, p2), Nat.mul(x2, m2), Nat.mul(x2, p3), Nat.mul(x2, m3))) : {Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), Nat.mul(x2, Nat.add(m2, m3))) == _ : C.Int} %N.Nat.mul_add(x2, p2, p3) : {Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), Nat.mul(x2, Nat.add(m2, m3))) == Int.sub_nat(_, Nat.add(Nat.mul(x2, m2), Nat.mul(x2, m3))) : C.Int} %N.Nat.mul_add(x2, m2, m3) : {Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), Nat.mul(x2, Nat.add(m2, m3))) == Int.sub_nat(Nat.mul(x2, Nat.add(p2, p3)), _) : C.Int} {==} case C.NegS{m}: +m2b = m %Equal.sym(C.Int, C.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3)), Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3)), Int.add_sub(p2, m2, p3, m3)) : {C.Int.mul(C.NegS{m2b}, _) == C.Int.add(C.Int.mul(C.NegS{m2b}, Int.sub_nat(p2, m2)), C.Int.mul(C.NegS{m2b}, Int.sub_nat(p3, m3))) : C.Int} %Equal.sym(C.Int, C.Int.mul(C.NegS{m2b}, Int.sub_nat(p2, m2)), Int.sub_nat(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2)), Int.mul_negs(m2b, p2, m2)) : {C.Int.mul(C.NegS{m2b}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(_, C.Int.mul(C.NegS{m2b}, Int.sub_nat(p3, m3))) : C.Int} %Equal.sym(C.Int, C.Int.mul(C.NegS{m2b}, Int.sub_nat(p3, m3)), Int.sub_nat(Nat.mul(1n+m2b, m3), Nat.mul(1n+m2b, p3)), Int.mul_negs(m2b, p3, m3)) : {C.Int.mul(C.NegS{m2b}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))) == C.Int.add(Int.sub_nat(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2)), _) : C.Int} %Equal.sym(C.Int, C.Int.mul(C.NegS{m2b}, Int.sub_nat(Nat.add(p2, p3), Nat.add(m2, m3))), Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), Nat.mul(1n+m2b, Nat.add(p2, p3))), Int.mul_negs(m2b, Nat.add(p2, p3), Nat.add(m2, m3))) : {_ == C.Int.add(Int.sub_nat(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2)), Int.sub_nat(Nat.mul(1n+m2b, m3), Nat.mul(1n+m2b, p3))) : C.Int} %Equal.sym(C.Int, C.Int.add(Int.sub_nat(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2)), Int.sub_nat(Nat.mul(1n+m2b, m3), Nat.mul(1n+m2b, p3))), Int.sub_nat(Nat.add(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, m3)), Nat.add(Nat.mul(1n+m2b, p2), Nat.mul(1n+m2b, p3))), Int.add_sub(Nat.mul(1n+m2b, m2), Nat.mul(1n+m2b, p2), Nat.mul(1n+m2b, m3), Nat.mul(1n+m2b, p3))) : {Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), Nat.mul(1n+m2b, Nat.add(p2, p3))) == _ : C.Int} %N.Nat.mul_add(1n+m2b, m2, m3) : {Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), Nat.mul(1n+m2b, Nat.add(p2, p3))) == Int.sub_nat(_, Nat.add(Nat.mul(1n+m2b, p2), Nat.mul(1n+m2b, p3))) : C.Int} %N.Nat.mul_add(1n+m2b, p2, p3) : {Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), Nat.mul(1n+m2b, Nat.add(p2, p3))) == Int.sub_nat(Nat.mul(1n+m2b, Nat.add(m2, m3)), _) : C.Int} {==}def C.mul_add(a, b, c): Int.by2(y => z => {C.Int.mul(a, C.Int.add(y, z)) == C.Int.add(C.Int.mul(a, y), C.Int.mul(a, z)) : C.Int}, b, c, Int.mul_add.core(a, Int.toP(b), Int.toM(b), Int.toP(c), Int.toM(c)))# ---- the order, through the same view -----------------------------------## Int.Le(p - m, q - n) is exactly Nat.Le(p + n, q + m). Both directions# are needed: the forward one to open a hypothesis, the backward one to# close a goal.def Int.le_cast(-x: Nat, -y: Nat, -c: Nat, e: {x == y : Nat}, h: N.Nat.Le(x, c)) -> N.Nat.Le(y, c): %e : N.Nat.Le(_, c) hdef Int.le_cast_r(-x: Nat, -y: Nat, -c: Nat, e: {x == y : Nat}, h: N.Nat.Le(c, x)) -> N.Nat.Le(c, y): %e : N.Nat.Le(c, _) hdef Int.le_succ_zero(-k: Nat, h: N.Nat.Le(1n+k, 0n)) -> Empty: match h:def Int.neg_sub(p: Nat, m: Nat) -> {C.Int.neg(Int.sub_nat(p, m)) == Int.sub_nat(m, p) : C.Int}: match p m: case 0n 0n: {==} case 0n 1n+mp: {==} case 1n+pp 0n: {==} case 1n+pp 1n+mp: Int.neg_sub(pp, mp)def Int.le_pos_f(+x: Nat, q: Nat, n: Nat, h: C.Int.Le(C.Pos{x}, Int.sub_nat(q, n))) -> N.Nat.Le(Nat.add(x, n), q): match q n: case 0n 0n: %Equal.sym(Nat, Nat.add(x, 0n), x, N.Nat.add_zero(x)) : N.Nat.Le(_, 0n) h case 0n 1n+np: match h: case 1n+qp 0n: %Equal.sym(Nat, Nat.add(x, 0n), x, N.Nat.add_zero(x)) : N.Nat.Le(_, 1n+qp) h case 1n+qp 1n+np: %Equal.sym(Nat, Nat.add(x, 1n+np), 1n+Nat.add(x, np), N.Nat.add_succ(x, np)) : N.Nat.Le(_, 1n+qp) Int.le_pos_f(x, qp, np, h)def Int.le_negs_f(+m: Nat, q: Nat, n: Nat, h: C.Int.Le(C.NegS{m}, Int.sub_nat(q, n))) -> N.Nat.Le(n, Nat.add(q, 1n+m)): match q n: case 0n 0n: Unit{} case 0n 1n+np: h case 1n+qp 0n: Unit{} case 1n+qp 1n+np: Int.le_negs_f(m, qp, np, h)def Int.le_f(p: Nat, m: Nat, +q: Nat, +n: Nat, h: C.Int.Le(Int.sub_nat(p, m), Int.sub_nat(q, n))) -> N.Nat.Le(Nat.add(p, n), Nat.add(q, m)): match p m: case 0n 0n: %Equal.sym(Nat, Nat.add(q, 0n), q, N.Nat.add_zero(q)) : N.Nat.Le(Nat.add(0n, n), _) Int.le_pos_f(0n, q, n, h) case 0n 1n+mp: Int.le_negs_f(mp, q, n, h) case 1n+pp 0n: %Equal.sym(Nat, Nat.add(q, 0n), q, N.Nat.add_zero(q)) : N.Nat.Le(Nat.add(1n+pp, n), _) Int.le_pos_f(1n+pp, q, n, h) case 1n+pp 1n+mp: %Equal.sym(Nat, Nat.add(q, 1n+mp), 1n+Nat.add(q, mp), N.Nat.add_succ(q, mp)) : N.Nat.Le(Nat.add(1n+pp, n), _) Int.le_f(pp, mp, q, n, h)def Int.le_pos_b(+x: Nat, q: Nat, n: Nat, h: N.Nat.Le(Nat.add(x, n), q)) -> C.Int.Le(C.Pos{x}, Int.sub_nat(q, n)): match q n: case 0n 0n: %N.Nat.add_zero(x) : N.Nat.Le(_, 0n) h case 0n 1n+np: Empty.absurd(C.Int.Le(C.Pos{x}, C.NegS{np}), Int.le_succ_zero(Nat.add(x, np), Int.le_cast(Nat.add(x, 1n+np), 1n+Nat.add(x, np), 0n, N.Nat.add_succ(x, np), h))) case 1n+qp 0n: %N.Nat.add_zero(x) : N.Nat.Le(_, 1n+qp) h case 1n+qp 1n+np: Int.le_pos_b(x, qp, np, Int.le_cast(Nat.add(x, 1n+np), 1n+Nat.add(x, np), 1n+qp, N.Nat.add_succ(x, np), h))def Int.le_negs_b(+m: Nat, q: Nat, n: Nat, h: N.Nat.Le(n, Nat.add(q, 1n+m))) -> C.Int.Le(C.NegS{m}, Int.sub_nat(q, n)): match q n: case 0n 0n: Unit{} case 0n 1n+np: h case 1n+qp 0n: Unit{} case 1n+qp 1n+np: Int.le_negs_b(m, qp, np, h)def Int.le_b(p: Nat, m: Nat, +q: Nat, +n: Nat, h: N.Nat.Le(Nat.add(p, n), Nat.add(q, m))) -> C.Int.Le(Int.sub_nat(p, m), Int.sub_nat(q, n)): match p m: case 0n 0n: Int.le_pos_b(0n, q, n, Int.le_cast_r(Nat.add(q, 0n), q, Nat.add(0n, n), N.Nat.add_zero(q), h)) case 0n 1n+mp: Int.le_negs_b(mp, q, n, h) case 1n+pp 0n: Int.le_pos_b(1n+pp, q, n, Int.le_cast_r(Nat.add(q, 0n), q, Nat.add(1n+pp, n), N.Nat.add_zero(q), h)) case 1n+pp 1n+mp: Int.le_b(pp, mp, q, n, Int.le_cast_r(Nat.add(q, 1n+mp), 1n+Nat.add(q, mp), Nat.add(1n+pp, n), N.Nat.add_succ(q, mp), h))def Int.le_split(+a: C.Int, +b: C.Int, h: C.Int.Le(a, b)) -> C.Int.Le(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b))): %Equal.sym(C.Int, Int.sub_nat(Int.toP(a), Int.toM(a)), a, Int.split(a)) : C.Int.Le(_, Int.sub_nat(Int.toP(b), Int.toM(b))) %Equal.sym(C.Int, Int.sub_nat(Int.toP(b), Int.toM(b)), b, Int.split(b)) : C.Int.Le(a, _) hdef Int.le_neg.core(+pa: Nat, +ma: Nat, +pb: Nat, +mb: Nat, h: N.Nat.Le(Nat.add(pa, mb), Nat.add(pb, ma))) -> C.Int.Le(C.Int.neg(Int.sub_nat(pb, mb)), C.Int.neg(Int.sub_nat(pa, ma))): %Equal.sym(C.Int, C.Int.neg(Int.sub_nat(pb, mb)), Int.sub_nat(mb, pb), Int.neg_sub(pb, mb)) : C.Int.Le(_, C.Int.neg(Int.sub_nat(pa, ma))) %Equal.sym(C.Int, C.Int.neg(Int.sub_nat(pa, ma)), Int.sub_nat(ma, pa), Int.neg_sub(pa, ma)) : C.Int.Le(Int.sub_nat(mb, pb), _) Int.le_b(mb, pb, ma, pa, Int.le_cast_r(Nat.add(pb, ma), Nat.add(ma, pb), Nat.add(mb, pa), N.Nat.add_comm(pb, ma), Int.le_cast(Nat.add(pa, mb), Nat.add(mb, pa), Nat.add(pb, ma), N.Nat.add_comm(pa, mb), h)))def C.le_neg(a, b, h): Int.by2(x => y => C.Int.Le(C.Int.neg(y), C.Int.neg(x)), a, b, Int.le_neg.core(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.le_f(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.le_split(a, b, h))))def Int.le_add.core(+pa: Nat, +ma: Nat, +pb: Nat, +mb: Nat, +pc: Nat, +mc: Nat, h: N.Nat.Le(Nat.add(pa, mb), Nat.add(pb, ma))) -> C.Int.Le(C.Int.add(Int.sub_nat(pa, ma), Int.sub_nat(pc, mc)), C.Int.add(Int.sub_nat(pb, mb), Int.sub_nat(pc, mc))): %Equal.sym(C.Int, C.Int.add(Int.sub_nat(pa, ma), Int.sub_nat(pc, mc)), Int.sub_nat(Nat.add(pa, pc), Nat.add(ma, mc)), Int.add_sub(pa, ma, pc, mc)) : C.Int.Le(_, C.Int.add(Int.sub_nat(pb, mb), Int.sub_nat(pc, mc))) %Equal.sym(C.Int, C.Int.add(Int.sub_nat(pb, mb), Int.sub_nat(pc, mc)), Int.sub_nat(Nat.add(pb, pc), Nat.add(mb, mc)), Int.add_sub(pb, mb, pc, mc)) : C.Int.Le(Int.sub_nat(Nat.add(pa, pc), Nat.add(ma, mc)), _) Int.le_b(Nat.add(pa, pc), Nat.add(ma, mc), Nat.add(pb, pc), Nat.add(mb, mc), Int.le_cast_r(Nat.add(Nat.add(pb, ma), Nat.add(pc, mc)), Nat.add(Nat.add(pb, pc), Nat.add(ma, mc)), Nat.add(Nat.add(pa, pc), Nat.add(mb, mc)), N.Nat.add_add_swap(pb, ma, pc, mc), Int.le_cast(Nat.add(Nat.add(pa, mb), Nat.add(pc, mc)), Nat.add(Nat.add(pa, pc), Nat.add(mb, mc)), Nat.add(Nat.add(pb, ma), Nat.add(pc, mc)), N.Nat.add_add_swap(pa, mb, pc, mc), N.Nat.le_add_both(Nat.add(pa, mb), Nat.add(pb, ma), Nat.add(pc, mc), Nat.add(pc, mc), h, N.Nat.le_refl(Nat.add(pc, mc))))))def C.le_add(a, b, c, h): Int.by3(x => y => z => C.Int.Le(C.Int.add(x, z), C.Int.add(y, z)), a, b, c, Int.le_add.core(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.toP(c), Int.toM(c), Int.le_f(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.le_split(a, b, h))))# x <= y gives xc <= ycdef Int.le_mul_r(x: Nat, y: Nat, +c: Nat, h: N.Nat.Le(x, y)) -> N.Nat.Le(Nat.mul(x, c), Nat.mul(y, c)): match x y: case 0n 0n: Unit{} case 0n 1n+yp: Unit{} case 1n+xp 0n: match h: case 1n+xp 1n+yp: N.Nat.le_add_mono_l(c, Nat.mul(xp, c), Nat.mul(yp, c), Int.le_mul_r(xp, yp, c, h))# (p - m) * k = pk - mkdef Int.mul_sub_r(+p: Nat, +m: Nat, +k: Nat) -> {C.Int.mul(Int.sub_nat(p, m), C.Pos{k}) == Int.sub_nat(Nat.mul(p, k), Nat.mul(m, k)) : C.Int}: %Equal.sym(C.Int, C.Int.mul(Int.sub_nat(p, m), C.Pos{k}), C.Int.mul(C.Pos{k}, Int.sub_nat(p, m)), C.mul_comm(Int.sub_nat(p, m), C.Pos{k})) : {_ == Int.sub_nat(Nat.mul(p, k), Nat.mul(m, k)) : C.Int} %Equal.sym(C.Int, C.Int.mul(C.Pos{k}, Int.sub_nat(p, m)), Int.sub_nat(Nat.mul(k, p), Nat.mul(k, m)), Int.mul_pos(k, p, m)) : {_ == Int.sub_nat(Nat.mul(p, k), Nat.mul(m, k)) : C.Int} %N.Nat.mul_comm(k, p) : {Int.sub_nat(Nat.mul(k, p), Nat.mul(k, m)) == Int.sub_nat(_, Nat.mul(m, k)) : C.Int} %N.Nat.mul_comm(k, m) : {Int.sub_nat(Nat.mul(k, p), Nat.mul(k, m)) == Int.sub_nat(Nat.mul(k, p), _) : C.Int} {==}def Int.le_mul.core(+pa: Nat, +ma: Nat, +pb: Nat, +mb: Nat, +k: Nat, h: N.Nat.Le(Nat.add(pa, mb), Nat.add(pb, ma))) -> C.Int.Le(C.Int.mul(Int.sub_nat(pa, ma), C.Pos{k}), C.Int.mul(Int.sub_nat(pb, mb), C.Pos{k})): %Equal.sym(C.Int, C.Int.mul(Int.sub_nat(pa, ma), C.Pos{k}), Int.sub_nat(Nat.mul(pa, k), Nat.mul(ma, k)), Int.mul_sub_r(pa, ma, k)) : C.Int.Le(_, C.Int.mul(Int.sub_nat(pb, mb), C.Pos{k})) %Equal.sym(C.Int, C.Int.mul(Int.sub_nat(pb, mb), C.Pos{k}), Int.sub_nat(Nat.mul(pb, k), Nat.mul(mb, k)), Int.mul_sub_r(pb, mb, k)) : C.Int.Le(Int.sub_nat(Nat.mul(pa, k), Nat.mul(ma, k)), _) Int.le_b(Nat.mul(pa, k), Nat.mul(ma, k), Nat.mul(pb, k), Nat.mul(mb, k), Int.le_cast_r(Nat.mul(Nat.add(pb, ma), k), Nat.add(Nat.mul(pb, k), Nat.mul(ma, k)), Nat.add(Nat.mul(pa, k), Nat.mul(mb, k)), N.Nat.add_mul(pb, ma, k), Int.le_cast(Nat.mul(Nat.add(pa, mb), k), Nat.add(Nat.mul(pa, k), Nat.mul(mb, k)), Nat.mul(Nat.add(pb, ma), k), N.Nat.add_mul(pa, mb, k), Int.le_mul_r(Nat.add(pa, mb), Nat.add(pb, ma), k, h))))def C.le_mul_nonneg(a, b, n, h): Int.by2(x => y => C.Int.Le(C.Int.mul(x, C.Pos{n}), C.Int.mul(y, C.Pos{n})), a, b, Int.le_mul.core(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), n, Int.le_f(Int.toP(a), Int.toM(a), Int.toP(b), Int.toM(b), Int.le_split(a, b, h))))# ---- the sign/magnitude view (what multiplication really is) ------------def Int.sgn(s: Bool, k: Nat) -> C.Int: match s: case True{}: C.Pos{k} case False{}: Int.neg_nat(k)def Int.sign(a: C.Int) -> Bool: match a: case C.Pos{n}: True{} case C.NegS{n}: False{}def Int.sgn_split(a: C.Int) -> {Int.sgn(Int.sign(a), C.Int.abs(a)) == a : C.Int}: match a: case C.Pos{n}: {==} case C.NegS{n}: {==}def Int.mul_pos_neg(+k: Nat, j: Nat) -> {C.Int.mul(C.Pos{k}, Int.neg_nat(j)) == Int.neg_nat(Nat.mul(k, j)) : C.Int}: match j: case 0n: %Equal.sym(Nat, Nat.mul(k, 0n), 0n, N.Nat.mul_zero(k)) : {C.Pos{_} == Int.neg_nat(_) : C.Int} {==} case 1n+jp: {==}def Int.mul_neg_pos(k: Nat, +j: Nat) -> {C.Int.mul(Int.neg_nat(k), C.Pos{j}) == Int.neg_nat(Nat.mul(k, j)) : C.Int}: match k: case 0n: {==} case 1n+kp: {==}def Int.mul_neg_neg(k: Nat, j: Nat) -> {C.Int.mul(Int.neg_nat(k), Int.neg_nat(j)) == C.Pos{Nat.mul(k, j)} : C.Int}: match k j: case 0n 0n: {==} case 0n 1n+jp: {==} case 1n+kp 0n: %Equal.sym(Nat, Nat.mul(1n+kp, 0n), 0n, N.Nat.mul_zero(1n+kp)) : {Int.neg_nat(_) == C.Pos{_} : C.Int} {==} case 1n+kp 1n+jp: {==}def Int.mul_sgn(s: Bool, t: Bool, +k: Nat, +j: Nat) -> {C.Int.mul(Int.sgn(s, k), Int.sgn(t, j)) == Int.sgn(N.Bool.same(s, t), Nat.mul(k, j)) : C.Int}: match s t: case True{} True{}: {==} case True{} False{}: Int.mul_pos_neg(k, j) case False{} True{}: Int.mul_neg_pos(k, j) case False{} False{}: Int.mul_neg_neg(k, j)def Int.same_assoc(a: Bool, b: Bool, c: Bool) -> {N.Bool.same(a, N.Bool.same(b, c)) == N.Bool.same(N.Bool.same(a, b), c) : Bool}: match a b c: case True{} True{} True{}: {==} case True{} True{} False{}: {==} case True{} False{} True{}: {==} case True{} False{} False{}: {==} case False{} True{} True{}: {==} case False{} True{} False{}: {==} case False{} False{} True{}: {==} case False{} False{} False{}: {==}def Int.sby3(-P: C.Int -> C.Int -> C.Int -> Type, +a: C.Int, +b: C.Int, +c: C.Int, w: P(Int.sgn(Int.sign(a), C.Int.abs(a)), Int.sgn(Int.sign(b), C.Int.abs(b)), Int.sgn(Int.sign(c), C.Int.abs(c)))) -> P(a, b, c): %Int.sgn_split(a) : P(_, b, c) %Int.sgn_split(b) : P(Int.sgn(Int.sign(a), C.Int.abs(a)), _, c) %Int.sgn_split(c) : P(Int.sgn(Int.sign(a), C.Int.abs(a)), Int.sgn(Int.sign(b), C.Int.abs(b)), _) wdef Int.mul_assoc.core(+sa: Bool, +ka: Nat, +sb: Bool, +kb: Nat, +sc: Bool, +kc: Nat) -> {C.Int.mul(Int.sgn(sa, ka), C.Int.mul(Int.sgn(sb, kb), Int.sgn(sc, kc))) == C.Int.mul(C.Int.mul(Int.sgn(sa, ka), Int.sgn(sb, kb)), Int.sgn(sc, kc)) : C.Int}: %Equal.sym(C.Int, C.Int.mul(Int.sgn(sb, kb), Int.sgn(sc, kc)), Int.sgn(N.Bool.same(sb, sc), Nat.mul(kb, kc)), Int.mul_sgn(sb, sc, kb, kc)) : {C.Int.mul(Int.sgn(sa, ka), _) == C.Int.mul(C.Int.mul(Int.sgn(sa, ka), Int.sgn(sb, kb)), Int.sgn(sc, kc)) : C.Int} %Equal.sym(C.Int, C.Int.mul(Int.sgn(sa, ka), Int.sgn(sb, kb)), Int.sgn(N.Bool.same(sa, sb), Nat.mul(ka, kb)), Int.mul_sgn(sa, sb, ka, kb)) : {C.Int.mul(Int.sgn(sa, ka), Int.sgn(N.Bool.same(sb, sc), Nat.mul(kb, kc))) == C.Int.mul(_, Int.sgn(sc, kc)) : C.Int} %Equal.sym(C.Int, C.Int.mul(Int.sgn(sa, ka), Int.sgn(N.Bool.same(sb, sc), Nat.mul(kb, kc))), Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), Nat.mul(ka, Nat.mul(kb, kc))), Int.mul_sgn(sa, N.Bool.same(sb, sc), ka, Nat.mul(kb, kc))) : {_ == C.Int.mul(Int.sgn(N.Bool.same(sa, sb), Nat.mul(ka, kb)), Int.sgn(sc, kc)) : C.Int} %Equal.sym(C.Int, C.Int.mul(Int.sgn(N.Bool.same(sa, sb), Nat.mul(ka, kb)), Int.sgn(sc, kc)), Int.sgn(N.Bool.same(N.Bool.same(sa, sb), sc), Nat.mul(Nat.mul(ka, kb), kc)), Int.mul_sgn(N.Bool.same(sa, sb), sc, Nat.mul(ka, kb), kc)) : {Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), Nat.mul(ka, Nat.mul(kb, kc))) == _ : C.Int} %Int.same_assoc(sa, sb, sc) : {Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), Nat.mul(ka, Nat.mul(kb, kc))) == Int.sgn(_, Nat.mul(Nat.mul(ka, kb), kc)) : C.Int} %N.Nat.mul_assoc(ka, kb, kc) : {Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), Nat.mul(ka, Nat.mul(kb, kc))) == Int.sgn(N.Bool.same(sa, N.Bool.same(sb, sc)), _) : C.Int} {==}def C.mul_assoc(a, b, c): Int.sby3(x => y => z => {C.Int.mul(x, C.Int.mul(y, z)) == C.Int.mul(C.Int.mul(x, y), z) : C.Int}, a, b, c, Int.mul_assoc.core(Int.sign(a), C.Int.abs(a), Int.sign(b), C.Int.abs(b), Int.sign(c), C.Int.abs(c)))# ---- no zero divisors ---------------------------------------------------def Int.abs_neg_nat(k: Nat) -> {C.Int.abs(Int.neg_nat(k)) == k : Nat}: match k: case 0n: {==} case 1n+kp: {==}def Int.abs_mul(a: C.Int, b: C.Int) -> {C.Int.abs(C.Int.mul(a, b)) == Nat.mul(C.Int.abs(a), C.Int.abs(b)) : Nat}: match a b: case C.Pos{x} C.Pos{y}: {==} case C.Pos{x} C.NegS{y}: Int.abs_neg_nat(Nat.mul(x, 1n+y)) case C.NegS{x} C.Pos{y}: Int.abs_neg_nat(Nat.mul(1n+x, y)) case C.NegS{x} C.NegS{y}: {==}def Int.abs_zero(a: C.Int, e: {C.Int.abs(a) == 0n : Nat}) -> {a == C.Pos{0n} : C.Int}: match a: case C.Pos{n}: %e : {C.Pos{n} == C.Pos{_} : C.Int} {==} case C.NegS{n}: Empty.absurd({C.NegS{n} == C.Pos{0n} : C.Int}, N.Nat.succ_neq_zero(n, e))def Int.mul_eq_zero_nat(x: Nat, +y: Nat, e: {Nat.mul(x, y) == 0n : Nat}, nx: {x == 0n : Nat} -> Empty) -> {y == 0n : Nat}: match x: case 0n: Empty.absurd({y == 0n : Nat}, nx({==})) case 1n+xp: N.Nat.add_eq_zero_l(y, Nat.mul(xp, y), e)def C.mul_eq_zero(a, b, e, na): Int.abs_zero(b, Int.mul_eq_zero_nat(C.Int.abs(a), C.Int.abs(b), Equal.trans(Nat, Nat.mul(C.Int.abs(a), C.Int.abs(b)), C.Int.abs(C.Int.mul(a, b)), 0n, Equal.sym(Nat, C.Int.abs(C.Int.mul(a, b)), Nat.mul(C.Int.abs(a), C.Int.abs(b)), Int.abs_mul(a, b)), Equal.cong(C.Int, Nat, z => C.Int.abs(z), C.Int.mul(a, b), C.Pos{0n}, e)), k => na(Int.abs_zero(a, k))))