diff options
| -rw-r--r-- | Common/List.lean | 12 | ||||
| -rw-r--r-- | Day5.lean | 271 | ||||
| -rw-r--r-- | Main.lean | 2 | ||||
| -rw-r--r-- | inputs/day5.input | 193 | ||||
| -rw-r--r-- | lakefile.lean | 2 |
5 files changed, 475 insertions, 5 deletions
diff --git a/Common/List.lean b/Common/List.lean index 1a76c3e..1d770a8 100644 --- a/Common/List.lean +++ b/Common/List.lean @@ -12,17 +12,19 @@ theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length assumption | true => simp_arith[hi] -def quicksort {α : Type} [Ord α] : List α → List α +def quicksortBy {α : Type} (pred : α → α → Bool): List α → List α | [] => [] | a :: as => - let smallerPred := λ b ↦ Ord.compare b a == Ordering.lt - let largerEqualPred := λ b ↦ Ord.compare b a != Ordering.lt + let smallerPred := λ b ↦ pred b a + let largerEqualPred := not ∘ smallerPred have : List.length (List.filter smallerPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList] have : List.length (List.filter largerEqualPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList] let smallers := as.filter smallerPred let biggers := as.filter largerEqualPred - (quicksort smallers) ++ [a] ++ (quicksort biggers) - termination_by quicksort l => l.length + (quicksortBy pred smallers) ++ [a] ++ (quicksortBy pred biggers) + termination_by quicksortBy pred l => l.length + +def quicksort {α : Type} [Ord α] : List α → List α := quicksortBy λ a b ↦ Ord.compare a b == Ordering.lt /-- Maps a List to another list, but keeps state. The output list is a list of the state, and **has** the initial state diff --git a/Day5.lean b/Day5.lean new file mode 100644 index 0000000..18f9aeb --- /dev/null +++ b/Day5.lean @@ -0,0 +1,271 @@ +import Common.DayPart +import Common.List + +namespace Day5 + +structure Seed where + id : Nat + deriving BEq, Ord, Repr + +structure Soil where + id : Nat + deriving BEq, Ord, Repr + +structure Fertilizer where + id : Nat + deriving BEq, Ord, Repr + +structure Water where + id : Nat + deriving BEq, Ord, Repr + +structure Light where + id : Nat + deriving BEq, Ord, Repr + +structure Temperature where + id : Nat + deriving BEq, Ord, Repr + +structure Humidity where + id : Nat + deriving BEq, Ord, Repr + +structure Location where + id : Nat + deriving BEq, Ord, Repr + +private class NatId (α : Type) where + fromNat : Nat → α + toNat : α → Nat + +private instance : NatId Seed where + fromNat := Seed.mk + toNat := Seed.id + +private instance : NatId Soil where + fromNat := Soil.mk + toNat := Soil.id + +private instance : NatId Fertilizer where + fromNat := Fertilizer.mk + toNat := Fertilizer.id + +private instance : NatId Water where + fromNat := Water.mk + toNat := Water.id + +private instance : NatId Light where + fromNat := Light.mk + toNat := Light.id + +private instance : NatId Temperature where + fromNat := Temperature.mk + toNat := Temperature.id + +private instance : NatId Humidity where + fromNat := Humidity.mk + toNat := Humidity.id + +private instance : NatId Location where + fromNat := Location.mk + toNat := Location.id + +private instance : Min Location where + min a b := if Ord.compare a b == Ordering.lt then a else b + +structure Mapping (α β : Type) where + inputStart : α + outputStart : β + length : Nat + deriving Repr + +structure Mappings (α β : Type) where + mappings : List $ Mapping α β + deriving Repr + +private def Mapping.apply? {α β : Type} [NatId α] [NatId β] (mapping : Mapping α β) (input : α) : Option β := + let input := NatId.toNat input + let fromStart := NatId.toNat mapping.inputStart + let toStart := NatId.toNat mapping.outputStart + if input ≥ fromStart ∧ input < fromStart + mapping.length then + some $ NatId.fromNat $ toStart + input - fromStart + else + none + +private def Mappings.apply {α β : Type} [NatId α] [NatId β] (mappings : Mappings α β) (input : α) : β := + let applied := mappings.mappings.findSome? $ flip Mapping.apply? input + applied.getD $ NatId.fromNat $ NatId.toNat input + +structure Almanach where + seedsToSoil : Mappings Seed Soil + soilToFertilizer : Mappings Soil Fertilizer + fertilizerToWater : Mappings Fertilizer Water + waterToLight : Mappings Water Light + lightToTemperature : Mappings Light Temperature + temperatureToHumidity : Mappings Temperature Humidity + humidityToLocation : Mappings Humidity Location + deriving Repr + +private def parseSeeds (input : String) : Option (List Seed) := + if input.startsWith "seeds: " then + let input := input.drop 7 + let input := String.trim <$> input.split Char.isWhitespace + let numbers := input.mapM String.toNat? + List.map NatId.fromNat <$> numbers + else + none + +private def parseMapping {α β : Type} [NatId α] [NatId β] (input : String) : Option $ Mapping α β := do + let input := String.trim <$> input.split Char.isWhitespace + let nums ← input.mapM String.toNat? + match nums with + | [a,b,c] => some $ {inputStart := NatId.fromNat b, outputStart := NatId.fromNat a, length := c} + | _ => none + +private def parseMappings (α β : Type) [NatId α] [NatId β] (input : String) (header : String) : Option $ Mappings α β := + if input.startsWith header then + let lines := String.trim <$> input.splitOn "\n" |> List.drop 1 |> List.filter (not ∘ String.isEmpty) + let mappings := lines.mapM parseMapping + Mappings.mk <$> mappings + else + none + +def parse (input : String) : Option ((List Seed) × Almanach) := do + let blocks := input.splitOn "\n\n" |> List.filter (not ∘ String.isEmpty) + let blocks := String.trim <$> blocks + if let [seeds, seedToSoil, soilToFertilizer, fertilizerToWater, waterToLight, lightToTemperature, temperatureToHumidity, humidityToLocation] := blocks then + let seeds ← parseSeeds seeds + let seedToSoil ← parseMappings Seed Soil seedToSoil "seed-to-soil map:" + let soilToFertilizer ← parseMappings Soil Fertilizer soilToFertilizer "soil-to-fertilizer map:" + let fertilizerToWater ← parseMappings Fertilizer Water fertilizerToWater "fertilizer-to-water map:" + let waterToLight ← parseMappings Water Light waterToLight "water-to-light map:" + let lightToTemperature ← parseMappings Light Temperature lightToTemperature "light-to-temperature map:" + let temperatureToHumidity ← parseMappings Temperature Humidity temperatureToHumidity "temperature-to-humidity map:" + let humidityToLocation ← parseMappings Humidity Location humidityToLocation "humidity-to-location map:" + (seeds, { + seedsToSoil := seedToSoil + soilToFertilizer := soilToFertilizer + fertilizerToWater := fertilizerToWater + waterToLight := waterToLight + lightToTemperature := lightToTemperature + temperatureToHumidity := temperatureToHumidity + humidityToLocation := humidityToLocation + : Almanach}) + else + none + +def part1 (input : ((List Seed) × Almanach)) : Option Nat := + let a := input.snd + let seedToLocation := a.humidityToLocation.apply + ∘ a.temperatureToHumidity.apply + ∘ a.lightToTemperature.apply + ∘ a.waterToLight.apply + ∘ a.fertilizerToWater.apply + ∘ a.soilToFertilizer.apply + ∘ a.seedsToSoil.apply + let locations := input.fst.map seedToLocation + NatId.toNat <$> locations.minimum? + + +-- Part 2 seems unmanageable by brute force. +-- So, let's rather combine the mappings in a smart way, and then invert them. +-- Then we can do binary search if any seed is in the domain of the combined mapping. +-- if not, the answer is just the smallest seed. + +private def Mappings.combine {α β γ : Type} [NatId α] [NatId β] [NatId γ] (a : Mappings α β) (b : Mappings β γ) : Mappings α γ := + -- the combined mapping contains all ranges in b that aren't "shielded" by ranges of a. + -- then it contains all ranges of a, but their codomain needs to be checked if it overlaps with + -- any ranges in b, and if yes, those ranges need to be split accordingly. + let domain := λ {δ ε : Type} [NatId δ] [NatId ε] (e :Mapping δ ε) ↦ (NatId.toNat e.inputStart, NatId.toNat e.inputStart + e.length) + let codomain := λ {δ ε : Type} [NatId δ] [NatId ε] (e :Mapping δ ε) ↦ (NatId.toNat e.outputStart, NatId.toNat e.outputStart + e.length) + let unshieldedB : List (Mapping α γ) := b.mappings.bind λ bm ↦ + let bmd := domain bm + let bmcd := codomain bm + let shielded := a.mappings.filterMap λ am ↦ + let amd := domain am + let s := Nat.max amd.fst bmd.fst + let e := Nat.min amd.snd bmd.snd + if e > s then some (s,e) else none + -- add a range before and after to shielded, then we can take those between + -- we anyhow need to sort shielded, sooo + let shielded := (bmd.fst, bmd.fst) :: (bmd.snd, bmd.snd) :: shielded + let shielded := shielded.quicksortBy (·.fst < ·.fst) + let rs := shielded.zip (shielded.drop 1) + let rs : List (Nat × Nat):= rs.map λ x ↦ (x.fst.snd, x.snd.fst) + let rs := rs.filter λ l ↦ l.snd > l.fst -- skip emtpy, they are just noise + rs.map λ (x : Nat × Nat) ↦ + let is : α := NatId.fromNat x.fst + let os : γ := NatId.fromNat $ bmcd.fst + x.fst - bmd.fst + let l : Nat := (x.snd - x.fst) + { inputStart := is, outputStart := os, length := l} + --TODO: Unify the onlyAffectedByA and affectedByBoth computations. + let onlyAffectedByA : List (Mapping α γ) := a.mappings.bind λ am ↦ + let amd := domain am + let amcd := codomain am + let overlapping := b.mappings.filterMap λ bm ↦ + let bmd := domain bm + let s := Nat.max amcd.fst bmd.fst + let e := Nat.min amcd.snd bmd.snd + if e > s then some (s,e) else none + -- overlapping is in the **codomain** of a. Transform to domain: + let overlapping := overlapping.map λ p ↦ (p.fst + amd.fst - amcd.fst, p.snd + amd.fst - amcd.fst) + let overlapping := (amd.fst, amd.fst) :: (amd.snd, amd.snd) :: overlapping + let overlapping := overlapping.quicksortBy (·.fst < ·.fst) + let rs := overlapping.zip (overlapping.drop 1) + let rs : List (Nat × Nat):= rs.map λ x ↦ (x.fst.snd, x.snd.fst) + let rs := rs.filter λ l ↦ l.snd > l.fst + rs.map λ (x : Nat × Nat) ↦ + let is : α := NatId.fromNat x.fst + let os : γ := NatId.fromNat $ amcd.fst + x.fst - amd.fst + let l : Nat := (x.snd - x.fst) + { inputStart := is, outputStart := os, length := l} + let affectedByBoth : List (Mapping α γ) := sorry + sorry + + +open DayPart +instance : Parse ⟨5, by simp⟩ (ι := (List Seed) × Almanach) where + parse := parse + +instance : Part ⟨5, _⟩ Parts.One (ι := (List Seed) × Almanach) (ρ := Nat) where + run := part1 + + +private def TestInput := "seeds: 79 14 55 13 + +seed-to-soil map: +50 98 2 +52 50 48 + +soil-to-fertilizer map: +0 15 37 +37 52 2 +39 0 15 + +fertilizer-to-water map: +49 53 8 +0 11 42 +42 0 7 +57 7 4 + +water-to-light map: +88 18 7 +18 25 70 + +light-to-temperature map: +45 77 23 +81 45 19 +68 64 13 + +temperature-to-humidity map: +0 69 1 +1 0 69 + +humidity-to-location map: +60 56 37 +56 93 4 +" + +#eval parse TestInput +#eval parse TestInput >>= part1 @@ -3,6 +3,7 @@ import «Day1» import «Day2» import «Day3» import «Day4» +import «Day5» open DayPart @@ -26,6 +27,7 @@ def try_run_day_part (day : Days) (part : Parts) (data : String) : IO String := | ⟨3,_⟩, Parts.Two => impl ⟨3,_⟩ Parts.Two data | ⟨4,_⟩, Parts.One => impl ⟨4,_⟩ Parts.One data | ⟨4,_⟩, Parts.Two => impl ⟨4,_⟩ Parts.Two data + | ⟨5,_⟩, Parts.One => impl ⟨5,_⟩ 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 diff --git a/inputs/day5.input b/inputs/day5.input new file mode 100644 index 0000000..bf97ee3 --- /dev/null +++ b/inputs/day5.input @@ -0,0 +1,193 @@ +seeds: 2276375722 160148132 3424292843 82110297 1692203766 342813967 3289792522 103516087 2590548294 590357761 1365412380 80084180 3574751516 584781136 4207087048 36194356 1515742281 174009980 6434225 291842774 + +seed-to-soil map: +4170452318 3837406401 124514978 +2212408060 1593776674 105988696 +3837406401 4016132523 278834773 +1475766470 1699765370 492158296 +3698488336 1475766470 118010204 +2318396756 2191923666 46351359 +4116241174 3961921379 54211144 +2193579298 3791037069 18828762 +2364748115 2578360543 354997036 +3085506703 3439828590 106510622 +1967924766 3546339212 219021823 +2719745151 3765361035 25676034 +2745421185 2238275025 340085518 +2186946589 3809865831 6632709 +3192017325 2933357579 506471011 + +soil-to-fertilizer map: +2067774073 3521970321 52706909 +3338663639 285713733 377282283 +4175452431 2125409520 119514865 +3950920796 1900877885 224531635 +285713733 3604616580 690350716 +976064449 3368036703 153933618 +2120480982 662996016 210956413 +2763248642 1355402238 545475647 +3715945922 873952429 49638562 +3765584484 3182700391 185336312 +2331437395 923590991 431811247 +1129998067 2244924385 937776006 +3308724289 3574677230 29939350 + +fertilizer-to-water map: +1898912715 0 159034880 +0 781591504 125461131 +4234890433 2427770485 8749678 +176481534 1845116986 384152450 +822014814 539693831 241897673 +125461131 907052635 47763268 +1476125220 244008638 19613711 +3828547378 4170474998 124492298 +2643114268 2457193301 126243103 +173224399 2229269436 3257135 +2916187764 3376015556 236473226 +764735505 186729329 57279309 +2427770485 3802085897 160735547 +2895514626 2436520163 20673138 +3152660990 2671736916 584987016 +1495738931 1131222975 403173784 +1339983969 1534396759 136141251 +2588506032 3612488782 54608236 +3737648006 2583436404 88300512 +737041056 159034880 27694449 +2057947595 1677521625 167595361 +1063912487 263622349 276071482 +3953039676 4041226796 129248202 +2225542956 1670538010 6983615 +560633984 954815903 176407072 +2847762723 3328263653 47751903 +2769357371 3962821444 78405352 +3825948518 3256723932 2598860 +4082287878 3667097018 134988879 +4243640111 3276936468 51327185 +4217276757 3259322792 17613676 + +water-to-light map: +527906959 2908176499 284796856 +1306013866 0 139756297 +500839409 1466481782 27067550 +1269694476 139756297 36319390 +0 778456518 2402633 +4218077327 4154765934 76889969 +812703815 4004150799 56130996 +153843304 3657154694 8975056 +2402633 905946004 132694584 +3795108796 2776082693 132093806 +3927202602 1422228955 44252827 +1445770163 1493549332 1282533361 +3794865694 780859151 243102 +2728303524 176075687 602380831 +162818360 3666129750 338021049 +3330684355 3319846298 337308396 +4154765934 4231655903 63311393 +135097217 887199917 18746087 +3667992751 3192973355 126872943 +3971455429 781102253 88826366 +1252423178 869928619 17271298 +868834811 1038640588 383588367 + +light-to-temperature map: +2621973104 3678827401 230150807 +1333642604 1531317439 615453278 +3364444750 2854318675 314483239 +2978187907 3908978208 107198609 +1117308885 1110453605 216333719 +1951157390 4016176817 152726483 +4168382203 2717095112 26843204 +0 312822387 5553076 +287414983 245463475 67358912 +1949095882 2597527252 2061508 +3836867339 1522015715 9301724 +648138229 2599588760 117506352 +4132690450 1486323962 35691753 +2852123911 4168903300 126063996 +2468610361 3525464658 153362743 +526108840 988424216 122029389 +5553076 0 148736111 +3265904462 1326787324 98540288 +4195225407 716774234 17303853 +181751976 318375463 105663007 +843084177 3275513023 249951635 +2214264232 734078087 254346129 +154289187 218000686 27462789 +3146382866 684048190 32726044 +765644581 2433292104 77439596 +3179108910 2510731700 86795552 +3846169063 2146770717 286521387 +2103883873 2743938316 110380359 +3085386516 1425327612 60996350 +3678927989 526108840 157939350 +4212529260 3193074987 82438036 +354773895 148736111 69264575 +1093035812 3168801914 24273073 + +temperature-to-humidity map: +1008510114 1939290935 27755995 +2205283444 4197517502 16218189 +1119061522 3123774174 108864966 +1566495924 221087407 33939034 +3089618547 3728555042 25452278 +2341294643 3455988869 16076350 +2286651827 3754007320 54642816 +704748216 2542375745 76754089 +445299830 3938069116 259448386 +1036266109 1300576315 82795413 +178337856 1565003866 40230920 +2122934367 1605234786 81339593 +1484902828 980285858 81593096 +2823460240 1967046930 266158307 +3827446421 1526750766 38253100 +984919715 1161567987 23590399 +218568776 1061878954 99689033 +4049237602 3232639140 223349729 +953670836 2233205237 3881060 +318257809 3472065219 89705062 +1727156113 3113814046 9960128 +3733360236 444372828 94086185 +4272587331 3688491436 22379965 +910921285 178337856 42749551 +781502305 3808650136 129418980 +957551896 2798966448 27367819 +1870217811 1686574379 252716556 +407962871 2998327877 37336959 +2508087592 2826334267 171993610 +1600434958 3561770281 126721155 +3865699521 812829188 167456670 +1737116241 1185158386 115417929 +1852534170 3710871401 17683641 +3420360273 255026441 38629788 +1227926488 2620139318 178827130 +4033156191 4250190027 16081411 +2204273960 2619129834 1009484 +2250197491 4213735691 36454336 +2680081202 1383371728 143379038 +3458990061 538459013 274370175 +3115070825 2237086297 305289448 +2357370993 293656229 150716599 +1406753618 3035664836 78149210 +2221501633 4266271438 28695858 + +humidity-to-location map: +2849843584 4147982382 56632112 +3849085050 3618212322 355529444 +1632881348 407047779 65646492 +3056274757 2246063521 686771203 +2729873863 4028012661 26534599 +3779070915 1543896540 70014135 +2571854216 2932834724 91402738 +2192942437 1028113266 378911779 +2960746591 932585100 95528166 +765942740 0 407047779 +2663256954 1441254676 66616909 +2756408462 4054547260 93435122 +1698527840 1407025045 34229631 +0 3024237462 156854744 +3743045960 1507871585 36024955 +156854744 3181092206 437120116 +1172990519 472694271 459890829 +2906475696 3973741766 54270895 +593974860 2074095641 171967880 +1732757471 1613910675 460184966 diff --git a/lakefile.lean b/lakefile.lean index e9ccab8..a9f27b9 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -13,6 +13,8 @@ lean_lib «Day3» where lean_lib «Day4» where +lean_lib «Day5» where + lean_lib «Common» where @[default_target] |