diff options
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/Parsing.lean | 6 | ||||
| -rw-r--r-- | Common/String.lean | 2 | ||||
| -rw-r--r-- | Common/Substring.lean | 18 |
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 |