proofs/lib/lemmas/proofs/map_index.bend
bend-collections-laws-containers@1.0.0.0 · 92 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Logic
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as N
4
5# Existing Base.divmod quotient translation; no replacement division algorithm.
6def next_quotient(pair: Nat & Nat) -> Nat & Nat:
7 (q, r) = pair
8 (1n+q, r)
9
10law quotient_translation:
11 for n: Nat
12 for m: Nat
13 for +q: Nat
14 for r: Nat
15 {Nat.divmod.go(n, m, 1n+q, r) == next_quotient(Nat.divmod.go(n, m, q, r)) : Nat & Nat}
16def quotient_translation(n, m, q, r):
17 match n:
18 case 0n: {==}
19 case 1n+p:
20 match m:
21 case 0n:
22 quotient_translation(p, r, 1n+q, 0n)
23 case 1n+k:
24 quotient_translation(p, k, q, 1n+r)
25
26law character_stride:
27 for position: Nat
28 {Nat.divmod(Nat.add(33n, position), 33n) == next_quotient(Nat.divmod(position, 33n)) : Nat & Nat}
29def character_stride(position):
30 quotient_translation(position, 32n, 0n, 0n)
31
32law bit_at_next:
33 for h: Char
34 for tail: String
35 for pair: Nat & Nat
36 {Map.bit.at(SCon{h, tail}, next_quotient(pair)) == Map.bit.go.rec(h, Map.bit.at(tail, pair)) : String & Bool}
37def bit_at_next(h, tail, pair):
38 match pair:
39 case Tuple{q, r}: {==}
40
41# This exact key-preserving result connects bit positions across String prefixes
42# using the native division and bit traversal definitions.
43law native_character_stride:
44 for +h: Char
45 for +tail: String
46 for +position: Nat
47 {Map.bit(SCon{h, tail}, Nat.add(33n, position)) == Map.bit.go.rec(h, Map.bit(tail, position)) : String & Bool}
48def native_character_stride(h, tail, position):
49 Equal.trans(String & Bool, Map.bit(SCon{h, tail}, Nat.add(33n, position)), Map.bit.at(SCon{h, tail}, next_quotient(Nat.divmod(position, 33n))), Map.bit.go.rec(h, Map.bit(tail, position)), Equal.cong(Nat & Nat, String & Bool, qr => Map.bit.at(SCon{h, tail}, qr), Nat.divmod(Nat.add(33n, position), 33n), next_quotient(Nat.divmod(position, 33n)), character_stride(position)), bit_at_next(h, tail, Nat.divmod(position, 33n)))
50
51law add_right_successor:
52 for a: Nat
53 for +b: Nat
54 {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}
55def add_right_successor(a, b):
56 match a:
57 case 0n: {==}
58 case 1n+ +p:
59 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 1n+b), 1n+Nat.add(p, b), add_right_successor(p, b))
60
61law division_no_wrap:
62 for n: Nat
63 for m: Nat
64 for +q: Nat
65 for +r: Nat
66 for bound: {Nat.is_le(n, m) == True{} : Bool}
67 {Nat.divmod.go(n, m, q, r) == (q, Nat.add(n, r)) : Nat & Nat}
68def division_no_wrap(n, m, q, r, bound):
69 match n:
70 case 0n: {==}
71 case 1n+ +p:
72 match m:
73 case 0n:
74 Empty.absurd({Nat.divmod.go(1n+p, 0n, q, r) == (q, Nat.add(1n+p, r)) : Nat & Nat}, Logic.false_true(bound))
75 case 1n+ +k:
76 Equal.trans(Nat & Nat, Nat.divmod.go(p, k, q, 1n+r), (q, Nat.add(p, 1n+r)), (q, 1n+Nat.add(p, r)), division_no_wrap(p, k, q, 1n+r, bound), Equal.cong(Nat, Nat & Nat, s => (q, s), Nat.add(p, 1n+r), 1n+Nat.add(p, r), add_right_successor(p, r)))
77
78law first_character_division:
79 for +position: Nat
80 for bound: {Nat.is_le(position, 32n) == True{} : Bool}
81 {Nat.divmod(position, 33n) == (0n, position) : Nat & Nat}
82def first_character_division(position, bound):
83 Equal.trans(Nat & Nat, Nat.divmod(position, 33n), (0n, Nat.add(position, 0n)), (0n, position), division_no_wrap(position, 32n, 0n, 0n, bound), Equal.cong(Nat, Nat & Nat, r => (0n, r), Nat.add(position, 0n), position, N.natural_add_right_zero(position)))
84
85law native_first_character:
86 for +head: Char
87 for +tail: String
88 for +position: Nat
89 for bound: {Nat.is_le(position, 32n) == True{} : Bool}
90 {Map.bit(SCon{head, tail}, position) == Map.bit.go.chr(tail, Map.bit.chr(head, position)) : String & Bool}
91def native_first_character(head, tail, position, bound):
92 Equal.cong(Nat & Nat, String & Bool, qr => Map.bit.at(SCon{head, tail}, qr), Nat.divmod(position, 33n), (0n, position), first_character_division(position, bound))