Compare commits

..

3 Commits

Author SHA1 Message Date
Joachim Breitner
7f1f95e107 fix: propagate parent cancel token to asTask subtasks
`CancelToken` now supports an optional parent pointer. When `isSet` is
called, it checks both the token itself and its parent (recursively).
This ensures that server-level cancellation propagates to subtasks
spawned via `TacticM.asTask'` (as used by `TacticM.par` in `try?`).

Previously, `Core.wrapAsync` replaced the cancel token with a fresh one,
so subtasks were completely disconnected from the server's cancellation.
This meant that when a file was re-elaborated, `try?`'s parallel subtasks
would continue running until they finished or hit heartbeat limits.

Now `CoreM.asTask` creates a child token with the parent's token as its
parent, so `Core.checkInterrupted` in the subtask also detects when the
parent has been cancelled.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-31 12:44:28 +00:00
Joachim Breitner
a583459614 test: add cancellation test for asTask' subtasks
This adds a server_interactive test that demonstrates that subtasks
spawned via `TacticM.asTask'` (as used by `TacticM.par` in `try?`)
do not inherit their parent's cancellation token.

The test currently FAILS because `Core.wrapAsync` replaces the cancel
token with a fresh one, so server-level cancellation never reaches the
subtask. The expected output assumes the fix is in place
("subtask-cancelled\!" instead of "leaked\!").

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-31 11:01:42 +00:00
Joachim Breitner
f506964bde feat: add try? => tac syntax for testing evalSuggest directly
This adds a `try? => tacticSeq` variant that skips the automatic tactic
generation phase and feeds the user-supplied tactic directly to
`evalSuggest`. This is useful for testing `evalSuggest` with explicit
tactic scripts using `try?`'s internal combinators (`attempt_all`,
`attempt_all_par`, `first_par`, etc.).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-31 10:55:44 +00:00
1549 changed files with 8238 additions and 8337 deletions

View File

@@ -7,11 +7,6 @@ To build Lean you should use `make -j$(nproc) -C build/release`.
The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
To rebuild individual modules without a full build, use Lake directly:
```
cd src && lake build Init.Prelude
```
## Running Tests
See `tests/README.md` for full documentation. Quick reference:
@@ -61,11 +56,6 @@ make -C build/release/stage2 clean-stdlib
```
must be run manually before building.
To rebuild individual stage 2 modules without a full `make stage2`, use Lake directly:
```
cd build/release/stage2 && lake build Init.Prelude
```
## New features
When asked to implement new features:

View File

@@ -157,16 +157,6 @@ Note: `gh pr checks --watch` exits as soon as ALL checks complete (pass or fail)
fail while others are still running, `--watch` will continue until everything settles, then exit
with a non-zero code. So a background `--watch` finishing = all checks done; check which failed.
## Mathlib Bump Branches
Mathlib `bump/v4.X.0` branches live on the **fork** `leanprover-community/mathlib4-nightly-testing`,
NOT on `leanprover-community/mathlib4`.
## Never Force-Update Remote Refs Without Confirmation
Never force-update an existing remote branch or tag via `git push --force` or the GitHub API
without explicit user confirmation.
## Error Handling
**CRITICAL**: If something goes wrong or a command fails:

View File

@@ -276,10 +276,10 @@ jobs:
- name: Check rebootstrap
run: |
set -e
git config user.email "stage0@lean-fro.org"
git config user.name "update-stage0"
# clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
# changes yet
make -C build update-stage0
git commit --allow-empty -m "chore: update-stage0"
make -C build/stage1 clean-stdlib
time make -C build -j$NPROC
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC
if: matrix.check-rebootstrap

View File

@@ -143,7 +143,7 @@ jobs:
CMAKE_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " src/CMakeLists.txt | grep -oE '[0-9]+')
CMAKE_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " src/CMakeLists.txt | grep -oE '[0-9]+')
CMAKE_PATCH=$(grep -E "^set\(LEAN_VERSION_PATCH " src/CMakeLists.txt | grep -oE '[0-9]+')
CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+' | head -1)
CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | sed -nE 's/^set\(LEAN_VERSION_IS_RELEASE ([0-9]+)\).*/\1/p')
# Expected values from tag parsing
TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"

View File

@@ -6,6 +6,6 @@ vscode:
- leanprover.lean4
tasks:
- name: Build
init: cmake --preset dev
- name: Release build
init: cmake --preset release
command: make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)

View File

@@ -1,6 +1,4 @@
cmake_minimum_required(VERSION 3.21)
include(ExternalProject)
include(FetchContent)
if(NOT CMAKE_GENERATOR MATCHES "Makefiles")
message(FATAL_ERROR "Only makefile generators are supported")
@@ -36,6 +34,7 @@ foreach(var ${vars})
endif()
endforeach()
include(ExternalProject)
project(LEAN CXX C)
if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
@@ -120,16 +119,17 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
endif()
if(USE_MIMALLOC)
FetchContent_Declare(
ExternalProject_Add(
mimalloc
PREFIX mimalloc
GIT_REPOSITORY https://github.com/microsoft/mimalloc
GIT_TAG v2.2.3
# Unnecessarily deep directory structure, but it saves us from a complicated
# stage0 update for now. If we ever update the other dependencies like
# cadical, it might be worth reorganizing the directory structure.
SOURCE_DIR "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
# just download, we compile it as part of each stage as it is small
CONFIGURE_COMMAND ""
BUILD_COMMAND ""
INSTALL_COMMAND ""
)
FetchContent_MakeAvailable(mimalloc)
list(APPEND EXTRA_DEPENDS mimalloc)
endif()
if(NOT STAGE1_PREV_STAGE)

View File

@@ -8,26 +8,16 @@
"configurePresets": [
{
"name": "release",
"displayName": "Release build config",
"displayName": "Default development optimized build config",
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/release"
},
{
"name": "dev",
"displayName": "Default development optimized build config",
"cacheVariables": {
"STRIP_BINARIES": "OFF"
},
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/dev"
},
{
"name": "debug",
"displayName": "Debug build config",
"cacheVariables": {
"CMAKE_BUILD_TYPE": "Debug",
"LEAN_EXTRA_CXX_FLAGS": "-DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
"STRIP_BINARIES": "OFF"
"CMAKE_BUILD_TYPE": "Debug"
},
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/debug"
@@ -36,8 +26,7 @@
"name": "reldebug",
"displayName": "Release with assertions enabled",
"cacheVariables": {
"CMAKE_BUILD_TYPE": "RelWithAssert",
"STRIP_BINARIES": "OFF"
"CMAKE_BUILD_TYPE": "RelWithAssert"
},
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/reldebug"
@@ -49,7 +38,6 @@
"LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined -DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
"LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined",
"LEAN_EXTRA_LINKER_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
"STRIP_BINARIES": "OFF",
"SMALL_ALLOCATOR": "OFF",
"USE_MIMALLOC": "OFF",
"BSYMBOLIC": "OFF",
@@ -70,10 +58,6 @@
"name": "release",
"configurePreset": "release"
},
{
"name": "dev",
"configurePreset": "dev"
},
{
"name": "debug",
"configurePreset": "debug"
@@ -97,11 +81,6 @@
"configurePreset": "release",
"output": {"outputOnFailure": true, "shortProgress": true}
},
{
"name": "dev",
"configurePreset": "dev",
"output": {"outputOnFailure": true, "shortProgress": true}
},
{
"name": "debug",
"configurePreset": "debug",

View File

@@ -30,9 +30,6 @@ cd lean4
cmake --preset release
make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)
```
For development, `cmake --preset dev` is recommended instead.
You can replace `$(nproc || sysctl -n hw.logicalcpu)` with the desired parallelism amount.
The above commands will compile the Lean library and binaries into the

View File

