Map properties

This file proves useful properties of canonical list-based maps defined in Cedar.Data.Map.

Well-formed maps

def Cedar.Data.Map.WellFormed {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] (m : Map α β) : Prop

Equations

• m.WellFormed = (m = Cedar.Data.Map.make m.toList)

theorem Cedar.Data.Map.if_wellformed_then_exists_make {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] (m : Map α β) : m.WellFormed → ∃ (list : List (α × β)), m = make list

theorem Cedar.Data.Map.wf_iff_sorted {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] {m : Map α β} : m.WellFormed ↔ List.SortedBy Prod.fst m.toList

theorem Cedar.Data.Map.wf_implies_tail_wf {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] {hd : α × β} {tl : List (α × β)} (hwf : (mk (hd :: tl)).WellFormed) : (mk tl).WellFormed

theorem Cedar.Data.Map.wf_empty {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] : empty.WellFormed

theorem Cedar.Data.Map.wf_singleton {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] (a : α) (b : β) : (mk [(a, b)]).WellFormed

theorem Cedar.Data.Map.key_maps_to_one_value {α : Type u_1} {β : Type u_2} [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] (k : α) (v₁ v₂ : β) (m : Map α β) : m.WellFormed → (k, v₁) ∈ m.toList → (k, v₂) ∈ m.toList → v₁ = v₂

In well-formed maps, if there are two pairs with the same key, then they have the same value

@[simp]

theorem Cedar.Data.Map.eq_iff_toList_eq {α : Type u_1} {β : Type u_2} {m₁ m₂ : Map α β} : m₁.toList = m₂.toList ↔ m₁ = m₂

If two maps have exactly equal (k,v) sets, then the maps are equal

This doesn't require WellFormed, but we use it in the proof of eq_iff_toList_equiv below

@[simp]

theorem Cedar.Data.Map.eq_iff_toList_equiv {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] {m₁ m₂ : Map α β} (wf₁ : m₁.WellFormed) (wf₂ : m₂.WellFormed) : m₁.toList ≡ m₂.toList ↔ m₁ = m₂

If two well-formed maps have equivalent (k,v) sets, then the maps are actually equal

empty, contains, mem, toList, keys, values

theorem Cedar.Data.Map.keys_wf {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] (m : Map α β) : m.WellFormed → m.keys.WellFormed

@[simp]

theorem Cedar.Data.Map.toList_empty {α : Type u_1} {β : Type u_2} : empty.toList = []

@[simp]

theorem Cedar.Data.Map.toList_nil_iff_empty {α : Type u_1} {β : Type u_2} {m : Map α β} : m.toList = [] ↔ m = empty

@[simp]

theorem Cedar.Data.Map.mk_toList_id {α : Type u_1} {β : Type u_2} (m : Map α β) : mk m.toList = m

@[simp]

theorem Cedar.Data.Map.toList_mk_id {α : Type u_1} {β : Type u_2} (kvs : List (α × β)) : (mk kvs).toList = kvs

theorem Cedar.Data.Map.deprecated_toList_def {α : Type u_1} {β : Type u_2} (m : Map α β) : m.toList = m.1

As a crutch to accommodate some pre-existing usage, we provide this theorem. But TODO in the future we should transition users of this theorem to instead use public theorems about toList and not have to expose the internals of Data.Map.

theorem Cedar.Data.Map.in_list_in_map {β : Type u_1} {α : Type u} (k : α) (v : β) (m : Map α β) : (k, v) ∈ m.toList → k ∈ m

theorem Cedar.Data.Map.in_list_in_keys {α : Type u_1} {β : Type u_2} {k : α} {v : β} {m : Map α β} : (k, v) ∈ m.toList → k ∈ m.keys

theorem Cedar.Data.Map.in_list_in_values {α : Type u_1} {β : Type u_2} {k : α} {v : β} {m : Map α β} : (k, v) ∈ m.toList → v ∈ m.values

theorem Cedar.Data.Map.in_keys_iff_in_map {α : Type u_1} {β : Type u_2} {k : α} {m : Map α β} : k ∈ m.keys ↔ k ∈ m

theorem Cedar.Data.Map.in_keys_iff_contains {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] {k : α} {m : Map α β} : k ∈ m.keys ↔ m.contains k = true

theorem Cedar.Data.Map.in_values_exists_key {α : Type u_1} {β : Type u_2} {m : Map α β} {v : β} : v ∈ m.values → ∃ (k : α), (k, v) ∈ m.toList

kinda the converse of in_list_in_values

theorem Cedar.Data.Map.in_keys_exists_value {α : Type u_1} {β : Type u_2} {m : Map α β} {k : α} : k ∈ m.keys → ∃ (v : β), (k, v) ∈ m.toList

