def split_eq

bend-collections-laws-math@1.0.0.0 · proofs/lib/two_list.bend:35

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-math@1.0.0.0/src/containers/deque.bend as D

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))