proofs/lib/lemmas/proofs/string_compare.bend
bend-collections-laws-crypto@1.0.0.0 · 262 lines · 21 definitions
1import Base
2
3
4
5
6
7law boolean_compare_self:
8 for b: Bool
9 {Bool.cmp(b, b) == EQ{} : Cmp}
10def boolean_compare_self(b):
11 match b:
12 case False{}:
13 {==}
14 case True{}:
15 {==}
16
17law word_compare_self:
18 for n: Nat
19 for w: Word(n)
20 {Word.cmp(n, w, w) == EQ{} : Cmp}
21def word_compare_self(n, w):
22 match n:
23 case 0n:
24 {==}
25 case 1n+p:
26 match w:
27 case WCon{+b, t}:
28 Equal.trans(Cmp, Word.cmp.fin(b, b, Word.cmp(p, t, t)), Bool.cmp(b, b), EQ{},
29 Equal.cong(Cmp, Cmp, x => Word.cmp.fin(b, b, x), Word.cmp(p, t, t), EQ{}, word_compare_self(p, t)),
30 boolean_compare_self(b))
31
32law character_compare_self:
33 for c: Char
34 {Char.cmp(c, c) == ((c, c), EQ{}) : (Char & Char) & Cmp}
35def character_compare_self(c):
36 match c:
37 case Chr{U32{w}}:
38 %word_compare_self(32n, w) : {((Chr{U32{w}}, Chr{U32{w}}), Word.cmp(32n, w, w)) == ((Chr{U32{w}}, Chr{U32{w}}), _) : (Char & Char) & Cmp}
39 {==}
40
41law string_compare_self:
42 for s: String
43 {String.cmp(s, s) == ((s, s), EQ{}) : (String & String) & Cmp}
44def string_compare_self(s):
45 match s:
46 case SNil{}:
47 {==}
48 case SCon{h, t}:
49 %Equal.sym((Char & Char) & Cmp, Char.cmp(h, h), ((h, h), EQ{}), character_compare_self(h)) : {String.cmp.fin(t, t, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
50 %Equal.sym((String & String) & Cmp, String.cmp(t, t), ((t, t), EQ{}), string_compare_self(t)) : {String.cmp.rec(h, h, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
51 {==}
52
53def comparison_identity(-A: Type, a: A, b: A, c: Cmp) -> Type:
54 match c:
55 case LT{}:
56 Unit
57 case EQ{}:
58 {a == b : A}
59 case GT{}:
60 Unit
61
62law word_comparison_step:
63 for n: Nat
64 for a: Word(n)
65 for b: Word(n)
66 for c: Cmp
67 for x: Bool
68 for y: Bool
69 for proof: comparison_identity(Word(n), a, b, c)
70 comparison_identity(Word(1n+n), WCon{x, a}, WCon{y, b}, Word.cmp.fin(x, y, c))
71def word_comparison_step(n, a, b, c, x, y, proof):
72 match c:
73 case LT{}:
74 Unit{}
75 case GT{}:
76 Unit{}
77 case EQ{}:
78 match x y:
79 case False{} False{}:
80 Equal.cong(Word(n), Word(1n+n), t => WCon{False{}, t}, a, b, proof)
81 case True{} True{}:
82 Equal.cong(Word(n), Word(1n+n), t => WCon{True{}, t}, a, b, proof)
83 case False{} True{}:
84 Unit{}
85 case True{} False{}:
86 Unit{}
87
88law word_comparison_identity:
89 for n: Nat
90 for a: Word(n)
91 for b: Word(n)
92 comparison_identity(Word(n), a, b, Word.cmp(n, a, b))
93def word_comparison_identity(n, a, b):
94 match n:
95 case 0n:
96 match a b:
97 case WNil{} WNil{}:
98 {==}
99 case 1n+ +p:
100 match a b:
101 case WCon{x, +at} WCon{y, +bt}:
102 word_comparison_step(p, at, bt, Word.cmp(p, at, bt), x, y, word_comparison_identity(p, at, bt))
103
104law comparison_lift:
105 for -A: Type
106 for -B: Type
107 for f: A -> B
108 for a: A
109 for b: A
110 for c: Cmp
111 for proof: comparison_identity(A, a, b, c)
112 comparison_identity(B, f(a), f(b), c)
113def comparison_lift(A, B, f, a, b, c, proof):
114 match c:
115 case LT{}:
116 Unit{}
117 case GT{}:
118 Unit{}
119 case EQ{}:
120 Equal.cong(A, B, f, a, b, proof)
121
122def comparison_result_identity(-A: Type, r: (A & A) & Cmp) -> Type:
123 ((a, b), c) = r
124 comparison_identity(A, a, b, c)
125
126law character_comparison_identity:
127 for a: Char
128 for b: Char
129 comparison_result_identity(Char, Char.cmp(a, b))
130def character_comparison_identity(a, b):
131 match a b:
132 case Chr{U32{+x}} Chr{U32{+y}}:
133 comparison_lift(Word(32n), Char, w => Chr{U32{w}}, x, y, Word.cmp(32n, x, y), word_comparison_identity(32n, x, y))
134
135law string_comparison_rec_identity:
136 for h: Char
137 for r: (String & String) & Cmp
138 for proof: comparison_result_identity(String, r)
139 comparison_result_identity(String, String.cmp.rec(h, h, r))
140def string_comparison_rec_identity(h, r, proof):
141 match r:
142 case Tuple{Tuple{a, b}, c}:
143 comparison_lift(String, String, t => SCon{h, t}, a, b, c, proof)
144
145law string_comparison_fin_identity:
146 for t1: String
147 for t2: String
148 for hc: (Char & Char) & Cmp
149 for hp: comparison_result_identity(Char, hc)
150 for tp: comparison_result_identity(String, String.cmp(t1, t2))
151 comparison_result_identity(String, String.cmp.fin(t1, t2, hc))
152def string_comparison_fin_identity(t1, t2, hc, hp, tp):
153 match hc:
154 case Tuple{Tuple{h1, h2}, LT{}}:
155 Unit{}
156 case Tuple{Tuple{h1, h2}, GT{}}:
157 Unit{}
158 case Tuple{Tuple{h1, h2}, EQ{}}:
159 %hp : comparison_result_identity(String, String.cmp.rec(h1, _, String.cmp(t1, t2)))
160 string_comparison_rec_identity(h1, String.cmp(t1, t2), tp)
161
162law string_comparison_identity:
163 for a: String
164 for b: String
165 comparison_result_identity(String, String.cmp(a, b))
166def string_comparison_identity(a, b):
167 match a b:
168 case SNil{} SNil{}:
169 {==}
170 case SNil{} SCon{h, t}:
171 Unit{}
172 case SCon{h, t} SNil{}:
173 Unit{}
174 case SCon{+h1, +t1} SCon{+h2, +t2}:
175 string_comparison_fin_identity(t1, t2, Char.cmp(h1, h2), character_comparison_identity(h1, h2), string_comparison_identity(t1, t2))
176
177def comparison_tag(-A: Type, r: (A & A) & Cmp) -> Cmp:
178 (pair, c) = r
179 c
180
181law string_comparison_shape_step:
182 for h1: Char
183 for h2: Char
184 for t1: String
185 for t2: String
186 for c: Cmp
187 for tp: {String.cmp(t1, t2) == ((t1, t2), comparison_tag(String, String.cmp(t1, t2))) : (String & String) & Cmp}
188 {String.cmp.fin(t1, t2, ((h1, h2), c)) == ((SCon{h1, t1}, SCon{h2, t2}), comparison_tag(String, String.cmp.fin(t1, t2, ((h1, h2), c)))) : (String & String) & Cmp}
189def string_comparison_shape_step(h1, h2, t1, t2, c, tp):
190 match c:
191 case LT{}:
192 {==}
193 case GT{}:
194 {==}
195 case EQ{}:
196 %Equal.sym((String & String) & Cmp, String.cmp(t1, t2), ((t1, t2), comparison_tag(String, String.cmp(t1, t2))), tp) : {String.cmp.rec(h1, h2, _) == ((SCon{h1, t1}, SCon{h2, t2}), comparison_tag(String, String.cmp.rec(h1, h2, _))) : (String & String) & Cmp}
197 {==}
198
199law string_comparison_shape:
200 for a: String
201 for b: String
202 {String.cmp(a, b) == ((a, b), comparison_tag(String, String.cmp(a, b))) : (String & String) & Cmp}
203def string_comparison_shape(a, b):
204 match a b:
205 case SNil{} SNil{}:
206 {==}
207 case SNil{} SCon{h, t}:
208 {==}
209 case SCon{h, t} SNil{}:
210 {==}
211 case SCon{Chr{U32{+x}}, +t1} SCon{Chr{U32{+y}}, +t2}:
212 string_comparison_shape_step(Chr{U32{x}}, Chr{U32{y}}, t1, t2, Word.cmp(32n, x, y), string_comparison_shape(t1, t2))
213
214law string_comparison_original_identity:
215 for +a: String
216 for +b: String
217 comparison_identity(String, a, b, comparison_tag(String, String.cmp(a, b)))
218def string_comparison_original_identity(a, b):
219 %string_comparison_shape(a, b) : comparison_result_identity(String, _)
220 string_comparison_identity(a, b)
221
222law string_equal_from_comparison:
223 for a: String
224 for b: String
225 for e: {comparison_tag(String, String.cmp(a, b)) == EQ{} : Cmp}
226 {a == b : String}
227def string_equal_from_comparison(a, b, e):
228 %e : comparison_identity(String, a, b, _)
229 string_comparison_original_identity(a, b)
230
231law string_equal_comparison:
232 for a: String
233 for b: String
234 for e: {a == b : String}
235 {String.cmp(a, b) == ((a, b), EQ{}) : (String & String) & Cmp}
236def string_equal_comparison(a, b, e):
237 %e : {String.cmp(a, _) == ((a, _), EQ{}) : (String & String) & Cmp}
238 string_compare_self(a)
239
240
241law natural_add_associative:
242 for a: Nat
243 for b: Nat
244 for c: Nat
245 {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
246def natural_add_associative(a, b, c):
247 match a:
248 case 0n:
249 {==}
250 case 1n+p:
251 Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, Nat.add(b, c)), Nat.add(Nat.add(p, b), c), natural_add_associative(p, b, c))
252
253law natural_add_right_zero:
254 for a: Nat
255 {Nat.add(a, 0n) == a : Nat}
256def natural_add_right_zero(a):
257 match a:
258 case 0n:
259 {==}
260 case 1n+p:
261 Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, natural_add_right_zero(p))
262