update to Lean 4.16

Dockerfile

@@ -1,8 +1,8 @@
-FROM amazonlinux:2 AS prepare
+FROM amazonlinux:2023 AS prepare
 
 RUN yum update -y \
   && yum install -y \
-  curl clang tar zip unzip python3 git xz \
+  curl-minimal clang tar zip unzip python3 git xz \
   make wget \
   && yum clean all
 
@@ -32,7 +32,10 @@ RUN git clone --depth 1 https://github.com/cedar-policy/cedar
 
 # Build the Lean formalization and extract to static C libraries
 WORKDIR $CEDAR_SPEC_ROOT/cedar-lean
-RUN source /root/.profile && source ../cedar-drt/set_env_vars.sh && elan default "$(cat lean-toolchain)" && ../cedar-drt/build_lean_lib.sh
+RUN source /root/.profile \
+  && elan default "$(cat lean-toolchain)" \
+  && source ../cedar-drt/set_env_vars.sh \
+  && ../cedar-drt/build_lean_lib.sh
 
 # Build DRT
 WORKDIR $CEDAR_SPEC_ROOT/cedar-drt

cedar-lean/Cedar/Data/LT.lean

@@ -45,6 +45,14 @@ theorem StrictLT.if_not_lt_gt_then_eq [LT α] [StrictLT α] (x y : α) :
   have h₄ := StrictLT.connected x y h₃
   simp [h₁, h₂] at h₄
 
+theorem StrictLT.if_not_lt_eq_then_gt [LT α] [StrictLT α] (x y : α) :
+  ¬ x < y → ¬ x = y → x > y
+:= by
+  intro h₁ h₂
+  by_contra h₃
+  have h₄ := StrictLT.connected x y h₂
+  simp [h₁, h₃] at h₄
+
 theorem StrictLT.not_eq [LT α] [StrictLT α] (x y : α) :
   x < y → ¬ x = y
 := by
@@ -62,69 +70,51 @@ end Cedar.Data
 
 open Cedar.Data
 
-theorem List.lt_cons_cases [LT α] {x y : α} {xs ys : List α} :
+theorem List.lt_cons_cases [LT α] [Cedar.Data.DecidableLT α] {x y : α} {xs ys : List α} :
   x :: xs < y :: ys →
   (x < y ∨ (¬ x < y ∧ ¬ y < x ∧ xs < ys))
 := by
   intro h₁
-  cases h₁
-  case head _ h₁ => simp [h₁]
-  case tail _ h₁ h₂ h₃ => simp [h₁, h₂]; assumption
+  cases h₁ <;> simp_all [lex_lt, Decidable.em]
 
 theorem List.cons_lt_cons [LT α] [StrictLT α] (x : α) (xs ys : List α) :
   xs < ys → x :: xs < x :: ys
 := by
   intro h₁
-  apply List.lt.tail (StrictLT.irreflexive x) (StrictLT.irreflexive x) h₁
+  apply List.Lex.cons
+  simp only [lex_lt, h₁]
 
-theorem List.slt_irrefl [LT α] [StrictLT α] (xs : List α) :
+theorem List.slt_irrefl [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List α) :
   ¬ xs < xs
 := by
   induction xs
   case nil => by_contra; contradiction
   case cons _ _ hd tl ih =>
     by_contra h₁
-    have h₂ := StrictLT.irreflexive hd
-    cases tl
-    case nil =>
-      have h₃ := List.lt_cons_cases h₁
-      simp [h₂] at h₃
-      contradiction
-    case cons _ _ hd' tl' =>
-      have h₃ := List.lt_cons_cases h₁
-      simp [h₂] at h₃
-      contradiction
+    replace h₁ := List.lt_cons_cases h₁
+    simp [StrictLT.irreflexive hd] at h₁
+    contradiction
 
 theorem List.slt_trans [LT α] [StrictLT α] {xs ys zs : List α} :
   xs < ys → ys < zs → xs < zs
 := by
   intro h₁ h₂
   cases h₁