theorem Cedar.Data.Map.values_cons {α : Type u_1} {β : Type u_2} {k : α} {v : β} {tl : List (α × β)} {m : Map α β} : m.toList = (k, v) :: tl → m.values = v :: (mk tl).values

theorem Cedar.Data.Map.contains_eq_isSome_find? {α : Type u_1} {β : Type u_2} [BEq α] (m : Map α β) (k : α) : m.contains k = (m.find? k).isSome

Characterizes contains in terms of find?, for clients that cannot unfold contains.

theorem Cedar.Data.Map.contains_iff_some_find? {α : Type u_1} {β : Type u_2} [BEq α] {m : Map α β} {k : α} : m.contains k = true ↔ ∃ (v : β), m.find? k = some v

theorem Cedar.Data.Map.find?_some_implies_contains {α : Type u_1} {β : Type u_2} [BEq α] {m : Map α β} {k : α} {v : β} : m.find? k = some v → m.contains k = true

@[simp]

theorem Cedar.Data.Map.not_find?_of_empty {α : Type u_1} {β : Type u_2} [BEq α] {k : α} : empty.find? k = none

theorem Cedar.Data.Map.not_contains_of_empty {α : Type u_1} {β : Type u_2} [BEq α] (k : α) : ¬empty.contains k = true

make and mk

theorem Cedar.Data.Map.make_wf {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableLT α] (xs : List (α × β)) : (make xs).WellFormed

theorem Cedar.Data.Map.mk_wf {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableLT α] {xs : List (α × β)} : List.SortedBy Prod.fst xs → (mk xs).WellFormed

theorem Cedar.Data.Map.make_eq_mk_canonicalize {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableLT α] {xs : List (α × β)} : make xs = mk (List.canonicalize Prod.fst xs)

theorem Cedar.Data.Map.make_eq_mk {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableLT α] {xs : List (α × β)} : List.SortedBy Prod.fst xs ↔ make xs = mk xs

theorem Cedar.Data.Map.toList_make_eq_canonicalize {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableLT α] (xs : List (α × β)) : (make xs).toList = List.canonicalize Prod.fst xs

theorem Cedar.Data.Map.make_singleton {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] (k : α) (v : β) : make [(k, v)] = mk [(k, v)]

theorem Cedar.Data.Map.mem_make_mem_list {α : Type u_1} {β : Type u_2} {x : α × β} [LT α] [StrictLT α] [DecidableLT α] {xs : List (α × β)} : x ∈ (make xs).toList → x ∈ xs

Note that the converse of this is not true: counterexample xs = [(1, false), (1, true)]. (The property here would not hold for either x = (1, false) or x = (1, true).)

For a limited converse, see mem_list_mem_make below.

theorem Cedar.Data.Map.mem_values_make {α : Type u_1} {β : Type u_2} {v : β} [LT α] [StrictLT α] [DecidableLT α] {xs : List (α × β)} : v ∈ (make xs).values → v ∈ List.map Prod.snd xs

Very similar to mem_make_mem_list above

theorem Cedar.Data.Map.mem_list_mem_make {α : Type u_1} {β : Type u_2} {x : α × β} [LT α] [StrictLT α] [DecidableLT α] {xs : List (α × β)} : List.SortedBy Prod.fst xs → x ∈ xs → x ∈ (make xs).toList

This limited converse of mem_make_mem_list requires that the input list is SortedBy Prod.fst.

@[simp]

theorem Cedar.Data.Map.make_nil_is_empty {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] : make [] = empty

theorem Cedar.Data.Map.make_cons {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] {xs ys : List (α × β)} {ab : α × β} : make xs = make ys → make (ab :: xs) = make (ab :: ys)

Note that the converse of this is not true: counterexample xs = [(1, false)], ys = [], ab = (1, false).

@[simp]

theorem Cedar.Data.Map.make_of_make_is_id {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] (xs : List (α × β)) : make (make xs).toList = make xs

find?, findOrErr, and mapOnValues

@[simp]

theorem Cedar.Data.Map.find?_empty {α : Type u_1} {β : Type u_2} [DecidableEq α] (k : α) : empty.find? k = none

@[simp]

theorem Cedar.Data.Map.singleton_find? {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] (k : α) (v : β) : (make [(k, v)]).find? k = some v

@[simp]

