chore: remove lean4checker from release repos (#13121)

Lean4checker has been merged into this repository and is no longer a
standalone repo.

.github/workflows/ci.yml

@@ -76,9 +76,20 @@ jobs:
               fi
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
             else
-              # Scheduled: do nothing if commit already has a different tag
+              # Scheduled: do nothing if commit already has a different tag (e.g. a release tag)
               LEAN_VERSION_STRING="nightly-$(date -u +%F)"
-              if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
+              HEAD_TAG="$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || true)"
+              if [[ -n "$HEAD_TAG" && "$HEAD_TAG" != "$LEAN_VERSION_STRING" ]]; then
+                echo "HEAD already tagged as ${HEAD_TAG}, skipping nightly"
+              elif git rev-parse "refs/tags/${LEAN_VERSION_STRING}" >/dev/null 2>&1; then
+                # Today's nightly already exists (e.g. from a manual release), create a revision
+                REV=1
+                while git rev-parse "refs/tags/${LEAN_VERSION_STRING}-rev${REV}" >/dev/null 2>&1; do
+                  REV=$((REV + 1))
+                done
+                LEAN_VERSION_STRING="${LEAN_VERSION_STRING}-rev${REV}"
+                echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
+              else
                 echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
               fi
             fi

script/release_repos.yml

@@ -14,13 +14,6 @@ repositories:
     bump-branch: true
     dependencies: []
 
-  - name: lean4checker
-    url: https://github.com/leanprover/lean4checker
-    toolchain-tag: true
-    stable-branch: true
-    branch: master
-    dependencies: []
-
   - name: quote4
     url: https://github.com/leanprover-community/quote4
     toolchain-tag: true

src/Init/Control/ExceptCps.lean

@@ -37,7 +37,7 @@ set_option linter.unusedVariables false in  -- `s` unused
 Use a monadic action that may throw an exception by providing explicit success and failure
 continuations.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β :=
   x _ ok error
 
@@ -83,6 +83,8 @@ of `True`.
 -/
 instance : MonadAttach (ExceptCpsT ε m) := .trivial
 
+@[simp] theorem throw_bind [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : (throw e >>= f : ExceptCpsT ε m β) = throw e := rfl
+
 @[simp] theorem run_pure [Monad m] : run (pure x : ExceptCpsT ε m α) = pure (Except.ok x) := rfl
 
 @[simp] theorem run_lift {α ε : Type u} [Monad m] (x : m α) : run (ExceptCpsT.lift x : ExceptCpsT ε m α) = (x >>= fun a => pure (Except.ok a) : m (Except ε α)) := rfl
@@ -91,7 +93,20 @@ instance : MonadAttach (ExceptCpsT ε m) := .trivial
 
 @[simp] theorem run_bind_lift [Monad m] (x : m α) (f : α → ExceptCpsT ε m β) : run (ExceptCpsT.lift x >>= f : ExceptCpsT ε m β) = x >>= fun a => run (f a) := rfl
 
-@[simp] theorem run_bind_throw [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : run (throw e >>= f : ExceptCpsT ε m β) = run (throw e) := rfl
+@[deprecated throw_bind (since := "2026-03-13")]
+theorem run_bind_throw [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : run (throw e >>= f : ExceptCpsT ε m β) = run (throw e) := rfl
+
+@[simp] theorem runK_pure :
+    runK (pure x : ExceptCpsT ε m α) s ok error = ok x := rfl
+
+@[simp] theorem runK_lift {α ε : Type u} [Monad m] (x : m α) (s : ε) (ok : α → m β) (error : ε → m β) :
+    runK (ExceptCpsT.lift x : ExceptCpsT ε m α) s ok error = x >>= ok := rfl
+
+@[simp] theorem runK_throw [Monad m] :
+    runK (throw e : ExceptCpsT ε m β) s ok error = error e := rfl
+
+@[simp] theorem runK_bind_lift [Monad m] (x : m α) (f : α → ExceptCpsT ε m β) :
+    runK (ExceptCpsT.lift x >>= f : ExceptCpsT ε m β) s ok error = x >>= fun a => runK (f a) s ok error := rfl
 
 @[simp] theorem runCatch_pure [Monad m] : runCatch (pure x : ExceptCpsT α m α) = pure x := rfl
 
@@ -102,6 +117,7 @@ instance : MonadAttach (ExceptCpsT ε m) := .trivial
 
 @[simp] theorem runCatch_bind_lift [Monad m] (x : m α) (f : α → ExceptCpsT β m β) : runCatch (ExceptCpsT.lift x >>= f : ExceptCpsT β m β) = x >>= fun a => runCatch (f a) := rfl
 
-@[simp] theorem runCatch_bind_throw [Monad m] (e : β) (f : α → ExceptCpsT β m β) : runCatch (throw e >>= f : ExceptCpsT β m β) = pure e := rfl
+@[deprecated throw_bind (since := "2026-03-13")]
+theorem runCatch_bind_throw [Monad m] (e : β) (f : α → ExceptCpsT β m β) : runCatch (throw e >>= f : ExceptCpsT β m β) = pure e := rfl
 
 end ExceptCpsT

src/Init/Data/String/Lemmas/FindPos.lean

@@ -201,6 +201,10 @@ theorem Pos.prev_eq_iff {s : Slice} {p q : s.Pos} {h} :
 theorem Pos.prev_lt {s : Slice} {p : s.Pos} {h} : p.prev h < p := by
   simp
 
+@[simp]
+theorem Pos.prev_le {s : Slice} {p : s.Pos} {h} : p.prev h ≤ p :=
+  Std.le_of_lt (by simp)
+
 @[simp]
 theorem Pos.prev_ne_endPos {s : Slice} {p : s.Pos} {h} : p.prev h ≠ s.endPos :=
   ne_endPos_of_lt prev_lt
@@ -211,6 +215,29 @@ theorem Pos.prevn_le {s : Slice} {p : s.Pos} {n : Nat} : p.prevn n ≤ p := by
   | case2 p n h ih => exact Std.le_of_lt (by simpa using ih)
   | case3 => simp
 
+theorem Pos.ofSliceTo_prev {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
+    Pos.ofSliceTo (p.prev h) = (Pos.ofSliceTo p).prev (by simpa [← Pos.ofSliceTo_inj] using h) := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [Pos.ofSliceTo_lt_ofSliceTo_iff, Pos.le_ofSliceTo_iff]
+  simp [Pos.lt_ofSliceTo_iff]
+
+theorem Pos.prev_ofSliceTo {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
+    (Pos.ofSliceTo p).prev h = Pos.ofSliceTo (p.prev (by simpa [← Pos.ofSliceTo_inj])) := by
+  simp [ofSliceTo_prev]
+
+theorem Pos.ofSliceFrom_prev {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
+    Pos.ofSliceFrom (p.prev h) = (Pos.ofSliceFrom p).prev (by exact ofSliceFrom_ne_startPos h) := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [Pos.ofSliceFrom_lt_ofSliceFrom_iff,  Pos.le_ofSliceFrom_iff]
+  simp [Pos.lt_ofSliceFrom_iff]
+
+theorem Pos.ofSlice_prev {s : Slice} {p₀ p₁ : s.Pos} {h}
+    {p : (s.slice p₀ p₁ h).Pos} {h'} :
+    Pos.ofSlice (p.prev h') = (Pos.ofSlice p).prev (by exact ofSlice_ne_startPos h') := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [ofSlice_lt_ofSlice_iff,  le_ofSlice_iff]
+  simpa +contextual [← ofSlice_lt_ofSlice_iff] using fun q hq => Std.le_of_lt (Std.lt_of_lt_of_le hq ofSlice_le)
+
 @[simp]
 theorem Pos.prev_next {s : Slice} {p : s.Pos} {h} : (p.next h).prev (by simp) = p :=
   prev_eq_iff.2 (by simp)
@@ -439,6 +466,10 @@ theorem Pos.prev_eq_iff {s : String} {p q : s.Pos} {h} :
 theorem Pos.prev_lt {s : String} {p : s.Pos} {h} : p.prev h < p := by
   simp
 
+@[simp]
+theorem Pos.prev_le {s : String} {p : s.Pos} {h} : p.prev h ≤ p :=
+  Std.le_of_lt (by simp)
+
 @[simp]
 theorem Pos.prev_ne_endPos {s : String} {p : s.Pos} {h} : p.prev h ≠ s.endPos :=
   ne_endPos_of_lt prev_lt
@@ -463,6 +494,29 @@ theorem Pos.prevn_le {s : String} {p : s.Pos} {n : Nat} :
     p.prevn n ≤ p := by
   simpa [Pos.le_iff, ← offset_toSlice] using Slice.Pos.prevn_le
 
+theorem Pos.ofSliceTo_prev {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
+    Pos.ofSliceTo (p.prev h) = (Pos.ofSliceTo p).prev (by simpa [← Pos.ofSliceTo_inj] using h) := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [Pos.ofSliceTo_lt_ofSliceTo_iff, Pos.le_ofSliceTo_iff]
+  simp [Pos.lt_ofSliceTo_iff]
+
+theorem Pos.prev_ofSliceTo {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
+    (Pos.ofSliceTo p).prev h = Pos.ofSliceTo (p.prev (by simpa [← Pos.ofSliceTo_inj])) := by
+  simp [ofSliceTo_prev]
+
+theorem Pos.ofSliceFrom_prev {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
+    Pos.ofSliceFrom (p.prev h) = (Pos.ofSliceFrom p).prev (by exact ofSliceFrom_ne_startPos h) := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [Pos.ofSliceFrom_lt_ofSliceFrom_iff, Pos.le_ofSliceFrom_iff]
+  simp [Pos.lt_ofSliceFrom_iff]
+
+theorem Pos.ofSlice_prev {s : String} {p₀ p₁ : s.Pos} {h}
+    {p : (s.slice p₀ p₁ h).Pos} {h'} :
+    Pos.ofSlice (p.prev h') = (Pos.ofSlice p).prev (by exact ofSlice_ne_startPos h') := by
+  rw [eq_comm, Pos.prev_eq_iff]
+  simp only [ofSlice_lt_ofSlice_iff, le_ofSlice_iff]
+  simpa +contextual [← ofSlice_lt_ofSlice_iff] using fun q hq => Std.le_of_lt (Std.lt_of_lt_of_le hq ofSlice_le)
+
 @[simp]
 theorem Pos.prev_next {s : String} {p : s.Pos} {h} : (p.next h).prev (by simp) = p :=
   prev_eq_iff.2 (by simp)

src/Init/Data/String/Lemmas/IsEmpty.lean

@@ -204,7 +204,7 @@ theorem Slice.copy_sliceTo_startPos {s : Slice} : (s.sliceTo s.startPos).copy =
   simp
 
 @[simp]
-theorem Slice.copy_sliceFrom_startPos {s : Slice} : (s.sliceFrom s.endPos).copy = "" := by
+theorem Slice.copy_sliceFrom_endPos {s : Slice} : (s.sliceFrom s.endPos).copy = "" := by
   simp
 
 end CopyEqEmpty

src/Init/Data/String/Lemmas/Order.lean

@@ -11,6 +11,7 @@ import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.Basic
 import Init.Data.Order.Lemmas
 import Init.Omega
+import Init.ByCases
 
 public section
 
@@ -70,7 +71,7 @@ theorem Pos.le_startPos {s : String} (p : s.Pos) : p ≤ s.startPos ↔ p = s.st
   ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩
 
 @[simp]
-theorem Pos.startPos_lt_iff {s : String} {p : s.Pos} : s.startPos < p ↔ p ≠ s.startPos := by
+theorem Pos.startPos_lt_iff {s : String} (p : s.Pos) : s.startPos < p ↔ p ≠ s.startPos := by
   simp [← le_startPos, Std.not_le]
 
 @[simp]
@@ -235,6 +236,10 @@ theorem Slice.Pos.ofSliceFrom_next {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom
     Pos.next_le_iff_lt, true_and]
   simp [Pos.ofSliceFrom_lt_iff]
 
+theorem Slice.Pos.next_ofSliceFrom {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
+    (Pos.ofSliceFrom p).next h = Pos.ofSliceFrom (p.next (by simpa [← Pos.ofSliceFrom_inj])) := by
+  simp [ofSliceFrom_next]
+
 theorem Pos.ofSliceFrom_next {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
     Pos.ofSliceFrom (p.next h) = (Pos.ofSliceFrom p).next (by simpa [← Pos.ofSliceFrom_inj] using h) := by
   rw [eq_comm, Pos.next_eq_iff]
@@ -242,6 +247,10 @@ theorem Pos.ofSliceFrom_next {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀)
     Slice.Pos.next_le_iff_lt, true_and]
   simp [Pos.ofSliceFrom_lt_iff]
 
+theorem Pos.next_ofSliceFrom {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h} :
+    (Pos.ofSliceFrom p).next h = Pos.ofSliceFrom (p.next (by simpa [← Pos.ofSliceFrom_inj])) := by
+  simp [Pos.ofSliceFrom_next]
+
 theorem Slice.Pos.le_ofSliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} :
     q ≤ Pos.ofSliceTo p ↔ ∃ h, Slice.Pos.sliceTo p₀ q h ≤ p := by
   refine ⟨fun h => ⟨Slice.Pos.le_trans h Pos.ofSliceTo_le, ?_⟩, fun ⟨h, h'⟩ => ?_⟩
@@ -359,11 +368,21 @@ theorem Slice.Pos.ofSliceTo_ne_endPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo
   refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₀))
   simpa [← lt_endPos_iff, ← ofSliceTo_lt_ofSliceTo_iff] using h
 
+theorem Slice.Pos.ofSliceFrom_ne_startPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos}
+    (h : p ≠ (s.sliceFrom p₀).startPos) : Pos.ofSliceFrom p ≠ s.startPos := by
+  refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
+  simpa [← startPos_lt_iff, ← ofSliceFrom_lt_ofSliceFrom_iff] using h
+
 theorem Pos.ofSliceTo_ne_endPos {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos}
     (h : p ≠ (s.sliceTo p₀).endPos) : Pos.ofSliceTo p ≠ s.endPos := by
   refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₀))
   simpa [← Slice.Pos.lt_endPos_iff, ← ofSliceTo_lt_ofSliceTo_iff] using h
 
+theorem Pos.ofSliceFrom_ne_startPos {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos}
+    (h : p ≠ (s.sliceFrom p₀).startPos) : Pos.ofSliceFrom p ≠ s.startPos := by
+  refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
+  simpa [← Slice.Pos.startPos_lt_iff, ← ofSliceFrom_lt_ofSliceFrom_iff] using h
+
 theorem Slice.Pos.ofSliceTo_next {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
     Pos.ofSliceTo (p.next h) = (Pos.ofSliceTo p).next (ofSliceTo_ne_endPos h) := by
   rw [eq_comm, Pos.next_eq_iff]
@@ -406,16 +425,110 @@ theorem Pos.slice_le_slice_iff {s : String} {p₀ p₁ : s.Pos} {q r : s.Pos}
   simp [Slice.Pos.le_iff, Pos.le_iff, Pos.Raw.le_iff] at h₁ h₁' ⊢
   omega
 
+theorem Slice.Pos.le_ofSlice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    q ≤ Pos.ofSlice p ↔ ∃ h₁, ∀ h₀, Slice.Pos.slice q p₀ p₁ h₀ h₁ ≤ p := by
+  refine ⟨fun h => ⟨Std.le_trans h ofSlice_le, fun h' => ?_⟩, fun ⟨h₁, h⟩ => ?_⟩
+  · simp only [← Slice.Pos.slice_ofSlice (pos := p), slice_le_slice_iff]
+    simpa
+  · by_cases h₀ : p₀ ≤ q
+    · simpa only [← Slice.Pos.ofSlice_slice (h₁ := h₀) (h₂ := h₁), ofSlice_le_ofSlice_iff] using h h₀
+    · exact Std.le_of_lt (Std.lt_of_lt_of_le (Std.not_le.1 h₀) le_ofSlice)
+
+theorem Slice.Pos.ofSlice_lt_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    Pos.ofSlice p < q ↔ ∀ h₁, ∃ h₀, p < Slice.Pos.slice q p₀ p₁ h₀ h₁ := by
+  simp [← Std.not_le, le_ofSlice_iff]
+
+theorem Slice.Pos.lt_ofSlice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    q < Pos.ofSlice p ↔ ∃ h₁, ∀ h₀, Slice.Pos.slice q p₀ p₁ h₀ h₁ < p := by
+  refine ⟨fun h => ⟨Std.le_of_lt (Std.lt_of_lt_of_le h ofSlice_le), fun h' => ?_⟩, fun ⟨h₁, h⟩ => ?_⟩
+  · simp only [← Slice.Pos.slice_ofSlice (pos := p), slice_lt_slice_iff]
+    simpa
+  · by_cases h₀ : p₀ ≤ q
+    · simpa only [← Slice.Pos.ofSlice_slice (h₁ := h₀) (h₂ := h₁), ofSlice_lt_ofSlice_iff] using h h₀
+    · exact Std.lt_of_lt_of_le (Std.not_le.1 h₀) le_ofSlice
+
+theorem Slice.Pos.ofSlice_le_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    Pos.ofSlice p ≤ q ↔ ∀ h₁, ∃ h₀, p ≤ Slice.Pos.slice q p₀ p₁ h₀ h₁ := by
+  simp [← Std.not_lt, lt_ofSlice_iff]
+
+theorem Pos.le_ofSlice_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    q ≤ Pos.ofSlice p ↔ ∃ h₁, ∀ h₀, Pos.slice q p₀ p₁ h₀ h₁ ≤ p := by
+  refine ⟨fun h => ⟨Std.le_trans h ofSlice_le, fun h' => ?_⟩, fun ⟨h₁, h⟩ => ?_⟩
+  · simp only [← Pos.slice_ofSlice (pos := p), slice_le_slice_iff]
+    simpa
+  · by_cases h₀ : p₀ ≤ q
+    · simpa only [← Pos.ofSlice_slice (h₁ := h₀) (h₂ := h₁), ofSlice_le_ofSlice_iff] using h h₀
+    · exact Std.le_of_lt (Std.lt_of_lt_of_le (Std.not_le.1 h₀) le_ofSlice)
+
+theorem Pos.ofSlice_lt_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    Pos.ofSlice p < q ↔ ∀ h₁, ∃ h₀, p < Pos.slice q p₀ p₁ h₀ h₁ := by
+  simp [← Std.not_le, le_ofSlice_iff]
+
+theorem Pos.lt_ofSlice_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    q < Pos.ofSlice p ↔ ∃ h₁, ∀ h₀, Pos.slice q p₀ p₁ h₀ h₁ < p := by
+  refine ⟨fun h => ⟨Std.le_of_lt (Std.lt_of_lt_of_le h ofSlice_le), fun h' => ?_⟩, fun ⟨h₁, h⟩ => ?_⟩
+  · simp only [← Pos.slice_ofSlice (pos := p), slice_lt_slice_iff]
+    simpa
+  · by_cases h₀ : p₀ ≤ q
+    · simpa only [← Pos.ofSlice_slice (h₁ := h₀) (h₂ := h₁), ofSlice_lt_ofSlice_iff] using h h₀
+    · exact Std.lt_of_lt_of_le (Std.not_le.1 h₀) le_ofSlice
+
+theorem Pos.ofSlice_le_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} :
+    Pos.ofSlice p ≤ q ↔ ∀ h₁, ∃ h₀, p ≤ Pos.slice q p₀ p₁ h₀ h₁ := by
+  simp [← Std.not_lt, lt_ofSlice_iff]
+
+theorem Slice.Pos.slice_le_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    Slice.Pos.slice q p₀ p₁ h₀ h₁ ≤ p ↔ q ≤ Pos.ofSlice p := by
+  simp [le_ofSlice_iff, h₀, h₁]
+
+theorem Slice.Pos.lt_slice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    p < Slice.Pos.slice q p₀ p₁ h₀ h₁ ↔ Pos.ofSlice p < q := by
+  simp [ofSlice_lt_iff, h₀, h₁]
+
+theorem Slice.Pos.slice_lt_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    Slice.Pos.slice q p₀ p₁ h₀ h₁ < p ↔ q < Pos.ofSlice p := by
+  simp [lt_ofSlice_iff, h₀, h₁]
+
+theorem Slice.Pos.le_slice_iff {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    p ≤ Slice.Pos.slice q p₀ p₁ h₀ h₁ ↔ Pos.ofSlice p ≤ q := by
+  simp [ofSlice_le_iff, h₀, h₁]
+
+theorem Pos.slice_le_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    Pos.slice q p₀ p₁ h₀ h₁ ≤ p ↔ q ≤ Pos.ofSlice p := by
+  simp [le_ofSlice_iff, h₀, h₁]
+
+theorem Pos.lt_slice_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    p < Pos.slice q p₀ p₁ h₀ h₁ ↔ Pos.ofSlice p < q := by
+  simp [ofSlice_lt_iff, h₀, h₁]
+
+theorem Pos.slice_lt_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    Pos.slice q p₀ p₁ h₀ h₁ < p ↔ q < Pos.ofSlice p := by
+  simp [lt_ofSlice_iff, h₀, h₁]
+
+theorem Pos.le_slice_iff {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ h₁} :
+    p ≤ Pos.slice q p₀ p₁ h₀ h₁ ↔ Pos.ofSlice p ≤ q := by
+  simp [ofSlice_le_iff, h₀, h₁]
+
 theorem Slice.Pos.ofSlice_ne_endPos {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
     (h : p ≠ (s.slice p₀ p₁ h).endPos) : Pos.ofSlice p ≠ s.endPos := by
   refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₁))
   simpa [← lt_endPos_iff, ← ofSlice_lt_ofSlice_iff] using h
 
+theorem Slice.Pos.ofSlice_ne_startPos {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
+    (h : p ≠ (s.slice p₀ p₁ h).startPos) : Pos.ofSlice p ≠ s.startPos := by
+  refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
+  simpa [← startPos_lt_iff, ← ofSlice_lt_ofSlice_iff] using h
+
 theorem Pos.ofSlice_ne_endPos {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
     (h : p ≠ (s.slice p₀ p₁ h).endPos) : Pos.ofSlice p ≠ s.endPos := by
   refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₁))
   simpa [← Slice.Pos.lt_endPos_iff, ← ofSlice_lt_ofSlice_iff] using h
 
+theorem Pos.ofSlice_ne_startPos {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
+    (h : p ≠ (s.slice p₀ p₁ h).startPos) : Pos.ofSlice p ≠ s.startPos := by
+  refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
+  simpa [← Slice.Pos.startPos_lt_iff, ← ofSlice_lt_ofSlice_iff] using h
+
 @[simp]
 theorem Slice.Pos.offset_le_rawEndPos {s : Slice} {p : s.Pos} :
     p.offset ≤ s.rawEndPos :=

src/Init/Data/String/Lemmas/Pattern/Basic.lean

@@ -19,6 +19,7 @@ import Init.Data.Order.Lemmas
 import Init.ByCases
 import Init.Data.Option.Lemmas
 import Init.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.String.Lemmas.FindPos
 
 set_option doc.verso true
 
@@ -31,19 +32,20 @@ This file develops basic theory around searching in strings.
 
 We provide a typeclass for providing semantics to a pattern and then define the relevant notions
 of matching a pattern that let us state compatibility typeclasses for {name}`ForwardPattern` and
-{name}`ToForwardSearcher`. These typeclasses can then be required by correctness results for
-string functions which are implemented using the pattern framework.
+{name}`ToForwardSearcher` as well as their backwards variants. These typeclasses can then be
+required by correctness results for string functions which are implemented using the pattern
+framework.
 -/
 
 /--
 This data-carrying typeclass is used to give semantics to a pattern type that implements
 {name}`ForwardPattern` and/or {name}`ToForwardSearcher` by providing an abstract, not necessarily
-decidable {name}`ForwardPatternModel.Matches` predicate that implementates of {name}`ForwardPattern`
+decidable {name}`PatternModel.Matches` predicate that implementates of {name}`ForwardPattern`
 and {name}`ToForwardSearcher` can be validated against.
 
 Correctness results for generic functions relying on the pattern infrastructure, for example the
 correctness result for {name (scope := "Init.Data.String.Slice")}`String.Slice.split`, are then
-stated in terms of {name}`ForwardPatternModel.Matches`, and can be specialized to specific patterns
+stated in terms of {name}`PatternModel.Matches`, and can be specialized to specific patterns
 from there.
 
 The corresponding compatibility typeclasses are
@@ -59,7 +61,7 @@ searching.
 This means that pattern types that allow searching for the empty string will have to special-case
 the empty string in their correctness statements.
 -/
-class ForwardPatternModel {ρ : Type} (pat : ρ) : Type where
+class PatternModel {ρ : Type} (pat : ρ) : Type where
   /-- The predicate that says which strings match the pattern. -/
   Matches : String → Prop
   not_matches_empty : ¬ Matches ""
@@ -69,49 +71,72 @@ Predicate stating that the region between the start of the slice {name}`s` and t
 {name}`endPos` matches the pattern {name}`pat`. Note that there might be a longer match, see
 {name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.IsLongestMatch`.
 -/
-structure IsMatch (pat : ρ) [ForwardPatternModel pat] {s : Slice} (endPos : s.Pos) : Prop where
-  matches_copy : ForwardPatternModel.Matches pat (s.sliceTo endPos).copy
+structure IsMatch (pat : ρ) [PatternModel pat] {s : Slice} (endPos : s.Pos) : Prop where
+  matches_copy : PatternModel.Matches pat (s.sliceTo endPos).copy
 
-theorem IsMatch.ne_startPos {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos}
+theorem IsMatch.ne_startPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
     (h : IsMatch pat pos) : pos ≠ s.startPos := by
   intro hc
-  apply ForwardPatternModel.not_matches_empty (pat := pat)
+  apply PatternModel.not_matches_empty (pat := pat)
   simpa [hc] using h.matches_copy
 
-theorem isMatch_iff {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} :
-    IsMatch pat pos ↔ ForwardPatternModel.Matches pat (s.sliceTo pos).copy :=
+theorem isMatch_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
+    IsMatch pat pos ↔ PatternModel.Matches pat (s.sliceTo pos).copy :=
   ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩
 
-theorem isMatch_iff_exists_splits {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} :
-    IsMatch pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ t₂ ∧ ForwardPatternModel.Matches pat t₁ := by
+theorem isMatch_iff_exists_splits {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
+    IsMatch pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ t₂ ∧ PatternModel.Matches pat t₁ := by
   rw [isMatch_iff]
   refine ⟨fun h => ⟨_, _, pos.splits, h⟩, fun ⟨t₁, t₂, h₁, h₂⟩ => ?_⟩
   rwa [h₁.eq_left pos.splits] at h₂
 
+/--
+Predicate stating that the region between the position {name}`startPos` and the end of the slice
+{name}`s` matches the pattern {name}`pat`. Note that there might be a longer match.
+-/
+structure IsRevMatch (pat : ρ) [PatternModel pat] {s : Slice} (startPos : s.Pos) : Prop where
+  matches_copy : PatternModel.Matches pat (s.sliceFrom startPos).copy
+
+theorem IsRevMatch.ne_endPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
+    (h : IsRevMatch pat pos) : pos ≠ s.endPos := by
+  intro hc
+  apply PatternModel.not_matches_empty (pat := pat)
+  simpa [hc] using h.matches_copy
+
+theorem isRevMatch_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
+    IsRevMatch pat pos ↔ PatternModel.Matches pat (s.sliceFrom pos).copy :=
+  ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩
+
+theorem isRevMatch_iff_exists_splits {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
+    IsRevMatch pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ t₂ ∧ PatternModel.Matches pat t₂ := by
+  rw [isRevMatch_iff]
+  refine ⟨fun h => ⟨_, _, pos.splits, h⟩, fun ⟨t₁, t₂, h₁, h₂⟩ => ?_⟩
+  rwa [h₁.eq_right pos.splits] at h₂
+
 /--
 Predicate stating that the region between the start of the slice {name}`s` and the position
-{name}`endPos` matches that pattern {name}`pat`, and that there is no longer match starting at the
+{name}`pos` matches the pattern {name}`pat`, and that there is no longer match starting at the
 beginning of the slice. This is what a correct matcher should match.
 
 In some cases, being a match and being a longest match will coincide, see
-{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.Model.NoPrefixForwardPatternModel`.
+{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.Model.NoPrefixPatternModel`.
 -/
-structure IsLongestMatch (pat : ρ) [ForwardPatternModel pat] {s : Slice} (pos : s.Pos) where
+structure IsLongestMatch (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) where
   isMatch : IsMatch pat pos
   not_isMatch : ∀ pos', pos < pos' → ¬ IsMatch pat pos'
 
-theorem IsLongestMatch.ne_startPos {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos}
+theorem IsLongestMatch.ne_startPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
     (h : IsLongestMatch pat pos) : pos ≠ s.startPos :=
   h.isMatch.ne_startPos
 
-theorem IsLongestMatch.eq {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos pos' : s.Pos}
+theorem IsLongestMatch.eq {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos}
     (h : IsLongestMatch pat pos) (h' : IsLongestMatch pat pos') : pos = pos' := by
   apply Std.le_antisymm
   · exact Std.not_lt.1 (fun hlt => h'.not_isMatch _ hlt h.isMatch)
   · exact Std.not_lt.1 (fun hlt => h.not_isMatch _ hlt h'.isMatch)
 
 open Classical in
-theorem IsMatch.exists_isLongestMatch {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} :
+theorem IsMatch.exists_isLongestMatch {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
     IsMatch pat pos → ∃ (pos' : s.Pos), IsLongestMatch pat pos' := by
   induction pos using WellFounded.induction Pos.wellFounded_gt with | h pos ih
   intro h₁
@@ -120,61 +145,118 @@ theorem IsMatch.exists_isLongestMatch {pat : ρ} [ForwardPatternModel pat] {s :
     exact ih _ hp₁ hp₂
   · exact ⟨pos, ⟨h₁, fun p' hp₁ hp₂ => h₂ ⟨_, hp₁, hp₂⟩⟩⟩
 
-theorem IsLongestMatch.le_of_isMatch {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos pos' : s.Pos}
+theorem IsLongestMatch.le_of_isMatch {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos}
     (h : IsLongestMatch pat pos) (h' : IsMatch pat pos') : pos' ≤ pos :=
   Std.not_lt.1 (fun hlt => h.not_isMatch _ hlt h')
 
+/--
+Predicate stating that the region between the start of the slice {name}`s` and the position
+{name}`pos` matches the patten {name}`pat`, and that there is no longer match starting at the
+beginning of the slice. This is what a correct matcher should match.
+
+In some cases, being a match and being a longest match will coincide, see
+{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.Model.NoPrefixPatternModel`.
+-/
+structure IsLongestRevMatch (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) where
+  isRevMatch : IsRevMatch pat pos
+  not_isRevMatch : ∀ pos', pos' < pos → ¬ IsRevMatch pat pos'
+
+theorem IsLongestRevMatch.ne_endPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
+    (h : IsLongestRevMatch pat pos) : pos ≠ s.endPos :=
+  h.isRevMatch.ne_endPos
+
+theorem IsLongestRevMatch.eq {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos}
+    (h : IsLongestRevMatch pat pos) (h' : IsLongestRevMatch pat pos') : pos = pos' := by
+  apply Std.le_antisymm
+  · exact Std.not_lt.1 (fun hlt => h.not_isRevMatch _ hlt h'.isRevMatch)
+  · exact Std.not_lt.1 (fun hlt => h'.not_isRevMatch _ hlt h.isRevMatch)
+
+open Classical in
+theorem IsRevMatch.exists_isLongestRevMatch {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
+    IsRevMatch pat pos → ∃ (pos' : s.Pos), IsLongestRevMatch pat pos' := by
+  induction pos using WellFounded.induction Pos.wellFounded_lt with | h pos ih
+  intro h₁
+  by_cases h₂ : ∃ pos', pos' < pos ∧ IsRevMatch pat pos'
+  · obtain ⟨pos', hp₁, hp₂⟩ := h₂
+    exact ih _ hp₁ hp₂
+  · exact ⟨pos, ⟨h₁, fun p' hp₁ hp₂ => h₂ ⟨_, hp₁, hp₂⟩⟩⟩
+
+theorem IsLongestRevMatch.le_of_isRevMatch {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos}
+    (h : IsLongestRevMatch pat pos) (h' : IsRevMatch pat pos') : pos ≤ pos' :=
+  Std.not_lt.1 (fun hlt => h.not_isRevMatch _ hlt h')
+
 /--
 Predicate stating that a match for a given pattern is never a proper prefix of another match.
 
 This implies that the notion of match and longest match coincide.
 -/
-class NoPrefixForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPatternModel pat] : Prop where
-  eq_empty (s t) : ForwardPatternModel.Matches pat s → ForwardPatternModel.Matches pat (s ++ t) → t = ""
+class NoPrefixPatternModel {ρ : Type} (pat : ρ) [PatternModel pat] : Prop where
+  eq_empty (s t) : PatternModel.Matches pat s → PatternModel.Matches pat (s ++ t) → t = ""
 
-theorem NoPrefixForwardPatternModel.of_length_eq {ρ : Type} {pat : ρ} [ForwardPatternModel pat]
-    (h : ∀ s t, ForwardPatternModel.Matches pat s → ForwardPatternModel.Matches pat t → s.length = t.length) :
-    NoPrefixForwardPatternModel pat where
+theorem NoPrefixPatternModel.of_length_eq {ρ : Type} {pat : ρ} [PatternModel pat]
+    (h : ∀ s t, PatternModel.Matches pat s → PatternModel.Matches pat t → s.length = t.length) :
+    NoPrefixPatternModel pat where
   eq_empty s t hs ht := by simpa using h s _ hs ht
 
-theorem isLongestMatch_iff_isMatch {ρ : Type} (pat : ρ) [ForwardPatternModel pat] [NoPrefixForwardPatternModel pat]
+theorem isLongestMatch_iff_isMatch {ρ : Type} (pat : ρ) [PatternModel pat] [NoPrefixPatternModel pat]
     {s : Slice} {pos : s.Pos} : IsLongestMatch pat pos ↔ IsMatch pat pos := by
   refine ⟨fun h => h.isMatch, fun h => ⟨h, fun pos' hpos' hm => ?_⟩⟩
   obtain ⟨t₁, t₂, ht₁, ht₂⟩ := isMatch_iff_exists_splits.1 h
   obtain ⟨t₁', t₂', ht₁', ht₂'⟩ := isMatch_iff_exists_splits.1 hm
   obtain ⟨t₅, ht₅, ht₅', ht₅''⟩ := (ht₁.lt_iff_exists_eq_append ht₁').1 hpos'
-  exact ht₅ (NoPrefixForwardPatternModel.eq_empty _ _ ht₂ (ht₅' ▸ ht₂'))
+  exact ht₅ (NoPrefixPatternModel.eq_empty _ _ ht₂ (ht₅' ▸ ht₂'))
+
+/--
+Predicate stating that a match for a given pattern is never a proper suffix of another match.
+
+This implies that the notion of reverse match and longest reverse match coincide.
+-/
+class NoSuffixPatternModel {ρ : Type} (pat : ρ) [PatternModel pat] : Prop where
+  eq_empty (s t) : PatternModel.Matches pat t → PatternModel.Matches pat (s ++ t) → s = ""
+
+theorem NoSuffixPatternModel.of_length_eq {ρ : Type} {pat : ρ} [PatternModel pat]
+    (h : ∀ s t, PatternModel.Matches pat s → PatternModel.Matches pat t → s.length = t.length) :
+    NoSuffixPatternModel pat where
+  eq_empty s t hs ht := by simpa using h t _ hs ht
+
+theorem isLongestRevMatch_iff_isRevMatch {ρ : Type} (pat : ρ) [PatternModel pat] [NoSuffixPatternModel pat]
+    {s : Slice} {pos : s.Pos} : IsLongestRevMatch pat pos ↔ IsRevMatch pat pos := by
+  refine ⟨fun h => h.isRevMatch, fun h => ⟨h, fun pos' hpos' hm => ?_⟩⟩
+  obtain ⟨t₁, t₂, ht₁, ht₂⟩ := isRevMatch_iff_exists_splits.1 h
+  obtain ⟨t₁', t₂', ht₁', ht₂'⟩ := isRevMatch_iff_exists_splits.1 hm
+  obtain ⟨t₅, ht₅, ht₅', ht₅''⟩ := (ht₁'.lt_iff_exists_eq_append ht₁).1 hpos'
+  exact ht₅ (NoSuffixPatternModel.eq_empty _ _ ht₂ (ht₅'' ▸ ht₂'))
 
 /--
 Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains is a match
 of {name}`pat` in {name}`s` and it is longest among matches starting at {name}`startPos`.
 -/
-structure IsLongestMatchAt (pat : ρ) [ForwardPatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop where
+structure IsLongestMatchAt (pat : ρ) [PatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop where
   le : startPos ≤ endPos
   isLongestMatch_sliceFrom : IsLongestMatch pat (Slice.Pos.sliceFrom _ _ le)
 
-theorem isLongestMatchAt_iff {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos₁ pos₂ : s.Pos} :
+theorem isLongestMatchAt_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos₁ pos₂ : s.Pos} :
     IsLongestMatchAt pat pos₁ pos₂ ↔
       ∃ (h : pos₁ ≤ pos₂), IsLongestMatch pat (Slice.Pos.sliceFrom _ _ h) :=
   ⟨fun ⟨h, h'⟩ => ⟨h, h'⟩, fun ⟨h, h'⟩ => ⟨h, h'⟩⟩
 
-theorem IsLongestMatchAt.lt {pat : ρ} [ForwardPatternModel pat] {s : Slice} {startPos endPos : s.Pos}
+theorem IsLongestMatchAt.lt {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
     (h : IsLongestMatchAt pat startPos endPos) : startPos < endPos := by
   have := h.isLongestMatch_sliceFrom.ne_startPos
   rw [← Pos.startPos_lt_iff, ← Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff] at this
   simpa
 
-theorem IsLongestMatchAt.eq {pat : ρ} [ForwardPatternModel pat] {s : Slice} {startPos endPos endPos' : s.Pos}
+theorem IsLongestMatchAt.eq {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos endPos' : s.Pos}
     (h : IsLongestMatchAt pat startPos endPos) (h' : IsLongestMatchAt pat startPos endPos') :
     endPos = endPos' := by
   simpa using h.isLongestMatch_sliceFrom.eq h'.isLongestMatch_sliceFrom
 
-private theorem isLongestMatch_of_eq {pat : ρ} [ForwardPatternModel pat] {s t : Slice}
+private theorem isLongestMatch_of_eq {pat : ρ} [PatternModel pat] {s t : Slice}
     {pos : s.Pos} {pos' : t.Pos} (h_eq : s = t) (h_pos : pos.offset = pos'.offset)
     (hm : IsLongestMatch pat pos) : IsLongestMatch pat pos' := by
   subst h_eq; exact (Slice.Pos.ext h_pos) ▸ hm
 
-theorem isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat]
+theorem isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom {pat : ρ} [PatternModel pat]
     {s : Slice} {base : s.Pos} {startPos endPos : (s.sliceFrom base).Pos} :
     IsLongestMatchAt pat startPos endPos ↔ IsLongestMatchAt pat (Pos.ofSliceFrom startPos) (Pos.ofSliceFrom endPos) := by
   constructor
@@ -187,35 +269,88 @@ theorem isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPat
     exact isLongestMatch_of_eq Slice.sliceFrom_sliceFrom.symm
       (by simp [Pos.Raw.ext_iff]; omega) h.isLongestMatch_sliceFrom
 
-theorem IsLongestMatch.isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat] {s : Slice}
+theorem IsLongestMatch.isLongestMatchAt_ofSliceFrom {pat : ρ} [PatternModel pat] {s : Slice}
     {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} (h : IsLongestMatch pat pos) :
     IsLongestMatchAt pat p₀ (Slice.Pos.ofSliceFrom pos) where
   le := Slice.Pos.le_ofSliceFrom
   isLongestMatch_sliceFrom := by simpa
 
 @[simp]
-theorem isLongestMatchAt_startPos_iff {pat : ρ} [ForwardPatternModel pat] {s : Slice} {endPos : s.Pos} :
+theorem isLongestMatchAt_startPos_iff {pat : ρ} [PatternModel pat] {s : Slice} {endPos : s.Pos} :
     IsLongestMatchAt pat s.startPos endPos ↔ IsLongestMatch pat endPos := by
   simpa [isLongestMatchAt_iff] using
     ⟨fun h => isLongestMatch_of_eq (by simp) (by simp) h,
      fun h => isLongestMatch_of_eq (by simp) (by simp) h⟩
 
+/--
+Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains is a match
+of {name}`pat` in {name}`s` and it is longest among matches ending at {name}`endPos`.
+-/
+structure IsLongestRevMatchAt (pat : ρ) [PatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop where
+  le : startPos ≤ endPos
+  isLongestRevMatch_sliceTo : IsLongestRevMatch pat (Slice.Pos.sliceTo _ _ le)
+
+theorem isLongestRevMatchAt_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos₁ pos₂ : s.Pos} :
+    IsLongestRevMatchAt pat pos₁ pos₂ ↔
+      ∃ (h : pos₁ ≤ pos₂), IsLongestRevMatch pat (Slice.Pos.sliceTo _ _ h) :=
+  ⟨fun ⟨h, h'⟩ => ⟨h, h'⟩, fun ⟨h, h'⟩ => ⟨h, h'⟩⟩
+
+theorem IsLongestRevMatchAt.lt {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
+    (h : IsLongestRevMatchAt pat startPos endPos) : startPos < endPos := by
+  have := h.isLongestRevMatch_sliceTo.ne_endPos
+  rw [← Pos.lt_endPos_iff, ← Slice.Pos.ofSliceTo_lt_ofSliceTo_iff] at this
+  simpa
+
+theorem IsLongestRevMatchAt.eq {pat : ρ} [PatternModel pat] {s : Slice} {startPos startPos' endPos : s.Pos}
+    (h : IsLongestRevMatchAt pat startPos endPos) (h' : IsLongestRevMatchAt pat startPos' endPos) :
+    startPos = startPos' := by
+  simpa using h.isLongestRevMatch_sliceTo.eq h'.isLongestRevMatch_sliceTo
+
+private theorem isLongestRevMatch_of_eq {pat : ρ} [PatternModel pat] {s t : Slice}
+    {pos : s.Pos} {pos' : t.Pos} (h_eq : s = t) (h_pos : pos.offset = pos'.offset)
+    (hm : IsLongestRevMatch pat pos) : IsLongestRevMatch pat pos' := by
+  subst h_eq; exact (Slice.Pos.ext h_pos) ▸ hm
+
+theorem isLongestRevMatchAt_iff_isLongestRevMatchAt_ofSliceTo {pat : ρ} [PatternModel pat]
+    {s : Slice} {base : s.Pos} {startPos endPos : (s.sliceTo base).Pos} :
+    IsLongestRevMatchAt pat startPos endPos ↔ IsLongestRevMatchAt pat (Pos.ofSliceTo startPos) (Pos.ofSliceTo endPos) := by
+  constructor
+  · intro h
+    refine ⟨Slice.Pos.ofSliceTo_le_ofSliceTo_iff.mpr h.le, ?_⟩
+    exact isLongestRevMatch_of_eq Slice.sliceTo_sliceTo (by simp) h.isLongestRevMatch_sliceTo
+  · intro h
+    refine ⟨Slice.Pos.ofSliceTo_le_ofSliceTo_iff.mp h.le, ?_⟩
+    exact isLongestRevMatch_of_eq Slice.sliceTo_sliceTo.symm (by simp) h.isLongestRevMatch_sliceTo
+
+theorem IsLongestRevMatch.isLongestRevMatchAt_ofSliceTo {pat : ρ} [PatternModel pat] {s : Slice}
+    {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} (h : IsLongestRevMatch pat pos) :
+    IsLongestRevMatchAt pat (Slice.Pos.ofSliceTo pos) p₀ where
+  le := Slice.Pos.ofSliceTo_le
+  isLongestRevMatch_sliceTo := by simpa
+
+@[simp]
+theorem isLongestRevMatchAt_endPos_iff {pat : ρ} [PatternModel pat] {s : Slice} {startPos : s.Pos} :
+    IsLongestRevMatchAt pat startPos s.endPos ↔ IsLongestRevMatch pat startPos := by
+  simpa [isLongestRevMatchAt_iff] using
+    ⟨fun h => isLongestRevMatch_of_eq (by simp) (by simp) h,
+     fun h => isLongestRevMatch_of_eq (by simp) (by simp) h⟩
+
 /--
 Predicate stating that there is a (longest) match starting at the given position.
 -/
-structure MatchesAt (pat : ρ) [ForwardPatternModel pat] {s : Slice} (pos : s.Pos) : Prop where
+structure MatchesAt (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) : Prop where
   exists_isLongestMatchAt : ∃ endPos, IsLongestMatchAt pat pos endPos
 
-theorem matchesAt_iff_exists_isLongestMatchAt {pat : ρ} [ForwardPatternModel pat] {s : Slice}
+theorem matchesAt_iff_exists_isLongestMatchAt {pat : ρ} [PatternModel pat] {s : Slice}
     {pos : s.Pos} : MatchesAt pat pos ↔ ∃ endPos, IsLongestMatchAt pat pos endPos :=
   ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩
 
-theorem matchesAt_iff_exists_isLongestMatch {pat : ρ} [ForwardPatternModel pat] {s : Slice}
+theorem matchesAt_iff_exists_isLongestMatch {pat : ρ} [PatternModel pat] {s : Slice}
     {pos : s.Pos} :
     MatchesAt pat pos ↔ ∃ (endPos : s.Pos), ∃ h, IsLongestMatch pat (pos.sliceFrom endPos h) :=
   ⟨fun ⟨p, h⟩ => ⟨p, h.le, h.isLongestMatch_sliceFrom⟩, fun ⟨p, h₁, h₂⟩ => ⟨p, ⟨h₁, h₂⟩⟩⟩
 
-theorem matchesAt_iff_exists_isMatch {pat : ρ} [ForwardPatternModel pat] {s : Slice}
+theorem matchesAt_iff_exists_isMatch {pat : ρ} [PatternModel pat] {s : Slice}
     {pos : s.Pos} :
     MatchesAt pat pos ↔ ∃ (endPos : s.Pos), ∃ h, IsMatch pat (pos.sliceFrom endPos h) := by
   refine ⟨fun ⟨p, h⟩ => ⟨p, h.le, h.isLongestMatch_sliceFrom.isMatch⟩, fun ⟨p, h₁, h₂⟩ => ?_⟩
@@ -225,13 +360,13 @@ theorem matchesAt_iff_exists_isMatch {pat : ρ} [ForwardPatternModel pat] {s : S
      by simpa using hq⟩⟩
 
 @[simp]
-theorem not_matchesAt_endPos {pat : ρ} [ForwardPatternModel pat] {s : Slice} :
+theorem not_matchesAt_endPos {pat : ρ} [PatternModel pat] {s : Slice} :
     ¬ MatchesAt pat s.endPos := by
   simp only [matchesAt_iff_exists_isMatch, Pos.endPos_le, exists_prop_eq]
   intro h
   simpa [← Pos.ofSliceFrom_inj] using h.ne_startPos
 
-theorem matchesAt_iff_matchesAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat] {s : Slice} {base : s.Pos}
+theorem matchesAt_iff_matchesAt_ofSliceFrom {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos}
     {pos : (s.sliceFrom base).Pos} : MatchesAt pat pos ↔ MatchesAt pat (Pos.ofSliceFrom pos) := by
   simp only [matchesAt_iff_exists_isLongestMatchAt]
   constructor
@@ -241,21 +376,66 @@ theorem matchesAt_iff_matchesAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat]
     exact ⟨base.sliceFrom endPos (Std.le_trans Slice.Pos.le_ofSliceFrom h.le),
            isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom.mpr (by simpa using h)⟩
 
-theorem IsLongestMatchAt.matchesAt {pat : ρ} [ForwardPatternModel pat] {s : Slice} {startPos endPos : s.Pos}
+theorem IsLongestMatchAt.matchesAt {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
     (h : IsLongestMatchAt pat startPos endPos) : MatchesAt pat startPos where
   exists_isLongestMatchAt := ⟨_, h⟩
 
+/--
+Predicate stating that there is a (longest) match ending at the given position.
+-/
+structure RevMatchesAt (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) : Prop where
+  exists_isLongestRevMatchAt : ∃ startPos, IsLongestRevMatchAt pat startPos pos
+
+theorem revMatchesAt_iff_exists_isLongestRevMatchAt {pat : ρ} [PatternModel pat] {s : Slice}
+    {pos : s.Pos} : RevMatchesAt pat pos ↔ ∃ startPos, IsLongestRevMatchAt pat startPos pos :=
+  ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩
+
+theorem revMatchesAt_iff_exists_isLongestRevMatch {pat : ρ} [PatternModel pat] {s : Slice}
+    {pos : s.Pos} :
+    RevMatchesAt pat pos ↔ ∃ (startPos : s.Pos), ∃ h, IsLongestRevMatch pat (pos.sliceTo startPos h) :=
+  ⟨fun ⟨p, h⟩ => ⟨p, h.le, h.isLongestRevMatch_sliceTo⟩, fun ⟨p, h₁, h₂⟩ => ⟨p, ⟨h₁, h₂⟩⟩⟩
+
+theorem revMatchesAt_iff_exists_isRevMatch {pat : ρ} [PatternModel pat] {s : Slice}
+    {pos : s.Pos} :
+    RevMatchesAt pat pos ↔ ∃ (startPos : s.Pos), ∃ h, IsRevMatch pat (pos.sliceTo startPos h) := by
+  refine ⟨fun ⟨p, h⟩ => ⟨p, h.le, h.isLongestRevMatch_sliceTo.isRevMatch⟩, fun ⟨p, h₁, h₂⟩ => ?_⟩
+  obtain ⟨q, hq⟩ := h₂.exists_isLongestRevMatch
+  exact ⟨Pos.ofSliceTo q,
+    ⟨Std.le_trans (by simpa [← Pos.ofSliceTo_le_ofSliceTo_iff] using hq.le_of_isRevMatch h₂) h₁,
+     by simpa using hq⟩⟩
+
+@[simp]
+theorem not_revMatchesAt_startPos {pat : ρ} [PatternModel pat] {s : Slice} :
+    ¬ RevMatchesAt pat s.startPos := by
+  simp only [revMatchesAt_iff_exists_isRevMatch, Pos.le_startPos, exists_prop_eq]
+  intro h
+  simpa [← Pos.ofSliceTo_inj] using h.ne_endPos
+
+theorem revMatchesAt_iff_revMatchesAt_ofSliceto {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos}
+    {pos : (s.sliceTo base).Pos} : RevMatchesAt pat pos ↔ RevMatchesAt pat (Pos.ofSliceTo pos) := by
+  simp only [revMatchesAt_iff_exists_isLongestRevMatchAt]
+  constructor
+  · rintro ⟨startPos, h⟩
+    exact ⟨Pos.ofSliceTo startPos, isLongestRevMatchAt_iff_isLongestRevMatchAt_ofSliceTo.mp h⟩
+  · rintro ⟨startPos, h⟩
+    exact ⟨base.sliceTo startPos (Std.le_trans h.le Slice.Pos.ofSliceTo_le),
+           isLongestRevMatchAt_iff_isLongestRevMatchAt_ofSliceTo.mpr (by simpa using h)⟩
+
+theorem IsLongestRevMatchAt.revMatchesAt {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
+    (h : IsLongestRevMatchAt pat startPos endPos) : RevMatchesAt pat endPos where
+  exists_isLongestRevMatchAt := ⟨_, h⟩
+
 open Classical in
 /--
 Noncomputable model function returning the end point of the longest match starting at the given
 position, or {lean}`none` if there is no match.
 -/
-noncomputable def matchAt? {ρ : Type} (pat : ρ) [ForwardPatternModel pat]
+noncomputable def matchAt? {ρ : Type} (pat : ρ) [PatternModel pat]
     {s : Slice} (startPos : s.Pos) : Option s.Pos :=
   if h : ∃ endPos, IsLongestMatchAt pat startPos endPos then some h.choose else none
 
 @[simp]
-theorem matchAt?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat]
+theorem matchAt?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat]
     {s : Slice} {startPos endPos : s.Pos} :
     matchAt? pat startPos = some endPos ↔ IsLongestMatchAt pat startPos endPos := by
   fun_cases matchAt? with
@@ -263,40 +443,92 @@ theorem matchAt?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat]
   | case2 => simp_all
 
 @[simp]
-theorem matchAt?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat]
+theorem matchAt?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat]
     {s : Slice} {startPos : s.Pos} :
     matchAt? pat startPos = none ↔ ¬ MatchesAt pat startPos := by
   fun_cases matchAt? with
   | case1 h => simpa using ⟨h⟩
   | case2 h => simpa using fun ⟨h'⟩ => h h'
 
+open Classical in
 /--
-Predicate stating compatibility between {name}`ForwardPatternModel` and {name}`ForwardPattern`.
+Noncomputable model function returning the start point of the longest match ending at the given
+position, or {lean}`none` if there is no match.
+-/
+noncomputable def revMatchAt? {ρ : Type} (pat : ρ) [PatternModel pat]
+    {s : Slice} (endPos : s.Pos) : Option s.Pos :=
+  if h : ∃ startPos, IsLongestRevMatchAt pat startPos endPos then some h.choose else none
+
+@[simp]
+theorem revMatchAt?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat]
+    {s : Slice} {startPos endPos : s.Pos} :
+    revMatchAt? pat endPos = some startPos ↔ IsLongestRevMatchAt pat startPos endPos := by
+  fun_cases revMatchAt? with
+  | case1 h => simpa using ⟨by rintro rfl; exact h.choose_spec, fun h' => h.choose_spec.eq h'⟩
+  | case2 => simp_all
+
+@[simp]
+theorem revMatchAt?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat]
+    {s : Slice} {endPos : s.Pos} :
+    revMatchAt? pat endPos = none ↔ ¬ RevMatchesAt pat endPos := by
+  fun_cases revMatchAt? with
+  | case1 h => simpa using ⟨h⟩
+  | case2 h => simpa using fun ⟨h'⟩ => h h'
+
+/--
+Predicate stating compatibility between {name}`PatternModel` and {name}`ForwardPattern`.
 
 This extends {name}`LawfulForwardPattern`, but it is much stronger because it forces the
 {name}`ForwardPattern` to match the longest prefix of the given slice that matches the property
-supplied by the {name}`ForwardPatternModel` instance.
+supplied by the {name}`PatternModel` instance.
 -/
 class LawfulForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPattern pat]
-    [ForwardPatternModel pat] : Prop extends LawfulForwardPattern pat where
+    [PatternModel pat] : Prop extends LawfulForwardPattern pat where
   skipPrefix?_eq_some_iff (pos) : ForwardPattern.skipPrefix? pat s = some pos ↔ IsLongestMatch pat pos
 
-open Classical in
-theorem LawfulForwardPatternModel.skipPrefix?_sliceFrom_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel pat]
+theorem LawfulForwardPatternModel.skipPrefix?_sliceFrom_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
     [LawfulForwardPatternModel pat] {s : Slice} {p₀ : s.Pos} :
     ForwardPattern.skipPrefix? pat (s.sliceFrom p₀) = none ↔ ¬ MatchesAt pat p₀ := by
+  classical
   rw [← Decidable.not_iff_not]
   simp [Option.ne_none_iff_exists', LawfulForwardPatternModel.skipPrefix?_eq_some_iff]
   refine ⟨fun ⟨p, hp⟩ => ?_, fun ⟨p, hp⟩ => ?_⟩
   · exact ⟨Slice.Pos.ofSliceFrom p, hp.isLongestMatchAt_ofSliceFrom⟩
   · exact ⟨p₀.sliceFrom p hp.le, hp.isLongestMatch_sliceFrom⟩
 
-theorem LawfulForwardPatternModel.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel pat]
+theorem LawfulForwardPatternModel.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
     [LawfulForwardPatternModel pat] {s : Slice} :
     ForwardPattern.skipPrefix? pat s = none ↔ ¬ MatchesAt pat s.startPos := by
   conv => lhs; rw [← sliceFrom_startPos (s := s)]
   simp [skipPrefix?_sliceFrom_eq_none_iff]
 
+/--
+Predicate stating compatibility between {name}`PatternModel` and {name}`BackwardPattern`.
+
+This extends {name}`LawfulForwardPattern`, but it is much stronger because it forces the
+{name}`ForwardPattern` to match the longest prefix of the given slice that matches the property
+supplied by the {name}`PatternModel` instance.
+-/
+class LawfulBackwardPatternModel {ρ : Type} (pat : ρ) [BackwardPattern pat]
+    [PatternModel pat] : Prop extends LawfulBackwardPattern pat where
+  skipSuffix?_eq_some_iff (pos) : BackwardPattern.skipSuffix? pat s = some pos ↔ IsLongestRevMatch pat pos
+
+theorem LawfulBackwardPatternModel.skipSuffix?_sliceTo_eq_none_iff {ρ : Type} {pat : ρ} [BackwardPattern pat] [PatternModel pat]
+    [LawfulBackwardPatternModel pat] {s : Slice} {p₀ : s.Pos} :
+    BackwardPattern.skipSuffix? pat (s.sliceTo p₀) = none ↔ ¬ RevMatchesAt pat p₀ := by
+  classical
+  rw [← Decidable.not_iff_not]
+  simp [Option.ne_none_iff_exists', LawfulBackwardPatternModel.skipSuffix?_eq_some_iff]
+  refine ⟨fun ⟨p, hp⟩ => ?_, fun ⟨p, hp⟩ => ?_⟩
+  · exact ⟨Slice.Pos.ofSliceTo p, hp.isLongestRevMatchAt_ofSliceTo⟩
+  · exact ⟨p₀.sliceTo p hp.le, hp.isLongestRevMatch_sliceTo⟩
+
+theorem LawfulBackwardPatternModel.skipSuffix?_eq_none_iff {ρ : Type} {pat : ρ} [BackwardPattern pat] [PatternModel pat]
+    [LawfulBackwardPatternModel pat] {s : Slice} :
+    BackwardPattern.skipSuffix? pat s = none ↔ ¬ RevMatchesAt pat s.endPos := by
+  conv => lhs; rw [← sliceTo_endPos (s := s)]
+  simp [skipSuffix?_sliceTo_eq_none_iff]
+
 /--
 Inductive predicate stating that a list of search steps represents a valid search from a given
 position in a slice.
@@ -306,7 +538,7 @@ matches.
 
 Hence, this predicate determines the list of search steps up to grouping of rejections.
 -/
-inductive IsValidSearchFrom (pat : ρ) [ForwardPatternModel pat] {s : Slice} :
+inductive IsValidSearchFrom (pat : ρ) [PatternModel pat] {s : Slice} :
     s.Pos → List (SearchStep s) → Prop where
   | endPos : IsValidSearchFrom pat s.endPos []
   | matched {startPos endPos : s.Pos} :
@@ -316,14 +548,14 @@ inductive IsValidSearchFrom (pat : ρ) [ForwardPatternModel pat] {s : Slice} :
       (∀ pos, startPos ≤ pos → pos < endPos → ¬ MatchesAt pat pos) →
       IsValidSearchFrom pat endPos l → IsValidSearchFrom pat startPos (.rejected startPos endPos :: l)
 
-theorem IsValidSearchFrom.matched_of_eq {pat : ρ} [ForwardPatternModel pat] {s : Slice}
+theorem IsValidSearchFrom.matched_of_eq {pat : ρ} [PatternModel pat] {s : Slice}
     {startPos startPos' endPos : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidSearchFrom pat endPos l)
     (h₂ : IsLongestMatchAt pat startPos' endPos)
     (h₃ : startPos = startPos') : IsValidSearchFrom pat startPos' (.matched startPos endPos :: l) := by
   cases h₃
   exact IsValidSearchFrom.matched h₂ h₁
 
-theorem IsValidSearchFrom.mismatched_of_eq {pat : ρ} [ForwardPatternModel pat] {s : Slice}
+theorem IsValidSearchFrom.mismatched_of_eq {pat : ρ} [PatternModel pat] {s : Slice}
     {startPos startPos' endPos : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidSearchFrom pat endPos l)
       (h₀ : startPos' < endPos)
       (h₂ : ∀ pos, startPos' ≤ pos → pos < endPos → ¬ MatchesAt pat pos) (h₃ : startPos = startPos') :
@@ -331,7 +563,7 @@ theorem IsValidSearchFrom.mismatched_of_eq {pat : ρ} [ForwardPatternModel pat]
   cases h₃
   exact IsValidSearchFrom.mismatched h₀ h₂ h₁
 
-theorem IsValidSearchFrom.endPos_of_eq {pat : ρ} [ForwardPatternModel pat] {s : Slice}
+theorem IsValidSearchFrom.endPos_of_eq {pat : ρ} [PatternModel pat] {s : Slice}
     {p : s.Pos} {l : List (SearchStep s)} (hp : p = s.endPos) (hl : l = []) :
     IsValidSearchFrom pat p l := by
   cases hp
@@ -339,18 +571,18 @@ theorem IsValidSearchFrom.endPos_of_eq {pat : ρ} [ForwardPatternModel pat] {s :
   exact IsValidSearchFrom.endPos
 
 /--
-Predicate stating compatibility between {name}`ForwardPatternModel` and {name}`ToForwardSearcher`.
+Predicate stating compatibility between {name}`PatternModel` and {name}`ToForwardSearcher`.
 
 We require the searcher to always match the longest match at the first position where the pattern
 matches; see {name}`IsValidSearchFrom`.
 -/
-class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type}
+class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type}
     [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
     [∀ s, Std.Iterators.Finite (σ s) Id] : Prop where
   isValidSearchFrom_toList (s) : IsValidSearchFrom pat s.startPos (ToForwardSearcher.toSearcher pat s).toList
 
 theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPattern pat] [StrictForwardPattern pat]
-    [ForwardPatternModel pat] [LawfulForwardPatternModel pat] :
+    [PatternModel pat] [LawfulForwardPatternModel pat] :
     letI : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation
     LawfulToForwardSearcherModel pat := by
   let inst : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation
@@ -390,4 +622,97 @@ theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPa
     · split at heq <;> simp at heq
     · split at heq <;> simp at heq
 
+/--
+Inductive predicate stating that a list of search steps represents a valid backwards search from a
+given position in a slice.
+
+"Searching" here means always taking the longest match at the first position where the pattern
+matches.
+
+Hence, this predicate determines the list of search steps up to grouping of rejections.
+-/
+inductive IsValidRevSearchFrom (pat : ρ) [PatternModel pat] {s : Slice} :
+    s.Pos → List (SearchStep s) → Prop where
+  | startPos : IsValidRevSearchFrom pat s.startPos []
+  | matched {startPos endPos : s.Pos} :
+      IsLongestRevMatchAt pat startPos endPos → IsValidRevSearchFrom pat startPos l →
+      IsValidRevSearchFrom pat endPos (.matched startPos endPos :: l)
+  | mismatched {startPos endPos : s.Pos} : startPos < endPos →
+      (∀ pos, startPos < pos → pos ≤ endPos → ¬ RevMatchesAt pat pos) →
+      IsValidRevSearchFrom pat startPos l → IsValidRevSearchFrom pat endPos (.rejected startPos endPos :: l)
+
+theorem IsValidRevSearchFrom.matched_of_eq {pat : ρ} [PatternModel pat] {s : Slice}
+    {startPos endPos endPos' : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidRevSearchFrom pat startPos l)
+    (h₂ : IsLongestRevMatchAt pat startPos endPos')
+    (h₃ : endPos = endPos') : IsValidRevSearchFrom pat endPos' (.matched startPos endPos :: l) := by
+  cases h₃
+  exact IsValidRevSearchFrom.matched h₂ h₁
+
+theorem IsValidRevSearchFrom.mismatched_of_eq {pat : ρ} [PatternModel pat] {s : Slice}
+    {startPos endPos endPos' : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidRevSearchFrom pat startPos l)
+      (h₀ : startPos < endPos')
+      (h₂ : ∀ pos, startPos < pos → pos ≤ endPos' → ¬ RevMatchesAt pat pos) (h₃ : endPos = endPos') :
+      IsValidRevSearchFrom pat endPos' (.rejected startPos endPos :: l) := by
+  cases h₃
+  exact IsValidRevSearchFrom.mismatched h₀ h₂ h₁
+
+theorem IsValidRevSearchFrom.startPos_of_eq {pat : ρ} [PatternModel pat] {s : Slice}
+    {p : s.Pos} {l : List (SearchStep s)} (hp : p = s.startPos) (hl : l = []) :
+    IsValidRevSearchFrom pat p l := by
+  cases hp
+  cases hl
+  exact IsValidRevSearchFrom.startPos
+
+/--
+Predicate stating compatibility between {name}`PatternModel` and {name}`ToBackwardSearcher`.
+
+We require the searcher to always match the longest match at the first position where the pattern
+matches; see {name}`IsValidRevSearchFrom`.
+-/
+class LawfulToBackwardSearcherModel {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type}
+    [ToBackwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
+    [∀ s, Std.Iterators.Finite (σ s) Id] : Prop where
+  isValidRevSearchFrom_toList (s) : IsValidRevSearchFrom pat s.endPos (ToBackwardSearcher.toSearcher pat s).toList
+
+theorem LawfulToBackwardSearcherModel.defaultImplementation {pat : ρ} [BackwardPattern pat] [StrictBackwardPattern pat]
+    [PatternModel pat] [LawfulBackwardPatternModel pat] :
+    letI : ToBackwardSearcher pat (ToBackwardSearcher.DefaultBackwardSearcher pat) := .defaultImplementation
+    LawfulToBackwardSearcherModel pat := by
+  let inst : ToBackwardSearcher pat (ToBackwardSearcher.DefaultBackwardSearcher pat) := .defaultImplementation
+  refine ⟨fun s => ?_⟩
+  suffices ∀ (pos : s.Pos),
+      IsValidRevSearchFrom pat pos (Std.Iter.mk (α := ToBackwardSearcher.DefaultBackwardSearcher pat s) ⟨pos⟩).toList from
+    this s.endPos
+  intro pos
+  induction pos using WellFounded.induction Slice.Pos.wellFounded_lt with | h pos ih
+  rw [Std.Iter.toList_eq_match_step, Std.Iter.step_eq]
+  simp only [Std.Iter.toIterM, ne_eq]
+  by_cases h : pos = s.startPos
+  · simpa [h] using IsValidRevSearchFrom.startPos
+  · simp only [h, ↓reduceDIte]
+    split <;> rename_i heq
+    · split at heq <;> rename_i pos' heq'
+      · simp only [Id.run_pure, Std.Shrink.inflate_deflate, Std.IterM.Step.toPure_yield,
+          Std.PlausibleIterStep.yield, Std.IterStep.yield.injEq] at heq
+        rw [← heq.1, ← heq.2]
+        apply IsValidRevSearchFrom.matched
+        · rw [LawfulBackwardPattern.skipSuffixOfNonempty?_eq,
+            LawfulBackwardPatternModel.skipSuffix?_eq_some_iff] at heq'
+          exact heq'.isLongestRevMatchAt_ofSliceTo
+        · simp only [Std.IterM.toIter]
+          apply ih
+          refine Std.lt_of_lt_of_le (Slice.Pos.ofSliceTo_lt_ofSliceTo_iff.2 ?_)
+            (Slice.Pos.ofSliceTo_le (pos := Slice.endPos _))
+          simpa using StrictBackwardPattern.ne_endPos _ _ heq'
+      · simp only [Id.run_pure, Std.Shrink.inflate_deflate, Std.IterM.Step.toPure_yield,
+          Std.PlausibleIterStep.yield, Std.IterStep.yield.injEq] at heq
+        rw [← heq.1, ← heq.2]
+        apply IsValidRevSearchFrom.mismatched (by simp) _ (ih _ (by simp))
+        intro p' hp' hp''
+        obtain rfl : pos = p' := Std.le_antisymm (by simpa using hp') hp''
+        rwa [LawfulBackwardPattern.skipSuffixOfNonempty?_eq,
+          LawfulBackwardPatternModel.skipSuffix?_sliceTo_eq_none_iff] at heq'
+    · split at heq <;> simp at heq
+    · split at heq <;> simp at heq
+
 end String.Slice.Pattern.Model

src/Init/Data/String/Lemmas/Pattern/Char.lean

@@ -20,28 +20,42 @@ import Init.Data.String.Lemmas.Order
 import Init.Data.Order.Lemmas
 import Init.Data.String.OrderInstances
 import Init.Omega
+import Init.Data.String.Lemmas.FindPos
 
 public section
 
 namespace String.Slice.Pattern.Model.Char
 
-instance {c : Char} : ForwardPatternModel c where
+instance {c : Char} : PatternModel c where
   Matches s := s = String.singleton c
   not_matches_empty := by simp
 
-instance {c : Char} : NoPrefixForwardPatternModel c :=
-  .of_length_eq (by simp +contextual [ForwardPatternModel.Matches])
+instance {c : Char} : NoPrefixPatternModel c :=
+  .of_length_eq (by simp +contextual [PatternModel.Matches])
+
+instance {c : Char} : NoSuffixPatternModel c :=
+  .of_length_eq (by simp +contextual [PatternModel.Matches])
 
 theorem isMatch_iff {c : Char} {s : Slice} {pos : s.Pos} :
     IsMatch c pos ↔
       ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c := by
-  simp only [Model.isMatch_iff, ForwardPatternModel.Matches, sliceTo_copy_eq_iff_exists_splits]
+  simp only [Model.isMatch_iff, PatternModel.Matches, copy_sliceTo_eq_iff_exists_splits]
   refine ⟨?_, ?_⟩
   · simp only [splits_singleton_iff]
     exact fun ⟨t₂, h, h₁, h₂, h₃⟩ => ⟨h, h₁, h₂⟩
   · rintro ⟨h, rfl, rfl⟩
     exact ⟨_, Slice.splits_next_startPos⟩
 
+theorem isRevMatch_iff {c : Char} {s : Slice} {pos : s.Pos} :
+    IsRevMatch c pos ↔
+      ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get (by simp) = c := by
+  simp only [Model.isRevMatch_iff, PatternModel.Matches, copy_sliceFrom_eq_iff_exists_splits]
+  refine ⟨?_, ?_⟩
+  · simp only [splits_singleton_right_iff]
+    exact fun ⟨t₂, h, h₁, h₂, h₃⟩ => ⟨h, h₁, h₂⟩
+  · rintro ⟨h, rfl, rfl⟩
+    exact ⟨_, Slice.splits_prev_endPos⟩
+
 theorem isLongestMatch_iff {c : Char} {s : Slice} {pos : s.Pos} :
     IsLongestMatch c pos ↔
       ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c := by
@@ -52,21 +66,46 @@ theorem isLongestMatchAt_iff {c : Char} {s : Slice} {pos pos' : s.Pos} :
   simp +contextual [Model.isLongestMatchAt_iff, isLongestMatch_iff, ← Pos.ofSliceFrom_inj,
     Pos.get_eq_get_ofSliceFrom, Pos.ofSliceFrom_next]
 
+theorem isLongestRevMatch_iff {c : Char} {s : Slice} {pos : s.Pos} :
+    IsLongestRevMatch c pos ↔
+      ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get (by simp) = c := by
+  rw [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff]
+
+theorem isLongestRevMatchAt_iff {c : Char} {s : Slice} {pos pos' : s.Pos} :
+    IsLongestRevMatchAt c pos pos' ↔ ∃ h, pos = pos'.prev h ∧ (pos'.prev h).get (by simp) = c := by
+  simp +contextual [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff, ← Pos.ofSliceTo_inj,
+    Pos.get_eq_get_ofSliceTo, Pos.ofSliceTo_prev]
+
 theorem isLongestMatchAt_of_get_eq {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos}
     (hc : pos.get h = c) : IsLongestMatchAt c pos (pos.next h) :=
   isLongestMatchAt_iff.2 ⟨h, by simp [hc]⟩
 
+theorem isLongestRevMatchAt_of_get_eq {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos}
+    (hc : (pos.prev h).get (by simp) = c) : IsLongestRevMatchAt c (pos.prev h) pos :=
+  isLongestRevMatchAt_iff.2 ⟨h, by simp [hc]⟩
+
 instance {c : Char} : LawfulForwardPatternModel c where
   skipPrefix?_eq_some_iff {s} pos := by
     simp [isLongestMatch_iff, ForwardPattern.skipPrefix?, and_comm, eq_comm (b := pos)]
 
+instance {c : Char} : LawfulBackwardPatternModel c where
+  skipSuffix?_eq_some_iff {s} pos := by
+    simp [isLongestRevMatch_iff, BackwardPattern.skipSuffix?, and_comm, eq_comm (b := pos)]
+
 theorem toSearcher_eq {c : Char} {s : Slice} :
   ToForwardSearcher.toSearcher c s = ToForwardSearcher.toSearcher (· == c) s := (rfl)
 
+theorem toBackwardSearcher_eq {c : Char} {s : Slice} :
+  ToBackwardSearcher.toSearcher c s = ToBackwardSearcher.toSearcher (· == c) s := (rfl)
+
 theorem matchesAt_iff {c : Char} {s : Slice} {pos : s.Pos} :
     MatchesAt c pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c := by
   simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff, exists_comm]
 
+theorem revMatchesAt_iff {c : Char} {s : Slice} {pos : s.Pos} :
+    RevMatchesAt c pos ↔ ∃ (h : pos ≠ s.startPos), (pos.prev h).get (by simp) = c := by
+  simp [revMatchesAt_iff_exists_isLongestRevMatchAt, isLongestRevMatchAt_iff, exists_comm]
+
 theorem matchesAt_iff_splits {c : Char} {s : Slice} {pos : s.Pos} :
     MatchesAt c pos ↔ ∃ t₁ t₂, pos.Splits t₁ (singleton c ++ t₂) := by
   rw [matchesAt_iff]
@@ -77,37 +116,81 @@ theorem matchesAt_iff_splits {c : Char} {s : Slice} {pos : s.Pos} :
     have hne := hs.ne_endPos_of_singleton
     exact ⟨hne, (singleton_append_inj.mp (hs.eq_right (pos.splits_next_right hne))).1.symm⟩
 
+theorem revMatchesAt_iff_splits {c : Char} {s : Slice} {pos : s.Pos} :
+    RevMatchesAt c pos ↔ ∃ t₁ t₂, pos.Splits (t₁ ++ singleton c) t₂ := by
+  rw [revMatchesAt_iff]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨h, rfl⟩
+    exact ⟨_, _, pos.splits_prev_right h⟩
+  · rintro ⟨t₁, t₂, hs⟩
+    have hne := hs.ne_startPos_of_singleton
+    refine ⟨hne, ?_⟩
+    have := hs.eq_left (pos.splits_prev_right hne)
+    simp only [append_singleton, push_inj] at this
+    exact this.2.symm
+
 theorem not_matchesAt_of_get_ne {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos}
     (hc : pos.get h ≠ c) : ¬ MatchesAt c pos := by
   simp [matchesAt_iff, hc]
 
+theorem not_revMatchesAt_of_get_ne {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos}
+    (hc : (pos.prev h).get (by simp) ≠ c) : ¬ RevMatchesAt c pos := by
+  simp [revMatchesAt_iff, hc]
+
 theorem matchAt?_eq {s : Slice} {pos : s.Pos} {c : Char} :
     matchAt? c pos =
       if h₀ : ∃ (h : pos ≠ s.endPos), pos.get h = c then some (pos.next h₀.1) else none := by
   split <;> simp_all [isLongestMatchAt_iff, matchesAt_iff]
 
+theorem revMatchAt?_eq {s : Slice} {pos : s.Pos} {c : Char} :
+    revMatchAt? c pos =
+      if h₀ : ∃ (h : pos ≠ s.startPos), (pos.prev h).get (by simp) = c then some (pos.prev h₀.1) else none := by
+  split <;> simp_all [isLongestRevMatchAt_iff, revMatchesAt_iff]
+
 theorem isMatch_iff_isMatch_beq {c : Char} {s : Slice} {pos : s.Pos} :
     IsMatch c pos ↔ IsMatch (· == c) pos := by
   simp [isMatch_iff, CharPred.isMatch_iff, beq_iff_eq]
 
+theorem isRevMatch_iff_isRevMatch_beq {c : Char} {s : Slice} {pos : s.Pos} :
+    IsRevMatch c pos ↔ IsRevMatch (· == c) pos := by
+  simp [isRevMatch_iff, CharPred.isRevMatch_iff, beq_iff_eq]
+
 theorem isLongestMatch_iff_isLongestMatch_beq {c : Char} {s : Slice} {pos : s.Pos} :
     IsLongestMatch c pos ↔ IsLongestMatch (· == c) pos := by
   simp [isLongestMatch_iff_isMatch, isMatch_iff_isMatch_beq]
 
+theorem isLongestRevMatch_iff_isLongestRevMatch_beq {c : Char} {s : Slice} {pos : s.Pos} :
+    IsLongestRevMatch c pos ↔ IsLongestRevMatch (· == c) pos := by
+  simp [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff_isRevMatch_beq]
+
 theorem isLongestMatchAt_iff_isLongestMatchAt_beq {c : Char} {s : Slice}
     {pos pos' : s.Pos} :
     IsLongestMatchAt c pos pos' ↔ IsLongestMatchAt (· == c) pos pos' := by
   simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_isLongestMatch_beq]
 
+theorem isLongestRevMatchAt_iff_isLongestRevMatchAt_beq {c : Char} {s : Slice}
+    {pos pos' : s.Pos} :
+    IsLongestRevMatchAt c pos pos' ↔ IsLongestRevMatchAt (· == c) pos pos' := by
+  simp [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff_isLongestRevMatch_beq]
+
 theorem matchesAt_iff_matchesAt_beq {c : Char} {s : Slice} {pos : s.Pos} :
     MatchesAt c pos ↔ MatchesAt (· == c) pos := by
   simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_beq]
 
+theorem revMatchesAt_iff_revMatchesAt_beq {c : Char} {s : Slice} {pos : s.Pos} :
+    RevMatchesAt c pos ↔ RevMatchesAt (· == c) pos := by
+  simp [revMatchesAt_iff_exists_isLongestRevMatchAt, isLongestRevMatchAt_iff_isLongestRevMatchAt_beq]
+
 theorem matchAt?_eq_matchAt?_beq {c : Char} {s : Slice} {pos : s.Pos} :
     matchAt? c pos = matchAt? (· == c) pos := by
   refine Option.ext (fun pos' => ?_)
   simp [matchAt?_eq_some_iff, isLongestMatchAt_iff_isLongestMatchAt_beq]
 
+theorem revMatchAt?_eq_revMatchAt?_beq {c : Char} {s : Slice} {pos : s.Pos} :
+    revMatchAt? c pos = revMatchAt? (· == c) pos := by
+  refine Option.ext (fun pos' => ?_)
+  simp [revMatchAt?_eq_some_iff, isLongestRevMatchAt_iff_isLongestRevMatchAt_beq]
+
 theorem isValidSearchFrom_iff_isValidSearchFrom_beq {c : Char} {s : Slice} {p : s.Pos}
     {l : List (SearchStep s)} : IsValidSearchFrom c p l ↔ IsValidSearchFrom (· == c) p l := by
   refine ⟨fun h => ?_, fun h => ?_⟩
@@ -120,11 +203,28 @@ theorem isValidSearchFrom_iff_isValidSearchFrom_beq {c : Char} {s : Slice} {p :
     | matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_beq]
     | mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_beq]
 
+theorem isValidRevSearchFrom_iff_isValidRevSearchFrom_beq {c : Char} {s : Slice} {p : s.Pos}
+    {l : List (SearchStep s)} : IsValidRevSearchFrom c p l ↔ IsValidRevSearchFrom (· == c) p l := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · induction h with
+    | startPos => simpa using IsValidRevSearchFrom.startPos
+    | matched => simp_all [IsValidRevSearchFrom.matched, isLongestRevMatchAt_iff_isLongestRevMatchAt_beq]
+    | mismatched => simp_all [IsValidRevSearchFrom.mismatched, revMatchesAt_iff_revMatchesAt_beq]
+  · induction h with
+    | startPos => simpa using IsValidRevSearchFrom.startPos
+    | matched => simp_all [IsValidRevSearchFrom.matched, isLongestRevMatchAt_iff_isLongestRevMatchAt_beq]
+    | mismatched => simp_all [IsValidRevSearchFrom.mismatched, revMatchesAt_iff_revMatchesAt_beq]
+
 instance {c : Char} : LawfulToForwardSearcherModel c where
   isValidSearchFrom_toList s := by
     simpa [toSearcher_eq, isValidSearchFrom_iff_isValidSearchFrom_beq] using
       LawfulToForwardSearcherModel.isValidSearchFrom_toList (pat := (· == c)) (s := s)
 
+instance {c : Char} : LawfulToBackwardSearcherModel c where
+  isValidRevSearchFrom_toList s := by
+    simpa [toBackwardSearcher_eq, isValidRevSearchFrom_iff_isValidRevSearchFrom_beq] using
+      LawfulToBackwardSearcherModel.isValidRevSearchFrom_toList (pat := (· == c)) (s := s)
+
 end Pattern.Model.Char
 
 theorem startsWith_char_eq_startsWith_beq {c : Char} {s : Slice} :

src/Init/Data/String/Lemmas/Pattern/Find/Basic.lean

@@ -23,7 +23,7 @@ open Std String.Slice Pattern Pattern.Model
 
 namespace String.Slice
 
-theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type}
+theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type}
     [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
     [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
     [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} :
@@ -40,7 +40,7 @@ theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [ForwardPatternMo
   | matched h₁ _ _ => have := h₁.matchesAt; grind
   | mismatched => grind
 
-theorem Pattern.Model.find?_eq_none_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type}
+theorem Pattern.Model.find?_eq_none_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type}
     [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
     [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
     [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} :
@@ -65,14 +65,14 @@ theorem find?_eq_none_iff {ρ : Type} (pat : ρ) {σ : Slice → Type}
     [ToForwardSearcher pat σ] {s : Slice} : s.find? pat = none ↔ s.contains pat = false := by
   rw [← Option.isNone_iff_eq_none, ← Option.isSome_eq_false_iff, isSome_find?]
 
-theorem Pattern.Model.contains_eq_false_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type}
+theorem Pattern.Model.contains_eq_false_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type}
     [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
     [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
     [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} :
     s.contains pat = false ↔ ∀ (pos : s.Pos), ¬ MatchesAt pat pos := by
   rw [← find?_eq_none_iff, Slice.find?_eq_none_iff]
 
-theorem Pattern.Model.contains_eq_true_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type}
+theorem Pattern.Model.contains_eq_true_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type}
     [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
     [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
     [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} :
@@ -85,7 +85,7 @@ theorem Pos.find?_eq_find?_sliceFrom {ρ : Type} {pat : ρ} {σ : Slice → Type
     p.find? pat = ((s.sliceFrom p).find? pat).map Pos.ofSliceFrom :=
   (rfl)
 
-theorem Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {σ : Slice → Type}
+theorem Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] {σ : Slice → Type}
     [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
     [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
     [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos pos' : s.Pos} :
@@ -100,7 +100,7 @@ theorem Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatter
     refine ⟨Pos.sliceFrom _ _ h₁, ⟨by simpa using h₂, fun p hp₁ hp₂ => ?_⟩, by simp⟩
     exact h₃ (Pos.ofSliceFrom p) Slice.Pos.le_ofSliceFrom (Pos.lt_sliceFrom_iff.1 hp₁) hp₂
 
-theorem Pattern.Model.posFind?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {σ : Slice → Type}
+theorem Pattern.Model.posFind?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] {σ : Slice → Type}
     [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
     [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
     [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} :

src/Init/Data/String/Lemmas/Pattern/Pred.lean

@@ -19,124 +19,228 @@ import Init.Data.String.Lemmas.Order
 import Init.Data.Order.Lemmas
 import Init.Data.String.OrderInstances
 import Init.Omega
+import Init.Data.String.Lemmas.FindPos
 
 public section
 
 namespace String.Slice.Pattern.Model.CharPred
 
-instance {p : Char → Bool} : ForwardPatternModel p where
+instance {p : Char → Bool} : PatternModel p where
   Matches s := ∃ c, s = singleton c ∧ p c
   not_matches_empty := by
     simp
 
-instance {p : Char → Bool} : NoPrefixForwardPatternModel p :=
-  .of_length_eq (by simp +contextual [ForwardPatternModel.Matches])
+instance {p : Char → Bool} : NoPrefixPatternModel p :=
+  .of_length_eq (by simp +contextual [PatternModel.Matches])
+
+instance {p : Char → Bool} : NoSuffixPatternModel p :=
+  .of_length_eq (by simp +contextual [PatternModel.Matches])
 
 theorem isMatch_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
     IsMatch p pos ↔
       ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) := by
-  simp only [Model.isMatch_iff, ForwardPatternModel.Matches, sliceTo_copy_eq_iff_exists_splits]
+  simp only [Model.isMatch_iff, PatternModel.Matches, copy_sliceTo_eq_iff_exists_splits]
   refine ⟨?_, ?_⟩
   · simp only [splits_singleton_iff]
     refine fun ⟨c, ⟨t₂, h, h₁, h₂, h₃⟩, hc⟩ => ⟨h, h₁, h₂ ▸ hc⟩
   · rintro ⟨h, rfl, h'⟩
     exact ⟨s.startPos.get h, ⟨_, Slice.splits_next_startPos⟩, h'⟩
 
+theorem isRevMatch_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
+    IsRevMatch p pos ↔
+      ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get (by simp)) := by
+  simp only [Model.isRevMatch_iff, PatternModel.Matches, copy_sliceFrom_eq_iff_exists_splits]
+  refine ⟨?_, ?_⟩
+  · simp only [splits_singleton_right_iff]
+    refine fun ⟨c, ⟨t₂, h, h₁, h₂, h₃⟩, hc⟩ => ⟨h, h₁, h₂ ▸ hc⟩
+  · rintro ⟨h, rfl, h'⟩
+    exact ⟨(s.endPos.prev h).get (by simp), ⟨_, Slice.splits_prev_endPos⟩, h'⟩
+
 theorem isLongestMatch_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
     IsLongestMatch p pos ↔
       ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) := by
   rw [isLongestMatch_iff_isMatch, isMatch_iff]
 
+theorem isLongestRevMatch_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
+    IsLongestRevMatch p pos ↔
+      ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get (by simp)) := by
+  rw [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff]
+
 theorem isLongestMatchAt_iff {p : Char → Bool} {s : Slice} {pos pos' : s.Pos} :
     IsLongestMatchAt p pos pos' ↔ ∃ h, pos' = pos.next h ∧ p (pos.get h) := by
   simp +contextual [Model.isLongestMatchAt_iff, isLongestMatch_iff, ← Pos.ofSliceFrom_inj,
     Pos.get_eq_get_ofSliceFrom, Pos.ofSliceFrom_next]
 
+theorem isLongestRevMatchAt_iff {p : Char → Bool} {s : Slice} {pos pos' : s.Pos} :
+    IsLongestRevMatchAt p pos pos' ↔ ∃ h, pos = pos'.prev h ∧ p ((pos'.prev h).get (by simp)) := by
+  simp +contextual [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff, ← Pos.ofSliceTo_inj,
+    Pos.get_eq_get_ofSliceTo, Pos.ofSliceTo_prev]
+
 theorem isLongestMatchAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos}
     (hc : p (pos.get h)) : IsLongestMatchAt p pos (pos.next h) :=
   isLongestMatchAt_iff.2 ⟨h, by simp [hc]⟩
 
+theorem isLongestRevMatchAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos}
+    (hc : p ((pos.prev h).get (by simp))) : IsLongestRevMatchAt p (pos.prev h) pos :=
+  isLongestRevMatchAt_iff.2 ⟨h, by simp [hc]⟩
+
 instance {p : Char → Bool} : LawfulForwardPatternModel p where
   skipPrefix?_eq_some_iff {s} pos := by
     simp [isLongestMatch_iff, ForwardPattern.skipPrefix?, and_comm, eq_comm (b := pos)]
 
+instance {p : Char → Bool} : LawfulBackwardPatternModel p where
+  skipSuffix?_eq_some_iff {s} pos := by
+    simp [isLongestRevMatch_iff, BackwardPattern.skipSuffix?, and_comm, eq_comm (b := pos)]
+
 instance {p : Char → Bool} : LawfulToForwardSearcherModel p :=
   .defaultImplementation
 
+instance {p : Char → Bool} : LawfulToBackwardSearcherModel p :=
+  .defaultImplementation
+
 theorem matchesAt_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
     MatchesAt p pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) := by
   simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff, exists_comm]
 
+theorem revMatchesAt_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
+    RevMatchesAt p pos ↔ ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get (by simp)) := by
+  simp [revMatchesAt_iff_exists_isLongestRevMatchAt, isLongestRevMatchAt_iff, exists_comm]
+
 theorem not_matchesAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos}
     (hc : p (pos.get h) = false) : ¬ MatchesAt p pos := by
   simp [matchesAt_iff, hc]
 
+theorem not_revMatchesAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos}
+    (hc : p ((pos.prev h).get (by simp)) = false) : ¬ RevMatchesAt p pos := by
+  simp [revMatchesAt_iff, hc]
+
 theorem matchAt?_eq {s : Slice} {pos : s.Pos} {p : Char → Bool} :
     matchAt? p pos =
       if h₀ : ∃ (h : pos ≠ s.endPos), p (pos.get h) then some (pos.next h₀.1) else none := by
   split <;> simp_all [isLongestMatchAt_iff, matchesAt_iff]
 
+theorem revMatchAt?_eq {s : Slice} {pos : s.Pos} {p : Char → Bool} :
+    revMatchAt? p pos =
+      if h₀ : ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get (by simp)) then some (pos.prev h₀.1) else none := by
+  split <;> simp_all [isLongestRevMatchAt_iff, revMatchesAt_iff]
+
 namespace Decidable
 
-instance {p : Char → Prop} [DecidablePred p] : ForwardPatternModel p where
-  Matches := ForwardPatternModel.Matches (decide <| p ·)
-  not_matches_empty := ForwardPatternModel.not_matches_empty (pat := (decide <| p ·))
+instance {p : Char → Prop} [DecidablePred p] : PatternModel p where
+  Matches := PatternModel.Matches (decide <| p ·)
+  not_matches_empty := PatternModel.not_matches_empty (pat := (decide <| p ·))
 
-instance {p : Char → Prop} [DecidablePred p] : NoPrefixForwardPatternModel p where
-  eq_empty := NoPrefixForwardPatternModel.eq_empty (pat := (decide <| p ·))
+instance {p : Char → Prop} [DecidablePred p] : NoPrefixPatternModel p where
+  eq_empty := NoPrefixPatternModel.eq_empty (pat := (decide <| p ·))
+
+instance {p : Char → Prop} [DecidablePred p] : NoSuffixPatternModel p where
+  eq_empty := NoSuffixPatternModel.eq_empty (pat := (decide <| p ·))
 
 theorem isMatch_iff_isMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
     IsMatch p pos ↔ IsMatch (decide <| p ·) pos :=
   ⟨fun ⟨h⟩ => ⟨h⟩, fun ⟨h⟩ => ⟨h⟩⟩
 
+theorem isRevMatch_iff_isRevMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
+    IsRevMatch p pos ↔ IsRevMatch (decide <| p ·) pos :=
+  ⟨fun ⟨h⟩ => ⟨h⟩, fun ⟨h⟩ => ⟨h⟩⟩
+
 theorem isMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
     IsMatch p pos ↔
       ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) := by
   simp [isMatch_iff_isMatch_decide, CharPred.isMatch_iff]
 
+theorem isRevMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
+    IsRevMatch p pos ↔
+      ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get (by simp)) := by
+  simp [isRevMatch_iff_isRevMatch_decide, CharPred.isRevMatch_iff]
+
 theorem isLongestMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
     IsLongestMatch p pos ↔
       ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) := by
   rw [isLongestMatch_iff_isMatch, isMatch_iff]
 
+theorem isLongestRevMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
+    IsLongestRevMatch p pos ↔
+      ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get (by simp)) := by
+  simp [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff]
+
 theorem isLongestMatch_iff_isLongestMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
     {pos : s.Pos} : IsLongestMatch p pos ↔ IsLongestMatch (decide <| p ·) pos := by
   simp [isLongestMatch_iff_isMatch, isMatch_iff_isMatch_decide]
 
+theorem isLongestRevMatch_iff_isLongestRevMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
+    {pos : s.Pos} : IsLongestRevMatch p pos ↔ IsLongestRevMatch (decide <| p ·) pos := by
+  simp [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff_isRevMatch_decide]
+
 theorem isLongestMatchAt_iff_isLongestMatchAt_decide {p : Char → Prop} [DecidablePred p]
     {s : Slice} {pos pos' : s.Pos} :
     IsLongestMatchAt p pos pos' ↔ IsLongestMatchAt (decide <| p ·) pos pos' := by
   simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_isLongestMatch_decide]
 
+theorem isLongestRevMatchAt_iff_isLongestRevMatchAt_decide {p : Char → Prop} [DecidablePred p]
+    {s : Slice} {pos pos' : s.Pos} :
+    IsLongestRevMatchAt p pos pos' ↔ IsLongestRevMatchAt (decide <| p ·) pos pos' := by
+  simp [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff_isLongestRevMatch_decide]
+
 theorem isLongestMatchAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice}
     {pos pos' : s.Pos} :
     IsLongestMatchAt p pos pos' ↔ ∃ h, pos' = pos.next h ∧ p (pos.get h) := by
   simp [isLongestMatchAt_iff_isLongestMatchAt_decide, CharPred.isLongestMatchAt_iff]
 
+theorem isLongestRevMatchAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice}
+    {pos pos' : s.Pos} :
+    IsLongestRevMatchAt p pos pos' ↔ ∃ h, pos = pos'.prev h ∧ p ((pos'.prev h).get (by simp)) := by
+  simp [isLongestRevMatchAt_iff_isLongestRevMatchAt_decide, CharPred.isLongestRevMatchAt_iff]
+
 theorem isLongestMatchAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos}
     {h : pos ≠ s.endPos} (hc : p (pos.get h)) : IsLongestMatchAt p pos (pos.next h) :=
   isLongestMatchAt_iff.2 ⟨h, by simp [hc]⟩
 
+theorem isLongestRevMatchAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos}
+    {h : pos ≠ s.startPos} (hc : p ((pos.prev h).get (by simp))) :
+    IsLongestRevMatchAt p (pos.prev h) pos :=
+  isLongestRevMatchAt_iff.2 ⟨h, by simp [hc]⟩
+
 theorem matchesAt_iff_matchesAt_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
     {pos : s.Pos} : MatchesAt p pos ↔ MatchesAt (decide <| p ·) pos := by
   simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_decide]
 
+theorem revMatchesAt_iff_revMatchesAt_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
+    {pos : s.Pos} : RevMatchesAt p pos ↔ RevMatchesAt (decide <| p ·) pos := by
+  simp [revMatchesAt_iff_exists_isLongestRevMatchAt, isLongestRevMatchAt_iff_isLongestRevMatchAt_decide]
+
 theorem matchAt?_eq_matchAt?_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
     {pos : s.Pos} : matchAt? p pos = matchAt? (decide <| p ·) pos := by
   ext endPos
   simp [isLongestMatchAt_iff_isLongestMatchAt_decide]
 
+theorem revMatchAt?_eq_revMatchAt?_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
+    {pos : s.Pos} : revMatchAt? p pos = revMatchAt? (decide <| p ·) pos := by
+  ext startPos
+  simp [isLongestRevMatchAt_iff_isLongestRevMatchAt_decide]
+
 theorem skipPrefix?_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] :
     ForwardPattern.skipPrefix? p = ForwardPattern.skipPrefix? (decide <| p ·) := rfl
 
+theorem skipSuffix?_eq_skipSuffix?_decide {p : Char → Prop} [DecidablePred p] :
+    BackwardPattern.skipSuffix? p = BackwardPattern.skipSuffix? (decide <| p ·) := rfl
+
 instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPatternModel p where
   skipPrefix?_eq_some_iff {s} pos := by
     rw [skipPrefix?_eq_skipPrefix?_decide, isLongestMatch_iff_isLongestMatch_decide]
     exact LawfulForwardPatternModel.skipPrefix?_eq_some_iff ..
 
+instance {p : Char → Prop} [DecidablePred p] : LawfulBackwardPatternModel p where
+  skipSuffix?_eq_some_iff {s} pos := by
+    rw [skipSuffix?_eq_skipSuffix?_decide, isLongestRevMatch_iff_isLongestRevMatch_decide]
+    exact LawfulBackwardPatternModel.skipSuffix?_eq_some_iff ..
+
 theorem toSearcher_eq {p : Char → Prop} [DecidablePred p] {s : Slice} :
     ToForwardSearcher.toSearcher p s = ToForwardSearcher.toSearcher (decide <| p ·) s := (rfl)
 
+theorem toBackwardSearcher_eq {p : Char → Prop} [DecidablePred p] {s : Slice} :
+    ToBackwardSearcher.toSearcher p s = ToBackwardSearcher.toSearcher (decide <| p ·) s := (rfl)
+
 theorem isValidSearchFrom_iff_isValidSearchFrom_decide {p : Char → Prop} [DecidablePred p]
     {s : Slice} {pos : s.Pos} {l : List (SearchStep s)} :
     IsValidSearchFrom p pos l ↔ IsValidSearchFrom (decide <| p ·) pos l := by
@@ -150,24 +254,55 @@ theorem isValidSearchFrom_iff_isValidSearchFrom_decide {p : Char → Prop} [Deci
     | matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_decide]
     | mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_decide]
 
+theorem isValidRevSearchFrom_iff_isValidRevSearchFrom_decide {p : Char → Prop} [DecidablePred p]
+    {s : Slice} {pos : s.Pos} {l : List (SearchStep s)} :
+    IsValidRevSearchFrom p pos l ↔ IsValidRevSearchFrom (decide <| p ·) pos l := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · induction h with
+    | startPos => simpa using IsValidRevSearchFrom.startPos
+    | matched => simp_all [IsValidRevSearchFrom.matched, isLongestRevMatchAt_iff_isLongestRevMatchAt_decide]
+    | mismatched => simp_all [IsValidRevSearchFrom.mismatched, revMatchesAt_iff_revMatchesAt_decide]
+  · induction h with
+    | startPos => simpa using IsValidRevSearchFrom.startPos
+    | matched => simp_all [IsValidRevSearchFrom.matched, isLongestRevMatchAt_iff_isLongestRevMatchAt_decide]
+    | mismatched => simp_all [IsValidRevSearchFrom.mismatched, revMatchesAt_iff_revMatchesAt_decide]
+
 instance {p : Char → Prop} [DecidablePred p] : LawfulToForwardSearcherModel p where
   isValidSearchFrom_toList s := by
     simpa [toSearcher_eq, isValidSearchFrom_iff_isValidSearchFrom_decide] using
       LawfulToForwardSearcherModel.isValidSearchFrom_toList (pat := (decide <| p ·)) (s := s)
 
+instance {p : Char → Prop} [DecidablePred p] : LawfulToBackwardSearcherModel p where
+  isValidRevSearchFrom_toList s := by
+    simpa [toBackwardSearcher_eq, isValidRevSearchFrom_iff_isValidRevSearchFrom_decide] using
+      LawfulToBackwardSearcherModel.isValidRevSearchFrom_toList (pat := (decide <| p ·)) (s := s)
+
 theorem matchesAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
     MatchesAt p pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) := by
   simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff, exists_comm]
 
+theorem revMatchesAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
+    RevMatchesAt p pos ↔ ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get (by simp)) := by
+  simp [revMatchesAt_iff_exists_isLongestRevMatchAt, isLongestRevMatchAt_iff, exists_comm]
+
 theorem not_matchesAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos}
     {h : pos ≠ s.endPos} (hc : ¬ p (pos.get h)) : ¬ MatchesAt p pos := by
   simp [matchesAt_iff, hc]
 
+theorem not_revMatchesAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos}
+    {h : pos ≠ s.startPos} (hc : ¬ p ((pos.prev h).get (by simp))) : ¬ RevMatchesAt p pos := by
+  simp [revMatchesAt_iff, hc]
+
 theorem matchAt?_eq {s : Slice} {pos : s.Pos} {p : Char → Prop} [DecidablePred p] :
     matchAt? p pos =
       if h₀ : ∃ (h : pos ≠ s.endPos), p (pos.get h) then some (pos.next h₀.1) else none := by
   split <;> simp_all [isLongestMatchAt_iff, matchesAt_iff]
 
+theorem revMatchAt?_eq {s : Slice} {pos : s.Pos} {p : Char → Prop} [DecidablePred p] :
+    revMatchAt? p pos =
+      if h₀ : ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get (by simp)) then some (pos.prev h₀.1) else none := by
+  split <;> simp_all [isLongestRevMatchAt_iff, revMatchesAt_iff]
+
 end Decidable
 
 end Pattern.Model.CharPred

src/Init/Data/String/Lemmas/Pattern/Split/Basic.lean

@@ -28,7 +28,7 @@ set_option doc.verso true
 # Verification of {name}`String.Slice.splitToSubslice`
 
 This PR verifies the {name}`String.Slice.splitToSubslice` function by relating it to a model
-implementation based on the {name}`String.Slice.Pattern.Model.ForwardPatternModel` class.
+implementation based on the {name}`String.Slice.Pattern.Model.PatternModel` class.
 
 This gives a low-level correctness proof from which higher-level API lemmas can be derived.
 -/
@@ -36,7 +36,7 @@ This gives a low-level correctness proof from which higher-level API lemmas can
 namespace String.Slice.Pattern.Model
 
 @[cbv_opaque]
-public protected noncomputable def split {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {s : Slice}
+public protected noncomputable def split {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice}
     (firstRejected curr : s.Pos) (hle : firstRejected ≤ curr) : List s.Subslice :=
   if h : curr = s.endPos then
     [s.subslice _ _ hle]
@@ -49,12 +49,12 @@ public protected noncomputable def split {ρ : Type} (pat : ρ) [ForwardPatternM
 termination_by curr
 
 @[simp]
-public theorem split_endPos {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {s : Slice}
+public theorem split_endPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice}
     {firstRejected : s.Pos} :
     Model.split (s := s) pat firstRejected s.endPos (by simp) = [s.subslice firstRejected s.endPos (by simp)] := by
   simp [Model.split]
 
-public theorem split_eq_of_isLongestMatchAt {ρ : Type} {pat : ρ} [ForwardPatternModel pat]
+public theorem split_eq_of_isLongestMatchAt {ρ : Type} {pat : ρ} [PatternModel pat]
     {s : Slice} {firstRejected start stop : s.Pos} {hle} (h : IsLongestMatchAt pat start stop) :
     Model.split pat firstRejected start hle =
       s.subslice _ _ hle :: Model.split pat stop stop (by exact Std.le_refl _) := by
@@ -63,7 +63,7 @@ public theorem split_eq_of_isLongestMatchAt {ρ : Type} {pat : ρ} [ForwardPatte
   · congr <;> exact (matchAt?_eq_some_iff.1 ‹_›).eq h
   · simp [matchAt?_eq_some_iff.2 ‹_›] at *
 
-public theorem split_eq_of_not_matchesAt {ρ : Type} {pat : ρ} [ForwardPatternModel pat]
+public theorem split_eq_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pat]
     {s : Slice} {firstRejected start} (stop : s.Pos) (h₀ : start ≤ stop) {hle}
     (h : ∀ p, start ≤ p → p < stop → ¬ MatchesAt pat p) :
     Model.split pat firstRejected start hle =
@@ -80,7 +80,7 @@ public theorem split_eq_of_not_matchesAt {ρ : Type} {pat : ρ} [ForwardPatternM
   · obtain rfl : start = stop := Std.le_antisymm h₀ (Std.not_lt.1 h')
     simp
 
-public theorem split_eq_next_of_not_matchesAt {ρ : Type} {pat : ρ} [ForwardPatternModel pat]
+public theorem split_eq_next_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pat]
     {s : Slice} {firstRejected start} {hle} (hs : start ≠ s.endPos) (h : ¬ MatchesAt pat start) :
     Model.split pat firstRejected start hle =
       Model.split pat firstRejected (start.next hs) (by exact Std.le_trans hle (by simp)) := by
@@ -103,7 +103,7 @@ def splitFromSteps {s : Slice} (currPos : s.Pos) (l : List (SearchStep s)) : Lis
   | .matched p q :: l => s.subslice! currPos p :: splitFromSteps q l
 
 theorem IsValidSearchFrom.splitFromSteps_eq_extend_split {ρ : Type} (pat : ρ)
-    [ForwardPatternModel pat] (l : List (SearchStep s)) (pos pos' : s.Pos) (h₀ : pos ≤ pos')
+    [PatternModel pat] (l : List (SearchStep s)) (pos pos' : s.Pos) (h₀ : pos ≤ pos')
     (h' : ∀ p, pos ≤ p → p < pos' → ¬ MatchesAt pat p)
     (h : IsValidSearchFrom pat pos' l) :
     splitFromSteps pos l = Model.split pat pos pos' h₀ := by
@@ -155,7 +155,7 @@ end Model
 open Model
 
 @[cbv_eval]
-public theorem toList_splitToSubslice_eq_modelSplit {ρ : Type} (pat : ρ) [ForwardPatternModel pat]
+public theorem toList_splitToSubslice_eq_modelSplit {ρ : Type} (pat : ρ) [PatternModel pat]
     {σ : Slice → Type} [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
     [∀ s, Std.Iterators.Finite (σ s) Id] [LawfulToForwardSearcherModel pat] (s : Slice) :
     (s.splitToSubslice pat).toList = Model.split pat s.startPos s.startPos (by exact Std.le_refl _) := by
@@ -168,7 +168,7 @@ end Pattern
 open Pattern
 
 public theorem toList_splitToSubslice_of_isEmpty {ρ : Type} (pat : ρ)
-    [Model.ForwardPatternModel pat] {σ : Slice → Type}
+    [Model.PatternModel pat] {σ : Slice → Type}
     [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
     [∀ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] {s : Slice}
     (h : s.isEmpty = true) :
@@ -182,7 +182,7 @@ public theorem toList_split_eq_splitToSubslice {ρ : Type} (pat : ρ) {σ : Slic
   simp [split, Std.Iter.toList_map]
 
 public theorem toList_split_of_isEmpty {ρ : Type} (pat : ρ)
-    [Model.ForwardPatternModel pat] {σ : Slice → Type}
+    [Model.PatternModel pat] {σ : Slice → Type}
     [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
     [∀ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] {s : Slice}
     (h : s.isEmpty = true) :
@@ -200,7 +200,7 @@ public theorem split_eq_split_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Typ
 
 @[simp]
 public theorem toList_split_empty {ρ : Type} (pat : ρ)
-    [Model.ForwardPatternModel pat] {σ : Slice → Type}
+    [Model.PatternModel pat] {σ : Slice → Type}
     [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
     [∀ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] :
     ("".split pat).toList.map Slice.copy = [""] := by

src/Init/Data/String/Lemmas/Pattern/String/Basic.lean

@@ -19,12 +19,12 @@ namespace String.Slice.Pattern.Model
 
 namespace ForwardSliceSearcher
 
-instance {pat : Slice} : ForwardPatternModel pat where
+instance {pat : Slice} : PatternModel pat where
   /-
-  See the docstring of `ForwardPatternModel` for an explanation about why we disallow matching the
+  See the docstring of `PatternModel` for an explanation about why we disallow matching the
   empty string.
 
-  Requiring `s ≠ ""` is a trick that allows us to give a `ForwardPatternModel` instance
+  Requiring `s ≠ ""` is a trick that allows us to give a `PatternModel` instance
   unconditionally, without forcing `pat.copy` to be non-empty (which would make it very awkward
   to state theorems about the instance). It does not change anything about the fact that all lemmas
   about this instance require `pat.isEmpty = false`.
@@ -32,34 +32,60 @@ instance {pat : Slice} : ForwardPatternModel pat where
   Matches s := s ≠ "" ∧ s = pat.copy
   not_matches_empty := by simp
 
-instance {pat : Slice} : NoPrefixForwardPatternModel pat :=
-  .of_length_eq (by simp +contextual [ForwardPatternModel.Matches])
+instance {pat : Slice} : NoPrefixPatternModel pat :=
+  .of_length_eq (by simp +contextual [PatternModel.Matches])
+
+instance {pat : Slice} : NoSuffixPatternModel pat :=
+  .of_length_eq (by simp +contextual [PatternModel.Matches])
 
 theorem isMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
     IsMatch pat pos ↔ (s.sliceTo pos).copy = pat.copy := by
-  simp only [Model.isMatch_iff, ForwardPatternModel.Matches, ne_eq, copy_eq_empty_iff,
+  simp only [Model.isMatch_iff, PatternModel.Matches, ne_eq, copy_eq_empty_iff,
     Bool.not_eq_true, and_iff_right_iff_imp]
   intro h'
   rw [← isEmpty_copy (s := s.sliceTo pos), h', isEmpty_copy, h]
 
+theorem isRevMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
+    IsRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat.copy := by
+  simp only [Model.isRevMatch_iff, PatternModel.Matches, ne_eq, copy_eq_empty_iff,
+    Bool.not_eq_true, and_iff_right_iff_imp]
+  intro h'
+  rw [← isEmpty_copy (s := s.sliceFrom pos), h', isEmpty_copy, h]
+
 theorem isLongestMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
     IsLongestMatch pat pos ↔ (s.sliceTo pos).copy = pat.copy := by
   rw [isLongestMatch_iff_isMatch, isMatch_iff h]
 
+theorem isLongestRevMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
+    IsLongestRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat.copy := by
+  rw [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff h]
+
 theorem isLongestMatchAt_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
     IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ h, (s.slice pos₁ pos₂ h).copy = pat.copy := by
   simp [Model.isLongestMatchAt_iff, isLongestMatch_iff h]
 
+theorem isLongestRevMatchAt_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
+    IsLongestRevMatchAt pat pos₁ pos₂ ↔ ∃ h, (s.slice pos₁ pos₂ h).copy = pat.copy := by
+  simp [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff h]
+
 theorem isLongestMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
     IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ t₁ t₂, pos₁.Splits t₁ (pat.copy ++ t₂) ∧
       pos₂.Splits (t₁ ++ pat.copy) t₂ := by
   simp only [isLongestMatchAt_iff h, copy_slice_eq_iff_splits]
 
+theorem isLongestRevMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos}
+    (h : pat.isEmpty = false) :
+    IsLongestRevMatchAt pat pos₁ pos₂ ↔ ∃ t₁ t₂, pos₁.Splits t₁ (pat.copy ++ t₂) ∧
+      pos₂.Splits (t₁ ++ pat.copy) t₂ := by
+  simp only [isLongestRevMatchAt_iff h, copy_slice_eq_iff_splits]
+
 theorem isLongestMatch_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
     IsLongestMatch pat pos ↔ ∃ t, pos.Splits pat.copy t := by
-  simp only [← isLongestMatchAt_startPos_iff, isLongestMatchAt_iff_splits h, splits_startPos_iff,
-    and_assoc, exists_and_left, exists_eq_left, empty_append]
-  exact ⟨fun ⟨h, _, h'⟩ => ⟨h, h'⟩, fun ⟨h, h'⟩ => ⟨h, h'.eq_append.symm, h'⟩⟩
+  rw [isLongestMatch_iff h, copy_sliceTo_eq_iff_exists_splits]
+
+theorem isLongestRevMatch_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
+    IsLongestRevMatch pat pos ↔ ∃ t, pos.Splits t pat.copy := by
+  rw [isLongestRevMatch_iff h, copy_sliceFrom_eq_iff_exists_splits]
 
 theorem isLongestMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
     IsLongestMatchAt pat pos₁ pos₂ ↔
@@ -71,6 +97,18 @@ theorem isLongestMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos} (h
     exact ⟨by simp [Pos.le_iff, Pos.Raw.le_iff]; omega,
       by simp [← h', ← toByteArray_inj, toByteArray_copy_slice]⟩
 
+theorem isLongestRevMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos}
+    (h : pat.isEmpty = false) :
+    IsLongestRevMatchAt pat pos₁ pos₂ ↔
+      s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx =
+        pat.copy.toByteArray := by
+  rw [isLongestRevMatchAt_iff h]
+  refine ⟨fun ⟨h, h'⟩ => ?_, fun h' => ?_⟩
+  · simp [← h', toByteArray_copy_slice]
+  · rw [← Slice.toByteArray_copy_ne_empty_iff, ← h', ne_eq, ByteArray.extract_eq_empty_iff] at h
+    exact ⟨by simp [Pos.le_iff, Pos.Raw.le_iff]; omega,
+      by simp [← h', ← toByteArray_inj, toByteArray_copy_slice]⟩
+
 theorem offset_of_isLongestMatchAt {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false)
     (h' : IsLongestMatchAt pat pos₁ pos₂) : pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize := by
   simp only [Pos.Raw.ext_iff, Pos.Raw.byteIdx_increaseBy]
@@ -81,12 +119,29 @@ theorem offset_of_isLongestMatchAt {pat s : Slice} {pos₁ pos₂ : s.Pos} (h :
   suffices pos₂.offset.byteIdx ≤ s.utf8ByteSize by omega
   simpa [Pos.le_iff, Pos.Raw.le_iff] using pos₂.le_endPos
 
+theorem offset_of_isLongestRevMatchAt {pat s : Slice} {pos₁ pos₂ : s.Pos}
+    (h : pat.isEmpty = false) (h' : IsLongestRevMatchAt pat pos₁ pos₂) :
+    pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize := by
+  simp only [Pos.Raw.ext_iff, Pos.Raw.byteIdx_increaseBy]
+  rw [isLongestRevMatchAt_iff_extract h] at h'
+  rw [← Slice.toByteArray_copy_ne_empty_iff, ← h', ne_eq, ByteArray.extract_eq_empty_iff] at h
+  replace h' := congrArg ByteArray.size h'
+  simp only [ByteArray.size_extract, size_toByteArray, utf8ByteSize_copy] at h'
+  suffices pos₂.offset.byteIdx ≤ s.utf8ByteSize by omega
+  simpa [Pos.le_iff, Pos.Raw.le_iff] using pos₂.le_endPos
+
 theorem matchesAt_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
     MatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ (pat.copy ++ t₂) := by
   simp only [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_splits h]
   exact ⟨fun ⟨e, t₁, t₂, ht₁, ht₂⟩ => ⟨t₁, t₂, ht₁⟩,
     fun ⟨t₁, t₂, ht⟩ => ⟨ht.rotateRight, t₁, t₂, ht, ht.splits_rotateRight⟩⟩
 
+theorem revMatchesAt_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
+    RevMatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits (t₁ ++ pat.copy) t₂ := by
+  simp only [revMatchesAt_iff_exists_isLongestRevMatchAt, isLongestRevMatchAt_iff_splits h]
+  exact ⟨fun ⟨e, t₁, t₂, ht₁, ht₂⟩ => ⟨t₁, t₂, ht₂⟩,
+    fun ⟨t₁, t₂, ht⟩ => ⟨ht.rotateLeft, t₁, t₂, ht.splits_rotateLeft, ht⟩⟩
+
 theorem exists_matchesAt_iff_eq_append {pat s : Slice} (h : pat.isEmpty = false) :
     (∃ (pos : s.Pos), MatchesAt pat pos) ↔ ∃ t₁ t₂, s.copy = t₁ ++ pat.copy ++ t₂ := by
   simp only [matchesAt_iff_splits h]
@@ -99,6 +154,18 @@ theorem exists_matchesAt_iff_eq_append {pat s : Slice} (h : pat.isEmpty = false)
         ⟨t₁, pat.copy ++ t₂, by rw [← append_assoc]; exact heq, rfl⟩
     exact ⟨s.pos _ hvalid, t₁, t₂, ⟨by rw [← append_assoc]; exact heq, by simp⟩⟩
 
+theorem exists_revMatchesAt_iff_eq_append {pat s : Slice} (h : pat.isEmpty = false) :
+    (∃ (pos : s.Pos), RevMatchesAt pat pos) ↔ ∃ t₁ t₂, s.copy = t₁ ++ pat.copy ++ t₂ := by
+  simp only [revMatchesAt_iff_splits h]
+  constructor
+  · rintro ⟨pos, t₁, t₂, hsplit⟩
+    exact ⟨t₁, t₂, by rw [hsplit.eq_append, append_assoc]⟩
+  · rintro ⟨t₁, t₂, heq⟩
+    have hvalid : (t₁ ++ pat.copy).rawEndPos.IsValidForSlice s :=
+      Pos.Raw.isValidForSlice_iff_exists_append.mpr
+        ⟨t₁ ++ pat.copy, t₂, heq, rfl⟩
+    exact ⟨s.pos _ hvalid, t₁, t₂, ⟨heq, by simp⟩⟩
+
 theorem matchesAt_iff_isLongestMatchAt {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
     MatchesAt pat pos ↔ ∃ (h : (pos.offset.increaseBy pat.utf8ByteSize).IsValidForSlice s),
       IsLongestMatchAt pat pos (s.pos _ h) := by
@@ -108,6 +175,25 @@ theorem matchesAt_iff_isLongestMatchAt {pat s : Slice} {pos : s.Pos} (h : pat.is
   obtain rfl : p = s.pos _ this := by simpa [Pos.ext_iff] using offset_of_isLongestMatchAt h h'
   exact h'
 
+theorem revMatchesAt_iff_isLongestRevMatchAt {pat s : Slice} {pos : s.Pos}
+    (h : pat.isEmpty = false) :
+    RevMatchesAt pat pos ↔
+      ∃ (h : (pos.offset.decreaseBy pat.utf8ByteSize).IsValidForSlice s),
+        IsLongestRevMatchAt pat (s.pos _ h) pos := by
+  refine ⟨fun ⟨⟨p, h'⟩⟩ => ?_, fun ⟨_, h⟩ => ⟨⟨_, h⟩⟩⟩
+  have hoff := offset_of_isLongestRevMatchAt h h'
+  have hvalid : (pos.offset.decreaseBy pat.utf8ByteSize).IsValidForSlice s := by
+    rw [show pos.offset.decreaseBy pat.utf8ByteSize = p.offset from by
+      simp [Pos.Raw.ext_iff, Pos.Raw.byteIdx_decreaseBy, Pos.Raw.byteIdx_increaseBy] at hoff ⊢
+      omega]
+    exact p.isValidForSlice
+  refine ⟨hvalid, ?_⟩
+  obtain rfl : p = s.pos _ hvalid := by
+    simp only [Pos.ext_iff, offset_pos]
+    simp [Pos.Raw.ext_iff, Pos.Raw.byteIdx_decreaseBy, Pos.Raw.byteIdx_increaseBy] at hoff ⊢
+    omega
+  exact h'
+
 theorem matchesAt_iff_getElem {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
     MatchesAt pat pos ↔
       ∃ (h : pos.offset.byteIdx + pat.copy.toByteArray.size ≤ s.copy.toByteArray.size),
@@ -146,31 +232,56 @@ end ForwardSliceSearcher
 
 namespace ForwardStringSearcher
 
-instance {pat : String} : ForwardPatternModel pat where
+instance {pat : String} : PatternModel pat where
   Matches s := s ≠ "" ∧ s = pat
   not_matches_empty := by simp
 
-instance {pat : String} : NoPrefixForwardPatternModel pat :=
-  .of_length_eq (by simp +contextual [ForwardPatternModel.Matches])
+instance {pat : String} : NoPrefixPatternModel pat :=
+  .of_length_eq (by simp +contextual [PatternModel.Matches])
+
+instance {pat : String} : NoSuffixPatternModel pat :=
+  .of_length_eq (by simp +contextual [PatternModel.Matches])
 
 theorem isMatch_iff_slice {pat : String} {s : Slice} {pos : s.Pos} :
     IsMatch (ρ := String) pat pos ↔ IsMatch (ρ := Slice) pat.toSlice pos := by
-  simp only [Model.isMatch_iff, ForwardPatternModel.Matches, copy_toSlice]
+  simp only [Model.isMatch_iff, PatternModel.Matches, copy_toSlice]
+
+theorem isRevMatch_iff_slice {pat : String} {s : Slice} {pos : s.Pos} :
+    IsRevMatch (ρ := String) pat pos ↔ IsRevMatch (ρ := Slice) pat.toSlice pos := by
+  simp only [Model.isRevMatch_iff, PatternModel.Matches, copy_toSlice]
 
 theorem isLongestMatch_iff_isLongestMatch_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
     IsLongestMatch (ρ := String) pat pos ↔ IsLongestMatch (ρ := Slice) pat.toSlice pos where
   mp h := ⟨isMatch_iff_slice.1 h.isMatch, fun p hp hm => h.not_isMatch p hp (isMatch_iff_slice.2 hm)⟩
   mpr h := ⟨isMatch_iff_slice.2 h.isMatch, fun p hp hm => h.not_isMatch p hp (isMatch_iff_slice.1 hm)⟩
 
+theorem isLongestRevMatch_iff_isLongestRevMatch_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
+    IsLongestRevMatch (ρ := String) pat pos ↔ IsLongestRevMatch (ρ := Slice) pat.toSlice pos where
+  mp h := ⟨isRevMatch_iff_slice.1 h.isRevMatch,
+    fun p hp hm => h.not_isRevMatch p hp (isRevMatch_iff_slice.2 hm)⟩
+  mpr h := ⟨isRevMatch_iff_slice.2 h.isRevMatch,
+    fun p hp hm => h.not_isRevMatch p hp (isRevMatch_iff_slice.1 hm)⟩
+
 theorem isLongestMatchAt_iff_isLongestMatchAt_toSlice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
     IsLongestMatchAt (ρ := String) pat pos₁ pos₂ ↔
       IsLongestMatchAt (ρ := Slice) pat.toSlice pos₁ pos₂ := by
   simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_isLongestMatch_toSlice]
 
+theorem isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice {pat : String} {s : Slice}
+    {pos₁ pos₂ : s.Pos} :
+    IsLongestRevMatchAt (ρ := String) pat pos₁ pos₂ ↔
+      IsLongestRevMatchAt (ρ := Slice) pat.toSlice pos₁ pos₂ := by
+  simp [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff_isLongestRevMatch_toSlice]
+
 theorem matchesAt_iff_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
     MatchesAt (ρ := String) pat pos ↔ MatchesAt (ρ := Slice) pat.toSlice pos := by
   simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_toSlice]
 
+theorem revMatchesAt_iff_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
+    RevMatchesAt (ρ := String) pat pos ↔ RevMatchesAt (ρ := Slice) pat.toSlice pos := by
+  simp [revMatchesAt_iff_exists_isLongestRevMatchAt,
+    isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice]
+
 private theorem toSlice_isEmpty (h : pat ≠ "") : pat.toSlice.isEmpty = false := by
   rwa [isEmpty_toSlice, isEmpty_eq_false_iff]
 
@@ -179,16 +290,31 @@ theorem isMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") :
   rw [isMatch_iff_slice, ForwardSliceSearcher.isMatch_iff (toSlice_isEmpty h)]
   simp
 
+theorem isRevMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") :
+    IsRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat := by
+  rw [isRevMatch_iff_slice, ForwardSliceSearcher.isRevMatch_iff (toSlice_isEmpty h)]
+  simp
+
 theorem isLongestMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") :
     IsLongestMatch pat pos ↔ (s.sliceTo pos).copy = pat := by
   rw [isLongestMatch_iff_isMatch, isMatch_iff h]
 
+theorem isLongestRevMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") :
+    IsLongestRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat := by
+  rw [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff h]
+
 theorem isLongestMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat ≠ "") :
     IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ h, (s.slice pos₁ pos₂ h).copy = pat := by
   rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice,
     ForwardSliceSearcher.isLongestMatchAt_iff (toSlice_isEmpty h)]
   simp
 
+theorem isLongestRevMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat ≠ "") :
+    IsLongestRevMatchAt pat pos₁ pos₂ ↔ ∃ h, (s.slice pos₁ pos₂ h).copy = pat := by
+  rw [isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice,
+    ForwardSliceSearcher.isLongestRevMatchAt_iff (toSlice_isEmpty h)]
+  simp
+
 theorem isLongestMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
     (h : pat ≠ "") :
     IsLongestMatchAt pat pos₁ pos₂ ↔
@@ -197,6 +323,14 @@ theorem isLongestMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ :
     ForwardSliceSearcher.isLongestMatchAt_iff_splits (toSlice_isEmpty h)]
   simp
 
+theorem isLongestRevMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
+    (h : pat ≠ "") :
+    IsLongestRevMatchAt pat pos₁ pos₂ ↔
+      ∃ t₁ t₂, pos₁.Splits t₁ (pat ++ t₂) ∧ pos₂.Splits (t₁ ++ pat) t₂ := by
+  rw [isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice,
+    ForwardSliceSearcher.isLongestRevMatchAt_iff_splits (toSlice_isEmpty h)]
+  simp
+
 theorem isLongestMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
     (h : pat ≠ "") :
     IsLongestMatchAt pat pos₁ pos₂ ↔
@@ -205,6 +339,14 @@ theorem isLongestMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ :
     ForwardSliceSearcher.isLongestMatchAt_iff_extract (toSlice_isEmpty h)]
   simp
 
+theorem isLongestRevMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
+    (h : pat ≠ "") :
+    IsLongestRevMatchAt pat pos₁ pos₂ ↔
+      s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.toByteArray := by
+  rw [isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice,
+    ForwardSliceSearcher.isLongestRevMatchAt_iff_extract (toSlice_isEmpty h)]
+  simp
+
 theorem offset_of_isLongestMatchAt {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
     (h : pat ≠ "") (h' : IsLongestMatchAt pat pos₁ pos₂) :
     pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize := by
@@ -212,12 +354,25 @@ theorem offset_of_isLongestMatchAt {pat : String} {s : Slice} {pos₁ pos₂ : s
   exact ForwardSliceSearcher.offset_of_isLongestMatchAt (toSlice_isEmpty h)
     (isLongestMatchAt_iff_isLongestMatchAt_toSlice.1 h')
 
+theorem offset_of_isLongestRevMatchAt {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
+    (h : pat ≠ "") (h' : IsLongestRevMatchAt pat pos₁ pos₂) :
+    pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize := by
+  rw [show pat.utf8ByteSize = pat.toSlice.utf8ByteSize from utf8ByteSize_toSlice.symm]
+  exact ForwardSliceSearcher.offset_of_isLongestRevMatchAt (toSlice_isEmpty h)
+    (isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice.1 h')
+
 theorem matchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") :
     MatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ (pat ++ t₂) := by
   rw [matchesAt_iff_toSlice,
     ForwardSliceSearcher.matchesAt_iff_splits (toSlice_isEmpty h)]
   simp
 
+theorem revMatchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") :
+    RevMatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits (t₁ ++ pat) t₂ := by
+  rw [revMatchesAt_iff_toSlice,
+    ForwardSliceSearcher.revMatchesAt_iff_splits (toSlice_isEmpty h)]
+  simp
+
 theorem exists_matchesAt_iff_eq_append {pat : String} {s : Slice} (h : pat ≠ "") :
     (∃ (pos : s.Pos), MatchesAt pat pos) ↔ ∃ t₁ t₂, s.copy = t₁ ++ pat ++ t₂ := by
   simp only [matchesAt_iff_splits h]
@@ -230,6 +385,14 @@ theorem exists_matchesAt_iff_eq_append {pat : String} {s : Slice} (h : pat ≠ "
         ⟨t₁, pat ++ t₂, by rw [← append_assoc]; exact heq, rfl⟩
     exact ⟨s.pos _ hvalid, t₁, t₂, ⟨by rw [← append_assoc]; exact heq, by simp⟩⟩
 
+theorem exists_revMatchesAt_iff_eq_append {pat : String} {s : Slice} (h : pat ≠ "") :
+    (∃ (pos : s.Pos), RevMatchesAt pat pos) ↔ ∃ t₁ t₂, s.copy = t₁ ++ pat ++ t₂ := by
+  rw [show (∃ (pos : s.Pos), RevMatchesAt (ρ := String) pat pos) ↔
+      (∃ (pos : s.Pos), RevMatchesAt (ρ := Slice) pat.toSlice pos) from by
+    simp [revMatchesAt_iff_toSlice],
+    ForwardSliceSearcher.exists_revMatchesAt_iff_eq_append (toSlice_isEmpty h)]
+  simp
+
 theorem matchesAt_iff_isLongestMatchAt {pat : String} {s : Slice} {pos : s.Pos}
     (h : pat ≠ "") :
     MatchesAt pat pos ↔ ∃ (h : (pos.offset.increaseBy pat.utf8ByteSize).IsValidForSlice s),
@@ -239,6 +402,16 @@ theorem matchesAt_iff_isLongestMatchAt {pat : String} {s : Slice} {pos : s.Pos}
   simp only [utf8ByteSize_toSlice, ← isLongestMatchAt_iff_isLongestMatchAt_toSlice] at key
   rwa [matchesAt_iff_toSlice]
 
+theorem revMatchesAt_iff_isLongestRevMatchAt {pat : String} {s : Slice} {pos : s.Pos}
+    (h : pat ≠ "") :
+    RevMatchesAt pat pos ↔
+      ∃ (h : (pos.offset.decreaseBy pat.utf8ByteSize).IsValidForSlice s),
+        IsLongestRevMatchAt pat (s.pos _ h) pos := by
+  have key := ForwardSliceSearcher.revMatchesAt_iff_isLongestRevMatchAt (pat := pat.toSlice)
+    (toSlice_isEmpty h) (pos := pos)
+  simp only [utf8ByteSize_toSlice, ← isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice] at key
+  rwa [revMatchesAt_iff_toSlice]
+
 theorem matchesAt_iff_getElem {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") :
     MatchesAt pat pos ↔
       ∃ (h : pos.offset.byteIdx + pat.toByteArray.size ≤ s.copy.toByteArray.size),
@@ -259,6 +432,11 @@ theorem matchesAt_iff_matchesAt_toSlice {pat : String} {s : Slice}
     {pos : s.Pos} : MatchesAt pat pos ↔ MatchesAt pat.toSlice pos := by
   simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_toSlice]
 
+theorem revMatchesAt_iff_revMatchesAt_toSlice {pat : String} {s : Slice}
+    {pos : s.Pos} : RevMatchesAt pat pos ↔ RevMatchesAt pat.toSlice pos := by
+  simp [revMatchesAt_iff_exists_isLongestRevMatchAt,
+    isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice]
+
 theorem toSearcher_eq {pat : String} {s : Slice} :
     ToForwardSearcher.toSearcher pat s = ToForwardSearcher.toSearcher pat.toSlice s := (rfl)
 
@@ -275,6 +453,21 @@ theorem isValidSearchFrom_iff_isValidSearchFrom_toSlice {pat : String}
     | matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_toSlice]
     | mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_toSlice]
 
+theorem isValidRevSearchFrom_iff_isValidRevSearchFrom_toSlice {pat : String}
+    {s : Slice} {pos : s.Pos} {l : List (SearchStep s)} :
+    IsValidRevSearchFrom pat pos l ↔ IsValidRevSearchFrom pat.toSlice pos l := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · induction h with
+    | startPos => simpa using IsValidRevSearchFrom.startPos
+    | matched => simp_all [IsValidRevSearchFrom.matched,
+        isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice]
+    | mismatched => simp_all [IsValidRevSearchFrom.mismatched, revMatchesAt_iff_revMatchesAt_toSlice]
+  · induction h with
+    | startPos => simpa using IsValidRevSearchFrom.startPos
+    | matched => simp_all [IsValidRevSearchFrom.matched,
+        isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice]
+    | mismatched => simp_all [IsValidRevSearchFrom.mismatched, revMatchesAt_iff_revMatchesAt_toSlice]
+
 end ForwardStringSearcher
 
 end String.Slice.Pattern.Model

src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean

@@ -76,10 +76,12 @@ namespace Model.ForwardSliceSearcher
 
 open Pattern.ForwardSliceSearcher
 
+public instance {pat : Slice} : LawfulForwardPattern pat where
+  skipPrefixOfNonempty?_eq _ := rfl
+  startsWith_eq _ := isSome_skipPrefix?.symm
+
 public theorem lawfulForwardPatternModel {pat : Slice} (hpat : pat.isEmpty = false) :
     LawfulForwardPatternModel pat where
-  skipPrefixOfNonempty?_eq h := rfl
-  startsWith_eq s := isSome_skipPrefix?.symm
   skipPrefix?_eq_some_iff pos := by
     simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff hpat]
 
@@ -89,15 +91,116 @@ namespace Model.ForwardStringSearcher
 
 open Pattern.ForwardSliceSearcher
 
+public instance {pat : String} : LawfulForwardPattern pat where
+  skipPrefixOfNonempty?_eq _ := rfl
+  startsWith_eq _ := isSome_skipPrefix?.symm
+
 public theorem lawfulForwardPatternModel {pat : String} (hpat : pat ≠ "") :
     LawfulForwardPatternModel pat where
-  skipPrefixOfNonempty?_eq h := rfl
-  startsWith_eq s := isSome_skipPrefix?.symm
   skipPrefix?_eq_some_iff pos := by
     simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff hpat]
 
 end Model.ForwardStringSearcher
 
+namespace BackwardSliceSearcher
+
+theorem endsWith_iff {pat s : Slice} : endsWith pat s ↔ ∃ t, s.copy = t ++ pat.copy := by
+  rw [endsWith]
+  simp [Internal.memcmpSlice_eq_true_iff, utf8ByteSize_eq_size_toByteArray_copy, -size_toByteArray]
+  generalize pat.copy = pat
+  generalize s.copy = s
+  refine ⟨fun ⟨h₁, h₂⟩ => ?_, ?_⟩
+  · rw [Nat.sub_add_cancel h₁] at h₂
+    suffices (s.rawEndPos.unoffsetBy pat.rawEndPos).IsValid s by
+      have h₃ : (s.sliceFrom (s.pos _ this)).copy = pat := by
+        rw [← toByteArray_inj, (s.pos _ this).splits.toByteArray_right_eq]
+        simpa [offset_pos, Pos.Raw.byteIdx_unoffsetBy, byteIdx_rawEndPos]
+      have := (s.pos _ this).splits
+      rw [h₃] at this
+      exact ⟨_, this.eq_append⟩
+    rw [Pos.Raw.isValid_iff_isValidUTF8_extract_utf8ByteSize]
+    refine ⟨by simp [Pos.Raw.le_iff, Pos.Raw.byteIdx_unoffsetBy], ?_⟩
+    simp only [size_toByteArray] at h₂
+    simpa [Pos.Raw.byteIdx_unoffsetBy, byteIdx_rawEndPos, h₂] using pat.isValidUTF8
+  · rintro ⟨t, rfl⟩
+    exact ⟨by simp, by rw [Nat.sub_add_cancel (by simp)]; exact
+      ByteArray.extract_append_eq_right (by simp) (by simp)⟩
+
+theorem skipSuffix?_eq_some_iff {pat s : Slice} {pos : s.Pos} :
+    skipSuffix? pat s = some pos ↔ (s.sliceFrom pos).copy = pat.copy := by
+  fun_cases skipSuffix? with
+  | case1 h =>
+    simp only [Option.some.injEq]
+    obtain ⟨t, ht⟩ := endsWith_iff.1 h
+    have hpc : pat.copy.utf8ByteSize = pat.utf8ByteSize := Slice.utf8ByteSize_copy
+    have hsz : s.utf8ByteSize = t.utf8ByteSize + pat.utf8ByteSize := by
+      have := congrArg String.utf8ByteSize ht
+      simp only [utf8ByteSize_append, Slice.utf8ByteSize_copy] at this
+      exact this
+    have hoff : (s.endPos.offset.unoffsetBy pat.rawEndPos) = t.rawEndPos := by
+      ext
+      simp only [offset_endPos, Pos.Raw.byteIdx_unoffsetBy, byteIdx_rawEndPos,
+        String.byteIdx_rawEndPos]
+      omega
+    have hval : (s.endPos.offset.unoffsetBy pat.rawEndPos).IsValidForSlice s :=
+      Pos.Raw.isValidForSlice_iff_exists_append.mpr ⟨t, pat.copy, ht, hoff⟩
+    have hsp : (s.pos _ hval).Splits t pat.copy := ⟨ht, hoff⟩
+    rw [Slice.pos!_eq_pos hval]
+    exact ⟨(· ▸ hsp.copy_sliceFrom_eq),
+      fun h => hsp.pos_eq_of_eq_right (h ▸ pos.splits)⟩
+  | case2 h =>
+    simp only [endsWith_iff, not_exists] at h
+    simp only [reduceCtorEq, false_iff]
+    intro heq
+    have := h (s.sliceTo pos).copy
+    simp [← heq, pos.splits.eq_append] at this
+
+theorem isSome_skipSuffix? {pat s : Slice} : (skipSuffix? pat s).isSome = endsWith pat s := by
+  fun_cases skipSuffix? <;> simp_all
+
+public theorem endsWith_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    BackwardPattern.endsWith pat s = true := by
+  suffices pat.copy = "" by simp [BackwardPattern.endsWith, endsWith_iff, this]
+  simpa
+
+public theorem skipSuffix?_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    BackwardPattern.skipSuffix? pat s = some s.endPos := by
+  simpa [BackwardPattern.skipSuffix?, skipSuffix?_eq_some_iff]
+
+end BackwardSliceSearcher
+
+namespace Model.BackwardSliceSearcher
+
+open Pattern.BackwardSliceSearcher
+
+public instance {pat : Slice} : LawfulBackwardPattern pat where
+  skipSuffixOfNonempty?_eq _ := rfl
+  endsWith_eq _ := isSome_skipSuffix?.symm
+
+public theorem lawfulBackwardPatternModel {pat : Slice} (hpat : pat.isEmpty = false) :
+    LawfulBackwardPatternModel pat where
+  skipSuffix?_eq_some_iff pos := by
+    simp [BackwardPattern.skipSuffix?, skipSuffix?_eq_some_iff,
+      ForwardSliceSearcher.isLongestRevMatch_iff hpat]
+
+end Model.BackwardSliceSearcher
+
+namespace Model.BackwardStringSearcher
+
+open Pattern.BackwardSliceSearcher
+
+public instance {pat : String} : LawfulBackwardPattern pat where
+  skipSuffixOfNonempty?_eq _ := rfl
+  endsWith_eq _ := isSome_skipSuffix?.symm
+
+public theorem lawfulBackwardPatternModel {pat : String} (hpat : pat ≠ "") :
+    LawfulBackwardPatternModel pat where
+  skipSuffix?_eq_some_iff pos := by
+    simp [BackwardPattern.skipSuffix?, skipSuffix?_eq_some_iff,
+      ForwardStringSearcher.isLongestRevMatch_iff hpat]
+
+end Model.BackwardStringSearcher
+
 end Pattern
 
 public theorem startsWith_string_eq_startsWith_toSlice {pat : String} {s : Slice} :

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Basic.lean

@@ -29,12 +29,12 @@ theorem startsWith_eq_forwardPatternStartsWith {ρ : Type} {pat : ρ} [ForwardPa
 theorem dropPrefix?_eq_map_skipPrefix? {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : Slice} :
     s.dropPrefix? pat = (s.skipPrefix? pat).map s.sliceFrom := (rfl)
 
-theorem Pattern.Model.skipPrefix?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+theorem Pattern.Model.skipPrefix?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat]
     [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} :
     s.skipPrefix? pat = some pos ↔ IsLongestMatch pat pos := by
   rw [skipPrefix?_eq_forwardPatternSkipPrefix?, LawfulForwardPatternModel.skipPrefix?_eq_some_iff]
 
-theorem Pattern.Model.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+theorem Pattern.Model.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat]
     [LawfulForwardPatternModel pat] {s : Slice} :
     s.skipPrefix? pat = none ↔ ¬ MatchesAt pat s.startPos := by
   rw [skipPrefix?_eq_forwardPatternSkipPrefix?, LawfulForwardPatternModel.skipPrefix?_eq_none_iff]
@@ -44,13 +44,13 @@ theorem isSome_skipPrefix? {ρ : Type} {pat : ρ} [ForwardPattern pat] [LawfulFo
     (s.skipPrefix? pat).isSome = s.startsWith pat := by
   rw [startsWith_eq_forwardPatternStartsWith, skipPrefix?, LawfulForwardPattern.startsWith_eq]
 
-theorem Pattern.Model.startsWith_eq_false_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+theorem Pattern.Model.startsWith_eq_false_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat]
     [LawfulForwardPatternModel pat] {s : Slice} :
     s.startsWith pat = false ↔ ¬ MatchesAt pat s.startPos := by
   rw [← Pattern.Model.skipPrefix?_eq_none_iff, ← Option.isNone_iff_eq_none,
     ← isSome_skipPrefix?, Option.isSome_eq_false_iff]
 
-theorem Pattern.Model.startsWith_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+theorem Pattern.Model.startsWith_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat]
     [LawfulForwardPatternModel pat] {s : Slice} :
     s.startsWith pat = true ↔ MatchesAt pat s.startPos := by
   rw [← Bool.not_eq_false, startsWith_eq_false_iff, Classical.not_not]
@@ -65,13 +65,65 @@ theorem dropPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [Law
     {s : Slice} : s.dropPrefix? pat = none ↔ s.startsWith pat = false := by
   simp [dropPrefix?_eq_map_skipPrefix?]
 
-theorem Pattern.Model.eq_append_of_dropPrefix?_eq_some {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+theorem Pattern.Model.eq_append_of_dropPrefix?_eq_some {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat]
     [LawfulForwardPatternModel pat] {s res : Slice} (h : s.dropPrefix? pat = some res) :
-    ∃ t, ForwardPatternModel.Matches pat t ∧ s.copy = t ++ res.copy := by
+    ∃ t, PatternModel.Matches pat t ∧ s.copy = t ++ res.copy := by
   simp only [dropPrefix?_eq_map_skipPrefix?, Option.map_eq_some_iff, skipPrefix?_eq_some_iff] at h
   obtain ⟨pos, h₁, h₂⟩ := h
   exact ⟨(s.sliceTo pos).copy, h₁.isMatch.matches_copy, by simp [← h₂, ← copy_eq_copy_sliceTo]⟩
 
+theorem skipSuffix?_eq_backwardPatternSkipSuffix? {ρ : Type} {pat : ρ} [BackwardPattern pat] {s : Slice} :
+    s.skipSuffix? pat = BackwardPattern.skipSuffix? pat s := (rfl)
+
+theorem endsWith_eq_backwardPatternEndsWith {ρ : Type} {pat : ρ} [BackwardPattern pat] {s : Slice} :
+    s.endsWith pat = BackwardPattern.endsWith pat s := (rfl)
+
+theorem dropSuffix?_eq_map_skipSuffix? {ρ : Type} {pat : ρ} [BackwardPattern pat] {s : Slice} :
+    s.dropSuffix? pat = (s.skipSuffix? pat).map s.sliceTo := (rfl)
+
+theorem Pattern.Model.skipSuffix?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat]
+    [LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} :
+    s.skipSuffix? pat = some pos ↔ IsLongestRevMatch pat pos := by
+  rw [skipSuffix?_eq_backwardPatternSkipSuffix?, LawfulBackwardPatternModel.skipSuffix?_eq_some_iff]
+
+theorem Pattern.Model.skipSuffix?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat]
+    [LawfulBackwardPatternModel pat] {s : Slice} :
+    s.skipSuffix? pat = none ↔ ¬ RevMatchesAt pat s.endPos := by
+  rw [skipSuffix?_eq_backwardPatternSkipSuffix?, LawfulBackwardPatternModel.skipSuffix?_eq_none_iff]
+
+@[simp]
+theorem isSome_skipSuffix? {ρ : Type} {pat : ρ} [BackwardPattern pat] [LawfulBackwardPattern pat] {s : Slice} :
+    (s.skipSuffix? pat).isSome = s.endsWith pat := by
+  rw [endsWith_eq_backwardPatternEndsWith, skipSuffix?, LawfulBackwardPattern.endsWith_eq]
+
+theorem Pattern.Model.endsWith_eq_false_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat]
+    [LawfulBackwardPatternModel pat] {s : Slice} :
+    s.endsWith pat = false ↔ ¬ RevMatchesAt pat s.endPos := by
+  rw [← Pattern.Model.skipSuffix?_eq_none_iff, ← Option.isNone_iff_eq_none,
+    ← isSome_skipSuffix?, Option.isSome_eq_false_iff]
+
+theorem Pattern.Model.endsWith_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat]
+    [LawfulBackwardPatternModel pat] {s : Slice} :
+    s.endsWith pat = true ↔ RevMatchesAt pat s.endPos := by
+  rw [← Bool.not_eq_false, endsWith_eq_false_iff, Classical.not_not]
+
+@[simp]
+theorem skipSuffix?_eq_none_iff {ρ : Type} {pat : ρ} [BackwardPattern pat] [LawfulBackwardPattern pat]
+    {s : Slice} : s.skipSuffix? pat = none ↔ s.endsWith pat = false := by
+  rw [← Option.isNone_iff_eq_none, ← Option.isSome_eq_false_iff, isSome_skipSuffix?]
+
+@[simp]
+theorem dropSuffix?_eq_none_iff {ρ : Type} {pat : ρ} [BackwardPattern pat] [LawfulBackwardPattern pat]
+    {s : Slice} : s.dropSuffix? pat = none ↔ s.endsWith pat = false := by
+  simp [dropSuffix?_eq_map_skipSuffix?]
+
+theorem Pattern.Model.eq_append_of_dropSuffix?_eq_some {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat]
+    [LawfulBackwardPatternModel pat] {s res : Slice} (h : s.dropSuffix? pat = some res) :
+    ∃ t, PatternModel.Matches pat t ∧ s.copy = res.copy ++ t := by
+  simp only [dropSuffix?_eq_map_skipSuffix?, Option.map_eq_some_iff, skipSuffix?_eq_some_iff] at h
+  obtain ⟨pos, h₁, h₂⟩ := h
+  exact ⟨(s.sliceFrom pos).copy, h₁.isRevMatch.matches_copy, by simp [← h₂, ← copy_eq_copy_sliceTo]⟩
+
 end Slice
 
 theorem skipPrefix?_eq_skipPrefix?_toSlice {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : String} :
@@ -83,4 +135,13 @@ theorem startsWith_eq_startsWith_toSlice {ρ : Type} {pat : ρ} [ForwardPattern
 theorem dropPrefix?_eq_dropPrefix?_toSlice {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : String} :
     s.dropPrefix? pat = s.toSlice.dropPrefix? pat := (rfl)
 
+theorem skipSuffix?_eq_skipSuffix?_toSlice {ρ : Type} {pat : ρ} [BackwardPattern pat] {s : String} :
+    s.skipSuffix? pat = (s.toSlice.skipSuffix? pat).map Pos.ofToSlice := (rfl)
+
+theorem endsWith_eq_endsWith_toSlice {ρ : Type} {pat : ρ} [BackwardPattern pat] {s : String} :
+    s.endsWith pat = s.toSlice.endsWith pat := (rfl)
+
+theorem dropSuffix?_eq_dropSuffix?_toSlice {ρ : Type} {pat : ρ} [BackwardPattern pat] {s : String} :
+    s.dropSuffix? pat = s.toSlice.dropSuffix? pat := (rfl)
+
 end String

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Char.lean

@@ -11,6 +11,8 @@ public import Init.Data.String.TakeDrop
 import Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
 import Init.Data.String.Lemmas.Pattern.Char
 import Init.Data.Option.Lemmas
+import Init.Data.String.Lemmas.FindPos
+import Init.Data.List.Sublist
 
 public section
 
@@ -52,7 +54,42 @@ theorem startsWith_char_eq_false_iff_forall_append {c : Char} {s : Slice} :
 
 theorem eq_append_of_dropPrefix?_char_eq_some {c : Char} {s res : Slice} (h : s.dropPrefix? c = some res) :
     s.copy = singleton c ++ res.copy := by
-  simpa [ForwardPatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
+  simpa [PatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
+
+theorem skipSuffix?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} :
+    s.skipSuffix? c = some pos ↔ ∃ h, pos = s.endPos.prev h ∧ (s.endPos.prev h).get (by simp) = c := by
+  rw [Pattern.Model.skipSuffix?_eq_some_iff, Char.isLongestRevMatch_iff]
+
+theorem endsWith_char_iff_get {c : Char} {s : Slice} :
+    s.endsWith c ↔ ∃ h, (s.endPos.prev h).get (by simp) = c := by
+  simp [Pattern.Model.endsWith_iff, Char.revMatchesAt_iff]
+
+theorem endsWith_char_eq_false_iff_get {c : Char} {s : Slice} :
+    s.endsWith c = false ↔ ∀ h, (s.endPos.prev h).get (by simp) ≠ c := by
+  simp [Pattern.Model.endsWith_eq_false_iff, Char.revMatchesAt_iff]
+
+theorem endsWith_char_iff_exists_append {c : Char} {s : Slice} :
+    s.endsWith c ↔ ∃ t, s.copy = t ++ singleton c := by
+  rw [Pattern.Model.endsWith_iff, Char.revMatchesAt_iff_splits]
+  simp only [splits_endPos_iff, exists_eq_right, eq_comm (a := s.copy)]
+
+theorem endsWith_char_eq_getLast? {c : Char} {s : Slice} :
+    s.endsWith c = (s.copy.toList.getLast? == some c) := by
+  rw [Bool.eq_iff_iff, endsWith_char_iff_exists_append, beq_iff_eq,
+    ← List.singleton_suffix_iff_getLast?_eq_some, List.suffix_iff_exists_eq_append]
+  constructor
+  · rintro ⟨t, ht⟩
+    exact ⟨t.toList, by rw [ht, toList_append, toList_singleton]⟩
+  · rintro ⟨l, hl⟩
+    exact ⟨ofList l, by rw [← toList_inj, toList_append, toList_singleton, toList_ofList]; exact hl⟩
+
+theorem endsWith_char_eq_false_iff_forall_append {c : Char} {s : Slice} :
+    s.endsWith c = false ↔ ∀ t, s.copy ≠ t ++ singleton c := by
+  simp [← Bool.not_eq_true, endsWith_char_iff_exists_append]
+
+theorem eq_append_of_dropSuffix?_char_eq_some {c : Char} {s res : Slice} (h : s.dropSuffix? c = some res) :
+    s.copy = res.copy ++ singleton c := by
+  simpa [PatternModel.Matches] using Pattern.Model.eq_append_of_dropSuffix?_eq_some h
 
 end Slice
 
@@ -86,4 +123,34 @@ theorem eq_append_of_dropPrefix?_char_eq_some {c : Char} {s : String} {res : Sli
   rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
   simpa using Slice.eq_append_of_dropPrefix?_char_eq_some h
 
+theorem skipSuffix?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} :
+    s.skipSuffix? c = some pos ↔ ∃ h, pos = s.endPos.prev h ∧ (s.endPos.prev h).get (by simp) = c := by
+  simp [skipSuffix?_eq_skipSuffix?_toSlice, Slice.skipSuffix?_char_eq_some_iff, ← Pos.toSlice_inj,
+    Pos.prev_toSlice]
+
+theorem endsWith_char_iff_get {c : Char} {s : String} :
+    s.endsWith c ↔ ∃ h, (s.endPos.prev h).get (by simp) = c := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_char_iff_get, Pos.prev_toSlice]
+
+theorem endsWith_char_eq_false_iff_get {c : Char} {s : String} :
+    s.endsWith c = false ↔ ∀ h, (s.endPos.prev h).get (by simp) ≠ c := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_char_eq_false_iff_get, Pos.prev_toSlice]
+
+theorem endsWith_char_eq_getLast? {c : Char} {s : String} :
+    s.endsWith c = (s.toList.getLast? == some c) := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_char_eq_getLast?]
+
+theorem endsWith_char_iff_exists_append {c : Char} {s : String} :
+    s.endsWith c ↔ ∃ t, s = t ++ singleton c := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_char_iff_exists_append]
+
+theorem endsWith_char_eq_false_iff_forall_append {c : Char} {s : String} :
+    s.endsWith c = false ↔ ∀ t, s ≠ t ++ singleton c := by
+  simp [← Bool.not_eq_true, endsWith_char_iff_exists_append]
+
+theorem eq_append_of_dropSuffix?_char_eq_some {c : Char} {s : String} {res : Slice} (h : s.dropSuffix? c = some res) :
+    s = res.copy ++ singleton c := by
+  rw [dropSuffix?_eq_dropSuffix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropSuffix?_char_eq_some h
+
 end String

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Pred.lean

@@ -11,6 +11,7 @@ public import Init.Data.String.TakeDrop
 import Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
 import Init.Data.String.Lemmas.Pattern.Pred
 import Init.Data.Option.Lemmas
+import Init.Data.String.Lemmas.FindPos
 import Init.ByCases
 
 public section
@@ -45,7 +46,7 @@ theorem startsWith_bool_eq_head? {p : Char → Bool} {s : Slice} :
 
 theorem eq_append_of_dropPrefix?_bool_eq_some {p : Char → Bool} {s res : Slice} (h : s.dropPrefix? p = some res) :
     ∃ c, s.copy = singleton c ++ res.copy ∧ p c = true := by
-  obtain ⟨_, ⟨c, ⟨rfl, h₁⟩⟩, h₂⟩ := by simpa [ForwardPatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
+  obtain ⟨_, ⟨c, ⟨rfl, h₁⟩⟩, h₂⟩ := by simpa [PatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
   exact ⟨_, h₂, h₁⟩
 
 theorem skipPrefix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} :
@@ -69,6 +70,54 @@ theorem eq_append_of_dropPrefix_prop_eq_some {P : Char → Prop} [DecidablePred
   rw [dropPrefix?_prop_eq_dropPrefix?_decide] at h
   simpa using eq_append_of_dropPrefix?_bool_eq_some h
 
+theorem skipSuffix?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
+    s.skipSuffix? p = some pos ↔ ∃ h, pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get (by simp)) = true := by
+  rw [Pattern.Model.skipSuffix?_eq_some_iff, CharPred.isLongestRevMatch_iff]
+
+theorem endsWith_bool_iff_get {p : Char → Bool} {s : Slice} :
+    s.endsWith p ↔ ∃ h, p ((s.endPos.prev h).get (by simp)) = true := by
+  simp [Pattern.Model.endsWith_iff, CharPred.revMatchesAt_iff]
+
+theorem endsWith_bool_eq_false_iff_get {p : Char → Bool} {s : Slice} :
+    s.endsWith p = false ↔ ∀ h, p ((s.endPos.prev h).get (by simp)) = false := by
+  simp [Pattern.Model.endsWith_eq_false_iff, CharPred.revMatchesAt_iff]
+
+theorem endsWith_bool_eq_getLast? {p : Char → Bool} {s : Slice} :
+    s.endsWith p = s.copy.toList.getLast?.any p := by
+  rw [Bool.eq_iff_iff, Pattern.Model.endsWith_iff, CharPred.revMatchesAt_iff]
+  by_cases h : s.endPos = s.startPos
+  · refine ⟨fun ⟨h', _⟩ => by simp_all, ?_⟩
+    have : s.copy = "" := by simp_all [Slice.startPos_eq_endPos_iff.mp h.symm]
+    simp [this]
+  · obtain ⟨t, ht⟩ := s.splits_endPos.exists_eq_append_singleton_of_ne_startPos h
+    simp [h, ht]
+
+theorem eq_append_of_dropSuffix?_bool_eq_some {p : Char → Bool} {s res : Slice} (h : s.dropSuffix? p = some res) :
+    ∃ c, s.copy = res.copy ++ singleton c ∧ p c = true := by
+  obtain ⟨_, ⟨c, ⟨rfl, h₁⟩⟩, h₂⟩ := by simpa [PatternModel.Matches] using Pattern.Model.eq_append_of_dropSuffix?_eq_some h
+  exact ⟨_, h₂, h₁⟩
+
+theorem skipSuffix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} :
+    s.skipSuffix? P = some pos ↔ ∃ h, pos = s.endPos.prev h ∧ P ((s.endPos.prev h).get (by simp)) := by
+  simp [skipSuffix?_prop_eq_skipSuffix?_decide, skipSuffix?_bool_eq_some_iff]
+
+theorem endsWith_prop_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} :
+    s.endsWith P ↔ ∃ h, P ((s.endPos.prev h).get (by simp)) := by
+  simp [endsWith_prop_eq_endsWith_decide, endsWith_bool_iff_get]
+
+theorem endsWith_prop_eq_false_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} :
+    s.endsWith P = false ↔ ∀ h, ¬ P ((s.endPos.prev h).get (by simp)) := by
+  simp [endsWith_prop_eq_endsWith_decide, endsWith_bool_eq_false_iff_get]
+
+theorem endsWith_prop_eq_getLast? {P : Char → Prop} [DecidablePred P] {s : Slice} :
+    s.endsWith P = s.copy.toList.getLast?.any (decide <| P ·) := by
+  simp [endsWith_prop_eq_endsWith_decide, endsWith_bool_eq_getLast?]
+
+theorem eq_append_of_dropSuffix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropSuffix? P = some res) :
+    ∃ c, s.copy = res.copy ++ singleton c ∧ P c := by
+  rw [dropSuffix?_prop_eq_dropSuffix?_decide] at h
+  simpa using eq_append_of_dropSuffix?_bool_eq_some h
+
 end Slice
 
 theorem skipPrefix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
@@ -115,4 +164,48 @@ theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred
   rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
   simpa using Slice.eq_append_of_dropPrefix_prop_eq_some h
 
+theorem skipSuffix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
+    s.skipSuffix? p = some pos ↔ ∃ h, pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get (by simp)) = true := by
+  simp [skipSuffix?_eq_skipSuffix?_toSlice, Slice.skipSuffix?_bool_eq_some_iff, ← Pos.toSlice_inj,
+    Pos.prev_toSlice]
+
+theorem endsWith_bool_iff_get {p : Char → Bool} {s : String} :
+    s.endsWith p ↔ ∃ h, p ((s.endPos.prev h).get (by simp)) = true := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_bool_iff_get, Pos.prev_toSlice]
+
+theorem endsWith_bool_eq_false_iff_get {p : Char → Bool} {s : String} :
+    s.endsWith p = false ↔ ∀ h, p ((s.endPos.prev h).get (by simp)) = false := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_bool_eq_false_iff_get, Pos.prev_toSlice]
+
+theorem endsWith_bool_eq_getLast? {p : Char → Bool} {s : String} :
+    s.endsWith p = s.toList.getLast?.any p := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_bool_eq_getLast?]
+
+theorem eq_append_of_dropSuffix?_bool_eq_some {p : Char → Bool} {s : String} {res : Slice} (h : s.dropSuffix? p = some res) :
+    ∃ c, s = res.copy ++ singleton c ∧ p c = true := by
+  rw [dropSuffix?_eq_dropSuffix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropSuffix?_bool_eq_some h
+
+theorem skipSuffix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} :
+    s.skipSuffix? P = some pos ↔ ∃ h, pos = s.endPos.prev h ∧ P ((s.endPos.prev h).get (by simp)) := by
+  simp [skipSuffix?_eq_skipSuffix?_toSlice, Slice.skipSuffix?_prop_eq_some_iff, ← Pos.toSlice_inj,
+    Pos.prev_toSlice]
+
+theorem endsWith_prop_iff_get {P : Char → Prop} [DecidablePred P] {s : String} :
+    s.endsWith P ↔ ∃ h, P ((s.endPos.prev h).get (by simp)) := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_prop_iff_get, Pos.prev_toSlice]
+
+theorem endsWith_prop_eq_false_iff_get {P : Char → Prop} [DecidablePred P] {s : String} :
+    s.endsWith P = false ↔ ∀ h, ¬ P ((s.endPos.prev h).get (by simp)) := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_prop_eq_false_iff_get, Pos.prev_toSlice]
+
+theorem endsWith_prop_eq_getLast? {P : Char → Prop} [DecidablePred P] {s : String} :
+    s.endsWith P = s.toList.getLast?.any (decide <| P ·) := by
+  simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_prop_eq_getLast?]
+
+theorem eq_append_of_dropSuffix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s : String} {res : Slice}
+    (h : s.dropSuffix? P = some res) : ∃ c, s = res.copy ++ singleton c ∧ P c := by
+  rw [dropSuffix?_eq_dropSuffix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropSuffix?_prop_eq_some h
+
 end String

src/Init/Data/String/Lemmas/Pattern/TakeDrop/String.lean

@@ -67,7 +67,7 @@ theorem eq_append_of_dropPrefix?_slice_eq_some {pat s res : Slice} (h : s.dropPr
   | false =>
     have := ForwardSliceSearcher.lawfulForwardPatternModel hpat
     have := Pattern.Model.eq_append_of_dropPrefix?_eq_some h
-    simp only [ForwardPatternModel.Matches] at this
+    simp only [PatternModel.Matches] at this
     obtain ⟨_, ⟨-, rfl⟩, h⟩ := this
     exact h
   | true => simp [Option.some.inj (h ▸ dropPrefix?_slice_of_isEmpty hpat), (show pat.copy = "" by simpa)]
@@ -104,6 +104,87 @@ theorem eq_append_of_dropPrefix?_string_eq_some {pat : String} {s res : Slice} (
   rw [dropPrefix?_string_eq_dropPrefix?_toSlice] at h
   simpa using eq_append_of_dropPrefix?_slice_eq_some h
 
+theorem skipSuffix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    s.skipSuffix? pat = some s.endPos := by
+  rw [skipSuffix?_eq_backwardPatternSkipSuffix?, BackwardSliceSearcher.skipSuffix?_of_isEmpty hpat]
+
+@[simp]
+theorem skipSuffix?_slice_eq_some_iff {pat s : Slice} {pos : s.Pos} :
+    s.skipSuffix? pat = some pos ↔ ∃ t, pos.Splits t pat.copy := by
+  match h : pat.isEmpty with
+  | false =>
+    have := BackwardSliceSearcher.lawfulBackwardPatternModel h
+    rw [Pattern.Model.skipSuffix?_eq_some_iff, ForwardSliceSearcher.isLongestRevMatch_iff_splits h]
+  | true => simp [skipSuffix?_slice_of_isEmpty h, (show pat.copy = "" by simpa), eq_comm]
+
+theorem endsWith_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    s.endsWith pat = true := by
+  rw [endsWith_eq_backwardPatternEndsWith, BackwardSliceSearcher.endsWith_of_isEmpty hpat]
+
+@[simp]
+theorem endsWith_slice_iff {pat s : Slice} :
+    s.endsWith pat ↔ pat.copy.toList <:+ s.copy.toList := by
+  match h : pat.isEmpty with
+  | false =>
+    have := BackwardSliceSearcher.lawfulBackwardPatternModel h
+    simp only [Model.endsWith_iff, ForwardSliceSearcher.revMatchesAt_iff_splits h,
+      splits_endPos_iff, exists_eq_right]
+    simp only [← toList_inj, toList_append, List.suffix_iff_exists_append_eq]
+    exact ⟨fun ⟨t, ht⟩ => ⟨t.toList, by simp [ht]⟩, fun ⟨t, ht⟩ => ⟨String.ofList t, by simp [← ht]⟩⟩
+  | true => simp [endsWith_slice_of_isEmpty h, (show pat.copy = "" by simpa)]
+
+@[simp]
+theorem endsWith_slice_eq_false_iff {pat s : Slice} :
+    s.endsWith pat = false ↔ ¬ (pat.copy.toList <:+ s.copy.toList) := by
+  simp [← Bool.not_eq_true, endsWith_slice_iff]
+
+theorem dropSuffix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    s.dropSuffix? pat = some s := by
+  simp [dropSuffix?_eq_map_skipSuffix?, skipSuffix?_slice_of_isEmpty hpat]
+
+theorem eq_append_of_dropSuffix?_slice_eq_some {pat s res : Slice} (h : s.dropSuffix? pat = some res) :
+    s.copy = res.copy ++ pat.copy := by
+  match hpat : pat.isEmpty with
+  | false =>
+    have := BackwardSliceSearcher.lawfulBackwardPatternModel hpat
+    have := Pattern.Model.eq_append_of_dropSuffix?_eq_some h
+    simp only [PatternModel.Matches] at this
+    obtain ⟨_, ⟨-, rfl⟩, h⟩ := this
+    exact h
+  | true => simp [Option.some.inj (h ▸ dropSuffix?_slice_of_isEmpty hpat), (show pat.copy = "" by simpa)]
+
+@[simp]
+theorem skipSuffix?_string_eq_some_iff' {pat : String} {s : Slice} {pos : s.Pos} :
+    s.skipSuffix? pat = some pos ↔ ∃ t, pos.Splits t pat := by
+  simp [skipSuffix?_string_eq_skipSuffix?_toSlice]
+
+@[simp]
+theorem skipSuffix?_string_empty {s : Slice} : s.skipSuffix? "" = some s.endPos := by
+  simp
+
+@[simp]
+theorem endsWith_string_iff {pat : String} {s : Slice} :
+    s.endsWith pat ↔ pat.toList <:+ s.copy.toList := by
+  simp [endsWith_string_eq_endsWith_toSlice]
+
+@[simp]
+theorem endsWith_string_empty {s : Slice} : s.endsWith "" = true := by
+  simp
+
+@[simp]
+theorem endsWith_string_eq_false_iff {pat : String} {s : Slice} :
+    s.endsWith pat = false ↔ ¬ (pat.toList <:+ s.copy.toList) := by
+  simp [endsWith_string_eq_endsWith_toSlice]
+
+@[simp]
+theorem dropSuffix?_string_empty {s : Slice} : s.dropSuffix? "" = some s := by
+  simpa [dropSuffix?_string_eq_dropSuffix?_toSlice] using dropSuffix?_slice_of_isEmpty (by simp)
+
+theorem eq_append_of_dropSuffix?_string_eq_some {pat : String} {s res : Slice} (h : s.dropSuffix? pat = some res) :
+    s.copy = res.copy ++ pat := by
+  rw [dropSuffix?_string_eq_dropSuffix?_toSlice] at h
+  simpa using eq_append_of_dropSuffix?_slice_eq_some h
+
 end Slice
 
 theorem skipPrefix?_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) :

src/Init/Data/String/Lemmas/Splits.lean

@@ -367,7 +367,7 @@ theorem Slice.Pos.Splits.of_prev {s : Slice} {p : s.Pos} {hp}
   obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_prev p hp)
   exact splits_prev_right p hp
 
-theorem Slice.sliceTo_copy_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ : String} :
+theorem Slice.copy_sliceTo_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ : String} :
     (s.sliceTo p).copy = t₁ ↔ ∃ t₂, p.Splits t₁ t₂ := by
   refine ⟨?_, ?_⟩
   · rintro rfl
@@ -375,13 +375,21 @@ theorem Slice.sliceTo_copy_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ :
   · rintro ⟨t₂, h⟩
     exact p.splits.eq_left h
 
-theorem sliceTo_copy_eq_iff_exists_splits {s : String} {p : s.Pos} {t₁ : String} :
-    (s.sliceTo p).copy = t₁ ↔ ∃ t₂, p.Splits t₁ t₂ := by
+theorem Slice.copy_sliceFrom_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₂ : String} :
+    (s.sliceFrom p).copy = t₂ ↔ ∃ t₁, p.Splits t₁ t₂ := by
   refine ⟨?_, ?_⟩
   · rintro rfl
     exact ⟨_, p.splits⟩
   · rintro ⟨t₂, h⟩
-    exact p.splits.eq_left h
+    exact p.splits.eq_right h
+
+theorem copy_sliceTo_eq_iff_exists_splits {s : String} {p : s.Pos} {t₁ : String} :
+    (s.sliceTo p).copy = t₁ ↔ ∃ t₂, p.Splits t₁ t₂ := by
+  simp [← Pos.splits_toSlice_iff, ← Slice.copy_sliceTo_eq_iff_exists_splits]
+
+theorem copy_sliceFrom_eq_iff_exists_splits {s : String} {p : s.Pos} {t₂ : String} :
+    (s.sliceFrom p).copy = t₂ ↔ ∃ t₁, p.Splits t₁ t₂ := by
+  simp [← Pos.splits_toSlice_iff, ← Slice.copy_sliceFrom_eq_iff_exists_splits]
 
 theorem Pos.Splits.offset_eq_decreaseBy {s : String} {p : s.Pos} (h : p.Splits t₁ t₂) :
     p.offset = s.rawEndPos.decreaseBy t₂.utf8ByteSize := by
@@ -427,8 +435,7 @@ theorem Slice.splits_singleton_iff {s : Slice} {p : s.Pos} {c : Char} {t : Strin
       simp [startPos_ne_endPos_iff, ← copy_ne_empty_iff, h.eq_append]
     have spl : (s.startPos.next this).Splits (singleton c) t := by
       rw [← empty_append (s := singleton c)]
-      apply Pos.Splits.next
-      simp [h.eq_append]
+      exact Pos.Splits.next (by simp [h.eq_append])
     refine ⟨this, ⟨h.pos_eq spl, ?_, h.eq_append⟩⟩
     rw [← empty_append (s := singleton c)] at spl
     exact spl.get_eq_of_singleton
@@ -442,6 +449,27 @@ theorem splits_singleton_iff {s : String} {p : s.Pos} {c : Char} {t : String} :
   rw [← Pos.splits_toSlice_iff, Slice.splits_singleton_iff]
   simp [← Pos.ofToSlice_inj]
 
+theorem Slice.splits_singleton_right_iff {s : Slice} {p : s.Pos} {c : Char} {t : String} :
+    p.Splits t (singleton c) ↔
+      ∃ h, p = s.endPos.prev h ∧ (s.endPos.prev h).get (by simp) = c ∧ s.copy = t ++ singleton c := by
+  refine ⟨fun h => ?_, ?_⟩
+  · have : s.endPos ≠ s.startPos := by
+      simp [ne_comm (a := s.endPos), startPos_ne_endPos_iff, ← copy_ne_empty_iff, h.eq_append]
+    have spl : (s.endPos.prev this).Splits t (singleton c) := by
+      rw [← append_empty (s := singleton c)]
+      exact Pos.Splits.prev (by simp [h.eq_append])
+    refine ⟨this, ⟨h.pos_eq spl, ?_, h.eq_append⟩⟩
+    exact (h.eq_append ▸ Pos.next_prev (h := this) ▸ s.splits_endPos).get_eq_of_singleton
+  · rintro ⟨h, ⟨rfl, rfl, h'⟩⟩
+    rw [← String.append_empty (s := singleton _)]
+    exact Pos.Splits.prev (by simp [h'])
+
+theorem splits_singleton_right_iff {s : String} {p : s.Pos} {c : Char} {t : String} :
+    p.Splits t (singleton c) ↔
+      ∃ h, p = s.endPos.prev h ∧ (s.endPos.prev h).get (by simp) = c ∧ s = t ++ singleton c := by
+  rw [← Pos.splits_toSlice_iff, Slice.splits_singleton_right_iff]
+  simp [← Pos.ofToSlice_inj, Pos.prev_toSlice]
+
 theorem Slice.splits_next_startPos {s : Slice} {h : s.startPos ≠ s.endPos} :
     (s.startPos.next h).Splits
       (singleton (s.startPos.get h)) (s.sliceFrom (s.startPos.next h)).copy := by
@@ -456,6 +484,20 @@ theorem splits_next_startPos {s : String} {h : s.startPos ≠ s.endPos} :
   rw [← Pos.splits_toSlice_iff]
   apply (Slice.splits_next_startPos).of_eq <;> simp [String.Pos.next_toSlice]
 
+theorem Slice.splits_prev_endPos {s : Slice} {h : s.endPos ≠ s.startPos} :
+    (s.endPos.prev h).Splits
+      (s.sliceTo (s.endPos.prev h)).copy (singleton ((s.endPos.prev h).get (by simp))) := by
+  rw [← String.append_empty (s := singleton _)]
+  apply Slice.Pos.Splits.prev
+  have := Slice.Pos.splits_prev_right s.endPos h
+  rwa [copy_sliceFrom_endPos] at this
+
+theorem splits_prev_endPos {s : String} {h : s.endPos ≠ s.startPos} :
+    (s.endPos.prev h).Splits
+      (s.sliceTo (s.endPos.prev h)).copy (singleton ((s.endPos.prev h).get (by simp))) := by
+  rw [← Pos.splits_toSlice_iff]
+  apply (Slice.splits_prev_endPos).of_eq <;> simp [String.Pos.prev_toSlice, h]
+
 theorem Slice.Pos.Splits.toByteArray_eq_left {s : Slice} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) :
     t₁.toByteArray = s.copy.toByteArray.extract 0 p.offset.byteIdx := by
   rw [h.eq_left p.splits]

src/Init/Data/String/Pattern/Basic.lean

@@ -117,7 +117,7 @@ class ForwardPattern {ρ : Type} (pat : ρ) where
   -/
   startsWith : (s : Slice) → Bool := fun s => (skipPrefix? s).isSome
 
-@[deprecated ForwardPattern.dropPrefix? (since := "2026-03-19")]
+@[deprecated ForwardPattern.skipPrefix? (since := "2026-03-19")]
 def ForwardPattern.dropPrefix? {ρ : Type} (pat : ρ) [ForwardPattern pat] (s : Slice) : Option s.Pos :=
   ForwardPattern.skipPrefix? pat s
 

src/Init/Data/String/Pattern/Char.lean

@@ -47,8 +47,8 @@ instance {c : Char} : LawfulBackwardPattern c where
   skipSuffixOfNonempty?_eq h := LawfulBackwardPattern.skipSuffixOfNonempty?_eq (pat := (· == c)) h
   endsWith_eq s := LawfulBackwardPattern.endsWith_eq (pat := (· == c)) s
 
-instance {c : Char} : ToBackwardSearcher c (ToBackwardSearcher.DefaultBackwardSearcher c) :=
-  .defaultImplementation
+instance {c : Char} : ToBackwardSearcher c (ToBackwardSearcher.DefaultBackwardSearcher (· == c)) where
+  toSearcher s := ToBackwardSearcher.toSearcher (· == c) s
 
 end Char
 

src/Init/Data/String/Pattern/Pred.lean

@@ -139,8 +139,9 @@ instance {p : Char → Prop} [DecidablePred p] : LawfulBackwardPattern p where
   skipSuffixOfNonempty?_eq h := LawfulBackwardPattern.skipSuffixOfNonempty?_eq (pat := (decide <| p ·)) h
   endsWith_eq s := LawfulBackwardPattern.endsWith_eq (pat := (decide <| p ·)) s
 
-instance {p : Char → Prop} [DecidablePred p] : ToBackwardSearcher p (ToBackwardSearcher.DefaultBackwardSearcher p) :=
-  .defaultImplementation
+instance {p : Char → Prop} [DecidablePred p] :
+    ToBackwardSearcher p (ToBackwardSearcher.DefaultBackwardSearcher (decide <| p ·)) where
+  toSearcher s := ToBackwardSearcher.toSearcher (decide <| p ·) s
 
 end Decidable
 

src/Init/Prelude.lean

@@ -185,15 +185,21 @@ example : foo.default = (default, default) :=
 abbrev inferInstance {α : Sort u} [i : α] : α := i
 
 set_option checkBinderAnnotations false in
-/-- `inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
-"instance normal form": the result is a constructor application whose sub-instance fields
-are canonical instances and whose types match `α` exactly. This is useful when `α` is
-definitionally equal to some `α'` for which instances are registered, as it prevents
-leaking the definition's RHS at lower transparencies. See `Lean.Meta.InstanceNormalForm`
-for details. Example:
+/-- `inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
+definitionally equal type if necessary. This is useful when `α` is definitionally equal to
+some `α'` for which instances are registered, as it prevents leaking the definition's RHS
+at lower transparencies.
+
+`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
+instance without transporting between types, use `inferInstance` instead.
+
+Example:
 ```
-#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
+def D := Nat
+instance : Inhabited D := inferInstanceAs (Inhabited Nat)
 ```
+
+See `Lean.Meta.WrapInstance` for details.
 -/
 abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i
 

src/Init/Tactics.lean

@@ -2259,42 +2259,6 @@ with grind
 ```
 This is more convenient than the equivalent `· by rename_i _ acc _; exact I1 acc`.
 
-### Witnesses
-
-When a specification has a parameter whose type is tagged with `@[mvcgen_witness_type]`, `mvcgen`
-classifies the corresponding goal as a *witness* rather than a verification condition.
-Witnesses are concrete values that the user must provide (inspired by zero-knowledge proofs),
-as opposed to invariants (predicates maintained across loop iterations) or verification conditions
-(propositions to prove).
-
-Witness goals are labelled `witness1`, `witness2`, etc. and can be provided in a `witnesses` section
-that appears before the `invariants` section:
-```
-mvcgen [...] witnesses
-· W1
-· W2
-invariants
-· I1
-with grind
-```
-Like invariants, witnesses support case label syntax:
-```
-mvcgen [...] witnesses
-| witness1 => W1
-```
-
-See the `@[mvcgen_witness_type]` attribute for how to register custom witness types.
-
-### Invariant and witness type attributes
-
-The `@[mvcgen_invariant_type]` and `@[mvcgen_witness_type]` tag attributes control how `mvcgen`
-classifies subgoals:
-* A goal whose type is an application of a type tagged with `@[mvcgen_invariant_type]` is classified
-  as an invariant (`inv<n>`).
-* A goal whose type is an application of a type tagged with `@[mvcgen_witness_type]` is classified
-  as a witness (`witness<n>`).
-* All other goals are classified as verification conditions (`vc<n>`).
-
 ### Invariant suggestions
 
 `mvcgen` will suggest invariants for you if you use the `invariants?` keyword.

src/Lean/Compiler/IR/CompilerM.lean

@@ -10,6 +10,7 @@ public import Lean.Compiler.IR.Format
 public import Lean.Compiler.ExportAttr
 public import Lean.Compiler.LCNF.PublicDeclsExt
 import Lean.Compiler.InitAttr
+import all Lean.Compiler.ModPkgExt
 import Init.Data.Format.Macro
 import Lean.Compiler.LCNF.Basic
 
@@ -129,8 +130,14 @@ private def exportIREntries (env : Environment) : Array (Name × Array EnvExtens
   -- safety: cast to erased type
   let initDecls : Array EnvExtensionEntry := unsafe unsafeCast initDecls
 
+  -- needed during initialization via interpreter
+  let modPkg : Array (Option PkgId) := modPkgExt.exportEntriesFn env (modPkgExt.getState env) .private
+  -- safety: cast to erased type
+  let modPkg : Array EnvExtensionEntry := unsafe unsafeCast modPkg
+
   #[(declMapExt.name, irEntries),
-    (Lean.regularInitAttr.ext.name, initDecls)]
+    (Lean.regularInitAttr.ext.name, initDecls),
+    (modPkgExt.name, modPkg)]
 
 def findEnvDecl (env : Environment) (declName : Name) : Option Decl :=
   Compiler.LCNF.findExtEntry? env declMapExt declName findAtSorted? (·.2.find?)

src/Lean/Compiler/LCNF/Basic.lean

@@ -342,6 +342,11 @@ def LetValue.toExpr (e : LetValue pu) : Expr :=
   | .unbox var _ => mkApp (.const `unbox []) (.fvar var)
   | .isShared fvarId _ => mkApp (.const `isShared []) (.fvar fvarId)
 
+def LetValue.isPersistent (val : LetValue .impure) : Bool :=
+  match val with
+  | .fap _ xs => xs.isEmpty -- all global constants are persistent
+  | _ => false
+
 structure LetDecl (pu : Purity) where
   fvarId : FVarId
   binderName : Name

src/Lean/Compiler/LCNF/ExplicitRC.lean

@@ -235,11 +235,6 @@ def withParams (ps : Array (Param .impure)) (x : RcM α) : RcM α := do
       { ctx with idx := ctx.idx + 1, varMap }
   withReader update x
 
-def LetValue.isPersistent (val : LetValue .impure) : Bool :=
-  match val with
-  | .fap _ xs => xs.isEmpty -- all global constants are persistent
-  | _ => false
-
 @[inline]
 def withLetDecl (decl : LetDecl .impure) (x : RcM α) : RcM α := do
   let update := fun ctx =>

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -390,9 +390,12 @@ where
       if let .fvar parent := args[1]! then
         if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
     | .fap f args =>
-      let ps ← getParamInfo (.decl f)
-      ownFVar z (.functionCallResult z)
-      ownArgsUsingParams args ps (.functionCallArg z)
+      -- Constants remain alive at least until the end of execution and can thus effectively be seen
+      -- as a "borrowed" read.
+      if args.size > 0 then
+        let ps ← getParamInfo (.decl f)
+        ownFVar z (.functionCallResult z)
+        ownArgsUsingParams args ps (.functionCallArg z)
     | .fvar x args =>
       ownFVar z (.functionCallResult z); ownFVar x (.fvarCall z); ownArgs (.fvarCall z) args
     | .pap _ args => ownFVar z (.functionCallResult z); ownArgs (.partialApplication z) args

src/Lean/Compiler/LCNF/PropagateBorrow.lean

@@ -121,7 +121,10 @@ where
       if let .fvar parent := args[1]! then
         let parentVal ← getOwnedness parent
         join z parentVal
-    | .ctor .. | .fap .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
+    | .fap _ args =>
+      let value := if args.isEmpty then .borrow else .own
+      join z value
+    | .ctor .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
       join z .own
     | _ => unreachable!
 

src/Lean/Elab/BuiltinTerm.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lean.Meta.Diagnostics
-public import Lean.Meta.InstanceNormalForm
+public import Lean.Meta.WrapInstance
 public import Lean.Elab.Open
 public import Lean.Elab.SetOption
 public import Lean.Elab.Eval
@@ -334,10 +334,10 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let type ← abstractInstImplicitArgs type
   let inst ← synthInstance type
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
-    -- Normalize to instance normal form.
+    -- Wrap instance so its type matches the expected type exactly.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
     let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
-    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
+    withNewMCtxDepth <| wrapInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/Deriving/Basic.lean

@@ -9,7 +9,7 @@ prelude
 public import Lean.Elab.App
 public import Lean.Elab.DeclNameGen
 import Lean.Compiler.NoncomputableAttr
-import Lean.Meta.InstanceNormalForm
+import Lean.Meta.WrapInstance
 
 public section
 
@@ -211,10 +211,10 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
           -- We don't reduce because of abbreviations such as `DecidableEq`
           forallTelescope classExpr fun _ classExpr => do
             let result ← mkInst classExpr declName decl value
-            -- Save the pre-normalization value for the noncomputable check below,
-            -- since `normalizeInstance` may inline noncomputable constants.
+            -- Save the pre-wrapping value for the noncomputable check below,
+            -- since `wrapInstance` may inline noncomputable constants.
             let preNormClosure ← Closure.mkValueTypeClosure result.instType result.instVal (zetaDelta := true)
-            -- Compute instance name early so `normalizeInstance` can use it for aux def naming.
+            -- Compute instance name early so `wrapInstance` can use it for aux def naming.
             let env ← getEnv
             let mut instName := (← getCurrNamespace) ++ (← NameGen.mkBaseNameWithSuffix "inst" preNormClosure.type)
             instName ← liftMacroM <| mkUnusedBaseName instName
@@ -223,7 +223,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
-                normalizeInstance result.instVal result.instType
+                wrapInstance result.instVal result.instType
                   (logCompileErrors := false)  -- covered by noncomputable check below
                   (isMeta := isMeta)
             else

src/Lean/Elab/PreDefinition/Basic.lean

@@ -10,7 +10,7 @@ public import Lean.Compiler.NoncomputableAttr
 public import Lean.Util.NumApps
 public import Lean.Meta.Eqns
 public import Lean.Elab.RecAppSyntax
-public import Lean.Meta.InstanceNormalForm
+public import Lean.Meta.WrapInstance
 public import Lean.Elab.DefView
 public section
 

src/Lean/Elab/Tactic/Do/Attr.lean

@@ -268,24 +268,3 @@ def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool :=
     mvcgenInvariantAttr.hasTag env name
   else
     false
-
-/--
-Marks a type as a witness type for the `mvcgen` tactic.
-Goals whose type is an application of a tagged type will be classified
-as witnesses rather than verification conditions.
-In the spirit of zero-knowledge proofs, witnesses are concrete values that the user
-must provide, as opposed to invariants (predicates maintained across iterations)
-or verification conditions (propositions to prove).
--/
-builtin_initialize mvcgenWitnessTypeAttr : TagAttribute ←
-  registerTagAttribute `mvcgen_witness_type
-    "marks a type as a witness type for the `mvcgen` tactic"
-
-/--
-Returns `true` if `ty` is an application of a type tagged with `@[mvcgen_witness_type]`.
--/
-def isMVCGenWitnessType (env : Environment) (ty : Expr) : Bool :=
-  if let .const name .. := ty.getAppFn then
-    mvcgenWitnessTypeAttr.hasTag env name
-  else
-    false

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -35,7 +35,6 @@ namespace VCGen
 
 structure Result where
   invariants : Array MVarId
-  witnesses : Array MVarId
   vcs : Array MVarId
 
 partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result := do
@@ -46,13 +45,10 @@ partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result
     for h : idx in *...state.invariants.size do
       let mv := state.invariants[idx]
       mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1)))
-    for h : idx in *...state.witnesses.size do
-      let mv := state.witnesses[idx]
-      mv.setTag (Name.mkSimple ("witness" ++ toString (idx + 1)))
     for h : idx in *...state.vcs.size do
       let mv := state.vcs[idx]
       mv.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ (← mv.getTag).eraseMacroScopes)
-    return { invariants := state.invariants, witnesses := state.witnesses, vcs := state.vcs }
+    return { invariants := state.invariants, vcs := state.vcs }
 where
   onFail (goal : MGoal) (name : Name) : VCGenM Expr := do
     -- trace[Elab.Tactic.Do.vcgen] "fail {goal.toExpr}"
@@ -356,70 +352,53 @@ where
 
 end VCGen
 
-/-- Shared implementation for elaborating goal sections (invariants, witnesses).
-    `tagPrefix` is `"inv"` or `"witness"`, used to parse labels like `inv1` or `witness2`.
-    `label` is `"invariant"` or `"witness"`, used in error messages.
-    When `requireAll` is true, an error is thrown if fewer alts are provided than goals. -/
-private def elabGoalSection (goals : Array MVarId) (alts : Array Syntax)
-    (tagPrefix : String) (label : String) (requireAll := true) : TacticM Unit := do
-  let goals ← goals.filterM (not <$> ·.isAssigned)
-  let mut dotOrCase := LBool.undef -- .true => dot
-  for h : n in 0...alts.size do
-    let alt := alts[n]
-    match alt with
-    | `(goalDotAlt| · $rhs) =>
-      if dotOrCase matches .false then
-        logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported."
-        break
-      dotOrCase := .true
-      let some mv := goals[n]? | do
-        logErrorAt alt m!"More {label}s have been defined ({alts.size}) than there were unassigned {label} goals `{tagPrefix}<n>` ({goals.size})."
-        continue
-      withRef rhs do
-      discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
-    | `(goalCaseAlt| | $tag $args* => $rhs) =>
-      if dotOrCase matches .true then
-        logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported."
-        break
-      dotOrCase := .false
-      let n? : Option Nat := do
-          let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal
-          let .str .anonymous s := tag.getId | none
-          s.dropPrefix? tagPrefix >>= String.Slice.toNat?
-      let some mv := do goals[(← n?) - 1]? | do
-        logErrorAt alt m!"No {label} with label {tag} {repr tag}."
-        continue
-      if ← mv.isAssigned then
-        logErrorAt alt m!"{label} {n?.get!} is already assigned."
-        continue
-      withRef rhs do
-      discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv
-    | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}"
-  if requireAll && alts.size < goals.size then
-    let missingTypes ← goals[alts.size:].toArray.mapM (·.getType)
-    throwError "Lacking definitions for the following {label}s.\n{toMessageList missingTypes}"
-
-def elabWitnesses (stx : Syntax) (witnesses : Array MVarId) : TacticM Unit := do
-  let some stx := stx.getOptional? | return ()
-  let stx : TSyntax ``witnessAlts := ⟨stx⟩
-  withRef stx do
-  match stx with
-  | `(witnessAlts| witnesses $alts*) =>
-    elabGoalSection witnesses alts "witness" "witness"
-  | _ => logErrorAt stx m!"Expected witnessAlts, got {stx}"
-
 def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) : TacticM Unit := do
   let some stx := stx.getOptional? | return ()
   let stx : TSyntax ``invariantAlts := ⟨stx⟩
   withRef stx do
   match stx with
   | `(invariantAlts| $invariantsKW $alts*) =>
+    let invariants ← invariants.filterM (not <$> ·.isAssigned)
+
+    let mut dotOrCase := LBool.undef -- .true => dot
+    for h : n in 0...alts.size do
+      let alt := alts[n]
+      match alt with
+      | `(goalDotAlt| · $rhs) =>
+        if dotOrCase matches .false then
+          logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
+          break
+        dotOrCase := .true
+        let some mv := invariants[n]? | do
+          logErrorAt alt m!"More invariants have been defined ({alts.size}) than there were unassigned invariants goals `inv<n>` ({invariants.size})."
+          continue
+        withRef rhs do
+        discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
+      | `(goalCaseAlt| | $tag $args* => $rhs) =>
+        if dotOrCase matches .true then
+          logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
+          break
+        dotOrCase := .false
+        let n? : Option Nat := do
+            let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal
+            let .str .anonymous s := tag.getId | none
+            s.dropPrefix? "inv" >>= String.Slice.toNat?
+        let some mv := do invariants[(← n?) - 1]? | do
+          logErrorAt alt m!"No invariant with label {tag} {repr tag}."
+          continue
+        if ← mv.isAssigned then
+          logErrorAt alt m!"Invariant {n?.get!} is already assigned."
+          continue
+        withRef rhs do
+        discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv
+      | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}"
+
     if let `(invariantsKW| invariants) := invariantsKW then
-      elabGoalSection invariants alts "inv" "invariant"
+      if alts.size < invariants.size then
+        let missingTypes ← invariants[alts.size:].toArray.mapM (·.getType)
+        throwErrorAt stx m!"Lacking definitions for the following invariants.\n{toMessageList missingTypes}"
     else
-      -- We have `invariants?`. First elaborate any user-provided alts, then suggest the rest.
-      elabGoalSection invariants alts "inv" "invariant" (requireAll := false)
-      let invariants ← invariants.filterM (not <$> ·.isAssigned)
+      -- Otherwise, we have `invariants?`. Suggest missing invariants.
       let mut suggestions := #[]
       for i in 0...invariants.size do
         let mv := invariants[i]!
@@ -478,8 +457,8 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
     | none => .unlimited
   let goal ← getMainGoal
   let goal ← if ctx.config.elimLets then elimLets goal else pure goal
-  let { invariants, witnesses, vcs } ← VCGen.genVCs goal ctx fuel
-  trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  let { invariants, vcs } ← VCGen.genVCs goal ctx fuel
+  trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
   let runOnVCs (tac : TSyntax `tactic) (extraMsg : MessageData) (vcs : Array MVarId) : TermElabM (Array MVarId) :=
     vcs.flatMapM fun vc =>
       tryCatchRuntimeEx
@@ -488,13 +467,10 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
         (fun ex => throwError "Error while running {tac} on {vc}Message: {indentD ex.toMessageData}\n{extraMsg}")
   let invariants ←
     if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." invariants else pure invariants
-  trace[Elab.Tactic.Do.vcgen] "before elabWitnesses {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  elabWitnesses stx[3] witnesses
-  let witnesses ← witnesses.filterM (not <$> ·.isAssigned)
-  trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  elabInvariants stx[4] invariants (suggestInvariant vcs)
+  trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  elabInvariants stx[3] invariants (suggestInvariant vcs)
   let invariants ← invariants.filterM (not <$> ·.isAssigned)
-  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
   let vcs ← do
     let vcs ← if ctx.config.trivial then runOnVCs (← `(tactic| try mvcgen_trivial)) "Try again with -trivial." vcs else pure vcs
     let vcs ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." vcs else pure vcs
@@ -502,17 +478,17 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
   -- Eliminating lets here causes some metavariables in `mkFreshPair_triple` to become nonassignable
   -- so we don't do it. Presumably some weird delayed assignment thing is going on.
   -- let vcs ← if ctx.config.elimLets then liftMetaM <| vcs.mapM elimLets else pure vcs
-  trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  let vcs ← elabVCs stx[5] vcs
-  trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  replaceMainGoal (invariants ++ witnesses ++ vcs).toList
+  trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  let vcs ← elabVCs stx[4] vcs
+  trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  replaceMainGoal (invariants ++ vcs).toList
   -- trace[Elab.Tactic.Do.vcgen] "replaced main goal, new: {← getGoals}"
 
 @[builtin_tactic Lean.Parser.Tactic.mvcgenHint]
 def elabMVCGenHint : Tactic := fun stx => withMainContext do
   let stx' : TSyntax ``mvcgen := TSyntax.mk <| stx
     |>.setKind ``Lean.Parser.Tactic.mvcgen
-    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push mkNullNode |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
+    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
   -- logInfo m!"{stx}\n{toString stx}\n{repr stx}"
   -- logInfo m!"{stx'}\n{toString stx'}\n{repr stx'}"
   Lean.Meta.Tactic.TryThis.addSuggestion stx stx'

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -73,10 +73,6 @@ structure State where
   -/
   invariants : Array MVarId := #[]
   /--
-  Holes of witness type that have been generated so far.
-  -/
-  witnesses : Array MVarId := #[]
-  /--
   The verification conditions that have been generated so far.
   -/
   vcs : Array MVarId := #[]
@@ -108,11 +104,8 @@ def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
   -- VC to the user as-is, without abstracting any variables in the local context.
   -- This only makes sense for synthetic opaque metavariables.
   goal.setKind .syntheticOpaque
-  let env ← getEnv
-  if isMVCGenInvariantType env ty then
+  if isMVCGenInvariantType (← getEnv) ty then
     modify fun s => { s with invariants := s.invariants.push goal }
-  else if isMVCGenWitnessType env ty then
-    modify fun s => { s with witnesses := s.witnesses.push goal }
   else
     modify fun s => { s with vcs := s.vcs.push goal }
 

src/Lean/Meta.lean

@@ -27,7 +27,7 @@ public import Lean.Meta.Match
 public import Lean.Meta.ReduceEval
 public import Lean.Meta.Closure
 public import Lean.Meta.AbstractNestedProofs
-public import Lean.Meta.InstanceNormalForm
+public import Lean.Meta.WrapInstance
 public import Lean.Meta.LetToHave
 public import Lean.Meta.ForEachExpr
 public import Lean.Meta.Transform

src/Lean/Meta/Sym/SymM.lean

@@ -15,6 +15,8 @@ register_builtin_option sym.debug : Bool := {
   descr    := "check invariants"
 }
 
+builtin_initialize registerTraceClass `sym.issues
+
 /-!
 ## Sym Extensions
 
@@ -134,9 +136,16 @@ structure SharedExprs where
   ordEqExpr  : Expr
   intExpr    : Expr
 
+/-- Configuration options for the symbolic computation framework. -/
+structure Config where
+  /-- When `true`, issues are collected during proof search and reported on failure. -/
+  verbose : Bool := true
+  deriving Inhabited
+
 /-- Readonly context for the symbolic computation framework. -/
 structure Context where
   sharedExprs : SharedExprs
+  config      : Config := {}
 
 /-- Mutable state for the symbolic computation framework. -/
 structure State where
@@ -177,6 +186,11 @@ structure State where
   defEqI : PHashMap (ExprPtr × ExprPtr) Bool := {}
   /-- State for registered `SymExtension`s, indexed by extension id. -/
   extensions : Array SymExtensionState := #[]
+  /--
+  Issues found during symbolic computation. Accumulated across operations
+  within a `sym =>` block and reported when a tactic fails.
+  -/
+  issues : List MessageData := []
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
@@ -266,6 +280,55 @@ abbrev share (e : Expr) : SymM Expr :=
 @[inline] def isDebugEnabled : SymM Bool :=
   return (← get).debug
 
+def getConfig : SymM Config :=
+  return (← readThe Context).config
+
+/-- Adds an issue message to the issue tracker. -/
+def reportIssue (msg : MessageData) : SymM Unit := do
+  let msg ← addMessageContext msg
+  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
+  trace[sym.issues] msg
+
+/-- Reports an issue if `verbose` mode is enabled. Does nothing if `verbose` is `false`. -/
+@[inline] def reportIssueIfVerbose (msg : MessageData) : SymM Unit := do
+  if (← getConfig).verbose then
+    reportIssue msg
+
+private meta def expandReportIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| Sym.reportIssueIfVerbose $msg)
+
+/-- Reports an issue if `verbose` mode is enabled. -/
+macro "reportIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandReportIssueMacro s.raw
+
+/-- Reports an issue if both `verbose` and `sym.debug` are enabled. Does nothing otherwise. -/
+@[inline] def reportDbgIssue (msg : MessageData) : SymM Unit := do
+  if (← getConfig).verbose then
+    if sym.debug.get (← getOptions) then
+      reportIssue msg
+
+meta def expandReportDbgIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| Sym.reportDbgIssue $msg)
+
+/-- Similar to `reportIssue!`, but only reports issue if `sym.debug` is set to `true`. -/
+macro "reportDbgIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandReportDbgIssueMacro s.raw
+
+/-- Returns all accumulated issues without clearing them. -/
+def getIssues : SymM (List MessageData) :=
+  return (← get).issues
+
+/--
+Runs `x` with a fresh issue context. Issues reported during `x` are
+prepended to the issues that existed before the call.
+-/
+def withNewIssueContext (x : SymM α) : SymM α := do
+  let saved := (← get).issues
+  modify fun s => { s with issues := [] }
+  try x finally modify fun s => { s with issues := s.issues ++ saved }
+
 /-- Similar to `Meta.isDefEqI`, but the result is cache using pointer equality. -/
 def isDefEqI (s t : Expr) : SymM Bool := do
   let key := (⟨s⟩, ⟨t⟩)

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -206,7 +206,7 @@ def handleApp : Simproc := fun e => do
   match fn with
   | .const constName _ =>
     if (← isCbvOpaque constName) then
-      return (← tryCbvTheorems e).markAsDone
+      return markAsDoneIfFailed <| ← tryCbvTheorems e
     let info ← getConstInfo constName
     tryCbvTheorems <|> (guardSimproc (fun _ => info.hasValue) handleConstApp) <|> reduceRecMatcher <| e
   | .lam .. => betaReduce e
@@ -215,7 +215,7 @@ def handleApp : Simproc := fun e => do
 def handleOpaqueConst : Simproc := fun e => do
   let .const constName _ := e | return .rfl
   if (← isCbvOpaque constName) then
-    return (← tryCbvTheorems e).markAsDone
+    return markAsDoneIfFailed <| ← tryCbvTheorems e
   return .rfl
 
 def foldLit : Simproc := fun e => do

src/Lean/Meta/Tactic/Cbv/Util.lean

@@ -108,4 +108,8 @@ public partial def getListLitElems (e : Expr) (acc : Array Expr := #[]) : Option
   | List.cons _ a as => getListLitElems as <| acc.push a
   | _ => none
 
+public def markAsDoneIfFailed : Result → Result
+  | .rfl _ cd => .rfl true cd
+  | .step e h d cd => .step e h d cd
+
 end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Grind.lean

@@ -63,7 +63,6 @@ builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
 builtin_initialize registerTraceClass `grind.ematch.instance.delayed
 builtin_initialize registerTraceClass `grind.eqResolution
-builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.split
 builtin_initialize registerTraceClass `grind.split.candidate

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -53,7 +53,7 @@ def mkEqCnstr (p : Poly) (h : EqCnstrProof) : RingM EqCnstr := do
 Returns the ring expression denoting the given Lean expression.
 Recall that we compute the ring expressions during internalization.
 -/
-private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadRing m] (e : Expr) : m (Option RingExpr) := do
+private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadLiftT Sym.SymM m] [MonadRing m] (e : Expr) : m (Option RingExpr) := do
   let ring ← getRing
   if let some re := ring.denote.find? { expr := e } then
     return some re
@@ -67,7 +67,7 @@ private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadRing m] (e : Expr)
 Returns the semiring expression denoting the given Lean expression.
 Recall that we compute the semiring expressions during internalization.
 -/
-private def toSemiringExpr? [Monad m] [MonadLiftT GrindM m] [MonadSemiring m] (e : Expr) : m (Option SemiringExpr) := do
+private def toSemiringExpr? [Monad m] [MonadLiftT GrindM m] [MonadLiftT Sym.SymM m] [MonadSemiring m] (e : Expr) : m (Option SemiringExpr) := do
   let semiring ← getSemiring
   if let some re := semiring.denote.find? { expr := e } then
     return some re

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -456,7 +456,7 @@ private def getUnassignedLevelMVars (e : Expr) : MetaM (Array LMVarId) := do
 -- **Note**: issues reported by the E-matching module are too distractive. We only
 -- report them if `set_option grind.debug true`
 macro "reportEMatchIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
-  expandReportDbgIssueMacro s.raw
+  Sym.expandReportDbgIssueMacro s.raw
 
 /--
 Stores new theorem instance in the state.

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -104,6 +104,8 @@ private def discharge? (e : Expr) : SimpM (Option Expr) := do
 open Sym
 
 def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTactic := none) : MetaM α := Sym.SymM.run do
+  withNewIssueContext do
+  withReader (fun ctx => { ctx with config.verbose := params.config.verbose }) do
   /- **Note**: Consider using `Sym.simp` in the future. -/
   let simprocs  := params.normProcs
   let simpMethods := Simp.mkMethods simprocs discharge? (wellBehavedDischarge := true)
@@ -332,7 +334,7 @@ private def initCore (mvarId : MVarId) : GrindM Goal := do
     processHypotheses goal
 
 def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
-  let issues     := (← get).issues
+  let issues     ← Sym.getIssues
   let counters   := (← get).counters
   let splitDiags := (← get).splitDiags
   let simp       := { (← get).simp with }

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -214,11 +214,6 @@ structure State where
   and implement the macro `trace_goal`.
   -/
   lastTag    : Name := .anonymous
-  /--
-  Issues found during the proof search. These issues are reported to
-  users when `grind` fails.
-  -/
-  issues     : List MessageData := []
   /-- Performance counters -/
   counters   : Counters := {}
   /-- Split diagnostic information. This information is only collected when `set_option diagnostics true` -/
@@ -401,35 +396,6 @@ def mkHCongrWithArity (f : Expr) (numArgs : Nat) : GrindM CongrTheorem := do
   modify fun s => { s with congrThms := s.congrThms.insert key result }
   return result
 
-def reportIssue (msg : MessageData) : GrindM Unit := do
-  let msg ← addMessageContext msg
-  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
-  /-
-  We also add a trace message because we may want to know when
-  an issue happened relative to other trace messages.
-  -/
-  trace[grind.issues] msg
-
-private meta def expandReportIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
-  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
-  `(doElem| do
-    if (← getConfig).verbose then
-      reportIssue $msg)
-
-macro "reportIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
-  expandReportIssueMacro s.raw
-
-/-- Similar to `expandReportIssueMacro`, but only reports issue if `grind.debug` is set to `true` -/
-meta def expandReportDbgIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
-  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
-  `(doElem| do
-    if (← getConfig).verbose then
-      if grind.debug.get (← getOptions) then
-        reportIssue $msg)
-
-/-- Similar to `reportIssue!`, but only reports issue if `grind.debug` is set to `true` -/
-macro "reportDbgIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
-  expandReportDbgIssueMacro s.raw
 
 /--
 Each E-node may have "solver terms" attached to them.

src/Lean/Meta/Tactic/Grind/Util.lean

@@ -130,7 +130,7 @@ def foldProjs (e : Expr) : MetaM Expr := do
   let post (e : Expr) := do
     let .proj structName idx s := e | return .done e
     let some info := getStructureInfo? (← getEnv) structName |
-      trace[grind.issues] "found `Expr.proj` but `{structName}` is not marked as structure{indentExpr e}"
+      trace[sym.issues] "found `Expr.proj` but `{structName}` is not marked as structure{indentExpr e}"
       return .done e
     if h : idx < info.fieldNames.size then
       let fieldName := info.fieldNames[idx]
@@ -149,7 +149,7 @@ def foldProjs (e : Expr) : MetaM Expr := do
       -/
       return .visit (← withDefault <| mkProjection s fieldName)
     else
-      trace[grind.issues] "found `Expr.proj` with invalid field index `{idx}`{indentExpr e}"
+      trace[sym.issues] "found `Expr.proj` with invalid field index `{idx}`{indentExpr e}"
       return .done e
   Meta.transform e (post := post)
 

src/Lean/Meta/WrapInstance.lean

@@ -13,17 +13,16 @@ public import Lean.Meta.CtorRecognizer
 public section
 
 /-!
-# Instance Normal Form
+# Instance Wrapping
 
-Both `inferInstanceAs` and the default `deriving` handler normalize instance bodies to
-"instance normal form". This ensures that when deriving or inferring an instance for a
-semireducible type definition, the definition's RHS is not leaked when reduced at lower
-than semireducible transparency.
+Both `inferInstanceAs` and the default `deriving` handler wrap instance bodies to ensure
+that when deriving or inferring an instance for a semireducible type definition, the
+definition's RHS is not leaked when reduced at lower than semireducible transparency.
 
 ## Algorithm
 
 Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
-`normalizeInstance` constructs a result instance as follows, executing all steps at
+`wrapInstance` constructs a result instance as follows, executing all steps at
 `instances` transparency:
 
 1. If `I'` is not a class, return `i` unchanged.
@@ -46,7 +45,7 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 
 ## Options
 
-- `backward.inferInstanceAs.wrap`: master switch for normalization in both `inferInstanceAs`
+- `backward.inferInstanceAs.wrap`: master switch for wrapping in both `inferInstanceAs`
   and the default `deriving` handler
 - `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for sub-instance
   fields to avoid non-defeq instance diamonds
@@ -59,7 +58,7 @@ namespace Lean.Meta
 
 register_builtin_option backward.inferInstanceAs.wrap : Bool := {
   defValue := true
-  descr := "normalize instance bodies to constructor-based normal form in `inferInstanceAs` and the default `deriving` handler"
+  descr := "wrap instance bodies in `inferInstanceAs` and the default `deriving` handler"
 }
 
 register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
@@ -77,7 +76,7 @@ register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
   descr := "wrap data fields in auxiliary definitions to fix their types"
 }
 
-builtin_initialize registerTraceClass `Meta.instanceNormalForm
+builtin_initialize registerTraceClass `Meta.wrapInstance
 
 /--
 Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
@@ -95,16 +94,16 @@ def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
   instantiateMVars (mkAppN fn args)
 
 /--
-Normalize an instance value to "instance normal form".
+Wrap an instance value so its type matches the expected type exactly.
 See the module docstring for the full algorithm specification.
 -/
-partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
+partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
     (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
-  withTraceNode `Meta.instanceNormalForm
+  withTraceNode `Meta.wrapInstance
       (fun _ => return m!"type: {expectedType}") do
   let some className ← isClass? expectedType
     | return inst
-  trace[Meta.instanceNormalForm] "class is {className}"
+  trace[Meta.wrapInstance] "class is {className}"
 
   if ← isProp expectedType then
     if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
@@ -117,7 +116,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
   inst.withApp fun f args => do
     let some (.ctorInfo ci) ← f.constName?.mapM getConstInfo
       | do
-        trace[Meta.instanceNormalForm] "did not reduce to constructor application, returning/wrapping as is: {inst}"
+        trace[Meta.wrapInstance] "did not reduce to constructor application, returning/wrapping as is: {inst}"
         if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
           let instType ← inferType inst
           if ← isDefEq expectedType instType then
@@ -135,11 +134,11 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
           return inst
     let (mvars, _, cls) ← forallMetaTelescope (← inferType f)
     if h₁ : args.size ≠ mvars.size then
-      throwError "instance normal form: incorrect number of arguments for \
+      throwError "wrapInstance: incorrect number of arguments for \
         constructor application `{f}`: {args}"
     else
       unless ← isDefEq expectedType cls do
-        throwError "instance normal form: `{expectedType}` does not unify with the conclusion of \
+        throwError "wrapInstance: `{expectedType}` does not unify with the conclusion of \
           `{.ofConstName ci.name}`"
       for h₂ : i in ci.numParams...args.size do
         have : i < mvars.size := by
@@ -155,7 +154,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
           if ← isDefEq argExpectedType argType then
             mvarId.assign arg
           else
-            trace[Meta.instanceNormalForm] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
+            trace[Meta.wrapInstance] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
             mvarId.assign (← mkAuxTheorem argExpectedType arg (zetaDelta := true))
         -- Recurse into instance arguments of the constructor
         else if (← isClass? argExpectedType).isSome then
@@ -165,12 +164,12 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             -- semireducible transparency.
             try
               if let .some new ← trySynthInstance argExpectedType then
-                trace[Meta.instanceNormalForm] "using existing instance {new}"
+                trace[Meta.wrapInstance] "using existing instance {new}"
                 mvarId.assign new
                 continue
             catch _ => pure ()
 
-          mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
+          mvarId.assign (← wrapInstance arg argExpectedType (compile := compile)
             (logCompileErrors := logCompileErrors) (isMeta := isMeta))
         else
           -- For data fields, assign directly or wrap in aux def to fix types.

src/Lean/Parser/Term.lean

@@ -774,10 +774,15 @@ In particular, it is like a unary operation with a fixed parameter `b`, where on
 @[builtin_term_parser] def noImplicitLambda := leading_parser
   "no_implicit_lambda% " >> termParser maxPrec
 /--
-`inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
-"instance normal form": the result is a constructor application whose sub-instance
-fields are canonical instances and whose types match `α` exactly. See
-`Lean.Meta.InstanceNormalForm` for details.
+`inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
+definitionally equal type if necessary. This is useful when `α` is definitionally equal to
+some `α'` for which instances are registered, as it prevents leaking the definition's RHS
+at lower transparencies.
+
+`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
+instance without transporting between types, use `inferInstance` instead.
+
+See `Lean.Meta.WrapInstance` for details.
 -/
 @[builtin_term_parser] def «inferInstanceAs» := leading_parser
   "inferInstanceAs" >> (((" $ " <|> " <| ") >> termParser minPrec) <|> (ppSpace >> termParser argPrec))

src/Std/Tactic/Do/Syntax.lean

@@ -364,30 +364,15 @@ macro "mvcgen_trivial" : tactic =>
   )
 
 /--
-A goal section alternative of the form `· term`, one per goal.
-Used by both `invariants` and `witnesses` sections.
+An invariant alternative of the form `· term`, one per invariant goal.
 -/
 syntax goalDotAlt := ppDedent(ppLine) cdotTk (colGe term)
 
 /--
-A goal section alternative of the form `| label<n> a b c => term`, one per goal.
-Used by both `invariants` and `witnesses` sections.
+An invariant alternative of the form `| inv<n> a b c => term`, one per invariant goal.
 -/
 syntax goalCaseAlt := ppDedent(ppLine) "| " caseArg " => " (colGe term)
 
-/--
-The contextual keyword ` witnesses `.
--/
-syntax witnessesKW := &"witnesses "
-
-/--
-After `mvcgen [...]`, there can be an optional `witnesses` followed by either
-* a bulleted list of witnesses `· term; · term`.
-* a labelled list of witnesses `| witness1 => term; witness2 a b c => term`, which is useful for
-  naming inaccessibles.
--/
-syntax witnessAlts := witnessesKW withPosition((colGe (goalDotAlt <|> goalCaseAlt))*)
-
 /--
 Either the contextual keyword ` invariants ` or its tracing form ` invariants? ` which suggests
 skeletons for missing invariants as a hint.
@@ -395,7 +380,7 @@ skeletons for missing invariants as a hint.
 syntax invariantsKW := &"invariants " <|> &"invariants? "
 
 /--
-After `mvcgen [...] witnesses ...`, there can be an optional `invariants` followed by either
+After `mvcgen [...]`, there can be an optional `invariants` followed by either
 * a bulleted list of invariants `· term; · term`.
 * a labelled list of invariants `| inv1 => term; inv2 a b c => term`, which is useful for naming
   inaccessibles.
@@ -419,7 +404,7 @@ syntax vcAlts := "with " (ppSpace colGt tactic)? withPosition((colGe vcAlt)*)
 @[tactic_alt Lean.Parser.Tactic.mvcgenMacro]
 syntax (name := mvcgen) "mvcgen" optConfig
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
-  (witnessAlts)? (invariantAlts)? (vcAlts)? : tactic
+  (invariantAlts)? (vcAlts)? : tactic
 
 /--
 A hint tactic that expands to `mvcgen invariants?`.