Lean 4.23

8 files changed, 17 insertions, 18 deletions

diff --git a/Common/List.lean b/Common/List.lean
index f6c0de5..9db3b86 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -23,7 +23,7 @@ def quicksortBy {α : Type} (pred : α → α → Bool): List α → List α
   termination_by l => l.length
   decreasing_by
     all_goals
-      simp +arith only [unattach_filter, unattach_attach, length_cons, gt_iff_lt, listFilterSmallerOrEqualList]
+      simp +arith only [unattach_filter, unattach_attach, length_cons, listFilterSmallerOrEqualList]
 
 def quicksort {α : Type} [Ord α] : List α → List α := quicksortBy λ a b ↦ Ord.compare a b == Ordering.lt
 
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index 7834e00..ff54ef0 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -101,7 +101,7 @@ instance [ToString Element] : ToString (MaybeEmptyRectangularGrid Element) where
       r := r.push '\n'
       for h₁ : x in [0:e.width] do
         have : x + e.width *y < e.elements.size := by
-          simp[Membership.mem, inferInstance, Std.instMembershipNatRange] at h₁ h₂
+          simp[Membership.mem] at h₁ h₂
           rw[e.size_valid]
           exact Nat.two_d_coordinate_to_index_lt_size h₁.left h₂.left
         r := r ++ (ToString.toString e.elements[x+e.width*y])