@@ -311,16 +311,16 @@ def check_cmake_version(repo_url, branch, version_major, version_minor, github_t
print(f" ❌ Could not retrieve {cmake_file_path} from {branch}")
return False
expected_patterns = [
(f"LEAN_VERSION_MAJOR", rf"^set\(LEAN_VERSION_MAJOR\s+{version_major}[\s)]", f"set(LEAN_VERSION_MAJOR {version_major} ...)"),
(f"LEAN_VERSION_MINOR", rf"^set\(LEAN_VERSION_MINOR\s+{version_minor}[\s)]", f"set(LEAN_VERSION_MINOR {version_minor} ...)"),
(f"LEAN_VERSION_PATCH", rf"^set\(LEAN_VERSION_PATCH\s+0[\s)]", f"set(LEAN_VERSION_PATCH 0 ...)"),
(f"LEAN_VERSION_IS_RELEASE", rf"^set\(LEAN_VERSION_IS_RELEASE\s+1[\s)]", f"set(LEAN_VERSION_IS_RELEASE 1 ...)"),
expected_lines = [
f"set(LEAN_VERSION_MAJOR {version_major})",
f"set(LEAN_VERSION_MINOR {version_minor})",
f"set(LEAN_VERSION_PATCH 0)",
f"set(LEAN_VERSION_IS_RELEASE 1)"
]
for name, pattern, display in expected_patterns:
if not any(re.match(pattern, l.strip()) for l in content.splitlines()):
print(f" ❌ Missing or incorrect line in {cmake_file_path}: {display}")
for line in expected_lines:
if not any(l.strip().startswith(line) for l in content.splitlines()):
print(f" ❌ Missing or incorrect line in {cmake_file_path}: {line}")
return False
print(f" ✅ CMake version settings are correct in {cmake_file_path}")
@@ -343,11 +343,11 @@ def check_stage0_version(repo_url, branch, version_major, version_minor, github_
for line in content.splitlines():
stripped = line.strip()
if stripped.startswith("set(LEAN_VERSION_MAJOR "):
actual = stripped.split()[1].rstrip(")")
actual = stripped.split()[-1].rstrip(")")
if actual != str(version_major):
errors.append(f"LEAN_VERSION_MAJOR: expected {version_major}, found {actual}")
elif stripped.startswith("set(LEAN_VERSION_MINOR "):
actual = stripped.split()[1].rstrip(")")
actual = stripped.split()[-1].rstrip(")")
if actual != str(version_minor):
errors.append(f"LEAN_VERSION_MINOR: expected {version_minor}, found {actual}")

View File

@@ -14,6 +14,13 @@ 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

View File

@@ -8,7 +8,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4 CACHE STRING "")
set(LEAN_VERSION_MINOR 31 CACHE STRING "")
set(LEAN_VERSION_MINOR 30 CACHE STRING "")
set(LEAN_VERSION_PATCH 0 CACHE STRING "")
set(LEAN_VERSION_IS_RELEASE 0 CACHE STRING "") # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -80,7 +80,6 @@ option(CCACHE "use ccache" ON)
option(SPLIT_STACK "SPLIT_STACK" OFF)
# When OFF we disable LLVM support
option(LLVM "LLVM" OFF)
option(STRIP_BINARIES "Strip produced binaries" ON)
# When ON we include githash in the version string
option(USE_GITHASH "GIT_HASH" ON)
@@ -615,38 +614,6 @@ else()
OUTPUT_VARIABLE GIT_SHA1
OUTPUT_STRIP_TRAILING_WHITESPACE
)
# Fallback for jj workspaces where git cannot find .git directly.
# Use `jj git root` to find the backing git repo, then `jj log` to
# resolve the current workspace's commit (git HEAD points to the root
# workspace, not the current one).
if("${GIT_SHA1}" STREQUAL "")
find_program(JJ_EXECUTABLE jj)
if(JJ_EXECUTABLE)
execute_process(
COMMAND "${JJ_EXECUTABLE}" git root
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
OUTPUT_VARIABLE _jj_git_dir
OUTPUT_STRIP_TRAILING_WHITESPACE
ERROR_QUIET
RESULT_VARIABLE _jj_git_root_result
)
execute_process(
COMMAND "${JJ_EXECUTABLE}" log -r @ --no-graph -T "commit_id"
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
OUTPUT_VARIABLE _jj_commit
OUTPUT_STRIP_TRAILING_WHITESPACE
ERROR_QUIET
RESULT_VARIABLE _jj_rev_result
)
if(_jj_git_root_result EQUAL 0 AND _jj_rev_result EQUAL 0)
execute_process(
COMMAND git --git-dir "${_jj_git_dir}" ls-tree "${_jj_commit}" stage0 --object-only
OUTPUT_VARIABLE GIT_SHA1
OUTPUT_STRIP_TRAILING_WHITESPACE
)
endif()
endif()
endif()
message(STATUS "stage0 sha1: ${GIT_SHA1}")
# Now that we've prepared the information for the next stage, we can forget that we will use
# Lake in the future as we won't use it in this stage
@@ -830,14 +797,7 @@ if(LLVM AND STAGE GREATER 0)
set(EXTRA_LEANMAKE_OPTS "LLVM=1")
endif()
set(
STDLIBS
Init
Std
Lean
Leanc
LeanIR
)
set(STDLIBS Init Std Lean Leanc LeanIR)
if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
list(APPEND STDLIBS Lake LeanChecker)
endif()
@@ -945,7 +905,10 @@ if(PREV_STAGE)
endif()
if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
add_custom_target(leanir ALL DEPENDS leanshared COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir VERBATIM)
add_custom_target(leanir ALL
DEPENDS leanshared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir
VERBATIM)
endif()
# use Bash version for building, use Lean version in bin/ for tests & distribution

View File

@@ -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, expose]
@[always_inline, inline]
def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α m β) (error : ε m β) : m β :=
x _ ok error
@@ -83,8 +83,6 @@ 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
@@ -93,20 +91,7 @@ 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
@[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 run_bind_throw [Monad m] (e : ε) (f : α ExceptCpsT ε m β) : run (throw e >>= f : ExceptCpsT ε m β) = run (throw e) := rfl
@[simp] theorem runCatch_pure [Monad m] : runCatch (pure x : ExceptCpsT α m α) = pure x := rfl
@@ -117,7 +102,6 @@ theorem run_bind_throw [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : run
@[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
@[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
@[simp] theorem runCatch_bind_throw [Monad m] (e : β) (f : α ExceptCpsT β m β) : runCatch (throw e >>= f : ExceptCpsT β m β) = pure e := rfl
end ExceptCpsT

View File

@@ -113,7 +113,7 @@ public theorem _root_.List.min?_toArray [Min α] {l : List α} :
· simp [List.min_toArray, List.min_eq_get_min?, - List.get_min?]
· simp_all
@[simp, grind =, cbv_eval ]
@[simp, grind =]
public theorem min?_toList [Min α] {xs : Array α} :
xs.toList.min? = xs.min? := by
cases xs; simp
@@ -153,7 +153,7 @@ public theorem _root_.List.max?_toArray [Max α] {l : List α} :
· simp [List.max_toArray, List.max_eq_get_max?, - List.get_max?]
· simp_all
@[simp, grind =, cbv_eval ]
@[simp, grind =]
public theorem max?_toList [Max α] {xs : Array α} :
xs.toList.max? = xs.max? := by
cases xs; simp

View File

@@ -20,20 +20,12 @@ universe u
namespace ByteArray
@[extern "lean_sarray_dec_eq"]
def beq (lhs rhs : @& ByteArray) : Bool :=
lhs.data == rhs.data
instance : BEq ByteArray where
beq := beq
deriving instance BEq for ByteArray
attribute [ext] ByteArray
@[extern "lean_sarray_dec_eq"]
def decEq (lhs rhs : @& ByteArray) : Decidable (lhs = rhs) :=
decidable_of_decidable_of_iff ByteArray.ext_iff.symm
instance : DecidableEq ByteArray := decEq
instance : DecidableEq ByteArray :=
fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm
instance : Inhabited ByteArray where
default := empty

View File

@@ -527,14 +527,6 @@ theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.ca
@[simp, grind =] theorem val_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
/-
**Note**
The current pattern inference heuristic includes the implicit term `n + m` as pattern of the pattern,
but arithmetic is problematic in patterns because it is an interpreted symbol. For example,
we will fail to match `@val n (castNat 0 i)`. Thus, we mark the implicit subterm with `no_index`
-/
grind_pattern val_castAdd => @val (no_index _) (castAdd m i)
@[deprecated val_castAdd (since := "2025-11-21")]
theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
@@ -645,15 +637,7 @@ theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i)
theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := rfl
@[simp] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
/-
**Note**
The current pattern inference heuristic includes the implicit term `n + m` as pattern of the pattern,
but arithmetic is problematic in patterns because it is an interpreted symbol. For example,
we will fail to match `@val n (addNat i 0)`. Thus, we mark the implicit subterm with `no_index`
-/
grind_pattern val_addNat => @val (no_index _) (addNat i m)
@[simp, grind =] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
@[deprecated val_addNat (since := "2025-11-21")]
theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl

View File

@@ -66,7 +66,7 @@ lists are prepend-only, this `toListRev` is usually more efficient that `toList`
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toListRev` always terminates after finitely many steps.
-/
@[always_inline, inline, cbv_opaque]
@[always_inline, inline]
def Iter.toListRev {α : Type w} {β : Type w}
[Iterator α Id β] (it : Iter (α := α) β) : List β :=
it.toIterM.toListRev.run

View File

@@ -226,7 +226,7 @@ any element emitted by the iterator {name}`it`.
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
examined in order of iteration.
-/
@[inline, cbv_opaque]
@[inline]
def Iter.any {α β : Type w}
[Iterator α Id β] [IteratorLoop α Id Id]
(p : β Bool) (it : Iter (α := α) β) : Bool :=
@@ -292,7 +292,7 @@ all element emitted by the iterator {name}`it`.
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
examined in order of iteration.
-/
@[inline, cbv_opaque]
@[inline]
def Iter.all {α β : Type w}
[Iterator α Id β] [IteratorLoop α Id Id]
(p : β Bool) (it : Iter (α := α) β) : Bool :=
@@ -644,7 +644,7 @@ Examples:
* `[7, 6].iter.first? = some 7`
* `[].iter.first? = none`
-/
@[inline, cbv_opaque]
@[inline]
def Iter.first? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
(it : Iter (α := α) β) : Option β :=
it.toIterM.first?.run

View File

@@ -110,7 +110,6 @@ theorem Iter.reverse_toListRev_ensureTermination [Iterator α Id β] [Finite α
it.ensureTermination.toListRev.reverse = it.toList := by
simp
@[cbv_eval]
theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id]
{it : Iter (α := α) β} :
it.toListRev = it.toList.reverse := by

View File

@@ -637,7 +637,6 @@ theorem Iter.any_eq_forIn {α β : Type w} [Iterator α Id β]
return .yield false)).run := by
simp [any_eq_anyM, anyM_eq_forIn]
@[cbv_eval ]
theorem Iter.any_toList {α β : Type w} [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
{it : Iter (α := α) β} {p : β Bool} :
@@ -728,7 +727,6 @@ theorem Iter.all_eq_forIn {α β : Type w} [Iterator α Id β]
return .done false)).run := by
simp [all_eq_allM, allM_eq_forIn]
@[cbv_eval ]
theorem Iter.all_toList {α β : Type w} [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
{it : Iter (α := α) β} {p : β Bool} :
@@ -956,7 +954,7 @@ theorem Iter.first?_eq_match_step {α β : Type w} [Iterator α Id β] [Iterator
generalize it.toIterM.step.run.inflate = s
rcases s with _|_|_, _ <;> simp [Iter.first?_eq_first?_toIterM]
@[simp, grind =, cbv_eval ]
@[simp, grind =]
theorem Iter.head?_toList {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
[Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} :
it.toList.head? = it.first? := by

View File

@@ -9,7 +9,7 @@ prelude
public import Init.Data.Order.Ord
public import Init.Data.String.Basic
import Init.Data.Char.Lemmas
import Init.Data.String.Lemmas.StringOrder
import Init.Data.String.Lemmas
public section

View File

@@ -193,7 +193,6 @@ public theorem Array.toSubarray_eq_toSubarray_of_min_eq_min {xs : Array α}
simp [*]; omega
· simp
@[cbv_eval]
public theorem Array.toSubarray_eq_min {xs : Array α} {lo hi : Nat} :
xs.toSubarray lo hi = xs, min lo (min hi xs.size), min hi xs.size, Nat.min_le_right _ _,
Nat.min_le_right _ _ := by

View File

@@ -17,7 +17,6 @@ namespace Std
/--
Appends all the elements in the iterator, in order.
-/
@[inline]
public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
(it : Std.Iter (α := α) β) : String :=
(it.map toString).fold (init := "") (· ++ ·)

View File

@@ -20,4 +20,49 @@ public import Init.Data.String.Lemmas.Intercalate
public import Init.Data.String.Lemmas.Iter
public import Init.Data.String.Lemmas.Hashable
public import Init.Data.String.Lemmas.TakeDrop
public import Init.Data.String.Lemmas.StringOrder
import Init.Data.Order.Lemmas
public import Init.Data.String.Basic
import Init.Data.Char.Lemmas
import Init.Data.Char.Order
import Init.Data.List.Lex
public section
open Std
namespace String
@[deprecated toList_inj (since := "2025-10-30")]
protected theorem data_eq_of_eq {a b : String} (h : a = b) : a.toList = b.toList :=
h rfl
@[deprecated toList_inj (since := "2025-10-30")]
protected theorem ne_of_data_ne {a b : String} (h : a.toList b.toList) : a b := by
simpa [ toList_inj]
@[simp] protected theorem not_le {a b : String} : ¬ a b b < a := Decidable.not_not
@[simp] protected theorem not_lt {a b : String} : ¬ a < b b a := Iff.rfl
@[simp] protected theorem le_refl (a : String) : a a := List.le_refl _
@[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
attribute [local instance] Char.notLTTrans Char.ltTrichotomous Char.ltAsymm
protected theorem le_trans {a b c : String} : a b b c a c := List.le_trans
protected theorem lt_trans {a b c : String} : a < b b < c a < c := List.lt_trans
protected theorem le_total (a b : String) : a b b a := List.le_total _ _
protected theorem le_antisymm {a b : String} : a b b a a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.toList) (bs := b.toList) h₁ h₂)
protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
protected theorem ne_of_lt {a b : String} (h : a < b) : a b := by
have := String.lt_irrefl a
intro h; subst h; contradiction
instance instIsLinearOrder : IsLinearOrder String := by
apply IsLinearOrder.of_le
case le_antisymm => constructor; apply String.le_antisymm
case le_trans => constructor; apply String.le_trans
case le_total => constructor; apply String.le_total
instance : LawfulOrderLT String where
lt_iff a b := by
simp [ String.not_le, Decidable.imp_iff_not_or, Std.Total.total]
end String

View File

@@ -201,10 +201,6 @@ 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
@@ -215,29 +211,6 @@ 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)
@@ -466,10 +439,6 @@ 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
@@ -494,29 +463,6 @@ 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)

View File

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

View File

@@ -11,7 +11,6 @@ import Init.Data.String.OrderInstances
import Init.Data.String.Lemmas.Basic
import Init.Data.Order.Lemmas
import Init.Omega
import Init.ByCases
public section
@@ -71,7 +70,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]
@@ -236,10 +235,6 @@ 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]
@@ -247,10 +242,6 @@ 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' => ?_
@@ -368,21 +359,11 @@ 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]
@@ -425,110 +406,16 @@ 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 :=

View File

@@ -19,7 +19,6 @@ 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
@@ -32,20 +31,19 @@ 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` 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.
{name}`ToForwardSearcher`. 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}`PatternModel.Matches` predicate that implementations of {name}`ForwardPattern`
decidable {name}`ForwardPatternModel.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}`PatternModel.Matches`, and can be specialized to specific patterns
stated in terms of {name}`ForwardPatternModel.Matches`, and can be specialized to specific patterns
from there.
The corresponding compatibility typeclasses are
@@ -61,7 +59,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 PatternModel {ρ : Type} (pat : ρ) : Type where
class ForwardPatternModel {ρ : Type} (pat : ρ) : Type where
/-- The predicate that says which strings match the pattern. -/
Matches : String Prop
not_matches_empty : ¬ Matches ""
@@ -71,72 +69,49 @@ 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 : ρ) [PatternModel pat] {s : Slice} (endPos : s.Pos) : Prop where
matches_copy : PatternModel.Matches pat (s.sliceTo endPos).copy
structure IsMatch (pat : ρ) [ForwardPatternModel pat] {s : Slice} (endPos : s.Pos) : Prop where
matches_copy : ForwardPatternModel.Matches pat (s.sliceTo endPos).copy
theorem IsMatch.ne_startPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
theorem IsMatch.ne_startPos {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos}
(h : IsMatch pat pos) : pos s.startPos := by
intro hc
apply PatternModel.not_matches_empty (pat := pat)
apply ForwardPatternModel.not_matches_empty (pat := pat)
simpa [hc] using h.matches_copy
theorem isMatch_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
IsMatch pat pos PatternModel.Matches pat (s.sliceTo pos).copy :=
theorem isMatch_iff {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} :
IsMatch pat pos ForwardPatternModel.Matches pat (s.sliceTo pos).copy :=
fun h => h, fun h => h
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
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
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}`pos` matches the pattern {name}`pat`, and that there is no longer match starting at the
{name}`endPos` matches that 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.NoPrefixPatternModel`.
{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.Model.NoPrefixForwardPatternModel`.
-/
structure IsLongestMatch (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) where
structure IsLongestMatch (pat : ρ) [ForwardPatternModel pat] {s : Slice} (pos : s.Pos) where
isMatch : IsMatch pat pos
not_isMatch : pos', pos < pos' ¬ IsMatch pat pos'
theorem IsLongestMatch.ne_startPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
theorem IsLongestMatch.ne_startPos {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos}
(h : IsLongestMatch pat pos) : pos s.startPos :=
h.isMatch.ne_startPos
theorem IsLongestMatch.eq {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos}
theorem IsLongestMatch.eq {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
theorem IsMatch.exists_isLongestMatch {pat : ρ} [ForwardPatternModel 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₁
@@ -145,118 +120,61 @@ theorem IsMatch.exists_isLongestMatch {pat : ρ} [PatternModel pat] {s : Slice}
exact ih _ hp₁ hp₂
· exact pos, h₁, fun p' hp₁ hp₂ => h₂ _, hp₁, hp₂
theorem IsLongestMatch.le_of_isMatch {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos}
theorem IsLongestMatch.le_of_isMatch {pat : ρ} [ForwardPatternModel 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 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.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 NoPrefixPatternModel {ρ : Type} (pat : ρ) [PatternModel pat] : Prop where
eq_empty (s t) : PatternModel.Matches pat s PatternModel.Matches pat (s ++ t) t = ""
class NoPrefixForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPatternModel pat] : Prop where
eq_empty (s t) : ForwardPatternModel.Matches pat s ForwardPatternModel.Matches pat (s ++ t) t = ""
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
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
eq_empty s t hs ht := by simpa using h s _ hs ht
theorem isLongestMatch_iff_isMatch {ρ : Type} (pat : ρ) [PatternModel pat] [NoPrefixPatternModel pat]
theorem isLongestMatch_iff_isMatch {ρ : Type} (pat : ρ) [ForwardPatternModel pat] [NoPrefixForwardPatternModel 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₅ (NoPrefixPatternModel.eq_empty _ _ ht₂ (ht₅' ht₂'))
exact ht₅ (NoPrefixForwardPatternModel.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 a match
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 : ρ) [PatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop where
structure IsLongestMatchAt (pat : ρ) [ForwardPatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop where
le : startPos endPos
isLongestMatch_sliceFrom : IsLongestMatch pat (Slice.Pos.sliceFrom _ _ le)
theorem isLongestMatchAt_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos₁ pos₂ : s.Pos} :
theorem isLongestMatchAt_iff {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
theorem IsLongestMatchAt.lt {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] {s : Slice} {startPos endPos endPos' : s.Pos}
theorem IsLongestMatchAt.eq {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] {s t : Slice}
private theorem isLongestMatch_of_eq {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat]
theorem isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPatternModel 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
@@ -269,88 +187,35 @@ theorem isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom {pat : ρ} [PatternMod
exact isLongestMatch_of_eq Slice.sliceFrom_sliceFrom.symm
(by simp [Pos.Raw.ext_iff]; omega) h.isLongestMatch_sliceFrom
theorem IsLongestMatch.isLongestMatchAt_ofSliceFrom {pat : ρ} [PatternModel pat] {s : Slice}
theorem IsLongestMatch.isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] {s : Slice} {endPos : s.Pos} :
theorem isLongestMatchAt_startPos_iff {pat : ρ} [ForwardPatternModel 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 : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) : Prop where
structure MatchesAt (pat : ρ) [ForwardPatternModel pat] {s : Slice} (pos : s.Pos) : Prop where
exists_isLongestMatchAt : endPos, IsLongestMatchAt pat pos endPos
theorem matchesAt_iff_exists_isLongestMatchAt {pat : ρ} [PatternModel pat] {s : Slice}
theorem matchesAt_iff_exists_isLongestMatchAt {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] {s : Slice}
theorem matchesAt_iff_exists_isLongestMatch {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] {s : Slice}
theorem matchesAt_iff_exists_isMatch {pat : ρ} [ForwardPatternModel 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₂ => ?_
@@ -360,13 +225,13 @@ theorem matchesAt_iff_exists_isMatch {pat : ρ} [PatternModel pat] {s : Slice}
by simpa using hq
@[simp]
theorem not_matchesAt_endPos {pat : ρ} [PatternModel pat] {s : Slice} :
theorem not_matchesAt_endPos {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] {s : Slice} {base : s.Pos}
theorem matchesAt_iff_matchesAt_ofSliceFrom {pat : ρ} [ForwardPatternModel 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
@@ -376,66 +241,21 @@ theorem matchesAt_iff_matchesAt_ofSliceFrom {pat : ρ} [PatternModel pat] {s : S
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 : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
theorem IsLongestMatchAt.matchesAt {pat : ρ} [ForwardPatternModel 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 : ρ) [PatternModel pat]
noncomputable def matchAt? {ρ : Type} (pat : ρ) [ForwardPatternModel 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 : ρ} [PatternModel pat]
theorem matchAt?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat]
{s : Slice} {startPos endPos : s.Pos} :
matchAt? pat startPos = some endPos IsLongestMatchAt pat startPos endPos := by
fun_cases matchAt? with
@@ -443,92 +263,40 @@ theorem matchAt?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat]
| case2 => simp_all
@[simp]
theorem matchAt?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat]
theorem matchAt?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPatternModel 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
/--
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`.
Predicate stating compatibility between {name}`ForwardPatternModel` 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}`PatternModel` instance.
supplied by the {name}`ForwardPatternModel` instance.
-/
class LawfulForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPattern pat]
[PatternModel pat] : Prop extends LawfulForwardPattern pat where
[ForwardPatternModel pat] : Prop extends LawfulForwardPattern pat where
skipPrefix?_eq_some_iff (pos) : ForwardPattern.skipPrefix? pat s = some pos IsLongestMatch pat pos
theorem LawfulForwardPatternModel.skipPrefix?_sliceFrom_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
open Classical in
theorem LawfulForwardPatternModel.skipPrefix?_sliceFrom_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel 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] [PatternModel pat]
theorem LawfulForwardPatternModel.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel 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}`LawfulBackwardPattern`, but it is much stronger because it forces the
{name}`BackwardPattern` 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.
@@ -538,7 +306,7 @@ matches.
Hence, this predicate determines the list of search steps up to grouping of rejections.
-/
inductive IsValidSearchFrom (pat : ρ) [PatternModel pat] {s : Slice} :
inductive IsValidSearchFrom (pat : ρ) [ForwardPatternModel pat] {s : Slice} :
s.Pos List (SearchStep s) Prop where
| endPos : IsValidSearchFrom pat s.endPos []
| matched {startPos endPos : s.Pos} :
@@ -548,14 +316,14 @@ inductive IsValidSearchFrom (pat : ρ) [PatternModel 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 : ρ} [PatternModel pat] {s : Slice}
theorem IsValidSearchFrom.matched_of_eq {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] {s : Slice}
theorem IsValidSearchFrom.mismatched_of_eq {pat : ρ} [ForwardPatternModel 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') :
@@ -563,7 +331,7 @@ theorem IsValidSearchFrom.mismatched_of_eq {pat : ρ} [PatternModel pat] {s : Sl
cases h₃
exact IsValidSearchFrom.mismatched h₀ h₂ h₁
theorem IsValidSearchFrom.endPos_of_eq {pat : ρ} [PatternModel pat] {s : Slice}
theorem IsValidSearchFrom.endPos_of_eq {pat : ρ} [ForwardPatternModel pat] {s : Slice}
{p : s.Pos} {l : List (SearchStep s)} (hp : p = s.endPos) (hl : l = []) :
IsValidSearchFrom pat p l := by
cases hp
@@ -571,18 +339,18 @@ theorem IsValidSearchFrom.endPos_of_eq {pat : ρ} [PatternModel pat] {s : Slice}
exact IsValidSearchFrom.endPos
/--
Predicate stating compatibility between {name}`PatternModel` and {name}`ToForwardSearcher`.
Predicate stating compatibility between {name}`ForwardPatternModel` 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 : ρ) [PatternModel pat] {σ : Slice Type}
class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [ForwardPatternModel 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]
[PatternModel pat] [LawfulForwardPatternModel pat] :
[ForwardPatternModel pat] [LawfulForwardPatternModel pat] :
letI : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation
LawfulToForwardSearcherModel pat := by
let inst : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation
@@ -622,97 +390,4 @@ 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

View File

@@ -20,42 +20,28 @@ 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} : PatternModel c where
instance {c : Char} : ForwardPatternModel c where
Matches s := s = String.singleton c
not_matches_empty := by simp
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])
instance {c : Char} : NoPrefixForwardPatternModel c :=
.of_length_eq (by simp +contextual [ForwardPatternModel.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, PatternModel.Matches, copy_sliceTo_eq_iff_exists_splits]
simp only [Model.isMatch_iff, ForwardPatternModel.Matches, sliceTo_copy_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
@@ -66,46 +52,21 @@ 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]
@@ -116,81 +77,37 @@ 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 => ?_
@@ -203,28 +120,11 @@ 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} :

