def get_put_other

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

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

974def get_put_other(
975  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp),
976  ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp),
977  t: O.OMap<K, V>, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k2: K, +k: K, +v: V,
978  +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, ub) == True{} : Bool},
979  +ea: {Laws.above(~K, ~cmp, lb, k2) == True{} : Bool},
980  +eb: {Laws.below(~K, ~cmp, ub, k2) == True{} : Bool},
981  +nef: {Cmp.is_eq(cmp(k2, k)) == False{} : Bool}
982) -> {g(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, t, k2, v), k)
983      == g(~K, ~V, ~cmp, t, k) : Maybe<&2, V>}:
984  match t:
985    case O.OTip{}:
986      split(c => {getc(~K, ~V, ~cmp, c, k, v, O.OTip{}, O.OTip{}) == None{} : Maybe<&2, V>},
987        cmp(k, k2),
988        e => {==},
989        e => ne_absurd({Some{v} == None{} : Maybe<&2, V>}, cmp(k2, k), nef,
990          eq_flip(~K, ~cmp, ~flip, k, k2, e)),
991        e => {==})
992    case O.OBin{+s, +key, +val, +lo, +hi}:
993      +b_l = bn.l(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt)
994      +b_h = bn.h(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt)
995      +plo = O.OMap.put(~K, ~V, ~cmp, lo, k2, v)
996      +phi = O.OMap.put(~K, ~V, ~cmp, hi, k2, v)
997      +old = {O.OBin{s, key, val, lo, hi} : O.OMap<K, V>}
998      cmp.split(O.OMap<K, V>, Maybe<&2, V>, y => g(~K, ~V, ~cmp, y, k),
999        g(~K, ~V, ~cmp, old, k), cmp(k2, key),
1000        u => O.OMap.balance(K, V, key, val, O.OMap.put(~K, ~V, ~cmp, lo, k2, v), hi),
1001        u => O.OBin{s, key, v, lo, hi},
1002        u => O.OMap.balance(K, V, key, val, lo, O.OMap.put(~K, ~V, ~cmp, hi, k2, v)),
1003        +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, plo, hi), k),
1004          g(~K, ~V, ~cmp, O.OBin{0, key, val, plo, hi}, k), g(~K, ~V, ~cmp, old, k),
1005          balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, plo, hi,
1006            put.bnd(~K, ~V, ~cmp, ~flip, ~trans, lo, lb, Some{key}, k2, v, b_l, ea,
1007              lt_true(cmp(k2, key), e)),
1008            b_h),
1009          split(c => {getc(~K, ~V, ~cmp, c, k, val, plo, hi)
1010              == getc(~K, ~V, ~cmp, c, k, val, lo, hi) : Maybe<&2, V>},
1011            cmp(k, key),
1012            e2 => get_put_other(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lo, lb, Some{key},
1013              k2, k, v, b_l, ea, lt_true(cmp(k2, key), e), nef),
1014            e2 => {==},
1015            e2 => {==})),
1016        +e => split(c => {getc(~K, ~V, ~cmp, c, k, v, lo, hi)
1017            == getc(~K, ~V, ~cmp, c, k, val, lo, hi) : Maybe<&2, V>},
1018          cmp(k, key),
1019          e2 => {==},
1020          e2 => ne_absurd({Some{v} == Some{val} : Maybe<&2, V>}, cmp(k2, k), nef,
1021            rw(K, y => {cmp(y, k) == EQ{} : Cmp}, k2, key, eq(k2, key, e),
1022              eq_flip(~K, ~cmp, ~flip, k, key, e2))),
1023          e2 => {==}),
1024        +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, lo, phi), k),
1025          g(~K, ~V, ~cmp, O.OBin{0, key, val, lo, phi}, k), g(~K, ~V, ~cmp, old, k),
1026          balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, lo, phi,
1027            b_l,
1028            put.bnd(~K, ~V, ~cmp, ~flip, ~trans, hi, Some{key}, ub, k2, v, b_h,
1029              lt_true(cmp(key, k2), gt_flip(~K, ~cmp, ~flip, k2, key, e)), eb)),
1030          split(c => {getc(~K, ~V, ~cmp, c, k, val, lo, phi)
1031              == getc(~K, ~V, ~cmp, c, k, val, lo, hi) : Maybe<&2, V>},
1032            cmp(k, key),
1033            e2 => {==},
1034            e2 => {==},
1035            e2 => get_put_other(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, hi, Some{key}, ub,
1036              k2, k, v, b_h, lt_true(cmp(key, k2), gt_flip(~K, ~cmp, ~flip, k2, key, e)),
1037              eb, nef))))