proofs/containers/deque/rebalance.bend
bend-collections-laws-containers@1.0.0.0 · 125 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/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/arith.bend as AR
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/two_list.bend as TL
8import bend-collections-laws-containers@1.0.0.0/src/containers/deque.bend as DQ
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/state.bend as ST
10
11# Rebalancing: ready_front / ready_back move half of the other list over.
12# They keep the model, and leave the requested end nonempty unless the whole
13# deque is empty.
14
15def is_nil(-T: Data, xs: List<&2, T>) -> Bool:
16 match xs:
17 case Nil{}:
18 True{}
19 case Con{h, t}:
20 False{}
21
22# the front can be read: nonempty, or the deque is empty
23def rdy_f(-T: Data, sh: ST.Shadow<T>) -> Bool:
24 match sh:
25 case ST.Sh{Nil{}, b}:
26 is_nil(T, b)
27 case ST.Sh{Con{x, f}, b}:
28 True{}
29
30# the back can be read: nonempty, or the deque is empty
31def rdy_b(-T: Data, sh: ST.Shadow<T>) -> Bool:
32 match sh:
33 case ST.Sh{f, Nil{}}:
34 is_nil(T, f)
35 case ST.Sh{f, Con{x, b}}:
36 True{}
37
38def RF(~T: Data, sh: ST.Shadow<T>) -> Type:
39 Sigma<&1, &1, ST.Shadow<T>, sh1 => {DQ.ready_front(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque<T>} & ({ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>} & {rdy_f(T, sh1) == True{} : Bool})>
40
41def RB(~T: Data, sh: ST.Shadow<T>) -> Type:
42 Sigma<&1, &1, ST.Shadow<T>, sh1 => {DQ.ready_back(~T, ST.real(T, sh)) == ST.real(T, sh1) : DQ.Deque<T>} & ({ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>} & {rdy_b(T, sh1) == True{} : Bool})>
43
44def sub_pos(+n: Nat, +h: Nat, +lt: {Nat.is_lt(h, n) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.sub(n, h)) == True{} : Bool}:
45 match n h:
46 case 0n _:
47 Empty.absurd({Nat.is_lt(0n, Nat.sub(0n, h)) == True{} : Bool}, N.lt_zero_absurd(h, lt))
48 case 1n+m 0n:
49 {==}
50 case 1n+m 1n+k:
51 sub_pos(m, k, lt)
52
53def rdy_f_len(-T: Data, +m: List<&2, T>, +k: List<&2, T>, +h: {Nat.is_lt(0n, SC.length(T, m)) == True{} : Bool}) -> {rdy_f(T, ST.Sh{m, k}) == True{} : Bool}:
54 match m:
55 case Nil{}:
56 Empty.absurd({rdy_f(T, ST.Sh{Nil{}, k}) == True{} : Bool}, L.false_true(h))
57 case Con{x, t}:
58 {==}
59
60def rdy_b_len(-T: Data, +k: List<&2, T>, +m: List<&2, T>, +h: {Nat.is_lt(0n, SC.length(T, m)) == True{} : Bool}) -> {rdy_b(T, ST.Sh{k, m}) == True{} : Bool}:
61 match m:
62 case Nil{}:
63 Empty.absurd({rdy_b(T, ST.Sh{k, Nil{}}) == True{} : Bool}, L.false_true(h))
64 case Con{x, t}:
65 {==}
66
67# the split of a nonempty list at half its length: lengths of the two parts
68def half_lt(-T: Data, +y: T, +t: List<&2, T>) -> {Nat.is_lt(Nat.div(SC.length(T, Con{y, t}), 2n), SC.length(T, Con{y, t})) == True{} : Bool}:
69 N.le_lt_succ(Nat.div(1n+SC.length(T, t), 2n), SC.length(T, t), TL.half_le(SC.length(T, t)))
70
71def moved_len(-T: Data, +b: List<&2, T>, +h: Nat) -> {SC.length(T, SC.reverse(T, SC.drop(T, b, h))) == Nat.sub(SC.length(T, b), h) : Nat}:
72 Equal.trans(Nat, SC.length(T, SC.reverse(T, SC.drop(T, b, h))), SC.length(T, SC.drop(T, b, h)), Nat.sub(SC.length(T, b), h), TL.len_rev(T, SC.drop(T, b, h)), TL.len_drop(T, b, h))
73
74def kept_len(-T: Data, +b: List<&2, T>, +h: Nat, +hl: {Nat.is_le(h, SC.length(T, b)) == True{} : Bool}) -> {SC.length(T, SC.take(T, b, h)) == h : Nat}:
75 TL.len_take(T, b, h, hl)
76
77def rf_move(~T: Data, +y: T, +t: List<&2, T>) -> RF(~T, ST.Sh{Nil{}, Con{y, t}}):
78 +b = {Con{y, t} : List<&2, T>}
79 +n = SC.length(T, b)
80 +h = Nat.div(n, 2n)
81 +kk = SC.take(T, b, h)
82 +mm = SC.reverse(T, SC.drop(T, b, h))
83 +hlt = half_lt(T, y, t)
84 +e1 = Equal.cong(List<&2, T> & List<&2, T>, DQ.Deque<T>, r => DQ.front_split(~T, n, h, r), DQ.split(~T, h, b), (kk, mm), TL.split_eq(~T, h, b))
85 +e2 = Equal.cong(Nat, DQ.Deque<T>, z => DQ.DE{mm, kk, z, h}, Nat.sub(n, h), SC.length(T, mm), Equal.sym(Nat, SC.length(T, mm), Nat.sub(n, h), moved_len(T, b, h)))
86 +e3 = Equal.cong(Nat, DQ.Deque<T>, z => DQ.DE{mm, kk, SC.length(T, mm), z}, h, SC.length(T, kk), Equal.sym(Nat, SC.length(T, kk), h, kept_len(T, b, h, N.lt_le(h, n, hlt))))
87 +em = Equal.trans(List<&2, T>, SC.append(T, mm, SC.reverse(T, kk)), SC.reverse(T, SC.append(T, kk, SC.drop(T, b, h))), SC.reverse(T, b),
88 Equal.sym(List<&2, T>, SC.reverse(T, SC.append(T, kk, SC.drop(T, b, h))), SC.append(T, mm, SC.reverse(T, kk)), LL.rev_append(T, kk, SC.drop(T, b, h))),
89 Equal.cong(List<&2, T>, List<&2, T>, z => SC.reverse(T, z), SC.append(T, kk, SC.drop(T, b, h)), b, TL.take_drop(T, b, h)))
90 +hr = rdy_f_len(T, mm, kk, L.subst(Nat, z => {Nat.is_lt(0n, z) == True{} : Bool}, Nat.sub(n, h), SC.length(T, mm), Equal.sym(Nat, SC.length(T, mm), Nat.sub(n, h), moved_len(T, b, h)), sub_pos(n, h, hlt)))
91 (ST.Sh{mm, kk}, (Equal.trans(DQ.Deque<T>, DQ.front_split(~T, n, h, DQ.split(~T, h, b)), DQ.DE{mm, kk, Nat.sub(n, h), h}, ST.real(T, ST.Sh{mm, kk}), e1, Equal.trans(DQ.Deque<T>, DQ.DE{mm, kk, Nat.sub(n, h), h}, DQ.DE{mm, kk, SC.length(T, mm), h}, ST.real(T, ST.Sh{mm, kk}), e2, e3)), (em, hr)))
92
93def rb_move(~T: Data, +y: T, +t: List<&2, T>) -> RB(~T, ST.Sh{Con{y, t}, Nil{}}):
94 +f = {Con{y, t} : List<&2, T>}
95 +n = SC.length(T, f)
96 +h = Nat.div(n, 2n)
97 +kk = SC.take(T, f, h)
98 +mm = SC.reverse(T, SC.drop(T, f, h))
99 +hlt = half_lt(T, y, t)
100 +e1 = Equal.cong(List<&2, T> & List<&2, T>, DQ.Deque<T>, r => DQ.back_split(~T, n, h, r), DQ.split(~T, h, f), (kk, mm), TL.split_eq(~T, h, f))
101 +e2 = Equal.cong(Nat, DQ.Deque<T>, z => DQ.DE{kk, mm, z, Nat.sub(n, h)}, h, SC.length(T, kk), Equal.sym(Nat, SC.length(T, kk), h, kept_len(T, f, h, N.lt_le(h, n, hlt))))
102 +e3 = Equal.cong(Nat, DQ.Deque<T>, z => DQ.DE{kk, mm, SC.length(T, kk), z}, Nat.sub(n, h), SC.length(T, mm), Equal.sym(Nat, SC.length(T, mm), Nat.sub(n, h), moved_len(T, f, h)))
103 +em = Equal.trans(List<&2, T>, SC.append(T, kk, SC.reverse(T, mm)), SC.append(T, kk, SC.drop(T, f, h)), SC.append(T, f, Nil{}),
104 Equal.cong(List<&2, T>, List<&2, T>, z => SC.append(T, kk, z), SC.reverse(T, mm), SC.drop(T, f, h), LL.spec_rev_rev(T, SC.drop(T, f, h))),
105 Equal.trans(List<&2, T>, SC.append(T, kk, SC.drop(T, f, h)), f, SC.append(T, f, Nil{}), TL.take_drop(T, f, h), Equal.sym(List<&2, T>, SC.append(T, f, Nil{}), f, LL.append_nil(T, f))))
106 +hr = rdy_b_len(T, kk, mm, L.subst(Nat, z => {Nat.is_lt(0n, z) == True{} : Bool}, Nat.sub(n, h), SC.length(T, mm), Equal.sym(Nat, SC.length(T, mm), Nat.sub(n, h), moved_len(T, f, h)), sub_pos(n, h, hlt)))
107 (ST.Sh{kk, mm}, (Equal.trans(DQ.Deque<T>, DQ.back_split(~T, n, h, DQ.split(~T, h, f)), DQ.DE{kk, mm, h, Nat.sub(n, h)}, ST.real(T, ST.Sh{kk, mm}), e1, Equal.trans(DQ.Deque<T>, DQ.DE{kk, mm, h, Nat.sub(n, h)}, DQ.DE{kk, mm, SC.length(T, kk), Nat.sub(n, h)}, ST.real(T, ST.Sh{kk, mm}), e2, e3)), (em, hr)))
108
109def ready_front(~T: Data, +sh: ST.Shadow<T>) -> RF(~T, sh):
110 match sh:
111 case ST.Sh{Con{x, f}, b}:
112 (ST.Sh{Con{x, f}, b}, ({==}, ({==}, {==})))
113 case ST.Sh{Nil{}, Nil{}}:
114 (ST.Sh{Nil{}, Nil{}}, ({==}, ({==}, {==})))
115 case ST.Sh{Nil{}, Con{y, t}}:
116 rf_move(~T, y, t)
117
118def ready_back(~T: Data, +sh: ST.Shadow<T>) -> RB(~T, sh):
119 match sh:
120 case ST.Sh{f, Con{x, b}}:
121 (ST.Sh{f, Con{x, b}}, ({==}, ({==}, {==})))
122 case ST.Sh{Nil{}, Nil{}}:
123 (ST.Sh{Nil{}, Nil{}}, ({==}, ({==}, {==})))
124 case ST.Sh{Con{y, t}, Nil{}}:
125 rb_move(~T, y, t)