proofs/lib/two_list.bend
bend-collections-laws-containers@1.0.0.0 · 62 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@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)