Today’s problem was about paper rolls in a grid. Or actually Chars in a grid. Quite easy once the code for working with positions and neighbours was in place.

Since I was working with a grid I copied my Position type from last year’s AoC into my utility library:

structure Position where
  x : Int
  y : Int
  deriving BEq, Ord, Hashable, Repr, Inhabited

(I also added a function for creating a Position -> α map from a two-dimensional list of αs: toMap (xs : List (List α)) : Std.HashMap Position α.)

With that in place, solving the problem was quite straightforward. With the main workhorse isRemovable (see solution below) in place, we can simply remove rolls as long as there are some to remove:

partial def removeRolls (map : Map) : Map :=
  let removable := map.keys.filter (isRemovable map)
  if removable.isEmpty then
    map
  else
    let newMap := removable.foldl (λ m pos => m.insert pos '.') map
    removeRolls newMap

But! Did you notice the partial in the definition? The default in Lean is that functions are total, and the termination checker will check that a function terminates. However in this case it’s not able to:

fail to show termination for
  removeRolls
with errors
failed to infer structural recursion:
Cannot use parameter map:
  the type Std.HashMap Position Char does not have a `.brecOn` recursor

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal

This is basically saying that we need to convince it that the map argument is decreasing on each recursive call. That isn’t really the case here, since it cannot know that inserting a '.' means that fewer rolls will be present for the next round.

By some re-jigging, it is probably possible to show that this structural recursion terminates, but since I’m easing into Lean here, I’ll use a method I learned from the excellent book Type-Driven Development with Idris. We can introduce the notion of “fuel” that serves as an upper limit of recursion by spending one unit of fuel for each recursive call. This lets the termination checker trivially see that the recursion will end, and since we know how many rolls there are to begin with, and we always remove at least one roll, we have a natural upper limit; I wrapped this up in an inner function (go) that gets passed this upper limit. No more partial!

def removeRolls (map : Map) : Map :=
  let rec go (map : Map) (fuel : Nat) :=
    match fuel with
      | 0 => map
      | n + 1 =>
        let removable := map.keys.filter (isRemovable map)
        if removable.isEmpty then
          map
        else
          let map' := removable.foldl (λ m pos => m.insert pos '.') map
          go map' n

  let limit := map.values.filter (· == '@') |> List.length
  go map limit

Done and dusted!

Things I (re-)learned today

• I can use partial to tell the termination checker that a function is not total, and that it shouldn’t try to show that it terminates.
• I can use repr to print a debug representation of a term.
• I can use λ instead of fun when defining an anonymous function. This has already proved too tempting, as can be seen from my code.

Solution

import Aoc
open Aoc

abbrev Map := Std.HashMap Position Char

def isRemovable (map : Map) (pos : Position) : Bool :=
  match map.get? pos with
  | some '@' =>
    let neighbours := pos.neighbourhood.map (map.get? ·)
    let neighbouringRolls := (neighbours.filter (· == some '@')).length
    neighbouringRolls < 4
  | _ => false

def removeRolls (map : Map) : Map :=
  let rec go (map : Map) (fuel : Nat) :=
    match fuel with
      | 0 => map
      | n + 1 =>
        let removable := map.keys.filter (isRemovable map)
        if removable.isEmpty then
          map
        else
          let map' := removable.foldl (λ m pos => m.insert pos '.') map
          go map' n

  let limit := map.values.filter (· == '@') |> List.length
  go map limit

def main : IO Unit := do
  let lines ← readLines "Day04/input.txt"
  let map := lines.toList.map (·.toList) |> toMap

  -- part 1
  let removable := map.keys.filter (isRemovable map)
  IO.println s!"Part 1: {removable.length}"

  -- part 2
  let afterRemoval := removeRolls map
  let rollsBefore := map.values.filter (· == '@') |> List.length
  let rollsAfter := afterRemoval.values.filter (· == '@') |> List.length
  IO.println s!"Part 2: {rollsBefore - rollsAfter}"