feat: 2025 day 4

.src/2025_desc.txt

@@ -48,3 +48,17 @@ Their sum would be `55`.
 
 For the second part, we should do the same as in part 1, except that we want to sum the largest
 12-digit numbers that can be extracted.
+-- Day 4
+The input is a grid with the positions of rolls of paper.
+
+### Description
+
+#### Part 1
+
+We should find the number of rolls of papers that have fewer than `4` nearby rolls of paper.
+
+#### Part 2
+
+For the second part, we should recursively remove all rolls of paper that have fewer than `4` nearby
+rolls of paper, until no more rolls can be removed.
+We should report how rolls we removed in the process.

Advents.lean

@@ -2,3 +2,4 @@ import Advents.Utils
 import Advents.AoC2025.day01
 import Advents.AoC2025.day02
 import Advents.AoC2025.day03
+import Advents.AoC2025.day04

Advents/AoC2025/2025_descriptions.md

@@ -3,3 +3,4 @@
 | [1](2025_descriptions_with_tests.md#day-1) | The input is a lists strings, starting with either `L` or `R` and continuing with a natural number. |
 | [2](2025_descriptions_with_tests.md#day-2) | The input is a sequence of ranges of IDs that are all natural numbers.                              |
 | [3](2025_descriptions_with_tests.md#day-3) | The input is a list of sequences of joltages, each of which is a natural number from `1` to `9`.    |
+| [4](2025_descriptions_with_tests.md#day-4) | The input is a grid with the positions of rolls of paper.                                           |

Advents/AoC2025/2025_descriptions_with_tests.md

@@ -96,3 +96,38 @@ For the second part, we should do the same as in part 1, except that we want to
 [Solution in Lean](day03.lean)
 
 ---
+
+#  [Day 4](https://adventofcode.com/2025/day/4)
+
+The input is a grid with the positions of rolls of paper.
+
+####  Test
+
+<pre>
+..@@.@@@@.
+@@@.@.@.@@
+@@@@@.@.@@
+@.@@@@..@.
+@@.@@@@.@@
+.@@@@@@@.@
+.@.@.@.@@@
+@.@@@.@@@@
+.@@@@@@@@.
+@.@.@@@.@.
+</pre>
+
+### Description
+
+#### Part 1
+
+We should find the number of rolls of papers that have fewer than `4` nearby rolls of paper.
+
+#### Part 2
+
+For the second part, we should recursively remove all rolls of paper that have fewer than `4` nearby
+rolls of paper, until no more rolls can be removed.
+We should report how rolls we removed in the process.
+
+[Solution in Lean](day04.lean)
+
+---

Advents/AoC2025/day04.lean

@@ -0,0 +1,90 @@
+import Advents.Utils
+open Std
+
+namespace AoC2025_Day04
+
+open System in
+/-- `input` is the location of the file with the data for the problem. -/
+def input : FilePath := ("Advents"/"AoC2025"/"day04" : FilePath).withExtension "input"
+
+/-!
+#  Question 1
+-/
+
+/-- `test` is the test string for the problem. -/
+def test := "..@@.@@@@.
+@@@.@.@.@@
+@@@@@.@.@@
+@.@@@@..@.
+@@.@@@@.@@
+.@@@@@@@.@
+.@.@.@.@@@
+@.@@@.@@@@
+.@@@@@@@@.
+@.@.@@@.@."
+
+/-- `atest` is the test string for the problem, split into rows. -/
+def atest := (test.splitOn "\n").toArray
+
+/--
+Finds the elements of `h` that are neighbours of position `p`,
+in one of the possible `8` directions.
+-/
+def neighs (h : HashSet pos) (p : pos) : HashSet pos := Id.run do
+  let mut fin := ∅
+  for ns in [(1, 0), (0, 1), (-1, 0), (0, -1), (1, 1), (1, -1), (-1, 1), (-1, -1)] do
+    let new := p + ns
+    if h.contains new then
+      fin := fin.insert new
+  return fin
+
+/-- `part1 dat` takes as input the input of the problem and returns the solution to part 1. -/
+def part1 (dat : Array String) : Nat :=
+  let gr := sparseGrid dat (· == '@')
+  let le4 := gr.filter fun p => (neighs gr p).size < 4
+  le4.size
+
+#assert part1 atest == 13
+
+solve 1 1409
+
+/-!
+#  Question 2
+-/
+
+/--
+Given two `h rem : HashSet pos`, returns the `HashSet` of those elements of `h` that are
+neighbours of some element of `rem`.
+-/
+def getNbs (h rem : HashSet pos) : HashSet pos :=
+  rem.fold (init := ∅) fun tot p => Id.run do
+    let mut here : HashSet pos := ∅
+    for n in [(1, 0), (0, 1), (-1, 0), (0, -1), (1, 1), (1, -1), (-1, 1), (-1, -1)] do
+      let shifted := p + n
+      if shifted ∈ h then here := here.insert shifted
+    tot.insertMany here
+
+/-- `part2 dat` takes as input the input of the problem and returns the solution to part 2. -/
+def part2 (dat : Array String) : Nat := Id.run do
+  let gr := sparseGrid dat (· == '@')
+  let mut old := gr
+  let mut (new, removed) := old.partition fun p => 4 ≤ (neighs old p).size
+  let mut nearRemoved := getNbs old removed
+  let mut rems := old.size - new.size
+  while old != new do
+    old := new
+    let mut (new', removed') : HashSet pos × HashSet pos := (old, ∅)
+    for p in nearRemoved do
+      if (neighs old p).size < 4 then
+        new' := new'.erase p
+        removed' := removed'.insert p
+    (new, removed) := (new', removed')
+    nearRemoved := getNbs old removed
+    rems := rems + old.size - new.size
+  return rems
+
+#assert part2 atest == 43
+
+solve 2 8366
+
+end AoC2025_Day04

Advents/Utils.lean

@@ -349,7 +349,12 @@ def drawHash {α} [ToString α] (h : HashMap pos α) (Nx Ny : Nat) : Array Strin
     fin := fin.push str
   return fin
 
-/-- A function to draw `HashSet`s. -/
+/--
+A function to draw `HashSet`s.
+
+The `Nx` input is the *vertical* span of the `HashSet`,
+the `Ny` input is the *horizontal* span of the `HashSet`.
+-/
 def drawSparseWith (h : HashSet pos) (Nx Ny : Nat)
     (yes : pos → String := fun _ => "#") (no : pos → String := fun _ => ".") :
     Array String := Id.run do
@@ -363,7 +368,12 @@ def drawSparseWith (h : HashSet pos) (Nx Ny : Nat)
     fin := fin.push str
   return fin
 
-/-- A function to draw `HashSet`s. -/
+/--
+A function to draw `HashSet`s.
+
+If `h` is obtained by reading a "grid" `dat : Array String`, then
+the `Nx` input is likely `dat.size` and the `Ny` input is likely `dat[0]!.length`.
+-/
 def drawSparse (h : HashSet pos) (Nx Ny : Nat) (yes : String := "#") (no : String := "·") :
     Array String := Id.run do
   let mut fin := #[]