def p2w

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/shrn.bend:52

import Base
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
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/word.bend as WD

52# the 2^k table is the word with bit k set
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))