feat: update to v4.10.0

Author: bergmannjg

Regex/Backtrack.lean

@@ -93,7 +93,7 @@ def next (cp : CharPos) : CharPos :=
   else
     match cp.curr? with
     | some c =>
-      let nextPos : String.Pos := ⟨cp.pos.byteIdx + (String.csize c)⟩
+      let nextPos : String.Pos := ⟨cp.pos.byteIdx + c.utf8Size⟩
       {cp with pos := nextPos, prev? := cp.curr?, curr? := get? cp.s nextPos}
     | none => cp
 
@@ -1067,9 +1067,9 @@ private def slotsWithUnanchoredPrefix (s : Substring) («at» : String.Pos) (nfa
     match (msgs, slots) with
     | (msgs, #[]) =>
       let c : Char := s.get «at»
-      let size := c.utf8Size.toNat
+      let size := c.utf8Size
       have : s.stopPos.byteIdx - (at.byteIdx + size) < s.stopPos.byteIdx - at.byteIdx := by
-        have  : 0 < c.utf8Size.toNat := Char.utf8Size_pos c
+        have  : 0 < c.utf8Size := Char.utf8Size_pos c
         have ha : at.byteIdx < s.stopPos.byteIdx := by omega
         have hb : at.byteIdx < at.byteIdx + size := by omega
         simp [Nat.sub_lt_sub_left ha hb]

Regex/Data/Array/Lemmas.lean

@@ -77,8 +77,8 @@ theorem last?_eq_getLast (a : Array α) (h1: Array.last? a = some last) (h2 : a.
     : List.getLast a.data h2 = last := by
   unfold Array.last? at h1
   split at h1 <;> simp_all
-  rw [← List.getLast_eq_get a.data h2] at h1
-  simp [h1]
+  rw [← h1]
+  simp [List.getLast_eq_get a.data h2]
 
 theorem lt_of_pop?_eq_last? {arr : Array α} (h : Array.pop? arr = some (last, arr'))
     : 0 < arr.data.length := by
@@ -94,7 +94,7 @@ theorem get_last_of_pop? {arr : Array α} (h1 : Array.pop? arr = some (last, arr
 theorem concat_of_pop? {arr : Array α} (h : Array.pop? arr = some (last, arr'))
     : arr.data = arr'.data ++ [last] := by
   have hlt : 0 < arr.data.length := by simp_all[Array.lt_of_pop?_eq_last? h]
-  have hlt : arr.data.length - 1 < arr.data.length := Nat.pred_lt' hlt
+  have hlt : arr.data.length - 1 < arr.data.length := Nat.pred_lt_of_lt hlt
   have hlast : List.get arr.data ⟨arr.data.length - 1, hlt⟩ = last :=
      Array.get_last_of_pop? h hlt
   unfold Array.pop? at h
@@ -108,4 +108,4 @@ theorem concat_of_pop? {arr : Array α} (h : Array.pop? arr = some (last, arr'))
     rw [← hy] at hr
     rw [hr]
   simp [List.eq_of_dropLast_eq_last_eq hz hlt (by simp_all)
-          (by rw [List.get_last_of_concat _]; rw [hlast])]
+          (by rw [List.get_last_of_concat _]; rw [← hlast]; simp_all)]

Regex/Data/List/Lemmas.lean

@@ -10,10 +10,7 @@ namespace List
 
 theorem singleton_val_of (a : α) (arr : List α) (h1 : arr = [a]) (h2 : 0 < List.length arr)
     : List.get arr ⟨0, h2⟩ = a  := by
-  unfold List.get
-  split <;> simp_all
-  unfold List.get
-  split <;> simp_all
+  simp_all [List.get]
 
 theorem singleton_val (a : α) (h : 0 < List.length [a])
     : List.get [a] ⟨0, h⟩ = a  := by
@@ -37,8 +34,8 @@ theorem eq_of_dropLast_eq_last_eq {l1 l2 : List α} (hd : List.dropLast l1 = Lis
   List.ext_get hl fun n h1 h2 =>
     if hx1 : n < l1.dropLast.length then by
       have hx2 : n < l2.dropLast.length := Nat.lt_of_lt_of_eq hx1 hdl
-      have hy1 : l1.dropLast.get ⟨n, hx1⟩ = l1.get ⟨n, h1⟩ := List.get_dropLast l1 ⟨n, hx1⟩
-      have hy2 : l2.dropLast.get ⟨n, hx2⟩ = l2.get ⟨n, h2⟩ := List.get_dropLast l2 ⟨n, hx2⟩
+      have hy1 : l1.dropLast.get ⟨n, hx1⟩ = l1.get ⟨n, h1⟩ := List.getElem_dropLast l1 n hx1
+      have hy2 : l2.dropLast.get ⟨n, hx2⟩ = l2.get ⟨n, h2⟩ := List.getElem_dropLast l2 n hx2
       have hy3 : l1.dropLast.get ⟨n, hx1⟩ = l2.dropLast.get ⟨n, hx2⟩ := List.get_of_fun_eq hd ⟨n, hx1⟩
       rw [hy3, hy2] at hy1
       rw [hy1]
@@ -59,6 +56,22 @@ theorem get_last_of_concat {l : List α} (h : (l ++ [last]).length - 1 < (l ++ [
     : List.get (l ++ [last]) ⟨(l ++ [last]).length - 1, h⟩ = last  := by
   simp [List.get_last _]
 
+theorem eq_succ_of_tail_nth {head : α} {tail : List α} (data : List α) (h1 : n+1 < data.length)
+  (h2 : data = head :: tail) (h3 : n < tail.length)
+    : tail.get ⟨n, h3⟩ = data.get ⟨n+1, h1⟩ := by
+  cases h2
+  have h : (head :: tail).get ⟨n+1, h1⟩ = tail.get ⟨n, h3⟩ := List.get_cons_succ
+  exact h.symm
+
+theorem eq_succ_of_tail_nth_pred {head : α} {tail : List α} (data : List α) (h0 : n ≠ 0)
+  (h1 : n < data.length) (h2 : data = head :: tail) (h3 : n - 1 < tail.length)
+    : tail.get ⟨n - 1, h3⟩ = data.get ⟨n, h1⟩ := by
+  have hps : n - 1 + 1 = n := Nat.succ_pred (by simp_all)
+  have hpl : n - 1 + 1 < data.length := by simp only [hps, h1]
+  have : data.get ⟨n, h1⟩ = data.get ⟨n - 1 + 1, hpl⟩ := by simp_all
+  rw [this]
+  exact List.eq_succ_of_tail_nth data hpl h2 h3
+
 /- see Mathlib/Data/List/Chain.lean -/
 theorem chain_split {a b : α} {l₁ l₂ : List α} :
     Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂ := by
@@ -86,7 +99,7 @@ theorem chain_iff_get {R} : ∀ {a : α} {l : List α}, Chain R a l ↔
         exact R
       intro i w
       cases i
-      · simp [h0]
+      · apply h0
       · rename_i i
         exact h i (by simp only [length_cons] at w; omega)
     rintro ⟨h0, h⟩; constructor

Regex/Data/UInt/Basic.lean

@@ -70,6 +70,9 @@ theorem toNat_sub_toNat {n m : UInt32} (hmn : m.val ≤ n.val) (h2 : n.val < UIn
   have h : (n.val.val + (UInt32.size - m.val.val)) % UInt32.size
             = n.val.val - m.val.val := Nat.mod_sub_eq_of_lt hmn h1 (Nat.le_of_lt h2)
   simp [h]
+  have : n.val.val + (UInt32.size - m.val.val) = (UInt32.size - m.val.val) +  n.val.val := by simp_arith
+  rw [← this]
+  simp [h]
 
 theorem toUInt32_add_toUInt32 (n m : Nat) (hn : n < UInt32.size) (hm : m < UInt32.size)
   (hnm : n + m < UInt32.size) : n.toUInt32 + m.toUInt32 = (n + m).toUInt32 := by

Regex/Interval/Lemmas.lean

@@ -128,7 +128,6 @@ theorem nonOverlappingWithLast_of_singleton (l r : NonemptyInterval Char) (h : I
   split at heq <;> simp_all
   unfold Interval.nonOverlapping  at h
   rename_i last' _ _ _
-  have heq' : List.get #[l].data ⟨0, by simp⟩ = l := List.singleton_val l (by simp)
   simp_all
 
 theorem nonOverlapping_of_push (acc : Acc) (next : NonemptyInterval Char)
@@ -182,18 +181,6 @@ theorem Array.eq_head_of_get_first (arr : Array α) (h1 : 0 < arr.size)
   (h2 : arr.data = head :: tail) : head = arr.get ⟨0, h1⟩ :=
   List.eq_head_of_get_first arr.data h1 h2
 
-theorem List.eq_succ_of_tail_nth (arr : List α) (h1 : i+1 < arr.length)
-  (h2 : arr = head :: tail) (h3 : i < tail.length)
-    : tail.get ⟨i, h3⟩ = arr.get ⟨i+1, h1⟩ := by
-  cases h2
-  have h : (head :: tail).get ⟨i+1, h1⟩ = tail.get ⟨i, h3⟩ := List.get_cons_succ
-  exact h.symm
-
-theorem Array.eq_succ_of_tail_nth (arr : Array α) (h1 : i+1 < arr.size)
-  (h2 : arr.data = head :: tail) (h3 : i < tail.length)
-    : tail.get ⟨i, h3⟩ = arr.get ⟨i+1, h1⟩ :=
-  List.eq_succ_of_tail_nth arr.data h1 h2 h3
-
 theorem nonOverlapping_of_nth (ranges : Array $ NonemptyInterval Char) (n : Nat)
   (h1 : 0 < n) (h2 : n+1 < Array.size ranges) (h3: ranges.data = head :: tail)
   (h4 : ∀ (i : Nat) (h : i < List.length tail-1),
@@ -211,18 +198,10 @@ theorem nonOverlapping_of_nth (ranges : Array $ NonemptyInterval Char) (n : Nat)
   have ht2 : n-1 < tail.length := by omega
   have ht3 : n-1+1 < tail.length := by simp [hps, ht0]
   have : Interval.nonOverlapping (tail.get ⟨n-1, ht2⟩) (tail.get ⟨n-1+1, ht3⟩) := h4 (n-1) ht1
-  have : tail.get ⟨n-1, ht2⟩ = ranges.get ⟨n, hlt⟩ := by
-    let i := n-1
-    have h : i+1 < ranges.size := by simp [hps, hlt]
-    simp [Array.eq_succ_of_tail_nth ranges h h3 ht2]
-    simp [hps]
-  have : tail.get ⟨n-1+1, ht3⟩ = ranges.get ⟨n+1, hf⟩ := by
-    let i := n-1+1
-    have hi : i = n-1+1 := by simp
-    have hi' : i = n := by simp_all only [hi]
-    have h : i < tail.length := by simp_all [hps, ht0]
-    simp [Array.eq_succ_of_tail_nth ranges (by rw [← hi'] at hf; simp_all) h3 h]
-    simp_all [hps]
+  have : tail.get ⟨n-1, ht2⟩ = ranges.get ⟨n, hlt⟩ :=
+    List.eq_succ_of_tail_nth_pred ranges.data hne hlt h3 ht2
+  have : tail.get ⟨n, ht0⟩ = ranges.get ⟨n+1, hf⟩ :=
+    List.eq_succ_of_tail_nth ranges.data (by simp [h2]) h3 ht0
   simp_all
 
 theorem nonOverlapping_of_pred (ranges : Array $ NonemptyInterval Char) (i : Fin (Array.size ranges))
@@ -250,7 +229,7 @@ theorem nonOverlapping_of_pred (ranges : Array $ NonemptyInterval Char) (i : Fin
       have hx1 : 0 < ranges.size := by simp [Nat.lt_trans h hf]
       have hx2 : 0 < tail.length := by cases tail <;> simp_all
       have : head = ranges.get ⟨0, hx1⟩  := Array.eq_head_of_get_first ranges hx1 heq
-      have : tail.get ⟨0, hx2⟩  = ranges.get ⟨1, hf⟩ := Array.eq_succ_of_tail_nth ranges hf heq hx2
+      have : tail.get ⟨0, hx2⟩  = ranges.get ⟨1, hf⟩ := List.eq_succ_of_tail_nth ranges.data hf heq hx2
       simp_all
     | ⟨n+2, hf⟩ =>
       have hx1 : n+1 < ranges.size := by simp [Nat.lt_trans _ hf]
@@ -266,16 +245,3 @@ theorem nonOverlappingWithLast_of_push(acc : Acc)
   rename_i last next heq _
   unfold Array.last? at heq
   split at heq <;> try simp_all
-  have hne : acc.set.intervals.data ++ [l] ≠ [] := by simp_all
-  have h : List.getLast (acc.set.intervals.data ++ [l]) hne
-    = List.get (acc.set.intervals.data ++ [l]) ⟨acc.set.intervals.data.length, (by simp_all)⟩ := by
-    have h : List.get (acc.set.intervals.data ++ [l]) ⟨acc.set.intervals.data.length, (by simp_all)⟩
-            = List.get (acc.set.intervals.data ++ [l])
-                ⟨(acc.set.intervals.data ++ [l]).length-1, (by simp_all)⟩ := by
-      simp_all
-    rw [h]
-    rw [List.getLast_eq_get (acc.set.intervals.data ++ [l]) hne]
-  rw [← h] at heq
-  simp [List.getLast_append] at heq
-  rw [heq] at h3
-  simp [h3]

lake-manifest.json

@@ -1,22 +1,24 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/fgdorais/lean4-unicode-basic.git",
    "type": "git",
    "subDir": null,
-   "rev": "48563d6b516f178851bd9abad05ebfaba84a3ee8",
+   "scope": "",
+   "rev": "6c260d58b9c9fe49f1312a6ecc0437de84e2fb8d",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "48563d6b516f178851bd9abad05ebfaba84a3ee8",
+   "inputRev": "6c260d58b9c9fe49f1312a6ecc0437de84e2fb8d",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
+   "scope": "",
+   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.9.0",
+   "inputRev": "v4.10.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Regex",

lakefile.lean

@@ -3,12 +3,12 @@ open Lake DSL
 
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4"
-    @ "v4.9.0"
+    @ "v4.10.0"
 
 require UnicodeBasic from git "https://github.com/fgdorais/lean4-unicode-basic.git"
-    @ "48563d6b516f178851bd9abad05ebfaba84a3ee8"
+    @ "6c260d58b9c9fe49f1312a6ecc0437de84e2fb8d"
 
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.9.0"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.10.0"
 
 package «Regex» {
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.10.0