-  case nil => cases h₂ <;> apply List.lt.nil
-  case head _ _ xhd xtl yhd ytl h₃ =>
-    cases h₂
-    case head _ _ zhd ztl h₄ =>
-      apply List.lt.head
-      apply StrictLT.transitive _ _ _ h₃ h₄
-    case tail _ _ zhd ztl h₄ h₅ h₆ =>
-      have h₇ := StrictLT.if_not_lt_gt_then_eq yhd zhd h₄ h₅
-      subst h₇
-      apply List.lt.head
-      exact h₃
-  case tail _ _ xhd xtl yhd ytl h₃ h₄ h₅ =>
+  case nil => cases h₂ <;> apply List.Lex.nil
+  case rel _ _ xhd xtl yhd ytl h₃ =>
+    cases h₂ <;> apply List.Lex.rel
+    case rel _ _ zhd ztl h₄ => exact StrictLT.transitive _ _ _ h₃ h₄
+    case cons _ _ ztl h₄ => exact h₃
+  case cons _ _ xhd xtl ytl h₃ =>
     cases h₂
-    case head _ _ zhd ztl h₆ =>
-      have h₇ := StrictLT.if_not_lt_gt_then_eq xhd yhd h₃ h₄
-      subst h₇
-      apply List.lt.head
+    case rel _ _ zhd ztl h₆ =>
+      apply List.Lex.rel
       exact h₆
-    case tail _ _ zhd ztl h₆ h₇ h₈ =>
-      have h₉ := StrictLT.if_not_lt_gt_then_eq xhd yhd h₃ h₄
-      subst h₉
-      apply List.lt.tail h₆ h₇
-      apply List.slt_trans h₅ h₈
+    case cons _ _ ztl h₆ =>
+      apply List.Lex.cons
+      exact List.slt_trans h₃ h₆
 
-theorem List.lt_asymm [LT α] [StrictLT α] {xs ys : List α} :
+theorem List.lt_asymm' [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] {xs ys : List α} :
   xs < ys → ¬ ys < xs
 := by
   intro h₁
@@ -146,38 +136,42 @@ theorem List.lt_conn [LT α] [StrictLT α] {xs ys : List α} :
 := by
   intro h₁
   by_contra h₂
-  simp [not_or] at h₂
-  have ⟨h₂, h₃⟩ := h₂
+  simp only [not_or] at h₂
+  replace ⟨h₂, h₃⟩ := h₂
   cases xs <;> cases ys
   case nil.nil => contradiction
-  case nil.cons _ _ xhd xtl _ =>
-    have h₄ := List.lt.nil xhd xtl
-    contradiction
-  case cons.nil _ _ yhd ytl _ =>
-    have h₄ := List.lt.nil yhd ytl
-    contradiction
-  case cons.cons _ _ xhd xtl yhd ytl _ =>
+  case nil.cons xhd xtl =>
+    simp_all only [ne_eq, nil_eq, not_false_eq_true, and_self, nil_lt_cons, not_true_eq_false]
+  case cons.nil yhd ytl =>
+    simp_all only [ne_eq, not_false_eq_true, and_self, not_lt_nil, nil_lt_cons, not_true_eq_false]
+  case cons.cons xhd xtl yhd ytl =>
     by_cases (xhd < yhd)
     case pos h₄ =>
-      have h₅ := List.lt.head xtl ytl h₄
+      have h₅ : xhd :: xtl < yhd :: ytl := List.Lex.rel h₄
       contradiction
     case neg h₄ =>
-      by_cases (yhd < xhd)
+      by_cases (xhd = yhd)
       case pos h₅ =>
