def sc_take_split

bend-collections-laws-math@1.0.0.0 · proofs/lib/list.bend:356

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC

356def sc_take_split(-A: Data, +xs: List<&2, A>, +l: Nat, +r: Nat, +h: {Nat.is_le(l, r) == True{} : Bool}) -> {SC.take(A, xs, r) == SC.append(A, SC.take(A, xs, l), SC.take(A, SC.drop(A, xs, l), Nat.sub(r, l))) : List<&2, A>}:
357  match xs l r:
358    case Nil{} _ _:
359      {==}
360    case Con{a, t} 0n r:
361      %Equal.sym(Nat, Nat.sub(r, 0n), r, sub_zero_eq(r)) : {SC.take(A, Con{a, t}, r) == SC.take(A, Con{a, t}, _) : List<&2, A>}
362      {==}
363    case Con{a, t} 1n+k 0n:
364      Empty.absurd({SC.take(A, Con{a, t}, 0n) == SC.append(A, SC.take(A, Con{a, t}, 1n+k), SC.take(A, SC.drop(A, Con{a, t}, 1n+k), Nat.sub(0n, 1n+k))) : List<&2, A>}, L.false_true(h))
365    case Con{a, t} 1n+k 1n+s:
366      cons_cong(A, a, SC.take(A, t, s), SC.append(A, SC.take(A, t, k), SC.take(A, SC.drop(A, t, k), Nat.sub(s, k))), sc_take_split(A, t, k, s, h))