1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/u32.bend as U
5	import ../../lib/array.bend as AR
6	import ../../lib/array_ext.bend as AX
7	import ../../lib/list.bend as LL
8	import ../../../spec/lib/common.bend as SC
9	
10	# The block of a list with a default: a perfect tree of depth d whose slots
11	# are the list's items followed by the default v. (mk.bend is the Maybe
12	# instance: items Some, default None.) The TreeMap's node store keeps one
13	# such block per node field.
14	
15	# the first k slots: the items xs, then v
16	def fillv(-T: Data, +k: Nat, xs: List<&2, T>, +v: T) -> List<&2, T>:
17	  match k xs:
18	    case 0n _:
19	      Nil{}
20	    case 1n+j Nil{}:
21	      Con{v, fillv(T, j, Nil{}, v)}
22	    case 1n+j Con{x, r}:
23	      Con{x, fillv(T, j, r, v)}
24	
25	def headv(-T: Data, xs: List<&2, T>, +v: T) -> T:
26	  match xs:
27	    case Nil{}:
28	      v
29	    case Con{x, r}:
30	      x
31	
32	def bk(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T) -> AR.Tree<T>:
33	  match d:
34	    case 0n:
35	      AR.TLeaf{headv(T, xs, v)}
36	    case 1n+p:
37	      AR.TNode{bk(T, p, xs, v), bk(T, p, SC.drop(T, xs, SC.pow2(p)), v)}
38	
39	def bk_perfect(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T) -> {AR.perfect(T, d, bk(T, d, xs, v)) == True{} : Bool}:
40	  match d:
41	    case 0n:
42	      {==}
43	    case 1n+p:
44	      L.and_intro(AR.perfect(T, p, bk(T, p, xs, v)), AR.perfect(T, p, bk(T, p, SC.drop(T, xs, SC.pow2(p)), v)), bk_perfect(T, p, xs, v), bk_perfect(T, p, SC.drop(T, xs, SC.pow2(p)), v))
45	
46	def fill_add(-T: Data, +a: Nat, +b: Nat, +xs: List<&2, T>, +v: T) -> {fillv(T, Nat.add(a, b), xs, v) == SC.append(T, fillv(T, a, xs, v), fillv(T, b, SC.drop(T, xs, a), v)) : List<&2, T>}:
47	  match a xs:
48	    case 0n _:
49	      Equal.cong(List<&2, T>, List<&2, T>, z => fillv(T, b, z, v), xs, SC.drop(T, xs, 0n), Equal.sym(List<&2, T>, SC.drop(T, xs, 0n), xs, AX.drop_zero(T, xs)))
50	    case 1n+j Nil{}:
51	      LL.cons_cong(T, v, fillv(T, Nat.add(j, b), Nil{}, v), SC.append(T, fillv(T, j, Nil{}, v), fillv(T, b, Nil{}, v)), fill_add(T, j, b, Nil{}, v))
52	    case 1n+j Con{+x, +r}:
53	      LL.cons_cong(T, x, fillv(T, Nat.add(j, b), r, v), SC.append(T, fillv(T, j, r, v), fillv(T, b, SC.drop(T, r, j), v)), fill_add(T, j, b, r, v))
54	
55	def dbl(+p: Nat) -> {SC.pow2(1n+p) == Nat.add(SC.pow2(p), SC.pow2(p)) : Nat}:
56	  Equal.trans(Nat, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), Nat.add(SC.pow2(p), 0n)), Nat.add(SC.pow2(p), SC.pow2(p)), U.double_pow(SC.pow2(p)), Equal.cong(Nat, Nat, z => Nat.add(SC.pow2(p), z), Nat.add(SC.pow2(p), 0n), SC.pow2(p), N.add_zero(SC.pow2(p))))
57	
58	def fill_one(-T: Data, +xs: List<&2, T>, +v: T) -> {fillv(T, 1n, xs, v) == Con{headv(T, xs, v), Nil{}} : List<&2, T>}:
59	  match xs:
60	    case Nil{}:
61	      {==}
62	    case Con{x, r}:
63	      {==}
64	
65	# the slots of the block
66	def bk_slots(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T) -> {AR.slots(T, bk(T, d, xs, v)) == fillv(T, SC.pow2(d), xs, v) : List<&2, T>}:
67	  match d:
68	    case 0n:
69	      Equal.sym(List<&2, T>, fillv(T, 1n, xs, v), Con{headv(T, xs, v), Nil{}}, fill_one(T, xs, v))
70	    case 1n+p:
71	      +P = SC.pow2(p)
72	      %Equal.sym(List<&2, T>, AR.slots(T, bk(T, p, xs, v)), fillv(T, P, xs, v), bk_slots(T, p, xs, v)) : {SC.append(T, _, AR.slots(T, bk(T, p, SC.drop(T, xs, P), v))) == fillv(T, SC.pow2(1n+p), xs, v) : List<&2, T>}
73	      %Equal.sym(List<&2, T>, AR.slots(T, bk(T, p, SC.drop(T, xs, P), v)), fillv(T, P, SC.drop(T, xs, P), v), bk_slots(T, p, SC.drop(T, xs, P), v)) : {SC.append(T, fillv(T, P, xs, v), _) == fillv(T, SC.pow2(1n+p), xs, v) : List<&2, T>}
74	      %Equal.sym(Nat, SC.pow2(1n+p), Nat.add(P, P), dbl(p)) : {SC.append(T, fillv(T, P, xs, v), fillv(T, P, SC.drop(T, xs, P), v)) == fillv(T, _, xs, v) : List<&2, T>}
75	      Equal.sym(List<&2, T>, fillv(T, Nat.add(P, P), xs, v), SC.append(T, fillv(T, P, xs, v), fillv(T, P, SC.drop(T, xs, P), v)), fill_add(T, P, P, xs, v))
76	
77	def fill_len(-T: Data, +k: Nat, +xs: List<&2, T>, +v: T) -> {SC.length(T, fillv(T, k, xs, v)) == k : Nat}:
78	  match k xs:
79	    case 0n _:
80	      {==}
81	    case 1n+j Nil{}:
82	      N.succ_cong(SC.length(T, fillv(T, j, Nil{}, v)), j, fill_len(T, j, Nil{}, v))
83	    case 1n+j Con{x, +r}:
84	      N.succ_cong(SC.length(T, fillv(T, j, r, v)), j, fill_len(T, j, r, v))
85	
86	# a slot below the length reads the item
87	def fill_nth(-T: Data, +k: Nat, +xs: List<&2, T>, +v: T, +i: Nat, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}, +hk: {Nat.is_le(SC.length(T, xs), k) == True{} : Bool}) -> {SC.nth(T, fillv(T, k, xs, v), i) == SC.nth(T, xs, i) : Maybe<&2, T>}:
88	  match k xs i:
89	    case 0n Nil{} _:
90	      Empty.absurd({SC.nth(T, Nil{}, i) == SC.nth(T, Nil{}, i) : Maybe<&2, T>}, N.lt_zero_absurd(i, h))
91	    case 0n Con{x, r} _:
92	      Empty.absurd({SC.nth(T, Nil{}, i) == SC.nth(T, Con{x, r}, i) : Maybe<&2, T>}, L.false_true(hk))
93	    case 1n+j Nil{} _:
94	      Empty.absurd({SC.nth(T, fillv(T, 1n+j, Nil{}, v), i) == SC.nth(T, Nil{}, i) : Maybe<&2, T>}, N.lt_zero_absurd(i, h))
95	    case 1n+j Con{x, r} 0n:
96	      {==}
97	    case 1n+j Con{x, +r} 1n+q:
98	      fill_nth(T, j, r, v, q, h, hk)
99	
100	def fill_upd(-T: Data, +k: Nat, +xs: List<&2, T>, +v: T, +i: Nat, +y: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> {SC.update(T, fillv(T, k, xs, v), i, y) == fillv(T, k, SC.update(T, xs, i, y), v) : List<&2, T>}:
101	  match k xs i:
102	    case 0n _ _:
103	      {==}
104	    case 1n+j Nil{} _:
105	      Empty.absurd({SC.update(T, fillv(T, 1n+j, Nil{}, v), i, y) == fillv(T, 1n+j, Nil{}, v) : List<&2, T>}, N.lt_zero_absurd(i, h))
106	    case 1n+j Con{x, r} 0n:
107	      {==}
108	    case 1n+j Con{+x, +r} 1n+q:
109	      LL.cons_cong(T, x, SC.update(T, fillv(T, j, r, v), q, y), fillv(T, j, SC.update(T, r, q, y), v), fill_upd(T, j, r, v, q, y, h))
110	
111	def fill_snoc(-T: Data, +k: Nat, +xs: List<&2, T>, +v: T, +y: T, +h: {Nat.is_lt(SC.length(T, xs), k) == True{} : Bool}) -> {SC.update(T, fillv(T, k, xs, v), SC.length(T, xs), y) == fillv(T, k, SC.snoc(T, xs, y), v) : List<&2, T>}:
112	  match k xs:
113	    case 0n _:
114	      Empty.absurd({SC.update(T, Nil{}, SC.length(T, xs), y) == Nil{} : List<&2, T>}, N.lt_zero_absurd(SC.length(T, xs), h))
115	    case 1n+j Nil{}:
116	      {==}
117	    case 1n+j Con{+x, +r}:
118	      LL.cons_cong(T, x, SC.update(T, fillv(T, j, r, v), SC.length(T, r), y), fillv(T, j, SC.snoc(T, r, y), v), fill_snoc(T, j, r, v, y, h))
119	
120	def fill_init_c(-T: Data, +j: Nat, +x: T, +r: List<&2, T>, +v: T, +m: Nat, +hm: {SC.length(T, Con{x, r}) == 1n+m : Nat}, ih: @+m2: Nat -> @+hm2: {SC.length(T, r) == 1n+m2 : Nat} -> {SC.update(T, fillv(T, j, r, v), m2, v) == fillv(T, j, SC.init(T, r), v) : List<&2, T>}) -> {SC.update(T, fillv(T, 1n+j, Con{x, r}, v), m, v) == fillv(T, 1n+j, SC.init(T, Con{x, r}), v) : List<&2, T>}:
121	  match r m:
122	    case Nil{} 0n:
123	      {==}
124	    case Nil{} 1n+q:
125	      Empty.absurd({SC.update(T, fillv(T, 1n+j, Con{x, Nil{}}, v), 1n+q, v) == fillv(T, 1n+j, SC.init(T, Con{x, Nil{}}), v) : List<&2, T>}, N.zero_succ(q, N.succ_inj(0n, 1n+q, hm)))
126	    case Con{y, t} 0n:
127	      Empty.absurd({SC.update(T, fillv(T, 1n+j, Con{x, Con{y, t}}, v), 0n, v) == fillv(T, 1n+j, SC.init(T, Con{x, Con{y, t}}), v) : List<&2, T>}, N.succ_zero(SC.length(T, t), N.succ_inj(1n+SC.length(T, t), 0n, hm)))
128	    case Con{+y, +t} 1n+q:
129	      LL.cons_cong(T, x, SC.update(T, fillv(T, j, Con{y, t}, v), q, v), fillv(T, j, SC.init(T, Con{y, t}), v), ih(q, N.succ_inj(1n+SC.length(T, t), 1n+q, hm)))
130	
131	# the last item reset to the default (a pop)
132	def fill_init(-T: Data, +k: Nat, +xs: List<&2, T>, +v: T, +m: Nat, +hm: {SC.length(T, xs) == 1n+m : Nat}) -> {SC.update(T, fillv(T, k, xs, v), m, v) == fillv(T, k, SC.init(T, xs), v) : List<&2, T>}:
133	  match k xs:
134	    case 0n _:
135	      {==}
136	    case 1n+j Nil{}:
137	      Empty.absurd({SC.update(T, fillv(T, 1n+j, Nil{}, v), m, v) == fillv(T, 1n+j, SC.init(T, Nil{}), v) : List<&2, T>}, N.zero_succ(m, hm))
138	    case 1n+j Con{+x, +r}:
139	      fill_init_c(T, j, x, r, v, m, hm, m2 => hm2 => fill_init(T, j, r, v, m2, hm2))
140	
141	# ---- trees equal to blocks ----
142	
143	def bk_eq(-T: Data, +d: Nat, +u: AR.Tree<T>, +xs: List<&2, T>, +v: T, +pu: {AR.perfect(T, d, u) == True{} : Bool}, +e: {AR.slots(T, u) == fillv(T, SC.pow2(d), xs, v) : List<&2, T>}) -> {u == bk(T, d, xs, v) : AR.Tree<T>}:
144	  AX.tree_ext(T, d, u, bk(T, d, xs, v), pu, bk_perfect(T, d, xs, v), Equal.trans(List<&2, T>, AR.slots(T, u), fillv(T, SC.pow2(d), xs, v), AR.slots(T, bk(T, d, xs, v)), e, Equal.sym(List<&2, T>, AR.slots(T, bk(T, d, xs, v)), fillv(T, SC.pow2(d), xs, v), bk_slots(T, d, xs, v))))
145	
146	def bk_upd(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T, +i: Nat, +y: T, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +ys: List<&2, T>, +hf: {SC.update(T, fillv(T, SC.pow2(d), xs, v), i, y) == fillv(T, SC.pow2(d), ys, v) : List<&2, T>}) -> {AR.upd(T, d, bk(T, d, xs, v), i, y) == bk(T, d, ys, v) : AR.Tree<T>}:
147	  +es = Equal.trans(List<&2, T>, AR.slots(T, AR.upd(T, d, bk(T, d, xs, v), i, y)), SC.update(T, AR.slots(T, bk(T, d, xs, v)), i, y), fillv(T, SC.pow2(d), ys, v), AR.upd_slots(T, d, bk(T, d, xs, v), i, y, hi, bk_perfect(T, d, xs, v)), Equal.trans(List<&2, T>, SC.update(T, AR.slots(T, bk(T, d, xs, v)), i, y), SC.update(T, fillv(T, SC.pow2(d), xs, v), i, y), fillv(T, SC.pow2(d), ys, v), Equal.cong(List<&2, T>, List<&2, T>, z => SC.update(T, z, i, y), AR.slots(T, bk(T, d, xs, v)), fillv(T, SC.pow2(d), xs, v), bk_slots(T, d, xs, v)), hf))
148	  bk_eq(T, d, AR.upd(T, d, bk(T, d, xs, v), i, y), ys, v, AR.upd_perfect(T, d, bk(T, d, xs, v), i, y, bk_perfect(T, d, xs, v)), es)
149	
150	# a slot written below the length
151	def bk_set(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T, +i: Nat, +y: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.upd(T, d, bk(T, d, xs, v), i, y) == bk(T, d, SC.update(T, xs, i, y), v) : AR.Tree<T>}:
152	  bk_upd(T, d, xs, v, i, y, N.lt_le_trans(i, SC.length(T, xs), SC.pow2(d), h, hc), SC.update(T, xs, i, y), fill_upd(T, SC.pow2(d), xs, v, i, y, h))
153	
154	# the slot at the length written (a push with room)
155	def bk_push(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T, +y: T, +h: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.upd(T, d, bk(T, d, xs, v), SC.length(T, xs), y) == bk(T, d, SC.snoc(T, xs, y), v) : AR.Tree<T>}:
156	  bk_upd(T, d, xs, v, SC.length(T, xs), y, h, SC.snoc(T, xs, y), fill_snoc(T, SC.pow2(d), xs, v, y, h))
157	
158	# the last slot reset to the default (a pop)
159	def bk_pop(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T, +m: Nat, +hm: {SC.length(T, xs) == 1n+m : Nat}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.upd(T, d, bk(T, d, xs, v), m, v) == bk(T, d, SC.init(T, xs), v) : AR.Tree<T>}:
160	  +hl = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(T, xs), 1n+m, hm, hc)
161	  bk_upd(T, d, xs, v, m, v, N.lt_le_trans(m, 1n+m, SC.pow2(d), N.lt_succ(m), hl), SC.init(T, xs), fill_init(T, SC.pow2(d), xs, v, m, hm))
162	
163	def fill_rep(-T: Data, +k: Nat, +v: T) -> {fillv(T, k, Nil{}, v) == SC.replicate(T, k, v) : List<&2, T>}:
164	  match k:
165	    case 0n:
166	      {==}
167	    case 1n+j:
168	      LL.cons_cong(T, v, fillv(T, j, Nil{}, v), SC.replicate(T, j, v), fill_rep(T, j, v))
169	
170	def drop_all(-T: Data, +xs: List<&2, T>, +k: Nat, +h: {Nat.is_le(SC.length(T, xs), k) == True{} : Bool}) -> {SC.drop(T, xs, k) == Nil{} : List<&2, T>}:
171	  match xs k:
172	    case Nil{} _:
173	      {==}
174	    case Con{x, r} 0n:
175	      Empty.absurd({Con{x, r} == Nil{} : List<&2, T>}, L.false_true(h))
176	    case Con{x, +r} 1n+j:
177	      drop_all(T, r, j, h)
178	
179	def bk_empty(-T: Data, +d: Nat, +v: T) -> {AR.trep(T, d, v) == bk(T, d, Nil{}, v) : AR.Tree<T>}:
180	  bk_eq(T, d, AR.trep(T, d, v), Nil{}, v, AR.trep_perfect(T, d, v), Equal.trans(List<&2, T>, AR.slots(T, AR.trep(T, d, v)), SC.replicate(T, SC.pow2(d), v), fillv(T, SC.pow2(d), Nil{}, v), AR.trep_slots(T, d, v), Equal.sym(List<&2, T>, fillv(T, SC.pow2(d), Nil{}, v), SC.replicate(T, SC.pow2(d), v), fill_rep(T, SC.pow2(d), v))))
181	
182	# the doubled block (the old block and a default half)
183	def bk_grow(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.TNode{bk(T, d, xs, v), AR.trep(T, d, v)} == bk(T, 1n+d, xs, v) : AR.Tree<T>}:
184	  +e1 = Equal.trans(AR.Tree<T>, AR.trep(T, d, v), bk(T, d, Nil{}, v), bk(T, d, SC.drop(T, xs, SC.pow2(d)), v), bk_empty(T, d, v), Equal.cong(List<&2, T>, AR.Tree<T>, z => bk(T, d, z, v), Nil{}, SC.drop(T, xs, SC.pow2(d)), Equal.sym(List<&2, T>, SC.drop(T, xs, SC.pow2(d)), Nil{}, drop_all(T, xs, SC.pow2(d), hc))))
185	  Equal.cong(AR.Tree<T>, AR.Tree<T>, z => AR.TNode{bk(T, d, xs, v), z}, AR.trep(T, d, v), bk(T, d, SC.drop(T, xs, SC.pow2(d)), v), e1)
186	
187	# the slot at the length (inside the capacity) holds the default
188	def fill_at_len(-T: Data, +k: Nat, +xs: List<&2, T>, +v: T, +h: {Nat.is_lt(SC.length(T, xs), k) == True{} : Bool}) -> {SC.nth(T, fillv(T, k, xs, v), SC.length(T, xs)) == Some{v} : Maybe<&2, T>}:
189	  match k xs:
190	    case 0n _:
191	      Empty.absurd({SC.nth(T, Nil{}, SC.length(T, xs)) == Some{v} : Maybe<&2, T>}, N.lt_zero_absurd(SC.length(T, xs), h))
192	    case 1n+j Nil{}:
193	      {==}
194	    case 1n+j Con{x, +r}:
195	      fill_at_len(T, j, r, v, h)