1	import Base
2	import ./nat.bend as N
3	import ./list.bend as LL
4	import ../../spec/lib/common.bend as SC
5	import ../../src/containers/deque.bend as D
6	
7	# List facts for the two-list deque and queue: splitting a back list for a
8	# rebalance, and the halving bound that keeps the moved half nonempty.
9	
10	def zero_sub(+k: Nat) -> {Nat.sub(0n, k) == 0n : Nat}:
11	  match k:
12	    case 0n:
13	      {==}
14	    case 1n+p:
15	      {==}
16	
17	def take_drop(-T: Data, +xs: List<&2, T>, +k: Nat) -> {SC.append(T, SC.take(T, xs, k), SC.drop(T, xs, k)) == xs : List<&2, T>}:
18	  match xs k:
19	    case Nil{} _:
20	      {==}
21	    case Con{h, t} 0n:
22	      {==}
23	    case Con{h, t} 1n+p:
24	      LL.cons_cong(T, h, SC.append(T, SC.take(T, t, p), SC.drop(T, t, p)), t, take_drop(T, t, p))
25	
26	def len_drop(-T: Data, +xs: List<&2, T>, +k: Nat) -> {SC.length(T, SC.drop(T, xs, k)) == Nat.sub(SC.length(T, xs), k) : Nat}:
27	  match xs k:
28	    case Nil{} _:
29	      Equal.sym(Nat, Nat.sub(0n, k), 0n, zero_sub(k))
30	    case Con{h, t} 0n:
31	      Equal.sym(Nat, Nat.sub(1n+SC.length(T, t), 0n), 1n+SC.length(T, t), N.sub_zero(1n+SC.length(T, t)))
32	    case Con{h, t} 1n+p:
33	      len_drop(T, t, p)
34	
35	# the deque's split keeps the first n and reverses the rest
36	def split_eq(~T: Data, +n: Nat, +xs: List<&2, T>) -> {D.split(~T, n, xs) == (SC.take(T, xs, n), SC.reverse(T, SC.drop(T, xs, n))) : List<&2, T> & List<&2, T>}:
37	  match n xs:
38	    case 0n Nil{}:
39	      {==}
40	    case 0n Con{h, t}:
41	      Equal.cong(List<&2, T>, List<&2, T> & List<&2, T>, r => (Nil{}, r), List.reverse(&2, T, Con{h, t}), SC.reverse(T, Con{h, t}), LL.base_rev(T, Con{h, t}))
42	    case 1n+p Nil{}:
43	      {==}
44	    case 1n+p Con{x, t}:
45	      Equal.cong(List<&2, T> & List<&2, T>, List<&2, T> & List<&2, T>, r => D.split_cons(~T, x, r), D.split(~T, p, t), (SC.take(T, t, p), SC.reverse(T, SC.drop(T, t, p))), split_eq(~T, p, t))
46	
47	# half of a nonempty length is below it
48	def half_le(+n: Nat) -> {Nat.is_le(Nat.div(1n+n, 2n), n) == True{} : Bool}:
49	  match n:
50	    case 0n:
51	      {==}
52	    case 1n+0n:
53	      {==}
54	    case 1n+1n+k:
55	      %Equal.sym(Nat, Nat.div(Nat.add(2n, 1n+k), 2n), 1n+Nat.div(1n+k, 2n), N.div2_step(1n+k)) : {Nat.is_le(_, 2n+k) == True{} : Bool}
56	      N.le_trans(1n+Nat.div(1n+k, 2n), 1n+k, 2n+k, half_le(k), N.le_succ(1n+k))
57	
58	def len_take(-T: Data, +xs: List<&2, T>, +n: Nat, +h: {Nat.is_le(n, SC.length(T, xs)) == True{} : Bool}) -> {SC.length(T, SC.take(T, xs, n)) == n : Nat}:
59	  LL.sc_length_take(T, xs, n, h)
60	
61	def len_rev(-T: Data, +xs: List<&2, T>) -> {SC.length(T, SC.reverse(T, xs)) == SC.length(T, xs) : Nat}:
62	  LL.length_rev(T, xs)