more work on List/Map/Set lemmas

cedar-lean/Cedar/Data/List.lean

@@ -297,7 +297,7 @@ theorem insertCanonical_singleton [LT β] [DecidableLT β] (f : α → β)  (x :
   insertCanonical f x [] = [x]
 := by unfold insertCanonical; rfl
 
-theorem insertCanonical_not_nil [DecidableEq β] [LT β] [DecidableRel (α := β) (· < ·)] (f : α → β) (x : α) (xs : List α) :
+theorem insertCanonical_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) :
   insertCanonical f x xs ≠ []
 := by
   unfold insertCanonical
@@ -434,6 +434,23 @@ theorem canonicalize_nil [LT β] [DecidableLT β] (f : α → β) :
   canonicalize f [] = []
 := by unfold canonicalize; rfl
 
+theorem canonicalize_nil' [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (xs : List α) :
+  xs = [] ↔ (canonicalize f xs) = []
+:= by
+  constructor
+  case mp =>
+    intro h₁ ; subst h₁
+    exact canonicalize_nil f
+  case mpr =>
+    intro h₁
+    cases xs with
+    | nil => trivial
+    | cons x xs =>
+      simp
+      unfold canonicalize at h₁
+      apply insertCanonical_not_nil f x (canonicalize f xs)
+      exact h₁
+
 theorem canonicalize_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (xs : List α) :
   xs ≠ [] ↔ (canonicalize f xs) ≠ []
 := by

cedar-lean/Cedar/Data/Map.lean

@@ -55,6 +55,10 @@ def empty {α β} : Map α β := .mk []
 def keys {α β} (m : Map α β) : Set α :=
   Set.mk (m.kvs.map Prod.fst) -- well-formed by construction
 
+/-- Returns the values of `m` as a list. -/
+def values {α β} (m : Map α β) : List β :=
+  m.kvs.map Prod.snd
+
 /-- Returns the binding for `k` in `m`, if any. -/
 def find? {α β} [BEq α] (m : Map α β) (k : α) : Option β :=
   match m.kvs.find? (fun ⟨k', _⟩ => k' == k) with
@@ -116,6 +120,10 @@ theorem not_contains_of_empty {α β} [BEq α] (k : α) :
   ¬ (Map.empty : Map α β).contains k
 := by simp [contains, empty, find?, List.find?]
 
+theorem make_nil_is_empty {α β} [LT α] [DecidableLT α] :
+  (Map.make [] : Map α β) = Map.empty
+:= by simp [make, empty, List.canonicalize_nil]
+
 end Map
 
 end Cedar.Data

cedar-lean/Cedar/Data/Set.lean

@@ -75,6 +75,9 @@ def intersect {α} [BEq α] (s₁ s₂ : Set α) : Set α :=
 def union {α} [LT α] [DecidableLT α] (s₁ s₂ : Set α) : Set α :=
   make (s₁.elts ++ s₂.elts)           -- enforce well-formedness
 
+instance [LT α] [DecidableLT α] : HAppend (Set α) (Set α) (Set α) where
+  hAppend := Set.union
+
 /-- Filters `s` using `f`. -/
 def filter {α} (f : α → Bool) (s : Set α) : Set α :=
   Set.mk (s.elts.filter f)            -- well-formed by construction
@@ -128,16 +131,62 @@ theorem contains_prop_bool_equiv [DecidableEq α] {v : α} {s : Set α} :
   apply List.elem_eq_true_of_mem
   assumption
 
-theorem in_list_in_set {α : Type u} (v : α) (s : Set α) :
-  v ∈ s.elts → v ∈ s
+theorem in_list_iff_in_set {α : Type u} (v : α) (s : Set α) :
+  v ∈ s.elts ↔ v ∈ s
 := by
-  intro h0
-  apply h0
+  constructor
+  case mp => intro h ; apply h
+  case mpr => simp [elts, Membership.mem]
+
+theorem in_list_iff_in_mk {α : Type u} (v : α) (xs : List α) :
+  v ∈ xs ↔ v ∈ mk xs
+:= by
+  constructor
+  case mp => intro h ; apply h
+  case mpr => simp [elts, Membership.mem]
 
-theorem in_set_in_list {α : Type u} (v : α) (s : Set α) :
-  v ∈ s → v ∈ s.elts
+theorem non_empty_iff_exists [DecidableEq α] (s : Set α) :
+  ¬ s.isEmpty ↔ ∃ a, a ∈ s
 := by
