Compare commits

..

7 Commits

Author SHA1 Message Date
Kim Morrison
302dc94544 fix tests 2025-11-13 08:14:14 +11:00
Kim Morrison
788b82cfe6 fix 2025-11-12 06:18:46 +01:00
Kim Morrison
535cdc1e6a comment 2025-11-12 06:13:05 +01:00
Kim Morrison
f2a95f6655 looks good 2025-11-12 06:13:05 +01:00
Kim Morrison
a214d8c432 capture try: this 2025-11-12 06:13:05 +01:00
Kim Morrison
e3ebd747b7 checkpoint 2025-11-12 06:13:05 +01:00
Kim Morrison
27b0a0f1cc checkpoint 2025-11-12 06:13:03 +01:00
2483 changed files with 9694 additions and 36061 deletions

View File

@@ -1,34 +1,14 @@
To build Lean you should use `make -j -C build/release`.
To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
## New features
When asked to implement new features:
* begin by reviewing existing relevant code and tests
* write comprehensive tests first (expecting that these will initially fail)
* and then iterate on the implementation until the tests pass.
All new tests should go in `tests/lean/run/`. These tests don't have expected output; we just check there are no errors. You should use `#guard_msgs` to check for specific messages.
To build Lean you should use `make -j$(nproc) -C build/release`.
## Success Criteria
To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.
*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass. You have to keep working until you have verified both of these.
## Build System Safety
All new tests should go in `tests/lean/run/`. Note that these tests don't have expected output, and just run on a success or failure basis. So you should use `#guard_msgs` to check for specific messages.
**NEVER manually delete build directories** (build/, stage0/, stage1/, etc.) even when builds fail.
- ONLY use the project's documented build command: `make -j -C build/release`
- If a build is broken, ask the user before attempting any manual cleanup
## LSP and IDE Diagnostics
After rebuilding, LSP diagnostics may be stale until the user interacts with files. Trust command-line test results over IDE diagnostics.
## Update prompting when the user is frustrated
If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
## Creating pull requests.
All PRs must have a first paragraph starting with "This PR". This paragraph is automatically incorporated into release notes. Read `lean4/doc/dev/commit_convention.md` when making PRs.
If you are not following best practices specific to this repository and the user expresses frustration, stop and ask them to help update this `.claude/CLAUDE.md` file with the missing guidance.

View File

@@ -106,54 +106,9 @@ jobs:
TAG_NAME="${GITHUB_REF##*/}"
echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
- name: Validate CMakeLists.txt version matches tag
if: steps.set-release.outputs.RELEASE_TAG != ''
run: |
echo "Validating CMakeLists.txt version matches tag ${{ steps.set-release.outputs.RELEASE_TAG }}"
# Extract version values from CMakeLists.txt
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 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+')
# Expected values from tag parsing
TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"
TAG_MINOR="${{ steps.set-release.outputs.LEAN_VERSION_MINOR }}"
TAG_PATCH="${{ steps.set-release.outputs.LEAN_VERSION_PATCH }}"
ERRORS=""
if [[ "$CMAKE_MAJOR" != "$TAG_MAJOR" ]]; then
ERRORS+="LEAN_VERSION_MAJOR: expected $TAG_MAJOR, found $CMAKE_MAJOR\n"
fi
if [[ "$CMAKE_MINOR" != "$TAG_MINOR" ]]; then
ERRORS+="LEAN_VERSION_MINOR: expected $TAG_MINOR, found $CMAKE_MINOR\n"
fi
if [[ "$CMAKE_PATCH" != "$TAG_PATCH" ]]; then
ERRORS+="LEAN_VERSION_PATCH: expected $TAG_PATCH, found $CMAKE_PATCH\n"
fi
if [[ "$CMAKE_IS_RELEASE" != "1" ]]; then
ERRORS+="LEAN_VERSION_IS_RELEASE: expected 1, found $CMAKE_IS_RELEASE\n"
fi
if [[ -n "$ERRORS" ]]; then
echo "::error::Version mismatch between tag and src/CMakeLists.txt"
echo ""
echo "Tag ${{ steps.set-release.outputs.RELEASE_TAG }} expects version $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
echo "But src/CMakeLists.txt has mismatched values:"
echo -e "$ERRORS"
echo ""
echo "Fix src/CMakeLists.txt, delete the tag, and re-tag."
exit 1
fi
echo "Version validation passed: $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
# 0: PRs without special label
# 1: PRs with `merge-ci` label, merge queue checks, master commits
# 2: nightlies
# 3: PRs with `release-ci` label, full releases
# 2: PRs with `release-ci` label, releases (incl. nightlies)
- name: Set check level
id: set-level
# We do not use github.event.pull_request.labels.*.name here because
@@ -163,16 +118,14 @@ jobs:
check_level=0
fast=false
if [[ -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
check_level=3
elif [[ -n "${{ steps.set-nightly.outputs.nightly }}" ]]; then
if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
check_level=2
elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
check_level=1
else
labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')"
if echo "$labels" | grep -q "release-ci"; then
check_level=3
check_level=2
elif echo "$labels" | grep -q "merge-ci"; then
check_level=1
fi
@@ -257,22 +210,17 @@ jobs:
"test": true,
"CMAKE_PRESET": "reldebug",
},
{
// TODO: suddenly started failing in CI
/*{
"name": "Linux fsanitize",
// Always run on large if available, more reliable regarding timeouts
"os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
"os": "ubuntu-latest",
"enabled": level >= 2,
// do not fail nightlies on this for now
"secondary": level <= 2,
"test": true,
// turn off custom allocator & symbolic functions to make LSAN do its magic
"CMAKE_PRESET": "sanitize",
// `StackOverflow*` correctly triggers ubsan
// `reverse-ffi` fails to link in sanitizers
// `interactive` and `async_select_channel` fail nondeterministically, would need to
// be investigated.
"CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel'"
},
// exclude seriously slow/problematic tests (laketests crash)
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},*/
{
"name": "macOS",
"os": "macos-15-intel",
@@ -304,7 +252,7 @@ jobs:
},
{
"name": "Windows",
"os": large && (fast || level >= 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
"os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
"release": true,
"enabled": level >= 2,
"test": true,

View File

@@ -41,7 +41,7 @@
"SMALL_ALLOCATOR": "OFF",
"USE_MIMALLOC": "OFF",
"BSYMBOLIC": "OFF",
"LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
"LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000"
},
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/sanitize"

View File

@@ -72,9 +72,6 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
The github repository will automatically update stage0 on `master` once
`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
To trigger this, modify `stage0/src/stdlib_flags.h` (e.g., by adding or changing
a comment). When `update-stage0` runs, it will overwrite `stage0/src/stdlib_flags.h`
with the contents of `src/stdlib_flags.h`, bringing them back in sync.
NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.

View File

@@ -129,7 +129,8 @@ For all other modules imported by `lean`, the initializer is run without `builti
Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtin_init]` functions are only run for native executable or plugins, regardless of whether their module is imported or not.
`lean` uses built-in initializers for e.g. registering basic parsers that should be available even without importing their module (which is necessary for bootstrapping).
The initializer for module `A.B` in a package `foo` is called `initialize_foo_A_B`. For modules in the Lean core (e.g., `Init.Prelude`), the initializer is called `initialize_Init_Prelude`. Module initializers will automatically initialize any imported modules. They are also idempotent (when run with the same `builtin` flag), but not thread-safe.
The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
**Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) **before** calling `lean_initialize()` or `lean_initialize_runtime_module()`. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.

View File

@@ -1,54 +0,0 @@
This release introduces the Lean module system, which allows files to
control the visibility of their contents for other files. In previous
releases, this feature was available as a preview when the option
`experimental.module` was set to `true`; it is now a fully supported
feature of Lean.
# Benefits
Because modules reduce the amount of information exposed to other
code, they speed up rebuilds because irrelevant changes can be
ignored, they make it possible to be deliberate about API evolution by
hiding details that may change from clients, they help proofs be
checked faster by avoiding accidentally unfolding definitions, and
they lead to smaller executable files through improved dead code
elimination.
# Visibility
A source file is a module if it begins with the `module` keyword. By
default, declarations in a module are private; the `public` modifier
exports them. Proofs of theorems and bodies of definitions are private
by default even when their signatures are public; the bodies of
definitions can be made public by adding the `@[expose]`
attribute. Theorems and opaque constants never expose their bodies.
`public section` and `@[expose] section` change the default visibility
of declarations in the section.
# Imports
Modules may only import other modules. By default, `import` adds the
public information of the imported module to the private scope of the
current module. Adding the `public` modifier to an import places the
imported modules's public information in the public scope of the
current module, exposing it in turn to the current module's clients.
Within a package, `import all` can be used to import another module's
private scope into the current module; this can be used to separate
lemmas or tests from definition modules without exposing details to
downstream clients.
# Meta Code
Code used in metaprograms must be marked `meta`. This ensures that the
code is compiled and available for execution when it is needed during
elaboration. Meta code may only reference other meta code. A whole
module can be made available in the meta phase using `meta import`;
this allows code to be shared across phases by importing the module in
each phase. Code that is reachable from public metaprograms must be
imported via `public meta import`, while local metaprograms can use
plain `meta import` for their dependencies.
The module system is described in detail in [the Lean language reference](https://lean-reference-manual-review.netlify.app/find/?domain=Verso.Genre.Manual.section&name=files).

View File

@@ -0,0 +1,132 @@
/-
Copyright (c) 2025 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
-/
import Lean
namespace Lean.Meta.Grind.Analyzer
/-!
A simple E-matching annotation analyzer.
For each theorem annotated as an E-matching candidate, it creates an artificial goal, executes `grind` and shows the
number of instances created.
For a theorem of the form `params -> type`, the artificial goal is of the form `params -> type -> False`.
-/
/--
`grind` configuration for the analyzer. We disable case-splits and lookahead,
increase the number of generations, and limit the number of instances generated.
-/
def config : Grind.Config := {
splits := 0
lookahead := false
mbtc := false
ematch := 20
instances := 100
gen := 10
}
structure Config where
/-- Minimum number of instantiations to trigger summary report -/
min : Nat := 10
/-- Minimum number of instantiations to trigger detailed report -/
detailed : Nat := 50
def mkParams : MetaM Params := do
let params Grind.mkParams config
let ematch getEMatchTheorems
let casesTypes Grind.getCasesTypes
return { params with ematch, casesTypes }
/-- Returns the total number of generated instances. -/
private def sum (cs : PHashMap Origin Nat) : Nat := Id.run do
let mut r := 0
for (_, c) in cs do
r := r + c
return r
private def thmsToMessageData (thms : PHashMap Origin Nat) : MetaM MessageData := do
let data := thms.toArray.filterMap fun (origin, c) =>
match origin with
| .decl declName => some (declName, c)
| _ => none
let data := data.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then Name.lt d₁ d₂ else c₁ > c₂
let data data.mapM fun (declName, counter) =>
return .trace { cls := `thm } m!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
return .trace { cls := `thm } "instances" data
/--
Analyzes theorem `declName`. That is, creates the artificial goal based on `declName` type,
and invokes `grind` on it.
-/
def analyzeEMatchTheorem (declName : Name) (c : Config) : MetaM Unit := do
let info getConstInfo declName
let mvarId forallTelescope info.type fun _ type => do
withLocalDeclD `h type fun _ => do
return ( mkFreshExprMVar (mkConst ``False)).mvarId!
let result Grind.main mvarId ( mkParams) (pure ())
let thms := result.counters.thm
let s := sum thms
if s > c.min then
IO.println s!"{declName} : {s}"
if s > c.detailed then
logInfo m!"{declName}\n{← thmsToMessageData thms}"
-- Not sure why this is failing: `down_pure` perhaps has an unnecessary universe parameter?
run_meta analyzeEMatchTheorem ``Std.Do.SPred.down_pure {}
/-- Analyzes all theorems in the standard library marked as E-matching theorems. -/
def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
let origins := ( getEMatchTheorems).getOrigins
let decls := origins.filterMap fun | .decl declName => some declName | _ => none
for declName in decls.mergeSort Name.lt do
try
analyzeEMatchTheorem declName c
catch e =>
logError m!"{declName} failed with {e.toMessageData}"
logInfo m!"Finished analyzing {decls.length} theorems"
/-- Macro for analyzing E-match theorems with unlimited heartbeats -/
macro "#analyzeEMatchTheorems" : command => `(
set_option maxHeartbeats 0 in
run_meta analyzeEMatchTheorems
)
#analyzeEMatchTheorems
-- -- We can analyze specific theorems using commands such as
set_option trace.grind.ematch.instance true
-- 1. grind immediately sees `(#[] : Array α) = ([] : List α).toArray` but probably this should be hidden.
-- 2. `Vector.toArray_empty` keys on `Array.mk []` rather than `#v[].toArray`
-- I guess we could add `(#[].extract _ _).extract _ _` as a stop pattern.
run_meta analyzeEMatchTheorem ``Array.extract_empty {}
-- Neither `Option.bind_some` nor `Option.bind_fun_some` fire, because the terms appear inside
-- lambdas. So we get crazy things like:
-- `fun x => ((some x).bind some).bind fun x => (some x).bind fun x => (some x).bind some`
-- We could consider replacing `filterMap_some` with
-- `filterMap g (filterMap f xs) = filterMap (f >=> g) xs`
-- to avoid the lambda that `grind` struggles with, but this would require more API around the fish.
run_meta analyzeEMatchTheorem ``Array.filterMap_some {}
-- Not entirely certain what is wrong here, but certainly
-- `eq_empty_of_append_eq_empty` is firing too often.
-- Ideally we could instantiate this is we fine `xs ++ ys` in the same equivalence class,
-- note just as soon as we see `xs ++ ys`.
-- I've tried removing this in https://github.com/leanprover/lean4/pull/10162
run_meta analyzeEMatchTheorem ``Array.range'_succ {}
-- Perhaps the same story here.
run_meta analyzeEMatchTheorem ``Array.range_succ {}
-- `zip_map_left` and `zip_map_right` are bad grind lemmas,
-- checking if they can be removed in https://github.com/leanprover/lean4/pull/10163
run_meta analyzeEMatchTheorem ``Array.zip_map {}
-- It seems crazy to me that as soon as we have `0 >>> n = 0`, we instantiate based on the
-- pattern `0 >>> n >>> m` by substituting `0` into `0 >>> n` to produce the `0 >>> n >>> n`.
-- I don't think any forbidden subterms can help us here. I don't know what to do. :-(
run_meta analyzeEMatchTheorem ``Int.zero_shiftRight {}

View File

@@ -300,7 +300,7 @@ def parseHeaderFromString (text path : String) :
throw <| .userError "parse errors in file"
-- the insertion point for `add` is the first newline after the imports
let insertion := header.raw.getTailPos?.getD parserState.pos
let insertion := text.findAux (· == '\n') text.rawEndPos insertion + '\n'
let insertion := text.findAux (· == '\n') text.endPos insertion + '\n'
pure (path, inputCtx, header, insertion)
/-- Parse a source file to extract the location of the import lines, for edits and error messages.
@@ -593,16 +593,16 @@ def main (args : List String) : IO UInt32 := do
for stx in imports do
let mod := decodeImport stx
if remove.contains mod || seen.contains mod then
out := out ++ String.Pos.Raw.extract text pos stx.raw.getPos?.get!
out := out ++ text.extract pos stx.raw.getPos?.get!
-- We use the end position of the syntax, but include whitespace up to the first newline
pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + '\n'
seen := seen.insert mod
out := out ++ String.Pos.Raw.extract text pos insertion
out := out ++ text.extract pos insertion
for mod in add do
if !seen.contains mod then
seen := seen.insert mod
out := out ++ s!"{mod}\n"
out := out ++ String.Pos.Raw.extract text insertion text.rawEndPos
out := out ++ text.extract insertion text.rawEndPos
IO.FS.writeFile path out
count := count + 1

View File

@@ -60,7 +60,7 @@ if (arity == fixed + {n}) \{
for j in [n:max + 1] do
let fs := mkFsArgs (j - n)
let sep := if j = n then "" else ", "
emit s!" case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); lean_free_object(f); return r; }\n"
emit s!" case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); lean_free_small_object(f); return r; }\n"
emit " }
}
switch (arity) {\n"
@@ -162,7 +162,7 @@ static obj* fix_args(obj* f, unsigned n, obj*const* as) {
for (unsigned i = 0; i < fixed; i++, source++, target++) {
*target = *source;
}
lean_free_object(f);
lean_free_small_object(f);
}
for (unsigned i = 0; i < n; i++, as++, target++) {
*target = *as;

96
script/bench.sh Executable file
View File

@@ -0,0 +1,96 @@
#!/usr/bin/env bash
set -euxo pipefail
cmake --preset release 1>&2
# We benchmark against stage2/bin to test new optimizations.
timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2
export PATH=$PWD/build/release/stage2/bin:$PATH
# The extra opts used to be passed to the Makefile during benchmarking only but with Lake it is
# easier to configure them statically.
cmake -B build/release/stage3 -S src -DLEAN_EXTRA_LAKEFILE_TOML='weakLeanArgs=["-Dprofiler=true", "-Dprofiler.threshold=9999999", "--stats"]' 1>&2
(
cd tests/bench
timeout -s KILL 1h time temci exec --config speedcenter.yaml --in speedcenter.exec.velcom.yaml 1>&2
temci report run_output.yaml --reporter codespeed2
)
if [ -d .git ]; then
DIR="$(git rev-parse @)"
BASE_URL="https://speed.lean-lang.org/lean4-out/$DIR"
{
cat <<'EOF'
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<title>Lakeprof Report</title>
</head>
<h1>Lakeprof Report</h1>
<button type="button" id="btn_fetch">View build trace in Perfetto</button>
<script type="text/javascript">
const ORIGIN = 'https://ui.perfetto.dev';
const btnFetch = document.getElementById('btn_fetch');
async function fetchAndOpen(traceUrl) {
const resp = await fetch(traceUrl);
// Error checking is left as an exercise to the reader.
const blob = await resp.blob();
const arrayBuffer = await blob.arrayBuffer();
openTrace(arrayBuffer, traceUrl);
}
function openTrace(arrayBuffer, traceUrl) {
const win = window.open(ORIGIN);
if (!win) {
btnFetch.style.background = '#f3ca63';
btnFetch.onclick = () => openTrace(arrayBuffer);
btnFetch.innerText = 'Popups blocked, click here to open the trace file';
return;
}
const timer = setInterval(() => win.postMessage('PING', ORIGIN), 50);
const onMessageHandler = (evt) => {
if (evt.data !== 'PONG') return;
// We got a PONG, the UI is ready.
window.clearInterval(timer);
window.removeEventListener('message', onMessageHandler);
const reopenUrl = new URL(location.href);
reopenUrl.hash = `#reopen=${traceUrl}`;
win.postMessage({
perfetto: {
buffer: arrayBuffer,
title: 'Lake Build Trace',
url: reopenUrl.toString(),
}}, ORIGIN);
};
window.addEventListener('message', onMessageHandler);
}
// This is triggered when following the link from the Perfetto UI's sidebar.
if (location.hash.startsWith('#reopen=')) {
const traceUrl = location.hash.substr(8);
fetchAndOpen(traceUrl);
}
EOF
cat <<EOF
btnFetch.onclick = () => fetchAndOpen("$BASE_URL/lakeprof.trace_event");
</script>
EOF
echo "<pre><code>"
(cd src; lakeprof report -prc)
echo "</code></pre>"
echo "</body></html>"
} | tee index.html
curl -T index.html $BASE_URL/index.html
curl -T src/lakeprof.log $BASE_URL/lakeprof.log
curl -T src/lakeprof.trace_event $BASE_URL/lakeprof.trace_event
fi

View File

@@ -10,16 +10,6 @@ Tests language server memory use by repeatedly re-elaborate a given file.
NOTE: only works on Linux for now.
-/
def determineRSS (pid : UInt32) : IO Nat := do
let status IO.FS.readFile s!"/proc/{pid}/smaps_rollup"
let some rssLine := status.splitOn "\n" |>.find? (·.startsWith "Rss:")
| throw <| IO.userError "No RSS in proc status"
let rssLine := rssLine.dropPrefix "Rss:"
let rssLine := rssLine.dropWhile Char.isWhitespace
let some rssInKB := rssLine.takeWhile Char.isDigit |>.toNat?
| throw <| IO.userError "Cannot parse RSS"
return rssInKB
def main (args : List String) : IO Unit := do
let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
let file IO.FS.realPath file
@@ -44,14 +34,11 @@ def main (args : List String) : IO Unit := do
let text IO.FS.readFile file
let (_, headerEndPos, _) Elab.parseImports text
let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
let n := iters.toNat!
let mut lastRSS? : Option Nat := none
let mut totalRSSDelta : Int := 0
let mut requestNo : Nat := 1
let mut versionNo : Nat := 1
Ipc.writeNotification "textDocument/didOpen", {
textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }
for i in [0:n] do
for i in [0:iters.toNat!] do
if i > 0 then
versionNo := versionNo + 1
let params : DidChangeTextDocumentParams := {
@@ -74,16 +61,9 @@ def main (args : List String) : IO Unit := do
IO.eprintln diag.message
requestNo := requestNo + 1
let rss determineRSS ( read).pid
-- The first `didChange` usually results in a significantly higher RSS increase than
-- the others, so we ignore it.
if i > 1 then
if let some lastRSS := lastRSS? then
totalRSSDelta := totalRSSDelta + ((rss : Int) - (lastRSS : Int))
lastRSS? := some rss
let avgRSSDelta := totalRSSDelta / (n - 2)
IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
let status IO.FS.readFile s!"/proc/{(← read).pid}/status"
for line in status.splitOn "\n" |>.filter (·.startsWith "RssAnon") do
IO.eprintln line
let _ Ipc.collectDiagnostics requestNo uri versionNo
( Ipc.stdin).writeLspMessage (Message.notification "exit" none)

View File

@@ -1,89 +0,0 @@
import Lean.Data.Lsp
import Lean.Elab.Import
open Lean
open Lean.Lsp
open Lean.JsonRpc
/-!
Tests watchdog memory use by repeatedly re-elaborate a given file.
NOTE: only works on Linux for now.
-/
def determineRSS (pid : UInt32) : IO Nat := do
let status IO.FS.readFile s!"/proc/{pid}/smaps_rollup"
let some rssLine := status.splitOn "\n" |>.find? (·.startsWith "Rss:")
| throw <| IO.userError "No RSS in proc status"
let rssLine := rssLine.dropPrefix "Rss:"
let rssLine := rssLine.dropWhile Char.isWhitespace
let some rssInKB := rssLine.takeWhile Char.isDigit |>.toNat?
| throw <| IO.userError "Cannot parse RSS"
return rssInKB
def main (args : List String) : IO Unit := do
let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
let file IO.FS.realPath file
let uri := s!"file://{file}"
Ipc.runWith leanCmd (#["--server", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do
let capabilities := {
textDocument? := some {
completion? := some {
completionItem? := some {
insertReplaceSupport? := true
}
}
}
}
Ipc.writeRequest 0, "initialize", { capabilities : InitializeParams }
discard <| Ipc.readResponseAs 0 InitializeResult
Ipc.writeNotification "initialized", InitializedParams.mk
let text IO.FS.readFile file
let (_, headerEndPos, _) Elab.parseImports text
let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
let n := iters.toNat!
let mut lastRSS? : Option Nat := none
let mut totalRSSDelta : Int := 0
let mut requestNo : Nat := 1
let mut versionNo : Nat := 1
Ipc.writeNotification "textDocument/didOpen", {
textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }
for i in [0:iters.toNat!] do
if i > 0 then
versionNo := versionNo + 1
let params : DidChangeTextDocumentParams := {
textDocument := {
uri := uri
version? := versionNo
}
contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
start := headerEndPos
«end» := headerEndPos
} " "]
}
let params := toJson params
Ipc.writeNotification "textDocument/didChange", params
requestNo := requestNo + 1
let diags Ipc.collectDiagnostics requestNo uri versionNo
if let some diags := diags then
for diag in diags.param.diagnostics do
IO.eprintln diag.message
requestNo := requestNo + 1
Ipc.waitForILeans requestNo uri versionNo
let rss determineRSS ( read).pid
-- The first `didChange` usually results in a significantly higher RSS increase than
-- the others, so we ignore it.
if i > 1 then
if let some lastRSS := lastRSS? then
totalRSSDelta := totalRSSDelta + ((rss : Int) - (lastRSS : Int))
lastRSS? := some rss
let avgRSSDelta := totalRSSDelta / (n - 2)
IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
let _ Ipc.collectDiagnostics requestNo uri versionNo
Ipc.shutdown requestNo
discard <| Ipc.waitForExit

View File

@@ -58,11 +58,7 @@ OPTIONS=()
# We build cadical using the custom toolchain on Linux to avoid glibc versioning issues
echo -n " -DLEAN_STANDALONE=ON -DCADICAL_USE_CUSTOM_CXX=ON"
echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
# these should also be used for cadical, so do not use `LEAN_EXTRA_CXX_FLAGS` here
echo -n " -DCMAKE_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
# the above does not include linker flags which will be added below based on context, so skip the
# generic check by cmake
echo -n " -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER_WORKS=1"
echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
# use target compiler directly when not cross-compiling
if [[ -L llvm-host ]]; then
echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"

View File

@@ -31,8 +31,6 @@ What this script does:
- Ensures tags are merged into stable branches (for non-RC releases)
- Verifies bump branches exist and are configured correctly
- Special handling for ProofWidgets4 release tags
- For mathlib4: runs verify_version_tags.py to validate the release tag
(checks git/GitHub consistency, toolchain, elan, cache, and build)
3. Optionally automates missing steps (when not in --dry-run mode):
- Creates missing release tags using push_repo_release_tag.py
@@ -501,57 +499,6 @@ def check_proofwidgets4_release(repo_url, target_toolchain, github_token):
print(f" You will need to create and push a tag v0.0.{next_version}")
return False
def run_mathlib_verify_version_tags(toolchain, verbose=False):
"""Run mathlib4's verify_version_tags.py script to validate the release tag.
This clones mathlib4 to a temp directory and runs the verification script.
Returns True if verification passes, False otherwise.
"""
import tempfile
print(f" ... Running mathlib4 verify_version_tags.py {toolchain}")
with tempfile.TemporaryDirectory() as tmpdir:
# Clone mathlib4 (shallow clone is sufficient for running the script)
clone_result = subprocess.run(
['git', 'clone', '--depth', '1', 'https://github.com/leanprover-community/mathlib4.git', tmpdir],
capture_output=True,
text=True
)
if clone_result.returncode != 0:
print(f" ❌ Failed to clone mathlib4: {clone_result.stderr.strip()[:200]}")
return False
# Run the verification script
script_path = os.path.join(tmpdir, 'scripts', 'verify_version_tags.py')
if not os.path.exists(script_path):
print(f" ❌ verify_version_tags.py not found in mathlib4 (expected at scripts/verify_version_tags.py)")
return False
# Run from the mathlib4 directory so git operations work
result = subprocess.run(
['python3', script_path, toolchain],
cwd=tmpdir,
capture_output=True,
text=True,
timeout=900 # 15 minutes timeout for cache download etc.
)
# Print output with indentation
if result.stdout:
for line in result.stdout.strip().split('\n'):
print(f" {line}")
if result.stderr:
for line in result.stderr.strip().split('\n'):
print(f" {line}")
if result.returncode != 0:
print(f" ❌ mathlib4 verify_version_tags.py failed")
return False
print(f" ✅ mathlib4 verify_version_tags.py passed")
return True
def main():
parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories")
parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)")
@@ -816,12 +763,6 @@ def main():
repo_status[name] = False
continue
# For mathlib4, run verify_version_tags.py to validate the release tag
if name == "mathlib4":
if not run_mathlib_verify_version_tags(toolchain, verbose):
repo_status[name] = False
continue
repo_status[name] = success
# Final check for lean4 master branch

View File

@@ -10,7 +10,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 27)
set(LEAN_VERSION_MINOR 26)
set(LEAN_VERSION_PATCH 0)
set(LEAN_VERSION_IS_RELEASE 0) # 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'")
@@ -42,7 +42,7 @@ if(LLD_PATH)
endif()
set(LEAN_EXTRA_LINKER_FLAGS ${LEAN_EXTRA_LINKER_FLAGS_DEFAULT} CACHE STRING "Additional flags used by the linker")
set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler. Unlike `CMAKE_CXX_FLAGS`, these will not be used to build e.g. cadical.")
set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler")
set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests")
if (NOT CMAKE_BUILD_TYPE)
@@ -191,7 +191,7 @@ endif()
set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
# Initialize CXXFLAGS.
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
set(CMAKE_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
set(CMAKE_CXX_FLAGS_DEBUG "-DLEAN_DEBUG")
set(CMAKE_CXX_FLAGS_MINSIZEREL "-DNDEBUG")
set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG")

View File

@@ -205,5 +205,3 @@ export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
/-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/
theorem Exists.choose_spec {p : α Prop} (P : a, p a) : p P.choose := Classical.choose_spec P
grind_pattern Exists.choose_spec => P.choose

View File

@@ -25,7 +25,7 @@ instances are provided for the same type.
instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
forIn x b f := forIn' x b fun a _ => f a
@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} (x : ρ) (b : β)
@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
(f : (a : α) a x β m (ForInStep β)) (g : (a : α) β m (ForInStep β))
(h : a m b, f a m b = g a b) :
forIn' x b f = forIn x b g := by
@@ -40,7 +40,7 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
simp [h]
rfl
@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β}
@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m]
(x : ρ) (b : β) (f : (a : α) β m (ForInStep β)) :
forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
rfl
@@ -403,7 +403,7 @@ class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂))
/--
Runs the monadic action `f` on each element of the collection `coll`.
-/
forM (coll : γ) (f : α m PUnit) : m PUnit
forM [Monad m] (coll : γ) (f : α m PUnit) : m PUnit
export ForM (forM)

