From 7e50958adb75487cef49807b1a515591544cf6ac Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 8 Sep 2024 22:21:23 +0200
Subject: Begin Day 10 Part 2

---
 Day10.lean | 49 ++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 38 insertions(+), 11 deletions(-)

(limited to 'Day10.lean')

diff --git a/Day10.lean b/Day10.lean
index 5bc283e..8191f55 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -1,4 +1,5 @@
 import «Common»
+import «BinaryHeap»
 
 namespace Day10
 
@@ -946,18 +947,21 @@ private def Area.nextPathStep (last_step: Area.PathHead area) : Option (Area.Bid
       none
 end
 
+private def Area.pathStarts (area : Area) : List (Area.PathHead area) :=
+  [area.start.goNorth, area.start.goEast, area.start.goSouth, area.start.goWest]
+  |> .filterMap λ c ↦ c.bind λc ↦
+    if h: area.can_connect_to c area.start then
+      some {
+        current := c
+        previous := area.start
+        current_can_connect_to_previous := h
+      }
+    else
+      none
+
+
 def part1 (area : Area) : Option Nat := do
-  let mut paths : List (Area.PathHead area) :=
-    [area.start.goNorth, area.start.goEast, area.start.goSouth, area.start.goWest]
-    |> .filterMap λ c ↦ c.bind λc ↦
-      if h: area.can_connect_to c area.start then
-        some {
-          current := c
-          previous := area.start
-          current_can_connect_to_previous := h
-        }
-      else
-        none
+  let mut paths : List (Area.PathHead area) := area.pathStarts
 
   let mut steps := 1
   -- The condition in the while-loop is not needed. The program always terminates, as the
@@ -985,6 +989,29 @@ where
   | _ :: [] => true
   | _ => false
 
+------------------------------------------------------------------------------------------------------------
+
+private def coordinateSorter (a b : Coordinate w h) : Bool :=
+  a.y < b.y ∨ (a.y = b.y ∧ a.x ≤ b.x)
+
+private theorem coordiateSorter_transitive {w h : Nat} : BinaryHeap.transitive_le (coordinateSorter (w := w) (h := h)) := by
+  unfold BinaryHeap.transitive_le
+  intros a b c
+  unfold coordinateSorter
+  simp
+  omega
+
+private theorem coordinateSorter_total {w h : Nat} : BinaryHeap.total_le (coordinateSorter (w := w) (h := h)) := by
+  unfold BinaryHeap.total_le
+  intros a b
+  unfold coordinateSorter
+  simp
+  omega
+
+def part2 (area : Area) : Option Nat :=
+  sorry
+
+
 ------------------------------------------------------------------------------------------------------------
 open DayPart
 instance : Parse ⟨10, by simp⟩ (ι := Area) where
-- 
cgit v1.2.3