feat: update to v4.11.0-rc2

Regex/Compiler.lean

@@ -432,20 +432,20 @@ private def c (hir : Hir) : CompilerM ThompsonRef :=
  | .Class (.Unicode cls) => c_unicode_class cls
  | .Look look => c_look look
  | .Lookaround look =>
- have : sizeOf look < sizeOf hir.kind := by simp [h]; omega
+ have : sizeOf look < sizeOf hir.kind := by simp [h]
  c_lookaround look
  | .BackRef f n => c_back_ref f n
  | .Repetition rep =>
- have : sizeOf rep < sizeOf hir.kind := by simp [h]; omega
+ have : sizeOf rep < sizeOf hir.kind := by simp [h]
  c_repetition rep
  | .Capture cap =>
- have : sizeOf cap < sizeOf hir.kind := by simp [h]; omega
+ have : sizeOf cap < sizeOf hir.kind := by simp [h]
  c_cap cap
  | .Concat items =>
- have : sizeOf items < sizeOf hir.kind := by simp [h]; omega
+ have : sizeOf items < sizeOf hir.kind := by simp [h]
  c_concat items
  | .Alternation sub =>
- have : sizeOf sub < sizeOf hir.kind := by simp [h]; omega
+ have : sizeOf sub < sizeOf hir.kind := by simp [h]
  c_alt_iter sub
 termination_by sizeOf hir
 

Regex/Data/Array/Lemmas.lean

