def qeq_f

bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:332

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/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

332def qeq_f(+k: Nat, +m: Nat, +x: Nat, +u: Nat, +c1: Bool, +hc1: {Nat.is_le(x, u) == c1 : Bool}, +hc2: {Nat.is_le(Nat.add(x, k), u) == False{} : Bool}) -> {SF.pick(Nat, c1, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))) == C.shift(Nat.sub(Nat.add(x, k), u), m) : Nat}:
333  match c1:
334    case True{}:
335      +t = Nat.sub(u, x)
336      +eu = N.sub_add(u, x, hc1)
337      +hlt0 = N.not_le_lt(Nat.add(x, k), u, hc2)
338      +hlt1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(x, k)) == True{} : Bool}, u, Nat.add(x, t), Equal.sym(Nat, Nat.add(x, t), u, eu), hlt0)
339      +hlt2 = Equal.trans(Bool, Nat.is_lt(t, k), Nat.is_lt(Nat.add(x, t), Nat.add(x, k)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(x, t), Nat.add(x, k)), Nat.is_lt(t, k), WW.lt_cancel_l(x, t, k)), hlt1)
340      +htk = N.lt_le(t, k, hlt2)
341      +es = NC.sh_split(k, t, m, htk)
342      +e1 = Equal.trans(Nat, SF.rne(C.shift(k, m), t), SF.rne(C.shift(t, C.shift(Nat.sub(k, t), m)), t), C.shift(Nat.sub(k, t), m), Equal.cong(Nat, Nat, z => SF.rne(z, t), C.shift(k, m), C.shift(t, C.shift(Nat.sub(k, t), m)), es), rne_exact(t, C.shift(Nat.sub(k, t), m)))
343      +e2 = Equal.trans(Nat, Nat.sub(k, t), Nat.sub(Nat.add(k, x), Nat.add(t, x)), Nat.sub(Nat.add(x, k), u), Equal.sym(Nat, Nat.sub(Nat.add(k, x), Nat.add(t, x)), Nat.sub(k, t), sub_cancel_r(k, t, x)), Equal.trans(Nat, Nat.sub(Nat.add(k, x), Nat.add(t, x)), Nat.sub(Nat.add(x, k), Nat.add(t, x)), Nat.sub(Nat.add(x, k), u), Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(t, x)), Nat.add(k, x), Nat.add(x, k), NA.add_comm(k, x)), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(x, k), z), Nat.add(t, x), u, Equal.trans(Nat, Nat.add(t, x), Nat.add(x, t), u, NA.add_comm(t, x), eu))))
344      Equal.trans(Nat, SF.rne(C.shift(k, m), t), C.shift(Nat.sub(k, t), m), C.shift(Nat.sub(Nat.add(x, k), u), m), e1, Equal.cong(Nat, Nat, z => C.shift(z, m), Nat.sub(k, t), Nat.sub(Nat.add(x, k), u), e2))
345    case False{}:
346      +hux = N.lt_le(u, x, N.not_le_lt(x, u, hc1))
347      Equal.trans(Nat, C.shift(Nat.sub(x, u), C.shift(k, m)), C.shift(Nat.add(Nat.sub(x, u), k), m), C.shift(Nat.sub(Nat.add(x, k), u), m), Equal.sym(Nat, C.shift(Nat.add(Nat.sub(x, u), k), m), C.shift(Nat.sub(x, u), C.shift(k, m)), WW.shift_comp(Nat.sub(x, u), k, m)), Equal.cong(Nat, Nat, z => C.shift(z, m), Nat.add(Nat.sub(x, u), k), Nat.sub(Nat.add(x, k), u), Equal.sym(Nat, Nat.sub(Nat.add(x, k), u), Nat.add(Nat.sub(x, u), k), sub_add_r(x, k, u, hux))))