address a bunch of review comments

cedar-lean/Cedar/Data/List.lean

@@ -123,8 +123,8 @@ theorem Equiv.trans {a b c : List α} :
   simp
   intro h₁ h₂ h₃ h₄
   apply And.intro
-  case _ => exact List.Subset.trans h₁ h₃
-  case _ => exact List.Subset.trans h₄ h₂
+  exact List.Subset.trans h₁ h₃
+  exact List.Subset.trans h₄ h₂
 
 theorem cons_equiv_cons (x : α) (xs ys : List α) :
   xs ≡ ys → x :: xs ≡ x :: ys
@@ -158,13 +158,8 @@ theorem filter_equiv (f : α -> Bool) (xs ys : List α) :
   intro a h₃ <;>
   simp [List.mem_filter] <;>
   rw [List.mem_filter] at h₃
-  constructor
-  case _ => exact h₁ h₃.left
-  case _ => exact h₃.right
-  case _ =>
-    constructor
-    case _ => exact h₂ h₃.left
-    case _ => exact h₃.right
+  exact And.intro (h₁ h₃.left) h₃.right
+  exact And.intro (h₂ h₃.left) h₃.right
 
 theorem map_equiv (f : α → β) (xs ys : List α) :
   xs ≡ ys → xs.map f ≡ ys.map f
@@ -176,8 +171,8 @@ theorem map_equiv (f : α → β) (xs ys : List α) :
   apply Exists.intro p <;>
   rw [List.subset_def] at a b <;>
   simp
-  case _ => exact a h
-  case _ => exact b h
+  exact a h
+  exact b h
 
 theorem filterMap_equiv (f : α → Option β) (xs ys : List α) :
   xs ≡ ys → xs.filterMap f ≡ ys.filterMap f
@@ -188,15 +183,15 @@ theorem filterMap_equiv (f : α → Option β) (xs ys : List α) :
   intro b a h₃ h₄ <;>
   apply Exists.intro a <;>
   simp [h₄]
-  case left => exact h₁ h₃
-  case right => exact h₂ h₃
+  exact h₁ h₃
+  exact h₂ h₃
 
 theorem tail_of_sorted_is_sorted {x : α} {xs : List α} [LT α] :
   Sorted (x :: xs) → Sorted xs
 := by
   intro h₁; cases h₁
-  case cons_nil => exact Sorted.nil
-  case cons_cons => assumption
+  exact Sorted.nil
+  assumption
 
 theorem if_strictly_sorted_then_head_lt_tail [LT α] [StrictLT α] (x : α) (xs : List α) :
   Sorted (x :: xs) → ∀ y, y ∈ xs → x < y
@@ -267,10 +262,10 @@ theorem if_strictly_sorted_equiv_then_tail_equiv [LT α] [StrictLT α] (x : α)
 := by
   unfold List.Equiv
   intro h₁ h₂ h₃
-  rcases h₃ with ⟨h₃, h₄⟩
+  replace ⟨h₃, h₄⟩ := h₃
   apply And.intro
-  case _ => exact if_strictly_sorted_equiv_then_tail_subset x xs ys h₁ h₂ h₃
-  case _ => exact if_strictly_sorted_equiv_then_tail_subset x ys xs h₂ h₁ h₄
+  exact if_strictly_sorted_equiv_then_tail_subset x xs ys h₁ h₂ h₃
+  exact if_strictly_sorted_equiv_then_tail_subset x ys xs h₂ h₁ h₄
 
 theorem if_strictly_sorted_equiv_then_eq [LT α] [StrictLT α] (xs ys : List α) :
   Sorted xs → Sorted ys → xs ≡ ys → xs = ys