theorem Cedar.Data.Map.singleton_contains {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] (k k' : α) (v : β) : (make [(k', v)]).contains k = true ↔ (k' == k) = true

theorem Cedar.Data.Map.find?_eq_toList_find? {α : Type u_1} {β : Type u_2} [BEq α] (m : Map α β) (k : α) : m.find? k = Option.map Prod.snd (List.find? (fun (x : α × β) => x.fst == k) m.toList)

Map.find? returns the value of the first entry with the key.

theorem Cedar.Data.Map.find?_mem_toList {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [DecidableEq α] {m : Map α β} {k : α} {v : β} (h₁ : m.find? k = some v) : (k, v) ∈ m.toList

Converse is available at in_list_iff_find?_some (requires wf though)

Inverse is available at find?_notmem_keys (requires wf though)

theorem Cedar.Data.Map.in_list_iff_find?_some {α : Type u_1} {β : Type u_2} [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] {k : α} {v : β} {m : Map α β} (wf : m.WellFormed) : (k, v) ∈ m.toList ↔ m.find? k = some v

The mpr direction of this does not need the wf precondition and, in fact, is available separately as find?_mem_toList above

theorem Cedar.Data.Map.find?_notmem_keys {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} (wf : m.WellFormed) : m.find? k = none ↔ ¬k ∈ m.keys

Inverse of find?_mem_toList, except that this requires wf

theorem Cedar.Data.Map.find?_ext {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m₁ m₂ : Map α β} (wf₁ : m₁.WellFormed) (wf₂ : m₂.WellFormed) (h : ∀ (k : α), m₁.find? k = m₂.find? k) : m₁ = m₂

Two well-formed maps are equal if they have the same find? for every key.

theorem Cedar.Data.Map.find?_none_all_absent {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} : m.find? k = none → ∀ (v : β), ¬(k, v) ∈ m.toList

theorem Cedar.Data.Map.in_list_implies_contains {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} {v : β} : (k, v) ∈ m.toList → m.contains k = true

theorem Cedar.Data.Map.all_absent_find?_none {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} : (∀ (v : β), ¬(k, v) ∈ m.toList) → m.find? k = none

theorem Cedar.Data.Map.find?_none_iff_all_absent {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} : m.find? k = none ↔ ∀ (v : β), ¬(k, v) ∈ m.toList

theorem Cedar.Data.Map.list_find?_some_iff_map_find?_some {α β : Type} [BEq α] [LawfulBEq α] {l : List (α × β)} {k : α} {v : β} : List.find? (fun (x : α × β) => x.fst == k) l = some (k, v) ↔ (mk l).find? k = some v

theorem Cedar.Data.Map.list_find?_mapM_implies_exists_mapped {α β γ : Type} [BEq α] [LawfulBEq α] {ls : List (α × β)} (fn : β → Option γ) {ys : List (α × γ)} {k : α} {x : β} : List.mapM (fun (x : α × β) => (fn x.snd).bind fun (v : γ) => some (x.fst, v)) ls = some ys → List.find? (fun (x : α × β) => x.fst == k) ls = some (k, x) → ∃ (y : γ), fn x = some y ∧ List.find? (fun (x : α × γ) => x.fst == k) ys = some (k, y)

theorem Cedar.Data.Map.list_find?_mapM_implies_exists_unmapped {α β γ : Type} [BEq α] [LawfulBEq α] {ls : List (α × β)} (fn : β → Option γ) {ys : List (α × γ)} {k : α} {y : γ} : List.mapM (fun (x : α × β) => (fn x.snd).bind fun (v : γ) => some (x.fst, v)) ls = some ys → List.find? (fun (x : α × γ) => x.fst == k) ys = some (k, y) → ∃ (x : β), fn x = some y ∧ List.find? (fun (x : α × β) => x.fst == k) ls = some (k, x)

theorem Cedar.Data.Map.find?_mapM_key_id {α β : Type} [BEq α] [LawfulBEq α] {ks : List α} {kvs : List (α × β)} {fn : α → Option β} {k : α} (h₁ : List.mapM (fun (k : α) => do let __do_lift ← fn k some (k, __do_lift)) ks = some kvs) (h₂ : k ∈ ks) : (mk kvs).find? k = fn k

theorem Cedar.Data.Map.find?_filterMap_key_id {α β : Type} [BEq α] [LawfulBEq α] {ks : List α} {fn : α → Option β} {k : α} (h₂ : k ∈ ks) : (mk (List.filterMap (fun (k : α) => do let __do_lift ← fn k some (k, __do_lift)) ks)).find? k = fn k

theorem Cedar.Data.Map.filterMap_key_id_key_none_implies_find?_none {α β : Type} [DecidableEq α] [LT α] [StrictLT α] [DecidableLT α] {ks : List α} {fn : α → Option β} {k : α} (h₁ : fn k = none) : (make (List.filterMap (fun (k : α) => do let __do_lift ← fn k some (k, __do_lift)) ks)).find? k = none

theorem Cedar.Data.Map.mapOnValues_wf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] {f : β → γ} {m : Map α β} : m.WellFormed ↔ (mapOnValues f m).WellFormed

@[simp]

theorem Cedar.Data.Map.mapOnValues_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] {f : β → γ} : mapOnValues f empty = empty

