proofs/containers/bitset/lists.bend
bend-collections-laws-containers@1.0.0.0 · 413 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
8
9# Boolean-sequence facts used by the bitset proof: element-wise combination
10# (zipk, indexed by the implementation's word-operation tag), all-False
11# tails, counting and member enumeration over take/drop/append.
12
13def bop(k: B.WordOp, a: Bool, b: Bool) -> Bool:
14 match k:
15 case B.KOr{}:
16 Bool.or(a, b)
17 case B.KAnd{}:
18 Bool.and(a, b)
19 case B.KDiff{}:
20 Bool.and(a, Bool.not(b))
21 case B.KXor{}:
22 Bool.xor(a, b)
23
24def zipk(+k: B.WordOp, xs: List<&2, Bool>, ys: List<&2, Bool>) -> List<&2, Bool>:
25 match xs ys:
26 case Nil{} _:
27 Nil{}
28 case Con{a, s} Nil{}:
29 Nil{}
30 case Con{a, s} Con{b, t}:
31 Con{bop(k, a, b), zipk(k, s, t)}
32
33def allf(xs: List<&2, Bool>) -> Bool:
34 match xs:
35 case Nil{}:
36 True{}
37 case Con{False{}, t}:
38 allf(t)
39 case Con{True{}, t}:
40 False{}
41
42def rep(n: Nat) -> List<&2, Bool>:
43 SC.replicate(Bool, n, False{})
44
45# ---- spec combinators are zipk instances ----
46
47def spec_or(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.zip_or(xs, ys) == zipk(B.KOr{}, xs, ys) : List<&2, Bool>}:
48 match xs ys:
49 case Nil{} Nil{}:
50 {==}
51 case Nil{} Con{b, t}:
52 {==}
53 case Con{a, s} Nil{}:
54 {==}
55 case Con{a, s} Con{b, t}:
56 LL.cons_cong(Bool, Bool.or(a, b), S.zip_or(s, t), zipk(B.KOr{}, s, t), spec_or(s, t))
57
58def spec_and(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.zip_and(xs, ys) == zipk(B.KAnd{}, xs, ys) : List<&2, Bool>}:
59 match xs ys:
60 case Nil{} Nil{}:
61 {==}
62 case Nil{} Con{b, t}:
63 {==}
64 case Con{a, s} Nil{}:
65 {==}
66 case Con{a, s} Con{b, t}:
67 LL.cons_cong(Bool, Bool.and(a, b), S.zip_and(s, t), zipk(B.KAnd{}, s, t), spec_and(s, t))
68
69def spec_diff(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.zip_diff(xs, ys) == zipk(B.KDiff{}, xs, ys) : List<&2, Bool>}:
70 match xs ys:
71 case Nil{} Nil{}:
72 {==}
73 case Nil{} Con{b, t}:
74 {==}
75 case Con{a, s} Nil{}:
76 {==}
77 case Con{a, s} Con{b, t}:
78 LL.cons_cong(Bool, Bool.and(a, Bool.not(b)), S.zip_diff(s, t), zipk(B.KDiff{}, s, t), spec_diff(s, t))
79
80def spec_xor(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.zip_xor(xs, ys) == zipk(B.KXor{}, xs, ys) : List<&2, Bool>}:
81 match xs ys:
82 case Nil{} Nil{}:
83 {==}
84 case Nil{} Con{b, t}:
85 {==}
86 case Con{a, s} Nil{}:
87 {==}
88 case Con{a, s} Con{b, t}:
89 LL.cons_cong(Bool, Bool.xor(a, b), S.zip_xor(s, t), zipk(B.KXor{}, s, t), spec_xor(s, t))
90
91# ---- zipk structure ----
92
93def zipk_nil_r(+k: B.WordOp, +xs: List<&2, Bool>) -> {zipk(k, xs, Nil{}) == Nil{} : List<&2, Bool>}:
94 match xs:
95 case Nil{}:
96 {==}
97 case Con{a, s}:
98 {==}
99
100def zipk_append(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +xs2: List<&2, Bool>, +ys2: List<&2, Bool>, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {zipk(k, SC.append(Bool, xs, xs2), SC.append(Bool, ys, ys2)) == SC.append(Bool, zipk(k, xs, ys), zipk(k, xs2, ys2)) : List<&2, Bool>}:
101 match xs ys:
102 case Nil{} Nil{}:
103 {==}
104 case Nil{} Con{b, t}:
105 Empty.absurd({zipk(k, xs2, SC.append(Bool, Con{b, t}, ys2)) == zipk(k, xs2, ys2) : List<&2, Bool>}, N.zero_succ(SC.length(Bool, t), h))
106 case Con{a, s} Nil{}:
107 Empty.absurd({zipk(k, SC.append(Bool, Con{a, s}, xs2), ys2) == SC.append(Bool, zipk(k, Con{a, s}, Nil{}), zipk(k, xs2, ys2)) : List<&2, Bool>}, N.succ_zero(SC.length(Bool, s), h))
108 case Con{a, s} Con{b, t}:
109 LL.cons_cong(Bool, bop(k, a, b), zipk(k, SC.append(Bool, s, xs2), SC.append(Bool, t, ys2)), SC.append(Bool, zipk(k, s, t), zipk(k, xs2, ys2)), zipk_append(k, s, t, xs2, ys2, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h)))
110
111def take_zipk(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +n: Nat) -> {SC.take(Bool, zipk(k, xs, ys), n) == zipk(k, SC.take(Bool, xs, n), SC.take(Bool, ys, n)) : List<&2, Bool>}:
112 match xs ys n:
113 case Nil{} _ _:
114 {==}
115 case Con{a, s} Nil{} _:
116 Equal.sym(List<&2, Bool>, zipk(k, SC.take(Bool, Con{a, s}, n), Nil{}), Nil{}, zipk_nil_r(k, SC.take(Bool, Con{a, s}, n)))
117 case Con{a, s} Con{b, t} 0n:
118 {==}
119 case Con{a, s} Con{b, t} 1n+m:
120 LL.cons_cong(Bool, bop(k, a, b), SC.take(Bool, zipk(k, s, t), m), zipk(k, SC.take(Bool, s, m), SC.take(Bool, t, m)), take_zipk(k, s, t, m))
121
122def drop_zipk(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +n: Nat) -> {SC.drop(Bool, zipk(k, xs, ys), n) == zipk(k, SC.drop(Bool, xs, n), SC.drop(Bool, ys, n)) : List<&2, Bool>}:
123 match xs ys n:
124 case Nil{} _ _:
125 {==}
126 case Con{a, s} Nil{} _:
127 Equal.sym(List<&2, Bool>, zipk(k, SC.drop(Bool, Con{a, s}, n), Nil{}), Nil{}, zipk_nil_r(k, SC.drop(Bool, Con{a, s}, n)))
128 case Con{a, s} Con{b, t} 0n:
129 {==}
130 case Con{a, s} Con{b, t} 1n+m:
131 drop_zipk(k, s, t, m)
132
133def bop_ff(+k: B.WordOp) -> {bop(k, False{}, False{}) == False{} : Bool}:
134 match k:
135 case B.KOr{}:
136 {==}
137 case B.KAnd{}:
138 {==}
139 case B.KDiff{}:
140 {==}
141 case B.KXor{}:
142 {==}
143
144def allf_zipk(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +hx: {allf(xs) == True{} : Bool}, +hy: {allf(ys) == True{} : Bool}) -> {allf(zipk(k, xs, ys)) == True{} : Bool}:
145 match xs ys:
146 case Nil{} _:
147 {==}
148 case Con{a, s} Nil{}:
149 {==}
150 case Con{True{}, s} Con{b, t}:
151 Empty.absurd({allf(zipk(k, Con{True{}, s}, Con{b, t})) == True{} : Bool}, L.false_true(hx))
152 case Con{False{}, s} Con{True{}, t}:
153 Empty.absurd({allf(zipk(k, Con{False{}, s}, Con{True{}, t})) == True{} : Bool}, L.false_true(hy))
154 case Con{False{}, s} Con{False{}, t}:
155 %Equal.sym(Bool, bop(k, False{}, False{}), False{}, bop_ff(k)) : {allf(Con{_, zipk(k, s, t)}) == True{} : Bool}
156 allf_zipk(k, s, t, hx, hy)
157
158def length_zipk_le(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {Nat.is_le(SC.length(Bool, zipk(k, xs, ys)), SC.length(Bool, xs)) == True{} : Bool}:
159 match xs ys:
160 case Nil{} _:
161 {==}
162 case Con{a, s} Nil{}:
163 {==}
164 case Con{a, s} Con{b, t}:
165 length_zipk_le(k, s, t)
166
167def le_length_zipk(+k: B.WordOp, +n: Nat, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +hx: {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}, +hy: {Nat.is_le(n, SC.length(Bool, ys)) == True{} : Bool}) -> {Nat.is_le(n, SC.length(Bool, zipk(k, xs, ys))) == True{} : Bool}:
168 match n xs ys:
169 case 0n _ _:
170 N.zero_le(SC.length(Bool, zipk(k, xs, ys)))
171 case 1n+m Nil{} _:
172 Empty.absurd({Nat.is_le(1n+m, SC.length(Bool, zipk(k, Nil{}, ys))) == True{} : Bool}, L.false_true(hx))
173 case 1n+m Con{a, s} Nil{}:
174 Empty.absurd({Nat.is_le(1n+m, SC.length(Bool, zipk(k, Con{a, s}, Nil{}))) == True{} : Bool}, L.false_true(hy))
175 case 1n+m Con{a, s} Con{b, t}:
176 le_length_zipk(k, m, s, t, hx, hy)
177
178# ---- all-False sequences ----
179
180def allf_append(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +hx: {allf(xs) == True{} : Bool}, +hy: {allf(ys) == True{} : Bool}) -> {allf(SC.append(Bool, xs, ys)) == True{} : Bool}:
181 match xs:
182 case Nil{}:
183 hy
184 case Con{False{}, t}:
185 allf_append(t, ys, hx, hy)
186 case Con{True{}, t}:
187 Empty.absurd({allf(SC.append(Bool, Con{True{}, t}, ys)) == True{} : Bool}, L.false_true(hx))
188
189def allf_rep(+n: Nat) -> {allf(rep(n)) == True{} : Bool}:
190 match n:
191 case 0n:
192 {==}
193 case 1n+m:
194 allf_rep(m)
195
196def drop_allf(+xs: List<&2, Bool>, +n: Nat, +h: {allf(xs) == True{} : Bool}) -> {allf(SC.drop(Bool, xs, n)) == True{} : Bool}:
197 match xs n:
198 case Nil{} _:
199 {==}
200 case Con{a, t} 0n:
201 h
202 case Con{False{}, t} 1n+m:
203 drop_allf(t, m, h)
204 case Con{True{}, t} 1n+m:
205 Empty.absurd({allf(SC.drop(Bool, Con{True{}, t}, 1n+m)) == True{} : Bool}, L.false_true(h))
206
207def take_allf(+xs: List<&2, Bool>, +n: Nat, +h: {allf(xs) == True{} : Bool}, +hn: {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}) -> {SC.take(Bool, xs, n) == rep(n) : List<&2, Bool>}:
208 match xs n:
209 case Nil{} 0n:
210 {==}
211 case Nil{} 1n+m:
212 Empty.absurd({SC.take(Bool, Nil{}, 1n+m) == rep(1n+m) : List<&2, Bool>}, L.false_true(hn))
213 case Con{a, t} 0n:
214 {==}
215 case Con{False{}, t} 1n+m:
216 LL.cons_cong(Bool, False{}, SC.take(Bool, t, m), rep(m), take_allf(t, m, h, hn))
217 case Con{True{}, t} 1n+m:
218 Empty.absurd({SC.take(Bool, Con{True{}, t}, 1n+m) == rep(1n+m) : List<&2, Bool>}, L.false_true(h))
219
220def count_allf(+xs: List<&2, Bool>, +h: {allf(xs) == True{} : Bool}) -> {S.count(xs) == 0n : Nat}:
221 match xs:
222 case Nil{}:
223 {==}
224 case Con{False{}, t}:
225 count_allf(t, h)
226 case Con{True{}, t}:
227 Empty.absurd({S.count(Con{True{}, t}) == 0n : Nat}, L.false_true(h))
228
229def members_allf(+xs: List<&2, Bool>, +off: Nat, +h: {allf(xs) == True{} : Bool}) -> {S.members(xs, off) == Nil{} : List<&2, Nat>}:
230 match xs:
231 case Nil{}:
232 {==}
233 case Con{False{}, t}:
234 members_allf(t, 1n+off, h)
235 case Con{True{}, t}:
236 Empty.absurd({S.members(Con{True{}, t}, off) == Nil{} : List<&2, Nat>}, L.false_true(h))
237
238# ---- count / members over append, take ----
239
240def count_append(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.count(SC.append(Bool, xs, ys)) == Nat.add(S.count(xs), S.count(ys)) : Nat}:
241 match xs:
242 case Nil{}:
243 {==}
244 case Con{False{}, t}:
245 count_append(t, ys)
246 case Con{True{}, t}:
247 N.succ_cong(S.count(SC.append(Bool, t, ys)), Nat.add(S.count(t), S.count(ys)), count_append(t, ys))
248
249def members_append(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +off: Nat) -> {S.members(SC.append(Bool, xs, ys), off) == SC.append(Nat, S.members(xs, off), S.members(ys, Nat.add(SC.length(Bool, xs), off))) : List<&2, Nat>}:
250 match xs:
251 case Nil{}:
252 {==}
253 case Con{False{}, t}:
254 %N.add_succ(SC.length(Bool, t), off) : {S.members(SC.append(Bool, t, ys), 1n+off) == SC.append(Nat, S.members(t, 1n+off), S.members(ys, _)) : List<&2, Nat>}
255 members_append(t, ys, 1n+off)
256 case Con{True{}, t}:
257 %N.add_succ(SC.length(Bool, t), off) : {Con{off, S.members(SC.append(Bool, t, ys), 1n+off)} == Con{off, SC.append(Nat, S.members(t, 1n+off), S.members(ys, _))} : List<&2, Nat>}
258 LL.cons_cong(Nat, off, S.members(SC.append(Bool, t, ys), 1n+off), SC.append(Nat, S.members(t, 1n+off), S.members(ys, Nat.add(SC.length(Bool, t), 1n+off))), members_append(t, ys, 1n+off))
259
260def count_take_snoc(+xs: List<&2, Bool>, +m: Nat) -> {S.count(SC.take(Bool, SC.snoc(Bool, xs, False{}), m)) == S.count(SC.take(Bool, xs, m)) : Nat}:
261 match xs m:
262 case Nil{} 0n:
263 {==}
264 case Nil{} 1n+p:
265 {==}
266 case Con{a, t} 0n:
267 {==}
268 case Con{False{}, t} 1n+p:
269 count_take_snoc(t, p)
270 case Con{True{}, t} 1n+p:
271 N.succ_cong(S.count(SC.take(Bool, SC.snoc(Bool, t, False{}), p)), S.count(SC.take(Bool, t, p)), count_take_snoc(t, p))
272
273def members_take_snoc(+xs: List<&2, Bool>, +m: Nat, +off: Nat) -> {S.members(SC.take(Bool, SC.snoc(Bool, xs, False{}), m), off) == S.members(SC.take(Bool, xs, m), off) : List<&2, Nat>}:
274 match xs m:
275 case Nil{} 0n:
276 {==}
277 case Nil{} 1n+p:
278 {==}
279 case Con{a, t} 0n:
280 {==}
281 case Con{False{}, t} 1n+p:
282 members_take_snoc(t, p, 1n+off)
283 case Con{True{}, t} 1n+p:
284 LL.cons_cong(Nat, off, S.members(SC.take(Bool, SC.snoc(Bool, t, False{}), p), 1n+off), S.members(SC.take(Bool, t, p), 1n+off), members_take_snoc(t, p, 1n+off))
285
286# ---- take / drop / update ----
287
288def take_all(+xs: List<&2, Bool>) -> {SC.take(Bool, xs, SC.length(Bool, xs)) == xs : List<&2, Bool>}:
289 match xs:
290 case Nil{}:
291 {==}
292 case Con{a, t}:
293 LL.cons_cong(Bool, a, SC.take(Bool, t, SC.length(Bool, t)), t, take_all(t))
294
295def take_drop(+xs: List<&2, Bool>, +n: Nat) -> {SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)) == xs : List<&2, Bool>}:
296 match xs n:
297 case Nil{} _:
298 {==}
299 case Con{a, t} 0n:
300 {==}
301 case Con{a, t} 1n+m:
302 LL.cons_cong(Bool, a, SC.append(Bool, SC.take(Bool, t, m), SC.drop(Bool, t, m)), t, take_drop(t, m))
303
304def length_take(+xs: List<&2, Bool>, +n: Nat, +h: {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}) -> {SC.length(Bool, SC.take(Bool, xs, n)) == n : Nat}:
305 match xs n:
306 case Nil{} 0n:
307 {==}
308 case Nil{} 1n+m:
309 Empty.absurd({SC.length(Bool, SC.take(Bool, Nil{}, 1n+m)) == 1n+m : Nat}, L.false_true(h))
310 case Con{a, t} 0n:
311 {==}
312 case Con{a, t} 1n+m:
313 N.succ_cong(SC.length(Bool, SC.take(Bool, t, m)), m, length_take(t, m, h))
314
315def nth_take(+xs: List<&2, Bool>, +n: Nat, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {SC.nth(Bool, SC.take(Bool, xs, n), i) == SC.nth(Bool, xs, i) : Maybe<&2, Bool>}:
316 match xs n i:
317 case Nil{} _ _:
318 {==}
319 case Con{a, t} 0n _:
320 Empty.absurd({SC.nth(Bool, SC.take(Bool, Con{a, t}, 0n), i) == SC.nth(Bool, Con{a, t}, i) : Maybe<&2, Bool>}, N.lt_zero_absurd(i, h))
321 case Con{a, t} 1n+m 0n:
322 {==}
323 case Con{a, t} 1n+m 1n+j:
324 nth_take(t, m, j, h)
325
326def take_update(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +n: Nat) -> {SC.take(Bool, SC.update(Bool, xs, i, v), n) == SC.update(Bool, SC.take(Bool, xs, n), i, v) : List<&2, Bool>}:
327 match xs i n:
328 case Nil{} _ _:
329 {==}
330 case Con{a, t} 0n 0n:
331 {==}
332 case Con{a, t} 1n+j 0n:
333 {==}
334 case Con{a, t} 0n 1n+m:
335 {==}
336 case Con{a, t} 1n+j 1n+m:
337 LL.cons_cong(Bool, a, SC.take(Bool, SC.update(Bool, t, j, v), m), SC.update(Bool, SC.take(Bool, t, m), j, v), take_update(t, j, v, m))
338
339def drop_update(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +n: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {SC.drop(Bool, SC.update(Bool, xs, i, v), n) == SC.drop(Bool, xs, n) : List<&2, Bool>}:
340 match xs i n:
341 case Nil{} _ _:
342 {==}
343 case Con{a, t} _ 0n:
344 Empty.absurd({SC.drop(Bool, SC.update(Bool, Con{a, t}, i, v), 0n) == SC.drop(Bool, Con{a, t}, 0n) : List<&2, Bool>}, N.lt_zero_absurd(i, h))
345 case Con{a, t} 0n 1n+m:
346 {==}
347 case Con{a, t} 1n+j 1n+m:
348 drop_update(t, j, v, m, h)
349
350# ---- single-bit masks ----
351
352def take_rep_succ(+m: Nat) -> {SC.take(Bool, rep(1n+m), m) == rep(m) : List<&2, Bool>}:
353 match m:
354 case 0n:
355 {==}
356 case 1n+q:
357 LL.cons_cong(Bool, False{}, SC.take(Bool, rep(1n+q), q), rep(q), take_rep_succ(q))
358
359# Shifting a one-hot mask up by one position.
360def take_onehot(+m: Nat, +p: Nat, +h: {Nat.is_lt(p, m) == True{} : Bool}) -> {SC.take(Bool, SC.update(Bool, rep(1n+m), p, True{}), m) == SC.update(Bool, rep(m), p, True{}) : List<&2, Bool>}:
361 match m p:
362 case 0n _:
363 Empty.absurd({SC.take(Bool, SC.update(Bool, rep(1n), p, True{}), 0n) == SC.update(Bool, rep(0n), p, True{}) : List<&2, Bool>}, N.lt_zero_absurd(p, h))
364 case 1n+q 0n:
365 LL.cons_cong(Bool, True{}, SC.take(Bool, rep(1n+q), q), rep(q), take_rep_succ(q))
366 case 1n+q 1n+j:
367 LL.cons_cong(Bool, False{}, SC.take(Bool, SC.update(Bool, rep(1n+q), j, True{}), q), SC.update(Bool, rep(q), j, True{}), take_onehot(q, j, h))
368
369def or_rep(+xs: List<&2, Bool>) -> {zipk(B.KOr{}, xs, rep(SC.length(Bool, xs))) == xs : List<&2, Bool>}:
370 match xs:
371 case Nil{}:
372 {==}
373 case Con{True{}, t}:
374 LL.cons_cong(Bool, True{}, zipk(B.KOr{}, t, rep(SC.length(Bool, t))), t, or_rep(t))
375 case Con{False{}, t}:
376 LL.cons_cong(Bool, False{}, zipk(B.KOr{}, t, rep(SC.length(Bool, t))), t, or_rep(t))
377
378def diff_rep(+xs: List<&2, Bool>) -> {zipk(B.KDiff{}, xs, rep(SC.length(Bool, xs))) == xs : List<&2, Bool>}:
379 match xs:
380 case Nil{}:
381 {==}
382 case Con{True{}, t}:
383 LL.cons_cong(Bool, True{}, zipk(B.KDiff{}, t, rep(SC.length(Bool, t))), t, diff_rep(t))
384 case Con{False{}, t}:
385 LL.cons_cong(Bool, False{}, zipk(B.KDiff{}, t, rep(SC.length(Bool, t))), t, diff_rep(t))
386
387# OR with the one-hot mask for k sets bit k.
388def or_onehot(+xs: List<&2, Bool>, +k: Nat) -> {zipk(B.KOr{}, xs, SC.update(Bool, rep(SC.length(Bool, xs)), k, True{})) == SC.update(Bool, xs, k, True{}) : List<&2, Bool>}:
389 match xs k:
390 case Nil{} _:
391 {==}
392 case Con{True{}, t} 0n:
393 LL.cons_cong(Bool, True{}, zipk(B.KOr{}, t, rep(SC.length(Bool, t))), t, or_rep(t))
394 case Con{False{}, t} 0n:
395 LL.cons_cong(Bool, True{}, zipk(B.KOr{}, t, rep(SC.length(Bool, t))), t, or_rep(t))
396 case Con{True{}, t} 1n+j:
397 LL.cons_cong(Bool, True{}, zipk(B.KOr{}, t, SC.update(Bool, rep(SC.length(Bool, t)), j, True{})), SC.update(Bool, t, j, True{}), or_onehot(t, j))
398 case Con{False{}, t} 1n+j:
399 LL.cons_cong(Bool, False{}, zipk(B.KOr{}, t, SC.update(Bool, rep(SC.length(Bool, t)), j, True{})), SC.update(Bool, t, j, True{}), or_onehot(t, j))
400
401# AND NOT with the one-hot mask for k clears bit k.
402def diff_onehot(+xs: List<&2, Bool>, +k: Nat) -> {zipk(B.KDiff{}, xs, SC.update(Bool, rep(SC.length(Bool, xs)), k, True{})) == SC.update(Bool, xs, k, False{}) : List<&2, Bool>}:
403 match xs k:
404 case Nil{} _:
405 {==}
406 case Con{True{}, t} 0n:
407 LL.cons_cong(Bool, False{}, zipk(B.KDiff{}, t, rep(SC.length(Bool, t))), t, diff_rep(t))
408 case Con{False{}, t} 0n:
409 LL.cons_cong(Bool, False{}, zipk(B.KDiff{}, t, rep(SC.length(Bool, t))), t, diff_rep(t))
410 case Con{True{}, t} 1n+j:
411 LL.cons_cong(Bool, True{}, zipk(B.KDiff{}, t, SC.update(Bool, rep(SC.length(Bool, t)), j, True{})), SC.update(Bool, t, j, False{}), diff_onehot(t, j))
412 case Con{False{}, t} 1n+j:
413 LL.cons_cong(Bool, False{}, zipk(B.KDiff{}, t, SC.update(Bool, rep(SC.length(Bool, t)), j, True{})), SC.update(Bool, t, j, False{}), diff_onehot(t, j))