diff options
| -rw-r--r-- | Common/Parsing.lean | 6 | ||||
| -rw-r--r-- | Common/String.lean | 2 | ||||
| -rw-r--r-- | Common/Substring.lean | 18 | ||||
| -rw-r--r-- | Day1.lean | 2 | ||||
| -rw-r--r-- | Day4.lean | 2 | ||||
| -rw-r--r-- | Day5.lean | 4 | ||||
| -rw-r--r-- | Day6.lean | 2 | ||||
| -rw-r--r-- | Day7.lean | 2 | ||||
| -rw-r--r-- | Day9.lean | 2 | ||||
| -rw-r--r-- | lakefile.lean | 4 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
11 files changed, 23 insertions, 23 deletions
diff --git a/Common/Parsing.lean b/Common/Parsing.lean index ff54ef0..4fb6767 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -134,12 +134,12 @@ protected def RectangularGrid.parseSingleLine (parseCharacter : Char → Except termination_by remainingLine.bsize decreasing_by simp only [Substring.isEmpty, Substring.bsize, Nat.sub_eq, beq_iff_eq] at _h₁ - simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.add_byteIdx, Nat.sub_eq] + simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.Raw.byteIdx_offsetBy, Nat.sub_eq] split case isTrue h₂ => - simp[←(congrArg String.Pos.byteIdx h₂)] at _h₁ + simp[←(congrArg String.Pos.Raw.byteIdx h₂)] at _h₁ case isFalse h₂ => - simp[String.next, Char.utf8Size] + simp[String.Pos.Raw.next, Char.utf8Size] split <;> try split <;> try split all_goals omega diff --git a/Common/String.lean b/Common/String.lean index 3edbd63..955affe 100644 --- a/Common/String.lean +++ b/Common/String.lean @@ -1,6 +1,6 @@ namespace String def splitTrim (c : Char → Bool) (s : String) : List String := - String.trim <$> s.split c + String.trim <$> s.splitToList c def notEmpty : String → Bool := not ∘ isEmpty diff --git a/Common/Substring.lean b/Common/Substring.lean index f51b088..d38c97d 100644 --- a/Common/Substring.lean +++ b/Common/Substring.lean @@ -2,7 +2,7 @@ import Common.Nat namespace Substring -theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos) : s.nextn n p ≥ p := by +theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos.Raw) : s.nextn n p ≥ p := by unfold Substring.nextn cases n case zero => simp @@ -10,16 +10,16 @@ theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos) : s.nextn n p ≥ p simp unfold Substring.next simp - if h₁ :s.startPos + p = s.stopPos then + if h₁ : p.offsetBy s.startPos = s.stopPos then simp[h₁] exact nextn_ge s nn p else simp[h₁] - have h₂ : { byteIdx := (s.str.next (s.startPos + p)).byteIdx - s.startPos.byteIdx : String.Pos} ≤ s.nextn nn { byteIdx := (s.str.next (s.startPos + p)).byteIdx - s.startPos.byteIdx } := + have h₂ : { byteIdx := (String.Pos.Raw.next s.str (p.offsetBy s.startPos)).byteIdx - s.startPos.byteIdx : String.Pos.Raw} ≤ s.nextn nn { byteIdx := (String.Pos.Raw.next s.str (p.offsetBy s.startPos)).byteIdx - s.startPos.byteIdx } := nextn_ge _ nn _ - simp[String.Pos.le_iff] + simp[String.Pos.Raw.le_iff] apply Nat.le_trans _ h₂ - unfold String.next + unfold String.Pos.Raw.next simp[Char.utf8Size] split <;> try split <;> try split all_goals @@ -28,15 +28,15 @@ theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos) : s.nextn n p ≥ p theorem drop_bsize_dec (s : Substring) (n : Nat) (h₁ : ¬s.isEmpty) (h₂ : n ≠ 0) : (s.drop n).bsize < s.bsize := by cases n ; contradiction case succ nn => - simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.add_byteIdx, Nat.sub_eq] + simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.Raw.byteIdx_offsetBy, Nat.sub_eq] simp only [Substring.isEmpty, Substring.bsize, Nat.sub_eq, beq_iff_eq] at h₁ - if h₃ : (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring}.nextn nn (if s.startPos + 0 = s.stopPos then 0 else { byteIdx := (s.str.next (s.startPos + 0)).byteIdx - s.startPos.byteIdx })).byteIdx) ≤ s.stopPos.byteIdx then + if h₃ : (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring}.nextn nn (if String.Pos.Raw.offsetBy 0 s.startPos = s.stopPos then 0 else {byteIdx := (String.Pos.Raw.next s.str (String.Pos.Raw.offsetBy 0 s.startPos)).byteIdx - s.startPos.byteIdx })).byteIdx) ≤ s.stopPos.byteIdx then apply Nat.sub_lt_of_gt; exact h₃ split case h₂.isTrue hx => simp[←hx] at h₁ case h₂.isFalse h₄ => - unfold String.next + unfold String.Pos.Raw.next simp unfold Char.utf8Size simp @@ -45,7 +45,7 @@ theorem drop_bsize_dec (s : Substring) (n : Nat) (h₁ : ¬s.isEmpty) (h₂ : n all_goals simp else - have h₄ : s.stopPos.byteIdx - (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring}.nextn nn (if s.startPos + 0 = s.stopPos then 0 else { byteIdx := (s.str.next (s.startPos + 0)).byteIdx - s.startPos.byteIdx })).byteIdx) = 0 := by + have h₄ : s.stopPos.byteIdx - (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring }.nextn nn (if String.Pos.Raw.offsetBy 0 s.startPos = s.stopPos then 0 else {byteIdx := (String.Pos.Raw.next s.str (String.Pos.Raw.offsetBy 0 s.startPos)).byteIdx - s.startPos.byteIdx })).byteIdx) = 0 := by omega rw[h₄] omega @@ -3,7 +3,7 @@ import Common namespace Day1 def parse (input : String) : List String := - input.split Char.isWhitespace |> List.filter (not ∘ String.isEmpty) + input.splitToList Char.isWhitespace |> List.filter (not ∘ String.isEmpty) -- Both parts could still be improved by doing two searches, one from the left, one from the right @@ -38,7 +38,7 @@ def parse (input : String) : Except String Deck := do let winners := String.trim $ g[0]'(by simp[q]) let draws := String.trim $ g[1]'(by simp[q]) let toNumbers := λ(s : String) ↦ - s.split (·.isWhitespace) + s.splitToList (·.isWhitespace) |> List.filter (not ∘ String.isEmpty) |> List.mapM String.toNat? let winners ← if let some winners := toNumbers winners then pure winners else throw "Failed to parse winning numbers." @@ -110,7 +110,7 @@ structure Almanach where private def parseSeeds (input : String) : Except String (List Seed) := if input.startsWith "seeds: " then let input := input.drop 7 - let input := String.trim <$> input.split Char.isWhitespace + let input := String.trim <$> input.splitToList Char.isWhitespace let numbers := input.mapM String.toNat? let numbers := if let some numbers := numbers then pure numbers else throw s!"Failed to parse a seed number in {input}" List.map NatId.fromNat <$> numbers @@ -118,7 +118,7 @@ private def parseSeeds (input : String) : Except String (List Seed) := throw s!"Seeds line does not start with \"seeds: \": {input}" private def parseMapping {α β : Type} [NatId α] [NatId β] (input : String) : Except String $ Mapping α β := do - let input := String.trim <$> input.split Char.isWhitespace + let input := String.trim <$> input.splitToList Char.isWhitespace let nums ← input.mapM $ (λ o ↦ if let some o := o then pure o else throw s!"Failed to parse mapping {input}, expected number") ∘ String.toNat? match nums with | [a,b,c] => pure $ {inputStart := NatId.fromNat b, outputStart := NatId.fromNat a, length := c} @@ -12,7 +12,7 @@ private def parseLine (header : String) (input : String) : Except String (List N if not $ input.startsWith header then throw s!"Unexpected line header: {header}, {input}" let input := input.drop header.length |> String.trim - let numbers := input.split Char.isWhitespace + let numbers := input.splitToList Char.isWhitespace |> List.map String.trim |> List.filter (not ∘ String.isEmpty) numbers.mapM $ Option.toExcept s!"Failed to parse input line: Not a number {input}" ∘ String.toNat? @@ -109,7 +109,7 @@ structure Player where def parse (input : String) : Except String (List Player) := do let lines := input.splitOn "\n" |> List.map String.trim |> List.filter String.notEmpty let parseLine := λ (line : String) ↦ - if let [hand, bid] := line.split Char.isWhitespace |> List.map String.trim |> List.filter String.notEmpty then + if let [hand, bid] := line.splitToList Char.isWhitespace |> List.map String.trim |> List.filter String.notEmpty then Option.zip (Hand.fromString? hand) (String.toNat? bid) |> Option.map (uncurry Player.mk) |> Option.toExcept s!"Line could not be parsed: {line}" @@ -3,7 +3,7 @@ import «Common» namespace Day9 private def parseLine (line : String) : Except String $ List Int := - line.split Char.isWhitespace + line.splitToList Char.isWhitespace |> List.map String.trim |> List.filter String.notEmpty |> List.mapM String.toInt? diff --git a/lakefile.lean b/lakefile.lean index 1e5c419..25f8d92 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"@"429534106cc509d0fb5b79c67da51b432a798243" + "http://git.grois.info/BinaryHeap"@"75f99635f27dbbedae9769395460b33092180b46" require «lean-astar» from git - "http://git.grois.info/lean-astar"@"088301828d9234c778faac314133922347c0d47f" + "http://git.grois.info/lean-astar"@"d630448964447d0b0953893152873db85db4c9e0" diff --git a/lean-toolchain b/lean-toolchain index 077c4ce..f942ecf 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.24.0 +leanprover/lean4:4.25.0 |