def nth_put

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/shuffle.bend:66

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend as R

66# writing y at i keeps an element y at j
67def nth_put(-A: Data, +xs: List<&2, A>, +i: Nat, +j: Nat, +y: A, +h: {R.nth(A, xs, j) == Some{y} : Maybe<&2, A>}) -> {R.nth(A, R.put(A, xs, i, y), j) == Some{y} : Maybe<&2, A>}:
68  match xs i j:
69    case Nil{} _ _:
70      Empty.absurd({R.nth(A, R.put(A, Nil{}, i, y), j) == Some{y} : Maybe<&2, A>}, none_some(A, y, h))
71    case Con{+hd, +t} 0n 0n:
72      {==}
73    case Con{+hd, +t} 0n 1n+q:
74      h
75    case Con{+hd, +t} 1n+r 0n:
76      h
77    case Con{+hd, +t} 1n+r 1n+q:
78      nth_put(A, t, r, q, y, h)