proofs/lib/two_list.bend source

proofs/lib/two_list.bend on the hub · documented module

import Baseimport ./nat.bend as Nimport ./list.bend as LLimport ../../spec/lib/common.bend as SCimport ../../src/containers/deque.bend as D# List facts for the two-list deque and queue: splitting a back list for a# rebalance, and the halving bound that keeps the moved half nonempty.def zero_sub(+k: Nat) -> {Nat.sub(0n, k) == 0n : Nat}:  match k:    case 0n:      {==}    case 1n+p:      {==}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>}:  match xs k:    case Nil{} _:      {==}    case Con{h, t} 0n:      {==}    case Con{h, t} 1n+p:      LL.cons_cong(T, h, SC.append(T, SC.take(T, t, p), SC.drop(T, t, p)), t, take_drop(T, t, p))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}:  match xs k:    case Nil{} _:      Equal.sym(Nat, Nat.sub(0n, k), 0n, zero_sub(k))    case Con{h, t} 0n:      Equal.sym(Nat, Nat.sub(1n+SC.length(T, t), 0n), 1n+SC.length(T, t), N.sub_zero(1n+SC.length(T, t)))    case Con{h, t} 1n+p:      len_drop(T, t, p)# the deque's split keeps the first n and reverses the restdef 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>}:  match n xs:    case 0n Nil{}:      {==}    case 0n Con{h, t}:      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}))    case 1n+p Nil{}:      {==}    case 1n+p Con{x, t}:      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))# half of a nonempty length is below itdef half_le(+n: Nat) -> {Nat.is_le(Nat.div(1n+n, 2n), n) == True{} : Bool}:  match n:    case 0n:      {==}    case 1n+0n:      {==}    case 1n+1n+k:      %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}      N.le_trans(1n+Nat.div(1n+k, 2n), 1n+k, 2n+k, half_le(k), N.le_succ(1n+k))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}:  LL.sc_length_take(T, xs, n, h)def len_rev(-T: Data, +xs: List<&2, T>) -> {SC.length(T, SC.reverse(T, xs)) == SC.length(T, xs) : Nat}:  LL.length_rev(T, xs)