a few more utilities (#513)

Signed-off-by: Craig Disselkoen <cdiss@amazon.com>

cedar-lean/Cedar/Data/Set.lean

@@ -109,6 +109,13 @@ def size {α} (s : Set α) : Nat :=
 def singleton {α} (a : α) : Set α :=
   Set.mk [a]
 
+/-- If `s` is a singleton set, returns the single element -/
+def singleton? [Inhabited α] (s : Set α) : Option α :=
+  match s.elts with
+  | [] => none
+  | [x] => x
+  | _ => none
+
 def foldl {α β} (f : α → β → α) (init : α) (s : Set β) : α :=
   s.elts.foldl f init
 

cedar-lean/Cedar/Spec/Value.lean

@@ -41,12 +41,21 @@ structure Name where
   id : Id
   path : List Id
 
+instance : ToString Name where
+  toString n := String.join (n.path.map λ s => s!"{s}::") ++ n.id
+
 abbrev EntityType := Name
 
+instance : ToString EntityType where
+  toString ety := let n : Name := ety ; ToString.toString n
+
 structure EntityUID where
   ty : EntityType
   eid : String
 
+instance : ToString EntityUID where
+  toString euid := s!"{euid.ty}::\"{euid.eid}\""
+
 inductive Prim where
   | bool (b : Bool)
   | int (i : Data.Int64)

cedar-lean/Cedar/Thm/Data/List/Lemmas.lean

@@ -865,6 +865,21 @@ theorem foldl_pmap_subtype
   case nil => simp only [pmap, foldl_nil]
   case cons ih => apply ih
 
+theorem foldl_congr {f g : β → α → β} {init : β} {l : List α} :
+  (∀ b x, x ∈ l → f b x = g b x) → foldl f init l = foldl g init l
+:= by
+  intro h
+  induction l generalizing init
+  case nil =>
+    simp only [not_mem_nil, false_implies, implies_true, foldl_nil, imp_self]
+  case cons lhd ltl ih =>
+    simp only [mem_cons, forall_eq_or_imp, foldl_cons,
+      h init lhd (by simp only [mem_cons, true_or])]
+    apply ih
+    intro b x hin
+    apply h b x
+    simp only [mem_cons, hin, or_true]
+
 /-! ### foldlM -/
 
 theorem foldlM_of_assoc_some (f : α → α → Option α) (x₀ x₁ x₂ x₃ : α) (xs : List α)

cedar-lean/Cedar/Thm/Data/Map.lean

@@ -359,6 +359,18 @@ theorem find?_notmem_keys [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α
       replace h₂ := List.mem_of_find?_eq_some h₂
       exact in_list_in_keys h₂
 
+theorem find?_none_all_absent [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} :
+  m.find? k = none → ∀ v, ¬ (k, v) ∈ m.kvs
+:= by
+  intro hn v
+  by_contra hc
+  simp only [find?] at hn
+  cases hf : List.find? (fun x => x.fst == k) m.kvs <;>
+  simp only [hf, reduceCtorEq] at hn
+  simp only [List.find?_eq_none, beq_iff_eq] at hf
+  specialize hf (k, v) hc
+  simp only [not_true_eq_false] at hf
+
 theorem mapOnValues_wf [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] {f : β → γ} {m : Map α β} :
   m.WellFormed ↔ (m.mapOnValues f).WellFormed
 := by

cedar-lean/DiffTest/Main.lean

@@ -34,6 +34,7 @@ open Proto
 
 structure Timed (α : Type) where
   data : α
+  /-- Duration in nanoseconds -/
   duration : Nat
 deriving Lean.ToJson
 
@@ -46,6 +47,15 @@ def runAndTime (f : Unit -> α) : BaseIO (Timed α) := do
     duration := stop - start
   }
 
+def runAndTimeIO (f : IO α) : IO (Timed α) := do
+  let start ← IO.monoNanosNow
+  let result ← f
+  let stop ← IO.monoNanosNow
+  .ok {
+    data := result,
+    duration := stop - start
+  }
+
 /--
   `req`: binary protobuf for an `AuthorizationRequest`