From 406c23a9f6c6a4c7e03f9aad4131921e589623bc Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 22 Dec 2024 23:17:05 +0100
Subject: Day 17, part 1 (hopefully)

---
 Day17.lean | 76 ++++++++++++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 64 insertions(+), 12 deletions(-)

(limited to 'Day17.lean')

diff --git a/Day17.lean b/Day17.lean
index 602ae39..539baaf 100644
--- a/Day17.lean
+++ b/Day17.lean
@@ -46,6 +46,21 @@ instance : LawfulBEq Direction where
   rfl := λ{x} ↦ by cases x <;> rfl
   eq_of_beq := λ {a b} ↦ by cases a <;> cases b <;> simp <;> rfl
 
+instance : Finite Direction where
+  cardinality := 4
+  enumerate := λ
+  | .Up => 0
+  | .Right => 1
+  | .Down => 2
+  | .Left => 3
+  nth := λ
+  | 0 => .Up
+  | 1 => .Right
+  | 2 => .Down
+  | 3 => .Left
+  nth_inverse_enumerate := by funext x; cases x <;> rfl
+  enumerate_inverse_nth := by funext x; revert x; decide
+
 private inductive StepsInDirection
 | One
 | Two
@@ -56,6 +71,19 @@ instance : LawfulBEq StepsInDirection where
   rfl := λ{x} ↦ by cases x <;> rfl
   eq_of_beq := λ {a b} ↦ by cases a <;> cases b <;> simp <;> rfl
 
+instance : Finite StepsInDirection where
+  cardinality := 3
+  enumerate := λ
+  | .One => 0
+  | .Two => 1
+  | .Three => 2
+  nth := λ
+  | 0 => .One
+  | 1 => .Two
+  | 2 => .Three
+  nth_inverse_enumerate := by funext x; cases x <;> rfl
+  enumerate_inverse_nth := by funext x; revert x; decide
+
 private def StepsInDirection.next (s : StepsInDirection) (h₁ : s ≠ .Three) : StepsInDirection :=
   match s with
   | .One => .Two
@@ -284,6 +312,30 @@ instance {heatLossMap : HeatLossMap} : LawfulBEq (ClosedSetEntry heatLossMap) wh
     simp! at h₁
     simp[h₁]
 
+private def ClosedSetEntry.toTuple {heatLossMap : HeatLossMap} : (ClosedSetEntry heatLossMap) → (heatLossMap.Coordinate × Direction × StepsInDirection)
+| {coordinate, direction, steps} => (coordinate, direction, steps)
+
+private def ClosedSetEntry.ofTuple {heatLossMap : HeatLossMap} : (heatLossMap.Coordinate × Direction × StepsInDirection) → (ClosedSetEntry heatLossMap)
+| (coordinate, direction, steps) => {coordinate, direction, steps}
+
+private theorem ClosedSetEntry.toTuple_inv_ofTuple {heatLossMap : HeatLossMap} : (ClosedSetEntry.toTuple (heatLossMap := heatLossMap)) ∘ ClosedSetEntry.ofTuple = id := rfl
+private theorem ClosedSetEntry.ofTuple_inv_toTuple {heatLossMap : HeatLossMap} : (ClosedSetEntry.ofTuple (heatLossMap := heatLossMap)) ∘ ClosedSetEntry.toTuple = id := rfl
+
+instance {heatLossMap : HeatLossMap} : Finite (ClosedSetEntry heatLossMap) where
+  cardinality := Finite.cardinality (heatLossMap.Coordinate × Direction × StepsInDirection)
+  enumerate := Finite.enumerate ∘ ClosedSetEntry.toTuple
+  nth := ClosedSetEntry.ofTuple ∘ Finite.nth
+  enumerate_inverse_nth := by
+    funext x
+    rewrite[Function.comp_assoc]
+    rewrite (occs := .pos [2]) [←Function.comp_assoc]
+    simp only[ClosedSetEntry.toTuple_inv_ofTuple, Function.id_comp, Finite.enumerate_inverse_nth]
+  nth_inverse_enumerate := by
+    funext x
+    rewrite[Function.comp_assoc]
+    rewrite (occs := .pos [2]) [←Function.comp_assoc]
+    simp only[Finite.nth_inverse_enumerate, Function.id_comp, ClosedSetEntry.ofTuple_inv_toTuple]
+
 instance {heatLossMap : HeatLossMap} : Coe (PathNode heatLossMap) (ClosedSetEntry heatLossMap) where
   coe := λ{coordinate, currentDirection, takenSteps, ..} ↦ {coordinate, direction := currentDirection, steps := takenSteps}
 
@@ -314,7 +366,7 @@ private theorem OpenSet.findFirstNotInClosedSet_not_in_closed_set {heatLossMap :
     subst result
     assumption
 
-private partial def HeatLossMap.findPath {heatLossMap : HeatLossMap} {n : Nat} (openSet : OpenSet heatLossMap n) (closedSet : ClosedSet heatLossMap) : Option Nat :=
+private def HeatLossMap.findPath {heatLossMap : HeatLossMap} {n : Nat} (openSet : OpenSet heatLossMap n) (closedSet : ClosedSet heatLossMap) : Option Nat :=
   match h₁ : openSet.findFirstNotInClosedSet closedSet with
   | none => none
   | some ⟨_,(node, openSet)⟩ =>
@@ -325,17 +377,17 @@ private partial def HeatLossMap.findPath {heatLossMap : HeatLossMap} {n : Nat} (
       let newClosedSet := closedSet.insert node
       let openSet := openSet.pushList neighbours
       findPath openSet newClosedSet
---termination_by (ClosedSet.full heatLossMap).size - closedSet.size
---decreasing_by
---  have h₃ := Std.HashSet.size_insert (m := closedSet) (k := { coordinate := node.coordinate, direction := node.currentDirection, steps := node.takenSteps })
---  split at h₃
---  case isTrue =>
---    have := OpenSet.findFirstNotInClosedSet_not_in_closed_set _ _ h₁
---    contradiction
---  case isFalse oldOpenSet h₂ =>
---    rw[h₃]
---    have : closedSet.size < (ClosedSet.full heatLossMap).size := sorry --contradiction, h₂, ClosedSet.full_is_full, Std.HashSet.size_insert
---    omega
+termination_by (Finite.cardinality (ClosedSetEntry heatLossMap)) - closedSet.size
+decreasing_by
+  have h₃ := Std.HashSet.size_insert (m := closedSet) (k := { coordinate := node.coordinate, direction := node.currentDirection, steps := node.takenSteps })
+  split at h₃
+  case isTrue =>
+    have := OpenSet.findFirstNotInClosedSet_not_in_closed_set _ _ h₁
+    contradiction
+  case isFalse h₂ =>
+    rw[h₃]
+    have : closedSet.size < (Finite.cardinality (ClosedSetEntry heatLossMap)) := Std.HashSet.size_lt_finite_cardinality_of_not_mem closedSet ⟨_,h₂⟩
+    omega
 
 
 
-- 
cgit v1.2.3

