diff --git a/cedar-lean/Cedar/Thm/TPE/PreservesTypeOf.lean b/cedar-lean/Cedar/Thm/TPE/PreservesTypeOf.lean index faf6c196f..ffc23ef9e 100644 --- a/cedar-lean/Cedar/Thm/TPE/PreservesTypeOf.lean +++ b/cedar-lean/Cedar/Thm/TPE/PreservesTypeOf.lean @@ -28,29 +28,22 @@ open Cedar.Spec open Cedar.Validation open Cedar.TPE -abbrev PEPreservesTypeOf (env : TypeEnv) - (res : Residual) - (req : Request) - (preq : PartialRequest) - (es : Entities) - (pes : PartialEntities) : Prop := - InstanceOfWellFormedEnvironment req es env → - RequestAndEntitiesRefine req es preq pes → - Residual.WellTyped env res → - (TPE.evaluate res preq pes).typeOf = res.typeOf +abbrev PEPreservesTypeOf (res : Residual) : Prop := + ∀ {env : TypeEnv} , Residual.WellTyped env res → + ∀ (preq : PartialRequest) (pes : PartialEntities), + (TPE.evaluate res preq pes).typeOf = res.typeOf -private theorem partial_eval_preserves_typeof_and {env : TypeEnv} {a b : Residual} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} - (ih_a : PEPreservesTypeOf env a req preq es pes) - (ih_b : PEPreservesTypeOf env b req preq es pes) : - PEPreservesTypeOf env (Residual.and a b ty) req preq es pes +private theorem partial_eval_preserves_typeof_and {a b : Residual} {ty : CedarType} + (ih_a : PEPreservesTypeOf a) + (ih_b : PEPreservesTypeOf b) : + PEPreservesTypeOf (Residual.and a b ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.and] split · cases h_wt rename_i h_bwt h_bty - replace ih_b := ih_b h_wf h_ref h_bwt + specialize ih_b h_bwt preq pes rw [h_bty] at ih_b exact ih_b · simp only [Residual.typeOf] @@ -59,7 +52,7 @@ private theorem partial_eval_preserves_typeof_and {env : TypeEnv} {a b : Residua · simp [Residual.typeOf] · cases h_wt rename_i h_awt h_aty _ _ - replace ih_a := ih_a h_wf h_ref h_awt + specialize ih_a h_awt preq pes rw [h_aty] at ih_a exact ih_a · split @@ -69,13 +62,12 @@ private theorem partial_eval_preserves_typeof_and {env : TypeEnv} {a b : Residua · simp [Residual.typeOf] · simp [Residual.typeOf] -private theorem partial_eval_preserves_typeof_or {env : TypeEnv} {a b : Residual} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} - (ih_a : PEPreservesTypeOf env a req preq es pes) - (ih_b : PEPreservesTypeOf env b req preq es pes) : - PEPreservesTypeOf env (Residual.or a b ty) req preq es pes +private theorem partial_eval_preserves_typeof_or {a b : Residual} {ty : CedarType} + (ih_a : PEPreservesTypeOf a) + (ih_b : PEPreservesTypeOf b) : + PEPreservesTypeOf (Residual.or a b ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.or] split · simp only [Residual.typeOf] @@ -83,13 +75,13 @@ private theorem partial_eval_preserves_typeof_or {env : TypeEnv} {a b : Residual rfl · cases h_wt rename_i h_bwt h_bty - replace ih_b := ih_b h_wf h_ref h_bwt + specialize ih_b h_bwt preq pes rw [h_bty] at ih_b exact ih_b · simp [Residual.typeOf] · cases h_wt rename_i h_awt h_aty _ _ - replace ih_a := ih_a h_wf h_ref h_awt + specialize ih_a h_awt preq pes rw [h_aty] at ih_a exact ih_a · split @@ -99,30 +91,28 @@ private theorem partial_eval_preserves_typeof_or {env : TypeEnv} {a b : Residual · simp [Residual.typeOf] · simp [Residual.typeOf] -private theorem partial_eval_preserves_typeof_ite {env : TypeEnv} {c t e : Residual} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} - (ih_t : PEPreservesTypeOf env t req preq es pes) - (ih_e : PEPreservesTypeOf env e req preq es pes) : - PEPreservesTypeOf env (Residual.ite c t e ty) req preq es pes +private theorem partial_eval_preserves_typeof_ite {c t e : Residual} {ty : CedarType} + (ih_t : PEPreservesTypeOf t) + (ih_e : PEPreservesTypeOf e) : + PEPreservesTypeOf (Residual.ite c t e ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.ite] split · cases h_wt split · rename_i h_twt _ _ _ - exact ih_t h_wf h_ref h_twt + exact ih_t h_twt preq pes · rename_i h_ewt h_teq _ rw [h_teq] - exact ih_e h_wf h_ref h_ewt + exact ih_e h_ewt preq pes · simp [Residual.typeOf] · simp [Residual.typeOf] -private theorem partial_eval_preserves_typeof_unaryApp {env : TypeEnv} {op : UnaryOp} {e : Residual} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} : - PEPreservesTypeOf env (Residual.unaryApp op e ty) req preq es pes +private theorem partial_eval_preserves_typeof_unaryApp {op : UnaryOp} {e : Residual} {ty : CedarType} : + PEPreservesTypeOf (Residual.unaryApp op e ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.apply₁] split . simp [Residual.typeOf] @@ -139,17 +129,14 @@ private theorem partial_eval_preserves_typeof_unaryApp {env : TypeEnv} {op : Una case h_2 => rename Int64 => i cases h₃ : i.neg? - all_goals simp [intOrErr] . simp [Residual.typeOf] -private theorem partial_eval_preserves_typeof_binaryApp {env : TypeEnv} {op : BinaryOp} {e1 e2 : Residual} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} - (ih_e1 : PEPreservesTypeOf env e1 req preq es pes) : - PEPreservesTypeOf env (Residual.binaryApp op e1 e2 ty) req preq es pes +private theorem partial_eval_preserves_typeof_binaryApp {op : BinaryOp} {e1 e2 : Residual} {ty : CedarType} : + PEPreservesTypeOf (Residual.binaryApp op e1 e2 ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.apply₂, Option.pure_def, Option.bind_eq_bind] split case h_1 => @@ -182,7 +169,6 @@ private theorem partial_eval_preserves_typeof_binaryApp {env : TypeEnv} {op : Bi case h_17 uid₁ tag _ _ => cases h_wt with | binaryApp h₆ h₇ h₈ => - have ih := ih_e1 h_wf h_ref h₆ unfold TPE.getTag cases pes.tags uid₁ case binaryApp.none => @@ -196,11 +182,10 @@ private theorem partial_eval_preserves_typeof_binaryApp {env : TypeEnv} {op : Bi · simp [Residual.typeOf] · simp [apply₂.self, Residual.typeOf] -private theorem partial_eval_preserves_typeof_call {env : TypeEnv} {xfn : ExtFun} {args : List Residual} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} : - PEPreservesTypeOf env (Residual.call xfn args ty) req preq es pes +private theorem partial_eval_preserves_typeof_call {xfn : ExtFun} {args : List Residual} {ty : CedarType} : + PEPreservesTypeOf (Residual.call xfn args ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.call] split · simp only [someOrError] @@ -211,11 +196,10 @@ private theorem partial_eval_preserves_typeof_call {env : TypeEnv} {xfn : ExtFun · simp [Residual.typeOf] · simp [Residual.typeOf] -private theorem partial_eval_preserves_typeof_getAttr {env : TypeEnv} {expr : Residual} {attr : Attr} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} : - PEPreservesTypeOf env (Residual.getAttr expr attr ty) req preq es pes +private theorem partial_eval_preserves_typeof_getAttr {expr : Residual} {attr : Attr} {ty : CedarType} : + PEPreservesTypeOf (Residual.getAttr expr attr ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.getAttr] split . simp [Residual.typeOf] @@ -226,11 +210,10 @@ private theorem partial_eval_preserves_typeof_getAttr {env : TypeEnv} {expr : Re . simp [Residual.typeOf] . simp [Residual.typeOf] -private theorem partial_eval_preserves_typeof_hasAttr {env : TypeEnv} {expr : Residual} {attr : Attr} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} : - PEPreservesTypeOf env (Residual.hasAttr expr attr ty) req preq es pes +private theorem partial_eval_preserves_typeof_hasAttr {expr : Residual} {attr : Attr} {ty : CedarType} : + PEPreservesTypeOf (Residual.hasAttr expr attr ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.hasAttr] split . simp [Residual.typeOf] @@ -240,11 +223,10 @@ private theorem partial_eval_preserves_typeof_hasAttr {env : TypeEnv} {expr : Re . simp [Residual.typeOf] . simp [Residual.typeOf] -private theorem partial_eval_preserves_typeof_set {env : TypeEnv} {ls : List Residual} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} : - PEPreservesTypeOf env (Residual.set ls ty) req preq es pes +private theorem partial_eval_preserves_typeof_set {ls : List Residual} {ty : CedarType} : + PEPreservesTypeOf (Residual.set ls ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.set] split · simp [Residual.typeOf] @@ -252,11 +234,10 @@ private theorem partial_eval_preserves_typeof_set {env : TypeEnv} {ls : List Res · simp [Residual.typeOf] · simp [Residual.typeOf] -private theorem partial_eval_preserves_typeof_record {env : TypeEnv} {ls : List (Attr × Residual)} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} : - PEPreservesTypeOf env (Residual.record ls ty) req preq es pes +private theorem partial_eval_preserves_typeof_record {ls : List (Attr × Residual)} {ty : CedarType} : + PEPreservesTypeOf (Residual.record ls ty) := by - unfold PEPreservesTypeOf - intros h_wf h_ref h_wt + intro env h_wt preq pes simp only [TPE.evaluate, TPE.record] split · simp [Residual.typeOf] @@ -270,26 +251,15 @@ Theorem: TPE.evaluate preserves the typeOf property. If a residual has a certain type, then partially evaluating it produces a residual with the same type. -/ -theorem partial_eval_preserves_typeof - {env : TypeEnv} - {res : Residual} - {req : Request} - {preq : PartialRequest} - {es : Entities} - {pes : PartialEntities} : - InstanceOfWellFormedEnvironment req es env → - RequestAndEntitiesRefine req es preq pes → - Residual.WellTyped env res → - (TPE.evaluate res preq pes).typeOf = res.typeOf +theorem partial_eval_preserves_typeof : + ∀ res, PEPreservesTypeOf res := by - intro h_wf h_ref h_wt - have h_ref₂ := h_ref - unfold RequestAndEntitiesRefine at h_ref₂ - rcases h_ref₂ with ⟨h_rref, h_eref⟩ - cases h₁: res with + intro res env + cases res with | val v ty => simp [TPE.evaluate, Residual.typeOf] | var v ty => + intro _ preq simp only [Residual.typeOf, TPE.evaluate] unfold varₚ simp only [varₚ.varₒ, someOrSelf] @@ -303,70 +273,25 @@ theorem partial_eval_preserves_typeof | error ty => simp [TPE.evaluate, Residual.typeOf] | and a b ty => - apply partial_eval_preserves_typeof_and - · exact fun h_wf h_ref h_wt => partial_eval_preserves_typeof h_wf h_ref h_wt - · exact fun h_wf h_ref h_wt => partial_eval_preserves_typeof h_wf h_ref h_wt - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt + exact partial_eval_preserves_typeof_and + (partial_eval_preserves_typeof a) (partial_eval_preserves_typeof b) | or a b ty => - apply partial_eval_preserves_typeof_or - · exact fun h_wf h_ref h_wt => partial_eval_preserves_typeof h_wf h_ref h_wt - · exact fun h_wf h_ref h_wt => partial_eval_preserves_typeof h_wf h_ref h_wt - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt + exact partial_eval_preserves_typeof_or + (partial_eval_preserves_typeof a) (partial_eval_preserves_typeof b) | ite c t e ty => - apply partial_eval_preserves_typeof_ite - · exact fun h_wf h_ref h_wt => partial_eval_preserves_typeof h_wf h_ref h_wt - · exact fun h_wf h_ref h_wt => partial_eval_preserves_typeof h_wf h_ref h_wt - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt + exact partial_eval_preserves_typeof_ite + (partial_eval_preserves_typeof t) (partial_eval_preserves_typeof e) | unaryApp op e ty => - apply partial_eval_preserves_typeof_unaryApp - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt + exact partial_eval_preserves_typeof_unaryApp | binaryApp op e1 e2 ty => - apply partial_eval_preserves_typeof_binaryApp - · exact fun h_wf h_ref h_wt => partial_eval_preserves_typeof h_wf h_ref h_wt - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt + exact partial_eval_preserves_typeof_binaryApp | call xfn args ty => - apply partial_eval_preserves_typeof_call - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt + exact partial_eval_preserves_typeof_call | getAttr expr attr ty => - apply partial_eval_preserves_typeof_getAttr - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt + exact partial_eval_preserves_typeof_getAttr | hasAttr expr attr ty => - apply partial_eval_preserves_typeof_hasAttr - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt + exact partial_eval_preserves_typeof_hasAttr | set ls ty => - apply partial_eval_preserves_typeof_set - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt + exact partial_eval_preserves_typeof_set | record ls ty => - apply partial_eval_preserves_typeof_record - · exact h_wf - · exact h_ref - · rw [← h₁] - exact h_wt -termination_by sizeOf res + exact partial_eval_preserves_typeof_record diff --git a/cedar-lean/Cedar/Thm/TPE/WellTypedCases.lean b/cedar-lean/Cedar/Thm/TPE/WellTypedCases.lean index 3a7934a81..f4f55324c 100644 --- a/cedar-lean/Cedar/Thm/TPE/WellTypedCases.lean +++ b/cedar-lean/Cedar/Thm/TPE/WellTypedCases.lean @@ -277,22 +277,22 @@ theorem partial_eval_well_typed_and {env : TypeEnv} {a b : Residual} {ty : Cedar · exact well_typed_bool · rename_i bty h_eval_b _ _ _ _ replace h_ty_b : bty = CedarType.bool BoolType.anyBool := by - replace h_ty_b' := partial_eval_preserves_typeof h_wf h_ref h_b + replace h_ty_b' := partial_eval_preserves_typeof _ h_b preq pes simp only [h_eval_b, h_ty_b] at h_ty_b' simpa [Residual.typeOf] using h_ty_b' apply Residual.WellTyped.and · exact h_a_wt · rw [h_ty_b] exact well_typed_bool - · rw [partial_eval_preserves_typeof h_wf h_ref h_a] + · rw [partial_eval_preserves_typeof _ h_a] exact h_ty_a · simp [h_ty_b, Residual.typeOf] . apply Residual.WellTyped.and · exact h_a_wt · exact h_b_wt - · rw [partial_eval_preserves_typeof h_wf h_ref h_a] + · rw [partial_eval_preserves_typeof _ h_a] exact h_ty_a - · rw [partial_eval_preserves_typeof h_wf h_ref h_b] + · rw [partial_eval_preserves_typeof _ h_b] exact h_ty_b /-- @@ -317,22 +317,22 @@ theorem partial_eval_well_typed_or {env : TypeEnv} {a b : Residual} {ty : CedarT · exact well_typed_bool · rename_i bty h_eval_b _ _ _ _ replace h_ty_b : bty = CedarType.bool BoolType.anyBool := by - replace h_ty_b' := partial_eval_preserves_typeof h_wf h_ref h_b + replace h_ty_b' := partial_eval_preserves_typeof _ h_b preq pes simp only [h_eval_b, h_ty_b] at h_ty_b' simpa [Residual.typeOf] using h_ty_b' apply Residual.WellTyped.or · exact h_a_wt · rw [h_ty_b] exact well_typed_bool - · rw [partial_eval_preserves_typeof h_wf h_ref h_a] + · rw [partial_eval_preserves_typeof _ h_a] exact h_ty_a · simp [h_ty_b, Residual.typeOf] . apply Residual.WellTyped.or · exact h_a_wt · exact h_b_wt - · rw [partial_eval_preserves_typeof h_wf h_ref h_a] + · rw [partial_eval_preserves_typeof _ h_a] exact h_ty_a - · rw [partial_eval_preserves_typeof h_wf h_ref h_b] + · rw [partial_eval_preserves_typeof _ h_b] exact h_ty_b /-- @@ -354,16 +354,16 @@ theorem partial_eval_well_typed_ite {env : TypeEnv} {c t e : Residual} {ty : Ced · exact h_t_wt · exact h_e_wt . apply Residual.WellTyped.error - . have h_t_type_eq : t.typeOf = (TPE.evaluate t preq pes).typeOf := (partial_eval_preserves_typeof h_wf h_ref h_t).symm - rw [h_t_type_eq] + . have h_t_type_eq := partial_eval_preserves_typeof _ h_t preq pes + rw [←h_t_type_eq] apply Residual.WellTyped.ite · exact h_c_wt · exact h_t_wt · exact h_e_wt - · rw [partial_eval_preserves_typeof h_wf h_ref h_c] + · rw [partial_eval_preserves_typeof _ h_c] exact h_ty_c - · rw [partial_eval_preserves_typeof h_wf h_ref h_t] - rw [partial_eval_preserves_typeof h_wf h_ref h_e] + · rw [partial_eval_preserves_typeof _ h_t] + rw [partial_eval_preserves_typeof _ h_e] exact h_ty_t /-- @@ -423,7 +423,7 @@ theorem partial_eval_well_typed_unaryApp {env : TypeEnv} {op : UnaryOp} {expr : | apply UnaryResidualWellTyped.isEmpty | apply UnaryResidualWellTyped.like | apply UnaryResidualWellTyped.is - rw [partial_eval_preserves_typeof h_wf h_ref h_expr] + rw [partial_eval_preserves_typeof _ h_expr] assumption /-- @@ -448,7 +448,7 @@ theorem partial_eval_well_typed_set {env : TypeEnv} {ls : List Residual} {ty : C have h₅ := List.mem_mapM_some_implies_exists_unmapped h₃ h₄ rcases h₅ with ⟨y, h₆, h₇⟩ specialize h₀ y h₆ - let h₈ := partial_eval_preserves_typeof h_wf h_ref h₀ + let h₈ := partial_eval_preserves_typeof _ h₀ preq pes simp only [Function.comp_apply, Residual.asValue] at h₇ split at h₇ case h_2 => @@ -483,7 +483,7 @@ theorem partial_eval_well_typed_set {env : TypeEnv} {ls : List Residual} {ty : C simp only [List.map₁, List.attach, List.map_subtype, List.unattach_attachWith, List.mem_map] at h₅ rcases h₅ with ⟨x₂, h₆, h₇⟩ specialize h₀ x₂ h₆ - let h₆ := partial_eval_preserves_typeof h_wf h_ref h₀ + let h₆ := partial_eval_preserves_typeof _ h₀ preq pes rw [h₇] at h₆ rename_i h₈ specialize h₁ x₂ h₈ @@ -571,7 +571,7 @@ theorem partial_eval_well_typed_record {env : TypeEnv} {ls : List (Attr × Resid injection h₁₄; rename_i h₁₅ simp only [Qualified.getType] rename_i h₁₆ - have h₁₇ := partial_eval_preserves_typeof h_wf h_ref h₁₁ + have h₁₇ := partial_eval_preserves_typeof _ h₁₁ preq pes rw [h₁₆] at h₁₇ rw [←h₁₇] simp only [Residual.typeOf] @@ -630,7 +630,7 @@ theorem partial_eval_well_typed_record {env : TypeEnv} {ls : List (Attr × Resid rename_i k v specialize h₀ k v h₄ simp only - let h₅ := partial_eval_preserves_typeof h_wf h_ref h₀ + let h₅ := partial_eval_preserves_typeof _ h₀ rw [h₅] /-- @@ -665,7 +665,7 @@ theorem partial_eval_well_typed_getAttr {env : TypeEnv} {expr : Residual} {attr apply Residual.WellTyped.error . simp only [someOrError] apply Residual.WellTyped.val - have h₁₁ := partial_eval_preserves_typeof h_wf h_ref h₅ + have h₁₁ := partial_eval_preserves_typeof _ h₅ preq pes rw [h₃, h₆] at h₁₁ simp [Residual.typeOf] at h₁₁ case getAttr_record rty h₄ h₅ h₆ => @@ -681,7 +681,7 @@ theorem partial_eval_well_typed_getAttr {env : TypeEnv} {expr : Residual} {attr . rename_i v simp only [someOrError] apply Residual.WellTyped.val - have h₁₁ := partial_eval_preserves_typeof h_wf h_ref h₄ + have h₁₁ := partial_eval_preserves_typeof _ h₄ preq pes rw [h₃] at h₁₁ rw [h₅] at h₁₁ simp only [Residual.typeOf, CedarType.record.injEq] at h₁₁ @@ -708,7 +708,7 @@ theorem partial_eval_well_typed_getAttr {env : TypeEnv} {expr : Residual} {attr . rename_i v simp only [someOrError] apply Residual.WellTyped.val - have h₁₁ := partial_eval_preserves_typeof h_wf h_ref h₅ + have h₁₁ := partial_eval_preserves_typeof _ h₅ preq pes rw [h₃, h₆] at h₁₁ simp only [Residual.typeOf, CedarType.entity.injEq] at h₁₁ unfold RequestAndEntitiesRefine at h_ref @@ -784,7 +784,7 @@ theorem partial_eval_well_typed_getAttr {env : TypeEnv} {expr : Residual} {attr rw [e₃] at h₁₂ simp [Map.empty, Map.find?] at h₁₂ case getAttr_record rty h₄ h₅ h₆ => - have h₇ := partial_eval_preserves_typeof h_wf h_ref h₄ + have h₇ := partial_eval_preserves_typeof _ h₄ preq pes rw [h₃] at h₇ rw [h₅] at h₇ simp only [Residual.typeOf] at h₇ @@ -803,7 +803,7 @@ theorem partial_eval_well_typed_getAttr {env : TypeEnv} {expr : Residual} {attr case h₁ => exact h_expr_wt case h₂ => - have h₈ := partial_eval_preserves_typeof h_wf h_ref h₆ + have h₈ := partial_eval_preserves_typeof _ h₆ rw [h₈] rw [h₇] case h₃ => @@ -815,7 +815,7 @@ theorem partial_eval_well_typed_getAttr {env : TypeEnv} {expr : Residual} {attr case h₁ => exact h_expr_wt case h₂ => - have h₁₀ := partial_eval_preserves_typeof h_wf h_ref h₆ + have h₁₀ := partial_eval_preserves_typeof _ h₆ rw [h₁₀, h₇] case h₃ => rw [h₈] @@ -996,7 +996,7 @@ theorem partial_eval_well_typed_call {env : TypeEnv} {xfn : ExtFun} {args : List case a => intro x h₄ specialize h₁ x h₄ - apply partial_eval_preserves_typeof h_wf h_ref h₁ + apply partial_eval_preserves_typeof _ h₁ case a => intro x h₄ cases x @@ -1029,14 +1029,14 @@ theorem partial_eval_well_typed_hasAttr {env : TypeEnv} {expr : Residual} {attr case h₁ => exact h_expr_wt case h₂ => - have h₁₀ := partial_eval_preserves_typeof h_wf h_ref h₅ + have h₁₀ := partial_eval_preserves_typeof _ h₅ rw [h₁₀, h₆] case hasAttr_record rty h₆ h₇ => apply Residual.WellTyped.hasAttr_record case h₁ => exact h_expr_wt case h₂ => - have h₁₀ := partial_eval_preserves_typeof h_wf h_ref h₆ + have h₁₀ := partial_eval_preserves_typeof _ h₆ rw [h₁₀] rw [h₇] @@ -1090,7 +1090,7 @@ theorem partial_eval_well_typed_app₂_values_hasTag : . simp only [Residual.typeOf] rename_i ety₂ eq₁ eq₂ have hᵣ : (ty₁ = CedarType.entity ety₂) := by { - have h₁₀ := partial_eval_preserves_typeof h_wf h_ref h_expr1 + have h₁₀ := partial_eval_preserves_typeof _ h_expr1 rw [← h₁₀] at eq₁ rw [h₃] at eq₁ simp only [Residual.typeOf] at eq₁ @@ -1100,7 +1100,7 @@ theorem partial_eval_well_typed_app₂_values_hasTag : . simp only [Residual.typeOf] rename_i ety₂ eq₁ eq₂ have hᵣ : (ty₂ = CedarType.string) := by { - have h₁₀ := partial_eval_preserves_typeof h_wf h_ref h_expr2 + have h₁₀ := partial_eval_preserves_typeof _ h_expr2 rw [← h₁₀] at eq₂ rw [h₇] at eq₂ simp [Residual.typeOf] at eq₂ @@ -1197,7 +1197,7 @@ theorem partial_eval_well_typed_app₂_values_getTag : rename Data.Map.find? env.ets id₁.ty = some w => h₂₁ unfold EntitySchema.tags? at h₄ have h_ety_eq : ety = id₁.ty := by { - have h₂₁ := partial_eval_preserves_typeof h_wf h_ref h_expr1 + have h₂₁ := partial_eval_preserves_typeof _ h_expr1 preq pes rw [← h₂₁] at h₅ unfold Residual.asValue at h₁ cases h₂₂: TPE.evaluate expr1 preq pes @@ -1247,7 +1247,7 @@ theorem partial_eval_well_typed_app₂_values_getTag : rw [h₃] at ih₁ rw [h₁] at ih₁ have h_ety_eq : ty = (CedarType.entity id₁.ty) := by { - have h₄ := partial_eval_preserves_typeof h_wf h_ref h_expr1 + have h₄ := partial_eval_preserves_typeof _ h_expr1 preq pes cases ih₁ rename_i h₅ cases h₅ @@ -1267,7 +1267,7 @@ theorem partial_eval_well_typed_app₂_values_getTag : . simp [Residual.typeOf] . rename_i ety ty have h₄ : ety = id₁.ty := by - have h₄ := partial_eval_preserves_typeof h_wf h_ref h_expr1 + have h₄ := partial_eval_preserves_typeof _ h_expr1 preq pes simp only [Residual.asValue] at h₁ split at h₁ case h_2 => @@ -1336,7 +1336,7 @@ theorem partial_eval_well_typed_app₂_values_mem : . simp only [Residual.typeOf] rename_i ety₁ ety₂ eq₁ eq₂ have hᵣ : (ty₁ = CedarType.entity ety₁) := by { - have h₁₀ := partial_eval_preserves_typeof h_wf h_ref h_expr1 + have h₁₀ := partial_eval_preserves_typeof _ h_expr1 rw [← h₁₀] at eq₁ rw [h₃] at eq₁ simp only [Residual.typeOf] at eq₁ @@ -1346,7 +1346,7 @@ theorem partial_eval_well_typed_app₂_values_mem : . simp only [Residual.typeOf] rename_i ety₁ ety₂ eq₁ eq₂ have hᵣ : (ty₂ = CedarType.entity ety₂) := by { - have h₁₀ := partial_eval_preserves_typeof h_wf h_ref h_expr2 + have h₁₀ := partial_eval_preserves_typeof _ h_expr2 rw [← h₁₀] at eq₂ rw [h₇] at eq₂ simp only [Residual.typeOf] at eq₂ @@ -1357,7 +1357,7 @@ theorem partial_eval_well_typed_app₂_values_mem : . simp only [Residual.typeOf] rename_i ety₁ ety₂ eq₁ eq₂ have hᵣ : (ty₁ = CedarType.entity ety₁) := by { - have h₁₀ := partial_eval_preserves_typeof h_wf h_ref h_expr1 + have h₁₀ := partial_eval_preserves_typeof _ h_expr1 rw [← h₁₀] at eq₁ rw [h₃] at eq₁ simp only [Residual.typeOf] at eq₁ @@ -1367,7 +1367,7 @@ theorem partial_eval_well_typed_app₂_values_mem : . simp only [Residual.typeOf] rename_i ety₁ ety₂ eq₁ eq₂ have hᵣ : (ty₂ = (CedarType.entity ety₂).set) := by { - have h₁₀ := partial_eval_preserves_typeof h_wf h_ref h_expr2 + have h₁₀ := partial_eval_preserves_typeof _ h_expr2 rw [← h₁₀] at eq₂ rw [h₇] at eq₂ simp only [Residual.typeOf] at eq₂ @@ -1465,8 +1465,8 @@ theorem partial_eval_well_typed_app₂_nonvalues : rw [h₁] at h₃ contradiction case h_2 _ _ => - let h₁ := partial_eval_preserves_typeof h_wf h_ref h_expr1 - have h₂ := partial_eval_preserves_typeof h_wf h_ref h_expr2 + have h₁ := partial_eval_preserves_typeof _ h_expr1 + have h₂ := partial_eval_preserves_typeof _ h_expr2 split case h_1 => apply Residual.WellTyped.error