@@ -418,15 +413,15 @@ theorem insertCanonical_equiv [LT α] [StrictLT α] [DecidableLT α] (x : α) (x
           case inr _ _ _ h₃ =>
             cases h₃
             case inr _ _ _ h₃ =>
-              rcases h₃ with ⟨h₃, h₄, h₅⟩
+              replace ⟨h₃, h₄, h₅⟩ := h₃
               simp [h₅]
               unfold GT.gt at h₄
               have h₆ := StrictLT.if_not_lt_gt_then_eq x hd' h₃ h₄
               subst h₆
               unfold List.Equiv
               simp only [cons_subset, mem_cons, true_or, or_true, Subset.refl, and_self, subset_cons]
             case inl _ _ _ h₃ =>
-              rcases h₃ with ⟨h₃, h₄, h₅⟩
+              replace ⟨h₃, h₄, h₅⟩ := h₃
               simp [h₅]
               simp [h₃, h₄] at ih
               have h₆ := swap_cons_cons_equiv x hd (hd' :: tl')
@@ -443,16 +438,16 @@ theorem canonicalize_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : α 
 := by
   apply Iff.intro
   case _ =>
-    intro h0
+    intro h₀
     cases xs with
     | nil => contradiction
     | cons hd tl =>
       unfold canonicalize
       apply insertCanonical_not_nil
   case _ =>
     unfold canonicalize
-    intro h0
-    cases xs <;> simp at h0; simp
+    intro h₀
+    cases xs <;> simp at h₀; simp
 
 theorem canonicalize_equiv [LT α] [StrictLT α] [DecidableLT α] (xs : List α) :
   xs ≡ canonicalize id xs
@@ -544,8 +539,7 @@ theorem canonicalize_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [Decid
   simp [Forallᵥ]
   intro h₁
   cases h₁
-  case nil =>
-    simp [canonicalize_nil]
+  case nil => simp [canonicalize_nil]
   case cons hd₁ hd₂ tl₁ tl₂ h₂ h₃ =>
     simp [canonicalize]
     have h₄ := canonicalize_preserves_forallᵥ p tl₁ tl₂ h₃
@@ -560,7 +554,7 @@ theorem any_of_mem {f : α → Bool} {x : α} {xs : List α}
   case cons hd tl =>
     simp [List.any_cons]
     rcases h₁ with h₁ | h₁
-    case inl => subst h₁ ; simp [h₂]
-    case inr => apply Or.inr ; exists x
+    subst h₁ ; simp [h₂]
+    apply Or.inr ; exists x
 
 end List

cedar-lean/Cedar/Data/Set.lean

@@ -167,17 +167,7 @@ theorem make_non_empty [DecidableEq α] [LT α] [DecidableLT α] (xs : List α)
   simp only [beq_eq_false_iff_ne, ne_eq, mk.injEq]
   apply List.canonicalize_not_nil
 
-theorem make_eq_if_eqv [LT α] [DecidableLT α] [StrictLT α] (xs ys : List α) :
-  xs ≡ ys → Set.make xs = Set.make ys
-:= by
-  intro h; unfold make; simp
-  apply List.if_equiv_strictLT_then_canonical _ _ h
-
-/--
-  careful: this is not exactly the converse of the theorem above.
-  For the converse of the theorem above, use `make_make_eqv`
--/
-theorem make_eqv [LT α] [DecidableLT α] [StrictLT α] {xs ys : List α} :
+theorem make_mk_eqv [LT α] [DecidableLT α] [StrictLT α] {xs ys : List α} :
   Set.make xs = Set.mk ys → xs ≡ ys
 := by
   simp [make] ; intro h₁
@@ -189,15 +179,17 @@ theorem make_make_eqv [LT α] [DecidableLT α] [StrictLT α] {xs ys : List α} :
   Set.make xs = Set.make ys ↔ xs ≡ ys
 := by
   constructor
-  case _ =>
+  case mp =>
     intro h; unfold make at h; simp at h
     have h₁ := List.canonicalize_equiv xs
     have h₂ := List.canonicalize_equiv ys
     unfold id at h₁ h₂
     rw [← h] at h₂
     have h₃ := List.Equiv.symm h₂; clear h₂
     exact List.Equiv.trans (a := xs) (b := List.canonicalize (fun x => x) xs) (c := ys) h₁ h₃
-  case _ => exact Set.make_eq_if_eqv (α := α) (xs := xs) (ys := ys)
+  case mpr =>
+    intro h; unfold make; simp
+    apply List.if_equiv_strictLT_then_canonical _ _ h
 
 theorem make_mem [LT α] [DecidableLT α] [StrictLT α] (x : α) (xs : List α) :
   x ∈ xs ↔ x ∈ Set.make xs

cedar-lean/Cedar/Spec/Authorizer.lean

@@ -27,13 +27,6 @@ open Effect
 def satisfied (policy : Policy) (req : Request) (entities : Entities) : Bool :=
   (evaluate policy.toExpr req entities) = .ok true
 
-/--
-  Despite its name, this function is not just a version of `satisfied` that takes
-  into account the `effect`.
-
-  While `satisfied` returns Bool, `satisfiedWithEffect` returns `Option PolicyID`
-  with the policy's id if it is satisfied.
--/
 def satisfiedWithEffect (effect : Effect) (policy : Policy) (req : Request) (entities : Entities) : Option PolicyID :=
   if policy.effect == effect && satisfied policy req entities
   then some policy.id
@@ -52,18 +45,18 @@ def hasError (policy : Policy) (req : Request) (entities : Entities) : Bool :=
   `Option PolicyID`, but not analogous to `satisfiedWithEffect` in that it does
   not consider the policy's effect.
 -/
-def idIfHasError (policy : Policy) (req : Request) (entities : Entities) : Option PolicyID :=
+def errored (policy : Policy) (req : Request) (entities : Entities) : Option PolicyID :=
   if hasError policy req entities then some policy.id else none
 
 def errorPolicies (policies : Policies) (req : Request) (entities : Entities) : Set PolicyID :=
-  Set.make (policies.filterMap (idIfHasError · req entities))
+  Set.make (policies.filterMap (errored · req entities))
 
 def isAuthorized (req : Request) (entities : Entities) (policies : Policies) : Response :=
   let forbids := satisfiedPolicies .forbid policies req entities
   let permits := satisfiedPolicies .permit policies req entities
-  let error_policies := errorPolicies policies req entities
+  let erroredPolicies := errorPolicies policies req entities
   if forbids.isEmpty && !permits.isEmpty
-  then { decision := .allow, determining_policies := permits, error_policies }
-  else { decision := .deny,  determining_policies := forbids, error_policies }
+  then { decision := .allow, determiningPolicies := permits, erroredPolicies }
+  else { decision := .deny,  determiningPolicies := forbids, erroredPolicies }
 
 end Cedar.Spec

cedar-lean/Cedar/Spec/Response.lean

@@ -32,8 +32,8 @@ inductive Decision where
 
 structure Response where
   decision : Decision
-  determining_policies : Set PolicyID
-  error_policies : Set PolicyID
+  determiningPolicies : Set PolicyID
+  erroredPolicies : Set PolicyID
 
 ----- Derivations -----
 

cedar-lean/Cedar/Thm/Authorization/Authorizer.lean

@@ -87,7 +87,7 @@ theorem satisfiedPolicies_order_and_dup_independent (effect : Effect) (request :
 := by
   intro h₁
   unfold satisfiedPolicies
-  apply Set.make_eq_if_eqv
+  rw [Set.make_make_eqv]
   exact List.filterMap_equiv (satisfiedWithEffect effect · request entities) policies₁ policies₂ h₁
 
 theorem errorPolicies_order_and_dup_independent (request : Request) (entities : Entities) (policies₁ policies₂ : Policies) :
@@ -96,8 +96,8 @@ theorem errorPolicies_order_and_dup_independent (request : Request) (entities :
 := by
   intro h₁
   unfold errorPolicies
-  apply Set.make_eq_if_eqv
-  exact List.filterMap_equiv (idIfHasError · request entities) policies₁ policies₂ h₁
+  rw [Set.make_make_eqv]
+  exact List.filterMap_equiv (errored · request entities) policies₁ policies₂ h₁
 
 theorem sound_policy_slice_is_equisatisfied (effect : Effect) (request : Request) (entities : Entities) (slice policies : Policies) :
   IsSoundPolicySlice request entities slice policies →
@@ -128,7 +128,7 @@ theorem satisfiedPolicies_eq_for_sound_policy_slice (effect : Effect) (request :
 := by
   intro h
   unfold satisfiedPolicies
-  apply Set.make_eq_if_eqv
+  rw [Set.make_make_eqv]
   exact sound_policy_slice_is_equisatisfied effect request entities slice policies h
 
 theorem sound_policy_slice_is_equierror (request : Request) (entities : Entities) (slice policies : Policies) :
@@ -163,28 +163,28 @@ theorem alternate_errorPolicies_equiv_errorPolicies {policies : Policies} {reque
   errorPolicies policies request entities = alternateErrorPolicies policies request entities
 := by
   unfold errorPolicies alternateErrorPolicies
-  apply Set.make_eq_if_eqv
+  rw [Set.make_make_eqv]
   simp [List.Equiv, List.subset_def]
   apply And.intro
-  case a.left =>
+  case left =>
     intro pid p h₁ h₂
     apply Exists.intro p
-    unfold idIfHasError hasError at h₂
+    unfold errored hasError at h₂
     split at h₂
     case inl h₃ =>
       unfold hasError
       apply And.intro
       case left => simp [h₃, h₁, List.mem_filter]
       case right => simp at h₂; exact h₂
     case inr => contradiction
-  case a.right =>
+  case right =>
     intro p h₁
     apply Exists.intro p
     simp [List.mem_filter] at h₁
     apply And.intro
     case left => exact h₁.left
     case right =>
-      unfold idIfHasError
+      unfold errored
       split
       case inl => rfl
       case inr h₃ => simp [h₃] at h₁
@@ -196,7 +196,7 @@ theorem errorPolicies_eq_for_sound_policy_slice (request : Request) (entities :
   intro h
   repeat rw [alternate_errorPolicies_equiv_errorPolicies]
   unfold alternateErrorPolicies
-  apply Set.make_eq_if_eqv
+  rw [Set.make_make_eqv]
   apply List.map_equiv
   exact sound_policy_slice_is_equierror request entities slice policies h
 
@@ -385,16 +385,16 @@ theorem mapOrErr_value_asEntityUID_on_uids_produces_set {list : List EntityUID}
     -- in this case, mapping Value.asEntityUID over the set returns .ok
     replace h := mapM'_asEntityUID_eq_entities h
     have ⟨h₁, h₂⟩ := Set.elts_make_is_id_then_equiv h; clear h
-    apply Set.make_eq_if_eqv
+    rw [Set.make_make_eqv]
     unfold List.Equiv at *
     repeat rw [List.subset_def] at *
     constructor <;> intro a h₃ <;>
     replace h₃ := List.mem_map_of_mem (Value.prim ∘ Prim.entityUID) h₃
-    case a.left =>
+    case left =>
       specialize h₁ h₃
       simp at h₁
       exact h₁
-    case a.right =>
+    case right =>
       specialize h₂ h₃
       simp at h₂
       exact h₂
@@ -427,7 +427,8 @@ theorem principal_scope_produces_boolean {policy : Policy} {request : Request} {
     simp [Result.as, Lean.Internal.coeM, Coe.coe, Value.asBool, pure, Except.pure, CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe]
     generalize (inₑ request.principal uid entities) = b₁
     generalize (ety == request.principal.ty) = b₂
-    split <;> simp
+    split
+    case h_1 => trivial
     case h_2 h => split at h <;> simp at h
 
 /--
@@ -439,7 +440,8 @@ theorem action_scope_produces_boolean {policy : Policy} {request : Request} {ent
   simp [producesBool, evaluate, ActionScope.toExpr, Scope.toExpr]
   cases policy.actionScope
   case actionInAny list =>
-    split <;> simp
+    split
+    case h_1 => trivial
     case h_2 res h =>
       simp at h
       have h₁ := @action_in_set_of_euids_produces_boolean list request entities
@@ -454,7 +456,8 @@ theorem action_scope_produces_boolean {policy : Policy} {request : Request} {ent
       simp [Result.as, Lean.Internal.coeM, Coe.coe, Value.asBool, pure, Except.pure, CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe]
       generalize (inₑ request.action uid entities) = b₁
       generalize (ety == request.action.ty) = b₂
-      split <;> simp
+      split
+      case h_1 => trivial
       case h_2 h => split at h <;> simp at h
 
 /--
@@ -470,7 +473,8 @@ theorem resource_scope_produces_boolean {policy : Policy} {request : Request} {e
     simp [Result.as, Lean.Internal.coeM, Coe.coe, Value.asBool, pure, Except.pure, CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe]
     generalize (inₑ request.resource uid entities) = b₁
     generalize (ety == request.resource.ty) = b₂
-    split <;> simp
+    split
+    case h_1 => trivial
     case h_2 h => split at h <;> simp at h
 
 /--

cedar-lean/Cedar/Thm/Authorization/Evaluator.lean

@@ -73,14 +73,14 @@ theorem and_true_implies_right_true {e₁ e₂ : Expr} {request : Request} {enti
 /--
   `producesBool` means the expression evaluates to a bool (and not an error)
 -/
-def producesBool (e : Expr) (request : Request) (entities : Entities) : Bool :=
+def producesBool (e : Expr) (request : Request) (entities : Entities) : Prop :=
   match (evaluate e request entities) with
   | .ok (.prim (.bool _)) => true
   | _ => false
 /--
   `producesNonBool` means the expression evaluates to a non-bool (and not an error)
 -/
-def producesNonBool (e : Expr) (request : Request) (entities : Entities) : Bool :=
+def producesNonBool (e : Expr) (request : Request) (entities : Entities) : Prop :=
   match (evaluate e request entities) with
   | .ok (.prim (.bool _)) => false
   | .error _ => false
@@ -136,7 +136,10 @@ theorem ways_and_can_error {e₁ e₂ : Expr} {request : Request} {entities : En
   Every `and` expression produces either .ok bool or .error
 -/
 theorem and_produces_bool_or_error {e₁ e₂ : Expr} {request : Request} {entities : Entities} :
-  match (evaluate (Expr.and e₁ e₂) request entities) with | .ok (.prim (.bool _)) => true | .error _ => true | _ => false
+  match (evaluate (Expr.and e₁ e₂) request entities) with
+  | .ok (.prim (.bool _)) => true
+  | .error _ => true
+  | _ => false
 := by
   cases h : evaluate (Expr.and e₁ e₂) request entities <;> simp
   case ok val =>

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

@@ -682,7 +682,7 @@ theorem evaluate_entity_set_eqv {vs : List Value} {euids euids' : List EntityUID
   rw [List.map_map] at h₃
   rw [←List.mapM'_eq_mapM] at h₂
   replace h₂ := mapM'_asEntityUID_eq_entities h₂
-  replace h₁ := Set.make_eqv h₁
+  replace h₁ := Set.make_mk_eqv h₁
   subst h₂ h₃
   simp [List.Equiv, List.subset_def] at *
   have ⟨hl₁, hr₁⟩ := h₁