update to Lean 4.9 (#421)

Signed-off-by: Craig Disselkoen <[email protected]>

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

@@ -60,7 +60,7 @@ abbrev IPv4Prefix := IPNetPrefix V4_WIDTH
 abbrev IPv6Prefix := IPNetPrefix V6_WIDTH
 
 def IPNetPrefix.ofNat (w : Nat) (pre : Nat) : IPNetPrefix w :=
-  if pre < ADDR_SIZE w then .some pre#w else .none
+  if pre < ADDR_SIZE w then .some pre else .none
 
 def IPNetPrefix.toNat {w} : IPNetPrefix w → Nat
   | .none         => ADDR_SIZE w
@@ -83,7 +83,7 @@ def CIDR.subnetWidth {w} (cidr : CIDR w) : BitVec (ADDR_SIZE w) :=
   let n := ADDR_SIZE w
   match cidr.pre with
   | .none            => 0#n
-  | .some prefixSize => n#n - (prefixSize.zeroExtend n)
+  | .some prefixSize => n - (prefixSize.zeroExtend n)
 
 def CIDR.range {w} (cidr : CIDR w) : (IPNetAddr w) × (IPNetAddr w) :=
   let n := ADDR_SIZE w
@@ -145,7 +145,7 @@ private def parseNumV4 (str : String) : Option (BitVec 8) :=
   if 0 < len && len ≤ 3 && (str.startsWith "0" → str = "0")
   then do
     let n ← str.toNat?
-    if n ≤ 0xff then .some n#8 else .none
+    if n ≤ 0xff then .some n else .none
   else .none
 
 private def parseSegsV4 (str : String) : Option IPv4Addr :=
@@ -187,7 +187,7 @@ private def parseNumV6 (str : String) : Option (BitVec 16) :=
   if 0 < len && len ≤ 4 && str.all isHexDigit
   then
     let n := str.foldl (fun n c => n * 16 + toHexNat c) 0
-    if n ≤ 0xffff then .some n#16 else .none
+    if n ≤ 0xffff then .some n else .none
   else .none
 
 private def parseNumSegsV6 (str : String) : Option (List (BitVec 16)) :=

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

@@ -47,6 +47,11 @@ notation together with `Except` and `Option`.
   (bind Option.none f : Option β) = Option.none
 := by rfl
 
+theorem do_some {opt : Option α} {f : α → β} :
+  (do let v ← opt ; some (f v)) = some b ↔
+  ∃ a, opt = some a ∧ f a = b
+:= by cases opt <;> simp
+
 theorem do_error {res : Except ε α} {e : ε} {f : α → β} :
   (do let v ← res ; .ok (f v)) = .error e ↔
   res = .error e

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

@@ -58,7 +58,7 @@ theorem insertCanonical_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α
     split <;> rename_i h₂
     · exact SortedBy.cons_cons h₂ h₁
     · split
-      case inl h₃ =>
+      case isTrue h₃ =>
         cases h₁
         case cons_nil =>
           apply SortedBy.cons_cons h₃
@@ -79,12 +79,11 @@ theorem insertCanonical_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α
               case cons_nil => exact SortedBy.cons_nil
               case cons_cons z zs h₉ h₁₀ =>
                 exact SortedBy.cons_cons (by simp [h₈, h₁₀]) h₉
-      case inr h₃ =>
+      case isFalse h₃ =>
         have h₄ := StrictLT.if_not_lt_gt_then_eq (f x) (f hd) h₂ h₃
         cases h₁
         case cons_nil => exact SortedBy.cons_nil
-        case cons_cons h₅ h₆ =>
-          exact SortedBy.cons_cons (by simp only [h₄, h₆]) h₅
+        case cons_cons h₅ h₆ => exact SortedBy.cons_cons (by simp only [h₄, h₆]) h₅
 
 theorem insertCanonical_cases [LT β] [DecidableLT β] (f : α → β) (x y : α) (ys : List α) :
   (f x < f y ∧ insertCanonical f x (y :: ys) = x :: y :: ys) ∨
@@ -127,14 +126,14 @@ theorem insertCanonical_equiv [LT α] [StrictLT α] [DecidableLT α] (x : α) (x
   case cons hd tl ih =>
     simp only [id_eq, gt_iff_lt]
     split
-    case inl => exact Equiv.refl
-    case inr _ _ h₁ =>
+    case isTrue => exact Equiv.refl
+    case isFalse h₁ =>
       split
-      case inr _ _ h₂ =>
+      case isFalse h₂ =>
         have h₃ := StrictLT.if_not_lt_gt_then_eq x hd h₁ h₂
         subst h₃
         exact dup_head_equiv x tl
-      case inl _ _ h₂ =>
+      case isTrue h₂ =>
         cases tl
         case nil =>
           simp only [insertCanonical_singleton id x]

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

@@ -652,7 +652,7 @@ theorem mapMOnValues_some_wf_alt_proof [LT α] [DecidableLT α] [StrictLT α] {f
 := by
   simp only [wf_iff_sorted, toList]
   intro wf h₁
-  simp [mapMOnValues] at h₁
+  simp only [mapMOnValues, Option.pure_def, do_some] at h₁
   replace ⟨xs, h₁, h₂⟩ := h₁
   subst h₂
   simp [kvs]

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

@@ -59,12 +59,12 @@ theorem type_of_and_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : En
     rename_i res₂
     split at h₁ <;> simp at h₁ <;>
     have ⟨hty, hc⟩ := h₁ <;> subst hty hc
-    case inr.ok.h_1 hty₂ =>
+    case isFalse.ok.h_1 hty₂ =>
       exists BoolType.ff, res₂.snd ; simp [←hty₂]
-    case inr.ok.h_2 hty₂ =>
+    case isFalse.ok.h_2 hty₂ =>
       exists BoolType.tt, res₂.snd ; simp [←hty₂, hc₁]
       cases bty₁ <;> simp at h₃ <;> simp [lubBool]
-    case inr.ok.h_3 bty₂ h₄ h₅ hty₂ =>
+    case isFalse.ok.h_3 bty₂ h₄ h₅ hty₂ =>
       exists BoolType.anyBool, res₂.snd
       cases bty₂ <;> simp at *
       simp [←hty₂, hc₁, lubBool]
@@ -87,7 +87,7 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env
   have ⟨b₁, hb₁⟩ := instance_of_bool_is_bool ih₁₃
   subst hb₁
   split at h₅
-  case inl h₆ =>
+  case isTrue h₆ =>
     subst h₆
     have ⟨hty, hc⟩ := h₅
     subst hty hc
@@ -99,10 +99,10 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env
     simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool] <;>
     try exact type_is_inhabited (CedarType.bool BoolType.ff)
     exact false_is_instance_of_ff
-  case inr h₆ =>
+  case isFalse h₆ =>
     have ⟨bty₂, rc₂, hₜ, h₇⟩ := h₅
     split at h₇ <;> have ⟨hty, hc⟩ := h₇ <;> subst hty hc
-    case inl h₈ =>
+    case isTrue h₈ =>
       subst h₈
       apply And.intro empty_guarded_capabilities_invariant
       exists false ; simp [false_is_instance_of_ff]
@@ -124,7 +124,7 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env
         have h₈ := instance_of_ff_is_false ih₂₃
         subst h₈
         simp [CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe, Coe.coe]
-    case inr h₈ =>
+    case isFalse h₈ =>
       cases b₁
       case false =>
         rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;>

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

@@ -114,11 +114,11 @@ theorem type_of_eq_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env :
   split at hty
   case h_1 =>
     split at hty <;> subst hty
-    case inl heq _ _ =>
+    case isTrue heq _ _ =>
       subst heq
       simp [EvaluatesTo, evaluate, apply₂]
       exact true_is_instance_of_tt
-    case inr p₁ p₂ heq _ _ =>
+    case isFalse p₁ p₂ heq _ _ =>
       simp [EvaluatesTo, evaluate, apply₂]
       cases h₃ : Value.prim p₁ == Value.prim p₂ <;>
       simp only [beq_iff_eq, beq_eq_false_iff_ne, ne_eq, Value.prim.injEq] at h₃
@@ -432,31 +432,34 @@ theorem actionUID?_some_implies_action_lit {x : Expr} {euid : EntityUID} {acts :
   replace h₂ := entityUID?_some_implies_entity_lit h₂
   rename_i euid'
   replace ⟨h₀, h₁⟩ := h₁
-  subst h₀
-  simp [h₁, h₂]
+  subst euid'
+  simp [h₀, h₂]
 
 theorem entityUIDs?_some_implies_entity_lits {x : Expr} {euids : List EntityUID}
   (h₁ : entityUIDs? x = some euids) :
   x = Expr.set ((List.map (Expr.lit ∘ Prim.entityUID) euids))
 := by
   simp [entityUIDs?] at h₁
   split at h₁ <;> try simp at h₁
-  rw [←List.mapM'_eq_mapM] at h₁ ; rename_i xs
+  rename_i xs
+  simp [List.mapM_some_iff_forall₂] at *
   cases euids
   case nil =>
-    cases hxs : xs <;> subst xs <;> simp at *
+    cases xs <;> simp only [List.Forall₂.nil, List.map_nil] at *
+    case cons hd tl => simp only [List.forall₂_nil_right_iff] at h₁
   case cons hd tl =>
-    cases hxs : xs <;> subst xs <;> simp [pure, Except.pure] at *
-    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₁ ; 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₃
-    have h₄ := @entityUIDs?_some_implies_entity_lits (.set tl') tl
-    simp [entityUIDs?, h₃] at h₄
-    exact h₄
+    cases xs <;> simp [pure, Except.pure] at *
+    case nil => simp only [List.forall₂_nil_left_iff] at h₁
+    case cons hd' tl' =>
+      cases h₂ : entityUID? hd' <;> simp [h₂] at h₁
+      replace ⟨h₁', h₁⟩ := h₁
+      replace h₂ := entityUID?_some_implies_entity_lit h₂
+      subst hd hd'
+      simp only [true_and]
+      have h₄ := @entityUIDs?_some_implies_entity_lits (.set tl') tl
+      simp [entityUIDs?] at h₄
+      apply h₄ ; clear h₄
+      simp only [List.mapM_some_iff_forall₂, h₁]
 
 theorem entity_type_in_false_implies_inₑ_false {euid₁ euid₂ : EntityUID} {env : Environment} {entities : Entities}
   (h₁ : InstanceOfEntitySchema entities env.ets)

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

@@ -74,11 +74,11 @@ theorem type_of_hasAttr_is_sound_for_records {x₁ : Expr} {a : Attr} {c₁ c₁
     cases h₆ : (Map.contains r a) <;> simp
     rename_i h₇ _
     cases h₇
-    case inl.h₁.false.inl _ h₇ =>
+    case isTrue.h₁.false.inl _ h₇ =>
       simp [CapabilitiesInvariant] at h₁
       specialize h₁ x₁ a h₇
       simp [EvaluatesTo, evaluate, h₄, hasAttr, attrsOf, h₆] at h₁
-    case inl.h₁.false.inr h₇ _ h₈ =>
+    case isTrue.h₁.false.inr h₇ _ h₈ =>
       simp [Qualified.isRequired] at h₈
       split at h₈ <;> simp at h₈
       have h₉ := required_attribute_is_present h₅ h₇

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

@@ -192,7 +192,7 @@ theorem lub_comm {ty₁ ty₂ : CedarType} :
   case h_4 =>
     rename_i h₁ h₂ h₃
     split <;> split <;> rename_i h₄
-    case inl.h_4 | inr.h_4 =>
+    case isTrue.h_4 | isFalse.h_4 =>
       rename_i _ _ h₅ _ _ _ _
       rw [eq_comm] at h₅
       simp [h₅]
@@ -306,8 +306,8 @@ theorem lub_trans {ty₁ ty₂ ty₃ : CedarType} :
     simp [h₅]
   case h_4 =>
     split
-    case inl h₃ => simp [h₃]
-    case inr h₃ h₄ h₅ h₆ =>
+    case isTrue h₃ => simp [h₃]
+    case isFalse h₃ h₄ h₅ h₆ =>
       unfold lub? at h₁ h₂
       cases ty₁ <;> cases ty₂ <;> simp at h₁ <;>
       cases ty₃ <;> simp at h₂ <;> simp at h₆

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

@@ -98,7 +98,7 @@ theorem type_of_or_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env :
   have ⟨ih₁₁, v₁, ih₁₂, ih₁₃⟩ := ih₁
   have ⟨b₁, hb₁⟩ := instance_of_bool_is_bool ih₁₃ ; subst hb₁
   split at h₅
-  case inl h₆ =>
+  case isTrue h₆ =>
     subst h₆
     have ⟨hty, hc⟩ := h₅ ; subst hty hc
     apply And.intro empty_guarded_capabilities_invariant
@@ -109,7 +109,7 @@ theorem type_of_or_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env :
     simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool] <;>
     try exact type_is_inhabited (CedarType.bool BoolType.tt)
     exact true_is_instance_of_tt
-  case inr =>
+  case isFalse =>
     have ⟨bty₂, rc₂, h₅', h₇⟩ := h₅
     specialize ih₂ h₁ h₂ h₅'
     have ⟨ih₂₁, v₂, ih₂₂, ih₂₃⟩ := ih₂

cedar-lean/UnitTest/Decimal.lean

@@ -23,14 +23,14 @@ namespace UnitTest.Decimal
 
 open Cedar.Spec.Ext.Decimal
 
-theorem test1 : toString ((parse "3.14").get!) = "3.1400" := by decide
-theorem test2 : toString ((parse "11.0003").get!) = "11.0003" := by decide
-theorem test3 : toString ((parse "11.003").get!) = "11.0030" := by decide
-theorem test4 : toString ((parse "11.3000").get!) = "11.3000" := by decide
-theorem test5 : toString ((parse "123.0").get!) = "123.0000" := by decide
-theorem test6 : toString ((parse "-123.0").get!) = "-123.0000" := by decide
-theorem test7 : toString ((parse "-3.14").get!) = "-3.1400" := by decide
-theorem test8 : toString ((parse "-11.0003").get!) = "-11.0003" := by decide
+theorem test1 : toString ((parse "3.14").get!) = "3.1400" := by native_decide
+theorem test2 : toString ((parse "11.0003").get!) = "11.0003" := by native_decide
+theorem test3 : toString ((parse "11.003").get!) = "11.0030" := by native_decide
+theorem test4 : toString ((parse "11.3000").get!) = "11.3000" := by native_decide
+theorem test5 : toString ((parse "123.0").get!) = "123.0000" := by native_decide
+theorem test6 : toString ((parse "-123.0").get!) = "-123.0000" := by native_decide
+theorem test7 : toString ((parse "-3.14").get!) = "-3.1400" := by native_decide
+theorem test8 : toString ((parse "-11.0003").get!) = "-11.0003" := by native_decide
 
 private def testValid (str : String) (rep : Int) : TestCase IO :=
   test str ⟨λ _ => checkEq (parse str) (decimal? rep)⟩

cedar-lean/UnitTest/IPAddr.lean

@@ -23,14 +23,14 @@ namespace UnitTest.IPAddr
 
 open Cedar.Spec.Ext.IPAddr
 
-theorem test1 : toString ((parse "192.168.0.1/32").get!) = "192.168.0.1/32" := by decide
-theorem test2 : toString ((parse "0.0.0.0/1").get!) = "0.0.0.0/1" := by decide
-theorem test3 : toString ((parse "8.8.8.8/24").get!) = "8.8.8.8/24" := by decide
-theorem test4 : toString ((parse "1:2:3:4:a:b:c:d/128").get!) = "0001:0002:0003:0004:000a:000b:000c:000d/128" := by decide
-theorem test5 : toString ((parse "1:22:333:4444:a:bb:ccc:dddd/128").get!) = "0001:0022:0333:4444:000a:00bb:0ccc:dddd/128" := by decide
-theorem test6 : toString ((parse "7:70:700:7000::a00/128").get!) = "0007:0070:0700:7000:0000:0000:0000:0a00/128" := by decide
-theorem test7 : toString ((parse "::ffff/128").get!) = "0000:0000:0000:0000:0000:0000:0000:ffff/128" := by decide
-theorem test8 : toString ((parse "ffff::/4").get!) = "ffff:0000:0000:0000:0000:0000:0000:0000/4" := by decide
+theorem test1 : toString ((parse "192.168.0.1/32").get!) = "192.168.0.1/32" := by native_decide
+theorem test2 : toString ((parse "0.0.0.0/1").get!) = "0.0.0.0/1" := by native_decide
+theorem test3 : toString ((parse "8.8.8.8/24").get!) = "8.8.8.8/24" := by native_decide
+theorem test4 : toString ((parse "1:2:3:4:a:b:c:d/128").get!) = "0001:0002:0003:0004:000a:000b:000c:000d/128" := by native_decide
+theorem test5 : toString ((parse "1:22:333:4444:a:bb:ccc:dddd/128").get!) = "0001:0022:0333:4444:000a:00bb:0ccc:dddd/128" := by native_decide
+theorem test6 : toString ((parse "7:70:700:7000::a00/128").get!) = "0007:0070:0700:7000:0000:0000:0000:0a00/128" := by native_decide
+theorem test7 : toString ((parse "::ffff/128").get!) = "0000:0000:0000:0000:0000:0000:0000:ffff/128" := by native_decide
+theorem test8 : toString ((parse "ffff::/4").get!) = "ffff:0000:0000:0000:0000:0000:0000:0000/4" := by native_decide
 
 private def ipv4 (a₀ a₁ a₂ a₃ : BitVec 8) (pre : Nat) : IPNet :=
   IPNet.V4 ⟨IPv4Addr.mk a₀ a₁ a₂ a₃, pre⟩

cedar-lean/lake-manifest.json

@@ -1,13 +1,13 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "51e6e0d24db9341fb031288c298b7e6b56102253",
+   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0",
+   "inputRev": "v4.9.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Cedar",

cedar-lean/lakefile.lean

@@ -21,7 +21,7 @@ meta if get_config? env = some "dev" then -- dev is so not everyone has to build
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "c7f4ac84b973b6efd8f24ba2b006cad1b32c9c53"
 
 require batteries from git
-  "https://github.com/leanprover-community/batteries" @ "v4.8.0"
+  "https://github.com/leanprover-community/batteries" @ "v4.9.0"
 
 package Cedar
 

cedar-lean/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.9.0