update to Lean 4.10 (#423)

Signed-off-by: Craig Disselkoen <cdiss@amazon.com>

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

@@ -1218,21 +1218,21 @@ theorem removeAll_singleton_cons_of_neq [DecidableEq α] (x y : α) (xs : List 
   x ≠ y → (x :: xs).removeAll [y] = x :: (xs.removeAll [y])
 := by
   intro _
-  simp only [removeAll, notElem, elem_eq_mem, mem_singleton, filter_cons, Bool.not_eq_true',
+  simp only [removeAll, elem_eq_mem, mem_singleton, filter_cons, Bool.not_eq_true',
     decide_eq_false_iff_not, ite_not, ite_eq_right_iff]
   intro _
   contradiction
 
 theorem removeAll_singleton_cons_of_eq [DecidableEq α] (x : α) (xs : List α) :
   (x :: xs).removeAll [x] = xs.removeAll [x]
 := by
-  simp only [removeAll, notElem, elem_eq_mem, mem_singleton, decide_True, Bool.not_true,
-    Bool.false_eq_true, not_false_eq_true, filter_cons_of_neg]
+  simp only [removeAll, elem_eq_mem, mem_singleton, decide_True, Bool.not_true, Bool.false_eq_true,
+    not_false_eq_true, filter_cons_of_neg]
 
 theorem mem_removeAll_singleton_of_eq [DecidableEq α] (x : α) (xs : List α) :
   x ∉ xs.removeAll [x]
 := by
-  simp only [removeAll, notElem, elem_eq_mem, mem_singleton]
+  simp only [removeAll, elem_eq_mem, mem_singleton]
   by_contra h
   simp only [mem_filter, decide_True, Bool.not_true, Bool.false_eq_true, and_false] at h
 
@@ -1262,8 +1262,7 @@ theorem removeAll_singleton_equiv [DecidableEq α] (x : α) (xs : List α) :
 theorem length_removeAll_le {α : Type u_1} [BEq α] (xs ys : List α) :
   (xs.removeAll ys).length ≤ xs.length
 := by
-  simp only [List.length_cons, Nat.succ_eq_add_one,
-    List.removeAll, List.notElem, List.elem_eq_mem, List.mem_singleton]
+  simp only [removeAll]
   have _ := List.length_filter_le (fun x => !elem x ys) xs
   omega
 

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

@@ -387,10 +387,10 @@ theorem inter_self_eq {α} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq 
     simp only [List.mem_cons, true_or, decide_True, List.filter_cons_of_pos, List.cons.injEq, true_and]
     rw [eq_comm]
     rw (config := {occs := .pos [1]}) [← ih]
-    rw [List.filter_congr']
-    simp only [decide_eq_true_eq]
+    rw [List.filter_congr]
+    simp only [Bool.decide_or, Bool.iff_or_self, decide_eq_true_eq]
     intro _ h
-    simp only [h, or_true]
+    simp only [h, implies_true]
 
 theorem intersects_def {α} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {s₁ s₂ : Set α} :
  s₁.intersects s₂ = ¬ (s₁ ∩ s₂).isEmpty

cedar-lean/lake-manifest.json

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

cedar-lean/lakefile.lean

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

cedar-lean/lean-toolchain

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