def splice_app_left

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

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/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

489def splice_app_left(+ws: List<&2, U32>, +i: Nat, +X: List<&2, U32>, +P: List<&2, U32>, +h: {Nat.is_le(Nat.add(i, SC.length(U32, ws)), SC.length(U32, X)) == True{} : Bool}) -> {splice(ws, i, SC.append(U32, X, P)) == SC.append(U32, splice(ws, i, X), P) : List<&2, U32>}:
490  match ws:
491    case Nil{}:
492      {==}
493    case +w <> +rest:
494      +hi = N.lt_le_trans(i, Nat.add(i, 1n+SC.length(U32, rest)), SC.length(U32, X), lt_add_succ(i, SC.length(U32, rest)), h)
495      +X2 = SC.update(U32, X, i, w)
496      +h2 = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), z) == True{} : Bool}, SC.length(U32, X), SC.length(U32, X2), Equal.sym(Nat, SC.length(U32, X2), SC.length(U32, X), LL.length_update(U32, X, i, w)),
497        L.subst(Nat, z => {Nat.is_le(z, SC.length(U32, X)) == True{} : Bool}, Nat.add(i, 1n+SC.length(U32, rest)), Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Equal.sym(Nat, Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Nat.add(i, 1n+SC.length(U32, rest)), add_one_assoc(i, SC.length(U32, rest))), h))
498      %Equal.sym(List<&2, U32>, SC.update(U32, SC.append(U32, X, P), i, w), SC.append(U32, X2, P), LL.update_append_left(U32, X, P, i, w, hi)) : {splice(rest, Nat.add(i, 1n), _) == SC.append(U32, splice(rest, Nat.add(i, 1n), X2), P) : List<&2, U32>}
499      splice_app_left(rest, Nat.add(i, 1n), X2, P, h2)