Cleanup TPE helper lemmas

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

@@ -87,13 +87,10 @@ public theorem to_option_some {v : α} {res: Except ε α} :
     simp only [Except.toOption, h]
 
 public theorem to_option_none {res: Except ε α} :
-  res.toOption = .none → (∃ err, res = .error err)
+  res.toOption = .none ↔ (∃ err, res = .error err)
 := by
-  intro h
-  simp [Except.toOption] at h
-  split at h <;> simp at h
-  rename_i err
-  exists err
+  simp only [Except.toOption]
+  split <;> simp
 
 public theorem to_option_left_ok {α ε₁ ε₂} {v : α} {res₁ : Except ε₁ α} {res₂ : Except ε₂ α} :
   res₁.toOption = res₂.toOption → res₁ = .ok v → res₂ = .ok v
@@ -150,3 +147,55 @@ public theorem do_error_to_option {res : Except ε α} {e : ε} :
   (do let (_ : α) ← res ; (.error e : Except ε α)).toOption = .none
 := by
   cases res <;> simp [Except.toOption]
+
+public theorem do_to_option_none {ε α β} {res : Except ε α} {f : α → Except ε β} :
+  res.toOption = none → (do let x ← res; f x).toOption = none
+:= by
+  intro h
+  replace ⟨_, h⟩ := to_option_none.mp h
+  simp [h, Except.toOption]
+
+public theorem do_to_option_some {ε α β} {res : Except ε α} {v : α} {f : α → Except ε β} :
+  res.toOption = .some v → (do let x ← res; f x) = f v
+:= by
+  intro h
+  simp [to_option_some.mp h]
+
+public theorem to_option_eq_do₁ {α β ε} {res₁ res₂: Except ε α} (f : α → Except ε β) :
+  res₁.toOption = res₂.toOption →
+  (do let x ← res₁; f x).toOption = (do let x ← res₂; f x).toOption
+:= by
+  cases h₁ : res₁.toOption
+  · intro h₂
+    simp [do_to_option_none h₁, do_to_option_none h₂.symm]
+  · intro h₂
+    simp [do_to_option_some h₁, do_to_option_some h₂.symm]
+
+public theorem to_option_eq_do₂ {α ε} {res₁ res₂ res₃ res₄: Except ε α} (f : α → α → Except ε α) :
+  res₁.toOption = res₃.toOption →
+  res₂.toOption = res₄.toOption →
+  (do let x ← res₁; let y ← res₂; f x y).toOption = (do let x ← res₃; let y ← res₄; f x y).toOption
+:= by
+  intro h₁ h₂
+  have h₁' := to_option_eq_do₁ (λ x => (do let y ← res₂ ; f x y)) h₁
+  simp only [h₁']
+  cases h₃ : res₃.toOption
+  · simp [do_to_option_none h₃]
+  · rename_i x
+    simp [do_to_option_some h₃]
+    have h₂' := to_option_eq_do₁ (f x) h₂
+    simp [h₂']
+
+@[simp]
+public theorem to_option_distr_map {ε α β} {x : Except ε α} {f : α → β} :
+  (x.map f).toOption = x.toOption.map f
+:= by
+  cases x <;>
+    simp [Except.toOption, Except.map]
+
+@[simp]
+public theorem to_option_distr_fmap {ε α β} {x : Except ε α} {f : α → β} :
+  (f <$> x).toOption = f <$> x.toOption
+:= by
+  cases x <;>
+    simp [Except.toOption, Except.map, Functor.map]

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

@@ -956,6 +956,16 @@ public theorem element_error_implies_mapM_error {x : α} {xs : List α} {f : α
   rw [← List.mapM'_eq_mapM]
   exact element_error_implies_mapM'_error
 
+public theorem element_to_option_none_implies_mapM_none {α β ε} {ls : List α} {x : α}
+  {f : α → Except ε β}
+  (h₁ : x ∈ ls)
+  (h₂ : (f x).toOption = none) :
+  (List.mapM f ls).toOption = none
+:= by
+  rw [to_option_none] at h₂
+  have ⟨_, he⟩ := List.element_error_implies_mapM_error h₁ h₂.choose_spec
+  simp [he, Except.toOption]
+
 public theorem mapM'_ok_eq_filterMap {α β} {f : α → Except ε β} {xs : List α} {ys : List β} :
   xs.mapM' f = .ok ys →
   xs.filterMap (λ x => match f x with | .ok y => some y | .error _ => none) = ys
@@ -1223,6 +1233,31 @@ public theorem mapM_congr [Monad m] [LawfulMonad m] {f g : α → m β} : ∀ {l
   rw [← mapM'_eq_mapM, ← mapM'_eq_mapM]
   exact mapM'_congr
 
+public theorem to_option_distr_mapM' {α β ε} {l : List α} {f: α → Except ε β} :
+  (List.mapM' f l).toOption = (List.mapM' (Except.toOption ∘ f) l)
+:= by
+  induction l
+  case nil => rfl
+  case cons head tail hᵢ =>
+    simp only [mapM'_cons, bind_pure_comp, Function.comp_apply, Option.pure_def, Option.bind_eq_bind]
+    cases h₃ : (f head).toOption
+    · simp [do_to_option_none h₃]
+    · simp only [do_to_option_some h₃]
+      cases h₄ : (mapM' (Except.toOption ∘ f) tail) <;> simp [hᵢ, h₄]
+
+public theorem to_option_distr_mapM {α β ε} {l : List α} {f: α → Except ε β} :
+  (List.mapM f l).toOption = (List.mapM (Except.toOption ∘ f) l)
+:= by
+  rw [← mapM'_eq_mapM, ← mapM'_eq_mapM]
+  exact to_option_distr_mapM'
+
+public theorem mapM_to_option_congr {α β ε₁ ε₂} {l : List α} {f: α → Except ε₁ β} {g: α → Except ε₂ β} :
+  (∀ x ∈ l, (f x).toOption = (g x).toOption) →
+  (List.mapM f l).toOption = (List.mapM g l).toOption
+:= by
+  simp only [to_option_distr_mapM]
+  exact mapM_congr
+
 /-! ### foldl -/
 
 public theorem foldl_pmap_subtype
@@ -2104,4 +2139,32 @@ public theorem find?_filter_sorted {α : Type u} {β : Type v} [BEq α] [LawfulB
         simp only [ih, List.find?_cons_eq_some, Bool.not_eq_eq_eq_not, Bool.not_true, beq_eq_false_iff_ne, and_true]
         exact .inr h_k
 
+public theorem anyM_some_implies_any {α} {xs : List α} {b : Bool}  (f : α → Option Bool) (g : α → Bool) :
+  (∀ x b, f x = some b → g x = b) → List.anyM f xs = some b → xs.any g = b
+:= by
+  intro h₁ h₂
+  induction xs generalizing b
+  case nil =>
+    simp only [anyM_nil, Option.pure_def, Option.some.injEq, Bool.false_eq] at h₂
+    simp only [any_nil, h₂]
+  case cons head tail hᵢ =>
+    simp only [any_cons]
+    simp only [anyM_cons, Option.pure_def, Option.bind_eq_bind] at h₂
+    generalize h₃ : f head = res
+    cases res <;> simp [h₃] at h₂
+    case some =>
+      split at h₂
+      case _ h₄ =>
+        simp only [Option.some.injEq, Bool.true_eq] at h₂
+        subst h₂ h₄
+        specialize h₁ head true h₃
+        simp only [h₁, Bool.true_or]
+      case _ h₄ =>
+        specialize hᵢ h₂
+        simp only [hᵢ, Bool.or_eq_right_iff_imp]
+        simp only [Bool.not_eq_true] at h₄
+        subst h₄
+        specialize h₁ head false h₃
+        simp only [h₁, Bool.false_eq_true, false_implies]
+
 end List

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

@@ -211,9 +211,8 @@ theorem partial_authorize_error_policies_is_sound
   have h₄ : (Spec.isAuthorized req es policies).erroringPolicies =  errorPolicies policies req es :=
     by grind [Spec.isAuthorized]
   simp only [errorPolicies, errored, hasError] at h₄
-  simp only [h₄, isAuthorized.errorPolicies, Set.subset_def, Set.mem_make, List.mem_filterMap,
-    ResidualPolicy.erroredWithEffect, ResidualPolicy.hasError, Residual.isError, Bool.and_eq_true,
-    beq_iff_eq, Option.ite_none_right_eq_some, Option.some.injEq, forall_exists_index, and_imp]
+  simp only [isAuthorized.errorPolicies, h₄, Set.subset_def, Set.mem_make, List.mem_filterMap,
+    ResidualPolicy.erroredWithEffect, Bool.and_eq_true,  Option.ite_none_right_eq_some, forall_exists_index, and_imp]
   intro pid rp hrp hef herr hpid
 
   have ⟨p, hp₁, hp₂⟩ := List.forall₂_implies_all_right h₁ rp hrp
@@ -225,9 +224,10 @@ theorem partial_authorize_error_policies_is_sound
   · exact hp₁
   · replace ⟨_, ha⟩ : ∃ e, Spec.evaluate p.toExpr req es = .error e := by
       rename_i r
-      replace ⟨_, herr⟩ : ∃ ty, r = .error ty := by grind
+      replace herr := isError_evaluate_err herr req es
+      simp only [← hp₂] at herr
       have ha := partial_evaluate_policy_is_sound hp₃ h₂
-      simp only [herr, Residual.evaluate] at ha
+      rw [herr.choose_spec] at ha
       exact to_option_right_err ha
     simp [ha]
   · simpa [←hp₂] using hpid

cedar-lean/Cedar/Thm/TPE/Soundness/And.lean

@@ -64,12 +64,11 @@ theorem partial_evaluate_is_sound_and
       rw [hᵢ₄] at h₆
       rcases instance_of_anyBool_is_bool h₆ with ⟨_, h₆⟩
       replace hᵢ₆ := to_option_left_ok hᵢ₆ heq₁
-      simp only [h₆, Except.map_ok, hᵢ₆]
+      simp [h₆, hᵢ₆, Except.toOption]
     case _ heq₁ =>
-      simp only [Except.map_error]
       rw [heq₁] at hᵢ₆
       rcases to_option_left_err hᵢ₆ with ⟨_, hᵢ₆⟩
-      simp only [hᵢ₆, Except.toOption]
+      simp [hᵢ₆, Except.toOption]
   case _ heq =>
     simp [heq, Residual.evaluate] at hᵢ₅
     have h₅ := to_option_right_ok' hᵢ₅

cedar-lean/Cedar/Thm/TPE/Soundness/Basic.lean

@@ -36,110 +36,38 @@ open Cedar.Validation
 open Cedar.TPE
 open Cedar.Thm
 
-theorem as_value_some {r : Residual} {v : Value} :
-  r.asValue = .some v → (∃ ty, r = .val v ty)
+theorem asValue_some {r : Residual} {v : Value} :
+  r.asValue = .some v ↔ (∃ ty, r = .val v ty)
 := by
-  intro h
-  simp only [Residual.asValue] at h
-  split at h <;> simp at h
-  subst h
-  simp only [Residual.val.injEq, true_and, exists_eq']
+  simp only [Residual.asValue]
+  split
+  · simp
+  · rename_i h
+    simp only [reduceCtorEq, false_iff]
+    exact not_exists.mpr (h v)
 
-theorem anyM_some_implies_any {α} {xs : List α} {b : Bool}  (f : α → Option Bool) (g : α → Bool) :
-(∀ x b, f x = some b → g x = b) → List.anyM f xs = some b → xs.any g = b
+theorem isError_true {r : Residual} :
+  r.isError ↔ (∃ ty, r = .error ty)
 := by
-  intro h₁ h₂
-  induction xs generalizing b
-  case nil =>
-    simp only [List.anyM, Option.pure_def, Option.some.injEq, Bool.false_eq] at h₂
-    simp only [List.any_nil, h₂]
-  case cons head tail hᵢ =>
-    simp only [List.any_cons]
-    simp only [List.anyM, Option.pure_def, Option.bind_eq_bind] at h₂
-    generalize h₃ : f head = res
-    cases res <;> simp [h₃] at h₂
-    case some =>
-      split at h₂
-      case _ =>
-        simp only [Option.some.injEq, Bool.true_eq] at h₂
-        subst h₂
-        specialize h₁ head true h₃
-        simp only [h₁, Bool.true_or]
-      case _ =>
-        specialize hᵢ h₂
-        simp only [hᵢ, Bool.or_eq_right_iff_imp]
-        specialize h₁ head false h₃
-        simp only [h₁, Bool.false_eq_true, false_implies]
+  simp only [Residual.isError]
+  split
+  · simp
+  · rename_i h
+    simp only [reduceCtorEq, false_iff]
+    exact not_exists.mpr h
 
-theorem to_option_eq_do₁ {α β ε} {res₁ res₂: Except ε α} (f : α → Except ε β) :
-  Except.toOption res₁ = Except.toOption res₂ →
-  Except.toOption (do let x ← res₁; f x) = Except.toOption (do let x ← res₂; f x)
+theorem asValue_evaluate_val {r : Residual} {v : Value} :
+  r.asValue = .some v → ∀ req es, r.evaluate req es = Except.ok v
 := by
-  intro h₁
-  simp [Except.toOption] at *
-  split at h₁ <;>
-  split at h₁ <;>
-  simp at h₁
-  case _ => subst h₁; simp only [Except.bind_ok]
-  case _ => simp only [Except.bind_err]
+  simp only [asValue_some, forall_exists_index]
+  intro _ hv
+  simp [hv, Residual.evaluate]
 
-theorem to_option_eq_map {α β ε} {res₁ res₂: Except ε α} (f : α → β) :
-  Except.toOption res₁ = Except.toOption res₂ →
-  Except.toOption (f <$> res₁) = Except.toOption (f <$> res₂)
+theorem isError_evaluate_err {r : Spec.Residual} :
+  r.isError → ∀ req es, ∃ e, r.evaluate req es = .error e
 := by
-  intro h₁
-  simp [Except.toOption] at *
-  split at h₁ <;>
-  split at h₁ <;>
-  simp at h₁
-  case _ => subst h₁; simp only
-  case _ => simp only [Except.map_error]
-
-theorem to_option_eq_do₂ {α ε} {res₁ res₂ res₃ res₄: Except ε α} (f : α → α → Except ε α) :
-  Except.toOption res₁ = Except.toOption res₃ →
-  Except.toOption res₂ = Except.toOption res₄ →
-  Except.toOption (do let x ← res₁; let y ← res₂; f x y) = Except.toOption (do let x ← res₃; let y ← res₄; f x y)
-:= by
-  intro h₁ h₂
-  simp [Except.toOption] at *
-  split at h₁ <;>
-  split at h₁ <;>
-  split at h₂ <;>
-  split at h₂ <;>
-  simp at h₁ <;>
-  simp at h₂
-  case _ => subst h₁; subst h₂; simp only [Except.bind_ok]
-  case _ => simp only [Except.bind_err, Except.bind_ok]
-  case _ => simp only [Except.bind_ok, Except.bind_err]
-  case _ => simp only [Except.bind_err]
-
-theorem to_option_eq_mapM {α β ε} {ls : List α} (f g: α → Except ε β) :
-(∀ x,
-  x ∈ ls →
-    Except.toOption (f x) = Except.toOption (g x)) →
-  Except.toOption (List.mapM f ls) =
-  Except.toOption (List.mapM g ls)
-:= by
-  induction ls
-  case nil => simp only [List.not_mem_nil, false_implies, implies_true, List.mapM_nil]
-  case cons head tail hᵢ =>
-    simp only [List.mem_cons, forall_eq_or_imp, List.mapM_cons, bind_pure_comp, and_imp]
-    intro h
-    simp only [Except.toOption] at h
-    split at h <;> split at h <;> simp at h
-    case _ heq₁ _ _ heq₂ =>
-      subst h
-      simp only [heq₁, Except.bind_ok, heq₂]
-      intro h
-      specialize hᵢ h
-      simp only [Except.toOption] at hᵢ
-      split at hᵢ <;> split at hᵢ <;> simp at hᵢ
-      case _ heq₃ _ _ heq₄ =>
-        subst hᵢ
-        simp only [heq₃, Except.map_ok, heq₄]
-      case _ heq₃ _ _ heq₄ =>
-        simp only [Except.toOption, heq₃, Except.map_error, heq₄]
-    case _ heq₁ _ _ heq₂ =>
-      simp only [Except.toOption, heq₁, Except.bind_err, heq₂, implies_true]
+  simp only [isError_true, forall_exists_index]
+  intro _ he
+  simp [he, Spec.Residual.evaluate]
 
 end Cedar.Thm