Extend typechecker inversion lemma for type annotation

Signed-off-by: John Kastner <jkastner@amazon.com>

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

@@ -26,17 +26,20 @@ open Cedar.Data
 open Cedar.Spec
 open Cedar.Validation
 
-theorem type_of_and_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {ty : TypedExpr}
-  (h₁ : typeOf (Expr.and x₁ x₂) c env = Except.ok (ty, c')) :
-  ∃ bty₁ c₁,
-    (typeOf x₁ c env).typeOf = .ok (.bool bty₁, c₁) ∧
+theorem type_of_and_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {tx : TypedExpr}
+  (h₁ : typeOf (Expr.and x₁ x₂) c env = Except.ok (tx, c')) :
+  ∃ tx₁ bty₁ c₁,
+    typeOf x₁ c env = .ok (tx₁, c₁) ∧
+    tx₁.typeOf = .bool bty₁ ∧
     if bty₁ = BoolType.ff
-    then ty.typeOf = .bool BoolType.ff ∧ c' = ∅
-    else ∃ bty₂ c₂,
-      (typeOf x₂ (c ∪ c₁) env).typeOf = .ok (.bool bty₂, c₂) ∧
+    then tx = (.and tx₁ tx₁ (.bool BoolType.ff)) ∧ c' = ∅
+    else ∃ bty tx₂ bty₂ c₂,
+      tx = (.and tx₁ tx₂ (.bool bty)) ∧
+      typeOf x₂ (c ∪ c₁) env = .ok (tx₂, c₂) ∧
+      tx₂.typeOf = .bool bty₂ ∧
       if bty₂ = BoolType.ff
-      then ty.typeOf = .bool BoolType.ff ∧ c' = ∅
-      else ty.typeOf = .bool (lubBool bty₁ bty₂) ∧ c' = c₁ ∪ c₂
+      then bty = BoolType.ff ∧ c' = ∅
+      else bty = lubBool bty₁ bty₂ ∧ c' = c₁ ∪ c₂
 := by
   simp [typeOf] at h₁
   cases h₂ : typeOf x₁ c env <;> simp [h₂] at *
@@ -46,49 +49,55 @@ theorem type_of_and_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : En
   case ok.h_1 h₃ =>
     have ⟨ hl₁, hr₁ ⟩ := h₁
     subst hl₁ hr₁
-    exists BoolType.ff, res₁.snd
-    simp [ResultType.typeOf, Except.map, h₃]
+    exists res₁.fst, BoolType.ff, res₁.snd
   case ok.h_2 bty₁ h₃ h₄ =>
-    exists bty₁, res₁.snd
+    exists res₁.fst, bty₁, res₁.snd
     simp [h₄, ResultType.typeOf, Except.map]
     split ; contradiction
     cases h₄ : typeOf x₂ (c ∪ res₁.snd) env <;> simp [h₄] at *
     rename_i res₂
     split at h₁ <;> simp at h₁ <;>
     have ⟨hty, hc⟩ := h₁ <;> subst hty hc
     case isFalse.ok.h_1 hty₂ =>
-      exists BoolType.ff, res₂.snd
+      exists .ff, res₂.fst
+      apply And.intro (by simp)
+      exists .ff, res₂.snd
     case isFalse.ok.h_2 hty₂ =>
-      exists BoolType.tt, res₂.snd ; simp [←hty₂]
-      cases bty₁ <;> simp at h₃ <;> simp [lubBool, TypedExpr.typeOf]
+      exists bty₁, res₂.fst
+      apply And.intro (by simp)
+      exists BoolType.tt, res₂.snd
+      cases bty₁
+      case ff => contradiction
+      all_goals
+        simp [hty₂, lubBool]
     case isFalse.ok.h_3 bty₂ h₄ h₅ hty₂ =>
+      exists .anyBool, res₂.fst
+      apply And.intro (by simp)
       exists BoolType.anyBool, res₂.snd
-      cases bty₂ <;> simp at *
-      simp [hty₂, lubBool]
-      split <;> rename_i h₆
-      · simp [h₆, TypedExpr.typeOf]
-      · rfl
+      have _ : bty₂ = .anyBool := by
+        cases bty₂ <;> simp at h₄ h₅ ⊢
+      subst bty₂
+      cases bty₁ <;> simp [hty₂, lubBool]
 
-theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities}
+theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr} {request : Request} {entities : Entities}
   (h₁ : CapabilitiesInvariant c₁ request entities)
   (h₂ : RequestAndEntitiesMatchEnvironment env request entities)
-  (h₃ : typeOf (Expr.and x₁ x₂) c₁ env = Except.ok (ty, c₂))
+  (h₃ : typeOf (Expr.and x₁ x₂) c₁ env = Except.ok (tx, c₂))
   (ih₁ : TypeOfIsSound x₁)
   (ih₂ : TypeOfIsSound x₂) :
   GuardedCapabilitiesInvariant (Expr.and x₁ x₂) c₂ request entities ∧
-  ∃ v, EvaluatesTo (Expr.and x₁ x₂) request entities v ∧ InstanceOfType v ty.typeOf
+  ∃ v, EvaluatesTo (Expr.and x₁ x₂) request entities v ∧ InstanceOfType v tx.typeOf
 := by
-  have ⟨bty₁, rc₁, h₄, h₅⟩ := type_of_and_inversion h₃
-  split_type_of h₄ ; rename_i h₄ hl₄ hr₄
+  have ⟨tx₁, bty₁, rc₁, h₄, h₅, h₆⟩ := type_of_and_inversion h₃
   specialize ih₁ h₁ h₂ h₄
   have ⟨ih₁₁, v₁, ih₁₂, ih₁₃⟩ := ih₁
-  rw [hl₄] at ih₁₃
+  rw [h₅] at ih₁₃
   have ⟨b₁, hb₁⟩ := instance_of_bool_is_bool ih₁₃
   subst hb₁
-  split at h₅
-  case isTrue h₆ =>
-    subst h₆
-    have ⟨hty, hc⟩ := h₅
+  split at h₆
+  case isTrue h₇ =>
+    subst h₇
+    have ⟨hty, hc⟩ := h₆
     rw [hty, hc]
     apply And.intro empty_guarded_capabilities_invariant
     have h₇ := instance_of_ff_is_false ih₁₃
@@ -98,13 +107,13 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env
     simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool] <;>
     try exact type_is_inhabited (CedarType.bool BoolType.ff)
     exact false_is_instance_of_ff
-  case isFalse h₆ =>
-    have ⟨bty₂, rc₂, hₜ, h₇⟩ := h₅
-    split at h₇ <;> have ⟨hty, hc⟩ := h₇ <;> rw [hty, hc]
-    case isTrue h₈ =>
-      subst h₈
+  case isFalse h₇ =>
+    replace ⟨bty, tx₂, bty₂, rc₂, htx, htx₂, hty₂, h₆⟩ := h₆
+    split at h₆ <;> have ⟨hbty, hc⟩ := h₆ <;> subst bty c₂ tx
+    case isTrue hbty₂ =>
+      subst bty₂
       apply And.intro empty_guarded_capabilities_invariant
-      exists false ; simp [false_is_instance_of_ff]
+      exists false ; simp [TypedExpr.typeOf, false_is_instance_of_ff]
       cases b₁
       case false =>
         rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;>
@@ -115,22 +124,20 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env
         simp [GuardedCapabilitiesInvariant] at ih₁₁
         specialize ih₁₁ ih₁₂
         have h₇ := capability_union_invariant h₁ ih₁₁
-        split_type_of hₜ ; rename_i hₜ hlₜ hrₜ
-        subst hr₄
-        specialize ih₂ h₇ h₂ hₜ
+        specialize ih₂ h₇ h₂ htx₂
         have ⟨_, v₂, ih₂₂, ih₂₃⟩ := ih₂
         simp [EvaluatesTo] at ih₂₂
         rcases ih₂₂ with ih₂₂ | ih₂₂ | ih₂₂ | ih₂₂ <;>
         simp [Result.as, ih₂₂, Coe.coe, Value.asBool, Lean.Internal.coeM, pure, Except.pure]
-        rw [hlₜ] at ih₂₃
+        rw [hty₂] at ih₂₃
         have h₈ := instance_of_ff_is_false ih₂₃
         subst h₈
         simp [CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe, Coe.coe]
-    case isFalse h₈ =>
+    case isFalse hbty₂ =>
       cases b₁
       case false =>
         rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;>
-        simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool, GuardedCapabilitiesInvariant] <;>
+        simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool, GuardedCapabilitiesInvariant, TypedExpr.typeOf] <;>
         try exact type_is_inhabited (CedarType.bool (lubBool bty₁ bty₂))
         apply instance_of_lubBool
         simp [ih₁₃]
