Compare commits

..

1 Commits

Author SHA1 Message Date
Leonardo de Moura
7786813bef chore: remove dead code at Structure.lean 2024-04-27 15:54:12 -07:00
1442 changed files with 5380 additions and 21331 deletions

View File

@@ -9,15 +9,9 @@ assignees: ''
### Prerequisites
Please put an X between the brackets as you perform the following steps:
* [ ] Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues
* [ ] Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries.
* [ ] Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
* [ ] Put an X between the brackets on this line if you have done all of the following:
* Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
* Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
### Description
@@ -39,8 +33,8 @@ Please put an X between the brackets as you perform the following steps:
### Versions
[Output of `#eval Lean.versionString`]
[OS version, if not using live.lean-lang.org.]
[Output of `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in]
[OS version]
### Additional Information

View File

@@ -6,6 +6,7 @@ on:
tags:
- '*'
pull_request:
types: [opened, synchronize, reopened, labeled]
merge_group:
schedule:
- cron: '0 7 * * *' # 8AM CET/11PM PT
@@ -20,10 +21,8 @@ jobs:
configure:
runs-on: ubuntu-latest
outputs:
# 0: PRs without special label
# 1: PRs with `merge-ci` label, merge queue checks, master commits
# 2: PRs with `release-ci` label, releases (incl. nightlies)
check-level: ${{ steps.set-level.outputs.check-level }}
# Should we run only a quick CI? Yes on a pull request without the full-ci label
quick: ${{ steps.set-quick.outputs.quick }}
# The build matrix, dynamically generated here
matrix: ${{ steps.set-matrix.outputs.result }}
# Should we make a nightly release? If so, this output contains the lean version string, else it is empty
@@ -40,6 +39,158 @@ jobs:
RELEASE_TAG: ${{ steps.set-release.outputs.RELEASE_TAG }}
steps:
- name: Run quick CI?
id: set-quick
env:
quick: ${{
github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
}}
run: |
echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT"
- name: Configure build matrix
id: set-matrix
uses: actions/github-script@v7
with:
script: |
const quick = ${{ steps.set-quick.outputs.quick }};
console.log(`quick: ${quick}`)
let matrix = [
{
// portable release build: use channel with older glibc (2.27)
"name": "Linux LLVM",
"os": "ubuntu-latest",
"release": false,
"quick": false,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"binary-check": "ldd -v",
// foreign code may be linked against more recent glibc
// reverse-ffi needs to be updated to link to LLVM libraries
"CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
"CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
},
{
"name": "Linux release",
"os": "ubuntu-latest",
"release": true,
"quick": true,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"binary-check": "ldd -v",
// foreign code may be linked against more recent glibc
"CTEST_OPTIONS": "-E 'foreign'"
},
{
"name": "Linux",
"os": "ubuntu-latest",
"check-stage3": true,
"test-speedcenter": true,
"quick": false,
},
{
"name": "Linux Debug",
"os": "ubuntu-latest",
"quick": false,
"CMAKE_OPTIONS": "-DCMAKE_BUILD_TYPE=Debug",
// exclude seriously slow tests
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},
// TODO: suddenly started failing in CI
/*{
"name": "Linux fsanitize",
"os": "ubuntu-latest",
"quick": false,
// turn off custom allocator & symbolic functions to make LSAN do its magic
"CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF",
// exclude seriously slow/problematic tests (laketests crash)
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},*/
{
"name": "macOS",
"os": "macos-13",
"release": true,
"quick": false,
"shell": "bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
"binary-check": "otool -L",
"tar": "gtar" // https://github.com/actions/runner-images/issues/2619
},
{
"name": "macOS aarch64",
"os": "macos-13",
"release": true,
"quick": false,
"cross": true,
"cross_target": "aarch64-apple-darwin",
"shell": "bash -euxo pipefail {0}",
"CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm-aarch64-* lean-llvm-x86_64-*",
"binary-check": "otool -L",
"tar": "gtar" // https://github.com/actions/runner-images/issues/2619
},
{
"name": "Windows",
"os": "windows-2022",
"release": true,
"quick": false,
"shell": "msys2 {0}",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
// for reasons unknown, interactivetests are flaky on Windows
"CTEST_OPTIONS": "--repeat until-pass:2",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
"binary-check": "ldd"
},
{
"name": "Linux aarch64",
"os": "ubuntu-latest",
"CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"release": true,
"quick": false,
"cross": true,
"cross_target": "aarch64-unknown-linux-gnu",
"shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
},
{
"name": "Linux 32bit",
"os": "ubuntu-latest",
// Use 32bit on stage0 and stage1 to keep oleans compatible
"CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86",
"cmultilib": true,
"release": true,
"quick": false,
"cross": true,
"shell": "bash -euxo pipefail {0}"
},
{
"name": "Web Assembly",
"os": "ubuntu-latest",
// Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
"CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32",
"wasm": true,
"cmultilib": true,
"release": true,
"quick": false,
"cross": true,
"shell": "bash -euxo pipefail {0}",
// Just a few selected tests because wasm is slow
"CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean\""
}
];
console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
if (quick) {
return matrix.filter((job) => job.quick)
} else {
return matrix
}
- name: Checkout
uses: actions/checkout@v3
# don't schedule nightlies on forks
@@ -90,171 +241,6 @@ jobs:
echo "Tag ${TAG_NAME} did not match SemVer regex."
fi
- name: Set check level
id: set-level
# We do not use github.event.pull_request.labels.*.name here because
# re-running a run does not update that list, and we do want to be able to
# rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
run: |
check_level=0
if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.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=2
elif echo "$labels" | grep -q "merge-ci"; then
check_level=1
fi
fi
echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
env:
GH_TOKEN: ${{ github.token }}
- name: Configure build matrix
id: set-matrix
uses: actions/github-script@v7
with:
script: |
const level = ${{ steps.set-level.outputs.check-level }};
console.log(`level: ${level}`);
// use large runners outside PRs where available (original repo)
// disabled for now as this mostly just speeds up the test suite which is not a bottleneck
// let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : "";
let matrix = [
{
// portable release build: use channel with older glibc (2.27)
"name": "Linux LLVM",
"os": "ubuntu-latest",
"release": false,
"check-level": 2,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"binary-check": "ldd -v",
// foreign code may be linked against more recent glibc
// reverse-ffi needs to be updated to link to LLVM libraries
"CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
"CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
},
{
"name": "Linux release",
"os": "ubuntu-latest",
"release": true,
"check-level": 0,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"binary-check": "ldd -v",
// foreign code may be linked against more recent glibc
"CTEST_OPTIONS": "-E 'foreign'"
},
{
"name": "Linux",
"os": "ubuntu-latest",
"check-stage3": level >= 2,
"test-speedcenter": level >= 2,
"check-level": 1,
},
{
"name": "Linux Debug",
"os": "ubuntu-latest",
"check-level": 2,
"CMAKE_PRESET": "debug",
// exclude seriously slow tests
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},
// TODO: suddenly started failing in CI
/*{
"name": "Linux fsanitize",
"os": "ubuntu-latest",
"check-level": 2,
// turn off custom allocator & symbolic functions to make LSAN do its magic
"CMAKE_PRESET": "sanitize",
// exclude seriously slow/problematic tests (laketests crash)
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},*/
{
"name": "macOS",
"os": "macos-13",
"release": true,
"check-level": 2,
"shell": "bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
"binary-check": "otool -L",
"tar": "gtar" // https://github.com/actions/runner-images/issues/2619
},
{
"name": "macOS aarch64",
"os": "macos-14",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
"release": true,
"check-level": 1,
"shell": "bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
"binary-check": "otool -L",
"tar": "gtar" // https://github.com/actions/runner-images/issues/2619
},
{
"name": "Windows",
"os": "windows-2022",
"release": true,
"check-level": 2,
"shell": "msys2 {0}",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
// for reasons unknown, interactivetests are flaky on Windows
"CTEST_OPTIONS": "--repeat until-pass:2",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
"binary-check": "ldd"
},
{
"name": "Linux aarch64",
"os": "ubuntu-latest",
"CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"release": true,
"check-level": 2,
"cross": true,
"cross_target": "aarch64-unknown-linux-gnu",
"shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
},
{
"name": "Linux 32bit",
"os": "ubuntu-latest",
// Use 32bit on stage0 and stage1 to keep oleans compatible
"CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86",
"cmultilib": true,
"release": true,
"check-level": 2,
"cross": true,
"shell": "bash -euxo pipefail {0}"
},
{
"name": "Web Assembly",
"os": "ubuntu-latest",
// Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
"CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32",
"wasm": true,
"cmultilib": true,
"release": true,
"check-level": 2,
"cross": true,
"shell": "bash -euxo pipefail {0}",
// Just a few selected tests because wasm is slow
"CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean\""
}
];
console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
return matrix.filter((job) => level >= job["check-level"])
build:
needs: [configure]
if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
@@ -333,9 +319,6 @@ jobs:
# store in current directory, for easy uploading together with binary
echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
if: runner.os == 'Linux'
- name: Set up NPROC
run: |
echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
- name: Build
run: |
mkdir build
@@ -366,8 +349,8 @@ jobs:
OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }})
fi
# contortion to support empty OPTIONS with old macOS bash
cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
make -j$NPROC
cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
make -j4
make install
- name: Check Binaries
run: ${{ matrix.binary-check }} lean-*/bin/* || true
@@ -396,29 +379,32 @@ jobs:
build/stage1/bin/lean --stats src/Lean.lean
if: ${{ !matrix.cross }}
- name: Test
id: test
run: |
cd build/stage1
ulimit -c unlimited # coredumps
ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.check-level >= 1
# exclude nonreproducible test
ctest -j4 --progress --output-junit test-results.xml --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
- name: Test Summary
uses: test-summary/action@v2
with:
paths: build/stage1/test-results.xml
# prefix `if` above with `always` so it's run even if tests failed
if: always() && steps.test.conclusion != 'skipped'
if: always() && (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
- name: Check Test Binary
run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
if: (!matrix.cross) && steps.test.conclusion != 'skipped'
if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}
- name: Build Stage 2
run: |
cd build
ulimit -c unlimited # coredumps
make -C build -j$NPROC stage2
make -j4 stage2
if: matrix.test-speedcenter
- name: Check Stage 3
run: |
cd build
ulimit -c unlimited # coredumps
make -C build -j$NPROC stage3
make -j4 check-stage3
if: matrix.test-speedcenter
- name: Test Speedcenter Benchmarks
run: |
@@ -429,10 +415,11 @@ jobs:
if: matrix.test-speedcenter
- name: Check rebootstrap
run: |
cd build
ulimit -c unlimited # coredumps
# clean rebuild in case of Makefile changes
make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
if: matrix.name == 'Linux' && needs.configure.outputs.check-level >= 1
make update-stage0 && rm -rf ./stage* && make -j4
if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
- name: CCache stats
run: ccache -s
- name: Show stacktrace for coredumps

View File

@@ -6,6 +6,7 @@ on:
tags:
- '*'
pull_request:
types: [opened, synchronize, reopened, labeled]
merge_group:
concurrency:

View File

@@ -126,11 +126,11 @@ jobs:
if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
echo "The merge base of this PR coincides with the nightly release"
BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
if [[ -n "$STD_REMOTE_TAGS" ]]; then
echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
@@ -140,8 +140,8 @@ jobs:
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
else
echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
fi
else
@@ -151,7 +151,7 @@ jobs:
git -C lean4.git fetch origin nightly-with-mathlib
NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
fi
if [[ -n "$MESSAGE" ]]; then
@@ -223,27 +223,27 @@ jobs:
description: description,
});
# We next automatically create a Batteries branch using this toolchain.
# Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
# Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
# We next automatically create a Std branch using this toolchain.
# Std doesn't itself have a mechanism to report results of CI from this branch back to Lean
# Instead this is taken care of by Mathlib CI, which will fail if Std fails.
- name: Cleanup workspace
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
run: |
sudo rm -rf ./*
# Checkout the Batteries repository with all branches
- name: Checkout Batteries repository
# Checkout the Std repository with all branches
- name: Checkout Std repository
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
uses: actions/checkout@v3
with:
repository: leanprover-community/batteries
repository: leanprover/std4
token: ${{ secrets.MATHLIB4_BOT }}
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.
- name: Check if tag exists
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
id: check_batteries_tag
id: check_std_tag
run: |
git config user.name "leanprover-community-mathlib4-bot"
git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
@@ -251,7 +251,7 @@ jobs:
if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
else
echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Std. Falling back to 'nightly-testing'."
BASE=nightly-testing
fi
@@ -268,7 +268,7 @@ jobs:
else
echo "Branch already exists, pushing an empty commit."
git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
# The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
# The Std `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
# (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
@@ -321,7 +321,7 @@ jobs:
git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
git add lean-toolchain
sed -i "s/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \".\+\"/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
sed -i "s/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
git add lakefile.lean
git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
else

View File

@@ -1,31 +0,0 @@
name: Restart by label
on:
pull_request_target:
types:
- unlabeled
- labeled
jobs:
restart-on-label:
runs-on: ubuntu-latest
if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci')
steps:
- run: |
# Finding latest CI workflow run on current pull request
# (unfortunately cannot search by PR number, only base branch,
# and that is't even unique given PRs from forks, but the risk
# of confusion is low and the danger is mild)
run_id=$(gh run list -e pull_request -b "$head_ref" --workflow 'CI' --limit 1 \
--limit 1 --json databaseId --jq '.[0].databaseId')
echo "Run id: ${run_id}"
gh run view "$run_id"
echo "Cancelling (just in case)"
gh run cancel "$run_id" || echo "(failed)"
echo "Waiting for 10s"
sleep 10
echo "Rerunning"
gh run rerun "$run_id"
shell: bash
env:
head_ref: ${{ github.head_ref }}
GH_TOKEN: ${{ github.token }}
GH_REPO: ${{ github.repository }}

View File

@@ -1,83 +0,0 @@
{
"version": 2,
"cmakeMinimumRequired": {
"major": 3,
"minor": 10,
"patch": 0
},
"configurePresets": [
{
"name": "release",
"displayName": "Default development optimized build config",
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/release"
},
{
"name": "debug",
"displayName": "Debug build config",
"cacheVariables": {
"CMAKE_BUILD_TYPE": "Debug"
},
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/debug"
},
{
"name": "sanitize",
"displayName": "Sanitize build config",
"cacheVariables": {
"LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined",
"LEANC_EXTRA_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
"SMALL_ALLOCATOR": "OFF",
"BSYMBOLIC": "OFF"
},
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/sanitize"
},
{
"name": "sandebug",
"inherits": ["debug", "sanitize"],
"displayName": "Sanitize+debug build config",
"binaryDir": "${sourceDir}/build/sandebug"
}
],
"buildPresets": [
{
"name": "release",
"configurePreset": "release"
},
{
"name": "debug",
"configurePreset": "debug"
},
{
"name": "sanitize",
"configurePreset": "sanitize"
},
{
"name": "sandebug",
"configurePreset": "sandebug"
}
],
"testPresets": [
{
"name": "release",
"configurePreset": "release",
"output": {"outputOnFailure": true, "shortProgress": true}
},
{
"name": "debug",
"configurePreset": "debug",
"inherits": "release"
},
{
"name": "sanitize",
"configurePreset": "sanitize",
"inherits": "release"
},
{
"name": "sandebug",
"configurePreset": "sandebug",
"inherits": "release"
}
]
}

View File

@@ -22,4 +22,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
# Building from Source
See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).
See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html).

View File

