def drop_all

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:72

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

72def drop_all(+xs: List<&2, U32>, +ys: List<&2, U32>, +n: Nat, +h: {SC.length(U32, xs) == n : Nat}) -> {SC.drop(U32, SC.append(U32, xs, ys), n) == ys : List<&2, U32>}:
73  match xs n:
74    case Nil{} 0n:
75      drop_zero(ys)
76    case Nil{} 1n+p:
77      Empty.absurd({SC.drop(U32, ys, 1n+p) == ys : List<&2, U32>}, N.zero_succ(p, h))
78    case Con{h1, t} 0n:
79      Empty.absurd({SC.drop(U32, SC.append(U32, Con{h1, t}, ys), 0n) == ys : List<&2, U32>}, N.succ_zero(SC.length(U32, t), h))
80    case Con{+h1, +t} 1n+ +p:
81      drop_all(t, ys, p, N.succ_inj(SC.length(U32, t), p, h))