View File

@@ -148,23 +148,6 @@ This is the inverse of `ExceptT.mk`.
@[always_inline, inline, expose]
def ExceptT.run {ε : Type u} {m : Type u Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
/--
Use a monadic action that may throw an exception by providing explicit success and failure
continuations.
-/
@[always_inline, inline, expose]
def ExceptT.runK [Monad m] (x : ExceptT ε m α) (ok : α m β) (error : ε m β) : m β :=
x.run >>= (·.casesOn error ok)
/--
Returns the value of a computation, forgetting whether it was an exception or a success.
This corresponds to early return.
-/
@[always_inline, inline, expose]
def ExceptT.runCatch [Monad m] (x : ExceptT α m α) : m α :=
x.runK pure pure
namespace ExceptT
variable {ε : Type u} {m : Type u Type v} [Monad m]

View File

@@ -377,7 +377,7 @@ class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v))
More information about the translation of `for` loops into `ForIn.forIn` is available in [the Lean
reference manual](lean-manual://section/monad-iteration-syntax).
-/
forIn {β} (xs : ρ) (b : β) (f : α β m (ForInStep β)) : m β
forIn {β} [Monad m] (xs : ρ) (b : β) (f : α β m (ForInStep β)) : m β
export ForIn (forIn)
@@ -405,7 +405,7 @@ class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)
More information about the translation of `for` loops into `ForIn'.forIn'` is available in [the
Lean reference manual](lean-manual://section/monad-iteration-syntax).
-/
forIn' {β} (x : ρ) (b : β) (f : (a : α) a x β m (ForInStep β)) : m β
forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) a x β m (ForInStep β)) : m β
export ForIn' (forIn')
@@ -1590,7 +1590,7 @@ gen_injective_theorems% PSum
gen_injective_theorems% Sigma
gen_injective_theorems% String
gen_injective_theorems% String.Pos.Raw
gen_injective_theorems% Substring.Raw
gen_injective_theorems% Substring
gen_injective_theorems% Subtype
gen_injective_theorems% Sum
gen_injective_theorems% Task
@@ -2507,7 +2507,8 @@ class Antisymm (r : αα → Prop) : Prop where
/-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
antisymm (a b : α) : r a b r b a a = b
/-- `Asymm r` means that the binary relation `r` is asymmetric, that is, `r a b → ¬ r b a`. -/
/-- `Asymm r` means that the binary relation `r` is asymmetric, that is,
`r a b → ¬ r b a`. -/
class Asymm (r : α α Prop) : Prop where
/-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
asymm : a b, r a b ¬r b a
@@ -2517,19 +2518,16 @@ class Symm (r : αα → Prop) : Prop where
/-- A symmetric relation satisfies `r a b → r b a`. -/
symm : a b, r a b r b a
/-- `Total X r` means that the binary relation `r` on `X` is total, that is, `r a b` or `r b a`. -/
/-- `Total X r` means that the binary relation `r` on `X` is total, that is, that for any
`x y : X` we have `r x y` or `r y x`. -/
class Total (r : α α Prop) : Prop where
/-- A total relation satisfies `r a b` or `r b a`. -/
/-- A total relation satisfies `r a b r b a`. -/
total : a b, r a b r b a
/-- `Irrefl r` means the binary relation `r` is irreflexive, that is, `r x x` never holds. -/
/-- `Irrefl r` means the binary relation `r` is irreflexive, that is, `r x x` never
holds. -/
class Irrefl (r : α α Prop) : Prop where
/-- An irreflexive relation satisfies `¬ r a a`. -/
irrefl : a, ¬r a a
/-- `Trichotomous r` says that `r` is trichotomous, that is, `¬ r a b → ¬ r b a → a = b`. -/
class Trichotomous (r : α α Prop) : Prop where
/-- An trichotomous relation `r` satisfies `¬ r a b → ¬ r b a → a = b`. -/
trichotomous (a b : α) : ¬ r a b ¬ r b a a = b
end Std

View File

