Reorgnaize TPE helper lemmas

Author: john-h-kastner-aws

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,53 @@ 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₂']
+
+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]
+
+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,32 @@ public theorem mapM_congr [Monad m] [LawfulMonad m] {f g : α → m β} : ∀ {l
   rw [← mapM'_eq_mapM, ← mapM'_eq_mapM]
   exact mapM'_congr
 
+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
+  induction l
+  case nil =>
+    simp only [not_mem_nil, false_implies, implies_true, mapM'_nil, forall_const]
+    rfl
+  case cons head tail hᵢ =>
+    intro h
+    let ⟨h₁, h₂⟩ := forall_mem_cons.1 h ; clear h
+    simp only [mapM'_cons, bind_pure_comp]
+    cases h₃ : (f head).toOption <;> rw [h₃] at h₁
+    · simp [do_to_option_none h₁.symm, do_to_option_none h₃]
+    · simp only [do_to_option_some h₃, do_to_option_some h₁.symm]
+      rw [to_option_distr_fmap]
+      rw [to_option_distr_fmap]
+      rw [hᵢ h₂]
+
+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
+  rw [← mapM'_eq_mapM, ← mapM'_eq_mapM]
+  exact mapM'_to_option_congr
+
 /-! ### foldl -/
 
 public theorem foldl_pmap_subtype
@@ -2106,4 +2142,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/Soundness/Basic.lean

@@ -36,8 +36,7 @@ open Cedar.Validation
 open Cedar.TPE
 open Cedar.Thm
 
-@[simp]
-theorem as_value_some {r : Residual} {v : Value} :
+theorem asValue_some {r : Residual} {v : Value} :
   r.asValue = .some v ↔ (∃ ty, r = .val v ty)
 := by
   simp only [Residual.asValue]
@@ -47,108 +46,19 @@ theorem as_value_some {r : Residual} {v : Value} :
     simp only [reduceCtorEq, false_iff]
     exact not_exists.mpr (h v)
 
-theorem as_value_evaluates_to {r : Residual} {v : Value} :
-  r.asValue = .some v → r.evaluate req es = Except.ok v
+theorem asValue_evaluate_val {r : Residual} {v : Value} :
+  r.asValue = .some v → ∀ req es, r.evaluate req es = Except.ok v
 := by
-  simp only [as_value_some, forall_exists_index]
+  simp only [asValue_some, forall_exists_index]
   intro _ hv
   simp [hv, Residual.evaluate]
 
-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_evaluate_err {r : Spec.Residual} :
+  r.isError → ∀ req es, ∃ e, r.evaluate req es = .error e
 := 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]
-
-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)
-:= 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]
-
-theorem to_option_eq_map {α β ε} {res₁ res₂: Except ε α} (f : α → β) :
-  Except.toOption res₁ = Except.toOption res₂ →
-  Except.toOption (f <$> res₁) = Except.toOption (f <$> res₂)
-:= 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]
+  intro h
+  simp only [Residual.isError] at h
+  split at h <;> cases h
+  simp [Spec.Residual.evaluate]
 
 end Cedar.Thm

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

@@ -55,17 +55,11 @@ theorem partial_evaluate_is_sound_binary_app
   simp [TPE.evaluate, TPE.apply₂]
   split
   case _ heq₁ heq₂ =>
-    -- TODO: rewrite `Residual.asValue` using standard lib so that we can use theorems to unwrap it
-    simp [Residual.asValue] at heq₁
-    simp [Residual.asValue] at heq₂
-    split at heq₁ <;> cases heq₁
-    split at heq₂ <;> cases heq₂
-    rename_i heq₁ _ _ heq₂
-    simp [heq₁, Residual.evaluate] at hᵢ₁
-    simp [heq₂, Residual.evaluate] at hᵢ₂
+    rw [as_value_evaluates_to heq₁] at hᵢ₁
+    rw [as_value_evaluates_to heq₂] at hᵢ₂
     replace hᵢ₁ := to_option_right_ok' hᵢ₁
-    replace hᵢ₅ := to_option_right_ok' hᵢ₂
-    simp [Residual.evaluate, hᵢ₁, hᵢ₅, Spec.apply₂]
+    replace hᵢ₂ := to_option_right_ok' hᵢ₂
+    simp [Residual.evaluate, hᵢ₁, hᵢ₂, Spec.apply₂]
     -- TODO: rewrite one of the two binary app evaluation function so that we don't need this amount of case splits.
     split <;> simp [Residual.evaluate]
     any_goals
@@ -85,7 +79,7 @@ theorem partial_evaluate_is_sound_binary_app
       case _ =>
         simp only [Except.toOption, Residual.evaluate]
     case _ uid₁ uid₂ =>
-      simp [apply₂.self, heq₁, heq₂, someOrSelf]
+      simp [apply₂.self, someOrSelf]
       split
       case _ heq₃ =>
         simp only [Option.bind_eq_some_iff] at heq₃
@@ -117,9 +111,11 @@ theorem partial_evaluate_is_sound_binary_app
             simp only [beq_eq_false_iff_ne, ne_eq, heq₄, not_false_eq_true]
           simp only [this, Bool.false_or]
       case _ heq₃ =>
+        rw [as_value_some] at heq₁ heq₂
+        rw [heq₁.choose_spec, heq₂.choose_spec]
         simp only [Residual.evaluate, Spec.apply₂, Except.bind_ok]
     case _ =>
-      simp [apply₂.self, heq₁, heq₂, someOrSelf]
+      simp [apply₂.self, someOrSelf]
       split
       case _ uid vs _ _ _ _ _ heq₃ =>
         simp only [Option.bind_eq_some_iff] at heq₃
@@ -128,7 +124,7 @@ theorem partial_evaluate_is_sound_binary_app
         subst heq₃₂
         simp [Spec.inₛ]
         cases howt <;>
-        (rename_i h₅; have h₆ := residual_well_typed_is_sound h₂ hwt hᵢ₅; rw [h₅] at h₆; cases h₆)
+        (rename_i h₅; have h₆ := residual_well_typed_is_sound h₂ hwt hᵢ₂; rw [h₅] at h₆; cases h₆)
         rename_i h₆
         simp [Data.Set.mapOrErr]
         generalize h₇ : List.mapM Value.asEntityUID vs.elts = res
@@ -186,6 +182,8 @@ theorem partial_evaluate_is_sound_binary_app
           subst heq₃₂
           simp only [Residual.evaluate]
       case _ =>
+        rw [as_value_some] at heq₁ heq₂
+        rw [heq₁.choose_spec, heq₂.choose_spec]
         simp only [Spec.inₛ, Residual.evaluate, Spec.apply₂, Except.bind_ok]
     case _ uid _ =>
       simp [someOrSelf, apply₂.self]
@@ -211,7 +209,9 @@ theorem partial_evaluate_is_sound_binary_app
         subst heq₅
         simp only [Spec.hasTag, Entities.tagsOrEmpty, h₄₁, Residual.evaluate]
       case _ =>
-        simp only [heq₁, heq₂, Residual.evaluate, Spec.apply₂, Except.bind_ok]
+        rw [as_value_some] at heq₁ heq₂
+        rw [heq₁.choose_spec, heq₂.choose_spec]
+        simp only [Residual.evaluate, Spec.apply₂, Except.bind_ok]
     case _ uid _ =>
       simp [TPE.getTag, someOrError]
       split