diff options
| -rw-r--r-- | Common/List.lean | 6 | ||||
| -rw-r--r-- | Common/Parsing.lean | 2 | ||||
| -rw-r--r-- | Day10.lean | 6 | ||||
| -rw-r--r-- | Day12.lean | 2 | ||||
| -rw-r--r-- | Day13.lean | 2 | ||||
| -rw-r--r-- | Day15.lean | 8 | ||||
| -rw-r--r-- | Day16.lean | 4 | ||||
| -rw-r--r-- | Day3.lean | 2 | ||||
| -rw-r--r-- | Day8.lean | 2 | ||||
| -rw-r--r-- | lakefile.lean | 4 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
11 files changed, 20 insertions, 20 deletions
diff --git a/Common/List.lean b/Common/List.lean index 1c8f4a6..f6c0de5 100644 --- a/Common/List.lean +++ b/Common/List.lean @@ -54,7 +54,7 @@ instance {α : Type} [Ord α] : Ord (List α) where def not_empty_iff_size_gt_zero {list : List α} : list.isEmpty = false ↔ list.length > 0 := match list with | [] => ⟨nofun, nofun⟩ - | l :: ls => ⟨λ_ ↦ (List.length_cons l ls).substr (Nat.succ_pos ls.length), λ_ => rfl⟩ + | _l :: ls => ⟨λ_ ↦ (List.length_cons).substr (Nat.succ_pos ls.length), λ_ => rfl⟩ def ne_nil_of_not_empty {list : List α} : list.isEmpty = false ↔ list ≠ [] := match list with @@ -79,14 +79,14 @@ where | [], _, bs => bs.reverse | a :: as, f, bs => let g : (e : α) → (e ∈ as) → β := λ e h ↦ f e (List.mem_cons_of_mem a h) - worker as g (f a (List.mem_cons_self _ _) :: bs) + worker as g (f a (List.mem_cons_self) :: bs) protected theorem length_mapWithProof_Aux {α : Type u} {β : Type v} (list : List α) (f : (e : α) → (e ∈ list) → β) (acc : List β) : list.length + acc.length = (List.mapWithProof.worker list f acc).length := by induction list generalizing acc case nil => unfold mapWithProof.worker; simp only [length_nil, Nat.zero_add, length_reverse] case cons l ls hi => unfold mapWithProof.worker - have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self _ _) :: acc) + have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self) :: acc) simp +arith[←hi] theorem length_mapWithProof {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list.length = (list.mapWithProof f).length := diff --git a/Common/Parsing.lean b/Common/Parsing.lean index 8237613..7834e00 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -88,7 +88,7 @@ def RectangularGrid.set {grid : RectangularGrid Element} (coordinate : grid.Coor { grid with elements := grid.elements.set index value - size_valid := (grid.elements.size_set index value index.isLt).substr grid.size_valid + size_valid := (grid.elements.size_set index.isLt).substr grid.size_valid } theorem RectangularGrid.set_same_size {grid : RectangularGrid Element} (coordinate : grid.Coordinate) (value : Element) : (grid.set coordinate value).width = grid.width ∧ (grid.set coordinate value).height = grid.height := @@ -515,7 +515,7 @@ private theorem Area.ParseLine_start_at_tile (previous : Area.Raw) (pos : Nat) ( split at h₄; contradiction case isFalse h₇ => have h₈ : (previous.fields.push t)[previous.width * (previous.height - 1) + pos]! = t := by - have := Array.getElem_push_eq previous.fields t + have : (previous.fields.push t)[previous.fields.size] = t := Array.getElem_push_eq simp[h₂, Array.getElem!_eq_getElem] at this assumption have : t = Tile.start := beq_iff_eq.mp h₆ @@ -1060,7 +1060,7 @@ private theorem Area.PathsPart.tail_connect_start {area : Area} (pp : area.Paths match hs : pp.steps, pp.list_not_empty, pp.connected with | _ :: [], _, h₁ => h₁ | s :: ss :: sss, _, ⟨_,h₂⟩ => - have : (ss :: sss).length < pp.steps.length := hs.substr $ (List.length_cons s (ss :: sss)).substr $ Nat.lt.base (ss :: sss).length + have : (ss :: sss).length < pp.steps.length := hs.substr $ (List.length_cons).substr $ Nat.lt.base (ss :: sss).length Area.PathsPart.tail_connect_start ⟨ss::sss,h₂⟩ termination_by pp.steps.length @@ -1558,7 +1558,7 @@ where let ⟨(_ : t ≠ Tile.ground), (_ : t ≠ Tile.start)⟩ := Area.can_connect_to_imp_not_start_not_ground s_connects_to_ss.left match t with | Tile.pipe p => - have : (ss :: sss).length < pp.steps.length := hs.substr $ (List.length_cons s (ss :: sss)).substr $ Nat.lt_add_one (ss :: sss).length + have : (ss :: sss).length < pp.steps.length := hs.substr $ (List.length_cons).substr $ Nat.lt_add_one (ss :: sss).length worker { steps := ss :: sss, connected := rest_is_connected } $ {coordinate := s, pipe :=p} :: o termination_by x => x.steps.length worker cp.toPathsPart [] @@ -161,7 +161,7 @@ def countPossiblePositions (remainingSpace : List SpringState) (remainingDamaged else 0 else - Prod.snd $ countPossiblePositionsWithDamagedMemoized Std.HashMap.empty remainingSpace remainingDamagedGroups (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h) + Prod.snd $ countPossiblePositionsWithDamagedMemoized Std.HashMap.emptyWithCapacity remainingSpace remainingDamagedGroups (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h) def part1 (springs : List SpringArrangement) : Nat := @@ -62,7 +62,7 @@ match parse input with cases List.mapM' (Parsing.RectangularGrid.ofSubstring Day13.Tile.ofChar?) bs case error e => exact True.intro case ok ts => - have h₄ := List.length_cons t ts + have h₄ : (t :: ts).length = ts.length + 1 := List.length_cons unfold bind Monad.toBind Except.instMonad simp only [Except.bind, Except.map, h₄, Nat.zero_lt_succ] @@ -65,8 +65,8 @@ private structure HolidayAsciiStringHelperManualArrangementProcedure (α β : Ty private def HolidayAsciiStringHelperManualArrangementProcedure.empty (α β : Type) : HolidayAsciiStringHelperManualArrangementProcedure α β := { - boxes := Array.mkArray UInt8.size [], - valid := Array.size_mkArray _ _ + boxes := Array.replicate UInt8.size [], + valid := Array.size_replicate } private def HolidayAsciiStringHelperManualArrangementProcedure.insert {α β : Type} [HolidayAsciiStringHelperAble α] [BEq α] (label : α) (data : β) (old : HolidayAsciiStringHelperManualArrangementProcedure α β) : HolidayAsciiStringHelperManualArrangementProcedure α β := @@ -76,7 +76,7 @@ private def HolidayAsciiStringHelperManualArrangementProcedure.insert {α β : T let box := updateOrAppend box [] { boxes := old.boxes.set index box - valid := (Array.size_set old.boxes index box index.isLt).substr old.valid + valid := (Array.size_set index.isLt).substr old.valid } where updateOrAppend (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) := @@ -95,7 +95,7 @@ private def HolidayAsciiStringHelperManualArrangementProcedure.remove {α β : T let box := tryRemove box [] { boxes := old.boxes.set index box - valid := (Array.size_set old.boxes index box index.isLt).substr old.valid + valid := (Array.size_set index.isLt).substr old.valid } where tryRemove (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) := @@ -197,9 +197,9 @@ private def SeenExitDirections.empty (table : OpticsTable) : SeenExitDirections { width := table.width height := table.height - elements := Array.mkArray (table.width * table.height) default + elements := Array.replicate (table.width * table.height) default not_empty := table.not_empty - size_valid := Array.size_mkArray _ _ + size_valid := Array.size_replicate sameHeight := rfl sameWidth := rfl } @@ -92,7 +92,7 @@ def parse (schematic : String) : Except String Schematic := do def part1 (schematic : Schematic) : Nat := -- fast lookup: We need to know if a part is at a given coordinate open Std(HashSet) in - let partCoordinates := HashSet.insertMany HashSet.empty $ schematic.parts.map Part.position + let partCoordinates := HashSet.insertMany HashSet.emptyWithCapacity $ schematic.parts.map Part.position let partNumbers := schematic.numbers.filter λnumber ↦ number.positions.any λposition ↦ position.adjacents.any partCoordinates.contains @@ -50,7 +50,7 @@ private def parseWaypoints (input : List String) : Except String $ List Waypoint open Std in private def validateWaypointLinks (waypoints : List Waypoint) : Bool := - let validLinks := HashSet.insertMany HashSet.empty $ waypoints.map Waypoint.id + let validLinks := HashSet.insertMany HashSet.emptyWithCapacity $ waypoints.map Waypoint.id waypoints.all λw ↦ validLinks.contains w.left && validLinks.contains w.right def target : WaypointId := "ZZZ" diff --git a/lakefile.lean b/lakefile.lean index 3775d13..cd9af36 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -32,7 +32,7 @@ lean_exe «aoc-2023» where supportInterpreter := true require BinaryHeap from git - "http://git.grois.info/BinaryHeap"@"60832223e03e50cbffca8bc90b1dec40b48f1f14" + "http://git.grois.info/BinaryHeap"@"93c883d5332469d90a4f1c42d45c66e2b6a89eb8" require «lean-astar» from git - "http://git.grois.info/lean-astar"@"2402a88a863e41f5bceefcdc13323ef609809a8a" + "http://git.grois.info/lean-astar"@"973225b1c5ed10f2a99374c91a9d6a957067f654" diff --git a/lean-toolchain b/lean-toolchain index 9f78e65..a0922e9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.18.0 +leanprover/lean4:4.19.0 |