diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/WellFormed.lean b/cedar-lean/Cedar/Thm/Validation/Levels/WellFormed.lean index de1de3568..429cfe16e 100644 --- a/cedar-lean/Cedar/Thm/Validation/Levels/WellFormed.lean +++ b/cedar-lean/Cedar/Thm/Validation/Levels/WellFormed.lean @@ -1235,6 +1235,15 @@ theorem SameAttrs_inv₂ {α β : Type} {lhs : List (Attr × α)} {rhs : List (A def EvaluatesToOk (request : Request) (entities : Entities) (lhs : (Attr × Expr)) (rhs : Attr × Value) : Prop := lhs.fst = rhs.fst ∧ evaluate lhs.snd request entities = .ok rhs.snd +def EvaluatesToOk' (request : Request) (entities : Entities) (lhs : Expr) (rhs : Value) : Prop := + evaluate lhs request entities = .ok rhs + +theorem EvaluatesToOk_same_keys {request : Request} {entities : Entities} {lhs : (Attr × Expr)} {rhs : Attr × Value} : + lhs.fst = rhs.fst ∧ EvaluatesToOk' request entities lhs.snd rhs.snd ↔ EvaluatesToOk request entities lhs rhs := by + simp [EvaluatesToOk, EvaluatesToOk'] + + + theorem evalutesToOk_is_AttributeRelation (request : Request) (entities : Entities) : AttributeRelation (EvaluatesToOk request entities) := by @@ -1366,85 +1375,138 @@ theorem record_typing (attrs : List (Attr × Expr)) (ty_map : Map Attr Qualified exists ty' simp [h'] -theorem insertCanonical_preserves_attr_relation {α β} - {r : (Attr × α) → (Attr × β) → Prop} - {kv₁ : Attr × α} {kv₂ : Attr × β} {kvs₁ : List (Attr × α)} {kvs₂ : List (Attr × β)} - (h₁ : kv₁.fst = kv₂.fst ∧ r kv₁ kv₂) - (h₂ : List.Forall₂ r kvs₁ kvs₂) - (h₃ : AttributeRelation r) - (h₄ : SameAttrs kvs₁ kvs₂) : - List.Forall₂ r (List.insertCanonical Prod.fst kv₁ kvs₁) (List.insertCanonical Prod.fst kv₂ kvs₂) - ∧ SameAttrs (List.insertCanonical Prod.fst kv₁ kvs₁) (List.insertCanonical Prod.fst kv₂ kvs₂) +theorem forall_same_lengths {α β : Type} (r : α → β → Prop) (lhs : List α) (rhs : List β) + (h : List.Forall₂ r lhs rhs) : + lhs.length = rhs.length := by - cases h₂ - case nil => + cases h + case _ => + simp + case _ => + simp + apply forall_same_lengths + assumption + + +theorem forall_attr_relation_implies_same_attrs {α β : Type} + (r : (Attr × α) → (Attr × β) → Prop) + (kvs₁ : List (Attr × α)) (kvs₂ : List (Attr × β)) + (h₁ : List.Forall₂ r kvs₁ kvs₂) + (h₂ : AttributeRelation r) : + SameAttrs kvs₁ kvs₂ + := by + cases h₁ + case _ => + simp [SameAttrs] + case _ => + apply SameAttrs_cons + case _ => + simp [AttributeRelation] at h₂ + apply h₂ + assumption + case _ => + apply forall_attr_relation_implies_same_attrs + repeat assumption + + +theorem forallᵥ_is_forall₂ {α β : Type} + (r : α → β → Prop) + (kvs₁ : List (Attr × α)) (kvs₂ : List (Attr × β)) + (h₁ : List.Forallᵥ r kvs₁ kvs₂) : + List.Forall₂ (λ lhs rhs => lhs.fst = rhs.fst ∧ r lhs.snd rhs.snd) kvs₁ kvs₂ + := by + simp [List.Forallᵥ] at h₁ + cases h₁ + case _ => + constructor + case _ head₁ tail₁ head₂ tail₂ head_prop tail_prop => constructor case _ => - simp only [List.insertCanonical_singleton, h₁, List.forall₂_cons, List.Forall₂.nil, and_true] + apply head_prop case _ => - simp [SameAttrs, List.map, h₁] - case cons hd₁ hd₂ tl₁ tl₂ h₅ h₆ => - simp only [List.insertCanonical, gt_iff_lt] - split <;> split <;> rename_i h₇ h₈ + apply tail_prop + +theorem forall₂_is_forallᵥ {α β : Type} + (r : (Attr × α) → (Attr × β) → Prop) + (r' : α → β → Prop) + (kvs₁ : List (Attr × α)) (kvs₂ : List (Attr × β)) + (h₁ : List.Forall₂ r kvs₁ kvs₂) + (h₂ : AttributeRelation r) + (h₃ : ∀ kv₁ kv₂, kv₁.fst = kv₂.fst ∧ r' kv₁.snd kv₂.snd ↔ r kv₁ kv₂) : + List.Forallᵥ r' kvs₁ kvs₂ + := by + cases h₁ + case _ => + constructor + case _ head₁ tail₁ head₂ tail₂ head_prop tail_prop => + constructor case _ => - constructor - case _ => - constructor - case _ => - simp [h₁] - case _ => - constructor - case _ => - assumption - case _ => - assumption - case _ => - apply SameAttrs_cons - simp [h₁] - apply SameAttrs_cons - apply SameAttrs_inv₁ - apply h₄ - apply SameAttrs_inv₂ - apply h₄ + rw [h₃] + assumption case _ => + apply forall₂_is_forallᵥ + repeat assumption + +theorem forall₂_weakening {α β : Type} (r r' : α → β → Prop) (lhs : List α) (rhs : List β) + (h₁ : List.Forall₂ r' lhs rhs) + (h₂ : ∀ a b, r' a b → r a b) : + List.Forall₂ r lhs rhs + := by + cases h₁ <;> constructor + case _ => + apply h₂ + assumption + case _ => + apply forall₂_weakening + repeat assumption + + + + +theorem canonicalize_preserves_attr_relations' {α β} + (r : (Attr × α) → (Attr × β) → Prop) + (r' : α → β → Prop) + (h₄ : ∀ kv₁ kv₂, kv₁.fst = kv₂.fst ∧ r' kv₁.snd kv₂.snd ↔ r kv₁ kv₂) + (kvs₁ : List (Attr × α)) (kvs₂ : List (Attr × β)) + (h₁ : List.Forall₂ r kvs₁ kvs₂) + (h₂ : AttributeRelation r) : + List.Forall₂ r (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂) + := by + have step₁ : List.Forallᵥ r' kvs₁ kvs₂ := by + apply forall₂_is_forallᵥ + repeat assumption + have step₂ : List.Forallᵥ r' (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂) := by + apply List.canonicalize_preserves_forallᵥ + apply step₁ + have step₃ : List.Forall₂ (λ lhs rhs => lhs.fst = rhs.fst ∧ r' lhs.snd rhs.snd) (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂) := by + apply forallᵥ_is_forall₂ + apply step₂ + apply forall₂_weakening + repeat assumption + intros a b h + rw [h₄] at h + apply h - sorry - all_goals sorry - -- · apply Forall₂.cons (by exact h₁) - -- exact Forall₂.cons (by exact h₃) (by exact h₄) - -- · simp only [h₁, h₃] at h₅ - -- have _ := StrictLT.asymmetric kv₂.fst hd₂.fst h₅ - -- split <;> contradiction - -- · simp only [h₁, h₃] at h₅ h₆ - -- split - -- · contradiction - -- · apply Forall₂.cons (by exact h₃) - -- exact insertCanonical_preserves_forallᵥ h₁ h₄ - -- · simp only [h₁, h₃] at h₅ h₆ - -- split - -- · contradiction - -- · exact Forall₂.cons (by exact h₁) (by exact h₄) theorem canonicalize_preserves_attr_relations {α β} (r : (Attr × α) → (Attr × β) → Prop) + (r' : α → β → Prop) + (h₄ : ∀ kv₁ kv₂, kv₁.fst = kv₂.fst ∧ r' kv₁.snd kv₂.snd ↔ r kv₁ kv₂) (kvs₁ : List (Attr × α)) (kvs₂ : List (Attr × β)) (h₁ : List.Forall₂ r kvs₁ kvs₂) (h₂ : AttributeRelation r) - (h₃ : SameAttrs kvs₁ kvs₂) : + (_h₃ : SameAttrs kvs₁ kvs₂) + : List.Forall₂ r (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂) ∧ SameAttrs (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂) := by - cases h₁ - case nil => - constructor - · simp [List.canonicalize_nil] - · simp [SameAttrs, List.map] - case cons hd₁ hd₂ tl₁ tl₂ h₃ h₄ => - simp only [List.canonicalize] - sorry - - -- apply insertCanonical_preserves_forallᵥ h₂ h₄ + have step : List.Forall₂ r (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂) := by + apply canonicalize_preserves_attr_relations' + repeat assumption + simp [step] + apply forall_attr_relation_implies_same_attrs + repeat assumption def List.find_indx_inner? {α : Type} (p : α → Bool) (l : List α) (idx : Nat) : Option (α × Nat) := match l with @@ -1629,6 +1691,8 @@ theorem map_preserves_attrprops₃ {α β : Type} (kvs₁ : List (Attr × α)) (kvs₂ : List (Attr × β)) (k : Attr) (v₁ : α) (v₂ : β) (r : (Attr × α) → (Attr × β) → Prop) + (r' : α → β → Prop) + (h₆ : ∀ kv₁ kv₂, kv₁.fst = kv₂.fst ∧ r' kv₁.snd kv₂.snd ↔ r kv₁ kv₂) (h₁ : AttributeRelation r) (h₂ : List.Forall₂ r kvs₁ kvs₂) (h₃ : SameAttrs kvs₁ kvs₂) @@ -1639,7 +1703,7 @@ theorem map_preserves_attrprops₃ {α β : Type} simp [Map.make] at h₄ simp [Map.make] at h₅ have ⟨step₁, step₂⟩ : List.Forall₂ r (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂) ∧ SameAttrs (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂) := by - exact canonicalize_preserves_attr_relations r kvs₁ kvs₂ h₂ h₁ h₃ + exact canonicalize_preserves_attr_relations r r' h₆ kvs₁ kvs₂ h₂ h₁ h₃ apply map_preserves_attrprops₂ apply h₁ apply step₁ @@ -1723,7 +1787,9 @@ theorem evaluates_to_well_formed_record {attrs : List (Attr × Expr)} {v : Value simp [Map.make] at hexprmap rw [hexprmap] refine - canonicalize_preserves_attr_relations (EvaluatesToOk request entities) attrs vs evals ?h₂ + canonicalize_preserves_attr_relations (EvaluatesToOk request entities) (EvaluatesToOk' request entities) + (by simp [EvaluatesToOk, EvaluatesToOk']) + attrs vs evals ?h₂ evals_sameattrs exact evalutesToOk_is_AttributeRelation request entities have matching_expr : ∃ e, (Map.mk attrs_canonical).find? k = some e ∧ (flip (EvaluatesToOk request entities)) (k, v) (k, e) := by @@ -1743,7 +1809,9 @@ theorem evaluates_to_well_formed_record {attrs : List (Attr × Expr)} {v : Value rw [hexprmap] simp [Map.make] at h_ty_map rw [← h_ty_map] - apply canonicalize_preserves_attr_relations + apply canonicalize_preserves_attr_relations (AttrExprHasAttrType c₁ env l₁) (AttrExprHasAttrType' c₁ env l₁) + intros kv₁ kv₂ + apply AttrExprHasAttrType_same_keys assumption apply attrExprHasAttrType_is_AttributeRelation assumption diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean index fcc5e7e92..ee27cd9bf 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean @@ -35,6 +35,28 @@ def AttrExprHasAttrType (c : Capabilities) (env : Environment) (l : Level) (ax : aqty = (ax.fst, .required ty') ∧ typeOf ax.snd c env (l == .infinite) = Except.ok (ty', c') +def AttrExprHasAttrType' (c : Capabilities) (env : Environment) (l : Level) (x : Expr) (qty : QualifiedType) : Prop := + ∃ ty' c', + qty = .required ty' ∧ + typeOf x c env (l == .infinite) = Except.ok (ty', c') + + +theorem AttrExprHasAttrType_same_keys (c : Capabilities) (env : Environment) (l : Level) (ax : Attr × Expr) (aqty : Attr × QualifiedType) : + ax.fst = aqty.fst ∧ AttrExprHasAttrType' c env l ax.snd aqty.snd ↔ AttrExprHasAttrType c env l ax aqty + := by + simp [AttrExprHasAttrType, AttrExprHasAttrType'] + constructor + case _ => + intros h + have ⟨h₁,ty, h₂, c', h₃⟩ := h + exists ty + simp [h₁,h₂,h₃] + rw [← h₂] + case _ => + intros h + have ⟨ty, h₁, c', h₂ ⟩ := h + simp [h₁,h₂] + theorem type_of_record_inversion_forall {axs : List (Attr × Expr)} {c : Capabilities} {env : Environment} {rty : List (Attr × QualifiedType)} {l : Level} (h₁ : List.mapM (fun x => requiredAttr x.fst (typeOf x.snd c env (l == .infinite))) axs = Except.ok rty) : List.Forall₂ (AttrExprHasAttrType c env l) axs rty