diff options
| -rw-r--r-- | Day12.lean | 8 | ||||
| -rw-r--r-- | Day2.lean | 2 | ||||
| -rw-r--r-- | Day3.lean | 8 | ||||
| -rw-r--r-- | Day5.lean | 6 | ||||
| -rw-r--r-- | Day8.lean | 30 |
5 files changed, 27 insertions, 27 deletions
@@ -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 := @@ -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 @@ -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 @@ -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 @@ -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}) |