def take_take

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/kdf/okm.bend:45

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

45def take_take(+xs: List<&2, U32>, +a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {List.take(&2, U32, List.take(&2, U32, xs, b), a) == List.take(&2, U32, xs, a) : List<&2, U32>}:
46  match xs a b:
47    case Nil{} _ _:
48      {==}
49    case +x <> +rest 0n _:
50      take_zero(List.take(&2, U32, x <> rest, b))
51    case x <> rest 1n+p 0n:
52      Empty.absurd({List.take(&2, U32, List.take(&2, U32, x <> rest, 0n), 1n+p) == List.take(&2, U32, x <> rest, 1n+p) : List<&2, U32>}, L.false_true(h))
53    case +x <> +rest 1n+ +p 1n+ +q:
54      %take_take(rest, p, q, h) : {x <> List.take(&2, U32, List.take(&2, U32, rest, q), p) == x <> _ : List<&2, U32>}
55      {==}