Lookups in an insertion-ordered map

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_mk_cons {K V : Type} [DecidableEq K] (k' : K) (v' : V) (ps : List (K × V)) (k : K) : { pairs := (k', v') :: ps }.get? k = if k' = k then some v' else { pairs := ps }.get? k

@[simp]

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_mk_nil {K V : Type} [DecidableEq K] (k : K) : { pairs := [] }.get? k = none

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_eq_some {K V : Type} [DecidableEq K] {d : Dict K V} {k : K} {v : V} (h : d.get? k = some v) : (k, v) ∈ d.pairs

theorem Cryptlib.Protocols.GroupComm.Common.Dict.contains_iff {K V : Type} [DecidableEq K] {d : Dict K V} {k : K} : d.contains k = true ↔ ∃ (v : V), (k, v) ∈ d.pairs

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_replace {K V : Type} [DecidableEq K] (ps : List (K × V)) (k k' : K) (v : V) : { pairs := List.map (fun (p : K × V) => if p.1 = k then (k, v) else p) ps }.get? k' = if k = k' then Option.map (fun (x : V) => v) ({ pairs := ps }.get? k) else { pairs := ps }.get? k'

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_append {K V : Type} [DecidableEq K] (ps : List (K × V)) (k k' : K) (v : V) : { pairs := ps ++ [(k, v)] }.get? k' = ({ pairs := ps }.get? k').or (if k = k' then some v else none)

@[simp]

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_set_self {K V : Type} [DecidableEq K] (d : Dict K V) (k : K) (v : V) : (d.set k v).get? k = some v

@[simp]

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_set_ne {K V : Type} [DecidableEq K] (d : Dict K V) {k k' : K} (v : V) (h : k ≠ k') : (d.set k v).get? k' = d.get? k'

@[simp]

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_mapValues {K V : Type} [DecidableEq K] {W : Type} (d : Dict K V) (f : V → W) (k : K) : (d.mapValues f).get? k = Option.map f (d.get? k)

theorem Cryptlib.Protocols.GroupComm.Common.Dict.mem_filter {K V : Type} {d : Dict K V} {p : K → V → Bool} {e : K × V} : e ∈ (d.filter p).pairs ↔ e ∈ d.pairs ∧ p e.1 e.2 = true

theorem Cryptlib.Protocols.GroupComm.Common.Dict.mem_mapValues {K V W : Type} {d : Dict K V} {f : V → W} {e : K × W} : e ∈ (d.mapValues f).pairs ↔ ∃ (v : V), (e.1, v) ∈ d.pairs ∧ e.2 = f v

theorem Cryptlib.Protocols.GroupComm.Common.Dict.mem_mapWithKey {K V W : Type} {d : Dict K V} {f : K → V → W} {e : K × W} : e ∈ (d.mapWithKey f).pairs ↔ ∃ (v : V), (e.1, v) ∈ d.pairs ∧ e.2 = f e.1 v

theorem Cryptlib.Protocols.GroupComm.Common.Dict.mem_set {K V : Type} [DecidableEq K] {d : Dict K V} {k : K} {v : V} {e : K × V} (h : e ∈ (d.set k v).pairs) : e = (k, v) ∨ e ∈ d.pairs

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_setDefault_self {K V : Type} [DecidableEq K] (d : Dict K V) (k : K) (v : V) : (d.setDefault k v).get? k = some ((d.get? k).getD v)

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_setDefault_ne {K V : Type} [DecidableEq K] (d : Dict K V) {k k' : K} (v : V) (h : k ≠ k') : (d.setDefault k v).get? k' = d.get? k'

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_erase {K V : Type} [DecidableEq K] (d : Dict K V) (k k' : K) : (d.erase k).get? k' = if k = k' then none else d.get? k'

theorem Cryptlib.Protocols.GroupComm.Common.Dict.get?_modify {K V : Type} [DecidableEq K] (d : Dict K V) (k k' : K) (f : V → V) : (d.modify k f).get? k' = if k = k' then Option.map f (d.get? k) else d.get? k'