@@ -242,7 +242,7 @@ Examples:
* `#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]`
* `#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]`
-/
@[extern "lean_array_swap", expose]
@[extern "lean_array_swap", grind]
def swapIfInBounds (xs : Array α) (i j : @& Nat) : Array α :=
if h₁ : i < xs.size then
if h₂ : j < xs.size then swap xs i j
@@ -570,7 +570,7 @@ protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
| ForInStep.yield b => loop i (Nat.le_of_lt h') b
loop as.size (Nat.le_refl _) b
instance [Monad m] : ForIn' m (Array α) α inferInstance where
instance : ForIn' m (Array α) α inferInstance where
forIn' := Array.forIn'
-- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -1001,7 +1001,7 @@ unless `start < stop`. By default, the entire array is used.
protected def forM {α : Type u} {m : Type v Type w} [Monad m] (f : α m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
as.foldlM (fun _ => f) start stop
instance [Monad m] : ForM m (Array α) α where
instance : ForM m (Array α) α where
forM xs f := Array.forM f xs
-- We simplify `Array.forM` to `forM`.

View File

@@ -100,15 +100,9 @@ abbrev push_toList := @toList_push
@[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
apply ext'; simp only [toList_append, List.nil_append]
@[simp] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
@[simp, grind _=_] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
apply ext'; simp only [toList_append, List.append_assoc]
grind_pattern append_assoc => (xs ++ ys) ++ zs where
xs =/= #[]; ys =/= #[]; zs =/= #[]
grind_pattern append_assoc => xs ++ (ys ++ zs) where
xs =/= #[]; ys =/= #[]; zs =/= #[]
@[simp] theorem appendList_eq_append {xs : Array α} {l : List α} : xs.appendList l = xs ++ l := rfl
@[simp, grind =] theorem toList_appendList {xs : Array α} {l : List α} :
@@ -116,4 +110,6 @@ grind_pattern append_assoc => xs ++ (ys ++ zs) where
rw [ appendList_eq_append]; unfold Array.appendList
induction l generalizing xs <;> simp [*]
end Array

View File

@@ -89,41 +89,11 @@ theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs
theorem isEqv_self [DecidableEq α] (xs : Array α) : Array.isEqv xs xs (· = ·) = true := by
simp [isEqv, isEqvAux_self]
def instDecidableEqImpl [DecidableEq α] : DecidableEq (Array α) := fun xs ys =>
match h:isEqv xs ys (fun a b => a = b) with
| true => isTrue (eq_of_isEqv xs ys h)
| false => isFalse (by subst ·; rw [isEqv_self] at h; contradiction)
instance instDecidableEq [DecidableEq α] : DecidableEq (Array α) := fun xs ys =>
match xs with
| [] =>
match ys with
| [] => isTrue rfl
| _ :: _ => isFalse (Array.noConfusion · (List.noConfusion ·))
| a :: as =>
match ys with
| [] => isFalse (Array.noConfusion · (List.noConfusion ·))
| b :: bs => instDecidableEqImpl a :: as b :: bs
@[csimp]
theorem instDecidableEq_csimp : @instDecidableEq = @instDecidableEqImpl :=
Subsingleton.allEq _ _
/--
Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
-/
instance instDecidableEqEmp (xs : Array α) : Decidable (xs = #[]) :=
match xs with
| [] => isTrue rfl
| _ :: _ => isFalse (Array.noConfusion · (List.noConfusion ·))
/--
Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
-/
instance instDecidableEmpEq (ys : Array α) : Decidable (#[] = ys) :=
match ys with
| [] => isTrue rfl
| _ :: _ => isFalse (Array.noConfusion · (List.noConfusion ·))
instance [DecidableEq α] : DecidableEq (Array α) :=
fun xs ys =>
match h:isEqv xs ys (fun a b => a = b) with
| true => isTrue (eq_of_isEqv xs ys h)
| false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
theorem beq_eq_decide [BEq α] (xs ys : Array α) :
(xs == ys) = if h : xs.size = ys.size then

View File

@@ -200,7 +200,7 @@ theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
simp [getElem?_extract]
omega
@[simp] theorem extract_extract {as : Array α} {i j k l : Nat} :
@[simp, grind =] theorem extract_extract {as : Array α} {i j k l : Nat} :
(as.extract i j).extract k l = as.extract (i + k) (min (i + l) j) := by
ext m h₁ h₂
· simp
@@ -208,9 +208,6 @@ theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
· simp only [size_extract] at h₁ h₂
simp [Nat.add_assoc]
grind_pattern extract_extract => (as.extract i j).extract k l where
as =/= #[]
theorem extract_eq_empty_of_eq_empty {as : Array α} {i j : Nat} (h : as = #[]) :
as.extract i j = #[] := by
simp [h]
@@ -409,6 +406,8 @@ theorem popWhile_append {xs ys : Array α} :
rcases ys with ys
simp only [List.append_toArray, List.popWhile_toArray, List.reverse_append, List.dropWhile_append,
List.isEmpty_iff, List.isEmpty_toArray, List.isEmpty_reverse]
-- Why do these not fire with `simp`?
rw [List.popWhile_toArray, List.isEmpty_toArray, List.isEmpty_reverse]
split
· rfl
· simp

View File

@@ -1628,15 +1628,12 @@ theorem filterMap_eq_filter {p : α → Bool} (w : stop = as.size) :
cases as
simp
@[grind =]
theorem filterMap_filterMap {f : α Option β} {g : β Option γ} {xs : Array α} :
filterMap g (filterMap f xs) = filterMap (fun x => (f x).bind g) xs := by
cases xs
simp [List.filterMap_filterMap]
grind_pattern filterMap_filterMap => filterMap g (filterMap f xs) where
f =/= some
g =/= some
@[grind =]
theorem map_filterMap {f : α Option β} {g : β γ} {xs : Array α} :
map g (filterMap f xs) = filterMap (fun x => (f x).map g) xs := by
@@ -2231,8 +2228,8 @@ theorem push_eq_flatten_iff {xss : Array (Array α)} {ys : Array α} {y : α} :
-- zs = cs ++ ds.flatten := by sorry
/-- Two arrays of arrays are equal iff their flattens coincide, as well as the sizes of the
arrays. -/
/-- Two arrays of subarrays are equal iff their flattens coincide, as well as the sizes of the
subarrays. -/
theorem eq_iff_flatten_eq {xss₁ xss₂ : Array (Array α)} :
xss₁ = xss₂ xss₁.flatten = xss₂.flatten map size xss₁ = map size xss₂ := by
cases xss₁ using array₂_induction with
@@ -3555,6 +3552,11 @@ theorem mem_of_back? {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs
rcases ys with ys
simp only [List.append_toArray, List.back_toArray, List.getLast_append, List.isEmpty_iff,
List.isEmpty_toArray]
split
· rw [dif_pos]
simpa only [List.isEmpty_toArray]
· rw [dif_neg]
simpa only [List.isEmpty_toArray]
theorem back_append_right {xs ys : Array α} (h : 0 < ys.size) :
(xs ++ ys).back (by simp; omega) = ys.back h := by
@@ -3966,29 +3968,28 @@ theorem getElem_modify_of_ne {xs : Array α} {i : Nat} (h : i ≠ j)
/-! ### swap -/
@[grind =]
theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
(xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
simp only [swap_def, getElem_set, eq_comm (a := k)]
split <;> split <;> simp_all
@[simp] theorem getElem_swap_right {xs : Array α} {i j : Nat} {hi hj} :
(xs.swap i j hi hj)[j]'(by simpa using hj) = xs[i] := by
simp +contextual [getElem_swap]
simp [swap_def]
@[simp] theorem getElem_swap_left {xs : Array α} {i j : Nat} {hi hj} :
(xs.swap i j hi hj)[i]'(by simpa using hi) = xs[j] := by
simp [getElem_swap]
simp +contextual [swap_def, getElem_set]
@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj}
{h : k < (xs.swap i j hi hj).size} (hi' : k i) (hj' : k j) :
(xs.swap i j hi hj)[k] = xs[k]'(by simp_all) := by
simp [getElem_swap, hi', hj']
@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj} (hp : k < xs.size)
(hi' : k i) (hj' : k j) : (xs.swap i j hi hj)[k]'(xs.size_swap .. |>.symm hp) = xs[k] := by
simp [swap_def, getElem_set, hi'.symm, hj'.symm]
@[deprecated getElem_swap (since := "2025-10-10")]
theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs.size) :
(xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] :=
getElem_swap _ _ _
(xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
split
· simp_all only [getElem_swap_left]
· split <;> simp_all
@[grind =]
theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
(xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
apply getElem_swap'
@[simp] theorem swap_swap {xs : Array α} {i j : Nat} (hi hj) :
(xs.swap i j hi hj).swap i j ((xs.size_swap ..).symm hi) ((xs.size_swap ..).symm hj) = xs := by
@@ -4009,66 +4010,8 @@ theorem swap_comm {xs : Array α} {i j : Nat} (hi hj) : xs.swap i j hi hj = xs.s
· split <;> simp_all
· split <;> simp_all
/-! ### swapIfInBounds -/
@[grind =] theorem swapIfInBounds_def {xs : Array α} {i j : Nat} :
xs.swapIfInBounds i j = if h₁ : i < xs.size then
if h₂ : j < xs.size then swap xs i j else xs else xs := rfl
@[simp, grind =] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
(xs.swapIfInBounds i j).size = xs.size := by
unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
@[grind =] theorem getElem_swapIfInBounds {xs : Array α} {i j k : Nat}
(hk : k < (xs.swapIfInBounds i j).size) :
(xs.swapIfInBounds i j)[k] =
if h₁ : k = i j < xs.size then xs[j]'h₁.2 else if h₂ : k = j i < xs.size then xs[i]'h₂.2
else xs[k]'(by simp_all) := by
rw [size_swapIfInBounds] at hk
unfold swapIfInBounds
split <;> rename_i hi
· split <;> rename_i hj
· simp only [hi, hj, and_true]
exact getElem_swap _ _ _
· simp only [hi, hj, and_true, and_false, dite_false]
split <;> simp_all
· simp only [hi, and_false, dite_false]
split <;> simp_all
@[simp]
theorem getElem_swapIfInBounds_of_size_le_left {xs : Array α} {i j k : Nat} (hi : xs.size i)
(hk : k < (xs.swapIfInBounds i j).size) :
(xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
have h₁ : k i := Nat.ne_of_lt <| Nat.lt_of_lt_of_le hk <|
Nat.le_trans (Nat.le_of_eq (size_swapIfInBounds)) hi
have h₂ : ¬ (i < xs.size) := Nat.not_lt_of_le hi
simp [getElem_swapIfInBounds, h₁, h₂]
@[simp]
theorem getElem_swapIfInBounds_of_size_le_right {xs : Array α} {i j k : Nat} (hj : xs.size j)
(hk : k < (xs.swapIfInBounds i j).size) :
(xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
have h₁ : ¬ (j < xs.size) := Nat.not_lt_of_le hj
have h₂ : k j := Nat.ne_of_lt <| Nat.lt_of_lt_of_le hk <|
Nat.le_trans (Nat.le_of_eq (size_swapIfInBounds)) hj
simp [getElem_swapIfInBounds, h₁, h₂]
@[simp]
theorem getElem_swapIfInBounds_left {xs : Array α} {i j : Nat} (hj : j < xs.size)
(hi : i < (xs.swapIfInBounds i j).size) : (xs.swapIfInBounds i j)[i] = xs[j] := by
simp [getElem_swapIfInBounds, hj]
@[simp]
theorem getElem_swapIfInBounds_right {xs : Array α} {i j : Nat} (hi : i < xs.size)
(hj : j < (xs.swapIfInBounds i j).size) :
(xs.swapIfInBounds i j)[j] = xs[i] := by
simp +contextual [getElem_swapIfInBounds, hi]
@[simp]
theorem getElem_swapIfInBounds_of_ne_of_ne {xs : Array α} {i j k : Nat} (hi : k i) (hj : k j)
(hk : k < (xs.swapIfInBounds i j).size) :
(xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
simp [getElem_swapIfInBounds, hi, hj]
(xs.swapIfInBounds i j).size = xs.size := by unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
/-! ### swapAt -/
@@ -4330,10 +4273,6 @@ theorem size_uset {xs : Array α} {v : α} {i : USize} (h : i.toNat < xs.size) :
theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i default := by
rfl
theorem getElem_eq_getD {xs : Array α} {i} {h : i < xs.size} (fallback : α) :
xs[i]'h = xs.getD i fallback := by
rw [getD_eq_getD_getElem?, getElem_eq_getElem?_get, Option.get_eq_getD]
/-! # mem -/
@[deprecated mem_toList_iff (since := "2025-05-26")]

View File

@@ -75,11 +75,11 @@ private theorem cons_lex_cons [BEq α] {lt : αα → Bool} {a b : α} {xs
Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList]
conv =>
lhs; congr; congr
rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if_roo rfl (fun _ _ _ => rfl)]
rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if rfl (fun _ _ _ => rfl)]
simp only [bind_pure_comp, map_pure]
rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
simp only [Std.toList_roo_eq_toList_rco_of_isSome_succ? (lo := 0) (h := rfl),
Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_rco_succ_succ,
simp only [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? (lo := 0) (h := rfl),
Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ,
Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
cases lt a b
@@ -151,7 +151,7 @@ protected theorem lt_of_le_of_lt [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrd
@[deprecated Array.lt_of_le_of_lt (since := "2025-08-01")]
protected theorem lt_of_le_of_lt' [LT α]
[i₁ : Std.Asymm (· < · : α α Prop)]
[i₂ : Std.Trichotomous (· < · : α α Prop)]
[i₂ : Std.Antisymm (¬ · < · : α α Prop)]
[i₃ : Trans (¬ · < · : α α Prop) (¬ · < ·) (¬ · < ·)]
{xs ys zs : Array α} (h₁ : xs ys) (h₂ : ys < zs) : xs < zs :=
letI := LE.ofLT α
@@ -165,7 +165,7 @@ protected theorem le_trans [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α]
@[deprecated Array.le_trans (since := "2025-08-01")]
protected theorem le_trans' [LT α]
[i₁ : Std.Asymm (· < · : α α Prop)]
[i₂ : Std.Trichotomous (· < · : α α Prop)]
[i₂ : Std.Antisymm (¬ · < · : α α Prop)]
[i₃ : Trans (¬ · < · : α α Prop) (¬ · < ·) (¬ · < ·)]
{xs ys zs : Array α} (h₁ : xs ys) (h₂ : ys zs) : xs zs :=
letI := LE.ofLT α
@@ -196,7 +196,7 @@ protected theorem le_of_lt [LT α]
protected theorem le_iff_lt_or_eq [LT α]
[Std.Irrefl (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
[Std.Asymm (· < · : α α Prop)]
{xs ys : Array α} : xs ys xs < ys xs = ys := by
simpa using List.le_iff_lt_or_eq (l₁ := xs.toList) (l₂ := ys.toList)
@@ -285,7 +285,7 @@ protected theorem lt_iff_exists [LT α] {xs ys : Array α} :
protected theorem le_iff_exists [LT α]
[Std.Asymm (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)] {xs ys : Array α} :
[Std.Antisymm (¬ · < · : α α Prop)] {xs ys : Array α} :
xs ys
(xs = ys.take xs.size)
( (i : Nat) (h₁ : i < xs.size) (h₂ : i < ys.size),
@@ -304,7 +304,7 @@ theorem append_left_lt [LT α] {xs ys zs : Array α} (h : ys < zs) :
theorem append_left_le [LT α]
[Std.Asymm (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
{xs ys zs : Array α} (h : ys zs) :
xs ++ ys xs ++ zs := by
cases xs
@@ -327,9 +327,9 @@ protected theorem map_lt [LT α] [LT β]
protected theorem map_le [LT α] [LT β]
[Std.Asymm (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
[Std.Asymm (· < · : β β Prop)]
[Std.Trichotomous (· < · : β β Prop)]
[Std.Antisymm (¬ · < · : β β Prop)]
{xs ys : Array α} {f : α β} (w : x y, x < y f x < f y) (h : xs ys) :
map f xs map f ys := by
cases xs

View File

@@ -1056,7 +1056,7 @@ theorem toInt_setWidth' {m n : Nat} (p : m ≤ n) {x : BitVec m} :
@[simp, grind =] theorem toFin_setWidth' {m n : Nat} (p : m n) (x : BitVec m) :
(setWidth' p x).toFin = x.toFin.castLE (Nat.pow_le_pow_right (by omega) (by omega)) := by
ext
rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat, Fin.val_castLE, val_toFin,
rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat, Fin.coe_castLE, val_toFin,
Nat.mod_eq_of_lt (by apply BitVec.toNat_lt_twoPow_of_le p)]
theorem toNat_setWidth_of_le {w w' : Nat} {b : BitVec w} (h : w w') : (b.setWidth w').toNat = b.toNat := by

View File

@@ -132,11 +132,6 @@ Copies the bytes with indices {name}`b` (inclusive) to {name}`e` (exclusive) to
def extract (a : ByteArray) (b e : Nat) : ByteArray :=
a.copySlice b empty 0 (e - b)
/--
Appends two byte arrays using fast array primitives instead of converting them into lists and back.
In compiled code, this function replaces calls to {name}`ByteArray.append`.
-/
@[inline]
protected def fastAppend (a : ByteArray) (b : ByteArray) : ByteArray :=
-- we assume that `append`s may be repeated, so use asymptotic growing; use `copySlice` directly to customize
@@ -248,7 +243,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
| ForInStep.yield b => loop i (Nat.le_of_lt h') b
loop as.size (Nat.le_refl _) b
instance [Monad m] : ForIn m ByteArray UInt8 where
instance : ForIn m ByteArray UInt8 where
forIn := ByteArray.forIn
/--

View File

@@ -55,12 +55,8 @@ instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
antisymm _ _ := Char.le_antisymm
-- This instance is useful while setting up instances for `String`.
instance ltTrichotomous : Std.Trichotomous (· < · : Char Char Prop) where
trichotomous _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
@[deprecated ltTrichotomous (since := "2025-10-27")]
def notLTAntisymm : Std.Antisymm (¬ · < · : Char Char Prop) where
antisymm := Char.ltTrichotomous.trichotomous
antisymm _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
instance ltAsymm : Std.Asymm (· < · : Char Char Prop) where
asymm _ _ := Char.lt_asymm

View File

@@ -246,11 +246,6 @@ instance neg (n : Nat) : Neg (Fin n) :=
theorem neg_def (a : Fin n) : -a = (n - a) % n, Nat.mod_lt _ a.pos := rfl
-- Later we give another version called `Fin.val_neg` that splits on `a = 0`.
protected theorem val_neg' (a : Fin n) : ((-a : Fin n) : Nat) = (n - a) % n :=
rfl
@[deprecated Fin.val_neg' (since := "2025-11-21")]
protected theorem coe_neg (a : Fin n) : ((-a : Fin n) : Nat) = (n - a) % n :=
rfl

View File

@@ -16,25 +16,17 @@ open Std
namespace Fin
@[simp, grind =] theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := rfl
@[simp] theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := rfl
@[deprecated ofNat_zero (since := "2025-05-28")] abbrev ofNat'_zero := @ofNat_zero
theorem mod_def (a m : Fin n) : a % m = Fin.mk (a.val % m.val) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
rfl
theorem val_mod (a m : Fin n) : (a % m).val = a.val % m.val := rfl
theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a.val * b.val) % n) (Nat.mod_lt _ a.pos) := rfl
theorem val_mul (a b : Fin n) : (a * b).val = (a.val * b.val) % n := rfl
theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b.val) + a.val) % n) (Nat.mod_lt _ a.pos) := rfl
@[grind =]
theorem val_sub (a b : Fin n) : (a - b).val = ((n - b.val) + a.val) % n := rfl
@[grind ]
theorem pos' : [Nonempty (Fin n)], 0 < n | i => i.pos
@[simp] theorem is_lt (a : Fin n) : (a : Nat) < n := a.2
@@ -46,8 +38,7 @@ theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
@[simp] protected theorem eta (a : Fin n) (h : a < n) : (a, h : Fin n) = a := rfl
@[ext, grind ext]
protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
@[ext] protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
theorem val_ne_iff {a b : Fin n} : a.1 b.1 a b := not_congr val_inj
@@ -78,7 +69,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
@[deprecated val_ofNat (since := "2025-05-28")] abbrev val_ofNat' := @val_ofNat
@[simp, grind =] theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by
@[simp] theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by
ext
simp
congr
@@ -98,7 +89,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
@[simp] theorem div_val (a b : Fin n) : (a / b).val = a.val / b.val :=
rfl
@[simp, grind =] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
@[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
rfl
@[simp] theorem val_eq_zero (a : Fin 1) : a.val = 0 :=
@@ -268,9 +259,7 @@ instance : LawfulOrderLT (Fin n) where
lt_iff := by
simp [ Fin.not_le, Decidable.imp_iff_not_or, Std.Total.total]
@[simp] theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := rfl
grind_pattern val_rev => i.rev
@[simp, grind =] theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := rfl
@[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := Fin.ext <| by
rw [val_rev, val_rev, Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
@@ -295,8 +284,6 @@ theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
@[simp] theorem val_last (n : Nat) : (last n).1 = n := rfl
grind_pattern val_last => last n
@[simp] theorem last_zero : (Fin.last 0 : Fin 1) = 0 := by
ext
simp
@@ -406,8 +393,6 @@ theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt zero_lt_one
@[simp] theorem val_succ (j : Fin n) : (j.succ : Nat) = j + 1 := rfl
grind_pattern val_succ => j.succ
@[simp] theorem succ_pos (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by
simp [Fin.lt_def]
@@ -468,18 +453,12 @@ theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) 1 :=
Fin.ne_of_gt (one_lt_succ_succ a)
@[simp, grind =] theorem val_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
@[deprecated val_castLT (since := "2025-11-21")]
theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
@[simp] theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
@[simp] theorem castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) : castLT i, hn hm = i, hm :=
rfl
@[simp, grind =] theorem val_castLE (h : n m) (i : Fin n) : (castLE h i : Nat) = i := rfl
@[deprecated val_castLE (since := "2025-11-21")]
theorem coe_castLE (h : n m) (i : Fin n) : (castLE h i : Nat) = i := rfl
@[simp, grind =] theorem coe_castLE (h : n m) (i : Fin n) : (castLE h i : Nat) = i := rfl
@[simp] theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n m) :
castLE h i, hn = i, Nat.lt_of_lt_of_le hn h := rfl
@@ -491,16 +470,13 @@ theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
@[simp] theorem castLE_castLE {k m n} (km : k m) (mn : m n) (i : Fin k) :
Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i :=
Fin.ext (by simp only [val_castLE])
Fin.ext (by simp only [coe_castLE])
@[simp] theorem castLE_comp_castLE {k m n} (km : k m) (mn : m n) :
Fin.castLE mn Fin.castLE km = Fin.castLE (Nat.le_trans km mn) :=
funext (castLE_castLE km mn)
@[simp, grind =] theorem val_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
@[deprecated val_cast (since := "2025-11-21")]
theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
@[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
@[simp] theorem cast_castLE {k m n} (km : k m) (mn : m = n) (i : Fin k) :
Fin.cast mn (i.castLE km) = i.castLE (mn km) :=
@@ -513,7 +489,7 @@ theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
@[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
@[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h = last n' :=
Fin.ext (by rw [val_cast, val_last, val_last, Nat.succ.inj h])
Fin.ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
@[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h i, hn = i, h hn := rfl
@@ -528,10 +504,7 @@ theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m n} : castLE h' = Fin.cast h := rfl
@[simp, grind =] theorem val_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
@[deprecated val_castAdd (since := "2025-11-21")]
theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
@[simp] theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
@[simp] theorem castAdd_zero : (castAdd 0 : Fin n Fin (n + 0)) = Fin.cast rfl := rfl
@@ -567,10 +540,7 @@ the reverse direction. -/
theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
(i.cast h).succ = i.succ.cast (by rw [h]) := rfl
@[simp, grind =] theorem val_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
@[deprecated val_castSucc (since := "2025-11-21")]
theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
@[simp] theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
@[simp] theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc i, h = i, Nat.lt_succ_of_lt h := rfl
@@ -578,7 +548,7 @@ theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := rfl
theorem castSucc_lt_succ {i : Fin n} : i.castSucc < i.succ :=
lt_def.2 <| by simp only [val_castSucc, val_succ, Nat.lt_succ_self]
lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i j.castSucc i < j.succ := by
simpa only [lt_def, le_def] using Nat.add_one_le_add_one_iff.symm
@@ -632,7 +602,7 @@ theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ := by
@[deprecated castSucc_lt_succ (since := "2025-10-29")]
theorem lt_succ {a : Fin n} : a.castSucc < a.succ := by
rw [castSucc, lt_def, val_castAdd, val_succ]; exact Nat.lt_succ_self a.val
rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : ( j, castSucc j = i) i last n :=
fun j, hj => hj Fin.ne_of_lt j.castSucc_lt_last,
@@ -640,10 +610,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, 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
@[simp] theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
@[simp] theorem addNat_zero (n : Nat) (i : Fin n) : addNat i 0 = i := by
ext
@@ -671,10 +638,7 @@ theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
(addNat i m').cast h = addNat i m :=
Fin.ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
@[simp, grind =] theorem val_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
@[deprecated val_natAdd (since := "2025-11-21")]
theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
@[simp] theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
@[simp] theorem natAdd_mk (n i : Nat) (hi : i < m) :
natAdd n i, hi = n + i, Nat.add_lt_add_left hi n := rfl
@@ -731,7 +695,7 @@ theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSu
omega
theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := Fin.ext <| by
rw [val_rev, val_castAdd, val_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by
rw [ rev_rev (castAdd ..), rev_castAdd, rev_rev]
@@ -753,12 +717,7 @@ theorem castSucc_natAdd (n : Nat) (i : Fin k) :
/-! ### pred -/
@[simp] theorem val_pred (j : Fin (n + 1)) (h : j 0) : (j.pred h : Nat) = j - 1 := rfl
grind_pattern val_pred => j.pred h
@[deprecated val_pred (since := "2025-11-21")]
theorem coe_pred (j : Fin (n + 1)) (h : j 0) : (j.pred h : Nat) = j - 1 := rfl
@[simp] theorem coe_pred (j : Fin (n + 1)) (h : j 0) : (j.pred h : Nat) = j - 1 := rfl
@[simp] theorem succ_pred : (i : Fin (n + 1)) (h : i 0), (i.pred h).succ = i
| 0, _, hi => by simp only [mk_zero, ne_eq, not_true] at hi
@@ -776,7 +735,7 @@ theorem pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin
theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
Fin.pred i + 1, Nat.add_lt_add_right h 1 (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
i, h := by
simp only [Fin.ext_iff, val_pred, Nat.add_sub_cancel]
simp only [Fin.ext_iff, coe_pred, Nat.add_sub_cancel]
@[simp] theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
Fin.pred i + 1, h₁ h₂ = i, Nat.lt_of_succ_lt_succ h₁ := pred_mk_succ i _
@@ -803,13 +762,10 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by
rw [Fin.ext_iff, val_pred, val_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
rw [Fin.ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
exact Nat.add_lt_add_right h 1
@[simp, grind =] theorem val_subNat (i : Fin (n + m)) (h : m i) : (i.subNat m h : Nat) = i - m := rfl
@[deprecated val_subNat (since := "2025-11-21")]
theorem coe_subNat (i : Fin (n + m)) (h : m i) : (i.subNat m h : Nat) = i - m := rfl
@[simp] theorem coe_subNat (i : Fin (n + m)) (h : m i) : (i.subNat m h : Nat) = i - m := rfl
@[simp] theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m i) :
subNat m i, h₁ h₂ = i - m, Nat.sub_lt_right_of_lt_add h₂ h₁ := rfl
@@ -874,11 +830,11 @@ step. `Fin.succRec` is a version of this induction principle that takes the `Fin
(zero : n, motive (n + 1) 0) (succ : n i, motive n i motive (Nat.succ n) i.succ) :
motive n i := i.succRec zero succ
@[simp, grind =] theorem succRecOn_zero {motive : n, Fin n Sort _} {zero succ} (n) :
@[simp] theorem succRecOn_zero {motive : n, Fin n Sort _} {zero succ} (n) :
@Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by
cases n <;> rfl
@[simp, grind =] theorem succRecOn_succ {motive : n, Fin n Sort _} {zero succ} {n} (i : Fin n) :
@[simp] theorem succRecOn_succ {motive : n, Fin n Sort _} {zero succ} {n} (i : Fin n) :
@Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
cases i; rfl
@@ -906,11 +862,11 @@ where
| 0, hi => by rwa [Fin.mk_zero]
| i+1, hi => succ i, Nat.lt_of_succ_lt_succ hi (go i (Nat.lt_of_succ_lt hi))
@[simp, grind =] theorem induction_zero {motive : Fin (n + 1) Sort _} (zero : motive 0)
@[simp] theorem induction_zero {motive : Fin (n + 1) Sort _} (zero : motive 0)
(hs : i : Fin n, motive (castSucc i) motive i.succ) :
(induction zero hs : i : Fin (n + 1), motive i) 0 = zero := rfl
@[simp, grind =] theorem induction_succ {motive : Fin (n + 1) Sort _} (zero : motive 0)
@[simp] theorem induction_succ {motive : Fin (n + 1) Sort _} (zero : motive 0)
(succ : i : Fin n, motive (castSucc i) motive i.succ) (i : Fin n) :
induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := rfl
@@ -942,13 +898,13 @@ The corresponding induction principle is `Fin.induction`.
(zero : motive 0) (succ : i : Fin n, motive i.succ) :
i : Fin (n + 1), motive i := induction zero fun i _ => succ i
@[simp, grind =] theorem cases_zero {n} {motive : Fin (n + 1) Sort _} {zero succ} :
@[simp] theorem cases_zero {n} {motive : Fin (n + 1) Sort _} {zero succ} :
@Fin.cases n motive zero succ 0 = zero := rfl
@[simp, grind =] theorem cases_succ {n} {motive : Fin (n + 1) Sort _} {zero succ} (i : Fin n) :
@[simp] theorem cases_succ {n} {motive : Fin (n + 1) Sort _} {zero succ} (i : Fin n) :
@Fin.cases n motive zero succ i.succ = succ i := rfl
@[simp, grind =] theorem cases_succ' {n} {motive : Fin (n + 1) Sort _} {zero succ}
@[simp] theorem cases_succ' {n} {motive : Fin (n + 1) Sort _} {zero succ}
{i : Nat} (h : i + 1 < n + 1) :
@Fin.cases n motive zero succ i.succ, h = succ i, Nat.lt_of_succ_lt_succ h := rfl
@@ -998,7 +954,7 @@ For the induction:
| j + 1 => go j (by omega) (by omega) (cast j, by omega x)
go _ _ (by omega) last
@[simp, grind =] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) Sort _} {zero succ} :
@[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) Sort _} {zero succ} :
(reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
rw [reverseInduction, reverseInduction.go]; simp
@@ -1015,7 +971,7 @@ private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1)
dsimp only
rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 _; omega)]
@[simp, grind =] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) Sort _} {zero succ}
@[simp] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) Sort _} {zero succ}
(i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
succ i (reverseInduction zero succ i.succ) := by
rw [reverseInduction, reverseInduction_castSucc_aux _ _ _ i.isLt, reverseInduction]
@@ -1034,11 +990,11 @@ The corresponding induction principle is `Fin.reverseInduction`.
(cast : i : Fin n, motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
reverseInduction last (fun i _ => cast i) i
@[simp, grind =] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) Sort _} {last cast} :
@[simp] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) Sort _} {last cast} :
(Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last :=
reverseInduction_last ..
@[simp, grind =] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) Sort _} {last cast}
@[simp] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) Sort _} {last cast}
(i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i :=
reverseInduction_castSucc ..
@@ -1058,11 +1014,11 @@ as `Fin.natAdd m (j : Fin n)`.
if hi : (i : Nat) < m then (castAdd_castLT n i hi) (left (castLT i hi))
else (natAdd_subNat_cast (Nat.le_of_not_lt hi)) (right _)
@[simp, grind =] theorem addCases_left {m n : Nat} {motive : Fin (m + n) Sort _} {left right} (i : Fin m) :
@[simp] theorem addCases_left {m n : Nat} {motive : Fin (m + n) Sort _} {left right} (i : Fin m) :
addCases (motive := motive) left right (Fin.castAdd n i) = left i := by
rw [addCases, dif_pos (castAdd_lt _ _)]; rfl
@[simp, grind =]
@[simp]
theorem addCases_right {m n : Nat} {motive : Fin (m + n) Sort _} {left right} (i : Fin n) :
addCases (motive := motive) left right (natAdd m i) = right i := by
have : ¬(natAdd m i : Nat) < m := Nat.not_lt.2 (le_coe_natAdd ..)
@@ -1095,7 +1051,6 @@ theorem add_ofNat [NeZero n] (x : Fin n) (y : Nat) :
/-! ### sub -/
@[deprecated val_sub (since := "2025-11-21")]
protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by
cases a; cases b; rfl
@@ -1147,7 +1102,6 @@ theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b
/-! ### neg -/
@[grind =]
theorem val_neg {n : Nat} [NeZero n] (x : Fin n) :
(-x).val = if x = 0 then 0 else n - x.val := by
change (n - x) % n = _
@@ -1163,7 +1117,7 @@ protected theorem sub_eq_add_neg {n : Nat} (x y : Fin n) : x - y = x + -y := by
apply elim0 x
· replace h : NeZero n := h
ext
rw [Fin.val_sub, Fin.val_add, val_neg]
rw [Fin.coe_sub, Fin.val_add, val_neg]
split
· simp_all
· simp [Nat.add_comm]
@@ -1184,6 +1138,9 @@ theorem mul_ofNat [NeZero n] (x : Fin n) (y : Nat) :
@[deprecated mul_ofNat (since := "2025-05-28")] abbrev mul_ofNat' := @mul_ofNat
theorem val_mul {n : Nat} : a b : Fin n, (a * b).val = a.val * b.val % n
| _, _, _, _ => rfl
@[deprecated val_mul (since := "2025-10-26")]
theorem coe_mul {n : Nat} : a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
| _, _, _, _ => rfl

View File

@@ -129,7 +129,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatA
| ForInStep.yield b => loop i (Nat.le_of_lt h') b
loop as.size (Nat.le_refl _) b
instance [Monad m] : ForIn m FloatArray Float where
instance : ForIn m FloatArray Float where
forIn := FloatArray.forIn
/-- See comment at `forInUnsafe` -/

View File

@@ -7,7 +7,7 @@ module
prelude
public import Init.Data.Array.Basic
import Init.Data.String.Search
import Init.Data.String.Basic
public section
@@ -47,7 +47,7 @@ Converts a string to a pretty-printer document, replacing newlines in the string
`Std.Format.line`.
-/
def String.toFormat (s : String) : Std.Format :=
Std.Format.joinSep (s.split '\n').toList Std.Format.line
Std.Format.joinSep (s.splitOn "\n") Std.Format.line
instance : ToFormat String.Pos.Raw where
format p := format p.byteIdx

View File

@@ -392,9 +392,9 @@ Examples:
* `(0 : Int) ^ 10 = 0`
* `(-7 : Int) ^ 3 = -343`
-/
protected def pow : Int Nat Int
| (m : Nat), n => Int.ofNat (m ^ n)
| m@-[_+1], n => if n % 2 = 0 then Int.ofNat (m.natAbs ^ n) else - Int.ofNat (m.natAbs ^ n)
protected def pow (m : Int) : Nat Int
| 0 => 1
| succ n => Int.pow m n * m
instance : NatPow Int where
pow := Int.pow

View File

@@ -24,17 +24,12 @@ theorem natCast_shiftRight (n s : Nat) : n >>> s = (n : Int) >>> s := rfl
theorem negSucc_shiftRight (m n : Nat) :
-[m+1] >>> n = -[m >>>n +1] := rfl
@[grind _=_]
theorem shiftRight_add (i : Int) (m n : Nat) :
i >>> (m + n) = i >>> m >>> n := by
simp only [shiftRight_eq, Int.shiftRight]
cases i <;> simp [Nat.shiftRight_add]
grind_pattern shiftRight_add => i >>> (m + n) where
i =/= 0
grind_pattern shiftRight_add => i >>> m >>> n where
i =/= 0
theorem shiftRight_eq_div_pow (m : Int) (n : Nat) :
m >>> n = m / ((2 ^ n) : Nat) := by
simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow]

View File

@@ -1781,16 +1781,6 @@ theorem ediv_lt_ediv_iff_of_dvd_of_neg_of_neg {a b c d : Int} (hb : b < 0) (hd :
obtain x, rfl, y, rfl := hba, hdc
simp [*, Int.ne_of_lt, d.mul_assoc, b.mul_comm]
theorem ediv_lt_ediv_of_lt {a b c : Int} (h : a < b) (hcb : c b) (hc : 0 < c) :
a / c < b / c :=
Int.lt_ediv_of_mul_lt (Int.le_of_lt hc) hcb
(Int.lt_of_le_of_lt (Int.ediv_mul_le _ (Int.ne_of_gt hc)) h)
theorem ediv_lt_ediv_of_lt_of_neg {a b c : Int} (h : b < a) (hca : c a) (hc : c < 0) :
a / c < b / c :=
(Int.ediv_lt_iff_of_dvd_of_neg hc hca).2
(Int.lt_of_le_of_lt (Int.mul_ediv_self_le (Int.ne_of_lt hc)) h)
/-! ### `tdiv` and ordering -/
-- Theorems about `tdiv` and ordering, whose `ediv` analogues are in `Bootstrap.lean`.

View File

@@ -377,15 +377,6 @@ protected theorem le_iff_lt_add_one {a b : Int} : a ≤ b ↔ a < b + 1 := by
@[grind =] protected theorem max_def (n m : Int) : max n m = if n m then m else n := rfl
end Int
namespace Lean.Meta.Grind.Lia
scoped grind_pattern Int.min_def => min n m
scoped grind_pattern Int.max_def => max n m
end Lean.Meta.Grind.Lia
namespace Int
@[simp] protected theorem neg_min_neg (a b : Int) : min (-a) (-b) = -max a b := by
rw [Int.min_def, Int.max_def]
simp

View File

@@ -14,20 +14,9 @@ namespace Int
/-! # pow -/
@[simp, norm_cast]
theorem natCast_pow (m n : Nat) : (m ^ n : Nat) = (m : Int) ^ n := rfl
theorem negSucc_pow (m n : Nat) : (-[m+1] : Int) ^ n = if n % 2 = 0 then Int.ofNat (m.succ ^ n) else Int.negOfNat (m.succ ^ n) := rfl
@[simp] protected theorem pow_zero (m : Int) : m ^ 0 = 1 := by cases m <;> simp [ natCast_pow, negSucc_pow]
protected theorem pow_succ (m : Int) (n : Nat) : m ^ n.succ = m ^ n * m := by
rcases m with _ | a
· rfl
· simp only [negSucc_pow, Nat.succ_mod_succ_eq_zero_iff, Nat.reduceAdd, Nat.mod_two_ne_zero,
Nat.pow_succ, ofNat_eq_natCast, @negOfNat_eq (_ * _), ite_not, apply_ite (· * -[a+1]),
ofNat_mul_negSucc, negOfNat_mul_negSucc]
@[simp] protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
rw [Int.mul_comm, Int.pow_succ]
@@ -50,9 +39,6 @@ protected theorem mul_pow {a b : Int} {n : Nat} : (a * b) ^ n = a ^ n * b ^ n :=
rw [Int.pow_succ, Int.pow_succ, Int.pow_succ, ih, Int.mul_assoc, Int.mul_assoc,
Int.mul_left_comm (b^n)]
protected theorem pow_one (a : Int) : a ^ 1 = a := by
rw [Int.pow_succ, Int.pow_zero, Int.one_mul]
protected theorem pow_mul {a : Int} {n m : Nat} : a ^ (n * m) = (a ^ n) ^ m := by
induction m with
| zero => simp
@@ -62,27 +48,26 @@ protected theorem pow_mul {a : Int} {n m : Nat} : a ^ (n * m) = (a ^ n) ^ m := b
protected theorem pow_pos {n : Int} {m : Nat} : 0 < n 0 < n ^ m := by
induction m with
| zero => simp
| succ m ih =>
simp only [Int.pow_succ]
exact fun h => Int.mul_pos (ih h) h
| succ m ih => exact fun h => Int.mul_pos (ih h) h
protected theorem pow_nonneg {n : Int} {m : Nat} : 0 n 0 n ^ m := by
induction m with
| zero => simp
| succ m ih =>
simp only [Int.pow_succ]
exact fun h => Int.mul_nonneg (ih h) h
| succ m ih => exact fun h => Int.mul_nonneg (ih h) h
protected theorem pow_ne_zero {n : Int} {m : Nat} : n 0 n ^ m 0 := by
induction m with
| zero => simp
| succ m ih =>
simp only [Int.pow_succ]
exact fun h => Int.mul_ne_zero (ih h) h
| succ m ih => exact fun h => Int.mul_ne_zero (ih h) h
instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := Int.pow_ne_zero (NeZero.ne _)
instance {n : Int} : NeZero (n^0) := by simp
@[simp, norm_cast]
protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
match n with
| 0 => rfl
| n + 1 =>
simp only [Nat.pow_succ, Int.pow_succ, Int.natCast_mul, Int.natCast_pow _ n]
@[simp]
protected theorem two_pow_pred_sub_two_pow {w : Nat} (h : 0 < w) :
@@ -105,7 +90,7 @@ theorem pow_lt_pow_of_lt {a : Int} {b c : Nat} (ha : 1 < a) (hbc : b < c):
omega
@[simp] theorem natAbs_pow (n : Int) : (k : Nat) (n ^ k).natAbs = n.natAbs ^ k
| 0 => by simp
| 0 => rfl
| k + 1 => by rw [Int.pow_succ, natAbs_mul, natAbs_pow, Nat.pow_succ]
theorem toNat_pow_of_nonneg {x : Int} (h : 0 x) (k : Nat) : (x ^ k).toNat = x.toNat ^ k := by
@@ -115,7 +100,8 @@ theorem toNat_pow_of_nonneg {x : Int} (h : 0 ≤ x) (k : Nat) : (x ^ k).toNat =
rw [Int.pow_succ, Int.toNat_mul (Int.pow_nonneg h) h, ih, Nat.pow_succ]
protected theorem sq_nonnneg (m : Int) : 0 m ^ 2 := by
rw [Int.pow_succ, Int.pow_one]
change 0 1 * m * m
rw [Int.one_mul]
cases m
· apply Int.mul_nonneg <;> simp
· apply Int.mul_nonneg_of_nonpos_of_nonpos <;> exact negSucc_le_zero _
@@ -131,4 +117,25 @@ protected theorem neg_pow {m : Int} {n : Nat} : (-m)^n = (-1)^(n % 2) * m^n := b
rw [Int.pow_add, Int.pow_mul]
simp [Int.one_pow]
/-- The runtime behaviour of `Int.pow` is slow, so we replace it via a `@[csimp]` lemma. -/
def powImp (m : Int) (n : Nat) : Int :=
if m 0 n % 2 = 0 then
Int.ofNat <| m.natAbs ^ n
else
- (Int.ofNat <| m.natAbs ^ n)
@[csimp]
theorem pow_eq_powImp : @Int.pow = @powImp := by
funext m n
change m^n = _
dsimp [powImp]
split <;> rename_i h
· rcases h with (h | h)
· simp [ofNat_natAbs_of_nonneg h]
· rw [ natAbs_pow, ofNat_natAbs_of_nonneg (Int.pow_nonneg_of_even h)]
· simp at h
obtain h₁, h₂ := h
rw [Int.natCast_pow, ofNat_natAbs_of_nonpos (by omega), Int.neg_pow, h₂]
simp
end Int

View File

@@ -9,7 +9,6 @@ prelude
public import Init.Data.Iterators.Basic
public import Init.Data.Iterators.PostconditionMonad
public import Init.Data.Iterators.Consumers
public import Init.Data.Iterators.Producers
public import Init.Data.Iterators.Combinators
public import Init.Data.Iterators.Lemmas
public import Init.Data.Iterators.ToIterator

View File

@@ -678,7 +678,6 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
`it.finitelyManySteps` as a termination measure.
-/
class Finite (α : Type w) (m : Type w Type w') {β : Type w} [Iterator α m β] : Prop where
/-- The relation of plausible successors is well-founded. -/
wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
theorem Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
@@ -798,7 +797,6 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
`it.finitelyManySkips` as a termination measure.
-/
class Productive (α m) {β} [Iterator α m β] : Prop where
/-- The relation of plausible successors during skips is well-founded. -/
wf : WellFounded (IterM.IsPlausibleSkipSuccessorOf (α := α) (m := m))
/--
@@ -819,24 +817,6 @@ def IterM.TerminationMeasures.Productive.Rel
TerminationMeasures.Productive α m TerminationMeasures.Productive α m Prop :=
Relation.TransGen <| InvImage IterM.IsPlausibleSkipSuccessorOf IterM.TerminationMeasures.Productive.it
theorem IterM.TerminationMeasures.Finite.Rel.of_productive
{α : Type w} {m : Type w Type w'} {β : Type w} [Iterator α m β] {a b : Finite α m} :
Productive.Rel a.it b.it Finite.Rel a b := by
generalize ha' : Productive.mk a.it = a'
generalize hb' : Productive.mk b.it = b'
have ha : a = a'.it := by simp [ ha']
have hb : b = b'.it := by simp [ hb']
rw [ha, hb]
clear ha hb ha' hb' a b
rw [Productive.Rel, Finite.Rel]
intro h
induction h
· rename_i ih
exact .single _, rfl, ih
· rename_i hab ih
refine .trans ih ?_
exact .single _, rfl, hab
instance {α : Type w} {m : Type w Type w'} {β : Type w} [Iterator α m β]
[Productive α m] : WellFoundedRelation (IterM.TerminationMeasures.Productive α m) where
rel := IterM.TerminationMeasures.Productive.Rel

View File

@@ -9,5 +9,4 @@ prelude
public import Init.Data.Iterators.Combinators.Monadic
public import Init.Data.Iterators.Combinators.FilterMap
public import Init.Data.Iterators.Combinators.FlatMap
public import Init.Data.Iterators.Combinators.Take
public import Init.Data.Iterators.Combinators.ULift

View File

@@ -8,5 +8,4 @@ module
prelude
public import Init.Data.Iterators.Combinators.Monadic.FilterMap
public import Init.Data.Iterators.Combinators.Monadic.FlatMap
public import Init.Data.Iterators.Combinators.Monadic.Take
public import Init.Data.Iterators.Combinators.Monadic.ULift

View File

@@ -106,6 +106,16 @@ instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w'
IteratorLoopPartial (Attach α m P) m n :=
.defaultImplementation
instance {α β : Type w} {m : Type w Type w'} [Monad m]
{P : β Prop} [Iterator α m β] [IteratorSize α m] :
IteratorSize (Attach α m P) m where
size it := IteratorSize.size it.internalState.inner
instance {α β : Type w} {m : Type w Type w'} [Monad m]
{P : β Prop} [Iterator α m β] [IteratorSizePartial α m] :
IteratorSizePartial (Attach α m P) m where
size it := IteratorSizePartial.size it.internalState.inner
end Types
/--

View File

@@ -604,4 +604,30 @@ def IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [M
(f : β Bool) (it : IterM (α := α) m β) :=
(it.filterMap (fun b => if f b then some b else none) : IterM m β)
instance {α β γ : Type w} {m : Type w Type w'}
{n : Type w Type w''} [Monad n] [Iterator α m β] {lift : α : Type w m α n α}
{f : β PostconditionT n (Option γ)} [Finite α m] :
IteratorSize (FilterMap α m n lift f) n :=
.defaultImplementation
instance {α β γ : Type w} {m : Type w Type w'}
{n : Type w Type w''} [Monad n] [Iterator α m β] {lift : α : Type w m α n α}
{f : β PostconditionT n (Option γ)} :
IteratorSizePartial (FilterMap α m n lift f) n :=
.defaultImplementation
instance {α β γ : Type w} {m : Type w Type w'}
{n : Type w Type w''} [Monad n] [Iterator α m β]
{lift : α : Type w m α n α}
{f : β PostconditionT n γ} [IteratorSize α m] :
IteratorSize (Map α m n lift f) n where
size it := lift (IteratorSize.size it.internalState.inner)
instance {α β γ : Type w} {m : Type w Type w'}
{n : Type w Type w''} [Monad n] [Iterator α m β]
{lift : α : Type w m α n α}
{f : β PostconditionT n γ} [IteratorSizePartial α m] :
IteratorSizePartial (Map α m n lift f) n where
size it := lift (IteratorSizePartial.size it.internalState.inner)
end Std.Iterators

View File

@@ -1,223 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Nat.Lemmas
public import Init.Data.Iterators.Consumers.Monadic.Collect
public import Init.Data.Iterators.Consumers.Monadic.Loop
public import Init.Data.Iterators.Internal.Termination
@[expose] public section
/-!
This module provides the iterator combinator `IterM.take`.
-/
namespace Std.Iterators
variable {α : Type w} {m : Type w Type w'} {β : Type w}
/--
The internal state of the `IterM.take` iterator combinator.
-/
@[unbox]
structure Take (α : Type w) (m : Type w Type w') {β : Type w} [Iterator α m β] where
/--
Internal implementation detail of the iterator library.
Caution: For `take n`, `countdown` is `n + 1`.
If `countdown` is zero, the combinator only terminates when `inner` terminates.
-/
countdown : Nat
/-- Internal implementation detail of the iterator library -/
inner : IterM (α := α) m β
/--
Internal implementation detail of the iterator library.
This proof term ensures that a `take` always produces a finite iterator from a productive one.
-/
finite : countdown > 0 Finite α m
/--
Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
up to the first `n` of `it`'s values in order and then terminates.
**Marble diagram:**
```text
it ---a----b---c--d-e--
it.take 3 ---a----b---c⊥
it ---a--
it.take 3 ---a--
```
**Termination properties:**
* `Finite` instance: only if `it` is productive
* `Productive` instance: only if `it` is productive
**Performance:**
This combinator incurs an additional O(1) cost with each output of `it`.
-/
@[always_inline, inline]
def IterM.take [Iterator α m β] (n : Nat) (it : IterM (α := α) m β) :=
toIterM (Take.mk (n + 1) it (Or.inl <| Nat.zero_lt_succ _)) m β
/--
This combinator is only useful for advanced use cases.
Given a finite iterator `it`, returns an iterator that behaves exactly like `it` but is of the same
type as `it.take n`.
**Marble diagram:**
```text
it ---a----b---c--d-e--
it.toTake ---a----b---c--d-e--
```
**Termination properties:**
* `Finite` instance: always
* `Productive` instance: always
**Performance:**
This combinator incurs an additional O(1) cost with each output of `it`.
-/
@[always_inline, inline]
def IterM.toTake [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) :=
toIterM (Take.mk 0 it (Or.inr inferInstance)) m β
theorem IterM.take.surjective_of_zero_lt {α : Type w} {m : Type w Type w'} {β : Type w}
[Iterator α m β] (it : IterM (α := Take α m) m β) (h : 0 < it.internalState.countdown) :
(it₀ : IterM (α := α) m β) (k : Nat), it = it₀.take k := by
refine it.internalState.inner, it.internalState.countdown - 1, ?_
simp only [take, Nat.sub_add_cancel (m := 1) (n := it.internalState.countdown) (by omega)]
rfl
inductive Take.PlausibleStep [Iterator α m β] (it : IterM (α := Take α m) m β) :
(step : IterStep (IterM (α := Take α m) m β) β) Prop where
| yield : {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out)
(h : it.internalState.countdown 1) PlausibleStep it (.yield it.internalState.countdown - 1, it', it.internalState.finite.imp_left (by omega) out)
| skip : {it'}, it.internalState.inner.IsPlausibleStep (.skip it')
it.internalState.countdown 1 PlausibleStep it (.skip it.internalState.countdown, it', it.internalState.finite)
| done : it.internalState.inner.IsPlausibleStep .done PlausibleStep it .done
| depleted : it.internalState.countdown = 1
PlausibleStep it .done
@[always_inline, inline]
instance Take.instIterator [Monad m] [Iterator α m β] : Iterator (Take α m) m β where
IsPlausibleStep := Take.PlausibleStep
step it :=
if h : it.internalState.countdown = 1 then
pure <| .deflate <| .done (.depleted h)
else do
match ( it.internalState.inner.step).inflate with
| .yield it' out h' =>
pure <| .deflate <| .yield it.internalState.countdown - 1, it', (it.internalState.finite.imp_left (by omega)) out (.yield h' h)
| .skip it' h' => pure <| .deflate <| .skip it.internalState.countdown, it', it.internalState.finite (.skip h' h)
| .done h' => pure <| .deflate <| .done (.done h')
def Take.Rel (m : Type w Type w') [Monad m] [Iterator α m β] [Productive α m] :
IterM (α := Take α m) m β IterM (α := Take α m) m β Prop :=
open scoped Classical in
if _ : Finite α m then
InvImage (Prod.Lex Nat.lt_wfRel.rel IterM.TerminationMeasures.Finite.Rel)
(fun it => (it.internalState.countdown, it.internalState.inner.finitelyManySteps))
else
InvImage (Prod.Lex Nat.lt_wfRel.rel IterM.TerminationMeasures.Productive.Rel)
(fun it => (it.internalState.countdown, it.internalState.inner.finitelyManySkips))
theorem Take.rel_of_countdown [Monad m] [Iterator α m β] [Productive α m]
{it it' : IterM (α := Take α m) m β}
(h : it'.internalState.countdown < it.internalState.countdown) : Take.Rel m it' it := by
simp only [Rel]
split <;> exact Prod.Lex.left _ _ h
theorem Take.rel_of_inner [Monad m] [Iterator α m β] [Productive α m] {remaining : Nat}
{it it' : IterM (α := α) m β}
(h : it'.finitelyManySkips.Rel it.finitelyManySkips) :
Take.Rel m (it'.take remaining) (it.take remaining) := by
simp only [Rel]
split
· exact Prod.Lex.right _ (.of_productive h)
· exact Prod.Lex.right _ h
theorem Take.rel_of_zero_of_inner [Monad m] [Iterator α m β]
{it it' : IterM (α := Take α m) m β}
(h : it.internalState.countdown = 0) (h' : it'.internalState.countdown = 0)
(h'' : haveI := it.internalState.finite.resolve_left (by omega); it'.internalState.inner.finitelyManySteps.Rel it.internalState.inner.finitelyManySteps) :
haveI := it.internalState.finite.resolve_left (by omega)
Take.Rel m it' it := by
haveI := it.internalState.finite.resolve_left (by omega)
simp only [Rel, this, reduceDIte, InvImage, h, h']
exact Prod.Lex.right _ h''
private def Take.instFinitenessRelation [Monad m] [Iterator α m β]
[Productive α m] :
FinitenessRelation (Take α m) m where
rel := Take.Rel m
wf := by
rw [Rel]
split
all_goals
apply InvImage.wf
refine fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b
· exact WellFoundedRelation.wf
· exact WellFoundedRelation.wf
subrelation {it it'} h := by
obtain step, h, h' := h
cases h'
case yield it' out k h' h'' =>
cases h
cases it.internalState.finite
· apply rel_of_countdown
simp only
omega
· by_cases h : it.internalState.countdown = 0
· simp only [h, Nat.zero_le, Nat.sub_eq_zero_of_le]
apply rel_of_zero_of_inner h rfl
exact .single _, rfl, h'
· apply rel_of_countdown
simp only
omega
case skip it' out k h' h'' =>
cases h
by_cases h : it.internalState.countdown = 0
· simp only [h]
apply Take.rel_of_zero_of_inner h rfl
exact .single _, rfl, h'
· obtain it, k, rfl := IterM.take.surjective_of_zero_lt it (by omega)
apply Take.rel_of_inner
exact IterM.TerminationMeasures.Productive.rel_of_skip h'
case done _ =>
cases h
case depleted _ =>
cases h
instance Take.instFinite [Monad m] [Iterator α m β] [Productive α m] :
Finite (Take α m) m :=
by exact Finite.of_finitenessRelation instFinitenessRelation
instance Take.instIteratorCollect {n : Type w Type w'} [Monad m] [Monad n] [Iterator α m β] :
IteratorCollect (Take α m) m n :=
.defaultImplementation
instance Take.instIteratorCollectPartial {n : Type w Type w'} [Monad m] [Monad n] [Iterator α m β] :
IteratorCollectPartial (Take α m) m n :=
.defaultImplementation
instance Take.instIteratorLoop {n : Type x Type x'} [Monad m] [Monad n] [Iterator α m β] :
IteratorLoop (Take α m) m n :=
.defaultImplementation
instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] :
IteratorLoopPartial (Take α m) m n :=
.defaultImplementation
end Std.Iterators

View File

@@ -74,7 +74,7 @@ variable {α : Type u} {m : Type u → Type u'} {n : Type max u v → Type v'}
/--
Transforms a step of the base iterator into a step of the `uLift` iterator.
-/
@[always_inline, inline, expose]
@[always_inline, inline]
def Types.ULiftIterator.Monadic.modifyStep (step : IterStep (IterM (α := α) m β) β) :
IterStep (IterM (α := ULiftIterator.{v} α m n β lift) n (ULift.{v} β)) (ULift.{v} β) :=
match step with
@@ -140,6 +140,15 @@ instance Types.ULiftIterator.instIteratorCollectPartial {o} [Monad n] [Monad o]
IteratorCollectPartial (ULiftIterator α m n β lift) n o :=
.defaultImplementation
instance Types.ULiftIterator.instIteratorSize [Monad n] [Iterator α m β] [IteratorSize α m]
[Finite (ULiftIterator α m n β lift) n] :
IteratorSize (ULiftIterator α m n β lift) n :=
.defaultImplementation
instance Types.ULiftIterator.instIteratorSizePartial [Monad n] [Iterator α m β] [IteratorSize α m] :
IteratorSizePartial (ULiftIterator α m n β lift) n :=
.defaultImplementation
/--
Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with
values in `ULift β`. Requires a `MonadLift m (ULiftT n)` instance.

View File

@@ -1,70 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Iterators.Combinators.Monadic.Take
@[expose] public section
namespace Std.Iterators
/--
Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
up to the first `n` of `it`'s values in order and then terminates.
**Marble diagram:**
```text
it ---a----b---c--d-e--
it.take 3 ---a----b---c⊥
it ---a--
it.take 3 ---a--
```
**Termination properties:**
* `Finite` instance: only if `it` is productive
* `Productive` instance: only if `it` is productive
**Performance:**
This combinator incurs an additional O(1) cost with each output of `it`.
-/
@[always_inline, inline]
def Iter.take {α : Type w} {β : Type w} [Iterator α Id β] (n : Nat) (it : Iter (α := α) β) :
Iter (α := Take α Id) β :=
it.toIterM.take n |>.toIter
/--
This combinator is only useful for advanced use cases.
Given a finite iterator `it`, returns an iterator that behaves exactly like `it` but is of the same
type as `it.take n`.
**Marble diagram:**
```text
it ---a----b---c--d-e--
it.toTake ---a----b---c--d-e--
```
**Termination properties:**
* `Finite` instance: always
* `Productive` instance: always
**Performance:**
This combinator incurs an additional O(1) cost with each output of `it`.
-/
@[always_inline, inline]
def Iter.toTake {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) :
Iter (α := Take α Id) β :=
it.toIterM.toTake.toIter
end Std.Iterators

View File

@@ -9,8 +9,6 @@ prelude
public import Init.Data.Iterators.Consumers.Collect
public import Init.Data.Iterators.Consumers.Monadic.Loop
set_option linter.missingDocs true
public section
/-!
@@ -48,9 +46,6 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
haveI : ForIn' n (Iter (α := α) β) β _ := Iter.instForIn'
instForInOfForIn'
/--
An implementation of `for h : ... in ... do ...` notation for partial iterators.
-/
@[always_inline, inline]
def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x Type x'} [Monad n]
[Iterator α Id β] [IteratorLoopPartial α Id n] :
@@ -68,12 +63,12 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
instForInOfForIn'
instance {m : Type x Type x'}
{α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] [Monad m] :
{α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] :
ForM m (Iter (α := α) β) β where
forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
instance {m : Type x Type x'}
{α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] [Monad m] :
{α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] :
ForM m (Iter.Partial (α := α) β) β where
forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
@@ -207,11 +202,6 @@ def Iter.all {α β : Type w}
(p : β Bool) (it : Iter (α := α) β) : Bool :=
(it.allM (fun x => pure (f := Id) (p x))).run
/--
Steps through the iterator until the monadic function `f` returns `some` for an element, at which
point iteration stops and the result of `f` is returned. If the iterator is completely consumed
without `f` returning `some`, then the result is `none`.
-/
@[inline]
def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x Type w'} [Monad m] [Iterator α Id β]
[IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β m (Option γ)) :
@@ -221,7 +211,7 @@ def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Mon
| none => return .yield none
| some fx => return .done (some fx))
@[inline, inherit_doc Iter.findSomeM?]
@[inline]
def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x Type w'} [Monad m]
[Iterator α Id β] [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β)
(f : β m (Option γ)) :
@@ -231,100 +221,62 @@ def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type
| none => return .yield none
| some fx => return .done (some fx))
/--
Steps through the iterator until `f` returns `some` for an element, at which point iteration stops
and the result of `f` is returned. If the iterator is completely consumed without `f` returning
`some`, then the result is `none`.
-/
@[inline]
def Iter.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id Id] [Finite α Id] (it : Iter (α := α) β) (f : β Option γ) :
Option γ :=
Id.run (it.findSomeM? (pure <| f ·))
@[inline, inherit_doc Iter.findSome?]
@[inline]
def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoopPartial α Id Id] (it : Iter.Partial (α := α) β) (f : β Option γ) :
Option γ :=
Id.run (it.findSomeM? (pure <| f ·))
/--
Steps through the iterator until an element satisfies the monadic predicate `f`, at which point
iteration stops and the element is returned. If no element satisfies `f`, then the result is
`none`.
-/
@[inline]
def Iter.findM? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α Id β]
[IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β m (ULift Bool)) :
m (Option β) :=
it.findSomeM? (fun x => return if ( f x).down then some x else none)
@[inline, inherit_doc Iter.findM?]
@[inline]
def Iter.Partial.findM? {α β : Type w} {m : Type w Type w'} [Monad m] [Iterator α Id β]
[IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β) (f : β m (ULift Bool)) :
m (Option β) :=
it.findSomeM? (fun x => return if ( f x).down then some x else none)
/--
Steps through the iterator until an element satisfies `f`, at which point iteration stops and the
element is returned. If no element satisfies `f`, then the result is `none`.
-/
@[inline]
def Iter.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
[Finite α Id] (it : Iter (α := α) β) (f : β Bool) : Option β :=
Id.run (it.findM? (pure <| .up <| f ·))
@[inline, inherit_doc Iter.find?]
@[inline]
def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
(it : Iter.Partial (α := α) β) (f : β Bool) : Option β :=
Id.run (it.findM? (pure <| .up <| f ·))
/--
Steps through the whole iterator, counting the number of outputs emitted.
**Performance**:
This function's runtime is linear in the number of steps taken by the iterator.
-/
@[always_inline, inline, expose]
def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
@[always_inline, inline, expose, inherit_doc IterM.size]
def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
(it : Iter (α := α) β) : Nat :=
it.toIterM.count.run.down
(IteratorSize.size it.toIterM).run.down
/--
Steps through the whole iterator, counting the number of outputs emitted.
**Performance**:
This function's runtime is linear in the number of steps taken by the iterator.
-/
@[always_inline, inline, expose, deprecated Iter.count (since := "2025-10-29")]
def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
@[always_inline, inline, inherit_doc IterM.Partial.size]
def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id]
(it : Iter (α := α) β) : Nat :=
it.count
(IteratorSizePartial.size it.toIterM).run.down
/--
Steps through the whole iterator, counting the number of outputs emitted.
`LawfulIteratorSize α m` ensures that the `size` function of an iterator behaves as if it
iterated over the whole iterator, counting its elements and causing all the monadic side effects
of the iterations. This is a fairly strong condition for monadic iterators and it will be false
for many efficient implementations of `size` that compute the size without actually iterating.
**Performance**:
This function's runtime is linear in the number of steps taken by the iterator.
This class is experimental and users of the iterator API should not explicitly depend on it.
-/
@[always_inline, inline, expose]
def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
(it : Iter.Partial (α := α) β) : Nat :=
it.it.toIterM.allowNontermination.count.run.down
/--
Steps through the whole iterator, counting the number of outputs emitted.
**Performance**:
This function's runtime is linear in the number of steps taken by the iterator.
-/
@[always_inline, inline, expose, deprecated Iter.Partial.count (since := "2025-10-29")]
def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
(it : Iter.Partial (α := α) β) : Nat :=
it.count
class LawfulIteratorSize (α : Type w) {β : Type w} [Iterator α Id β] [Finite α Id]
[IteratorSize α Id] where
size_eq_size_toArray {it : Iter (α := α) β} : it.size =
haveI : IteratorCollect α Id Id := .defaultImplementation
it.toArray.size
end Std.Iterators

View File

@@ -88,6 +88,27 @@ class IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [
(it : IterM (α := α) m β) γ
((b : β) it.IsPlausibleIndirectOutput b (c : γ) n (ForInStep γ)) n γ
/--
`IteratorSize α m` provides an implementation of the `IterM.size` function.
This class is experimental and users of the iterator API should not explicitly depend on it.
They can, however, assume that consumers that require an instance will work for all iterators
provided by the standard library.
-/
class IteratorSize (α : Type w) (m : Type w Type w') {β : Type w} [Iterator α m β] where
size : IterM (α := α) m β m (ULift Nat)
/--
`IteratorSizePartial α m` provides an implementation of the `IterM.Partial.size` function that
can be used as `it.allowTermination.size`.
This class is experimental and users of the iterator API should not explicitly depend on it.
They can, however, assume that consumers that require an instance will work for all iterators
provided by the standard library.
-/
class IteratorSizePartial (α : Type w) (m : Type w Type w') {β : Type w} [Iterator α m β] where
size : IterM (α := α) m β m (ULift Nat)
end Typeclasses
/-- Internal implementation detail of the iterator library. -/
@@ -247,10 +268,10 @@ This `ForIn'`-style loop construct traverses a finite iterator using an `Iterato
-/
@[always_inline, inline]
def IteratorLoop.finiteForIn' {m : Type w Type w'} {n : Type x Type x'}
{α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
{α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
(lift : γ δ, (γ n δ) m γ n δ) :
ForIn' n (IterM (α := α) m β) β fun it out => it.IsPlausibleIndirectOutput out where
forIn' {γ} it init f :=
forIn' {γ} [Monad n] it init f :=
IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
wellFounded_of_finite
it init (fun out h acc => (·, .intro) <$> f out h acc)
@@ -288,13 +309,13 @@ instance {m : Type w → Type w'} {n : Type w → Type w''}
instForInOfForIn'
instance {m : Type w Type w'} {n : Type w Type w''}
{α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
{α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
[MonadLiftT m n] :
ForM n (IterM (α := α) m β) β where
forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
instance {m : Type w Type w'} {n : Type w Type w''}
{α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [Monad n]
{α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoopPartial α m n]
[MonadLiftT m n] :
ForM n (IterM.Partial (α := α) m β) β where
forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
@@ -612,58 +633,86 @@ def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Ite
m (Option β) :=
it.findM? (pure <| .up <| f ·)
section Count
section Size
/--
Steps through the whole iterator, counting the number of outputs emitted.
**Performance**:
This function's runtime is linear in the number of steps taken by the iterator.
This is the implementation of the default instance `IteratorSize.defaultImplementation`.
-/
@[always_inline, inline]
def IterM.count {α : Type w} {m : Type w Type w'} {β : Type w} [Iterator α m β] [Finite α m]
[IteratorLoop α m m]
[Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
def IterM.DefaultConsumers.size {α : Type w} {m : Type w Type w'} [Monad m] {β : Type w}
[Iterator α m β] [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) :
m (ULift Nat) :=
it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
/--
Steps through the whole iterator, counting the number of outputs emitted.
**Performance**:
This function's runtime is linear in the number of steps taken by the iterator.
-/
@[always_inline, inline, deprecated IterM.count (since := "2025-10-29")]
def IterM.size {α : Type w} {m : Type w Type w'} {β : Type w} [Iterator α m β] [Finite α m]
[IteratorLoop α m m]
[Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
it.count
/--
Steps through the whole iterator, counting the number of outputs emitted.
**Performance**:
This function's runtime is linear in the number of steps taken by the iterator.
This is the implementation of the default instance `IteratorSizePartial.defaultImplementation`.
-/
@[always_inline, inline]
def IterM.Partial.count {α : Type w} {m : Type w Type w'} {β : Type w} [Iterator α m β]
[IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
def IterM.DefaultConsumers.sizePartial {α : Type w} {m : Type w Type w'} [Monad m] {β : Type w}
[Iterator α m β] [IteratorLoopPartial α m m] (it : IterM (α := α) m β) :
m (ULift Nat) :=
it.allowNontermination.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
/--
Steps through the whole iterator, counting the number of outputs emitted.
This is the default implementation of the `IteratorSize` class.
It simply iterates using `IteratorLoop` and counts the elements.
For certain iterators, more efficient implementations are possible and should be used instead.
-/
@[always_inline, inline]
def IteratorSize.defaultImplementation {α β : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [Finite α m] [IteratorLoop α m m] :
IteratorSize α m where
size := IterM.DefaultConsumers.size
/--
This is the default implementation of the `IteratorSizePartial` class.
It simply iterates using `IteratorLoopPartial` and counts the elements.
For certain iterators, more efficient implementations are possible and should be used instead.
-/
@[always_inline, inline]
instance IteratorSizePartial.defaultImplementation {α β : Type w} {m : Type w Type w'} [Monad m]
[Iterator α m β] [IteratorLoopPartial α m m] :
IteratorSizePartial α m where
size := IterM.DefaultConsumers.sizePartial
/--
Computes how many elements the iterator returns. In monadic situations, it is unclear which effects
are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the
returned value should be. The reference implementation, `IteratorSize.defaultImplementation`,
simply iterates over the whole iterator monadically, counting the number of emitted values.
An `IteratorSize` instance is considered lawful if it is equal to the reference implementation.
**Performance**:
This function's runtime is linear in the number of steps taken by the iterator.
Default performance is linear in the number of steps taken by the iterator.
-/
@[always_inline, inline, deprecated IterM.Partial.count (since := "2025-10-29")]
def IterM.Partial.size {α : Type w} {m : Type w Type w'} {β : Type w} [Iterator α m β]
[IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
it.count
@[always_inline, inline]
def IterM.size {α : Type} {m : Type Type w'} {β : Type} [Iterator α m β] [Monad m]
(it : IterM (α := α) m β) [IteratorSize α m] : m Nat :=
ULift.down <$> IteratorSize.size it
end Count
/--
Computes how many elements the iterator emits.
With monadic iterators (`IterM`), it is unclear which effects
are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the
returned value should be. The reference implementation, `IteratorSize.defaultImplementation`,
simply iterates over the whole iterator monadically, counting the number of emitted values.
An `IteratorSize` instance is considered lawful if it is equal to the reference implementation.
This is the partial version of `size`. It does not require a proof of finiteness and might loop
forever. It is not possible to verify the behavior in Lean because it uses `partial`.
**Performance**:
Default performance is linear in the number of steps taken by the iterator.
-/
@[always_inline, inline]
def IterM.Partial.size {α : Type} {m : Type Type w'} {β : Type} [Iterator α m β] [Monad m]
(it : IterM.Partial (α := α) m β) [IteratorSizePartial α m] : m Nat :=
ULift.down <$> IteratorSizePartial.size it.it
end Size
end Std.Iterators

View File

@@ -8,4 +8,3 @@ module
prelude
public import Init.Data.Iterators.Lemmas.Consumers
public import Init.Data.Iterators.Lemmas.Combinators
public import Init.Data.Iterators.Lemmas.Producers

View File

@@ -10,5 +10,4 @@ public import Init.Data.Iterators.Lemmas.Combinators.Attach
public import Init.Data.Iterators.Lemmas.Combinators.Monadic
public import Init.Data.Iterators.Lemmas.Combinators.FilterMap
public import Init.Data.Iterators.Lemmas.Combinators.FlatMap
public import Init.Data.Iterators.Lemmas.Combinators.Take
public import Init.Data.Iterators.Lemmas.Combinators.ULift

View File

@@ -11,7 +11,6 @@ import all Init.Data.Iterators.Combinators.Attach
import all Init.Data.Iterators.Combinators.Monadic.Attach
public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
public import Init.Data.Iterators.Lemmas.Consumers.Collect
public import Init.Data.Iterators.Lemmas.Consumers.Loop
public import Init.Data.Array.Attach
public section
@@ -83,14 +82,4 @@ theorem Iter.toArray_attachWith [Iterator α Id β]
simpa only [Array.toList_inj]
simp [Iter.toList_toArray]
@[simp]
theorem Iter.count_attachWith [Iterator α Id β]
{it : Iter (α := α) β} {hP}
[Finite α Id] [IteratorLoop α Id Id]
[LawfulIteratorLoop α Id Id] :
(it.attachWith P hP).count = it.count := by
letI : IteratorCollect α Id Id := .defaultImplementation
rw [ Iter.length_toList_eq_count, toList_attachWith]
simp
end Std.Iterators

View File

@@ -467,17 +467,6 @@ theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
end Fold
section Count
@[simp]
theorem Iter.count_map {α β β' : Type w} [Iterator α Id β]
[IteratorLoop α Id Id] [Finite α Id] [LawfulIteratorLoop α Id Id]
{it : Iter (α := α) β} {f : β β'} :
(it.map f).count = it.count := by
simp [map_eq_toIter_map_toIterM, count_eq_count_toIterM]
end Count
theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w Type w'}
[Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
{it : Iter (α := α) β} {f : β m (Option β')} {p : β' m (ULift Bool)} :

View File

@@ -9,5 +9,4 @@ prelude
public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift

View File

@@ -9,7 +9,6 @@ prelude
public import Init.Data.Iterators.Combinators.Monadic.Attach
import all Init.Data.Iterators.Combinators.Monadic.Attach
public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
public section
@@ -60,14 +59,4 @@ theorem IterM.map_unattach_toArray_attachWith [Iterator α m β] [Monad m] [Mona
rw [ toArray_toList, toArray_toList, map_unattach_toList_attachWith (it := it) (hP := hP)]
simp [-map_unattach_toList_attachWith, -IterM.toArray_toList]
@[simp]
theorem IterM.count_attachWith [Iterator α m β] [Monad m] [Monad n]
{it : IterM (α := α) m β} {hP}
[Finite α m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] :
(it.attachWith P hP).count = it.count := by
letI : IteratorCollect α m m := .defaultImplementation
rw [ up_length_toList_eq_count, up_length_toList_eq_count,
map_unattach_toList_attachWith (it := it) (P := P) (hP := hP)]
simp only [Functor.map_map, List.length_unattach]
end Std.Iterators

View File

@@ -895,23 +895,6 @@ theorem IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'}
end Fold
section Count
@[simp]
theorem IterM.count_map {α β β' : Type w} {m : Type w Type w'} [Iterator α m β] [Monad m]
[IteratorLoop α m m] [Finite α m] [LawfulMonad m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} {f : β β'} :
(it.map f).count = it.count := by
induction it using IterM.inductSteps with | step it ihy ihs
rw [count_eq_match_step, count_eq_match_step, step_map, bind_assoc]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp [ihy _]
· simp [ihs _]
· simp
end Count
section AnyAll
theorem IterM.anyM_filterMapM {α β β' : Type w} {m : Type w Type w'} {n : Type w Type w''}

View File

@@ -1,77 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Iterators.Combinators.Monadic.Take
public import Init.Data.Iterators.Lemmas.Consumers.Monadic
@[expose] public section
namespace Std.Iterators
theorem Take.isPlausibleStep_take_yield [Monad m] [Iterator α m β] {n : Nat}
{it : IterM (α := α) m β} (h : it.IsPlausibleStep (.yield it' out)) :
(it.take (n + 1)).IsPlausibleStep (.yield (it'.take n) out) :=
(.yield h (by simp [IterM.take]))
theorem Take.isPlausibleStep_take_skip [Monad m] [Iterator α m β] {n : Nat}
{it : IterM (α := α) m β} (h : it.IsPlausibleStep (.skip it')) :
(it.take (n + 1)).IsPlausibleStep (.skip (it'.take (n + 1))) :=
(.skip h (by simp [IterM.take]))
theorem IterM.step_take {α m β} [Monad m] [Iterator α m β] {n : Nat}
{it : IterM (α := α) m β} :
(it.take n).step = (match n with
| 0 => pure <| .deflate <| .done (.depleted rfl)
| k + 1 => do
match ( it.step).inflate with
| .yield it' out h => pure <| .deflate <| .yield (it'.take k) out (Take.isPlausibleStep_take_yield h)
| .skip it' h => pure <| .deflate <| .skip (it'.take (k + 1)) (Take.isPlausibleStep_take_skip h)
| .done h => pure <| .deflate <| .done (.done h)) := by
simp only [take, step, Iterator.step, internalState_toIterM]
cases n
case zero => rfl
case succ k =>
apply bind_congr
intro step
cases step.inflate using PlausibleIterStep.casesOn <;> rfl
theorem IterM.toList_take_zero {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
[Finite (Take α m) m]
[IteratorCollect (Take α m) m m] [LawfulIteratorCollect (Take α m) m m]
{it : IterM (α := α) m β} :
(it.take 0).toList = pure [] := by
rw [toList_eq_match_step]
simp [step_take]
theorem IterM.step_toTake {α m β} [Monad m] [Iterator α m β] [Finite α m]
{it : IterM (α := α) m β} :
it.toTake.step = (do
match ( it.step).inflate with
| .yield it' out h => pure <| .deflate <| .yield it'.toTake out (.yield h Nat.zero_ne_one)
| .skip it' h => pure <| .deflate <| .skip it'.toTake (.skip h Nat.zero_ne_one)
| .done h => pure <| .deflate <| .done (.done h)) := by
simp only [toTake, step, Iterator.step, internalState_toIterM]
apply bind_congr
intro step
cases step.inflate using PlausibleIterStep.casesOn <;> rfl
@[simp]
theorem IterM.toList_toTake {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
{it : IterM (α := α) m β} :
it.toTake.toList = it.toList := by
induction it using IterM.inductSteps with | step it ihy ihs
rw [toList_eq_match_step, toList_eq_match_step]
simp only [step_toTake, bind_assoc]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp [ihy _]
· simp [ihs _]
· simp
end Std.Iterators

View File

@@ -7,8 +7,8 @@ module
prelude
public import Init.Data.Iterators.Combinators.Monadic.ULift
import all Init.Data.Iterators.Combinators.Monadic.ULift
public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
public section
@@ -20,13 +20,9 @@ variable {α : Type u} {m : Type u → Type u'} {n : Type max u v → Type v'}
theorem IterM.step_uLift [Iterator α m β] [Monad n] {it : IterM (α := α) m β}
[MonadLiftT m (ULiftT n)] :
(it.uLift n).step = (do
match ( (monadLift it.step : ULiftT n _).run).down.inflate with
| .yield it' out h => return .deflate (.yield (it'.uLift n) (.up out) _, h, rfl)
| .skip it' h => return .deflate (.skip (it'.uLift n) _, h, rfl)
| .done h => return .deflate (.done _, h, rfl)) := by
simp only [IterM.step, Iterator.step, IterM.uLift]
apply bind_congr; intro step
split <;> simp [Types.ULiftIterator.Monadic.modifyStep, *]
let step := ( (monadLift it.step : ULiftT n _).run).down
return .deflate Types.ULiftIterator.Monadic.modifyStep step.inflate.val, step.inflate.val, step.inflate.property, rfl) :=
rfl
@[simp]
theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β}
@@ -37,11 +33,14 @@ theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (
(fun l => l.down.map ULift.up) <$> (monadLift it.toList : ULiftT n _).run := by
induction it using IterM.inductSteps with | step it ihy ihs
rw [IterM.toList_eq_match_step, IterM.toList_eq_match_step, step_uLift]
simp only [bind_assoc, map_eq_pure_bind, monadLift_bind, ULiftT.run_bind]
apply bind_congr; intro step
simp only [bind_pure_comp, bind_map_left, liftM_bind, ULiftT.run_bind, map_bind]
apply bind_congr
intro step
simp [Types.ULiftIterator.Monadic.modifyStep]
cases step.down.inflate using PlausibleIterStep.casesOn
· simp [ihy _]
· simp [ihs _]
· simp only [uLift] at ihy
simp [ihy _]
· exact ihs _
· simp
@[simp]
@@ -64,20 +63,4 @@ theorem IterM.toArray_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (
rw [ toArray_toList, toArray_toList, toList_uLift, monadLift_map]
simp
@[simp]
theorem IterM.count_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β}
[MonadLiftT m (ULiftT n)] [Finite α m] [IteratorLoop α m m]
[LawfulMonad m] [LawfulMonad n] [LawfulIteratorLoop α m m]
[LawfulMonadLiftT m (ULiftT n)] :
(it.uLift n).count =
(.up ·.down.down) <$> (monadLift (n := ULiftT n) it.count).run := by
induction it using IterM.inductSteps with | step it ihy ihs
rw [count_eq_match_step, count_eq_match_step, monadLift_bind, map_eq_pure_bind, step_uLift]
simp only [bind_assoc, ULiftT.run_bind]
apply bind_congr; intro step
cases step.down.inflate using PlausibleIterStep.casesOn
· simp [ihy _]
· simp [ihs _]
· simp
end Std.Iterators

View File

@@ -10,7 +10,6 @@ public import Init.Data.Iterators.Combinators.ULift
import all Init.Data.Iterators.Combinators.ULift
public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
public import Init.Data.Iterators.Lemmas.Consumers.Collect
public import Init.Data.Iterators.Lemmas.Consumers.Loop
public section
@@ -23,16 +22,14 @@ theorem Iter.uLift_eq_toIter_uLift_toIterM {it : Iter (α := α) β} :
rfl
theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} :
it.uLift.step = match it.step with
| .yield it' out h => .yield it'.uLift (.up out) _, h, rfl
| .skip it' h => .skip it'.uLift _, h, rfl
| .done h => .done _, h, rfl := by
it.uLift.step =
Types.ULiftIterator.modifyStep it.step.val,
it.step.val.mapIterator Iter.toIterM, it.step.property,
by simp [Types.ULiftIterator.modifyStep] := by
rw [Subtype.ext_iff]
simp only [uLift_eq_toIter_uLift_toIterM, step, IterM.Step.toPure, toIterM_toIter,
IterM.step_uLift, toIter_toIterM]
simp only [monadLift, ULiftT.run_pure, PlausibleIterStep.yield, PlausibleIterStep.skip,
PlausibleIterStep.done, pure_bind]
cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
IterM.step_uLift, bind_pure_comp, Id.run_map, toIter_toIterM]
simp [Types.ULiftIterator.modifyStep, monadLift]
@[simp]
theorem Iter.toList_uLift [Iterator α Id β] {it : Iter (α := α) β}
@@ -58,12 +55,4 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β}
rw [ toArray_toList, toArray_toList, toList_uLift]
simp [-toArray_toList]
@[simp]
theorem Iter.count_uLift [Iterator α Id β] {it : Iter (α := α) β}
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] :
it.uLift.count = it.count := by
simp only [monadLift, uLift_eq_toIter_uLift_toIterM, count_eq_count_toIterM, toIterM_toIter]
rw [IterM.count_uLift]
simp [monadLift]
end Std.Iterators

View File

@@ -68,7 +68,8 @@ theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
rw [ h]
theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
[Finite α Id] {m : Type w Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
[Finite α Id] {m : Type w Type w''} [Monad m] [LawfulMonad m]
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
{γ : Type w} {it : Iter (α := α) β} {init : γ}
{f : (out : β) _ γ m (ForInStep γ)} :
letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
@@ -80,7 +81,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
[Finite α Id] {m : Type w Type w''} [Monad m] [LawfulMonad m]
[IteratorLoop α Id m]
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
{γ : Type w} {it : Iter (α := α) β} {init : γ}
{f : β γ m (ForInStep γ)} :
ForIn.forIn it init f =
@@ -330,7 +331,7 @@ theorem Iter.foldM_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β] [
theorem Iter.foldM_eq_foldM_toIterM {α β : Type w} [Iterator α Id β]
[Finite α Id] {m : Type w Type w''} [Monad m] [LawfulMonad m]
[IteratorLoop α Id m]
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
{γ : Type w} {it : Iter (α := α) β} {init : γ} {f : γ β m γ} :
it.foldM (init := init) f = it.toIterM.foldM (init := init) f := by
simp [foldM_eq_forIn, IterM.foldM_eq_forIn, forIn_eq_forIn_toIterM]
@@ -395,7 +396,7 @@ theorem Iter.fold_eq_foldM {α β : Type w} {γ : Type x} [Iterator α Id β]
simp [foldM_eq_forIn, fold_eq_forIn]
theorem Iter.fold_eq_fold_toIterM {α β : Type w} {γ : Type w} [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id Id]
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
{f : γ β γ} {init : γ} {it : Iter (α := α) β} :
it.fold (init := init) f = (it.toIterM.fold (init := init) f).run := by
rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]
@@ -421,9 +422,8 @@ theorem Iter.fold_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id
cases step using PlausibleIterStep.casesOn <;> simp
-- The argument `f : γ₁ → γ₂` is intentionally explicit, as it is sometimes not found by unification.
theorem Iter.fold_hom {γ₁ : Type x₁} {γ₂ : Type x₂} [Iterator α Id β] [Finite α Id]
[IteratorLoop α Id Id.{x₁}] [LawfulIteratorLoop α Id Id.{x₁}]
[IteratorLoop α Id Id.{x₂}] [LawfulIteratorLoop α Id Id.{x₂}]
theorem Iter.fold_hom [Iterator α Id β] [Finite α Id]
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
{it : Iter (α := α) β}
(f : γ₁ γ₂) {g₁ : γ₁ β γ₁} {g₂ : γ₂ β γ₂} {init : γ₁}
(H : x y, g₂ (f x) y = f (g₁ x y)) :
@@ -469,72 +469,30 @@ theorem Iter.foldl_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [F
it.toArray.foldl (init := init) f = it.fold (init := init) f := by
rw [fold_eq_foldM, Array.foldl_eq_foldlM, Iter.foldlM_toArray]
theorem Iter.count_eq_count_toIterM {α β : Type w} [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id Id.{w}] {it : Iter (α := α) β} :
it.count = it.toIterM.count.run.down :=
(rfl)
theorem Iter.count_eq_fold {α β : Type w} [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id Id.{w}] [LawfulIteratorLoop α Id Id.{w}]
[IteratorLoop α Id Id.{0}] [LawfulIteratorLoop α Id Id.{0}]
@[simp]
theorem Iter.size_toArray_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
[IteratorSize α Id] [LawfulIteratorSize α]
{it : Iter (α := α) β} :
it.count = it.fold (γ := Nat) (init := 0) (fun acc _ => acc + 1) := by
rw [count_eq_count_toIterM, IterM.count_eq_fold, fold_eq_fold_toIterM]
rw [ fold_hom (f := ULift.down)]
simp
theorem Iter.count_eq_forIn {α β : Type w} [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id Id.{w}] [LawfulIteratorLoop α Id Id.{w}]
[IteratorLoop α Id Id.{0}] [LawfulIteratorLoop α Id Id.{0}]
{it : Iter (α := α) β} :
it.count = (ForIn.forIn (m := Id) it 0 (fun _ acc => return .yield (acc + 1))).run := by
rw [count_eq_fold, forIn_pure_yield_eq_fold, Id.run_pure]
theorem Iter.count_eq_match_step {α β : Type w} [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
{it : Iter (α := α) β} :
it.count = (match it.step.val with
| .yield it' _ => it'.count + 1
| .skip it' => it'.count
| .done => 0) := by
simp only [count_eq_count_toIterM]
rw [IterM.count_eq_match_step]
simp only [bind_pure_comp, id_map', Id.run_bind, Iter.step]
cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
it.toArray.size = it.size := by
simp only [toArray_eq_toArray_toIterM, LawfulIteratorCollect.toArray_eq]
simp [ toArray_eq_toArray_toIterM, LawfulIteratorSize.size_eq_size_toArray]
@[simp]
theorem Iter.size_toArray_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id]
theorem Iter.length_toList_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
[IteratorSize α Id] [LawfulIteratorSize α]
{it : Iter (α := α) β} :
it.toArray.size = it.count := by
simp only [toArray_eq_toArray_toIterM, count_eq_count_toIterM, Id.run_map,
IterM.up_size_toArray_eq_count]
@[deprecated Iter.size_toArray_eq_count (since := "2025-10-29")]
def Iter.size_toArray_eq_size := @size_toArray_eq_count
it.toList.length = it.size := by
rw [ toList_toArray, Array.length_toList, size_toArray_eq_size]
@[simp]
theorem Iter.length_toList_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id]
theorem Iter.length_toListRev_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
[IteratorSize α Id] [LawfulIteratorSize α]
{it : Iter (α := α) β} :
it.toList.length = it.count := by
rw [ toList_toArray, Array.length_toList, size_toArray_eq_count]
@[deprecated Iter.length_toList_eq_count (since := "2025-10-29")]
def Iter.length_toList_eq_size := @length_toList_eq_count
@[simp]
theorem Iter.length_toListRev_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
{it : Iter (α := α) β} :
it.toListRev.length = it.count := by
rw [toListRev_eq, List.length_reverse, length_toList_eq_count]
@[deprecated Iter.length_toListRev_eq_count (since := "2025-10-29")]
def Iter.length_toListRev_eq_size := @length_toListRev_eq_count
it.toListRev.length = it.size := by
rw [toListRev_eq, List.length_reverse, length_toList_eq_size]
theorem Iter.anyM_eq_forIn {α β : Type w} {m : Type Type w'} [Iterator α Id β]
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]

View File

@@ -335,73 +335,6 @@ theorem IterM.drain_eq_map_toArray {α β : Type w} {m : Type w → Type w'} [It
it.drain = (fun _ => .unit) <$> it.toList := by
simp [IterM.drain_eq_map_toList]
theorem IterM.count_eq_fold {α β : Type w} {m : Type w Type w'} [Iterator α m β]
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m]
{it : IterM (α := α) m β} :
it.count = it.fold (init := .up 0) (fun acc _ => .up <| acc.down + 1) :=
(rfl)
theorem IterM.count_eq_forIn {α β : Type w} {m : Type w Type w'} [Iterator α m β]
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m]
{it : IterM (α := α) m β} :
it.count = ForIn.forIn it (.up 0) (fun _ acc => return .yield (.up (acc.down + 1))) :=
(rfl)
theorem IterM.count_eq_match_step {α β : Type w} {m : Type w Type w'} [Iterator α m β]
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} :
it.count = (do
match ( it.step).inflate.val with
| .yield it' _ => return .up (( it'.count).down + 1)
| .skip it' => return .up ( it'.count).down
| .done => return .up 0) := by
simp only [count_eq_fold]
have (acc : Nat) (it' : IterM (α := α) m β) :
it'.fold (init := ULift.up acc) (fun acc _ => .up (acc.down + 1)) =
(ULift.up <| ·.down + acc) <$>
it'.fold (init := ULift.up 0) (fun acc _ => .up (acc.down + 1)) := by
rw [ fold_hom]
· simp only [Nat.zero_add]; rfl
· simp only [ULift.up.injEq]; omega
rw [fold_eq_match_step]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [Nat.zero_add, bind_pure_comp]
rw [this 1]
· simp
· simp
@[simp]
theorem IterM.up_size_toArray_eq_count {α β : Type w} [Iterator α m β] [Finite α m]
[Monad m] [LawfulMonad m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
[IteratorLoop α m m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} :
(.up <| ·.size) <$> it.toArray = it.count := by
rw [toArray_eq_fold, count_eq_fold, fold_hom]
· simp only [List.size_toArray, List.length_nil]; rfl
· simp
@[simp]
theorem IterM.up_length_toList_eq_count {α β : Type w} [Iterator α m β] [Finite α m]
[Monad m] [LawfulMonad m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
[IteratorLoop α m m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} :
(.up <| ·.length) <$> it.toList = it.count := by
rw [toList_eq_fold, count_eq_fold, fold_hom]
· simp only [List.length_nil]; rfl
· simp
@[simp]
theorem IterM.up_length_toListRev_eq_count {α β : Type w} [Iterator α m β] [Finite α m]
[Monad m] [LawfulMonad m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
[IteratorLoop α m m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} :
(.up <| ·.length) <$> it.toListRev = it.count := by
simp only [toListRev_eq, Functor.map_map, List.length_reverse, up_length_toList_eq_count]
theorem IterM.anyM_eq_forIn {α β : Type w} {m : Type w Type w'} [Iterator α m β]
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
{it : IterM (α := α) m β} {p : β m (ULift Bool)} :

View File

@@ -1,10 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Iterators.Lemmas.Producers.Monadic
public import Init.Data.Iterators.Lemmas.Producers.List

View File

@@ -1,9 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Iterators.Lemmas.Producers.Monadic.List

View File

@@ -1,71 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Iterators.Lemmas.Consumers.Monadic
public import Init.Data.Iterators.Producers.Monadic.List
@[expose] public section
/-!
# Lemmas about list iterators
This module provides lemmas about the interactions of `List.iterM` with `IterM.step` and various
collectors.
-/
namespace Std.Iterators
open Std.Internal
variable {m : Type w Type w'} {n : Type w Type w''} [Monad m] {β : Type w}
@[simp]
theorem _root_.List.step_iterM_nil :
(([] : List β).iterM m).step = pure (.deflate .done, rfl) := by
simp only [IterM.step, Iterator.step]; rfl
@[simp]
theorem _root_.List.step_iterM_cons {x : β} {xs : List β} :
((x :: xs).iterM m).step = pure (.deflate .yield (xs.iterM m) x, rfl) := by
simp only [List.iterM, IterM.step, Iterator.step]; rfl
theorem _root_.List.step_iterM {l : List β} :
(l.iterM m).step = match l with
| [] => pure (.deflate .done, rfl)
| x :: xs => pure (.deflate .yield (xs.iterM m) x, rfl) := by
cases l <;> simp [List.step_iterM_cons, List.step_iterM_nil]
theorem ListIterator.toArrayMapped_iterM [Monad n] [LawfulMonad n]
{β : Type w} {γ : Type w} {lift : δ : Type w m δ n δ}
[LawfulMonadLiftFunction lift] {f : β n γ} {l : List β} :
IteratorCollect.toArrayMapped lift f (l.iterM m) (m := m) = List.toArray <$> l.mapM f := by
rw [LawfulIteratorCollect.toArrayMapped_eq]
induction l with
| nil =>
rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
simp [List.step_iterM_nil, LawfulMonadLiftFunction.lift_pure]
| cons x xs ih =>
rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih, LawfulMonadLiftFunction.lift_pure]
@[simp]
theorem _root_.List.toArray_iterM [LawfulMonad m] {l : List β} :
(l.iterM m).toArray = pure l.toArray := by
simp only [IterM.toArray, ListIterator.toArrayMapped_iterM]
rw [List.mapM_pure, map_pure, List.map_id']
@[simp]
theorem _root_.List.toList_iterM [LawfulMonad m] {l : List β} :
(l.iterM m).toList = pure l := by
rw [ IterM.toList_toArray, List.toArray_iterM, map_pure, List.toList_toArray]
@[simp]
theorem _root_.List.toListRev_iterM [LawfulMonad m] {l : List β} :
(l.iterM m).toListRev = pure l.reverse := by
simp [IterM.toListRev_eq, List.toList_iterM]
end Std.Iterators

View File

@@ -1,10 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Iterators.Producers.Monadic
public import Init.Data.Iterators.Producers.List

View File

@@ -1,9 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Iterators.Producers.Monadic.List

View File

@@ -19,45 +19,104 @@ open Std.Iterators
namespace Std.Iterators
/-- This typeclass provides an iterator for elements of type `γ`. -/
class ToIterator (γ : Type u) (m : Type w Type w') (α β : outParam (Type w)) where
iterMInternal (x : γ) : IterM (α := α) m β
/--
This typeclass provides an iterator for the given element `x : γ`. Usually, instances are provided
for all elements of a type `γ`.
-/
class ToIterator {γ : Type u} (x : γ) (m : Type w Type w') (β : outParam (Type w)) where
State : Type w
iterMInternal : IterM (α := State) m β
/-- Converts `x` into a monadic iterator. -/
@[always_inline, inline, expose]
def ToIterator.iterM (x : γ) [ToIterator γ m α β] : IterM (α := α) m β :=
def ToIterator.iterM (x : γ) [ToIterator x m β] : IterM (α := ToIterator.State x m) m β :=
ToIterator.iterMInternal (x := x)
/-- Converts `x` into a pure iterator. -/
@[always_inline, inline, expose]
def ToIterator.iter [ToIterator γ Id α β] (x : γ) : Iter (α := α) β :=
def ToIterator.iter (x : γ) [ToIterator x Id β] : Iter (α := ToIterator.State x Id) β :=
ToIterator.iterM x |>.toIter
/-- Creates a monadic `ToIterator` instance. -/
@[always_inline, inline, expose]
def ToIterator.ofM (α : Type w)
(iterM : γ IterM (α := α) m β) :
ToIterator γ m α β where
iterMInternal x := iterM x
def ToIterator.ofM {x : γ} (State : Type w)
(iterM : IterM (α := State) m β) :
ToIterator x m β where
State := State
iterMInternal := iterM
/-- Creates a pure `ToIterator` instance. -/
@[always_inline, inline, expose]
def ToIterator.of (α : Type w)
(iter : γ Iter (α := α) β) :
ToIterator γ Id α β where
iterMInternal x := iter x |>.toIterM
def ToIterator.of {x : γ} (State : Type w)
(iter : Iter (α := State) β) :
ToIterator x Id β where
State := State
iterMInternal := iter.toIterM
/-- Replaces `ToIterator.iterM` with its definition. -/
theorem ToIterator.iterM_eq {γ : Type u} {α β : Type v}
{it : γ IterM (α := α) Id β} {x} :
letI : ToIterator γ Id α β := .ofM α it
ToIterator.iterM x = it x :=
theorem ToIterator.iterM_eq {γ : Type u} {x : γ} {State : Type v} {β : Type v} {it} :
letI : ToIterator x Id β := .ofM State it
ToIterator.iterM x = it :=
rfl
/-- Replaces `ToIterator.iter` with its definition. -/
theorem ToIterator.iter_eq {γ : Type u} {x : γ} {α β : Type v} {it} :
letI : ToIterator γ Id α β := .ofM α it
ToIterator.iter x = (it x).toIter :=
theorem ToIterator.iter_eq {γ : Type u} {x : γ} {State : Type v} {β : Type v} {it} :
letI : ToIterator x Id β := .ofM State it
ToIterator.iter x = it.toIter :=
rfl
/-!
## Instance forwarding
If the type defined as `ToIterator.State` implements an iterator typeclass, then this typeclass
should also be available when the type is syntactically visible as `ToIteratorState`. The following
instances are responsible for this forwarding.
-/
instance {x : γ} {State : Type w} {iter}
[Iterator State m β] :
letI i : ToIterator x m β := .ofM State iter
Iterator (α := i.State) m β :=
inferInstanceAs <| Iterator State m β
instance {x : γ} {State : Type w} {iter}
[Iterator (α := State) m β] [Finite State m] :
letI i : ToIterator x m β := .ofM State iter
Finite (α := i.State) m :=
inferInstanceAs <| Finite (α := State) m
instance {x : γ} {State : Type w} {iter}
[Iterator (α := State) m β] [IteratorCollect State m n] :
letI i : ToIterator x m β := .ofM State iter
IteratorCollect (α := i.State) m n :=
inferInstanceAs <| IteratorCollect (α := State) m n
instance {x : γ} {State : Type w} {iter}
[Iterator (α := State) m β] [IteratorCollectPartial State m n] :
letI i : ToIterator x m β := .ofM State iter
IteratorCollectPartial (α := i.State) m n :=
inferInstanceAs <| IteratorCollectPartial (α := State) m n
instance {x : γ} {State : Type w} {iter}
[Iterator (α := State) m β] [IteratorLoop State m n] :
letI i : ToIterator x m β := .ofM State iter
IteratorLoop (α := i.State) m n :=
inferInstanceAs <| IteratorLoop (α := State) m n
instance {x : γ} {State : Type w} {iter}
[Iterator (α := State) m β] [IteratorLoopPartial State m n] :
letI i : ToIterator x m β := .ofM State iter
IteratorLoopPartial (α := i.State) m n :=
inferInstanceAs <| IteratorLoopPartial (α := State) m n
instance {x : γ} {State : Type w} {iter}
[Iterator (α := State) m β] [IteratorSize State m] :
letI i : ToIterator x m β := .ofM State iter
IteratorSize (α := i.State) m :=
inferInstanceAs <| IteratorSize (α := State) m
instance {x : γ} {State : Type w} {iter}
[Iterator (α := State) m β] [IteratorSizePartial State m] :
letI i : ToIterator x m β := .ofM State iter
IteratorSizePartial (α := i.State) m :=
inferInstanceAs <| IteratorSizePartial (α := State) m
end Std.Iterators

View File

@@ -622,17 +622,11 @@ instance : Std.LawfulIdentity (α := List α) (· ++ ·) [] where
| nil => simp
| cons _ as ih => simp [ih, Nat.succ_add]
@[simp] theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs) := by
@[simp, grind _=_] theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs) := by
induction as with
| nil => rfl
| cons a as ih => simp [ih]
grind_pattern append_assoc => (as ++ bs) ++ cs where
as =/= []; bs =/= []; cs =/= []
grind_pattern append_assoc => as ++ (bs ++ cs) where
as =/= []; bs =/= []; cs =/= []
instance : Std.Associative (α := List α) (· ++ ·) := append_assoc
-- Arguments are explicit as there is often ambiguity inferring the arguments.

View File

@@ -272,8 +272,8 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
apply Nat.lt_trans ih
simp +arith
theorem lex_trichotomous [DecidableEq α] {r : α α Prop} [DecidableRel r]
(trichotomous : x y : α, ¬ r x y ¬ r y x x = y)
theorem not_lex_antisymm [DecidableEq α] {r : α α Prop} [DecidableRel r]
(antisymm : x y : α, ¬ r x y ¬ r y x x = y)
{as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
match as, bs with
| [], [] => rfl
@@ -286,26 +286,20 @@ theorem lex_trichotomous [DecidableEq α] {r : αα → Prop} [DecidableRel
· subst eq
have h₁ : ¬ Lex r bs as := fun h => h₁ (List.Lex.cons h)
have h₂ : ¬ Lex r as bs := fun h => h₂ (List.Lex.cons h)
simp [lex_trichotomous trichotomous h₁ h₂]
simp [not_lex_antisymm antisymm h₁ h₂]
· exfalso
by_cases hba : r b a
· exact h₁ (Lex.rel hba)
· exact eq (trichotomous _ _ hab hba)
@[deprecated lex_trichotomous (since := "2025-10-27")]
theorem not_lex_antisymm [DecidableEq α] {r : α α Prop} [DecidableRel r]
(antisymm : x y : α, ¬ r x y ¬ r y x x = y)
{as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
lex_trichotomous antisymm h₁ h₂
· exact eq (antisymm _ _ hab hba)
protected theorem le_antisymm [LT α]
[i : Std.Trichotomous (· < · : α α Prop)]
[i : Std.Antisymm (¬ · < · : α α Prop)]
{as bs : List α} (h₁ : as bs) (h₂ : bs as) : as = bs :=
open Classical in
lex_trichotomous i.trichotomous h₁ h₂
not_lex_antisymm i.antisymm h₁ h₂
instance [LT α]
[s : Std.Trichotomous (· < · : α α Prop)] :
[s : Std.Antisymm (¬ · < · : α α Prop)] :
Std.Antisymm (· · : List α List α Prop) where
antisymm _ _ h₁ h₂ := List.le_antisymm h₁ h₂

View File

@@ -471,7 +471,7 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
loop as' b this
loop as init [], rfl
instance [Monad m] : ForIn' m (List α) α inferInstance where
instance : ForIn' m (List α) α inferInstance where
forIn' := List.forIn'
-- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -485,7 +485,7 @@ instance [Monad m] : ForIn' m (List α) α inferInstance where
@[simp, grind =] theorem forIn_nil [Monad m] {f : α β m (ForInStep β)} {b : β} : forIn [] b f = pure b :=
rfl
instance [Monad m] : ForM m (List α) α where
instance : ForM m (List α) α where
forM := List.forM
-- We simplify `List.forM` to `forM`.

View File

@@ -291,11 +291,9 @@ theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ¬ q a) :
· simp [h₁, h₂]
· simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
@[grind ]
theorem head_eraseP_mem {xs : List α} {p : α Bool} (h) : (xs.eraseP p).head h xs :=
eraseP_sublist.head_mem h
@[grind ]
theorem getLast_eraseP_mem {xs : List α} {p : α Bool} (h) : (xs.eraseP p).getLast h xs :=
eraseP_sublist.getLast_mem h

View File

@@ -13,9 +13,6 @@ import all Init.Data.List.BasicAux
public import Init.Data.List.Control
import all Init.Data.List.Control
public import Init.BinderPredicates
import Init.Grind.Annotated
grind_annotated "2025-01-24"
public section
@@ -254,10 +251,6 @@ theorem getElem_eq_getElem?_get {l : List α} {i : Nat} (h : i < l.length) :
l[i] = l[i]?.get (by simp [h]) := by
simp
theorem getElem_eq_getD {l : List α} {i : Nat} {h : i < l.length} (fallback : α) :
l[i] = l.getD i fallback := by
rw [getElem_eq_getElem?_get, List.getD, Option.get_eq_getD]
theorem getD_getElem? {l : List α} {i : Nat} {d : α} :
l[i]?.getD d = if p : i < l.length then l[i]'p else d := by
if h : i < l.length then
@@ -305,12 +298,6 @@ theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
have h₁ := Nat.le_of_not_lt h₁
rw [getElem?_eq_none h₁, getElem?_eq_none]; rwa [ hl]
theorem ext_getElem_iff {l₁ l₂ : List α} :
l₁ = l₂ l₁.length = l₂.length (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i]'h₁ = l₂[i]'h₂ := by
constructor
· simp +contextual
· exact fun h => ext_getElem h.1 h.2
@[simp] theorem getElem_concat_length {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
(l ++ [a])[i]'w = a := by
subst h; simp
@@ -1230,13 +1217,9 @@ theorem tailD_map {f : α → β} {l l' : List α} :
theorem getLastD_map {f : α β} {l : List α} {a : α} : (map f l).getLastD (f a) = f (l.getLastD a) := by
simp
@[simp] theorem map_map {g : β γ} {f : α β} {l : List α} :
@[simp, grind _=_] theorem map_map {g : β γ} {f : α β} {l : List α} :
map g (map f l) = map (g f) l := by induction l <;> simp_all
grind_pattern map_map => map g (map f l) where
g =/= List.reverse
f =/= List.reverse
/-! ### filter -/
@[simp] theorem filter_cons_of_pos {p : α Bool} {a : α} {l} (pa : p a) :
@@ -1445,16 +1428,13 @@ theorem filterMap_eq_filter {p : α → Bool} :
| nil => rfl
| cons a l IH => by_cases pa : p a <;> simp [Option.guard, pa, IH]
@[grind =]
theorem filterMap_filterMap {f : α Option β} {g : β Option γ} {l : List α} :
filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l := by
induction l with
| nil => rfl
| cons a l IH => cases h : f a <;> simp [filterMap_cons, *]
grind_pattern filterMap_filterMap => filterMap g (filterMap f l) where
f =/= some
g =/= some
@[grind =]
theorem map_filterMap {f : α Option β} {g : β γ} {l : List α} :
map g (filterMap f l) = filterMap (fun x => (f x).map g) l := by
@@ -2476,28 +2456,16 @@ theorem getLast_of_mem_getLast? {l : List α} (hx : x ∈ l.getLast?) :
simp only [reverse_cons, filterMap_append, filterMap_cons, ih]
split <;> simp_all
@[simp] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
@[simp, grind _=_] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
induction as <;> simp_all
grind_pattern reverse_append => (as ++ bs).reverse where
as =/= []
bs =/= []
grind_pattern reverse_append => bs.reverse ++ as.reverse where
as =/= []
bs =/= []
@[simp] theorem reverse_eq_append_iff {xs ys zs : List α} :
xs.reverse = ys ++ zs xs = zs.reverse ++ ys.reverse := by
rw [reverse_eq_iff, reverse_append]
theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
@[grind _=_] theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
rw [reverse_append]; rfl
grind_pattern reverse_concat => (l ++ [a]).reverse where
l =/= []
grind_pattern reverse_concat => a :: l.reverse where
l =/= []
theorem reverse_eq_concat {xs ys : List α} {a : α} :
xs.reverse = ys ++ [a] xs = a :: ys.reverse := by
rw [reverse_eq_iff, reverse_concat]
@@ -2515,15 +2483,9 @@ theorem flatten_reverse {L : List (List α)} :
@[grind =] theorem reverse_flatMap {β} {l : List α} {f : α List β} : (l.flatMap f).reverse = l.reverse.flatMap (reverse f) := by
induction l <;> simp_all
grind_pattern reverse_flatMap => (l.flatMap f).reverse where
f =/= List.reverse _
theorem flatMap_reverse {β} {l : List α} {f : α List β} : l.reverse.flatMap f = (l.flatMap (reverse f)).reverse := by
@[grind =] theorem flatMap_reverse {β} {l : List α} {f : α List β} : (l.reverse.flatMap f) = (l.flatMap (reverse f)).reverse := by
induction l <;> simp_all
grind_pattern flatMap_reverse => l.reverse.flatMap f where
f =/= List.reverse _
@[simp] theorem reverseAux_eq {as bs : List α} : reverseAux as bs = reverse as ++ bs :=
reverseAux_eq_append ..

View File

@@ -98,7 +98,7 @@ theorem not_cons_lex_cons_iff [DecidableEq α] [DecidableRel r] {a b} {l₁ l₂
theorem cons_le_cons_iff [LT α]
[i₁ : Std.Asymm (· < · : α α Prop)]
[i₂ : Std.Trichotomous (· < · : α α Prop)]
[i₂ : Std.Antisymm (¬ · < · : α α Prop)]
{a b} {l₁ l₂ : List α} :
(a :: l₁) (b :: l₂) a < b a = b l₁ l₂ := by
dsimp only [instLE, instLT, List.le, List.lt]
@@ -110,12 +110,12 @@ theorem cons_le_cons_iff [LT α]
apply Decidable.byContradiction
intro h₃
apply h₂
exact i₂.trichotomous _ _ h₁ h₃
exact i₂.antisymm _ _ h₁ h₃
· if h₃ : a < b then
exact .inl h₃
else
right
exact i₂.trichotomous _ _ h₃ h₁, h₂
exact i₂.antisymm _ _ h₃ h₁, h₂
· rintro (h | h₁, h₂)
· left
exact i₁.asymm _ _ h, fun w => Irrefl.irrefl _ (w h)
@@ -124,7 +124,7 @@ theorem cons_le_cons_iff [LT α]
theorem not_lt_of_cons_le_cons [LT α]
[i₁ : Std.Asymm (· < · : α α Prop)]
[i₂ : Std.Trichotomous (· < · : α α Prop)]
[i₂ : Std.Antisymm (¬ · < · : α α Prop)]
{a b : α} {l₁ l₂ : List α} (h : a :: l₁ b :: l₂) : ¬ b < a := by
rw [cons_le_cons_iff] at h
rcases h with h | rfl, h
@@ -138,7 +138,7 @@ theorem left_le_left_of_cons_le_cons [LT α] [LE α] [IsLinearOrder α]
theorem le_of_cons_le_cons [LT α]
[i₀ : Std.Irrefl (· < · : α α Prop)]
[i₁ : Std.Asymm (· < · : α α Prop)]
[i₂ : Std.Trichotomous (· < · : α α Prop)]
[i₂ : Std.Antisymm (¬ · < · : α α Prop)]
{a} {l₁ l₂ : List α} (h : a :: l₁ a :: l₂) : l₁ l₂ := by
rw [cons_le_cons_iff] at h
rcases h with h | _, h
@@ -212,7 +212,7 @@ protected theorem lt_of_le_of_lt [LT α] [LE α] [IsLinearOrder α] [LawfulOrder
@[deprecated List.lt_of_le_of_lt (since := "2025-08-01")]
protected theorem lt_of_le_of_lt' [LT α]
[Std.Asymm (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
[Trans (¬ · < · : α α Prop) (¬ · < ·) (¬ · < ·)]
{l₁ l₂ l₃ : List α} (h₁ : l₁ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
letI : LE α := .ofLT α
@@ -226,7 +226,7 @@ protected theorem le_trans [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α]
@[deprecated List.le_trans (since := "2025-08-01")]
protected theorem le_trans' [LT α]
[Std.Asymm (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
[Trans (¬ · < · : α α Prop) (¬ · < ·) (¬ · < ·)]
{l₁ l₂ l₃ : List α} (h₁ : l₁ l₂) (h₂ : l₂ l₃) : l₁ l₃ :=
letI := LE.ofLT α
@@ -298,7 +298,7 @@ protected theorem le_of_lt [LT α]
protected theorem le_iff_lt_or_eq [LT α]
[Std.Irrefl (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
[Std.Asymm (· < · : α α Prop)]
{l₁ l₂ : List α} : l₁ l₂ l₁ < l₂ l₁ = l₂ := by
constructor
@@ -484,7 +484,7 @@ protected theorem lt_iff_exists [LT α] {l₁ l₂ : List α} :
protected theorem le_iff_exists [LT α]
[Std.Asymm (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)] {l₁ l₂ : List α} :
[Std.Antisymm (¬ · < · : α α Prop)] {l₁ l₂ : List α} :
l₁ l₂
(l₁ = l₂.take l₁.length)
( (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
@@ -497,7 +497,7 @@ protected theorem le_iff_exists [LT α]
conv => lhs; simp +singlePass [exists_comm]
· simpa using Std.Irrefl.irrefl
· simpa using Std.Asymm.asymm
· simpa using Std.Trichotomous.trichotomous
· simpa using Std.Antisymm.antisymm
theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
l₁ ++ l₂ < l₁ ++ l₃ := by
@@ -507,7 +507,7 @@ theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
theorem append_left_le [LT α]
[Std.Asymm (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
{l₁ l₂ l₃ : List α} (h : l₂ l₃) :
l₁ ++ l₂ l₁ ++ l₃ := by
induction l₁ with
@@ -540,9 +540,9 @@ protected theorem map_lt [LT α] [LT β]
protected theorem map_le [LT α] [LT β]
[Std.Asymm (· < · : α α Prop)]
[Std.Trichotomous (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
[Std.Asymm (· < · : β β Prop)]
[Std.Trichotomous (· < · : β β Prop)]
[Std.Antisymm (¬ · < · : β β Prop)]
{l₁ l₂ : List α} {f : α β} (w : x y, x < y f x < f y) (h : l₁ l₂) :
map f l₁ map f l₂ := by
rw [List.le_iff_exists] at h

View File

@@ -68,13 +68,10 @@ theorem getElem?_modifyHead {l : List α} {f : αα} {i} :
@[simp, grind =] theorem tail_modifyHead {f : α α} {l : List α} :
(l.modifyHead f).tail = l.tail := by cases l <;> simp
@[simp] theorem take_modifyHead {f : α α} {l : List α} {i} :
@[simp, grind =] theorem take_modifyHead {f : α α} {l : List α} {i} :
(l.modifyHead f).take i = (l.take i).modifyHead f := by
cases l <;> cases i <;> simp
grind_pattern take_modifyHead => (l.modifyHead f).take i where
i =/= 0
@[simp] theorem drop_modifyHead_of_pos {f : α α} {l : List α} {i} (h : 0 < i) :
(l.modifyHead f).drop i = l.drop i := by
cases l <;> cases i <;> simp_all
@@ -106,9 +103,7 @@ theorem eraseIdx_eq_modifyTailIdx : ∀ i (l : List α), eraseIdx l i = l.modify
| _+1, [] => rfl
| _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
-- This is not suitable as a `@[grind =]` lemma:
-- as soon as it is instantiated the hypothesis `H` causes an infinite chain of instantiations.
@[simp] theorem length_modifyTailIdx (f : List α List α) (H : l, (f l).length = l.length) :
@[simp, grind =] theorem length_modifyTailIdx (f : List α List α) (H : l, (f l).length = l.length) :
(l : List α) i, (l.modifyTailIdx i f).length = l.length
| _, 0 => H _
| [], _+1 => rfl
@@ -218,6 +213,7 @@ theorem modify_eq_self {f : αα} {i} {l : List α} (h : l.length ≤ i) :
intro h
omega
@[grind =]
theorem modify_modify_eq (f g : α α) (i) (l : List α) :
(l.modify i f).modify i g = l.modify i (g f) := by
apply ext_getElem
@@ -226,9 +222,6 @@ theorem modify_modify_eq (f g : αα) (i) (l : List α) :
simp only [getElem_modify, Function.comp_apply]
split <;> simp
grind_pattern modify_modify_eq => (l.modify i f).modify i g where
l =/= []
theorem modify_modify_ne (f g : α α) {i j} (l : List α) (h : i j) :
(l.modify i f).modify j g = (l.modify j g).modify i f := by
apply ext_getElem

View File

@@ -374,22 +374,6 @@ theorem drop_take : ∀ {i j : Nat} {l : List α}, drop i (take j l) = take (j -
rw [drop_take]
simp
@[simp]
theorem drop_eq_drop_iff :
{l : List α} {i j : Nat}, l.drop i = l.drop j min i l.length = min j l.length
| [], i, j => by simp
| _ :: xs, 0, 0 => by simp
| x :: xs, i + 1, 0 => by
rw [List.ext_getElem_iff]
simp [succ_min_succ, show ¬ xs.length - i = xs.length + 1 by omega]
| x :: xs, 0, j + 1 => by
rw [List.ext_getElem_iff]
simp [succ_min_succ, show ¬ xs.length + 1 = xs.length - j by omega]
| x :: xs, i + 1, j + 1 => by simp [succ_min_succ, drop_eq_drop_iff]
theorem drop_eq_drop_min {l : List α} {i : Nat} : l.drop i = l.drop (min i l.length) := by
simp
theorem take_reverse {α} {xs : List α} {i : Nat} :
xs.reverse.take i = (xs.drop (xs.length - i)).reverse := by
by_cases h : i xs.length

View File

@@ -98,18 +98,14 @@ theorem eq_nil_of_subset_nil {l : List α} : l ⊆ [] → l = [] := subset_nil.m
theorem map_subset {l₁ l₂ : List α} (f : α β) (h : l₁ l₂) : map f l₁ map f l₂ :=
fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _)
grind_pattern map_subset => l₁ l₂, map f l₁ where
l₂ =/= List.map _ _
grind_pattern map_subset => l₁ l₂, map f l₂ where
l₁ =/= List.map _ _
grind_pattern map_subset => l₁ l₂, map f l₁
grind_pattern map_subset => l₁ l₂, map f l₂
theorem filter_subset {l₁ l₂ : List α} (p : α Bool) (H : l₁ l₂) : filter p l₁ filter p l₂ :=
fun x => by simp_all [mem_filter, subset_def.1 H]
grind_pattern filter_subset => l₁ l₂, filter p l₁ where
l₂ =/= List.filter _ _
grind_pattern filter_subset => l₁ l₂, filter p l₂ where
l₁ =/= List.filter _ _
grind_pattern filter_subset => l₁ l₂, filter p l₁
grind_pattern filter_subset => l₁ l₂, filter p l₂
theorem filterMap_subset {l₁ l₂ : List α} (f : α Option β) (H : l₁ l₂) :
filterMap f l₁ filterMap f l₂ := by
@@ -118,10 +114,8 @@ theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁
rintro a, h, w
exact a, H h, w
grind_pattern filterMap_subset => l₁ l₂, filterMap f l₁ where
l₂ =/= List.filterMap _ _
grind_pattern filterMap_subset => l₁ l₂, filterMap f l₂ where
l₁ =/= List.filterMap _ _
grind_pattern filterMap_subset => l₁ l₂, filterMap f l₁
grind_pattern filterMap_subset => l₁ l₂, filterMap f l₂
theorem subset_append_left (l₁ l₂ : List α) : l₁ l₁ ++ l₂ := fun _ => mem_append_left _
@@ -212,11 +206,13 @@ theorem Sublist.head_mem (s : ys <+ xs) (h) : ys.head h ∈ xs :=
s.mem (List.head_mem h)
grind_pattern Sublist.head_mem => ys <+ xs, ys.head h
grind_pattern Sublist.head_mem => ys.head h xs -- This is somewhat aggressive, as it initiates sublist based reasoning.
theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h xs :=
s.mem (List.getLast_mem h)
grind_pattern Sublist.getLast_mem => ys <+ xs, ys.getLast h
grind_pattern Sublist.getLast_mem => ys.getLast h xs -- This is somewhat aggressive, as it initiates sublist based reasoning.
instance : Trans (@Sublist α) Subset Subset :=
fun h₁ h₂ => trans h₁.subset h₂
@@ -286,28 +282,20 @@ protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : m
grind_pattern Sublist.map => l₁ <+ l₂, map f l₁
grind_pattern Sublist.map => l₁ <+ l₂, map f l₂
@[grind ]
protected theorem Sublist.filterMap (f : α Option β) (s : l₁ <+ l₂) :
filterMap f l₁ <+ filterMap f l₂ := by
induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons]
grind_pattern Sublist.filterMap => filterMap f l₁ <+ filterMap f l where
l₁ =/= List.filterMap _ _
l₂ =/= List.filterMap _ _
grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₁ where
l₂ =/= List.filterMap _ _
grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₂ where
l₁ =/= List.filterMap _ _
grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l
grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₂
@[grind ]
protected theorem Sublist.filter (p : α Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
rw [ filterMap_eq_filter]; apply s.filterMap
grind_pattern Sublist.filter => filter p l₁ <+ filter p l₂ where
l₁ =/= List.filter _ _
l₂ =/= List.filter _ _
grind_pattern Sublist.filter => l₁ <+ l₂, l₁.filter p where
l₂ =/= List.filter _ _
grind_pattern Sublist.filter => l₁ <+ l₂, l₂.filter p where
l₁ =/= List.filter _ _
grind_pattern Sublist.filter => l₁ <+ l₂, l₁.filter p
grind_pattern Sublist.filter => l₁ <+ l₂, l₂.filter p
theorem head_filter_mem (xs : List α) (p : α Bool) (h) : (xs.filter p).head h xs :=
filter_sublist.head_mem h

View File

@@ -473,13 +473,8 @@ protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤
instance : Std.Antisymm ( . . : Nat Nat Prop) where
antisymm _ _ h₁ h₂ := Nat.le_antisymm h₁ h₂
instance : Std.Trichotomous (. < . : Nat Nat Prop) where
trichotomous _ _ h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
set_option linter.missingDocs false in
@[deprecated Nat.instTrichotomousLt (since := "2025-10-27")]
def Nat.instAntisymmNotLt : Std.Antisymm (¬ . < . : Nat Nat Prop) where
antisymm := Nat.instTrichotomousLt.trichotomous
instance : Std.Antisymm (¬ . < . : Nat Nat Prop) where
antisymm _ _ h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
protected theorem add_le_add_left {n m : Nat} (h : n m) (k : Nat) : k + n k + m :=
match le.dest h with
@@ -822,8 +817,6 @@ protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pow_pos (by decide)
instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
Nat.ne_zero_iff_zero_lt.mpr (Nat.pow_pos (pos_of_neZero _))
instance {n : Nat} : NeZero (n^0) := Nat.one_ne_zero
protected theorem mul_pow (a b n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by
induction n with
| zero => simp [Nat.pow_zero]

View File

@@ -139,12 +139,4 @@ Returns `true` if the `(n+1)`th least significant bit is `1`, or `false` if it i
-- `1 &&& n` is faster than `n &&& 1` for big `n`.
1 &&& (m >>> n) != 0
/--
Asserts that the `(n+1)`th least significant bit of `m` is not set.
(This definition is used by Lean internally for compact bitmaps.)
-/
@[expose, reducible] protected def hasNotBit (m n : Nat) : Prop :=
Nat.land 1 (Nat.shiftRight m n) 1
end Nat

View File

@@ -485,16 +485,11 @@ protected theorem and_comm (x y : Nat) : x &&& y = y &&& x := by
apply Nat.eq_of_testBit_eq
simp [Bool.and_comm]
@[grind _=_]
protected theorem and_assoc (x y z : Nat) : (x &&& y) &&& z = x &&& (y &&& z) := by
apply Nat.eq_of_testBit_eq
simp [Bool.and_assoc]
grind_pattern Nat.and_assoc => (x &&& y) &&& z where
x =/= 0; y =/= 0; z =/= 0
grind_pattern Nat.and_assoc => x &&& (y &&& z) where
x =/= 0; y =/= 0; z =/= 0
instance : Std.Associative (α := Nat) (· &&& ·) where
assoc := Nat.and_assoc

View File

@@ -1719,16 +1719,11 @@ theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
| 0 => by simp
| n + 1 => by simp [zero_shiftRight n, shiftRight_succ]
@[grind _=_]
theorem shiftLeft_add (m n : Nat) : k, m <<< (n + k) = (m <<< n) <<< k
| 0 => rfl
| k + 1 => by simp [ Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]
grind_pattern shiftLeft_add => m <<< (n + k) where
m =/= 0
grind_pattern shiftLeft_add => (m <<< n) <<< k where
m =/= 0
@[simp] theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x := by
rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]

View File

@@ -15,40 +15,7 @@ public section
namespace Option
instance instDecidableEq {α} [inst : DecidableEq α] : DecidableEq (Option α) := fun a b =>
/-
Structured for compatibility with the decidable-equality-with-none instances.
-/
match a with
| none => match b with
| none => .isTrue rfl
| some _ => .isFalse Option.noConfusion
| some a => match b with
| none => .isFalse Option.noConfusion
| some b => match inst a b with
| .isTrue h => .isTrue (h rfl)
| .isFalse n => .isFalse (Option.noConfusion · n)
/--
Equality with `none` is decidable even if the wrapped type does not have decidable equality.
-/
instance decidableEqNone (o : Option α) : Decidable (o = none) :=
/- We use a `match` instead of transferring from `isNone_iff_eq_none` for
compatibility with the `DecidableEq` instance. -/
match o with
| none => .isTrue rfl
| some _ => .isFalse Option.noConfusion
/--
Equality with `none` is decidable even if the wrapped type does not have decidable equality.
-/
instance decidableNoneEq (o : Option α) : Decidable (none = o) :=
/- We use a `match` instead of transferring from `isNone_iff_eq_none` for
compatibility with the `DecidableEq` instance. -/
match o with
| none => .isTrue rfl
| some _ => .isFalse Option.noConfusion
deriving instance DecidableEq for Option
deriving instance BEq for Option
@[simp, grind =] theorem getD_none : getD none a = a := rfl

View File

@@ -35,6 +35,17 @@ instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o) :=
theorem some_inj {a b : α} : some a = some b a = b := by simp; rfl
/--
Equality with `none` is decidable even if the wrapped type does not have decidable equality.
This is not an instance because it is not definitionally equal to the standard instance of
`DecidableEq (Option α)`, which can cause problems. It can be locally bound if needed.
Try to use the Boolean comparisons `Option.isNone` or `Option.isSome` instead.
-/
@[inline] def decidableEqNone {o : Option α} : Decidable (o = none) :=
decidable_of_decidable_of_iff isNone_iff_eq_none
instance decidableForallMem {p : α Prop} [DecidablePred p] :
o : Option α, Decidable ( a, a o p a)
| none => isTrue nofun
@@ -168,10 +179,10 @@ Examples:
| none , _ => pure
| some a, f => f a
instance [Monad m] : ForM m (Option α) α :=
instance : ForM m (Option α) α :=
Option.forM
instance [Monad m] : ForIn' m (Option α) α inferInstance where
instance : ForIn' m (Option α) α inferInstance where
forIn' x init f := do
match x with
| none => return init

View File

@@ -212,13 +212,10 @@ theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β)
(a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
cases a <;> cases b <;> rfl
@[grind =]
theorem bind_assoc (x : Option α) (f : α Option β) (g : β Option γ) :
(x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl
grind_pattern bind_assoc => (x.bind f).bind g where
f =/= some
g =/= some
theorem bind_congr {α β} {o : Option α} {f g : α Option β} :
(h : a, o = some a f a = g a) o.bind f = o.bind g := by
cases o <;> simp

View File

@@ -631,7 +631,7 @@ instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) := fun a b =>
decidable_of_bool (compare a b).isLT Ordering.isLT_iff_eq_lt
/--
Constructs an `LE` instance from an `Ord` instance that asserts that the result of `compare`
Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
satisfies `Ordering.isLE`.
-/
@[expose] def leOfOrd [Ord α] : LE α where

View File

@@ -234,13 +234,13 @@ If an `LT α` instance is asymmetric and its negation is transitive and antisymm
public theorem IsLinearOrder.of_lt {α : Type u} [LT α]
(lt_asymm : Asymm (α := α) (· < ·) := by exact inferInstance)
(not_lt_trans : Trans (α := α) (¬ · < ·) (¬ · < ·) (¬ · < ·) := by exact inferInstance)
(lt_trichotomous : Trichotomous (α := α) (· < ·) := by exact inferInstance) :
(not_lt_antisymm : Antisymm (α := α) (¬ · < ·) := by exact inferInstance) :
haveI := LE.ofLT α
IsLinearOrder α :=
letI := LE.ofLT α
haveI : IsLinearPreorder α := .of_lt
{ le_antisymm := by
simpa [LE.ofLT] using fun a b hab hba => lt_trichotomous.trichotomous a b hba hab }
simpa [LE.ofLT] using fun a b hab hba => not_lt_antisymm.antisymm a b hba hab }
/--
This lemma characterizes in terms of `LT α` when a `Min α` instance

View File

@@ -22,53 +22,17 @@ section AxiomaticInstances
public instance (r : α α Prop) [Asymm r] : Irrefl r where
irrefl a h := Asymm.asymm a a h h
public instance (r : α α Prop) [Total r] : Refl r where
public instance {r : α α Prop} [Total r] : Refl r where
refl a := by simpa using Total.total a a
public instance (r : α α Prop) [Asymm r] : Antisymm r where
antisymm a b h h' := (Asymm.asymm a b h h').elim
public instance (r : α α Prop) [Total r] : Trichotomous r where
trichotomous a b h h' := by simpa [h, h'] using Total.total (r := r) a b
public theorem Trichotomous.rel_or_eq_or_rel_swap {r : α α Prop} [i : Trichotomous r] {a b} :
r a b a = b r b a := match Classical.em (r a b) with
| .inl hab => .inl hab | .inr hab => match Classical.em (r b a) with
| .inl hba => .inr <| .inr hba
| .inr hba => .inr <| .inl <| i.trichotomous _ _ hab hba
public theorem trichotomous_of_rel_or_eq_or_rel_swap {r : α α Prop}
(h : {a b}, r a b a = b r b a) : Trichotomous r where
trichotomous _ _ hab hba := (h.resolve_left hab).resolve_right hba
public instance Antisymm.trichotomous_of_antisymm_not {r : α α Prop} [i : Antisymm (¬ r · ·)] :
Trichotomous r where trichotomous := i.antisymm
public theorem Trichotomous.antisymm_not {r : α α Prop} [i : Trichotomous r] :
Antisymm (¬ r · ·) where antisymm := i.trichotomous
public theorem Total.rel_of_not_rel_swap {r : α α Prop} [Total r] {a b} (h : ¬ r a b) : r b a :=
(Total.total a b).elim (fun h' => (h h').elim) (·)
public theorem total_of_not_rel_swap_imp_rel {r : α α Prop} (h : {a b}, ¬ r a b r b a) :
Total r where
total a b := match Classical.em (r a b) with | .inl hab => .inl hab | .inr hab => .inr (h hab)
public theorem total_of_refl_of_trichotomous (r : α α Prop) [Refl r] [Trichotomous r] :
Total r where
total a b := (Trichotomous.rel_or_eq_or_rel_swap (a := a) (b := b) (r := r)).elim Or.inl <|
fun h => h.elim (fun h => h Or.inl (Refl.refl _)) Or.inr
public theorem asymm_of_irrefl_of_antisymm (r : α α Prop) [Irrefl r] [Antisymm r] :
Asymm r where asymm a b h h' := Irrefl.irrefl _ (Antisymm.antisymm a b h h' h)
public instance Total.asymm_of_total_not {r : α α Prop} [i : Total (¬ r · ·)] : Asymm r where
asymm a b h := (i.total a b).resolve_left (· h)
asymm a b h := by cases i.total a b <;> trivial
public theorem Asymm.total_not {r : α α Prop} [i : Asymm r] : Total (¬ r · ·) where
total a b := match Classical.em (r b a) with
| .inl hba => .inl <| i.asymm b a hba
| .inr hba => .inr hba
total a b := by
apply Classical.byCases (p := r a b) <;> intro hab
· exact Or.inr <| i.asymm a b hab
· exact Or.inl hab
public instance {α : Type u} [LE α] [IsPartialOrder α] :
Antisymm (α := α) (· ·) where
@@ -110,7 +74,9 @@ public theorem le_total {α : Type u} [LE α] [Std.Total (α := α) (· ≤ ·)]
Std.Total.total a b
public theorem le_of_not_ge {α : Type u} [LE α] [Std.Total (α := α) (· ·)] {a b : α} :
¬ b a a b := Total.rel_of_not_rel_swap
¬ b a a b := by
intro h
simpa [h] using Std.Total.total a b (r := (· ·))
end LE
@@ -124,30 +90,18 @@ public theorem lt_iff_le_and_not_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT
a < b a b ¬ b a :=
LawfulOrderLT.lt_iff a b
public theorem not_lt_iff_not_le_or_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α]
{a b : α} : ¬ a < b ¬ a b b a := by
simp only [lt_iff_le_and_not_ge, Classical.not_and_iff_not_or_not, Classical.not_not]
public theorem not_le_of_gt {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α}
(h : a < b) : ¬ b a := (lt_iff_le_and_not_ge.1 h).2
public theorem not_lt_of_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α}
(h : a b) : ¬ b < a := imp_not_comm.1 not_le_of_gt h
public instance {α : Type u} {_ : LE α} [LT α] [LawfulOrderLT α]
[Trichotomous (α := α) (· < ·)] : Antisymm (α := α) (· ·) where
antisymm _ _ hab hba := Trichotomous.trichotomous _ _ (not_lt_of_ge hba) (not_lt_of_ge hab)
public theorem not_lt {α : Type u} [LT α] [LE α] [Std.Total (α := α) (· ·)] [LawfulOrderLT α]
{a b : α} : ¬ a < b b a := by
simp [lt_iff_le_and_not_ge, Classical.not_not, Std.Total.total]
public theorem not_gt_of_lt {α : Type u} [LT α] [i : Std.Asymm (α := α) (· < ·)] {a b : α}
(h : a < b) : ¬ b < a :=
i.asymm a b h
public theorem le_of_lt {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} (h : a < b) :
a b := (lt_iff_le_and_not_ge.1 h).1
public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
[Antisymm (α := α) (· ·)] : Antisymm (α := α) (· < ·) where
antisymm _ _ hab hba := Antisymm.antisymm _ _ (le_of_lt hab) (le_of_lt hba)
a b := by
simp only [LawfulOrderLT.lt_iff] at h
exact h.1
public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
Std.Asymm (α := α) (· < ·) where
@@ -156,9 +110,8 @@ public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
intro h h'
exact h.2.elim h'.1
@[deprecated instIrreflOfAsymm (since := "2025-10-24")]
public theorem instIrreflLtOfIsPreorderOfLawfulOrderLT {α : Type u} [LT α] [LE α]
[LawfulOrderLT α] : Std.Irrefl (α := α) (· < ·) := inferInstance
public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
Std.Irrefl (α := α) (· < ·) := inferInstance
public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ·) (· ·) (· ·) ]
[LawfulOrderLT α] : Trans (α := α) (· < ·) (· < ·) (· < ·) where
@@ -169,19 +122,10 @@ public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (·
· intro hca
exact hab.2.elim (le_trans hbc.1 hca)
public theorem not_lt {α : Type u} [LT α] [LE α] [Std.Total (α := α) (· ·)] [LawfulOrderLT α]
{a b : α} : ¬ a < b b a := by
simp [not_lt_iff_not_le_or_ge]
exact le_of_not_ge
public theorem not_le {α : Type u} [LT α] [LE α] [Std.Total (α := α) (· ·)] [LawfulOrderLT α]
{a b : α} : ¬ a b b < a := by
simp [lt_iff_le_and_not_ge]
exact le_of_not_ge
public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
[Total (α := α) (· ·)] [Antisymm (α := α) (· ·)] : Trichotomous (α := α) (· < ·) where
trichotomous a b hab hba := by
[Total (α := α) (· ·)] [Antisymm (α := α) (· ·)] :
Antisymm (α := α) (¬ · < ·) where
antisymm a b hab hba := by
simp only [not_lt] at hab hba
exact Antisymm.antisymm (r := (· ·)) a b hba hab
@@ -192,9 +136,9 @@ public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
simp only [not_lt] at hab hbc
exact le_trans hbc hab
@[deprecated Asymm.total_not (since := "2025-10-24")]
public theorem instTotalNotLtOfLawfulOrderLTOfLe {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
: Total (α := α) (¬ · < ·) := Asymm.total_not
public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α] [Total (α := α) (· ·)] :
Total (α := α) (¬ · < ·) where
total a b := by simp [not_lt, Std.Total.total]
public theorem lt_of_le_of_lt {α : Type u} [LE α] [LT α]
[Trans (α := α) (· ·) (· ·) (· ·)] [LawfulOrderLT α] {a b c : α} (hab : a b)

View File

@@ -43,7 +43,7 @@ universe u v
have := range.step_pos
loop init range.start (by simp)
instance [Monad m] : ForIn' m Range Nat inferInstance where
instance : ForIn' m Range Nat inferInstance where
forIn' := Range.forIn'
-- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -59,7 +59,7 @@ instance [Monad m] : ForIn' m Range Nat inferInstance where
have := range.step_pos
loop range.start
instance [Monad m] : ForM m Range Nat where
instance : ForM m Range Nat where
forM := Range.forM
syntax:max "[" withoutPosition(":" term) "]" : term

View File

@@ -18,7 +18,6 @@ public import Init.Data.Range.Polymorphic.UInt
public import Init.Data.Range.Polymorphic.SInt
public import Init.Data.Range.Polymorphic.NatLemmas
public import Init.Data.Range.Polymorphic.IntLemmas
public import Init.Data.Range.Polymorphic.GetElemTactic
public section

View File

@@ -1,39 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alexander Bentkamp
-/
module
prelude
public import Init.Data.Range.Polymorphic.Int
public import Init.Data.Range.Polymorphic.Lemmas
public section
namespace Std.PRange.Int
@[simp]
theorem size_rco {a b : Int} :
(a...b).size = (b - a).toNat := by
simp only [Rco.size, Rxo.HasSize.size, Rxc.HasSize.size]
omega
@[simp]
theorem size_rcc {a b : Int} :
(a...=b).size = (b + 1 - a).toNat := by
simp [Rcc.size, Rxc.HasSize.size]
@[simp]
theorem size_roc {a b : Int} :
(a<...=b).size = (b - a).toNat := by
simp only [Roc.size, Rxc.HasSize.size]
omega
@[simp]
theorem size_roo {a b : Int} :
(a<...b).size = (b - a - 1).toNat := by
simp [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size]
omega
end Std.PRange.Int

View File

@@ -19,6 +19,45 @@ open Std.Iterators
namespace Std
open PRange
namespace Rxc
/--
Iterators for right-closed ranges implementing {name}`Rxc.HasSize` support {name}`Iter.size`.
-/
instance [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] :
IteratorSize (Rxc.Iterator α) Id where
size it := match it.internalState.next with
| none => pure (.up 0)
| some next => pure (.up (Rxc.HasSize.size next it.internalState.upperBound))
end Rxc
namespace Rxo
/--
Iterators for ranges implementing {name}`Rxo.HasSize` support {name}`Iter.size`.
-/
instance [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] :
IteratorSize (Rxo.Iterator α) Id where
size it := match it.internalState.next with
| none => pure (.up 0)
| some next => pure (.up (Rxo.HasSize.size next it.internalState.upperBound))
end Rxo
namespace Rxi
/--
Iterators for ranges implementing {name}`Rxi.HasSize` support {name}`Iter.size`.
-/
instance [Rxi.HasSize α] [UpwardEnumerable α] :
IteratorSize (Rxi.Iterator α) Id where
size it := match it.internalState.next with
| none => pure (.up 0)
| some next => pure (.up (Rxi.HasSize.size next))
end Rxi
namespace Rcc
variable {α : Type u}
@@ -53,8 +92,8 @@ def toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerab
Returns the number of elements contained in the given closed range.
-/
@[always_inline, inline]
def size [Rxc.HasSize α] (r : Rcc α) : Nat :=
Rxc.HasSize.size r.lower r.upper
def size [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] (r : Rcc α) : Nat :=
Internal.iter r |>.size
section Iterator
@@ -139,8 +178,8 @@ def toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerab
Returns the number of elements contained in the given left-closed right-open range.
-/
@[always_inline, inline]
def size [Rxo.HasSize α] (r : Rco α) : Nat :=
Rxo.HasSize.size r.lower r.upper
def size [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] (r : Rco α) : Nat :=
Internal.iter r |>.size
section Iterator
@@ -226,8 +265,8 @@ def toArray [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinit
Returns the number of elements contained in the given left-closed right-unbounded range.
-/
@[always_inline, inline]
def size [Rxi.HasSize α] (r : Rci α) : Nat :=
Rxi.HasSize.size r.lower
def size [Rxi.HasSize α] [UpwardEnumerable α] (r : Rci α) : Nat :=
Internal.iter r |>.size
section Iterator
@@ -310,10 +349,8 @@ def toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerab
Returns the number of elements contained in the given left-open right-closed range.
-/
@[always_inline, inline]
def size [Rxc.HasSize α] [UpwardEnumerable α] (r : Roc α) : Nat :=
match UpwardEnumerable.succ? r.lower with
| none => 0
| some lower => Rxc.HasSize.size lower r.upper
def size [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] (r : Roc α) : Nat :=
Internal.iter r |>.size
section Iterator
@@ -391,10 +428,8 @@ def toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerab
Returns the number of elements contained in the given open range.
-/
@[always_inline, inline]
def size [Rxo.HasSize α] [UpwardEnumerable α] (r : Roo α) : Nat :=
match UpwardEnumerable.succ? r.lower with
| none => 0
| some lower => Rxo.HasSize.size lower r.upper
def size [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] (r : Roo α) : Nat :=
Internal.iter r |>.size
section Iterator
@@ -472,9 +507,7 @@ Returns the number of elements contained in the given left-open right-unbounded
-/
@[always_inline, inline]
def size [Rxi.HasSize α] [UpwardEnumerable α] (r : Roi α) : Nat :=
match UpwardEnumerable.succ? r.lower with
| none => 0
| some lower => Rxi.HasSize.size lower
Internal.iter r |>.size
section Iterator
@@ -547,10 +580,8 @@ def toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUp
Returns the number of elements contained in the given closed range.
-/
@[always_inline, inline]
def size [Rxc.HasSize α] [Least? α] (r : Ric α) : Nat :=
match Least?.least? (α := α) with
| none => 0
| some least => Rxc.HasSize.size least r.upper
def size [Rxc.HasSize α] [UpwardEnumerable α] [Least? α] [LE α] [DecidableLE α] (r : Ric α) : Nat :=
Internal.iter r |>.size
section Iterator
@@ -622,10 +653,8 @@ def toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUp
Returns the number of elements contained in the given closed range.
-/
@[always_inline, inline]
def size [Rxo.HasSize α] [Least? α] (r : Rio α) : Nat :=
match Least?.least? (α := α) with
| none => 0
| some least => Rxo.HasSize.size least r.upper
def size [Rxo.HasSize α] [UpwardEnumerable α] [Least? α] [LT α] [DecidableLT α] (r : Rio α) : Nat :=
Internal.iter r |>.size
section Iterator
@@ -698,10 +727,8 @@ def toArray {α} [UpwardEnumerable α] [Least? α] (r : Rii α)
Returns the number of elements contained in the full range.
-/
@[always_inline, inline]
def size (_ : Rii α) [Least? α] [Rxi.HasSize α] : Nat :=
match Least?.least? (α := α) with
| none => 0
| some least => Rxi.HasSize.size least
def size [UpwardEnumerable α] [Least? α] (r : Rii α) [IteratorSize (Rxi.Iterator α) Id] : Nat :=
Internal.iter r |>.size
section Iterator

File diff suppressed because it is too large Load Diff

View File

@@ -16,64 +16,52 @@ namespace Std.PRange.Nat
theorem succ_eq {n : Nat} : succ n = n + 1 :=
rfl
theorem toList_rco_succ_succ {m n : Nat} :
theorem toList_Rco_succ_succ {m n : Nat} :
((m+1)...(n+1)).toList = (m...n).toList.map (· + 1) := by
simp only [ succ_eq]
rw [Std.Rco.toList_succ_succ_eq_map]
@[deprecated toList_rco_succ_succ (since := "2025-10-30")]
def toList_Rco_succ_succ := @toList_rco_succ_succ
@[deprecated toList_rco_succ_succ (since := "2025-08-22")]
def ClosedOpen.toList_succ_succ := @toList_rco_succ_succ
@[deprecated toList_Rco_succ_succ (since := "2025-08-22")]
theorem ClosedOpen.toList_succ_succ {m n : Nat} :
((m+1)...(n+1)).toList = (m...n).toList.map (· + 1) := toList_Rco_succ_succ
@[simp]
theorem size_rcc {a b : Nat} :
theorem size_Rcc {a b : Nat} :
(a...=b).size = b + 1 - a := by
simp [Rcc.size, Rxc.HasSize.size]
@[deprecated size_rcc (since := "2025-10-30")]
def size_Rcc := @size_rcc
simp [Rcc.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size,
Rcc.Internal.iter, Std.Iterators.Iter.toIterM, Rxc.HasSize.size]
@[simp]
theorem size_rco {a b : Nat} :
theorem size_Rco {a b : Nat} :
(a...b).size = b - a := by
simp only [Rco.size, Rxo.HasSize.size, Rxc.HasSize.size]
simp only [Rco.size, Iterators.Iter.size, Iterators.IteratorSize.size, Iterators.Iter.toIterM,
Rco.Internal.iter, Rxo.HasSize.size, Rxc.HasSize.size, Id.run_pure]
omega
@[deprecated size_rco (since := "2025-10-30")]
def size_Rco := @size_rco
@[simp]
theorem size_roc {a b : Nat} :
theorem size_Roc {a b : Nat} :
(a<...=b).size = b - a := by
simp [Roc.size, Rxc.HasSize.size]
@[deprecated size_roc (since := "2025-10-30")]
def size_Roc := @size_roc
simp [Roc.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size,
Roc.Internal.iter, Std.Iterators.Iter.toIterM, Rxc.HasSize.size]
@[simp]
theorem size_roo {a b : Nat} :
theorem size_Roo {a b : Nat} :
(a<...b).size = b - a - 1 := by
simp [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size]
@[deprecated size_roo (since := "2025-10-30")]
def size_Roo := @size_roo
simp only [Roo.size, Iterators.Iter.size, Iterators.IteratorSize.size, Iterators.Iter.toIterM,
Roo.Internal.iter, Rxo.HasSize.size, Rxc.HasSize.size, Id.run_pure]
omega
@[simp]
theorem size_ric {b : Nat} :
theorem size_Ric {b : Nat} :
(*...=b).size = b + 1 := by
simp [Ric.size, Rxc.HasSize.size]
@[deprecated size_ric (since := "2025-10-30")]
def size_Ric := @size_ric
simp [Ric.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size,
Ric.Internal.iter, Std.Iterators.Iter.toIterM, Rxc.HasSize.size]
@[simp]
theorem size_rio {b : Nat} :
theorem size_Rio {b : Nat} :
(*...b).size = b := by
simp [Rio.size, Rxo.HasSize.size, Rxc.HasSize.size]
@[deprecated size_rio (since := "2025-10-30")]
def size_Rio := @size_rio
simp only [Rio.size, Iterators.Iter.size, Iterators.IteratorSize.size, Iterators.Iter.toIterM,
Rio.Internal.iter, Rxo.HasSize.size, Rxc.HasSize.size, Id.run_pure]
omega
end Std.PRange.Nat

View File

@@ -9,7 +9,6 @@ prelude
public import Init.Data.Range.Polymorphic.UpwardEnumerable
set_option doc.verso true
set_option linter.missingDocs true
public section
@@ -24,13 +23,7 @@ A range of elements of {given}`α` with closed lower and upper bounds.
equal to {given}`b : α`. This is notation for {lean}`Rcc.mk a b`.
-/
structure Rcc (α : Type u) where
/--
The lower bound of the range. {name (full := Rcc.lower)}`lower` is included in the range.
-/
lower : α
/--
The upper bound of the range. {name (full := Rcc.upper)}`upper` is included in the range.
-/
upper : α
/--
@@ -40,13 +33,7 @@ A range of elements of {given}`α` with a closed lower bound and an open upper b
less than {given}`b : α`. This is notation for {lean}`Rco.mk a b`.
-/
structure Rco (α : Type u) where
/--
The lower bound of the range. {name (full := Rco.lower)}`lower` is included in the range.
-/
lower : α
/--
The upper bound of the range. {name (full := Rco.upper)}`upper` is not included in the range.
-/
upper : α
/--
@@ -56,9 +43,6 @@ An upward-unbounded range of elements of {given}`α` with a closed lower bound.
This is notation for {lean}`Rci.mk a`.
-/
structure Rci (α : Type u) where
/--
The lower bound of the range. {name (full := Rci.lower)}`lower` is included in the range.
-/
lower : α
/--
@@ -68,13 +52,7 @@ A range of elements of {given}`α` with an open lower bound and a closed upper b
{given}`b : α`. This is notation for {lean}`Roc.mk a b`.
-/
structure Roc (α : Type u) where
/--
The lower bound of the range. {name (full := Roc.lower)}`lower` is not included in the range.
-/
lower : α
/--
The upper bound of the range. {name (full := Roc.upper)}`upper` is included in the range.
-/
upper : α
/--
@@ -84,13 +62,7 @@ A range of elements of {given}`α` with an open lower and upper bounds.
{given}`b : α`. This is notation for {lean}`Roo.mk a b`.
-/
structure Roo (α : Type u) where
/--
The lower bound of the range. {name (full := Roo.lower)}`lower` is not included in the range.
-/
lower : α
/--
The upper bound of the range. {name (full := Roo.upper)}`upper` is not included in the range.
-/
upper : α
/--
@@ -100,9 +72,6 @@ An upward-unbounded range of elements of {given}`α` with an open lower bound.
This is notation for {lean}`Roi.mk a`.
-/
structure Roi (α : Type u) where
/--
The lower bound of the range. {name (full := Roi.lower)}`lower` is not included in the range.
-/
lower : α
/--
@@ -112,9 +81,6 @@ A downward-unbounded range of elements of {given}`α` with a closed upper bound.
This is notation for {lean}`Ric.mk b`.
-/
structure Ric (α : Type u) where
/--
The upper bound of the range. {name (full := Ric.upper)}`upper` is included in the range.
-/
upper : α
/--
@@ -124,9 +90,6 @@ A downward-unbounded range of elements of {given}`α` with an open upper bound.
This is notation for {lean}`Rio.mk b`.
-/
structure Rio (α : Type u) where
/--
The upper bound of the range. {name (full := Rio.upper)}`upper` is not included in the range.
-/
upper : α
/--
@@ -199,10 +162,6 @@ This is a prerequisite for many functions and instances, such as
{name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rcc.toList` or {name}`ForIn'`.
-/
class Rxc.IsAlwaysFinite (α : Type u) [UpwardEnumerable α] [LE α] : Prop where
/--
For every pair of elements {name}`init` and {name}`hi`, there exists a chain of successors that
results in an element that either has no successors or is greater than {name}`hi`.
-/
finite (init : α) (hi : α) :
n, (UpwardEnumerable.succMany? n init).elim True (¬ · hi)
@@ -213,10 +172,6 @@ This is a prerequisite for many functions and instances, such as
{name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rco.toList` or {name}`ForIn'`.
-/
class Rxo.IsAlwaysFinite (α : Type u) [UpwardEnumerable α] [LT α] : Prop where
/--
For every pair of elements {name}`init` and {name}`hi`, there exists a chain of successors that
results in an element that either has no successors or is greater than {name}`hi`.
-/
finite (init : α) (hi : α) :
n, (UpwardEnumerable.succMany? n init).elim True (¬ · < hi)
@@ -227,10 +182,6 @@ This is a prerequisite for many functions and instances, such as
{name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rci.toList` or {name}`ForIn'`.
-/
class Rxi.IsAlwaysFinite (α : Type u) [UpwardEnumerable α] : Prop where
/--
For every elements {name}`init`, there exists a chain of successors that
results in an element that has no successors.
-/
finite (init : α) : n, UpwardEnumerable.succMany? n init = none
namespace Rcc
@@ -340,7 +291,6 @@ This type class allows taking the intersection of a closed range with a
left-closed right-open range, resulting in another left-closed right-open range.
-/
class Rcc.HasRcoIntersection (α : Type w) where
/-- The intersection operator. -/
intersection : Rcc α Rco α Rco α
/--
@@ -349,9 +299,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
-/
class Rcc.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
[HasRcoIntersection α] where
/--
Every element of the intersection is an element of both original ranges.
-/
mem_intersection_iff {a : α} {r : Rcc α} {s : Rco α} :
a HasRcoIntersection.intersection r s a r a s
@@ -360,7 +307,6 @@ This type class allows taking the intersection of two left-closed right-open ran
another left-closed right-open range.
-/
class Rco.HasRcoIntersection (α : Type w) where
/-- The intersection operator. -/
intersection : Rco α Rco α Rco α
/--
@@ -369,9 +315,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
-/
class Rco.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
[HasRcoIntersection α] where
/--
Every element of the intersection is an element of both original ranges.
-/
mem_intersection_iff {a : α} {r : Rco α} {s : Rco α} :
a HasRcoIntersection.intersection r s a r a s
@@ -380,7 +323,6 @@ This type class allows taking the intersection of a left-closed right-unbounded
left-closed right-open range, resulting in another left-closed right-open range.
-/
class Rci.HasRcoIntersection (α : Type w) where
/-- The intersection operator. -/
intersection : Rci α Rco α Rco α
/--
@@ -389,9 +331,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
-/
class Rci.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
[HasRcoIntersection α] where
/--
Every element of the intersection is an element of both original ranges.
-/
mem_intersection_iff {a : α} {r : Rci α} {s : Rco α} :
a HasRcoIntersection.intersection r s a r a s
@@ -400,7 +339,6 @@ This type class allows taking the intersection of a left-open right-closed range
left-closed right-open range, resulting in another left-closed right-open range.
-/
class Roc.HasRcoIntersection (α : Type w) where
/-- The intersection operator. -/
intersection : Roc α Rco α Rco α
/--
@@ -409,9 +347,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
-/
class Roc.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
[HasRcoIntersection α] where
/--
Every element of the intersection is an element of both original ranges.
-/
mem_intersection_iff {a : α} {r : Roc α} {s : Rco α} :
a HasRcoIntersection.intersection r s a r a s
@@ -420,7 +355,6 @@ This type class allows taking the intersection of an open range with a
left-closed right-open range, resulting in another left-closed right-open range.
-/
class Roo.HasRcoIntersection (α : Type w) where
/-- The intersection operator. -/
intersection : Roo α Rco α Rco α
/--
@@ -429,9 +363,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
-/
class Roo.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
[HasRcoIntersection α] where
/--
Every element of the intersection is an element of both original ranges.
-/
mem_intersection_iff {a : α} {r : Roo α} {s : Rco α} :
a HasRcoIntersection.intersection r s a r a s
@@ -440,7 +371,6 @@ This type class allows taking the intersection of a left-open right-unbounded ra
left-closed right-open range, resulting in another left-closed right-open range.
-/
class Roi.HasRcoIntersection (α : Type w) where
/-- The intersection operator. -/
intersection : Roi α Rco α Rco α
/--
@@ -449,9 +379,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
-/
class Roi.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
[HasRcoIntersection α] where
/--
Every element of the intersection is an element of both original ranges.
-/
mem_intersection_iff {a : α} {r : Roi α} {s : Rco α} :
a HasRcoIntersection.intersection r s a r a s
@@ -460,7 +387,6 @@ This type class allows taking the intersection of a left-unbounded right-closed
left-closed right-open range, resulting in another left-closed right-open range.
-/
class Ric.HasRcoIntersection (α : Type w) where
/-- The intersection operator. -/
intersection : Ric α Rco α Rco α
/--
@@ -469,9 +395,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
-/
class Ric.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
[HasRcoIntersection α] where
/--
Every element of the intersection is an element of both original ranges.
-/
mem_intersection_iff {a : α} {r : Ric α} {s : Rco α} :
a HasRcoIntersection.intersection r s a r a s
@@ -480,7 +403,6 @@ This type class allows taking the intersection of a left-unbounded right-open ra
left-closed right-open range, resulting in another left-closed right-open range.
-/
class Rio.HasRcoIntersection (α : Type w) where
/-- The intersection operator. -/
intersection : Rio α Rco α Rco α
/--
@@ -489,9 +411,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
-/
class Rio.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
[HasRcoIntersection α] where
/--
Every element of the intersection is an element of both original ranges.
-/
mem_intersection_iff {a : α} {r : Rio α} {s : Rco α} :
a HasRcoIntersection.intersection r s a r a s

View File

@@ -295,15 +295,6 @@ theorem add_def (a b : Rat) :
theorem add_def' (a b : Rat) : a + b = mkRat (a.num * b.den + b.num * a.den) (a.den * b.den) := by
rw [add_def, normalize_eq_mkRat]
theorem num_add (a b : Rat) : (a + b).num =
(a.num * b.den + b.num * a.den) /
((a.num * b.den + b.num * a.den).natAbs.gcd (a.den * b.den)) := by
rw [add_def, num_normalize]
theorem den_add (a b : Rat) : (a + b).den =
a.den * b.den / (a.num * b.den + b.num * a.den).natAbs.gcd (a.den * b.den) := by
rw [add_def, den_normalize]
@[local simp]
protected theorem add_zero (a : Rat) : a + 0 = a := by simp [add_def', mkRat_self]
@[local simp]
@@ -415,13 +406,6 @@ theorem mul_def (a b : Rat) :
theorem mul_def' (a b : Rat) : a * b = mkRat (a.num * b.num) (a.den * b.den) := by
rw [mul_def, normalize_eq_mkRat]
theorem num_mul (a b : Rat) :
(a * b).num = a.num * b.num / ((a.num * b.num).natAbs.gcd (a.den * b.den)) := by
rw [mul_def, num_normalize]
theorem den_mul (a b : Rat) :
(a * b).den = a.den * b.den / (a.num * b.num).natAbs.gcd (a.den * b.den) := by
rw [mul_def, den_normalize]
protected theorem mul_comm (a b : Rat) : a * b = b * a := by
simp [mul_def, normalize_eq_mkRat, Int.mul_comm, Nat.mul_comm]
@@ -567,9 +551,7 @@ theorem pow_def (q : Rat) (n : Nat) :
@[simp] theorem num_pow (q : Rat) (n : Nat) : (q ^ n).num = q.num ^ n := rfl
@[simp] theorem den_pow (q : Rat) (n : Nat) : (q ^ n).den = q.den ^ n := rfl
@[simp] protected theorem pow_zero (q : Rat) : q ^ 0 = 1 := by
simp only [pow_def, Int.pow_zero, Nat.pow_zero, mk_den_one]
rfl
@[simp] protected theorem pow_zero (q : Rat) : q ^ 0 = 1 := rfl
protected theorem pow_succ (q : Rat) (n : Nat) : q ^ (n + 1) = q ^ n * q := by
rcases q with n, d, hn, r
@@ -585,8 +567,7 @@ protected theorem zpow_natCast (q : Rat) (n : Nat) : q ^ (n : Int) = q ^ n := rf
protected theorem zpow_neg (q : Rat) (n : Int) : q ^ (-n : Int) = (q ^ n)⁻¹ := by
rcases n with (_ | n) | n
· simp only [Int.ofNat_eq_natCast, Int.cast_ofNat_Int, Int.neg_zero, Rat.zpow_zero]
with_unfolding_all rfl
· with_unfolding_all rfl
· rfl
· exact (Rat.inv_inv _).symm

View File

@@ -414,8 +414,8 @@ instance : Repr String where
instance : Repr String.Pos.Raw where
reprPrec p _ := "{ byteIdx := " ++ repr p.byteIdx ++ " }"
instance : Repr Substring.Raw where
reprPrec s _ := Format.text <| String.Internal.append (String.quote (Substring.Raw.Internal.toString s)) ".toRawSubstring"
instance : Repr Substring where
reprPrec s _ := Format.text <| String.Internal.append (String.quote (Substring.Internal.toString s)) ".toSubstring"
instance (n : Nat) : Repr (Fin n) where
reprPrec f _ := repr f.val

View File

@@ -10,7 +10,6 @@ public import Init.Data.Slice.Basic
public import Init.Data.Slice.Notation
public import Init.Data.Slice.Operations
public import Init.Data.Slice.Array
public import Init.Data.Slice.List
public import Init.Data.Slice.Lemmas
public section

View File

@@ -23,82 +23,45 @@ variable {α : Type u}
instance : Rcc.Sliceable (Array α) Nat (Subarray α) where
mkSlice xs range :=
xs.toSubarray range.lower (range.upper + 1)
let halfOpenRange := Rcc.HasRcoIntersection.intersection range 0...<xs.size
(xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
instance : Rco.Sliceable (Array α) Nat (Subarray α) where
mkSlice xs range :=
xs.toSubarray range.lower range.upper
let halfOpenRange := Rco.HasRcoIntersection.intersection range 0...<xs.size
(xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
instance : Rci.Sliceable (Array α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Rci.HasRcoIntersection.intersection range 0...<xs.size
xs.toSubarray halfOpenRange.lower halfOpenRange.upper
(xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
instance : Roc.Sliceable (Array α) Nat (Subarray α) where
mkSlice xs range :=
xs.toSubarray (range.lower + 1) (range.upper + 1)
let halfOpenRange := Roc.HasRcoIntersection.intersection range 0...<xs.size
(xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
instance : Roo.Sliceable (Array α) Nat (Subarray α) where
mkSlice xs range :=
xs.toSubarray (range.lower + 1) range.upper
let halfOpenRange := Roo.HasRcoIntersection.intersection range 0...<xs.size
(xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
instance : Roi.Sliceable (Array α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Roi.HasRcoIntersection.intersection range 0...<xs.size
xs.toSubarray halfOpenRange.lower halfOpenRange.upper
(xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
instance : Ric.Sliceable (Array α) Nat (Subarray α) where
mkSlice xs range :=
xs.toSubarray 0 (range.upper + 1)
let halfOpenRange := Ric.HasRcoIntersection.intersection range 0...<xs.size
(xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
instance : Rio.Sliceable (Array α) Nat (Subarray α) where
mkSlice xs range :=
xs.toSubarray 0 range.upper
let halfOpenRange := Rio.HasRcoIntersection.intersection range 0...<xs.size
(xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
instance : Rii.Sliceable (Array α) Nat (Subarray α) where
mkSlice xs _ :=
xs.toSubarray 0 xs.size
instance : Rcc.Sliceable (Subarray α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Rcc.HasRcoIntersection.intersection range 0...<xs.size
xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
instance : Rco.Sliceable (Subarray α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Rco.HasRcoIntersection.intersection range 0...<xs.size
xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
instance : Rci.Sliceable (Subarray α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Rci.HasRcoIntersection.intersection range 0...<xs.size
xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
instance : Roc.Sliceable (Subarray α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Roc.HasRcoIntersection.intersection range 0...<xs.size
xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
instance : Roo.Sliceable (Subarray α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Roo.HasRcoIntersection.intersection range 0...<xs.size
xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
instance : Roi.Sliceable (Subarray α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Roi.HasRcoIntersection.intersection range 0...<xs.size
xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
instance : Ric.Sliceable (Subarray α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Ric.HasRcoIntersection.intersection range 0...<xs.size
xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
instance : Rio.Sliceable (Subarray α) Nat (Subarray α) where
mkSlice xs range :=
let halfOpenRange := Rio.HasRcoIntersection.intersection range 0...<xs.size
xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
instance : Rii.Sliceable (Subarray α) Nat (Subarray α) where
mkSlice xs _ :=
xs
let halfOpenRange := 0...<xs.size
(xs.toSubarray halfOpenRange.lower halfOpenRange.upper)

View File

@@ -7,75 +7,56 @@ module
prelude
public import Init.Data.Slice.Array.Basic
public import Init.Data.Slice.Operations
import Init.Data.Iterators.Combinators.Attach
public import Init.Data.Iterators.Combinators.ULift
import all Init.Data.Range.Polymorphic.Basic
public import Init.Data.Range.Polymorphic.Iterators
public import Init.Data.Slice.Operations
import Init.Omega
import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
public section
/-!
This module implements an iterator for array slices (`Subarray`).
This module provides slice notation for array slices (a.k.a. `Subarray`) and implements an iterator
for those slices.
-/
open Std Slice PRange Iterators
variable {shape : RangeShape} {α : Type u}
@[unbox]
structure SubarrayIterator (α : Type u) where
xs : Subarray α
@[inline, expose]
def SubarrayIterator.step :
IterM (α := SubarrayIterator α) Id α IterStep (IterM (α := SubarrayIterator α) m α) α
| xs =>
if h : xs.start < xs.stop then
have := xs.start_le_stop; have := xs.stop_le_array_size
.yield xs.array, xs.start + 1, xs.stop, by omega, xs.stop_le_array_size xs.array[xs.start]
else
.done
instance : Iterator (SubarrayIterator α) Id α where
IsPlausibleStep it step := step = SubarrayIterator.step it
step it := pure <| .deflate SubarrayIterator.step it, rfl
private def SubarrayIterator.instFinitelessRelation : FinitenessRelation (SubarrayIterator α) Id where
rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.xs.stop - it.internalState.xs.start)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step] at h
split at h
· cases h
simp only [InvImage, Subarray.stop, Subarray.start, WellFoundedRelation.rel, InvImage,
Nat.lt_wfRel, sizeOf_nat]
exact Nat.sub_succ_lt_self _ _ _
· cases h
instance SubarrayIterator.instFinite : Finite (SubarrayIterator α) Id :=
.of_finitenessRelation instFinitelessRelation
instance [Monad m] : IteratorCollect (SubarrayIterator α) Id m := .defaultImplementation
instance [Monad m] : IteratorCollectPartial (SubarrayIterator α) Id m := .defaultImplementation
instance [Monad m] : IteratorLoop (SubarrayIterator α) Id m := .defaultImplementation
instance [Monad m] : IteratorLoopPartial (SubarrayIterator α) Id m := .defaultImplementation
@[inline, expose]
def Subarray.instToIterator :=
ToIterator.of (γ := Slice (Internal.SubarrayData α)) (β := α) (SubarrayIterator α) (·)
attribute [instance] Subarray.instToIterator
instance {s : Subarray α} : ToIterator s Id α :=
.of _
(Rco.Internal.iter (s.internalRepresentation.start...<s.internalRepresentation.stop)
|>.attachWith (· < s.internalRepresentation.array.size) ?h
|>.uLift
|>.map fun | .up i => s.internalRepresentation.array[i.1])
where finally
case h =>
simp only [Rco.Internal.isPlausibleIndirectOutput_iter_iff, Membership.mem, and_imp]
intro out _ h
have := s.internalRepresentation.stop_le_array_size
omega
universe v w
instance : SliceSize (Internal.SubarrayData α) where
size s := s.internalRepresentation.stop - s.internalRepresentation.start
@[no_expose] instance {s : Subarray α} : Iterator (ToIterator.State s Id) Id α := inferInstance
@[no_expose] instance {s : Subarray α} : Finite (ToIterator.State s Id) Id := inferInstance
@[no_expose] instance {s : Subarray α} : IteratorCollect (ToIterator.State s Id) Id Id := inferInstance
@[no_expose] instance {s : Subarray α} : IteratorCollectPartial (ToIterator.State s Id) Id Id := inferInstance
@[no_expose] instance {s : Subarray α} {m : Type v Type w} [Monad m] :
IteratorLoop (ToIterator.State s Id) Id m := inferInstance
@[no_expose] instance {s : Subarray α} {m : Type v Type w} [Monad m] :
IteratorLoopPartial (ToIterator.State s Id) Id m := inferInstance
@[no_expose] instance {s : Subarray α} :
IteratorSize (ToIterator.State s Id) Id := inferInstance
@[no_expose] instance {s : Subarray α} :
IteratorSizePartial (ToIterator.State s Id) Id := inferInstance
instance {α : Type u} {m : Type v Type w} [Monad m] : ForIn m (Subarray α) α :=
inferInstance
@[no_expose]
instance {α : Type u} {m : Type v Type w} :
ForIn m (Subarray α) α where
forIn xs init f := forIn (Std.Slice.Internal.iter xs) init f
/-!
Without defining the following function `Subarray.foldlM`, it is still possible to call

View File

@@ -8,750 +8,41 @@ module
prelude
import all Init.Data.Array.Subarray
import all Init.Data.Slice.Array.Basic
import Init.Data.Slice.Lemmas
public import Init.Data.Slice.Array.Iterator
import all Init.Data.Slice.Array.Iterator
import all Init.Data.Slice.Operations
import all Init.Data.Range.Polymorphic.Iterators
public import Init.Data.Range.Polymorphic.Lemmas
import all Init.Data.Range.Polymorphic.Lemmas
public import Init.Data.Slice.Lemmas
public import Init.Data.Iterators.Lemmas
import Init.Data.Slice.List.Lemmas
import Init.Data.Range.Polymorphic.NatLemmas
open Std Std.Iterators Std.PRange Std.Slice
public section
namespace SubarrayIterator
open Std.Iterators Std.PRange
theorem step_eq {it : Iter (α := SubarrayIterator α) α} :
it.step = if h : it.1.xs.start < it.1.xs.stop then
haveI := it.1.xs.start_le_stop
haveI := it.1.xs.stop_le_array_size
.yield it.1.xs.array, it.1.xs.start + 1, it.1.xs.stop, by omega, by assumption
(it.1.xs.array[it.1.xs.start]'(by omega)),
(by
simp_all [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
SubarrayIterator.step, Iter.toIterM])
else
.done, (by
simpa [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
SubarrayIterator.step] using h) := by
simp only [Iter.step, IterM.Step.toPure, Iter.toIter_toIterM, IterStep.mapIterator, IterM.step,
Iterator.step, SubarrayIterator.step, Id.run_pure, Shrink.inflate_deflate]
by_cases h : it.internalState.xs.start < it.internalState.xs.stop
· simp only [h, reduceDIte]
split
· rfl
· rename_i h'
exact h'.elim h
· simp only [h, reduceDIte]
split
· rename_i h'
exact h.elim h'
· rfl
namespace Std.Slice.Array
theorem val_step_eq {it : Iter (α := SubarrayIterator α) α} :
it.step.val = if h : it.1.xs.start < it.1.xs.stop then
haveI := it.1.xs.start_le_stop
haveI := it.1.xs.stop_le_array_size
.yield it.1.xs.array, it.1.xs.start + 1, it.1.xs.stop, by omega, by assumption
it.1.xs.array[it.1.xs.start]
else
.done := by
simp only [step_eq]
split <;> simp
private theorem internalIter_Rco_eq {α : Type u} {s : Subarray α} :
Internal.iter s = (Rco.Internal.iter (s.start...<s.stop)
|>.attachWith (· < s.array.size)
(fun out h => h
|> Rco.Internal.isPlausibleIndirectOutput_iter_iff.mp
|> Rco.lt_upper_of_mem
|> (Nat.lt_of_lt_of_le · s.stop_le_array_size))
|>.uLift
|>.map fun | .up i => s.array[i.1]) := by
simp [Internal.iter, ToIterator.iter_eq, Subarray.start, Subarray.stop, Subarray.array]
theorem toList_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} :
it.toList =
(it.internalState.xs.array.toList.take it.internalState.xs.stop).drop it.internalState.xs.start := by
induction it using Iter.inductSteps with | step it ihy ihs
rw [Iter.toList_eq_match_step, SubarrayIterator.val_step_eq]
by_cases h : it.internalState.xs.start < it.internalState.xs.stop
· simp [h]
have := it.1.xs.start_le_stop
have := it.1.xs.stop_le_array_size
rw [ihy (out := it.internalState.xs.array[it.internalState.xs.start])]
· simp only [Subarray.start]
rw (occs := [2]) [List.drop_eq_getElem_cons]; rotate_left
· rw [List.length_take]
simp [it.internalState.xs.stop_le_array_size]
exact h
· simp [Subarray.array, Subarray.stop]
· simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
IterStep.mapIterator_yield, SubarrayIterator.step]
rw [dif_pos]; rotate_left; exact h
rfl
· rw [dif_neg]; rotate_left; exact h
simp_all [it.internalState.xs.stop_le_array_size]
theorem count_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} :
it.count = it.internalState.xs.stop - it.internalState.xs.start := by
simp [ Iter.length_toList_eq_count, toList_eq, it.internalState.xs.stop_le_array_size]
end SubarrayIterator
namespace Subarray
theorem internalIter_eq {α : Type u} {s : Subarray α} :
Internal.iter s = s :=
rfl
theorem toList_internalIter {α : Type u} {s : Subarray α} :
private theorem toList_internalIter {α : Type u} {s : Subarray α} :
(Internal.iter s).toList =
(s.array.toList.take s.stop).drop s.start := by
simp [SubarrayIterator.toList_eq, Internal.iter_eq_toIteratorIter, ToIterator.iter_eq]
public instance : LawfulSliceSize (Internal.SubarrayData α) where
lawful s := by
simp [SliceSize.size, ToIterator.iter_eq, Iter.toIter_toIterM,
Iter.length_toList_eq_count, SubarrayIterator.toList_eq,
s.internalRepresentation.stop_le_array_size, start, stop, array]
public theorem toArray_eq_sliceToArray {α : Type u} {s : Subarray α} :
s.toArray = Slice.toArray s := by
simp [Subarray.toArray, Array.ofSubarray]
@[simp]
public theorem forIn_toList {α : Type u} {s : Subarray α}
{m : Type v Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
{f : α γ m (ForInStep γ)} :
ForIn.forIn s.toList init f = ForIn.forIn s init f :=
Slice.forIn_toList
@[simp]
public theorem forIn_toArray {α : Type u} {s : Subarray α}
{m : Type v Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
{f : α γ m (ForInStep γ)} :
ForIn.forIn s.toArray init f = ForIn.forIn s init f :=
Slice.forIn_toArray
end Subarray
public theorem Array.toSubarray_eq_toSubarray_of_min_eq_min {xs : Array α}
{start stop stop' : Nat} (h : min stop xs.size = min stop' xs.size) :
xs.toSubarray start stop = xs.toSubarray start stop' := by
simp only [Array.toSubarray]
split
· split
· have h₁ : start xs.size := by omega
have h₂ : start stop' := by omega
simp only [dif_pos h₁, dif_pos h₂]
split
· simp_all
· simp_all [Nat.min_eq_right (Nat.le_of_lt _)]
· simp only [Nat.min_eq_left, *] at h
split
· simp only [Nat.min_eq_left, *] at h
simp only [h, right_eq_dite_iff, Slice.mk.injEq, Internal.SubarrayData.mk.injEq, and_true,
true_and]
omega
· simp only [ge_iff_le, not_false_eq_true, Nat.min_eq_right (Nat.le_of_not_ge _), *] at h
simp [h]
omega
· split
· split
· simp only [not_false_eq_true, Nat.min_eq_right (Nat.le_of_not_ge _),
Nat.min_eq_left, Nat.not_le, *] at *
simp [*]; omega
· simp
· simp [Nat.min_eq_right (Nat.le_of_not_ge _), *] at h
split
· simp only [Nat.min_eq_left, *] at h
simp [*]; omega
· simp
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
simp only [Array.toSubarray]
split <;> split <;> simp [Nat.min_eq_right (Nat.le_of_not_ge _), *]
@[simp]
public theorem Array.array_toSubarray {xs : Array α} {lo hi : Nat} :
(xs.toSubarray lo hi).array = xs := by
simp [toSubarray_eq_min, Subarray.array]
@[simp]
public theorem Array.start_toSubarray {xs : Array α} {lo hi : Nat} :
(xs.toSubarray lo hi).start = min lo (min hi xs.size) := by
simp [toSubarray_eq_min, Subarray.start]
@[simp]
public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
(xs.toSubarray lo hi).stop = min hi xs.size := by
simp [toSubarray_eq_min, Subarray.stop]
theorem Subarray.toList_eq {xs : Subarray α} :
xs.toList = (xs.array.extract xs.start xs.stop).toList := by
let aslice := xs
obtain array, start, stop, h₁, h₂ := xs
let lslice : ListSlice α := array.toList.drop start, some (stop - start)
simp only [Subarray.start, Subarray.stop, Subarray.array]
change aslice.toList = _
have : aslice.toList = lslice.toList := by
rw [ListSlice.toList_eq]
simp only [aslice, lslice, Std.Slice.toList, toList_internalIter]
apply List.ext_getElem
· have : stop - start array.size - start := by omega
simp [Subarray.start, Subarray.stop, *, Subarray.array]
· intros
simp [Subarray.array, Subarray.start, Subarray.stop]
simp [this, ListSlice.toList_eq, lslice]
public theorem Subarray.size_eq {xs : Subarray α} :
xs.size = xs.stop - xs.start := by
simp [Subarray.size]
@[simp]
public theorem Subarray.toArray_toList {xs : Subarray α} :
xs.toList.toArray = xs.toArray := by
simp [Std.Slice.toList, Subarray.toArray, Array.ofSubarray, Std.Slice.toArray]
@[simp]
public theorem Subarray.toList_toArray {xs : Subarray α} :
xs.toArray.toList = xs.toList := by
simp [Std.Slice.toList, Subarray.toArray, Array.ofSubarray, Std.Slice.toArray]
@[simp]
public theorem Subarray.length_toList {xs : Subarray α} :
xs.toList.length = xs.size := by
have : xs.start xs.stop := xs.internalRepresentation.start_le_stop
have : xs.stop xs.array.size := xs.internalRepresentation.stop_le_array_size
simp [Subarray.toList_eq, Subarray.size]; omega
@[simp]
public theorem Subarray.size_toArray {xs : Subarray α} :
xs.toArray.size = xs.size := by
simp [ Subarray.toArray_toList, Subarray.size, Slice.size, SliceSize.size, start, stop]
namespace Array
@[simp]
public theorem array_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].array = xs := by
simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp]
public theorem start_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].start = min lo (min hi xs.size) := by
simp [Std.Rco.Sliceable.mkSlice]
@[simp]
public theorem stop_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].stop = min hi xs.size := by
simp [Std.Rco.Sliceable.mkSlice]
public theorem mkSlice_rco_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
xs[lo...hi] = xs[(min lo (min hi xs.size))...(min hi xs.size)] := by
simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray_eq_min]
@[simp]
public theorem toList_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
rw [List.take_eq_take_min, List.drop_eq_drop_min]
simp [Std.Rco.Sliceable.mkSlice, Subarray.toList_eq, List.take_drop,
Nat.add_sub_of_le (Nat.min_le_right _ _)]
@[simp]
public theorem toArray_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].toArray = xs.extract lo hi := by
simp only [ Subarray.toArray_toList, toList_mkSlice_rco]
rw [show xs = xs.toList.toArray by simp, List.extract_toArray, List.extract_eq_drop_take]
simp only [List.take_drop, mk.injEq]
by_cases h : lo hi
· congr 1
rw [List.take_eq_take_iff, Nat.add_sub_cancel' h]
· rw [List.drop_eq_nil_of_le, List.drop_eq_nil_of_le]
· simp; omega
· simp; omega
@[simp]
public theorem size_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].size = min hi xs.size - lo := by
simp [ Subarray.length_toList]
@[simp]
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...=hi] = xs[lo...(hi + 1)] := by
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
public theorem mkSlice_rcc_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
xs[lo...=hi] = xs[(min lo (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp]
public theorem array_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
xs[lo...=hi].array = xs := by
simp [Std.Rcc.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp]
public theorem start_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
xs[lo...=hi].start = min lo (min (hi + 1) xs.size) := by
simp [Std.Rco.Sliceable.mkSlice]
@[simp]
public theorem stop_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
xs[lo...=hi].stop = min (hi + 1) xs.size := by
simp [Std.Rco.Sliceable.mkSlice]
@[simp]
public theorem toList_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
xs[lo...=hi].toList = (xs.toList.take (hi + 1)).drop lo := by
simp
@[simp]
public theorem toArray_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
xs[lo...=hi].toArray = xs.extract lo (hi + 1) := by
simp
@[simp]
public theorem size_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
xs[lo...=hi].size = min (hi + 1) xs.size - lo := by
simp [ Subarray.length_toList]
@[simp]
public theorem array_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo...*].array = xs := by
simp [Std.Rci.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp]
public theorem start_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo...*].start = min lo xs.size := by
simp [Std.Rci.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
@[simp]
public theorem stop_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo...*].stop = xs.size := by
simp [Std.Rci.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
@[simp]
public theorem mkSlice_rci_eq_mkSlice_rco {xs : Array α} {lo : Nat} :
xs[lo...*] = xs[lo...xs.size] := by
simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
public theorem mkSlice_rci_eq_mkSlice_rco_min {xs : Array α} {lo : Nat} :
xs[lo...*] = xs[(min lo xs.size)...xs.size] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp]
public theorem toList_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo...*].toList = xs.toList.drop lo := by
rw [mkSlice_rci_eq_mkSlice_rco, toList_mkSlice_rco, Array.length_toList, List.take_length]
@[simp]
public theorem toArray_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo...*].toArray = xs.extract lo := by
simp
@[simp]
public theorem size_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo...*].size = xs.size - lo := by
simp [ Subarray.length_toList]
@[simp]
public theorem array_mkSlice_roo {xs : Array α} {lo hi : Nat} :
xs[lo<...hi].array = xs := by
simp [Std.Roo.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp]
public theorem start_mkSlice_roo {xs : Array α} {lo hi : Nat} :
xs[lo<...hi].start = min (lo + 1) (min hi xs.size) := by
simp [Std.Roo.Sliceable.mkSlice]
@[simp]
public theorem stop_mkSlice_roo {xs : Array α} {lo hi : Nat} :
xs[lo<...hi].stop = min hi xs.size := by
simp [Std.Roo.Sliceable.mkSlice]
@[simp]
public theorem mkSlice_roo_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo<...hi] = xs[(lo + 1)...hi] := by
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
public theorem mkSlice_roo_eq_mkSlice_roo_min {xs : Array α} {lo hi : Nat} :
xs[lo<...hi] = xs[(min (lo + 1) (min hi xs.size))...(min hi xs.size)] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp]
public theorem toList_mkSlice_roo {xs : Array α} {lo hi : Nat} :
xs[lo<...hi].toList = (xs.toList.take hi).drop (lo + 1) := by
simp
@[simp]
public theorem toArray_mkSlice_roo {xs : Array α} {lo hi : Nat} :
xs[lo<...hi].toArray = xs.extract (lo + 1) hi := by
simp
@[simp]
public theorem size_mkSlice_roo {xs : Array α} {lo hi : Nat} :
xs[lo<...hi].size = min hi xs.size - (lo + 1) := by
simp [ Subarray.length_toList]
@[simp]
public theorem array_mkSlice_roc {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi].array = xs := by
simp [Std.Roc.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp]
public theorem start_mkSlice_roc {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi].start = min (lo + 1) (min (hi + 1) xs.size) := by
simp [Std.Roc.Sliceable.mkSlice]
@[simp]
public theorem stop_mkSlice_roc {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi].stop = min (hi + 1) xs.size := by
simp [Std.Roc.Sliceable.mkSlice]
@[simp]
public theorem mkSlice_roc_eq_mkSlice_roo {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice]
public theorem mkSlice_roc_eq_mkSlice_roo_min {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi] = xs[(min (lo + 1) (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp]
public theorem toList_mkSlice_roc {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi].toList = (xs.toList.take (hi + 1)).drop (lo + 1) := by
simp
@[simp]
public theorem toArray_mkSlice_roc {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi].toArray = xs.extract (lo + 1) (hi + 1) := by
simp
@[simp]
public theorem size_mkSlice_roc {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi].size = min (hi + 1) xs.size - (lo + 1) := by
simp [ Subarray.length_toList]
@[simp]
public theorem array_mkSlice_roi {xs : Array α} {lo : Nat} :
xs[lo<...*].array = xs := by
simp [Std.Roi.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp]
public theorem start_mkSlice_roi {xs : Array α} {lo : Nat} :
xs[lo<...*].start = min (lo + 1) xs.size := by
simp [Std.Roi.Sliceable.mkSlice, Std.Roi.HasRcoIntersection.intersection]
@[simp]
public theorem stop_mkSlice_roi {xs : Array α} {lo : Nat} :
xs[lo...*].stop = xs.size := by
simp [Std.Rco.Sliceable.mkSlice]
@[simp]
public theorem mkSlice_roi_eq_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo<...*] = xs[(lo + 1)...*] := by
simp [Std.Roi.Sliceable.mkSlice, Std.Roi.HasRcoIntersection.intersection,
Std.Rci.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
public theorem mkSlice_roi_eq_mkSlice_roo {xs : Array α} {lo : Nat} :
xs[lo<...*] = xs[lo<...xs.size] := by
simp [mkSlice_rci_eq_mkSlice_rco]
public theorem mkSlice_roi_eq_mkSlice_roo_min {xs : Array α} {lo : Nat} :
xs[lo<...*] = xs[(min (lo + 1) xs.size)...xs.size] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp]
public theorem toList_mkSlice_roi {xs : Array α} {lo : Nat} :
xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
rw [mkSlice_roi_eq_mkSlice_rci, toList_mkSlice_rci]
@[simp]
public theorem toArray_mkSlice_roi {xs : Array α} {lo : Nat} :
xs[lo<...*].toArray = xs.drop (lo + 1) := by
simp
@[simp]
public theorem size_mkSlice_roi {xs : Array α} {lo : Nat} :
xs[lo<...*].size = xs.size - (lo + 1) := by
simp [ Subarray.length_toList]
@[simp]
public theorem array_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...hi].array = xs := by
simp [Std.Rio.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp]
public theorem start_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...hi].start = 0 := by
simp [Std.Rio.Sliceable.mkSlice]
@[simp]
public theorem stop_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...hi].stop = min hi xs.size := by
simp [Std.Rio.Sliceable.mkSlice]
@[simp]
public theorem mkSlice_rio_eq_mkSlice_rco {xs : Array α} {hi : Nat} :
xs[*...hi] = xs[0...hi] := by
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
public theorem mkSlice_rio_eq_mkSlice_rio_min {xs : Array α} {hi : Nat} :
xs[*...hi] = xs[*...(min hi xs.size)] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp]
public theorem toList_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...hi].toList = xs.toList.take hi := by
simp
@[simp]
public theorem toArray_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...hi].toArray = xs.extract 0 hi := by
simp
@[simp]
public theorem size_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...hi].size = min hi xs.size := by
simp [ Subarray.length_toList]
@[simp]
public theorem array_mkSlice_ric {xs : Array α} {hi : Nat} :
xs[*...=hi].array = xs := by
simp [Std.Ric.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp]
public theorem start_mkSlice_ric {xs : Array α} {hi : Nat} :
xs[*...=hi].start = 0 := by
simp [Std.Ric.Sliceable.mkSlice]
@[simp]
public theorem stop_mkSlice_ric {xs : Array α} {hi : Nat} :
xs[*...=hi].stop = min (hi + 1) xs.size := by
simp [Std.Ric.Sliceable.mkSlice]
@[simp]
public theorem mkSlice_ric_eq_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...=hi] = xs[*...(hi + 1)] := by
simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice]
public theorem mkSlice_ric_eq_mkSlice_rio_min {xs : Array α} {hi : Nat} :
xs[*...=hi] = xs[*...(min (hi + 1) xs.size)] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp]
public theorem toList_mkSlice_ric {xs : Array α} {hi : Nat} :
xs[*...=hi].toList = xs.toList.take (hi + 1) := by
simp
@[simp]
public theorem toArray_mkSlice_ric {xs : Array α} {hi : Nat} :
xs[*...=hi].toArray = xs.extract 0 (hi + 1) := by
simp
@[simp]
public theorem size_mkSlice_ric {xs : Array α} {hi : Nat} :
xs[*...=hi].size = min (hi + 1) xs.size := by
simp [ Subarray.length_toList]
@[simp]
public theorem mkSlice_rii_eq_mkSlice_rci {xs : Array α} :
xs[*...*] = xs[0...*] := by
simp [Std.Rii.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice,
Std.Rci.HasRcoIntersection.intersection]
public theorem mkSlice_rii_eq_mkSlice_rio {xs : Array α} :
xs[*...*] = xs[*...xs.size] := by
simp [mkSlice_rci_eq_mkSlice_rco]
public theorem mkSlice_rii_eq_mkSlice_rio_min {xs : Array α} :
xs[*...*] = xs[*...xs.size] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp]
public theorem toList_mkSlice_rii {xs : Array α} :
xs[*...*].toList = xs.toList := by
rw [mkSlice_rii_eq_mkSlice_rci, toList_mkSlice_rci, List.drop_zero]
@[simp]
public theorem toArray_mkSlice_rii {xs : Array α} :
xs[*...*].toArray = xs := by
simp
@[simp]
public theorem size_mkSlice_rii {xs : Array α} :
xs[*...*].size = xs.size := by
simp [ Subarray.length_toList]
@[simp]
public theorem array_mkSlice_rii {xs : Array α} :
xs[*...*].array = xs := by
simp
@[simp]
public theorem start_mkSlice_rii {xs : Array α} :
xs[*...*].start = 0 := by
simp
@[simp]
public theorem stop_mkSlice_rii {xs : Array α} :
xs[*...*].stop = xs.size := by
simp [Std.Rii.Sliceable.mkSlice]
end Array
section SubarraySlices
namespace Subarray
@[simp]
public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
simp only [Std.Rco.Sliceable.mkSlice, Std.Rco.HasRcoIntersection.intersection, toList_eq,
Array.start_toSubarray, Array.stop_toSubarray, Array.toList_extract, List.take_drop,
List.take_take]
rw [Nat.add_sub_cancel' (by omega)]
simp [Subarray.size, Array.length_toList, List.take_eq_take_min, Nat.add_comm xs.start]
@[simp]
public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
xs[lo...hi].toArray = xs.toArray.extract lo hi := by
simp [ Subarray.toArray_toList, List.drop_take]
@[simp]
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
xs[lo...=hi] = xs[lo...(hi + 1)] := by
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
Std.Rcc.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
@[simp]
public theorem toList_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
xs[lo...=hi].toList = (xs.toList.take (hi + 1)).drop lo := by
simp
@[simp]
public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
xs[lo...=hi].toArray = xs.toArray.extract lo (hi + 1) := by
simp
@[simp]
public theorem mkSlice_rci_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
xs[lo...*] = xs[lo...xs.size] := by
simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
Std.Rci.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
@[simp]
public theorem toList_mkSlice_rci {xs : Subarray α} {lo : Nat} :
xs[lo...*].toList = xs.toList.drop lo := by
rw [mkSlice_rci_eq_mkSlice_rco, toList_mkSlice_rco, Subarray.length_toList, List.take_length]
@[simp]
public theorem toArray_mkSlice_rci {xs : Subarray α} {lo : Nat} :
xs[lo...*].toArray = xs.toArray.extract lo := by
simp
@[simp]
public theorem mkSlice_roc_eq_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice,
Std.Roc.HasRcoIntersection.intersection, Std.Roo.HasRcoIntersection.intersection]
@[simp]
public theorem mkSlice_roo_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
xs[lo<...hi] = xs[(lo + 1)...hi] := by
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
Std.Roo.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
@[simp]
public theorem toList_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
xs[lo<...hi].toList = (xs.toList.take hi).drop (lo + 1) := by
simp
@[simp]
public theorem toArray_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
xs[lo<...hi].toArray = xs.toArray.extract (lo + 1) hi := by
simp
@[simp]
public theorem mkSlice_roc_eq_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
Std.Roc.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
@[simp]
public theorem toList_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
xs[lo<...=hi].toList = (xs.toList.take (hi + 1)).drop (lo + 1) := by
simp
@[simp]
public theorem toArray_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
xs[lo<...=hi].toArray = xs.toArray.extract (lo + 1) (hi + 1) := by
simp
@[simp]
public theorem mkSlice_roi_eq_mkSlice_rci {xs : Subarray α} {lo : Nat} :
xs[lo<...*] = xs[(lo + 1)...*] := by
simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice,
Std.Roi.HasRcoIntersection.intersection, Std.Rci.HasRcoIntersection.intersection]
@[simp]
public theorem toList_mkSlice_roi {xs : Subarray α} {lo : Nat} :
xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
rw [mkSlice_roi_eq_mkSlice_rci, toList_mkSlice_rci]
@[simp]
public theorem toArray_mkSlice_roi {xs : Subarray α} {lo : Nat} :
xs[lo<...*].toArray = xs.toArray.extract (lo + 1) := by
simp
@[simp]
public theorem mkSlice_ric_eq_mkSlice_rio {xs : Subarray α} {hi : Nat} :
xs[*...=hi] = xs[*...(hi + 1)] := by
simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice,
Std.Ric.HasRcoIntersection.intersection, Std.Rio.HasRcoIntersection.intersection]
@[simp]
public theorem mkSlice_rio_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} :
xs[*...hi] = xs[0...hi] := by
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
Std.Rio.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
@[simp]
public theorem toList_mkSlice_rio {xs : Subarray α} {hi : Nat} :
xs[*...hi].toList = xs.toList.take hi := by
simp
@[simp]
public theorem toArray_mkSlice_rio {xs : Subarray α} {hi : Nat} :
xs[*...hi].toArray = xs.toArray.extract 0 hi := by
simp
@[simp]
public theorem mkSlice_ric_eq_mkSlice_rcc {xs : Subarray α} {hi : Nat} :
xs[*...=hi] = xs[0...=hi] := by
simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
Std.Ric.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
@[simp]
public theorem toList_mkSlice_ric {xs : Subarray α} {hi : Nat} :
xs[*...=hi].toList = xs.toList.take (hi + 1) := by
simp
@[simp]
public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} :
xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by
simp
@[simp]
public theorem mkSlice_rii {xs : Subarray α} :
xs[*...*] = xs := by
simp [Std.Rii.Sliceable.mkSlice]
@[simp]
public theorem toList_mkSlice_rii {xs : Subarray α} :
xs[*...*].toList = xs.toList := by
rw [mkSlice_rii]
@[simp]
public theorem toArray_mkSlice_rii {xs : Subarray α} :
xs[*...*].toArray = xs.toArray := by
rw [mkSlice_rii]
end Subarray
end SubarraySlices
((s.start...s.stop).toList
|>.attachWith (· < s.array.size)
(fun out h => h
|> Rco.mem_toList_iff_mem.mp
|> Rco.lt_upper_of_mem
|> (Nat.lt_of_lt_of_le · s.stop_le_array_size))
|>.map fun i => s.array[i.1]) := by
rw [internalIter_Rco_eq, Iter.toList_map, Iter.toList_uLift, Iter.toList_attachWith]
simp [Rco.toList]
end Std.Slice.Array

View File

@@ -8,9 +8,7 @@ module
prelude
public import Init.Data.Slice.Operations
import all Init.Data.Slice.Operations
import Init.Data.Iterators.Consumers
import Init.Data.Iterators.Lemmas.Consumers
public import Init.Data.List.Control
public section
@@ -18,104 +16,63 @@ namespace Std.Slice
open Std.Iterators
variable {γ : Type u} {α β : Type v}
variable {γ : Type u} {β : Type v}
theorem Internal.iter_eq_toIteratorIter {γ : Type u}
[ToIterator (Slice γ) Id α β] {s : Slice γ} :
theorem Internal.iter_eq_toIteratorIter {γ : Type u} {s : Slice γ}
[ToIterator s Id β] :
Internal.iter s = ToIterator.iter s :=
(rfl)
theorem forIn_internalIter {γ : Type u} {β : Type v}
{m : Type w Type x} [Monad m] {δ : Type w}
[ToIterator (Slice γ) Id α β]
[Iterator α Id β]
[IteratorLoop α Id m]
[LawfulIteratorLoop α Id m]
[Finite α Id] {s : Slice γ}
{init : δ} {f : β δ m (ForInStep δ)} :
ForIn.forIn (Internal.iter s) init f = ForIn.forIn s init f :=
theorem Internal.size_eq_size_iter {s : Slice γ} [ToIterator s Id β]
[Iterator (ToIterator.State s Id) Id β] [IteratorSize (ToIterator.State s Id) Id] :
s.size = (Internal.iter s).size :=
(rfl)
@[simp]
public theorem forIn_toList {γ : Type u} {β : Type v}
{m : Type w Type x} [Monad m] [LawfulMonad m] {δ : Type w}
[ToIterator (Slice γ) Id α β]
[Iterator α Id β]
[IteratorLoop α Id m]
[LawfulIteratorLoop α Id m]
[IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id]
[Finite α Id] {s : Slice γ}
{init : δ} {f : β δ m (ForInStep δ)} :
ForIn.forIn s.toList init f = ForIn.forIn s init f := by
rw [ forIn_internalIter, Iter.forIn_toList, Slice.toList]
@[simp]
public theorem forIn_toArray {γ : Type u} {β : Type v}
{m : Type w Type x} [Monad m] [LawfulMonad m] {δ : Type w}
[ToIterator (Slice γ) Id α β]
[Iterator α Id β]
[IteratorLoop α Id m]
[LawfulIteratorLoop α Id m]
[IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id]
[Finite α Id] {s : Slice γ}
{init : δ} {f : β δ m (ForInStep δ)} :
ForIn.forIn s.toArray init f = ForIn.forIn s init f := by
rw [ forIn_internalIter, Iter.forIn_toArray, Slice.toArray]
theorem Internal.size_eq_count_iter [ToIterator (Slice γ) Id α β]
[Iterator α Id β] [Finite α Id]
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
{s : Slice γ} [SliceSize γ] [LawfulSliceSize γ] :
s.size = (Internal.iter s).count := by
letI : IteratorCollect α Id Id := .defaultImplementation
simp only [Slice.size, iter, LawfulSliceSize.lawful, Iter.length_toList_eq_count]
theorem Internal.toArray_eq_toArray_iter {s : Slice γ} [ToIterator (Slice γ) Id α β]
[Iterator α Id β] [IteratorCollect α Id Id]
[Finite α Id] :
theorem Internal.toArray_eq_toArray_iter {s : Slice γ} [ToIterator s Id β]
[Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id]
[Finite (ToIterator.State s Id) Id] :
s.toArray = (Internal.iter s).toArray :=
(rfl)
theorem Internal.toList_eq_toList_iter {s : Slice γ} [ToIterator (Slice γ) Id α β]
[Iterator α Id β] [IteratorCollect α Id Id]
[Finite α Id] :
theorem Internal.toList_eq_toList_iter {s : Slice γ} [ToIterator s Id β]
[Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id]
[Finite (ToIterator.State s Id) Id] :
s.toList = (Internal.iter s).toList :=
(rfl)
theorem Internal.toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator (Slice γ) Id α β]
[Iterator α Id β] [Finite α Id] :
theorem Internal.toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator s Id β]
[Iterator (ToIterator.State s Id) Id β] [Finite (ToIterator.State s Id) Id] :
s.toListRev = (Internal.iter s).toListRev :=
(rfl)
@[simp]
theorem size_toArray_eq_size [ToIterator (Slice γ) Id α β]
[Iterator α Id β] [SliceSize γ] [LawfulSliceSize γ]
[IteratorCollect α Id Id] [Finite α Id]
[LawfulIteratorCollect α Id Id] {s : Slice γ} :
theorem size_toArray_eq_size {s : Slice γ} [ToIterator s Id β]
[Iterator (ToIterator.State s Id) Id β] [IteratorSize (ToIterator.State s Id) Id]
[IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id]
[LawfulIteratorSize (ToIterator.State s Id)]
[LawfulIteratorCollect (ToIterator.State s Id) Id Id] :
s.toArray.size = s.size := by
letI : IteratorLoop α Id Id := .defaultImplementation
rw [Internal.size_eq_count_iter, Internal.toArray_eq_toArray_iter, Iter.size_toArray_eq_count]
simp [Internal.size_eq_size_iter, Internal.toArray_eq_toArray_iter,
Iter.size_toArray_eq_size]
@[simp]
theorem length_toList_eq_size [ToIterator (Slice γ) Id α β]
[Iterator α Id β] {s : Slice γ}
[SliceSize γ] [LawfulSliceSize γ] [IteratorCollect α Id Id]
[Finite α Id] [LawfulIteratorCollect α Id Id] :
theorem length_toList_eq_size {s : Slice γ} [ToIterator s Id β]
[Iterator (ToIterator.State s Id) Id β] [IteratorSize (ToIterator.State s Id) Id]
[IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id]
[LawfulIteratorSize (ToIterator.State s Id)]
[LawfulIteratorCollect (ToIterator.State s Id) Id Id] :
s.toList.length = s.size := by
letI : IteratorLoop α Id Id := .defaultImplementation
rw [Internal.size_eq_count_iter, Internal.toList_eq_toList_iter, Iter.length_toList_eq_count]
simp [Internal.size_eq_size_iter, Internal.toList_eq_toList_iter,
Iter.length_toList_eq_size]
@[simp]
theorem length_toListRev_eq_size [ToIterator (Slice γ) Id α β]
[Iterator α Id β] {s : Slice γ}
[IteratorLoop α Id Id.{v}] [SliceSize γ] [LawfulSliceSize γ]
[Finite α Id]
[LawfulIteratorLoop α Id Id] :
theorem length_toListRev_eq_size {s : Slice γ} [ToIterator s Id β]
[Iterator (ToIterator.State s Id) Id β] [IteratorSize (ToIterator.State s Id) Id]
[IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id]
[LawfulIteratorSize (ToIterator.State s Id)]
[LawfulIteratorCollect (ToIterator.State s Id) Id Id] :
s.toListRev.length = s.size := by
letI : IteratorCollect α Id Id := .defaultImplementation
rw [Internal.size_eq_count_iter, Internal.toListRev_eq_toListRev_iter,
Iter.length_toListRev_eq_count]
simp [Internal.size_eq_size_iter, Internal.toListRev_eq_toListRev_iter,
Iter.length_toListRev_eq_size]
end Std.Slice

View File

@@ -1,11 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Slice.List.Basic
public import Init.Data.Slice.List.Iterator
public import Init.Data.Slice.List.Lemmas

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