@@ -1,23 +1,143 @@
# Lean 4 releases
This file contains release notes for each stable release.
Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
of each version.
During development, drafts of future release notes appear in [`releases_drafts`](https://github.com/leanprover/lean4/tree/master/script).
We intend to provide regular "minor version" releases of the Lean language at approximately monthly intervals.
There is not yet a strong guarantee of backwards compatibility between versions,
only an expectation that breaking changes will be documented in this file.
v4.9.0
This file contains work-in-progress notes for the upcoming release, as well as previous stable releases.
Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
of each version.
v4.8.0 (development in progress)
---------
Development in progress.
* **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
v4.8.0
---------
The way Lean is built on Windows has changed (see PR [#3601](https://github.com/leanprover/lean4/pull/3601)). As a result, Lake now dynamically links executables with `supportInterpreter := true` on Windows to `libleanshared.dll` and `libInit_shared.dll`. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part of `PATH`. Running the executable via `lake exe` will ensure these libraries are part of `PATH`.
Release candidate, release notes will be copied from branch `releases/v4.8.0` once completed.
In a related change, the signature of the `nativeFacets` Lake configuration options has changed from a static `Array` to a function `(shouldExport : Bool) → Array`. See its docstring or Lake's [README](src/lake/README.md) for further details on the changed option.
* Lean now generates an error if the type of a theorem is **not** a proposition.
* Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
* Functional induction principles.
Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is created that is tailored to proofs about that function.
For example from:
```
def ackermann : Nat → Nat → Nat
| 0, m => m + 1
| n+1, 0 => ackermann n 1
| n+1, m+1 => ackermann n (ackermann (n + 1) m)
```
we get
```
ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
(case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
(case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
(x x : Nat) : motive x x
```
It can be used in the `induction` tactic using the `using` syntax:
```
induction n, m using ackermann.induct
```
* The termination checker now recognizes more recursion patterns without an
explicit `termination_by`. In particular the idiom of counting up to an upper
bound, as in
```
def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
if _ : i < arr.size then
Array.sum arr (i+1) (acc + arr[i])
else
acc
```
is recognized without having to say `termination_by arr.size - i`.
* Shorter instances names. There is a new algorithm for generating names for anonymous instances.
Across Std and Mathlib, the median ratio between lengths of new names and of old names is about 72%.
With the old algorithm, the longest name was 1660 characters, and now the longest name is 202 characters.
The new algorithm's 95th percentile name length is 67 characters, versus 278 for the old algorithm.
While the new algorithm produces names that are 1.2% less unique,
it avoids cross-project collisions by adding a module-based suffix
when it does not refer to declarations from the same "project" (modules that share the same root).
PR [#3089](https://github.com/leanprover/lean4/pull/3089).
* Attribute `@[pp_using_anonymous_constructor]` to make structures pretty print like `⟨x, y, z⟩`
rather than `{a := x, b := y, c := z}`.
This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
* Now structure instances pretty print with parent structures' fields inlined.
That is, if `B` extends `A`, then `{ toA := { x := 1 }, y := 2 }` now pretty prints as `{ x := 1, y := 2 }`.
Setting option `pp.structureInstances.flatten` to false turns this off.
* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is now a suboption `pp.fieldNotation.generalized`
to enable pretty printing function applications using generalized field notation (defaults to true).
Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
* Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
When `pp.mvars` is false, expression metavariables pretty print as `?_` and universe metavariables pretty print as `_`.
When `pp.mvars.withType` is true, expression metavariables pretty print with a type ascription.
These can be set when using `#guard_msgs` to make tests not depend on the particular names of metavariables.
[#3798](https://github.com/leanprover/lean4/pull/3798) and
[#3978](https://github.com/leanprover/lean4/pull/3978).
* Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`
rather than `Nat.zero` and `Nat.succ n`.
Added option `tactic.customEliminators` to control whether to use custom eliminators.
Added a hack for `rcases`/`rintro`/`obtain` to use the custom eliminator for `Nat`.
[#3629](https://github.com/leanprover/lean4/pull/3629),
[#3655](https://github.com/leanprover/lean4/pull/3655), and
[#3747](https://github.com/leanprover/lean4/pull/3747).
* The `#guard_msgs` command now has options to change whitespace normalization and sensitivity to message ordering.
For example, `#guard_msgs (whitespace := lax) in cmd` collapses whitespace before checking messages,
and `#guard_msgs (ordering := sorted) in cmd` sorts the messages in lexicographic order before checking.
PR [#3883](https://github.com/leanprover/lean4/pull/3883).
* The `#guard_msgs` command now supports showing a diff between the expected and actual outputs. This feature is currently
disabled by default, but can be enabled with `set_option guard_msgs.diff true`. Depending on user feedback, this option
may default to `true` in a future version of Lean.
Breaking changes:
* Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:
```
def fact : Nat → Nat
| 0 => 1
| n+1 => (n+1) * fact n
theorem ex : fact 0 = 1 := by unfold fact; decide
#check fact.eq_1
-- fact.eq_1 : fact 0 = 1
#check fact.eq_2
-- fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n
#check fact.def
/-
fact.def :
∀ (x : Nat),
fact x =
match x with
| 0 => 1
| Nat.succ n => (n + 1) * fact n
-/
```
* The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`.
* The `Subarray` fields `as`, `h₁` and `h₂` have been renamed to `array`, `start_le_stop`, and `stop_le_array_size`, respectively. This more closely follows standard Lean conventions. Deprecated aliases for the field projections were added; these will be removed in a future release.
* The change to the instance name algorithm (described above) can break projects that made use of the auto-generated names.
* `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed.
v4.7.0
---------

View File

@@ -1,4 +1,4 @@
open Batteries
open Std
open Lean
inductive BoolExpr where

View File

@@ -84,12 +84,10 @@ gh workflow run update-stage0.yml
Leaving stage0 updates to the CI automation is preferable, but should you need
to do it locally, you can use `make update-stage0-commit` in `build/release` to
update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
update from another stage. This command will automatically stage the updated files
and introduce a commit,so make sure to commit your work before that.
update from another stage.
If you rebased the branch (either onto a newer version of `master`, or fixing
up some commits prior to the stage0 update, recreate the stage0 update commits.
The script `script/rebase-stage0.sh` can be used for that.
This command will automatically stage the updated files and introduce a commit,
so make sure to commit your work before that.
The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
from entering `master` through the (squashing!) merge queue, and label such PRs
@@ -97,7 +95,6 @@ with the `changes-stage0` label. Such PRs should have a cleaned up history,
with separate stage0 update commits; then coordinate with the admins to merge
your PR using rebase merge, bypassing the merge queue.
## Further Bootstrapping Complications
As written above, changes in meta code in the current stage usually will only

View File

@@ -53,59 +53,10 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
* Any other type is represented by `lean_object *`.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see respective declarations in `lean.h`) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
Example: the runtime value of `u : Unit` is always `lean_box(0)`.
#### Inductive types
For inductive types which are in the fallback `lean_object *` case above and not trivial constructors, the type is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. A `lean_ctor_object` stores the constructor index in the header, and the fields are stored in the `m_objs` portion of the object.
The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
* Non-scalar fields stored as `lean_object *`
* Fields of type `USize`
* Other scalar fields, in decreasing order by size
Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
* To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
For example, a structure such as
```lean
structure S where
ptr_1 : Array Nat
usize_1 : USize
sc64_1 : UInt64
ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
sc64_2 : Float -- `Float` is 64 bit
sc8_1 : Bool
sc16_1 : UInt16
sc8_2 : UInt8
sc64_3 : UInt64
usize_2 : USize
ptr_3 : Char -- trivial wrapper around `UInt32`
sc32_1 : UInt32
sc16_2 : UInt16
```
would get re-sorted into the following memory order:
* `S.ptr_1` - `lean_ctor_get(val, 0)`
* `S.ptr_2` - `lean_ctor_get(val, 1)`
* `S.ptr_3` - `lean_ctor_get(val, 2)`
* `S.usize_1` - `lean_ctor_get_usize(val, 3)`
* `S.usize_2` - `lean_ctor_get_usize(val, 4)`
* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)`
* `S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)`
* `S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)`
* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)`
* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)`
* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)`
* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)`
* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)`
### Borrowing
By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.

View File

@@ -50,13 +50,13 @@ We'll use `v4.6.0` as the intended release version as a running example.
- Toolchain bump PR
- Create and push the tag
- Merge the tag into `stable`
- [Batteries](https://github.com/leanprover-community/batteries)
- [Std](https://github.com/leanprover-community/std4)
- No dependencies
- Toolchain bump PR
- Create and push the tag
- Merge the tag into `stable`
- [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
- Dependencies: `Batteries`
- Dependencies: `Std`
- Note on versions and branches:
- `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
which does not refer to the toolchain being used.
@@ -65,7 +65,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
- Toolchain bump PR
- Create and push the tag, following the version convention of the repository
- [Aesop](https://github.com/leanprover-community/aesop)
- Dependencies: `Batteries`
- Dependencies: `Std`
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- Merge the tag into `stable`
@@ -79,7 +79,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
- Create and push the tag
- There is no `stable` branch; skip this step
- [Mathlib](https://github.com/leanprover-community/mathlib4)
- Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph`
- Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Std`, `doc-gen4`, `import-graph`
- Toolchain bump PR notes:
- In addition to updating the `lean-toolchain` and `lakefile.lean`,
in `.github/workflows/build.yml.in` in the `lean4checker` section update the line
@@ -123,8 +123,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
- Decide which nightly release you want to turn into a release candidate.
We will use `nightly-2024-02-29` in this example.
- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly.
- Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
- It is essential that Std and Mathlib already have reviewed branches compatible with this nightly.
- Check that both Std and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
in their `lean-toolchain`.
- The steps required to reach that state are beyond the scope of this checklist, but see below!
- Create the release branch from this nightly tag:
@@ -182,7 +182,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
- We do this for the same list of repositories as for stable releases, see above.
As above, there are dependencies between these, and so the process above is iterative.
It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
- For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
- For Std/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
`nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
(create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
- Make an announcement!
@@ -204,7 +204,7 @@ In particular, updating the downstream repositories is significantly more work
# Preparing `bump/v4.7.0` branches
While not part of the release process per se,
this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions.
this is a brief summary of the work that goes into updating Std/Aesop/Mathlib to new versions.
Please read https://leanprover-community.github.io/contribute/tags_and_branches.html

View File

@@ -1,4 +1,4 @@
#!/usr/bin/env bash
source ../../tests/common.sh
exec_check lean -Dlinter.all=false "$f"
exec_check lean -j 0 -Dlinter.all=false "$f"

100
doc/latex/lean4.py Normal file
View File

@@ -0,0 +1,100 @@
# -*- coding: utf-8 -*-
"""
pygments.lexers.theorem
~~~~~~~~~~~~~~~~~~~~~~~
Lexers for theorem-proving languages.
:copyright: Copyright 2006-2017 by the Pygments team, see AUTHORS.
:license: BSD, see LICENSE for details.
"""
import re
from pygments.lexer import RegexLexer, default, words
from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
Number, Punctuation, Generic
__all__ = ['Lean4Lexer']
class Lean4Lexer(RegexLexer):
"""
For the `Lean 4 <https://github.com/leanprover/lean4>`_
theorem prover.
.. versionadded:: 2.0
"""
name = 'Lean4'
aliases = ['lean4']
filenames = ['*.lean']
mimetypes = ['text/x-lean']
flags = re.MULTILINE | re.UNICODE
keywords1 = (
'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition',
'renaming', 'inline', 'hiding', 'parameter', 'lemma', 'variable',
'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias',
'help', 'options', 'precedence', 'postfix', 'prefix',
'infix', 'infixl', 'infixr', 'notation', '#eval',
'#check', '#reduce', '#exit', 'coercion', 'end', 'private', 'using', 'namespace',
'including', 'instance', 'section', 'context', 'protected', 'expose',
'export', 'set_option', 'extends', 'open', 'example',
'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible',
'def', 'macro', 'elab', 'syntax', 'macro_rules', 'reduce', 'where',
'abbrev', 'noncomputable', 'class', 'attribute', 'synth', 'mutual',
)
keywords2 = (
'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume',
'take', 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin',
'proof', 'qed', 'calc', 'match', 'nomatch', 'do', 'at',
)
keywords3 = (
# Sorts
'Type', 'Prop', 'Sort',
)
operators = (
u'!=', u'#', u'&', u'&&', u'*', u'+', u'-', u'/', u'@', u'!', u'`',
u'-.', u'->', u'.', u'..', u'...', u'::', u':>', u';', u';;', u'<',
u'<-', u'=', u'==', u'>', u'_', u'|', u'||', u'~', u'=>', u'<=', u'>=',
u'/\\', u'\\/', u'', u'Π', u'λ', u'', u'', u'', u'', u'', u'',
u'¬', u'⁻¹', u'', u'', u'', u'', u'', u'', u'', u'×', u'',
u'', u'', u'', u'',
)
punctuation = (u'(', u')', u':', u'{', u'}', u'[', u']', u'', u'',
u':=', u',')
tokens = {
'root': [
(r'\s+', Text),
(r'/-', Comment, 'comment'),
(r'--.*?$', Comment.Single),
(words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace),
(words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword),
(words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type),
(words(operators), Name.Builtin.Pseudo),
(words(punctuation), Operator),
(u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]"
u"[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079"
u"\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*", Name),
(r'\d+', Number.Integer),
(r'"', String.Double, 'string'),
(r'[~?][a-z][\w\']*:', Name.Variable)
],
'comment': [
# Multiline Comments
(r'[^/-]', Comment.Multiline),
(r'/-', Comment.Multiline, '#push'),
(r'-/', Comment.Multiline, '#pop'),
(r'[/-]', Comment.Multiline)
],
'string': [
(r'[^\\"]+', String.Double),
(r'\\[n"\\]', String.Escape),
('"', String.Double, '#pop'),
],
}

View File

@@ -1,7 +1,3 @@
These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](doc/dev/index.md).
We strongly suggest that new users instead follow the [Quickstart](doc/quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
Requirements
------------
@@ -21,27 +17,39 @@ Platform-Specific Setup
Generic Build Instructions
--------------------------
Setting up a basic parallelized release build:
Setting up a basic release build:
```bash
git clone https://github.com/leanprover/lean4
git clone https://github.com/leanprover/lean4 --recurse-submodules
cd lean4
cmake --preset release
make -C build/release -j$(nproc) # see below for macOS
mkdir -p build/release
cd build/release
cmake ../..
make
```
You can replace `$(nproc)`, which is not available on macOS and some alternative shells, with the desired parallelism amount.
For regular development, we recommend running
```bash
git config submodule.recurse true
```
in the checkout so that `--recurse-submodules` doesn't have to be
specified with `git pull/checkout/...`.
The above commands will compile the Lean library and binaries into the
`stage1` subfolder; see below for details.
`stage1` subfolder; see below for details. Add `-j N` for an
appropriate `N` to `make` for a parallel build.
You should not usually run `cmake --install` after a successful build.
For example, on an AMD Ryzen 9 `make` takes 00:04:55, whereas `make -j 10`
takes 00:01:38. Your results may vary depending on the speed of your hard
drive.
You should not usually run `make install` after a successful build.
See [Dev setup using elan](../dev/index.md#dev-setup-using-elan) on how to properly set up your editor to use the correct stage depending on the source directory.
Useful CMake Configuration Settings
-----------------------------------
Pass these along with the `cmake --preset release` command.
There are also two alternative presets that combine some of these options you can use instead of `release`: `debug` and `sandebug` (sanitize + debug).
Pass these along with the `cmake ../..` command.
* `-D CMAKE_BUILD_TYPE=`\
Select the build type. Valid values are `RELEASE` (default), `DEBUG`,

39
doc/make/msvc.md Normal file
View File

@@ -0,0 +1,39 @@
# Compiling Lean with Visual Studio
WARNING: Compiling Lean with Visual Studio doesn't currently work.
There's an ongoing effort to port Lean to Visual Studio.
The instructions below are for VS 2017.
In the meantime you can use [MSYS2](msys2.md) or [WSL](wsl.md).
## Installing dependencies
First, install `vcpkg` from https://github.com/Microsoft/vcpkg if you haven't
done so already.
Then, open a console in the directory you cloned `vcpkg` to, and type:
`vcpkg install mpir` for the 32-bit library or
`vcpkg install mpir:x64-windows` for the x64 one.
In Visual Studio, use the "open folder" feature and open the Lean directory.
Go to the `CMake->Change CMake Settings` menu. File `CMakeSettings.json` opens.
In each of the targets, add the following snippet (i.e., after every
`ctestCommandArgs`):
```json
"variables": [
{
"name": "CMAKE_TOOLCHAIN_FILE",
"value": "C:\\path\\to\\vcpkg\\scripts\\buildsystems\\vcpkg.cmake"
}
]
```
## Enable Intellisense
In Visual Studio, press Ctrl+Q and type `CppProperties.json` and press Enter.
Ensure `includePath` variables include `"${workspaceRoot}\\src"`.
## Build Lean
Press F7.

View File

@@ -38,9 +38,10 @@ cmake --version
Then follow the [generic build instructions](index.md) in the MSYS2
MinGW shell, using:
```
cmake --preset release -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
cmake ../.. -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
```
instead of `cmake --preset release`. This will use the clang compiler instead of gcc, which is required with msys2.
instead of `cmake ../..`. This ensures that cmake will call `sh` instead of `cmd.exe`
for script tasks and it will use the clang compiler instead of gcc, which is required.
## Install lean

View File

@@ -1,4 +1,4 @@
# Install Packages on OS X 14.5
# Install Packages on OS X 10.9
We assume that you are using [homebrew][homebrew] as a package manager.
@@ -22,7 +22,7 @@ brew install gcc
```
To install clang++-3.5 via homebrew, please execute:
```bash
brew install llvm
brew install llvm --with-clang --with-asan
```
To use compilers other than the default one (Apple's clang++), you
need to use `-DCMAKE_CXX_COMPILER` option to specify the compiler

View File

@@ -15,7 +15,7 @@ data type containing several important pieces of information. First and foremost
current player, and it has a random generator.
-/
open Batteries (HashMap)
open Std (HashMap)
abbrev TileIndex := Nat × Nat -- a 2D index
inductive TileState where

View File

@@ -6,7 +6,6 @@ Platforms built & tested by our CI, available as binary releases via elan (see b
* x86-64 Linux with glibc 2.27+
* x86-64 macOS 10.15+
* aarch64 (Apple Silicon) macOS 10.15+
* x86-64 Windows 10+
### Tier 2
@@ -17,6 +16,7 @@ Releases may be silently broken due to the lack of automated testing.
Issue reports and fixes are welcome.
* aarch64 Linux with glibc 2.27+
* aarch64 (Apple Silicon) macOS
* x86 (32-bit) Linux
* Emscripten Web Assembly

View File

@@ -43,8 +43,7 @@ $ pdflatex test.tex
## Example with `minted`
First [install Pygments](https://pygments.org/download/) (version 2.18 or newer).
Then save the following sample LaTeX file `test.tex` into the same directory:
First [install Pygments](https://pygments.org/download/). Then save [`lean4.py`](https://raw.githubusercontent.com/leanprover/lean4/master/doc/latex/lean4.py), which contains an version of the Lean highlighter updated for Lean 4, and the following sample LaTeX file `test.tex` into the same directory:
```latex
\documentclass{article}
@@ -52,8 +51,9 @@ Then save the following sample LaTeX file `test.tex` into the same directory:
% switch to a monospace font supporting more Unicode characters
\setmonofont{FreeMono}
\usepackage{minted}
\newmintinline[lean]{lean4}{bgcolor=white}
\newminted[leancode]{lean4}{fontsize=\footnotesize}
% instruct minted to use our local theorem.py
\newmintinline[lean]{lean4.py:Lean4Lexer -x}{bgcolor=white}
\newminted[leancode]{lean4.py:Lean4Lexer -x}{fontsize=\footnotesize}
\usemintedstyle{tango} % a nice, colorful theme
\begin{document}
@@ -67,6 +67,9 @@ theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f
\end{document}
```
If your version of `minted` is v2.7 or newer, but before v3.0,
you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.
You can then compile `test.tex` by executing the following command:
```bash
@@ -78,14 +81,11 @@ Some remarks:
- either `xelatex` or `lualatex` is required to handle Unicode characters in the code.
- `--shell-escape` is needed to allow `xelatex` to execute `pygmentize` in a shell.
- If the chosen monospace font is missing some Unicode symbols, you can direct them to be displayed using a fallback font or other replacement LaTeX code.
``` latex
\usepackage{newunicodechar}
\newfontfamily{\freeserif}{DejaVu Sans}
\newunicodechar{✝}{\freeserif{✝}}
\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
```
- If you are using an old version of Pygments, you can copy
[`lean.py`](https://raw.githubusercontent.com/pygments/pygments/master/pygments/lexers/lean.py) into your working directory,
and use `lean4.py:Lean4Lexer -x` instead of `lean4` above.
If your version of `minted` is v2.7 or newer, but before v3.0,
you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.
``` latex
\usepackage{newunicodechar}
\newfontfamily{\freeserif}{DejaVu Sans}
\newunicodechar{✝}{\freeserif{✝}}
\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
```
- minted has a "helpful" feature that draws red boxes around characters the chosen lexer doesn't recognize.
Since the Lean lexer cannot encompass all user-defined syntax, it is advisable to [work around](https://tex.stackexchange.com/a/343506/14563) this feature.

View File

@@ -170,7 +170,7 @@ rec {
ln -sf ${lean-all}/* .
'';
buildPhase = ''
ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_init' -j$NIX_BUILD_CORES
ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
'';
installPhase = ''
mkdir $out
@@ -180,7 +180,7 @@ rec {
update-stage0 =
let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in
writeShellScriptBin "update-stage0" ''
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/update-stage0"}
'';
update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
set -euo pipefail

View File

@@ -1,22 +0,0 @@
Draft release notes
-------------------
This folder contains drafts of release notes for inclusion in `RELEASES.md`.
During the process to create a release candidate, we look through all the commits that make up the release
to prepare the release notes, and in that process we take these drafts into account.
Guidelines:
- You should prefer adding release notes to commit messages over adding anything to this folder.
A release note should briefly explain the impact of a change from a user's point of view.
Please mark these parts out with words such as **release notes** and/or **breaking changes**.
- It is not necessary to add anything to this folder. It is meant for larger features that span multiple PRs,
or for anything that would be helpful when preparing the release notes that might be missed
by someone reading through the change log.
- If the PR that adds a feature simultaneously adds a draft release note, including the PR number is not required
since it can be obtained from the git history for the file.
When release notes are prepared, all the draft release notes are deleted from this folder.
For release candidates beyond the first one, you can either update `RELEASE.md` directly
or continue to add drafts.
When a release is finalized, we will copy the completed release notes from `RELEASE.md` to the `master` branch.

View File

@@ -1,13 +0,0 @@
* The `MessageData.ofPPFormat` constructor has been removed.
Its functionality has been split into two:
- for lazy structured messages, please use `MessageData.lazy`;
- for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
* The `MessageData.ofFormat` constructor has been turned into a function.
If you need to inspect `MessageData`,
you can pattern-match on `MessageData.ofFormatWithInfos`.
part of #3929

View File

@@ -1,12 +0,0 @@
Functions defined by well-founded recursion are now marked as
`@[irreducible]`, which should prevent expensive and often unfruitful
unfolding of such definitions.
Existing proofs that hold by definitional equality (e.g. `rfl`) can be
rewritten to explictly unfold the function definition (using `simp`,
`unfold`, `rw`), or the recursive function can be temporariliy made
semireducible (using `unseal f in` before the command) or the function
definition itself can be marked as `@[semireducible]` to get the previous
behavor.
#4061

View File

@@ -1,2 +0,0 @@
This directory contains various scripts that are *not* meant to be called
directly, but through other scripts or makefiles.

View File

@@ -1,19 +0,0 @@
#!/usr/bin/env bash
# Script internal to `./script/rebase-stage0.sh`
# Determine OS type for sed in-place editing
SED_CMD=("sed" "-i")
if [[ "$OSTYPE" == "darwin"* ]]
then
# macOS requires an empty string argument with -i for in-place editing
SED_CMD=("sed" "-i" "")
fi
if [ "$STAGE0_WITH_NIX" = true ]
then
"${SED_CMD[@]}" '/chore: update stage0/ s,.*,x nix run .#update-stage0-commit,' "$1"
else
"${SED_CMD[@]}" '/chore: update stage0/ s,.*,x make -j32 -C build/release update-stage0 \&\& git commit -m "chore: update stage0",' "$1"
fi

View File

@@ -1,24 +0,0 @@
#!/usr/bin/env bash
# This script rebases onto the given branch/commit, and updates
# all `chore: update stage0` commits along the way.
# Whether to use nix or make to update stage0
if [ "$1" = "-nix" ]
then
export STAGE0_WITH_NIX=true
shift
fi
# Check if an argument is provided
if [ "$#" -eq 0 ]; then
echo "Usage: $0 [-nix] <options to git rebase -i>"
exit 1
fi
REPO_ROOT=$(git rev-parse --show-toplevel)
# Run git rebase in interactive mode, but automatically edit the todo list
# using the defined GIT_SEQUENCE_EDITOR command
GIT_SEQUENCE_EDITOR="$REPO_ROOT/script/lib/rebase-editor.sh" git rebase -i "$@"

View File

@@ -9,7 +9,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 9)
set(LEAN_VERSION_MINOR 8)
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'")
@@ -315,12 +315,6 @@ endif()
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
# in local builds, link executables and not just dynlibs against C++ stdlib as well,
# which is required for e.g. asan
if(NOT LEAN_STANDALONE)
string(APPEND CMAKE_EXE_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
endif()
# flags for user binaries = flags for toolchain binaries + Lake
string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
@@ -591,7 +585,7 @@ endif()
if(PREV_STAGE)
add_custom_target(update-stage0
COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/lib/update-stage0'
COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0'
DEPENDS make_stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")

View File

@@ -34,4 +34,3 @@ import Init.BinderPredicates
import Init.Ext
import Init.Omega
import Init.MacroTrace
import Init.Grind

View File

@@ -63,16 +63,3 @@ theorem ite_some_none_eq_none [Decidable P] :
@[simp] theorem ite_some_none_eq_some [Decidable P] :
(if P then some x else none) = some y P x = y := by
split <;> simp_all
-- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
theorem dite_some_none_eq_none [Decidable P] {x : P α} :
(if h : P then some (x h) else none) = none ¬P := by
simp only [dite_eq_right_iff]
rfl
@[simp] theorem dite_some_none_eq_some [Decidable P] {x : P α} {y : α} :
(if h : P then some (x h) else none) = some y h : P, x h = y := by
by_cases h : P <;> simp only [h, dite_cond_eq_true, dite_cond_eq_false, Option.some.injEq,
false_iff, not_exists]
case pos => exact fun h_eq Exists.intro h h_eq, fun h_exists => h_exists.2
case neg => exact fun h_false _ h_false

View File

@@ -1114,6 +1114,9 @@ theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
cases a
exact rfl
instance {α : Type u} {p : α Prop} {a : α} (h : p a) : Inhabited {x // p x} where
default := a, h
instance {α : Type u} {p : α Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
fun a, h₁ b, h₂ =>
if h : a = b then isTrue (by subst h; exact rfl)

View File

@@ -31,7 +31,6 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
go (i : Nat) (acc : Array α) : Array α :=
if h : i < n then go (i+1) (acc.push (f i, h)) else acc
termination_by n - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
/-- The array `#[0, 1, ..., n - 1]`. -/
def range (n : Nat) : Array Nat :=
@@ -44,7 +43,7 @@ instance : EmptyCollection (Array α) := ⟨Array.empty⟩
instance : Inhabited (Array α) where
default := Array.empty
@[simp] def isEmpty (a : Array α) : Bool :=
def isEmpty (a : Array α) : Bool :=
a.size = 0
def singleton (v : α) : Array α :=
@@ -53,7 +52,7 @@ def singleton (v : α) : Array α :=
/-- Low-level version of `fget` which is as fast as a C array read.
`Fin` values are represented as tag pointers in the Lean runtime. Thus,
`fget` may be slightly slower than `uget`. -/
@[extern "lean_array_uget", simp]
@[extern "lean_array_uget"]
def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
a[i.toNat]
@@ -307,7 +306,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
else
pure r
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
map 0 (mkEmpty as.size)
@[inline]
@@ -380,7 +378,6 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
else
pure false
termination_by stop - j
decreasing_by simp_wf; decreasing_trivial_pre_omega
loop start
if h : stop as.size then
any stop h
@@ -466,7 +463,6 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
if p as[j] then some j else loop (j + 1)
else none
termination_by as.size - j
decreasing_by simp_wf; decreasing_trivial_pre_omega
loop 0
def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
@@ -561,7 +557,6 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : αα → Bool) (
else
true
termination_by a.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
@[inline] def isEqv (a b : Array α) (p : α α Bool) : Bool :=
if h : a.size = b.size then
@@ -666,7 +661,6 @@ def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)
else indexOfAux a v (i+1)
else none
termination_by a.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
indexOfAux a v 0
@@ -709,7 +703,6 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
else
as
termination_by as.size
decreasing_by simp_wf; decreasing_trivial_pre_omega
def takeWhile (p : α Bool) (as : Array α) : Array α :=
let rec go (i : Nat) (r : Array α) : Array α :=
@@ -722,7 +715,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
else
r
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
go 0 #[]
/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
@@ -733,15 +725,16 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
if h : i.val + 1 < a.size then
let a' := a.swap i.val + 1, h i
let i' : Fin a'.size := i.val + 1, by simp [a', h]
have : a'.size - i' < a.size - i := by
simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
a'.feraseIdx i'
else
a.pop
termination_by a.size - i.val
decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
induction a, i using Array.feraseIdx.induct with
| @case1 a i h a' _ ih =>
| @case1 a i h a' _ _ ih =>
unfold feraseIdx
simp [h, a', ih]
| case2 a i h =>
@@ -770,7 +763,6 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
else
as
termination_by j.1
decreasing_by simp_wf; decreasing_trivial_pre_omega
let j := as.size
let as := as.push a
loop as j, size_push .. j.lt_succ_self
@@ -824,7 +816,6 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
else
true
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
/-- Return true iff `as` is a prefix of `bs`.
That is, `bs = as ++ t` for some `t : List α`.-/
@@ -846,7 +837,6 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
else
true
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def allDiff [BEq α] (as : Array α) : Bool :=
allDiffAux as 0
@@ -862,7 +852,6 @@ def allDiff [BEq α] (as : Array α) : Bool :=
else
cs
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
@[inline] def zipWith (as : Array α) (bs : Array β) (f : α β γ) : Array γ :=
zipWithAux f as bs 0 #[]

View File

@@ -48,7 +48,6 @@ where
let b f as[i]
go (i+1) acc.val.push b, by simp [acc.property] hlt
termination_by as.size - i
decreasing_by decreasing_trivial_pre_omega
@[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α m α) : m (Array α) :=
go 0 as

View File

@@ -21,8 +21,6 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
subst heq
exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
termination_by a.size - i
decreasing_by decreasing_trivial_pre_omega
theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) a = b := by
simp [Array.isEqv]
@@ -39,7 +37,6 @@ theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux
case inl h => simp [h, isEqvAux_self a (i+1)]
case inr h => simp [h]
termination_by a.size - i
decreasing_by decreasing_trivial_pre_omega
theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
simp [isEqv, isEqvAux_self]

View File

@@ -21,13 +21,6 @@ namespace Array
attribute [simp] data_toArray uset
@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
@[simp] theorem toArray_data : (a : Array α) a.data.toArray = a
| l => ext' (data_toArray l)
@[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl
@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
@@ -138,7 +131,6 @@ where
simp [aux (i+1), map_eq_pure_bind]; rfl
· rw [List.drop_length_le (Nat.ge_of_not_lt _)]; rfl
termination_by arr.size - i
decreasing_by decreasing_trivial_pre_omega
@[simp] theorem map_data (f : α β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
rw [map, mapM_eq_foldlM]
@@ -148,8 +140,7 @@ where
simp [H]
@[simp] theorem size_map (f : α β) (arr : Array α) : (arr.map f).size = arr.size := by
simp only [ data_length]
simp
simp [size]
@[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
@@ -316,749 +307,5 @@ termination_by n - i
(ofFn f)[i] = f i, size_ofFn f h :=
getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
/-- # mkArray -/
@[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
(mkArray n v)[i] = v := by simp [Array.getElem_eq_data_get]
/-- # mem -/
theorem mem_data {a : α} {l : Array α} : a l.data a l := (mem_def _ _).symm
theorem not_mem_nil (a : α) : ¬ a #[] := nofun
/-- # get lemmas -/
theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] l := by
erw [Array.mem_def, getElem_eq_data_get]
apply List.get_mem
theorem getElem_fin_eq_data_get (a : Array α) (i : Fin _) : a[i] = a.data.get i := rfl
@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
a[i] = a[i.toNat] := rfl
theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? = a[i] :=
getElem?_pos ..
theorem get?_len_le (a : Array α) (i : Nat) (h : a.size i) : a[i]? = none := by
simp [getElem?_neg, h]
theorem getElem_mem_data (a : Array α) (h : i < a.size) : a[i] a.data := by
simp only [getElem_eq_data_get, List.get_mem]
theorem getElem?_eq_data_get? (a : Array α) (i : Nat) : a[i]? = a.data.get? i := by
by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
theorem get?_eq_data_get? (a : Array α) (i : Nat) : a.get? i = a.data.get? i :=
getElem?_eq_data_get? ..
theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
simp [get!_eq_getD]
@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
simp [back, back?]
@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
simp [back?, getElem?_eq_data_get?]
theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
(a.push x)[i]? = some a[i] := by
rw [getElem?_pos, get_push_lt]
theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
rw [getElem?_pos, get_push_eq]
theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
match Nat.lt_trichotomy i a.size with
| Or.inl g =>
have h1 : i < a.size + 1 := by omega
have h2 : i a.size := by omega
simp [getElem?, size_push, g, h1, h2, get_push_lt]
| Or.inr (Or.inl heq) =>
simp [heq, getElem?_pos, get_push_eq]
| Or.inr (Or.inr g) =>
simp only [getElem?, size_push]
have h1 : ¬ (i < a.size) := by omega
have h2 : ¬ (i < a.size + 1) := by omega
have h3 : i a.size := by omega
simp [h1, h2, h3]
@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
simp only [getElem?, Nat.lt_irrefl, dite_false]
@[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1] = v := by
simp only [set, getElem_eq_data_get, List.get_set_eq]
theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
(h : i.1 j) : (a.set i v)[j]? = a[j]? := by
by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
(a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
if h : i.1 = j then subst j; simp [*] else simp [*]
theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
(a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
if h : i.1 = j then subst j; simp [*] else simp [*]
@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
(h : i.1 j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
(setD a i v)[i] = v := by
simp at h
simp only [setD, h, dite_true, get_set, ite_true]
theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
(a.set i v).set i, by simp [i.2] v' = a.set i v' := by simp [set, List.set_set]
private theorem fin_cast_val (e : n = n') (i : Fin n) : e i = i.1, e i.2 := by cases e; rfl
theorem swap_def (a : Array α) (i j : Fin a.size) :
a.swap i j = (a.set i (a.get j)).set j.1, by simp [j.2] (a.get i) := by
simp [swap, fin_cast_val]
theorem data_swap (a : Array α) (i j : Fin a.size) :
(a.swap i j).data = (a.data.set i (a.get j)).set j (a.get i) := by simp [swap_def]
theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
simp [swap_def, get?_set, getElem_fin_eq_data_get]
@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
a.swapAt i v = (a[i.1], a.set i v) := rfl
-- @[simp] -- FIXME: gives a weird linter error
theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
a.swapAt! i v = (a[i], a.set i, h v) := by simp [swapAt!, h]
@[simp] theorem data_pop (a : Array α) : a.pop.data = a.data.dropLast := by simp [pop]
@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
@[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]
@[simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop hi) (Nat.sub_le _ _)) :=
List.get_dropLast ..
theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] := by
apply ext
· simp [h]
· intros; contradiction
theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size 0) :
as = as.pop.push as.back := by
apply ext
· simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
· intros i h h'
if hlt : i < as.pop.size then
rw [get_push_lt (h:=hlt), getElem_pop]
else
have heq : i = as.pop.size :=
Nat.le_antisymm (size_pop .. Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
cases heq; rw [get_push_eq, back, size_pop, get!_eq_getD, getD, dif_pos h]; rfl
theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size 0) :
(bs : Array α) (c : α), as = bs.push c :=
let _ : Inhabited α := as[0]
as.pop, as.back, eq_push_pop_back_of_size_ne_zero h
theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
@[simp] theorem size_swap! (a : Array α) (i j) :
(a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
rw [reverse.loop]
if h : i < j then
have := reverse.termination h
simp [(go · (i+1) j-1, ·), h]
else simp [h]
termination_by j - i
simp only [reverse]; split <;> simp [go]
@[simp] theorem size_range {n : Nat} : (range n).size = n := by
unfold range
induction n with
| zero => simp [Nat.fold]
| succ k ih =>
rw [Nat.fold, flip]
simp only [mkEmpty_eq, size_push] at *
omega
@[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
let rec go (as : Array α) (i j hj)
(h : i + j + 1 = a.size) (h₂ : as.size = a.size)
(H : k, as.data.get? k = if i k k j then a.data.get? k else a.data.reverse.get? k)
(k) : (reverse.loop as i j, hj).data.get? k = a.data.reverse.get? k := by
rw [reverse.loop]; dsimp; split <;> rename_i h₁
· have := reverse.termination h₁
match j with | j+1 => ?_
simp at *
rw [(go · (i+1) j)]
· rwa [Nat.add_right_comm i]
· simp [size_swap, h₂]
· intro k
rw [ getElem?_eq_data_get?, get?_swap]
simp [getElem?_eq_data_get?, getElem_eq_data_get, List.get?_eq_get, H, Nat.le_of_lt h₁]
split <;> rename_i h₂
· simp [ h₂, Nat.not_le.2 (Nat.lt_succ_self _)]
exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
split <;> rename_i h₃
· simp [ h₃, Nat.not_le.2 (Nat.lt_succ_self _)]
exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
· rw [H]; split <;> rename_i h₂
· cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
cases Nat.le_antisymm h₂.1 h₂.2
exact (List.get?_reverse' _ _ h).symm
· rfl
termination_by j - i
simp only [reverse]; split
· match a with | [] | [_] => rfl
· have := Nat.sub_add_cancel (Nat.le_of_not_le _)
refine List.ext <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
split; {rfl}; rename_i h
simp [ show k < _ + 1 _ from Nat.lt_succ (n := a.size - 1), this] at h
rw [List.get?_eq_none.2 _, List.get?_eq_none.2 (a.data.length_reverse _)]
/-! ### foldl / foldr -/
-- This proof is the pure version of `Array.SatisfiesM_foldlM`,
-- reproduced to avoid a dependency on `SatisfiesM`.
theorem foldl_induction
{as : Array α} (motive : Nat β Prop) {init : β} (h0 : motive 0 init) {f : β α β}
(hf : i : Fin as.size, b, motive i.1 b motive (i.1 + 1) (f b as[i])) :
motive as.size (as.foldl f init) := by
let rec go {i j b} (h₁ : j as.size) (h₂ : as.size i + j) (H : motive j b) :
(motive as.size) (foldlM.loop (m := Id) f as as.size (Nat.le_refl _) i j b) := by
unfold foldlM.loop; split
· next hj =>
split
· cases Nat.not_le_of_gt (by simp [hj]) h₂
· exact go hj (by rwa [Nat.succ_add] at h₂) (hf j, hj b H)
· next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) H
simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0
-- This proof is the pure version of `Array.SatisfiesM_foldrM`,
-- reproduced to avoid a dependency on `SatisfiesM`.
theorem foldr_induction
{as : Array α} (motive : Nat β Prop) {init : β} (h0 : motive as.size init) {f : α β β}
(hf : i : Fin as.size, b, motive (i.1 + 1) b motive i.1 (f as[i] b)) :
motive 0 (as.foldr f init) := by
let rec go {i b} (hi : i as.size) (H : motive i b) :
(motive 0) (foldrM.fold (m := Id) f as 0 i hi b) := by
unfold foldrM.fold; simp; split
· next hi => exact (hi H)
· next hi =>
split; {simp at hi}
· next i hi' =>
exact go _ (hf i, hi' b H)
simp [foldr, foldrM]; split; {exact go _ h0}
· next h => exact (Nat.eq_zero_of_not_pos h h0)
/-! ### map -/
@[simp] theorem mem_map {f : α β} {l : Array α} : b l.map f a, a l f a = b := by
simp only [mem_def, map_data, List.mem_map]
theorem mapM_eq_mapM_data [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
arr.mapM f = return mk ( arr.data.mapM f) := by
rw [mapM_eq_foldlM, foldlM_eq_foldlM_data, List.foldrM_reverse]
conv => rhs; rw [ List.reverse_reverse arr.data]
induction arr.data.reverse with
| nil => simp; rfl
| cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
theorem mapM_map_eq_foldl (as : Array α) (f : α β) (i) :
mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
unfold mapM.map
split <;> rename_i h
· simp only [Id.bind_eq]
dsimp [foldl, Id.run, foldlM]
rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
-- Calling `split` here gives a bad goal.
have : size as - i = Nat.succ (size as - i - 1) := by omega
rw [this]
simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
· dsimp [foldl, Id.run, foldlM]
rw [dif_pos (by omega), foldlM.loop, dif_neg h]
rfl
termination_by as.size - i
theorem map_eq_foldl (as : Array α) (f : α β) :
as.map f = as.foldl (fun r a => r.push (f a)) #[] :=
mapM_map_eq_foldl _ _ _
theorem map_induction (as : Array α) (f : α β) (motive : Nat Prop) (h0 : motive 0)
(p : Fin as.size β Prop) (hs : i, motive i.1 p i (f as[i]) motive (i+1)) :
motive as.size
eq : (as.map f).size = as.size, i h, p i, h ((as.map f)[i]) := by
have t := foldl_induction (as := as) (β := Array β)
(motive := fun i arr => motive i arr.size = i i h2, p i arr[i.1])
(init := #[]) (f := fun r a => r.push (f a)) ?_ ?_
obtain m, eq, w := t
· refine m, by simpa [map_eq_foldl] using eq, ?_
intro i h
simp [eq] at w
specialize w i, h h
simpa [map_eq_foldl] using w
· exact h0, rfl, nofun
· intro i b m, eq, w
refine ?_, ?_, ?_
· exact (hs _ m).2
· simp_all
· intro j h
simp at h
by_cases h' : j < size b
· rw [get_push]
simp_all
· rw [get_push, dif_neg h']
simp only [show j = i by omega]
exact (hs _ m).1
theorem map_spec (as : Array α) (f : α β) (p : Fin as.size β Prop)
(hs : i, p i (f as[i])) :
eq : (as.map f).size = as.size, i h, p i, h ((as.map f)[i]) := by
simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
@[simp] theorem getElem_map (f : α β) (as : Array α) (i : Nat) (h) :
((as.map f)[i]) = f (as[i]'(size_map .. h)) := by
have := map_spec as f (fun i b => b = f (as[i]))
simp only [implies_true, true_implies] at this
obtain eq, w := this
apply w
simp_all
/-! ### mapIdx -/
-- This could also be prove from `SatisfiesM_mapIdxM`.
theorem mapIdx_induction (as : Array α) (f : Fin as.size α β)
(motive : Nat Prop) (h0 : motive 0)
(p : Fin as.size β Prop)
(hs : i, motive i.1 p i (f i as[i]) motive (i + 1)) :
motive as.size eq : (Array.mapIdx as f).size = as.size,
i h, p i, h ((Array.mapIdx as f)[i]) := by
let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : i h h', p i, h bs[i]) (hm : motive j) :
let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
motive as.size eq : arr.size = as.size, i h, p i, h arr[i] := by
induction i generalizing j bs with simp [mapIdxM.map]
| zero =>
have := (Nat.zero_add _).symm.trans h
exact this hm, h₁ this, fun _ _ => h₂ ..
| succ i ih =>
apply @ih (bs.push (f j, by omega as[j])) (j + 1) (by omega) (by simp; omega)
· intro i i_lt h'
rw [get_push]
split
· apply h₂
· simp only [size_push] at h'
obtain rfl : i = j := by omega
apply (hs i, by omega hm).1
· exact (hs j, by omega hm).2
simp [mapIdx, mapIdxM]; exact go rfl nofun h0
theorem mapIdx_spec (as : Array α) (f : Fin as.size α β)
(p : Fin as.size β Prop) (hs : i, p i (f i as[i])) :
eq : (Array.mapIdx as f).size = as.size,
i h, p i, h ((Array.mapIdx as f)[i]) :=
(mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => hs .., trivial).2
@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size α β) : (a.mapIdx f).size = a.size :=
(mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
Array.size_mapIdx _ _
@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size α β) (i : Nat)
(h : i < (mapIdx a f).size) :
haveI : i < a.size := by simp_all
(a.mapIdx f)[i] = f i, this a[i] :=
(mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
/-! ### modify -/
@[simp] theorem size_modify (a : Array α) (i : Nat) (f : α α) : (a.modify i f).size = a.size := by
unfold modify modifyM Id.run
split <;> simp
theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
(arr.modify x f).get i, by simp [h] =
if x = i then f (arr.get i, h) else arr.get i, h := by
simp [modify, modifyM, Id.run]; split
· simp [get_set _ _ _ h]; split <;> simp [*]
· rw [if_neg (mt (by rintro rfl; exact h) _)]
/-! ### filter -/
@[simp] theorem filter_data (p : α Bool) (l : Array α) :
(l.filter p).data = l.data.filter p := by
dsimp only [filter]
rw [foldl_eq_foldl_data]
generalize l.data = l
suffices a, (List.foldl (fun r a => if p a = true then push r a else r) a l).data =
a.data ++ List.filter p l by
simpa using this #[]
induction l with simp
| cons => split <;> simp [*]
@[simp] theorem filter_filter (q) (l : Array α) :
filter p (filter q l) = filter (fun a => p a q a) l := by
apply ext'
simp only [filter_data, List.filter_filter]
@[simp] theorem mem_filter : x filter p as x as p x := by
simp only [mem_def, filter_data, List.mem_filter]
theorem mem_of_mem_filter {a : α} {l} (h : a filter p l) : a l :=
(mem_filter.mp h).1
/-! ### filterMap -/
@[simp] theorem filterMap_data (f : α Option β) (l : Array α) :
(l.filterMap f).data = l.data.filterMap f := by
dsimp only [filterMap, filterMapM]
rw [foldlM_eq_foldlM_data]
generalize l.data = l
have this : a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).data =
a.data ++ List.filterMap f l := ?_
exact this #[]
induction l
· simp_all [Id.run]
· simp_all [Id.run]
split <;> simp_all
@[simp] theorem mem_filterMap (f : α Option β) (l : Array α) {b : β} :
b filterMap f l a, a l f a = some b := by
simp only [mem_def, filterMap_data, List.mem_filterMap]
/-! ### empty -/
theorem size_empty : (#[] : Array α).size = 0 := rfl
theorem empty_data : (#[] : Array α).data = [] := rfl
/-! ### append -/
theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
@[simp] theorem mem_append {a : α} {s t : Array α} : a s ++ t a s a t := by
simp only [mem_def, append_data, List.mem_append]
theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
simp only [size, append_data, List.length_append]
theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
(as ++ bs)[i] = as[i] := by
simp only [getElem_eq_data_get]
have h' : i < (as.data ++ bs.data).length := by rwa [ data_length, append_data] at h
conv => rhs; rw [ List.get_append_left (bs:=bs.data) (h':=h')]
apply List.get_of_eq; rw [append_data]
theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size i)
(hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. h)) :
(as ++ bs)[i] = bs[i - as.size] := by
simp only [getElem_eq_data_get]
have h' : i < (as.data ++ bs.data).length := by rwa [ data_length, append_data] at h
conv => rhs; rw [ List.get_append_right (h':=h') (h:=Nat.not_lt_of_ge hle)]
apply List.get_of_eq; rw [append_data]
@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
apply ext'; simp only [append_data, empty_data, List.append_nil]
@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
apply ext'; simp only [append_data, empty_data, List.nil_append]
theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
apply ext'; simp only [append_data, List.append_assoc]
/-! ### extract -/
theorem extract_loop_zero (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs := by
rw [extract.loop]; split <;> rfl
theorem extract_loop_succ (as bs : Array α) (size start : Nat) (h : start < as.size) :
extract.loop as (size+1) start bs = extract.loop as size (start+1) (bs.push as[start]) := by
rw [extract.loop, dif_pos h]; rfl
theorem extract_loop_of_ge (as bs : Array α) (size start : Nat) (h : start as.size) :
extract.loop as size start bs = bs := by
rw [extract.loop, dif_neg (Nat.not_lt_of_ge h)]
theorem extract_loop_eq_aux (as bs : Array α) (size start : Nat) :
extract.loop as size start bs = bs ++ extract.loop as size start #[] := by
induction size using Nat.recAux generalizing start bs with
| zero => rw [extract_loop_zero, extract_loop_zero, append_nil]
| succ size ih =>
if h : start < as.size then
rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton]
rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, nil_append]
rw [append_assoc]
else
rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
rw [append_nil]
theorem extract_loop_eq (as bs : Array α) (size start : Nat) (h : start + size as.size) :
extract.loop as size start bs = bs ++ as.extract start (start + size) := by
simp [extract]; rw [extract_loop_eq_aux, Nat.min_eq_left h, Nat.add_sub_cancel_left]
theorem size_extract_loop (as bs : Array α) (size start : Nat) :
(extract.loop as size start bs).size = bs.size + min size (as.size - start) := by
induction size using Nat.recAux generalizing start bs with
| zero => rw [extract_loop_zero, Nat.zero_min, Nat.add_zero]
| succ size ih =>
if h : start < as.size then
rw [extract_loop_succ (h:=h), ih, size_push, Nat.add_assoc, Nat.add_min_add_left,
Nat.sub_succ, Nat.one_add, Nat.one_add, Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)]
else
have h := Nat.le_of_not_gt h
rw [extract_loop_of_ge (h:=h), Nat.sub_eq_zero_of_le h, Nat.min_zero, Nat.add_zero]
@[simp] theorem size_extract (as : Array α) (start stop : Nat) :
(as.extract start stop).size = min stop as.size - start := by
simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
Nat.min_assoc, Nat.min_self]
theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
i < (extract.loop as size start bs).size := by
rw [size_extract_loop]
apply Nat.lt_of_lt_of_le hlt
exact Nat.le_add_right ..
theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
(h := get_extract_loop_lt_aux as bs size start hlt) :
(extract.loop as size start bs)[i] = bs[i] := by
apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
· rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
· congr; rw [extract_loop_eq_aux]
theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i bs.size)
(h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
have h : i < bs.size + (as.size - start) := by
apply Nat.lt_of_lt_of_le h
rw [size_extract_loop]
apply Nat.add_le_add_left
exact Nat.min_le_right ..
rw [Nat.add_sub_assoc hge]
apply Nat.add_lt_of_lt_sub'
exact Nat.sub_lt_left_of_lt_add hge h
theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i bs.size)
(h : i < (extract.loop as size start bs).size)
(h' := get_extract_loop_ge_aux as bs size start hge h) :
(extract.loop as size start bs)[i] = as[start + i - bs.size] := by
induction size using Nat.recAux generalizing start bs with
| zero =>
rw [size_extract_loop, Nat.zero_min, Nat.add_zero] at h
omega
| succ size ih =>
have : start < as.size := by
apply Nat.lt_of_le_of_lt (Nat.le_add_right start (i - bs.size))
rwa [ Nat.add_sub_assoc hge]
have : i < (extract.loop as size (start+1) (bs.push as[start])).size := by
rwa [ extract_loop_succ]
have heq : (extract.loop as (size+1) start bs)[i] =
(extract.loop as size (start+1) (bs.push as[start]))[i] := by
congr 1; rw [extract_loop_succ]
rw [heq]
if hi : bs.size = i then
cases hi
have h₁ : bs.size < (bs.push as[start]).size := by rw [size_push]; exact Nat.lt_succ_self ..
have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
rw [h]; congr; rw [Nat.add_sub_cancel]
else
have hge : bs.size + 1 i := Nat.lt_of_le_of_ne hge hi
rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm hge)]
congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]
theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
start + i < as.size := by
rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
apply Nat.sub_le_sub_right; apply Nat.min_le_right
@[simp] theorem get_extract {as : Array α} {start stop : Nat}
(h : i < (as.extract start stop).size) :
(as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
show (extract.loop as (min stop as.size - start) start #[])[i]
= as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _
@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
apply ext
· rw [size_extract, Nat.min_self, Nat.sub_zero]
· intros; rw [get_extract]; congr; rw [Nat.zero_add]
theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop start) :
as.extract start stop = #[] := by
simp [extract]; rw [Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.zero_min,
extract_loop_zero]
theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : as.size start) :
as.extract start stop = #[] := by
simp [extract]; rw [Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.min_zero,
extract_loop_zero]
@[simp] theorem extract_empty (start stop : Nat) : (#[] : Array α).extract start stop = #[] :=
extract_empty_of_size_le_start _ (Nat.zero_le _)
/-! ### any -/
-- Auxiliary for `any_iff_exists`.
theorem anyM_loop_iff_exists (p : α Bool) (as : Array α) (start stop) (h : stop as.size) :
anyM.loop (m := Id) p as stop h start = true
i : Fin as.size, start i i < stop p as[i] = true := by
unfold anyM.loop
split <;> rename_i h₁
· dsimp
split <;> rename_i h₂
· simp only [true_iff]
refine start, by omega, by dsimp; omega, by dsimp; omega, h₂
· rw [anyM_loop_iff_exists]
constructor
· rintro i, ge, lt, h
have : start i := by rintro rfl; omega
exact i, by omega, lt, h
· rintro i, ge, lt, h
have : start i := by rintro rfl; erw [h] at h₂; simp_all
exact i, by omega, lt, h
· simp
omega
termination_by stop - start
-- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
theorem any_iff_exists (p : α Bool) (as : Array α) (start stop) :
any as p start stop i : Fin as.size, start i.1 i.1 < stop p as[i] := by
dsimp [any, anyM, Id.run]
split
· rw [anyM_loop_iff_exists]; rfl
· rw [anyM_loop_iff_exists]
constructor
· rintro i, ge, _, h
exact i, by omega, by omega, h
· rintro i, ge, _, h
exact i, by omega, by omega, h
theorem any_eq_true (p : α Bool) (as : Array α) :
any as p i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
theorem any_def {p : α Bool} (as : Array α) : as.any p = as.data.any p := by
rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
exact fun i, h => _, i, rfl, h, fun _, i, rfl, h => i, h
/-! ### all -/
theorem all_eq_not_any_not (p : α Bool) (as : Array α) (start stop) :
all as p start stop = !(any as (!p ·) start stop) := by
dsimp [all, allM]
rfl
theorem all_iff_forall (p : α Bool) (as : Array α) (start stop) :
all as p start stop i : Fin as.size, start i.1 i.1 < stop p as[i] := by
rw [all_eq_not_any_not]
suffices ¬(any as (!p ·) start stop = true)
i : Fin as.size, start i.1 i.1 < stop p as[i] by
simp_all
rw [any_iff_exists]
simp
theorem all_eq_true (p : α Bool) (as : Array α) : all as p i : Fin as.size, p as[i] := by
simp [all_iff_forall, Fin.isLt]
theorem all_def {p : α Bool} (as : Array α) : as.all p = as.data.all p := by
rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_get]
constructor
· rintro w x r, rfl
rw [ getElem_eq_data_get]
apply w
· intro w i
exact w as[i] i, (getElem_eq_data_get as i.2).symm
theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p x, x l p x := by
simp only [all_def, List.all_eq_true, mem_def]
/-! ### contains -/
theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a a as := by
rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a as) :=
decidable_of_iff _ contains_def
/-! ### swap -/
open Fin
@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
if he : ((Array.size_set _ _ _).symm j).val = i.val then by
simp only [he, fin_cast_val, get_swap_right, getElem_fin]
else by
apply Eq.trans
· apply Array.get_set_ne
· simp only [size_set, Fin.isLt]
· assumption
· simp [get_set_ne]
@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
(hi : p i) (hj : p j) : (a.swap i j)[p]'(a.size_swap .. |>.symm hp) = a[p] := by
apply Eq.trans
· have : ((a.size_set i (a.get j)).symm j).val = j.val := by simp only [fin_cast_val]
apply Array.get_set_ne
· simp only [this]
apply Ne.symm
· assumption
· apply Array.get_set_ne
· apply Ne.symm
· assumption
theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
(a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
split
· simp_all only [get_swap_left]
· split <;> simp_all
theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
(a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
apply get_swap
@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
(a.swap i j).swap i.1, (a.size_swap ..).symm i.2 j.1, (a.size_swap ..).symm j.2 = a := by
apply ext
· simp only [size_swap]
· intros
simp only [get_swap']
split
· simp_all
· split <;> simp_all
theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i := by
apply ext
· simp only [size_swap]
· intros
simp only [get_swap']
split
· split <;> simp_all
· split <;> simp_all
end Array

View File

@@ -27,20 +27,13 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
cases as with | _ as =>
exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
@[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
/-- This tactic, added to the `decreasing_trivial` toolbox, proves that
`sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions
over a nested inductive like `inductive T | mk : Array T → T`. -/
macro "array_get_dec" : tactic =>
`(tactic| first
-- subsumed by simp
-- | with_reducible apply sizeOf_get
-- | with_reducible apply sizeOf_getElem
| (with_reducible apply Nat.lt_trans (sizeOf_get ..)); simp_arith
| (with_reducible apply Nat.lt_trans (sizeOf_getElem ..)); simp_arith
)
| apply sizeOf_get
| apply Nat.lt_trans (sizeOf_get ..); simp_arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
@@ -50,10 +43,9 @@ provided that `a ∈ arr` which is useful for well founded recursions over a nes
-- NB: This is analogue to tactic `sizeOf_list_dec`
macro "array_mem_dec" : tactic =>
`(tactic| first
| with_reducible apply Array.sizeOf_lt_of_mem; assumption; done
| with_reducible
apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
case' h => assumption
| apply Array.sizeOf_lt_of_mem; assumption; done
| apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
case' h => assumption
simp_arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

View File

@@ -27,7 +27,6 @@ def qpartition (as : Array α) (lt : αα → Bool) (lo hi : Nat) : Nat ×
let as := as.swap! i hi
(i, as)
termination_by hi - j
decreasing_by all_goals simp_wf; decreasing_trivial_pre_omega
loop as lo lo
@[inline] partial def qsort (as : Array α) (lt : α α Bool) (low := 0) (high := as.size - 1) : Array α :=

View File

@@ -15,14 +15,14 @@ structure Subarray (α : Type u) where
start_le_stop : start stop
stop_le_array_size : stop array.size
@[deprecated Subarray.array (since := "2024-04-13")]
@[deprecated Subarray.array]
abbrev Subarray.as (s : Subarray α) : Array α := s.array
@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
@[deprecated Subarray.start_le_stop]
theorem Subarray.h₁ (s : Subarray α) : s.start s.stop := s.start_le_stop
@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
theorem Subarray.h₂ (s : Subarray α) : s.stop s.array.size := s.stop_le_array_size
@[deprecated Subarray.stop_le_array_size]
theorem Subarray.h₂ (s : Subarray α) : s.stop s.as.size := s.stop_le_array_size
namespace Subarray

View File

@@ -34,8 +34,7 @@ structure BitVec (w : Nat) where
O(1), because we use `Fin` as the internal representation of a bitvector. -/
toFin : Fin (2^w)
@[deprecated (since := "2024-04-12")]
protected abbrev Std.BitVec := _root_.BitVec
@[deprecated] protected abbrev Std.BitVec := _root_.BitVec
-- We manually derive the `DecidableEq` instances for `BitVec` because
-- we want to have builtin support for bit-vector literals, and we
@@ -74,7 +73,7 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
/-- Return the bound in terms of toNat. -/
theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
@[deprecated isLt (since := "2024-03-12")]
@[deprecated isLt]
theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
/-- Theorem for normalizing the bit vector literal representation. -/
@@ -534,11 +533,6 @@ def sshiftRight (a : BitVec n) (s : Nat) : BitVec n := .ofInt n (a.toInt >>> s)
instance {n} : HShiftLeft (BitVec m) (BitVec n) (BitVec m) := fun x y => x <<< y.toNat
instance {n} : HShiftRight (BitVec m) (BitVec n) (BitVec m) := fun x y => x >>> y.toNat
/-- Auxiliary function for `rotateLeft`, which does not take into account the case where
the rotation amount is greater than the bitvector width. -/
def rotateLeftAux (x : BitVec w) (n : Nat) : BitVec w :=
x <<< n ||| x >>> (w - n)
/--
Rotate left for bit vectors. All the bits of `x` are shifted to higher positions, with the top `n`
bits wrapping around to fill the low bits.
@@ -548,15 +542,7 @@ rotateLeft 0b0011#4 3 = 0b1001
```
SMT-Lib name: `rotate_left` except this operator uses a `Nat` shift amount.
-/
def rotateLeft (x : BitVec w) (n : Nat) : BitVec w := rotateLeftAux x (n % w)
/--
Auxiliary function for `rotateRight`, which does not take into account the case where
the rotation amount is greater than the bitvector width.
-/
def rotateRightAux (x : BitVec w) (n : Nat) : BitVec w :=
x >>> n ||| x <<< (w - n)
def rotateLeft (x : BitVec w) (n : Nat) : BitVec w := x <<< n ||| x >>> (w - n)
/--
Rotate right for bit vectors. All the bits of `x` are shifted to lower positions, with the
@@ -567,7 +553,7 @@ rotateRight 0b01001#5 1 = 0b10100
```
SMT-Lib name: `rotate_right` except this operator uses a `Nat` shift amount.
-/
def rotateRight (x : BitVec w) (n : Nat) : BitVec w := rotateRightAux x (n % w)
def rotateRight (x : BitVec w) (n : Nat) : BitVec w := x >>> n ||| x <<< (w - n)
/--
Concatenation of bitvectors. This uses the "big endian" convention that the more significant

View File

@@ -159,80 +159,4 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
rw [ add_not_self x, BitVec.add_comm, add_sub_cancel]
/-! ### Negation -/
theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
getLsb (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) i.val = !(getLsb x i.val) := by
apply iunfoldr_getLsb (fun _ => ()) i (by simp)
theorem bit_not_add_self (x : BitVec w) :
((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd + x = -1 := by
simp only [add_eq_adc]
apply iunfoldr_replace_snd (fun _ => false) (-1) false rfl
intro i; simp only [ BitVec.not, adcb, testBit_toNat]
rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd)]
<;> simp [bit_not_testBit, negOne_eq_allOnes, getLsb_allOnes]
theorem bit_not_eq_not (x : BitVec w) :
((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd = ~~~ x := by
simp [allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), negOne_eq_allOnes]
theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
simp only [ add_eq_adc]
rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) _ rfl]
· rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]
simp [ sub_toAdd, BitVec.sub_add_cancel]
· simp [bit_not_testBit x _]
/-! ### Inequalities (le / lt) -/
theorem ult_eq_not_carry (x y : BitVec w) : x.ult y = !carry w x (~~~y) true := by
simp only [BitVec.ult, carry, toNat_mod_cancel, toNat_not, toNat_true, ge_iff_le, decide_not,
Nat.not_le, decide_eq_decide]
rw [Nat.mod_eq_of_lt (by omega)]
omega
theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by
simp [BitVec.ule, BitVec.ult, decide_not]
theorem ule_eq_carry (x y : BitVec w) : x.ule y = carry w y (~~~x) true := by
simp [ule_eq_not_ult, ult_eq_not_carry]
/-- If two bitvectors have the same `msb`, then signed and unsigned comparisons coincide -/
theorem slt_eq_ult_of_msb_eq {x y : BitVec w} (h : x.msb = y.msb) :
x.slt y = x.ult y := by
simp only [BitVec.slt, toInt_eq_msb_cond, BitVec.ult, decide_eq_decide, h]
cases y.msb <;> simp
/-- If two bitvectors have different `msb`s, then unsigned comparison is determined by this bit -/
theorem ult_eq_msb_of_msb_neq {x y : BitVec w} (h : x.msb y.msb) :
x.ult y = y.msb := by
simp only [BitVec.ult, msb_eq_decide, ne_eq, decide_eq_decide] at *
omega
/-- If two bitvectors have different `msb`s, then signed and unsigned comparisons are opposites -/
theorem slt_eq_not_ult_of_msb_neq {x y : BitVec w} (h : x.msb y.msb) :
x.slt y = !x.ult y := by
simp only [BitVec.slt, toInt_eq_msb_cond, Bool.eq_not_of_ne h, ult_eq_msb_of_msb_neq h]
cases y.msb <;> (simp; omega)
theorem slt_eq_ult (x y : BitVec w) :
x.slt y = (x.msb != y.msb).xor (x.ult y) := by
by_cases h : x.msb = y.msb
· simp [h, slt_eq_ult_of_msb_eq]
· have h' : x.msb != y.msb := by simp_all
simp [slt_eq_not_ult_of_msb_neq h, h']
theorem slt_eq_not_carry (x y : BitVec w) :
x.slt y = (x.msb == y.msb).xor (carry w x (~~~y) true) := by
simp only [slt_eq_ult, bne, ult_eq_not_carry]
cases x.msb == y.msb <;> simp
theorem sle_eq_not_slt (x y : BitVec w) : x.sle y = !y.slt x := by
simp only [BitVec.sle, BitVec.slt, decide_not, decide_eq_decide]; omega
theorem sle_eq_carry (x y : BitVec w) :
x.sle y = !((x.msb == y.msb).xor (carry w y (~~~x) true)) := by
rw [sle_eq_not_slt, slt_eq_not_carry, beq_comm]
end BitVec

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joe Hendrix, Harun Khan
Authors: Joe Hendrix
-/
prelude
import Init.Data.BitVec.Lemmas
@@ -48,51 +48,6 @@ private theorem iunfoldr.eq_test
intro i
simp_all [truncate_succ]
theorem iunfoldr_getLsb' {f : Fin w α α × Bool} (state : Nat α)
(ind : (i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
( i : Fin w, getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
(iunfoldr f (state 0)).fst = state w := by
unfold iunfoldr
simp
apply Fin.hIterate_elim
(fun j (p : α × BitVec j) => (hj : j w)
( i : Fin j, getLsb p.snd i.val = (f i.val, Nat.lt_of_lt_of_le i.isLt hj (state i.val)).snd)
p.fst = state j)
case hj => simp
case init =>
intro
apply And.intro
· intro i
have := Fin.size_pos i
contradiction
· rfl
case step =>
intro j s, v ih hj
apply And.intro
case left =>
intro i
simp only [getLsb_cons]
have hj2 : j.val w := by simp
cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
| inl h3 => simp [if_neg, (Nat.ne_of_lt h3)]
exact (ih hj2).1 i.val, h3
| inr h3 => simp [h3, if_pos]
cases (Nat.eq_zero_or_pos j.val) with
| inl hj3 => congr
rw [ (ih hj2).2]
| inr hj3 => congr
exact (ih hj2).2
case right =>
simp
have hj2 : j.val w := by simp
rw [ ind j, (ih hj2).2]
theorem iunfoldr_getLsb {f : Fin w α α × Bool} (state : Nat α) (i : Fin w)
(ind : (i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd := by
exact (iunfoldr_getLsb' state ind).1 i
/--
Correctness theorem for `iunfoldr`.
-/
@@ -103,11 +58,4 @@ theorem iunfoldr_replace
iunfoldr f a = (state w, value) := by
simp [iunfoldr.eq_test state value a init step]
theorem iunfoldr_replace_snd
{f : Fin w α α × Bool} (state : Nat α) (value : BitVec w) (a : α)
(init : state 0 = a)
(step : (i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
(iunfoldr f a).snd = value := by
simp [iunfoldr.eq_test state value a init step]
end BitVec

View File

@@ -2,15 +2,12 @@
Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed,
-/
prelude
import Init.Data.Bool
import Init.Data.BitVec.Basic
import Init.Data.Fin.Lemmas
import Init.Data.Nat.Lemmas
import Init.Data.Nat.Mod
import Init.Data.Int.Bitwise.Lemmas
namespace BitVec
@@ -106,13 +103,7 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
have q := pred w - 1 - i, q_lt
simpa [q_lt, Nat.sub_sub_self, r] using q
-- This cannot be a `@[simp]` lemma, as it would be tried at every term.
theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
@[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
@[simp] theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp [of_length_zero]
@[simp] theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp [of_length_zero]
@[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
@[simp] theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
theorem eq_of_toFin_eq : {x y : BitVec w}, x.toFin = y.toFin x = y
| _, _, _, _, rfl => rfl
@@ -142,16 +133,13 @@ theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b'
@[simp, bv_toNat] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by
simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
@[simp] theorem toFin_ofNat (x : Nat) : toFin x#w = Fin.ofNat' x (Nat.two_pow_pos w) := rfl
-- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
-- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
getLsb (x#n) i = (i < n && x.testBit i) := by
simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
@[simp, deprecated toNat_ofNat (since := "2024-02-22")]
theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
@[simp, deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
@[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]
@@ -178,7 +166,8 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
x.getLsb (w-1) = decide (2 ^ (w-1) x.toNat) := by
rcases w with rfl | w
· simp
· simp only [getLsb, Nat.testBit_to_div_mod, Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
· simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
· simp [Nat.div_eq_of_lt h, h]
· simp only [h]
@@ -225,21 +214,9 @@ theorem toInt_eq_toNat_cond (i : BitVec n) :
if 2*i.toNat < 2^n then
(i.toNat : Int)
else
(i.toNat : Int) - (2^n : Nat) :=
rfl
theorem msb_eq_false_iff_two_mul_lt (x : BitVec w) : x.msb = false 2 * x.toNat < 2^w := by
cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide]
theorem msb_eq_true_iff_two_mul_ge (x : BitVec w) : x.msb = true 2 * x.toNat 2^w := by
simp [ Bool.ne_false_iff, msb_eq_false_iff_two_mul_lt]
/-- Characterize `x.toInt` in terms of `x.msb`. -/
theorem toInt_eq_msb_cond (x : BitVec w) :
x.toInt = if x.msb then (x.toNat : Int) - (2^w : Nat) else (x.toNat : Int) := by
simp only [BitVec.toInt, msb_eq_false_iff_two_mul_lt]
cases x.msb <;> rfl
(i.toNat : Int) - (2^n : Nat) := by
unfold BitVec.toInt
split <;> omega
theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
simp only [toInt_eq_toNat_cond]
@@ -261,12 +238,6 @@ theorem eq_of_toInt_eq {i j : BitVec n} : i.toInt = j.toInt → i = j := by
have _jlt := j.isLt
split <;> split <;> omega
theorem toInt_inj (x y : BitVec n) : x.toInt = y.toInt x = y :=
Iff.intro eq_of_toInt_eq (congrArg BitVec.toInt)
theorem toInt_ne (x y : BitVec n) : x.toInt y.toInt x y := by
rw [Ne, toInt_inj]
@[simp] theorem toNat_ofInt {n : Nat} (i : Int) :
(BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by
unfold BitVec.ofInt
@@ -282,9 +253,6 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
have p : 0 i % (2^n : Nat) := by omega
simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]
@[simp] theorem ofInt_natCast (w n : Nat) :
BitVec.ofInt w (n : Int) = BitVec.ofNat w n := rfl
/-! ### zeroExtend and truncate -/
@[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m n) (x : BitVec m) :
@@ -368,7 +336,7 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
@[simp] theorem getMsb_zeroExtend_add {x : BitVec w} (h : k i) :
(x.zeroExtend (w + k)).getMsb i = x.getMsb (i - k) := by
by_cases h : w = 0
· subst h; simp [of_length_zero]
· subst h; simp
simp only [getMsb, getLsb_zeroExtend]
by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
<;> simp [h₁, h₂, h₃]
@@ -467,11 +435,6 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
ext
simp
theorem or_assoc (x y z : BitVec w) :
x ||| y ||| z = x ||| (y ||| z) := by
ext i
simp [Bool.or_assoc]
/-! ### and -/
@[simp] theorem toNat_and (x y : BitVec v) :
@@ -498,11 +461,6 @@ theorem or_assoc (x y z : BitVec w) :
ext
simp
theorem and_assoc (x y z : BitVec w) :
x &&& y &&& z = x &&& (y &&& z) := by
ext i
simp [Bool.and_assoc]
/-! ### xor -/
@[simp] theorem toNat_xor (x y : BitVec v) :
@@ -523,11 +481,6 @@ theorem and_assoc (x y z : BitVec w) :
ext
simp
theorem xor_assoc (x y z : BitVec w) :
x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by
ext i
simp [Bool.xor_assoc]
/-! ### not -/
theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@@ -642,17 +595,6 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
(shiftLeftZeroExtend x i).msb = x.msb := by
simp [shiftLeftZeroExtend_eq, BitVec.msb]
theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
(x <<< n) <<< m = x <<< (n + m) := by
ext i
simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
rw [show i - (n + m) = (i - m - n) by omega]
cases h₂ : decide (i < m) <;>
cases h₃ : decide (i - m < w) <;>
cases h₄ : decide (i - m < n) <;>
cases h₅ : decide (i < n + m) <;>
simp at * <;> omega
/-! ### ushiftRight -/
@[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@@ -662,70 +604,6 @@ theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
getLsb (x >>> i) j = getLsb x (i+j) := by
unfold getLsb ; simp
/-! ### sshiftRight -/
theorem sshiftRight_eq {x : BitVec n} {i : Nat} :
x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i) := by
apply BitVec.eq_of_toInt_eq
simp [BitVec.sshiftRight]
/-- if the msb is false, the arithmetic shift right equals logical shift right -/
theorem sshiftRight_eq_of_msb_false {x : BitVec w} {s : Nat} (h : x.msb = false) :
(x.sshiftRight s) = x >>> s := by
apply BitVec.eq_of_toNat_eq
rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond]
have hxbound : 2 * x.toNat < 2 ^ w := (BitVec.msb_eq_false_iff_two_mul_lt x).mp h
simp only [hxbound, reduceIte, Int.natCast_shiftRight, Int.ofNat_eq_coe, ofInt_natCast,
toNat_ofNat, toNat_ushiftRight]
replace hxbound : x.toNat >>> s < 2 ^ w := by
rw [Nat.shiftRight_eq_div_pow]
exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) x.isLt
apply Nat.mod_eq_of_lt hxbound
/--
If the msb is `true`, the arithmetic shift right equals negating,
then logical shifting right, then negating again.
The double negation preserves the lower bits that have been shifted,
and the outer negation ensures that the high bits are '1'. -/
theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
(x.sshiftRight s) = ~~~((~~~x) >>> s) := by
apply BitVec.eq_of_toNat_eq
rcases w with rfl | w
· simp
· rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond]
have hxbound : (2 * x.toNat 2 ^ (w + 1)) := (BitVec.msb_eq_true_iff_two_mul_ge x).mp h
replace hxbound : ¬ (2 * x.toNat < 2 ^ (w + 1)) := by omega
simp only [hxbound, reduceIte, toNat_ofInt, toNat_not, toNat_ushiftRight]
rw [ Int.subNatNat_eq_coe, Int.subNatNat_of_lt (by omega),
Nat.pred_eq_sub_one, Int.negSucc_shiftRight,
Int.emod_negSucc, Int.natAbs_ofNat, Nat.succ_eq_add_one,
Int.subNatNat_of_le (by omega), Int.toNat_ofNat, Nat.mod_eq_of_lt,
Nat.sub_right_comm]
omega
· rw [Nat.shiftRight_eq_div_pow]
apply Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (by omega)
theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) :
getLsb (x.sshiftRight s) i =
(!decide (w i) && if s + i < w then x.getLsb (s + i) else x.msb) := by
rcases hmsb : x.msb with rfl | rfl
· simp only [sshiftRight_eq_of_msb_false hmsb, getLsb_ushiftRight, Bool.if_false_right]
by_cases hi : i w
· simp only [hi, decide_True, Bool.not_true, Bool.false_and]
apply getLsb_ge
omega
· simp only [hi, decide_False, Bool.not_false, Bool.true_and, Bool.iff_and_self,
decide_eq_true_eq]
intros hlsb
apply BitVec.lt_of_getLsb _ _ hlsb
· by_cases hi : i w
· simp [hi]
· simp only [sshiftRight_eq_of_msb_true hmsb, getLsb_not, getLsb_ushiftRight, Bool.not_and,
Bool.not_not, hi, decide_False, Bool.not_false, Bool.if_true_right, Bool.true_and,
Bool.and_iff_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not,
Nat.not_lt, decide_eq_true_eq]
omega
/-! ### append -/
theorem append_def (x : BitVec v) (y : BitVec w) :
@@ -802,11 +680,6 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
simp only [getLsb_append, cond_eq_if]
split <;> simp [*]
theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
(x >>> n) >>> m = x >>> (n + m) := by
ext i
simp [Nat.add_assoc n m i]
/-! ### rev -/
theorem getLsb_rev (x : BitVec w) (i : Fin w) :
@@ -1009,10 +882,6 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : x#n - y#n = .ofNat n (x + (2^n - y % 2
@[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
simp [Neg.neg, BitVec.neg]
@[simp] theorem toFin_neg (x : BitVec n) :
(-x).toFin = Fin.ofNat' (2^n - x.toNat) (Nat.two_pow_pos _) :=
rfl
theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
apply eq_of_toNat_eq
simp
@@ -1021,19 +890,10 @@ theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
apply eq_of_toNat_eq
have y_toNat_le := Nat.le_of_lt y.isLt
have y_toNat_le := Nat.le_of_lt y.toNat_lt
rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, Nat.add_sub_assoc y_toNat_le,
Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
theorem sub_add_cancel (x y : BitVec w) : x - y + y = x := by
rw [sub_toAdd, BitVec.add_assoc, BitVec.add_comm _ y,
BitVec.add_assoc, sub_toAdd, add_sub_cancel]
theorem eq_sub_iff_add_eq {x y z : BitVec w} : x = z - y x + y = z := by
apply Iff.intro <;> intro h
· simp [h, sub_add_cancel]
· simp [h, add_sub_cancel]
theorem negOne_eq_allOnes : -1#w = allOnes w := by
apply eq_of_toNat_eq
if g : w = 0 then
@@ -1043,13 +903,6 @@ theorem negOne_eq_allOnes : -1#w = allOnes w := by
have r : (2^w - 1) < 2^w := by omega
simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1 := by
apply eq_of_toNat_eq
simp only [toNat_neg, ofNat_eq_ofNat, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]
congr
have hx : x.toNat < 2^w := x.isLt
rw [Nat.sub_sub, Nat.add_comm 1 x.toNat, Nat.sub_sub, Nat.sub_add_cancel (by omega)]
/-! ### mul -/
theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
@@ -1144,171 +997,4 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by
(ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
simp [getMsb_eq_getLsb]
/-! # Rotate Left -/
/-- rotateLeft is invariant under `mod` by the bitwidth. -/
@[simp]
theorem rotateLeft_mod_eq_rotateLeft {x : BitVec w} {r : Nat} :
x.rotateLeft (r % w) = x.rotateLeft r := by
simp only [rotateLeft, Nat.mod_mod]
/-- `rotateLeft` equals the bit fiddling definition of `rotateLeftAux` when the rotation amount is
smaller than the bitwidth. -/
theorem rotateLeft_eq_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) :
x.rotateLeft r = x.rotateLeftAux r := by
simp only [rotateLeft, Nat.mod_eq_of_lt hr]
/--
Accessing bits in `x.rotateLeft r` the range `[0, r)` is equal to
accessing bits `x` in the range `[w - r, w)`.
Proof by example:
Let x := <6 5 4 3 2 1 0> : BitVec 7.
x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
(x.rotateLeft 2).getLsb ⟨i, i < 2⟩
= <3 2 1 0 | 6 5>.getLsb ⟨i, i < 2⟩
= <6 5>[i]
= <6 5 | 4 3 2 1 0>[i + len(<4 3 2 1 0>)]
= <6 5 | 4 3 2 1 0>[i + 7 - 2]
-/
theorem getLsb_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
(x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i) := by
rw [rotateLeftAux, getLsb_or, getLsb_ushiftRight]
suffices (x <<< r).getLsb i = false by
simp; omega
simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
omega
/--
Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to
accessing bits `x` in the range `[0, w - r)`.
Proof by example:
Let x := <6 5 4 3 2 1 0> : BitVec 7.
x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
(x.rotateLeft 2).getLsb ⟨i, i ≥ 2⟩
= <3 2 1 0 | 6 5>.getLsb ⟨i, i ≥ 2⟩
= <3 2 1 0>[i - 2]
= <6 5 | 3 2 1 0>[i - 2]
Intuitively, grab the full width (7), then move the marker `|` by `r` to the right `(-2)`
Then, access the bit at `i` from the right `(+i)`.
-/
theorem getLsb_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i r) :
(x.rotateLeftAux r).getLsb i = (decide (i < w) && x.getLsb (i - r)) := by
rw [rotateLeftAux, getLsb_or]
suffices (x >>> (w - r)).getLsb i = false by
have hiltr : decide (i < r) = false := by
simp [hi]
simp [getLsb_shiftLeft, Bool.or_false, hi, hiltr, this]
simp only [getLsb_ushiftRight]
apply getLsb_ge
omega
/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
theorem getLsb_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
(x.rotateLeft r).getLsb i =
cond (i < r)
(x.getLsb (w - r + i))
(decide (i < w) && x.getLsb (i - r)) := by
· rw [rotateLeft_eq_rotateLeftAux_of_lt hr]
by_cases h : i < r
· simp [h, getLsb_rotateLeftAux_of_le h]
· simp [h, getLsb_rotateLeftAux_of_geq <| Nat.ge_of_not_lt h]
@[simp]
theorem getLsb_rotateLeft {x : BitVec w} {r i : Nat} :
(x.rotateLeft r).getLsb i =
cond (i < r % w)
(x.getLsb (w - (r % w) + i))
(decide (i < w) && x.getLsb (i - (r % w))) := by
rcases w with rfl, w
· simp
· rw [ rotateLeft_mod_eq_rotateLeft, getLsb_rotateLeft_of_le (Nat.mod_lt _ (by omega))]
/-! ## Rotate Right -/
/--
Accessing bits in `x.rotateRight r` the range `[0, w-r)` is equal to
accessing bits `x` in the range `[r, w)`.
Proof by example:
Let x := <6 5 4 3 2 1 0> : BitVec 7.
x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>
(x.rotateLeft 2).getLsb ⟨i, i ≤ 7 - 2⟩
= <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩
= <6 5 4 3 2>.getLsb i
= <6 5 4 3 2 | 1 0>[i + 2]
-/
theorem getLsb_rotateRightAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
(x.rotateRightAux r).getLsb i = x.getLsb (r + i) := by
rw [rotateRightAux, getLsb_or, getLsb_ushiftRight]
suffices (x <<< (w - r)).getLsb i = false by
simp only [this, Bool.or_false]
simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
omega
/--
Accessing bits in `x.rotateRight r` the range `[w-r, w)` is equal to
accessing bits `x` in the range `[0, r)`.
Proof by example:
Let x := <6 5 4 3 2 1 0> : BitVec 7.
x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>
(x.rotateLeft 2).getLsb ⟨i, i ≥ 7 - 2⟩
= <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩
= <1 0>.getLsb (i - len(<6 5 4 3 2>)
= <6 5 4 3 2 | 1 0> (i - len<6 4 4 3 2>)
-/
theorem getLsb_rotateRightAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i w - r) :
(x.rotateRightAux r).getLsb i = (decide (i < w) && x.getLsb (i - (w - r))) := by
rw [rotateRightAux, getLsb_or]
suffices (x >>> r).getLsb i = false by
simp only [this, getLsb_shiftLeft, Bool.false_or]
by_cases hiw : i < w
<;> simp [hiw, hi]
simp only [getLsb_ushiftRight]
apply getLsb_ge
omega
/-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is
smaller than the bitwidth. -/
theorem rotateRight_eq_rotateRightAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) :
x.rotateRight r = x.rotateRightAux r := by
simp only [rotateRight, Nat.mod_eq_of_lt hr]
/-- rotateRight is invariant under `mod` by the bitwidth. -/
@[simp]
theorem rotateRight_mod_eq_rotateRight {x : BitVec w} {r : Nat} :
x.rotateRight (r % w) = x.rotateRight r := by
simp only [rotateRight, Nat.mod_mod]
/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
theorem getLsb_rotateRight_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
(x.rotateRight r).getLsb i =
cond (i < w - r)
(x.getLsb (r + i))
(decide (i < w) && x.getLsb (i - (w - r))) := by
· rw [rotateRight_eq_rotateRightAux_of_lt hr]
by_cases h : i < w - r
· simp [h, getLsb_rotateRightAux_of_le h]
· simp [h, getLsb_rotateRightAux_of_geq <| Nat.le_of_not_lt h]
@[simp]
theorem getLsb_rotateRight {x : BitVec w} {r i : Nat} :
(x.rotateRight r).getLsb i =
cond (i < w - (r % w))
(x.getLsb ((r % w) + i))
(decide (i < w) && x.getLsb (i - (w - (r % w)))) := by
rcases w with rfl, w
· simp
· rw [ rotateRight_mod_eq_rotateRight, getLsb_rotateRight_of_le (Nat.mod_lt _ (by omega))]
end BitVec

View File

@@ -227,8 +227,6 @@ instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
@[simp] theorem bne_left_inj : (x y z : Bool), (x != y) = (x != z) y = z := by decide
@[simp] theorem bne_right_inj : (x y z : Bool), (x != z) = (y != z) x = y := by decide
theorem eq_not_of_ne : {x y : Bool}, x y x = !y := by decide
/-! ### coercision related normal forms -/
theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
@@ -362,8 +360,7 @@ def toNat (b:Bool) : Nat := cond b 1 0
theorem toNat_le (c : Bool) : c.toNat 1 := by
cases c <;> trivial
@[deprecated toNat_le (since := "2024-02-23")]
abbrev toNat_le_one := toNat_le
@[deprecated toNat_le] abbrev toNat_le_one := toNat_le
theorem toNat_lt (b : Bool) : b.toNat < 2 :=
Nat.lt_succ_of_le (toNat_le _)

View File

@@ -5,4 +5,3 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Data.Char.Basic
import Init.Data.Char.Lemmas

View File

@@ -1,25 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Data.Char.Basic
import Init.Data.UInt.Lemmas
namespace Char
theorem le_def {a b : Char} : a b a.1 b.1 := .rfl
theorem lt_def {a b : Char} : a < b a.1 < b.1 := .rfl
theorem lt_iff_val_lt_val {a b : Char} : a < b a.val < b.val := Iff.rfl
@[simp] protected theorem not_le {a b : Char} : ¬ a b b < a := UInt32.not_le
@[simp] protected theorem not_lt {a b : Char} : ¬ a < b b a := UInt32.not_lt
@[simp] protected theorem le_refl (a : Char) : a a := by simp [le_def]
@[simp] protected theorem lt_irrefl (a : Char) : ¬ a < a := by simp
protected theorem le_trans {a b c : Char} : a b b c a c := UInt32.le_trans
protected theorem lt_trans {a b c : Char} : a < b b < c a < c := UInt32.lt_trans
protected theorem le_total (a b : Char) : a b b a := UInt32.le_total a.1 b.1
protected theorem lt_asymm {a b : Char} (h : a < b) : ¬ b < a := UInt32.lt_asymm h
protected theorem ne_of_lt {a b : Char} (h : a < b) : a b := Char.ne_of_val_ne (UInt32.ne_of_lt h)
end Char

View File

@@ -6,15 +6,12 @@ Authors: François G. Dorais
prelude
import Init.Data.Nat.Linear
namespace Fin
/-- Folds over `Fin n` from the left: `foldl 3 f x = f (f (f x 0) 1) 2`. -/
@[inline] def foldl (n) (f : α Fin n α) (init : α) : α := loop init 0 where
/-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)` -/
loop (x : α) (i : Nat) : α :=
if h : i < n then loop (f x i, h) (i+1) else x
termination_by n - i
decreasing_by decreasing_trivial_pre_omega
/-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
@[inline] def foldr (n) (f : Fin n α α) (init : α) : α := loop n, Nat.le_refl n init where
@@ -22,5 +19,3 @@ namespace Fin
loop : {i // i n} α α
| 0, _, x => x
| i+1, h, x => loop i, Nat.le_of_lt h (f i, h x)
end Fin

View File

@@ -23,7 +23,6 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
_root_.cast (congrArg P p) a
termination_by n - i
decreasing_by decreasing_trivial_pre_omega
/--
`hIterate` is a heterogenous iterative operation that applies a

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Leonardo de Moura
Authors: Mario Carneiro
-/
prelude
import Init.Data.Fin.Basic
@@ -11,9 +11,6 @@ import Init.ByCases
import Init.Conv
import Init.Omega
-- Remove after the next stage0 update
set_option allowUnsafeReducibility true
namespace Fin
/-- If you actually have an element of `Fin n`, then the `n` is always positive -/
@@ -62,8 +59,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
@[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
(Fin.ofNat' a is_pos).val = a % n := rfl
@[deprecated ofNat'_zero_val (since := "2024-02-22")]
theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
@[deprecated ofNat'_zero_val] theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
@[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
rfl
@@ -94,18 +90,6 @@ theorem lt_iff_val_lt_val {a b : Fin n} : a < b ↔ a.val < b.val := Iff.rfl
@[simp] protected theorem not_lt {a b : Fin n} : ¬ a < b b a := Nat.not_lt
@[simp] protected theorem le_refl (a : Fin n) : a a := by simp [le_def]
@[simp] protected theorem lt_irrefl (a : Fin n) : ¬ a < a := by simp
protected theorem le_trans {a b c : Fin n} : a b b c a c := Nat.le_trans
protected theorem lt_trans {a b c : Fin n} : a < b b < c a < c := Nat.lt_trans
protected theorem le_total (a b : Fin n) : a b b a := Nat.le_total a b
protected theorem lt_asymm {a b : Fin n} (h : a < b) : ¬ b < a := Nat.lt_asymm h
protected theorem ne_of_lt {a b : Fin n} (h : a < b) : a b := Fin.ne_of_val_ne (Nat.ne_of_lt h)
protected theorem ne_of_gt {a b : Fin n} (h : a < b) : b a := Fin.ne_of_val_ne (Nat.ne_of_gt h)
@@ -618,7 +602,6 @@ A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
@Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
cases i; rfl
/-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
This function has two arguments: `zero` handles the base case on `motive 0`,
and `succ` defines the inductive step using `motive i.castSucc`.
@@ -627,12 +610,8 @@ and `succ` defines the inductive step using `motive i.castSucc`.
@[elab_as_elim] def induction {motive : Fin (n + 1) Sort _} (zero : motive 0)
(succ : i : Fin n, motive (castSucc i) motive i.succ) :
i : Fin (n + 1), motive i
| i, hi => go i hi
where
-- Use a curried function so that this is structurally recursive
go : (i : Nat) (hi : i < n + 1), motive i, hi
| 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))
| 0, hi => by rwa [Fin.mk_zero]
| i+1, hi => succ i, Nat.lt_of_succ_lt_succ hi (induction zero succ i, Nat.lt_of_succ_lt hi)
@[simp] theorem induction_zero {motive : Fin (n + 1) Sort _} (zero : motive 0)
(hs : i : Fin n, motive (castSucc i) motive i.succ) :
@@ -835,3 +814,27 @@ protected theorem zero_mul (k : Fin (n + 1)) : (0 : Fin (n + 1)) * k = 0 := by
simp [ext_iff, mul_def]
end Fin
namespace USize
@[simp] theorem lt_def {a b : USize} : a < b a.toNat < b.toNat := .rfl
@[simp] theorem le_def {a b : USize} : a b a.toNat b.toNat := .rfl
@[simp] theorem zero_toNat : (0 : USize).toNat = 0 := Nat.zero_mod _
@[simp] theorem mod_toNat (a b : USize) : (a % b).toNat = a.toNat % b.toNat :=
Fin.mod_val ..
@[simp] theorem div_toNat (a b : USize) : (a / b).toNat = a.toNat / b.toNat :=
Fin.div_val ..
@[simp] theorem modn_toNat (a : USize) (b : Nat) : (a.modn b).toNat = a.toNat % b :=
Fin.modn_val ..
theorem mod_lt (a b : USize) (h : 0 < b) : a % b < b := USize.modn_lt _ (by simp at h; exact h)
theorem toNat.inj : {a b : USize}, a.toNat = b.toNat a = b
| _, _, _, _, rfl => rfl
end USize

View File

@@ -1,37 +0,0 @@
/-
Copyright (c) 2023 Siddharth Bhat. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Siddharth Bhat, Jeremy Avigad
-/
prelude
import Init.Data.Nat.Bitwise.Lemmas
import Init.Data.Int.Bitwise
namespace Int
theorem shiftRight_eq (n : Int) (s : Nat) : n >>> s = Int.shiftRight n s := rfl
@[simp]
theorem natCast_shiftRight (n s : Nat) : (n : Int) >>> s = n >>> s := rfl
@[simp]
theorem negSucc_shiftRight (m n : Nat) :
-[m+1] >>> n = -[m >>>n +1] := rfl
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]
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]
split
· simp
· rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))]
rfl
@[simp]
theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by
simp [Int.shiftRight_eq_div_pow]
end Int

View File

@@ -14,8 +14,6 @@ import Init.RCases
# Lemmas about integer division needed to bootstrap `omega`.
-/
-- Remove after the next stage0 update
set_option allowUnsafeReducibility true
open Nat (succ)
@@ -144,14 +142,12 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => show -ofNat _ = _ by simp
unseal Nat.div in
@[simp] protected theorem div_zero : a : Int, div a 0 = 0
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => rfl
@[simp] theorem zero_fdiv (b : Int) : fdiv 0 b = 0 := by cases b <;> rfl
unseal Nat.div in
@[simp] protected theorem fdiv_zero : a : Int, fdiv a 0 = 0
| 0 => rfl
| succ _ => rfl
@@ -182,7 +178,7 @@ theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a
@[simp] theorem mod_zero : a : Int, mod a 0 = a
| ofNat _ => congrArg ofNat <| Nat.mod_zero _
| -[_+1] => congrArg (fun n => -ofNat n) <| Nat.mod_zero _
| -[_+1] => rfl
@[simp] theorem zero_fmod (b : Int) : fmod 0 b = 0 := by cases b <;> rfl
@@ -229,9 +225,7 @@ theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
| ofNat m, -[n+1] => by
show (m % succ n + -(succ n) * -(m / succ n) : Int) = m
rw [Int.neg_mul_neg]; exact congrArg ofNat (Nat.mod_add_div ..)
| -[m+1], 0 => by
show -(((succ m) % 0) : Int) + 0 * -(succ m / 0) = -(succ m)
rw [Nat.mod_zero, Int.zero_mul, Int.add_zero]
| -[_+1], 0 => rfl
| -[m+1], ofNat n => by
show -(((succ m) % n) : Int) + n * -(succ m / n) = -(succ m)
rw [Int.mul_neg, Int.neg_add]
@@ -420,9 +414,6 @@ theorem negSucc_emod (m : Nat) {b : Int} (bpos : 0 < b) : -[m+1] % b = b - 1 - m
match b, eq_succ_of_zero_lt bpos with
| _, n, rfl => rfl
theorem emod_negSucc (m : Nat) (n : Int) :
(Int.negSucc m) % n = Int.subNatNat (Int.natAbs n) (Nat.succ (m % Int.natAbs n)) := rfl
theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = (m % n) := rfl
theorem emod_nonneg : (a : Int) {b : Int}, b 0 0 a % b
@@ -772,13 +763,11 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
| (n:Nat) => congrArg ofNat (Nat.div_one _)
| -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
unseal Nat.div in
@[simp] protected theorem div_neg : a b : Int, a.div (-b) = -(a.div b)
| ofNat m, 0 => show ofNat (m / 0) = -(m / 0) by rw [Nat.div_zero]; rfl
| ofNat m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
| ofNat m, succ n | -[m+1], 0 | -[m+1], -[n+1] => rfl
unseal Nat.div in
@[simp] protected theorem neg_div : a b : Int, (-a).div b = -(a.div b)
| 0, n => by simp [Int.neg_zero]
| succ m, (n:Nat) | -[m+1], 0 | -[m+1], -[n+1] => rfl
@@ -947,7 +936,6 @@ theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :
match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
| _, _, _, rfl, _, rfl => ofNat_fdiv .. ofNat_zero_le _
unseal Nat.div in
theorem fdiv_nonpos : {a b : Int}, 0 a b 0 a.fdiv b 0
| 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => _

View File

@@ -96,7 +96,7 @@ protected theorem le_antisymm {a b : Int} (h₁ : a ≤ b) (h₂ : b ≤ a) : a
have := Int.ofNat.inj <| Int.add_left_cancel <| this.trans (Int.add_zero _).symm
rw [ hn, Nat.eq_zero_of_add_eq_zero_left this, ofNat_zero, Int.add_zero a]
@[simp] protected theorem lt_irrefl (a : Int) : ¬a < a := fun H =>
protected theorem lt_irrefl (a : Int) : ¬a < a := fun H =>
let n, hn := lt.dest H
have : (a+Nat.succ n) = a+0 := by
rw [hn, Int.add_zero]
@@ -813,20 +813,6 @@ protected theorem sub_lt_sub_right {a b : Int} (h : a < b) (c : Int) : a - c < b
protected theorem sub_lt_sub {a b c d : Int} (hab : a < b) (hcd : c < d) : a - d < b - c :=
Int.add_lt_add hab (Int.neg_lt_neg hcd)
protected theorem lt_of_sub_lt_sub_left {a b c : Int} (h : c - a < c - b) : b < a :=
Int.lt_of_neg_lt_neg <| Int.lt_of_add_lt_add_left h
protected theorem lt_of_sub_lt_sub_right {a b c : Int} (h : a - c < b - c) : a < b :=
Int.lt_of_add_lt_add_right h
@[simp] protected theorem sub_lt_sub_left_iff (a b c : Int) :
c - a < c - b b < a :=
Int.lt_of_sub_lt_sub_left, (Int.sub_lt_sub_left · c)
@[simp] protected theorem sub_lt_sub_right_iff (a b c : Int) :
a - c < b - c a < b :=
Int.lt_of_sub_lt_sub_right, (Int.sub_lt_sub_right · c)
protected theorem sub_lt_sub_of_le_of_lt {a b c d : Int}
(hab : a b) (hcd : c < d) : a - d < b - c :=
Int.add_lt_add_of_le_of_lt hab (Int.neg_lt_neg hcd)

View File

@@ -9,4 +9,3 @@ import Init.Data.List.BasicAux
import Init.Data.List.Control
import Init.Data.List.Lemmas
import Init.Data.List.Impl
import Init.Data.List.TakeDrop

View File

@@ -226,10 +226,9 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
over a nested inductive like `inductive T | mk : List T → T`. -/
macro "sizeOf_list_dec" : tactic =>
`(tactic| first
| with_reducible apply sizeOf_lt_of_mem; assumption; done
| with_reducible
apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
case' h => assumption
| apply sizeOf_lt_of_mem; assumption; done
| apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
case' h => assumption
simp_arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)

File diff suppressed because it is too large Load Diff

View File

@@ -1,360 +0,0 @@
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
-/
prelude
import Init.Data.List.Lemmas
import Init.Data.Nat.Lemmas
/-!
# Lemmas about `List.take`, `List.drop`, `List.zip` and `List.zipWith`.
These are in a separate file from most of the list lemmas
as they required importing more lemmas about natural numbers.
-/
namespace List
open Nat
/-! ### take -/
abbrev take_succ_cons := @take_cons_succ
@[simp] theorem length_take : (i : Nat) (l : List α), length (take i l) = min i (length l)
| 0, l => by simp [Nat.zero_min]
| succ n, [] => by simp [Nat.min_zero]
| succ n, _ :: l => by simp [Nat.succ_min_succ, length_take]
theorem length_take_le (n) (l : List α) : length (take n l) n := by simp [Nat.min_le_left]
theorem length_take_le' (n) (l : List α) : length (take n l) l.length :=
by simp [Nat.min_le_right]
theorem length_take_of_le (h : n length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
theorem take_all_of_le {n} {l : List α} (h : length l n) : take n l = l :=
take_length_le h
@[simp]
theorem take_left : l₁ l₂ : List α, take (length l₁) (l₁ ++ l₂) = l₁
| [], _ => rfl
| a :: l₁, l₂ => congrArg (cons a) (take_left l₁ l₂)
theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁ := by
rw [ h]; apply take_left
theorem take_take : (n m) (l : List α), take n (take m l) = take (min n m) l
| n, 0, l => by rw [Nat.min_zero, take_zero, take_nil]
| 0, m, l => by rw [Nat.zero_min, take_zero, take_zero]
| succ n, succ m, nil => by simp only [take_nil]
| succ n, succ m, a :: l => by
simp only [take, succ_min_succ, take_take n m l]
theorem take_replicate (a : α) : n m : Nat, take n (replicate m a) = replicate (min n m) a
| n, 0 => by simp [Nat.min_zero]
| 0, m => by simp [Nat.zero_min]
| succ n, succ m => by simp [succ_min_succ, take_replicate]
theorem map_take (f : α β) :
(L : List α) (i : Nat), (L.take i).map f = (L.map f).take i
| [], i => by simp
| _, 0 => by simp
| h :: t, n + 1 => by dsimp; rw [map_take f t n]
/-- Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements
of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
theorem take_append_eq_append_take {l₁ l₂ : List α} {n : Nat} :
take n (l₁ ++ l₂) = take n l₁ ++ take (n - l₁.length) l₂ := by
induction l₁ generalizing n
· simp
· cases n
· simp [*]
· simp only [cons_append, take_cons_succ, length_cons, succ_eq_add_one, cons.injEq,
append_cancel_left_eq, true_and, *]
congr 1
omega
theorem take_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n l₁.length) :
(l₁ ++ l₂).take n = l₁.take n := by
simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]
/-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
`i` elements of `l₂` to `l₁`. -/
theorem take_append {l₁ l₂ : List α} (i : Nat) :
take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂ := by
rw [take_append_eq_append_take, take_all_of_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
length `> i`. Version designed to rewrite from the big list to the small list. -/
theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
get L i, hi = get (L.take j) i, length_take .. Nat.lt_min.mpr hj, hi :=
get_of_eq (take_append_drop j L).symm _ get_append ..
/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
length `> i`. Version designed to rewrite from the small list to the big list. -/
theorem get_take' (L : List α) {j i} :
get (L.take j) i =
get L i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _) := by
let i, hi := i; rw [length_take, Nat.lt_min] at hi; rw [get_take L _ hi.1]
theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
induction n generalizing l m with
| zero =>
exact absurd h (Nat.not_lt_of_le m.zero_le)
| succ _ hn =>
cases l with
| nil => simp only [take_nil]
| cons hd tl =>
cases m
· simp only [get?, take]
· simpa only using hn (Nat.lt_of_succ_lt_succ h)
theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n m) :
(l.take n).get? m = none :=
get?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
theorem get?_take_eq_if {l : List α} {n m : Nat} :
(l.take n).get? m = if m < n then l.get? m else none := by
split
· next h => exact get?_take h
· next h => exact get?_take_eq_none (Nat.le_of_not_lt h)
@[simp]
theorem nth_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1)).get? n = l.get? n :=
get?_take (Nat.lt_succ_self n)
theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ (l.get? n).toList := by
induction l generalizing n with
| nil =>
simp only [Option.toList, get?, take_nil, append_nil]
| cons hd tl hl =>
cases n
· simp only [Option.toList, get?, eq_self_iff_true, take, nil_append]
· simp only [hl, cons_append, get?, eq_self_iff_true, take]
@[simp]
theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] l = [] k = 0 := by
cases l <;> cases k <;> simp [Nat.succ_ne_zero]
@[simp]
theorem take_eq_take :
{l : List α} {m n : Nat}, l.take m = l.take n min m l.length = min n l.length
| [], m, n => by simp [Nat.min_zero]
| _ :: xs, 0, 0 => by simp
| x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
| x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ]
| x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]; omega
theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n := by
suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by
rw [take_append_drop] at this
assumption
rw [take_append_eq_append_take, take_all_of_le, append_right_inj]
· simp only [take_eq_take, length_take, length_drop]
omega
apply Nat.le_trans (m := m)
· apply length_take_le
· apply Nat.le_add_right
theorem take_eq_nil_of_eq_nil : {as : List α} {i}, as = [] as.take i = []
| _, _, rfl => take_nil
theorem ne_nil_of_take_ne_nil {as : List α} {i : Nat} (h: as.take i []) : as [] :=
mt take_eq_nil_of_eq_nil h
theorem dropLast_eq_take (l : List α) : l.dropLast = l.take l.length.pred := by
cases l with
| nil => simp [dropLast]
| cons x l =>
induction l generalizing x with
| nil => simp [dropLast]
| cons hd tl hl => simp [dropLast, hl]
theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
(l.take n).dropLast = l.take n.pred := by
simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, take_take, pred_le, Nat.min_eq_left]
theorem map_eq_append_split {f : α β} {l : List α} {s₁ s₂ : List β}
(h : map f l = s₁ ++ s₂) : l₁ l₂, l = l₁ ++ l₂ map f l₁ = s₁ map f l₂ = s₂ := by
have := h
rw [ take_append_drop (length s₁) l] at this
rw [map_append] at this
refine _, _, rfl, append_inj this ?_
rw [length_map, length_take, Nat.min_eq_left]
rw [ length_map l f, h, length_append]
apply Nat.le_add_right
/-! ### drop -/
@[simp]
theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] l.length k := by
refine' fun h => _, drop_eq_nil_of_le
induction k generalizing l with
| zero =>
simp only [drop] at h
simp [h]
| succ k hk =>
cases l
· simp
· simp only [drop] at h
simpa [Nat.succ_le_succ_iff] using hk h
theorem drop_length_cons {l : List α} (h : l []) (a : α) :
(a :: l).drop l.length = [l.getLast h] := by
induction l generalizing a with
| nil =>
cases h rfl
| cons y l ih =>
simp only [drop, length]
by_cases h₁ : l = []
· simp [h₁]
rw [getLast_cons' _ h₁]
exact ih h₁ y
/-- Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n`
in `l₁`, dropping the elements up to `n - l₁.length` in `l₂`, and appending them. -/
theorem drop_append_eq_append_drop {l₁ l₂ : List α} {n : Nat} :
drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂ := by
induction l₁ generalizing n
· simp
· cases n
· simp [*]
· simp only [cons_append, drop_succ_cons, length_cons, succ_eq_add_one, append_cancel_left_eq, *]
congr 1
omega
theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n l₁.length) :
(l₁ ++ l₂).drop n = l₁.drop n ++ l₂ := by
simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]
/-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
up to `i` in `l₂`. -/
@[simp]
theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂ := by
rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
simp [Nat.add_sub_cancel_left, Nat.le_add_right]
theorem drop_sizeOf_le [SizeOf α] (l : List α) (n : Nat) : sizeOf (l.drop n) sizeOf l := by
induction l generalizing n with
| nil => rw [drop_nil]; apply Nat.le_refl
| cons _ _ lih =>
induction n with
| zero => apply Nat.le_refl
| succ n =>
exact Trans.trans (lih _) (Nat.le_add_left _ _)
theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L.drop i).length := by
have A : i < L.length := Nat.lt_of_le_of_lt (Nat.le.intro rfl) h
rw [(take_append_drop i L).symm] at h
simpa only [Nat.le_of_lt A, Nat.min_eq_left, Nat.add_lt_add_iff_left, length_take,
length_append] using h
/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
get L i + j, h = get (L.drop i) j, lt_length_drop L h := by
have : i L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
rw [get_of_eq (take_append_drop i L).symm i + j, h, get_append_right'] <;>
simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right]
/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
theorem get_drop' (L : List α) {i j} :
get (L.drop i) j = get L i + j, by
rw [Nat.add_comm]
exact Nat.add_lt_of_lt_sub (length_drop i L j.2) := by
rw [get_drop]
@[simp]
theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
ext
simp only [get?_eq_some, get_drop', Option.mem_def]
constructor <;> intro h, ha
· exact _, ha
· refine ?_, ha
rw [length_drop]
rw [Nat.add_comm] at h
apply Nat.lt_sub_of_add_lt h
@[simp] theorem drop_drop (n : Nat) : (m) (l : List α), drop n (drop m l) = drop (n + m) l
| m, [] => by simp
| 0, l => by simp
| m + 1, a :: l =>
calc
drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
_ = drop (n + m) l := drop_drop n m l
_ = drop (n + (m + 1)) (a :: l) := rfl
theorem take_drop : (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
| 0, _, _ => by simp
| _, _, [] => by simp
| _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
theorem drop_take : (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
| 0, _, _ => by simp
| _, 0, _ => by simp
| _, _, [] => by simp
| m+1, n+1, h :: t => by
simp [take_succ_cons, drop_succ_cons, drop_take m n t]
congr 1
omega
theorem map_drop (f : α β) :
(L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
| [], i => by simp
| L, 0 => by simp
| h :: t, n + 1 => by
dsimp
rw [map_drop f t]
theorem reverse_take {α} {xs : List α} (n : Nat) (h : n xs.length) :
xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
induction xs generalizing n <;>
simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
next xs_hd xs_tl xs_ih =>
cases Nat.lt_or_eq_of_le h with
| inl h' =>
have h' := Nat.le_of_succ_le_succ h'
rw [take_append_of_le_length, xs_ih _ h']
rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
· rwa [succ_eq_add_one, Nat.sub_add_comm]
· rwa [length_reverse]
| inr h' =>
subst h'
rw [length, Nat.sub_self, drop]
suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
rw [this, take_length, reverse_cons]
rw [length_append, length_reverse]
rfl
@[simp]
theorem get_cons_drop : (l : List α) i, get l i :: drop (i + 1) l = drop i l
| _::_, 0, _ => rfl
| _::_, i+1, _ => get_cons_drop _ i, _
theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l n, h :: drop (n + 1) l :=
(get_cons_drop _ n, h).symm
theorem drop_eq_nil_of_eq_nil : {as : List α} {i}, as = [] as.drop i = []
| _, _, rfl => drop_nil
theorem ne_nil_of_drop_ne_nil {as : List α} {i : Nat} (h: as.drop i []) : as [] :=
mt drop_eq_nil_of_eq_nil h
/-! ### zipWith -/
@[simp] theorem length_zipWith (f : α β γ) (l₁ l₂) :
length (zipWith f l₁ l₂) = min (length l₁) (length l₂) := by
induction l₁ generalizing l₂ <;> cases l₂ <;>
simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
/-! ### zip -/
@[simp] theorem length_zip (l₁ : List α) (l₂ : List β) :
length (zip l₁ l₂) = min (length l₁) (length l₂) := by
simp [zip]
end List

View File

@@ -78,8 +78,6 @@ of a number.
-/
/-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/
def testBit (m n : Nat) : Bool :=
-- `1 &&& n` is faster than `n &&& 1` for big `n`.
1 &&& (m >>> n) != 0
def testBit (m n : Nat) : Bool := (m >>> n) &&& 1 != 0
end Nat

View File

@@ -50,23 +50,13 @@ noncomputable def div2Induction {motive : Nat → Sort u}
apply hyp
exact Nat.div_lt_self n_pos (Nat.le_refl _)
@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by
simp only [HAnd.hAnd, AndOp.and, land]
unfold bitwise
simp
@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
@[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
simp only [HAnd.hAnd, AndOp.and, land]
unfold bitwise
simp
@[simp] theorem one_and_eq_mod_two (n : Nat) : 1 &&& n = n % 2 := by
if n0 : n = 0 then
subst n0; decide
else
simp only [HAnd.hAnd, AndOp.and, land]
cases mod_two_eq_zero_or_one n with | _ h => simp [bitwise, n0, h]
@[simp] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
if xz : x = 0 then
simp [xz, zero_and]
@@ -81,7 +71,7 @@ noncomputable def div2Induction {motive : Nat → Sort u}
/-! ### testBit -/
@[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
simp only [testBit, zero_shiftRight, and_zero, bne_self_eq_false]
simp only [testBit, zero_shiftRight, zero_and, bne_self_eq_false]
@[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
@@ -198,6 +188,8 @@ theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = fal
have test_false := p _ i_ge_n
simp only [test_true] at test_false
/-! ### testBit -/
private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
induction x with
| zero =>
@@ -241,7 +233,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
| d+1 =>
simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
@[simp] theorem testBit_mod_two_pow (x j i : Nat) :
testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
@@ -265,7 +257,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
exact Nat.lt_add_of_pos_right (Nat.two_pow_pos j)
simp only [hyp y y_lt_x]
if i_lt_j : i < j then
rw [Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
rw [ Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
else
simp [i_lt_j]
@@ -410,12 +402,12 @@ theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
/-! ### lor -/
@[simp] theorem zero_or (x : Nat) : 0 ||| x = x := by
@[simp] theorem or_zero (x : Nat) : 0 ||| x = x := by
simp only [HOr.hOr, OrOp.or, lor]
unfold bitwise
simp [@eq_comm _ 0]
@[simp] theorem or_zero (x : Nat) : x ||| 0 = x := by
@[simp] theorem zero_or (x : Nat) : x ||| 0 = x := by
simp only [HOr.hOr, OrOp.or, lor]
unfold bitwise
simp [@eq_comm _ 0]

View File

@@ -82,34 +82,22 @@ decreasing_by apply div_rec_lemma; assumption
@[extern "lean_nat_mod"]
protected def mod : @& Nat @& Nat Nat
/-
Nat.modCore is defined by well-founded recursion and thus irreducible. Nevertheless it is
desireable if trivial `Nat.mod` calculations, namely
* `Nat.mod 0 m` for all `m`
* `Nat.mod n (m+n)` for concrete literals `n`
reduce definitionally.
This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
definition.
-/
/- This case is not needed mathematically as the case below is equal to it; however, it makes
`0 % n = 0` true definitionally rather than just propositionally.
This property is desirable for `Fin n`, as it means `(ofNat 0 : Fin n).val = 0` by definition.
Primarily, this is valuable because mathlib in Lean3 assumed this was true definitionally, and so
keeping this definitional equality makes mathlib easier to port to mathlib4. -/
| 0, _ => 0
| n@(_ + 1), m =>
if m n -- NB: if n < m does not reduce as well as `m ≤ n`!
then Nat.modCore n m
else n
| x@(_ + 1), y => Nat.modCore x y
instance instMod : Mod Nat := Nat.mod
protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
show Nat.modCore n m = Nat.mod n m
match n, m with
| 0, _ =>
protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
cases x with
| zero =>
rw [Nat.modCore]
exact if_neg fun hlt, hle => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
| (_ + 1), _ =>
rw [Nat.mod]; dsimp
refine iteInduction (fun _ => rfl) (fun h => ?false) -- cannot use `split` this early yet
rw [Nat.modCore]
exact if_neg fun _hlt, hle => h hle
| succ x => rfl
theorem mod_eq (x y : Nat) : x % y = if 0 < y y x then (x - y) % y else x := by
rw [Nat.modCore_eq_mod, Nat.modCore_eq_mod, Nat.modCore]

View File

@@ -37,11 +37,11 @@ def gcd (m n : @& Nat) : Nat :=
termination_by m
decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y := by
rw [gcd]; rfl
@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
rfl
theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
rw [gcd]; rfl
theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
rfl
@[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
rw [gcd_succ, mod_one]
@@ -64,7 +64,7 @@ instance : Std.IdempotentOp gcd := ⟨gcd_self⟩
theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
match m with
| 0 => by have := (mod_zero n).symm; rwa [gcd, gcd_zero_right]
| 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
| _ + 1 => by simp [gcd_succ]
@[elab_as_elim] theorem gcd.induction {P : Nat Nat Prop} (m n : Nat)

View File

@@ -137,14 +137,14 @@ protected theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c
protected theorem le_sub_iff_add_le {n : Nat} (h : k m) : n m - k n + k m :=
Nat.add_le_of_le_sub h, Nat.le_sub_of_add_le
@[deprecated Nat.le_sub_iff_add_le (since := "2024-02-19")]
@[deprecated Nat.le_sub_iff_add_le]
protected theorem add_le_to_le_sub (n : Nat) (h : m k) : n + m k n k - m :=
(Nat.le_sub_iff_add_le h).symm
protected theorem add_le_of_le_sub' {n k m : Nat} (h : m k) : n k - m m + n k :=
Nat.add_comm .. Nat.add_le_of_le_sub h
@[deprecated Nat.add_le_of_le_sub' (since := "2024-02-19")]
@[deprecated Nat.add_le_of_le_sub']
protected theorem add_le_of_le_sub_left {n k m : Nat} (h : m k) : n k - m m + n k :=
Nat.add_le_of_le_sub' h
@@ -401,11 +401,11 @@ protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min
/-! ### mul -/
@[deprecated Nat.mul_le_mul_left (since := "2024-02-19")]
@[deprecated Nat.mul_le_mul_left]
protected theorem mul_le_mul_of_nonneg_left {a b c : Nat} : a b c * a c * b :=
Nat.mul_le_mul_left c
@[deprecated Nat.mul_le_mul_right (since := "2024-02-19")]
@[deprecated Nat.mul_le_mul_right]
protected theorem mul_le_mul_of_nonneg_right {a b c : Nat} : a b a * c b * c :=
Nat.mul_le_mul_right c
@@ -478,7 +478,6 @@ protected theorem mul_lt_mul_of_lt_of_lt {a b c d : Nat} (hac : a < c) (hbd : b
theorem succ_mul_succ (a b) : succ a * succ b = a * b + a + b + 1 := by
rw [succ_mul, mul_succ]; rfl
theorem mul_le_add_right (m k n : Nat) : k * m m + n (k-1) * m n := by
match k with
| 0 =>
@@ -678,10 +677,6 @@ protected theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
/-! ### log2 -/
@[simp]
theorem log2_zero : Nat.log2 0 = 0 := by
simp [Nat.log2]
theorem le_log2 (h : n 0) : k n.log2 2 ^ k n := by
match k with
| 0 => simp [show 1 n from Nat.pos_of_ne_zero h]
@@ -702,7 +697,7 @@ theorem log2_self_le (h : n ≠ 0) : 2 ^ n.log2 ≤ n := (le_log2 h).1 (Nat.le_r
theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
match n with
| 0 => by simp
| 0 => Nat.zero_lt_two
| n+1 => (log2_lt n.succ_ne_zero).1 (Nat.le_refl _)
/-! ### dvd -/
@@ -794,9 +789,6 @@ theorem shiftLeft_shiftLeft (m n : Nat) : ∀ k, (m <<< n) <<< k = m <<< (n + k)
| 0 => rfl
| k + 1 => by simp [ Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
@[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 _)]
theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
match x with
| 0 => simp

View File

@@ -714,10 +714,4 @@ theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly
simp [Expr.toNormPoly, Poly.norm] at h
assumption
end Linear
def elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b α) : α := by
simp_arith at h₁
exact h₂ h₁
end Nat
end Nat.Linear

View File

@@ -18,8 +18,8 @@ def getM [Alternative m] : Option α → m α
| none => failure
| some a => pure a
@[deprecated getM (since := "2024-04-17")]
def toMonad [Monad m] [Alternative m] : Option α m α := getM
@[deprecated getM] def toMonad [Monad m] [Alternative m] : Option α m α :=
getM
/-- Returns `true` on `some x` and `false` on `none`. -/
@[inline] def isSome : Option α Bool

View File

@@ -101,7 +101,7 @@ theorem ball_ne_none {p : Option α → Prop} : (∀ x (_ : x ≠ none), p x)
@[simp] theorem bind_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
cases x <;> rfl
theorem bind_eq_some : x.bind f = some b a, x = some a f a = some b := by
@[simp] theorem bind_eq_some : x.bind f = some b a, x = some a f a = some b := by
cases x <;> simp
@[simp] theorem bind_eq_none {o : Option α} {f : α Option β} :
@@ -119,7 +119,7 @@ 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
theorem join_eq_some : x.join = some a x = some (some a) := by
simp [bind_eq_some]
simp
theorem join_ne_none : x.join none z, x = some (some z) := by
simp only [ne_none_iff_exists', join_eq_some, iff_self]

View File

@@ -94,7 +94,7 @@ instance : Stream (Subarray α) α where
next? s :=
if h : s.start < s.stop then
have : s.start + 1 s.stop := Nat.succ_le_of_lt h
some (s.array.get s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size,
some (s.as.get s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size,
{ s with start := s.start + 1, start_le_stop := this })
else
none

View File

@@ -6,4 +6,3 @@ Authors: Leonardo de Moura
prelude
import Init.Data.String.Basic
import Init.Data.String.Extra
import Init.Data.String.Lemmas

View File

@@ -24,59 +24,23 @@ instance : LT String :=
instance decLt (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
List.hasDecidableLt s₁.data s₂.data
@[reducible] protected def le (a b : String) : Prop := ¬ b < a
instance : LE String :=
String.le
instance decLE (s₁ s₂ : String) : Decidable (s₁ s₂) :=
inferInstanceAs (Decidable (Not _))
/--
Returns the length of a string in Unicode code points.
Examples:
* `"".length = 0`
* `"abc".length = 3`
* `"L∃∀N".length = 4`
-/
@[extern "lean_string_length"]
def length : (@& String) Nat
| s => s.length
/--
Pushes a character onto the end of a string.
The internal implementation uses dynamic arrays and will perform destructive updates
if the string is not shared.
Example: `"abc".push 'd' = "abcd"`
-/
/-- The internal implementation uses dynamic arrays and will perform destructive updates
if the String is not shared. -/
@[extern "lean_string_push"]
def push : String Char String
| s, c => s ++ [c]
/--
Appends two strings.
The internal implementation uses dynamic arrays and will perform destructive updates
if the string is not shared.
Example: `"abc".append "def" = "abcdef"`
-/
/-- The internal implementation uses dynamic arrays and will perform destructive updates
if the String is not shared. -/
@[extern "lean_string_append"]
def append : String (@& String) String
| a, b => a ++ b
/--
Converts a string to a list of characters.
Even though the logical model of strings is as a structure that wraps a list of characters,
this operation takes time and space linear in the length of the string, because the compiler
uses an optimized representation as dynamic arrays.
Example: `"abc".toList = ['a', 'b', 'c']`
-/
/-- O(n) in the runtime, where n is the length of the String -/
def toList (s : String) : List Char :=
s.data
@@ -95,17 +59,9 @@ def utf8GetAux : List Char → Pos → Pos → Char
| c::cs, i, p => if i = p then c else utf8GetAux cs (i + c) p
/--
Returns the character at position `p` of a string. If `p` is not a valid position,
returns `(default : Char)`.
See `utf8GetAux` for the reference implementation.
Examples:
* `"abc".get ⟨1⟩ = 'b'`
* `"abc".get ⟨3⟩ = (default : Char) = 'A'`
Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
character. For example,`"L∃∀N".get ⟨2⟩ = (default : Char) = 'A'`.
Return character at position `p`. If `p` is not a valid position
returns `(default : Char)`.
See `utf8GetAux` for the reference implementation.
-/
@[extern "lean_string_utf8_get"]
def get (s : @& String) (p : @& Pos) : Char :=
@@ -116,30 +72,12 @@ def utf8GetAux? : List Char → Pos → Pos → Option Char
| [], _, _ => none
| c::cs, i, p => if i = p then c else utf8GetAux? cs (i + c) p
/--
Returns the character at position `p`. If `p` is not a valid position, returns `none`.
Examples:
* `"abc".get? ⟨1⟩ = some 'b'`
* `"abc".get? ⟨3⟩ = none`
Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
character. For example, `"L∃∀N".get? ⟨2⟩ = none`
-/
@[extern "lean_string_utf8_get_opt"]
def get? : (@& String) (@& Pos) Option Char
| s, p => utf8GetAux? s 0 p
/--
Returns the character at position `p` of a string. If `p` is not a valid position,
returns `(default : Char)` and produces a panic error message.
Examples:
* `"abc".get! ⟨1⟩ = 'b'`
* `"abc".get! ⟨3⟩` panics
Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example,
`"L∃∀N".get! ⟨2⟩` panics.
Similar to `get`, but produces a panic error message if `p` is not a valid `String.Pos`.
-/
@[extern "lean_string_utf8_get_bang"]
def get! (s : @& String) (p : @& Pos) : Char :=
@@ -151,49 +89,13 @@ def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
| c::cs, i, p =>
if i = p then (c'::cs) else c::(utf8SetAux c' cs (i + c) p)
/--
Replaces the character at a specified position in a string with a new character. If the position
is invalid, the string is returned unchanged.
If both the replacement character and the replaced character are ASCII characters and the string
is not shared, destructive updates are used.
Examples:
* `"abc".set ⟨1⟩ 'B' = "aBc"`
* `"abc".set ⟨3⟩ 'D' = "abc"`
* `"L∃∀N".set ⟨4⟩ 'X' = "L∃XN"`
Because `'∃'` is a multi-byte character, the byte index `2` in `L∃∀N` is an invalid position,
so `"L∃∀N".set ⟨2⟩ 'X' = "L∃∀N"`.
-/
@[extern "lean_string_utf8_set"]
def set : String (@& Pos) Char String
| s, i, c => utf8SetAux c s 0 i
/--
Replaces the character at position `p` in the string `s` with the result of applying `f` to that character.
If `p` is an invalid position, the string is returned unchanged.
Examples:
* `abc.modify ⟨1⟩ Char.toUpper = "aBc"`
* `abc.modify ⟨3⟩ Char.toUpper = "abc"`
-/
def modify (s : String) (i : Pos) (f : Char Char) : String :=
s.set i <| f <| s.get i
/--
Returns the next position in a string after position `p`. If `p` is not a valid position or `p = s.endPos`,
the result is unspecified.
Examples:
Given `def abc := "abc"` and `def lean := "L∃∀N"`,
* `abc.get (0 |> abc.next) = 'b'`
* `lean.get (0 |> lean.next |> lean.next) = '∀'`
Cases where the result is unspecified:
* `"abc".next ⟨3⟩`, since `3 = s.endPos`
* `"L∃∀N".next ⟨2⟩`, since `2` points into the middle of a multi-byte UTF-8 character
-/
@[extern "lean_string_utf8_next"]
def next (s : @& String) (p : @& Pos) : Pos :=
let c := get s p
@@ -205,52 +107,16 @@ def utf8PrevAux : List Char → Pos → Pos → Pos
let i' := i + c
if i' = p then i else utf8PrevAux cs i' p
/--
Returns the position in a string before a specified position, `p`. If `p = ⟨0⟩`, returns `0`.
If `p` is not a valid position, the result is unspecified.
Examples:
Given `def abc := "abc"` and `def lean := "L∃∀N"`,
* `abc.get (abc.endPos |> abc.prev) = 'c'`
* `lean.get (lean.endPos |> lean.prev |> lean.prev |> lean.prev) = '∃'`
* `"L∃∀N".prev ⟨3⟩` is unspecified, since byte 3 occurs in the middle of the multi-byte character `'∃'`.
-/
@[extern "lean_string_utf8_prev"]
def prev : (@& String) (@& Pos) Pos
| s, p => if p = 0 then 0 else utf8PrevAux s 0 p
/--
Returns the first character in `s`. If `s = ""`, returns `(default : Char)`.
Examples:
* `"abc".front = 'a'`
* `"".front = (default : Char)`
-/
def front (s : String) : Char :=
get s 0
/--
Returns the last character in `s`. If `s = ""`, returns `(default : Char)`.
Examples:
* `"abc".back = 'c'`
* `"".back = (default : Char)`
-/
def back (s : String) : Char :=
get s (prev s s.endPos)
/--
Returns `true` if a specified position is greater than or equal to the position which
points to the end of a string. Otherwise, returns `false`.
Examples:
Given `def abc := "abc"` and `def lean := "L∃∀N"`,
* `(0 |> abc.next |> abc.next |> abc.atEnd) = false`
* `(0 |> abc.next |> abc.next |> abc.next |> abc.next |> abc.atEnd) = true`
* `(0 |> lean.next |> lean.next |> lean.next |> lean.next |> lean.atEnd) = true`
Because `"L∃∀N"` contains multi-byte characters, `lean.next (lean.next 0)` is not equal to `abc.next (abc.next 0)`.
-/
@[extern "lean_string_utf8_at_end"]
def atEnd : (@& String) (@& Pos) Bool
| s, p => p.byteIdx utf8ByteSize s
@@ -728,15 +594,13 @@ def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos)
off1.byteIdx + sz s1.endPos.byteIdx && off2.byteIdx + sz s2.endPos.byteIdx && loop off1 off2 { byteIdx := off1.byteIdx + sz }
where
loop (off1 off2 stop1 : Pos) :=
if _h : off1.byteIdx < stop1.byteIdx then
if h : off1.byteIdx < stop1.byteIdx then
let c₁ := s1.get off1
let c₂ := s2.get off2
have := Nat.sub_lt_sub_left h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
else true
termination_by stop1.1 - off1.1
decreasing_by
have := Nat.sub_lt_sub_left _h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
decreasing_tactic
/-- Return true iff `p` is a prefix of `s` -/
def isPrefixOf (p : String) (s : String) : Bool :=
@@ -951,10 +815,6 @@ def beq (ss1 ss2 : Substring) : Bool :=
instance hasBeq : BEq Substring := beq
/-- Checks whether two substrings have the same position and content. -/
def sameAs (ss1 ss2 : Substring) : Bool :=
ss1.startPos == ss2.startPos && ss1 == ss2
end Substring
namespace String

View File

@@ -132,17 +132,13 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
exact Nat.sub_lt_sub_left h (String.lt_next s pos)
macro_rules
| `(tactic| decreasing_trivial) =>
`(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
have h : i.hasNext := decide_eq_true <| Nat.gt_of_not_le <| mt decide_eq_true h
sizeOf_next_lt_of_hasNext i h
macro_rules
| `(tactic| decreasing_trivial) =>
`(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
namespace Iterator
@@ -198,35 +194,4 @@ def removeLeadingSpaces (s : String) : String :=
let n := findLeadingSpacesSize s
if n == 0 then s else removeNumLeadingSpaces n s
/--
Replaces each `\r\n` with `\n` to normalize line endings,
but does not validate that there are no isolated `\r` characters.
It is an optimized version of `String.replace text "\r\n" "\n"`.
-/
def crlfToLf (text : String) : String :=
go "" 0 0
where
go (acc : String) (accStop pos : String.Pos) : String :=
if h : text.atEnd pos then
-- note: if accStop = 0 then acc is empty
if accStop = 0 then text else acc ++ text.extract accStop pos
else
let c := text.get' pos h
let pos' := text.next' pos h
if h' : ¬ text.atEnd pos' c == '\r' text.get pos' == '\n' then
let acc := acc ++ text.extract accStop pos
go acc pos' (text.next' pos' h'.1)
else
go acc accStop pos'
termination_by text.utf8ByteSize - pos.byteIdx
decreasing_by
decreasing_with
show text.utf8ByteSize - (text.next' (text.next' pos _) _).byteIdx < text.utf8ByteSize - pos.byteIdx
have k := Nat.gt_of_not_le <| mt decide_eq_true h
exact Nat.sub_lt_sub_left k (Nat.lt_trans (String.lt_next text pos) (String.lt_next _ _))
decreasing_with
show text.utf8ByteSize - (text.next' pos _).byteIdx < text.utf8ByteSize - pos.byteIdx
have k := Nat.gt_of_not_le <| mt decide_eq_true h
exact Nat.sub_lt_sub_left k (String.lt_next _ _)
end String

View File

@@ -1,21 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Data.Char.Lemmas
namespace String
protected theorem data_eq_of_eq {a b : String} (h : a = b) : a.data = b.data :=
h rfl
protected theorem ne_of_data_ne {a b : String} (h : a.data b.data) : a b :=
fun h' => absurd (String.data_eq_of_eq h') h
@[simp] protected theorem lt_irrefl (s : String) : ¬ s < s :=
List.lt_irrefl' Char.lt_irrefl s.data
protected theorem ne_of_lt {a b : String} (h : a < b) : a b := by
have := String.lt_irrefl a
intro h; subst h; contradiction
end String

View File

@@ -6,4 +6,3 @@ Authors: Henrik Böving
prelude
import Init.Data.UInt.Basic
import Init.Data.UInt.Log2
import Init.Data.UInt.Lemmas

View File

@@ -364,3 +364,6 @@ instance (a b : USize) : Decidable (a < b) := USize.decLt a b
instance (a b : USize) : Decidable (a b) := USize.decLe a b
instance : Max USize := maxOfLe
instance : Min USize := minOfLe
theorem USize.modn_lt {m : Nat} : (u : USize), m > 0 USize.toNat (u % m) < m
| u, h => Fin.modn_lt u h

View File

@@ -1,66 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Data.UInt.Basic
import Init.Data.Fin.Lemmas
set_option hygiene false in
macro "declare_uint_theorems" typeName:ident : command =>
`(
namespace $typeName
instance : Inhabited $typeName where
default := 0
theorem zero_def : (0 : $typeName) = 0 := rfl
theorem one_def : (1 : $typeName) = 1 := rfl
theorem sub_def (a b : $typeName) : a - b = a.val - b.val := rfl
theorem mul_def (a b : $typeName) : a * b = a.val * b.val := rfl
theorem mod_def (a b : $typeName) : a % b = a.val % b.val := rfl
theorem add_def (a b : $typeName) : a + b = a.val + b.val := rfl
@[simp] theorem mk_val_eq : (a : $typeName), mk a.val = a
| _, _ => rfl
theorem val_eq_of_lt {a : Nat} : a < size ((ofNat a).val : Nat) = a :=
Nat.mod_eq_of_lt
theorem le_def {a b : $typeName} : a b a.1 b.1 := .rfl
theorem lt_def {a b : $typeName} : a < b a.1 < b.1 := .rfl
theorem lt_iff_val_lt_val {a b : $typeName} : a < b a.val < b.val := .rfl
@[simp] protected theorem not_le {a b : $typeName} : ¬ a b b < a := Fin.not_le
@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b b a := Fin.not_lt
@[simp] protected theorem le_refl (a : $typeName) : a a := by simp [le_def]
@[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
protected theorem le_trans {a b c : $typeName} : a b b c a c := Fin.le_trans
protected theorem lt_trans {a b c : $typeName} : a < b b < c a < c := Fin.lt_trans
protected theorem le_total (a b : $typeName) : a b b a := Fin.le_total a.1 b.1
protected theorem lt_asymm {a b : $typeName} (h : a < b) : ¬ b < a := Fin.lt_asymm h
protected theorem val_eq_of_eq {a b : $typeName} (h : a = b) : a.val = b.val := h rfl
protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by cases a; cases b; simp at h; simp [h]
open $typeName (val_eq_of_eq) in
protected theorem ne_of_val_ne {a b : $typeName} (h : a.val b.val) : a b := fun h' => absurd (val_eq_of_eq h') h
open $typeName (ne_of_val_ne) in
protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a b := ne_of_val_ne (Fin.ne_of_lt h)
@[simp] protected theorem zero_toNat : (0 : $typeName).toNat = 0 := Nat.zero_mod _
@[simp] protected theorem mod_toNat (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
@[simp] protected theorem div_toNat (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
@[simp] protected theorem modn_toNat (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
protected theorem modn_lt {m : Nat} : (u : $typeName), m > 0 toNat (u % m) < m
| u, h => Fin.modn_lt u h
open $typeName (modn_lt) in
protected theorem mod_lt (a b : $typeName) (h : 0 < b) : a % b < b := modn_lt _ (by simp [lt_def] at h; exact h)
protected theorem toNat.inj : {a b : $typeName}, a.toNat = b.toNat a = b
| _, _, _, _, rfl => rfl
end $typeName
)
declare_uint_theorems UInt8
declare_uint_theorems UInt16
declare_uint_theorems UInt32
declare_uint_theorems UInt64
declare_uint_theorems USize

View File

@@ -1,10 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Grind.Norm
import Init.Grind.Tactics
import Init.Grind.Lemmas
import Init.Grind.Cases

View File

@@ -1,15 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Core
attribute [grind_cases] And Prod False Empty True Unit Exists
namespace Lean.Grind.Eager
attribute [scoped grind_cases] Or
end Lean.Grind.Eager

View File

@@ -1,14 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Core
namespace Lean.Grind
theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' q) : p q :=
fun hp => h (he.mp hp)
end Lean.Grind

View File

@@ -1,110 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.SimpLemmas
import Init.Classical
import Init.ByCases
namespace Lean.Grind
/-!
Normalization theorems for the `grind` tactic.
We are also going to use simproc's in the future.
-/
-- Not
attribute [grind_norm] Classical.not_not
-- Ne
attribute [grind_norm] ne_eq
-- Iff
@[grind_norm] theorem iff_eq (p q : Prop) : (p q) = (p = q) := by
by_cases p <;> by_cases q <;> simp [*]
-- Eq
attribute [grind_norm] eq_self heq_eq_eq
-- Prop equality
@[grind_norm] theorem eq_true_eq (p : Prop) : (p = True) = p := by simp
@[grind_norm] theorem eq_false_eq (p : Prop) : (p = False) = ¬p := by simp
@[grind_norm] theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q) := by
by_cases p <;> by_cases q <;> simp [*]
-- True
attribute [grind_norm] not_true
-- False
attribute [grind_norm] not_false_eq_true
-- Implication as a clause
@[grind_norm] theorem imp_eq (p q : Prop) : (p q) = (¬ p q) := by
by_cases p <;> by_cases q <;> simp [*]
-- And
@[grind_norm] theorem not_and (p q : Prop) : (¬(p q)) = (¬p ¬q) := by
by_cases p <;> by_cases q <;> simp [*]
attribute [grind_norm] and_true true_and and_false false_and and_assoc
-- Or
attribute [grind_norm] not_or
attribute [grind_norm] or_true true_or or_false false_or or_assoc
-- ite
attribute [grind_norm] ite_true ite_false
@[grind_norm] theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
by_cases p <;> simp [*]
-- Forall
@[grind_norm] theorem not_forall (p : α Prop) : (¬ x, p x) = x, ¬p x := by simp
attribute [grind_norm] forall_and
-- Exists
@[grind_norm] theorem not_exists (p : α Prop) : (¬ x, p x) = x, ¬p x := by simp
attribute [grind_norm] exists_const exists_or
-- Bool cond
@[grind_norm] theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
cases c <;> simp [*]
-- Bool or
attribute [grind_norm]
Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true Bool.or_assoc
-- Bool and
attribute [grind_norm]
Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
-- Bool not
attribute [grind_norm]
Bool.not_not
-- beq
attribute [grind_norm] beq_iff_eq
-- bne
attribute [grind_norm] bne_iff_ne
-- Bool not eq true/false
attribute [grind_norm] Bool.not_eq_true Bool.not_eq_false
-- decide
attribute [grind_norm] decide_eq_true_eq decide_not not_decide_eq_true
-- Nat LE
attribute [grind_norm] Nat.le_zero_eq
-- Nat/Int LT
@[grind_norm] theorem Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 b) := by
simp [Nat.lt, LT.lt]
@[grind_norm] theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 b) := by
simp [Int.lt, LT.lt]
-- GT GE
attribute [grind_norm] GT.gt GE.ge
end Lean.Grind

View File

@@ -1,25 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Tactics
namespace Lean.Grind
/--
The configuration for `grind`.
Passed to `grind` using, for example, the `grind (config := { eager := true })` syntax.
-/
structure Config where
/--
When `eager` is true (default: `false`), `grind` eagerly splits `if-then-else` and `match`
expressions.
-/
eager : Bool := false
deriving Inhabited, BEq
/-!
`grind` tactic and related tactics.
-/
end Lean.Grind

View File

@@ -1057,7 +1057,6 @@ where
else
Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args
termination_by xs.size - i
decreasing_by decreasing_trivial_pre_omega
instance [Quote α `term] : Quote (Array α) `term where
quote := quoteArray

View File

@@ -169,11 +169,6 @@ structure Config where
That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
-/
zetaDelta : Bool := false
/--
When `index` (default : `true`) is `false`, `simp` will only use the root symbol
to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
-/
index : Bool := true
deriving Inhabited, BEq
-- Configuration object for `simp_all`

View File

@@ -296,7 +296,7 @@ macro_rules | `($x - $y) => `(binop% HSub.hSub $x $y)
macro_rules | `($x * $y) => `(binop% HMul.hMul $x $y)
macro_rules | `($x / $y) => `(binop% HDiv.hDiv $x $y)
macro_rules | `($x % $y) => `(binop% HMod.hMod $x $y)
-- exponentiation should be considered a right action (#2854)
-- exponentiation should be considered a right action (#2220)
macro_rules | `($x ^ $y) => `(rightact% HPow.hPow $x $y)
macro_rules | `($x ++ $y) => `(binop% HAppend.hAppend $x $y)
macro_rules | `(- $x) => `(unop% Neg.neg $x)
@@ -687,27 +687,4 @@ syntax (name := checkSimp) "#check_simp " term "~>" term : command
-/
syntax (name := checkSimpFailure) "#check_simp " term "!~>" : command
/--
The `seal foo` command ensures that the definition of `foo` is sealed, meaning it is marked as `[irreducible]`.
This command is particularly useful in contexts where you want to prevent the reduction of `foo` in proofs.
In terms of functionality, `seal foo` is equivalent to `attribute [local irreducible] foo`.
This attribute specifies that `foo` should be treated as irreducible only within the local scope,
which helps in maintaining the desired abstraction level without affecting global settings.
-/
syntax "seal " (ppSpace ident)+ : command
/--
The `unseal foo` command ensures that the definition of `foo` is unsealed, meaning it is marked as `[semireducible]`, the
default reducibility setting. This command is useful when you need to allow some level of reduction of `foo` in proofs.
Functionally, `unseal foo` is equivalent to `attribute [local semireducible] foo`.
Applying this attribute makes `foo` semireducible only within the local scope.
-/
syntax "unseal " (ppSpace ident)+ : command
macro_rules
| `(seal $fs:ident*) => `(attribute [local irreducible] $fs:ident*)
| `(unseal $fs:ident*) => `(attribute [local semireducible] $fs:ident*)
end Parser

View File

@@ -87,7 +87,6 @@ macro:35 xs:bracketedExplicitBinders " × " b:term:35 : term => expandBrackedBi
macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders ``PSigma xs b
end
namespace Lean
-- first step of a `calc` block
syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
-- enforce indentation of calc steps so we know when to stop parsing them
@@ -137,7 +136,6 @@ syntax (name := calcTactic) "calc" calcSteps : tactic
@[inherit_doc «calc»]
macro tk:"calc" steps:calcSteps : conv =>
`(conv| tactic => calc%$tk $steps)
end Lean
@[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
| `($(_)) => `(())
@@ -363,7 +361,6 @@ macro_rules
| `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
namespace Lean
syntax cdotTk := patternIgnore("· " <|> ". ")
/-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
@@ -371,11 +368,12 @@ syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
/--
Similar to `first`, but succeeds only if one the given tactics solves the current goal.
-/
syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
syntax (name := solve) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
macro_rules
| `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
namespace Lean
/-! # `repeat` and `while` notation -/
inductive Loop where

View File

@@ -68,7 +68,7 @@ abbrev map (f : Int → Int) (xs : Coeffs) : Coeffs := List.map f xs
/-- Shim for `.enum.find?`. -/
abbrev findIdx? (f : Int Bool) (xs : Coeffs) : Option Nat :=
-- List.findIdx? f xs
-- We could avoid `Batteries.Data.List.Basic` by using the less efficient:
-- We could avoid `Std.Data.List.Basic` by using the less efficient:
xs.enum.find? (f ·.2) |>.map (·.1)
/-- Shim for `IntList.bmod`. -/
abbrev bmod (x : Coeffs) (m : Nat) : Coeffs := IntList.bmod x m

View File

@@ -3644,17 +3644,6 @@ def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
| synthetic (pos := pos) .., false => some pos
| _, _ => none
/--
Gets the end position information from a `SourceInfo`, if available.
If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
-/
def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
match info, canonicalOnly with
| original (endPos := endPos) .., _
| synthetic (endPos := endPos) (canonical := true) .., _
| synthetic (endPos := endPos) .., false => some endPos
| _, _ => none
end SourceInfo
/--
@@ -4383,7 +4372,7 @@ def defaultMaxRecDepth := 512
/-- The message to display on stack overflow. -/
def maxRecDepthErrorMessage : String :=
"maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
"maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)"
namespace Syntax

View File

@@ -210,44 +210,8 @@ def sleep (ms : UInt32) : BaseIO Unit :=
/-- Request cooperative cancellation of the task. The task must explicitly call `IO.checkCanceled` to react to the cancellation. -/
@[extern "lean_io_cancel"] opaque cancel : @& Task α BaseIO Unit
/-- The current state of a `Task` in the Lean runtime's task manager. -/
inductive TaskState
/--
The `Task` is waiting to be run.
It can be waiting for dependencies to complete or
sitting in the task manager queue waiting for a thread to run on.
-/
| waiting
/--
The `Task` is actively running on a thread or,
in the case of a `Promise`, waiting for a call to `IO.Promise.resolve`.
-/
| running
/--
The `Task` has finished running and its result is available.
Calling `Task.get` or `IO.wait` on the task will not block.
-/
| finished
deriving Inhabited, Repr, DecidableEq, Ord
instance : LT TaskState := ltOfOrd
instance : LE TaskState := leOfOrd
instance : Min TaskState := minOfLe
instance : Max TaskState := maxOfLe
protected def TaskState.toString : TaskState String
| .waiting => "waiting"
| .running => "running"
| .finished => "finished"
instance : ToString TaskState := TaskState.toString
/-- Returns current state of the `Task` in the Lean runtime's task manager. -/
@[extern "lean_io_get_task_state"] opaque getTaskState : @& Task α BaseIO TaskState
/-- Check if the task has finished execution, at which point calling `Task.get` will return immediately. -/
@[inline] def hasFinished (task : Task α) : BaseIO Bool := do
return ( getTaskState task) matches .finished
@[extern "lean_io_has_finished"] opaque hasFinished : @& Task α BaseIO Bool
/-- Wait for the task to finish, then return its result. -/
@[extern "lean_io_wait"] opaque wait (t : Task α) : BaseIO α :=
@@ -264,13 +228,6 @@ local macro "nonempty_list" : tactic =>
/-- Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread. -/
@[extern "lean_io_get_num_heartbeats"] opaque getNumHeartbeats : BaseIO Nat
/--
Adjusts the heartbeat counter of the current thread by the given amount. This can be useful to give
allocation-avoiding code additional "weight" and is also used to adjust the counter after resuming
from a snapshot.
-/
@[extern "lean_io_add_heartbeats"] opaque addHeartbeats (count : UInt64) : BaseIO Unit
/--
The mode of a file handle (i.e., a set of `open` flags and an `fdopen` mode).
@@ -668,13 +625,7 @@ partial def FS.removeDirAll (p : FilePath) : IO Unit := do
namespace Process
/-- Returns the current working directory of the calling process. -/
@[extern "lean_io_process_get_current_dir"] opaque getCurrentDir : IO FilePath
/-- Sets the current working directory of the calling process. -/
@[extern "lean_io_process_set_current_dir"] opaque setCurrentDir (path : @& FilePath) : IO Unit
/-- Returns the process ID of the calling process. -/
/-- Returns the process ID of the current process. -/
@[extern "lean_io_process_get_pid"] opaque getPID : BaseIO UInt32
inductive Stdio where
@@ -793,32 +744,6 @@ instance : MonadLift (ST IO.RealWorld) BaseIO := ⟨id⟩
def mkRef (a : α) : BaseIO (IO.Ref α) :=
ST.mkRef a
/--
Mutable cell that can be passed around for purposes of cooperative task cancellation: request
cancellation with `CancelToken.set` and check for it with `CancelToken.isSet`.
This is a more flexible alternative to `Task.cancel` as the token can be shared between multiple
tasks.
-/
structure CancelToken where
private ref : IO.Ref Bool
namespace CancelToken
/-- Creates a new cancellation token. -/
def new : BaseIO CancelToken :=
CancelToken.mk <$> IO.mkRef false
/-- Activates a cancellation token. Idempotent. -/
def set (tk : CancelToken) : BaseIO Unit :=
tk.ref.set true
/-- Checks whether the cancellation token has been activated. -/
def isSet (tk : CancelToken) : BaseIO Bool :=
tk.ref.get
end CancelToken
namespace FS
namespace Stream

View File

@@ -368,7 +368,7 @@ for new reflexive relations.
Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
reflexivity theorems (e.g., `Iff.rfl`).
-/
macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
@@ -835,8 +835,7 @@ syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : tactic
/--
`repeat tac` repeatedly applies `tac` to the main goal until it fails.
That is, if `tac` produces multiple subgoals, only subgoals up to the first failure will be visited.
See also the tactic `repeat'` which repeats separately in each subgoal.
The `Std` library provides `repeat'` which repeats separately in each subgoal.
-/
syntax "repeat " tacticSeq : tactic
macro_rules
@@ -1267,7 +1266,7 @@ Optional arguments passed via a configuration argument as `solve_by_elim (config
but it is often useful to change to `.reducible`,
so semireducible definitions will not be unfolded when trying to apply a lemma.
See also the doc-comment for `Lean.Meta.Tactic.Backtrack.BacktrackConfig` for the options
See also the doc-comment for `Std.Tactic.BacktrackConfig` for the options
`proc`, `suspend`, and `discharge` which allow further customization of `solve_by_elim`.
Both `apply_assumption` and `apply_rules` are implemented via these hooks.
-/
@@ -1426,16 +1425,6 @@ If there are several with the same priority, it is uses the "most recent one". E
-/
syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
/--
Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
-/
syntax (name := grind_norm) "grind_norm" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
/--
Simplification procedures tagged with the `grind_norm_proc` attribute are used by the `grind` tactic normalizer/pre-processor.
-/
syntax (name := grind_norm_proc) "grind_norm_proc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
/-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"

View File

@@ -25,16 +25,9 @@ syntax "decreasing_trivial" : tactic
macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
/--
Variant of `decreasing_trivial` that does not use `omega`, intended to be used in core modules
before `omega` is available.
-/
syntax "decreasing_trivial_pre_omega" : tactic
macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption) -- i-1 < i if i ≠ 0
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assumption) -- i-1 < i if i ≠ 0
/-- Constructs a proof of decreasing along a well founded relation, by applying
lexicographic order lemmas and using `ts` to solve the base case. If it fails,

View File

@@ -37,4 +37,3 @@ import Lean.Log
import Lean.Linter
import Lean.SubExpr
import Lean.LabelAttribute
import Lean.AddDecl

View File

@@ -1,31 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.CoreM
namespace Lean
def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
let env addDecl env opts decl
compileDecl env opts decl
def addDecl (decl : Declaration) : CoreM Unit := do
profileitM Exception "type checking" ( getOptions) do
withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
if !( MonadLog.hasErrors) && decl.hasSorry then
logWarning "declaration uses 'sorry'"
match ( getEnv).addDecl ( getOptions) decl with
| .ok env => setEnv env
| .error ex => throwKernelException ex
def addAndCompile (decl : Declaration) : CoreM Unit := do
addDecl decl
compileDecl decl
end Lean

View File

@@ -67,11 +67,13 @@ def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do
Helper methods for decoding the parameters of builtin attributes that are defined before `Lean.Parser`.
We have the following ones:
```
@[builtin_attr_parser] def simple := leading_parser ident >> optional (ppSpace >> (priorityParser <|> ident))
@[builtin_attr_parser] def simple := leading_parser ident >> optional ident >> optional priorityParser
/- We can't use `simple` for `class`, `instance`, `export` and `macro` because they are keywords. -/
@[builtin_attr_parser] def «class» := leading_parser "class"
@[builtin_attr_parser] def «instance» := leading_parser "instance" >> optional priorityParser
@[builtin_attr_parser] def «macro» := leading_parser "macro " >> ident
@[builtin_attr_parser] def «export» := leading_parser "export " >> ident
```
Note that we need the parsers for `class`, `instance`, `export` and `macros` because they are keywords.
Note that we need the parsers for `class`, `instance`, and `macros` because they are keywords.
-/
def Attribute.Builtin.ensureNoArgs (stx : Syntax) : AttrM Unit := do

View File

@@ -193,13 +193,12 @@ def foldCharOfNat (beforeErasure : Bool) (a : Expr) : Option Expr := do
else
return mkUInt32Lit 0
def foldToNat (size : Nat) (_ : Bool) (a : Expr) : Option Expr := do
def foldToNat (_ : Bool) (a : Expr) : Option Expr := do
let n getNumLit a
return mkRawNatLit (n % size)
return mkRawNatLit n
def uintFoldToNatFns : List (Name × UnFoldFn) :=
numScalarTypes.foldl (fun r info => (info.toNatFn, foldToNat info.size) :: r) []
numScalarTypes.foldl (fun r info => (info.toNatFn, foldToNat) :: r) []
def unFoldFns : List (Name × UnFoldFn) :=
[(``Nat.succ, foldNatSucc),

View File

@@ -66,13 +66,12 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
descr := "builtin and foreign functions"
getParam := fun _ stx => syntaxToExternAttrData stx
afterSet := fun declName _ => do
let env getEnv
if env.isProjectionFn declName || env.isConstructor declName then
if let some (.thmInfo ..) := env.find? declName then
-- We should not mark theorems as extern
return ()
let env ofExcept <| addExtern env declName
let mut env getEnv
if env.isProjectionFn declName || env.isConstructor declName then do
env ofExcept <| addExtern env declName
setEnv env
else
pure ()
}
@[export lean_get_extern_attr_data]

View File

@@ -9,10 +9,9 @@ import Lean.Compiler.IR.CompilerM
import Lean.Compiler.IR.LiveVars
namespace Lean.IR.ExplicitRC
/-!
Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
This transformation is applied before lower level optimizations
that introduce the instructions `release` and `set`
/-! Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
This transformation is applied before lower level optimizations
that introduce the instructions `release` and `set`
-/
structure VarInfo where

View File

@@ -9,238 +9,152 @@ import Lean.Compiler.IR.LiveVars
import Lean.Compiler.IR.Format
namespace Lean.IR.ResetReuse
/-!
Remark: the insertResetReuse transformation is applied before we have
inserted `inc/dec` instructions, and performed lower level optimizations
that introduce the instructions `release` and `set`.
/-! Remark: the insertResetReuse transformation is applied before we have
inserted `inc/dec` instructions, and performed lower level optimizations
that introduce the instructions `release` and `set`. -/
/-! Remark: the functions `S`, `D` and `R` defined here implement the
corresponding functions in the paper "Counting Immutable Beans"
Here are the main differences:
- We use the State monad to manage the generation of fresh variable names.
- Support for join points, and `uset` and `sset` instructions for unboxed data.
- `D` uses the auxiliary function `Dmain`.
- `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
the last occurrence of the variable `x`.
- Because we have join points in the actual implementation, a variable may be live even if it
does not occur in a function body. See example at `livevars.lean`.
-/
/-!
Remark: the functions `S`, `D` and `R` defined here implement the
corresponding functions in the paper "Counting Immutable Beans"
Here are the main differences:
- We use the State monad to manage the generation of fresh variable names.
- Support for join points, and `uset` and `sset` instructions for unboxed data.
- `D` uses the auxiliary function `Dmain`.
- `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
the last occurrence of the variable `x`.
- Because we have join points in the actual implementation, a variable may be live even if it
does not occur in a function body. See example at `livevars.lean`.
-/
private def mayReuse (c₁ c₂ : CtorInfo) (relaxedReuse : Bool) : Bool :=
private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
c₁.size == c₂.size && c₁.usize == c₂.usize && c₁.ssize == c₂.ssize &&
/- The following condition is a heuristic.
If `relaxedReuse := false`, then we don't want to reuse cells from
different constructors even when they are compatible
We don't want to reuse cells from different types even when they are compatible
because it produces counterintuitive behavior. -/
(relaxedReuse || c₁.name.getPrefix == c₂.name.getPrefix)
c₁.name.getPrefix == c₂.name.getPrefix
/--
Replace `ctor` applications with `reuse` applications if compatible.
`w` contains the "memory cell" being reused.
-/
private partial def S (w : VarId) (c : CtorInfo) (relaxedReuse : Bool) (b : FnBody) : FnBody :=
go b
where
go : FnBody FnBody
| .vdecl x t v@(.ctor c' ys) b =>
if mayReuse c c' relaxedReuse then
private partial def S (w : VarId) (c : CtorInfo) : FnBody FnBody
| FnBody.vdecl x t v@(Expr.ctor c' ys) b =>
if mayReuse c c' then
let updtCidx := c.cidx != c'.cidx
.vdecl x t (.reuse w c' updtCidx ys) b
FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b
else
.vdecl x t v (go b)
| .jdecl j ys v b =>
let v' := go v
if v == v' then
.jdecl j ys v (go b)
else
.jdecl j ys v' b
| .case tid x xType alts =>
.case tid x xType <| alts.map fun alt => alt.modifyBody go
FnBody.vdecl x t v (S w c b)
| FnBody.jdecl j ys v b =>
let v' := S w c v
if v == v' then FnBody.jdecl j ys v (S w c b)
else FnBody.jdecl j ys v' b
| FnBody.case tid x xType alts => FnBody.case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
| b =>
if b.isTerminal then
b
else
let (instr, b) := b.split
instr.setBody (go b)
structure Context where
lctx : LocalContext := {}
/--
Contains all variables in `cases` statements in the current path
and variables that are already in `reset` statements when we
invoke `R`.
We use this information to prevent double-reset in code such as
```
case x_i : obj of
Prod.mk →
case x_i : obj of
Prod.mk →
...
```
A variable can already be in a `reset` statement when we
invoke `R` because we execute it with and without `relaxedReuse`.
-/
alreadyFound : PHashSet VarId := {}
/--
If `relaxedReuse := true`, then allow memory cells from different
constructors to be reused. For example, we can reuse a `PSigma.mk`
to allocate a `Prod.mk`. To avoid counterintuitive behavior,
we first try `relaxedReuse := false`, and then `relaxedReuse := true`.
-/
relaxedReuse : Bool := false
if b.isTerminal then b
else let
(instr, b) := b.split
instr.setBody (S w c b)
/-- We use `Context` to track join points in scope. -/
abbrev M := ReaderT Context (StateT Index Id)
abbrev M := ReaderT LocalContext (StateT Index Id)
private def mkFresh : M VarId := do
let idx getModify fun n => n + 1
return { idx := idx }
let idx getModify (fun n => n + 1)
pure { idx := idx }
/--
Helper function for applying `S`. We only introduce a `reset` if we managed
to replace a `ctor` withe `reuse` in `b`.
-/
private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
let w mkFresh
let b' := S w c ( read).relaxedReuse b
if b == b' then
return b
else
return .vdecl w IRType.object (.reset c.size x) b'
let b' := S w c b
if b == b' then pure b
else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b'
private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool M FnBody
| (b, true) => return b
| (b, true) => pure b
| (b, false) => tryS x c b
private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
ys.any fun arg => match arg with
| .var y => x == y
| _ => false
| Arg.var y => x == y
| _ => false
private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
match b with
| .vdecl _ _ (.ctor _ ys) _ => argsContainsVar ys x
| (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
| _ => false
/--
Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
and `flag == true` if `x` is live in `b`.
/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
and `flag == true` if `x` is live in `b`.
Note that, in the function `D` defined in the paper, for each `let x := e; F`,
`D` checks whether `x` is live in `F` or not. This is great for clarity but it
is expensive: `O(n^2)` where `n` is the size of the function body. -/
private partial def Dmain (x : VarId) (c : CtorInfo) (e : FnBody) : M (FnBody × Bool) := do
match e with
| .case tid y yType alts =>
if e.hasLiveVar ( read).lctx x then
Note that, in the function `D` defined in the paper, for each `let x := e; F`,
`D` checks whether `x` is live in `F` or not. This is great for clarity but it
is expensive: `O(n^2)` where `n` is the size of the function body. -/
private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody M (FnBody × Bool)
| e@(FnBody.case tid y yType alts) => do
let ctx read
if e.hasLiveVar ctx x then do
/- If `x` is live in `e`, we recursively process each branch. -/
let alts alts.mapM fun alt => alt.mmodifyBody fun b => Dmain x c b >>= Dfinalize x c
return (.case tid y yType alts, true)
else
return (e, false)
| .jdecl j ys v b =>
let (b, found) withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (Dmain x c b)
pure (FnBody.case tid y yType alts, true)
else pure (e, false)
| FnBody.jdecl j ys v b => do
let (b, found) withReader (fun ctx => ctx.addJP j ys v) (Dmain x c b)
let (v, _ /- found' -/) Dmain x c v
/- If `found' == true`, then `Dmain b` must also have returned `(b, true)` since
we assume the IR does not have dead join points. So, if `x` is live in `j` (i.e., `v`),
then it must also live in `b` since `j` is reachable from `b` with a `jmp`.
On the other hand, `x` may be live in `b` but dead in `j` (i.e., `v`). -/
return (.jdecl j ys v b, found)
| e =>
pure (FnBody.jdecl j ys v b, found)
| e => do
let ctx read
if e.isTerminal then
return (e, e.hasLiveVar ( read).lctx x)
pure (e, e.hasLiveVar ctx x)
else do
let (instr, b) := e.split
if isCtorUsing instr x then
/- If the scrutinee `x` (the one that is providing memory) is being
stored in a constructor, then reuse will probably not be able to reuse memory at runtime.
It may work only if the new cell is consumed, but we ignore this case. -/
return (e, true)
pure (e, true)
else
let (b, found) Dmain x c b
/- Remark: it is fine to use `hasFreeVar` instead of `hasLiveVar`
since `instr` is not a `FnBody.jmp` (it is not a terminal) nor
it is a `FnBody.jdecl`. -/
since `instr` is not a `FnBody.jmp` (it is not a terminal) nor it is a `FnBody.jdecl`. -/
if found || !instr.hasFreeVar x then
return (instr.setBody b, found)
pure (instr.setBody b, found)
else
let b tryS x c b
return (instr.setBody b, true)
pure (instr.setBody b, true)
private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
Dmain x c b >>= Dfinalize x c
partial def R (e : FnBody) : M FnBody := do
match e with
| .case tid x xType alts =>
let alreadyFound := ( read).alreadyFound.contains x
withReader (fun ctx => { ctx with alreadyFound := ctx.alreadyFound.insert x }) do
partial def R : FnBody M FnBody
| FnBody.case tid x xType alts => do
let alts alts.mapM fun alt => do
let alt alt.mmodifyBody R
match alt with
| .ctor c b =>
if c.isScalar || alreadyFound then
-- If `alreadyFound`, then we don't try to reuse memory cell to avoid
-- double reset.
return alt
else
.ctor c <$> D x c b
| _ => return alt
return .case tid x xType alts
| .jdecl j ys v b =>
| Alt.ctor c b =>
if c.isScalar then pure alt
else Alt.ctor c <$> D x c b
| _ => pure alt
pure $ FnBody.case tid x xType alts
| FnBody.jdecl j ys v b => do
let v R v
let b withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (R b)
return .jdecl j ys v b
| e =>
if e.isTerminal then
return e
else
let b withReader (fun ctx => ctx.addJP j ys v) (R b)
pure $ FnBody.jdecl j ys v b
| e => do
if e.isTerminal then pure e
else do
let (instr, b) := e.split
let b R b
return instr.setBody b
abbrev N := StateT (PHashSet VarId) Id
partial def collectResets (e : FnBody) : N Unit := do
match e with
| .case _ _ _ alts => alts.forM fun alt => collectResets alt.body
| .jdecl _ _ v b => collectResets v; collectResets b
| .vdecl _ _ (.reset _ x) b => modify fun s => s.insert x; collectResets b
| e => unless e.isTerminal do
let (_, b) := e.split
collectResets b
pure (instr.setBody b)
end ResetReuse
open ResetReuse
def Decl.insertResetReuseCore (d : Decl) (relaxedReuse : Bool) : Decl :=
def Decl.insertResetReuse (d : Decl) : Decl :=
match d with
| .fdecl (body := b) .. =>
| .fdecl (body := b) ..=>
let nextIndex := d.maxIndex + 1
-- First time we execute `insertResetReuseCore`, `relaxedReuse := false`.
let alreadyFound : PHashSet VarId := if relaxedReuse then (collectResets b *> get).run' {} else {}
let bNew := R b { relaxedReuse, alreadyFound } |>.run' nextIndex
let bNew := (R b {}).run' nextIndex
d.updateBody! bNew
| other => other
def Decl.insertResetReuse (d : Decl) : Decl :=
/-
We execute the reset/reuse algorithm twice. The first time, we only reuse memory cells
between identical constructor memory cells. That is, we do not reuse a `PSigma.mk` memory cell
when allocating a `Prod.mk` memory cell, even though they have the same layout. Recall
that the reset/reuse placement algorithm is a heuristic, and the first pass prevents reuses
that are unlikely to be useful at runtime. Then, we run the procedure again,
relaxing this restriction. If there are still opportunities for reuse, we will take advantage of them.
The second pass addresses issue #4089.
-/
d.insertResetReuseCore (relaxedReuse := false)
|>.insertResetReuseCore (relaxedReuse := true)
end Lean.IR

View File

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.AddDecl
import Lean.MonadEnv
import Lean.Elab.InfoTree.Main
namespace Lean
@@ -140,7 +138,7 @@ def setBuiltinInitAttr (env : Environment) (declName : Name) (initFnName : Name
builtinInitAttr.setParam env declName initFnName
def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit := do
let name mkAuxName (`_regBuiltin ++ forDecl) 1
let name := `_regBuiltin ++ forDecl
let type := mkApp (mkConst `IO) (mkConst `Unit)
let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,
safety := DefinitionSafety.safe }

View File

@@ -67,4 +67,9 @@ opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name
def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment :=
compileDecls env opt (Compiler.getDeclNamesForCodeGen decl)
def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment := do
let env addDecl env decl
compileDecl env opt decl
end Environment

View File

@@ -11,30 +11,15 @@ import Lean.Eval
import Lean.ResolveName
import Lean.Elab.InfoTree.Types
import Lean.MonadEnv
import Lean.Elab.Exception
namespace Lean
register_builtin_option diagnostics : Bool := {
defValue := false
group := "diagnostics"
descr := "collect diagnostic information"
}
register_builtin_option diagnostics.threshold : Nat := {
defValue := 20
group := "diagnostics"
descr := "only diagnostic counters above this threshold are reported by the definitional equality"
}
namespace Core
register_builtin_option maxHeartbeats : Nat := {
defValue := 200000
descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
}
def useDiagnosticMsg := s!"use `set_option {diagnostics.name} true` to get diagnostic information"
namespace Core
builtin_initialize registerTraceClass `Kernel
def getMaxHeartbeats (opts : Options) : Nat :=
@@ -82,17 +67,11 @@ structure Context where
maxHeartbeats : Nat := getMaxHeartbeats options
currMacroScope : MacroScope := firstFrontendMacroScope
/--
If `diag := true`, different parts of the system collect diagnostics.
Use the `set_option diag true` to set it to true.
If `catchRuntimeEx = false`, then given `try x catch ex => h ex`,
an runtime exception occurring in `x` is not handled by `h`.
Recall that runtime exceptions are `maxRecDepth` or `maxHeartbeats`.
-/
diag : Bool := false
/-- If set, used to cancel elaboration from outside when results are not needed anymore. -/
cancelTk? : Option IO.CancelToken := none
/--
If set (when `showPartialSyntaxErrors` is not set and parsing failed), suppresses most elaboration
errors; see also `logMessage` below.
-/
suppressElabErrors : Bool := false
catchRuntimeEx : Bool := false
deriving Nonempty
/-- CoreM is a monad for manipulating the Lean environment.
@@ -125,22 +104,7 @@ instance : MonadOptions CoreM where
getOptions := return ( read).options
instance : MonadWithOptions CoreM where
withOptions f x := do
let options := f ( read).options
let diag := diagnostics.get options
if Kernel.isDiagnosticsEnabled ( getEnv) != diag then
modifyEnv fun env => Kernel.enableDiag env diag
withReader
(fun ctx =>
{ ctx with
options
diag
maxRecDepth := maxRecDepth.get options })
x
-- Helper function for ensuring fields that depend on `options` have the correct value.
@[inline] private def withConsistentCtx (x : CoreM α) : CoreM α := do
withOptions id x
withOptions f x := withReader (fun ctx => { ctx with options := f ctx.options }) x
instance : AddMessageContext CoreM where
addMessageContext := addMessageContextPartial
@@ -209,45 +173,16 @@ instance : MonadTrace CoreM where
getTraceState := return ( get).traceState
modifyTraceState f := modify fun s => { s with traceState := f s.traceState }
structure SavedState extends State where
/-- Number of heartbeats passed inside `withRestoreOrSaveFull`, not used otherwise. -/
passedHearbeats : Nat
deriving Nonempty
def saveState : CoreM SavedState := do
let s get
return { toState := s, passedHearbeats := 0 }
/-- Restore backtrackable parts of the state. -/
def restore (b : State) : CoreM Unit :=
modify fun s => { s with env := b.env, messages := b.messages, infoState := b.infoState }
/--
Incremental reuse primitive: if `reusableResult?` is `none`, runs `cont` with an action `save` that
on execution returns the saved monadic state at this point including the heartbeats used by `cont`
so far. If `reusableResult?` on the other hand is `some (a, state)`, restores full `state` including
heartbeats used and returns `a`.
The intention is for steps that support incremental reuse to initially pass `none` as
`reusableResult?` and call `save` as late as possible in `cont`. In a further run, if reuse is
possible, `reusableResult?` should be set to the previous state and result, ensuring that the state
after running `withRestoreOrSaveFull` is identical in both runs. Note however that necessarily this
is only an approximation in the case of heartbeats as heartbeats used by `withRestoreOrSaveFull`, by
the remainder of `cont` after calling `save`, as well as by reuse-handling code such as the one
supplying `reusableResult?` are not accounted for.
Restores full state including sources for unique identifiers. Only intended for incremental reuse
between elaboration runs, not for backtracking within a single run.
-/
@[specialize] def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
(cont : (save : CoreM SavedState) CoreM α) : CoreM α := do
if let some (val, state) := reusableResult? then
set state.toState
IO.addHeartbeats state.passedHearbeats.toUInt64
return val
let startHeartbeats IO.getNumHeartbeats
cont (do
let s get
let stopHeartbeats IO.getNumHeartbeats
return { toState := s, passedHearbeats := stopHeartbeats - startHeartbeats })
/-- Restore backtrackable parts of the state. -/
def SavedState.restore (b : SavedState) : CoreM Unit :=
modify fun s => { s with env := b.env, messages := b.messages, infoState := b.infoState }
def restoreFull (b : State) : CoreM Unit :=
set b
private def mkFreshNameImp (n : Name) : CoreM Name := do
let fresh modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
@@ -257,7 +192,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
mkFreshNameImp n
@[inline] def CoreM.run (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) :=
((withConsistentCtx x) ctx).run s
(x ctx).run s
@[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
Prod.fst <$> x.run ctx s
@@ -271,36 +206,20 @@ def mkFreshUserName (n : Name) : CoreM Name :=
instance [MetaEval α] : MetaEval (CoreM α) where
eval env opts x _ := do
let x : CoreM α := do try x finally printTraces
let (a, s) (withConsistentCtx x).toIO { fileName := "<CoreM>", fileMap := default, options := opts } { env := env }
let (a, s) x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default } { env := env }
MetaEval.eval s.env opts a (hideUnit := true)
-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
builtin_initialize interruptExceptionId : InternalExceptionId registerInternalExceptionId `interrupt
/--
Throws an internal interrupt exception if cancellation has been requested. The exception is not
caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
level of elaboration. In particular, we want to skip producing further incremental snapshots after
the exception has been thrown.
-/
@[inline] def checkInterrupted : CoreM Unit := do
if let some tk := ( read).cancelTk? then
if ( tk.isSet) then
throw <| .internal interruptExceptionId
register_builtin_option debug.moduleNameAtTimeout : Bool := {
defValue := true
group := "debug"
descr := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"
}
if ( IO.checkCanceled) then
-- should never be visible to users!
throw <| Exception.error .missing "elaboration interrupted"
def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
let includeModuleName := debug.moduleNameAtTimeout.get ( getOptions)
let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\n{useDiagnosticMsg}"
let msg := s!"(deterministic) timeout at '{moduleName}', maximum number of heartbeats ({max/1000}) has been reached (use 'set_option {optionName} <num>' to set the limit)"
throw <| Exception.error ( getRef) (MessageData.ofFormat (Std.Format.text msg))
def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
@@ -334,13 +253,11 @@ def getMessageLog : CoreM MessageLog :=
return ( get).messages
/--
Returns the current log and then resets its messages while adjusting `MessageLog.hadErrors`. Used
Returns the current log and then resets its messages but does NOT reset `MessageLog.hadErrors`. Used
for incremental reporting during elaboration of a single command.
-/
def getAndEmptyMessageLog : CoreM MessageLog :=
modifyGet fun s => (s.messages, { s with
messages.unreported := {}
messages.hadErrors := s.messages.hasErrors })
modifyGet fun log => ({ log with msgs := {} }, log)
instance : MonadLog CoreM where
getRef := getRef
@@ -348,12 +265,6 @@ instance : MonadLog CoreM where
getFileName := return ( read).fileName
hasErrors := return ( get).messages.hasErrors
logMessage msg := do
if ( read).suppressElabErrors then
-- discard elaboration errors, except for a few important and unlikely misleading ones, on
-- parse error
unless msg.data.hasTag (· matches `Elab.synthPlaceholder | `Tactic.unsolvedGoals) do
return
let ctx read
let msg := { msg with data := MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data };
modify fun s => { s with messages := s.messages.add msg }
@@ -385,8 +296,7 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
We used a similar hack at `Exception.isMaxRecDepth` -/
def Exception.isMaxHeartbeat (ex : Exception) : Bool :=
match ex with
| Exception.error _ (MessageData.ofFormatWithInfos Std.Format.text msg, _) =>
"(deterministic) timeout".isPrefixOf msg
| Exception.error _ (MessageData.ofFormat (Std.Format.text msg)) => "(deterministic) timeout".isPrefixOf msg
| _ => false
/-- Creates the expression `d → b` -/
@@ -396,6 +306,15 @@ def mkArrow (d b : Expr) : CoreM Expr :=
/-- Iterated `mkArrow`, creates the expression `a₁ → a₂ → … → aₙ → b`. Also see `arrowDomainsN`. -/
def mkArrowN (ds : Array Expr) (e : Expr) : CoreM Expr := ds.foldrM mkArrow e
def addDecl (decl : Declaration) : CoreM Unit := do
profileitM Exception "type checking" ( getOptions) do
withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
if !( MonadLog.hasErrors) && decl.hasSorry then
logWarning "declaration uses 'sorry'"
match ( getEnv).addDecl decl with
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
private def supportedRecursors :=
#[``Empty.rec, ``False.rec, ``Eq.ndrec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]
@@ -449,67 +368,51 @@ def compileDecls (decls : List Name) : CoreM Unit := do
| Except.error ex =>
throwKernelException ex
def getDiag (opts : Options) : Bool :=
diagnostics.get opts
/-- Return `true` if diagnostic information collection is enabled. -/
def isDiagnosticsEnabled : CoreM Bool :=
return ( read).diag
def addAndCompile (decl : Declaration) : CoreM Unit := do
addDecl decl;
compileDecl decl
def ImportM.runCoreM (x : CoreM α) : ImportM α := do
let ctx read
let (a, _) (withOptions (fun _ => ctx.opts) x).toIO { fileName := "<ImportM>", fileMap := default } { env := ctx.env }
let (a, _) x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
return a
/-- Return `true` if the exception was generated by one of our resource limits. -/
/-- Return `true` if the exception was generated by one our resource limits. -/
def Exception.isRuntime (ex : Exception) : Bool :=
ex.isMaxHeartbeat || ex.isMaxRecDepth
/-- Returns `true` if the exception is an interrupt generated by `checkInterrupted`. -/
def Exception.isInterrupt : Exception Bool
| Exception.internal id _ => id == Core.interruptExceptionId
| _ => false
/--
Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
exceptions" these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as
`MonadAlwaysExcept`. Also, we never want to catch interrupt exceptions inside the elaborator.
Custom `try-catch` for all monads based on `CoreM`. We don't want to catch "runtime exceptions"
in these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as `MonadAlwayExcept`.
-/
@[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception CoreM α) : CoreM α := do
try
x
catch ex =>
if ex.isInterrupt || ex.isRuntime then
throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
if ex.isRuntime && !( read).catchRuntimeEx then
throw ex
else
h ex
@[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception CoreM α) : CoreM α := do
try
x
catch ex =>
h ex
instance : MonadExceptOf Exception CoreM where
throw := throw
tryCatch := Core.tryCatch
class MonadRuntimeException (m : Type Type) where
tryCatchRuntimeEx (body : m α) (handler : Exception m α) : m α
export MonadRuntimeException (tryCatchRuntimeEx)
instance : MonadRuntimeException CoreM where
tryCatchRuntimeEx := Core.tryCatchRuntimeEx
@[inline] instance [MonadRuntimeException m] : MonadRuntimeException (ReaderT ρ m) where
tryCatchRuntimeEx := fun x c r => tryCatchRuntimeEx (x r) (fun e => (c e) r)
@[inline] instance [MonadRuntimeException m] : MonadRuntimeException (StateRefT' ω σ m) where
tryCatchRuntimeEx := fun x c s => tryCatchRuntimeEx (x s) (fun e => c e s)
@[inline] def Core.withCatchingRuntimeEx (flag : Bool) (x : CoreM α) : CoreM α :=
withReader (fun ctx => { ctx with catchRuntimeEx := flag }) x
@[inline] def mapCoreM [MonadControlT CoreM m] [Monad m] (f : forall {α}, CoreM α CoreM α) {α} (x : m α) : m α :=
controlAt CoreM fun runInBase => f <| runInBase x
/--
Execute `x` with `catchRuntimeEx = flag`. That is, given `try x catch ex => h ex`,
if `x` throws a runtime exception, the handler `h` will be invoked if `flag = true`
Recall that
-/
@[inline] def withCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
mapCoreM (Core.withCatchingRuntimeEx true) x
@[inline] def withoutCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
mapCoreM (Core.withCatchingRuntimeEx false) x
end Lean

View File

@@ -92,7 +92,6 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (targ
moveEntries (i+1) source target
else target
termination_by source.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
let bucketsNew : HashMapBucket α β :=
@@ -249,8 +248,6 @@ def toArray (m : HashMap α β) : Array (α × β) :=
def numBuckets (m : HashMap α β) : Nat :=
m.val.buckets.val.size
variable [BEq α] [Hashable α]
/-- Builds a `HashMap` from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences. -/
def ofList (l : List (α × β)) : HashMap α β :=
l.foldl (init := HashMap.empty) (fun m p => m.insert p.fst p.snd)
@@ -262,7 +259,6 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
match m.find? p.fst with
| none => m.insert p.fst p.snd
| some v => m.insert p.fst $ f v p.snd)
end Lean.HashMap
/--

View File

@@ -84,7 +84,6 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : Has
else
target
termination_by source.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
let bucketsNew : HashSetBucket α :=

View File

@@ -106,7 +106,7 @@ def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
/--
Returns the position of the start of (1-based) line `line`.
This gives the same result as `map.ofPosition ⟨line, 0⟩`, but is more efficient.
This gives the stame result as `map.ofPosition ⟨line, 0⟩`, but is more efficient.
-/
def lineStart (map : FileMap) (line : Nat) : String.Pos :=
if h : line - 1 < map.positions.size then

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