@@ -140,26 +147,23 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env
         try exact type_is_inhabited (CedarType.bool (lubBool bty₁ bty₂))
         simp [GuardedCapabilitiesInvariant] at ih₁₁
         specialize ih₁₁ ih₁₂
-        split_type_of hₜ ; rename_i hₜ hlₜ hrₜ
-        subst hr₄
         have h₇ := capability_union_invariant h₁ ih₁₁
-        specialize ih₂ h₇ h₂ hₜ
+        specialize ih₂ h₇ h₂ htx₂
         have ⟨ih₂₁, v₂, ih₂₂, ih₂₃⟩ := ih₂
         simp [EvaluatesTo] at ih₂₂
         rcases ih₂₂ with ih₂₂ | ih₂₂ | ih₂₂ | ih₂₂ <;>
         simp [EvaluatesTo, evaluate, Result.as, ih₂₂, Coe.coe, Value.asBool, Lean.Internal.coeM, pure, Except.pure] <;>
         try exact type_is_inhabited (CedarType.bool (lubBool bty₁ bty₂))
-        rw [hlₜ] at ih₂₃
+        rw [hty₂] at ih₂₃
         have ⟨b₂, hb₂⟩ := instance_of_bool_is_bool ih₂₃
         subst hb₂
-        cases b₂ <;> simp [CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe, Coe.coe]
+        cases b₂ <;> simp [TypedExpr.typeOf, CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe, Coe.coe]
         case false =>
           apply instance_of_lubBool ; simp [ih₂₃]
         case true =>
           apply And.intro
           · simp [GuardedCapabilitiesInvariant] at ih₂₁
             specialize ih₂₁ ih₂₂