theorem Cedar.Data.Map.mapOnValues_tail {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {hd₁ hd₂ : α × β} {tl₁ tl₂ : List (α × β)} : mapOnValues f (mk (hd₁ :: tl₁)) = mapOnValues f (mk (hd₂ :: tl₂)) → mapOnValues f (mk tl₁) = mapOnValues f (mk tl₂)

theorem Cedar.Data.Map.mapOnValues_doubleton {β : Type u_1} {γ : Type u_2} {f : β → γ} {s₁ s₂ : String} (b₁ b₂ : β) : mapOnValues f (mk [(s₁, b₁), (s₂, b₂)]) = mk [(s₁, f b₁), (s₂, f b₂)]

Ideally we wouldn't need this, but it's currently necessary because of the kludgy way that EntityTag.mk uses Map without relying on its proper constructors

@[simp]

theorem Cedar.Data.Map.find?_mapOnValues {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) (m : Map α β) (k : α) : (mapOnValues f m).find? k = Option.map f (m.find? k)

theorem Cedar.Data.Map.find?_mapOnValues_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} {v : β} : m.find? k = some v → (mapOnValues f m).find? k = some (f v)

theorem Cedar.Data.Map.find?_mapOnValues_some' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} {v : γ} : (mapOnValues f m).find? k = some v → ∃ (v' : β), m.find? k = some v' ∧ v = f v'

@[simp]

theorem Cedar.Data.Map.find?_mapOnValues_none {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} : (mapOnValues f m).find? k = none ↔ m.find? k = none

theorem Cedar.Data.Map.mapOnValues_eq_make_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [StrictLT α] [DecidableLT α] (f : β → γ) {m : Map α β} (wf : m.WellFormed) : mapOnValues f m = make (List.map (fun (kv : α × β) => (kv.fst, f kv.snd)) m.toList)

theorem Cedar.Data.Map.mem_toList_find? {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} {v : β} (h₁ : m.WellFormed) (h₂ : (k, v) ∈ m.toList) : m.find? k = some v

@[simp]

theorem Cedar.Data.Map.contains_mapOnValues {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} : (mapOnValues f m).contains k = m.contains k

@[simp]

theorem Cedar.Data.Map.keys_mapOnValues {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] (f : β → γ) (m : Map α β) : (mapOnValues f m).keys = m.keys

@[simp]

