diff options
| -rw-r--r-- | Common/BitVec.lean | 4 | ||||
| -rw-r--r-- | Common/List.lean | 13 | ||||
| -rw-r--r-- | Common/Parsing.lean | 2 | ||||
| -rw-r--r-- | Day10.lean | 16 | ||||
| -rw-r--r-- | Day13.lean | 2 | ||||
| -rw-r--r-- | Day15.lean | 4 | ||||
| -rw-r--r-- | Day16.lean | 2 | ||||
| -rw-r--r-- | Day8.lean | 8 | ||||
| -rw-r--r-- | Day9.lean | 4 | ||||
| -rw-r--r-- | lakefile.lean | 4 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
11 files changed, 33 insertions, 28 deletions
diff --git a/Common/BitVec.lean b/Common/BitVec.lean index ad46efb..31af340 100644 --- a/Common/BitVec.lean +++ b/Common/BitVec.lean @@ -1,8 +1,8 @@ def BitVec.setBitTrue {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n := - a ||| BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right]) + a ||| BitVec.ofNatLT (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right]) def BitVec.setBitFalse {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n := - a &&& BitVec.not (BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right])) + a &&& BitVec.not (BitVec.ofNatLT (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right])) def BitVec.setBit {n : Nat} (i : Fin n) (v : Bool) (a : BitVec n) : BitVec n := if v then diff --git a/Common/List.lean b/Common/List.lean index 704f8b2..1c8f4a6 100644 --- a/Common/List.lean +++ b/Common/List.lean @@ -10,19 +10,20 @@ theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length simp constructor assumption - | true => simp_arith[hi] + | true => simp[hi] def quicksortBy {α : Type} (pred : α → α → Bool): List α → List α | [] => [] | a :: as => 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 (quicksortBy pred smallers) ++ [a] ++ (quicksortBy pred biggers) termination_by l => l.length + decreasing_by + all_goals + simp +arith only [unattach_filter, unattach_attach, length_cons, gt_iff_lt, listFilterSmallerOrEqualList] def quicksort {α : Type} [Ord α] : List α → List α := quicksortBy λ a b ↦ Ord.compare a b == Ordering.lt @@ -86,7 +87,7 @@ protected theorem length_mapWithProof_Aux {α : Type u} {β : Type v} (list : Li 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) - simp_arith[←hi] + simp +arith[←hi] theorem length_mapWithProof {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list.length = (list.mapWithProof f).length := List.length_mapWithProof_Aux list f [] @@ -95,8 +96,8 @@ theorem mapWithProof_nil {α : Type u} {β : Type v} {f : (e : α) → (e ∈ [] theorem mapWithProof_neNilIffNeNil {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list ≠ [] ↔ (list.mapWithProof f) ≠ [] := ⟨ - λh₁ ↦ List.length_pos.mp $ length_mapWithProof.subst (List.length_pos.mpr h₁), - λh₁ ↦ List.length_pos.mp $ length_mapWithProof.substr (List.length_pos.mpr h₁) + λh₁ ↦ List.length_pos_iff.mp $ length_mapWithProof.subst (List.length_pos_iff.mpr h₁), + λh₁ ↦ List.length_pos_iff.mp $ length_mapWithProof.substr (List.length_pos_iff.mpr h₁) ⟩ theorem map_ne_nil {α : Type u} {β : Type v} {list : List α} {f : α → β} : list ≠ [] ↔ list.map f ≠ [] := diff --git a/Common/Parsing.lean b/Common/Parsing.lean index b1ee779..8237613 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -103,7 +103,7 @@ instance [ToString Element] : ToString (MaybeEmptyRectangularGrid Element) where have : x + e.width *y < e.elements.size := by simp[Membership.mem, inferInstance, Std.instMembershipNatRange] at h₁ h₂ rw[e.size_valid] - exact Nat.two_d_coordinate_to_index_lt_size h₁.right.left h₂.right.left + exact Nat.two_d_coordinate_to_index_lt_size h₁.left h₂.left r := r ++ (ToString.toString e.elements[x+e.width*y]) r @@ -439,16 +439,14 @@ private theorem Except.get_unfold' {α : Type u1} {ε : Type u2} {e : Except ε private theorem Except.get_pure {α : Type u1} (ε : Type u2) (v : α) : Except.get (α := α) (ε := ε) (pure v) (rfl) = v := rfl private theorem Array.getElem!_eq_getElem {α : Type u} [Inhabited α] {a : Array α} {index : Nat} (h : index < a.size ): a[index] = a[index]! := by - unfold getElem getElem! instGetElem?OfGetElemOfDecidable Array.instGetElemNatLtSize decidableGetElem? + unfold getElem getElem! Array.instGetElemNatLtSize Array.instGetElem?NatLtSize Array.get!Internal Array.getInternal Array.getD simp split - <;> rename_i blah - <;> simp[h] at blah - assumption + <;> rfl private theorem Array.get_push {α : Type u} (arr : Array α) (v : α) (index : Nat) (h₁ : index < arr.size) : arr[index] = (arr.push v)[index]'(by simp[Nat.lt_succ.mpr (Nat.le_of_lt h₁)]) := by cases arr - unfold Array.push getElem Array.instGetElemNatLtSize Array.get + unfold Array.push getElem Array.instGetElemNatLtSize simp[List.getElem_append, 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 @@ -537,7 +535,7 @@ private theorem Area.ParseLine_start_at_tile (previous : Area.Raw) (pos : Nat) ( simp[←h₉] assumption case isFalse => - have : (previous.fields.push t).size = previous.width * (previous.height - 1) + (pos + 1) := by simp_arith[h₂] + have : (previous.fields.push t).size = previous.width * (previous.height - 1) + (pos + 1) := by simp +arith[h₂] have h₆ := Area.ParseLine_start_at_tile { width := previous.width, height := previous.height, start := previous.start, fields := previous.fields.push t } (pos + 1) (line.drop 1) h₁ this h₃ h₄ simp[hindex] at h₆ assumption @@ -630,7 +628,7 @@ private theorem Area.ParseRaw_start_position_aux : case isFalse => rw[←hr] at h₁; contradiction case isTrue => rename_i hs _ - have : 0 < (String.splitTrim (fun x => x == '\n') input.trim).length := by let hs := List.isEmpty_eq_false.mpr hs; unfold List.isEmpty at hs; split at hs; contradiction; rename_i hx; simp[hx] + have : 0 < (String.splitTrim (fun x => x == '\n') input.trim).length := by let hs := List.isEmpty_eq_false_iff.mpr hs; unfold List.isEmpty at hs; split at hs; contradiction; rename_i hx; simp[hx] have := Area.ParseLines_start_position { width := (String.splitTrim (fun x => x == '\n') input.trim)[0].length, height := 0, start := none, fields := #[] } (String.splitTrim (fun x => x == '\n') input.trim) (hr.substr h₁) simp at this subst r @@ -1007,7 +1005,11 @@ private def removePathsMet {area : Area} : (List $ Area.PathHead area) → (List termination_by x => x.length decreasing_by all_goals + rw[List.unattach_filter (g := λs ↦ s.current ≠ p.current)] + simp exact Nat.lt_succ.mpr $ List.listFilterSmallerOrEqualList _ _ + intros x xe + simp private def noSolution {area : Area} : (List $ Area.PathHead area) → Bool @@ -51,7 +51,7 @@ match parse input with <;> simp only [Bool.false_eq_true, ↓reduceIte, gt_iff_lt] rw[←List.mapM'_eq_mapM] unfold List.mapM' - have h₂ : (input.toSubstring.splitOn "\n\n") ≠ [] := List.isEmpty_eq_false.mp h₁ + have h₂ : (input.toSubstring.splitOn "\n\n") ≠ [] := List.isEmpty_eq_false_iff.mp h₁ cases h₃ : input.toSubstring.splitOn "\n\n" case false.nil => contradiction case false.cons b bs => @@ -71,7 +71,7 @@ private def HolidayAsciiStringHelperManualArrangementProcedure.empty (α β : Ty private def HolidayAsciiStringHelperManualArrangementProcedure.insert {α β : Type} [HolidayAsciiStringHelperAble α] [BEq α] (label : α) (data : β) (old : HolidayAsciiStringHelperManualArrangementProcedure α β) : HolidayAsciiStringHelperManualArrangementProcedure α β := let h := HolidayAsciiStringHelperAble.holidayAsciiStringHelper label - let index := Fin.cast old.valid.symm h.val + let index := Fin.cast old.valid.symm h.toFin let box := old.boxes[index] let box := updateOrAppend box [] { @@ -90,7 +90,7 @@ where private def HolidayAsciiStringHelperManualArrangementProcedure.remove {α β : Type} [HolidayAsciiStringHelperAble α] [BEq α] (label : α) (old : HolidayAsciiStringHelperManualArrangementProcedure α β) : HolidayAsciiStringHelperManualArrangementProcedure α β := let h := HolidayAsciiStringHelperAble.holidayAsciiStringHelper label - let index := Fin.cast old.valid.symm h.val + let index := Fin.cast old.valid.symm h.toFin let box := old.boxes[index] let box := tryRemove box [] { @@ -170,8 +170,6 @@ private theorem SeenExitDirection.setDirection_increasesCountDirection (a : Seen unfold contains at h₁ simp[countDirection, setDirection, setTop, setLeft, setRight, setBottom, left, right, bottom, top] at h₁ ⊢ simp[h₁, BitVec.setBitTrue, Fin.val_three] - unfold getElem BitVec.instGetElemNatBoolLt BitVec.getLsb' Nat.testBit - simp private structure SeenExitDirections (table : OpticsTable) extends Parsing.RectangularGrid SeenExitDirection where sameWidth : width = table.width @@ -101,7 +101,7 @@ private def pass (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (alread private def part1_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) : Option Nat := let remainingStarts := possibleStarts.filter λs ↦ s != currentPosition - if remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy + if _ht: remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy let passResult := pass waypoints alreadyDoneSteps currentPosition instructions match passResult with | Except.ok n => some n @@ -110,6 +110,8 @@ private def part1_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) ( else none -- walking in circles termination_by possibleStarts.length + decreasing_by + exact _ht open Std in def part1 (input : List Instruction × List Waypoint) : Option Nat := @@ -266,7 +268,7 @@ private def findCyclingGoalsInPathPass (waypoints : Std.HashMap WaypointId Conne private def findCyclingGoalsInPath_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (visitedGoals : List Nat) (visitedStarts : List (WaypointId × Nat)) (currentPosition : WaypointId) (currentSteps : Nat) : List CyclingGoal := let remainingStarts := possibleStarts.filter λs ↦ s != currentPosition - if remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy + if _ht: remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy let visitedStarts := (currentPosition, currentSteps) :: visitedStarts let passResult := findCyclingGoalsInPathPass waypoints currentSteps currentPosition instructions visitedGoals match passResult with @@ -281,6 +283,8 @@ private def findCyclingGoalsInPath_impl (waypoints : Std.HashMap WaypointId Conn else none -- goal was reached before we started to walk in cycles, ignore. termination_by possibleStarts.length + decreasing_by + exact _ht private def findCyclingGoalsInPath (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (startPosition : WaypointId) : List CyclingGoal := findCyclingGoalsInPath_impl waypoints instructions possibleStarts [] [] startPosition 0 @@ -31,8 +31,8 @@ private def extrapolate : List Int → Int 0 else have : (differences (a :: as)).length < as.length + 1 := by - simp_arith[differences] - induction (as) <;> simp_arith[differences] + simp +arith[differences] + induction (as) <;> simp +arith[differences] case cons b bs hb => rw[←differences_length_independent_arg] assumption a + extrapolate (differences (a :: as)) diff --git a/lakefile.lean b/lakefile.lean index a155aab..3775d13 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -32,7 +32,7 @@ lean_exe «aoc-2023» where supportInterpreter := true require BinaryHeap from git - "https://github.com/soulsource/BinaryHeap"@"7896480adb78fc9f9b7a86a5eddd0fc5e3f9e4d5" + "http://git.grois.info/BinaryHeap"@"60832223e03e50cbffca8bc90b1dec40b48f1f14" require «lean-astar» from git - "https://github.com/soulsource/lean-astar"@"dee1a274a1c625462de03b58eaeff82e5db8b830" + "http://git.grois.info/lean-astar"@"2402a88a863e41f5bceefcdc13323ef609809a8a" diff --git a/lean-toolchain b/lean-toolchain index db29c97..9f78e65 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.17.0 +leanprover/lean4:4.18.0 |