View File

@@ -23,7 +23,7 @@ open Std String.Slice Pattern Pattern.Model
namespace String.Slice
theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice Type}
theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [ForwardPatternModel 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 : ρ) [PatternModel pat
| matched h₁ _ _ => have := h₁.matchesAt; grind
| mismatched => grind
theorem Pattern.Model.find?_eq_none_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice Type}
theorem Pattern.Model.find?_eq_none_iff {ρ : Type} (pat : ρ) [ForwardPatternModel 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 : ρ) [PatternModel pat] {σ : Slice Type}
theorem Pattern.Model.contains_eq_false_iff {ρ : Type} (pat : ρ) [ForwardPatternModel 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 : ρ) [PatternModel pat] {σ : Slice Type}
theorem Pattern.Model.contains_eq_true_iff {ρ : Type} (pat : ρ) [ForwardPatternModel 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 : ρ} [PatternModel pat] {σ : Slice Type}
theorem Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel
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 : ρ} [PatternModel pat] {σ : Slice Type}
theorem Pattern.Model.posFind?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPatternModel 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} :

View File

@@ -19,228 +19,124 @@ 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} : PatternModel p where
instance {p : Char Bool} : ForwardPatternModel p where
Matches s := c, s = singleton c p c
not_matches_empty := by
simp
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])
instance {p : Char Bool} : NoPrefixForwardPatternModel p :=
.of_length_eq (by simp +contextual [ForwardPatternModel.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, PatternModel.Matches, copy_sliceTo_eq_iff_exists_splits]
simp only [Model.isMatch_iff, ForwardPatternModel.Matches, sliceTo_copy_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] : PatternModel p where
Matches := PatternModel.Matches (decide <| p ·)
not_matches_empty := PatternModel.not_matches_empty (pat := (decide <| p ·))
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] : 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 ·))
instance {p : Char Prop} [DecidablePred p] : NoPrefixForwardPatternModel p where
eq_empty := NoPrefixForwardPatternModel.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
@@ -254,55 +150,24 @@ 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

View File

@@ -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.PatternModel` class.
implementation based on the {name}`String.Slice.Pattern.Model.ForwardPatternModel` 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 : ρ) [PatternModel pat] {s : Slice}
public protected noncomputable def split {ρ : Type} (pat : ρ) [ForwardPatternModel 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 : ρ) [PatternModel pa
termination_by curr
@[simp]
public theorem split_endPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice}
public theorem split_endPos {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat]
public theorem split_eq_of_isLongestMatchAt {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel
· 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 : ρ} [PatternModel pat]
public theorem split_eq_of_not_matchesAt {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pa
· obtain rfl : start = stop := Std.le_antisymm h₀ (Std.not_lt.1 h')
simp
public theorem split_eq_next_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pat]
public theorem split_eq_next_of_not_matchesAt {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ)
[PatternModel pat] (l : List (SearchStep s)) (pos pos' : s.Pos) (h₀ : pos pos')
[ForwardPatternModel 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 : ρ) [PatternModel pat]
public theorem toList_splitToSubslice_eq_modelSplit {ρ : Type} (pat : ρ) [ForwardPatternModel 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.PatternModel pat] {σ : Slice Type}
[Model.ForwardPatternModel 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.PatternModel pat] {σ : Slice Type}
[Model.ForwardPatternModel 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.PatternModel pat] {σ : Slice Type}
[Model.ForwardPatternModel 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

View File

@@ -19,12 +19,12 @@ namespace String.Slice.Pattern.Model
namespace ForwardSliceSearcher
instance {pat : Slice} : PatternModel pat where
instance {pat : Slice} : ForwardPatternModel pat where
/-
See the docstring of `PatternModel` for an explanation about why we disallow matching the
See the docstring of `ForwardPatternModel` for an explanation about why we disallow matching the
empty string.
Requiring `s ≠ ""` is a trick that allows us to give a `PatternModel` instance
Requiring `s ≠ ""` is a trick that allows us to give a `ForwardPatternModel` 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,60 +32,34 @@ instance {pat : Slice} : PatternModel pat where
Matches s := s "" s = pat.copy
not_matches_empty := by simp
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])
instance {pat : Slice} : NoPrefixForwardPatternModel pat :=
.of_length_eq (by simp +contextual [ForwardPatternModel.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, PatternModel.Matches, ne_eq, copy_eq_empty_iff,
simp only [Model.isMatch_iff, ForwardPatternModel.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
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]
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'
theorem isLongestMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
IsLongestMatchAt pat pos₁ pos₂
@@ -97,18 +71,6 @@ 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]
@@ -119,29 +81,12 @@ 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]
@@ -154,18 +99,6 @@ 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
@@ -175,25 +108,6 @@ 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),
@@ -232,56 +146,31 @@ end ForwardSliceSearcher
namespace ForwardStringSearcher
instance {pat : String} : PatternModel pat where
instance {pat : String} : ForwardPatternModel pat where
Matches s := s "" s = pat
not_matches_empty := by simp
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])
instance {pat : String} : NoPrefixForwardPatternModel pat :=
.of_length_eq (by simp +contextual [ForwardPatternModel.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, 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]
simp only [Model.isMatch_iff, ForwardPatternModel.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]
@@ -290,31 +179,16 @@ 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₂
@@ -323,14 +197,6 @@ 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₂
@@ -339,14 +205,6 @@ 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
@@ -354,25 +212,12 @@ 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]
@@ -385,14 +230,6 @@ 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),
@@ -402,16 +239,6 @@ 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),
@@ -432,11 +259,6 @@ 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)
@@ -453,21 +275,6 @@ 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

View File

@@ -76,12 +76,10 @@ 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]
@@ -91,116 +89,15 @@ 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} :

View File

@@ -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 : ρ} [PatternModel pat] [ForwardPattern pat]
theorem Pattern.Model.skipPrefix?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] [ForwardPattern pat]
theorem Pattern.Model.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] [ForwardPattern pat]
theorem Pattern.Model.startsWith_eq_false_iff {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [PatternModel pat] [ForwardPattern pat]
theorem Pattern.Model.startsWith_iff {ρ : Type} {pat : ρ} [ForwardPatternModel 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,65 +65,13 @@ 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 : ρ} [PatternModel pat] [ForwardPattern pat]
theorem Pattern.Model.eq_append_of_dropPrefix?_eq_some {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
[LawfulForwardPatternModel pat] {s res : Slice} (h : s.dropPrefix? pat = some res) :
t, PatternModel.Matches pat t s.copy = t ++ res.copy := by
t, ForwardPatternModel.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} :
@@ -135,13 +83,4 @@ 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

View File

@@ -11,8 +11,6 @@ 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
@@ -54,42 +52,7 @@ 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 [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
simpa [ForwardPatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
end Slice
@@ -123,34 +86,4 @@ 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

View File

@@ -11,7 +11,6 @@ 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
@@ -46,7 +45,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 [PatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
obtain _, c, rfl, h₁, h₂ := by simpa [ForwardPatternModel.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} :
@@ -65,59 +64,11 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Slic
s.startsWith P = s.copy.toList.head?.any (decide <| P ·) := by
simp [startsWith_prop_eq_startsWith_decide, startsWith_bool_eq_head?]
theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
theorem eq_append_of_dropPrefix_prop_eq_some {P : Char Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
c, s.copy = singleton c ++ res.copy P c := by
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} :
@@ -162,50 +113,6 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Stri
theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char Prop} [DecidablePred P] {s : String} {res : Slice}
(h : s.dropPrefix? P = some res) : c, s = singleton c ++ res.copy P c := by
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
simpa using Slice.eq_append_of_dropPrefix_prop_eq_some h
end String

View File

@@ -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 [PatternModel.Matches] at this
simp only [ForwardPatternModel.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,87 +104,6 @@ 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) :

View File

@@ -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.copy_sliceTo_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ : String} :
theorem Slice.sliceTo_copy_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,21 +375,13 @@ theorem Slice.copy_sliceTo_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ :
· rintro t₂, h
exact p.splits.eq_left h
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
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
refine ?_, ?_
· rintro rfl
exact _, p.splits
· rintro t₂, 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]
exact p.splits.eq_left h
theorem Pos.Splits.offset_eq_decreaseBy {s : String} {p : s.Pos} (h : p.Splits t₁ t₂) :
p.offset = s.rawEndPos.decreaseBy t₂.utf8ByteSize := by
@@ -435,7 +427,8 @@ 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)]
exact Pos.Splits.next (by simp [h.eq_append])
apply Pos.Splits.next
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
@@ -449,27 +442,6 @@ 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
@@ -484,20 +456,6 @@ 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]

View File

@@ -1,49 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Data.String.Basic
public import Init.Data.Order.Classes
import Init.Data.List.Lex
import Init.Data.Char.Lemmas
import Init.Data.Char.Order
import Init.Data.Order.Factories
import Init.Data.Order.Lemmas
public section
open Std
namespace String
@[simp] protected theorem not_le {a b : String} : ¬ a b b < a := Decidable.not_not
@[simp] protected theorem not_lt {a b : String} : ¬ a < b b a := Iff.rfl
@[simp] protected theorem le_refl (a : String) : a a := List.le_refl _
@[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
attribute [local instance] Char.notLTTrans Char.ltTrichotomous Char.ltAsymm
protected theorem le_trans {a b c : String} : a b b c a c := List.le_trans
protected theorem lt_trans {a b c : String} : a < b b < c a < c := List.lt_trans
protected theorem le_total (a b : String) : a b b a := List.le_total _ _
protected theorem le_antisymm {a b : String} : a b b a a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.toList) (bs := b.toList) h₁ h₂)
protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
protected theorem ne_of_lt {a b : String} (h : a < b) : a b := by
have := String.lt_irrefl a
intro h; subst h; contradiction
instance instIsLinearOrder : IsLinearOrder String := by
apply IsLinearOrder.of_le
case le_antisymm => constructor; apply String.le_antisymm
case le_trans => constructor; apply String.le_trans
case le_total => constructor; apply String.le_total
instance : LawfulOrderLT String where
lt_iff a b := by
simp [ String.not_le, Decidable.imp_iff_not_or, Std.Total.total]
end String

View File

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

View File

@@ -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)) where
toSearcher s := ToBackwardSearcher.toSearcher (· == c) s
instance {c : Char} : ToBackwardSearcher c (ToBackwardSearcher.DefaultBackwardSearcher c) :=
.defaultImplementation
end Char

View File

@@ -139,9 +139,8 @@ 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 (decide <| p ·)) where
toSearcher s := ToBackwardSearcher.toSearcher (decide <| p ·) s
instance {p : Char Prop} [DecidablePred p] : ToBackwardSearcher p (ToBackwardSearcher.DefaultBackwardSearcher p) :=
.defaultImplementation
end Decidable

View File

@@ -706,14 +706,14 @@ Returns {name}`none` otherwise.
This function is generic over all currently supported patterns.
-/
@[inline]
def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
((s.sliceFrom pos).skipSuffix? pat).map Pos.ofSliceFrom
def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
((s.sliceFrom pos).skipPrefix? pat).map Pos.ofSliceFrom
/--
If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
Use {name (scope := "Init.Data.String.Slice")}`String.Slice.dropSuffix` to return the slice
unchanged when {name}`pat` does not match a suffix.
unchanged when {name}`pat` does not match a prefix.
This function is generic over all currently supported patterns.
@@ -775,7 +775,7 @@ def Pos.revSkipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat]
termination_by pos.down
/--
Returns the position at the start of the longest suffix of {name}`s` for which {name}`pat` matches
Returns the position a the start of the longest suffix of {name}`s` for which {name}`pat` matches
(potentially repeatedly).
-/
@[inline]

View File

@@ -314,7 +314,7 @@ Returns {name}`none` otherwise.
This function is generic over all currently supported patterns.
-/
@[inline]
def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
(pos.toSlice.revSkip? pat).map Pos.ofToSlice
/--
@@ -461,7 +461,7 @@ def dropPrefix? (s : String) (pat : ρ) [ForwardPattern pat] : Option String.Sli
If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
Use {name (scope := "Init.Data.String.TakeDrop")}`String.dropSuffix` to return the slice
unchanged when {name}`pat` does not match a suffix.
unchanged when {name}`pat` does not match a prefix.
This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use {name}`String.Slice.copy`.

View File

@@ -30,13 +30,7 @@ simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true
```
using `eq_self`.
-/
@[expose] def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
/--
Gadget for protecting lambda abstractions created by `abstractGroundMismatches?`
from beta reduction during preprocessing. See `ProveEq.lean` for details.
-/
@[expose] def abstractFn {α : Sort u} (a : α) : α := a
def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
/-- Gadget for representing offsets `t+k` in patterns. -/
def offset (a b : Nat) : Nat := a + b

