proofs/lib/two_list.bend

bend-collections-laws-math@1.0.0.0 · 62 lines · 7 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend as LL
4import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-math@1.0.0.0/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
10def zero_sub(+k: Nat) -> {Nat.sub(0n, k) == 0n : Nat}:
11  match k:
12    case 0n:
13      {==}
14    case 1n+p:
15      {==}
16
17def 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
26def 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
36def 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
48def 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
58def 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
61def 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)