diff options
| -rw-r--r-- | Common/List.lean | 16 | ||||
| -rw-r--r-- | Day12.lean | 134 | ||||
| -rw-r--r-- | Main.lean | 2 |
3 files changed, 142 insertions, 10 deletions
diff --git a/Common/List.lean b/Common/List.lean index b34f1e2..1c029e7 100644 --- a/Common/List.lean +++ b/Common/List.lean @@ -54,3 +54,19 @@ def not_empty_iff_size_gt_zero {list : List α} : list.isEmpty = false ↔ list. match list with | [] => ⟨nofun, nofun⟩ | l :: ls => ⟨λ_ ↦ (List.length_cons l ls).substr (Nat.succ_pos ls.length), λ_ => rfl⟩ + +def ne_nil_of_not_empty {list : List α} : list.isEmpty = false ↔ list ≠ [] := + match list with + | [] => ⟨nofun, nofun⟩ + | _ :: _ => ⟨nofun, λ_ ↦ List.isEmpty_cons⟩ + +def drop_while_length_le (list : List α) (f : α → Bool) : (list.dropWhile f).length ≤ list.length := by + unfold dropWhile + split + case h_1 => exact Nat.le_refl _ + case h_2 => + split + case h_2 => exact Nat.le_refl _ + case h_1 a as _ _ => + have := drop_while_length_le as f + exact Nat.le_trans this (Nat.le_succ as.length) @@ -8,10 +8,25 @@ inductive SpringState | operational | damaged | unknown +deriving Repr, BEq + +instance : ToString (List SpringState) where + toString := λl ↦ + let rec w := λ + | .operational :: as => "." ++ (w as) + | .damaged :: as => "#" ++ (w as) + | .unknown :: as => "?" ++ (w as) + | [] => "" + w l + structure SpringArrangement where - Mask : List SpringState - DamagedGroups : List Nat + mask : List SpringState + damagedGroups : List Nat + +instance : ToString SpringArrangement where + toString := λ + | {mask, damagedGroups} => (inferInstance : ToString (List SpringState)).toString mask ++ " " ++ damagedGroups.toString inductive ParsingError | unknownSymbolInLeftBlock : Char → ParsingError @@ -32,7 +47,7 @@ instance : ToString ParsingError where -def parse (input : String) : Except ParsingError SpringArrangement := +def parse (input : String) : Except ParsingError (List SpringArrangement) := let input := input.toSubstring.trim let lines := input.splitOn "\n" let lines := lines.filterMap λx ↦ @@ -41,13 +56,11 @@ def parse (input : String) : Except ParsingError SpringArrangement := if lines.isEmpty then Except.error ParsingError.noInput else - let splitLines := lines.map (·.splitOn " ") - let invalidLines := splitLines.map List.length |> List.filter (· ≠ 2) - if h : !invalidLines.isEmpty then - Except.error $ ParsingError.invalidNumberOfBlockSeparators $ invalidLines.head (List.not_empty_iff_size_gt_zero.mp ((Bool.not_eq_true' _).mp h) |> List.ne_nil_of_length_pos) - else - --splitLines.mapM - sorry + lines.mapM λl ↦ + match l.splitOn " " with + | l :: r :: [] => parseLeftBlock l [] >>= λmask↦ parseRightBlock r <&> λdamagedGroups ↦ {mask, damagedGroups} + | _ :: [] => .error $ ParsingError.invalidNumberOfBlockSeparators 0 + | l => .error $ ParsingError.invalidNumberOfBlockSeparators (l.length - 1) where parseLeftBlock : Substring → List SpringState → Except ParsingError (List SpringState) := λs p ↦ if s.isEmpty then @@ -69,3 +82,104 @@ where parseRightBlock : Substring → Except ParsingError (List Nat) := λs ↦ s.splitOn "," |> List.mapM λs ↦ (Substring.toNat? s).toExcept (ParsingError.nonNumericSymbolInRightBlock s) + + +---------------------------------------------------------------------------------------------------- + +-- There is probably some nice closed form, but I don't have the brain for that right now. +-- Brute force, it is. + +inductive DefiniteSpringState +| operational +| damaged + +def canFirstNBeDamaged (states : List SpringState) (n : Nat) : Bool := + match n, states with + | 0, _ => true + | (_ + 1), [] => false + | (_ + 1), .operational :: _ => false + | (nn + 1), _ :: ss => canFirstNBeDamaged ss nn + +def canFirstBeOperational : (states : List SpringState) → Bool +| .operational :: _ => true +| .unknown :: _ => true +| _ => false + +def mustFirstBeDamaged : (states : List SpringState) → Bool +| .damaged :: _ => true +| _ => false + +def countPossiblePositionsWithDamaged (remainingSpace : List SpringState) (remainingDamagedGroups : List Nat) (h₁ : remainingDamagedGroups ≠ []) : Nat := + if h₂ : remainingSpace.isEmpty then + 0 + else + match remainingDamagedGroups with + | g :: gs => + let fromCurrentPosition := + if canFirstNBeDamaged remainingSpace g then + if h₃ : gs.isEmpty then + if (remainingSpace.drop g).any (· == .damaged) then + 0 + else + 1 + else + let d := (remainingSpace.drop g) + if canFirstBeOperational d then + countPossiblePositionsWithDamaged (d.drop 1) gs (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h₃) + else + 0 + else + 0 + have : remainingSpace.length > 0 := List.not_empty_iff_size_gt_zero.mp $ (Bool.not_eq_true _).mp h₂ + --have _termination : (List.dropWhile (fun x => x == SpringState.damaged) remainingSpace).length - 1 < remainingSpace.length := by + -- have := List.drop_while_length_le remainingSpace (· == .damaged) + -- omega + let fromOtherPositions := + if mustFirstBeDamaged remainingSpace then + 0 + else + --let remainingSpace := remainingSpace.dropWhile (· == .damaged) --before the damaged group there must be an operational one. + countPossiblePositionsWithDamaged (remainingSpace.drop 1) (g :: gs) h₁ + fromCurrentPosition + fromOtherPositions +termination_by remainingSpace.length + remainingDamagedGroups.length + +def countPossiblePositions (remainingSpace : List SpringState) (remainingDamagedGroups : List Nat) : Nat := + if h : remainingDamagedGroups.isEmpty then + let canAllBeOperational := remainingSpace.all λ + | .operational | .unknown => true + | _ => false + if canAllBeOperational then + 1 + else + 0 + else + countPossiblePositionsWithDamaged remainingSpace remainingDamagedGroups (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h) + + +def part1 (springs : List SpringArrangement) : Nat := + let possiblePositions := springs.map λ{mask, damagedGroups} ↦ countPossiblePositions mask damagedGroups + possiblePositions.foldl (· + ·) 0 + +---------------------------------------------------------------------------------------------------- + +open DayPart +instance : Parse ⟨12, by simp⟩ (ι := List SpringArrangement) where + parse := Except.mapError toString ∘ parse + +instance : Part ⟨12,_⟩ Parts.One (ι := List SpringArrangement) (ρ := Nat) where + run := some ∘ part1 + +---------------------------------------------------------------------------------------------------- + +def testData := "???.### 1,1,3 +.??..??...?##. 1,1,3 +?#?#?#?#?#?#?#? 1,3,1,6 +????.#...#... 4,1,1 +????.######..#####. 1,6,5 +?###???????? 3,2,1" + +#eval parse testData <&> part1 + +def testData2 := "?##?.##???????#??#.. 2,10,1" + +#eval parse testData2 <&> part1 @@ -10,6 +10,7 @@ import «Day8» import «Day9» import «Day10» import «Day11» +import «Day12» open DayPart @@ -44,6 +45,7 @@ def try_run_day_part (day : Days) (part : Parts) (data : String) : IO String := | ⟨10,_⟩, Parts.Two => try_run_day_part_impl ⟨10,_⟩ Parts.Two data | ⟨11,_⟩, Parts.One => try_run_day_part_impl ⟨11,_⟩ Parts.One data | ⟨11,_⟩, Parts.Two => try_run_day_part_impl ⟨11,_⟩ Parts.Two data + | ⟨12,_⟩, Parts.One => try_run_day_part_impl ⟨12,_⟩ Parts.One data | _, _ => throw $ IO.userError "The requested combination of day/part has not been implemented yet." def main (parameters : List String): IO Unit := do |