View File

@@ -624,23 +624,6 @@ existing code. It may be removed in a future version of the library.
syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
(" (" &"since" " := " str ")")? : attr
/--
The attribute `@[deprecated_arg old new]` marks a named parameter as deprecated.
When a caller uses the old name with a replacement available, a deprecation warning is emitted
and the argument is silently forwarded to the new parameter. When no replacement is provided,
the parameter is treated as removed and using it produces an error.
* `@[deprecated_arg old new (since := "2026-03-18")]` marks `old` as a deprecated alias for `new`.
* `@[deprecated_arg old new "use foo instead" (since := "2026-03-18")]` adds a custom message.
* `@[deprecated_arg old (since := "2026-03-18")]` marks `old` as a removed parameter (no replacement).
* `@[deprecated_arg old "no longer needed" (since := "2026-03-18")]` removed with a custom message.
A warning is emitted if `(since := "...")` is omitted.
-/
syntax (name := deprecated_arg) "deprecated_arg" ppSpace ident (ppSpace ident)? (ppSpace str)?
(" (" &"since" " := " str ")")? : attr
/--
The attribute `@[suggest_for ..]` on a declaration suggests likely ways in which
someone might **incorrectly** refer to a definition.

View File

@@ -36,6 +36,9 @@ private local instance : ToString Int where
private local instance : Repr Int where
reprPrec i prec := if i < 0 then Repr.addAppParen (toString i) prec else toString i
private local instance : Append String where
append := String.Internal.append
/-- Internal representation of a linear combination of atoms, and a constant term. -/
structure LinearCombo where
/-- Constant term. -/

View File

@@ -185,9 +185,13 @@ example : foo.default = (default, default) :=
abbrev inferInstance {α : Sort u} [i : α] : α := i
set_option checkBinderAnnotations false in
/--
`inferInstanceAs α` synthesizes an instance of type `α` and then adjusts it to conform to the
expected type `β`, which must be inferable from context.
/-- `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:
```
@@ -195,26 +199,7 @@ def D := Nat
instance : Inhabited D := inferInstanceAs (Inhabited Nat)
```
The adjustment will make sure that when the resulting instance will not "leak" the RHS `Nat` when
reduced at transparency levels below `semireducible`, i.e. where `D` would not be unfolded either,
preventing "defeq abuse".
More specifically, given the "source type" (the argument) and "target type" (the expected type),
`inferInstanceAs` synthesizes an instance for the source type and then unfolds and rewraps its
components (fields, nested instances) as necessary to make them compatible with the target type. The
individual steps are represented by the following options, which all default to enabled and can be
disabled to help with porting:
* `backward.inferInstanceAs.wrap`: master switch for instance adjustment in both `inferInstanceAs`
and the default deriving handler
* `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for the target type
for sub-instance fields to avoid non-defeq instance diamonds
* `backward.inferInstanceAs.wrap.instances`: wrap non-reducible instances in auxiliary definitions
* `backward.inferInstanceAs.wrap.data`: wrap data fields in auxiliary definitions (proof fields are
always wrapped)
If you just need to synthesize an instance without transporting between types, use `inferInstance`
instead, potentially with a type annotation for the expected type.
See `Lean.Meta.WrapInstance` for details.
-/
abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i
@@ -3688,7 +3673,7 @@ def panic {α : Sort u} [Inhabited α] (msg : String) : α :=
panicCore msg
-- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
attribute [weak_specialize] Inhabited
attribute [nospecialize] Inhabited
/--
The `>>=` operator is overloaded via instances of `bind`.

View File

@@ -1681,21 +1681,32 @@ tasks.
-/
structure CancelToken where
private ref : IO.Ref Bool
/-- Optional parent token. When set, `isSet` also checks the parent (recursively). -/
parent? : Option CancelToken := none
deriving Nonempty
namespace CancelToken
/-- Creates a new cancellation token. -/
def new : BaseIO CancelToken :=
CancelToken.mk <$> IO.mkRef false
def new : BaseIO CancelToken := do
return { ref := ( IO.mkRef false) }
/-- Activates a cancellation token. Idempotent. -/
/-- Creates a new cancellation token with a parent. The child token is considered set
whenever the parent is set (in addition to being set directly). -/
def newWithParent (parent : CancelToken) : BaseIO CancelToken := do
return { ref := ( IO.mkRef false), parent? := some parent }
/-- Activates a cancellation token. Idempotent. Does not activate the parent. -/
def set (tk : CancelToken) : BaseIO Unit :=
tk.ref.set true
/-- Checks whether the cancellation token has been activated. -/
def isSet (tk : CancelToken) : BaseIO Bool :=
tk.ref.get
/-- Checks whether the cancellation token has been activated, either directly or
via a parent token. -/
partial def isSet (tk : CancelToken) : BaseIO Bool := do
if ( tk.ref.get) then return true
if let some parent := tk.parent? then
return ( parent.isSet)
return false
-- separate definition as otherwise no unboxed version is generated
@[export lean_io_cancel_token_is_set]

View File

@@ -2259,6 +2259,42 @@ 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.

View File

@@ -52,6 +52,20 @@ namespace Lean.Parser.Tactic
syntax (name := tryTrace) "try?" optConfig : tactic
/--
`try? => tac` runs `tac` through `try?`'s suggestion engine (`evalSuggest`) without the
automatic tactic generation phase. This is useful for testing `evalSuggest` directly with
explicit tactic scripts using `try?`'s internal combinators (`attempt_all`, `attempt_all_par`,
`first_par`, etc.).
Example:
```
example : 1 = 1 := by
try? => first | rfl | simp
```
-/
syntax (name := tryTraceWith) "try?" optConfig " => " tacticSeq : tactic
/-- Helper internal tactic for implementing the tactic `try?`. -/
syntax (name := attemptAll) "attempt_all " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic

View File

@@ -186,11 +186,11 @@ def registerTagAttribute (name : Name) (descr : String)
mkInitial := pure {}
addImportedFn := fun _ _ => pure {}
addEntryFn := fun (s : NameSet) n => s.insert n
exportEntriesFnEx := fun env es =>
let all : Array Name := es.foldl (fun a e => a.push e) #[] |>.qsort Name.quickLt
-- Do not export info for private defs at exported/server levels
let exported := all.filter ((env.setExporting true).contains (skipRealize := false))
{ exported, server := exported, «private» := all }
exportEntriesFnEx := fun env es _ =>
let r : Array Name := es.foldl (fun a e => a.push e) #[]
-- Do not export info for private defs
let r := r.filter (env.contains (skipRealize := false))
r.qsort Name.quickLt
statsFn := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
asyncMode := asyncMode
replay? := some fun _ newState newConsts s =>
@@ -266,14 +266,15 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame
mkInitial := pure ([], {})
addImportedFn := fun _ => pure ([], {})
addEntryFn := fun (decls, m) (p : Name × α) => (p.1 :: decls, m.insert p.1 p.2)
exportEntriesFnEx := fun env (decls, m) => Id.run do
let all := if impl.preserveOrder then
exportEntriesFnEx := fun env (decls, m) lvl => Id.run do
let mut r := if impl.preserveOrder then
decls.toArray.reverse.filterMap (fun n => return (n, m.find? n))
else
let r := m.foldl (fun a n p => a.push (n, p)) #[]
r.qsort (fun a b => Name.quickLt a.1 b.1)
let exported := all.filter (fun n, a => impl.filterExport env n a)
{ exported, server := exported, «private» := all }
if lvl != .private then
r := r.filter (fun n, a => impl.filterExport env n a)
r
statsFn := fun (_, m) => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format m.size
}
let attrImpl : AttributeImpl := {
@@ -332,11 +333,11 @@ def registerEnumAttributes (attrDescrs : List (Name × String × α))
mkInitial := pure {}
addImportedFn := fun _ _ => pure {}
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2
exportEntriesFnEx := fun env m =>
let all : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[] |>.qsort (fun a b => Name.quickLt a.1 b.1)
-- Do not export info for private defs at exported/server levels
let exported := all.filter ((env.setExporting true).contains (skipRealize := false) ·.1)
{ exported, server := exported, «private» := all }
exportEntriesFnEx := fun env m _ =>
let r : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[]
-- Do not export info for private defs
let r := r.filter (env.contains (skipRealize := false) ·.1)
r.qsort (fun a b => Name.quickLt a.1 b.1)
statsFn := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
-- We assume (and check in `modifyState`) that, if used asynchronously, enum attributes are set
-- only in the same context in which the tagged declaration was created

View File

@@ -55,6 +55,11 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
entries := entries.push <| ExternEntry.inline backend str
return { entries := entries.toList }
-- Forward declaration
set_option compiler.ignoreBorrowAnnotation true in
@[extern "lean_add_extern"]
opaque addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit
builtin_initialize externAttr : ParametricAttribute ExternAttrData
registerParametricAttribute {
name := `extern
@@ -66,7 +71,7 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
if let some (.thmInfo ..) := env.find? declName then
-- We should not mark theorems as extern
return ()
compileDecls #[declName]
addExtern declName externAttrData
}
def getExternAttrData? (env : Environment) (n : Name) : Option ExternAttrData :=

View File

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
module
prelude
public import Lean.Compiler.IR.AddExtern
public import Lean.Compiler.IR.Basic
public import Lean.Compiler.IR.Format
public import Lean.Compiler.IR.CompilerM

View File

@@ -0,0 +1,86 @@
/-
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Cameron Zwarich
-/
module
prelude
import Init.While
import Lean.Compiler.IR.ToIR
import Lean.Compiler.LCNF.ToImpureType
import Lean.Compiler.LCNF.ToImpure
import Lean.Compiler.LCNF.ExplicitBoxing
import Lean.Compiler.LCNF.Internalize
public import Lean.Compiler.ExternAttr
import Lean.Compiler.LCNF.ExplicitRC
import Lean.Compiler.Options
public section
namespace Lean.IR
set_option compiler.ignoreBorrowAnnotation true in
@[export lean_add_extern]
def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit := do
if !isPrivateName declName then
modifyEnv (Compiler.LCNF.setDeclPublic · declName)
let monoDecl addMono declName
let impureDecls addImpure monoDecl
addIr impureDecls
where
addMono (declName : Name) : CoreM (Compiler.LCNF.Decl .pure) := do
let type Compiler.LCNF.getOtherDeclMonoType declName
let mut typeIter := type
let mut params := #[]
let ignoreBorrow := Compiler.compiler.ignoreBorrowAnnotation.get ( getOptions)
repeat
let .forallE binderName ty b _ := typeIter | break
let borrow := !ignoreBorrow && isMarkedBorrowed ty
params := params.push {
fvarId := ( mkFreshFVarId)
type := ty,
binderName,
borrow
}
typeIter := b
let decl := {
name := declName,
levelParams := [],
value := .extern externAttrData,
inlineAttr? := some .noinline,
type,
params,
}
decl.saveMono
return decl
addImpure (decl : Compiler.LCNF.Decl .pure) : CoreM (Array (Compiler.LCNF.Decl .impure)) := do
let type Compiler.LCNF.lowerResultType decl.type decl.params.size
let params decl.params.mapM fun param =>
return { param with type := Compiler.LCNF.toImpureType param.type }
let decl : Compiler.LCNF.Decl .impure := {
name := decl.name,
levelParams := decl.levelParams,
value := .extern externAttrData
inlineAttr? := some .noinline,
type,
params
}
Compiler.LCNF.CompilerM.run (phase := .impure) do
let decl decl.internalize
decl.saveImpure
let decls Compiler.LCNF.addBoxedVersions #[decl]
let decls Compiler.LCNF.runExplicitRc decls
for decl in decls do
decl.saveImpure
modifyEnv fun env => Compiler.LCNF.recordFinalImpureDecl env decl.name
return decls
addIr (decls : Array (Compiler.LCNF.Decl .impure)) : CoreM Unit := do
let decls toIR decls
logDecls `result decls
addDecls decls
end Lean.IR

View File

@@ -10,7 +10,6 @@ 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
@@ -86,11 +85,11 @@ builtin_initialize declMapExt : SimplePersistentEnvExtension Decl DeclMap ←
addEntryFn := fun s d => s.insert d.name d
-- Store `meta` closure only in `.olean`, turn all other decls into opaque externs.
-- Leave storing the remainder for `meta import` and server `#eval` to `exportIREntries` below.
exportEntriesFnEx? := some fun env s entries =>
exportEntriesFnEx? := some fun env s entries _ =>
let decls := entries.foldl (init := #[]) fun decls decl => decls.push decl
let entries := sortDecls decls
-- Do not save all IR even in .olean.private as it will be in .ir anyway
.uniform <| if env.header.isModule then
if env.header.isModule then
entries.filterMap fun d => do
if isDeclMeta env d.name then
return d
@@ -126,18 +125,12 @@ private def exportIREntries (env : Environment) : Array (Name × Array EnvExtens
-- save all initializers independent of meta/private. Non-meta initializers will only be used when
-- .ir is actually loaded, and private ones iff visible.
let initDecls : Array (Name × Name) :=
(regularInitAttr.ext.exportEntriesFn env (regularInitAttr.ext.getState env)).private
regularInitAttr.ext.exportEntriesFn env (regularInitAttr.ext.getState env) .private
-- 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),
(modPkgExt.name, modPkg)]
(Lean.regularInitAttr.ext.name, initDecls)]
def findEnvDecl (env : Environment) (declName : Name) : Option Decl :=
Compiler.LCNF.findExtEntry? env declMapExt declName findAtSorted? (·.2.find?)

View File

@@ -342,11 +342,6 @@ 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

View File

@@ -232,7 +232,6 @@ partial def checkCases (c : Cases .pure) : CheckM Unit := do
withParams params do check k
partial def check (code : Code .pure) : CheckM Unit := do
checkSystem "LCNF check"
match code with
| .let decl k => checkLetDecl decl; withFVarId decl.fvarId do check k
| .fun decl k =>

View File

@@ -1,104 +0,0 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
module
prelude
public import Lean.Compiler.LCNF.CompilerM
public import Lean.Compiler.LCNF.PassManager
namespace Lean.Compiler.LCNF
/-!
# Coalesce Reference Counting Operations
This pass coalesces multiple `inc`/`dec` operations on the same variable within a basic block.
Within a basic block, it is always safe to:
- Move all increments on a variable to the first `inc` location (summing the counts). Because if
there are later `inc`s no intermediate operation can observe RC=1 (as the value must stay alive
until the later inc) and thus doing all relevant `inc` in the beginning doesn't change
semantics.
- Move all decrements on a variable to the last `dec` location (summing the counts). Because the
value is guaranteed to stay alive until at least the last `dec` anyway so a similar argument to
`inc` holds.
Crucially this pass must be placed after `expandResetReuse` as that one relies on `inc`s still being
present in their original location for optimization purposes.
-/
private structure State where
/-- Total inc count per variable in the current basic block (accumulated going forward). -/
incTotal : Std.HashMap FVarId Nat := {}
/-- Total dec count per variable in the current basic block (accumulated going forward). -/
decTotal : Std.HashMap FVarId Nat := {}
/--
Inc count seen so far per variable going backward. When this equals `incTotal`, we've
reached the first inc and should emit the coalesced operation.
-/
incAccum : Std.HashMap FVarId Nat := {}
/--
Whether we've already emitted the coalesced dec for a variable (going backward, the first
dec encountered is the last in the block).
-/
decPlaced : Std.HashSet FVarId := {}
private abbrev M := StateRefT State CompilerM
/--
Coalesce inc/dec operations within individual basic blocks.
-/
partial def Code.coalesceRC (code : Code .impure) : CompilerM (Code .impure) := do
go code |>.run' {}
where
go (code : Code .impure) : M (Code .impure) := do
match code with
| .inc fvarId n check persistent k _ =>
modify fun s => { s with incTotal := s.incTotal.alter fvarId (fun v? => some ((v?.getD 0) + n)) }
let k go k
modify fun s => { s with incAccum := s.incAccum.alter fvarId (fun v? => some ((v?.getD 0) + n)) }
let s get
if s.incAccum[fvarId]! == s.incTotal[fvarId]! then
return .inc fvarId s.incTotal[fvarId]! check persistent k
else
return k
| .dec fvarId n check persistent k _ =>
modify fun s => { s with decTotal := s.decTotal.alter fvarId (fun v? => some ((v?.getD 0) + n)) }
let k go k
let s get
if !s.decPlaced.contains fvarId then
modify fun s => { s with decPlaced := s.decPlaced.insert fvarId }
return .dec fvarId s.decTotal[fvarId]! check persistent k
else
return k
| .let _ k =>
let k go k
return code.updateCont! k
| .jp decl k =>
let value decl.value.coalesceRC
let decl decl.updateValue value
let k go k
return code.updateFun! decl k
| .cases c =>
let alts c.alts.mapMonoM (·.mapCodeM (·.coalesceRC))
return code.updateAlts! alts
| .del _ k _ =>
let k go k
return code.updateCont! k
| .oset (k := k) .. | .uset (k := k) .. | .sset (k := k) .. | .setTag (k := k) .. =>
let k go k
return code.updateCont! k
| .return .. | .jmp .. | .unreach .. => return code
def Decl.coalesceRC (decl : Decl .impure) : CompilerM (Decl .impure) := do
let value decl.value.mapCodeM Code.coalesceRC
return { decl with value }
public def coalesceRC : Pass :=
.mkPerDeclaration `coalesceRc .impure Decl.coalesceRC
builtin_initialize
registerTraceClass `Compiler.coalesceRc (inherited := true)
end Lean.Compiler.LCNF

