Lean 4.25feature/day17

3 files changed, 13 insertions, 13 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