fix: correctness subproject after update to lean v4.31.0

Author: srghma

correctness/RegexCorrectness/Data/String.lean

@@ -37,7 +37,7 @@ theorem String.empty_or_eq_singleton_append (s : String) :
   obtain ⟨cs, rfl⟩ := String.exists_eq_ofList s
   match cs with
   | [] => exact .inl rfl
-  | c :: cs => exact .inr ⟨c, String.ofList cs, by simp [String.singleton_eq_ofList, ←String.ofList_append]⟩
+  | c :: cs => exact .inr ⟨c, String.ofList cs, by simp only [String.singleton_eq_ofList, ←String.ofList_append, List.singleton_append]⟩
 
 namespace Regex.Data.String
 

correctness/RegexCorrectness/Syntax/Ast.lean

@@ -47,6 +47,7 @@ theorem repeatConcat_go_tags_subset (e : Expr) (accum : Expr) (n : Nat) :
     simpa [Expr.tags] using ih (accum.concat e)
 
 theorem repeatConcat_tags (e : Expr) (n : Nat) : (repeatConcat e n).tags = e.tags := by
+  unfold repeatConcat
   refine Finset.Subset.antisymm ?_ ?_
   . simpa using repeatConcat_go_tags_subset e e (n - 1)
   . exact subset_repeatConcat_go_tags e e (n - 1) (by simp)

correctness/RegexCorrectness/Unicode/CaseFold/Equivalence.lean

@@ -41,7 +41,7 @@ public def CaseFoldEquiv (c₁ c₂ : Char) : Prop :=
 def CaseFoldEquiv' (c₁ c₂ : Char) : Prop :=
   getCaseFoldEquivChars c₁ = getCaseFoldEquivChars c₂
 
