proofs/lib/array_ext.bend
bend-collections-laws-containers@1.0.0.0 · 72 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/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7
8# Two perfect mirror trees of the same depth with the same slot lists are
9# the same tree (the slots determine a perfect tree).
10
11def take_len(-A: Data, +xs: List<&2, A>) -> {SC.take(A, xs, SC.length(A, xs)) == xs : List<&2, A>}:
12 match xs:
13 case Nil{}:
14 {==}
15 case Con{+h, +t}:
16 LL.cons_cong(A, h, SC.take(A, t, SC.length(A, t)), t, take_len(A, t))
17
18def drop_zero(-A: Data, +xs: List<&2, A>) -> {SC.drop(A, xs, 0n) == xs : List<&2, A>}:
19 match xs:
20 case Nil{}:
21 {==}
22 case Con{h, t}:
23 {==}
24
25def take_app_len(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> {SC.take(A, SC.append(A, xs, ys), SC.length(A, xs)) == xs : List<&2, A>}:
26 Equal.trans(List<&2, A>, SC.take(A, SC.append(A, xs, ys), SC.length(A, xs)), SC.take(A, xs, SC.length(A, xs)), xs, LL.sc_take_append_left(A, xs, ys, SC.length(A, xs), N.le_refl(SC.length(A, xs))), take_len(A, xs))
27
28def drop_app_len(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> {SC.drop(A, SC.append(A, xs, ys), SC.length(A, xs)) == ys : List<&2, A>}:
29 match xs:
30 case Nil{}:
31 drop_zero(A, ys)
32 case Con{+h, +t}:
33 drop_app_len(A, t, ys)
34
35def split_eq(-A: Data, +a1: List<&2, A>, +b1: List<&2, A>, +a2: List<&2, A>, +b2: List<&2, A>, +el: {SC.length(A, a1) == SC.length(A, a2) : Nat}, +e: {SC.append(A, a1, b1) == SC.append(A, a2, b2) : List<&2, A>}) -> {a1 == a2 : List<&2, A>}:
36 +t1 = Equal.trans(List<&2, A>, a1, SC.take(A, SC.append(A, a1, b1), SC.length(A, a1)), SC.take(A, SC.append(A, a2, b2), SC.length(A, a1)), Equal.sym(List<&2, A>, SC.take(A, SC.append(A, a1, b1), SC.length(A, a1)), a1, take_app_len(A, a1, b1)), Equal.cong(List<&2, A>, List<&2, A>, z => SC.take(A, z, SC.length(A, a1)), SC.append(A, a1, b1), SC.append(A, a2, b2), e))
37 Equal.trans(List<&2, A>, a1, SC.take(A, SC.append(A, a2, b2), SC.length(A, a1)), a2, t1, L.subst(Nat, z => {SC.take(A, SC.append(A, a2, b2), z) == a2 : List<&2, A>}, SC.length(A, a2), SC.length(A, a1), Equal.sym(Nat, SC.length(A, a1), SC.length(A, a2), el), take_app_len(A, a2, b2)))
38
39def split_eq_r(-A: Data, +a1: List<&2, A>, +b1: List<&2, A>, +a2: List<&2, A>, +b2: List<&2, A>, +el: {SC.length(A, a1) == SC.length(A, a2) : Nat}, +e: {SC.append(A, a1, b1) == SC.append(A, a2, b2) : List<&2, A>}) -> {b1 == b2 : List<&2, A>}:
40 +t1 = Equal.trans(List<&2, A>, b1, SC.drop(A, SC.append(A, a1, b1), SC.length(A, a1)), SC.drop(A, SC.append(A, a2, b2), SC.length(A, a1)), Equal.sym(List<&2, A>, SC.drop(A, SC.append(A, a1, b1), SC.length(A, a1)), b1, drop_app_len(A, a1, b1)), Equal.cong(List<&2, A>, List<&2, A>, z => SC.drop(A, z, SC.length(A, a1)), SC.append(A, a1, b1), SC.append(A, a2, b2), e))
41 Equal.trans(List<&2, A>, b1, SC.drop(A, SC.append(A, a2, b2), SC.length(A, a1)), b2, t1, L.subst(Nat, z => {SC.drop(A, SC.append(A, a2, b2), z) == b2 : List<&2, A>}, SC.length(A, a2), SC.length(A, a1), Equal.sym(Nat, SC.length(A, a1), SC.length(A, a2), el), drop_app_len(A, a2, b2)))
42
43def head_of(-A: Data, xs: List<&2, A>, +d: A) -> A:
44 match xs:
45 case Nil{}:
46 d
47 case Con{h, t}:
48 h
49
50def tree_ext(-A: Data, +d: Nat, +u: AR.Tree<A>, +v: AR.Tree<A>, +pu: {AR.perfect(A, d, u) == True{} : Bool}, +pv: {AR.perfect(A, d, v) == True{} : Bool}, +e: {AR.slots(A, u) == AR.slots(A, v) : List<&2, A>}) -> {u == v : AR.Tree<A>}:
51 match d u v:
52 case 0n AR.TLeaf{+x} AR.TLeaf{+y}:
53 Equal.cong(A, AR.Tree<A>, z => AR.TLeaf{z}, x, y, Equal.cong(List<&2, A>, A, z => head_of(A, z, x), Con{x, Nil{}}, Con{y, Nil{}}, e))
54 case 0n AR.TLeaf{x} AR.TNode{l, r}:
55 Empty.absurd({AR.TLeaf{x} == AR.TNode{l, r} : AR.Tree<A>}, L.false_true(pv))
56 case 0n AR.TNode{l, r} _:
57 Empty.absurd({AR.TNode{l, r} == v : AR.Tree<A>}, L.false_true(pu))
58 case 1n+p AR.TLeaf{x} _:
59 Empty.absurd({AR.TLeaf{x} == v : AR.Tree<A>}, L.false_true(pu))
60 case 1n+p AR.TNode{l, r} AR.TLeaf{y}:
61 Empty.absurd({AR.TNode{l, r} == AR.TLeaf{y} : AR.Tree<A>}, L.false_true(pv))
62 case 1n+ +p AR.TNode{+l1, +r1} AR.TNode{+l2, +r2}:
63 +pl1 = AR.pf_left(A, p, l1, r1, pu)
64 +pr1 = AR.pf_right(A, p, l1, r1, pu)
65 +pl2 = AR.pf_left(A, p, l2, r2, pv)
66 +pr2 = AR.pf_right(A, p, l2, r2, pv)
67 +el = Equal.trans(Nat, SC.length(A, AR.slots(A, l1)), SC.pow2(p), SC.length(A, AR.slots(A, l2)), AR.slots_length(A, p, l1, pl1), Equal.sym(Nat, SC.length(A, AR.slots(A, l2)), SC.pow2(p), AR.slots_length(A, p, l2, pl2)))
68 +el2 = tree_ext(A, p, l1, l2, pl1, pl2, split_eq(A, AR.slots(A, l1), AR.slots(A, r1), AR.slots(A, l2), AR.slots(A, r2), el, e))
69 +er2 = tree_ext(A, p, r1, r2, pr1, pr2, split_eq_r(A, AR.slots(A, l1), AR.slots(A, r1), AR.slots(A, l2), AR.slots(A, r2), el, e))
70 %Equal.sym(AR.Tree<A>, l1, l2, el2) : {AR.TNode{_, r1} == AR.TNode{l2, r2} : AR.Tree<A>}
71 %Equal.sym(AR.Tree<A>, r1, r2, er2) : {AR.TNode{l2, _} == AR.TNode{l2, r2} : AR.Tree<A>}
72 {==}