def cl_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natcmp.bend:102

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/math/typed/width.bend as WW

102# two limbs compare lexicographically
103def cl_c(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}, +c: Cmp, +hc: {Nat.cmp(y1, y2) == c : Cmp}) -> {Nat.cmp(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == lex(c, Nat.cmp(x1, x2)) : Cmp}:
104  match c:
105    case LT{}:
106      cmp_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), WW.lt_hi(k, x1, y1, x2, y2, hx1, lt_of_cmp(y1, y2, hc)))
107    case GT{}:
108      cmp_gt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), WW.lt_hi(k, x2, y2, x1, y1, hx2, lt_of_gt(y1, y2, hc)))
109    case EQ{}:
110      L.subst(Nat, z => {Nat.cmp(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, z))) == Nat.cmp(x1, x2) : Cmp}, y1, y2, eq_of_cmp(y1, y2, hc), cmp_addr(x1, x2, C.shift(k, y1)))