def uniq

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32alg.bend:73

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

73# r1 + 2^n x == r2 + 2^n y with r1, r2 < 2^n forces r1 == r2.
74def uniq(+n: Nat, +r1: Nat, +r2: Nat, +x: Nat, +y: Nat, +h: {Nat.add(r1, sc(n, x)) == Nat.add(r2, sc(n, y)) : Nat}, +b1: {Nat.is_lt(r1, sc(n, 1n)) == True{} : Bool}, +b2: {Nat.is_lt(r2, sc(n, 1n)) == True{} : Bool}) -> {r1 == r2 : Nat}:
75  match x y:
76    case 0n 0n:
77      +h0 = L.subst(Nat, q => {Nat.add(r1, q) == Nat.add(r2, q) : Nat}, sc(n, 0n), 0n, sc_zero(n), h)
78      add_cancel_r(r1, r2, 0n, h0)
79    case 0n 1n+q:
80      Empty.absurd({r1 == r2 : Nat}, uniq_gap(n, r1, r2, q, h, b1))
81    case 1n+p 0n:
82      Empty.absurd({r1 == r2 : Nat}, uniq_gap(n, r2, r1, p, Equal.sym(Nat, Nat.add(r1, sc(n, 1n+p)), Nat.add(r2, sc(n, 0n)), h), b2))
83    case 1n+p 1n+q:
84      -Mn = sc(n, 1n)
85      +h1 = L.subst(Nat, z => {Nat.add(r1, z) == Nat.add(r2, sc(n, 1n+q)) : Nat}, sc(n, 1n+p), Nat.add(sc(n, 1n), sc(n, p)), sc_succ(n, p), h)
86      +h2 = L.subst(Nat, z => {Nat.add(r1, Nat.add(sc(n, 1n), sc(n, p))) == Nat.add(r2, z) : Nat}, sc(n, 1n+q), Nat.add(sc(n, 1n), sc(n, q)), sc_succ(n, q), h1)
87      +l1 = Equal.trans(Nat, Nat.add(Nat.add(r1, sc(n, p)), sc(n, 1n)), Nat.add(r1, Nat.add(sc(n, p), sc(n, 1n))), Nat.add(r1, Nat.add(sc(n, 1n), sc(n, p))), N.add_assoc(r1, sc(n, p), sc(n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(r1, z), Nat.add(sc(n, p), sc(n, 1n)), Nat.add(sc(n, 1n), sc(n, p)), N.add_comm(sc(n, p), sc(n, 1n))))
88      +l2 = Equal.trans(Nat, Nat.add(Nat.add(r2, sc(n, q)), sc(n, 1n)), Nat.add(r2, Nat.add(sc(n, q), sc(n, 1n))), Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), N.add_assoc(r2, sc(n, q), sc(n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(r2, z), Nat.add(sc(n, q), sc(n, 1n)), Nat.add(sc(n, 1n), sc(n, q)), N.add_comm(sc(n, q), sc(n, 1n))))
89      uniq(n, r1, r2, p, q, add_cancel_r(Nat.add(r1, sc(n, p)), Nat.add(r2, sc(n, q)), sc(n, 1n), Equal.trans(Nat, Nat.add(Nat.add(r1, sc(n, p)), sc(n, 1n)), Nat.add(r1, Nat.add(sc(n, 1n), sc(n, p))), Nat.add(Nat.add(r2, sc(n, q)), sc(n, 1n)), l1, Equal.trans(Nat, Nat.add(r1, Nat.add(sc(n, 1n), sc(n, p))), Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), Nat.add(Nat.add(r2, sc(n, q)), sc(n, 1n)), h2, Equal.sym(Nat, Nat.add(Nat.add(r2, sc(n, q)), sc(n, 1n)), Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), l2)))), b1, b2)