View File

@@ -291,9 +291,10 @@ builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (Name ×
registerSimplePersistentEnvExtension {
addImportedFn := fun _ => {}
addEntryFn := fun s e, n => s.insert e n
exportEntriesFnEx? := some fun _ s _ =>
exportEntriesFnEx? := some fun _ s _ => fun
-- preserved for non-modules, make non-persistent at some point?
{ exported := #[], server := #[], «private» := s.toArray.qsort decLt }
| .private => s.toArray.qsort decLt
| _ => #[]
asyncMode := .sync -- compilation is non-parallel anyway
replay? := some <| SimplePersistentEnvExtension.replayOfFilter (!·.contains ·.1) (fun s e, n => s.insert e n)
}

View File

@@ -69,8 +69,8 @@ open ImpureType
abbrev Mask := Array (Option FVarId)
/--
Try to erase `inc` instructions on projections of `targetId` occurring in the tail of `ds`.
Return the updated `ds` and mask containing the `FVarId`s whose `inc` was removed.
Try to erase `inc` instructions on projections of `targetId` occuring in the tail of `ds`.
Return the updated `ds` and mask contianing the `FVarId`s whose `inc` was removed.
-/
partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (CodeDecl .impure)) :
CompilerM (Array (CodeDecl .impure) × Mask) := do

View File

@@ -31,12 +31,9 @@ namespace Lean.Compiler.LCNF
open ImpureType
/-!
The following section contains the derived value analysis. It figures out a dependency graph of
The following section contains the derived value analysis. It figures out a dependency tree of
values that were derived from other values through projections or `Array` accesses. This information
is later used in the derived borrow analysis to reduce reference counting pressure.
When a derived value has more than one parent, it is derived from one of the parent values but we
cannot statically determine which one.
-/
/--
@@ -44,10 +41,10 @@ Contains information about values derived through various forms of projection fr
-/
structure DerivedValInfo where
/--
The set of variables this value may derive from. This is always set except for parameters as they
have no value to be derived from.
The variable this value was derived from. This is always set except for parameters as they have no
value to be derived from.
-/
parents : Array FVarId
parent? : Option FVarId
/--
The set of variables that were derived from this value.
-/
@@ -59,85 +56,59 @@ abbrev DerivedValMap := Std.HashMap FVarId DerivedValInfo
namespace CollectDerivedValInfo
structure State where
/--
The dependency graph of values.
-/
varMap : DerivedValMap := {}
/--
The set of values that are to be interpreted as being borrowed by nature. This currently includes:
- borrowed parameters
- variables that are initialized from constants
-/
borrowedValues : FVarIdHashSet := {}
borrowedParams : FVarIdHashSet := {}
abbrev M := StateRefT State CompilerM
@[inline]
def addDerivedValue (parents : Array FVarId) (child : FVarId) : M Unit := do
def visitParam (p : Param .impure) : M Unit :=
modify fun s => { s with
varMap :=
let varMap := parents.foldl (init := s.varMap)
(·.modify · (fun info => { info with children := info.children.insert child }))
varMap.insert child { parents := parents, children := {} }
varMap := s.varMap.insert p.fvarId {
parent? := none
children := {}
}
borrowedParams :=
if p.borrow && p.type.isPossibleRef then
s.borrowedParams.insert p.fvarId
else
s.borrowedParams
}
@[inline]
def addBorrowedValue (fvarId : FVarId) : M Unit := do
modify fun s => { s with borrowedValues := s.borrowedValues.insert fvarId }
def addDerivedValue (parent : FVarId) (child : FVarId) : M Unit := do
modify fun s => { s with
varMap :=
s.varMap
|>.modify parent (fun info => { info with children := info.children.insert child })
|>.insert child { parent? := some parent, children := {} }
}
def addDerivedLetValue (parents : Array FVarId) (child : FVarId) : M Unit := do
let type getType child
if !type.isPossibleRef then
return ()
let parents parents.filterM fun fvarId => do
let type getType fvarId
return type.isPossibleRef
addDerivedValue parents child
if parents.isEmpty then
addBorrowedValue child
@[inline]
def visitParam (p : Param .impure) : M Unit := do
addDerivedValue #[] p.fvarId
if p.borrow && p.type.isPossibleRef then
addBorrowedValue p.fvarId
def removeFromParents (child : FVarId) : M Unit := do
if let some entry := ( get).varMap.get? child then
for parent in entry.parents do
modify fun s => { s with
varMap := s.varMap.modify parent fun info =>
{ info with children := info.children.erase child }
}
def removeFromParent (child : FVarId) : M Unit := do
if let some parent := ( get).varMap.get? child |>.bind (·.parent?) then
modify fun s => { s with
varMap := s.varMap.modify parent fun info =>
{ info with children := info.children.erase child }
}
partial def collectCode (code : Code .impure) : M Unit := do
match code with
| .let decl k =>
match decl.value with
| .oproj _ parent =>
addDerivedLetValue #[parent] decl.fvarId
addDerivedValue parent decl.fvarId
-- Keep in sync with PropagateBorrow, InferBorrow
| .fap ``Array.getInternal args =>
if let .fvar parent := args[1]! then
addDerivedLetValue #[parent] decl.fvarId
addDerivedValue parent decl.fvarId
| .fap ``Array.get!Internal args =>
let mut parents := #[]
/-
Because execution may continue after a panic, the value resulting from a get!InternalBorrowed
may be derived from either the `Inhabited` instance or the `Array` argument.
-/
if let .fvar parent := args[1]! then
parents := parents.push parent
if let .fvar parent := args[2]! then
parents := parents.push parent
addDerivedLetValue parents decl.fvarId
addDerivedValue parent decl.fvarId
| .fap ``Array.uget args =>
if let .fvar parent := args[1]! then
addDerivedLetValue #[parent] decl.fvarId
| .fap _ #[] =>
addDerivedLetValue #[] decl.fvarId
addDerivedValue parent decl.fvarId
| .reset _ target =>
removeFromParents target
removeFromParent target
| _ => pure ()
collectCode k
| .jp decl k =>
@@ -154,8 +125,8 @@ Collect the derived value tree as well as the set of parameters that take object
-/
def collect (ps : Array (Param .impure)) (code : Code .impure) :
CompilerM (DerivedValMap × FVarIdHashSet) := do
let _, { varMap, borrowedValues } go |>.run {}
return varMap, borrowedValues
let _, { varMap, borrowedParams } go |>.run {}
return varMap, borrowedParams
where
go : M Unit := do
ps.forM visitParam
@@ -199,21 +170,13 @@ def LiveVars.erase (liveVars : LiveVars) (fvarId : FVarId) : LiveVars :=
let borrows := liveVars.borrows.erase fvarId
{ vars, borrows }
@[inline]
def LiveVars.insertBorrow (liveVars : LiveVars) (fvarId : FVarId) : LiveVars :=
{ liveVars with borrows := liveVars.borrows.insert fvarId }
@[inline]
def LiveVars.insertLive (liveVars : LiveVars) (fvarId : FVarId) : LiveVars :=
{ liveVars with vars := liveVars.vars.insert fvarId }
abbrev JPLiveVarMap := FVarIdMap LiveVars
structure Context where
/--
The set of all values that are borrowed and potentially objects
The set of all parameters that are borrowed and take potential objects as arguments.
-/
borrowedValues : FVarIdHashSet
borrowedParams : FVarIdHashSet
/--
The derived value tree.
-/
@@ -272,6 +235,11 @@ 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 =>
@@ -314,21 +282,18 @@ def withCollectLiveVars (x : RcM α) : RcM (α × LiveVars) := do
return (ret, collected)
/--
Traverse the transitive closure of values derived from `fvarId` and add them to `s` if:
- they pass `shouldAdd`.
- all their parents are accessible
Traverse the transitive closure of values derived from `fvarId` and add them to `s` if they pass
`shouldAdd`.
-/
@[specialize]
partial def addDescendants (fvarId : FVarId) (derivedValMap : DerivedValMap) (liveVars : LiveVars)
(shouldAdd : FVarId Bool := fun _ => true) : LiveVars :=
partial def addDescendants (fvarId : FVarId) (derivedValMap : DerivedValMap) (s : FVarIdHashSet)
(shouldAdd : FVarId Bool := fun _ => true) : FVarIdHashSet :=
if let some info := derivedValMap.get? fvarId then
info.children.fold (init := liveVars) fun liveVars child =>
let cinfo := derivedValMap.get! child
let parentsOk := cinfo.parents.all fun fvarId => (liveVars.vars.contains fvarId || liveVars.borrows.contains fvarId)
let liveVars := if parentsOk && shouldAdd child then liveVars.insertBorrow child else liveVars
addDescendants child derivedValMap liveVars shouldAdd
info.children.fold (init := s) fun s child =>
let s := if shouldAdd child then s.insert child else s
addDescendants child derivedValMap s shouldAdd
else
liveVars
s
/--
Mark `fvarId` as live from here on out and if there are any derived values that are not live anymore
@@ -339,21 +304,20 @@ alive after all).
def useVar (fvarId : FVarId) (shouldBorrow : FVarId Bool := fun _ => true) : RcM Unit := do
if !( isLive fvarId) then
let derivedValMap := ( read).derivedValMap
modifyLive fun liveVars => { liveVars with vars := liveVars.vars.insert fvarId }
modifyLive fun liveVars =>
addDescendants fvarId derivedValMap liveVars fun y =>
!liveVars.vars.contains y && shouldBorrow y
{ liveVars with
borrows := addDescendants fvarId derivedValMap liveVars.borrows fun y =>
!liveVars.vars.contains y && shouldBorrow y
vars := liveVars.vars.insert fvarId
}
def useArgs (args : Array (Arg .impure)) : RcM Unit := do
args.forM fun arg =>
match arg with
| .fvar fvarId =>
useVar fvarId fun y =>
/-
If we are in a situation like `f x y` where `x` would imply that `y` remains borrowed we are
going to mark `y` as being live instead of borrowed later on anyways. Instead we skip this
intermediate state and don't even begin to consider it as borrowed.
-/
-- If a value is used as an argument we are going to mark it live anyways so don't mark it
-- as borrowed.
args.all fun arg =>
match arg with
| .fvar z => y != z
@@ -382,9 +346,9 @@ def setRetLiveVars : RcM Unit := do
let derivedValMap := ( read).derivedValMap
-- At the end of a function no values are live and all borrows derived from parameters will still
-- be around.
let liveVars := ( read).borrowedValues.fold (init := {}) fun liveVars x =>
addDescendants x derivedValMap (liveVars.insertBorrow x)
modifyLive (fun _ => liveVars)
let borrows := ( read).borrowedParams.fold (init := {}) fun borrows x =>
addDescendants x derivedValMap (borrows.insert x)
modifyLive fun _ => { vars := {}, borrows }
@[inline]
def addInc (fvarId : FVarId) (k : Code .impure) (n : Nat := 1) : RcM (Code .impure) := do
@@ -666,9 +630,9 @@ partial def Code.explicitRc (code : Code .impure) : RcM (Code .impure) := do
def Decl.explicitRc (decl : Decl .impure) :
CompilerM (Decl .impure) := do
let value decl.value.mapCodeM fun code => do
let derivedValMap, borrowedValues CollectDerivedValInfo.collect decl.params code
let derivedValMap, borrowedParams CollectDerivedValInfo.collect decl.params code
go code |>.run {
borrowedValues,
borrowedParams,
derivedValMap,
} |>.run' {}
return { decl with value }

View File

@@ -375,6 +375,7 @@ where
match v with
| .reset _ x => ownFVar z (.resetReuse z); ownFVar x (.resetReuse z)
| .reuse x _ _ args => ownFVar z (.resetReuse z); ownFVar x (.resetReuse z); ownArgsIfParam z args
| .ctor _ args => ownFVar z (.constructorResult z); ownArgsIfParam z args
| .oproj _ x _ =>
if isOwned x then ownFVar z (.forwardProjectionProp z)
if isOwned z then ownFVar x (.backwardProjectionProp z)
@@ -383,23 +384,15 @@ where
if let .fvar parent := args[1]! then
if isOwned parent then ownFVar z (.forwardProjectionProp z)
| .fap ``Array.get!Internal args =>
if let .fvar parent := args[1]! then
if isOwned parent then ownFVar z (.forwardProjectionProp z)
if let .fvar parent := args[2]! then
if isOwned parent then ownFVar z (.forwardProjectionProp z)
| .fap ``Array.uget args =>
if let .fvar parent := args[1]! then
if isOwned parent then ownFVar z (.forwardProjectionProp z)
| .fap f args =>
-- 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)
| .ctor i args =>
if !i.isScalar then
ownFVar z (.constructorResult z); ownArgsIfParam z args
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

View File

@@ -96,9 +96,9 @@ builtin_initialize postponedCompileDeclsExt : SimplePersistentEnvExtension Postp
asyncMode := .sync
replay? := some <| SimplePersistentEnvExtension.replayOfFilter
(fun s e => !e.declNames.any s.contains) (fun s e => e.declNames.foldl (·.insert · e) s)
exportEntriesFnEx? := some fun _ _ es =>
exportEntriesFnEx? := some fun _ _ es lvl =>
-- `leanir` imports the target module privately
{ exported := #[], server := #[], «private» := es.toArray }
if lvl == .private then es.toArray else #[]
}
def resumeCompilation (declName : Name) : CoreM Unit := do
@@ -188,7 +188,6 @@ where
profileitM Exception profilerName ( getOptions) do
let mut state : (pu : Purity) × Array (Decl pu) := inPhase, decls
for pass in passes do
checkSystem "LCNF compiler"
state withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
let decls withPhase pass.phase do
state.fst.withAssertPurity pass.phase.toPurity fun h => do

