Some lemmas to simplify UDFs.
theorem
Cedar.Thm.map_make_filterMap_find?
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
{κ : Type u_4}
[BEq α]
[LawfulBEq α]
[DecidableEq γ]
[LT γ]
[DecidableLT γ]
[Data.StrictLT γ]
{m : Data.Map α β}
{k : α}
{v : β}
{k' : γ}
{v' : κ}
{f : α × β → Option (γ × κ)}
(hfind : m.find? k = some v)
(hkv : f (k, v) = some (k', v'))
(hf : ∀ (kv : α × β), (∃ (v'' : κ), f kv = some (k', v'')) → kv.fst = k)
:
For simplifying Factory.app on a UDF with a table
of the form make (m.toList.filterMap f).
theorem
Cedar.Thm.map_make_filterMap_find?_none
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
{κ : Type u_4}
[LT α]
[DecidableLT α]
[Data.StrictLT α]
[DecidableEq α]
[DecidableEq γ]
[LT γ]
[DecidableLT γ]
[Data.StrictLT γ]
{m : Data.Map α β}
{k : α}
{k' : γ}
{f : α × β → Option (γ × κ)}
(hfind : m.find? k = none)
(hf : ∀ (kv : α × β), (∃ (v'' : κ), f kv = some (k', v'')) → kv.fst = k)
:
Similar to above but for the none case
theorem
Cedar.Thm.app_table_make_filterMap
{α : Type u_1}
{β : Type u_2}
[BEq α]
[LawfulBEq α]
{arg out : SymCC.TermType}
{default : SymCC.Term}
{m : Data.Map α β}
{k : α}
{v : β}
{t r : SymCC.Term}
{f : α × β → Option (SymCC.Term × SymCC.Term)}
(hfind : m.find? k = some v)
(hkv : f (k, v) = some (t, r))
(hf : ∀ (kv : α × β), (∃ (v'' : SymCC.Term), f kv = some (t, v'')) → kv.fst = k)
(hlit : t.isLiteral = true)
:
SymCC.Factory.app
(SymCC.UnaryFunction.udf
{ arg := arg, out := out, table := Data.Map.make (List.filterMap f m.toList), default := default })
t = r
Simplifying Factory.app on a UDF with a table
of the form make (m.toList.filterMap f).
theorem
Cedar.Thm.map_make_filterMap_flatten_find?
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{κ : Type u_4}
[BEq α]
[BEq β]
[LawfulBEq α]
[LawfulBEq β]
[DecidableEq γ]
[LT γ]
[DecidableLT γ]
[Data.StrictLT γ]
{m : Data.Map α β}
{k : α}
{v : β}
{k' : γ}
{v' : κ}
{f : α × β → Option (List (γ × κ))}
(hfind : m.find? k = some v)
(hkv : ∃ (l : List (γ × κ)), f (k, v) = some l ∧ List.find? (fun (x : γ × κ) => x.fst == k') l = some (k', v'))
(hf :
∀ (kv : α × β),
(∃ (l : List (γ × κ)), f kv = some l ∧ (List.find? (fun (x : γ × κ) => x.fst == k') l).isSome = true) → kv.fst = k)
:
For simplifying Factory.app on a UDF with a table
of the form make (m.toList.filterMap f).flatten.