lean: some tiny refactors (#224)

cedar-lean/Cedar/Data/LT.lean

@@ -168,8 +168,7 @@ theorem List.lt_conn [LT α] [StrictLT α] {xs ys : List α} :
         have h₆ := StrictLT.if_not_lt_gt_then_eq xhd yhd h₄ h₅
         subst h₆
         simp at h₁
-        have h₆ := List.lt_conn h₁
-        cases h₆
+        cases (List.lt_conn h₁)
         case inl _ _ h₆ =>
           have h₇ := List.cons_lt_cons xhd xtl ytl h₆
           contradiction

cedar-lean/Cedar/Data/List.lean

@@ -305,8 +305,9 @@ theorem insertCanonical_not_nil [DecidableEq β] [LT β] [DecidableRel (α := β
   | nil => simp
   | cons hd tl =>
     simp
-    by_cases h₁ : (f x) < (f hd) <;> simp [h₁]
-    by_cases h₂ : (f x) > (f hd) <;> simp [h₂]
+    intro h
+    split at h <;> try trivial
+    split at h <;> trivial
 
 theorem insertCanonical_cases [LT α] [DecidableLT α] (x y : α) (ys : List α) :
   (x < y ∧ insertCanonical id x (y :: ys) = x :: y :: ys) ∨

cedar-lean/Cedar/Thm/Core/LT.lean

@@ -219,7 +219,7 @@ theorem EntityUID.lt_conn {a b : EntityUID} :
   cases a ; cases b ; rename_i ty₁ eid₁ ty₂ eid₂
   simp [LT.lt]
   intro h₁
-  simp [EntityUID.lt]
+  unfold EntityUID.lt
   by_cases (ty₁ = ty₂)
   case pos h₂ =>
     subst h₂ ; simp only [forall_const, true_and] at *

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

@@ -130,23 +130,23 @@ theorem type_of_eq_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env :
         case false => exact false_is_instance_of_ff
         case true  => contradiction
     case h_2 =>
-      have ⟨ty₁, c₁', ty₂, c₂', ht₁, ht₂, hty⟩ := hty
-      specialize ih₁ h₁ h₂ ht₁ ; have ⟨_, v₁, ih₁⟩ := ih₁
-      specialize ih₂ h₁ h₂ ht₂ ; have ⟨_, v₂, ih₂⟩ := ih₂
+      replace ⟨ty₁, c₁', ty₂, c₂', ht₁, ht₂, hty⟩ := hty
+      specialize ih₁ h₁ h₂ ht₁ ; replace ⟨_, v₁, ih₁⟩ := ih₁
+      specialize ih₂ h₁ h₂ ht₂ ; replace ⟨_, v₂, ih₂⟩ := ih₂
       simp [EvaluatesTo, evaluate] at *
       cases h₄ : evaluate x₁ request entities <;> simp [h₄] at * <;>
       cases h₅ : evaluate x₂ request entities <;> simp [h₅] at * <;>
       try { simp [ih₁, ih₂] ; apply type_is_inhabited }
-      have ⟨ihl₁, ih₃⟩ := ih₁ ; clear ih₁
-      have ⟨ihl₂, ih₄⟩ := ih₂ ; clear ih₂
+      replace ⟨ihl₁, ih₃⟩ := ih₁
+      replace ⟨ihl₂, ih₄⟩ := ih₂
       rw [eq_comm] at ihl₁ ihl₂; subst ihl₁ ihl₂
       simp [apply₂]
       split at hty
       case h_1 =>
         rw [hty]
         apply bool_is_instance_of_anyBool
       case h_2 heq =>
-        have ⟨hty₀, ⟨ety₁, hty₁⟩, ⟨ety₂, hty₂⟩⟩ := hty
+        have ⟨hty₀, ⟨ety₁, hty₁⟩, ⟨ety₂, hty₂⟩⟩ := hty ; clear hty
         subst hty₀ hty₁ hty₂
         have h₆ := no_entity_type_lub_implies_not_eq ih₃ ih₄ heq
         cases h₇ : v₁ == v₂ <;>
@@ -192,16 +192,16 @@ theorem type_of_int_cmp_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c
   constructor
   case left => exact empty_guarded_capabilities_invariant
   case right =>
-    have ⟨c₁', ht₁⟩ := ht₁
-    have ⟨c₂', ht₂⟩ := ht₂
-    specialize ih₁ h₁ h₂ ht₁ ; have ⟨_, v₁, ih₁⟩ := ih₁
-    specialize ih₂ h₁ h₂ ht₂ ; have ⟨_, v₂, ih₂⟩ := ih₂
+    replace ⟨c₁', ht₁⟩ := ht₁
+    replace ⟨c₂', ht₂⟩ := ht₂
+    specialize ih₁ h₁ h₂ ht₁ ; replace ⟨_, v₁, ih₁⟩ := ih₁
+    specialize ih₂ h₁ h₂ ht₂ ; replace ⟨_, v₂, ih₂⟩ := ih₂
     simp [EvaluatesTo, evaluate] at *
     cases h₄ : evaluate x₁ request entities <;> simp [h₄] at * <;>
     cases h₅ : evaluate x₂ request entities <;> simp [h₅] at * <;>
     try { simp [ih₁, ih₂] ; exact type_is_inhabited (.bool .anyBool) }
-    have ⟨ihl₁, ih₃⟩ := ih₁ ; clear ih₁
-    have ⟨ihl₂, ih₄⟩ := ih₂ ; clear ih₂
+    replace ⟨ihl₁, ih₃⟩ := ih₁
+    replace ⟨ihl₂, ih₄⟩ := ih₂
     rw [eq_comm] at ihl₁ ihl₂; subst ihl₁ ihl₂
     have ⟨i₁, ih₁⟩ := instance_of_int_is_int ih₃
     have ⟨i₂, ih₂⟩ := instance_of_int_is_int ih₄
@@ -231,7 +231,7 @@ theorem type_of_int_arith_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c'
     split at h₂ <;> try contradiction
     simp at h₂ ; simp [h₂]
     rename_i tc₁ tc₂ _ _ _ _ h₅ h₆
-    have ⟨h₂, _⟩ := h₂
+    replace ⟨h₂, _⟩ := h₂
     constructor
     case left  => exists tc₁.snd ; simp [←h₂, ←h₅]
     case right => exists tc₂.snd ; simp [←h₂, ←h₆]
@@ -252,16 +252,16 @@ theorem type_of_int_arith_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c
   constructor
   case left => exact empty_guarded_capabilities_invariant
   case right =>
-    have ⟨c₁', ht₁⟩ := ht₁
-    have ⟨c₂', ht₂⟩ := ht₂
-    specialize ih₁ h₁ h₂ ht₁ ; have ⟨_, v₁, ih₁⟩ := ih₁
-    specialize ih₂ h₁ h₂ ht₂ ; have ⟨_, v₂, ih₂⟩ := ih₂
+    replace ⟨c₁', ht₁⟩ := ht₁
+    replace ⟨c₂', ht₂⟩ := ht₂
+    specialize ih₁ h₁ h₂ ht₁ ; replace ⟨_, v₁, ih₁⟩ := ih₁
+    specialize ih₂ h₁ h₂ ht₂ ; replace ⟨_, v₂, ih₂⟩ := ih₂
     simp [EvaluatesTo, evaluate] at *
     cases h₄ : evaluate x₁ request entities <;> simp [h₄] at * <;>
     cases h₅ : evaluate x₂ request entities <;> simp [h₅] at * <;>
     try { simp [ih₁, ih₂] ; exact type_is_inhabited .int }
-    have ⟨ihl₁, ih₃⟩ := ih₁ ; clear ih₁
-    have ⟨ihl₂, ih₄⟩ := ih₂ ; clear ih₂
+    replace ⟨ihl₁, ih₃⟩ := ih₁
+    replace ⟨ihl₂, ih₄⟩ := ih₂
     rw [eq_comm] at ihl₁ ihl₂; subst ihl₁ ihl₂
     have ⟨i₁, ih₁⟩ := instance_of_int_is_int ih₃
     have ⟨i₂, ih₂⟩ := instance_of_int_is_int ih₄
@@ -315,16 +315,16 @@ theorem type_of_contains_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities}
   constructor
   case left => exact empty_guarded_capabilities_invariant
   case right =>
-    have ⟨c₁', ht₁⟩ := ht₁
-    have ⟨c₂', ht₂⟩ := ht₂
-    specialize ih₁ h₁ h₂ ht₁ ; have ⟨_, v₁, ih₁⟩ := ih₁
-    specialize ih₂ h₁ h₂ ht₂ ; have ⟨_, v₂, ih₂⟩ := ih₂
+    replace ⟨c₁', ht₁⟩ := ht₁
+    replace ⟨c₂', ht₂⟩ := ht₂
+    specialize ih₁ h₁ h₂ ht₁ ; replace ⟨_, v₁, ih₁⟩ := ih₁
+    specialize ih₂ h₁ h₂ ht₂ ; replace ⟨_, v₂, ih₂⟩ := ih₂
     simp [EvaluatesTo, evaluate] at *
     cases h₄ : evaluate x₁ request entities <;> simp [h₄] at * <;>
     cases h₅ : evaluate x₂ request entities <;> simp [h₅] at * <;>
     try { simp [ih₁, ih₂] ; apply type_is_inhabited }
-    have ⟨ihl₁, ih₃⟩ := ih₁ ; clear ih₁
-    have ⟨ihl₂, ih₄⟩ := ih₂ ; clear ih₂
+    replace ⟨ihl₁, ih₃⟩ := ih₁
+    replace ⟨ihl₂, ih₄⟩ := ih₂
     rw [eq_comm] at ihl₁ ihl₂; subst ihl₁ ihl₂
     have ⟨s₁, ih₁⟩ := instance_of_set_type_is_set ih₃
     subst ih₁
@@ -376,16 +376,16 @@ theorem type_of_containsA_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c
   constructor
   case left => exact empty_guarded_capabilities_invariant
   case right =>
-    have ⟨c₁', ht₁⟩ := ht₁
-    have ⟨c₂', ht₂⟩ := ht₂
-    specialize ih₁ h₁ h₂ ht₁ ; have ⟨_, v₁, ih₁⟩ := ih₁
-    specialize ih₂ h₁ h₂ ht₂ ; have ⟨_, v₂, ih₂⟩ := ih₂
+    replace ⟨c₁', ht₁⟩ := ht₁
+    replace ⟨c₂', ht₂⟩ := ht₂
+    specialize ih₁ h₁ h₂ ht₁ ; replace ⟨_, v₁, ih₁⟩ := ih₁
+    specialize ih₂ h₁ h₂ ht₂ ; replace ⟨_, v₂, ih₂⟩ := ih₂
     simp [EvaluatesTo, evaluate] at *
     cases h₄ : evaluate x₁ request entities <;> simp [h₄] at * <;>
     cases h₅ : evaluate x₂ request entities <;> simp [h₅] at * <;>
     try { simp [ih₁, ih₂] ; apply type_is_inhabited }
-    have ⟨ihl₁, ih₃⟩ := ih₁ ; clear ih₁
-    have ⟨ihl₂, ih₄⟩ := ih₂ ; clear ih₂
+    replace ⟨ihl₁, ih₃⟩ := ih₁
+    replace ⟨ihl₂, ih₄⟩ := ih₂
     rw [eq_comm] at ihl₁ ihl₂; subst ihl₁ ihl₂
     have ⟨s₁, ih₁⟩ := instance_of_set_type_is_set ih₃
     have ⟨s₂, ih₂⟩ := instance_of_set_type_is_set ih₄
@@ -440,7 +440,7 @@ theorem actionUID?_some_implies_action_lit {x : Expr} {euid : EntityUID} {acts :
   cases h₂ : entityUID? x <;> simp [h₂] at h₁
   replace h₂ := entityUID?_some_implies_entity_lit h₂
   rename_i euid'
-  have ⟨h₀, h₁⟩ := h₁
+  replace ⟨h₀, h₁⟩ := h₁
   subst h₀
   simp [h₁, h₂]
 
@@ -459,7 +459,7 @@ theorem entityUIDs?_some_implies_entity_lits {x : Expr} {euids : List EntityUID}
     rename_i hd' tl'
     cases h₂ : entityUID? hd' <;> simp [h₂] at h₁
     cases h₃ : List.mapM' entityUID? tl' <;> simp [h₃] at h₁
-    have ⟨hhd, htl⟩ := h₁ ; rw [eq_comm] at hhd htl ; subst hhd htl
+    have ⟨hhd, htl⟩ := h₁ ; clear h₁ ; rw [eq_comm] at hhd htl ; subst hhd htl
     replace h₂ := entityUID?_some_implies_entity_lit h₂
     simp [h₂]
     rw [List.mapM'_eq_mapM] at h₃
@@ -522,19 +522,19 @@ theorem type_of_mem_is_soundₑ {x₁ x₂ : Expr} {c₁ c₁' c₂' : Capabilit
   try { apply type_is_inhabited }
   rw [eq_comm] at hev₂ ; subst hev₂
   replace hty₁ := instance_of_entity_type_is_entity hty₁
-  have ⟨euid₁, hty₁, hty₁'⟩ := hty₁
+  replace ⟨euid₁, hty₁, hty₁'⟩ := hty₁
   subst hty₁ hty₁'
   replace hty₂ := instance_of_entity_type_is_entity hty₂
-  have ⟨euid₂, hty₂, hty₂'⟩ := hty₂
+  replace ⟨euid₂, hty₂, hty₂'⟩ := hty₂
   subst hty₂ hty₂'
   simp [apply₂]
   apply InstanceOfType.instance_of_bool
   simp [InstanceOfBoolType]
   split <;> try simp only
   rename_i b bty  h₇ h₈ h₉
   simp [typeOfInₑ] at *
-  have ⟨_, hents, hacts⟩ := h₂
-  cases ha : actionUID? x₁ env.acts <;> simp [ha] at h₇ h₈ h₉
+  have ⟨_, hents, hacts⟩ := h₂ ; clear h₂
+  cases hₐ : actionUID? x₁ env.acts <;> simp [hₐ] at h₇ h₈ h₉
   case none =>
     cases hin : EntitySchema.descendentOf env.ets euid₁.ty euid₂.ty <;>
     simp [hin] at h₇ h₈ h₉
@@ -546,13 +546,12 @@ theorem type_of_mem_is_soundₑ {x₁ x₂ : Expr} {c₁ c₁' c₂' : Capabilit
       simp [hin] at h₇ h₈ h₉
       simp [entity_type_in_false_implies_inₑ_false hents hin] at h₉
     case some =>
-      replace ha := actionUID?_some_implies_action_lit ha
-      have ⟨ha', ha''⟩ := ha ; clear ha
-      subst ha'
+      replace ⟨hₐ, hₐ'⟩ := actionUID?_some_implies_action_lit hₐ
+      subst hₐ
       replace he := entityUID?_some_implies_entity_lit he ; subst he
       rename_i auid euid _ _
       simp [evaluate] at h₅ h₆ ; subst h₅ h₆
-      have h₁₀ := action_type_in_eq_action_inₑ auid euid hacts ha''
+      have h₁₀ := action_type_in_eq_action_inₑ auid euid hacts hₐ'
       simp [h₁₀] at h₈ h₉
       cases heq : ActionSchema.descendentOf env.acts auid euid <;> simp [heq] at h₈ h₉
 
@@ -571,8 +570,7 @@ theorem entity_set_type_implies_set_of_entities {vs : List Value} {ety : EntityT
     cases h₁ ; rename_i h₁
     have h₂ := h₁ hd
     simp [Set.mem_cons_self] at h₂
-    replace h₂ := instance_of_entity_type_is_entity h₂
-    have ⟨heuid, hdty, h₂⟩ := h₂
+    replace ⟨heuid, hdty, h₂⟩ := instance_of_entity_type_is_entity h₂
     subst h₂
     rw [Value.asEntityUID] ; simp
     rw [List.mapM'_eq_mapM]
@@ -597,7 +595,7 @@ theorem entity_type_in_false_implies_inₛ_false {euid : EntityUID} {euids : Lis
   simp [EntitySchema.descendentOf] at h₂
   rw [Set.make_any_iff_any]
   by_contra h₄ ; simp at h₄
-  have ⟨euid', h₄, h₅⟩ := h₄
+  replace ⟨euid', h₄, h₅⟩ := h₄
   simp [inₑ] at h₅
   rcases h₅ with h₅ | h₅
   case inl =>
@@ -608,7 +606,7 @@ theorem entity_type_in_false_implies_inₛ_false {euid : EntityUID} {euids : Lis
     simp [Entities.ancestorsOrEmpty, Set.contains, Set.elts, Set.empty] at h₅
     cases h₆ : Map.find? entities euid <;> simp [h₆] at h₅
     rename_i data
-    have ⟨entry, h₁, _, h₇⟩ := h₁ euid data h₆
+    replace ⟨entry, h₁, _, h₇⟩ := h₁ euid data h₆
     specialize h₇ euid' h₅
     split at h₂ <;> try contradiction
     rename_i h₈
@@ -705,12 +703,12 @@ theorem action_type_in_eq_action_inₛ {auid : EntityUID} {euids euids' : List E
   specialize h₁ auid entry
   constructor <;> intro h₄ <;> rename_i hfnd <;>
   simp [hfnd] at h₁ <;>
-  have ⟨data, hl₁, hr₁⟩ := h₁
+  have ⟨data, hl₁, hr₁⟩ := h₁ <;> clear h₁
   case some.mp =>
     rw [List.any_eq_true] at h₄
-    have ⟨euid, h₄, h₅⟩ := h₄
+    replace ⟨euid, h₄, h₅⟩ := h₄
     exists euid
-    have ⟨h₃, _⟩ := h₃
+    replace ⟨h₃, _⟩ := h₃
     simp [List.subset_def] at h₃
     specialize h₃ h₄ ; simp [h₃]
     simp [inₑ] at h₅
@@ -724,9 +722,9 @@ theorem action_type_in_eq_action_inₛ {auid : EntityUID} {euids euids' : List E
       exact h₅
   case some.mpr =>
     rw [List.any_eq_true]
-    have ⟨euid, h₄, h₅⟩ := h₄
+    replace ⟨euid, h₄, h₅⟩ := h₄
     exists euid
-    have ⟨_, h₃⟩ := h₃
+    replace ⟨_, h₃⟩ := h₃
     simp [List.subset_def] at h₃
     specialize h₃ h₄ ; simp [h₃]
     simp [ActionSchema.descendentOf, hfnd] at h₅
@@ -757,7 +755,7 @@ theorem type_of_mem_is_soundₛ {x₁ x₂ : Expr} {c₁ c₁' c₂' : Capabilit
   cases h₆ : evaluate x₂ request entities <;> simp [h₆] at hev₂ <;> simp [h₆, hev₂] <;>
   try { apply type_is_inhabited }
   rw [eq_comm] at hev₂ ; subst hev₂
-  have ⟨euid, hty₁, hty₁'⟩ := instance_of_entity_type_is_entity hty₁
+  replace ⟨euid, hty₁, hty₁'⟩ := instance_of_entity_type_is_entity hty₁
   subst hty₁ hty₁'
   have ⟨vs, hset⟩ := instance_of_set_type_is_set hty₂
   subst hset
@@ -770,7 +768,7 @@ theorem type_of_mem_is_soundₛ {x₁ x₂ : Expr} {c₁ c₁' c₂' : Capabilit
   simp [InstanceOfBoolType]
   split <;> try simp
   rename_i h₈ h₉ h₁₀
-  have ⟨_, hents, hacts⟩ := h₂
+  have ⟨_, hents, hacts⟩ := h₂ ; clear h₂
   simp [typeOfInₛ] at *
   cases ha : actionUID? x₁ env.acts <;> simp [ha] at h₈ h₉ h₁₀
   case none =>
@@ -784,8 +782,8 @@ theorem type_of_mem_is_soundₛ {x₁ x₂ : Expr} {c₁ c₁' c₂' : Capabilit
       simp [hin] at h₈ h₉ h₁₀
       simp [entity_type_in_false_implies_inₛ_false hents hin hty₇] at h₁₀
     case some =>
-      have ⟨ha', hac⟩ := actionUID?_some_implies_action_lit ha
-      subst ha'
+      replace ⟨ha, hac⟩ := actionUID?_some_implies_action_lit ha
+      subst ha
       have he := entityUIDs?_some_implies_entity_lits he
       subst he
       simp [evaluate] at h₅ ; rw [eq_comm] at h₅ ; subst h₅

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

@@ -545,8 +545,7 @@ theorem lubRecordType_assoc_none_some {rty₁ rty₂ rty₃ rty₄ : List (Attr
 := by
   unfold lubRecordType at h₂
   split at h₂ <;> try contradiction
-  case h_1 =>
-    simp at h₂ ; subst h₂ ; exact h₁
+  case h_1 => simp at h₂ ; subst h₂ ; exact h₁
   case h_2 a₂ qty₂ rty₂' a₃ qty₃ rty₃'  =>
     simp at h₂
     split at h₂ <;> try contradiction
@@ -561,11 +560,10 @@ theorem lubRecordType_assoc_none_some {rty₁ rty₂ rty₃ rty₄ : List (Attr
       simp [lubRecordType]
     case cons hd tl =>
       simp [hrty₁] at h₁
-      by_cases h₆ : hd.fst = a₂
+      unfold lubRecordType
+      by_cases h₆ : hd.fst = a₂ <;> simp [h₆]
       case pos =>
         simp [h₆] at h₁
-        unfold lubRecordType
-        simp [h₆]
         cases h₇ : lubQualifiedType hd.snd qty₂ <;> simp [h₇] at h₁
         case none =>
           have _ : sizeOf hd.snd < sizeOf rty₁ := by -- termination
@@ -577,9 +575,6 @@ theorem lubRecordType_assoc_none_some {rty₁ rty₂ rty₃ rty₄ : List (Attr
           cases h₈ : lubRecordType tl rty₂' <;> simp [h₈] at h₁
           have h₉ := lubRecordType_assoc_none_some h₈ h₅
           simp [h₉]
-      case neg =>
-        unfold lubRecordType
-        simp [h₆]
 
 theorem lubQualifiedType_assoc_none_some {qty₁ qty₂ qty₃ qty₄ : QualifiedType}
   (h₁ : (lubQualifiedType qty₁ qty₂) = none)