proofs/math/typed/f64bl.bend
bend-collections-laws-math@1.0.0.0 · 88 lines · 9 definitions
1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
5import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
6import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
7import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
10import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as BT
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
16
17
18
19def v(+x: U32) -> Nat:
20 U32.to_nat(x)
21
22def lbits(+k: Nat, +n: Nat) -> {F.low_bits(k, n) == C.low(k, n) : Nat}:
23 match k:
24 case 0n:
25 {==}
26 case 1n+ +p:
27 +e1 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(F.low_bits(p, Nat.div(n, 2n)))), Nat.mod(n, 2n), C.bit(n), Equal.sym(Nat, C.bit(n), Nat.mod(n, 2n), WW.bit_mod(n)))
28 +e2 = Equal.cong(Nat, Nat, z => Nat.add(C.bit(n), Nat.double(F.low_bits(p, z))), Nat.div(n, 2n), C.half(n), Equal.sym(Nat, C.half(n), Nat.div(n, 2n), WA.half_div(n)))
29 +e3 = Equal.cong(Nat, Nat, z => Nat.add(C.bit(n), Nat.double(z)), F.low_bits(p, C.half(n)), C.low(p, C.half(n)), lbits(p, C.half(n)))
30 Equal.trans(Nat, Nat.add(Nat.mod(n, 2n), Nat.double(F.low_bits(p, Nat.div(n, 2n)))), Nat.add(C.bit(n), Nat.double(F.low_bits(p, Nat.div(n, 2n)))), Nat.add(C.bit(n), Nat.double(C.low(p, C.half(n)))), e1, Equal.trans(Nat, Nat.add(C.bit(n), Nat.double(F.low_bits(p, Nat.div(n, 2n)))), Nat.add(C.bit(n), Nat.double(F.low_bits(p, C.half(n)))), Nat.add(C.bit(n), Nat.double(C.low(p, C.half(n)))), e2, e3))
31
32def hbits(+k: Nat, +n: Nat) -> {F.high_bits(k, n) == C.high(k, n) : Nat}:
33 match k:
34 case 0n:
35 {==}
36 case 1n+ +p:
37 Equal.trans(Nat, F.high_bits(p, Nat.div(n, 2n)), F.high_bits(p, C.half(n)), C.high(p, C.half(n)), Equal.cong(Nat, Nat, z => F.high_bits(p, z), Nat.div(n, 2n), C.half(n), Equal.sym(Nat, C.half(n), Nat.div(n, 2n), WA.half_div(n))), hbits(p, C.half(n)))
38
39def wval(+n: Nat, +h64: {C.fits(64n, n) == True{} : Bool}) -> {SW.value(WU.U64{U32.from_nat(F.low_bits(32n, n)), U32.from_nat(F.high_bits(32n, n))}) == n : Nat}:
40 +el = Equal.trans(Nat, v(U32.from_nat(F.low_bits(32n, n))), v(U32.from_nat(C.low(32n, n))), C.low(32n, n), Equal.cong(Nat, Nat, z => v(U32.from_nat(z)), F.low_bits(32n, n), C.low(32n, n), lbits(32n, n)), LW.vo(C.low(32n, n), WW.low_fits(32n, n)))
41 +eh = Equal.trans(Nat, v(U32.from_nat(F.high_bits(32n, n))), v(U32.from_nat(C.high(32n, n))), C.high(32n, n), Equal.cong(Nat, Nat, z => v(U32.from_nat(z)), F.high_bits(32n, n), C.high(32n, n), hbits(32n, n)), LW.vo(C.high(32n, n), SH.fits_high(32n, 32n, n, h64)))
42 Equal.trans(Nat, Nat.add(v(U32.from_nat(F.low_bits(32n, n))), C.shift(32n, v(U32.from_nat(F.high_bits(32n, n))))), Nat.add(C.low(32n, n), C.shift(32n, v(U32.from_nat(F.high_bits(32n, n))))), n, Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, v(U32.from_nat(F.high_bits(32n, n))))), v(U32.from_nat(F.low_bits(32n, n))), C.low(32n, n), el), Equal.trans(Nat, Nat.add(C.low(32n, n), C.shift(32n, v(U32.from_nat(F.high_bits(32n, n))))), Nat.add(C.low(32n, n), C.shift(32n, C.high(32n, n))), n, Equal.cong(Nat, Nat, z => Nat.add(C.low(32n, n), C.shift(32n, z)), v(U32.from_nat(F.high_bits(32n, n))), C.high(32n, n), eh), Equal.sym(Nat, n, Nat.add(C.low(32n, n), C.shift(32n, C.high(32n, n))), WW.low_high(32n, n))))
43
44
45
46def bl_le_n(+K: Nat, +n: Nat, +hn: {C.fits(K, n) == True{} : Bool}, +hp: {Nat.is_le(C.pow2(1n+K), C.pow2(M.bit_length(n))) == True{} : Bool}) -> {False{} == True{} : Bool}:
47 match n:
48 case 0n:
49 +h0 = BT.bit_length_zero()
50 +hp2 = L.subst(Nat, z => {Nat.is_le(C.pow2(1n+K), C.pow2(z)) == True{} : Bool}, M.bit_length(0n), 0n, h0, hp)
51 Equal.trans(Bool, False{}, Nat.is_le(C.pow2(1n+K), 1n), True{}, Equal.sym(Bool, Nat.is_le(C.pow2(1n+K), 1n), False{}, N.lt_not_le(1n, C.pow2(1n+K), N.le_lt_trans(1n, C.pow2(K), C.pow2(1n+K), N.pow2_pos(K), N.pow2_lt_succ(K)))), hp2)
52 case 1n+ +np:
53 +hd = N.double_lt(1n+np, C.pow2(K), WW.lt_of_fits(K, 1n+np, hn))
54 +P = C.pow2(1n+K)
55 Equal.trans(Bool, False{}, Nat.is_lt(P, P), True{}, Equal.sym(Bool, Nat.is_lt(P, P), False{}, N.lt_irrefl(P)), N.le_lt_trans(P, Nat.double(1n+np), P, N.le_trans(P, C.pow2(M.bit_length(1n+np)), Nat.double(1n+np), hp, BT.bit_length_le(np)), hd))
56
57def bl_le(+K: Nat, +n: Nat, +hn: {C.fits(K, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(M.bit_length(n), K) == c : Bool}) -> {c == True{} : Bool}:
58 match c:
59 case True{}:
60 {==}
61 case False{}:
62 +hk = N.lt_succ_le_succ(K, M.bit_length(n), N.not_le_lt(M.bit_length(n), K, hc))
63 +hp = N.pow2_mono(1n+K, M.bit_length(n), hk)
64 bl_le_n(K, n, hn, hp)
65
66
67def bl_pos(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}, +c: Nat, +hc: {M.bit_length(n) == c : Nat}) -> {Nat.is_le(1n, c) == True{} : Bool}:
68 match c:
69 case 0n:
70 +h0 = L.subst(Nat, z => {Nat.is_lt(n, C.pow2(z)) == True{} : Bool}, M.bit_length(n), 0n, hc, BT.bit_length_lt(n))
71 +e0 = U.lt_one_zero(n, h0)
72 Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, LW.true_ne_false(Equal.trans(Bool, True{}, Nat.is_eq(n, 0n), False{}, Equal.sym(Bool, Nat.is_eq(n, 0n), True{}, L.subst(Nat, z => {Nat.is_eq(z, 0n) == True{} : Bool}, 0n, n, Equal.sym(Nat, n, 0n, e0), {==})), hz)))
73 case 1n+ +cp:
74 N.zero_le(cp)
75
76def dle(+a: Nat, +c: Nat, +h: {Nat.is_le(Nat.double(a), Nat.double(c)) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
77 Equal.trans(Bool, Nat.is_le(a, c), Nat.is_le(Nat.double(a), Nat.double(c)), True{}, Equal.cong(Cmp, Bool, t => Cmp.is_le(t), Nat.cmp(a, c), Nat.cmp(Nat.double(a), Nat.double(c)), Equal.sym(Cmp, Nat.cmp(Nat.double(a), Nat.double(c)), Nat.cmp(a, c), NC.cmp_dbl(a, c))), h)
78
79def lower(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {Nat.is_le(C.pow2(Nat.sub(M.bit_length(n), 1n)), n) == True{} : Bool}:
80 match n:
81 case 0n:
82 Empty.absurd({Nat.is_le(C.pow2(Nat.sub(M.bit_length(0n), 1n)), 0n) == True{} : Bool}, LW.true_ne_false(hz))
83 case 1n+ +np:
84 +B = M.bit_length(1n+np)
85 +eb = N.sub_add(B, 1n, bl_pos(1n+np, hz, B, {==}))
86 +h1 = L.subst(Nat, z => {Nat.is_le(C.pow2(z), Nat.double(1n+np)) == True{} : Bool}, B, 1n+Nat.sub(B, 1n), Equal.sym(Nat, 1n+Nat.sub(B, 1n), B, eb), BT.bit_length_le(np))
87 dle(C.pow2(Nat.sub(B, 1n)), 1n+np, h1)
88