Of Env entities valid refs for wt expr
Cedar.Thm.ofEnv_entities_valid_refs_for_wt_expr
Plain-language statement
Given a well-formed environment and a well-typed expression in that environment, we show that the expression satisfies ValidRefs
Exact Lean statement
theorem ofEnv_entities_valid_refs_for_wt_expr
{Γ : TypeEnv} {tx : TypedExpr}
(hwf : Γ.WellFormed)
(hwt : TypedExpr.WellTyped Γ tx) :
tx.toExpr.ValidRefs ((SymEnv.ofEnv Γ).entities.isValidEntityUID ·)Formal artifact
Lean source
theorem ofEnv_entities_valid_refs_for_wt_expr {Γ : TypeEnv} {tx : TypedExpr} (hwf : Γ.WellFormed) (hwt : TypedExpr.WellTyped Γ tx) : tx.toExpr.ValidRefs ((SymEnv.ofEnv Γ).entities.isValidEntityUID ·):= by cases hwt with | lit hwt_prim => rename_i p ty cases hwt_prim with | bool | int | string => simp only [TypedExpr.toExpr] constructor constructor | entityUID uid huid => simp only [TypedExpr.toExpr] constructor simp only [Prim.ValidRef] apply entity_uid_wf_implies_sym_entities_is_valid_entity_uid hwf huid | var hwt_var => simp only [TypedExpr.toExpr] constructor | ite h₁ h₂ h₃ => simp only [TypedExpr.toExpr] constructor exact ofEnv_entities_valid_refs_for_wt_expr hwf h₁ exact ofEnv_entities_valid_refs_for_wt_expr hwf h₂ exact ofEnv_entities_valid_refs_for_wt_expr hwf h₃ | and h₁ h₂ | or h₁ h₂ => simp only [TypedExpr.toExpr] constructor exact ofEnv_entities_valid_refs_for_wt_expr hwf h₁ exact ofEnv_entities_valid_refs_for_wt_expr hwf h₂ | unaryApp h | hasAttr_entity h | hasAttr_record h | getAttr_entity h | getAttr_record h => simp only [TypedExpr.toExpr] constructor exact ofEnv_entities_valid_refs_for_wt_expr hwf h | binaryApp h₁ h₂ => simp only [TypedExpr.toExpr] constructor exact ofEnv_entities_valid_refs_for_wt_expr hwf h₁ exact ofEnv_entities_valid_refs_for_wt_expr hwf h₂ | set hs | call hs => simp only [TypedExpr.toExpr] constructor intros x hmem_x simp only [List.map₁, List.map_attach_eq_pmap] at hmem_x have ⟨x', hmem_x', hx'⟩ := List.mem_pmap.mp hmem_x simp only [←hx'] have := hs x' hmem_x' exact ofEnv_entities_valid_refs_for_wt_expr hwf this | record hrec => simp only [TypedExpr.toExpr] constructor intros attr hmem_attr rw [List.map₂_eq_map λ x => (x.fst, TypedExpr.toExpr x.snd)] at hmem_attr have ⟨attr', hmem_attr', hattr'⟩ := List.mem_map.mp hmem_attr cases attr with | _ fst snd => simp only [Prod.mk.injEq] at hattr' simp only [←hattr'] have := hrec attr'.fst attr'.snd hmem_attr' exact ofEnv_entities_valid_refs_for_wt_expr hwf this- Project
- Cedar Specification
- License
- Apache-2.0
- Commit
- 3f093947b8ae
- Source
- cedar-lean/Cedar/Thm/SymCC/Env/ofEnv.lean:1120-1183
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Find? ext
Cedar.Data.Map.find?_ext
Plain-language statement
Two well-formed maps are equal if they have the same find? for every key.
Source project: Cedar Specification
Person-level attribution pending.
Find? notmem keys
Cedar.Data.Map.find?_notmem_keys
Plain-language statement
Inverse of find?_mem_toList, except that this requires wf
Source project: Cedar Specification
Person-level attribution pending.
Find? some iff in values
Cedar.Data.Map.find?_some_iff_in_values
Plain-language statement
The mp direction of this does not need the wf precondition and, in fact, is available separately as find?_some_implies_in_values above
Source project: Cedar Specification
Person-level attribution pending.