1 import Base 2 import ../../lib/logic.bend as L 3 import ../../../spec/containers/hash_table.bend as S 4 import ./keys.bend as K 5 6 # Facts about the specification's association-list map. 7 8 def pick_t(~A: Data, +c: Bool, +h: {c == True{} : Bool}, +x: A, +y: A) -> {Bool.pick(A, c, x, y) == x : A}: 9 match c: 10 case True{}: 11 {==} 12 case False{}: 13 Empty.absurd({Bool.pick(A, False{}, x, y) == x : A}, L.false_true(h)) 14 15 def pick_f(~A: Data, +c: Bool, +h: {c == False{} : Bool}, +x: A, +y: A) -> {Bool.pick(A, c, x, y) == y : A}: 16 match c: 17 case True{}: 18 Empty.absurd({Bool.pick(A, True{}, x, y) == y : A}, L.true_false(h)) 19 case False{}: 20 {==} 21 22 # two keys equal to the same key are equal to each other, by str_eq 23 def eq_tr(+a: String, +b: String, +c: String, +hab: {S.str_eq(a, b) == True{} : Bool}, +e: Bool, +he: {S.str_eq(b, c) == e : Bool}) -> {S.str_eq(a, c) == e : Bool}: 24 L.subst(String, z => {S.str_eq(z, c) == e : Bool}, b, a, Equal.sym(String, a, b, K.str_eq_of(a, b, hab)), he) 25 26 # comparing with keys equal by str_eq agrees 27 def eq_tr2(+j: String, +key: String, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}) -> {S.str_eq(j, key) == S.str_eq(j, q) : Bool}: 28 Equal.cong(String, Bool, z => S.str_eq(j, z), key, q, K.str_eq_of(key, q, hq)) 29 30 # ---- set ---- 31 32 def ls_same_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +c: Bool, +hc: {S.str_eq(j, key) == c : Bool}, rec: @hc2: {S.str_eq(j, key) == False{} : Bool} -> {S.lookup(~V, S.set(~V, t, key, x), q) == Some{x} : Maybe<&2, V>}) -> {S.lookup(~V, Bool.pick(List<&2, S.Entry>, c, Con{S.E{key, x}, t}, Con{S.E{j, v}, S.set(~V, t, key, x)}), q) == Some{x} : Maybe<&2, V>}: 33 match c: 34 case True{}: 35 pick_t(~Maybe<&2, V>, S.str_eq(key, q), hq, Some{x}, S.lookup(~V, t, q)) 36 case False{}: 37 +jq = eq_tr(q, key, j, K.str_eq_true(q, key, Equal.sym(String, key, q, K.str_eq_of(key, q, hq))), False{}, Equal.trans(Bool, S.str_eq(key, j), S.str_eq(j, key), False{}, K.str_sym(key, j), hc)) 38 +jq2 = Equal.trans(Bool, S.str_eq(j, q), S.str_eq(q, j), False{}, K.str_sym(j, q), jq) 39 Equal.trans(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, S.set(~V, t, key, x), q)), S.lookup(~V, S.set(~V, t, key, x), q), Some{x}, pick_f(~Maybe<&2, V>, S.str_eq(j, q), jq2, Some{v}, S.lookup(~V, S.set(~V, t, key, x), q)), rec(hc)) 40 41 # looking up the key just set (or any key equal to it) 42 def lookup_set_same(~V: Data, +m: List<&2, S.Entry>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}) -> {S.lookup(~V, S.set(~V, m, key, x), q) == Some{x} : Maybe<&2, V>}: 43 match m: 44 case Nil{}: 45 pick_t(~Maybe<&2, V>, S.str_eq(key, q), hq, Some{x}, None{}) 46 case Con{S.E{+j, +v}, +t}: 47 ls_same_c(~V, j, v, t, key, x, q, hq, S.str_eq(j, key), {==}, hc2 => lookup_set_same(~V, t, key, x, q, hq)) 48 49 def ls_other_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +c: Bool, +hc: {S.str_eq(j, key) == c : Bool}, +ih: {S.lookup(~V, S.set(~V, t, key, x), q) == S.lookup(~V, t, q) : Maybe<&2, V>}) -> {S.lookup(~V, Bool.pick(List<&2, S.Entry>, c, Con{S.E{key, x}, t}, Con{S.E{j, v}, S.set(~V, t, key, x)}), q) == Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)) : Maybe<&2, V>}: 50 match c: 51 case True{}: 52 +jq = eq_tr(j, key, q, hc, False{}, hq) 53 Equal.trans(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(key, q), Some{x}, S.lookup(~V, t, q)), S.lookup(~V, t, q), Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)), pick_f(~Maybe<&2, V>, S.str_eq(key, q), hq, Some{x}, S.lookup(~V, t, q)), Equal.sym(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)), S.lookup(~V, t, q), pick_f(~Maybe<&2, V>, S.str_eq(j, q), jq, Some{v}, S.lookup(~V, t, q)))) 54 case False{}: 55 Equal.cong(Maybe<&2, V>, Maybe<&2, V>, z => Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, z), S.lookup(~V, S.set(~V, t, key, x), q), S.lookup(~V, t, q), ih) 56 57 # setting key leaves every other key's lookup 58 def lookup_set_other(~V: Data, +m: List<&2, S.Entry>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}) -> {S.lookup(~V, S.set(~V, m, key, x), q) == S.lookup(~V, m, q) : Maybe<&2, V>}: 59 match m: 60 case Nil{}: 61 pick_f(~Maybe<&2, V>, S.str_eq(key, q), hq, Some{x}, None{}) 62 case Con{S.E{+j, +v}, +t}: 63 ls_other_c(~V, j, v, t, key, x, q, hq, S.str_eq(j, key), {==}, lookup_set_other(~V, t, key, x, q, hq)) 64 65 def lr_other_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry>, +key: String, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +c: Bool, +hc: {S.str_eq(j, key) == c : Bool}, +ih: {S.lookup(~V, S.remove(~V, t, key), q) == S.lookup(~V, t, q) : Maybe<&2, V>}) -> {S.lookup(~V, Bool.pick(List<&2, S.Entry>, c, t, Con{S.E{j, v}, S.remove(~V, t, key)}), q) == Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)) : Maybe<&2, V>}: 66 match c: 67 case True{}: 68 Equal.sym(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)), S.lookup(~V, t, q), pick_f(~Maybe<&2, V>, S.str_eq(j, q), eq_tr(j, key, q, hc, False{}, hq), Some{v}, S.lookup(~V, t, q))) 69 case False{}: 70 Equal.cong(Maybe<&2, V>, Maybe<&2, V>, z => Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, z), S.lookup(~V, S.remove(~V, t, key), q), S.lookup(~V, t, q), ih) 71 72 # removing key leaves every other key's lookup 73 def lookup_remove_other(~V: Data, +m: List<&2, S.Entry>, +key: String, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}) -> {S.lookup(~V, S.remove(~V, m, key), q) == S.lookup(~V, m, q) : Maybe<&2, V>}: 74 match m: 75 case Nil{}: 76 {==} 77 case Con{S.E{+j, +v}, +t}: 78 lr_other_c(~V, j, v, t, key, q, hq, S.str_eq(j, key), {==}, lookup_remove_other(~V, t, key, q, hq)) 79 80 def or_false_l(+a: Bool, +b: Bool, +h: {Bool.or(a, b) == False{} : Bool}) -> {a == False{} : Bool}: 81 match a: 82 case True{}: 83 Empty.absurd({True{} == False{} : Bool}, L.true_false(h)) 84 case False{}: 85 {==} 86 87 def or_false_r(+a: Bool, +b: Bool, +h: {Bool.or(a, b) == False{} : Bool}) -> {b == False{} : Bool}: 88 match a: 89 case True{}: 90 Empty.absurd({b == False{} : Bool}, L.true_false(h)) 91 case False{}: 92 h 93 94 # a key not among the keys has no value 95 def lookup_not_mem(~V: Data, +m: List<&2, S.Entry>, +q: String, +h: {S.mem(q, S.keys(~V, m)) == False{} : Bool}) -> {S.lookup(~V, m, q) == None{} : Maybe<&2, V>}: 96 match m: 97 case Nil{}: 98 {==} 99 case Con{S.E{+j, +v}, +t}: 100 Equal.trans(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q)), S.lookup(~V, t, q), None{}, pick_f(~Maybe<&2, V>, S.str_eq(j, q), or_false_l(S.str_eq(j, q), S.mem(q, S.keys(~V, t)), h), Some{v}, S.lookup(~V, t, q)), lookup_not_mem(~V, t, q, or_false_r(S.str_eq(j, q), S.mem(q, S.keys(~V, t)), h))) 101 102 def lr_same_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry>, +key: String, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +hnm: {Bool.not(S.mem(j, S.keys(~V, t))) == True{} : Bool}, +c: Bool, +hc: {S.str_eq(j, key) == c : Bool}, rec: @hc2: {S.str_eq(j, key) == False{} : Bool} -> {S.lookup(~V, S.remove(~V, t, key), q) == None{} : Maybe<&2, V>}) -> {S.lookup(~V, Bool.pick(List<&2, S.Entry>, c, t, Con{S.E{j, v}, S.remove(~V, t, key)}), q) == None{} : Maybe<&2, V>}: 103 match c: 104 case True{}: 105 +ejq = K.str_eq_of(j, q, eq_tr(j, key, q, hc, True{}, hq)) 106 lookup_not_mem(~V, t, q, L.subst(String, z => {S.mem(z, S.keys(~V, t)) == False{} : Bool}, j, q, ejq, K.not_true_eq(S.mem(j, S.keys(~V, t)), hnm))) 107 case False{}: 108 +jq = Equal.trans(Bool, S.str_eq(j, q), S.str_eq(j, key), False{}, Equal.sym(Bool, S.str_eq(j, key), S.str_eq(j, q), eq_tr2(j, key, q, hq)), hc) 109 Equal.trans(Maybe<&2, V>, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, S.remove(~V, t, key), q)), S.lookup(~V, S.remove(~V, t, key), q), None{}, pick_f(~Maybe<&2, V>, S.str_eq(j, q), jq, Some{v}, S.lookup(~V, S.remove(~V, t, key), q)), rec(hc)) 110 111 # with keys unique, a removed key has no value 112 def lookup_remove_same(~V: Data, +m: List<&2, S.Entry>, +key: String, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +hnd: {S.nodup(S.keys(~V, m)) == True{} : Bool}) -> {S.lookup(~V, S.remove(~V, m, key), q) == None{} : Maybe<&2, V>}: 113 match m: 114 case Nil{}: 115 {==} 116 case Con{S.E{+j, +v}, +t}: 117 lr_same_c(~V, j, v, t, key, q, hq, L.and_left(Bool.not(S.mem(j, S.keys(~V, t))), S.nodup(S.keys(~V, t)), hnd), S.str_eq(j, key), {==}, hc2 => lookup_remove_same(~V, t, key, q, hq, L.and_right(Bool.not(S.mem(j, S.keys(~V, t))), S.nodup(S.keys(~V, t)), hnd))) 118 119 # ---- sizes ---- 120 121 def none_pick(~V: Data, +c: Bool, +v: V, +r: Maybe<&2, V>, +h: {Bool.pick(Maybe<&2, V>, c, Some{v}, r) == None{} : Maybe<&2, V>}) -> {c == False{} : Bool} & {r == None{} : Maybe<&2, V>}: 122 match c: 123 case True{}: 124 Empty.absurd({True{} == False{} : Bool} & {r == None{} : Maybe<&2, V>}, L.none_some(V, v, Equal.sym(Maybe<&2, V>, Some{v}, None{}, h))) 125 case False{}: 126 ({==}, h) 127 128 def ssn_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry>, +key: String, +x: V, +c: Bool, +hc: {c == False{} : Bool}, +ih: {S.size(~V, S.set(~V, t, key, x)) == 1n+S.size(~V, t) : Nat}) -> {S.size(~V, Bool.pick(List<&2, S.Entry>, c, Con{S.E{key, x}, t}, Con{S.E{j, v}, S.set(~V, t, key, x)})) == 2n+S.size(~V, t) : Nat}: 129 match c: 130 case True{}: 131 Empty.absurd({S.size(~V, Con{S.E{key, x}, t}) == 2n+S.size(~V, t) : Nat}, L.true_false(hc)) 132 case False{}: 133 Equal.cong(Nat, Nat, z => 1n+z, S.size(~V, S.set(~V, t, key, x)), 1n+S.size(~V, t), ih) 134 135 # setting an absent key adds one entry 136 def size_set_new(~V: Data, +m: List<&2, S.Entry>, +key: String, +x: V, +h: {S.lookup(~V, m, key) == None{} : Maybe<&2, V>}) -> {S.size(~V, S.set(~V, m, key, x)) == 1n+S.size(~V, m) : Nat}: 137 match m: 138 case Nil{}: 139 {==} 140 case Con{S.E{+j, +v}, +t}: 141 +c0 = Pair.fst({S.str_eq(j, key) == False{} : Bool}, {S.lookup(~V, t, key) == None{} : Maybe<&2, V>}, none_pick(~V, S.str_eq(j, key), v, S.lookup(~V, t, key), h)) 142 +r0 = Pair.snd({S.str_eq(j, key) == False{} : Bool}, {S.lookup(~V, t, key) == None{} : Maybe<&2, V>}, none_pick(~V, S.str_eq(j, key), v, S.lookup(~V, t, key), h)) 143 ssn_c(~V, j, v, t, key, x, S.str_eq(j, key), c0, size_set_new(~V, t, key, x, r0)) 144 145 def sso_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry>, +key: String, +x: V, +v0: V, +c: Bool, +h: {Bool.pick(Maybe<&2, V>, c, Some{v}, S.lookup(~V, t, key)) == Some{v0} : Maybe<&2, V>}, rec: @h2: {S.lookup(~V, t, key) == Some{v0} : Maybe<&2, V>} -> {S.size(~V, S.set(~V, t, key, x)) == S.size(~V, t) : Nat}) -> {S.size(~V, Bool.pick(List<&2, S.Entry>, c, Con{S.E{key, x}, t}, Con{S.E{j, v}, S.set(~V, t, key, x)})) == 1n+S.size(~V, t) : Nat}: 146 match c: 147 case True{}: 148 {==} 149 case False{}: 150 Equal.cong(Nat, Nat, z => 1n+z, S.size(~V, S.set(~V, t, key, x)), S.size(~V, t), rec(h)) 151 152 # setting a present key keeps the size 153 def size_set_old(~V: Data, +m: List<&2, S.Entry>, +key: String, +x: V, +v0: V, +h: {S.lookup(~V, m, key) == Some{v0} : Maybe<&2, V>}) -> {S.size(~V, S.set(~V, m, key, x)) == S.size(~V, m) : Nat}: 154 match m: 155 case Nil{}: 156 Empty.absurd({S.size(~V, S.set(~V, Nil{}, key, x)) == S.size(~V, Nil{}) : Nat}, L.none_some(V, v0, h)) 157 case Con{S.E{+j, +v}, +t}: 158 sso_c(~V, j, v, t, key, x, v0, S.str_eq(j, key), h, h2 => size_set_old(~V, t, key, x, v0, h2)) 159 160 def sro_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry>, +key: String, +v0: V, +c: Bool, +h: {Bool.pick(Maybe<&2, V>, c, Some{v}, S.lookup(~V, t, key)) == Some{v0} : Maybe<&2, V>}, rec: @h2: {S.lookup(~V, t, key) == Some{v0} : Maybe<&2, V>} -> {1n+S.size(~V, S.remove(~V, t, key)) == S.size(~V, t) : Nat}) -> {1n+S.size(~V, Bool.pick(List<&2, S.Entry>, c, t, Con{S.E{j, v}, S.remove(~V, t, key)})) == 1n+S.size(~V, t) : Nat}: 161 match c: 162 case True{}: 163 {==} 164 case False{}: 165 Equal.cong(Nat, Nat, z => 1n+z, 1n+S.size(~V, S.remove(~V, t, key)), S.size(~V, t), rec(h)) 166 167 # removing a present key drops one entry 168 def size_remove_old(~V: Data, +m: List<&2, S.Entry>, +key: String, +v0: V, +h: {S.lookup(~V, m, key) == Some{v0} : Maybe<&2, V>}) -> {1n+S.size(~V, S.remove(~V, m, key)) == S.size(~V, m) : Nat}: 169 match m: 170 case Nil{}: 171 Empty.absurd({1n+S.size(~V, S.remove(~V, Nil{}, key)) == S.size(~V, Nil{}) : Nat}, L.none_some(V, v0, h)) 172 case Con{S.E{+j, +v}, +t}: 173 sro_c(~V, j, v, t, key, v0, S.str_eq(j, key), h, h2 => size_remove_old(~V, t, key, v0, h2)) 174 175 def rn_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry>, +key: String, +c: Bool, +hc: {c == False{} : Bool}, +ih: {S.remove(~V, t, key) == t : List<&2, S.Entry>}) -> {Bool.pick(List<&2, S.Entry>, c, t, Con{S.E{j, v}, S.remove(~V, t, key)}) == Con{S.E{j, v}, t} : List<&2, S.Entry>}: 176 match c: 177 case True{}: 178 Empty.absurd({t == Con{S.E{j, v}, t} : List<&2, S.Entry>}, L.true_false(hc)) 179 case False{}: 180 Equal.cong(List<&2, S.Entry>, List<&2, S.Entry>, z => Con{S.E{j, v}, z}, S.remove(~V, t, key), t, ih) 181 182 # removing an absent key changes nothing 183 def remove_none(~V: Data, +m: List<&2, S.Entry>, +key: String, +h: {S.lookup(~V, m, key) == None{} : Maybe<&2, V>}) -> {S.remove(~V, m, key) == m : List<&2, S.Entry>}: 184 match m: 185 case Nil{}: 186 {==} 187 case Con{S.E{+j, +v}, +t}: 188 +c0 = Pair.fst({S.str_eq(j, key) == False{} : Bool}, {S.lookup(~V, t, key) == None{} : Maybe<&2, V>}, none_pick(~V, S.str_eq(j, key), v, S.lookup(~V, t, key), h)) 189 +r0 = Pair.snd({S.str_eq(j, key) == False{} : Bool}, {S.lookup(~V, t, key) == None{} : Maybe<&2, V>}, none_pick(~V, S.str_eq(j, key), v, S.lookup(~V, t, key), h)) 190 rn_c(~V, j, v, t, key, S.str_eq(j, key), c0, remove_none(~V, t, key, r0))