-        have h₆ := List.lt.head ytl xtl h₅
+        subst yhd
+        suffices xtl < ytl ∨ ytl < xtl by
+          cases this <;> rename_i h₅
+          · apply h₂ ; clear h₂
+            apply List.Lex.cons ; simp only [lex_lt]
+            exact h₅
+          · apply h₃ ; clear h₃
+            apply List.Lex.cons ; simp only [lex_lt]
+            exact h₅
+        apply List.lt_conn (xs := xtl) (ys := ytl)
+        intro h₅
+        subst ytl
         contradiction
       case neg h₅ =>
-        have h₆ := StrictLT.if_not_lt_gt_then_eq xhd yhd h₄ h₅
-        subst h₆
-        simp at h₁
-        cases (List.lt_conn h₁) <;> rename_i h₆
-        · have h₇ := List.cons_lt_cons xhd xtl ytl h₆
-          contradiction
-        · have h₇ := List.cons_lt_cons xhd ytl xtl h₆
-          contradiction
-
-instance List.strictLT (α) [LT α] [StrictLT α] : StrictLT (List α) where
-  asymmetric _ _   := List.lt_asymm
+        apply h₃ ; clear h₃
+        apply List.Lex.rel
+        exact StrictLT.if_not_lt_eq_then_gt xhd yhd h₄ h₅
+
+instance List.strictLT (α) [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] : StrictLT (List α) where
+  asymmetric _ _   := List.lt_asymm'
   transitive _ _ _ := List.slt_trans
   connected  _ _   := List.lt_conn
 

cedar-lean/Cedar/Data/List.lean

@@ -29,7 +29,7 @@ open Cedar.Data
 
 ----- Definitions -----
 
-def insertCanonical [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) : List α :=
+def insertCanonical [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x : α) (xs : List α) : List α :=
   match xs with
   | [] => [x]
   | hd :: tl =>
@@ -46,7 +46,7 @@ If the ordering relation < on β is strict, then `canonicalize` returns a
 canonical representation of the input list, which is sorted and free of
 duplicates.
 -/
-def canonicalize [LT β] [DecidableLT β] (f : α → β) : List α → List α
+def canonicalize [LT β] [Cedar.Data.DecidableLT β] (f : α → β) : List α → List α
   | [] => []
   | hd :: tl => insertCanonical f hd (canonicalize f tl)
 

cedar-lean/Cedar/Data/Map.lean

