proof_tree.bend

lawful-arrays@0.1.0.0 · 484 lines · 25 definitions

1import Base
2import lawful-arrays@0.1.0.0/defs.bend as D
3import lawful-arrays@0.1.0.0/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<T> 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<T> (a Data copy of the
11# shape and leaves) with fromT(t) == a; lemmas about fromT(t) may use t freely.
12
13type Tree<-T: Data> is Data:
14  TLeaf{x: T}
15  TNode{l: Tree<T>, r: Tree<T>}
16
17def fromT(-T: Data, t: Tree<T>) -> Array<T>:
18  match t:
19    case TLeaf{x}:
20      ALeaf{x}
21    case TNode{l, r}:
22      ANode{fromT(T, l), fromT(T, r)}
23
24def Mirror(-T: Data, -a: Array<T>) -> Data:
25  Sigma<&2, &2, Tree<T>, t => {fromT(T, t) == a : Array<T>}>
26
27law anode_eq:
28  for -T: Type
29  for -x1: Array<T>
30  for -x2: Array<T>
31  for -y1: Array<T>
32  for -y2: Array<T>
33  for e1: {x1 == y1 : Array<T>}
34  for e2: {x2 == y2 : Array<T>}
35  {ANode{x1, x2} == ANode{y1, y2} : Array<T>}
36
37def anode_eq(T, x1, x2, y1, y2, e1, e2):
38  %e1 : {ANode{x1, x2} == ANode{_, y2} : Array<T>}
39  %e2 : {ANode{x1, x2} == ANode{x1, _} : Array<T>}
40  {==}
41
42def mirror.node(-T: Data, -xs: Array<T>, -ys: Array<T>, 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
48def mirror(-T: Data, a: Array<T>) -> 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
58law lo_fst:
59  for -T: Type
60  for -ys: Array<T>
61  for r: Array<T> & T
62  {Pair.fst(Array<T>, T, Array.swap.lo(T, ys, r)) == ANode{Pair.fst(Array<T>, T, r), ys} : Array<T>}
63
64def lo_fst(T, ys, r):
65  (a, x) = r
66  {==}
67
68law lo_snd:
69  for -T: Type
70  for -ys: Array<T>
71  for r: Array<T> & T
72  {Pair.snd(Array<T>, T, Array.swap.lo(T, ys, r)) == Pair.snd(Array<T>, T, r) : T}
73
74def lo_snd(T, ys, r):
75  (a, x) = r
76  {==}
77
78law hi_fst:
79  for -T: Type
80  for -xs: Array<T>
81  for r: Array<T> & T
82  {Pair.fst(Array<T>, T, Array.swap.hi(T, xs, r)) == ANode{xs, Pair.fst(Array<T>, T, r)} : Array<T>}
83
84def hi_fst(T, xs, r):
85  (a, x) = r
86  {==}
87
88law hi_snd:
89  for -T: Type
90  for -xs: Array<T>
91  for r: Array<T> & T
92  {Pair.snd(Array<T>, T, Array.swap.hi(T, xs, r)) == Pair.snd(Array<T>, T, r) : T}
93
94def hi_snd(T, xs, r):
95  (a, x) = r
96  {==}
97
98law fin_fst:
99  for -T: Type
100  for r: Array<T> & T
101  {Array.set.fin(T, r) == Pair.fst(Array<T>, T, r) : Array<T>}
102
103def fin_fst(T, r):
104  (a, x) = r
105  {==}
106
107# Size
108# ====
109
110law size_eta:
111  for -T: Type
112  for a: Array<T>
113  {Array.size(T, a) == (a, Pair.snd(Array<T>, U32, Array.size(T, a))) : Array<T> & U32}
114
115def size_eta(T, a):
116  match a:
117    case ALeaf{x}:
118      {==}
119    case ANode{xs, ys}:
120      %Equal.sym(Array<T> & U32, Array.size(T, xs), (xs, Pair.snd(Array<T>, U32, Array.size(T, xs))),
121        size_eta(T, xs)) :
122        {Array.size.node(T, ys, _) == (ANode{xs, ys}, Pair.snd(Array<T>, U32, Array.size.node(T, ys, _))) : Array<T> & U32}
123      {==}
124
125law size_tree:
126  for -T: Data
127  for +d: Nat
128  for +t: Tree<T>
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<T> & U32}
131
132def 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<T> & 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<T> & U32},
141        B.false_ne_true(hf))
142    case 1n+p TNode{l, r}:
143      %Equal.sym(Array<T> & 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<T> & U32}
146      {==}
147
148# Leaves
149# ======
150
151law view_length:
152  for -T: Data
153  for +d: Nat
154  for +t: Tree<T>
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
158def 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
184law 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
190def 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
199law 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
205def 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
221law 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>, T, Array.get.go(T, Array.new(T, d, v), n, i, z)) == v : T}
229
230def 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>, 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>, 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>, 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>, 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
249law clone_pair:
250  for -T: Data
251  for a: Array<T>
252  {Array.clone(T, a) == (a, a) : Array<T> & Array<T>}
253
254def clone_pair(T, a):
255  match a:
256    case ALeaf{x}:
257      {==}
258    case ANode{xs, ys}:
259      %Equal.sym(Array<T> & Array<T>, 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<T> & Array<T>}
261      %Equal.sym(Array<T> & Array<T>, Array.clone(T, ys), (ys, ys), clone_pair(T, ys)) :
262        {Array.clone.node(T, (xs, xs), _) == (ANode{xs, ys}, ANode{xs, ys}) : Array<T> & Array<T>}
263      {==}
264
265# Reading hands the array back
266# ============================
267
268law get_go_eta:
269  for -T: Data
270  for a: Array<T>
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>, T, Array.get.go(T, a, n, i, z))) : Array<T> & T}
275
276def 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> & T, Array.get.go(T, xs, h, i, z2),
284        (xs, Pair.snd(Array<T>, 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>, T, Array.swap.lo(T, ys, _))) : Array<T> & 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> & T, Array.get.go(T, ys, h, j, z2),
292        (ys, Pair.snd(Array<T>, 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>, T, Array.swap.hi(T, xs, _))) : Array<T> & T}
294      {==}
295
296law get_pair_t:
297  for -T: Data
298  for +t: Tree<T>
299  for +i: U32
300  {Array.get(T, fromT(T, t), i) == (fromT(T, t), Pair.snd(Array<T>, T, Array.get(T, fromT(T, t), i))) : Array<T> & T}
301
302def get_pair_t(T, t, i):
303  %Equal.sym(Array<T> & U32, Array.size(T, fromT(T, t)), (fromT(T, t), Pair.snd(Array<T>, 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>, T, Array.get.at(T, i, _))) : Array<T> & T}
305  +n = Pair.snd(Array<T>, 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.
313law sz_sw:
314  for -T: Data
315  for +t: Tree<T>
316  for +n: U32
317  for +i: U32
318  for +v: T
319  for +z: Bool
320  {Array.size(T, Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, t), n, i, v, z)))
321    == (Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, t), n, i, v, z)),
322        Pair.snd(Array<T>, U32, Array.size(T, fromT(T, t)))) : Array<T> & U32}
323
324def 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<T>, Pair.fst(Array<T>, 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>, 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<T>, U32, Array.size(T, ANode{fromT(T, l), fromT(T, r)}))) : Array<T> & U32}
335      %Equal.sym(Array<T> & U32, Array.size(T, Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, l), h, i, v, z2))),
336        (Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), Pair.snd(Array<T>, 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>, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), fromT(T, r)},
340              Pair.snd(Array<T>, U32, Array.size.node(T, fromT(T, r), Array.size(T, fromT(T, l))))) : Array<T> & U32}
341      %Equal.sym(Array<T> & U32, Array.size(T, fromT(T, l)), (fromT(T, l), Pair.snd(Array<T>, U32, Array.size(T, fromT(T, l)))),
342        size_eta(T, fromT(T, l))) :
343        {(ANode{Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), fromT(T, r)},
344          U32.shl(Pair.snd(Array<T>, U32, Array.size(T, fromT(T, l)))))
345          == (ANode{Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), fromT(T, r)},
346              Pair.snd(Array<T>, U32, Array.size.node(T, fromT(T, r), _))) : Array<T> & 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<T>, Pair.fst(Array<T>, 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>, 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<T>, U32, Array.size(T, ANode{fromT(T, l), fromT(T, r)}))) : Array<T> & U32}
356      %Equal.sym(Array<T> & U32, Array.size(T, fromT(T, l)), (fromT(T, l), Pair.snd(Array<T>, U32, Array.size(T, fromT(T, l)))),
357        size_eta(T, fromT(T, l))) :
358        {Array.size.node(T, Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, r), h, j, v, z2)), _)
359          == (ANode{fromT(T, l), Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, r), h, j, v, z2))},
360              Pair.snd(Array<T>, U32, Array.size.node(T, fromT(T, r), _))) : Array<T> & U32}
361      {==}
362
363# Reading where a swap wrote gives the written value (any tree).
364law gss:
365  for -T: Data
366  for +t: Tree<T>
367  for +n: U32
368  for +i: U32
369  for +v: T
370  for +z: Bool
371  {Pair.snd(Array<T>, T, Array.get.go(T, Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, t), n, i, v, z)), n, i, z)) == v : T}
372
373def 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<T>, Pair.fst(Array<T>, 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>, 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>, T, Array.get.go(T, _, n, i, True{})) == v : T}
384      %Equal.sym(T, Pair.snd(Array<T>, T, Array.swap.lo(T, fromT(T, r),
385          Array.get.go(T, Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, l), h, i, v, z2)), h, i, z2))),
386        Pair.snd(Array<T>, T, Array.get.go(T, Pair.fst(Array<T>, 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>, 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<T>, Pair.fst(Array<T>, 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>, 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>, T, Array.get.go(T, _, n, i, False{})) == v : T}
398      %Equal.sym(T, Pair.snd(Array<T>, T, Array.swap.hi(T, fromT(T, l),
399          Array.get.go(T, Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, r), h, j, v, z2)), h, j, z2))),
400        Pair.snd(Array<T>, T, Array.get.go(T, Pair.fst(Array<T>, 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>, 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
405law get_set_same_t:
406  for -T: Data
407  for +t: Tree<T>
408  for +i: U32
409  for +v: T
410  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, fromT(T, t), i, v), i)) == v : T}
411
412def get_set_same_t(T, t, i, v):
413  +n = Pair.snd(Array<T>, 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<T> & U32, Array.size(T, fromT(T, t)), (fromT(T, t), n), size_eta(T, fromT(T, t))) :
417    {Pair.snd(Array<T>, T, Array.get(T, Array.set.fin(T, Array.swap.at(T, i, v, _)), i)) == v : T}
418  %Equal.sym(Array<T>, Array.set.fin(T, Array.swap.go(T, fromT(T, t), n, j, v, z)),
419    Pair.fst(Array<T>, 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>, T, Array.get(T, _, i)) == v : T}
422  %Equal.sym(Array<T> & U32, Array.size(T, Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, t), n, j, v, z))),
423    (Pair.fst(Array<T>, 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>, 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
430law view_inj_t:
431  for -T: Data
432  for +d: Nat
433  for +ta: Tree<T>
434  for +tb: Tree<T>
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<T>}
439
440def 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<T>}
444      {==}
445    case 0n TLeaf{x} TNode{lb, rb}:
446      Empty.absurd({ALeaf{x} == ANode{fromT(T, lb), fromT(T, rb)} : Array<T>}, 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<T>}, B.false_ne_true(ha))
449    case 1n+p TLeaf{x} _:
450      Empty.absurd({ALeaf{x} == fromT(T, tb) : Array<T>}, 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<T>}, 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
471law get_new_t:
472  for -T: Data
473  for +d: Nat
474  for +v: T
475  for +i: U32
476  {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}
477
478def get_new_t(T, d, v, i):
479  +n = Pair.snd(Array<T>, U32, Array.size(T, Array.new(T, d, v)))
480  +j = U32.and(i, U32.sub(n, 1))
481  %Equal.sym(Array<T> & 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>, T, Array.get.at(T, i, _)) == v : T}
484  get_new_go(T, d, v, n, j, U32.is_lt(j, U32.shr(n)))