diff --git a/Aoc2024/Day06/Types.lean b/Aoc2024/Day06/Types.lean index 38d64bf..1071906 100644 --- a/Aoc2024/Day06/Types.lean +++ b/Aoc2024/Day06/Types.lean @@ -1,13 +1,7 @@ import Std +import Aoc2024.Utils open Std (HashSet) -structure Point where - x : Int - y : Int -deriving BEq, Hashable, Repr, Inhabited - -def Point.toPair (p : Point) : (Int × Int) := (p.x, p.y) - inductive Direction where | Up | Right @@ -28,21 +22,6 @@ def Point.step (p : Point) (d : Direction) : Point := | Direction.Down => { p with y := p.y + 1 } | Direction.Left => { p with x := p.x - 1 } -def Point.origin : Point := { x := 0, y := 0 } - -structure Rectangle where - topLeft : Point - width: Nat - height: Nat -deriving Repr, BEq, Hashable, Inhabited - -def Rectangle.contains (r : Rectangle) (p : Point) : Bool := - r.topLeft.x ≤ p.x && p.x < r.topLeft.x + r.width && - r.topLeft.y ≤ p.y && p.y < r.topLeft.y + r.height - -#guard Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 1, y := 1 } -#guard !Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 2, y := 2 } - structure PuzzleInput where obstacles : HashSet Point bounds : Rectangle diff --git a/Aoc2024/Day08/Types.lean b/Aoc2024/Day08/Types.lean index 385ef96..5372917 100644 --- a/Aoc2024/Day08/Types.lean +++ b/Aoc2024/Day08/Types.lean @@ -2,47 +2,6 @@ import Aoc2024.Utils import Std open Std (HashSet) -structure Point where - x : Int - y : Int -deriving BEq, Hashable, Repr, Inhabited - -def Point.toPair (p : Point) : (Int × Int) := (p.x, p.y) - -def Point.origin : Point := { x := 0, y := 0 } - -structure Vector where - x : Int - y : Int -deriving BEq, Hashable, Repr, Inhabited - -def Point.vectorTo (from_ to : Point) : Vector := { x := to.x - from_.x, y := to.y - from_.y } -#guard ({ x := 1, y := 1 } : Point).vectorTo { x := 2, y := 2 } == { x := 1, y := 1 } - -def Point.add (p : Point) (v : Vector) : Point := { x := p.x + v.x, y := p.y + v.y } -#guard Point.add { x := 1, y := 1 } { x := 2, y := 2 } == { x := 3, y := 3 } - -structure Rectangle where - topLeft : Point - width: Nat - height: Nat -deriving Repr, BEq, Hashable, Inhabited - -def Rectangle.contains (r : Rectangle) (p : Point) : Bool := - r.topLeft.x ≤ p.x && p.x < r.topLeft.x + r.width && - r.topLeft.y ≤ p.y && p.y < r.topLeft.y + r.height - -#guard Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 1, y := 1 } -#guard !Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 2, y := 2 } - -def Rectangle.allPoints (r : Rectangle) : List Point := do - let x <- intRange r.topLeft.x (r.topLeft.x + r.width) - let y <- intRange r.topLeft.y (r.topLeft.y + r.height) - return { x := x, y := y } - -#guard Rectangle.allPoints { topLeft := Point.origin, width := 2, height := 2 } == - [{ x := 0, y := 0 }, { x := 0, y := 1 }, { x := 1, y := 0 }, { x := 1, y := 1 }] - structure PointAndChar where point: Point char: Char diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean index 9d7cfa6..68a813d 100644 --- a/Aoc2024/Utils.lean +++ b/Aoc2024/Utils.lean @@ -225,3 +225,44 @@ def intRange (m n : Int) : List Int := #guard intRange 1 1 == [] instance hashableChar: Hashable Char where hash c := c.toNat |> hash + +structure Point where + x : Int + y : Int +deriving BEq, Hashable, Repr, Inhabited + +def Point.toPair (p : Point) : (Int × Int) := (p.x, p.y) + +def Point.origin : Point := { x := 0, y := 0 } + +structure Vector where + x : Int + y : Int +deriving BEq, Hashable, Repr, Inhabited + +def Point.vectorTo (from_ to : Point) : Vector := { x := to.x - from_.x, y := to.y - from_.y } +#guard ({ x := 1, y := 1 } : Point).vectorTo { x := 2, y := 2 } == { x := 1, y := 1 } + +def Point.add (p : Point) (v : Vector) : Point := { x := p.x + v.x, y := p.y + v.y } +#guard Point.add { x := 1, y := 1 } { x := 2, y := 2 } == { x := 3, y := 3 } + +structure Rectangle where + topLeft : Point + width: Nat + height: Nat +deriving Repr, BEq, Hashable, Inhabited + +def Rectangle.contains (r : Rectangle) (p : Point) : Bool := + r.topLeft.x ≤ p.x && p.x < r.topLeft.x + r.width && + r.topLeft.y ≤ p.y && p.y < r.topLeft.y + r.height + +#guard Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 1, y := 1 } +#guard !Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 2, y := 2 } + +def Rectangle.allPoints (r : Rectangle) : List Point := do + let x <- intRange r.topLeft.x (r.topLeft.x + r.width) + let y <- intRange r.topLeft.y (r.topLeft.y + r.height) + return { x := x, y := y } + +#guard Rectangle.allPoints { topLeft := Point.origin, width := 2, height := 2 } == + [{ x := 0, y := 0 }, { x := 0, y := 1 }, { x := 1, y := 0 }, { x := 1, y := 1 }]