@@ -104,8 +104,8 @@ def mapMOnKeys {α β γ} [LT γ] [DecidableLT γ] [Monad m] (f : α → m γ) (
 instance [LT (Prod α β)] : LT (Map α β) where
   lt a b := a.kvs < b.kvs
 
-instance decLt [LT (Prod α β)] [DecidableRel (α:=(Prod α β)) (·<·)] : (n m : Map α β) → Decidable (n < m)
-  | .mk nkvs, .mk mkvs => List.hasDecidableLt nkvs mkvs
+instance decLt [LT (Prod α β)] [DecidableEq (Prod α β)] [Cedar.Data.DecidableLT (Prod α β)] : (n m : Map α β) → Decidable (n < m)
+  | .mk nkvs, .mk mkvs => List.decidableLT nkvs mkvs
 
 -- enables ∈ notation for map keys
 instance : Membership α (Map α β) where

cedar-lean/Cedar/Data/Set.lean

@@ -124,8 +124,8 @@ def foldl {α β} (f : α → β → α) (init : α) (s : Set β) : α :=
 instance [LT α] : LT (Set α) where
   lt a b := a.elts < b.elts
 
-instance decLt [LT α] [DecidableLT α] : (n m : Set α) → Decidable (n < m)
-  | .mk nelts, .mk melts => List.hasDecidableLt nelts melts
+instance decLt [LT α] [DecidableEq α] [Cedar.Data.DecidableLT α] : (n m : Set α) → Decidable (n < m)
+  | .mk nelts, .mk melts => List.decidableLT nelts melts
 
 -- enables ∅
 instance : EmptyCollection (Set α) where

cedar-lean/Cedar/Data/SizeOf.lean

@@ -40,15 +40,7 @@ theorem sizeOf_lt_of_value [SizeOf α] [SizeOf β] {m : Map α β} {k : α} {v :
   have m1_lt_m : sizeOf m.1 < sizeOf m := by
     simp only [sizeOf, Map._sizeOf_1]
     omega
-  let a := sizeOf v
-  let c := sizeOf m.1
-  let d := sizeOf m
-  have v_lt_m1 : a < c := by apply Nat.lt_trans v_lt_kv h
-  have v_lt_m : a < d := by apply Nat.lt_trans v_lt_m1 m1_lt_m
-  have ha : a = sizeOf v := by simp
-  have hd : d = sizeOf m := by simp
-  rw [ha, hd] at v_lt_m
-  exact v_lt_m
+  omega
 
 theorem sizeOf_lt_of_kvs [SizeOf α] [SizeOf β] (m : Map α β) :
   sizeOf m.kvs < sizeOf m
@@ -66,9 +58,6 @@ theorem sizeOf_lt_of_tl [SizeOf α] [SizeOf β] {m : Map α β} {tl : List (α 
   simp only
   unfold kvs at h
   simp only [h, List.cons.sizeOf_spec, Prod.mk.sizeOf_spec]
-  generalize sizeOf k = kn
-  generalize sizeOf v = vn
-  generalize sizeOf tl = tn
   omega
 
 end Cedar.Data.Map

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

@@ -306,7 +306,7 @@ theorem Except.isOk_iff_exists {x : Except ε α} :
 := by
   cases x <;> simp [Except.isOk, Except.toBool]
 
-theorem if_mapM_doesn't_fail_on_list_then_doesn't_fail_on_set [LT α] [DecidableLT α] [StrictLT α] {f : α → Except ε β} {as : List α} :
+theorem if_mapM_doesn't_fail_on_list_then_doesn't_fail_on_set [LT α] [Cedar.Data.DecidableLT α] [StrictLT α] {f : α → Except ε β} {as : List α} :
   Except.isOk (as.mapM f) →
   Except.isOk ((Set.elts (Set.make as)).mapM f)
 := by

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

@@ -164,13 +164,16 @@ instance Ext.strictLT : StrictLT Ext where
 
 instance Name.strictLT : StrictLT Name where
   asymmetric a b   := by
-    simp [LT.lt, Name.lt]
-    apply List.lt_asymm
+    simp only [LT.lt, Bool.not_eq_true]
+    simp only [Name.lt, decide_eq_true_eq, decide_eq_false_iff_not, List.not_lt]
+    apply List.lt_asymm'
   transitive a b c := by
-    simp [LT.lt, Name.lt]
+    simp only [LT.lt]
+    simp only [Name.lt, decide_eq_true_eq]
     apply List.slt_trans
   connected  a b   := by
-    simp [LT.lt, Name.lt]
+    simp only [ne_eq, LT.lt]
+    simp only [Name.lt, decide_eq_true_eq]
     intro h₁
     apply List.lt_conn
     by_contra h₂
@@ -203,24 +206,22 @@ theorem EntityUID.lt_asymm {a b : EntityUID} :
 theorem EntityUID.lt_trans {a b c : EntityUID} :
   a < b → b < c → a < c
 := by
-  simp [LT.lt, EntityUID.lt]
+  simp only [LT.lt]
+  simp only [EntityUID.lt, Bool.decide_or, Bool.decide_and, Bool.or_eq_true, decide_eq_true_eq,
+    Bool.and_eq_true]
   intro h₁ h₂
   rcases h₁ with h₁ | h₁ <;> rcases h₂ with h₂ | h₂
-  · have h₃ := Name.strictLT.transitive a.ty b.ty c.ty h₁ h₂
-    simp only [LT.lt] at h₃
-    simp [h₃]
-  · have ⟨h₂, _⟩ := h₂
+  · simp [Name.strictLT.transitive a.ty b.ty c.ty h₁ h₂]
+  · replace ⟨h₂, _⟩ := h₂
     simp [h₂] at h₁
     simp [h₁]
-  · have ⟨h₁, _⟩ := h₁
+  · replace ⟨h₁, _⟩ := h₁
     simp [←h₁] at h₂
     simp [h₂]
-  · have ⟨hl₁, hr₁⟩ := h₁
-    have ⟨hl₂, hr₂⟩ := h₂
+  · replace ⟨hl₁, hr₁⟩ := h₁ ; clear h₁
+    replace ⟨hl₂, hr₂⟩ := h₂ ; clear h₂
     simp [hl₁] at * ; simp [hl₂] at *
-    have h₃ := String.strictLT.transitive a.eid b.eid c.eid hr₁ hr₂
-    simp only [LT.lt] at h₃
-    simp [h₃]
+    simp [String.strictLT.transitive a.eid b.eid c.eid hr₁ hr₂]
 
 theorem EntityUID.lt_conn {a b : EntityUID} :
   a ≠ b → (a < b ∨ b < a)
@@ -387,7 +388,8 @@ theorem ValueAttrs.lt_asym {vs₁ vs₂: List (Attr × Value)} :
       have h₂ := String.strictLT.asymmetric a₁ a₂ h₁
       have h₃ := StrictLT.not_eq a₁ a₂ h₁
       rw [eq_comm] at h₃
-      simp [h₂, h₃]
+      simp only [h₃, false_implies, and_true, ge_iff_le]
+      simp_all only [String.not_lt]
     case inr =>
       have ⟨hl₁, h₂⟩ := h₁
       subst hl₁

cedar-lean/Cedar/Thm/Data/List/Basic.lean

@@ -294,7 +294,7 @@ theorem sortedBy_cons [LT β] [StrictLT β] {f : α → β} {x : α} {ys : List
     apply h₂
     simp only [mem_cons, true_or]
 
-theorem mem_of_sortedBy_unique {α β} [LT β] [StrictLT β] [DecidableLT β] [DecidableEq β]
+theorem mem_of_sortedBy_unique {α β} [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] [DecidableEq β]
   {f : α → β} {x y : α} {xs : List α} :
   xs.SortedBy f → x ∈ xs → y ∈ xs → f x = f y →
   x = y
@@ -317,7 +317,7 @@ theorem mem_of_sortedBy_unique {α β} [LT β] [StrictLT β] [DecidableLT β] [D
       simp only [hf, StrictLT.irreflexive] at hlt
     · exact ih hx hy
 
-theorem mem_of_sortedBy_implies_find? {α β} [LT β] [StrictLT β] [DecidableLT β] [DecidableEq β]
+theorem mem_of_sortedBy_implies_find? {α β} [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] [DecidableEq β]
   {f : α → β} {x : α} {xs : List α} :
   x ∈ xs → xs.SortedBy f →
   xs.find? (fun y => f y == f x) = x
@@ -384,7 +384,7 @@ theorem map_eq_implies_sortedBy [LT β] [StrictLT β] {f : α → β} {g : γ 
           apply sortedBy_implies_head_lt_tail h₂
           simp only [mem_cons, true_or]
 
-theorem filter_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} (p : α → Bool) {xs : List α} :
+theorem filter_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} (p : α → Bool) {xs : List α} :
   SortedBy f xs → SortedBy f (xs.filter p)
 := by
   intro h₁
@@ -401,7 +401,7 @@ theorem filter_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} (
       exact h₂.left
     · exact ih
 
-theorem filterMap_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} {g : α → Option γ} {f' : γ → β} {xs : List α} :
+theorem filterMap_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} {g : α → Option γ} {f' : γ → β} {xs : List α} :
   (∀ x y, g x = some y → f x = f' y) →
   SortedBy f xs →
   SortedBy f' (xs.filterMap g)