def afin

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addf.bend:231

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

231# F.add on finite operands is the spec's add_fin
232def afin(+xl: U32, +xh: U32, +yl: U32, +yh: U32, +ha: {Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n) == True{} : Bool}, +hb: {Nat.is_lt(SF.efield(F.Bits{yl, yh}), 2047n) == True{} : Bool}) -> {F.add(F.Bits{xl, xh}, F.Bits{yl, yh}) == SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}) : F.F64}:
233  +e0 = ap(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.not(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))))
234  +c1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(t, F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, t, F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, t, F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), F.signbit(F.Bits{xl, xh}), SF.sign(F.Bits{xl, xh}), FB.signbit_value(F.Bits{xl, xh}))
235  +c2 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), t)), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), F.signbit(F.Bits{yl, yh}), SF.sign(F.Bits{yl, yh}), FB.signbit_value(F.Bits{yl, yh}))
236  +c3 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, F.exp_field(F.Bits{yl, yh}), Nat.cmp(t, F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, F.exp_field(F.Bits{yl, yh}), Nat.cmp(t, F.exp_field(F.Bits{yl, yh})))), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), hea(xl, xh))
237  +c4 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), t, Nat.cmp(SF.efield(F.Bits{xl, xh}), t)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), t, Nat.cmp(SF.efield(F.Bits{xl, xh}), t))), F.exp_field(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), hea(yl, yh))
238  +r = core_c(1n, {==}, F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), SF.frac(F.Bits{xl, xh}), SF.frac(F.Bits{yl, yh}), hfr(xl, xh), hfr(yl, yh), hF(xl, xh), hF(yl, yh), ha, hb, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), {==}, Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})), {==})
239  Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.pick(F.F64, Bool.not(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), e0, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), c1, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), c2, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), c3, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), c4, r)))))