proofs/math/typed/shrn.bend
bend-collections-laws-math@1.0.0.0 · 157 lines · 12 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/src/math/w64.bend as X
4import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
7import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
8import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
10import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
11import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32P
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
14
15
16
17
18
19
20
21def v(+x: U32) -> Nat:
22 U32.to_nat(x)
23
24
25def hlf_half(+n: Nat) -> {UH.hlf(n) == C.half(n) : Nat}:
26 match n:
27 case 0n:
28 {==}
29 case 1n:
30 {==}
31 case 2n+q:
32 Equal.cong(Nat, Nat, z => 1n+z, UH.hlf(q), C.half(q), hlf_half(q))
33
34
35def high_half(+p: Nat, +n: Nat) -> {C.high(p, C.half(n)) == C.half(C.high(p, n)) : Nat}:
36 match p:
37 case 0n:
38 {==}
39 case 1n+q:
40 high_half(q, C.half(n))
41
42
43def shrn_high(+x: U32, +k: Nat) -> {v(U32.shrn(x, k)) == C.high(k, v(x)) : Nat}:
44 match k:
45 case 0n:
46 {==}
47 case 1n+p:
48 +e1 = Equal.trans(Nat, v(U32.shr(U32.shrn(x, p))), UH.hlf(v(U32.shrn(x, p))), C.half(v(U32.shrn(x, p))), UH.shr_value(U32.shrn(x, p)), hlf_half(v(U32.shrn(x, p))))
49 +e2 = Equal.cong(Nat, Nat, z => C.half(z), v(U32.shrn(x, p)), C.high(p, v(x)), shrn_high(x, p))
50 Equal.trans(Nat, v(U32.shr(U32.shrn(x, p))), C.half(C.high(p, v(x))), C.high(1n+p, v(x)), Equal.trans(Nat, v(U32.shr(U32.shrn(x, p))), C.half(v(U32.shrn(x, p))), C.half(C.high(p, v(x))), e1, e2), Equal.sym(Nat, C.high(1n+p, v(x)), C.half(C.high(p, v(x))), high_half(p, v(x))))
51
52
53def p2w(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {X.pow2(k) == U32{WD.pw(32n, k)} : U32}:
54 match k:
55 case 0n:
56 {==}
57 case 1n:
58 {==}
59 case 2n:
60 {==}
61 case 3n:
62 {==}
63 case 4n:
64 {==}
65 case 5n:
66 {==}
67 case 6n:
68 {==}
69 case 7n:
70 {==}
71 case 8n:
72 {==}
73 case 9n:
74 {==}
75 case 10n:
76 {==}
77 case 11n:
78 {==}
79 case 12n:
80 {==}
81 case 13n:
82 {==}
83 case 14n:
84 {==}
85 case 15n:
86 {==}
87 case 16n:
88 {==}
89 case 17n:
90 {==}
91 case 18n:
92 {==}
93 case 19n:
94 {==}
95 case 20n:
96 {==}
97 case 21n:
98 {==}
99 case 22n:
100 {==}
101 case 23n:
102 {==}
103 case 24n:
104 {==}
105 case 25n:
106 {==}
107 case 26n:
108 {==}
109 case 27n:
110 {==}
111 case 28n:
112 {==}
113 case 29n:
114 {==}
115 case 30n:
116 {==}
117 case 31n:
118 {==}
119 case 32n+j:
120 Empty.absurd({X.pow2(32n+j) == U32{WD.pw(32n, 32n+j)} : U32}, N.lt_zero_absurd(j, hk))
121def p2v(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {v(X.pow2(k)) == C.pow2(k) : Nat}:
122 Equal.trans(Nat, v(X.pow2(k)), WD.sc(k, 1n), C.pow2(k), PD.pow32(k, hk, 1n, {==}, X.pow2(k), p2w(k, hk)), Equal.sym(Nat, C.pow2(k), WD.sc(k, 1n), U.pow2_scale(k)))
123
124def pow2_eq(+k: Nat) -> {C.pow2(k) == 1n+Nat.sub(C.pow2(k), 1n) : Nat}:
125 Equal.sym(Nat, 1n+Nat.sub(C.pow2(k), 1n), C.pow2(k), N.sub_add(C.pow2(k), 1n, N.pow2_pos(k)))
126
127def is_zero_c(+a: U32, +c: Bool, +hc: {U32.is_zero(a) == c : Bool}, +n: Nat, +hn: {v(a) == n : Nat}) -> {c == Nat.is_eq(v(a), 0n) : Bool}:
128 match c:
129 case True{}:
130 %Equal.sym(U32, a, 0, A.eq_of(a, 0, hc)) : {True{} == Nat.is_eq(v(_), 0n) : Bool}
131 {==}
132 case False{}:
133 match n:
134 case 0n:
135 +hz = L.subst(U32, z => {U32.is_zero(z) == True{} : Bool}, 0, a, Equal.sym(U32, a, 0, U.injective(a, 0, hn)), {==})
136 Empty.absurd({False{} == Nat.is_eq(v(a), 0n) : Bool}, U32P.true_ne_false(Equal.trans(Bool, True{}, U32.is_zero(a), False{}, Equal.sym(Bool, U32.is_zero(a), True{}, hz), hc)))
137 case 1n+ +p:
138 %Equal.sym(Nat, v(a), 1n+p, hn) : {False{} == Nat.is_eq(_, 0n) : Bool}
139 {==}
140
141def zero_nat(+a: U32) -> {U32.is_zero(a) == Nat.is_eq(v(a), 0n) : Bool}:
142 is_zero_c(a, U32.is_zero(a), {==}, v(a), {==})
143
144
145def div_p2(+x: U32, +k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {v(U32.div(x, X.pow2(k))) == C.high(k, v(x)) : Nat}:
146 +pp = Nat.sub(C.pow2(k), 1n)
147 +ev = Equal.trans(Nat, v(X.pow2(k)), C.pow2(k), 1n+pp, p2v(k, hk), pow2_eq(k))
148 +nz = Equal.trans(Bool, U32.is_zero(X.pow2(k)), Nat.is_eq(v(X.pow2(k)), 0n), False{}, zero_nat(X.pow2(k)), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(X.pow2(k)), 1n+pp, ev))
149 Equal.trans(Nat, v(U32.div(x, X.pow2(k))), Nat.div(v(x), v(X.pow2(k))), C.high(k, v(x)), UD.div_nat(x, X.pow2(k), nz), Equal.trans(Nat, Nat.div(v(x), v(X.pow2(k))), Nat.div(v(x), 1n+pp), C.high(k, v(x)), Equal.cong(Nat, Nat, t => Nat.div(v(x), t), v(X.pow2(k)), 1n+pp, ev), Equal.sym(Nat, C.high(k, v(x)), Nat.div(v(x), 1n+pp), WW.high_div(k, v(x), pp, pow2_eq(k)))))
150
151
152def shrn_div(+x: U32, +k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {U32.shrn(x, k) == U32.div(x, X.pow2(k)) : U32}:
153 U.injective(U32.shrn(x, k), U32.div(x, X.pow2(k)), Equal.trans(Nat, v(U32.shrn(x, k)), C.high(k, v(x)), v(U32.div(x, X.pow2(k))), shrn_high(x, k), Equal.sym(Nat, v(U32.div(x, X.pow2(k))), C.high(k, v(x)), div_p2(x, k, hk))))
154
155
156def shr16(+x: U32) -> {U32.shrn(x, 16n) == U32.div(x, 65536) : U32}:
157 shrn_div(x, 16n, {==})