def qeq_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rtools.bend:113

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/math/typed/f64round.bend as FR

113def qeq_c(+k: Nat, +m: Nat, +x: Nat, +u: Nat, +c1: Bool, +hc1: {Nat.is_le(x, u) == c1 : Bool}, +c2: Bool, +hc2: {Nat.is_le(Nat.add(x, k), u) == c2 : 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))) == SF.pick(Nat, c2, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)) : Nat}:
114  match c2:
115    case True{}:
116      +h1 = N.le_trans(x, Nat.add(x, k), u, N.le_add_right(x, k), hc2)
117      +ec1 = Equal.trans(Bool, c1, Nat.is_le(x, u), True{}, Equal.sym(Bool, Nat.is_le(x, u), c1, hc1), h1)
118      +r = Nat.sub(u, Nat.add(x, k))
119      +base = Equal.trans(Nat, SF.rne(C.shift(k, m), Nat.sub(u, x)), SF.rne(C.shift(k, m), Nat.add(r, k)), SF.rne(m, r), Equal.cong(Nat, Nat, z => SF.rne(C.shift(k, m), z), Nat.sub(u, x), Nat.add(r, k), a1(x, k, u, hc2)), rne_shift(k, m, r))
120      Equal.trans(Nat, SF.pick(Nat, c1, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))), SF.rne(m, Nat.sub(u, Nat.add(x, k))), SF.pick(Nat, True{}, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)), L.subst(Bool, t => {SF.pick(Nat, t, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))) == SF.rne(m, r) : Nat}, True{}, c1, Equal.sym(Bool, c1, True{}, ec1), base), Equal.sym(Nat, SF.pick(Nat, True{}, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)), SF.rne(m, Nat.sub(u, Nat.add(x, k))), FR.pk_t(Nat, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m))))
121    case False{}:
122      Equal.trans(Nat, 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), SF.pick(Nat, False{}, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)), qeq_f(k, m, x, u, c1, hc1, hc2), Equal.sym(Nat, SF.pick(Nat, False{}, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)), C.shift(Nat.sub(Nat.add(x, k), u), m), FR.pk_f(Nat, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m))))