-instance instCaseFoldEquivEquivalence' : Equivalence CaseFoldEquiv' where
+theorem instCaseFoldEquivEquivalence' : Equivalence CaseFoldEquiv' where
   refl := by grind [CaseFoldEquiv']
   symm := by grind [CaseFoldEquiv']
   trans := by grind [CaseFoldEquiv']
@@ -98,7 +98,7 @@ theorem caseFoldEquiv'_iff_caseFoldEquiv {c₁ c₂ : Char} : CaseFoldEquiv' c
 theorem caseFoldEquiv'_eq_caseFoldEquiv : CaseFoldEquiv' = CaseFoldEquiv := by
   grind [caseFoldEquiv'_iff_caseFoldEquiv]
 
-public instance instCaseFoldEquivEquivalence : Equivalence CaseFoldEquiv :=
+public theorem instCaseFoldEquivEquivalence : Equivalence CaseFoldEquiv :=
   caseFoldEquiv'_eq_caseFoldEquiv ▸ instCaseFoldEquivEquivalence'
 
 end Regex.Unicode

correctness/RegexCorrectness/VM/CharStep/Lemmas.lean

@@ -28,19 +28,26 @@ theorem lower_bound (h : stepChar (HistoryStrategy s) nfa wf pos ne currentUpdat
   (lb : εClosure.LowerBound (pos.next ne) next.states) :
   εClosure.LowerBound (pos.next ne) next'.states := by
   simp only [HistoryStrategy.update_def, stepChar, Fin.getElem_fin] at h
-  grind [εClosure.lower_bound]
+  split at h
+  · expose_names; exact εClosure.lower_bound h lb
+  · grind only
 
 theorem eq_updates_of_mem_next {i k} (h : stepChar (HistoryStrategy s) nfa wf pos ne currentUpdates next i = (matched', next'))
   (mem : k ∈ next.states) :
   next'.updates[k] = next.updates[k] := by
   simp only [HistoryStrategy.update_def, stepChar, Fin.getElem_fin] at h
-  grind [εClosure.eq_updates_of_mem_next]
+  split at h
+  · · expose_names; exact εClosure.eq_updates_of_mem_next h mem
+  · grind only
+
 
 theorem done_of_matched_some (h : stepChar (HistoryStrategy s) nfa wf pos ne currentUpdates next state = (matched', next'))
   (isSome' : matched'.isSome) :
   ∃ state' ∈ next'.states, nfa[state'] = .done ∧ next'.updates[state'] = matched'.get isSome' := by
   simp only [HistoryStrategy.update_def, stepChar, Fin.getElem_fin] at h
-  grind [εClosure.matched_inv]
+  split at h
+  · exact εClosure.matched_inv h (fun isSome => Bool.noConfusion isSome) isSome'
+  · grind only [= Option.isSome_none]
 
 theorem mem_next_of_stepChar {i j k update}
   (h : stepChar (HistoryStrategy s) nfa wf pos ne currentUpdates next i = (matched', next'))
@@ -53,14 +60,18 @@ theorem mem_next_of_stepChar {i j k update}
     have eqj : j = state' := by
       split at hn
       next hn' =>
-        simp at hn
-        simp [NFA.CharStep.char hn'] at step
-        simp [Fin.ext_iff, step, ←hn.2]
+        split at hn
+        · injection hn with hn
+          simp [NFA.CharStep.char hn'] at step
+          simp [Fin.ext_iff, step, ←hn]
+        · contradiction
       next hn' =>
-        simp at hn
-        simp [NFA.CharStep.sparse hn'] at step
-        simp [Fin.ext_iff, step, ←hn.2]
-      next => simp at hn
+        split at hn
+        · injection hn with hn
+          simp [NFA.CharStep.sparse hn'] at step
+          simp [Fin.ext_iff, step, ←hn]
+        · contradiction
+      next => contradiction
     exact εClosure.mem_next h lb (eqj ▸ cls)
   next hn =>
     split at hn
@@ -88,8 +99,15 @@ theorem write_updates_of_mem_next {i k}
   next state' hn =>
     match εClosure.write_updates_of_mem_next h mem with
     | .inl mem => exact .inl mem
-    | .inr ⟨update', cls, write⟩ => exact .inr ⟨state', update', (by grind), cls, write⟩
-  next => grind
+    | .inr ⟨update', cls, write⟩ =>
+      have step : nfa.CharStep pos i state' := by
+        grind only [usr Fin.isLt, = CharStep.fail, = Fin.getElem_fin, => CharStep.char,
+          => CharStep.sparse, #6698, #51e9, #8818, #5c18, #c184]
+      exact .inr ⟨state', update', step, cls, write⟩
+  next hn =>
+    injection h with _ hnext
+    subst hnext
+    exact .inl mem
 
 theorem inv {pos₀ idx} (hlt : idx < current.states.count)
   (h : stepChar (HistoryStrategy s) nfa wf pos ne current.updates next current.states[idx] = (matched', next'))
@@ -126,8 +144,10 @@ theorem go.lower_bound {idx hle} (h : eachStepChar.go (HistoryStrategy s) nfa wf
   (lb : εClosure.LowerBound (pos.next ne) next.states) :
   εClosure.LowerBound (pos.next ne) next'.states := by
   induction idx, hle, next using eachStepChar.go.induct' (HistoryStrategy s) nfa wf pos ne current with
-  | base next => simp_all [HistoryStrategy.update_def]
-  | done i hlt next hn => simp_all [HistoryStrategy.update_def]
+  | base next =>
+    simp_all [eachStepChar.go_base, HistoryStrategy.update_def]
+  | done i hlt next hn =>
+    simp_all [eachStepChar.go_done, HistoryStrategy.update_def]
   | found i hlt next hn matched next'' h' found =>
     rw [eachStepChar.go_found hlt hn h' found] at h
     simp_all
@@ -140,8 +160,12 @@ theorem go.done_of_matched_some {idx hle} (h : eachStepChar.go (HistoryStrategy
   (isSome' : matched'.isSome) :
   ∃ state' ∈ next'.states, nfa[state'] = .done ∧ next'.updates[state'] = matched'.get isSome' := by
   induction idx, hle, next using eachStepChar.go.induct' (HistoryStrategy s) nfa wf pos ne current with
-  | base next => grind
-  | done i hlt next hn => grind
+  | base next =>
+    simp [eachStepChar.go_base] at h
+    injection h with h1 _; subst h1; contradiction
+  | done i hlt next hn =>
+    simp [eachStepChar.go_done hlt hn] at h
+    injection h with h1 _; subst h1; contradiction
   | found i hlt next hn matched next'' h' found =>
     rw [eachStepChar.go_found hlt hn h' found] at h
     simp [HistoryStrategy.update_def] at h

correctness/RegexCorrectness/VM/Correspondence/Refinement/Refinement.lean

@@ -72,7 +72,14 @@ theorem εClosure.refines (resultB resultH)
   induction matchedH, nextH, stackH using εClosure.induct' (HistoryStrategy s) nfa wf pos generalizing matchedB nextB stackB resultB resultH with
   | base matchedH nextH =>
     simp [εStack.materialize] at refStack
-    grind [εClosure.base, materializeResult]
+    subst stackB
+    simp [εClosure.base] at h'
+    subst h'
+    -- h : εClosure (BufferStrategy...) ... [] = resultB, hbase gives εClosure [] = (matched, next)
+    have hbase : εClosure (BufferStrategy s bufferSize) nfa wf pos matchedB nextB [] = (matchedB, nextB) := εClosure.base
+    have hresB : resultB = (matchedB, nextB) := h.symm.trans hbase
+    subst hresB
+    simp [materializeResult, refState, refMatched]
   | visited matched' next' update state' stack' mem ih =>
     simp only [εStack.materialize.cons] at refStack
     subst stackB
@@ -94,14 +101,19 @@ theorem εClosure.refines (resultB resultH)
       h
     rw [εClosure.not_visited (refState ▸ mem)] at h
     refine ih resultB resultH h h' ?_ ?_ ?_
-    . split
-      next eq => simp +instances [matched'', node, eq, ←refMatched]; grind only
-      next eq =>
-        simp at eq
-        simp [matched'', node, eq, refMatched]
+    . dsimp [matched'', node]
+      split
+      next =>
+        clear ih h h'
+        cases matched' <;> simp [←refMatched] <;> rfl
+      next =>
+        clear ih h h'
+        simp [←refMatched]
     . simp [SearchState.materialize] at refState
-      simp [SearchState.materialize, states'', ←refState]
-      split <;> grind
+      simp [SearchState.materialize, states'', ← refState, updates'', node]
+      split
+      · grind only [HistoryStrategy.update_def, Vector.map_set]
+      · grind only
     . exact pushNext.refines wf rfl rfl
 
 theorem stepChar.refines {currentUpdatesH currentUpdatesB state} (resultB resultH)
@@ -114,11 +126,17 @@ theorem stepChar.refines {currentUpdatesH currentUpdatesB state} (resultB result
   split at h'
   next state' hn =>
     simp [hn] at h
-    exact εClosure.refines resultB resultH h h' rfl refState (by simp [εStack.materialize, ←refUpdates]; grind)
+    have refStack : εStack.materialize [(currentUpdatesH[state], state')] = [(currentUpdatesB[state], state')] := by
+      have h_eq : (currentUpdatesH.map (materializeUpdates bufferSize))[state] = currentUpdatesB[state] :=
+        congrArg (fun v => v[state]) refUpdates
+      simp at h_eq
+      exact congrArg (fun x => [(x, state')]) h_eq
+    exact εClosure.refines resultB resultH h h' rfl refState refStack
   next hn =>
     simp [hn] at h
-    simp [←h', ←h, materializeResult]
-    grind
+    rw [←h', ←h]
+    simp [materializeResult, refState]
+    rfl
 
 theorem eachStepChar.go.refines {currentH currentB i hleB hleH} (resultB resultH)
   (h : eachStepChar.go (BufferStrategy s bufferSize) nfa wf pos ne currentB i hleB nextB = resultB)
@@ -156,7 +174,7 @@ theorem eachStepChar.go.refines {currentH currentB i hleB hleH} (resultB resultH
     simp [materializeResult] at refResult
 
     have isSomeB : matchedB.isSome := by
-      simpa [←refResult.1] using isSomeH
+      simpa [←refResult.1, HistoryStrategy.update_def] using isSomeH
 
     simp [eachStepChar.go_found hltH hnH hstepH isSomeH] at h'
     simp [eachStepChar.go_found hltB hnB hstepB isSomeB] at h
@@ -176,7 +194,7 @@ theorem eachStepChar.go.refines {currentH currentB i hleB hleH} (resultB resultH
     simp [materializeResult] at refResult
 
     have isSomeB : ¬matchedB.isSome := by
-      simpa [←refResult.1] using isSomeH
+      simpa [←refResult.1, HistoryStrategy.update_def] using isSomeH
 
     simp [eachStepChar.go_not_found hltH hnH hstepH isSomeH] at h'
     simp [eachStepChar.go_not_found hltB hnB hstepB isSomeB] at h
@@ -206,7 +224,7 @@ theorem captureNext.go.refines {currentH currentB resultB resultH}
     have isEmptyB : currentB.states.isEmpty := by
       simpa [←refCurrent] using isEmptyH
     have isSomeB : matchedB.isSome := by
-      simpa [←refMatched] using isSomeH
+      simpa [←refMatched, HistoryStrategy.update_def] using isSomeH
     rw [captureNext.go_found atEnd isEmptyH isSomeH] at h'
     rw [captureNext.go_found atEnd isEmptyB isSomeB] at h
     simp [←h', ←h, refMatched]
@@ -218,9 +236,9 @@ theorem captureNext.go.refines {currentH currentB resultB resultH}
     have refStepped := eachStepChar.refines steppedB steppedH rfl rfl refCurrent refNext
     have refExpanded := εClosure.refines expandedB expandedH rfl rfl rfl (by simp [←refStepped, materializeResult]) rfl
     have isNoneB₁ : matchedB = .none := by
-      simpa [←refMatched] using isNoneH₁
+      simpa [←refMatched, HistoryStrategy.update_def] using isNoneH₁
     have isNoneB₂ : steppedB.1 = .none := by
-      simpa [←refStepped, materializeResult] using isNoneH₂
+      simpa [←refStepped, materializeResult, HistoryStrategy.update_def] using isNoneH₂
 
     rw [captureNext.go_ind_not_found steppedH expandedH rfl rfl isNoneH₁ isNoneH₂] at h'
     rw [captureNext.go_ind_not_found steppedB expandedB rfl rfl isNoneB₁ isNoneB₂] at h
@@ -238,7 +256,7 @@ theorem captureNext.go.refines {currentH currentB resultB resultH}
       simp [←refMatched] at h
       exact refCurrent ▸ hempH h
     have isSomeB : matchedB.isSome ∨ steppedB.1.isSome := by
-      simpa [←refMatched, ←refStepped, materializeResult] using isSomeH
+      simpa [←refMatched, ←refStepped, materializeResult, HistoryStrategy.update_def] using isSomeH
 
     rw [captureNext.go_ind_found steppedH rfl hempH isSomeH] at h'
     rw [captureNext.go_ind_found steppedB rfl hempB isSomeB] at h

correctness/RegexCorrectness/VM/EpsilonClosure/Lemmas.lean

@@ -376,7 +376,8 @@ theorem preserves' {stack'} {node} (hn : nfa[entry.2] = node) (nextEntries) (hst
       simp [eq]
       have ⟨update', equpdate, cls⟩ := inv.mem_stack entry.1 entry.2 (by simp)
       refine .inr ⟨update', cls, fun write => ?_⟩
-      simpa [←hn, write] using equpdate
+      simp [←hn, write]
+      exact equpdate
     | inr mem =>
       match inv.mem_next j mem with
       | .inl mem => exact .inl mem

correctness/RegexCorrectness/VM/Path/VMPath.lean

@@ -20,9 +20,9 @@ theorem Step.εStep_or_charStep {i j : Nat} (wf : nfa.WellFormed) (step : nfa.St
   grind
 
 inductive VMPath (nfa : NFA) (wf : nfa.WellFormed) (pos₀ : Pos s) : Pos s → Fin nfa.size → List (Nat × Pos s) → Prop where
-  | init {pos i update} (le : pos₀ ≤ pos) (cls : nfa.εClosure' pos ⟨nfa.start, wf.start_lt⟩ i update) :
+  | init {pos : Pos s} {i : Fin nfa.size} {update : List (Nat × Pos s)} (le : pos₀ ≤ pos) (cls : nfa.εClosure' pos ⟨nfa.start, wf.start_lt⟩ i update) :
     VMPath nfa wf pos₀ pos i update
-  | more {i j k pos pos' update₁ update₂ update₃} (prev : VMPath nfa wf pos₀ pos i update₁) (step : nfa.CharStep pos i j) (cls : nfa.εClosure' (pos.next step.ne) j k update₂)
+  | more {i j k : Fin nfa.size} {pos pos' : Pos s} {update₁ update₂ update₃ : List (Nat × Pos s)} (prev : VMPath nfa wf pos₀ pos i update₁) (step : nfa.CharStep pos i j) (cls : nfa.εClosure' (pos.next step.ne) j k update₂)
     (hupdate : update₃ = update₁ ++ update₂) (hpos : pos' = pos.next step.ne) :
     VMPath nfa wf pos₀ pos' k update₃
 

correctness/lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"type": "path",
@@ -12,17 +12,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
+   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.31.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,17 +52,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
+   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.95",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -72,7 +72,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -82,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -92,11 +92,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
+   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.31.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "RegexCorrectness",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}