diff --git a/Day10.lean b/Day10.lean
index 6787658..c95ad12 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -266,7 +266,7 @@ private theorem Area.ParseLine_adds_returned_count (previous : Area.Raw) (pos :
       unfold bind Monad.toBind Except.instMonad at h₃
       simp at h₃
       cases h₄ : (Day10.Area.parseLine.parseCharacter line.front)
-      <;> simp[h₄, Option.toExcept, Except.bind] at h₃
+      <;> simp[h₄, Except.bind] at h₃
       case error => rw[←h₃] at h₂; contradiction
       case ok =>
         split at h₃
@@ -318,7 +318,7 @@ private theorem Area.ParseLine_leaves_width_and_height (previous : Area.Raw) (po
       unfold bind Monad.toBind Except.instMonad at h₃
       simp at h₃
       cases h₄ : (Day10.Area.parseLine.parseCharacter line.front)
-      <;> simp[h₄, Option.toExcept, Except.bind] at h₃
+      <;> simp[h₄, Except.bind] at h₃
       case error => rw[←h₃] at h₂; contradiction
       case ok =>
         split at h₃
@@ -448,7 +448,7 @@ private theorem Array.get_push {α : Type u} (arr : Array α) (v : α) (index :
   cases arr
   unfold Array.push getElem Array.instGetElemNatLtSize
   simp only [List.size_toArray] at h₁
-  simp[List.getElem_append, h₁]
+  simp[h₁]
 
 private theorem Area.ParseLine_leaves_start_if_some (previous : Area.Raw) (pos : Nat) (line : Substring) (h₁ : previous.height > 0) {res : (Nat × Area.Raw)} (h₂ : (Area.parseLine previous pos line h₁) = Except.ok res) (h₃ : previous.start.isSome) : Fin.val <$> res.2.start = Fin.val <$> previous.start := by
   unfold Area.parseLine at h₂
@@ -488,7 +488,6 @@ private theorem Area.ParseLine_only_adds_to_fields (previous : Area.Raw) (pos :
           simp at h₅
           rw[←h₅]
           have h₆ : ↑index < (previous.fields.push tile).size := by simp; exact Nat.lt_succ.mpr (Nat.le_of_lt index.isLt)
-          simp[←Array.getElem!_eq_getElem]
           simp[←Array.getElem!_eq_getElem h₆]
           apply Array.get_push
 termination_by previous.width - pos
@@ -682,7 +681,7 @@ private def Area.parse (input : String) : Except Area.ParseError Area :=
         rw[Except.get_unfold']
         exact he
       have sp : vraw.fields[(Coordinate.fromIndex s).toIndex] = Tile.start := by
-        simp[Except.get_unfold' he except_ok] at sp
+        simp at sp
         simp[Coordinate.toIndex_inv_fromIndex]
         rw[Array.getElem!_eq_getElem] at sp ⊢
         have : ((Day10.Except.get (Day10.Area.parseRaw input) _).start.get is_some).val = s.val := by
@@ -1286,13 +1285,13 @@ private theorem Area.PathsPart.join_a_last_last (a b : area.PathsPart) (h₁ : a
   generalize h₂ : (Day10.Area.PathsPart.join area a b h₁) = o
   unfold Area.PathsPart.join at h₂
   split at h₂
-  case h_1 bh ah as _ _ h₄ h₃ _ _ _ _ hb ha _ _ _ _ =>
-    simp[hb, ←h₂, ←ha]
+  case h_1 bh ah as _ _ h₄ h₃ _ _ _ _ _ ha _ _ _ _ =>
+    simp[←h₂, ←ha]
     apply List.getLast_cons
   case h_2 bh b1 bs ah as _ _ h₄ h₃ d4 d3 d2 d1 hb ha d5 d6 d7 d8 =>
     clear d1 d2 d3 d4 d5 d6 d7 d8
     simp only at h₂
-    simp[hb, ←h₂, ←ha]
+    simp[←h₂, ←ha]
     rw[←List.getLast_cons (a := bh) a.list_not_empty]
     have : bs.length + 1 < b.steps.length := by simp only [hb, List.length_cons, Nat.lt_add_one]
     apply Area.PathsPart.join_a_last_last
diff --git a/Day14.lean b/Day14.lean
index f83ece2..c55793e 100644
--- a/Day14.lean
+++ b/Day14.lean
@@ -211,11 +211,11 @@ private def compareControlPanels (a b : ControlPanel) : Bool :=
 
 /-- (Bad) Hash-Function for ControlPanel. It's good enough for this riddle, but that's about it. -/
 private def hashControlPanel (p : ControlPanel) : UInt64 := Id.run do
-  let mut hash : UInt64 := mixHash ⟨Fin.ofNat' UInt64.size p.width⟩ ⟨Fin.ofNat' UInt64.size p.height⟩
+  let mut hash : UInt64 := mixHash ⟨Fin.ofNat UInt64.size p.width⟩ ⟨Fin.ofNat UInt64.size p.height⟩
   for hi : index in [:p.elements.size] do
     match p.elements[index] with
-    | Tile.Round => hash := mixHash hash ⟨Fin.ofNat' UInt64.size index⟩
-    | Tile.Cube => hash := mixHash hash ⟨Fin.ofNat' UInt64.size (index + p.elements.size)⟩
+    | Tile.Round => hash := mixHash hash ⟨Fin.ofNat UInt64.size index⟩
+    | Tile.Cube => hash := mixHash hash ⟨Fin.ofNat UInt64.size (index + p.elements.size)⟩
     | Tile.Space => continue
   hash
 
diff --git a/Day16.lean b/Day16.lean
index abefc51..3777521 100644
--- a/Day16.lean
+++ b/Day16.lean
@@ -300,7 +300,7 @@ private theorem OpticsTable.findFirstExitDirectionNotSeenInQueue_notContains {ta
       have h₂ := Option.some.inj h₁
       subst result
       generalize { x := Fin.cast _ b.snd.x, y := Fin.cast _ b.snd.y : seenDirections.Coordinate } = c at *
-      have h₂ : ed ∈ List.filter (fun d => !seenDirections.toRectangularGrid[c].contains d) (OpticsElement.outputDirections table[b.snd] b.fst) := by simp only [heq, List.mem_singleton, List.mem_cons, true_or]
+      have h₂ : ed ∈ List.filter (fun d => !seenDirections.toRectangularGrid[c].contains d) (OpticsElement.outputDirections table[b.snd] b.fst) := by simp only [heq, List.mem_cons, true_or]
       exact (Bool.not_eq_true' _).mp (List.mem_filter.mp h₂).right
 
 private def OpticsTable.followPath {table : OpticsTable} (seenDirections : SeenExitDirections table) (beams : List (EnterDirection × table.Coordinate)) : SeenExitDirections table :=
diff --git a/Day9.lean b/Day9.lean
index 8fc449c..ac8edd8 100644
--- a/Day9.lean
+++ b/Day9.lean
@@ -31,7 +31,7 @@ private def extrapolate : List Int → Int
     0
   else
     have : (differences (a :: as)).length < as.length + 1 := by
-      simp +arith[differences]
+      simp +arith
       induction (as) <;> simp +arith[differences]
       case cons b bs hb => rw[←differences_length_independent_arg]
                            assumption
diff --git a/lakefile.lean b/lakefile.lean
index e89dba4..3e1521b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -32,7 +32,7 @@ lean_exe «aoc-2023» where
   supportInterpreter := true
 
 require BinaryHeap from git
-  "http://git.grois.info/BinaryHeap"@"ff5c64836ede27d87dbc56b3869021ad8b0d255b"
+  "http://git.grois.info/BinaryHeap"@"90a0fee45356cf5a1a4d29214c7f0f115fddbf23"
 
 require «lean-astar» from git
-  "http://git.grois.info/lean-astar"@"2539ac49ab6af74b31d91e03d7dbfceedc9c1f02"
+  "http://git.grois.info/lean-astar"@"7480e42e0a7ef6631b01fb7208b2b3b9c7fcc354"
diff --git a/lean-toolchain b/lean-toolchain
index 893a7f3..f434439 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.21.0
+leanprover/lean4:4.23.0