-  simp [elts, Membership.mem]
+  simp [Set.isEmpty, Set.empty]
+  constructor
+  case mp =>
+    intro h₁
+    apply List.exists_mem_of_ne_nil s.elts
+    intro h₂
+    apply h₁ ; clear h₁
+    cases s
+    simp [Set.elts] at *
+    assumption
+  case mpr =>
+    intro h₁
+    replace ⟨a, h₁⟩ := h₁
+    intro h₂
+    rw [← in_list_iff_in_set] at h₁
+    cases s
+    simp at h₂
+    subst h₂
+    simp [elts] at h₁
+
+theorem empty_iff_not_exists [DecidableEq α] (s : Set α) :
+  s.isEmpty ↔ ¬ ∃ a, a ∈ s
+:= by
+  simp [Set.isEmpty, Set.empty]
+  constructor
+  case mp =>
+    intro h₁
+    subst h₁
+    apply List.not_mem_nil
+  case mpr =>
+    intro h₁
+    cases s
+    case mk xs =>
+      rw [mk.injEq]
+      rw [List.eq_nil_iff_forall_not_mem]
+      intro x
+      specialize h₁ x
+      rw [in_list_iff_in_mk]
+      assumption
 
 theorem mem_cons_self {α : Type u} (hd : α) (tl : List α) :
   hd ∈ Set.mk (hd :: tl)
@@ -160,6 +209,20 @@ theorem in_set_means_list_non_empty {α : Type u} (v : α) (s : Set α) :
   specialize h1 v
   contradiction
 
+theorem make_empty [DecidableEq α] [LT α] [DecidableLT α] (xs : List α) :
+  xs = [] ↔ (Set.make xs).isEmpty
+:= by
+  unfold isEmpty; unfold empty; unfold make
+  constructor
+  case mp =>
+    intro h₁ ; subst h₁
+    simp
+    apply List.canonicalize_nil
+  case mpr =>
+    intro h₁ ; simp at h₁
+    apply (List.canonicalize_nil' id xs).mpr
+    assumption
+
 theorem make_non_empty [DecidableEq α] [LT α] [DecidableLT α] (xs : List α) :
   xs ≠ [] ↔ (Set.make xs).isEmpty = false
 := by
@@ -210,19 +273,14 @@ theorem elts_make_equiv [LT α] [DecidableLT α] [StrictLT α] {xs : List α} :
   case left =>
     intro a h₁
     rw [make_mem]
-    exact in_list_in_set a (make xs) h₁
+    rw [← in_list_iff_in_set]
+    exact h₁
   case right =>
     intro a h₁
-    apply in_set_in_list
+    rw [in_list_iff_in_set]
     rw [← make_mem]
     exact h₁
 
-theorem in_set_in_list' [LT α] [DecidableLT α] [StrictLT α] (v : α) (xs : List α) :
-  v ∈ (Set.make xs) → v ∈ xs
-:= by
-  rw [make_mem]
-  simp
-
 theorem make_any_iff_any [LT α] [DecidableLT α] [StrictLT α] (f : α → Bool) (xs : List α) :
   (Set.make xs).any f = xs.any f
 := by

cedar-lean/Cedar/Thm/Authorization/Authorizer.lean

@@ -362,8 +362,9 @@ theorem if_mapM'_doesn't_fail_on_list_then_doesn't_fail_on_set [LT α] [Decidabl
   simp [mapM'_ok_iff_f_ok_on_all_elements]
   intro h₁ y h₂
   apply h₁ y; clear h₁
-  apply Set.in_set_in_list' y list
-  exact Set.in_list_in_set y (Set.make list) h₂
+  rw [Set.make_mem]
+  rw [← Set.in_list_iff_in_set]
+  exact h₂
 
 theorem mapM'_asEntityUID_on_set_uids_produces_ok {uids : List EntityUID} :
   Except.isOk (List.mapM' Value.asEntityUID (Set.elts (Set.make (uids.map (Value.prim ∘ Prim.entityUID)))))

cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean

@@ -613,10 +613,10 @@ theorem entity_type_in_false_implies_inₛ_false {euid : EntityUID} {euids : Lis
     specialize h₃ euid' h₄ ; subst h₃
     split at h₂ <;> rename_i h₉ <;> simp [h₁] at h₉
     subst h₉
-    have h₉ := Set.in_set_in_list euid'.ty entry.ancestors h₇
-    simp [Set.contains, Set.elts] at h₂ h₉
-    rw [←List.elem_iff] at h₉
-    rw [h₂] at h₉
+    rw [← Set.in_list_iff_in_set] at h₇
+    simp [Set.contains, Set.elts] at h₂ h₇
+    rw [←List.elem_iff] at h₇
+    rw [h₂] at h₇
     contradiction