proofs/containers/bitset/index.bend
bend-collections-laws-containers@1.0.0.0 · 88 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/src/containers/bitset.bend as B
5
6# The two facts about the word index `B.wordix(i) = i / 32` and the bit
7# position `B.bitix(i) = i % 32` that the packed representation needs:
8#
9# i < 32 -> wordix(i) = 0 and bitix(i) = i
10# wordix(32 + i) = 1 + wordix(i) and bitix(32 + i) = bitix(i)
11#
12# Both are proved from Base's own `Nat.divmod.go`, which is a structural
13# recursion on the dividend, so 32 unfoldings of `Nat.add(32n, i)` are a
14# definitional step (`peel_go` below is literally `{==}`); only the quotient
15# accumulator has to be pushed out by an induction.
16
17def bump(p: Nat & Nat) -> Nat & Nat:
18 (q, r) = p
19 (1n+q, r)
20
21# The quotient accumulator of Nat.divmod.go is exactly an accumulator.
22def acc(i: Nat, m: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(i, m, 1n+d, r) == bump(Nat.divmod.go(i, m, d, r)) : Nat & Nat}:
23 match i m:
24 case 0n _:
25 {==}
26 case 1n+np 0n:
27 acc(np, r, 1n+d, 0n)
28 case 1n+np 1n+mp:
29 acc(np, mp, d, 1n+r)
30
31# 32 unfoldings: the dividend loses 32, the quotient gains one.
32def peel_go(+i: Nat, +d: Nat) -> {Nat.divmod.go(Nat.add(32n, i), 31n, d, 0n) == Nat.divmod.go(i, 31n, 1n+d, 0n) : Nat & Nat}:
33 {==}
34
35def peel(+i: Nat) -> {Nat.divmod(Nat.add(32n, i), 32n) == bump(Nat.divmod(i, 32n)) : Nat & Nat}:
36 Equal.trans(Nat & Nat, Nat.divmod.go(Nat.add(32n, i), 31n, 0n, 0n), Nat.divmod.go(i, 31n, 1n, 0n), bump(Nat.divmod.go(i, 31n, 0n, 0n)),
37 peel_go(i, 0n), acc(i, 31n, 0n, 0n))
38
39def fst_bump(p: Nat & Nat) -> {Pair.fst(Nat, Nat, bump(p)) == 1n+Pair.fst(Nat, Nat, p) : Nat}:
40 (q, r) = p
41 {==}
42
43def snd_bump(p: Nat & Nat) -> {Pair.snd(Nat, Nat, bump(p)) == Pair.snd(Nat, Nat, p) : Nat}:
44 (q, r) = p
45 {==}
46
47def wordix_peel(+i: Nat) -> {B.wordix(Nat.add(32n, i)) == 1n+B.wordix(i) : Nat}:
48 Equal.trans(Nat, Pair.fst(Nat, Nat, Nat.divmod(Nat.add(32n, i), 32n)), Pair.fst(Nat, Nat, bump(Nat.divmod(i, 32n))), 1n+Pair.fst(Nat, Nat, Nat.divmod(i, 32n)),
49 Equal.cong(Nat & Nat, Nat, pq => Pair.fst(Nat, Nat, pq), Nat.divmod(Nat.add(32n, i), 32n), bump(Nat.divmod(i, 32n)), peel(i)),
50 fst_bump(Nat.divmod(i, 32n)))
51
52def bitix_peel(+i: Nat) -> {B.bitix(Nat.add(32n, i)) == B.bitix(i) : Nat}:
53 Equal.trans(Nat, Pair.snd(Nat, Nat, Nat.divmod(Nat.add(32n, i), 32n)), Pair.snd(Nat, Nat, bump(Nat.divmod(i, 32n))), Pair.snd(Nat, Nat, Nat.divmod(i, 32n)),
54 Equal.cong(Nat & Nat, Nat, pq => Pair.snd(Nat, Nat, pq), Nat.divmod(Nat.add(32n, i), 32n), bump(Nat.divmod(i, 32n)), peel(i)),
55 snd_bump(Nat.divmod(i, 32n)))
56
57# A dividend that never reaches the divisor never advances the quotient.
58def small_go(i: Nat, m: Nat, +r: Nat, +h: {Nat.is_le(i, m) == True{} : Bool}) -> {Nat.divmod.go(i, m, 0n, r) == (0n, Nat.add(r, i)) : Nat & Nat}:
59 match i m:
60 case 0n _:
61 %Equal.sym(Nat, Nat.add(r, 0n), r, N.add_zero(r)) : {(0n, r) == (0n, _) : Nat & Nat}
62 {==}
63 case 1n+ +np 0n:
64 Empty.absurd({Nat.divmod.go(1n+np, 0n, 0n, r) == (0n, Nat.add(r, 1n+np)) : Nat & Nat}, L.false_true(h))
65 case 1n+ +np 1n+mp:
66 %Equal.sym(Nat, Nat.add(r, 1n+np), 1n+Nat.add(r, np), N.add_succ(r, np)) : {Nat.divmod.go(np, mp, 0n, 1n+r) == (0n, _) : Nat & Nat}
67 small_go(np, mp, 1n+r, h)
68
69def small(+i: Nat, +h: {Nat.is_lt(i, 32n) == True{} : Bool}) -> {Nat.divmod(i, 32n) == (0n, i) : Nat & Nat}:
70 small_go(i, 31n, 0n, N.lt_succ_le(i, 31n, h))
71
72def wordix_small(+i: Nat, +h: {Nat.is_lt(i, 32n) == True{} : Bool}) -> {B.wordix(i) == 0n : Nat}:
73 Equal.cong(Nat & Nat, Nat, pq => Pair.fst(Nat, Nat, pq), Nat.divmod(i, 32n), (0n, i), small(i, h))
74
75def bitix_small(+i: Nat, +h: {Nat.is_lt(i, 32n) == True{} : Bool}) -> {B.bitix(i) == i : Nat}:
76 Equal.cong(Nat & Nat, Nat, pq => Pair.snd(Nat, Nat, pq), Nat.divmod(i, 32n), (0n, i), small(i, h))
77
78# The form the word walk needs: for i >= 32, i = 32 + (i - 32).
79def add_sub32(+i: Nat, +h: {Nat.is_lt(i, 32n) == False{} : Bool}) -> {Nat.add(32n, Nat.sub(i, 32n)) == i : Nat}:
80 N.sub_add(i, 32n, N.not_lt_le(i, 32n, h))
81
82def wordix_step(+i: Nat, +h: {Nat.is_lt(i, 32n) == False{} : Bool}) -> {B.wordix(i) == 1n+B.wordix(Nat.sub(i, 32n)) : Nat}:
83 L.subst(Nat, x => {B.wordix(x) == 1n+B.wordix(Nat.sub(i, 32n)) : Nat},
84 Nat.add(32n, Nat.sub(i, 32n)), i, add_sub32(i, h), wordix_peel(Nat.sub(i, 32n)))
85
86def bitix_step(+i: Nat, +h: {Nat.is_lt(i, 32n) == False{} : Bool}) -> {B.bitix(i) == B.bitix(Nat.sub(i, 32n)) : Nat}:
87 L.subst(Nat, x => {B.bitix(x) == B.bitix(Nat.sub(i, 32n)) : Nat},
88 Nat.add(32n, Nat.sub(i, 32n)), i, add_sub32(i, h), bitix_peel(Nat.sub(i, 32n)))