First draft formalism of levels

Signed-off-by: Aaron Eline <[email protected]>

cedar-lean/Cedar/Data/Map.lean

@@ -88,6 +88,23 @@ def size {α β} (m : Map α β) : Nat :=
 def mapOnValues {α β γ} [LT α] [DecidableLT α] (f : β → γ) (m : Map α β) : Map α γ :=
   Map.mk (m.kvs.map (λ (k, v) => (k, f v)))
 
+def mapOnValuesAttach {α β γ} [LT α] [DecidableLT α] (m : Map α β) (f : {x : β // ∃ (k : α), (k,x) ∈ m.kvs} → γ) : Map α γ :=
+  let wrapper (prod : {x // x ∈ m.kvs}) : {x // ∃ k, (k,x) ∈ m.kvs} :=
+    let property : ∃ k, (k, prod.val.snd) ∈ m.kvs := by
+      have h := prod.property
+      cases heq : prod.val
+      rename_i fst snd
+      exists fst
+      simp
+      rw [← heq]
+      assumption
+    { val := prod.val.snd, property := property }
+  let f' (prod : {x // x ∈ m.kvs}) :=
+    let key := prod.val.fst
+    let value := wrapper prod
+    (key, f value)
+  Map.mk (m.kvs.map₁ (λ p => f' p))
+
 def mapOnKeys {α β γ} [LT γ] [DecidableLT γ] (f : α → γ) (m : Map α β) : Map γ β :=
   Map.make (m.kvs.map (λ (k, v) => (f k, v)))
 
@@ -99,6 +116,14 @@ def mapMOnKeys {α β γ} [LT γ] [DecidableLT γ] [Monad m] (f : α → m γ) (
   let kvs ← map.kvs.mapM (λ (k, v) => f k >>= λ k' => pure (k', v))
   pure (Map.make kvs)
 
+
+
+def Equiv {α β} [LT α] [DecidableLT α] [BEq α] (m₁ m₂ : Map α β) : Prop :=
+  ∀ (k : α),
+    m₁.find? k = m₂.find? k
+
+infix:50 " ≃ " => Equiv
+
 ----- Instances -----
 
 instance [LT (Prod α β)] : LT (Map α β) where

cedar-lean/Cedar/Spec/Value.lean

@@ -127,6 +127,19 @@ instance : Coe Value (Result (Data.Set Value)) where
 
 ----- Derivations -----
 
+instance : LawfulBEq Attr where
+  rfl := by
+    intros a
+    simp
+  eq_of_beq := by
+    intros a b h
+    unfold Attr at a
+    unfold Attr at b
+    apply LawfulBEq.eq_of_beq
+    assumption
+
+
+deriving instance Repr, DecidableEq, BEq, LT  for Attr
 deriving instance Repr, DecidableEq, BEq for Except
 deriving instance Repr, DecidableEq for Error
 deriving instance Repr, DecidableEq, Inhabited, Lean.ToJson for Name

cedar-lean/Cedar/Thm.lean

@@ -18,3 +18,5 @@ import Cedar.Thm.Authorization
 import Cedar.Thm.Partial
 import Cedar.Thm.Slicing
 import Cedar.Thm.Typechecking
+import Cedar.Thm.Entities
+import Cedar.Thm.Validation

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

@@ -1279,4 +1279,23 @@ theorem mem_pmap_subtype
 := by
   induction as <;> simp [*]
 
+theorem in_lists_means_smaller [SizeOf α] (x : α) (list : List α)
+  (h : x ∈ list) :
+  sizeOf x < sizeOf list
+  := by
+  cases list
+  case nil =>
+    cases h
+  case cons head tail =>
+    cases h
+    case _ =>
+      simp
+      omega
+    case _ in_tail =>
+      have step : sizeOf x < sizeOf tail := by
+        apply in_lists_means_smaller
+        assumption
+      simp
+      omega
+
 end List

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

@@ -559,6 +559,225 @@ theorem in_kvs_in_mapOnValues [LT α] [DecidableLT α] [DecidableEq α] {f : β
   simp only [kvs, List.mem_map, Prod.mk.injEq]
   exists (k, v)
 
+/--
+  We can remove the attach for the sake of proofs
+-/
+theorem mapOnValuesAttachIsMapOnValues
+  {α : Type u} {β γ : Type v} [LT α] [DecidableLT α]
+  {m : Map α β}
+  {f : β → γ} :
+  m.mapOnValues f = m.mapOnValuesAttach (λ prod => f prod.val)
+  := by
+  rw [← eq_iff_kvs_eq]
+  simp [mapOnValues, mapOnValuesAttach]
+  rw [← List.map₁_eq_map]
+
+theorem mapOnValues_cons
+  {α : Type u} {β γ : Type v} [LT α] [DecidableLT α] [BEq α ]
+  {f : β → γ}
+  {kv : α × β}
+  {kvs : List (α × β)}
+  :
+  (Map.mk (kv :: kvs)).mapOnValues f =
+  Map.mk ((kv.fst, f kv.snd) :: ((Map.mk kvs).mapOnValues f).kvs)
+  := by
+  rw [← eq_iff_kvs_eq]
+  simp [mapOnValues, List.map]
+
+/--
+  Keys are not effected by mapping on values
+  ie: the domain of a map is unchanged by map on values
+-/
+theorem mapOnValuesAttach_preservesContains
+  {α : Type u} {β γ : Type v} [LT α] [DecidableLT α] [BEq α ] [LawfulBEq α] [DecidableEq α]
+  {m : Map α β}
+  {f : β → γ}
+  {k : α} :
+  (m.contains k ) = (m.mapOnValuesAttach (λ v => f v.val)).contains k
+  := by
+  rw [← mapOnValuesAttachIsMapOnValues]
+  cases hcontains : (m.contains k) <;> cases m <;> rename_i kvs
+  case true =>
+    induction kvs
+    case nil =>
+      simp [contains, find?, List.find?] at hcontains
+    case cons head tail ih =>
+      cases head
+      rename_i key value
+      cases heq_head_key : decide (key = k) <;> simp at heq_head_key
+      case _ =>
+        have beq_false : (key == k) = false := by
+          rw [beq_eq_false_iff_ne]
+          assumption
+        rw [mapOnValues_cons]
+        simp [contains, find?, List.find?, beq_false]
+        simp [contains, find?, List.find?] at ih
+        apply ih
+        simp [contains, find?, List.find?, beq_false] at hcontains
+        assumption
+      case _ =>
+        subst heq_head_key
+        simp [contains, find?, List.find?]
+  case false =>
+    induction kvs
+    case nil =>
+      simp [contains, find?, List.find?]
+    case cons head tail ih =>
+      cases head
+      rename_i key value
+      cases heq_head_key : decide (key = k) <;> simp at heq_head_key
+      case _ =>
+        have beq_false : (key == k) = false := by
+          rw [beq_eq_false_iff_ne]
+          assumption
+        rw [mapOnValues_cons]
+        simp [contains, find?, List.find?, beq_false]
+        simp [contains, find?, List.find?] at ih
+        apply ih
+        simp [contains, find?, List.find?, beq_false] at hcontains
+        assumption
+      case _ =>
+        subst heq_head_key
+        simp [contains, find?, List.find?] at hcontains
+
+/--
+  An adapter that makes the above lemma easier to apply in context
+-/
+theorem mapOnValuesAttach_preservesContains_adapter
+  {α : Type u} {β γ : Type v} [LT α] [DecidableLT α] [BEq α ] [LawfulBEq α] [DecidableEq α]
+  {m : Map α β}
+  {f : {x // ∃ k, (k,x) ∈ m.kvs} → γ}
+  {k : α}
+  {h₁ : ∃ (f' : β → γ), f = (λ prod => f' prod.val)} :
+  (m.contains k ) = (m.mapOnValuesAttach f).contains k
+  := by
+  replace ⟨f', h₁⟩ := h₁
+  rw [h₁]
+  apply mapOnValuesAttach_preservesContains
+
+theorem mapOnValuesAttach_preservesKeys
+  {α : Type u} {β γ : Type v} [LT α] [DecidableLT α] [BEq α ] [LawfulBEq α] [DecidableEq α]
+  {m : Map α β}
+  {f : β → γ}
+  {k : α}
+  {h : m.contains k = true} :
+  (m.mapOnValuesAttach (λ v => f v.val)).contains k = true
+  := by
+  rw [← mapOnValuesAttachIsMapOnValues]
+  cases m
+  rename_i kvs
+  induction kvs
+  case nil =>
+    simp [mapOnValues, List.map, contains, find?, kvs] at h
+  case cons head tail ih =>
+    simp [contains, find?, kvs, List.find?] at h
+    simp [contains, find?, kvs, List.find?]
+    cases heq_head : (head.fst == k)
+    case true =>
+      simp
+    case false =>
+      simp
+      cases htail : (mk tail).contains k
+      case true =>
+        have hrecur : (mapOnValues f (mk tail)).contains k = true := by
+          apply ih
+          assumption
+        simp [mapOnValues, contains, find?, kvs ] at hrecur
+        assumption
+      case false =>
+        exfalso
+        rw [heq_head] at h
+        simp at h
+        simp [contains, find?, kvs] at htail
+        cases h' : List.find? (fun x => x.fst == k) tail
+        case none =>
+          rw [h'] at h
+          simp at h
+        case some =>
+          rw [h'] at htail
+          simp at htail
+
+theorem mapOnValuesAttach_preservesKeys_adapter
+  {α : Type u} {β γ : Type v} [LT α] [DecidableLT α] [BEq α ] [LawfulBEq α] [DecidableEq α]
+  {m : Map α β}
+  {f : { x // ∃ k, (k,x) ∈ m.kvs} → γ}
+  {k : α}
+  {h₁ : m.contains k = true}
+  {h₂ : ∃ (f' : β → γ), f = λ val => f' val.val } :
+  (m.mapOnValuesAttach f).contains k = true
+  := by
+  replace ⟨f', h₂⟩ := h₂
+  rw [h₂]
+  apply mapOnValuesAttach_preservesKeys
+  assumption
+
+theorem mapOnValues_maps
+  {α : Type u} {β γ : Type v} [LT α] [DecidableLT α] [BEq α] [LawfulBEq α] [DecidableEq α]
+  {m : Map α β}
+  {f : β → γ}
+  {k : α}
+  {v : β}
+  {h₁ : m.find? k = some v} :
+  (m.mapOnValuesAttach (λ prod => f prod.val)).find? k = .some (f v)
+  := by
+  rw [← mapOnValuesAttachIsMapOnValues]
+  cases m
+  rename_i kvs
+  induction kvs
+  case nil =>
+    simp [find?, List.find?] at h₁
+  case cons head tail ih =>
+    cases head
+    rename_i key value
+    cases heq : decide (key = k) <;> simp at heq
+    case _ =>
+      have beq_false : (key == k) = false := by
+        apply beq_false_of_ne
+        assumption
+      simp [find?, List.find?, beq_false] at h₁
+      rw [mapOnValues_cons]
+      simp [find?, List.find?, beq_false]
+      apply ih
+      split at h₁ <;> simp at h₁
+      rename_i heq
+      subst h₁
+      simp [find?, heq]
+    case _ =>
+      subst heq
+      rw [mapOnValues_cons]
+      simp [find?, List.find?] at h₁
+      simp [find?, List.find?]
+      subst h₁
+      rfl
+
+theorem mapOnValues_maps_adapter
+  {α : Type u} {β γ : Type v}
+  [LT α] [DecidableLT α] [BEq α] [LawfulBEq α] [DecidableEq α]
+  {m : Map α β}
+  {f : {x // ∃ k, (k,x) ∈ m.kvs} → γ}
+  {f': β → γ}
+  {k : α}
+  {v : β}
+  {h₁ : m.find? k = some v}
+  {h₂ : f = λ prod => f' prod.val} :
+  (m.mapOnValuesAttach f).find? k = .some (f' v)
+  := by
+  rw [h₂]
+  apply mapOnValues_maps
+  assumption
+
+theorem mapOnValuesAttachFunEq
+  {α : Type u} {β γ : Type v}
+  [LT α] [DecidableLT α] [BEq α]
+  {m : Map α β}
+  {k : α}
+  {f₁ : {x // ∃ k, (k,x) ∈ m.kvs} → γ}
+  {f₂ : {x // ∃ k, (k,x) ∈ m.kvs} → γ}
+  {h₁ : f₁ = f₂} :
+  (m.mapOnValuesAttach f₁).find? k = (m.mapOnValuesAttach f₂).find? k
+  := by
+  rw [h₁]
+
 /--
   Converse of `in_kvs_in_mapOnValues`; requires the extra preconditions that `m`
   is `WellFormed` and `f` is injective
@@ -934,4 +1153,83 @@ theorem mapMOnValues_error_implies_exists_error [LT α] [DecidableLT α] {f : β
   have h_values := in_list_in_values hkv
   exists v
 
+/-! ### `sizeOf` -/
+
+theorem find_means_mem
+  {α : Type u} {β : Type v}
+  [LT α] [DecidableLT α] [BEq α] [LawfulBEq α] [DecidableEq α]
+  {m : Map α β}
+  {k : α}
+  {v : β}
+  (h : m.find? k = some v) :
+  (k,v) ∈ m.kvs
+  := by
+  cases m
+  rename_i kvs
+  induction kvs
+  case nil =>
+    simp [find?, List.find?] at h
+  case cons head tail ih =>
+    simp [kvs]
+    cases head
+    rename_i key value
+    cases heq : decide (key = k) <;> simp at heq
+    case _ =>
+      have beq : (key == k) = false := by
+        rw [beq_eq_false_iff_ne]
+        assumption
+      apply Or.inr
+      simp [kvs] at ih
+      apply ih
+      simp [find?, List.find?, beq] at h
+      simp [find?, List.find?]
+      apply h
+    case _ =>
+      apply Or.inl
+      subst heq
+      simp [find?, List.find?] at h
+      subst h
+      rfl
+
+-- If you can find a value in a map, that value is smaller than the map
+theorem find_means_smaller
+  {α β : Type}
+  [LT α] [DecidableLT α] [DecidableEq α] [SizeOf α] [SizeOf β]
+  {m : Map α β}
+  {k : α}
+  {v : β}
+  {h : m.find? k = some v} :
+  sizeOf v < sizeOf m := by
+  have h₂ : (k,v) ∈ m.kvs := by
+    apply find?_mem_toList
+    assumption
+  have s₁ : sizeOf v < sizeOf (k,v) := by
+    simp
+    omega
+  have s₂ : sizeOf m.kvs < sizeOf m := by apply sizeOf_lt_of_kvs
+  have s₃ : sizeOf (k,v) < sizeOf m.kvs := by
+    apply List.sizeOf_lt_of_mem
+    assumption
+  omega
+
+def equiv_refl [LT α] [DecidableLT α] [BEq α] : ∀ (m₁ m₂ : Map α β),
+  m₁ ≃ m₂ →
+  m₂ ≃ m₂ := by
+  simp [Equiv]
+
+def equiv_sym [LT α] [DecidableLT α] [BEq α] : ∀ (m : Map α β),
+  m ≃ m := by
+  simp [Equiv]
+
+def equiv_trans [LT α] [DecidableLT α] [BEq α] : ∀ (m₁ m₂ m₃ : Map α β ),
+  m₁ ≃ m₂ →
+  m₂ ≃ m₃ →
+  m₁ ≃ m₃ := by
+  simp [Equiv]
+  intros m₁ m₂ m₃ h₁ h₂
+  intros k
+  simp [h₁, h₂]
+
+
+
 end Cedar.Data.Map