def length_take

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/list.bend:244

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

244def length_take(-A: Data, +xs: List<&2, A>, +k: Nat, +h: {Nat.is_le(k, SC.length(A, xs)) == True{} : Bool}) -> {SC.length(A, List.take(&2, A, xs, k)) == k : Nat}:
245  match xs k:
246    case Nil{} 0n:
247      {==}
248    case Nil{} 1n+p:
249      Empty.absurd({0n == 1n+p : Nat}, L.false_true(h))
250    case Con{x, t} 0n:
251      {==}
252    case Con{x, +t} 1n+p:
253      N.succ_cong(SC.length(A, List.take(&2, A, t, p)), p, length_take(A, t, p, h))