Fix deprecation warnings for Lean 4.13

5 files changed, 27 insertions, 27 deletions

diff --git a/Day12.lean b/Day12.lean
index f679f89..25fd28a 100644
--- a/Day12.lean
+++ b/Day12.lean
@@ -110,7 +110,7 @@ def mustFirstBeDamaged : (states : List SpringState) → Bool
 | .damaged :: _ => true
 | _ => false
 
-abbrev PossiblePositionsMemo := Lean.HashMap (List SpringState × List Nat) Nat
+abbrev PossiblePositionsMemo := Std.HashMap (List SpringState × List Nat) Nat
 
 def countPossiblePositionsWithDamagedMemoized (memo : PossiblePositionsMemo) (remainingSpace : List SpringState) (remainingDamagedGroups : List Nat) (h₁ : remainingDamagedGroups ≠ []) : (PossiblePositionsMemo × Nat) :=
   if h₂ : remainingSpace.isEmpty then
@@ -129,7 +129,7 @@ def countPossiblePositionsWithDamagedMemoized (memo : PossiblePositionsMemo) (re
             let d := (remainingSpace.drop g)
             if canFirstBeOperational d then
               let d := (d.drop 1)
-              if let some r := memo.find? (d, gs) then
+              if let some r := memo.get? (d, gs) then
                 (memo,r)
               else
                 let (memo, r) :=countPossiblePositionsWithDamagedMemoized memo d gs (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h₃)
@@ -144,7 +144,7 @@ def countPossiblePositionsWithDamagedMemoized (memo : PossiblePositionsMemo) (re
           (memo, 0)
         else
           let remainingSpace := (remainingSpace.drop 1)
-          if let some r := memo.find? (remainingSpace, g :: gs) then
+          if let some r := memo.get? (remainingSpace, g :: gs) then
             (memo,r)
           else
             let (memo, r) := countPossiblePositionsWithDamagedMemoized memo remainingSpace (g :: gs) h₁
@@ -162,7 +162,7 @@ def countPossiblePositions (remainingSpace : List SpringState) (remainingDamaged
     else
       0
   else
-    Prod.snd $ countPossiblePositionsWithDamagedMemoized Lean.HashMap.empty remainingSpace remainingDamagedGroups (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h)
+    Prod.snd $ countPossiblePositionsWithDamagedMemoized Std.HashMap.empty remainingSpace remainingDamagedGroups (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h)
 
 
 def part1 (springs : List SpringArrangement) : Nat :=
diff --git a/Day2.lean b/Day2.lean
index 7ed10aa..db85003 100644
--- a/Day2.lean
+++ b/Day2.lean
@@ -71,7 +71,7 @@ def part1 (games : List Game) : Nat :=
 def part2 (games : List Game) : Nat :=
   let powerOfGame := λ (g : Game) ↦
     let minReq := λ (c : Draw Nat → Nat) ↦
-      g.draw.map c |> List.maximum? |> flip Option.getD 0
+      g.draw.map c |> List.max? |> flip Option.getD 0
     minReq Draw.red * minReq Draw.green * minReq Draw.blue
   let powers := games.map powerOfGame
   powers.foldl Nat.add 0
diff --git a/Day3.lean b/Day3.lean
index fbc9e3e..8bf0874 100644
--- a/Day3.lean
+++ b/Day3.lean
@@ -91,7 +91,7 @@ def parse (schematic : String) : Except String Schematic := do
 
 def part1 (schematic : Schematic) : Nat :=
   -- fast lookup: We need to know if a part is at a given coordinate
-  open Lean(HashSet) in
+  open Std(HashSet) in
   let partCoordinates := HashSet.insertMany HashSet.empty $ schematic.parts.map Part.position
   let partNumbers := schematic.numbers.filter λnumber ↦
     number.positions.any λposition ↦
@@ -101,13 +101,13 @@ def part1 (schematic : Schematic) : Nat :=
 def part2 (schematic : Schematic) : Nat :=
   -- and now it is obvious that keeping the parsed input free of opinions was a good idea.
   -- because here we need quick lookup for the numbers, not the parts.
-  open Lean(HashMap) in
+  open Std(HashMap) in
   let numberCoordinates : HashMap Coordinate PartNumber :=
-    Lean.HashMap.ofList $ schematic.numbers.bind $ λ pn ↦ pn.positions.map (·, pn)
+    HashMap.ofList $ schematic.numbers.bind $ λ pn ↦ pn.positions.map (·, pn)
   let gearSymbols := schematic.parts.filter (Part.symbol · == '*')
   -- but the symbols aren't enough, they need to be adjacent to **exactly** 2 numbers
   let numbersNextGearSymbols := List.eraseReps <$> gearSymbols.map λgs ↦
-    gs.position.adjacents.filterMap numberCoordinates.find?
+    gs.position.adjacents.filterMap numberCoordinates.get?
   let gearSymbols := numbersNextGearSymbols.filter (List.length · == 2)
   let gearRatios := gearSymbols.map $ List.foldl (· * PartNumber.value ·) 1
   gearRatios.foldl (· + ·) 0
diff --git a/Day5.lean b/Day5.lean
index f1c96a5..44c3908 100644
--- a/Day5.lean
+++ b/Day5.lean
@@ -180,7 +180,7 @@ def part1 (input : ((List Seed) × Almanach)) : Option Nat :=
                       ∘ a.soilToFertilizer.apply
                       ∘ a.seedsToSoil.apply
   let locations := input.fst.map seedToLocation
-  NatId.toNat <$> locations.minimum?
+  NatId.toNat <$> locations.min?
 
 
 -- Part 2 seems unmanageable by brute force.
@@ -271,7 +271,7 @@ private def part1_2 (input : ((List Seed) × Almanach)) : Option Nat :=
   let seedsToLocation := seedsToHumidity.combine (Mappings2.fromMappings a.humidityToLocation)
   let seedToLocation  := seedsToLocation.apply
   let locations := input.fst.map seedToLocation
-  NatId.toNat <$> locations.minimum?
+  NatId.toNat <$> locations.min?
 
 private structure SeedRange where
   start : Seed
@@ -315,7 +315,7 @@ def part2 (input : ((List Seed) × Almanach)) : Option Nat :=
   let potentialSeeds := seedToLocation.mappings.filterMap λ m ↦
     (SeedRange.findSmallestSeedAbove seedRanges m.start) -- could filter by range end, but who cares?
   let locations := potentialSeeds.map seedToLocation.apply
-  NatId.toNat <$> locations.minimum?
+  NatId.toNat <$> locations.min?
 
 open DayPart
 instance : Parse ⟨5, by simp⟩ (ι := (List Seed) × Almanach) where
diff --git a/Day8.lean b/Day8.lean
index 2f64247..6bb7e99 100644
--- a/Day8.lean
+++ b/Day8.lean
@@ -48,7 +48,7 @@ private def parseWaypoint (input : String) : Except String Waypoint :=
 private def parseWaypoints (input : List String) : Except String $ List Waypoint :=
   input.mapM parseWaypoint
 
-open Lean in
+open Std in
 private def validateWaypointLinks (waypoints : List Waypoint) : Bool :=
   let validLinks := HashSet.insertMany HashSet.empty $ waypoints.map Waypoint.id
   waypoints.all λw ↦ validLinks.contains w.left && validLinks.contains w.right
@@ -88,18 +88,18 @@ private def ConnectedWaypoints.get : ConnectedWaypoints →  Instruction → Way
 
 -- does a single pass over all instructions. Returns err if no result has been found and another pass is needed.
 -- error is optional - if none, then there is an inconsistency in the input and we are stuck.
-private def pass (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) (instructions : List Instruction) : Except (Option (Nat × WaypointId)) Nat := do
+private def pass (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) (instructions : List Instruction) : Except (Option (Nat × WaypointId)) Nat := do
   if currentPosition == "ZZZ" then
     return alreadyDoneSteps
   match instructions with
   | [] => throw $ some (alreadyDoneSteps, currentPosition)
   | a :: as =>
-    let currentWaypoint := waypoints.find? currentPosition
+    let currentWaypoint := waypoints.get? currentPosition
     match currentWaypoint with
     | none => throw none -- should not happen
     | some currentWaypoint => pass waypoints (alreadyDoneSteps + 1) (currentWaypoint.get a) as
 
-private def part1_impl (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) : Option Nat :=
+private def part1_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) : Option Nat :=
   let remainingStarts := possibleStarts.filter λs ↦ s != currentPosition
   if remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy
     let passResult := pass waypoints alreadyDoneSteps currentPosition instructions
@@ -111,7 +111,7 @@ private def part1_impl (waypoints : Lean.HashMap WaypointId ConnectedWaypoints)
     none -- walking in circles
   termination_by possibleStarts.length
 
-open Lean in
+open Std in
 def part1 (input : List Instruction × List Waypoint) : Option Nat :=
   let possibleStarts := input.snd.map Waypoint.id
   let waypoints : HashMap WaypointId ConnectedWaypoints := HashMap.ofList $ input.snd.map λw ↦ (w.id, {left := w.left, right := w.right : ConnectedWaypoints})
@@ -130,13 +130,13 @@ def part1 (input : List Instruction × List Waypoint) : Option Nat :=
 
 -- let's try brute force first.
 
-private def parallelPass (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (alreadyDoneSteps : Nat) (currentPositions : List WaypointId) (instructions : List Instruction) : Except (Option (Nat × (List WaypointId))) Nat := do
+private def parallelPass (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (alreadyDoneSteps : Nat) (currentPositions : List WaypointId) (instructions : List Instruction) : Except (Option (Nat × (List WaypointId))) Nat := do
   if currentPositions.all λw ↦ w.endsWith "Z" then
     return alreadyDoneSteps
   match instructions with
   | [] => throw $ some (alreadyDoneSteps, currentPositions)
   | a :: as =>
-    let currentWaypoint := currentPositions.mapM waypoints.find?
+    let currentWaypoint := currentPositions.mapM waypoints.get?
     match currentWaypoint with
     | none => throw none -- should not happen
     | some currentWaypoints =>
@@ -147,7 +147,7 @@ private def parallelPass (waypoints : Lean.HashMap WaypointId ConnectedWaypoints
 private def totalRemainingStarts (s : List (List WaypointId)) : Nat :=
   s.foldl (·+·.length) 0
 
-private def part2_impl (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (alreadyDoneSteps : Nat) (possibleStarts : List (List WaypointId)) (currentPositions : List WaypointId) : Option Nat :=
+private def part2_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (alreadyDoneSteps : Nat) (possibleStarts : List (List WaypointId)) (currentPositions : List WaypointId) : Option Nat :=
   let remainingStarts := (possibleStarts.zip currentPositions).map λs ↦ s.fst.filter λt ↦ t != s.snd
   -- I _really_ don't want to prove stuff by hand... Luckily this works.
   if totalRemainingStarts remainingStarts < totalRemainingStarts possibleStarts then
@@ -251,7 +251,7 @@ private def CyclingGoal.combine (a b : CyclingGoal) : Option CyclingGoal :=
     let start := start.toNat
     some {start, interval }
 
-private def findCyclingGoalsInPathPass (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) (instructions : List Instruction) (visitedGoals : List Nat) : Option (Nat × WaypointId × (List Nat)) := do
+private def findCyclingGoalsInPathPass (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) (instructions : List Instruction) (visitedGoals : List Nat) : Option (Nat × WaypointId × (List Nat)) := do
   let visitedGoals := if currentPosition.endsWith "Z" then
     alreadyDoneSteps :: visitedGoals
   else
@@ -259,12 +259,12 @@ private def findCyclingGoalsInPathPass (waypoints : Lean.HashMap WaypointId Conn
   match instructions with
   | [] => some (alreadyDoneSteps, currentPosition, visitedGoals)
   | a :: as =>
-    let currentWaypoint := waypoints.find? currentPosition
+    let currentWaypoint := waypoints.get? currentPosition
     match currentWaypoint with
     | none => none -- should not happen
     | some currentWaypoint => findCyclingGoalsInPathPass waypoints (alreadyDoneSteps + 1) (currentWaypoint.get a) as visitedGoals
 
-private def findCyclingGoalsInPath_impl (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (visitedGoals : List Nat) (visitedStarts : List (WaypointId × Nat)) (currentPosition : WaypointId) (currentSteps : Nat) : List CyclingGoal :=
+private def findCyclingGoalsInPath_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (visitedGoals : List Nat) (visitedStarts : List (WaypointId × Nat)) (currentPosition : WaypointId) (currentSteps : Nat) : List CyclingGoal :=
   let remainingStarts := possibleStarts.filter λs ↦ s != currentPosition
   if remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy
     let visitedStarts := (currentPosition, currentSteps) :: visitedStarts
@@ -282,19 +282,19 @@ private def findCyclingGoalsInPath_impl (waypoints : Lean.HashMap WaypointId Con
       none -- goal was reached before we started to walk in cycles, ignore.
   termination_by possibleStarts.length
 
-private def findCyclingGoalsInPath (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (startPosition : WaypointId) : List CyclingGoal :=
+private def findCyclingGoalsInPath (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (startPosition : WaypointId) : List CyclingGoal :=
   findCyclingGoalsInPath_impl waypoints instructions possibleStarts [] [] startPosition 0
 
 -- returns the number of steps needed until the first _commmon_ goal that cycles is found.
-private def findFirstCommonCyclingGoal (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (startPositions : List WaypointId) : Option Nat :=
+private def findFirstCommonCyclingGoal (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (startPositions : List WaypointId) : Option Nat :=
   let cyclingGoals := startPositions.map $ findCyclingGoalsInPath waypoints instructions possibleStarts
   let combinedGoals : List CyclingGoal := match cyclingGoals with
     | [] => []
     | g :: gs => flip gs.foldl g λc n ↦ c.bind λ cc ↦ n.filterMap λ nn ↦ nn.combine cc
   let cyclingGoalStarts := combinedGoals.map CyclingGoal.start
-  cyclingGoalStarts.minimum?
+  cyclingGoalStarts.min?
 
-open Lean in
+open Std in
 def part2 (input : List Instruction × List Waypoint) : Option Nat :=
   let possibleStarts := input.snd.map Waypoint.id
   let waypoints : HashMap WaypointId ConnectedWaypoints := HashMap.ofList $ input.snd.map λw ↦ (w.id, {left := w.left, right := w.right : ConnectedWaypoints})