Upgrade to lean 4.15 (#512)

Signed-off-by: Emina Torlak <[email protected]>
Co-authored-by: Emina Torlak <[email protected]>

cedar-lean/Cedar/Data/LT.lean

@@ -77,7 +77,7 @@ theorem List.cons_lt_cons [LT α] [StrictLT α] (x : α) (xs ys : List α) :
   intro h₁
   apply List.lt.tail (StrictLT.irreflexive x) (StrictLT.irreflexive x) h₁
 
-theorem List.lt_irrefl [LT α] [StrictLT α] (xs : List α) :
+theorem List.slt_irrefl [LT α] [StrictLT α] (xs : List α) :
   ¬ xs < xs
 := by
   induction xs
@@ -95,7 +95,7 @@ theorem List.lt_irrefl [LT α] [StrictLT α] (xs : List α) :
       simp [h₂] at h₃
       contradiction
 
-theorem List.lt_trans [LT α] [StrictLT α] {xs ys zs : List α} :
+theorem List.slt_trans [LT α] [StrictLT α] {xs ys zs : List α} :
   xs < ys → ys < zs → xs < zs
 := by
   intro h₁ h₂
@@ -122,7 +122,7 @@ theorem List.lt_trans [LT α] [StrictLT α] {xs ys zs : List α} :
       have h₉ := StrictLT.if_not_lt_gt_then_eq xhd yhd h₃ h₄
       subst h₉
       apply List.lt.tail h₆ h₇
-      apply List.lt_trans h₅ h₈
+      apply List.slt_trans h₅ h₈
 
 theorem List.lt_asymm [LT α] [StrictLT α] {xs ys : List α} :
   xs < ys → ¬ ys < xs
@@ -137,8 +137,8 @@ theorem List.lt_asymm [LT α] [StrictLT α] {xs ys : List α} :
     case nil => contradiction
     case cons _ _ hd' tl' =>
       by_contra h₂
-      have h₃ := List.lt_trans h₁ h₂
-      have h₄ := List.lt_irrefl (hd :: tl)
+      have h₃ := List.slt_trans h₁ h₂
+      have h₄ := List.slt_irrefl (hd :: tl)
       contradiction
 
 theorem List.lt_conn [LT α] [StrictLT α] {xs ys : List α} :
@@ -178,7 +178,7 @@ theorem List.lt_conn [LT α] [StrictLT α] {xs ys : List α} :
 
 instance List.strictLT (α) [LT α] [StrictLT α] : StrictLT (List α) where
   asymmetric _ _   := List.lt_asymm
-  transitive _ _ _ := List.lt_trans
+  transitive _ _ _ := List.slt_trans
   connected  _ _   := List.lt_conn
 
 def Bool.lt (a b : Bool) : Bool := match a,b with
@@ -217,13 +217,18 @@ instance Int.strictLT : StrictLT Int where
   connected  a b   := by omega
 
 theorem UInt32.lt_iff {x y : UInt32} : x < y ↔ x.1.1 < y.1.1 := by
-  cases x; cases y; simp only [LT.lt]
+  cases x
+  cases y
+  simp only [LT.lt, Nat.lt, Nat.succ_eq_add_one, Nat.le_eq,
+    Nat.reducePow, BitVec.val_toFin]
+
 
 instance UInt32.strictLT : StrictLT UInt32 where
   asymmetric a b   := by apply Nat.strictLT.asymmetric
   transitive a b c := by apply Nat.strictLT.transitive
   connected  a b   := by
-    simp [UInt32.lt_iff, UInt32.ext_iff]
+    simp only [ne_eq, UInt32.ext_iff, LT.lt, Nat.lt,
+      toNat_toBitVec_eq_toNat, Nat.succ_eq_add_one, Nat.le_eq]
     omega
 
 instance Char.strictLT : StrictLT Char where

cedar-lean/Cedar/Spec/Evaluator.lean

@@ -26,7 +26,7 @@ namespace Cedar.Spec
 open Cedar.Data
 open Error
 
-def intOrErr : Option Int64 → Result Value
+def intOrErr : Option Data.Int64 → Result Value
   | .some i => .ok (.prim (.int i))
   | .none   => .error .arithBoundsError
 

cedar-lean/Cedar/Spec/Ext/Datetime.lean

@@ -38,7 +38,7 @@ open Cedar.Data
 
   A duration may be negative. Negative duration strings must begin with `-`.
 -/
-abbrev Duration := Int64
+abbrev Duration := Data.Int64
 
 namespace Datetime
 

cedar-lean/Cedar/Spec/Ext/Decimal.lean

@@ -32,7 +32,7 @@ We restrict the number of the digits after the decimal point to 4.
 
 def DECIMAL_DIGITS : Nat := 4
 
-abbrev Decimal := Int64
+abbrev Decimal := Data.Int64
 
 namespace Decimal
 

cedar-lean/Cedar/Spec/Ext/IPAddr.lean

@@ -137,7 +137,7 @@ private def parsePrefixNat (str : String) (digits : Nat) (size : Nat) : Option (
   if 0 < len && len ≤ digits && (str.startsWith "0" → str = "0")
   then do
     let n ← str.toNat?
-    if n ≤ size then .some (Fin.ofNat n) else .none
+    if n ≤ size then .some (Fin.ofNat' (size+1) n) else .none
   else .none
 
 private def parseNumV4 (str : String) : Option (BitVec 8) :=

cedar-lean/Cedar/Spec/Value.lean

@@ -49,7 +49,7 @@ structure EntityUID where
 
 inductive Prim where
   | bool (b : Bool)
-  | int (i : Int64)
+  | int (i : Data.Int64)
   | string (s : String)
   | entityUID (uid : EntityUID)
 
@@ -79,7 +79,7 @@ def Value.asString : Value →  Result String
   | .prim (.string s) => .ok s
   | _ => .error Error.typeError
 
-def Value.asInt : Value →  Result Int64
+def Value.asInt : Value →  Result Data.Int64
   | .prim (.int i) => .ok i
   | _ => .error Error.typeError
 
@@ -90,7 +90,7 @@ def Result.as {α} (β) [Coe α (Result β)] : Result α → Result β
 instance : Coe Bool Value where
   coe b := .prim (.bool b)
 
-instance : Coe Int64 Value where
+instance : Coe Data.Int64 Value where
   coe i := .prim (.int i)
 
 instance : Coe String Value where
@@ -114,7 +114,7 @@ instance : Coe (Map Attr Value) Value where
 instance : Coe Value (Result Bool) where
   coe v := v.asBool
 
-instance : Coe Value (Result Int64) where
+instance : Coe Value (Result Data.Int64) where
   coe v := v.asInt
 
 instance : Coe Value (Result String) where

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

@@ -18,7 +18,7 @@ import Cedar.Spec
 import Cedar.Spec.Authorizer
 import Cedar.Thm.Authorization.Slicing
 import Cedar.Thm.Authorization.Evaluator
-import Cedar.Thm.Data.LT
+import Cedar.Thm.Data
 import Cedar.Thm.Validation.Typechecker.BinaryApp -- mapM'_asEntityUID_eq_entities
 
 /-!
@@ -181,12 +181,12 @@ theorem alternate_errorPolicies_equiv_errorPolicies (policies : Policies) (reque
     intro pid p h₁ h₂
     exists p
     unfold errored hasError at h₂
-    split at h₂ <;> rename_i h₃
-    · unfold hasError
-      apply And.intro
-      · simp [h₃, h₁, List.mem_filter]
-      · simp at h₂; exact h₂
-    · contradiction
+    split at h₂ <;>
+    simp only [Bool.false_eq_true, ↓reduceIte, reduceCtorEq, Option.some.injEq] at h₂ <;>
+    rename_i h₃
+    unfold hasError
+    apply And.intro _ h₂
+    simp only [h₁, h₃, and_self]
   case right =>
     intro pid p h₁ h₂ h₃
     exists p

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

@@ -54,18 +54,21 @@ theorem and_true_implies_right_true {e₁ e₂ : Expr} {request : Request} {enti
 := by
   intro h₁
   have h₂ := and_true_implies_left_true h₁
-  simp [evaluate, h₂, Result.as, Coe.coe, Value.asBool] at h₁
+  simp only [evaluate, Result.as, h₂, Coe.coe, Value.asBool, Bool.not_eq_eq_eq_not, Bool.not_true,
+    bind_pure_comp, Except.bind_ok, Bool.true_eq_false, ↓reduceIte] at h₁
   generalize h₃ : (evaluate e₂ request entities) = r₂
-  simp [h₃] at h₁
-  cases r₂ <;> simp only [Except.bind_err, reduceCtorEq] at h₁
+  simp only [h₃] at h₁
+  cases r₂
+  case error => simp only [Except.map_error, reduceCtorEq] at h₁
   case ok v₂ =>
-    cases v₂ <;> try simp only [Except.bind_err, reduceCtorEq] at h₁
+    cases v₂ <;> try simp only [Except.map_error, reduceCtorEq] at h₁
     case _ p₂ =>
-      cases p₂ <;> simp only [Except.bind_ok, Except.bind_err, reduceCtorEq] at h₁
-      case _ b =>
+      cases p₂ <;> simp only [Except.map_error, Except.bind_ok, Except.bind_err, reduceCtorEq] at h₁
+      case bool b =>
         cases b
         case false =>
-          simp only [pure, Except.pure, Except.ok.injEq, Value.prim.injEq, Prim.bool.injEq, reduceCtorEq] at h₁
+          simp only [Except.map_ok, Except.ok.injEq, Value.prim.injEq, Prim.bool.injEq,
+            Bool.false_eq_true] at h₁
         case true => rfl
 
 /- some shorthand to make things easier to read and write -/
@@ -124,8 +127,8 @@ theorem ways_and_can_error {e₁ e₂ : Expr} {request : Request} {entities : En
               simp [h_e₂] at h₁ <;>
               simp [h₁]
           | error e =>
-            simp only [h_e₂, ↓reduceIte, Except.bind_err, Except.error.injEq] at h₁
-            simp [h₁]
+            simp only [↓reduceIte, h_e₂, Except.map_error, Except.error.injEq] at h₁
+            simp only [h₁, and_false, or_false]
         | false => simp [h_e₁] at h₁
   case error e =>
     simp [h_e₁, evaluate, Result.as, Coe.coe, Value.asBool] at h₁

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

@@ -41,22 +41,22 @@ instance IPNetPrefix.strictLT {w} : StrictLT (Ext.IPAddr.IPNetPrefix w) where
     simp only [LT.lt]
     unfold Ext.IPAddr.IPNetPrefix.lt Ext.IPAddr.IPNetPrefix.toNat Ext.IPAddr.ADDR_SIZE
     cases a <;> cases b <;>
-    simp only [Nat.lt_irrefl, decide_False, not_false_eq_true,
+    simp only [Nat.lt_irrefl, decide_false, not_false_eq_true,
       false_implies, decide_eq_true_eq, Nat.not_lt, reduceCtorEq]
     all_goals { omega }
   transitive a b c := by
     simp only [LT.lt]
     unfold Ext.IPAddr.IPNetPrefix.lt Ext.IPAddr.IPNetPrefix.toNat Ext.IPAddr.ADDR_SIZE
     cases a <;> cases b <;> cases c <;>
-    simp only [Nat.lt_irrefl, decide_False, imp_self,
+    simp only [Nat.lt_irrefl, decide_false, imp_self,
       decide_eq_true_eq, false_implies, implies_true]
     all_goals { omega }
   connected  a b   := by
     simp only [LT.lt]
     unfold Ext.IPAddr.IPNetPrefix.lt Ext.IPAddr.IPNetPrefix.toNat Ext.IPAddr.ADDR_SIZE
     cases a <;> cases b <;>
     simp only [ne_eq, not_true_eq_false, Nat.lt_irrefl, decide_eq_true_eq,
-      decide_False, or_self, imp_self, not_false_eq_true, forall_const, Option.some.injEq, reduceCtorEq]
+      decide_false, or_self, imp_self, not_false_eq_true, forall_const, Option.some.injEq, reduceCtorEq]
     · apply Or.inr ; omega
     · apply Or.inl ; omega
     · bv_omega
@@ -133,9 +133,9 @@ instance Ext.strictLT : StrictLT Ext where
     cases a <;> cases b <;> simp [LT.lt, Ext.lt] <;>
     rename_i x₁ x₂ <;> intro h₁
     case decimal =>
-      have h₂ := Int64.strictLT.asymmetric x₁ x₂
+      have h₂ := Data.Int64.strictLT.asymmetric x₁ x₂
       simp [LT.lt] at h₂
-      cases h₃ : Int64.lt x₁ x₂ <;>
+      cases h₃ : Data.Int64.lt x₁ x₂ <;>
       simp [h₃] at h₁ h₂ ; simp [h₂]
     case ipaddr =>
       have h₂ := IPNet.strictLT.asymmetric x₁ x₂
@@ -146,10 +146,10 @@ instance Ext.strictLT : StrictLT Ext where
     cases a <;> cases b <;> cases c <;> simp [LT.lt, Ext.lt] <;>
     rename_i x₁ x₂ x₃ <;> intro h₁ h₂
     case decimal =>
-      have h₃ := Int64.strictLT.transitive x₁ x₂ x₃
+      have h₃ := Data.Int64.strictLT.transitive x₁ x₂ x₃
       simp [LT.lt] at h₃
-      cases h₄ : Int64.lt x₁ x₂ <;> simp [h₄] at *
-      cases h₅ : Int64.lt x₂ x₃ <;> simp [h₅] at *
+      cases h₄ : Data.Int64.lt x₁ x₂ <;> simp [h₄] at *
+      cases h₅ : Data.Int64.lt x₂ x₃ <;> simp [h₅] at *
       simp [h₃]
     case ipaddr =>
       have h₃ := IPNet.strictLT.transitive x₁ x₂ x₃
@@ -161,7 +161,7 @@ instance Ext.strictLT : StrictLT Ext where
     cases a <;> cases b <;> simp [LT.lt, Ext.lt] <;>
     rename_i x₁ x₂ <;> intro h₁
     case decimal =>
-      have h₂ := Int64.strictLT.connected x₁ x₂
+      have h₂ := Data.Int64.strictLT.connected x₁ x₂
       simp [LT.lt, h₁] at h₂
       rcases h₂ with h₂ | h₂ <;> simp [h₂]
     case ipaddr =>
@@ -177,7 +177,7 @@ instance Name.strictLT : StrictLT Name where
     apply List.lt_asymm
   transitive a b c := by
     simp [LT.lt, Name.lt]
-    apply List.lt_trans
+    apply List.slt_trans
   connected  a b   := by
     simp [LT.lt, Name.lt]
     intro h₁
@@ -261,7 +261,7 @@ theorem Prim.lt_asymm {a b : Prim} :
   cases a <;> cases b <;> simp [LT.lt] <;>
   simp [Prim.lt]
   case bool b₁ b₂          => exact Bool.strictLT.asymmetric b₁ b₂
-  case int i₁ i₂           => exact (Int64.strictLT.asymmetric i₁ i₂)
+  case int i₁ i₂           => exact (Data.Int64.strictLT.asymmetric i₁ i₂)
   case string s₁ s₂        => exact (String.strictLT.asymmetric s₁ s₂)
   case entityUID uid₁ uid₂ => exact (EntityUID.strictLT.asymmetric uid₁ uid₂)
 
@@ -271,7 +271,7 @@ theorem Prim.lt_trans {a b c : Prim} :
   cases a <;> cases b <;> cases c <;> simp [LT.lt] <;>
   simp [Prim.lt]
   case bool b₁ b₂ b₃            => exact (Bool.strictLT.transitive b₁ b₂ b₃)
-  case int i₁ i₂ i₃             => exact (Int64.strictLT.transitive i₁ i₂ i₃)
+  case int i₁ i₂ i₃             => exact (Data.Int64.strictLT.transitive i₁ i₂ i₃)
   case string s₁ s₂ s₃          => exact (String.strictLT.transitive s₁ s₂ s₃)
   case entityUID uid₁ uid₂ uid₃ => exact (EntityUID.strictLT.transitive uid₁ uid₂ uid₃)
 
@@ -281,7 +281,7 @@ theorem Prim.lt_conn {a b : Prim} :
   cases a <;> cases b <;> simp [LT.lt] <;>
   simp [Prim.lt]
   case bool b₁ b₂          => exact (Bool.strictLT.connected b₁ b₂)
-  case int i₁ i₂           => exact (Int64.strictLT.connected i₁ i₂)
+  case int i₁ i₂           => exact (Data.Int64.strictLT.connected i₁ i₂)
   case string s₁ s₂        => exact (String.strictLT.connected s₁ s₂)
   case entityUID uid₁ uid₂ => exact (EntityUID.strictLT.connected uid₁ uid₂)
 
@@ -316,7 +316,7 @@ theorem Values.lt_irrefl (vs : List Value) :
   cases vs
   case nil => simp only [Values.lt, Bool.false_eq_true, not_false_eq_true]
   case cons hd tl =>
-    simp only [Values.lt, decide_True, Bool.true_and, Bool.or_eq_true, not_or, Bool.not_eq_true]
+    simp only [Values.lt, decide_true, Bool.true_and, Bool.or_eq_true, not_or, Bool.not_eq_true]
     simp only [Value.lt_irrefl hd, Values.lt_irrefl tl, and_self]
 termination_by sizeOf vs
 decreasing_by
@@ -329,7 +329,7 @@ theorem ValueAttrs.lt_irrefl (vs : List (Attr × Value)) :
   case nil => simp only [ValueAttrs.lt, Bool.false_eq_true, not_false_eq_true]
   case cons hd tl =>
     replace (a, v) := hd
-    simp only [ValueAttrs.lt, String.lt_irrefl, decide_False, decide_True, Bool.true_and,
+    simp only [ValueAttrs.lt, String.lt_irrefl, decide_false, decide_true, Bool.true_and,
       Bool.false_or, Bool.and_self, Bool.or_eq_true, not_or, Bool.not_eq_true]
     simp only [Value.lt_irrefl v, ValueAttrs.lt_irrefl tl, and_self]
 termination_by sizeOf vs
@@ -400,7 +400,7 @@ theorem ValueAttrs.lt_asym {vs₁ vs₂: List (Attr × Value)} :
     case inr =>
       have ⟨hl₁, h₂⟩ := h₁
       subst hl₁
-      simp only [decide_True, Bool.true_and]
+      simp only [decide_true, Bool.true_and]
       have h₃ := Value.lt_asymm h₂
       simp [LT.lt] at h₃ ; simp [h₃]
       have h₄ := StrictLT.irreflexive a₁
@@ -411,7 +411,7 @@ theorem ValueAttrs.lt_asym {vs₁ vs₂: List (Attr × Value)} :
     have ⟨h₂, h₃⟩ := h₁
     have ⟨hl₂, hr₂⟩ := h₂
     subst hl₂ hr₂
-    simp only [decide_True, Bool.true_and, Bool.and_self]
+    simp only [decide_true, Bool.true_and, Bool.and_self]
     have h₃ := ValueAttrs.lt_asym h₃
     have h₄ := StrictLT.irreflexive a₁
     have h₅ := Value.lt_irrefl v₁

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

@@ -354,7 +354,7 @@ theorem map_eq_implies_sortedBy [LT β] [StrictLT β] {f : α → β} {g : γ 
     case cons.cons xhd xtl yhd ytl =>
       replace ⟨h₁, h₃⟩ := h₁
       have ih := map_eq_implies_sortedBy h₃
-      cases ytl <;> simp only [map_nil, map_cons, map_eq_nil] at *
+      cases ytl <;> simp only [map_nil, map_cons, map_eq_nil_iff] at *
       case nil => exact SortedBy.cons_nil
       case cons yhd' ytl =>
         simp only [tail_sortedBy h₂, true_iff] at ih
@@ -372,7 +372,7 @@ theorem map_eq_implies_sortedBy [LT β] [StrictLT β] {f : α → β} {g : γ 
     case cons.cons xhd xtl yhd ytl =>
       replace ⟨h₁, h₃⟩ := h₁
       have ih := map_eq_implies_sortedBy h₃
-      cases xtl <;> simp only [map_nil, map_cons, map_eq_nil] at *
+      cases xtl <;> simp only [map_nil, map_cons, map_eq_nil_iff] at *
       case nil => exact SortedBy.cons_nil
       case cons xhd' xtl =>
         simp only [tail_sortedBy h₂, iff_true] at ih