From 77bbf59b64f36258ea3346dc4e2f3b80df64f850 Mon Sep 17 00:00:00 2001 From: "J. Bergmann" Date: Thu, 1 Aug 2024 14:27:58 +0200 Subject: [PATCH] feat: update to v4.10.0 --- Regex/Backtrack.lean | 6 ++--- Regex/Data/Array/Lemmas.lean | 8 +++---- Regex/Data/List/Lemmas.lean | 27 ++++++++++++++++------ Regex/Data/UInt/Basic.lean | 3 +++ Regex/Interval/Lemmas.lean | 44 ++++-------------------------------- lake-manifest.json | 12 ++++++---- lakefile.lean | 6 ++--- lean-toolchain | 2 +- 8 files changed, 46 insertions(+), 62 deletions(-) diff --git a/Regex/Backtrack.lean b/Regex/Backtrack.lean index ebd8497..5724b5f 100644 --- a/Regex/Backtrack.lean +++ b/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] diff --git a/Regex/Data/Array/Lemmas.lean b/Regex/Data/Array/Lemmas.lean index 2b14bf5..1822597 100644 --- a/Regex/Data/Array/Lemmas.lean +++ b/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)] diff --git a/Regex/Data/List/Lemmas.lean b/Regex/Data/List/Lemmas.lean index 64962ab..6d1beca 100644 --- a/Regex/Data/List/Lemmas.lean +++ b/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 diff --git a/Regex/Data/UInt/Basic.lean b/Regex/Data/UInt/Basic.lean index 0de8808..8803627 100644 --- a/Regex/Data/UInt/Basic.lean +++ b/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 diff --git a/Regex/Interval/Lemmas.lean b/Regex/Interval/Lemmas.lean index 83a0d5c..4af7e00 100644 --- a/Regex/Interval/Lemmas.lean +++ b/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] diff --git a/lake-manifest.json b/lake-manifest.json index 0d841b8..4fba0a2 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lakefile.lean b/lakefile.lean index 102048a..0b5ce42 100644 --- a/lakefile.lean +++ b/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» { } diff --git a/lean-toolchain b/lean-toolchain index 4ef27c4..7f0ea50 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0 +leanprover/lean4:v4.10.0