From 2a9261d1ba962deff9fcc1784be44563af513af5 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 10 Oct 2025 00:30:19 +0200
Subject: Lean 4.18

---
 Day8.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'Day8.lean')

diff --git a/Day8.lean b/Day8.lean
index 079e485..4e5d1bc 100644
--- a/Day8.lean
+++ b/Day8.lean
@@ -101,7 +101,7 @@ private def pass (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (alread
 
 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
+  if _ht: remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy
     let passResult := pass waypoints alreadyDoneSteps currentPosition instructions
     match passResult with
     | Except.ok n => some n
@@ -110,6 +110,8 @@ private def part1_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (
   else
     none -- walking in circles
   termination_by possibleStarts.length
+  decreasing_by
+    exact _ht
 
 open Std in
 def part1 (input : List Instruction × List Waypoint) : Option Nat :=
@@ -266,7 +268,7 @@ private def findCyclingGoalsInPathPass (waypoints : Std.HashMap WaypointId Conne
 
 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
+  if _ht: remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy
     let visitedStarts := (currentPosition, currentSteps) :: visitedStarts
     let passResult := findCyclingGoalsInPathPass waypoints currentSteps currentPosition instructions visitedGoals
     match passResult with
@@ -281,6 +283,8 @@ private def findCyclingGoalsInPath_impl (waypoints : Std.HashMap WaypointId Conn
     else
       none -- goal was reached before we started to walk in cycles, ignore.
   termination_by possibleStarts.length
+  decreasing_by
+    exact _ht
 
 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
-- 
cgit v1.2.3

