Day 9: Mirage Maintenance

Megathread guidelines

  • Keep top level comments as only solutions, if you want to say something other than a solution put it in a new post. (replies to comments can be whatever)
  • Code block support is not fully rolled out yet but likely will be in the middle of the event. Try to share solutions as both code blocks and using something such as https://topaz.github.io/paste/ , pastebin, or github (code blocks to future proof it for when 0.19 comes out and since code blocks currently function in some apps and some instances as well if they are running a 0.19 beta)

FAQ

  • What is this?: Here is a post with a large amount of details: https://programming.dev/post/6637268
  • Where do I participate?: https://adventofcode.com/
  • Is there a leaderboard for the community?: We have a programming.dev leaderboard with the info on how to join in this post: https://programming.dev/post/6631465

🔒 Thread is locked until there's at least 100 2 star entries on the global leaderboard

🔓 Unlocked after 5 mins

  • soulsource@discuss.tchncs.de
    ·
    7 months ago

    [Language: Lean4]

    This one was very easy, almost trivial. Lean4 did demand a proof of termination though, and I'm still not very good at writing proofs...

    I'm also pretty happy that this time I was able to re-use most of part 1 for part 2, and part 2 being a one-liner therefore.

    As always, here is only the file with the actual solution, some helper functions are implemented in different files - check my github for the whole project.

    Solution 
    
private def parseLine (line : String) : Except String $ List Int :=
  line.split Char.isWhitespace
  |> List.map String.trim
  |> List.filter String.notEmpty
  |> List.mapM String.toInt?
  |> Option.toExcept s!"Failed to parse numbers in line \"{line}\""

def parse (input : String) : Except String $ List $ List Int :=
  let lines := input.splitOn "\n" |> List.map String.trim |> List.filter String.notEmpty
  lines.mapM parseLine

-------------------------------------------------------------------------------------------

private def differences : List Int → List Int
| [] => []
| _ :: [] => []
| a :: b :: as => (a - b) :: differences (b::as)

private theorem differences_length_independent_arg (a b : Int) (bs : List Int) : (differences (a :: bs)).length = (differences (b :: bs)).length := by
  induction bs <;> simp[differences]

-- BEWARE: Extrapolate needs the input reversed.
private def extrapolate : List Int → Int
| [] => 0
| a :: as =>
  if a == 0 && as.all (· == 0) then
    0
  else
    have : (differences (a :: as)).length < as.length + 1 := by
      simp_arith[differences]
      induction (as) <;> simp_arith[differences]
      case cons b bs hb => rw[←differences_length_independent_arg]
                           assumption
    a + extrapolate (differences (a :: as))
termination_by extrapolate a => a.length

def part1 : List (List Int) → Int :=
  List.foldl Int.add 0 ∘ List.map (extrapolate ∘ List.reverse)

-------------------------------------------------------------------------------------------

def part2 : List (List Int) → Int :=
  List.foldl Int.add 0 ∘ List.map extrapolate