1 import Base 2 import ./defs.bend as D 3 import ./proof_base.bend as B 4 5 # Structural lemmas about Base's Array: the shape-only laws, and the tools the 6 # index proofs use. 7 # 8 # An Array is a Type, so a proof may use an array variable once: two lemmas 9 # about the same subtree (or a lemma and the induction hypothesis) cannot both 10 # take it. For Data elements, mirror(a) gives a Tree (a Data copy of the 11 # shape and leaves) with fromT(t) == a; lemmas about fromT(t) may use t freely. 12 13 type Tree<-T: Data> is Data: 14 TLeaf{x: T} 15 TNode{l: Tree, r: Tree} 16 17 def fromT(-T: Data, t: Tree) -> Array: 18 match t: 19 case TLeaf{x}: 20 ALeaf{x} 21 case TNode{l, r}: 22 ANode{fromT(T, l), fromT(T, r)} 23 24 def Mirror(-T: Data, -a: Array) -> Data: 25 Sigma<&2, &2, Tree, t => {fromT(T, t) == a : Array}> 26 27 law anode_eq: 28 for -T: Type 29 for -x1: Array 30 for -x2: Array 31 for -y1: Array 32 for -y2: Array 33 for e1: {x1 == y1 : Array} 34 for e2: {x2 == y2 : Array} 35 {ANode{x1, x2} == ANode{y1, y2} : Array} 36 37 def anode_eq(T, x1, x2, y1, y2, e1, e2): 38 %e1 : {ANode{x1, x2} == ANode{_, y2} : Array} 39 %e2 : {ANode{x1, x2} == ANode{x1, _} : Array} 40 {==} 41 42 def mirror.node(-T: Data, -xs: Array, -ys: Array, m1: Mirror(T, xs), m2: Mirror(T, ys)) 43 -> Mirror(T, ANode{xs, ys}): 44 (t1, e1) = m1 45 (t2, e2) = m2 46 (TNode{t1, t2}, anode_eq(T, fromT(T, t1), fromT(T, t2), xs, ys, e1, e2)) 47 48 def mirror(-T: Data, a: Array) -> Mirror(T, a): 49 match a: 50 case ALeaf{x}: 51 (TLeaf{x}, {==}) 52 case ANode{xs, ys}: 53 mirror.node(T, xs, ys, mirror(T, xs), mirror(T, ys)) 54 55 # Pairs returned by swap and get 56 # ============================== 57 58 law lo_fst: 59 for -T: Type 60 for -ys: Array 61 for r: Array & T 62 {Pair.fst(Array, T, Array.swap.lo(T, ys, r)) == ANode{Pair.fst(Array, T, r), ys} : Array} 63 64 def lo_fst(T, ys, r): 65 (a, x) = r 66 {==} 67 68 law lo_snd: 69 for -T: Type 70 for -ys: Array 71 for r: Array & T 72 {Pair.snd(Array, T, Array.swap.lo(T, ys, r)) == Pair.snd(Array, T, r) : T} 73 74 def lo_snd(T, ys, r): 75 (a, x) = r 76 {==} 77 78 law hi_fst: 79 for -T: Type 80 for -xs: Array 81 for r: Array & T 82 {Pair.fst(Array, T, Array.swap.hi(T, xs, r)) == ANode{xs, Pair.fst(Array, T, r)} : Array} 83 84 def hi_fst(T, xs, r): 85 (a, x) = r 86 {==} 87 88 law hi_snd: 89 for -T: Type 90 for -xs: Array 91 for r: Array & T 92 {Pair.snd(Array, T, Array.swap.hi(T, xs, r)) == Pair.snd(Array, T, r) : T} 93 94 def hi_snd(T, xs, r): 95 (a, x) = r 96 {==} 97 98 law fin_fst: 99 for -T: Type 100 for r: Array & T 101 {Array.set.fin(T, r) == Pair.fst(Array, T, r) : Array} 102 103 def fin_fst(T, r): 104 (a, x) = r 105 {==} 106 107 # Size 108 # ==== 109 110 law size_eta: 111 for -T: Type 112 for a: Array 113 {Array.size(T, a) == (a, Pair.snd(Array, U32, Array.size(T, a))) : Array & U32} 114 115 def size_eta(T, a): 116 match a: 117 case ALeaf{x}: 118 {==} 119 case ANode{xs, ys}: 120 %Equal.sym(Array & U32, Array.size(T, xs), (xs, Pair.snd(Array, U32, Array.size(T, xs))), 121 size_eta(T, xs)) : 122 {Array.size.node(T, ys, _) == (ANode{xs, ys}, Pair.snd(Array, U32, Array.size.node(T, ys, _))) : Array & U32} 123 {==} 124 125 law size_tree: 126 for -T: Data 127 for +d: Nat 128 for +t: Tree 129 for hf: {D.full(T, fromT(T, t), d) == True{} : Bool} 130 {Array.size(T, fromT(T, t)) == (fromT(T, t), U32.shln(1, d)) : Array & U32} 131 132 def size_tree(T, d, t, hf): 133 match d t: 134 case 0n TLeaf{x}: 135 {==} 136 case 0n TNode{l, r}: 137 Empty.absurd({Array.size(T, fromT(T, TNode{l, r})) == (fromT(T, TNode{l, r}), 1) : Array & U32}, 138 B.false_ne_true(hf)) 139 case 1n+p TLeaf{x}: 140 Empty.absurd({Array.size(T, ALeaf{x}) == (ALeaf{x}, U32.shln(1, 1n+p)) : Array & U32}, 141 B.false_ne_true(hf)) 142 case 1n+p TNode{l, r}: 143 %Equal.sym(Array & U32, Array.size(T, fromT(T, l)), (fromT(T, l), U32.shln(1, p)), 144 size_tree(T, p, l, B.and_true_l(D.full(T, fromT(T, l), p), D.full(T, fromT(T, r), p), hf))) : 145 {Array.size.node(T, fromT(T, r), _) == (ANode{fromT(T, l), fromT(T, r)}, U32.shln(1, 1n+p)) : Array & U32} 146 {==} 147 148 # Leaves 149 # ====== 150 151 law view_length: 152 for -T: Data 153 for +d: Nat 154 for +t: Tree 155 for +hf: {D.full(T, fromT(T, t), d) == True{} : Bool} 156 {List.length(&2, T, D.view(T, fromT(T, t))) == Nat.pow(2n, d) : Nat} 157 158 def view_length(T, d, t, hf): 159 match d t: 160 case 0n TLeaf{x}: 161 {==} 162 case 0n TNode{l, r}: 163 Empty.absurd({List.length(&2, T, D.view(T, fromT(T, TNode{l, r}))) == 1n : Nat}, B.false_ne_true(hf)) 164 case 1n+p TLeaf{x}: 165 Empty.absurd({1n == Nat.pow(2n, 1n+p) : Nat}, B.false_ne_true(hf)) 166 case 1n+p TNode{l, r}: 167 +VL = D.view(T, fromT(T, l)) 168 +VR = D.view(T, fromT(T, r)) 169 +P = Nat.pow(2n, p) 170 %Equal.sym(Nat, List.length(&2, T, List.append(&2, T, VL, VR)), 171 Nat.add(List.length(&2, T, VL), List.length(&2, T, VR)), B.length_append(T, VL, VR)) : 172 {_ == Nat.pow(2n, 1n+p) : Nat} 173 %Equal.sym(Nat, List.length(&2, T, VL), P, 174 view_length(T, p, l, B.and_true_l(D.full(T, fromT(T, l), p), D.full(T, fromT(T, r), p), hf))) : 175 {Nat.add(_, List.length(&2, T, VR)) == Nat.pow(2n, 1n+p) : Nat} 176 %Equal.sym(Nat, List.length(&2, T, VR), P, 177 view_length(T, p, r, B.and_true_r(D.full(T, fromT(T, l), p), D.full(T, fromT(T, r), p), hf))) : 178 {Nat.add(P, _) == Nat.pow(2n, 1n+p) : Nat} 179 Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.add(P, P), B.pow_succ(p)) 180 181 # New arrays 182 # ========== 183 184 law new_full: 185 for -T: Data 186 for +d: Nat 187 for +v: T 188 {D.full(T, Array.new(T, d, v), d) == True{} : Bool} 189 190 def new_full(T, d, v): 191 match d: 192 case 0n: 193 {==} 194 case 1n+p: 195 %Equal.sym(Bool, D.full(T, Array.new(T, p, v), p), True{}, new_full(T, p, v)) : 196 {Bool.and(_, _) == True{} : Bool} 197 {==} 198 199 law new_view: 200 for -T: Data 201 for +d: Nat 202 for +v: T 203 {D.view(T, Array.new(T, d, v)) == List.replicate(T, Nat.pow(2n, d), v) : List<&2, T>} 204 205 def new_view(T, d, v): 206 match d: 207 case 0n: 208 {==} 209 case 1n+p: 210 +V = D.view(T, Array.new(T, p, v)) 211 +P = Nat.pow(2n, p) 212 %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.add(P, P), B.pow_succ(p)) : 213 {List.append(&2, T, V, V) == List.replicate(T, _, v) : List<&2, T>} 214 %Equal.sym(List<&2, T>, List.replicate(T, Nat.add(P, P), v), 215 List.append(&2, T, List.replicate(T, P, v), List.replicate(T, P, v)), B.replicate_add(T, P, P, v)) : 216 {List.append(&2, T, V, V) == _ : List<&2, T>} 217 %new_view(T, p, v) : 218 {List.append(&2, T, V, V) == List.append(&2, T, _, _) : List<&2, T>} 219 {==} 220 221 law get_new_go: 222 for -T: Data 223 for +d: Nat 224 for +v: T 225 for +n: U32 226 for +i: U32 227 for +z: Bool 228 {Pair.snd(Array, T, Array.get.go(T, Array.new(T, d, v), n, i, z)) == v : T} 229 230 def get_new_go(T, d, v, n, i, z): 231 match d z: 232 case 0n _: 233 {==} 234 case 1n+p True{}: 235 +h = U32.shr(n) 236 %Equal.sym(T, Pair.snd(Array, T, Array.swap.lo(T, Array.new(T, p, v), Array.get.go(T, Array.new(T, p, v), h, i, U32.is_lt(i, U32.shr(h))))), Pair.snd(Array, T, Array.get.go(T, Array.new(T, p, v), h, i, U32.is_lt(i, U32.shr(h)))), 237 lo_snd(T, Array.new(T, p, v), Array.get.go(T, Array.new(T, p, v), h, i, U32.is_lt(i, U32.shr(h))))) : {_ == v : T} 238 get_new_go(T, p, v, h, i, U32.is_lt(i, U32.shr(h))) 239 case 1n+p False{}: 240 +h = U32.shr(n) 241 +j = U32.sub(i, h) 242 %Equal.sym(T, Pair.snd(Array, T, Array.swap.hi(T, Array.new(T, p, v), Array.get.go(T, Array.new(T, p, v), h, j, U32.is_lt(j, U32.shr(h))))), Pair.snd(Array, T, Array.get.go(T, Array.new(T, p, v), h, j, U32.is_lt(j, U32.shr(h)))), 243 hi_snd(T, Array.new(T, p, v), Array.get.go(T, Array.new(T, p, v), h, j, U32.is_lt(j, U32.shr(h))))) : {_ == v : T} 244 get_new_go(T, p, v, h, j, U32.is_lt(j, U32.shr(h))) 245 246 # Cloning 247 # ======= 248 249 law clone_pair: 250 for -T: Data 251 for a: Array 252 {Array.clone(T, a) == (a, a) : Array & Array} 253 254 def clone_pair(T, a): 255 match a: 256 case ALeaf{x}: 257 {==} 258 case ANode{xs, ys}: 259 %Equal.sym(Array & Array, Array.clone(T, xs), (xs, xs), clone_pair(T, xs)) : 260 {Array.clone.node(T, _, Array.clone(T, ys)) == (ANode{xs, ys}, ANode{xs, ys}) : Array & Array} 261 %Equal.sym(Array & Array, Array.clone(T, ys), (ys, ys), clone_pair(T, ys)) : 262 {Array.clone.node(T, (xs, xs), _) == (ANode{xs, ys}, ANode{xs, ys}) : Array & Array} 263 {==} 264 265 # Reading hands the array back 266 # ============================ 267 268 law get_go_eta: 269 for -T: Data 270 for a: Array 271 for +n: U32 272 for +i: U32 273 for +z: Bool 274 {Array.get.go(T, a, n, i, z) == (a, Pair.snd(Array, T, Array.get.go(T, a, n, i, z))) : Array & T} 275 276 def get_go_eta(T, a, n, i, z): 277 match a z: 278 case ALeaf{x} _: 279 {==} 280 case ANode{xs, ys} True{}: 281 +h = U32.shr(n) 282 +z2 = U32.is_lt(i, U32.shr(h)) 283 %Equal.sym(Array & T, Array.get.go(T, xs, h, i, z2), 284 (xs, Pair.snd(Array, T, Array.get.go(T, xs, h, i, z2))), get_go_eta(T, xs, h, i, z2)) : 285 {Array.swap.lo(T, ys, _) == (ANode{xs, ys}, Pair.snd(Array, T, Array.swap.lo(T, ys, _))) : Array & T} 286 {==} 287 case ANode{xs, ys} False{}: 288 +h = U32.shr(n) 289 +j = U32.sub(i, h) 290 +z2 = U32.is_lt(j, U32.shr(h)) 291 %Equal.sym(Array & T, Array.get.go(T, ys, h, j, z2), 292 (ys, Pair.snd(Array, T, Array.get.go(T, ys, h, j, z2))), get_go_eta(T, ys, h, j, z2)) : 293 {Array.swap.hi(T, xs, _) == (ANode{xs, ys}, Pair.snd(Array, T, Array.swap.hi(T, xs, _))) : Array & T} 294 {==} 295 296 law get_pair_t: 297 for -T: Data 298 for +t: Tree 299 for +i: U32 300 {Array.get(T, fromT(T, t), i) == (fromT(T, t), Pair.snd(Array, T, Array.get(T, fromT(T, t), i))) : Array & T} 301 302 def get_pair_t(T, t, i): 303 %Equal.sym(Array & U32, Array.size(T, fromT(T, t)), (fromT(T, t), Pair.snd(Array, U32, Array.size(T, fromT(T, t)))), size_eta(T, fromT(T, t))) : 304 {Array.get.at(T, i, _) == (fromT(T, t), Pair.snd(Array, T, Array.get.at(T, i, _))) : Array & T} 305 +n = Pair.snd(Array, U32, Array.size(T, fromT(T, t))) 306 +j = U32.and(i, U32.sub(n, 1)) 307 get_go_eta(T, fromT(T, t), n, j, U32.is_lt(j, U32.shr(n))) 308 309 # Writing then reading the same index 310 # =================================== 311 312 # A swap keeps the left spine, so the size. 313 law sz_sw: 314 for -T: Data 315 for +t: Tree 316 for +n: U32 317 for +i: U32 318 for +v: T 319 for +z: Bool 320 {Array.size(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, t), n, i, v, z))) 321 == (Pair.fst(Array, T, Array.swap.go(T, fromT(T, t), n, i, v, z)), 322 Pair.snd(Array, U32, Array.size(T, fromT(T, t)))) : Array & U32} 323 324 def sz_sw(T, t, n, i, v, z): 325 match t z: 326 case TLeaf{x} _: 327 {==} 328 case TNode{l, r} True{}: 329 +h = U32.shr(n) 330 +z2 = U32.is_lt(i, U32.shr(h)) 331 %Equal.sym(Array, Pair.fst(Array, T, Array.swap.lo(T, fromT(T, r), Array.swap.go(T, fromT(T, l), h, i, v, z2))), 332 ANode{Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), fromT(T, r)}, 333 lo_fst(T, fromT(T, r), Array.swap.go(T, fromT(T, l), h, i, v, z2))) : 334 {Array.size(T, _) == (_, Pair.snd(Array, U32, Array.size(T, ANode{fromT(T, l), fromT(T, r)}))) : Array & U32} 335 %Equal.sym(Array & U32, Array.size(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2))), 336 (Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), Pair.snd(Array, U32, Array.size(T, fromT(T, l)))), 337 sz_sw(T, l, h, i, v, z2)) : 338 {Array.size.node(T, fromT(T, r), _) 339 == (ANode{Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), fromT(T, r)}, 340 Pair.snd(Array, U32, Array.size.node(T, fromT(T, r), Array.size(T, fromT(T, l))))) : Array & U32} 341 %Equal.sym(Array & U32, Array.size(T, fromT(T, l)), (fromT(T, l), Pair.snd(Array, U32, Array.size(T, fromT(T, l)))), 342 size_eta(T, fromT(T, l))) : 343 {(ANode{Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), fromT(T, r)}, 344 U32.shl(Pair.snd(Array, U32, Array.size(T, fromT(T, l))))) 345 == (ANode{Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), fromT(T, r)}, 346 Pair.snd(Array, U32, Array.size.node(T, fromT(T, r), _))) : Array & U32} 347 {==} 348 case TNode{l, r} False{}: 349 +h = U32.shr(n) 350 +j = U32.sub(i, h) 351 +z2 = U32.is_lt(j, U32.shr(h)) 352 %Equal.sym(Array, Pair.fst(Array, T, Array.swap.hi(T, fromT(T, l), Array.swap.go(T, fromT(T, r), h, j, v, z2))), 353 ANode{fromT(T, l), Pair.fst(Array, T, Array.swap.go(T, fromT(T, r), h, j, v, z2))}, 354 hi_fst(T, fromT(T, l), Array.swap.go(T, fromT(T, r), h, j, v, z2))) : 355 {Array.size(T, _) == (_, Pair.snd(Array, U32, Array.size(T, ANode{fromT(T, l), fromT(T, r)}))) : Array & U32} 356 %Equal.sym(Array & U32, Array.size(T, fromT(T, l)), (fromT(T, l), Pair.snd(Array, U32, Array.size(T, fromT(T, l)))), 357 size_eta(T, fromT(T, l))) : 358 {Array.size.node(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, r), h, j, v, z2)), _) 359 == (ANode{fromT(T, l), Pair.fst(Array, T, Array.swap.go(T, fromT(T, r), h, j, v, z2))}, 360 Pair.snd(Array, U32, Array.size.node(T, fromT(T, r), _))) : Array & U32} 361 {==} 362 363 # Reading where a swap wrote gives the written value (any tree). 364 law gss: 365 for -T: Data 366 for +t: Tree 367 for +n: U32 368 for +i: U32 369 for +v: T 370 for +z: Bool 371 {Pair.snd(Array, T, Array.get.go(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, t), n, i, v, z)), n, i, z)) == v : T} 372 373 def gss(T, t, n, i, v, z): 374 match t z: 375 case TLeaf{x} _: 376 {==} 377 case TNode{l, r} True{}: 378 +h = U32.shr(n) 379 +z2 = U32.is_lt(i, U32.shr(h)) 380 %Equal.sym(Array, Pair.fst(Array, T, Array.swap.lo(T, fromT(T, r), Array.swap.go(T, fromT(T, l), h, i, v, z2))), 381 ANode{Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), fromT(T, r)}, 382 lo_fst(T, fromT(T, r), Array.swap.go(T, fromT(T, l), h, i, v, z2))) : 383 {Pair.snd(Array, T, Array.get.go(T, _, n, i, True{})) == v : T} 384 %Equal.sym(T, Pair.snd(Array, T, Array.swap.lo(T, fromT(T, r), 385 Array.get.go(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), h, i, z2))), 386 Pair.snd(Array, T, Array.get.go(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), h, i, z2)), 387 lo_snd(T, fromT(T, r), Array.get.go(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), h, i, z2))) : 388 {_ == v : T} 389 gss(T, l, h, i, v, z2) 390 case TNode{l, r} False{}: 391 +h = U32.shr(n) 392 +j = U32.sub(i, h) 393 +z2 = U32.is_lt(j, U32.shr(h)) 394 %Equal.sym(Array, Pair.fst(Array, T, Array.swap.hi(T, fromT(T, l), Array.swap.go(T, fromT(T, r), h, j, v, z2))), 395 ANode{fromT(T, l), Pair.fst(Array, T, Array.swap.go(T, fromT(T, r), h, j, v, z2))}, 396 hi_fst(T, fromT(T, l), Array.swap.go(T, fromT(T, r), h, j, v, z2))) : 397 {Pair.snd(Array, T, Array.get.go(T, _, n, i, False{})) == v : T} 398 %Equal.sym(T, Pair.snd(Array, T, Array.swap.hi(T, fromT(T, l), 399 Array.get.go(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, r), h, j, v, z2)), h, j, z2))), 400 Pair.snd(Array, T, Array.get.go(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, r), h, j, v, z2)), h, j, z2)), 401 hi_snd(T, fromT(T, l), Array.get.go(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, r), h, j, v, z2)), h, j, z2))) : 402 {_ == v : T} 403 gss(T, r, h, j, v, z2) 404 405 law get_set_same_t: 406 for -T: Data 407 for +t: Tree 408 for +i: U32 409 for +v: T 410 {Pair.snd(Array, T, Array.get(T, Array.set(T, fromT(T, t), i, v), i)) == v : T} 411 412 def get_set_same_t(T, t, i, v): 413 +n = Pair.snd(Array, U32, Array.size(T, fromT(T, t))) 414 +j = U32.and(i, U32.sub(n, 1)) 415 +z = U32.is_lt(j, U32.shr(n)) 416 %Equal.sym(Array & U32, Array.size(T, fromT(T, t)), (fromT(T, t), n), size_eta(T, fromT(T, t))) : 417 {Pair.snd(Array, T, Array.get(T, Array.set.fin(T, Array.swap.at(T, i, v, _)), i)) == v : T} 418 %Equal.sym(Array, Array.set.fin(T, Array.swap.go(T, fromT(T, t), n, j, v, z)), 419 Pair.fst(Array, T, Array.swap.go(T, fromT(T, t), n, j, v, z)), 420 fin_fst(T, Array.swap.go(T, fromT(T, t), n, j, v, z))) : 421 {Pair.snd(Array, T, Array.get(T, _, i)) == v : T} 422 %Equal.sym(Array & U32, Array.size(T, Pair.fst(Array, T, Array.swap.go(T, fromT(T, t), n, j, v, z))), 423 (Pair.fst(Array, T, Array.swap.go(T, fromT(T, t), n, j, v, z)), n), sz_sw(T, t, n, j, v, z)) : 424 {Pair.snd(Array, T, Array.get.at(T, i, _)) == v : T} 425 gss(T, t, n, j, v, z) 426 427 # Perfect trees with the same leaves are equal 428 # ============================================ 429 430 law view_inj_t: 431 for -T: Data 432 for +d: Nat 433 for +ta: Tree 434 for +tb: Tree 435 for +ha: {D.full(T, fromT(T, ta), d) == True{} : Bool} 436 for +hb: {D.full(T, fromT(T, tb), d) == True{} : Bool} 437 for +he: {D.view(T, fromT(T, ta)) == D.view(T, fromT(T, tb)) : List<&2, T>} 438 {fromT(T, ta) == fromT(T, tb) : Array} 439 440 def view_inj_t(T, d, ta, tb, ha, hb, he): 441 match d ta tb: 442 case 0n TLeaf{x} TLeaf{y}: 443 %B.cons_inj_h(T, x, y, Nil{}, Nil{}, he) : {ALeaf{x} == ALeaf{_} : Array} 444 {==} 445 case 0n TLeaf{x} TNode{lb, rb}: 446 Empty.absurd({ALeaf{x} == ANode{fromT(T, lb), fromT(T, rb)} : Array}, B.false_ne_true(hb)) 447 case 0n TNode{la, ra} _: 448 Empty.absurd({ANode{fromT(T, la), fromT(T, ra)} == fromT(T, tb) : Array}, B.false_ne_true(ha)) 449 case 1n+p TLeaf{x} _: 450 Empty.absurd({ALeaf{x} == fromT(T, tb) : Array}, B.false_ne_true(ha)) 451 case 1n+p TNode{la, ra} TLeaf{y}: 452 Empty.absurd({ANode{fromT(T, la), fromT(T, ra)} == ALeaf{y} : Array}, B.false_ne_true(hb)) 453 case 1n+p TNode{la, ra} TNode{lb, rb}: 454 +VLa = D.view(T, fromT(T, la)) 455 +VRa = D.view(T, fromT(T, ra)) 456 +VLb = D.view(T, fromT(T, lb)) 457 +VRb = D.view(T, fromT(T, rb)) 458 +hla = B.and_true_l(D.full(T, fromT(T, la), p), D.full(T, fromT(T, ra), p), ha) 459 +hra = B.and_true_r(D.full(T, fromT(T, la), p), D.full(T, fromT(T, ra), p), ha) 460 +hlb = B.and_true_l(D.full(T, fromT(T, lb), p), D.full(T, fromT(T, rb), p), hb) 461 +hrb = B.and_true_r(D.full(T, fromT(T, lb), p), D.full(T, fromT(T, rb), p), hb) 462 +hl = Equal.trans(Nat, List.length(&2, T, VLa), Nat.pow(2n, p), List.length(&2, T, VLb), 463 view_length(T, p, la, hla), Equal.sym(Nat, List.length(&2, T, VLb), Nat.pow(2n, p), view_length(T, p, lb, hlb))) 464 +ll = B.append_inj_l(T, VLa, VLb, VRa, VRb, hl, he) 465 +he2 = B.subst(List<&2, T>, X => {List.append(&2, T, VLa, VRa) == List.append(&2, T, X, VRb) : List<&2, T>}, 466 VLb, VLa, Equal.sym(List<&2, T>, VLa, VLb, ll), he) 467 +rr = B.append_cancel_l(T, VLa, VRa, VRb, he2) 468 anode_eq(T, fromT(T, la), fromT(T, ra), fromT(T, lb), fromT(T, rb), 469 view_inj_t(T, p, la, lb, hla, hlb, ll), view_inj_t(T, p, ra, rb, hra, hrb, rr)) 470 471 law get_new_t: 472 for -T: Data 473 for +d: Nat 474 for +v: T 475 for +i: U32 476 {Pair.snd(Array, T, Array.get(T, Array.new(T, d, v), i)) == v : T} 477 478 def get_new_t(T, d, v, i): 479 +n = Pair.snd(Array, U32, Array.size(T, Array.new(T, d, v))) 480 +j = U32.and(i, U32.sub(n, 1)) 481 %Equal.sym(Array & U32, Array.size(T, Array.new(T, d, v)), (Array.new(T, d, v), n), 482 size_eta(T, Array.new(T, d, v))) : 483 {Pair.snd(Array, T, Array.get.at(T, i, _)) == v : T} 484 get_new_go(T, d, v, n, j, U32.is_lt(j, U32.shr(n)))