From a6e4b8f15c28c374553684f63fa3f4108095da2d Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Wed, 18 Dec 2024 09:05:03 +0100
Subject: Start Day 17

---
 Day17.lean    | 76 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 lakefile.lean |  1 +
 2 files changed, 77 insertions(+)
 create mode 100644 Day17.lean

diff --git a/Day17.lean b/Day17.lean
new file mode 100644
index 0000000..496b40c
--- /dev/null
+++ b/Day17.lean
@@ -0,0 +1,76 @@
+import Common
+
+namespace Day17
+
+------------------------------------------------------------------------------------
+
+abbrev HeatLossMap := Parsing.RectangularGrid Nat
+
+structure CharacterParseError where
+  char : Char
+
+instance : ToString CharacterParseError where
+  toString := λ ({char}) ↦ s!"Unexpected character '{char}'. Expected a digit between 1 and 9."
+
+open Except in
+private def parseCharacter : Char → Except CharacterParseError Nat
+| '1' => ok 1
+| '2' => ok 2
+| '3' => ok 3
+| '4' => ok 4
+| '5' => ok 5
+| '6' => ok 6
+| '7' => ok 7
+| '8' => ok 8
+| '9' => ok 9
+| char => error {char}
+
+open Parsing in
+def parse : String → Except (RectangularGrid.ParseError CharacterParseError) HeatLossMap := Parsing.RectangularGrid.ofString parseCharacter
+
+------------------------------------------------------------------------------------
+
+section PathNode
+variable {heatLossMap : HeatLossMap}
+
+private inductive Direction
+| Up
+| Right
+| Down
+| Left
+deriving BEq
+
+instance : LawfulBEq Direction where
+  rfl := λ{x} ↦ by cases x <;> rfl
+  eq_of_beq := λ {a b} ↦ by cases a <;> cases b <;> simp <;> rfl
+
+private inductive StepsInDirection
+| One
+| Two
+| Three
+
+private def StepsInDirection.next (s : StepsInDirection) (h₁ : s ≠ .Three) : StepsInDirection :=
+  match s with
+  | .One => .Two
+  | .Two => .Three
+
+private structure PathNode (heatLossMap : HeatLossMap) where
+  coordinate : heatLossMap.Coordinate
+  accumulatedCosts : Nat
+  currentDirection : Direction
+  takenSteps : StepsInDirection
+
+private def PathNode.goUp? (node : PathNode heatLossMap) : Option (PathNode heatLossMap) :=
+  match node.coordinate.y, node.currentDirection, node.takenSteps with
+  | ⟨0,_⟩, _, _ => none
+  | _, Direction.Up, StepsInDirection.Three => none
+  | ⟨y,h₂⟩, Direction.Up, steps@h₁:StepsInDirection.One | ⟨y,h₂⟩, Direction.Up, steps@h₁:StepsInDirection.Two =>
+    have : steps ≠ .Three := λx ↦ StepsInDirection.noConfusion (x.subst h₁.symm)
+    sorry
+  | ⟨y,h₂⟩, _, _ => sorry
+
+private def PathNode.getNeighbours (node : PathNode heatLossMap) : List (PathNode heatLossMap) :=
+  sorry
+
+
+end PathNode
diff --git a/lakefile.lean b/lakefile.lean
index 78bd995..ae32628 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -19,6 +19,7 @@ lean_lib «Day13» where
 lean_lib «Day14» where
 lean_lib «Day15» where
 lean_lib «Day16» where
+lean_lib «Day17» where
 
 lean_lib «Common» where
 
-- 
cgit v1.2.3