View File

@@ -26,7 +26,6 @@ public import Lean.Compiler.LCNF.SimpCase
public import Lean.Compiler.LCNF.InferBorrow
public import Lean.Compiler.LCNF.ExplicitBoxing
public import Lean.Compiler.LCNF.ExplicitRC
public import Lean.Compiler.LCNF.CoalesceRC
public import Lean.Compiler.LCNF.Toposort
public import Lean.Compiler.LCNF.ExpandResetReuse
public import Lean.Compiler.LCNF.SimpleGroundExpr
@@ -150,7 +149,6 @@ def builtinPassManager : PassManager := {
explicitBoxing,
explicitRc,
expandResetReuse,
coalesceRC,
pushProj (occurrence := 1),
detectSimpleGround,
inferVisibility (phase := .impure),

View File

@@ -93,15 +93,16 @@ def mkDeclExt (phase : Phase) (name : Name := by exact decl_name%) :
mkInitial := pure {},
addImportedFn := fun _ => pure {},
addEntryFn := fun s decl => s.insert decl.name decl
exportEntriesFnEx env s := Id.run do
let all := sortedEntries s declLt
let exported := all.filterMap fun decl => do
guard <| isDeclPublic env decl.name
if isDeclTransparent env phase decl.name then
some decl
else
some { decl with value := .extern { entries := [.opaque] } }
return { exported, server := exported, «private» := all }
exportEntriesFnEx env s level := Id.run do
let mut entries := sortedEntries s declLt
if level != .private then
entries := entries.filterMap fun decl => do
guard <| isDeclPublic env decl.name
if isDeclTransparent env phase decl.name then
some decl
else
some { decl with value := .extern { entries := [.opaque] } }
return entries
statsFn := statsFn,
asyncMode := .sync,
replay? := some (replayFn phase)
@@ -137,12 +138,13 @@ def mkSigDeclExt (phase : Phase) (name : Name := by exact decl_name%) :
mkInitial := pure {},
addImportedFn := fun _ => pure {},
addEntryFn := fun s sig => s.insert sig.name sig
exportEntriesFnEx env s := Id.run do
let all := sortedEntries s sigLt
let exported := all.filterMap fun sig => do
guard <| isDeclPublic env sig.name
some sig
return { exported, server := exported, «private» := all }
exportEntriesFnEx env s level := Id.run do
let mut entries := sortedEntries s sigLt
if level != .private then
entries := entries.filterMap fun sig => do
guard <| isDeclPublic env sig.name
some sig
return entries
statsFn := statsFn,
asyncMode := .sync,
replay? := some (replayFn phase)

View File

@@ -114,9 +114,6 @@ where
let parentVal getOwnedness parent
join z parentVal
| .fap ``Array.get!Internal args =>
if let .fvar parent := args[1]! then
let parentVal getOwnedness parent
join z parentVal
if let .fvar parent := args[2]! then
let parentVal getOwnedness parent
join z parentVal
@@ -124,13 +121,7 @@ where
if let .fvar parent := args[1]! then
let parentVal getOwnedness parent
join z parentVal
| .fap _ args =>
let value := if args.isEmpty then .borrow else .own
join z value
| .ctor i _ =>
let value := if i.isScalar then .borrow else .own
join z value
| .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
| .ctor .. | .fap .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
join z .own
| _ => unreachable!

View File

@@ -146,7 +146,7 @@ Similar to the default `Lean.withIncRecDepth`, but include the `inlineStack` in
@[inline] def withIncRecDepth (x : SimpM α) : SimpM α := do
let curr MonadRecDepth.getRecDepth
let max MonadRecDepth.getMaxRecDepth
if max != 0 && curr == max then
if curr == max then
throwMaxRecDepth
else
MonadRecDepth.withRecDepth (curr+1) x

View File

@@ -178,11 +178,10 @@ partial def compileToSimpleGroundExpr (code : Code .impure) : CompilerM (Option
where
go (code : Code .impure) : DetectM SimpleGroundExpr := do
match code with
| .let decl (.return fvarId) | .let decl (.inc _ _ _ true (.return fvarId)) =>
| .let decl (.return fvarId) =>
guard <| decl.fvarId == fvarId
compileFinalLet decl.value
| .let decl k => compileNonFinalLet decl k
| .inc (persistent := true) (k := k) .. => go k
| _ => failure
@[inline]

View File

@@ -20,10 +20,8 @@ inductive SpecParamInfo where
/--
A parameter that is an type class instance (or an arrow that produces a type class instance),
and is fixed in recursive declarations. By default, Lean always specializes this kind of argument.
If the `weak` parameter is set we only specialize for this parameter iff another parameter causes
specialization as well.
-/
| fixedInst (weak : Bool)
| fixedInst
/--
A parameter that is a function and is fixed in recursive declarations. If the user tags a declaration
with `@[specialize]` without specifying which arguments should be specialized, Lean will specialize
@@ -51,15 +49,14 @@ namespace SpecParamInfo
@[inline]
def causesSpecialization : SpecParamInfo Bool
| .fixedInst false | .fixedHO | .user => true
| .fixedInst true | .fixedNeutral | .other => false
| .fixedInst | .fixedHO | .user => true
| .fixedNeutral | .other => false
end SpecParamInfo
instance : ToMessageData SpecParamInfo where
toMessageData
| .fixedInst false => "I"
| .fixedInst true => "W"
| .fixedInst => "I"
| .fixedHO => "H"
| .fixedNeutral => "N"
| .user => "U"
@@ -133,18 +130,6 @@ private def isNoSpecType (env : Environment) (type : Expr) : Bool :=
else
false
/--
Return `true` if `type` is a type tagged with `@[weak_specialize]` or an arrow that produces this kind of type.
-/
private def isWeakSpecType (env : Environment) (type : Expr) : Bool :=
match type with
| .forallE _ _ b _ => isWeakSpecType env b
| _ =>
if let .const declName _ := type.getAppFn then
hasWeakSpecializeAttribute env declName
else
false
/-!
*Note*: `fixedNeutral` must have forward dependencies.
@@ -175,7 +160,7 @@ See comment at `.fixedNeutral`.
private def hasFwdDeps (decl : Decl .pure) (paramsInfo : Array SpecParamInfo) (j : Nat) : Bool := Id.run do
let param := decl.params[j]!
for h : k in (j+1)...decl.params.size do
if paramsInfo[k]!.causesSpecialization || paramsInfo[k]! matches .fixedInst .. then
if paramsInfo[k]!.causesSpecialization then
let param' := decl.params[k]
if param'.type.containsFVar param.fvarId then
return true
@@ -214,7 +199,7 @@ def computeSpecEntries (decls : Array (Decl .pure)) (autoSpecialize : Name → O
else if isTypeFormerType param.type then
pure .fixedNeutral
else if ( isArrowClass? param.type).isSome then
pure (.fixedInst (weak := isWeakSpecType ( getEnv) param.type))
pure .fixedInst
/-
Recall that if `specArgs? == some #[]`, then user annotated function with `@[specialize]`, but did not
specify which arguments must be specialized besides instances. In this case, we try to specialize

View File

@@ -31,8 +31,11 @@ builtin_initialize specCacheExt : SimplePersistentEnvExtension CacheEntry Cache
registerSimplePersistentEnvExtension {
addEntryFn := addEntry
addImportedFn := fun es => (mkStateFromImportedEntries addEntry {} es).switch
exportEntriesFnEx? := some fun _ _ entries =>
{ exported := #[], server := #[], «private» := entries.toArray }
exportEntriesFnEx? := some fun _ _ entries level =>
if level == .private then
entries.toArray
else
#[]
asyncMode := .sync
replay? := some <| SimplePersistentEnvExtension.replayOfFilter
(!·.contains ·.key) addEntry
@@ -206,7 +209,7 @@ def collect (paramsInfo : Array SpecParamInfo) (args : Array (Arg .pure)) :
match paramInfo with
| .other =>
argMask := argMask.push none
| .fixedNeutral | .user | .fixedInst .. | .fixedHO =>
| .fixedNeutral | .user | .fixedInst | .fixedHO =>
argMask := argMask.push (some arg)
Closure.collectArg arg
return argMask
@@ -254,8 +257,7 @@ def shouldSpecialize (specEntry : SpecEntry) (args : Array (Arg .pure)) : Specia
match paramInfo with
| .other => pure ()
| .fixedNeutral => pure () -- If we want to monomorphize types such as `Array`, we need to change here
| .fixedInst true => pure () -- weak: don't trigger specialization on its own
| .fixedInst false | .user => if isGround arg then return true
| .fixedInst | .user => if isGround arg then return true
| .fixedHO => if hoCheck arg then return true
return false
@@ -507,7 +509,7 @@ def updateLocalSpecParamInfo : SpecializeM Unit := do
for entry in infos do
if let some mask := ( get).parentMasks[entry.declName]? then
let maskInfo info :=
mask.zipWith info (f := fun b i => if !b && (i.causesSpecialization || i matches .fixedInst ..) then .other else i)
mask.zipWith info (f := fun b i => if !b && i.causesSpecialization then .other else i)
let entry := { entry with paramsInfo := maskInfo entry.paramsInfo }
modify fun s => {
s with

View File

@@ -39,9 +39,11 @@ private builtin_initialize declMetaExt : SimplePersistentEnvExtension Name NameS
addEntryFn := fun s n => s.insert n
asyncMode := .sync
replay? := some <| SimplePersistentEnvExtension.replayOfFilter (!·.contains ·) (·.insert ·)
exportEntriesFnEx? := some fun env s entries =>
let decls := entries.foldl (init := #[]) fun decls decl => decls.push decl
{ exported := #[], server := #[], «private» := decls.qsort Name.quickLt }
exportEntriesFnEx? := some fun env s entries => fun
| .private =>
let decls := entries.foldl (init := #[]) fun decls decl => decls.push decl
decls.qsort Name.quickLt
| _ => #[]
}
/-- Whether a declaration should be exported for interpretation. -/

View File

@@ -24,17 +24,6 @@ Marks a definition to never be specialized during code generation.
builtin_initialize nospecializeAttr : TagAttribute
registerTagAttribute `nospecialize "mark definition to never be specialized"
/--
Marks a type for weak specialization: Parameters of this type are only specialized when
another argument already triggers specialization. Unlike `@[nospecialize]`, if specialization
happens for other reasons, parameters of this type will participate in the specialization
rather than being ignored.
-/
@[builtin_doc]
builtin_initialize weakSpecializeAttr : TagAttribute
registerTagAttribute `weak_specialize
"mark type for weak specialization: instances are only specialized when another argument already triggers specialization"
private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array Nat) := do
if args.isEmpty then return #[]
let info getConstInfo declName
@@ -93,7 +82,4 @@ def hasSpecializeAttribute (env : Environment) (declName : Name) : Bool :=
def hasNospecializeAttribute (env : Environment) (declName : Name) : Bool :=
nospecializeAttr.hasTag env declName
def hasWeakSpecializeAttribute (env : Environment) (declName : Name) : Bool :=
weakSpecializeAttr.hasTag env declName
end Lean.Compiler

View File

@@ -453,9 +453,6 @@ Throws an internal interrupt exception if cancellation has been requested. The e
caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
level of elaboration. In particular, we want to skip producing further incremental snapshots after
the exception has been thrown.
Like `checkSystem` but without the global heartbeat check, for callers that have their own
heartbeat tracking (e.g. `SynthInstance`).
-/
@[inline] def checkInterrupted : CoreM Unit := do
if let some tk := ( read).cancelTk? then

View File

@@ -60,7 +60,7 @@ instance : EmptyCollection (Trie α) :=
instance : Inhabited (Trie α) where
default := empty
/-- Insert or update the value at the given key `s`. -/
/-- Insert or update the value at a the given key `s`. -/
partial def upsert (t : Trie α) (s : String) (f : Option α α) : Trie α :=
let rec insertEmpty (i : Nat) : Trie α :=
if h : i < s.utf8ByteSize then
@@ -100,7 +100,7 @@ partial def upsert (t : Trie α) (s : String) (f : Option αα) : Trie α :
node (f v) cs ts
loop 0 t
/-- Inserts a value at the given key `s`, overriding an existing value if present. -/
/-- Inserts a value at a the given key `s`, overriding an existing value if present. -/
partial def insert (t : Trie α) (s : String) (val : α) : Trie α :=
upsert t s (fun _ => val)

View File

@@ -18,9 +18,10 @@ namespace Lean
builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) IO.mkRef {}
builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges
mkMapDeclarationExtension (exportEntriesFn := fun _ s =>
let ents := s.toArray
{ exported := #[], server := ents, «private» := ents })
mkMapDeclarationExtension (exportEntriesFn := fun _ s level =>
if level < .server then
#[]
else s.toArray)
def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) : IO Unit :=
builtinDeclRanges.modify (·.insert declName declRanges)

View File

@@ -1,45 +0,0 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Różowski
-/
module
prelude
public import Lean.Compiler.ModPkgExt
public section
namespace Lean
structure DeprecatedModuleEntry where
message? : Option String := none
since? : Option String := none
deriving Inhabited
register_builtin_option linter.deprecated.module : Bool := {
defValue := true
descr := "if true, generate warnings when importing deprecated modules"
}
builtin_initialize deprecatedModuleExt : ModuleEnvExtension <| Option DeprecatedModuleEntry
registerModuleEnvExtension <| pure none
def Environment.getDeprecatedModuleByIdx? (env : Environment) (idx : ModuleIdx) : Option DeprecatedModuleEntry :=
deprecatedModuleExt.getStateByIdx? env idx |>.join
def Environment.setDeprecatedModule (entry : Option DeprecatedModuleEntry) (env : Environment) : Environment :=
deprecatedModuleExt.setState env entry
def formatDeprecatedModuleWarning (env : Environment) (idx : ModuleIdx) (modName : Name)
(entry : DeprecatedModuleEntry) : String :=
let msg := entry.message?.getD ""
let replacements := env.header.moduleData[idx.toNat]!.imports.filter fun imp =>
imp.module != `Init
let lines := replacements.foldl (init := "") fun acc imp =>
acc ++ s!"import {imp.module}\n"
s!"{msg}\n\
'{modName}' has been deprecated: please replace this import by\n\n\
{lines}"
end Lean

View File

@@ -78,21 +78,27 @@ private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mk
builtin_initialize docStringExt : MapDeclarationExtension String
mkMapDeclarationExtension
(asyncMode := .async .asyncEnv)
(exportEntriesFn := fun _ s =>
let ents := s.toArray
{ exported := #[], server := ents, «private» := ents })
(exportEntriesFn := fun _ s level =>
if level < .server then
{}
else
s.toArray)
private builtin_initialize inheritDocStringExt : MapDeclarationExtension Name
mkMapDeclarationExtension (exportEntriesFn := fun _ s =>
let ents := s.toArray
{ exported := #[], server := ents, «private» := ents })
mkMapDeclarationExtension (exportEntriesFn := fun _ s level =>
if level < .server then
{}
else
s.toArray)
private builtin_initialize builtinVersoDocStrings : IO.Ref (NameMap VersoDocString) IO.mkRef {}
builtin_initialize versoDocStringExt : MapDeclarationExtension VersoDocString
mkMapDeclarationExtension
(asyncMode := .async .asyncEnv)
(exportEntriesFn := fun _ s =>
let ents := s.toArray
{ exported := #[], server := ents, «private» := ents })
(exportEntriesFn := fun _ s level =>
if level < .server then
{}
else
s.toArray)
/--
Adds a builtin docstring to the compiler.
@@ -190,9 +196,11 @@ private builtin_initialize moduleDocExt :
SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) registerSimplePersistentEnvExtension {
addImportedFn := fun _ => {}
addEntryFn := fun s e => s.push e
exportEntriesFnEx? := some fun _ _ es =>
let ents := es.toArray
{ exported := #[], server := ents, «private» := ents }
exportEntriesFnEx? := some fun _ _ es level =>
if level < .server then
#[]
else
es.toArray
}
def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
@@ -399,9 +407,11 @@ private builtin_initialize versoModuleDocExt :
SimplePersistentEnvExtension VersoModuleDocs.Snippet VersoModuleDocs registerSimplePersistentEnvExtension {
addImportedFn := fun _ => {}
addEntryFn := fun s e => s.add! e
exportEntriesFnEx? := some fun _ _ es =>
let ents := es.toArray
{ exported := #[], server := ents, «private» := ents }
exportEntriesFnEx? := some fun _ _ es level =>
if level < .server then
#[]
else
es.toArray
}

View File

@@ -39,7 +39,6 @@ public import Lean.Elab.Extra
public import Lean.Elab.GenInjective
public import Lean.Elab.BuiltinTerm
public import Lean.Elab.Arg
public import Lean.Elab.DeprecatedArg
public import Lean.Elab.PatternVar
public import Lean.Elab.ElabRules
public import Lean.Elab.Macro

View File

@@ -11,7 +11,6 @@ public import Lean.Elab.Binders
public import Lean.Elab.RecAppSyntax
public import Lean.IdentifierSuggestion
import all Lean.Elab.ErrorUtils
import Lean.Elab.DeprecatedArg
import Init.Omega
public section
@@ -89,38 +88,6 @@ def synthesizeAppInstMVars (instMVars : Array MVarId) (app : Expr) : TermElabM U
private def findBinderName? (namedArgs : List NamedArg) (binderName : Name) : Option NamedArg :=
namedArgs.find? fun namedArg => namedArg.name == binderName
/--
If the function being applied is a constant, search `namedArgs` for an argument whose name is
a deprecated alias of `binderName`. When `linter.deprecated.arg` is enabled (the default),
returns `some namedArg` after emitting a deprecation warning with a code action hint. When the
option is disabled, returns `none` (the old name falls through to the normal "invalid argument"
error). The returned `namedArg` retains its original (old) name.
-/
private def findDeprecatedBinderName? (namedArgs : List NamedArg) (f : Expr) (binderName : Name) :
TermElabM (Option NamedArg) := do
unless linter.deprecated.arg.get <| getOptions do return .none
unless f.getAppFn.isConst do return none
let declName := f.getAppFn.constName!
let env getEnv
for namedArg in namedArgs do
if let some entry := findDeprecatedArg? env declName namedArg.name then
if entry.newArg? == some binderName then
let msg := formatDeprecatedArgMsg entry
let span? := namedArg.ref[1]
let hint
if span?.getHeadInfo matches .original .. then
MessageData.hint "Rename this argument:" #[{
suggestion := .string entry.newArg?.get!.toString
span?
toCodeActionTitle? := some fun s =>
s!"Rename argument `{entry.oldArg}` to `{s}`"
}]
else
pure .nil
logWarningAt namedArg.ref <| .tagged ``deprecatedArgExt msg ++ hint
return some namedArg
return none
/-- Erase entry for `binderName` from `namedArgs`. -/
def eraseNamedArg (namedArgs : List NamedArg) (binderName : Name) : List NamedArg :=
namedArgs.filter (·.name != binderName)
@@ -271,23 +238,6 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do
else
for namedArg in s.namedArgs do
let f := s.f.getAppFn
if f.isConst then
let env getEnv
if linter.deprecated.arg.get ( getOptions) then
if let some entry := findDeprecatedArg? env f.constName! namedArg.name then
if entry.newArg?.isNone then
let msg := formatDeprecatedArgMsg entry
let hint
if namedArg.ref.getHeadInfo matches .original .. then
MessageData.hint "Delete this argument:" #[{
suggestion := .string ""
span? := namedArg.ref
toCodeActionTitle? := some fun _ =>
s!"Delete deprecated argument `{entry.oldArg}`"
}]
else
pure .nil
throwErrorAt namedArg.ref (msg ++ hint)
let validNames getFoundNamedArgs
let fnName? := if f.isConst then some f.constName! else none
throwInvalidNamedArg namedArg fnName? validNames
@@ -806,16 +756,13 @@ mutual
let binderName := fType.bindingName!
let binfo := fType.bindingInfo!
let s get
let namedArg? match findBinderName? s.namedArgs binderName with
| some namedArg => pure (some namedArg)
| none => findDeprecatedBinderName? s.namedArgs s.f binderName
match namedArg? with
match findBinderName? s.namedArgs binderName with
| some namedArg =>
propagateExpectedType namedArg.val
eraseNamedArg namedArg.name
eraseNamedArg binderName
elabAndAddNewArg binderName namedArg.val
main
| none =>
| none =>
unless binderName.hasMacroScopes do
pushFoundNamedArg binderName
match binfo with

View File

@@ -9,12 +9,10 @@ prelude
public import Lean.Meta.Reduce
public import Lean.Elab.Eval
public import Lean.Elab.Command
import Lean.Elab.DeprecatedSyntax
public import Lean.Elab.Open
import Init.Data.Nat.Order
import Init.Data.Order.Lemmas
import Init.System.Platform
import Lean.DeprecatedModule
public section
@@ -514,15 +512,6 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
modify fun s => { s with maxRecDepth := maxRecDepth.get options }
modifyScope fun scope => { scope with opts := options }
@[builtin_command_elab «unlock_limits»] def elabUnlockLimits : CommandElab := fun _ => do
let opts getOptions
let opts := maxHeartbeats.set opts 0
let opts := maxRecDepth.set opts 0
let opts := synthInstance.maxHeartbeats.set opts 0
modifyScope ({ · with opts })
-- update cached value as well
modify ({ · with maxRecDepth := 0 })
open Lean.Parser.Command.InternalSyntax in
@[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
| `($cmd₁ in%$tk $cmd₂) =>
@@ -717,54 +706,4 @@ where
let env getEnv
IO.eprintln ( env.dbgFormatAsyncState)
/-- Elaborate `deprecated_module`, marking the current module as deprecated. -/
@[builtin_command_elab Parser.Command.deprecated_module]
def elabDeprecatedModule : CommandElab
| `(Parser.Command.deprecated_module| deprecated_module $[$msg?]? $[(since := $since?)]?) => do
let message? := msg?.map TSyntax.getString
let since? := since?.map TSyntax.getString
if (deprecatedModuleExt.getState ( getEnv)).isSome then
logWarning "module is already marked as deprecated"
if since?.isNone then
logWarning "`deprecated_module` should specify the date or library version \
at which the deprecation was introduced, using `(since := \"...\")`"
modifyEnv fun env => env.setDeprecatedModule (some { message?, since? })
| _ => throwUnsupportedSyntax
/-- Elaborate `#show_deprecated_modules`, displaying all deprecated modules. -/
@[builtin_command_elab Parser.Command.showDeprecatedModules]
def elabShowDeprecatedModules : CommandElab := fun _ => do
let env getEnv
let mut parts : Array String := #["Deprecated modules\n"]
for h : idx in [:env.header.moduleNames.size] do
if let some entry := env.getDeprecatedModuleByIdx? idx then
let modName := env.header.moduleNames[idx]
let msg := match entry.message? with
| some str => s!"message '{str}'"
| none => "no message"
let replacements := env.header.moduleData[idx]!.imports.filter fun imp =>
imp.module != `Init
parts := parts.push s!"'{modName}' deprecates to\n{replacements.map (·.module)}\nwith {msg}\n"
-- Also show the current module's deprecation if set.
if let some entry := deprecatedModuleExt.getState env then
let modName := env.mainModule
let msg := match entry.message? with
| some str => s!"message '{str}'"
| none => "no message"
let replacements := env.imports.filter fun imp =>
imp.module != `Init
parts := parts.push s!"'{modName}' deprecates to\n{replacements.map (·.module)}\nwith {msg}\n"
logInfo (String.intercalate "\n" parts.toList)
@[builtin_command_elab Parser.Command.deprecatedSyntax] def elabDeprecatedSyntax : CommandElab := fun stx => do
let id := stx[1]
let kind liftCoreM <| checkSyntaxNodeKindAtNamespaces id.getId ( getCurrNamespace)
let text? := if stx[2].isNone then none else stx[2][0].isStrLit?
let since? := if stx[3].isNone then none else stx[3][3].isStrLit?
if since?.isNone then
logWarning "`deprecated_syntax` should specify the date or library version at which the \
deprecation was introduced, using `(since := \"...\")`"
modifyEnv fun env =>
deprecatedSyntaxExt.addEntry env { kind, text?, since? }
end Lean.Elab.Command

View File

@@ -63,6 +63,6 @@ where
doElabToSyntax "else branch of if with condition {cond}" (elabDiteBranch false) fun else_ => do
let mγ mkMonadicType ( read).doBlockResultType
match h with
| `(_%$tk) => Term.elabTermEnsuringType ( `(if _%$tk : $cond then $then_ else $else_)) mγ
| `(_%$tk) => Term.elabTermEnsuringType ( `(if $(tk):hole : $cond then $then_ else $else_)) mγ
| `($h:ident) => Term.elabTermEnsuringType ( `(if $h:ident : $cond then $then_ else $else_)) mγ
| _ => throwUnsupportedSyntax

View File

@@ -43,7 +43,7 @@ builtin_initialize
Upon such rewrite, the code for adding flat inductives does not diverge much from the usual
way its done for inductive declarations, but we omit applying attributes/modifiers and
we do not set the syntax references to track those declarations (as this is auxiliary piece of
we do not set the syntax references to track those declarations (as this is auxillary piece of
data hidden from the user).
Then, upon adding such flat inductives for each definition in the mutual block to the environment,
@@ -345,7 +345,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
| throwError "expected to be quantifier"
let motiveMVar mkFreshExprMVar type
/-
We intro all the indices and the occurrence of the coinductive predicate
We intro all the indices and the occurence of the coinductive predicate
-/
let (fvars, subgoal) motiveMVar.mvarId!.introN (info.numIndices + 1)
subgoal.withContext do
@@ -373,7 +373,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
-/
let originalCasesOn := mkAppN originalCasesOn indices
/-
The next argument is the occurrence of the coinductive predicate.
The next argument is the occurence of the coinductive predicate.
The original `casesOn` of the flat inductive mentions it in
unrolled form, so we need to rewrite it.
-/
@@ -447,7 +447,7 @@ public def elabCoinductive (coinductiveElabData : Array CoinductiveElabData) : T
let consts := namesAndTypes.map fun (name, _) => (mkConst name levelParams)
/-
We create values of each of PreDefinitions, by taking existential (see `Meta.SumOfProducts`)
form of the associated flat inductives and applying parameters, as well as recursive calls
form of the associated flat inductives and applying paramaters, as well as recursive calls
(with their parameters passed).
-/
let preDefVals forallBoundedTelescope infos[0]!.type originalNumParams fun params _ => do

View File

@@ -10,7 +10,6 @@ public import Lean.Meta.Diagnostics
public import Lean.Elab.Binders
public import Lean.Elab.Command.Scope
public import Lean.Elab.SetOption
import Lean.Elab.DeprecatedSyntax
public meta import Lean.Parser.Command
public section
@@ -469,7 +468,6 @@ where go := do
else withTraceNode `Elab.command (fun _ => return stx) (tag :=
-- special case: show actual declaration kind for `declaration` commands
(if stx.isOfKind ``Parser.Command.declaration then stx[1] else stx).getKind.toString) do
checkDeprecatedSyntax stx ( read).macroStack
let s get
match ( liftMacroM <| expandMacroImpl? s.env stx) with
| some (decl, stxNew?) =>

View File

@@ -1,97 +0,0 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Różowski
-/
module
prelude
public import Lean.EnvExtension
public import Lean.Message
import Lean.Elab.Term
public section
namespace Lean.Elab
open Meta
register_builtin_option linter.deprecated.arg : Bool := {
defValue := true
descr := "if true, generate deprecation warnings and errors for deprecated parameters"
}
/-- Entry mapping an old parameter name to a new (or no) parameter for a given declaration. -/
structure DeprecatedArgEntry where
declName : Name
oldArg : Name
newArg? : Option Name := none
text? : Option String := none
since? : Option String := none
deriving Inhabited
/-- State: `declName → (oldArg → entry)` -/
abbrev DeprecatedArgState := NameMap (NameMap DeprecatedArgEntry)
private def addDeprecatedArgEntry (s : DeprecatedArgState) (e : DeprecatedArgEntry) : DeprecatedArgState :=
let inner := (s.find? e.declName).getD {} |>.insert e.oldArg e
s.insert e.declName inner
builtin_initialize deprecatedArgExt :
SimplePersistentEnvExtension DeprecatedArgEntry DeprecatedArgState
registerSimplePersistentEnvExtension {
addEntryFn := addDeprecatedArgEntry
addImportedFn := mkStateFromImportedEntries addDeprecatedArgEntry {}
}
/-- Look up a deprecated argument mapping for `(declName, argName)`. -/
def findDeprecatedArg? (env : Environment) (declName : Name) (argName : Name) :
Option DeprecatedArgEntry :=
(deprecatedArgExt.getState env |>.find? declName) >>= (·.find? argName)
/-- Format the deprecation warning message for a deprecated argument. -/
def formatDeprecatedArgMsg (entry : DeprecatedArgEntry) : MessageData :=
let base := match entry.newArg? with
| some newArg =>
m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated, \
use `{newArg}` instead"
| none =>
m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated"
match entry.text? with
| some text => base ++ m!": {text}"
| none => base
builtin_initialize registerBuiltinAttribute {
name := `deprecated_arg
descr := "mark a parameter as deprecated"
add := fun declName stx _kind => do
let `(attr| deprecated_arg $oldId $[$newId?]? $[$text?]? $[(since := $since?)]?) := stx
| throwError "Invalid `[deprecated_arg]` attribute syntax"
let oldArg := oldId.getId
let newArg? := newId?.map TSyntax.getId
let text? := text?.map TSyntax.getString |>.filter (!·.isEmpty)
let since? := since?.map TSyntax.getString
let info getConstInfo declName
let paramNames MetaM.run' do
forallTelescopeReducing info.type fun xs _ =>
xs.mapM fun x => return ( x.fvarId!.getDecl).userName
if let some newArg := newArg? then
-- We have a replacement provided
unless Array.any paramNames (· == newArg) do
throwError "`{newArg}` is not a parameter of `{declName}`"
if Array.any paramNames (· == oldArg) then
throwError "`{oldArg}` is still a parameter of `{declName}`; \
rename it to `{newArg}` before adding `@[deprecated_arg]`"
else
-- We do not have a replacement provided
if Array.any paramNames (· == oldArg) then
throwError "`{oldArg}` is still a parameter of `{declName}`; \
remove it before adding `@[deprecated_arg]`"
if since?.isNone then
logWarning "`[deprecated_arg]` attribute should specify the date or library version \
at which the deprecation was introduced, using `(since := \"...\")`"
modifyEnv fun env => deprecatedArgExt.addEntry env {
declName, oldArg, newArg?, text?, since?
}
}
end Lean.Elab

View File

@@ -1,71 +0,0 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Różowski
-/
module
prelude
public import Lean.MonadEnv
public import Lean.Linter.Basic
public import Lean.Elab.Util
public section
namespace Lean.Linter
register_builtin_option linter.deprecated.syntax : Bool := {
defValue := true
descr := "if true, generate warnings when deprecated syntax is used"
}
end Lean.Linter
namespace Lean.Elab
/-- Entry recording that a syntax kind has been deprecated. -/
structure SyntaxDeprecationEntry where
/-- The syntax node kind that is deprecated. -/
kind : SyntaxNodeKind
/-- Optional deprecation message. -/
text? : Option String := none
/-- Optional version or date at which the syntax was deprecated. -/
since? : Option String := none
builtin_initialize deprecatedSyntaxExt :
SimplePersistentEnvExtension SyntaxDeprecationEntry (NameMap SyntaxDeprecationEntry)
registerSimplePersistentEnvExtension {
addImportedFn := mkStateFromImportedEntries (fun m e => m.insert e.kind e) {}
addEntryFn := fun m e => m.insert e.kind e
}
/--
Check whether `stx` is a deprecated syntax kind, and if so, emit a warning.
If `macroStack` is non-empty, the warning is attributed to the macro call site rather than the
syntax itself.
-/
def checkDeprecatedSyntax [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m]
[AddMessageContext m] [MonadRef m] (stx : Syntax) (macroStack : MacroStack) : m Unit := do
let env getEnv
let kind := stx.getKind
if let some entry := (deprecatedSyntaxExt.getState env).find? kind then
let extraMsg := match entry.text? with
| some text => m!": {text}"
| none => m!""
match macroStack with
| { before := macroStx, .. } :: { before := callerStx, .. } :: _ =>
let expandedFrom :=
if callerStx.getKind != macroStx.getKind then
m!" (expanded from '{callerStx.getKind}')"
else m!""
Linter.logLintIf Linter.linter.deprecated.syntax macroStx
m!"macro '{macroStx.getKind}'{expandedFrom} produces deprecated syntax '{kind}'{extraMsg}"
| { before := macroStx, .. } :: [] =>
Linter.logLintIf Linter.linter.deprecated.syntax macroStx
m!"macro '{macroStx.getKind}' produces deprecated syntax '{kind}'{extraMsg}"
| [] =>
Linter.logLintIf Linter.linter.deprecated.syntax stx
m!"syntax '{kind}' has been deprecated{extraMsg}"
end Lean.Elab

View File

@@ -85,10 +85,6 @@ structure State where
-/
lctx : LocalContext
/--
The local instances.
The `MonadLift TermElabM DocM` instance runs the lifted action with these instances, so elaboration
commands that mutate this state cause it to take effect in subsequent commands.
-/
localInstances : LocalInstances
/--

View File

@@ -9,7 +9,6 @@ prelude
public import Lean.Parser.Module
meta import Lean.Parser.Module
import Lean.Compiler.ModPkgExt
public import Lean.DeprecatedModule
public section
@@ -43,66 +42,12 @@ def HeaderSyntax.toModuleHeader (stx : HeaderSyntax) : ModuleHeader where
abbrev headerToImports := @HeaderSyntax.imports
/--
Check imported modules for deprecation and emit warnings.
The `-- deprecated_module: ignore` comment can be placed on the `module` keyword to suppress
all warnings, or on individual `import` statements to suppress specific ones.
This follows the same pattern as `-- shake: keep` in Lake shake.
The `headerStx?` parameter carries the header syntax used for checking trailing comments.
When called from the Language Server, the main header syntax may have its trailing trivia
stripped by `unsetTrailing` for caching purposes, so `origHeaderStx?` can supply the original
(untrimmed) syntax to preserve `-- deprecated_module: ignore` annotations on the last import.
-/
def checkDeprecatedImports
(env : Environment) (imports : Array Import) (opts : Options)
(inputCtx : Parser.InputContext) (startPos : String.Pos.Raw) (messages : MessageLog)
(headerStx? : Option HeaderSyntax := none)
(origHeaderStx? : Option HeaderSyntax := none)
: MessageLog := Id.run do
let mut opts := opts
let mut ignoreDeprecatedImports : NameSet := {}
if let some headerStx := origHeaderStx? <|> headerStx? then
match headerStx with
| `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$_]? $importsStx*) =>
if moduleTk.any (·.getTrailing?.any (·.toString.contains "deprecated_module: ignore")) then
opts := linter.deprecated.module.set opts false
for impStx in importsStx do
if impStx.raw.getTrailing?.any (·.toString.contains "deprecated_module: ignore") then
match impStx with
| `(Parser.Module.import| $[public%$_]? $[meta%$_]? import $[all%$_]? $n) =>
ignoreDeprecatedImports := ignoreDeprecatedImports.insert n.getId
| _ => pure ()
| _ => pure ()
if !linter.deprecated.module.get opts then
return messages
imports.foldl (init := messages) fun messages imp =>
if ignoreDeprecatedImports.contains imp.module then
messages
else
match env.getModuleIdx? imp.module with
| some idx =>
match env.getDeprecatedModuleByIdx? idx with
| some entry =>
let pos := inputCtx.fileMap.toPosition startPos
messages.add {
fileName := inputCtx.fileName
pos := pos
severity := .warning
data := .tagged ``deprecatedModuleExt <| formatDeprecatedModuleWarning env idx imp.module entry
}
| none => messages
| none => messages
def processHeaderCore
(startPos : String.Pos.Raw) (imports : Array Import) (isModule : Bool)
(opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
(trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv := false)
(mainModule := Name.anonymous) (package? : Option PkgId := none)
(arts : NameMap ImportArtifacts := {})
(headerStx? : Option HeaderSyntax := none)
(origHeaderStx? : Option HeaderSyntax := none)
: IO (Environment × MessageLog) := do
let level := if isModule then
if Elab.inServer.get opts then
@@ -121,7 +66,6 @@ def processHeaderCore
let pos := inputCtx.fileMap.toPosition startPos
pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
let env := env.setMainModule mainModule |>.setModulePackage package?
let messages := checkDeprecatedImports env imports opts inputCtx startPos messages headerStx? origHeaderStx?
return (env, messages)
/--
@@ -138,7 +82,6 @@ backwards compatibility measure not compatible with the module system.
: IO (Environment × MessageLog) := do
processHeaderCore header.startPos header.imports header.isModule
opts messages inputCtx trustLevel plugins leakEnv mainModule
(headerStx? := header)
def parseImports (input : String) (fileName : Option String := none) : IO (Array Import × Position × MessageLog) := do
let fileName := fileName.getD "<input>"

View File

@@ -26,11 +26,9 @@ public structure EqnInfo where
deriving Inhabited
public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo
mkMapDeclarationExtension (exportEntriesFn := fun env s =>
let all := s.toArray
-- Do not export for non-exposed defs at exported/server levels
let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
{ exported, server := exported, «private» := all })
mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
-- Do not export for non-exposed defs
s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name)
(fixedParamPerms : FixedParamPerms) (fixpointType : Array PartialFixpointType): MetaM Unit := do

View File

@@ -148,11 +148,9 @@ where
throwError "no progress at goal\n{MessageData.ofGoal mvarId}"
public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo
mkMapDeclarationExtension (exportEntriesFn := fun env s =>
let all := s.toArray
-- Do not export for non-exposed defs at exported/server levels
let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
{ exported, server := exported, «private» := all })
mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
-- Do not export for non-exposed defs
s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat)
(fixedParamPerms : FixedParamPerms) : CoreM Unit := do

View File

@@ -24,11 +24,9 @@ public structure EqnInfo where
deriving Inhabited
public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo
mkMapDeclarationExtension (exportEntriesFn := fun env s =>
let all := s.toArray
-- Do not export for non-exposed defs at exported/server levels
let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
{ exported, server := exported, «private» := all })
mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
-- Do not export for non-exposed defs
s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms)
(argsPacker : ArgsPacker) : MetaM Unit := do

View File

@@ -73,9 +73,8 @@ def splitMatchOrCasesOn (mvarId : MVarId) (e : Expr) (matcherInfo : MatcherInfo)
if ( isMatcherApp e) then
Split.splitMatch mvarId e
else
-- For casesOn, the last discriminant is the major premise;
-- `cases` will handle any index discriminants automatically.
let discr := e.getAppArgs[matcherInfo.numParams + matcherInfo.numDiscrs]!
assert! matcherInfo.numDiscrs = 1
let discr := e.getAppArgs[matcherInfo.numParams + 1]!
assert! discr.isFVar
let subgoals mvarId.cases discr.fvarId!
return subgoals.map (·.mvarId) |>.toList

View File

@@ -243,6 +243,10 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
@[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
| `(#print%$tk axioms $id) => withRef tk do
if ( getEnv).header.isModule then
throwError "cannot use `#print axioms` in a `module`; consider temporarily removing the \
`module` header or placing the command in a separate file"
let cs liftCoreM <| realizeGlobalConstWithInfos id
cs.forM printAxiomsOf
| _ => throwUnsupportedSyntax

View File

@@ -7,7 +7,6 @@ module
prelude
public import Lean.Elab.Quotation.Util
import Lean.Elab.DeprecatedSyntax
public section
@@ -57,14 +56,6 @@ unsafe builtin_initialize precheckAttribute : KeyedDeclsAttribute Precheck ←
}
partial def precheck : Precheck := fun stx => do
-- Check for deprecated syntax kinds in quotations
if let some entry := (deprecatedSyntaxExt.getState ( getEnv)).find? stx.getKind then
let extraMsg := match entry.text? with
| some text => m!": {text}"
| none => m!""
withRef stx do
Linter.logLintIf Linter.linter.deprecated.syntax stx
m!"quotation uses deprecated syntax '{stx.getKind}'{extraMsg}"
if let p::_ := precheckAttribute.getValues ( getEnv) stx.getKind then
if catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; pure true) (fun _ => pure false) then
return

View File

@@ -31,7 +31,7 @@ open Lean.Parser.Command
def allRecommendedSpellings : MetaM (Array RecommendedSpelling) := do
let all := recommendedSpellingExt.toEnvExtension.getState ( getEnv)
|>.importedEntries
|>.push ((recommendedSpellingExt.exportEntriesFn ( getEnv) (recommendedSpellingExt.getState ( getEnv))).exported)
|>.push (recommendedSpellingExt.exportEntriesFn ( getEnv) (recommendedSpellingExt.getState ( getEnv)) .exported)
return all.flatMap id
end Lean.Elab.Term.Doc

View File

@@ -582,7 +582,6 @@ mutual
-- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created.
-- It would not be incorrect to use `filterM`.
let remainingPendingMVars pendingMVars.filterRevM fun mvarId => do
checkSystem "synthesize pending MVars"
-- We use `traceM` because we want to make sure the metavar local context is used to trace the message
traceM `Elab.postpone (mvarId.withContext do addMessageContext m!"resuming {mkMVar mvarId}")
let succeeded synthesizeSyntheticMVar mvarId postponeOnError runTactics

View File

@@ -8,7 +8,6 @@ module
prelude
public import Lean.Meta.Tactic.Util
public import Lean.Elab.Term
import Lean.Elab.DeprecatedSyntax
import Init.Omega
public section
@@ -193,7 +192,6 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do
Term.withoutTacticIncrementality true <| withTacticInfoContext stx do
stx.getArgs.forM evalTactic
else withTraceNode `Elab.step (fun _ => return stx) (tag := stx.getKind.toString) do
checkDeprecatedSyntax stx ( readThe Term.Context).macroStack
let evalFns := tacticElabAttribute.getEntries ( getEnv) stx.getKind
let macros := macroAttribute.getEntries ( getEnv) stx.getKind
if evalFns.isEmpty && macros.isEmpty then

View File

@@ -256,15 +256,36 @@ Marks a type as an invariant type for the `mvcgen` tactic.
Goals whose type is an application of a tagged type will be classified
as invariants rather than verification conditions.
-/
builtin_initialize specInvariantAttr : TagAttribute
registerTagAttribute `spec_invariant_type
builtin_initialize mvcgenInvariantAttr : TagAttribute
registerTagAttribute `mvcgen_invariant_type
"marks a type as an invariant type for the `mvcgen` tactic"
/--
Returns `true` if `ty` is an application of a type tagged with `@[spec_invariant_type]`.
Returns `true` if `ty` is an application of a type tagged with `@[mvcgen_invariant_type]`.
-/
def isSpecInvariantType (env : Environment) (ty : Expr) : Bool :=
def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool :=
if let .const name .. := ty.getAppFn then
specInvariantAttr.hasTag env name
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

View File

@@ -75,7 +75,7 @@ def elabSpec (stx? : Option (TSyntax `term)) (wp : Expr) : TacticM SpecTheorem :
| none => findSpec ( getSpecTheorems) wp
| some stx => elabTermIntoSpecTheorem stx expectedTy
variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] [MonadEnv n]
variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n]
private def mkProj' (n : Name) (i : Nat) (Q : Expr) : MetaM Expr := do
return ( projectCore? Q i).getD (mkProj n i Q)
@@ -181,12 +181,11 @@ public def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag
-- Instantiation creates `.natural` MVars, which possibly get instantiated by the def eq checks
-- below when they occur in `P` or `Q`.
-- That's good for many such as MVars ("schematic variables"), but problematic for MVars
-- corresponding to invariant types, which should end up as user goals.
-- To prevent accidental instantiation, we mark all invariant MVars as synthetic opaque.
let env getEnv
-- corresponding to `Invariant`s, which should end up as user goals.
-- To prevent accidental instantiation, we mark all `Invariant` MVars as synthetic opaque.
for mvar in mvars do
let ty mvar.mvarId!.getType
if isSpecInvariantType env ty then mvar.mvarId!.setKind .syntheticOpaque
if ty.isAppOf ``Invariant then mvar.mvarId!.setKind .syntheticOpaque
-- Apply the spec to the excess arguments of the `wp⟦e⟧ Q` application
let T := goal.target.consumeMData

View File

@@ -35,6 +35,7 @@ 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
@@ -45,10 +46,13 @@ 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, vcs := state.vcs }
return { invariants := state.invariants, witnesses := state.witnesses, vcs := state.vcs }
where
onFail (goal : MGoal) (name : Name) : VCGenM Expr := do
-- trace[Elab.Tactic.Do.vcgen] "fail {goal.toExpr}"
@@ -352,60 +356,77 @@ 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
| `(invariantDotAlt| · $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
| `(invariantCaseAlt| | $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 `invariantDotAlt`, got {alt}"
if let `(invariantsKW| invariants) := invariantsKW then
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}"
elabGoalSection invariants alts "inv" "invariant"
else
-- Otherwise, we have `invariants?`. Suggest missing invariants.
-- 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)
let mut suggestions := #[]
for i in 0...invariants.size do
let mv := invariants[i]!
if mv.isAssigned then
continue
let invariant suggestInvariant mv
suggestions := suggestions.push ( `(invariantDotAlt| · $invariant))
suggestions := suggestions.push ( `(goalDotAlt| · $invariant))
let alts' := alts ++ suggestions
let stx' `(invariantAlts|invariants $alts'*)
if suggestions.size > 0 then
@@ -457,8 +478,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, vcs } VCGen.genVCs goal ctx fuel
trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
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 runOnVCs (tac : TSyntax `tactic) (extraMsg : MessageData) (vcs : Array MVarId) : TermElabM (Array MVarId) :=
vcs.flatMapM fun vc =>
tryCatchRuntimeEx
@@ -467,10 +488,13 @@ 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 elabInvariants {← (invariants ++ vcs).mapM fun m => m.getTag}"
elabInvariants stx[3] invariants (suggestInvariant vcs)
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)
let invariants invariants.filterM (not <$> ·.isAssigned)
trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ witnesses ++ 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
@@ -478,17 +502,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 ++ 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] "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] "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 #[ `(invariantAlts| invariants?)]) |>.push mkNullNode)
|>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push mkNullNode |>.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'

Some files were not shown because too many files have changed in this diff Show More