1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
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
|