@@ -20,7 +20,6 @@ theorem sizeOf_head?_of_tail [SizeOf α] {as : Array α} (h : Array.head? as = s
  cases as with | _ as =>
  cases as' with | _ as' =>
  simp_all
- apply Nat.add_lt_add_left _
  simp_arith
 
 theorem sizeOf_dropLast_cons [SizeOf α] (a : α) (as : List α)
@@ -40,7 +39,6 @@ theorem sizeOf_pop_non_empty [SizeOf α] (as : Array α) (h : 0 < as.data.length
  unfold Array.pop
  cases as with | _ as =>
  simp
- apply Nat.add_lt_add_left _
  exact sizeOf_dropLast_non_empty _ h
 
 theorem sizeOf_pop? [SizeOf α] {as : Array α} (h : Array.pop? as = some (a, as'))
@@ -78,7 +76,7 @@ theorem last?_eq_getLast (a : Array α) (h1: Array.last? a = some last) (h2 : a.
  unfold Array.last? at h1
  split at h1 <;> simp_all
  rw [← h1]
- simp [List.getLast_eq_get a.data h2]
+ simp [List.getLast_eq_getElem a.data h2]
 
 theorem lt_of_pop?_eq_last? {arr : Array α} (h : Array.pop? arr = some (last, arr'))
  : 0 < arr.data.length := by

Regex/Data/List/Lemmas.lean

@@ -89,7 +89,7 @@ theorem chain_iff_get {R} : ∀ {a : α} {l : List α}, Chain R a l ↔
  (∀ h : 0 < length l, R a (get l ⟨0, h⟩)) ∧
  ∀ (i : Nat) (h : i < l.length - 1),
  R (get l ⟨i, by omega⟩) (get l ⟨i+1, by omega⟩)
- | a, [] => iff_of_true (by simp) ⟨fun h => by simp at h, fun _ h => by simp at h; omega⟩
+ | a, [] => iff_of_true (by simp) ⟨fun h => by simp at h, fun _ h => by simp at h⟩
  | a, b :: t => by
  rw [chain_cons, @chain_iff_get _ _ _ t]
  constructor

Regex/Syntax/Ast/Ast.lean

@@ -987,7 +987,7 @@ def ast (rep : Repetition) : Ast := match rep with | .mk _ _ _ _ ast => ast
 
 theorem sizeOfAstOfRepetition (rep : Repetition) : sizeOf rep.ast < sizeOf rep := by
  unfold Syntax.AstItems.Repetition.ast
- split <;> simp_all; omega
+ split <;> simp_all
 
 end Repetition
 

Regex/Syntax/Hir.lean

@@ -239,44 +239,44 @@ def toString (hir : Hir) (col : Nat): String :=
  | .Lookaround lk =>
  match hr: lk with
  | .PositiveLookahead sub =>
- have : sizeOf lk < sizeOf hir.kind := by simp [hk, hr]; omega
- have : sizeOf sub < sizeOf lk := by simp [hr]; omega
+ have : sizeOf lk < sizeOf hir.kind := by simp [hk, hr]
+ have : sizeOf sub < sizeOf lk := by simp [hr]
  s!"PositiveLookahead {toString sub col}"
  | .NegativeLookahead sub =>
- have : sizeOf lk < sizeOf hir.kind := by simp [hk, hr]; omega
- have : sizeOf sub < sizeOf lk := by simp [hr]; omega
+ have : sizeOf lk < sizeOf hir.kind := by simp [hk, hr]
+ have : sizeOf sub < sizeOf lk := by simp [hr]
  s!"NegativeLookahead {toString sub col}"
  | .PositiveLookbehind i sub =>
- have : sizeOf lk < sizeOf hir.kind := by simp [hk, hr]; omega
+ have : sizeOf lk < sizeOf hir.kind := by simp [hk, hr]
  have : sizeOf sub < sizeOf lk := by simp [hr]; omega
  s!"PositiveLookbehind Length {i} {toString sub col}"
  | .NegativeLookbehind i sub =>
- have : sizeOf lk < sizeOf hir.kind := by simp [hk, hr]; omega
+ have : sizeOf lk < sizeOf hir.kind := by simp [hk, hr]
  have : sizeOf sub < sizeOf lk := by simp [hr]; omega
  s!"NegativeLookbehind Length {i} {toString sub col}"
  | .Repetition rep =>
  match hr : rep with
  | .mk min max greedy possessive sub =>
- have : sizeOf rep < sizeOf hir.kind := by simp [hk, hr]; omega
- have : sizeOf sub < sizeOf rep := by simp [hr]; omega
+ have : sizeOf rep < sizeOf hir.kind := by simp [hk, hr]
+ have : sizeOf sub < sizeOf rep := by simp [hr]
  s!"Repetition {min} {max} possessive {possessive} greedy {greedy}{pre}sub {toString sub col}"
  | .Capture c =>
  match hc : c with
  | .mk index name sub =>
- have : sizeOf c < sizeOf hir.kind := by simp [hk, hc]; omega
+ have : sizeOf c < sizeOf hir.kind := by simp [hk, hc]
  have : sizeOf sub < sizeOf c := by simp [hc]; omega
  s!"Capture {index} {name}{pre}sub {toString sub col}"
  | .Concat items =>
  let hirs := Array.mapIdx items.attach (fun i s => (i, s))
- have : sizeOf items < sizeOf hir.kind := by simp [hk]; omega
+ have : sizeOf items < sizeOf hir.kind := by simp [hk]
  let hirs := String.join (hirs.toList |> List.map (fun (i, ast) =>
  let iv := String.mk (Nat.toDigits 0 i.val)
  have : sizeOf ast.val < sizeOf items := Array.sizeOf_lt_of_mem ast.property
  pre ++ iv ++ ": " ++ (toString ast.val col)))
  s!"Concat {hirs}"
  | .Alternation items =>
  let hirs := Array.mapIdx items.attach (fun i s => (i, s))
- have : sizeOf items < sizeOf hir.kind := by simp [hk]; omega
+ have : sizeOf items < sizeOf hir.kind := by simp [hk]
  let hirs := String.join (hirs.toList |> List.map (fun (i, ast) =>
  let iv := String.mk (Nat.toDigits 0 i.val)
  have : sizeOf ast.val < sizeOf items := Array.sizeOf_lt_of_mem ast.property

lake-manifest.json

@@ -15,10 +15,10 @@
  "type": "git",
  "subDir": null,
  "scope": "",
- "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
+ "rev": "021e272cb5cdcc82b7e1e760fe915ff2f64169ad",
  "name": "batteries",
  "manifestFile": "lake-manifest.json",
- "inputRev": "v4.10.0",
+ "inputRev": "v4.11.0-rc1",
  "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.10.0"
+ @ "v4.11.0-rc1"
 
 require UnicodeBasic from git "https://github.com/fgdorais/lean4-unicode-basic.git"
  @ "6c260d58b9c9fe49f1312a6ecc0437de84e2fb8d"
 
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.10.0"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.11.0-rc1"
 
 package «Regex» {
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0-rc2