theorem Cedar.Data.Map.values_mapOnValues {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {f : β → γ} {m : Map α β} : (mapOnValues f m).values = List.map f m.values

@[simp]

theorem Cedar.Data.Map.mapOnValues_mapOnValues {α : Type u_1} {β : Type u_2} {γ : Type u_3} {φ : Type u_4} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {f : β → γ} {g : γ → φ} {m : Map α β} : mapOnValues g (mapOnValues f m) = mapOnValues (g ∘ f) m

theorem Cedar.Data.Map.mapOnValues_congr {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f g : β → γ} {m : Map α β} : (∀ (v : β), v ∈ m.values → f v = g v) → mapOnValues f m = mapOnValues g m

Like List.map_congr, but lifted to Map.mapOnValues

theorem Cedar.Data.Map.mapOnValues_restricted_id {β : Type u_1} {α : Type u_2} {f : β → β} {m : Map α β} : (∀ (b : β), b ∈ m.values → f b = b) → mapOnValues f m = m

theorem Cedar.Data.Map.mapOnValues_mk {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {kvs : List (α × β)} : mapOnValues f (mk kvs) = mk (List.map (fun (x : α × β) => match x with | (k, v) => (k, f v)) kvs)

@[simp]

theorem Cedar.Data.Map.mapOnValues_make {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [StrictLT α] {f : β → γ} {kvs : List (α × β)} : mapOnValues f (make kvs) = make (List.map (Prod.map id f) kvs)

@[simp]

theorem Cedar.Data.Map.mapOnValues₂_eq_mapOnValues {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizeOf α] [SizeOf β] (m : Map α β) (f : β → γ) : (m.mapOnValues₂ fun (x : { x : β // sizeOf x < sizeOf m }) => f x.val) = mapOnValues f m

theorem Cedar.Data.Map.findOrErr_returns {α : Type u_1} {β : Type u_2} {Error : Type u_3} [DecidableEq α] (m : Map α β) (k : α) (e : Error) : (∃ (v : β), m.findOrErr k e = Except.ok v) ∨ m.findOrErr k e = Except.error e

findOrErr cannot return any error other than e

@[simp]

theorem Cedar.Data.Map.findOrErr_mapOnValues {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Error : Type u_4} [LT α] [DecidableLT α] [DecidableEq α] {f : β → γ} {m : Map α β} {k : α} {e : Error} : (mapOnValues f m).findOrErr k e = Except.map f (m.findOrErr k e)

@[simp]

theorem Cedar.Data.Map.findOrErr_ok_iff_find?_some {α : Type u_1} {β : Type u_2} {Error : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] {m : Map α β} {k : α} {v : β} {e : Error} : m.findOrErr k e = Except.ok v ↔ m.find? k = some v

@[simp]

theorem Cedar.Data.Map.findOrErr_err_iff_find?_none {α : Type u_1} {β : Type u_2} {Error : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] {m : Map α β} {k : α} {e : Error} : m.findOrErr k e = Except.error e ↔ m.find? k = none

theorem Cedar.Data.Map.findOrErr_eq_match {α : Type u_1} {β : Type u_2} {ε : Type u_3} [BEq α] (m : Map α β) (k : α) (e : ε) : m.findOrErr k e = match m.find? k with | some v => Except.ok v | x => Except.error e

Equation lemma for findOrErr, for clients that cannot unfold it.

theorem Cedar.Data.Map.findOrErr_ok_implies_in_toList {α : Type u_1} {β : Type u_2} {Error : Type u_3} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} {v : β} {e : Error} : m.findOrErr k e = Except.ok v → (k, v) ∈ m.toList

The converse requires the wf precondition, and is available in findOrErr_ok_iff_in_toList below

theorem Cedar.Data.Map.findOrErr_ok_iff_in_toList {α : Type u_1} {β : Type u_2} {Error : Type u_3} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} {v : β} {e : Error} (wf : m.WellFormed) : m.findOrErr k e = Except.ok v ↔ (k, v) ∈ m.toList

The mp direction of this does not need the wf precondition and, in fact, is available separately as findOrErr_ok_implies_in_toList above

theorem Cedar.Data.Map.find?_some_implies_in_values {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [DecidableEq α] {m : Map α β} {k : α} {v : β} : m.find? k = some v → v ∈ m.values

The converse requires the wf precondition, and is available in find?_some_iff_in_values below

theorem Cedar.Data.Map.findOrErr_ok_implies_in_values {α : Type u_1} {β : Type u_2} {Error : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] {m : Map α β} {k : α} {v : β} {e : Error} : m.findOrErr k e = Except.ok v → v ∈ m.values

The converse requires the wf precondition, and is available in findOrErr_ok_iff_in_values below

theorem Cedar.Data.Map.find?_some_iff_in_values {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {v : β} (wf : m.WellFormed) : (∃ (k : α), m.find? k = some v) ↔ v ∈ m.values

The mp direction of this does not need the wf precondition and, in fact, is available separately as find?_some_implies_in_values above

theorem Cedar.Data.Map.findOrErr_ok_iff_in_values {α : Type u_1} {β : Type u_2} {Error : Type u_3} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {v : β} {e : Error} (wf : m.WellFormed) : (∃ (k : α), m.findOrErr k e = Except.ok v) ↔ v ∈ m.values

The mp direction of this does not need the wf precondition and, in fact, is available separately as findOrErr_ok_implies_in_values above

theorem Cedar.Data.Map.findOrErr_err_iff_not_in_keys {α : Type u_1} {β : Type u_2} {Error : Type u_3} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} {e : Error} (wf : m.WellFormed) : m.findOrErr k e = Except.error e ↔ ¬k ∈ m.keys

theorem Cedar.Data.Map.in_toList_in_mapOnValues {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} {v : β} : (k, v) ∈ m.toList → (k, f v) ∈ (mapOnValues f m).toList

The converse requires the extra precondition that f is injective, and is available as in_mapOnValues_in_toList

theorem Cedar.Data.Map.find?_none_iff_findorErr_errors {α : Type u_1} {β : Type u_2} {Error : Type u_3} [LT α] [DecidableLT α] [DecidableEq α] {m : Map α β} {k : α} (e : Error) : m.find? k = none ↔ m.findOrErr k e = Except.error e

TODO: This is redundant with findOrErr_err_iff_find?_none

theorem Cedar.Data.Map.in_mapOnValues_in_toList {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {f : β → γ} {m : Map α β} {k : α} {v : β} : (k, f v) ∈ (mapOnValues f m).toList → (∀ (v' : β), f v = f v' → v = v') → (k, v) ∈ m.toList

Converse of in_toList_in_mapOnValues; requires the extra precondition that f is injective

theorem Cedar.Data.Map.in_mapOnValues_in_toList' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {f : β → γ} {m : Map α β} {k : α} {v' : γ} : (k, v') ∈ (mapOnValues f m).toList → ∃ (v : β), f v = v' ∧ (k, v) ∈ m.toList

Slightly different formulation of in_mapOnValues_in_toList

mapMOnValues

theorem Cedar.Data.Map.mapMOnValues₂_eq_mapMOnValues {m : Type → Type u_1} {α β γ : Type} [LT α] [DecidableLT α] [SizeOf α] [SizeOf β] [Monad m] [LawfulMonad m] (map : Map α β) (f : β → m γ) : (map.mapMOnValues₂ fun (x : { x : β // sizeOf x < sizeOf map }) => f x.val) = mapMOnValues f map

@[simp]

theorem Cedar.Data.Map.mapMOnValues_empty {α : Type u_1} {m : Type (max u_1 u_2) → Type u_3} {β : Type u_4} {γ : Type (max u_1 u_2)} [LT α] [DecidableLT α] [Monad m] [LawfulMonad m] (f : β → m γ) : mapMOnValues f empty = pure empty

@[simp]

theorem Cedar.Data.Map.mapMOnValues_mapOnValues {α : Type u_1} {m : Type (max u_1 u_2) → Type u_3} {β : Type u_4} {γ : Type u_5} {φ : Type (max u_1 u_2)} [LT α] [DecidableLT α] [Monad m] [LawfulMonad m] (map : Map α β) (f : β → γ) (g : γ → m φ) : mapMOnValues g (mapOnValues f map) = mapMOnValues (g ∘ f) map

theorem Cedar.Data.Map.mapMOnValues_some {α : Type u_1} {β : Type (max u_1 u_2)} [LT α] [DecidableLT α] (m : Map α β) : mapMOnValues some m = some m

Mapping every value to some preserves the map.

theorem Cedar.Data.Map.mapMOnValues_isSome {α : Type u_1} {β : Type u_2} {γ : Type (max u_1 u_3)} [LT α] [DecidableLT α] (m : Map α β) (f : β → Option γ) : (mapMOnValues f m).isSome = m.values.all fun (value : β) => (f value).isSome

Mapping map values succeeds exactly when every application succeeds.

theorem Cedar.Data.Map.mapMOnValues_preserves_keys {α : Type u_1} {β : Type u_2} {γ : Type (max u_1 u_3)} [LT α] [DecidableLT α] [StrictLT α] {f : β → Option γ} {m₁ : Map α β} {m₂ : Map α γ} : mapMOnValues f m₁ = some m₂ → List.map Prod.fst m₁.toList = List.map Prod.fst m₂.toList

This is not stated in terms of Map.keys because Map.keys produces a Set, and we want the even stronger property that it not only preserves the key-set, but also the key-order. (We'll use this to prove mapMOnValues_some_wf.)

theorem Cedar.Data.Map.mapMOnValues_some_wf {α : Type u_1} {β : Type u_2} {γ : Type (max u_1 u_3)} [LT α] [DecidableLT α] [StrictLT α] {f : β → Option γ} {m₁ : Map α β} {m₂ : Map α γ} : m₁.WellFormed → mapMOnValues f m₁ = some m₂ → m₂.WellFormed

theorem Cedar.Data.Map.mapMOnValues_ok_wf {α : Type u_1} {β : Type u_2} {ε : Type u_3} {γ : Type (max u_1 u_4)} [LT α] [DecidableLT α] [StrictLT α] {f : β → Except ε γ} {m₁ : Map α β} {m₂ : Map α γ} : m₁.WellFormed → mapMOnValues f m₁ = Except.ok m₂ → m₂.WellFormed

theorem Cedar.Data.Map.mapMOnValues_cons {β : Type u_1} {γ : Type u_2} {α : Type} [LT α] [DecidableLT α] {f : β → Option γ} {m : Map α β} {k : α} {v : β} {tl : List (α × β)} : m.toList = (k, v) :: tl → mapMOnValues f m = do let v' ← f v let tl' ← mapMOnValues f (mk tl) pure (mk ((k, v') :: tl'.toList))

theorem Cedar.Data.Map.mapOnValues_eq_of_mapMOnValues_some {α : Type u_1} {β : Type u_2} {γ : Type (max u_1 u_3)} [LT α] [DecidableLT α] {m : Map α β} {out : Map α γ} {f : β → Option γ} (g : β → γ) (hmap : mapMOnValues f m = some out) (hfg : ∀ (input : β) (output : γ), f input = some output → g input = output) : mapOnValues g m = out

If a partial map of values succeeds, mapping a corresponding total function produces the same map.

theorem Cedar.Data.Map.mapMOnValues_some_implies_all_some {β : Type u_1} {γ : Type u_2} {α : Type} [LT α] [DecidableLT α] {f : β → Option γ} {m₁ : Map α β} {m₂ : Map α γ} : mapMOnValues f m₁ = some m₂ → ∀ (kv : α × β), kv ∈ m₁.toList → ∃ (v : γ), (kv.fst, v) ∈ m₂.toList ∧ f kv.snd = some v

theorem Cedar.Data.Map.mapMOnValues_some_implies_all_from_some {α : Type u_1} {β : Type u_2} {γ : Type (max u_1 u_3)} [LT α] [DecidableLT α] {f : β → Option γ} {m₁ : Map α β} {m₂ : Map α γ} : mapMOnValues f m₁ = some m₂ → ∀ (kv : α × γ), kv ∈ m₂.toList → ∃ (v : β), (kv.fst, v) ∈ m₁.toList ∧ f v = some kv.snd

theorem Cedar.Data.Map.mapMOnValues_none_iff_exists_none {β : Type u_1} {γ : Type u_2} {α : Type} [LT α] [DecidableLT α] {f : β → Option γ} {m : Map α β} : mapMOnValues f m = none ↔ ∃ (v : β), v ∈ m.values ∧ f v = none

theorem Cedar.Data.Map.mapMOnValues_ok_implies_all_ok {α : Type u_1} {β : Type u_2} {ε : Type u_3} {γ : Type (max u_1 u_4)} [LT α] [DecidableLT α] {f : β → Except ε γ} {m₁ : Map α β} {m₂ : Map α γ} : mapMOnValues f m₁ = Except.ok m₂ → ∀ (kv : α × β), kv ∈ m₁.toList → ∃ (v : γ), (kv.fst, v) ∈ m₂.toList ∧ f kv.snd = Except.ok v

Note that the converse is not true: counterexample m₁ is [(1, false)], m₂ is [(1, false), (2, true)], f is Except.ok

But for a limited converse, see all_ok_implies_mapMOnValues_ok

theorem Cedar.Data.Map.mapMOnValues_ok_implies_all_from_ok {α : Type u_1} {β : Type u_2} {ε : Type u_3} {γ : Type (max u_1 u_4)} [LT α] [DecidableLT α] {f : β → Except ε γ} {m₁ : Map α β} {m₂ : Map α γ} : mapMOnValues f m₁ = Except.ok m₂ → ∀ (kv : α × γ), kv ∈ m₂.toList → ∃ (v : β), (kv.fst, v) ∈ m₁.toList ∧ f v = Except.ok kv.snd

theorem Cedar.Data.Map.all_ok_implies_mapMOnValues_ok {α : Type u_1} {β : Type u_2} {ε : Type u_3} {γ : Type (max u_1 u_4)} [LT α] [DecidableLT α] {f : β → Except ε γ} {m₁ : Map α β} : (∀ (kv : α × β), kv ∈ m₁.toList → ∃ (v : γ), f kv.snd = Except.ok v) → ∃ (m₂ : Map α γ), mapMOnValues f m₁ = Except.ok m₂

theorem Cedar.Data.Map.mapMOnValues_error_implies_exists_error {α : Type u_1} {β : Type u_2} {ε : Type u_3} {γ : Type (max u_1 u_4)} [LT α] [DecidableLT α] {f : β → Except ε γ} {m : Map α β} {e : ε} : mapMOnValues f m = Except.error e → ∃ (v : β), v ∈ m.values ∧ f v = Except.error e

theorem Cedar.Data.Map.wellFormed_correct {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableLT α] {m : Map α β} : m.wellFormed = true ↔ m.WellFormed

theorem Cedar.Data.Map.make_find?_eq_list_find? {α : Type u_1} {β : Type u_2} [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] {l : List (α × β)} {k : α} : (make l).find? k = Option.map Prod.snd (List.find? (fun (x : α × β) => x.fst == k) l)

theorem Cedar.Data.Map.make_toList_map_find? {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] (m : Map α β) (g : α → β → γ) (k : α) : (make (List.map (fun (kv : α × β) => (kv.fst, g kv.fst kv.snd)) m.toList)).find? k = Option.map (g k) (m.find? k)

Rebuilding a map from its entries with key-dependent values.

theorem Cedar.Data.Map.list_find?_iff_make_find? {α : Type u_1} {β : Type u_2} [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] {l : List (α × β)} {k : α} {v : β} : List.find? (fun (x : α × β) => x.fst == k) l = some (k, v) ↔ (make l).find? k = some v

theorem Cedar.Data.Map.list_find?_iff_mk_find? {α : Type u_1} {β : Type u_2} [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] {l : List (α × β)} {k : α} {v : β} : List.find? (fun (x : α × β) => x.fst == k) l = some (k, v) ↔ (mk l).find? k = some v

theorem Cedar.Data.Map.map_make_append_find_disjoint {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableEq α] [DecidableLT α] [SizeOf α] [SizeOf β] {l₁ l₂ : List (α × β)} {k : α} (hfind₁ : List.find? (fun (x : α × β) => match x with | (k', snd) => k' == k) l₁ = none) (hfind₂ : (List.find? (fun (x : α × β) => match x with | (k', snd) => k' == k) l₂).isSome = true) : ∃ (v : β), (make (l₁ ++ l₂)).find? k = some v ∧ (k, v) ∈ l₂

If a key exists in l₂ but not in l₁, then Map.make (l₁ ++ l₂) contains that key.

theorem Cedar.Data.Map.make_map_values_find {α : Type u_1} {β : Type u_2} [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] {l : List α} {f : α → β} {k : α} (hfind : k ∈ l) : (make (List.map (fun (x : α) => (x, f x)) l)).find? k = some (f k)

theorem Cedar.Data.Map.map_toList_findSome? {α : Type u_1} {β : Type u_2} {γ : Type u_3} [BEq α] [LawfulBEq α] {m : Map α β} {k : α} {v : β} {v' : γ} {f : α × β → Option γ} (hfind : m.find? k = some v) (hf : ∀ (kv : α × β), (∃ (v' : γ), f kv = some v') → kv.fst = k) (hkv : f (k, v) = some v') : List.findSome? f m.toList = some v'

theorem Cedar.Data.Map.map_find?_to_list_find? {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] {m : Map α β} {k : α} {v : β} (hfind : m.find? k = some v) : List.find? (fun (x : α × β) => x.fst == k) m.toList = some (k, v)

theorem Cedar.Data.Map.map_make_append_find_disjoint' {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableEq α] [DecidableLT α] [SizeOf α] [SizeOf β] {l₁ l₂ : List (α × β)} {k : α} {v : β} (hfind₁ : List.find? (fun (x : α × β) => match x with | (k', snd) => k' == k) l₁ = none) (hfind₂ : List.find? (fun (x : α × β) => match x with | (k', snd) => k' == k) l₂ = some (k, v)) (heq : ∀ (x₁ x₂ : α × β), x₁ ∈ l₂ → x₂ ∈ l₂ → x₁.fst = x₂.fst → x₁ = x₂) : (make (l₁ ++ l₂)).find? k = some v

A variant of map_make_append_find_disjoint.

theorem Cedar.Data.Map.map_find?_implies_find?_weaker_pred {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] {m : Map α β} {k : α} {v : β} {f : α × β → Bool} (hfind : m.find? k = some v) (hf : ∀ (kv : α × β), f kv = true → kv.fst = k) (hkv : f (k, v) = true) : List.find? f m.toList = some (k, v)

theorem Cedar.Data.Map.map_keys_empty_implies_map_empty {α : Type u_1} {β : Type u_2} {m : Map α β} (h : m.keys.toList = []) : m = empty

theorem Cedar.Data.Map.toList_congr {α : Type u_1} {β : Type u_2} {m₁ m₂ : Map α β} (h : m₁.toList = m₂.toList) : m₁ = m₂

TODO: This is redundant with eq_iff_toList_eq

@[simp]

theorem Cedar.Data.Map.find?_append {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableEq α] [DecidableLT α] {m₁ m₂ : Map α β} {k : α} : (m₁ ++ m₂).find? k = (m₁.find? k).or (m₂.find? k)

@[simp]

theorem Cedar.Data.Map.contains_append {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {m₁ m₂ : Map α β} {k : α} : (m₁ ++ m₂).contains k = true ↔ m₁.contains k = true ∨ m₂.contains k = true

theorem Cedar.Data.Map.find?_append_right {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableEq α] [DecidableLT α] {m₁ m₂ : Map α β} {k : α} : m₁.contains k = false → (m₁ ++ m₂).find? k = m₂.find? k

theorem Cedar.Data.Map.find?_append_left {α : Type u_1} {β : Type u_2} [LT α] [StrictLT α] [DecidableEq α] [DecidableLT α] {m₁ m₂ : Map α β} {k : α} : m₂.contains k = false → (m₁ ++ m₂).find? k = m₁.find? k

theorem Cedar.Data.Map.filter_wf {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] (p : α → β → Bool) (m : Map α β) : m.WellFormed → (filter p m).WellFormed

theorem Cedar.Data.Map.find?_filter_if_find? {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {k : α} {val : β} {m : Map α β} {p : α → β → Bool} : m.find? k = some val → p k val = true → (filter p m).find? k = some val

theorem Cedar.Data.Map.find?_filter_iff_find {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [DecidableEq α] [LT α] [StrictLT α] [DecidableLT α] {k : α} {val : β} {m : Map α β} {p : α → β → Bool} : m.WellFormed → (m.find? k = some val ∧ p k val = true ↔ (filter p m).find? k = some val)

theorem Cedar.Data.Map.filter_contains_if_find_matching {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {k : α} {m : Map α β} {p : α → β → Bool} : (∃ (v : β), m.find? k = some v ∧ p k v = true) → (filter p m).contains k = true

theorem Cedar.Data.Map.find_matching_iff_filter_contains {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {k : α} {m : Map α β} (p : α → β → Bool) : m.WellFormed → ((∃ (v : β), m.find? k = some v ∧ p k v = true) ↔ (filter p m).contains k = true)

theorem Cedar.Data.Map.filter_not_contains {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] (k : α) (m : Map α β) : (filter (fun (k' : α) (x : β) => k' != k) m).contains k = false