def get_put_same

bend-kit-collections@0.1.4.1 · PROOF.bend:900

import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/omap.bend as O

900def get_put_same(
901  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp),
902  ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp),
903  t: O.OMap<K, V>, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V,
904  +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, ub) == True{} : Bool},
905  +ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool},
906  +eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}
907) -> {g(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, t, k, v), k) == Some{v} : Maybe<&2, V>}:
908  match t:
909    case O.OTip{}:
910      get.here(~K, ~V, ~cmp, ~refl, k, v, O.OTip{}, O.OTip{})
911    case O.OBin{+s, +key, +val, +lo, +hi}:
912      +b_l = bn.l(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt)
913      +b_h = bn.h(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt)
914      +plo = O.OMap.put(~K, ~V, ~cmp, lo, k, v)
915      +phi = O.OMap.put(~K, ~V, ~cmp, hi, k, v)
916      cmp.split(O.OMap<K, V>, Maybe<&2, V>, y => g(~K, ~V, ~cmp, y, k), Some{v},
917        cmp(k, key),
918        u => O.OMap.balance(K, V, key, val, O.OMap.put(~K, ~V, ~cmp, lo, k, v), hi),
919        u => O.OBin{s, key, v, lo, hi},
920        u => O.OMap.balance(K, V, key, val, lo, O.OMap.put(~K, ~V, ~cmp, hi, k, v)),
921        +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, plo, hi), k),
922          g(~K, ~V, ~cmp, O.OBin{0, key, val, plo, hi}, k), Some{v},
923          balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, plo, hi,
924            put.bnd(~K, ~V, ~cmp, ~flip, ~trans, lo, lb, Some{key}, k, v, b_l, ea,
925              lt_true(cmp(k, key), e)),
926            b_h),
927          mtr(V, g(~K, ~V, ~cmp, O.OBin{0, key, val, plo, hi}, k), g(~K, ~V, ~cmp, plo, k),
928            Some{v},
929            get.lt(~K, ~V, ~cmp, k, key, val, plo, hi, e),
930            get_put_same(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lo, lb, Some{key}, k, v,
931              b_l, ea, lt_true(cmp(k, key), e)))),
932        e => rw(Cmp, c => {getc(~K, ~V, ~cmp, c, k, v, lo, hi) == Some{v} : Maybe<&2, V>},
933          cmp(k, key), EQ{}, e, {==}),
934        +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, lo, phi), k),
935          g(~K, ~V, ~cmp, O.OBin{0, key, val, lo, phi}, k), Some{v},
936          balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, lo, phi,
937            b_l,
938            put.bnd(~K, ~V, ~cmp, ~flip, ~trans, hi, Some{key}, ub, k, v, b_h,
939              lt_true(cmp(key, k), gt_flip(~K, ~cmp, ~flip, k, key, e)), eb)),
940          mtr(V, g(~K, ~V, ~cmp, O.OBin{0, key, val, lo, phi}, k), g(~K, ~V, ~cmp, phi, k),
941            Some{v},
942            get.gt(~K, ~V, ~cmp, k, key, val, lo, phi, e),
943            get_put_same(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, hi, Some{key}, ub, k, v,
944              b_h, lt_true(cmp(key, k), gt_flip(~K, ~cmp, ~flip, k, key, e)), eb))))