diff options
| -rw-r--r-- | Common/List.lean | 2 | ||||
| -rw-r--r-- | Common/Parsing.lean | 2 | ||||
| -rw-r--r-- | Day10.lean | 15 | ||||
| -rw-r--r-- | Day14.lean | 6 | ||||
| -rw-r--r-- | Day16.lean | 2 | ||||
| -rw-r--r-- | Day9.lean | 2 | ||||
| -rw-r--r-- | lakefile.lean | 4 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
8 files changed, 17 insertions, 18 deletions
diff --git a/Common/List.lean b/Common/List.lean index f6c0de5..9db3b86 100644 --- a/Common/List.lean +++ b/Common/List.lean @@ -23,7 +23,7 @@ def quicksortBy {α : Type} (pred : α → α → Bool): List α → List α termination_by l => l.length decreasing_by all_goals - simp +arith only [unattach_filter, unattach_attach, length_cons, gt_iff_lt, listFilterSmallerOrEqualList] + simp +arith only [unattach_filter, unattach_attach, length_cons, listFilterSmallerOrEqualList] def quicksort {α : Type} [Ord α] : List α → List α := quicksortBy λ a b ↦ Ord.compare a b == Ordering.lt diff --git a/Common/Parsing.lean b/Common/Parsing.lean index 7834e00..ff54ef0 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -101,7 +101,7 @@ instance [ToString Element] : ToString (MaybeEmptyRectangularGrid Element) where r := r.push '\n' for h₁ : x in [0:e.width] do have : x + e.width *y < e.elements.size := by - simp[Membership.mem, inferInstance, Std.instMembershipNatRange] at h₁ h₂ + simp[Membership.mem] at h₁ h₂ rw[e.size_valid] exact Nat.two_d_coordinate_to_index_lt_size h₁.left h₂.left r := r ++ (ToString.toString e.elements[x+e.width*y]) @@ -266,7 +266,7 @@ private theorem Area.ParseLine_adds_returned_count (previous : Area.Raw) (pos : unfold bind Monad.toBind Except.instMonad at h₃ simp at h₃ cases h₄ : (Day10.Area.parseLine.parseCharacter line.front) - <;> simp[h₄, Option.toExcept, Except.bind] at h₃ + <;> simp[h₄, Except.bind] at h₃ case error => rw[←h₃] at h₂; contradiction case ok => split at h₃ @@ -318,7 +318,7 @@ private theorem Area.ParseLine_leaves_width_and_height (previous : Area.Raw) (po unfold bind Monad.toBind Except.instMonad at h₃ simp at h₃ cases h₄ : (Day10.Area.parseLine.parseCharacter line.front) - <;> simp[h₄, Option.toExcept, Except.bind] at h₃ + <;> simp[h₄, Except.bind] at h₃ case error => rw[←h₃] at h₂; contradiction case ok => split at h₃ @@ -448,7 +448,7 @@ private theorem Array.get_push {α : Type u} (arr : Array α) (v : α) (index : cases arr unfold Array.push getElem Array.instGetElemNatLtSize simp only [List.size_toArray] at h₁ - simp[List.getElem_append, h₁] + simp[h₁] private theorem Area.ParseLine_leaves_start_if_some (previous : Area.Raw) (pos : Nat) (line : Substring) (h₁ : previous.height > 0) {res : (Nat × Area.Raw)} (h₂ : (Area.parseLine previous pos line h₁) = Except.ok res) (h₃ : previous.start.isSome) : Fin.val <$> res.2.start = Fin.val <$> previous.start := by unfold Area.parseLine at h₂ @@ -488,7 +488,6 @@ private theorem Area.ParseLine_only_adds_to_fields (previous : Area.Raw) (pos : simp at h₅ rw[←h₅] have h₆ : ↑index < (previous.fields.push tile).size := by simp; exact Nat.lt_succ.mpr (Nat.le_of_lt index.isLt) - simp[←Array.getElem!_eq_getElem] simp[←Array.getElem!_eq_getElem h₆] apply Array.get_push termination_by previous.width - pos @@ -682,7 +681,7 @@ private def Area.parse (input : String) : Except Area.ParseError Area := rw[Except.get_unfold'] exact he have sp : vraw.fields[(Coordinate.fromIndex s).toIndex] = Tile.start := by - simp[Except.get_unfold' he except_ok] at sp + simp at sp simp[Coordinate.toIndex_inv_fromIndex] rw[Array.getElem!_eq_getElem] at sp ⊢ have : ((Day10.Except.get (Day10.Area.parseRaw input) _).start.get is_some).val = s.val := by @@ -1286,13 +1285,13 @@ private theorem Area.PathsPart.join_a_last_last (a b : area.PathsPart) (h₁ : a generalize h₂ : (Day10.Area.PathsPart.join area a b h₁) = o unfold Area.PathsPart.join at h₂ split at h₂ - case h_1 bh ah as _ _ h₄ h₃ _ _ _ _ hb ha _ _ _ _ => - simp[hb, ←h₂, ←ha] + case h_1 bh ah as _ _ h₄ h₃ _ _ _ _ _ ha _ _ _ _ => + simp[←h₂, ←ha] apply List.getLast_cons case h_2 bh b1 bs ah as _ _ h₄ h₃ d4 d3 d2 d1 hb ha d5 d6 d7 d8 => clear d1 d2 d3 d4 d5 d6 d7 d8 simp only at h₂ - simp[hb, ←h₂, ←ha] + simp[←h₂, ←ha] rw[←List.getLast_cons (a := bh) a.list_not_empty] have : bs.length + 1 < b.steps.length := by simp only [hb, List.length_cons, Nat.lt_add_one] apply Area.PathsPart.join_a_last_last @@ -211,11 +211,11 @@ private def compareControlPanels (a b : ControlPanel) : Bool := /-- (Bad) Hash-Function for ControlPanel. It's good enough for this riddle, but that's about it. -/ private def hashControlPanel (p : ControlPanel) : UInt64 := Id.run do - let mut hash : UInt64 := mixHash ⟨Fin.ofNat' UInt64.size p.width⟩ ⟨Fin.ofNat' UInt64.size p.height⟩ + let mut hash : UInt64 := mixHash ⟨Fin.ofNat UInt64.size p.width⟩ ⟨Fin.ofNat UInt64.size p.height⟩ for hi : index in [:p.elements.size] do match p.elements[index] with - | Tile.Round => hash := mixHash hash ⟨Fin.ofNat' UInt64.size index⟩ - | Tile.Cube => hash := mixHash hash ⟨Fin.ofNat' UInt64.size (index + p.elements.size)⟩ + | Tile.Round => hash := mixHash hash ⟨Fin.ofNat UInt64.size index⟩ + | Tile.Cube => hash := mixHash hash ⟨Fin.ofNat UInt64.size (index + p.elements.size)⟩ | Tile.Space => continue hash @@ -300,7 +300,7 @@ private theorem OpticsTable.findFirstExitDirectionNotSeenInQueue_notContains {ta have h₂ := Option.some.inj h₁ subst result generalize { x := Fin.cast _ b.snd.x, y := Fin.cast _ b.snd.y : seenDirections.Coordinate } = c at * - have h₂ : ed ∈ List.filter (fun d => !seenDirections.toRectangularGrid[c].contains d) (OpticsElement.outputDirections table[b.snd] b.fst) := by simp only [heq, List.mem_singleton, List.mem_cons, true_or] + have h₂ : ed ∈ List.filter (fun d => !seenDirections.toRectangularGrid[c].contains d) (OpticsElement.outputDirections table[b.snd] b.fst) := by simp only [heq, List.mem_cons, true_or] exact (Bool.not_eq_true' _).mp (List.mem_filter.mp h₂).right private def OpticsTable.followPath {table : OpticsTable} (seenDirections : SeenExitDirections table) (beams : List (EnterDirection × table.Coordinate)) : SeenExitDirections table := @@ -31,7 +31,7 @@ private def extrapolate : List Int → Int 0 else have : (differences (a :: as)).length < as.length + 1 := by - simp +arith[differences] + simp +arith induction (as) <;> simp +arith[differences] case cons b bs hb => rw[←differences_length_independent_arg] assumption diff --git a/lakefile.lean b/lakefile.lean index e89dba4..3e1521b 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"@"ff5c64836ede27d87dbc56b3869021ad8b0d255b" + "http://git.grois.info/BinaryHeap"@"90a0fee45356cf5a1a4d29214c7f0f115fddbf23" require «lean-astar» from git - "http://git.grois.info/lean-astar"@"2539ac49ab6af74b31d91e03d7dbfceedc9c1f02" + "http://git.grois.info/lean-astar"@"7480e42e0a7ef6631b01fb7208b2b3b9c7fcc354" diff --git a/lean-toolchain b/lean-toolchain index 893a7f3..f434439 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.21.0 +leanprover/lean4:4.23.0 |