-            rw [hrₜ] at ih₂₁
             exact capability_union_invariant ih₁₁ ih₂₁
           · apply instance_of_lubBool ; simp [ih₁₃]
 

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

@@ -35,6 +35,28 @@ open Cedar.Data
 open Cedar.Spec
 open Cedar.Validation
 
+theorem type_of_binaryApp_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {tx : TypedExpr}
+  (htx : typeOf (Expr.binaryApp op₂ x₁ x₂) c env = Except.ok (tx, c')) :
+  ∃ tx₁ c₁ tx₂ c₂,
+    typeOf x₁ c env = Except.ok (tx₁, c₁) ∧
+    typeOf x₂ c env = Except.ok (tx₂, c₂) ∧
+    ∃ ty, tx = .binaryApp op₂ tx₁ tx₂ ty
+:= by
+  simp only [typeOf] at htx
+  cases htx₁ : typeOf x₁ c env <;> simp only [htx₁, Except.bind_err, reduceCtorEq] at htx
+  cases htx₂ : typeOf x₂ c env <;> simp only [htx₂, Except.bind_err, Except.bind_ok, reduceCtorEq] at htx
+  rename_i r₁ r₂
+  simp [typeOfBinaryApp, typeOfEq, ifLubThenBool, typeOfGetTag, typeOfHasTag, ok, err] at htx
+  (split at htx <;> try split at htx <;> try split at htx <;> try split at htx) <;> try simp at htx
+  all_goals
+    have ⟨ htx, _ ⟩ := htx
+    rw [←htx]
+    exists r₁.fst, r₁.snd, r₂.fst, r₂.snd
+    and_intros
+    · rfl
+    · rfl
+    · simp only [TypedExpr.binaryApp.injEq, true_and, exists_eq']
+
 theorem type_of_binaryApp_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities}
   (h₁ : CapabilitiesInvariant c₁ request entities)
   (h₂ : RequestAndEntitiesMatchEnvironment env request entities)

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

@@ -26,13 +26,16 @@ open Cedar.Data
 open Cedar.Spec
 open Cedar.Validation
 
-theorem type_of_getTag_inversion {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr}
-  (h₁ : typeOf (Expr.binaryApp .getTag x₁ x₂) c₁ env = .ok (ty, c₂)) :
+theorem type_of_getTag_inversion {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr}
+  (h₁ : typeOf (Expr.binaryApp .getTag x₁ x₂) c₁ env = .ok (tx, c₂)) :
   c₂ = [] ∧
-  ∃ ety c₁' c₂',
-    (typeOf x₁ c₁ env).typeOf = .ok (.entity ety, c₁') ∧
-    (typeOf x₂ c₁ env).typeOf = .ok (.string, c₂') ∧
-    env.ets.tags? ety = some (some ty.typeOf) ∧
+  ∃ ety ty tx₁ tx₂ c₁' c₂',
+    typeOf x₁ c₁ env = .ok (tx₁, c₁') ∧
+    tx₁.typeOf = .entity ety ∧
+    typeOf x₂ c₁ env = .ok (tx₂, c₂') ∧
+    tx₂.typeOf = .string ∧
+    env.ets.tags? ety = some (some ty) ∧
+    tx = .binaryApp .getTag tx₁ tx₂ ty ∧
     (x₁, .tag x₂) ∈ c₁
 := by
   simp only [typeOf] at h₁
@@ -41,37 +44,36 @@ theorem type_of_getTag_inversion {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {
   rename_i tyc₁ tyc₂
   cases tyc₁
   cases tyc₂
-  rename_i ty₁ c₁' ty₂ c₂'
+  rename_i tx₁ c₁' tx₂ c₂'
   simp only at h₁
-  cases h₄ : ty₁.typeOf <;> simp [typeOfBinaryApp, err, reduceCtorEq, h₄] at h₁
-  cases h₅ : ty₂.typeOf <;> simp [typeOfBinaryApp, err, reduceCtorEq, h₅] at h₁
+  cases h₄ : tx₁.typeOf <;> simp [typeOfBinaryApp, err, reduceCtorEq, h₄] at h₁
+  cases h₅ : tx₂.typeOf <;> simp [typeOfBinaryApp, err, reduceCtorEq, h₅] at h₁
   rename_i ety
   simp only [typeOfGetTag, List.empty_eq] at h₁
   split at h₁ <;> simp only [ok, err, Except.bind_err, reduceCtorEq] at h₁
   split at h₁ <;> simp only [Except.bind_ok, Except.bind_err, Except.ok.injEq, Prod.mk.injEq, List.nil_eq, reduceCtorEq] at h₁
+  rename_i ty _ _
   rename_i h₆ h₇
   replace ⟨h₁, h₁'⟩ := h₁
   subst h₁ h₁'
   simp only [true_and]
-  exists ety
+  exists ety, ty, tx₁, tx₂
   simp only [ResultType.typeOf, Except.map, h₄, h₅, h₆, h₇]
   simp [TypedExpr.typeOf]
 
-theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities}
+theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr} {request : Request} {entities : Entities}
   (h₁ : CapabilitiesInvariant c₁ request entities)
   (h₂ : RequestAndEntitiesMatchEnvironment env request entities)
-  (h₃ : typeOf (Expr.binaryApp .getTag x₁ x₂) c₁ env = Except.ok (ty, c₂))
+  (h₃ : typeOf (Expr.binaryApp .getTag x₁ x₂) c₁ env = Except.ok (tx, c₂))
   (ih₁ : TypeOfIsSound x₁)
   (ih₂ : TypeOfIsSound x₂) :
   GuardedCapabilitiesInvariant (Expr.binaryApp .getTag x₁ x₂) c₂ request entities ∧
-  ∃ v, EvaluatesTo (Expr.binaryApp .getTag x₁ x₂) request entities v ∧ InstanceOfType v ty.typeOf
+  ∃ v, EvaluatesTo (Expr.binaryApp .getTag x₁ x₂) request entities v ∧ InstanceOfType v tx.typeOf
 := by
-  replace ⟨hc, ety, c₁', c₂', h₃, h₄, h₅, h₆⟩ := type_of_getTag_inversion h₃
+  replace ⟨hc, ety, ty, tx₁, tx₂, c₁', c₂', h₃, h₄, h₅, h₆, ht, htx, hc₁⟩ := type_of_getTag_inversion h₃
   subst hc
-  split_type_of h₃ ; rename_i h₃ hl₃ hr₃
-  split_type_of h₄ ; rename_i h₄ hl₄ hr₄
   replace ⟨_, v₁, ih₁, hty₁⟩ := ih₁ h₁ h₂ h₃
-  replace ⟨_, v₂, ih₂, hty₂⟩ := ih₂ h₁ h₂ h₄
+  replace ⟨_, v₂, ih₂, hty₂⟩ := ih₂ h₁ h₂ h₅
   simp only [EvaluatesTo] at *
   simp only [GuardedCapabilitiesInvariant, evaluate]
   rcases ih₁ with ih₁ | ih₁ | ih₁ | ih₁ <;>
@@ -80,9 +82,9 @@ theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {e
   rcases ih₂ with ih₂ | ih₂ | ih₂ | ih₂ <;>
   simp only [ih₂, Except.bind_ok, Except.bind_err, false_implies, Except.error.injEq, or_false, or_true, true_and, reduceCtorEq]
   any_goals (apply type_is_inhabited)
-  rw [hl₃] at hty₁
+  rw [h₄] at hty₁
   replace ⟨uid, hty₁, hv₁⟩ := instance_of_entity_type_is_entity hty₁
-  rw [hl₄] at hty₂
+  rw [h₆] at hty₂
   replace ⟨s, hv₂⟩ := instance_of_string_is_string hty₂
   subst hv₁ hv₂ hty₁
   simp only [apply₂, hasTag, Except.ok.injEq, Value.prim.injEq, Prim.bool.injEq, false_or, exists_eq_left']
@@ -94,26 +96,26 @@ theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {e
   rw [Map.findOrErr_ok_iff_find?_some] at hf₁
   replace ⟨entry, hf₂, _, _, _, h₂⟩  := h₂.right.left uid d hf₁
   simp only [InstanceOfEntityTags] at h₂
-  simp only [EntitySchema.tags?, Option.map_eq_some'] at h₅
-  replace ⟨_, h₅, h₇⟩ := h₅
-  simp only [hf₂, Option.some.injEq] at h₅
-  subst h₅
-  simp only [EntitySchemaEntry.tags?] at h₂ h₇
-  split at h₇
-  simp only [h₇] at h₂
+  simp [EntitySchema.tags?, Option.map_eq_some'] at ht
+  replace ⟨_, ht₁, ht₂⟩ := ht
+  simp only [hf₂, Option.some.injEq] at ht₁
+  subst ht₁
+  simp only [EntitySchemaEntry.tags?] at h₂ ht₂
+  split at ht₂
+  simp only [ht₂] at h₂
   have hf₃ := Map.findOrErr_returns d.tags s Error.tagDoesNotExist
   rcases hf₃ with ⟨v, hf₃⟩ | hf₃ <;>
   simp only [hf₃, false_implies, Except.error.injEq, or_self, false_and, exists_const, and_false,
     Except.ok.injEq, false_or, exists_eq_left', reduceCtorEq]
-  · simp only [← List.empty_eq, empty_capabilities_invariant request entities, implies_true, true_and, reduceCtorEq]
+  · simp only [htx, TypedExpr.typeOf, ← List.empty_eq, empty_capabilities_invariant request entities, implies_true, true_and, reduceCtorEq]
     apply h₂
     exact Map.findOrErr_ok_implies_in_values hf₃
-  · replace h₁ := h₁.right x₁ x₂ h₆
+  · replace h₁ := h₁.right x₁ x₂ hc₁
     simp only [EvaluatesTo, evaluate, ih₁, ih₂, apply₂, hasTag, Except.bind_ok, Except.ok.injEq,
       Value.prim.injEq, Prim.bool.injEq, false_or, reduceCtorEq] at h₁
     simp only [Entities.tagsOrEmpty, hf₁, Map.contains_iff_some_find?] at h₁
     replace ⟨_, h₁⟩ := h₁
     simp only [Map.findOrErr_err_iff_find?_none, h₁, reduceCtorEq] at hf₃
-  · cases h₇
+  · cases ht₂
 
 end Cedar.Thm

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

@@ -26,6 +26,55 @@ open Cedar.Data
 open Cedar.Spec
 open Cedar.Validation
 
+theorem type_of_call_args_inversion {xs : List Expr} {txs : List TypedExpr} {c : Capabilities} {env : Environment}
+  (htxs : (xs.mapM₁ λ x => justType (typeOf x.val c env)) = Except.ok txs) :
+  List.Forall₂ (λ xᵢ txᵢ => ∃ cᵢ, typeOf xᵢ c env = Except.ok (txᵢ, cᵢ)) xs txs
+:=
+match xs with
+| [] => by
+  replace htxs : txs = [] :=
+    by simpa [List.mapM₁, pure, Except.pure] using htxs
+  subst htxs
+  constructor
+| x :: xs => by
+  simp only [List.mapM₁, List.attach, List.attachWith, List.pmap_cons, List.mapM_cons, bind_pure_comp] at htxs
+  cases htx : justType (typeOf x c env) <;> simp only [htx, Except.bind_err, reduceCtorEq] at htxs
+  simp only [justType, Except.map] at htx
+  split at htx <;> simp only [reduceCtorEq, Except.ok.injEq] at htx
+  subst htx
+  simp only [List.mapM_pmap_subtype (fun x => justType (typeOf x c env))] at htxs
+  cases htxs' : List.mapM (fun x => justType (typeOf x c env)) xs <;>
+    simp only [htxs', Except.map_error, Except.map_ok, Except.bind_ok, reduceCtorEq, Except.ok.injEq] at htxs
+  subst txs
+  constructor
+  · rename_i r _ _
+    exists r.snd
+  · have ih := @type_of_call_args_inversion xs
+    simp [ih, htxs', List.mapM₁]
+
+theorem type_of_call_inversion {xs : List Expr} {c c' : Capabilities} {env : Environment} {tx : TypedExpr}
+  (htx : typeOf (Expr.call xfn xs) c env = Except.ok (tx, c')) :
+  ∃ txs,
+    (∃ ty, tx = .call xfn txs ty) ∧
+    List.Forall₂ (λ xᵢ txᵢ => ∃ cᵢ, typeOf xᵢ c env = .ok (txᵢ, cᵢ)) xs txs
+:= by
+  simp only [typeOf, typeOfCall] at htx
+  cases htx₁ : xs.mapM₁ fun x => justType (typeOf x.val c env) <;> simp only [htx₁, Except.bind_err, Except.bind_ok, reduceCtorEq] at htx
+  rename_i txs
+  exists txs
+  and_intros
+  · split at htx <;>
+    (first
+    | contradiction
+    | cases htx₁ : typeOfConstructor Ext.Decimal.decimal xs (CedarType.ext ExtType.decimal) <;> simp only [htx₁] at htx
+    | cases htx₁ : typeOfConstructor Ext.IPAddr.ip xs (CedarType.ext ExtType.ipAddr) <;> simp only [htx₁] at htx
+    | cases htx₁ : typeOfConstructor Cedar.Spec.Ext.Datetime.parse xs (.ext .datetime) <;> simp only [htx₁] at htx
+    | cases htx₁ : typeOfConstructor Cedar.Spec.Ext.Datetime.Duration.parse xs (.ext .duration) <;> simp only [htx₁] at htx
+    | skip) <;>
+    simp only [ok, err, Except.ok.injEq, Prod.mk.injEq, Except.bind_ok, Except.bind_err, reduceCtorEq] at htx <;>
+    simp [←htx]
+  · exact type_of_call_args_inversion htx₁
+
 theorem type_of_call_decimal_inversion {xs : List Expr} {c c' : Capabilities} {env : Environment} {ty : TypedExpr}
   (h₁ : typeOf (Expr.call .decimal xs) c env = Except.ok (ty, c')) :
   ty.typeOf = .ext .decimal ∧