Compare commits

..

4 Commits

Author SHA1 Message Date
Kim Morrison
e095aa340b cleanup test 2024-10-02 14:22:44 +10:00
Kim Morrison
721617d734 feat: Array.unattach 2024-10-02 14:21:26 +10:00
Kim Morrison
532c782e20 ?? 2024-10-02 14:06:34 +10:00
Kim Morrison
683fa8a794 . 2024-10-02 14:06:33 +10:00
793 changed files with 1685 additions and 8663 deletions

View File

@@ -257,7 +257,7 @@ jobs:
"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|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
"CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_libuv\\.lean\""
}
];
console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
@@ -452,7 +452,7 @@ jobs:
run: ccache -s
# This job collects results from all the matrix jobs
# This can be made the "required" job, instead of listing each
# This can be made the required job, instead of listing each
# matrix job separately
all-done:
name: Build matrix complete

View File

@@ -340,7 +340,7 @@ jobs:
# (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
lake update batteries
git add lake-manifest.json
get add lake-manifest.json
git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi

View File

@@ -181,7 +181,7 @@ v4.12.0
* [#4953](https://github.com/leanprover/lean4/pull/4953) defines "and-inverter graphs" (AIGs) as described in section 3 of [Davis-Swords 2013](https://arxiv.org/pdf/1304.7861.pdf).
* **Parsec**
* [#4774](https://github.com/leanprover/lean4/pull/4774) generalizes the `Parsec` library, allowing parsing of iterable data beyond `String` such as `ByteArray`. (See breaking changes.)
* [#4774](https://github.com/leanprover/lean4/pull/4774) generalizes the `Parsec` library, allowing parsing of iterable data beyong `String` such as `ByteArray`. (See breaking changes.)
* [#5115](https://github.com/leanprover/lean4/pull/5115) moves `Lean.Data.Parsec` to `Std.Internal.Parsec` for bootstrappng reasons.
* `Thunk`

View File

@@ -18,14 +18,14 @@ the stdlib.
## Installing dependencies
[The official webpage of MSYS2][msys2] provides one-click installers.
Once installed, you should run the "MSYS2 CLANG64" shell from the start menu (the one that runs `clang64.exe`).
Do not run "MSYS2 MSYS" or "MSYS2 MINGW64" instead!
MSYS2 has a package management system, [pacman][pacman].
Once installed, you should run the "MSYS2 MinGW 64-bit shell" from the start menu (the one that runs `mingw64.exe`).
Do not run "MSYS2 MSYS" instead!
MSYS2 has a package management system, [pacman][pacman], which is used in Arch Linux.
Here are the commands to install all dependencies needed to compile Lean on your machine.
```bash
pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp git unzip diffutils binutils
pacman -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache mingw-w64-x86_64-libuv mingw-w64-x86_64-gmp git unzip diffutils binutils
```
You should now be able to run these commands:
@@ -61,7 +61,8 @@ If you want a version that can run independently of your MSYS install
then you need to copy the following dependent DLL's from where ever
they are installed in your MSYS setup:
- libc++.dll
- libgcc_s_seh-1.dll
- libstdc++-6.dll
- libgmp-10.dll
- libuv-1.dll
- libwinpthread-1.dll
@@ -81,6 +82,6 @@ version clang to your path.
**-bash: gcc: command not found**
Make sure `/clang64/bin` is in your PATH environment. If it is not then
check you launched the MSYS2 CLANG64 shell from the start menu.
(The one that runs `clang64.exe`).
Make sure `/mingw64/bin` is in your PATH environment. If it is not then
check you launched the MSYS2 MinGW 64-bit shell from the start menu.
(The one that runs `mingw64.exe`).

View File

@@ -39,19 +39,7 @@
CTEST_OUTPUT_ON_FAILURE = 1;
} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
GMP = pkgsDist.gmp.override { withStatic = true; };
LIBUV = pkgsDist.libuv.overrideAttrs (attrs: {
configureFlags = ["--enable-static"];
hardeningDisable = [ "stackprotector" ];
# Sync version with CMakeLists.txt
version = "1.48.0";
src = pkgs.fetchFromGitHub {
owner = "libuv";
repo = "libuv";
rev = "v1.48.0";
sha256 = "100nj16fg8922qg4m2hdjh62zv4p32wyrllsvqr659hdhjc03bsk";
};
doCheck = false;
});
LIBUV = pkgsDist.libuv.overrideAttrs (attrs: { configureFlags = ["--enable-static"]; });
GLIBC = pkgsDist.glibc;
GLIBC_DEV = pkgsDist.glibc.dev;
GCC_LIB = pkgsDist.gcc.cc.lib;

View File

@@ -48,8 +48,6 @@ $CP llvm-host/lib/*/lib{c++,c++abi,unwind}.* llvm-host/lib/
$CP -r llvm/include/*-*-* llvm-host/include/
# glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)!
$CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
# libpthread_nonshared.a must be linked in order to be able to use `pthread_atfork(3)`. LibUV uses this function.
$CP $GLIBC/lib/libpthread_nonshared.a stage1/lib/glibc
for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
OPTIONS=()
echo -n " -DLEAN_STANDALONE=ON"
@@ -64,8 +62,8 @@ fi
# use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
# but do not change sysroot so users can still link against system libs
echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -lpthread -ldl -lrt -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
# when not using the above flags, link GMP dynamically/as usual
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -Wl,--no-as-needed'"
# do not set `LEAN_CC` for tests
echo -n " -DLEAN_TEST_VARS=''"

View File

@@ -31,15 +31,15 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
# runtime
(cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1)
# further dependencies
cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
echo -n " -DLEAN_STANDALONE=ON"
echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp -luv -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
# when not using the above flags, link GMP dynamically/as usual
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv -lucrtbase'"
# do not set `LEAN_CC` for tests
echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"
echo -n " -DLEAN_TEST_VARS=''"

View File

@@ -243,56 +243,11 @@ if("${USE_GMP}" MATCHES "ON")
endif()
endif()
# LibUV
if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
# Only on WebAssembly we compile LibUV ourselves
set(LIBUV_EMSCRIPTEN_FLAGS "${EMSCRIPTEN_SETTINGS}")
# LibUV does not compile on WebAssembly without modifications because
# building LibUV on a platform requires including stub implementations
# for features not present on the target platform. This patch includes
# the minimum amount of stub implementations needed for successfully
# running Lean on WebAssembly and using LibUV's temporary file support.
# It still leaves several symbols completely undefined: uv__fs_event_close,
# uv__hrtime, uv__io_check_fd, uv__io_fork, uv__io_poll, uv__platform_invalidate_fd
# uv__platform_loop_delete, uv__platform_loop_init. Making additional
# LibUV features available on WebAssembly might require adapting the
# patch to include additional LibUV source files.
set(LIBUV_PATCH_IN "
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5e8e0166..f3b29134 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -317,6 +317,11 @@ if(CMAKE_SYSTEM_NAME STREQUAL \"GNU\")
src/unix/hurd.c)
endif()
+if(CMAKE_SYSTEM_NAME STREQUAL \"Emscripten\")
+ list(APPEND uv_sources
+ src/unix/no-proctitle.c)
+endif()
+
if(CMAKE_SYSTEM_NAME STREQUAL \"Linux\")
list(APPEND uv_defines _GNU_SOURCE _POSIX_C_SOURCE=200112)
list(APPEND uv_libraries dl rt)
")
string(REPLACE "\n" "\\n" LIBUV_PATCH ${LIBUV_PATCH_IN})
ExternalProject_add(libuv
PREFIX libuv
GIT_REPOSITORY https://github.com/libuv/libuv
# Sync version with flake.nix
GIT_TAG v1.48.0
CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release -DLIBUV_BUILD_TESTS=OFF -DLIBUV_BUILD_SHARED=OFF -DCMAKE_AR=${CMAKE_AR} -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_FLAGS=${LIBUV_EMSCRIPTEN_FLAGS}
PATCH_COMMAND git reset --hard HEAD && printf "${LIBUV_PATCH}" > patch.diff && git apply patch.diff
BUILD_IN_SOURCE ON
INSTALL_COMMAND "")
set(LIBUV_INCLUDE_DIR "${CMAKE_BINARY_DIR}/libuv/src/libuv/include")
set(LIBUV_LIBRARIES "${CMAKE_BINARY_DIR}/libuv/src/libuv/libuv.a")
else()
if(NOT "${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
# LibUV
find_package(LibUV 1.0.0 REQUIRED)
include_directories(${LIBUV_INCLUDE_DIR})
endif()
include_directories(${LIBUV_INCLUDE_DIR})
if(NOT LEAN_STANDALONE)
string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LIBRARIES}")
endif()
@@ -567,10 +522,6 @@ if(${STAGE} GREATER 1)
endif()
else()
add_subdirectory(runtime)
if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
add_dependencies(leanrt libuv)
add_dependencies(leanrt_initial-exec libuv)
endif()
add_subdirectory(util)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:util>)
@@ -611,10 +562,7 @@ if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
# simple. (And we are not interested in `Lake` anyway.) To use dynamic
# linking, we would probably have to set MAIN_MODULE=2 on `leanshared`,
# SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js".
# We set `ERROR_ON_UNDEFINED_SYMBOLS=0` because our build of LibUV does not
# define all symbols, see the comment about LibUV on WebAssembly further up
# in this file.
string(APPEND LEAN_EXE_LINKER_FLAGS " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ERROR_ON_UNDEFINED_SYMBOLS=0")
string(APPEND LEAN_EXE_LINKER_FLAGS " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1")
endif()
# Build the compiler using the bootstrapped C sources for stage0, and use

View File

@@ -1864,8 +1864,7 @@ section
variable {α : Type u}
variable (r : α α Prop)
instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : (a b : α), Decidable (a b)]
: DecidableEq (Quotient s) :=
instance {α : Sort u} {s : Setoid α} [d : (a b : α), Decidable (a b)] : DecidableEq (Quotient s) :=
fun (q₁ q₂ : Quotient s) =>
Quotient.recOnSubsingleton₂ q₁ q₂
fun a₁ a₂ =>

View File

@@ -40,4 +40,3 @@ import Init.Data.ULift
import Init.Data.PLift
import Init.Data.Zero
import Init.Data.NeZero
import Init.Data.Function

View File

@@ -63,29 +63,29 @@ If not, usually the right approach is `simp [Array.unattach, -Array.map_subtype]
-/
def unattach {α : Type _} {p : α Prop} (l : Array { x // p x }) := l.map (·.val)
@[simp] theorem unattach_nil {p : α Prop} : (#[] : Array { x // p x }).unattach = #[] := rfl
@[simp] theorem unattach_push {p : α Prop} {a : { x // p x }} {l : Array { x // p x }} :
@[simp] theorem unattach_nil {α : Type _} {p : α Prop} : (#[] : Array { x // p x }).unattach = #[] := rfl
@[simp] theorem unattach_push {α : Type _} {p : α Prop} {a : { x // p x }} {l : Array { x // p x }} :
(l.push a).unattach = l.unattach.push a.1 := by
simp only [unattach, Array.map_push]
simp [unattach]
@[simp] theorem size_unattach {p : α Prop} {l : Array { x // p x }} :
@[simp] theorem size_unattach {α : Type _} {p : α Prop} {l : Array { x // p x }} :
l.unattach.size = l.size := by
unfold unattach
simp
@[simp] theorem _root_.List.unattach_toArray {p : α Prop} {l : List { x // p x }} :
@[simp] theorem _root_.List.unattach_toArray {α : Type _} {p : α Prop} {l : List { x // p x }} :
l.toArray.unattach = l.unattach.toArray := by
simp only [unattach, List.map_toArray, List.unattach]
simp [unattach, List.unattach]
@[simp] theorem toList_unattach {p : α Prop} {l : Array { x // p x }} :
@[simp] theorem toList_unattach {α : Type _} {p : α Prop} {l : Array { x // p x }} :
l.unattach.toList = l.toList.unattach := by
simp only [unattach, toList_map, List.unattach]
simp [unattach, List.unattach]
@[simp] theorem unattach_attach {l : Array α} : l.attach.unattach = l := by
@[simp] theorem unattach_attach {α : Type _} (l : Array α) : l.attach.unattach = l := by
cases l
simp
@[simp] theorem unattach_attachWith {p : α Prop} {l : Array α}
@[simp] theorem unattach_attachWith {α : Type _} {p : α Prop} {l : Array α}
{H : a l, p a} :
(l.attachWith p H).unattach = l := by
cases l
@@ -161,6 +161,8 @@ and simplifies these to the function directly taking the value.
(l.filter f).unattach = l.unattach.filter g := by
cases l
simp [hf]
rw [List.unattach_filter]
simp [hf]
/-! ### Simp lemmas pushing `unattach` inwards. -/

View File

@@ -11,7 +11,6 @@ import Init.Data.UInt.Basic
import Init.Data.Repr
import Init.Data.ToString.Basic
import Init.GetElem
import Init.Data.List.ToArray
universe u v w
/-! ### Array literal syntax -/
@@ -216,7 +215,7 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
if h : i < a.size then
swapAt a i, h v
else
have : Inhabited (α × Array α) := (v, a)
have : Inhabited α := v
panic! ("index " ++ toString i ++ " out of bounds")
def shrink (a : Array α) (n : Nat) : Array α :=

View File

@@ -582,13 +582,6 @@ theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]?
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 size_swapAt! (a : Array α) (i : Nat) (v : α) :
(a.swapAt! i v).2.size = a.size := by
simp only [swapAt!]
split
· simp
· rfl
@[simp] theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast := by simp [pop]
@[deprecated toList_pop (since := "2024-09-09")]
@@ -1067,7 +1060,7 @@ theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) :
/-! ### flatten -/
@[simp] theorem toList_flatten {l : Array (Array α)} : l.flatten.toList = (l.toList.map toList).flatten := by
@[simp] theorem toList_flatten {l : Array (Array α)} : l.flatten.toList = (l.toList.map toList).join := by
dsimp [flatten]
simp only [foldl_eq_foldl_toList]
generalize l.toList = l
@@ -1078,7 +1071,7 @@ theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) :
| cons h => induction h.toList <;> simp [*]
theorem mem_flatten : {L : Array (Array α)}, a L.flatten l, l L a l := by
simp only [mem_def, toList_flatten, List.mem_flatten, List.mem_map]
simp only [mem_def, toList_flatten, List.mem_join, List.mem_map]
intro l
constructor
· rintro _, s, m, rfl, h
@@ -1574,7 +1567,7 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
l.toArray.filterMap f = (l.filterMap f).toArray := by
simp
@[simp] theorem flatten_toArray (l : List (List α)) : (l.toArray.map List.toArray).flatten = l.flatten.toArray := by
@[simp] theorem flatten_toArray (l : List (List α)) : (l.toArray.map List.toArray).flatten = l.join.toArray := by
apply ext'
simp [Function.comp_def]

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed, Siddharth Bhat
Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed
-/
prelude
import Init.Data.Fin.Basic
@@ -718,8 +718,6 @@ section normalization_eqs
@[simp] theorem add_eq (x y : BitVec w) : BitVec.add x y = x + y := rfl
@[simp] theorem sub_eq (x y : BitVec w) : BitVec.sub x y = x - y := rfl
@[simp] theorem mul_eq (x y : BitVec w) : BitVec.mul x y = x * y := rfl
@[simp] theorem udiv_eq (x y : BitVec w) : BitVec.udiv x y = x / y := rfl
@[simp] theorem umod_eq (x y : BitVec w) : BitVec.umod x y = x % y := rfl
@[simp] theorem zero_eq : BitVec.zero n = 0#n := rfl
end normalization_eqs

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix
-/
prelude
import Init.Data.BitVec.Folds
@@ -18,80 +18,6 @@ as vectors of bits into proofs about Lean `BitVec` values.
The module is named for the bit-blasting operation in an SMT solver that converts bitvector
expressions into expressions about individual bits in each vector.
### Example: How bitblasting works for multiplication
We explain how the lemmas here are used for bitblasting,
by using multiplication as a prototypical example.
Other bitblasters for other operations follow the same pattern.
To bitblast a multiplication of the form `x * y`,
we must unfold the above into a form that the SAT solver understands.
We assume that the solver already knows how to bitblast addition.
This is known to `bv_decide`, by exploiting the lemma `add_eq_adc`,
which says that `x + y : BitVec w` equals `(adc x y false).2`,
where `adc` builds an add-carry circuit in terms of the primitive operations
(bitwise and, bitwise or, bitwise xor) that bv_decide already understands.
In this way, we layer bitblasters on top of each other,
by reducing the multiplication bitblaster to an addition operation.
The core lemma is given by `getLsbD_mul`:
```lean
x y : BitVec w ⊢ (x * y).getLsbD i = (mulRec x y w).getLsbD i
```
Which says that the `i`th bit of `x * y` can be obtained by
evaluating the `i`th bit of `(mulRec x y w)`.
Once again, we assume that `bv_decide` knows how to implement `getLsbD`,
given that `mulRec` can be understood by `bv_decide`.
We write two lemmas to enable `bv_decide` to unfold `(mulRec x y w)`
into a complete circuit, **when `w` is a known constant**`.
This is given by two recurrence lemmas, `mulRec_zero_eq` and `mulRec_succ_eq`,
which are applied repeatedly when the width is `0` and when the width is `w' + 1`:
```lean
mulRec_zero_eq :
mulRec x y 0 =
if y.getLsbD 0 then x else 0
mulRec_succ_eq
mulRec x y (s + 1) =
mulRec x y s +
if y.getLsbD (s + 1) then (x <<< (s + 1)) else 0 := rfl
```
By repeatedly applying the lemmas `mulRec_zero_eq` and `mulRec_succ_eq`,
one obtains a circuit for multiplication.
Note that this circuit uses `BitVec.add`, `BitVec.getLsbD`, `BitVec.shiftLeft`.
Here, `BitVec.add` and `BitVec.shiftLeft` are (recursively) bitblasted by `bv_decide`,
using the lemmas `add_eq_adc` and `shiftLeft_eq_shiftLeftRec`,
and `BitVec.getLsbD` is a primitive that `bv_decide` knows how to reduce to SAT.
The two lemmas, `mulRec_zero_eq`, and `mulRec_succ_eq`,
are used in `Std.Tactic.BVDecide.BVExpr.bitblast.blastMul`
to prove the correctness of the circuit that is built by `bv_decide`.
```lean
def blastMul (aig : AIG BVBit) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry BVBit w
theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment) :
...
⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
=
(lhs * rhs).getLsbD idx
```
The definition and theorem above are internal to `bv_decide`,
and use `mulRec_{zero,succ}_eq` to prove that the circuit built by `bv_decide`
computes the correct value for multiplication.
To zoom out, therefore, we follow two steps:
First, we prove bitvector lemmas to unfold a high-level operation (such as multiplication)
into already bitblastable operations (such as addition and left shift).
We then use these lemmas to prove the correctness of the circuit that `bv_decide` builds.
We use this workflow to implement bitblasting for all SMT-LIB2 operations.
## Main results
* `x + y : BitVec w` is `(adc x y false).2`.
@@ -571,7 +497,7 @@ then `n.udiv d = q`. -/
theorem udiv_eq_of_mul_add_toNat {d n q r : BitVec w} (hd : 0 < d)
(hrd : r < d)
(hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) :
n / d = q := by
n.udiv d = q := by
apply BitVec.eq_of_toNat_eq
rw [toNat_udiv]
replace hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat := by
@@ -587,7 +513,7 @@ theorem udiv_eq_of_mul_add_toNat {d n q r : BitVec w} (hd : 0 < d)
then `n.umod d = r`. -/
theorem umod_eq_of_mul_add_toNat {d n q r : BitVec w} (hrd : r < d)
(hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) :
n % d = r := by
n.umod d = r := by
apply BitVec.eq_of_toNat_eq
rw [toNat_umod]
replace hdqnr : (d.toNat * q.toNat + r.toNat) % d.toNat = n.toNat % d.toNat := by
@@ -688,7 +614,7 @@ quotient has been correctly computed.
theorem DivModState.udiv_eq_of_lawful {n d : BitVec w} {qr : DivModState w}
(h_lawful : DivModState.Lawful {n, d} qr)
(h_final : qr.wn = 0) :
n / d = qr.q := by
n.udiv d = qr.q := by
apply udiv_eq_of_mul_add_toNat h_lawful.hdPos h_lawful.hrLtDivisor
have hdiv := h_lawful.hdiv
simp only [h_final] at *
@@ -701,7 +627,7 @@ remainder has been correctly computed.
theorem DivModState.umod_eq_of_lawful {qr : DivModState w}
(h : DivModState.Lawful {n, d} qr)
(h_final : qr.wn = 0) :
n % d = qr.r := by
n.umod d = qr.r := by
apply umod_eq_of_mul_add_toNat h.hrLtDivisor
have hdiv := h.hdiv
simp only [shiftRight_zero] at hdiv
@@ -767,7 +693,7 @@ theorem DivModState.toNat_shiftRight_sub_one_eq
omega
/--
This is used when proving the correctness of the division algorithm,
This is used when proving the correctness of the divison algorithm,
where we know that `r < d`.
We then want to show that `((r.shiftConcat b) - d) < d` as the loop invariant.
In arithmetic, this is the same as showing that
@@ -875,7 +801,7 @@ theorem wn_divRec (args : DivModArgs w) (qr : DivModState w) :
/-- The result of `udiv` agrees with the result of the division recurrence. -/
theorem udiv_eq_divRec (hd : 0#w < d) :
let out := divRec w {n, d} (DivModState.init w)
n / d = out.q := by
n.udiv d = out.q := by
have := DivModState.lawful_init {n, d} hd
have := lawful_divRec this
apply DivModState.udiv_eq_of_lawful this (wn_divRec ..)
@@ -883,7 +809,7 @@ theorem udiv_eq_divRec (hd : 0#w < d) :
/-- The result of `umod` agrees with the result of the division recurrence. -/
theorem umod_eq_divRec (hd : 0#w < d) :
let out := divRec w {n, d} (DivModState.init w)
n % d = out.r := by
n.umod d = out.r := by
have := DivModState.lawful_init {n, d} hd
have := lawful_divRec this
apply DivModState.umod_eq_of_lawful this (wn_divRec ..)

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, Alex Keizer, Abdalrhman M Mohamed, Siddharth Bhat
Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed,
-/
prelude
@@ -219,25 +219,9 @@ theorem getMsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getMsbD i = false
theorem msb_of_zero_length (h : w = 0) (x : BitVec w) : x.msb = false := by
subst h; simp [msb_zero_length]
theorem ofFin_ofNat (n : Nat) :
ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
simp only [OfNat.ofNat, Fin.ofNat', BitVec.ofNat, Nat.and_pow_two_sub_one_eq_mod]
theorem eq_of_toFin_eq : {x y : BitVec w}, x.toFin = y.toFin x = y
| _, _, _, _, rfl => rfl
theorem toFin_inj {x y : BitVec w} : x.toFin = y.toFin x = y := by
apply Iff.intro
case mp =>
exact @eq_of_toFin_eq w x y
case mpr =>
intro h
simp [toFin, h]
theorem toFin_zero : toFin (0 : BitVec w) = 0 := rfl
theorem toFin_one : toFin (1 : BitVec w) = 1 := by
rw [toFin_inj]; simp only [ofNat_eq_ofNat, ofFin_ofNat]
@[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
cases b <;> rfl
@@ -286,19 +270,6 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
@[simp] theorem getMsbD_zero : (0#w).getMsbD i = false := by simp [getMsbD]
@[simp] theorem getLsbD_one : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0)) := by
simp only [getLsbD, toNat_ofNat, Nat.testBit_mod_two_pow]
by_cases h : i = 0
<;> simp [h, Nat.testBit_to_div_mod, Nat.div_eq_of_lt]
@[simp] theorem getElem_one (h : i < w) : (1#w)[i] = decide (i = 0) := by
simp [ getLsbD_eq_getElem, getLsbD_one, h, show 0 < w by omega]
/-- The msb at index `w-1` is the least significant bit, and is true when the width is nonzero. -/
@[simp] theorem getMsbD_one : (1#w).getMsbD i = (decide (i = w - 1) && decide (0 < w)) := by
simp only [getMsbD]
by_cases h : 0 < w <;> by_cases h' : i = w - 1 <;> simp [h, h'] <;> omega
@[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
Nat.mod_eq_of_lt x.isLt
@@ -360,10 +331,6 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
@[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
@[simp] theorem msb_one : (1#w).msb = decide (w = 1) := by
simp [BitVec.msb, getMsbD_one, Bool.decide_and]
omega
theorem msb_eq_getLsbD_last (x : BitVec w) :
x.msb = x.getLsbD (w - 1) := by
simp only [BitVec.msb, getMsbD]
@@ -467,7 +434,7 @@ theorem toInt_inj {x y : BitVec n} : x.toInt = y.toInt ↔ x = y :=
theorem toInt_ne {x y : BitVec n} : x.toInt y.toInt x y := by
rw [Ne, toInt_inj]
@[simp, bv_toNat] theorem toNat_ofInt {n : Nat} (i : Int) :
@[simp] theorem toNat_ofInt {n : Nat} (i : Int) :
(BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by
unfold BitVec.ofInt
simp
@@ -952,21 +919,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
_ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
· simp
@[simp] theorem ofInt_negSucc_eq_not_ofNat {w n : Nat} :
BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by
simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_coe, toNat_eq, toNat_ofNatLt, toNat_not,
toNat_ofNat]
cases h : Int.negSucc n % ((2 ^ w : Nat) : Int)
case ofNat =>
rw [Int.ofNat_eq_coe, Int.negSucc_emod] at h
· dsimp only
omega
· omega
case negSucc a =>
have neg := Int.negSucc_lt_zero a
have _ : 0 Int.negSucc n % ((2 ^ w : Nat) : Int) := Int.emod_nonneg _ (by omega)
omega
@[simp] theorem toFin_not (x : BitVec w) :
(~~~x).toFin = x.toFin.rev := by
apply Fin.val_inj.mp
@@ -1009,15 +961,6 @@ theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
ext i
simp
theorem not_eq_comm {x y : BitVec w} : ~~~ x = y x = ~~~ y := by
constructor
· intro h
rw [ h]
simp
· intro h
rw [h]
simp
@[simp] theorem getMsb_not {x : BitVec w} :
(~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by
simp only [getMsbD]
@@ -1240,28 +1183,6 @@ theorem toNat_ushiftRight_lt (x : BitVec w) (n : Nat) (hn : n ≤ w) :
· apply hn
· apply Nat.pow_pos (by decide)
@[simp]
theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
(x >>> n).getMsbD i = (decide (i < w) && (!decide (i < n) && x.getMsbD (i - n))) := by
simp only [getMsbD, getLsbD_ushiftRight]
by_cases h : i < n
· simp [getLsbD_ge, show w (n + (w - 1 - i)) by omega]
omega
· by_cases h₁ : i < w
· simp only [h, ushiftRight_eq, getLsbD_ushiftRight, show i - n < w by omega]
congr
omega
· simp [h, h₁]
@[simp]
theorem msb_ushiftRight {x : BitVec w} {n : Nat} :
(x >>> n).msb = (!decide (0 < n) && x.msb) := by
induction n
case zero =>
simp
case succ nn ih =>
simp [BitVec.ushiftRight_eq, getMsbD_ushiftRight, BitVec.msb, ih, show nn + 1 > 0 by omega]
/-! ### ushiftRight reductions from BitVec to Nat -/
@[simp]
@@ -1366,8 +1287,7 @@ theorem sshiftRight_or_distrib (x y : BitVec w) (n : Nat) :
<;> simp [*]
/-- The msb after arithmetic shifting right equals the original msb. -/
@[simp]
theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
theorem sshiftRight_msb_eq_msb {n : Nat} {x : BitVec w} :
(x.sshiftRight n).msb = x.msb := by
rw [msb_eq_getLsbD_last, getLsbD_sshiftRight, msb_eq_getLsbD_last]
by_cases hw₀ : w = 0
@@ -1394,7 +1314,7 @@ theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
by_cases h₃ : m + (n + i) < w
· simp [h₃]
omega
· simp [h₃, msb_sshiftRight]
· simp [h₃, sshiftRight_msb_eq_msb]
theorem not_sshiftRight {b : BitVec w} :
~~~b.sshiftRight n = (~~~b).sshiftRight n := by
@@ -1412,55 +1332,98 @@ theorem not_sshiftRight_not {x : BitVec w} {n : Nat} :
~~~((~~~x).sshiftRight n) = x.sshiftRight n := by
simp [not_sshiftRight]
@[simp]
theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by
simp only [getMsbD, BitVec.getLsbD_sshiftRight]
by_cases h : i < w
· simp only [h, decide_True, Bool.true_and]
by_cases h₁ : w w - 1 - i
· simp [h₁]
omega
· simp only [h₁, decide_False, Bool.not_false, Bool.true_and]
by_cases h₂ : i < n
· simp only [h₂, reduceIte, ite_eq_right_iff]
omega
· simp only [show i - n < w by omega, h₂, reduceIte, decide_True, Bool.true_and]
by_cases h₄ : n + (w - 1 - i) < w <;> (simp only [h₄, reduceIte]; congr; omega)
· simp [h]
/-! ### sshiftRight reductions from BitVec to Nat -/
@[simp]
theorem sshiftRight_eq' (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNat := rfl
@[simp]
theorem getLsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
getLsbD (x.sshiftRight' y) i =
(!decide (w i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
simp only [BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
/-! ### udiv -/
@[simp]
theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
(x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by
simp only [BitVec.sshiftRight', getMsbD, BitVec.getLsbD_sshiftRight]
by_cases h : i < w
· simp only [h, decide_True, Bool.true_and]
by_cases h₁ : w w - 1 - i
· simp [h₁]
omega
· simp only [h₁, decide_False, Bool.not_false, Bool.true_and]
by_cases h₂ : i < y.toNat
· simp only [h₂, reduceIte, ite_eq_right_iff]
omega
· simp only [show i - y.toNat < w by omega, h₂, reduceIte, decide_True, Bool.true_and]
by_cases h₄ : y.toNat + (w - 1 - i) < w <;> (simp only [h₄, reduceIte]; congr; omega)
theorem udiv_eq {x y : BitVec n} : x.udiv y = BitVec.ofNat n (x.toNat / y.toNat) := by
have h : x.toNat / y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
simp [udiv, bv_toNat, h, Nat.mod_eq_of_lt]
@[simp, bv_toNat]
theorem toNat_udiv {x y : BitVec n} : (x.udiv y).toNat = x.toNat / y.toNat := by
simp only [udiv_eq]
by_cases h : y = 0
· simp [h]
· rw [toNat_ofNat, Nat.mod_eq_of_lt]
exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
@[simp]
theorem msb_sshiftRight' {x y: BitVec w} :
(x.sshiftRight' y).msb = x.msb := by
simp [BitVec.sshiftRight', BitVec.msb_sshiftRight]
/-! ### umod -/
theorem umod_eq {x y : BitVec n} :
x.umod y = BitVec.ofNat n (x.toNat % y.toNat) := by
have h : x.toNat % y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt
simp [umod, bv_toNat, Nat.mod_eq_of_lt h]
@[simp, bv_toNat]
theorem toNat_umod {x y : BitVec n} :
(x.umod y).toNat = x.toNat % y.toNat := rfl
/-! ### sdiv -/
/-- Equation theorem for `sdiv` in terms of `udiv`. -/
theorem sdiv_eq (x y : BitVec w) : x.sdiv y =
match x.msb, y.msb with
| false, false => udiv x y
| false, true => - (x.udiv (- y))
| true, false => - ((- x).udiv y)
| true, true => (- x).udiv (- y) := by
rw [BitVec.sdiv]
rcases x.msb <;> rcases y.msb <;> simp
@[bv_toNat]
theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat =
match x.msb, y.msb with
| false, false => (udiv x y).toNat
| false, true => (- (x.udiv (- y))).toNat
| true, false => (- ((- x).udiv y)).toNat
| true, true => ((- x).udiv (- y)).toNat := by
simp only [sdiv_eq, toNat_udiv]
by_cases h : x.msb <;> by_cases h' : y.msb <;> simp [h, h']
theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
have hx : x = 0#1 x = 1#1 := by bv_omega
have hy : y = 0#1 y = 1#1 := by bv_omega
rcases hx with rfl | rfl <;>
rcases hy with rfl | rfl <;>
rfl
/-! ### smod -/
/-- Equation theorem for `smod` in terms of `umod`. -/
theorem smod_eq (x y : BitVec w) : x.smod y =
match x.msb, y.msb with
| false, false => x.umod y
| false, true =>
let u := x.umod (- y)
(if u = 0#w then u else u + y)
| true, false =>
let u := umod (- x) y
(if u = 0#w then u else y - u)
| true, true => - ((- x).umod (- y)) := by
rw [BitVec.smod]
rcases x.msb <;> rcases y.msb <;> simp
@[bv_toNat]
theorem toNat_smod {x y : BitVec w} : (x.smod y).toNat =
match x.msb, y.msb with
| false, false => (x.umod y).toNat
| false, true =>
let u := x.umod (- y)
(if u = 0#w then u.toNat else (u + y).toNat)
| true, false =>
let u := (-x).umod y
(if u = 0#w then u.toNat else (y - u).toNat)
| true, true => (- ((- x).umod (- y))).toNat := by
simp only [smod_eq, toNat_umod]
by_cases h : x.msb <;> by_cases h' : y.msb
<;> by_cases h'' : (-x).umod y = 0#w <;> by_cases h''' : x.umod (-y) = 0#w
<;> simp only [h, h', h'', h''']
<;> simp only [umod, toNat_eq, toNat_ofNatLt, toNat_ofNat, Nat.zero_mod] at h'' h'''
<;> simp [h'', h''']
/-! ### signExtend -/
@@ -1677,11 +1640,6 @@ theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
· simp [hi₂]
· simp [Nat.lt_one_iff, hi₂, show 1 + (i.val - 1) = i by omega]
@[simp]
theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
(x <<< n).msb = x.getMsbD n := by
simp [BitVec.msb]
@[deprecated shiftRight_add (since := "2024-06-02")]
theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
(x >>> n) >>> m = x >>> (n + m) := by
@@ -2056,7 +2014,7 @@ 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#w := by
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
@@ -2076,41 +2034,11 @@ theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by
subst h'
simp at h
@[simp]
theorem neg_eq_zero_iff {x : BitVec w} : -x = 0#w x = 0#w := by
constructor
· intro h
have : - (- x) = - 0 := by simp [h]
simpa using this
· intro h
simp [h]
theorem sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b := by
have ha : a = 0 a = 1 := eq_zero_or_eq_one _
have hb : b = 0 b = 1 := eq_zero_or_eq_one _
rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
@[simp]
theorem sub_eq_self {x : BitVec 1} : -x = x := by
have ha : x = 0 x = 1 := eq_zero_or_eq_one _
rcases ha with h | h <;> simp [h]
theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
rcases w with _ | w
· apply Subsingleton.elim
· rw [BitVec.not_eq_comm]
apply BitVec.eq_of_toNat_eq
simp only [BitVec.toNat_neg, BitVec.toNat_not, BitVec.toNat_add, BitVec.toNat_ofNat,
Nat.add_mod_mod]
by_cases hx : x.toNat = 0
· simp [hx]
· rw [show (_ - 1 % _) = _ by rw [Nat.mod_eq_of_lt (by omega)],
show _ + (_ - 1) = (x.toNat - 1) + 2^(w + 1) by omega,
Nat.add_mod_right,
show (x.toNat - 1) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)],
show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
omega
/-! ### abs -/
@[simp, bv_toNat]
@@ -2245,7 +2173,7 @@ protected theorem ne_of_lt {x y : BitVec n} : x < y → x ≠ y := by
simp only [lt_def, ne_eq, toNat_eq]
apply Nat.ne_of_lt
protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y x % y < y := by
protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y x.umod y < y := by
simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod, umod, toNat_ofNatLt]
apply Nat.mod_lt
@@ -2253,191 +2181,6 @@ theorem not_lt_iff_le {x y : BitVec w} : (¬ x < y) ↔ y ≤ x := by
constructor <;>
(intro h; simp only [lt_def, Nat.not_lt, le_def] at h ; omega)
/-! ### udiv -/
theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) := by
have h : x.toNat / y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
rw [ udiv_eq]
simp [udiv, bv_toNat, h, Nat.mod_eq_of_lt]
@[simp, bv_toNat]
theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat := by
rw [udiv_def]
by_cases h : y = 0
· simp [h]
· rw [toNat_ofNat, Nat.mod_eq_of_lt]
exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
@[simp]
theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w := by
simp [bv_toNat]
@[simp]
theorem udiv_zero {x : BitVec n} : x / 0#n = 0#n := by
simp [udiv_def]
@[simp]
theorem udiv_one {x : BitVec w} : x / 1#w = x := by
simp only [udiv_eq, toNat_eq, toNat_udiv, toNat_ofNat]
cases w
· simp [eq_nil x]
· simp
@[simp]
theorem udiv_eq_and {x y : BitVec 1} :
x / y = (x &&& y) := by
have hx : x = 0#1 x = 1#1 := by bv_omega
have hy : y = 0#1 y = 1#1 := by bv_omega
rcases hx with rfl | rfl <;>
rcases hy with rfl | rfl <;>
rfl
@[simp]
theorem udiv_self {x : BitVec w} :
x / x = if x == 0#w then 0#w else 1#w := by
by_cases h : x = 0#w
· simp [h]
· simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h
simp only [udiv_eq, beq_iff_eq, toNat_eq, toNat_ofNat, Nat.zero_mod, h,
reduceIte, toNat_udiv]
rw [Nat.div_self (by omega), Nat.mod_eq_of_lt (by omega)]
/-! ### umod -/
theorem umod_def {x y : BitVec n} :
x % y = BitVec.ofNat n (x.toNat % y.toNat) := by
rw [ umod_eq]
have h : x.toNat % y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt
simp [umod, bv_toNat, Nat.mod_eq_of_lt h]
@[simp, bv_toNat]
theorem toNat_umod {x y : BitVec n} :
(x % y).toNat = x.toNat % y.toNat := rfl
@[simp]
theorem umod_zero {x : BitVec n} : x % 0#n = x := by
simp [umod_def]
@[simp]
theorem zero_umod {x : BitVec w} : (0#w) % x = 0#w := by
simp [bv_toNat]
@[simp]
theorem umod_one {x : BitVec w} : x % (1#w) = 0#w := by
simp only [toNat_eq, toNat_umod, toNat_ofNat, Nat.zero_mod]
cases w
· simp [eq_nil x]
· simp [Nat.mod_one]
@[simp]
theorem umod_self {x : BitVec w} : x % x = 0#w := by
simp [bv_toNat]
@[simp]
theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
have hx : x = 0#1 x = 1#1 := by bv_omega
have hy : y = 0#1 y = 1#1 := by bv_omega
rcases hx with rfl | rfl <;>
rcases hy with rfl | rfl <;>
rfl
/-! ### sdiv -/
/-- Equation theorem for `sdiv` in terms of `udiv`. -/
theorem sdiv_eq (x y : BitVec w) : x.sdiv y =
match x.msb, y.msb with
| false, false => udiv x y
| false, true => - (x.udiv (- y))
| true, false => - ((- x).udiv y)
| true, true => (- x).udiv (- y) := by
rw [BitVec.sdiv]
rcases x.msb <;> rcases y.msb <;> simp
@[bv_toNat]
theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat =
match x.msb, y.msb with
| false, false => (udiv x y).toNat
| false, true => (- (x.udiv (- y))).toNat
| true, false => (- ((- x).udiv y)).toNat
| true, true => ((- x).udiv (- y)).toNat := by
simp only [sdiv_eq, toNat_udiv]
by_cases h : x.msb <;> by_cases h' : y.msb <;> simp [h, h']
@[simp]
theorem zero_sdiv {x : BitVec w} : (0#w).sdiv x = 0#w := by
simp only [sdiv_eq]
rcases x.msb with msb | msb <;> simp
@[simp]
theorem sdiv_zero {x : BitVec n} : x.sdiv 0#n = 0#n := by
simp only [sdiv_eq, msb_zero]
rcases x.msb with msb | msb <;> apply eq_of_toNat_eq <;> simp
@[simp]
theorem sdiv_one {x : BitVec w} : x.sdiv 1#w = x := by
simp only [sdiv_eq]
· by_cases h : w = 1
· subst h
rcases x.msb with msb | msb <;> simp
· rcases x.msb with msb | msb <;> simp [h]
theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
have hx : x = 0#1 x = 1#1 := by bv_omega
have hy : y = 0#1 y = 1#1 := by bv_omega
rcases hx with rfl | rfl <;>
rcases hy with rfl | rfl <;>
rfl
@[simp]
theorem sdiv_self {x : BitVec w} :
x.sdiv x = if x == 0#w then 0#w else 1#w := by
simp [sdiv_eq]
· by_cases h : w = 1
· subst h
rcases x.msb with msb | msb <;> simp
· rcases x.msb with msb | msb <;> simp [h]
/-! ### smod -/
/-- Equation theorem for `smod` in terms of `umod`. -/
theorem smod_eq (x y : BitVec w) : x.smod y =
match x.msb, y.msb with
| false, false => x.umod y
| false, true =>
let u := x.umod (- y)
(if u = 0#w then u else u + y)
| true, false =>
let u := umod (- x) y
(if u = 0#w then u else y - u)
| true, true => - ((- x).umod (- y)) := by
rw [BitVec.smod]
rcases x.msb <;> rcases y.msb <;> simp
@[bv_toNat]
theorem toNat_smod {x y : BitVec w} : (x.smod y).toNat =
match x.msb, y.msb with
| false, false => (x.umod y).toNat
| false, true =>
let u := x.umod (- y)
(if u = 0#w then u.toNat else (u + y).toNat)
| true, false =>
let u := (-x).umod y
(if u = 0#w then u.toNat else (y - u).toNat)
| true, true => (- ((- x).umod (- y))).toNat := by
simp only [smod_eq, toNat_umod]
by_cases h : x.msb <;> by_cases h' : y.msb
<;> by_cases h'' : (-x).umod y = 0#w <;> by_cases h''' : x.umod (-y) = 0#w
<;> simp only [h, h', h'', h''']
<;> simp only [umod, toNat_eq, toNat_ofNatLt, toNat_ofNat, Nat.zero_mod] at h'' h'''
<;> simp [h'', h''']
@[simp]
theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
simp only [smod_eq, msb_zero]
rcases x.msb with msb | msb <;> apply eq_of_toNat_eq
· simp
· by_cases h : x = 0#n <;> simp [h]
/-! ### ofBoolList -/
@[simp] theorem getMsbD_ofBoolListBE : (ofBoolListBE bs).getMsbD i = bs.getD i false := by
@@ -2697,6 +2440,14 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
apply eq_of_toNat_eq
simp
@[simp]
theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
rw [ twoPow_zero, getLsbD_twoPow]
@[simp]
theorem getElem_one {w i : Nat} (h : i < w) : (1#w)[i] = decide (i = 0) := by
rw [ twoPow_zero, getElem_twoPow]
theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
x <<< n = x * (BitVec.twoPow w n) := by
ext i
@@ -2716,6 +2467,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
@[simp] theorem zero_concat_true : concat 0#w true = 1#(w + 1) := by
ext
simp [getLsbD_concat]
omega
/- ### setWidth, setWidth, and bitwise operations -/
@@ -2756,7 +2508,7 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
ext i
simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_ofBool,
Bool.true_and]
by_cases h : ((i : Nat) = 0) <;> simp [h] <;> omega
by_cases h : (0 = (i : Nat)) <;> simp [h] <;> omega
@[simp]
theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by
@@ -2928,31 +2680,6 @@ theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) :
(x * y).toNat = x.toNat * y.toNat := by
rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h]
/--
`x ≤ y + z` if and only if `x - z ≤ y`
when `x - z` and `y + z` do not overflow.
-/
theorem le_add_iff_sub_le {x y z : BitVec w}
(hxz : z x) (hbz : y.toNat + z.toNat < 2^w) :
x y + z x - z y := by
simp_all only [BitVec.le_def]
rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega),
BitVec.toNat_add_of_lt (by omega)]
omega
/--
`x - z ≤ y - z` if and only if `x ≤ y`
when `x - z` and `y - z` do not overflow.
-/
theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z x) (hyz : z y) :
(x - z y - z) x y := by
simp_all only [BitVec.le_def]
rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega),
BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
omega
/-! ### Decidable quantifiers -/
theorem forall_zero_iff {P : BitVec 0 Prop} :
@@ -3157,7 +2884,4 @@ abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true
@[deprecated and_one_eq_setWidth_ofBool_getLsbD (since := "2024-09-18")]
abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLsbD
@[deprecated msb_sshiftRight (since := "2024-10-03")]
abbrev sshiftRight_msb_eq_msb := @msb_sshiftRight
end BitVec

View File

@@ -244,13 +244,9 @@ theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.siz
theorem val_add (a b : Fin n) : (a + b).val = (a.val + b.val) % n := rfl
@[simp] protected theorem zero_add [NeZero n] (k : Fin n) : (0 : Fin n) + k = k := by
@[simp] protected theorem zero_add {n : Nat} [NeZero n] (i : Fin n) : (0 : Fin n) + i = i := by
ext
simp [Fin.add_def, Nat.mod_eq_of_lt k.2]
@[simp] protected theorem add_zero [NeZero n] (k : Fin n) : k + 0 = k := by
ext
simp [add_def, Nat.mod_eq_of_lt k.2]
simp [Fin.add_def, Nat.mod_eq_of_lt i.2]
theorem val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last _) : (i + 1).1 = i + 1 := by
match n with

View File

@@ -1,35 +0,0 @@
/-
Copyright (c) 2024 Lean FRO. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
prelude
import Init.Core
namespace Function
@[inline]
def curry : (α × β φ) α β φ := fun f a b => f (a, b)
/-- Interpret a function with two arguments as a function on `α × β` -/
@[inline]
def uncurry : (α β φ) α × β φ := fun f a => f a.1 a.2
@[simp]
theorem curry_uncurry (f : α β φ) : curry (uncurry f) = f :=
rfl
@[simp]
theorem uncurry_curry (f : α × β φ) : uncurry (curry f) = f :=
funext fun _a, _b => rfl
@[simp]
theorem uncurry_apply_pair {α β γ} (f : α β γ) (x : α) (y : β) : uncurry f (x, y) = f x y :=
rfl
@[simp]
theorem curry_apply {α β γ} (f : α × β γ) (x : α) (y : β) : curry f x y = f (x, y) :=
rfl
end Function

View File

@@ -23,5 +23,3 @@ import Init.Data.List.TakeDrop
import Init.Data.List.Zip
import Init.Data.List.Perm
import Init.Data.List.Sort
import Init.Data.List.ToArray
import Init.Data.List.MapIdx

View File

@@ -568,22 +568,22 @@ If not, usually the right approach is `simp [List.unattach, -List.map_subtype]`
-/
def unattach {α : Type _} {p : α Prop} (l : List { x // p x }) := l.map (·.val)
@[simp] theorem unattach_nil {p : α Prop} : ([] : List { x // p x }).unattach = [] := rfl
@[simp] theorem unattach_cons {p : α Prop} {a : { x // p x }} {l : List { x // p x }} :
@[simp] theorem unattach_nil {α : Type _} {p : α Prop} : ([] : List { x // p x }).unattach = [] := rfl
@[simp] theorem unattach_cons {α : Type _} {p : α Prop} {a : { x // p x }} {l : List { x // p x }} :
(a :: l).unattach = a.val :: l.unattach := rfl
@[simp] theorem length_unattach {p : α Prop} {l : List { x // p x }} :
@[simp] theorem length_unattach {α : Type _} {p : α Prop} {l : List { x // p x }} :
l.unattach.length = l.length := by
unfold unattach
simp
@[simp] theorem unattach_attach {l : List α} : l.attach.unattach = l := by
@[simp] theorem unattach_attach {α : Type _} (l : List α) : l.attach.unattach = l := by
unfold unattach
induction l with
| nil => simp
| cons a l ih => simp [ih, Function.comp_def]
@[simp] theorem unattach_attachWith {p : α Prop} {l : List α}
@[simp] theorem unattach_attachWith {α : Type _} {p : α Prop} {l : List α}
{H : a l, p a} :
(l.attachWith p H).unattach = l := by
unfold unattach
@@ -666,13 +666,11 @@ and simplifies these to the function directly taking the value.
(l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach := by
simp [unattach, -map_subtype]
@[simp] theorem unattach_flatten {p : α Prop} {l : List (List { x // p x })} :
l.flatten.unattach = (l.map unattach).flatten := by
@[simp] theorem unattach_join {p : α Prop} {l : List (List { x // p x })} :
l.join.unattach = (l.map unattach).join := by
unfold unattach
induction l <;> simp_all
@[deprecated unattach_flatten (since := "2024-10-14")] abbrev unattach_join := @unattach_flatten
@[simp] theorem unattach_replicate {p : α Prop} {n : Nat} {x : { x // p x }} :
(List.replicate n x).unattach = List.replicate n x.1 := by
simp [unattach, -map_subtype]

View File

@@ -29,10 +29,9 @@ The operations are organized as follow:
* Lexicographic ordering: `lt`, `le`, and instances.
* Head and tail operators: `head`, `head?`, `headD?`, `tail`, `tail?`, `tailD`.
* Basic operations:
`map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `bind`, `replicate`, and
`map`, `filter`, `filterMap`, `foldr`, `append`, `join`, `pure`, `bind`, `replicate`, and
`reverse`.
* Additional functions defined in terms of these: `leftpad`, `rightPad`, and `reduceOption`.
* Operations using indexes: `mapIdx`.
* List membership: `isEmpty`, `elem`, `contains`, `mem` (and the `∈` notation),
and decidability for predicates quantifying over membership in a `List`.
* Sublists: `take`, `drop`, `takeWhile`, `dropWhile`, `partition`, `dropLast`,
@@ -369,7 +368,7 @@ def tailD (list fallback : List α) : List α :=
/-! ## Basic `List` operations.
We define the basic functional programming operations on `List`:
`map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `bind`, `replicate`, and `reverse`.
`map`, `filter`, `filterMap`, `foldr`, `append`, `join`, `pure`, `bind`, `replicate`, and `reverse`.
-/
/-! ### map -/
@@ -543,20 +542,18 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
simp [reverse, reverseAux]
rw [ reverseAux_eq_append]
/-! ### flatten -/
/-! ### join -/
/--
`O(|flatten L|)`. `join L` concatenates all the lists in `L` into one list.
* `flatten [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
`O(|join L|)`. `join L` concatenates all the lists in `L` into one list.
* `join [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
-/
def flatten : List (List α) List α
def join : List (List α) List α
| [] => []
| a :: as => a ++ flatten as
| a :: as => a ++ join as
@[simp] theorem flatten_nil : List.flatten ([] : List (List α)) = [] := rfl
@[simp] theorem flatten_cons : (l :: ls).flatten = l ++ ls.flatten := rfl
@[deprecated flatten (since := "2024-10-14"), inherit_doc flatten] abbrev join := @flatten
@[simp] theorem join_nil : List.join ([] : List (List α)) = [] := rfl
@[simp] theorem join_cons : (l :: ls).join = l ++ ls.join := rfl
/-! ### pure -/
@@ -570,11 +567,11 @@ def flatten : List (List α) → List α
to get a list of lists, and then concatenates them all together.
* `[2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]`
-/
@[inline] protected def bind {α : Type u} {β : Type v} (a : List α) (b : α List β) : List β := flatten (map b a)
@[inline] protected def bind {α : Type u} {β : Type v} (a : List α) (b : α List β) : List β := join (map b a)
@[simp] theorem bind_nil (f : α List β) : List.bind [] f = [] := by simp [flatten, List.bind]
@[simp] theorem bind_nil (f : α List β) : List.bind [] f = [] := by simp [join, List.bind]
@[simp] theorem bind_cons x xs (f : α List β) :
List.bind (x :: xs) f = f x ++ List.bind xs f := by simp [flatten, List.bind]
List.bind (x :: xs) f = f x ++ List.bind xs f := by simp [join, List.bind]
set_option linter.missingDocs false in
@[deprecated bind_nil (since := "2024-06-15")] abbrev nil_bind := @bind_nil
@@ -1398,17 +1395,8 @@ def unzip : List (α × β) → List α × List β
/-! ## Ranges and enumeration -/
/-- Sum of a list.
`List.sum [a, b, c] = a + (b + (c + 0))` -/
def sum {α} [Add α] [Zero α] : List α α :=
foldr (· + ·) 0
@[simp] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
@[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
/-- Sum of a list of natural numbers. -/
-- We intend to subsequently deprecate this in favor of `List.sum`.
-- This is not in the `List` namespace as later `List.sum` will be defined polymorphically.
protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
@[simp] theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
@@ -1539,7 +1527,7 @@ def intersperse (sep : α) : List α → List α
* `intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c`
-/
def intercalate (sep : List α) (xs : List (List α)) : List α :=
(intersperse sep xs).flatten
join (intersperse sep xs)
/-! ### eraseDups -/

View File

@@ -153,15 +153,13 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
simp only [length_filterMap_eq_countP]
congr
ext a
simp (config := { contextual := true }) [Option.getD_eq_iff, Option.isSome_eq_isSome]
simp (config := { contextual := true }) [Option.getD_eq_iff]
@[simp] theorem countP_flatten (l : List (List α)) :
countP p l.flatten = (l.map (countP p)).sum := by
simp only [countP_eq_length_filter, filter_flatten]
@[simp] theorem countP_join (l : List (List α)) :
countP p l.join = Nat.sum (l.map (countP p)) := by
simp only [countP_eq_length_filter, filter_join]
simp [countP_eq_length_filter']
@[deprecated countP_flatten (since := "2024-10-14")] abbrev countP_join := @countP_flatten
@[simp] theorem countP_reverse (l : List α) : countP p l.reverse = countP p l := by
simp [countP_eq_length_filter, filter_reverse]
@@ -232,10 +230,8 @@ theorem count_singleton (a b : α) : count a [b] = if b == a then 1 else 0 := by
@[simp] theorem count_append (a : α) : l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
countP_append _
theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = (l.map (count a)).sum := by
simp only [count_eq_countP, countP_flatten, count_eq_countP']
@[deprecated count_flatten (since := "2024-10-14")] abbrev count_join := @count_flatten
theorem count_join (a : α) (l : List (List α)) : count a l.join = Nat.sum (l.map (count a)) := by
simp only [count_eq_countP, countP_join, count_eq_countP']
@[simp] theorem count_reverse (a : α) (l : List α) : count a l.reverse = count a l := by
simp only [count_eq_countP, countP_eq_length_filter, filter_reverse, length_reverse]

View File

@@ -132,14 +132,14 @@ theorem findSome?_append {l₁ l₂ : List α} : (l₁ ++ l₂).findSome? f = (l
simp only [cons_append, findSome?]
split <;> simp_all
theorem head_flatten {L : List (List α)} (h : l, l L l []) :
(flatten L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
simp [head_eq_iff_head?_eq_some, head?_flatten]
theorem head_join {L : List (List α)} (h : l, l L l []) :
(join L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
simp [head_eq_iff_head?_eq_some, head?_join]
theorem getLast_flatten {L : List (List α)} (h : l, l L l []) :
(flatten L).getLast (by simpa using h) =
theorem getLast_join {L : List (List α)} (h : l, l L l []) :
(join L).getLast (by simpa using h) =
(L.reverse.findSome? fun l => l.getLast?).get (by simpa using h) := by
simp [getLast_eq_iff_getLast_eq_some, getLast?_flatten]
simp [getLast_eq_iff_getLast_eq_some, getLast?_join]
theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
cases n with
@@ -326,35 +326,35 @@ theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h
simp only [cons_append, find?]
by_cases h : p x <;> simp [h, ih]
@[simp] theorem find?_flatten (xs : List (List α)) (p : α Bool) :
xs.flatten.find? p = xs.findSome? (·.find? p) := by
@[simp] theorem find?_join (xs : List (List α)) (p : α Bool) :
xs.join.find? p = xs.findSome? (·.find? p) := by
induction xs with
| nil => simp
| cons x xs ih =>
simp only [flatten_cons, find?_append, findSome?_cons, ih]
simp only [join_cons, find?_append, findSome?_cons, ih]
split <;> simp [*]
theorem find?_flatten_eq_none {xs : List (List α)} {p : α Bool} :
xs.flatten.find? p = none ys xs, x ys, !p x := by
theorem find?_join_eq_none {xs : List (List α)} {p : α Bool} :
xs.join.find? p = none ys xs, x ys, !p x := by
simp
/--
If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
If `find? p` returns `some a` from `xs.join`, then `p a` holds, and
some list in `xs` contains `a`, and no earlier element of that list satisfies `p`.
Moreover, no earlier list in `xs` has an element satisfying `p`.
-/
theorem find?_flatten_eq_some {xs : List (List α)} {p : α Bool} {a : α} :
xs.flatten.find? p = some a
theorem find?_join_eq_some {xs : List (List α)} {p : α Bool} {a : α} :
xs.join.find? p = some a
p a as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs
( a as, x a, !p x) ( x ys, !p x) := by
rw [find?_eq_some]
constructor
· rintro h, ys, zs, h₁, h₂
refine h, ?_
rw [flatten_eq_append_iff] at h₁
rw [join_eq_append_iff] at h₁
obtain (as, bs, rfl, rfl, h₁ | as, bs, c, cs, ds, rfl, rfl, h₁) := h₁
· replace h₁ := h₁.symm
rw [flatten_eq_cons_iff] at h₁
rw [join_eq_cons_iff] at h₁
obtain bs, cs, ds, rfl, h₁, rfl := h₁
refine as ++ bs, [], cs, ds, by simp, ?_
simp
@@ -371,7 +371,7 @@ theorem find?_flatten_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
· intro x m
simpa using h₂ x (by simpa using .inr m)
· rintro h, as, ys, zs, bs, rfl, h₁, h₂
refine h, as.flatten ++ ys, zs ++ bs.flatten, by simp, ?_
refine h, as.join ++ ys, zs ++ bs.join, by simp, ?_
intro a m
simp at m
obtain l, ml, m | m := m
@@ -786,15 +786,15 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
induction xs with simp
| cons _ _ _ => split <;> simp_all [Option.map_or', Option.map_map]; rfl
theorem findIdx?_flatten {l : List (List α)} {p : α Bool} :
l.flatten.findIdx? p =
theorem findIdx?_join {l : List (List α)} {p : α Bool} :
l.join.findIdx? p =
(l.findIdx? (·.any p)).map
fun i => ((l.take i).map List.length).sum +
fun i => Nat.sum ((l.take i).map List.length) +
(l[i]?.map fun xs => xs.findIdx p).getD 0 := by
induction l with
| nil => simp
| cons xs l ih =>
simp only [flatten, findIdx?_append, map_take, map_cons, findIdx?, any_eq_true, Nat.zero_add,
simp only [join, findIdx?_append, map_take, map_cons, findIdx?, any_eq_true, Nat.zero_add,
findIdx?_succ]
split
· simp only [Option.map_some', take_zero, sum_nil, length_cons, zero_lt_succ,
@@ -976,13 +976,4 @@ theorem IsInfix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂
end lookup
/-! ### Deprecations -/
@[deprecated head_flatten (since := "2024-10-14")] abbrev head_join := @head_flatten
@[deprecated getLast_flatten (since := "2024-10-14")] abbrev getLast_join := @getLast_flatten
@[deprecated find?_flatten (since := "2024-10-14")] abbrev find?_join := @find?_flatten
@[deprecated find?_flatten_eq_none (since := "2024-10-14")] abbrev find?_join_eq_none := @find?_flatten_eq_none
@[deprecated find?_flatten_eq_some (since := "2024-10-14")] abbrev find?_join_eq_some := @find?_flatten_eq_some
@[deprecated findIdx?_flatten (since := "2024-10-14")] abbrev findIdx?_join := @findIdx?_flatten
end List

View File

@@ -109,12 +109,12 @@ The following operations are given `@[csimp]` replacements below:
| x::xs, acc => by simp [bindTR.go, bind, go xs]
exact (go as #[]).symm
/-! ### flatten -/
/-! ### join -/
/-- Tail recursive version of `List.flatten`. -/
@[inline] def flattenTR (l : List (List α)) : List α := bindTR l id
/-- Tail recursive version of `List.join`. -/
@[inline] def joinTR (l : List (List α)) : List α := bindTR l id
@[csimp] theorem flatten_eq_flattenTR : @flatten = @flattenTR := by
@[csimp] theorem join_eq_joinTR : @join = @joinTR := by
funext α l; rw [ List.bind_id, List.bind_eq_bindTR]; rfl
/-! ## Sublists -/
@@ -322,7 +322,7 @@ where
| [_] => simp
| x::y::xs =>
let rec go {acc x} : xs,
intercalateTR.go sep.toArray x xs acc = acc.toList ++ flatten (intersperse sep (x::xs))
intercalateTR.go sep.toArray x xs acc = acc.toList ++ join (intersperse sep (x::xs))
| [] => by simp [intercalateTR.go]
| _::_ => by simp [intercalateTR.go, go]
simp [intersperse, go]

View File

@@ -1343,12 +1343,12 @@ theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
simp
@[simp] theorem head_map (f : α β) (l : List α) (w) :
(map f l).head w = f (l.head (by simpa using w)) := by
head (map f l) w = f (head l (by simpa using w)) := by
cases l
· simp at w
· simp_all
@[simp] theorem head?_map (f : α β) (l : List α) : (map f l).head? = l.head?.map f := by
@[simp] theorem head?_map (f : α β) (l : List α) : head? (map f l) = (head? l).map f := by
cases l <;> rfl
@[simp] theorem map_tail? (f : α β) (l : List α) : (tail? l).map (map f) = tail? (map f l) := by
@@ -2068,97 +2068,106 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∃ L b, l = concat L b
| _, .inl rfl => .inr [], a, rfl
| _, .inr L, b, rfl => .inr a::L, b, rfl
/-! ### flatten -/
/-! ### join -/
@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = (L.map length).sum := by
@[simp] theorem length_join (L : List (List α)) : (join L).length = Nat.sum (L.map length) := by
induction L with
| nil => rfl
| cons =>
simp [flatten, length_append, *]
simp [join, length_append, *]
theorem flatten_singleton (l : List α) : [l].flatten = l := by simp
theorem join_singleton (l : List α) : [l].join = l := by simp
@[simp] theorem mem_flatten : {L : List (List α)}, a L.flatten l, l L a l
@[simp] theorem mem_join : {L : List (List α)}, a L.join l, l L a l
| [] => by simp
| b :: l => by simp [mem_flatten, or_and_right, exists_or]
| b :: l => by simp [mem_join, or_and_right, exists_or]
@[simp] theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] l L, l = [] := by
@[simp] theorem join_eq_nil_iff {L : List (List α)} : L.join = [] l L, l = [] := by
induction L <;> simp_all
theorem flatten_ne_nil_iff {xs : List (List α)} : xs.flatten [] x, x xs x [] := by
@[deprecated join_eq_nil_iff (since := "2024-09-05")] abbrev join_eq_nil := @join_eq_nil_iff
theorem join_ne_nil_iff {xs : List (List α)} : xs.join [] x, x xs x [] := by
simp
theorem exists_of_mem_flatten : a flatten L l, l L a l := mem_flatten.1
@[deprecated join_ne_nil_iff (since := "2024-09-05")] abbrev join_ne_nil := @join_ne_nil_iff
theorem mem_flatten_of_mem (lL : l L) (al : a l) : a flatten L := mem_flatten.2 l, lL, al
theorem exists_of_mem_join : a join L l, l L a l := mem_join.1
theorem forall_mem_flatten {p : α Prop} {L : List (List α)} :
( (x) (_ : x flatten L), p x) (l) (_ : l L) (x) (_ : x l), p x := by
simp only [mem_flatten, forall_exists_index, and_imp]
theorem mem_join_of_mem (lL : l L) (al : a l) : a join L := mem_join.2 l, lL, al
theorem forall_mem_join {p : α Prop} {L : List (List α)} :
( (x) (_ : x join L), p x) (l) (_ : l L) (x) (_ : x l), p x := by
simp only [mem_join, forall_exists_index, and_imp]
constructor <;> (intros; solve_by_elim)
theorem flatten_eq_bind {L : List (List α)} : flatten L = L.bind id := by
theorem join_eq_bind {L : List (List α)} : join L = L.bind id := by
induction L <;> simp [List.bind]
theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun l => l.head? := by
theorem head?_join {L : List (List α)} : (join L).head? = L.findSome? fun l => l.head? := by
induction L with
| nil => rfl
| cons =>
simp only [findSome?_cons]
split <;> simp_all
-- `getLast?_flatten` is proved later, after the `reverse` section.
-- `head_flatten` and `getLast_flatten` are proved in `Init.Data.List.Find`.
-- `getLast?_join` is proved later, after the `reverse` section.
-- `head_join` and `getLast_join` are proved in `Init.Data.List.Find`.
theorem foldl_flatten (f : β α β) (b : β) (L : List (List α)) :
(flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
theorem foldl_join (f : β α β) (b : β) (L : List (List α)) :
(join L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
induction L generalizing b <;> simp_all
theorem foldr_flatten (f : α β β) (b : β) (L : List (List α)) :
(flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
theorem foldr_join (f : α β β) (b : β) (L : List (List α)) :
(join L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
induction L <;> simp_all
@[simp] theorem map_flatten (f : α β) (L : List (List α)) : map f (flatten L) = flatten (map (map f) L) := by
@[simp] theorem map_join (f : α β) (L : List (List α)) : map f (join L) = join (map (map f) L) := by
induction L <;> simp_all
@[simp] theorem filterMap_flatten (f : α Option β) (L : List (List α)) :
filterMap f (flatten L) = flatten (map (filterMap f) L) := by
@[simp] theorem filterMap_join (f : α Option β) (L : List (List α)) :
filterMap f (join L) = join (map (filterMap f) L) := by
induction L <;> simp [*, filterMap_append]
@[simp] theorem filter_flatten (p : α Bool) (L : List (List α)) :
filter p (flatten L) = flatten (map (filter p) L) := by
@[simp] theorem filter_join (p : α Bool) (L : List (List α)) :
filter p (join L) = join (map (filter p) L) := by
induction L <;> simp [*, filter_append]
theorem flatten_filter_not_isEmpty :
{L : List (List α)}, flatten (L.filter fun l => !l.isEmpty) = L.flatten
theorem join_filter_not_isEmpty :
{L : List (List α)}, join (L.filter fun l => !l.isEmpty) = L.join
| [] => rfl
| [] :: L
| (a :: l) :: L => by
simp [flatten_filter_not_isEmpty (L := L)]
simp [join_filter_not_isEmpty (L := L)]
theorem flatten_filter_ne_nil [DecidablePred fun l : List α => l []] {L : List (List α)} :
flatten (L.filter fun l => l []) = L.flatten := by
theorem join_filter_ne_nil [DecidablePred fun l : List α => l []] {L : List (List α)} :
join (L.filter fun l => l []) = L.join := by
simp only [ne_eq, isEmpty_iff, Bool.not_eq_true, Bool.decide_eq_false,
flatten_filter_not_isEmpty]
join_filter_not_isEmpty]
@[simp] theorem flatten_append (L₁ L₂ : List (List α)) : flatten (L₁ ++ L₂) = flatten L₁ ++ flatten L₂ := by
@[deprecated filter_join (since := "2024-08-26")]
theorem join_map_filter (p : α Bool) (l : List (List α)) :
(l.map (filter p)).join = (l.join).filter p := by
rw [filter_join]
@[simp] theorem join_append (L₁ L₂ : List (List α)) : join (L₁ ++ L₂) = join L₁ ++ join L₂ := by
induction L₁ <;> simp_all
theorem flatten_concat (L : List (List α)) (l : List α) : flatten (L ++ [l]) = flatten L ++ l := by
theorem join_concat (L : List (List α)) (l : List α) : join (L ++ [l]) = join L ++ l := by
simp
theorem flatten_flatten {L : List (List (List α))} : flatten (flatten L) = flatten (map flatten L) := by
theorem join_join {L : List (List (List α))} : join (join L) = join (map join L) := by
induction L <;> simp_all
theorem flatten_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
xs.flatten = y :: ys
as bs cs, xs = as ++ (y :: bs) :: cs ( l, l as l = []) ys = bs ++ cs.flatten := by
theorem join_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
xs.join = y :: ys
as bs cs, xs = as ++ (y :: bs) :: cs ( l, l as l = []) ys = bs ++ cs.join := by
constructor
· induction xs with
| nil => simp
| cons x xs ih =>
intro h
simp only [flatten_cons] at h
simp only [join_cons] at h
replace h := h.symm
rw [cons_eq_append_iff] at h
obtain (rfl, h | z) := h
@@ -2169,23 +2178,23 @@ theorem flatten_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
refine [], a', xs, ?_
simp
· rintro as, bs, cs, rfl, h₁, rfl
simp [flatten_eq_nil_iff.mpr h₁]
simp [join_eq_nil_iff.mpr h₁]
theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} :
xs.flatten = ys ++ zs
( as bs, xs = as ++ bs ys = as.flatten zs = bs.flatten)
as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ys = as.flatten ++ bs
zs = c :: cs ++ ds.flatten := by
theorem join_eq_append_iff {xs : List (List α)} {ys zs : List α} :
xs.join = ys ++ zs
( as bs, xs = as ++ bs ys = as.join zs = bs.join)
as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ys = as.join ++ bs
zs = c :: cs ++ ds.join := by
constructor
· induction xs generalizing ys with
| nil =>
simp only [flatten_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const,
simp only [join_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const,
exists_false, or_false, and_imp, List.cons_ne_nil]
rintro rfl rfl
exact [], [], by simp
| cons x xs ih =>
intro h
simp only [flatten_cons] at h
simp only [join_cons] at h
rw [append_eq_append_iff] at h
obtain (ys, rfl, h | c', rfl, h) := h
· obtain (as, bs, rfl, rfl, rfl | as, bs, c, cs, ds, rfl, rfl, rfl) := ih h
@@ -2199,15 +2208,18 @@ theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} :
· simp
· simp
/-- Two lists of sublists are equal iff their flattens coincide, as well as the lengths of the
@[deprecated join_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @join_eq_cons_iff
@[deprecated join_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @join_eq_append_iff
/-- Two lists of sublists are equal iff their joins coincide, as well as the lengths of the
sublists. -/
theorem eq_iff_flatten_eq : {L L' : List (List α)},
L = L' L.flatten = L'.flatten map length L = map length L'
theorem eq_iff_join_eq : {L L' : List (List α)},
L = L' L.join = L'.join map length L = map length L'
| _, [] => by simp_all
| [], x' :: L' => by simp_all
| x :: L, x' :: L' => by
simp
rw [eq_iff_flatten_eq]
rw [eq_iff_join_eq]
constructor
· rintro rfl, h₁, h₂
simp_all
@@ -2217,12 +2229,12 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
/-! ### bind -/
theorem bind_def (l : List α) (f : α List β) : l.bind f = flatten (map f l) := by rfl
theorem bind_def (l : List α) (f : α List β) : l.bind f = join (map f l) := by rfl
@[simp] theorem bind_id (l : List (List α)) : List.bind l id = l.flatten := by simp [bind_def]
@[simp] theorem bind_id (l : List (List α)) : List.bind l id = l.join := by simp [bind_def]
@[simp] theorem mem_bind {f : α List β} {b} {l : List α} : b l.bind f a, a l b f a := by
simp [bind_def, mem_flatten]
simp [bind_def, mem_join]
exact fun _, a, h₁, rfl, h₂ => a, h₁, h₂, fun a, h₁, h₂ => _, a, h₁, rfl, h₂
theorem exists_of_mem_bind {b : β} {l : List α} {f : α List β} :
@@ -2233,7 +2245,7 @@ theorem mem_bind_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a
@[simp]
theorem bind_eq_nil_iff {l : List α} {f : α List β} : List.bind l f = [] x l, f x = [] :=
flatten_eq_nil_iff.trans <| by
join_eq_nil_iff.trans <| by
simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
@[deprecated bind_eq_nil_iff (since := "2024-09-05")] abbrev bind_eq_nil := @bind_eq_nil_iff
@@ -2471,23 +2483,23 @@ theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
(replicate n a).filterMap f = [] := by
simp [filterMap_replicate, h]
@[simp] theorem flatten_replicate_nil : (replicate n ([] : List α)).flatten = [] := by
@[simp] theorem join_replicate_nil : (replicate n ([] : List α)).join = [] := by
induction n <;> simp_all [replicate_succ]
@[simp] theorem flatten_replicate_singleton : (replicate n [a]).flatten = replicate n a := by
@[simp] theorem join_replicate_singleton : (replicate n [a]).join = replicate n a := by
induction n <;> simp_all [replicate_succ]
@[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a := by
@[simp] theorem join_replicate_replicate : (replicate n (replicate m a)).join = replicate (n * m) a := by
induction n with
| zero => simp
| succ n ih =>
simp only [replicate_succ, flatten_cons, ih, append_replicate_replicate, replicate_inj, or_true,
simp only [replicate_succ, join_cons, ih, append_replicate_replicate, replicate_inj, or_true,
and_true, add_one_mul, Nat.add_comm]
theorem bind_replicate {β} (f : α List β) : (replicate n a).bind f = (replicate n (f a)).flatten := by
theorem bind_replicate {β} (f : α List β) : (replicate n a).bind f = (replicate n (f a)).join := by
induction n with
| zero => simp
| succ n ih => simp only [replicate_succ, bind_cons, ih, flatten_cons]
| succ n ih => simp only [replicate_succ, bind_cons, ih, join_cons]
@[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
cases n <;> simp [replicate_succ]
@@ -2662,14 +2674,14 @@ theorem reverse_eq_concat {xs ys : List α} {a : α} :
xs.reverse = ys ++ [a] xs = a :: ys.reverse := by
rw [reverse_eq_iff, reverse_concat]
/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/
theorem reverse_flatten (L : List (List α)) :
L.flatten.reverse = (L.map reverse).reverse.flatten := by
/-- Reversing a join is the same as reversing the order of parts and reversing all parts. -/
theorem reverse_join (L : List (List α)) :
L.join.reverse = (L.map reverse).reverse.join := by
induction L <;> simp_all
/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/
theorem flatten_reverse (L : List (List α)) :
L.reverse.flatten = (L.map reverse).flatten.reverse := by
/-- Joining a reverse is the same as reversing all parts and reversing the joined result. -/
theorem join_reverse (L : List (List α)) :
L.reverse.join = (L.map reverse).join.reverse := by
induction L <;> simp_all
theorem reverse_bind {β} (l : List α) (f : α List β) : (l.bind f).reverse = l.reverse.bind (reverse f) := by
@@ -2789,8 +2801,8 @@ theorem getLast?_bind {L : List α} {f : α → List β} :
rw [head?_bind]
rfl
theorem getLast?_flatten {L : List (List α)} :
(flatten L).getLast? = L.reverse.findSome? fun l => l.getLast? := by
theorem getLast?_join {L : List (List α)} :
(join L).getLast? = L.reverse.findSome? fun l => l.getLast? := by
simp [ bind_id, getLast?_bind]
theorem getLast?_replicate (a : α) (n : Nat) : (replicate n a).getLast? = if n = 0 then none else some a := by
@@ -3290,16 +3302,12 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
| nil => rfl
| cons h t ih => simp_all [Bool.and_assoc]
@[simp] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
@[simp] theorem any_join {l : List (List α)} : l.join.any f = l.any (any · f) := by
induction l <;> simp_all
@[deprecated any_flatten (since := "2024-10-14")] abbrev any_join := @any_flatten
@[simp] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
@[simp] theorem all_join {l : List (List α)} : l.join.all f = l.all (all · f) := by
induction l <;> simp_all
@[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
@[simp] theorem any_bind {l : List α} {f : α List β} :
(l.bind f).any p = l.any fun a => (f a).any p := by
induction l <;> simp_all
@@ -3330,47 +3338,4 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
(l.insert a).all f = (f a && l.all f) := by
simp [all_eq]
/-! ### Deprecations -/
@[deprecated flatten_nil (since := "2024-10-14")] abbrev join_nil := @flatten_nil
@[deprecated flatten_cons (since := "2024-10-14")] abbrev join_cons := @flatten_cons
@[deprecated length_flatten (since := "2024-10-14")] abbrev length_join := @length_flatten
@[deprecated flatten_singleton (since := "2024-10-14")] abbrev join_singleton := @flatten_singleton
@[deprecated mem_flatten (since := "2024-10-14")] abbrev mem_join := @mem_flatten
@[deprecated flatten_eq_nil_iff (since := "2024-09-05")] abbrev join_eq_nil := @flatten_eq_nil_iff
@[deprecated flatten_eq_nil_iff (since := "2024-10-14")] abbrev join_eq_nil_iff := @flatten_eq_nil_iff
@[deprecated flatten_ne_nil_iff (since := "2024-09-05")] abbrev join_ne_nil := @flatten_ne_nil_iff
@[deprecated flatten_ne_nil_iff (since := "2024-10-14")] abbrev join_ne_nil_iff := @flatten_ne_nil_iff
@[deprecated exists_of_mem_flatten (since := "2024-10-14")] abbrev exists_of_mem_join := @exists_of_mem_flatten
@[deprecated mem_flatten_of_mem (since := "2024-10-14")] abbrev mem_join_of_mem := @mem_flatten_of_mem
@[deprecated forall_mem_flatten (since := "2024-10-14")] abbrev forall_mem_join := @forall_mem_flatten
@[deprecated flatten_eq_bind (since := "2024-10-14")] abbrev join_eq_bind := @flatten_eq_bind
@[deprecated head?_flatten (since := "2024-10-14")] abbrev head?_join := @head?_flatten
@[deprecated foldl_flatten (since := "2024-10-14")] abbrev foldl_join := @foldl_flatten
@[deprecated foldr_flatten (since := "2024-10-14")] abbrev foldr_join := @foldr_flatten
@[deprecated map_flatten (since := "2024-10-14")] abbrev map_join := @map_flatten
@[deprecated filterMap_flatten (since := "2024-10-14")] abbrev filterMap_join := @filterMap_flatten
@[deprecated filter_flatten (since := "2024-10-14")] abbrev filter_join := @filter_flatten
@[deprecated flatten_filter_not_isEmpty (since := "2024-10-14")] abbrev join_filter_not_isEmpty := @flatten_filter_not_isEmpty
@[deprecated flatten_filter_ne_nil (since := "2024-10-14")] abbrev join_filter_ne_nil := @flatten_filter_ne_nil
@[deprecated filter_flatten (since := "2024-08-26")]
theorem join_map_filter (p : α Bool) (l : List (List α)) :
(l.map (filter p)).flatten = (l.flatten).filter p := by
rw [filter_flatten]
@[deprecated flatten_append (since := "2024-10-14")] abbrev join_append := @flatten_append
@[deprecated flatten_concat (since := "2024-10-14")] abbrev join_concat := @flatten_concat
@[deprecated flatten_flatten (since := "2024-10-14")] abbrev join_join := @flatten_flatten
@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons_iff := @flatten_eq_cons_iff
@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @flatten_eq_cons_iff
@[deprecated flatten_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @flatten_eq_append_iff
@[deprecated flatten_eq_append_iff (since := "2024-10-14")] abbrev join_eq_append_iff := @flatten_eq_append_iff
@[deprecated eq_iff_flatten_eq (since := "2024-10-14")] abbrev eq_iff_join_eq := @eq_iff_flatten_eq
@[deprecated flatten_replicate_nil (since := "2024-10-14")] abbrev join_replicate_nil := @flatten_replicate_nil
@[deprecated flatten_replicate_singleton (since := "2024-10-14")] abbrev join_replicate_singleton := @flatten_replicate_singleton
@[deprecated flatten_replicate_replicate (since := "2024-10-14")] abbrev join_replicate_replicate := @flatten_replicate_replicate
@[deprecated reverse_flatten (since := "2024-10-14")] abbrev reverse_join := @reverse_flatten
@[deprecated flatten_reverse (since := "2024-10-14")] abbrev join_reverse := @flatten_reverse
@[deprecated getLast?_flatten (since := "2024-10-14")] abbrev getLast?_join := @getLast?_flatten
end List

View File

@@ -1,248 +0,0 @@
/-
Copyright (c) 2024 Lean FRO. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison, Mario Carneiro
-/
prelude
import Init.Data.Array.Lemmas
import Init.Data.List.Nat.Range
namespace List
/-! ## Operations using indexes -/
/-! ### mapIdx -/
/--
Given a function `f : Nat → α → β` and `as : list α`, `as = [a₀, a₁, ...]`, returns the list
`[f 0 a₀, f 1 a₁, ...]`.
-/
@[inline] def mapIdx (f : Nat α β) (as : List α) : List β := go as #[] where
/-- Auxiliary for `mapIdx`:
`mapIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]` -/
@[specialize] go : List α Array β List β
| [], acc => acc.toList
| a :: as, acc => go as (acc.push (f acc.size a))
@[simp]
theorem mapIdx_nil {f : Nat α β} : mapIdx f [] = [] :=
rfl
theorem mapIdx_go_append {l₁ l₂ : List α} {arr : Array β} :
mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (List.toArray (mapIdx.go f l₁ arr)) := by
generalize h : (l₁ ++ l₂).length = len
induction len generalizing l₁ arr with
| zero =>
have l₁_nil : l₁ = [] := by
cases l₁
· rfl
· contradiction
have l₂_nil : l₂ = [] := by
cases l₂
· rfl
· rw [List.length_append] at h; contradiction
rw [l₁_nil, l₂_nil]; simp only [mapIdx.go, List.toArray_toList]
| succ len ih =>
cases l₁ with
| nil =>
simp only [mapIdx.go, nil_append, List.toArray_toList]
| cons head tail =>
simp only [mapIdx.go, List.append_eq]
rw [ih]
· simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h
simp only [length_append, h]
theorem mapIdx_go_length {arr : Array β} :
length (mapIdx.go f l arr) = length l + arr.size := by
induction l generalizing arr with
| nil => simp only [mapIdx.go, length_nil, Nat.zero_add]
| cons _ _ ih =>
simp only [mapIdx.go, ih, Array.size_push, Nat.add_succ, length_cons, Nat.add_comm]
@[simp] theorem mapIdx_concat {l : List α} {e : α} :
mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e] := by
unfold mapIdx
rw [mapIdx_go_append]
simp only [mapIdx.go, Array.size_toArray, mapIdx_go_length, length_nil, Nat.add_zero,
Array.push_toList]
@[simp] theorem mapIdx_singleton {a : α} : mapIdx f [a] = [f 0 a] := by
simpa using mapIdx_concat (l := [])
theorem length_mapIdx_go : {l : List α} {arr : Array β},
(mapIdx.go f l arr).length = l.length + arr.size
| [], _ => by simp [mapIdx.go]
| a :: l, _ => by
simp only [mapIdx.go, length_cons]
rw [length_mapIdx_go]
simp
omega
@[simp] theorem length_mapIdx {l : List α} : (l.mapIdx f).length = l.length := by
simp [mapIdx, length_mapIdx_go]
theorem getElem?_mapIdx_go : {l : List α} {arr : Array β} {i : Nat},
(mapIdx.go f l arr)[i]? =
if h : i < arr.size then some arr[i] else Option.map (f i) l[i - arr.size]?
| [], arr, i => by
simp only [mapIdx.go, Array.toListImpl_eq, getElem?_eq, Array.length_toList,
Array.getElem_eq_getElem_toList, length_nil, Nat.not_lt_zero, reduceDIte, Option.map_none']
| a :: l, arr, i => by
rw [mapIdx.go, getElem?_mapIdx_go]
simp only [Array.size_push]
split <;> split
· simp only [Option.some.injEq]
rw [Array.getElem_eq_getElem_toList]
simp only [Array.push_toList]
rw [getElem_append_left, Array.getElem_eq_getElem_toList]
· have : i = arr.size := by omega
simp_all
· omega
· have : i - arr.size = i - (arr.size + 1) + 1 := by omega
simp_all
@[simp] theorem getElem?_mapIdx {l : List α} {i : Nat} :
(l.mapIdx f)[i]? = Option.map (f i) l[i]? := by
simp [mapIdx, getElem?_mapIdx_go]
@[simp] theorem getElem_mapIdx {l : List α} {f : Nat α β} {i : Nat} {h : i < (l.mapIdx f).length} :
(l.mapIdx f)[i] = f i (l[i]'(by simpa using h)) := by
apply Option.some_inj.mp
rw [ getElem?_eq_getElem, getElem?_mapIdx, getElem?_eq_getElem (by simpa using h)]
simp
theorem mapIdx_eq_enum_map {l : List α} :
l.mapIdx f = l.enum.map (Function.uncurry f) := by
ext1 i
simp only [getElem?_mapIdx, Option.map, getElem?_map, getElem?_enum]
split <;> simp
@[simp]
theorem mapIdx_cons {l : List α} {a : α} :
mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l := by
simp [mapIdx_eq_enum_map, enum_eq_zip_range, map_uncurry_zip_eq_zipWith,
range_succ_eq_map, zipWith_map_left]
theorem mapIdx_append {K L : List α} :
(K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.length) := by
induction K generalizing f with
| nil => rfl
| cons _ _ ih => simp [ih (f := fun i => f (i + 1)), Nat.add_assoc]
@[simp]
theorem mapIdx_eq_nil_iff {l : List α} : List.mapIdx f l = [] l = [] := by
rw [List.mapIdx_eq_enum_map, List.map_eq_nil_iff, List.enum_eq_nil]
theorem mapIdx_ne_nil_iff {l : List α} :
List.mapIdx f l [] l [] := by
simp
theorem exists_of_mem_mapIdx {b : β} {l : List α}
(h : b mapIdx f l) : (i : Nat) (h : i < l.length), f i l[i] = b := by
rw [mapIdx_eq_enum_map] at h
replace h := exists_of_mem_map h
simp only [Prod.exists, mk_mem_enum_iff_getElem?, Function.uncurry_apply_pair] at h
obtain i, b, h, rfl := h
rw [getElem?_eq_some_iff] at h
obtain h, rfl := h
exact i, h, rfl
@[simp] theorem mem_mapIdx {b : β} {l : List α} :
b mapIdx f l (i : Nat) (h : i < l.length), f i l[i] = b := by
constructor
· intro h
exact exists_of_mem_mapIdx h
· rintro i, h, rfl
rw [mem_iff_getElem]
exact i, by simpa using h, by simp
theorem mapIdx_eq_cons_iff {l : List α} {b : β} :
mapIdx f l = b :: l₂
(a : α) (l₁ : List α), l = a :: l₁ f 0 a = b mapIdx (fun i => f (i + 1)) l₁ = l₂ := by
cases l <;> simp [and_assoc]
theorem mapIdx_eq_cons_iff' {l : List α} {b : β} :
mapIdx f l = b :: l₂
l.head?.map (f 0) = some b l.tail?.map (mapIdx fun i => f (i + 1)) = some l₂ := by
cases l <;> simp
theorem mapIdx_eq_iff {l : List α} : mapIdx f l = l' i : Nat, l'[i]? = l[i]?.map (f i) := by
constructor
· intro w i
simpa using congrArg (fun l => l[i]?) w.symm
· intro w
ext1 i
simp [w]
theorem mapIdx_eq_mapIdx_iff {l : List α} :
mapIdx f l = mapIdx g l i : Nat, (h : i < l.length) f i l[i] = g i l[i] := by
constructor
· intro w i h
simpa [h] using congrArg (fun l => l[i]?) w
· intro w
apply ext_getElem
· simp
· intro i h₁ h₂
simp [w]
@[simp] theorem mapIdx_set {l : List α} {i : Nat} {a : α} :
(l.set i a).mapIdx f = (l.mapIdx f).set i (f i a) := by
simp only [mapIdx_eq_iff, getElem?_set, length_mapIdx, getElem?_mapIdx]
intro i
split
· split <;> simp_all
· rfl
@[simp] theorem head_mapIdx {l : List α} {f : Nat α β} {w : mapIdx f l []} :
(mapIdx f l).head w = f 0 (l.head (by simpa using w)) := by
cases l with
| nil => simp at w
| cons _ _ => simp
@[simp] theorem head?_mapIdx {l : List α} {f : Nat α β} : (mapIdx f l).head? = l.head?.map (f 0) := by
cases l <;> simp
@[simp] theorem getLast_mapIdx {l : List α} {f : Nat α β} {h} :
(mapIdx f l).getLast h = f (l.length - 1) (l.getLast (by simpa using h)) := by
cases l with
| nil => simp at h
| cons _ _ =>
simp only [ getElem_cons_length _ _ _ rfl]
simp only [mapIdx_cons]
simp only [ getElem_cons_length _ _ _ rfl]
simp only [ mapIdx_cons, getElem_mapIdx]
simp
@[simp] theorem getLast?_mapIdx {l : List α} {f : Nat α β} :
(mapIdx f l).getLast? = (getLast? l).map (f (l.length - 1)) := by
cases l
· simp
· rw [getLast?_eq_getLast, getLast?_eq_getLast, getLast_mapIdx] <;> simp
@[simp] theorem mapIdx_mapIdx {l : List α} {f : Nat α β} {g : Nat β γ} :
(l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i f i) := by
simp [mapIdx_eq_iff]
theorem mapIdx_eq_replicate_iff {l : List α} {f : Nat α β} {b : β} :
mapIdx f l = replicate l.length b (i : Nat) (h : i < l.length), f i l[i] = b := by
simp only [eq_replicate_iff, length_mapIdx, mem_mapIdx, forall_exists_index, true_and]
constructor
· intro w i h
apply w _ _ _ rfl
· rintro w _ i h rfl
exact w i h
@[simp] theorem mapIdx_reverse {l : List α} {f : Nat α β} :
l.reverse.mapIdx f = (mapIdx (fun i => f (l.length - 1 - i)) l).reverse := by
simp [mapIdx_eq_iff]
intro i
by_cases h : i < l.length
· simp [getElem?_reverse, h]
congr
omega
· simp at h
rw [getElem?_eq_none (by simp [h]), getElem?_eq_none (by simp [h])]
simp
end List

View File

@@ -20,28 +20,20 @@ open Nat
@[simp] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl
-- We don't put `@[simp]` on `min?_cons'`,
-- We don't put `@[simp]` on `min?_cons`,
-- because the definition in terms of `foldl` is not useful for proofs.
theorem min?_cons' [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl
@[simp] theorem min?_cons [Min α] [Std.Associative (min : α α α)] {xs : List α} :
(x :: xs).min? = some (xs.min?.elim x (min x)) := by
cases xs <;> simp [min?_cons', foldl_assoc]
theorem min?_cons [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl
@[simp] theorem min?_eq_none_iff {xs : List α} [Min α] : xs.min? = none xs = [] := by
cases xs <;> simp [min?]
theorem isSome_min?_of_mem {l : List α} [Min α] {a : α} (h : a l) :
l.min?.isSome := by
cases l <;> simp_all [List.min?_cons']
theorem min?_mem [Min α] (min_eq_or : a b : α, min a b = a min a b = b) :
{xs : List α} xs.min? = some a a xs := by
intro xs
match xs with
| nil => simp
| x :: xs =>
simp only [min?_cons', Option.some.injEq, List.mem_cons]
simp only [min?_cons, Option.some.injEq, List.mem_cons]
intro eq
induction xs generalizing x with
| nil =>
@@ -93,35 +85,23 @@ theorem min?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
(replicate n a).min? = if n = 0 then none else some a := by
induction n with
| zero => rfl
| succ n ih => cases n <;> simp_all [replicate_succ, min?_cons']
| succ n ih => cases n <;> simp_all [replicate_succ, min?_cons]
@[simp] theorem min?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
(replicate n a).min? = some a := by
simp [min?_replicate, Nat.ne_of_gt h, w]
theorem foldl_min [Min α] [Std.IdempotentOp (min : α α α)] [Std.Associative (min : α α α)]
{l : List α} {a : α} : l.foldl (init := a) min = min a (l.min?.getD a) := by
cases l <;> simp [min?, foldl_assoc, Std.IdempotentOp.idempotent]
/-! ### max? -/
@[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
-- We don't put `@[simp]` on `max?_cons'`,
-- We don't put `@[simp]` on `max?_cons`,
-- because the definition in terms of `foldl` is not useful for proofs.
theorem max?_cons' [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl
@[simp] theorem max?_cons [Max α] [Std.Associative (max : α α α)] {xs : List α} :
(x :: xs).max? = some (xs.max?.elim x (max x)) := by
cases xs <;> simp [max?_cons', foldl_assoc]
theorem max?_cons [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl
@[simp] theorem max?_eq_none_iff {xs : List α} [Max α] : xs.max? = none xs = [] := by
cases xs <;> simp [max?]
theorem isSome_max?_of_mem {l : List α} [Max α] {a : α} (h : a l) :
l.max?.isSome := by
cases l <;> simp_all [List.max?_cons']
theorem max?_mem [Max α] (min_eq_or : a b : α, max a b = a max a b = b) :
{xs : List α} xs.max? = some a a xs
| nil => by simp
@@ -164,16 +144,12 @@ theorem max?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
(replicate n a).max? = if n = 0 then none else some a := by
induction n with
| zero => rfl
| succ n ih => cases n <;> simp_all [replicate_succ, max?_cons']
| succ n ih => cases n <;> simp_all [replicate_succ, max?_cons]
@[simp] theorem max?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
(replicate n a).max? = some a := by
simp [max?_replicate, Nat.ne_of_gt h, w]
theorem foldl_max [Max α] [Std.IdempotentOp (max : α α α)] [Std.Associative (max : α α α)]
{l : List α} {a : α} : l.foldl (init := a) max = max a (l.max?.getD a) := by
cases l <;> simp [max?, foldl_assoc, Std.IdempotentOp.idempotent]
@[deprecated min?_nil (since := "2024-09-29")] abbrev minimum?_nil := @min?_nil
@[deprecated min?_cons (since := "2024-09-29")] abbrev minimum?_cons := @min?_cons
@[deprecated min?_eq_none_iff (since := "2024-09-29")] abbrev mininmum?_eq_none_iff := @min?_eq_none_iff

View File

@@ -96,22 +96,75 @@ theorem min?_eq_some_iff' {xs : List Nat} :
(min_eq_or := fun _ _ => Nat.min_def .. by split <;> simp)
(le_min_iff := fun _ _ _ => Nat.le_min)
theorem min?_get_le_of_mem {l : List Nat} {a : Nat} (h : a l) :
l.min?.get (isSome_min?_of_mem h) a := by
induction l with
| nil => simp at h
| cons b t ih =>
simp only [min?_cons, Option.get_some] at ih
rcases mem_cons.1 h with (rfl|h)
· cases t.min? with
| none => simp
| some b => simpa using Nat.min_le_left _ _
· obtain q, hq := Option.isSome_iff_exists.1 (isSome_min?_of_mem h)
simp only [hq, Option.elim_some] at ih
exact Nat.le_trans (Nat.min_le_right _ _) (ih h)
-- This could be generalized,
-- but will first require further work on order typeclasses in the core repository.
theorem min?_cons' {a : Nat} {l : List Nat} :
(a :: l).min? = some (match l.min? with
| none => a
| some m => min a m) := by
rw [min?_eq_some_iff']
split <;> rename_i h m
· simp_all
· rw [min?_eq_some_iff'] at m
obtain m, le := m
rw [Nat.min_def]
constructor
· split
· exact mem_cons_self a l
· exact mem_cons_of_mem a m
· intro b m
cases List.mem_cons.1 m with
| inl => split <;> omega
| inr h =>
specialize le b h
split <;> omega
theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a l) : l.min?.getD k a :=
Option.get_eq_getD _ min?_get_le_of_mem h
theorem foldl_min
{α : Type _} [Min α] [Std.IdempotentOp (min : α α α)] [Std.Associative (min : α α α)]
{l : List α} {a : α} :
l.foldl (init := a) min = min a (l.min?.getD a) := by
cases l with
| nil => simp [Std.IdempotentOp.idempotent]
| cons b l =>
simp only [min?]
induction l generalizing a b with
| nil => simp
| cons c l ih => simp [ih, Std.Associative.assoc]
theorem foldl_min_right {α β : Type _}
[Min β] [Std.IdempotentOp (min : β β β)] [Std.Associative (min : β β β)]
{l : List α} {b : β} {f : α β} :
(l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).min?.getD b) := by
rw [ foldl_map, foldl_min]
theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min a := by
induction l generalizing a with
| nil => simp
| cons c l ih =>
simp only [foldl_cons]
exact Nat.le_trans ih (Nat.min_le_left _ _)
theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a b) :
l.foldl (init := a) min b :=
Nat.le_trans (foldl_min_le) h
theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a l) :
l.min?.getD k a := by
cases l with
| nil => simp at h
| cons b l =>
simp [min?_cons]
simp at h
rcases h with (rfl | h)
· exact foldl_min_le
· induction l generalizing b with
| nil => simp_all
| cons c l ih =>
simp only [foldl_cons]
simp at h
rcases h with (rfl | h)
· exact foldl_min_min_of_le (Nat.min_le_right _ _)
· exact ih _ h
/-! ### max? -/
@@ -123,23 +176,75 @@ theorem max?_eq_some_iff' {xs : List Nat} :
(max_eq_or := fun _ _ => Nat.max_def .. by split <;> simp)
(max_le_iff := fun _ _ _ => Nat.max_le)
theorem le_max?_get_of_mem {l : List Nat} {a : Nat} (h : a l) :
a l.max?.get (isSome_max?_of_mem h) := by
induction l with
| nil => simp at h
| cons b t ih =>
simp only [max?_cons, Option.get_some] at ih
rcases mem_cons.1 h with (rfl|h)
· cases t.max? with
| none => simp
| some b => simpa using Nat.le_max_left _ _
· obtain q, hq := Option.isSome_iff_exists.1 (isSome_max?_of_mem h)
simp only [hq, Option.elim_some] at ih
exact Nat.le_trans (ih h) (Nat.le_max_right _ _)
-- This could be generalized,
-- but will first require further work on order typeclasses in the core repository.
theorem max?_cons' {a : Nat} {l : List Nat} :
(a :: l).max? = some (match l.max? with
| none => a
| some m => max a m) := by
rw [max?_eq_some_iff']
split <;> rename_i h m
· simp_all
· rw [max?_eq_some_iff'] at m
obtain m, le := m
rw [Nat.max_def]
constructor
· split
· exact mem_cons_of_mem a m
· exact mem_cons_self a l
· intro b m
cases List.mem_cons.1 m with
| inl => split <;> omega
| inr h =>
specialize le b h
split <;> omega
theorem foldl_max
{α : Type _} [Max α] [Std.IdempotentOp (max : α α α)] [Std.Associative (max : α α α)]
{l : List α} {a : α} :
l.foldl (init := a) max = max a (l.max?.getD a) := by
cases l with
| nil => simp [Std.IdempotentOp.idempotent]
| cons b l =>
simp only [max?]
induction l generalizing a b with
| nil => simp
| cons c l ih => simp [ih, Std.Associative.assoc]
theorem foldl_max_right {α β : Type _}
[Max β] [Std.IdempotentOp (max : β β β)] [Std.Associative (max : β β β)]
{l : List α} {b : β} {f : α β} :
(l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).max?.getD b) := by
rw [ foldl_map, foldl_max]
theorem le_foldl_max {l : List Nat} {a : Nat} : a l.foldl (init := a) max := by
induction l generalizing a with
| nil => simp
| cons c l ih =>
simp only [foldl_cons]
exact Nat.le_trans (Nat.le_max_left _ _) ih
theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a b) :
a l.foldl (init := b) max :=
Nat.le_trans h (le_foldl_max)
theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a l) :
a l.max?.getD k :=
Option.get_eq_getD _ le_max?_get_of_mem h
a l.max?.getD k := by
cases l with
| nil => simp at h
| cons b l =>
simp [max?_cons]
simp at h
rcases h with (rfl | h)
· exact le_foldl_max
· induction l generalizing b with
| nil => simp_all
| cons c l ih =>
simp only [foldl_cons]
simp at h
rcases h with (rfl | h)
· exact le_foldl_max_of_le (Nat.le_max_right b a)
· exact ih _ h
@[deprecated min?_eq_some_iff' (since := "2024-09-29")] abbrev minimum?_eq_some_iff' := @min?_eq_some_iff'
@[deprecated min?_cons' (since := "2024-09-29")] abbrev minimum?_cons' := @min?_cons'

View File

@@ -500,13 +500,4 @@ theorem enum_eq_zip_range (l : List α) : l.enum = (range l.length).zip l :=
theorem unzip_enum_eq_prod (l : List α) : l.enum.unzip = (range l.length, l) := by
simp only [enum_eq_zip_range, unzip_zip, length_range]
theorem enum_eq_cons_iff {l : List α} :
l.enum = x :: l' a as, l = a :: as x = (0, a) l' = enumFrom 1 as := by
rw [enum, enumFrom_eq_cons_iff]
theorem enum_eq_append_iff {l : List α} :
l.enum = l₁ ++ l₂
l₁' l₂', l = l₁' ++ l₂' l₁ = l₁'.enum l₂ = l₂'.enumFrom l₁'.length := by
simp [enum, enumFrom_eq_append_iff]
end List

View File

@@ -160,23 +160,21 @@ theorem pairwise_middle {R : αα → Prop} (s : ∀ {x y}, R x y → R y x
rw [ append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
simp only [mem_append, or_comm]
theorem pairwise_flatten {L : List (List α)} :
Pairwise R (flatten L)
theorem pairwise_join {L : List (List α)} :
Pairwise R (join L)
( l L, Pairwise R l) Pairwise (fun l₁ l₂ => x l₁, y l₂, R x y) L := by
induction L with
| nil => simp
| cons l L IH =>
simp only [flatten, pairwise_append, IH, mem_flatten, exists_imp, and_imp, forall_mem_cons,
simp only [join, pairwise_append, IH, mem_join, exists_imp, and_imp, forall_mem_cons,
pairwise_cons, and_assoc, and_congr_right_iff]
rw [and_comm, and_congr_left_iff]
intros; exact fun h a b c d e => h c d e a b, fun h c d e a b => h a b c d e
@[deprecated pairwise_flatten (since := "2024-10-14")] abbrev pairwise_join := @pairwise_flatten
theorem pairwise_bind {R : β β Prop} {l : List α} {f : α List β} :
List.Pairwise R (l.bind f)
( a l, Pairwise R (f a)) Pairwise (fun a₁ a₂ => x f a₁, y f a₂, R x y) l := by
simp [List.bind, pairwise_flatten, pairwise_map]
simp [List.bind, pairwise_join, pairwise_map]
theorem pairwise_reverse {l : List α} :
l.reverse.Pairwise R l.Pairwise (fun a b => R b a) := by

View File

@@ -461,17 +461,15 @@ theorem Perm.nodup {l l' : List α} (hl : l ~ l') (hR : l.Nodup) : l'.Nodup := h
theorem Perm.nodup_iff {l₁ l₂ : List α} : l₁ ~ l₂ (Nodup l₁ Nodup l₂) :=
Perm.pairwise_iff <| @Ne.symm α
theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatten ~ l₂.flatten := by
theorem Perm.join {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.join ~ l₂.join := by
induction h with
| nil => rfl
| cons _ _ ih => simp only [flatten_cons, perm_append_left_iff, ih]
| swap => simp only [flatten_cons, append_assoc, perm_append_right_iff]; exact perm_append_comm ..
| cons _ _ ih => simp only [join_cons, perm_append_left_iff, ih]
| swap => simp only [join_cons, append_assoc, perm_append_right_iff]; exact perm_append_comm ..
| trans _ _ ih₁ ih₂ => exact trans ih₁ ih₂
@[deprecated Perm.flatten (since := "2024-10-14")] abbrev Perm.join := @Perm.flatten
theorem Perm.bind_right {l₁ l₂ : List α} (f : α List β) (p : l₁ ~ l₂) : l₁.bind f ~ l₂.bind f :=
(p.map _).flatten
(p.map _).join
theorem Perm.eraseP (f : α Bool) {l₁ l₂ : List α}
(H : Pairwise (fun a b => f a f b False) l₁) (p : l₁ ~ l₂) : eraseP f l₁ ~ eraseP f l₂ := by

View File

@@ -20,6 +20,7 @@ open Nat
/-! ## Ranges and enumeration -/
/-! ### range' -/
theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) n step := by

View File

@@ -483,30 +483,30 @@ theorem sublist_replicate_iff : l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = re
rw [w]
exact (replicate_sublist_replicate a).2 le
theorem sublist_flatten_of_mem {L : List (List α)} {l} (h : l L) : l <+ L.flatten := by
theorem sublist_join_of_mem {L : List (List α)} {l} (h : l L) : l <+ L.join := by
induction L with
| nil => cases h
| cons l' L ih =>
rcases mem_cons.1 h with (rfl | h)
· simp [h]
· simp [ih h, flatten_cons, sublist_append_of_sublist_right]
· simp [ih h, join_cons, sublist_append_of_sublist_right]
theorem sublist_flatten_iff {L : List (List α)} {l} :
l <+ L.flatten
L' : List (List α), l = L'.flatten i (_ : i < L'.length), L'[i] <+ L[i]?.getD [] := by
theorem sublist_join_iff {L : List (List α)} {l} :
l <+ L.join
L' : List (List α), l = L'.join i (_ : i < L'.length), L'[i] <+ L[i]?.getD [] := by
induction L generalizing l with
| nil =>
constructor
· intro w
simp only [flatten_nil, sublist_nil] at w
simp only [join_nil, sublist_nil] at w
subst w
exact [], by simp, fun i x => by cases x
· rintro L', rfl, h
simp only [flatten_nil, sublist_nil, flatten_eq_nil_iff]
simp only [join_nil, sublist_nil, join_eq_nil_iff]
simp only [getElem?_nil, Option.getD_none, sublist_nil] at h
exact (forall_getElem (p := (· = []))).1 h
| cons l' L ih =>
simp only [flatten_cons, sublist_append_iff, ih]
simp only [join_cons, sublist_append_iff, ih]
constructor
· rintro l₁, l₂, rfl, s, L', rfl, h
refine l₁ :: L', by simp, ?_
@@ -517,21 +517,21 @@ theorem sublist_flatten_iff {L : List (List α)} {l} :
| nil =>
exact [], [], by simp, by simp, [], by simp, fun i x => by cases x
| cons l₁ L' =>
exact l₁, L'.flatten, by simp, by simpa using h 0 (by simp), L', rfl,
exact l₁, L'.join, by simp, by simpa using h 0 (by simp), L', rfl,
fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)
theorem flatten_sublist_iff {L : List (List α)} {l} :
L.flatten <+ l
L' : List (List α), l = L'.flatten i (_ : i < L.length), L[i] <+ L'[i]?.getD [] := by
theorem join_sublist_iff {L : List (List α)} {l} :
L.join <+ l
L' : List (List α), l = L'.join i (_ : i < L.length), L[i] <+ L'[i]?.getD [] := by
induction L generalizing l with
| nil =>
constructor
· intro _
exact [l], by simp, fun i x => by cases x
· rintro L', rfl, _
simp only [flatten_nil, nil_sublist]
simp only [join_nil, nil_sublist]
| cons l' L ih =>
simp only [flatten_cons, append_sublist_iff, ih]
simp only [join_cons, append_sublist_iff, ih]
constructor
· rintro l₁, l₂, rfl, s, L', rfl, h
refine l₁ :: L', by simp, ?_
@@ -543,7 +543,7 @@ theorem flatten_sublist_iff {L : List (List α)} {l} :
exact [], [], by simp, by simpa using h 0 (by simp), [], by simp,
fun i x => by simpa using h (i+1) (Nat.add_lt_add_right x 1)
| cons l₁ L' =>
exact l₁, L'.flatten, by simp, by simpa using h 0 (by simp), L', rfl,
exact l₁, L'.join, by simp, by simpa using h 0 (by simp), L', rfl,
fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)
@[simp] theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
@@ -938,14 +938,14 @@ theorem isInfix_replicate_iff {n} {a : α} {l : List α} :
· simpa using Nat.sub_add_cancel h
· simpa using w
theorem infix_of_mem_flatten : {L : List (List α)}, l L l <:+: flatten L
theorem infix_of_mem_join : {L : List (List α)}, l L l <:+: join L
| l' :: _, h =>
match h with
| List.Mem.head .. => infix_append [] _ _
| List.Mem.tail _ hlMemL =>
IsInfix.trans (infix_of_mem_flatten hlMemL) <| (suffix_append _ _).isInfix
IsInfix.trans (infix_of_mem_join hlMemL) <| (suffix_append _ _).isInfix
@[simp] theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂ l₁ <+: l₂ :=
theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂ l₁ <+: l₂ :=
exists_congr fun r => by rw [append_assoc, append_right_inj]
theorem prefix_cons_inj (a) : a :: l₁ <+: a :: l₂ l₁ <+: l₂ :=
@@ -976,7 +976,7 @@ theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l :=
drop_subset _ _ h
theorem drop_suffix_drop_left (l : List α) {m n : Nat} (h : m n) : drop n l <:+ drop m l := by
rw [ Nat.sub_add_cancel h, Nat.add_comm, drop_drop]
rw [ Nat.sub_add_cancel h, drop_drop]
apply drop_suffix
-- See `Init.Data.List.Nat.TakeDrop` for `take_prefix_take_left`.
@@ -1087,11 +1087,4 @@ theorem prefix_iff_eq_take : l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ :=
-- See `Init.Data.List.Nat.Sublist` for `suffix_iff_eq_append`, `prefix_take_iff`, and `suffix_iff_eq_drop`.
/-! ### Deprecations -/
@[deprecated sublist_flatten_of_mem (since := "2024-10-14")] abbrev sublist_join_of_mem := @sublist_flatten_of_mem
@[deprecated sublist_flatten_iff (since := "2024-10-14")] abbrev sublist_join_iff := @sublist_flatten_iff
@[deprecated flatten_sublist_iff (since := "2024-10-14")] abbrev flatten_join_iff := @flatten_sublist_iff
@[deprecated infix_of_mem_flatten (since := "2024-10-14")] abbrev infix_of_mem_join := @infix_of_mem_flatten
end List

View File

@@ -97,14 +97,14 @@ theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.
theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := by simp
@[simp] theorem drop_drop (n : Nat) : (m) (l : List α), drop n (drop m l) = drop (m + n) l
@[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 (m + n) l := drop_drop n m l
_ = drop ((m + 1) + n) (a :: l) := by rw [Nat.add_right_comm]; 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
@@ -112,7 +112,7 @@ theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (t
| _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
@[deprecated drop_drop (since := "2024-06-15")]
theorem drop_add (m n) (l : List α) : drop (m + n) l = drop n (drop m l) := by
theorem drop_add (m n) (l : List α) : drop (m + n) l = drop m (drop n l) := by
simp [drop_drop]
@[simp]
@@ -126,7 +126,7 @@ theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) :=
@[simp]
theorem drop_tail (l : List α) (n : Nat) : l.tail.drop n = l.drop (n + 1) := by
rw [Nat.add_comm, drop_drop, drop_one]
rw [ drop_drop, drop_one]
@[simp]
theorem drop_eq_nil_iff {l : List α} {k : Nat} : l.drop k = [] l.length k := by

View File

@@ -1,23 +0,0 @@
/-
Copyright (c) 2024 Lean FRO. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Init.Data.List.Basic
/--
Auxiliary definition for `List.toArray`.
`List.toArrayAux as r = r ++ as.toArray`
-/
@[inline_if_reduce]
def List.toArrayAux : List α Array α Array α
| nil, r => r
| cons a as, r => toArrayAux as (r.push a)
/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list. -/
-- This function is exported to C, where it is called by `Array.mk`
-- (the constructor) to implement this functionality.
@[inline, match_pattern, pp_nodot, export lean_list_to_array]
def List.toArrayImpl (as : List α) : Array α :=
as.toArrayAux (Array.mkEmpty as.length)

View File

@@ -5,7 +5,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
-/
prelude
import Init.Data.List.TakeDrop
import Init.Data.Function
/-!
# Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`.
@@ -239,14 +238,6 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : Li
| zero => rfl
| succ n ih => simp [replicate_succ, ih]
theorem map_uncurry_zip_eq_zipWith (f : α β γ) (l : List α) (l' : List β) :
map (Function.uncurry f) (l.zip l') = zipWith f l l' := by
rw [zip]
induction l generalizing l' with
| nil => simp
| cons hl tl ih =>
cases l' <;> simp [ih]
/-! ### zip -/
theorem zip_eq_zipWith : (l₁ : List α) (l₂ : List β), zip l₁ l₂ = zipWith Prod.mk l₁ l₂

View File

@@ -175,68 +175,4 @@ theorem filter_attach {o : Option α} {p : {x // x ∈ o} → Bool} :
o.attach.filter p = o.pbind fun a h => if p a, h then some a, h else none := by
cases o <;> simp [filter_some]
/-! ## unattach
`Option.unattach` is the (one-sided) inverse of `Option.attach`. It is a synonym for `Option.map Subtype.val`.
We use it by providing a simp lemma `l.attach.unattach = l`, and simp lemmas which recognize higher order
functions applied to `l : Option { x // p x }` which only depend on the value, not the predicate, and rewrite these
in terms of a simpler function applied to `l.unattach`.
Further, we provide simp lemmas that push `unattach` inwards.
-/
/--
A synonym for `l.map (·.val)`. Mostly this should not be needed by users.
It is introduced as an intermediate step by lemmas such as `map_subtype`,
and is ideally subsequently simplified away by `unattach_attach`.
If not, usually the right approach is `simp [Option.unattach, -Option.map_subtype]` to unfold.
-/
def unattach {α : Type _} {p : α Prop} (o : Option { x // p x }) := o.map (·.val)
@[simp] theorem unattach_none {p : α Prop} : (none : Option { x // p x }).unattach = none := rfl
@[simp] theorem unattach_some {p : α Prop} {a : { x // p x }} :
(some a).unattach = a.val := rfl
@[simp] theorem isSome_unattach {p : α Prop} {o : Option { x // p x }} :
o.unattach.isSome = o.isSome := by
simp [unattach]
@[simp] theorem isNone_unattach {p : α Prop} {o : Option { x // p x }} :
o.unattach.isNone = o.isNone := by
simp [unattach]
@[simp] theorem unattach_attach (o : Option α) : o.attach.unattach = o := by
cases o <;> simp
@[simp] theorem unattach_attachWith {p : α Prop} {o : Option α}
{H : a o, p a} :
(o.attachWith p H).unattach = o := by
cases o <;> simp
/-! ### Recognizing higher order functions on subtypes using a function that only depends on the value. -/
/--
This lemma identifies maps over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
@[simp] theorem map_subtype {p : α Prop} {o : Option { x // p x }}
{f : { x // p x } β} {g : α β} {hf : x h, f x, h = g x} :
o.map f = o.unattach.map g := by
cases o <;> simp [hf]
@[simp] theorem bind_subtype {p : α Prop} {o : Option { x // p x }}
{f : { x // p x } Option β} {g : α Option β} {hf : x h, f x, h = g x} :
(o.bind f) = o.unattach.bind g := by
cases o <;> simp [hf]
@[simp] theorem unattach_filter {p : α Prop} {o : Option { x // p x }}
{f : { x // p x } Bool} {g : α Bool} {hf : x h, f x, h = g x} :
(o.filter f).unattach = o.unattach.filter g := by
cases o
· simp
· simp only [filter_some, hf, unattach_some]
split <;> simp
end Option

View File

@@ -79,7 +79,7 @@ theorem eq_none_iff_forall_not_mem : o = none ↔ ∀ a, a ∉ o :=
theorem isSome_iff_exists : isSome x a, x = some a := by cases x <;> simp [isSome]
theorem isSome_eq_isSome : (isSome x = isSome y) (x = none y = none) := by
@[simp] theorem isSome_eq_isSome : (isSome x = isSome y) (x = none y = none) := by
cases x <;> cases y <;> simp
@[simp] theorem isNone_none : @isNone α none = true := rfl

View File

@@ -317,9 +317,6 @@ theorem _root_.Char.utf8Size_le_four (c : Char) : c.utf8Size ≤ 4 := by
@[simp] theorem pos_add_char (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size := rfl
protected theorem Pos.ne_zero_of_lt : {a b : Pos} a < b b 0
| _, _, hlt, rfl => Nat.not_lt_zero _ hlt
theorem lt_next (s : String) (i : Pos) : i.1 < (s.next i).1 :=
Nat.add_lt_add_left (Char.utf8Size_pos _) _
@@ -1024,66 +1021,6 @@ instance hasBeq : BEq Substring := ⟨beq⟩
def sameAs (ss1 ss2 : Substring) : Bool :=
ss1.startPos == ss2.startPos && ss1 == ss2
/--
Returns the longest common prefix of two substrings.
The returned substring will use the same underlying string as `s`.
-/
def commonPrefix (s t : Substring) : Substring :=
{ s with stopPos := loop s.startPos t.startPos }
where
/-- Returns the ending position of the common prefix, working up from `spos, tpos`. -/
loop spos tpos :=
if h : spos < s.stopPos tpos < t.stopPos then
if s.str.get spos == t.str.get tpos then
have := Nat.sub_lt_sub_left h.1 (s.str.lt_next spos)
loop (s.str.next spos) (t.str.next tpos)
else
spos
else
spos
termination_by s.stopPos.byteIdx - spos.byteIdx
/--
Returns the longest common suffix of two substrings.
The returned substring will use the same underlying string as `s`.
-/
def commonSuffix (s t : Substring) : Substring :=
{ s with startPos := loop s.stopPos t.stopPos }
where
/-- Returns the starting position of the common prefix, working down from `spos, tpos`. -/
loop spos tpos :=
if h : s.startPos < spos t.startPos < tpos then
let spos' := s.str.prev spos
let tpos' := t.str.prev tpos
if s.str.get spos' == t.str.get tpos' then
have : spos' < spos := s.str.prev_lt_of_pos spos (String.Pos.ne_zero_of_lt h.1)
loop spos' tpos'
else
spos
else
spos
termination_by spos.byteIdx
/--
If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
-/
def dropPrefix? (s : Substring) (pre : Substring) : Option Substring :=
let t := s.commonPrefix pre
if t.bsize = pre.bsize then
some { s with startPos := t.stopPos }
else
none
/--
If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
-/
def dropSuffix? (s : Substring) (suff : Substring) : Option Substring :=
let t := s.commonSuffix suff
if t.bsize = suff.bsize then
some { s with stopPos := t.startPos }
else
none
end Substring
namespace String
@@ -1145,28 +1082,6 @@ namespace String
@[inline] def decapitalize (s : String) :=
s.set 0 <| s.get 0 |>.toLower
/--
If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
-/
def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
s.toSubstring.dropPrefix? pre
/--
If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
-/
def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
s.toSubstring.dropSuffix? suff
/-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
or otherwise return `s`. -/
def stripPrefix (s : String) (pre : Substring) : String :=
s.dropPrefix? pre |>.map Substring.toString |>.getD s
/-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
or otherwise return `s`. -/
def stripSuffix (s : String) (suff : Substring) : String :=
s.dropSuffix? suff |>.map Substring.toString |>.getD s
end String
namespace Char

View File

@@ -121,7 +121,7 @@ def toUTF8 (a : @& String) : ByteArray :=
@[simp] theorem size_toUTF8 (s : String) : s.toUTF8.size = s.utf8ByteSize := by
simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.bind]
induction s.data <;> simp [List.map, List.flatten, utf8ByteSize.go, Nat.add_comm, *]
induction s.data <;> simp [List.map, List.join, utf8ByteSize.go, Nat.add_comm, *]
/-- Accesses a byte in the UTF-8 encoding of the `String`. O(1) -/
@[extern "lean_string_get_byte_fast"]

View File

@@ -535,21 +535,24 @@ syntax (name := includeStr) "include_str " term : term
/--
The `run_cmd doSeq` command executes code in `CommandElabM Unit`.
This is the same as `#eval show CommandElabM Unit from discard do doSeq`.
This is almost the same as `#eval show CommandElabM Unit from do doSeq`,
except that it doesn't print an empty diagnostic.
-/
syntax (name := runCmd) "run_cmd " doSeq : command
/--
The `run_elab doSeq` command executes code in `TermElabM Unit`.
This is the same as `#eval show TermElabM Unit from discard do doSeq`.
This is almost the same as `#eval show TermElabM Unit from do doSeq`,
except that it doesn't print an empty diagnostic.
-/
syntax (name := runElab) "run_elab " doSeq : command
/--
The `run_meta doSeq` command executes code in `MetaM Unit`.
This is the same as `#eval show MetaM Unit from do discard doSeq`.
This is almost the same as `#eval show MetaM Unit from do doSeq`,
except that it doesn't print an empty diagnostic.
(This is effectively a synonym for `run_elab` since `MetaM` lifts to `TermElabM`.)
(This is effectively a synonym for `run_elab`.)
-/
syntax (name := runMeta) "run_meta " doSeq : command
@@ -672,13 +675,6 @@ Message ordering:
For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and drop
everything else.
The command elaborator has special support for `#guard_msgs` for linting.
The `#guard_msgs` itself wants to capture linter warnings,
so it elaborates the command it is attached to as if it were a top-level command.
However, the command elaborator runs linters for *all* top-level commands,
which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings.
The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
-/
syntax (name := guardMsgsCmd)
(docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command

View File

@@ -223,6 +223,38 @@ end Lean
| `($_ $array $index) => `($array[$index]?)
| _ => throw ()
@[app_unexpander Name.mkStr1] def unexpandMkStr1 : Lean.PrettyPrinter.Unexpander
| `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a.getString)]
| _ => throw ()
@[app_unexpander Name.mkStr2] def unexpandMkStr2 : Lean.PrettyPrinter.Unexpander
| `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString)]
| _ => throw ()
@[app_unexpander Name.mkStr3] def unexpandMkStr3 : Lean.PrettyPrinter.Unexpander
| `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString)]
| _ => throw ()
@[app_unexpander Name.mkStr4] def unexpandMkStr4 : Lean.PrettyPrinter.Unexpander
| `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString)]
| _ => throw ()
@[app_unexpander Name.mkStr5] def unexpandMkStr5 : Lean.PrettyPrinter.Unexpander
| `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString)]
| _ => throw ()
@[app_unexpander Name.mkStr6] def unexpandMkStr6 : Lean.PrettyPrinter.Unexpander
| `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString)]
| _ => throw ()
@[app_unexpander Name.mkStr7] def unexpandMkStr7 : Lean.PrettyPrinter.Unexpander
| `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString)]
| _ => throw ()
@[app_unexpander Name.mkStr8] def unexpandMkStr8 : Lean.PrettyPrinter.Unexpander
| `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString ++ "." ++ a8.getString)]
| _ => throw ()
@[app_unexpander Array.empty] def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander
| _ => `(#[])

View File

@@ -2716,6 +2716,28 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
let sz' := Nat.sub (min stop as.size) start
loop sz' start (mkEmpty sz')
/--
Auxiliary definition for `List.toArray`.
`List.toArrayAux as r = r ++ as.toArray`
-/
@[inline_if_reduce]
def List.toArrayAux : List α Array α Array α
| nil, r => r
| cons a as, r => toArrayAux as (r.push a)
/-- A non-tail-recursive version of `List.length`, used for `List.toArray`. -/
@[inline_if_reduce]
def List.redLength : List α Nat
| nil => 0
| cons _ as => as.redLength.succ
/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list. -/
-- This function is exported to C, where it is called by `Array.mk`
-- (the constructor) to implement this functionality.
@[inline, match_pattern, pp_nodot, export lean_list_to_array]
def List.toArrayImpl (as : List α) : Array α :=
as.toArrayAux (Array.mkEmpty as.redLength)
/-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/
class Bind (m : Type u Type v) where
/-- If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the
@@ -2869,32 +2891,6 @@ instance (m n o) [MonadLift n o] [MonadLiftT m n] : MonadLiftT m o where
instance (m) : MonadLiftT m m where
monadLift x := x
/--
Typeclass used for adapting monads. This is similar to `MonadLift`, but instances are allowed to
make use of default state for the purpose of synthesizing such an instance, if necessary.
Every `MonadLift` instance gives a `MonadEval` instance.
The purpose of this class is for the `#eval` command,
which looks for a `MonadEval m CommandElabM` or `MonadEval m IO` instance.
-/
class MonadEval (m : semiOutParam (Type u Type v)) (n : Type u Type w) where
/-- Evaluates a value from monad `m` into monad `n`. -/
monadEval : {α : Type u} m α n α
instance [MonadLift m n] : MonadEval m n where
monadEval := MonadLift.monadLift
/-- The transitive closure of `MonadEval`. -/
class MonadEvalT (m : Type u Type v) (n : Type u Type w) where
/-- Evaluates a value from monad `m` into monad `n`. -/
monadEval : {α : Type u} m α n α
instance (m n o) [MonadEval n o] [MonadEvalT m n] : MonadEvalT m o where
monadEval x := MonadEval.monadEval (m := n) (MonadEvalT.monadEval x)
instance (m) : MonadEvalT m m where
monadEval x := x
/--
A functor in the category of monads. Can be used to lift monad-transforming functions.
Based on [`MFunctor`] from the `pipes` Haskell package, but not restricted to

View File

@@ -928,6 +928,41 @@ def withIsolatedStreams [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (x : m
end FS
end IO
universe u
namespace Lean
/-- Typeclass used for presenting the output of an `#eval` command. -/
class Eval (α : Type u) where
-- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval`
-- so that `()` output is hidden in chained instances such as for some `IO Unit`.
-- We take `Unit → α` instead of `α` because α` may contain effectful debugging primitives (e.g., `dbg_trace`)
eval : (Unit α) (hideUnit : Bool := true) IO Unit
instance instEval [ToString α] : Eval α where
eval a _ := IO.println (toString (a ()))
instance [Repr α] : Eval α where
eval a _ := IO.println (repr (a ()))
instance : Eval Unit where
eval u hideUnit := if hideUnit then pure () else IO.println (repr (u ()))
instance [Eval α] : Eval (IO α) where
eval x _ := do
let a x ()
Eval.eval fun _ => a
instance [Eval α] : Eval (BaseIO α) where
eval x _ := do
let a x ()
Eval.eval fun _ => a
def runEval [Eval α] (a : Unit α) : IO (String × Except IO.Error Unit) :=
IO.FS.withIsolatedStreams (Eval.eval a false |>.toBaseIO)
end Lean
syntax "println! " (interpolatedStr(term) <|> term) : term
macro_rules

View File

@@ -375,12 +375,12 @@ The same as `rfl`, but without trying `eq_refl` at the end.
-/
syntax (name := applyRfl) "apply_rfl" : tactic
-- We try `apply_rfl` first, because it produces a nice error message
-- We try `apply_rfl` first, beause it produces a nice error message
macro_rules | `(tactic| rfl) => `(tactic| apply_rfl)
-- But, mostly for backward compatibility, we try `eq_refl` too (reduces more aggressively)
macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
-- Also for backward compatibility, because `exact` can trigger the implicit lambda feature (see #5366)
-- Als for backward compatibility, because `exact` can trigger the implicit lambda feature (see #5366)
macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
/--
`rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
@@ -399,6 +399,19 @@ example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
-/
syntax (name := acRfl) "ac_rfl" : tactic
/--
`ac_nf` normalizes equalities up to application of an associative and commutative operator.
```
instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
ac_nf
-- goal: a + (b + (c + d)) = a + (b + (c + d))
```
-/
syntax (name := acNf) "ac_nf" : tactic
/--
The `sorry` tactic closes the goal using `sorryAx`. This is intended for stubbing out incomplete
parts of a proof while still having a syntactically correct proof skeleton. Lean will give
@@ -910,15 +923,6 @@ macro_rules | `(tactic| trivial) => `(tactic| simp)
-/
syntax "trivial" : tactic
/--
`classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority
local instance.
Note that `classical` is a scoping tactic: it adds the instance only within the
scope of the tactic.
-/
syntax (name := classical) "classical" ppDedent(tacticSeq) : tactic
/--
The `split` tactic is useful for breaking nested if-then-else and `match` expressions into separate cases.
For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals.
@@ -1168,9 +1172,6 @@ Currently the preprocessor is implemented as `try simp only [bv_toNat] at *`.
-/
macro "bv_omega" : tactic => `(tactic| (try simp only [bv_toNat] at *) <;> omega)
/-- Implementation of `ac_nf` (the full `ac_nf` calls `trivial` afterwards). -/
syntax (name := acNf0) "ac_nf0" (location)? : tactic
/-- Implementation of `norm_cast` (the full `norm_cast` calls `trivial` afterwards). -/
syntax (name := normCast0) "norm_cast0" (location)? : tactic
@@ -1221,24 +1222,6 @@ See also `push_cast`, which moves casts inwards rather than lifting them outward
macro "norm_cast" loc:(location)? : tactic =>
`(tactic| norm_cast0 $[$loc]? <;> try trivial)
/--
`ac_nf` normalizes equalities up to application of an associative and commutative operator.
- `ac_nf` normalizes all hypotheses and the goal target of the goal.
- `ac_nf at l` normalizes at location(s) `l`, where `l` is either `*` or a
list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
can also be used, to signify the target of the goal.
```
instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
ac_nf
-- goal: a + (b + (c + d)) = a + (b + (c + d))
```
-/
macro "ac_nf" loc:(location)? : tactic =>
`(tactic| ac_nf0 $[$loc]? <;> try trivial)
/--
`push_cast` rewrites the goal to move certain coercions (*casts*) inward, toward the leaf nodes.
This uses `norm_cast` lemmas in the forward direction.

View File

@@ -20,6 +20,7 @@ import Lean.MetavarContext
import Lean.AuxRecursor
import Lean.Meta
import Lean.Util
import Lean.Eval
import Lean.Structure
import Lean.PrettyPrinter
import Lean.CoreM
@@ -37,4 +38,3 @@ import Lean.Linter
import Lean.SubExpr
import Lean.LabelAttribute
import Lean.AddDecl
import Lean.Replay

View File

@@ -7,6 +7,7 @@ prelude
import Lean.Util.RecDepth
import Lean.Util.Trace
import Lean.Log
import Lean.Eval
import Lean.ResolveName
import Lean.Elab.InfoTree.Types
import Lean.MonadEnv
@@ -276,6 +277,12 @@ def mkFreshUserName (n : Name) : CoreM Name :=
| Except.error (Exception.internal id _) => throw <| IO.userError <| "internal exception #" ++ toString id.idx
| Except.ok a => return a
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 }
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)
@@ -302,7 +309,7 @@ register_builtin_option debug.moduleNameAtTimeout : Bool := {
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 ""
throw <| Exception.error ( getRef) <| .tagged `runtime.maxHeartbeats m!"\
throw <| Exception.error ( getRef) m!"\
(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\n\
Use `set_option {optionName} <num>` to set the limit.\
{useDiagnosticMsg}"
@@ -388,7 +395,10 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
This function is a bit hackish. The heartbeat exception should probably be an internal exception.
We used a similar hack at `Exception.isMaxRecDepth` -/
def Exception.isMaxHeartbeat (ex : Exception) : Bool :=
ex matches Exception.error _ (.tagged `runtime.maxHeartbeats _)
match ex with
| Exception.error _ (MessageData.ofFormatWithInfos Std.Format.text msg, _) =>
"(deterministic) timeout".isPrefixOf msg
| _ => false
/-- Creates the expression `d → b` -/
def mkArrow (d b : Expr) : CoreM Expr :=

View File

@@ -41,18 +41,6 @@ structure InsertReplaceEdit where
replace : Range
deriving FromJson, ToJson
inductive CompletionItemTag where
| deprecated
deriving Inhabited, DecidableEq, Repr
instance : ToJson CompletionItemTag where
toJson t := toJson (t.toCtorIdx + 1)
instance : FromJson CompletionItemTag where
fromJson? v := do
let i : Nat fromJson? v
return CompletionItemTag.ofNat (i-1)
structure CompletionItem where
label : String
detail? : Option String := none
@@ -61,8 +49,8 @@ structure CompletionItem where
textEdit? : Option InsertReplaceEdit := none
sortText? : Option String := none
data? : Option Json := none
tags? : Option (Array CompletionItemTag) := none
/-
tags? : CompletionItemTag[]
deprecated? : boolean
preselect? : boolean
filterText? : string
@@ -71,8 +59,7 @@ structure CompletionItem where
insertTextMode? : InsertTextMode
additionalTextEdits? : TextEdit[]
commitCharacters? : string[]
command? : Command
-/
command? : Command -/
deriving FromJson, ToJson, Inhabited
structure CompletionList where

View File

@@ -76,7 +76,7 @@ partial def upsert (t : Trie α) (s : String) (f : Option αα) : Trie α :
let c := s.getUtf8Byte i h
if c == c'
then node1 v c' (loop (i + 1) t')
else
else
let t := insertEmpty (i + 1)
node v (.mk #[c, c']) #[t, t']
else
@@ -190,7 +190,7 @@ private partial def toStringAux {α : Type} : Trie α → List Format
| node1 _ c t =>
[ format (repr c), Format.group $ Format.nest 4 $ flip Format.joinSep Format.line $ toStringAux t ]
| node _ cs ts =>
List.flatten $ List.zipWith (fun c t =>
List.join $ List.zipWith (fun c t =>
[ format (repr c), (Format.group $ Format.nest 4 $ flip Format.joinSep Format.line $ toStringAux t) ]
) cs.toList ts.toList

View File

@@ -42,9 +42,8 @@ builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ←
def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) : IO Unit :=
builtinDeclRanges.modify (·.insert declName declRanges)
def addDeclarationRanges [Monad m] [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) : m Unit := do
unless declRangeExt.contains ( getEnv) declName do
modifyEnv fun env => declRangeExt.insert env declName declRanges
def addDeclarationRanges [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) : m Unit :=
modifyEnv fun env => declRangeExt.insert env declName declRanges
def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
return declRangeExt.find? ( getEnv) declName

View File

@@ -16,7 +16,7 @@ import Init.Data.String.Extra
namespace Lean
private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) IO.mkRef {}
builtin_initialize docStringExt : MapDeclarationExtension String mkMapDeclarationExtension
private builtin_initialize docStringExt : MapDeclarationExtension String mkMapDeclarationExtension
def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)

View File

@@ -42,7 +42,6 @@ import Lean.Elab.Notation
import Lean.Elab.Mixfix
import Lean.Elab.MacroRules
import Lean.Elab.BuiltinCommand
import Lean.Elab.BuiltinEvalCommand
import Lean.Elab.RecAppSyntax
import Lean.Elab.Eval
import Lean.Elab.Calc

View File

@@ -528,7 +528,7 @@ mutual
main
/--
Create a fresh metavariable for the implicit argument, add it to `f`, and then execute the main loop.
Create a fresh metavariable for the implicit argument, add it to `f`, and thn execute the main loop.
-/
private partial def addImplicitArg (argName : Name) : M Expr := do
let argType getArgExpectedType
@@ -777,7 +777,7 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
forallTelescopeReducing elimType fun xs type => do
let motive := type.getAppFn
let motiveArgs := type.getAppArgs
unless motive.isFVar && motiveArgs.size > 0 do
unless motive.isFVar do
throwError "unexpected eliminator resulting type{indentExpr type}"
let motiveType inferType motive
forallTelescopeReducing motiveType fun motiveParams motiveResultType => do
@@ -1118,17 +1118,9 @@ where
/-- Auxiliary inductive datatype that represents the resolution of an `LVal`. -/
inductive LValResolution where
/-- When applied to `f`, effectively expands to `BaseStruct.fieldName (self := Struct.toBase f)`.
This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied. -/
| projFn (baseStructName : Name) (structName : Name) (fieldName : Name)
/-- Similar to `projFn`, but for extracting field indexed by `idx`. Works for structure-like inductive types in general. -/
| projIdx (structName : Name) (idx : Nat)
/-- When applied to `f`, effectively expands to `constName ... (Struct.toBase f)`, with the argument placed in the correct
positional argument if possible, or otherwise as a named argument. The `Struct.toBase` is not present if `baseStructName == structName`,
in which case these do not need to be structures. Supports generalized field notation. -/
| const (baseStructName : Name) (structName : Name) (constName : Name)
/-- Like `const`, but with `fvar` instead of `constName`.
The `fullName` is the name of the recursive function, and `baseName` is the base name of the type to search for in the parameter list. -/
| localRec (baseName : Name) (fullName : Name) (fvar : Expr)
private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
@@ -1298,70 +1290,45 @@ private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool :=
else
return ( whnfR type).isAppOf baseName
/--
Auxiliary method for field notation. Tries to add `e` as a new argument to `args` or `namedArgs`.
This method first finds the parameter with a type of the form `(baseName ...)`.
When the parameter is found, if it an explicit one and `args` is big enough, we add `e` to `args`.
Otherwise, if there isn't another parameter with the same name, we add `e` to `namedArgs`.
/-- Auxiliary method for field notation. It tries to add `e` as a new argument to `args` or `namedArgs`.
This method first finds the parameter with a type of the form `(baseName ...)`.
When the parameter is found, if it an explicit one and `args` is big enough, we add `e` to `args`.
Otherwise, if there isn't another parameter with the same name, we add `e` to `namedArgs`.
Remark: `fullName` is the name of the resolved "field" access function. It is used for reporting errors
-/
private partial def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Array Arg) (namedArgs : Array NamedArg) (f : Expr) :
MetaM (Array Arg × Array NamedArg) := do
withoutModifyingState <| go f ( inferType f) 0 namedArgs (namedArgs.map (·.name)) true
where
/--
* `argIdx` is the position into `args` for the next place an explicit argument can be inserted.
* `remainingNamedArgs` keeps track of named arguments that haven't been visited yet,
for handling the case where multiple parameters have the same name.
* `unusableNamedArgs` keeps track of names that can't be used as named arguments. This is initialized with user-provided named arguments.
* `allowNamed` is whether or not to allow using named arguments.
Disabled after using `CoeFun` since those parameter names unlikely to be meaningful,
and otherwise whether dot notation works or not could feel random.
-/
go (f fType : Expr) (argIdx : Nat) (remainingNamedArgs : Array NamedArg) (unusableNamedArgs : Array Name) (allowNamed : Bool) := withIncRecDepth do
/- Use metavariables (rather than `forallTelescope`) to prevent `coerceToFunction?` from succeeding when multiple instances could apply -/
let (xs, bInfos, fType') forallMetaTelescope fType
let mut argIdx := argIdx
let mut remainingNamedArgs := remainingNamedArgs
let mut unusableNamedArgs := unusableNamedArgs
for x in xs, bInfo in bInfos do
let xDecl x.mvarId!.getDecl
if let some idx := remainingNamedArgs.findIdx? (·.name == xDecl.userName) then
/- If there is named argument with name `xDecl.userName`, then it is accounted for and we can't make use of it. -/
Remark: `fullName` is the name of the resolved "field" access function. It is used for reporting errors -/
private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Array Arg) (namedArgs : Array NamedArg) (fType : Expr)
: TermElabM (Array Arg × Array NamedArg) :=
forallTelescopeReducing fType fun xs _ => do
let mut argIdx := 0 -- position of the next explicit argument
let mut remainingNamedArgs := namedArgs
for h : i in [:xs.size] do
let x := xs[i]
let xDecl x.fvarId!.getDecl
/- If there is named argument with name `xDecl.userName`, then we skip it. -/
match remainingNamedArgs.findIdx? (fun namedArg => namedArg.name == xDecl.userName) with
| some idx =>
remainingNamedArgs := remainingNamedArgs.eraseIdx idx
else
if ( typeMatchesBaseName xDecl.type baseName) then
| none =>
let type := xDecl.type
if ( typeMatchesBaseName type baseName) then
/- We found a type of the form (baseName ...).
First, we check if the current argument is an explicit one,
and if the current explicit position "fits" at `args` (i.e., it must be ≤ arg.size) -/
if argIdx args.size && bInfo.isExplicit then
/- We can insert `e` as an explicit argument -/
and the current explicit position "fits" at `args` (i.e., it must be ≤ arg.size) -/
if argIdx args.size && xDecl.binderInfo.isExplicit then
/- We insert `e` as an explicit argument -/
return (args.insertAt! argIdx (Arg.expr e), namedArgs)
else
/- If we can't add `e` to `args`, we try to add it using a named argument, but this is only possible
if there isn't an argument with the same name occurring before it. -/
if !allowNamed || unusableNamedArgs.contains xDecl.userName then
throwError "\
invalid field notation, function '{fullName}' has argument with the expected type\
{indentExpr xDecl.type}\n\
but it cannot be used"
else
return (args, namedArgs.push { name := xDecl.userName, val := Arg.expr e })
/- Advance `argIdx` and update seen named arguments. -/
if bInfo.isExplicit then
/- If we can't add `e` to `args`, we try to add it using a named argument, but this is only possible
if there isn't an argument with the same name occurring before it. -/
for j in [:i] do
let prev := xs[j]!
let prevDecl prev.fvarId!.getDecl
if prevDecl.userName == xDecl.userName then
throwError "invalid field notation, function '{fullName}' has argument with the expected type{indentExpr type}\nbut it cannot be used"
return (args, namedArgs.push { name := xDecl.userName, val := Arg.expr e })
if xDecl.binderInfo.isExplicit then
-- advance explicit argument position
argIdx := argIdx + 1
unusableNamedArgs := unusableNamedArgs.push xDecl.userName
/- If named arguments aren't allowed, then it must still be possible to pass the value as an explicit argument.
Otherwise, we can abort now. -/
if allowNamed || argIdx args.size then
if let fType'@(.forallE ..) whnf fType' then
return go (mkAppN f xs) fType' argIdx remainingNamedArgs unusableNamedArgs allowNamed
if let some f' coerceToFunction? (mkAppN f xs) then
return go f' ( inferType f') argIdx remainingNamedArgs unusableNamedArgs false
throwError "\
invalid field notation, function '{fullName}' does not have argument with type ({baseName} ...) that can be used, \
it must be explicit or implicit with a unique name"
throwError "invalid field notation, function '{fullName}' does not have argument with type ({baseName} ...) that can be used, it must be explicit or implicit with a unique name"
/-- Adds the `TermInfo` for the field of a projection. See `Lean.Parser.Term.identProjKind`. -/
private def addProjTermInfo
@@ -1408,7 +1375,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
let projFn mkConst constName
let projFn addProjTermInfo lval.getRef projFn
if lvals.isEmpty then
let (args, namedArgs) addLValArg baseStructName constName f args namedArgs projFn
let projFnType inferType projFn
let (args, namedArgs) addLValArg baseStructName constName f args namedArgs projFnType
elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
else
let f elabAppArgs projFn #[] #[Arg.expr f] (expectedType? := none) (explicit := false) (ellipsis := false)
@@ -1416,7 +1384,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
| LValResolution.localRec baseName fullName fvar =>
let fvar addProjTermInfo lval.getRef fvar
if lvals.isEmpty then
let (args, namedArgs) addLValArg baseName fullName f args namedArgs fvar
let fvarType inferType fvar
let (args, namedArgs) addLValArg baseName fullName f args namedArgs fvarType
elabAppArgs fvar namedArgs args expectedType? explicit ellipsis
else
let f elabAppArgs fvar #[] #[Arg.expr f] (expectedType? := none) (explicit := false) (ellipsis := false)
@@ -1425,6 +1394,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
private def elabAppLVals (f : Expr) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg)
(expectedType? : Option Expr) (explicit ellipsis : Bool) : TermElabM Expr := do
if !lvals.isEmpty && explicit then
throwError "invalid use of field notation with `@` modifier"
elabAppLValsAux namedArgs args expectedType? explicit ellipsis f lvals
def elabExplicitUnivs (lvls : Array Syntax) : TermElabM (List Level) := do
@@ -1523,21 +1494,19 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
withReader (fun ctx => { ctx with errToSorry := false }) do
f.getArgs.foldlM (init := acc) fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc
else
let elabFieldName (e field : Syntax) (explicit : Bool) := do
let elabFieldName (e field : Syntax) := do
let newLVals := field.identComponents.map fun comp =>
-- We use `none` in `suffix?` since `field` can't be part of a composite name
LVal.fieldName comp comp.getId.getString! none f
elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
let elabFieldIdx (e idxStx : Syntax) (explicit : Bool) := do
let elabFieldIdx (e idxStx : Syntax) := do
let some idx := idxStx.isFieldIdx? | throwError "invalid field index"
elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
match f with
| `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit
| `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit
| `($(e).$field:ident) => elabFieldName e field explicit
| `($e |>.$field:ident) => elabFieldName e field explicit
| `(@$(e).$idx:fieldIdx) => elabFieldIdx e idx (explicit := true)
| `(@$(e).$field:ident) => elabFieldName e field (explicit := true)
| `($(e).$idx:fieldIdx) => elabFieldIdx e idx
| `($e |>.$idx:fieldIdx) => elabFieldIdx e idx
| `($(e).$field:ident) => elabFieldName e field
| `($e |>.$field:ident) => elabFieldName e field
| `($_:ident@$_:term) =>
throwError "unexpected occurrence of named pattern"
| `($id:ident) => do
@@ -1694,10 +1663,8 @@ private def elabAtom : TermElab := fun stx expectedType? => do
@[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
match stx with
| `(@$_:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@`
| `(@$_:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@`
| `(@$_:ident.{$_us,*}) => elabAtom stx expectedType?
| `(@$(_).$_:fieldIdx) => elabAtom stx expectedType?
| `(@$(_).$_:ident) => elabAtom stx expectedType?
| `(@($t)) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas
| `(@$t) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas
| _ => throwUnsupportedSyntax

View File

@@ -311,6 +311,167 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
failIfSucceeds <| elabCheckCore (ignoreStuckTC := false) ( `(#check $term))
| _ => throwUnsupportedSyntax
private def mkEvalInstCore (evalClassName : Name) (e : Expr) : MetaM Expr := do
let α inferType e
let u getDecLevel α
let inst := mkApp (Lean.mkConst evalClassName [u]) α
try
synthInstance inst
catch _ =>
-- Put `α` in WHNF and try again
try
let α whnf α
synthInstance (mkApp (Lean.mkConst evalClassName [u]) α)
catch _ =>
-- Fully reduce `α` and try again
try
let α reduce (skipTypes := false) α
synthInstance (mkApp (Lean.mkConst evalClassName [u]) α)
catch _ =>
throwError "expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class"
private def mkRunMetaEval (e : Expr) : MetaM Expr :=
withLocalDeclD `env (mkConst ``Lean.Environment) fun env =>
withLocalDeclD `opts (mkConst ``Lean.Options) fun opts => do
let α inferType e
let u getDecLevel α
let instVal mkEvalInstCore ``Lean.MetaEval e
let e := mkAppN (mkConst ``Lean.runMetaEval [u]) #[α, instVal, env, opts, e]
instantiateMVars ( mkLambdaFVars #[env, opts] e)
private def mkRunEval (e : Expr) : MetaM Expr := do
let α inferType e
let u getDecLevel α
let instVal mkEvalInstCore ``Lean.Eval e
instantiateMVars (mkAppN (mkConst ``Lean.runEval [u]) #[α, instVal, mkSimpleThunk e])
unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax): CommandElabM Unit := do
let declName := `_eval
let addAndCompile (value : Expr) : TermElabM Unit := do
let value Term.levelMVarToParam ( instantiateMVars value)
let type inferType value
let us := collectLevelParams {} value |>.params
let value instantiateMVars value
let decl := Declaration.defnDecl {
name := declName
levelParams := us.toList
type := type
value := value
hints := ReducibilityHints.opaque
safety := DefinitionSafety.unsafe
}
Term.ensureNoUnassignedMVars decl
addAndCompile decl
-- Check for sorry axioms
let checkSorry (declName : Name) : MetaM Unit := do
unless bang do
let axioms collectAxioms declName
if axioms.contains ``sorryAx then
throwError ("cannot evaluate expression that depends on the `sorry` axiom.\nUse `#eval!` to " ++
"evaluate nevertheless (which may cause lean to crash).")
-- Elaborate `term`
let elabEvalTerm : TermElabM Expr := do
let e Term.elabTerm term none
Term.synthesizeSyntheticMVarsNoPostponing
if ( Term.logUnassignedUsingErrorInfos ( getMVars e)) then throwAbortTerm
if ( isProp e) then
mkDecide e
else
return e
-- Evaluate using term using `MetaEval` class.
let elabMetaEval : CommandElabM Unit := do
-- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
-- we don't pollute the environment with auxliary declarations.
-- We have special support for `CommandElabM` to ensure `#eval` can be used to execute commands
-- that modify `CommandElabM` state not just the `Environment`.
let act : Sum (CommandElabM Unit) (Environment Options IO (String × Except IO.Error Environment))
runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
let e elabEvalTerm
let eType instantiateMVars ( inferType e)
if eType.isAppOfArity ``CommandElabM 1 then
let mut stx Term.exprToSyntax e
unless ( isDefEq eType.appArg! (mkConst ``Unit)) do
stx `($stx >>= fun v => IO.println (repr v))
let act Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx
pure <| Sum.inl act
else
let e mkRunMetaEval e
addAndCompile e
checkSorry declName
let act evalConst (Environment Options IO (String × Except IO.Error Environment)) declName
pure <| Sum.inr act
match act with
| .inl act => act
| .inr act =>
let (out, res) act ( getEnv) ( getOptions)
logInfoAt tk out
match res with
| Except.error e => throwError e.toString
| Except.ok env => setEnv env; pure ()
-- Evaluate using term using `Eval` class.
let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
-- fall back to non-meta eval if MetaEval hasn't been defined yet
-- modify e to `runEval e`
let e mkRunEval ( elabEvalTerm)
addAndCompile e
checkSorry declName
let act evalConst (IO (String × Except IO.Error Unit)) declName
let (out, res) liftM (m := IO) act
logInfoAt tk out
match res with
| Except.error e => throwError e.toString
| Except.ok _ => pure ()
if ( getEnv).contains ``Lean.MetaEval then do
elabMetaEval
else
elabEval
@[implemented_by elabEvalCoreUnsafe]
opaque elabEvalCore (bang : Bool) (tk term : Syntax): CommandElabM Unit
@[builtin_command_elab «eval»]
def elabEval : CommandElab
| `(#eval%$tk $term) => elabEvalCore false tk term
| _ => throwUnsupportedSyntax
@[builtin_command_elab evalBang]
def elabEvalBang : CommandElab
| `(Parser.Command.evalBang|#eval!%$tk $term) => elabEvalCore true tk term
| _ => throwUnsupportedSyntax
private def checkImportsForRunCmds : CommandElabM Unit := do
unless ( getEnv).contains ``CommandElabM do
throwError "to use this command, include `import Lean.Elab.Command`"
@[builtin_command_elab runCmd]
def elabRunCmd : CommandElab
| `(run_cmd $elems:doSeq) => do
checkImportsForRunCmds
( liftTermElabM <| Term.withDeclName `_run_cmd <|
unsafe Term.evalTerm (CommandElabM Unit)
(mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
( `(discard do $elems)))
| _ => throwUnsupportedSyntax
@[builtin_command_elab runElab]
def elabRunElab : CommandElab
| `(run_elab $elems:doSeq) => do
checkImportsForRunCmds
( liftTermElabM <| Term.withDeclName `_run_elab <|
unsafe Term.evalTerm (CommandElabM Unit)
(mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
( `(Command.liftTermElabM <| discard do $elems)))
| _ => throwUnsupportedSyntax
@[builtin_command_elab runMeta]
def elabRunMeta : CommandElab := fun stx =>
match stx with
| `(run_meta $elems:doSeq) => do
checkImportsForRunCmds
let stxNew `(command| run_elab (show Lean.Meta.MetaM Unit from do $elems))
withMacroExpansion stx stxNew do elabCommand stxNew
| _ => throwUnsupportedSyntax
@[builtin_command_elab «synth»] def elabSynth : CommandElab := fun stx => do
let term := stx[1]
withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_synth_cmd do

View File

@@ -1,277 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kyle Miller
-/
prelude
import Lean.Util.CollectAxioms
import Lean.Elab.Deriving.Basic
import Lean.Elab.MutualDef
/-!
# Implementation of `#eval` command
-/
namespace Lean.Elab.Command
open Meta
register_builtin_option eval.pp : Bool := {
defValue := true
descr := "('#eval' command) enables using 'ToExpr' instances to pretty print the result, \
otherwise uses 'Repr' or 'ToString' instances"
}
register_builtin_option eval.type : Bool := {
defValue := false -- TODO: set to 'true'
descr := "('#eval' command) enables pretty printing the type of the result"
}
register_builtin_option eval.derive.repr : Bool := {
defValue := true
descr := "('#eval' command) enables auto-deriving 'Repr' instances as a fallback"
}
builtin_initialize
registerTraceClass `Elab.eval
/--
Elaborates the term, ensuring the result has no expression metavariables.
If there would be unsolved-for metavariables, tries hinting that the resulting type
is a monadic value with the `CommandElabM`, `TermElabM`, or `IO` monads.
Throws errors if the term is a proof or a type, but lifts props to `Bool` using `mkDecide`.
-/
private def elabTermForEval (term : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
let ty expectedType?.getDM mkFreshTypeMVar
let e Term.elabTermEnsuringType term ty
synthesizeWithHinting ty
let e instantiateMVars e
if ( Term.logUnassignedUsingErrorInfos ( getMVars e)) then throwAbortTerm
if isProof e then
throwError m!"cannot evaluate, proofs are not computationally relevant"
let e if ( isProp e) then mkDecide e else pure e
if isType e then
throwError m!"cannot evaluate, types are not computationally relevant"
trace[Elab.eval] "elaborated term:{indentExpr e}"
return e
where
/-- Try different strategies to make `Term.synthesizeSyntheticMVarsNoPostponing` succeed. -/
synthesizeWithHinting (ty : Expr) : TermElabM Unit := do
Term.synthesizeSyntheticMVarsUsingDefault
let s saveState
try
Term.synthesizeSyntheticMVarsNoPostponing
catch ex =>
let exS saveState
-- Try hinting that `ty` is a monad application.
for m in #[``CommandElabM, ``TermElabM, ``IO] do
s.restore true
try
if isDefEq ty ( mkFreshMonadApp m) then
Term.synthesizeSyntheticMVarsNoPostponing
return
catch _ => pure ()
-- None of the hints worked, so throw the original error.
exS.restore true
throw ex
mkFreshMonadApp (n : Name) : MetaM Expr := do
let m mkConstWithFreshMVarLevels n
let (args, _, _) forallMetaBoundedTelescope ( inferType m) 1
return mkAppN m args
private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorry := false) : TermElabM Unit := do
-- Use the `elabMutualDef` machinery to be able to support `let rec`.
-- Hack: since we are using the `TermElabM` version, we can insert the `value` as a metavariable via `exprToSyntax`.
-- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once
-- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages
-- such as "failed to infer definition type" can surface.
let defView := mkDefViewOfDef { isUnsafe := true }
( `(Parser.Command.definition|
def $(mkIdent <| `_root_ ++ declName) := $( Term.exprToSyntax value)))
Term.elabMutualDef #[] { header := "" } #[defView]
unless allowSorry do
let axioms collectAxioms declName
if axioms.contains ``sorryAx then
throwError "\
aborting evaluation since the expression depends on the 'sorry' axiom, \
which can lead to runtime instability and crashes.\n\n\
To attempt to evaluate anyway despite the risks, use the '#eval!' command."
/--
Try to make a `@projFn ty inst e` application, even if it takes unfolding the type `ty` of `e` to synthesize the instance `inst`.
-/
private partial def mkDeltaInstProj (inst projFn : Name) (e : Expr) (ty? : Option Expr := none) (tryReduce : Bool := true) : MetaM Expr := do
let ty ty?.getDM (inferType e)
if let .some inst trySynthInstance ( mkAppM inst #[ty]) then
mkAppOptM projFn #[ty, inst, e]
else
let ty whnfCore ty
let some ty unfoldDefinition? ty
| guard tryReduce
-- Reducing the type is a strategy `#eval` used before the refactor of #5627.
-- The test lean/run/hlistOverload.lean depends on it, so we preserve the behavior.
let ty reduce (skipTypes := false) ty
mkDeltaInstProj inst projFn e ty (tryReduce := false)
mkDeltaInstProj inst projFn e ty tryReduce
/-- Try to make a `toString e` application, even if it takes unfolding the type of `e` to find a `ToString` instance. -/
private def mkToString (e : Expr) (ty? : Option Expr := none) : MetaM Expr := do
mkDeltaInstProj ``ToString ``toString e ty?
/-- Try to make a `repr e` application, even if it takes unfolding the type of `e` to find a `Repr` instance. -/
private def mkRepr (e : Expr) (ty? : Option Expr := none) : MetaM Expr := do
mkDeltaInstProj ``Repr ``repr e ty?
/-- Try to make a `toExpr e` application, even if it takes unfolding the type of `e` to find a `ToExpr` instance. -/
private def mkToExpr (e : Expr) (ty? : Option Expr := none) : MetaM Expr := do
mkDeltaInstProj ``ToExpr ``toExpr e ty?
/--
Returns a representation of `e` using `Format`, or else fails.
If the `eval.derive.repr` option is true, then tries automatically deriving a `Repr` instance first.
Currently auto-derivation does not attempt to derive recursively.
-/
private def mkFormat (e : Expr) : MetaM Expr := do
mkRepr e <|> (do mkAppM ``Std.Format.text #[ mkToString e])
<|> do
if eval.derive.repr.get ( getOptions) then
if let .const name _ := ( whnf ( inferType e)).getAppFn then
try
trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{MessageData.ofConstName name}'"
liftCommandElabM do applyDerivingHandlers ``Repr #[name] none
resetSynthInstanceCache
return mkRepr e
catch ex =>
trace[Elab.eval] "Failed to use derived 'Repr' instance. Exception: {ex.toMessageData}"
throwError m!"could not synthesize a 'Repr' or 'ToString' instance for type{indentExpr (← inferType e)}"
/--
Returns a representation of `e` using `MessageData`, or else fails.
Tries `mkFormat` if a `ToExpr` instance can't be synthesized.
-/
private def mkMessageData (e : Expr) : MetaM Expr := do
(do guard <| eval.pp.get ( getOptions); mkAppM ``MessageData.ofExpr #[ mkToExpr e])
<|> (return mkApp (mkConst ``MessageData.ofFormat) ( mkFormat e))
<|> do throwError m!"could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type{indentExpr (← inferType e)}"
private structure EvalAction where
eval : CommandElabM MessageData
/-- Whether to print the result of evaluation.
If `some`, the expression is what type to use for the type ascription when `pp.type` is true. -/
printVal : Option Expr
unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) : CommandElabM Unit := withRef tk do
let declName := `_eval
-- `t` is either `MessageData` or `Format`, and `mkT` is for synthesizing an expression that yields a `t`.
-- The `toMessageData` function adapts `t` to `MessageData`.
let mkAct {t : Type} [Inhabited t] (toMessageData : t MessageData) (mkT : Expr MetaM Expr) (e : Expr) : TermElabM EvalAction := do
-- Create a monadic action given the name of the monad `mc`, the monad `m` itself,
-- and an expression `e` to evaluate in this monad.
-- A trick here is that `mkMAct?` makes use of `MonadEval` instances are currently available in this stage,
-- and we do not need them to be available in the target environment.
let mkMAct? (mc : Name) (m : Type Type) [Monad m] [MonadEvalT m CommandElabM] (e : Expr) : TermElabM (Option EvalAction) := do
let some e observing? (mkAppOptM ``MonadEvalT.monadEval #[none, mkConst mc, none, none, e])
| return none
let eType := e.appFn!.appArg!
if isDefEq eType (mkConst ``Unit) then
addAndCompileExprForEval declName e (allowSorry := bang)
let mf : m Unit evalConst (m Unit) declName
return some { eval := do MonadEvalT.monadEval mf; pure "", printVal := none }
else
let rf withLocalDeclD `x eType fun x => do mkLambdaFVars #[x] ( mkT x)
let r mkAppM ``Functor.map #[rf, e]
addAndCompileExprForEval declName r (allowSorry := bang)
let mf : m t evalConst (m t) declName
return some { eval := toMessageData <$> MonadEvalT.monadEval mf, printVal := some eType }
if let some act mkMAct? ``CommandElabM CommandElabM e
-- Fallbacks in case we are in the Lean package but don't have `CommandElabM` yet
<||> mkMAct? ``TermElabM TermElabM e <||> mkMAct? ``MetaM MetaM e <||> mkMAct? ``CoreM CoreM e
-- Fallback in case nothing is imported
<||> mkMAct? ``IO IO e then
return act
else
-- Otherwise, assume this is a pure value.
-- There is no need to adapt pure values to `CommandElabM`.
-- This enables `#eval` to work on pure values even when `CommandElabM` is not available.
let r try mkT e catch ex => do
-- Diagnose whether the value is monadic for a representable value, since it's better to mention `MonadEval` in that case.
try
let some (m, ty) isTypeApp? ( inferType e) | failure
guard <| ( isMonad? m).isSome
-- Verify that there is a way to form some representation:
discard <| withLocalDeclD `x ty fun x => mkT x
catch _ =>
throw ex
throwError m!"unable to synthesize '{MessageData.ofConstName ``MonadEval}' instance \
to adapt{indentExpr (← inferType e)}\n\
to '{MessageData.ofConstName ``IO}' or '{MessageData.ofConstName ``CommandElabM}'."
addAndCompileExprForEval declName r (allowSorry := bang)
-- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below.
let r toMessageData <$> evalConst t declName
return { eval := pure r, printVal := some ( inferType e) }
let (output, exOrRes) IO.FS.withIsolatedStreams do
try
-- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
-- we don't pollute the environment with auxiliary declarations.
let act : EvalAction liftTermElabM do Term.withDeclName declName do withoutModifyingEnv do
let e elabTermForEval term expectedType?
-- If there is an elaboration error, don't evaluate!
if e.hasSyntheticSorry then throwAbortTerm
-- We want `#eval` to work even in the core library, so if `ofFormat` isn't available,
-- we fall back on a `Format`-based approach.
if ( getEnv).contains ``Lean.MessageData.ofFormat then
mkAct id (mkMessageData ·) e
else
mkAct Lean.MessageData.ofFormat (mkFormat ·) e
let res act.eval
return Sum.inr (res, act.printVal)
catch ex =>
return Sum.inl ex
if !output.isEmpty then logInfoAt tk output
match exOrRes with
| .inl ex => logException ex
| .inr (_, none) => pure ()
| .inr (res, some type) =>
if eval.type.get ( getOptions) then
logInfo m!"{res} : {type}"
else
logInfo res
@[implemented_by elabEvalCoreUnsafe]
opaque elabEvalCore (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) : CommandElabM Unit
@[builtin_command_elab «eval»]
def elabEval : CommandElab
| `(#eval%$tk $term) => elabEvalCore false tk term none
| _ => throwUnsupportedSyntax
@[builtin_command_elab evalBang]
def elabEvalBang : CommandElab
| `(#eval!%$tk $term) => elabEvalCore true tk term none
| _ => throwUnsupportedSyntax
@[builtin_command_elab runCmd]
def elabRunCmd : CommandElab
| `(run_cmd%$tk $elems:doSeq) => do
unless ( getEnv).contains ``CommandElabM do
throwError "to use this command, include `import Lean.Elab.Command`"
elabEvalCore false tk ( `(discard do $elems)) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
| _ => throwUnsupportedSyntax
@[builtin_command_elab runElab]
def elabRunElab : CommandElab
| `(run_elab%$tk $elems:doSeq) => do
unless ( getEnv).contains ``TermElabM do
throwError "to use this command, include `import Lean.Elab.Term`"
elabEvalCore false tk ( `(discard do $elems)) (mkApp (mkConst ``TermElabM) (mkConst ``Unit))
| _ => throwUnsupportedSyntax
@[builtin_command_elab runMeta]
def elabRunMeta : CommandElab := fun stx =>
match stx with
| `(run_meta%$tk $elems:doSeq) => do
unless ( getEnv).contains ``MetaM do
throwError "to use this command, include `import Lean.Meta.Basic`"
elabEvalCore false tk ( `(discard do $elems)) (mkApp (mkConst ``MetaM) (mkConst ``Unit))
| _ => throwUnsupportedSyntax
end Lean.Elab.Command

View File

@@ -103,11 +103,9 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
@[builtin_term_elab Lean.Parser.Term.omission] def elabOmission : TermElab := fun stx expectedType? => do
logWarning m!"\
The '⋯' token is used by the pretty printer to indicate omitted terms, and it should not be used directly. \
It logs this warning and then elaborates like '_'.\
\n\n\
The presence of '⋯' in pretty printing output is controlled by the 'pp.maxSteps', 'pp.deepTerms' and 'pp.proofs' options. \
These options can be further adjusted using 'pp.deepTerms.threshold' and 'pp.proofs.threshold'. \
If this '⋯' was copied from the Infoview, the hover there for the original '⋯' explains which of these options led to the omission."
It logs this warning and then elaborates like `_`.\
\n\nThe presence of `⋯` in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. \
These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`."
elabHole stx expectedType?
@[builtin_term_elab «letMVar»] def elabLetMVar : TermElab := fun stx expectedType? => do

View File

@@ -520,12 +520,8 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
-- recovery more coarse. In particular, If `c` in `set_option ... in $c` fails, the remaining
-- `end` command of the `in` macro would be skipped and the option would be leaked to the outside!
elabCommand stx
-- Run the linters, unless `#guard_msgs` is present, which is special and runs `elabCommandTopLevel` itself,
-- so it is a "super-top-level" command. This is the only command that does this, so we just special case it here
-- rather than engineer a general solution.
unless (stx.find? (·.isOfKind ``Lean.guardMsgsCmd)).isSome do
withLogging do
runLinters stx
withLogging do
runLinters stx
finally
-- note the order: first process current messages & info trees, then add back old messages & trees,
-- then convert new traces to messages
@@ -619,9 +615,6 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
let ((ea, _), _) runCore x
MonadExcept.ofExcept ea
instance : MonadEval TermElabM CommandElabM where
monadEval := liftTermElabM
/--
Execute the monadic action `elabFn xs` as a `CommandElabM` monadic action, where `xs` are free variables
corresponding to all active scoped variables declared using the `variable` command.
@@ -730,12 +723,6 @@ Commands that modify the processing of subsequent commands,
such as `open` and `namespace` commands,
only have an effect for the remainder of the `CommandElabM` computation passed here,
and do not affect subsequent commands.
*Warning:* when using this from `MetaM` monads, the caches are *not* reset.
If the command defines new instances for example, you should use `Lean.Meta.resetSynthInstanceCache`
to reset the instance cache.
While the `modifyEnv` function for `MetaM` clears its caches entirely,
`liftCommandElabM` has no way to reset these caches.
-/
def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
let (a, commandState)

View File

@@ -136,8 +136,8 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
/-
leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
leading_parser "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor >> optDeriving
-/
private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
checkValidInductiveModifier modifiers
@@ -167,10 +167,6 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
let computedFields (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := cf[3], matchAlts := cf[4] }
let classes liftCoreM <| getOptDerivingClasses decl[6]
if decl[3][0].isToken ":=" then
-- https://github.com/leanprover/lean4/issues/5236
withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
"'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
return {
ref := decl
shortDeclName := name
@@ -386,28 +382,19 @@ def elabMutual : CommandElab := fun stx => do
for attrName in toErase do
Attribute.erase declName attrName
@[builtin_command_elab Lean.Parser.Command.«initialize»] def elabInitialize : CommandElab
@[builtin_macro Lean.Parser.Command.«initialize»] def expandInitialize : Macro
| stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ]? $doSeq) => do
let attrId := mkIdentFrom stx <| if kw.raw[0].isToken "initialize" then `init else `builtin_init
if let (some id, some type) := (id?, type?) then
let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(vis?)? $[unsafe%$unsafe?]?) := stx[0]
| throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
let defStx `($[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ),*] $(vis?)? opaque $id : $type)
let mut fullId := ( getCurrNamespace) ++ id.getId
if vis?.any (·.raw.isOfKind ``Parser.Command.private) then
fullId := mkPrivateName ( getEnv) fullId
-- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
-- otherwise the info context created by `with_decl_name` will be incomplete and break the
-- call hierarchy
addDeclarationRanges fullId defStx
elabCommand ( `(
$[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
$defStx:command))
| Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
`($[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% ?$id do $doSeq
$[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ),*] $(vis?)? opaque $id : $type)
else
let `(Parser.Command.declModifiersT| $[$doc?:docComment]? ) := declModifiers
| throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
elabCommand ( `($[$doc?:docComment]? @[$attrId:ident] def initFn : IO Unit := do $doSeq))
| _ => throwUnsupportedSyntax
| Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
`($[$doc?:docComment]? @[$attrId:ident] def initFn : IO Unit := do $doSeq)
| _ => Macro.throwUnsupported
builtin_initialize
registerTraceClass `Elab.axiom

View File

@@ -36,7 +36,7 @@ def mkToJsonBodyForStruct (header : Header) (indName : Name) : TermElabM Term :=
let target := mkIdent header.targetNames[0]!
if isOptField then ``(opt $nm $target.$(mkIdent field))
else ``([($nm, toJson ($target).$(mkIdent field))])
`(mkObj <| List.flatten [$fields,*])
`(mkObj <| List.join [$fields,*])
def mkToJsonBodyForInduct (ctx : Context) (header : Header) (indName : Name) : TermElabM Term := do
let indVal getConstInfoInduct indName

View File

@@ -140,7 +140,6 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
|>.trim |> removeTrailingWhitespaceMarker
let (whitespace, ordering, specFn) parseGuardMsgsSpec spec?
let initMsgs modifyGet fun st => (st.messages, { st with messages := {} })
-- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once.
elabCommandTopLevel cmd
let msgs := ( get).messages
let mut toCheck : MessageLog := .empty

View File

@@ -425,9 +425,9 @@ where
levelMVarToParam' (type : Expr) : TermElabM Expr := do
Term.levelMVarToParam type (except := fun mvarId => univToInfer? == some mvarId)
def mkResultUniverse (us : Array Level) (rOffset : Nat) (preferProp : Bool) : Level :=
def mkResultUniverse (us : Array Level) (rOffset : Nat) : Level :=
if us.isEmpty && rOffset == 0 then
if preferProp then levelZero else levelOne
levelOne
else
let r := Level.mkNaryMax us.toList
if rOffset == 0 && !r.isZero && !r.isNeverZero then
@@ -512,31 +512,6 @@ where
for ctorParam in ctorParams[numParams:] do
accLevelAtCtor ctor ctorParam r rOffset
/--
Decides whether the inductive type should be `Prop`-valued when the universe is not given
and when the universe inference algorithm `collectUniverses` determines
that the inductive type could naturally be `Prop`-valued.
Recall: the natural universe level is the mimimum universe level for all the types of all the constructor parameters.
Heuristic:
- We want `Prop` when each inductive type is a syntactic subsingleton.
That's to say, when each inductive type has at most one constructor.
Such types carry no data anyway.
- Exception: if no inductive type has any constructors, these are likely stubbed-out declarations,
so we prefer `Type` instead.
- Exception: if each constructor has no parameters, then these are likely partially-written enumerations,
so we prefer `Type` instead.
-/
private def isPropCandidate (numParams : Nat) (indTypes : List InductiveType) : MetaM Bool := do
unless indTypes.foldl (fun n indType => max n indType.ctors.length) 0 == 1 do
return false
for indType in indTypes do
for ctor in indType.ctors do
let cparams forallTelescopeReducing ctor.type fun ctorParams _ => pure (ctorParams.size - numParams)
unless cparams == 0 do
return true
return false
private def updateResultingUniverse (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) := do
let r getResultingUniverse indTypes
let rOffset : Nat := r.getOffset
@@ -545,7 +520,7 @@ private def updateResultingUniverse (views : Array InductiveView) (numParams : N
throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly: {r}"
let us collectUniverses views r rOffset numParams indTypes
trace[Elab.inductive] "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}"
let rNew := mkResultUniverse us rOffset ( isPropCandidate numParams indTypes)
let rNew := mkResultUniverse us rOffset
assignLevelMVar r.mvarId! rNew
indTypes.mapM fun indType => do
let type instantiateMVars indType.type
@@ -770,7 +745,7 @@ private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array Ind
forallBoundedTelescope indTypes[0]!.type numParams fun params type => do
let otherTypes indTypes[1:].toArray.mapM fun indType => do whnfD ( instantiateForall indType.type params)
let ctorTypes indTypes.toList.mapM fun indType => indType.ctors.mapM fun ctor => do whnfD ( instantiateForall ctor.type params)
let typesToCheck := otherTypes.toList ++ ctorTypes.flatten
let typesToCheck := otherTypes.toList ++ ctorTypes.join
let rec go (i : Nat) (type : Expr) (typesToCheck : List Expr) : MetaM Nat := do
if i < mask.size then
if !masks.all fun mask => i < mask.size && mask[i]! then

View File

@@ -83,7 +83,7 @@ inductive CompletionInfo where
| namespaceId (stx : Syntax)
| option (stx : Syntax)
| endSection (stx : Syntax) (scopeNames : List String)
| tactic (stx : Syntax)
| tactic (stx : Syntax) (goals : List MVarId)
-- TODO `import`
/-- Info for an option reference (e.g. in `set_option`). -/

View File

@@ -473,10 +473,7 @@ private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName
def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
if (findField? ( getEnv) structName fieldName).isNone then
return none
return some <|
mkNode ``Parser.Term.explicit
#[mkAtomFrom s "@",
mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]]
return some <| mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]
def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
fields.find? fun field =>
@@ -688,7 +685,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
let type := (d.getArg! 0).consumeTypeAnnotations
let mvar mkTacticMVar type stx (.fieldAutoParam fieldName s.structName)
-- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`.
-- (See the aforementioned `processExplicitArg` for a comment about this.)
-- (See the aformentioned `processExplicitArg` for a comment about this.)
addTermInfo' stx mvar
cont mvar field
| _ =>

View File

@@ -137,12 +137,7 @@ def structSimpleBinder := leading_parser atomic (declModifiers true >> ident)
def structFields := leading_parser many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
```
-/
private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM (Array StructFieldView) := do
if structStx[5][0].isToken ":=" then
-- https://github.com/leanprover/lean4/issues/5236
let cmd := if structStx[0].getKind == ``Parser.Command.classTk then "class" else "structure"
withRef structStx[0] <| Linter.logLintIf Linter.linter.deprecated structStx[5][0]
s!"{cmd} ... :=' has been deprecated in favor of '{cmd} ... where'."
private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM (Array StructFieldView) :=
let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs
fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
let mut fieldBinder := fieldBinder
@@ -637,19 +632,6 @@ where
msg := msg ++ "\nrecall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the structure resulting universe level"
throwError msg
/--
Decides whether the structure should be `Prop`-valued when the universe is not given
and when the universe inference algorithm `collectUniversesFromFields` determines
that the inductive type could naturally be `Prop`-valued.
See `Lean.Elab.Command.isPropCandidate` for an explanation.
Specialized to structures, the heuristic is that we prefer a `Prop` instead of a `Type` structure
when it could be a syntactic subsingleton.
Exception: no-field structures are `Type` since they are likely stubbed-out declarations.
-/
private def isPropCandidate (fieldInfos : Array StructFieldInfo) : Bool :=
!fieldInfos.isEmpty
private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type : Expr) : TermElabM Expr := do
let r getResultUniverse type
let rOffset : Nat := r.getOffset
@@ -657,7 +639,7 @@ private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type :
match r with
| Level.mvar mvarId =>
let us collectUniversesFromFields r rOffset fieldInfos
let rNew := mkResultUniverse us rOffset (isPropCandidate fieldInfos)
let rNew := mkResultUniverse us rOffset
assignLevelMVar mvarId rNew
instantiateMVars type
| _ => throwError "failed to compute resulting universe level of structure, provide universe explicitly"
@@ -884,8 +866,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
addDefaults lctx defaultAuxDecls
/-
leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >>
optional (("where" <|> ":=") >> optional structCtor >> structFields) >> optDeriving
leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields >> optDeriving
where
def «extends» := leading_parser " extends " >> sepBy1 termParser ", "

View File

@@ -43,4 +43,3 @@ import Lean.Elab.Tactic.Rewrites
import Lean.Elab.Tactic.DiscrTreeKey
import Lean.Elab.Tactic.BVDecide
import Lean.Elab.Tactic.BoolToPropSimps
import Lean.Elab.Tactic.Classical

View File

@@ -169,9 +169,8 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro
let out? runInterruptible timeout { cmd, args, stdin := .piped, stdout := .piped, stderr := .null }
match out? with
| .timeout =>
let mut err := "The SAT solver timed out while solving the problem.\n"
err := err ++ "Consider increasing the timeout with `set_option sat.timeout <sec>`.\n"
err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option."
let mut err := "The SAT solver timed out while solving the problem."
err := err ++ "\nConsider increasing the timeout with `set_option sat.timeout <sec>`"
throwError err
| .success { exitCode := exitCode, stdout := stdout, stderr := stderr} =>
if exitCode == 255 then

View File

@@ -52,11 +52,6 @@ register_builtin_option debug.bv.graphviz : Bool := {
descr := "Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the Lean process."
}
register_builtin_option bv.ac_nf : Bool := {
defValue := false
descr := "Canonicalize with respect to associativity and commutativitiy."
}
builtin_initialize bvNormalizeExt : Meta.SimpExtension
Meta.registerSimpAttr `bv_normalize "simp theorems used by bv_normalize"

View File

@@ -41,7 +41,7 @@ def lratChecker (cfg : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := d
@[inherit_doc Lean.Parser.Tactic.bvCheck]
def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
let unsatProver : UnsatProver := fun _ reflectionResult _ => do
let unsatProver : UnsatProver := fun reflectionResult _ => do
withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
let proof lratChecker cfg reflectionResult.bvExpr
return .ok proof, ""
@@ -60,8 +60,8 @@ def evalBvCheck : Tactic := fun
| some g' => bvCheck g' cfg
| none =>
let bvNormalizeStx `(tactic| bv_normalize)
logWarning m!"This goal can be closed by only applying bv_normalize, no need to keep the LRAT proof around."
TryThis.addSuggestion tk bvNormalizeStx (origSpan? := getRef)
throwError m!"This goal can be closed by only applying bv_normalize, no need to keep the LRAT proof around."
| _ => throwUnsupportedSyntax
end Frontend.BVCheck

View File

@@ -83,10 +83,6 @@ structure ReflectionResult where
A counter example generated from the bitblaster.
-/
structure CounterExample where
/--
The goal in which to interpret this counter example.
-/
goal : MVarId
/--
The set of unused but potentially relevant hypotheses. Useful for diagnosing spurious counter
examples.
@@ -101,7 +97,7 @@ structure UnsatProver.Result where
proof : Expr
lratCert : LratCert
abbrev UnsatProver := MVarId ReflectionResult Std.HashMap Nat (Nat × Expr)
abbrev UnsatProver := ReflectionResult Std.HashMap Nat (Nat × Expr)
MetaM (Except CounterExample UnsatProver.Result)
/--
@@ -116,9 +112,8 @@ abbrev DiagnosisM : Type → Type := ReaderT CounterExample <| StateRefT Diagnos
namespace DiagnosisM
def run (x : DiagnosisM Unit) (counterExample : CounterExample) : MetaM Diagnosis := do
counterExample.goal.withContext do
let (_, issues) ReaderT.run x counterExample |>.run {}
return issues
let (_, issues) ReaderT.run x counterExample |>.run {}
return issues
def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
return ( read).unusedHypotheses
@@ -182,7 +177,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
err := err ++ m!"Consider the following assignment:\n"
return err
def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult)
def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
(atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
MetaM (Except CounterExample UnsatProver.Result) := do
let bvExpr := reflectionResult.bvExpr
@@ -211,13 +206,11 @@ def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : Ref
match res with
| .ok cert =>
trace[Meta.Tactic.sat] "SAT solver found a proof."
let proof cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
return .ok proof, cert
| .error assignment =>
trace[Meta.Tactic.sat] "SAT solver found a counter example."
let equations := reconstructCounterExample map assignment aigSize atomsAssignment
return .error { goal, unusedHypotheses := reflectionResult.unusedHypotheses, equations }
return .error { unusedHypotheses := reflectionResult.unusedHypotheses, equations }
def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
@@ -255,7 +248,7 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
let atomsPairs := ( getThe State).atoms.toList.map (fun (expr, width, ident) => (ident, (width, expr)))
let atomsAssignment := Std.HashMap.ofList atomsPairs
match unsatProver g reflectionResult atomsAssignment with
match unsatProver reflectionResult atomsAssignment with
| .ok bvExprUnsat, cert =>
let proveFalse reflectionResult.proveFalse bvExprUnsat
g.assign proveFalse
@@ -263,9 +256,9 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
| .error counterExample => return .error counterExample
def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
let unsatProver : UnsatProver := fun g reflectionResult atomsAssignment => do
let unsatProver : UnsatProver := fun reflectionResult atomsAssignment => do
withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
lratBitblaster g cfg reflectionResult atomsAssignment
lratBitblaster cfg reflectionResult atomsAssignment
closeWithBVReflection g unsatProver
/--
@@ -296,11 +289,9 @@ def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
match bvDecide' g cfg with
| .ok result => return result
| .error counterExample =>
counterExample.goal.withContext do
let error explainCounterExampleQuality counterExample
let folder := fun error (var, value) => error ++ m!"{var} = {value.bv}\n"
let errorMessage := counterExample.equations.foldl (init := error) folder
throwError ( addMessageContextFull errorMessage)
let error explainCounterExampleQuality counterExample
let folder := fun error (var, value) => error ++ m!"{var} = {value.bv}\n"
throwError counterExample.equations.foldl (init := error) folder
@[builtin_tactic Lean.Parser.Tactic.bvDecide]
def evalBvTrace : Tactic := fun

View File

@@ -27,8 +27,6 @@ instance : ToExpr BVBinOp where
| .xor => mkConst ``BVBinOp.xor
| .add => mkConst ``BVBinOp.add
| .mul => mkConst ``BVBinOp.mul
| .udiv => mkConst ``BVBinOp.udiv
| .umod => mkConst ``BVBinOp.umod
toTypeExpr := mkConst ``BVBinOp
instance : ToExpr BVUnOp where

View File

@@ -80,10 +80,6 @@ partial def of (x : Expr) : M (Option ReifiedBVExpr) := do
binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
| HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
| HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
| HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
| Complement.complement _ _ innerExpr =>
unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
| HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>

View File

@@ -105,7 +105,7 @@ instance : ToExpr LRAT.IntAction where
mkApp3 (mkConst ``LRAT.Action.del [.zero, .zero]) beta alpha (toExpr ids)
toTypeExpr := mkConst ``LRAT.IntAction
def LratCert.ofFile (lratPath : System.FilePath) (trimProofs : Bool) : CoreM LratCert := do
def LratCert.ofFile (lratPath : System.FilePath) (trimProofs : Bool) : MetaM LratCert := do
let proofInput IO.FS.readBinFile lratPath
let proof
withTraceNode `sat (fun _ => return s!"Parsing LRAT file") do
@@ -139,8 +139,8 @@ Run an external SAT solver on the `CNF` to obtain an LRAT proof.
This will obtain an `LratCert` if the formula is UNSAT and throw errors otherwise.
-/
def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath)
(trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) :
CoreM (Except (Array (Bool × Nat)) LratCert) := do
(trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool)
: MetaM (Except (Array (Bool × Nat)) LratCert) := do
IO.FS.withTempFile fun cnfHandle cnfPath => do
withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do
-- lazyPure to prevent compiler lifting
@@ -162,7 +162,7 @@ def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.Fi
/--
Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.
-/
def mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit :=
def mkAuxDecl (name : Name) (value type : Expr) : MetaM Unit :=
addAndCompile <| .defnDecl {
name := name,
levelParams := [],
@@ -181,7 +181,8 @@ function together with a correctness theorem for it.
`∀ (b : α) (c : LratCert), verifier b c = true → unsat b`
-/
def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContext) (reflected : α)
(verifier : Name) (unsat_of_verifier_eq_true : Name) : MetaM Expr := do
(verifier : Name) (unsat_of_verifier_eq_true : Name) :
MetaM Expr := do
withTraceNode `sat (fun _ => return "Compiling expr term") do
mkAuxDecl cfg.exprDef (toExpr reflected) (toTypeExpr α)
@@ -197,20 +198,13 @@ def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContex
let auxValue := mkApp2 (mkConst verifier) reflectedExpr certExpr
mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool)
let auxType mkEq (mkConst cfg.reflectionDef) (toExpr true)
let auxProof :=
let nativeProof :=
mkApp3
(mkConst ``Lean.ofReduceBool)
(mkConst cfg.reflectionDef)
(toExpr true)
( mkEqRefl (toExpr true))
try
let auxLemma
withTraceNode `sat (fun _ => return "Verifying LRAT certificate") do
mkAuxLemma [] auxType auxProof
return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr (mkConst auxLemma)
catch e =>
throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"
return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr nativeProof
end Frontend

View File

@@ -5,7 +5,6 @@ Authors: Henrik Böving
-/
prelude
import Lean.Meta.AppBuilder
import Lean.Meta.Tactic.AC.Main
import Lean.Elab.Tactic.Simp
import Lean.Elab.Tactic.FalseOrByContra
import Lean.Elab.Tactic.BVDecide.Frontend.Attr
@@ -65,69 +64,6 @@ builtin_simproc [bv_normalize] maxUlt (BitVec.ult (_ : BitVec _) (_ : BitVec _))
else
return .continue
-- A specialised version of BitVec.neg_eq_not_add so it doesn't trigger on -constant
builtin_simproc [bv_normalize] neg_eq_not_add (-(_ : BitVec _)) := fun e => do
let_expr Neg.neg typ _ val := e | return .continue
let_expr BitVec widthExpr := typ | return .continue
let some w getNatValue? widthExpr | return .continue
match getBitVecValue? val with
| some _ => return .continue
| none =>
let proof := mkApp2 (mkConst ``BitVec.neg_eq_not_add) (toExpr w) val
let expr mkAppM ``HAdd.hAdd #[ mkAppM ``Complement.complement #[val], (toExpr 1#w)]
return .visit { expr := expr, proof? := some proof }
builtin_simproc [bv_normalize] bv_add_const ((_ : BitVec _) + ((_ : BitVec _) + (_ : BitVec _))) :=
fun e => do
let_expr HAdd.hAdd _ _ _ _ exp1 rhs := e | return .continue
let_expr HAdd.hAdd _ _ _ _ exp2 exp3 := rhs | return .continue
let some w, exp1Val getBitVecValue? exp1 | return .continue
let proofBuilder thm := mkApp4 (mkConst thm) (toExpr w) exp1 exp2 exp3
match getBitVecValue? exp2 with
| some w', exp2Val =>
if h : w = w' then
let newLhs := exp1Val + h exp2Val
let expr mkAppM ``HAdd.hAdd #[toExpr newLhs, exp3]
let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_left
return .visit { expr := expr, proof? := some proof }
else
return .continue
| none =>
let some w', exp3Val getBitVecValue? exp3 | return .continue
if h : w = w' then
let newLhs := exp1Val + h exp3Val
let expr mkAppM ``HAdd.hAdd #[toExpr newLhs, exp2]
let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_right
return .visit { expr := expr, proof? := some proof }
else
return .continue
builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _)) + (_ : BitVec _)) :=
fun e => do
let_expr HAdd.hAdd _ _ _ _ lhs exp3 := e | return .continue
let_expr HAdd.hAdd _ _ _ _ exp1 exp2 := lhs | return .continue
let some w, exp3Val getBitVecValue? exp3 | return .continue
let proofBuilder thm := mkApp4 (mkConst thm) (toExpr w) exp1 exp2 exp3
match getBitVecValue? exp1 with
| some w', exp1Val =>
if h : w = w' then
let newLhs := exp3Val + h exp1Val
-- TODO
let expr mkAppM ``HAdd.hAdd #[toExpr newLhs, exp2]
let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_left'
return .visit { expr := expr, proof? := some proof }
else
return .continue
| none =>
let some w', exp2Val getBitVecValue? exp2 | return .continue
if h : w = w' then
let newLhs := exp3Val + h exp2Val
let expr mkAppM ``HAdd.hAdd #[toExpr newLhs, exp1]
let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_right'
return .visit { expr := expr, proof? := some proof }
else
return .continue
/--
A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
the goal fully, indicated by returning `none`.
@@ -176,36 +112,11 @@ def rewriteRulesPass : Pass := fun goal => do
let some (_, newGoal) := result? | return none
return newGoal
/--
Normalize with respect to Associativity and Commutativity.
-/
def acNormalizePass : Pass := fun goal => do
let mut newGoal := goal
for hyp in ( goal.getNondepPropHyps) do
let result Lean.Meta.AC.acNfHypMeta newGoal hyp
if let .some nextGoal := result then
newGoal := nextGoal
else
return none
return newGoal
/--
The normalization passes used by `bv_normalize` and thus `bv_decide`.
-/
def defaultPipeline : List Pass := [rewriteRulesPass]
def passPipeline : MetaM (List Pass) := do
let opts getOptions
let mut passPipeline := defaultPipeline
if bv.ac_nf.get opts then
passPipeline := passPipeline ++ [acNormalizePass]
return passPipeline
end Pass
def bvNormalize (g : MVarId) : MetaM (Option MVarId) := do
@@ -213,7 +124,7 @@ def bvNormalize (g : MVarId) : MetaM (Option MVarId) := do
-- Contradiction proof
let some g g.falseOrByContra | return none
trace[Meta.Tactic.bv] m!"Running preprocessing pipeline on:\n{g}"
Pass.fixpointPipeline ( Pass.passPipeline) g
Pass.fixpointPipeline Pass.defaultPipeline g
@[builtin_tactic Lean.Parser.Tactic.bvNormalize]
def evalBVNormalize : Tactic := fun
@@ -226,3 +137,5 @@ def evalBVNormalize : Tactic := fun
end Frontend.Normalize
end Lean.Elab.Tactic.BVDecide

View File

@@ -313,7 +313,7 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
@[builtin_tactic skip] def evalSkip : Tactic := fun _ => pure ()
@[builtin_tactic unknown] def evalUnknown : Tactic := fun stx => do
addCompletionInfo <| CompletionInfo.tactic stx
addCompletionInfo <| CompletionInfo.tactic stx ( getGoals)
@[builtin_tactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx =>
Term.withoutErrToSorry <| withoutRecover do

View File

@@ -1,34 +0,0 @@
/-
Copyright (c) 2021 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Kim Morrison
-/
prelude
import Lean.Elab.Tactic.Basic
/-! # `classical` tactic -/
namespace Lean.Elab.Tactic
open Lean Meta Elab.Tactic
/--
`classical t` runs `t` in a scope where `Classical.propDecidable` is a low priority
local instance.
-/
def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : m α) :
m α := do
modifyEnv Meta.instanceExtension.pushScope
Meta.addInstance ``Classical.propDecidable .local 10
try
t
finally
modifyEnv Meta.instanceExtension.popScope
@[builtin_tactic Lean.Parser.Tactic.classical]
def evalClassical : Tactic := fun stx => do
match stx with
| `(tactic| classical $tacs:tacticSeq) =>
classical <| Elab.Tactic.evalTactic tacs
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic

View File

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
prelude
import Lean.Meta.Tactic.Constructor
import Lean.Meta.Tactic.Assert
import Lean.Meta.Tactic.AuxLemma
import Lean.Meta.Tactic.Clear
import Lean.Meta.Tactic.Rename
import Lean.Elab.Tactic.Basic
@@ -376,7 +375,7 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
Given the decidable instance `inst`, reduces it and returns a decidable instance expression
in whnf that can be regarded as the reason for the failure of `inst` to fully reduce.
-/
private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := withIncRecDepth do
private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do
let inst whnf inst
-- If it's the Decidable recursor, then blame the major premise.
if inst.isAppOfArity ``Decidable.rec 5 then
@@ -394,100 +393,74 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi
return blameDecideReductionFailure inst''
return inst
def evalDecideCore (tacticName : Name) (kernelOnly : Bool) : TacticM Unit :=
closeMainGoalUsing tacticName fun expectedType => do
@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
closeMainGoalUsing `decide fun expectedType => do
let expectedType preprocessPropToDecide expectedType
let pf mkDecideProof expectedType
-- Get instance from `pf`
let s := pf.appFn!.appArg!
if kernelOnly then
-- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
-- The `mkAuxLemma` function caches the result in two ways:
-- 1. First, the function makes use of a `type`-indexed cache per module.
-- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
let levelsInType := (collectLevelParams {} expectedType).params
-- Level variables occurring in `expectedType`, in ambient order
let lemmaLevels := ( Term.getLevelNames).reverse.filter levelsInType.contains
try
let lemmaName mkAuxLemma lemmaLevels expectedType pf
return mkConst lemmaName (lemmaLevels.map .param)
catch _ =>
diagnose expectedType s none
let d mkDecide expectedType
let d instantiateMVars d
-- Get instance from `d`
let s := d.appArg!
-- Reduce the instance rather than `d` itself for diagnostics purposes.
let r withAtLeastTransparency .default <| whnf s
if r.isAppOf ``isTrue then
-- Success!
-- While we have a proof from reduction, we do not embed it in the proof term,
-- and instead we let the kernel recompute it during type checking from the following more
-- efficient term. The kernel handles the unification `e =?= true` specially.
let rflPrf mkEqRefl (toExpr true)
return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
else
let r withAtLeastTransparency .default <| whnf s
if r.isAppOf ``isTrue then
-- Success!
-- While we have a proof from reduction, we do not embed it in the proof term,
-- and instead we let the kernel recompute it during type checking from the following more
-- efficient term. The kernel handles the unification `e =?= true` specially.
return pf
else
diagnose expectedType s r
where
diagnose {α : Type} (expectedType s : Expr) (r? : Option Expr) : TacticM α :=
-- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
throwError MessageData.ofLazyM (es := #[expectedType]) do
let r r?.getDM (withAtLeastTransparency .default <| whnf s)
if r.isAppOf ``isTrue then
return m!"\
tactic '{tacticName}' failed. internal error: the elaborator is able to reduce the \
'{MessageData.ofConstName ``Decidable}' instance, but the kernel is not able to"
else if r.isAppOf ``isFalse then
return m!"\
tactic '{tacticName}' proved that the proposition\
-- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
throwError MessageData.ofLazyM (es := #[expectedType]) do
if r.isAppOf ``isFalse then
return m!"\
tactic 'decide' proved that the proposition\
{indentExpr expectedType}\n\
is false"
-- Re-reduce the instance and collect diagnostics, to get all unfolded Decidable instances
let (reason, unfoldedInsts) withoutModifyingState <| withOptions (fun opt => diagnostics.set opt true) do
modifyDiag (fun _ => {})
let reason withAtLeastTransparency .default <| blameDecideReductionFailure s
let unfolded := ( get).diag.unfoldCounter.foldl (init := #[]) fun cs n _ => cs.push n
let unfoldedInsts unfolded |>.qsort Name.lt |>.filterMapM fun n => do
let e mkConstWithLevelParams n
if ( Meta.isClass? ( inferType e)) == ``Decidable then
return m!"'{MessageData.ofConst e}'"
-- Re-reduce the instance and collect diagnostics, to get all unfolded Decidable instances
let (reason, unfoldedInsts) withoutModifyingState <| withOptions (fun opt => diagnostics.set opt true) do
modifyDiag (fun _ => {})
let reason withAtLeastTransparency .default <| blameDecideReductionFailure s
let unfolded := ( get).diag.unfoldCounter.foldl (init := #[]) fun cs n _ => cs.push n
let unfoldedInsts unfolded |>.qsort Name.lt |>.filterMapM fun n => do
let e mkConstWithLevelParams n
if ( Meta.isClass? ( inferType e)) == ``Decidable then
return m!"'{MessageData.ofConst e}'"
else
return none
return (reason, unfoldedInsts)
let stuckMsg :=
if unfoldedInsts.isEmpty then
m!"Reduction got stuck at the '{MessageData.ofConstName ``Decidable}' instance{indentExpr reason}"
else
return none
return (reason, unfoldedInsts)
let stuckMsg :=
if unfoldedInsts.isEmpty then
m!"Reduction got stuck at the '{MessageData.ofConstName ``Decidable}' instance{indentExpr reason}"
else
let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
m!"After unfolding the {instances} {MessageData.andList unfoldedInsts.toList}, \
reduction got stuck at the '{MessageData.ofConstName ``Decidable}' instance{indentExpr reason}"
let hint :=
if reason.isAppOf ``Eq.rec then
m!"\n\n\
Hint: Reduction got stuck on '▸' ({MessageData.ofConstName ``Eq.rec}), \
which suggests that one of the '{MessageData.ofConstName ``Decidable}' instances is defined using tactics such as 'rw' or 'simp'. \
To avoid tactics, make use of functions such as \
'{MessageData.ofConstName ``inferInstanceAs}' or '{MessageData.ofConstName ``decidable_of_decidable_of_iff}' \
to alter a proposition."
else if reason.isAppOf ``Classical.choice then
m!"\n\n\
Hint: Reduction got stuck on '{MessageData.ofConstName ``Classical.choice}', \
which indicates that a '{MessageData.ofConstName ``Decidable}' instance \
is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
The '{tacticName}' tactic works by evaluating a decision procedure via reduction, \
and it cannot make progress with such instances. \
This can occur due to the 'opened scoped Classical' command, which enables the instance \
'{MessageData.ofConstName ``Classical.propDecidable}'."
else
MessageData.nil
return m!"\
tactic '{tacticName}' failed for proposition\
{indentExpr expectedType}\n\
since its '{MessageData.ofConstName ``Decidable}' instance\
{indentExpr s}\n\
did not reduce to '{MessageData.ofConstName ``isTrue}' or '{MessageData.ofConstName ``isFalse}'.\n\n\
{stuckMsg}{hint}"
@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
evalDecideCore `decide false
@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun _ =>
evalDecideCore `decide! true
let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
m!"After unfolding the {instances} {MessageData.andList unfoldedInsts.toList}, \
reduction got stuck at the '{MessageData.ofConstName ``Decidable}' instance{indentExpr reason}"
let hint :=
if reason.isAppOf ``Eq.rec then
m!"\n\n\
Hint: Reduction got stuck on '▸' ({MessageData.ofConstName ``Eq.rec}), \
which suggests that one of the '{MessageData.ofConstName ``Decidable}' instances is defined using tactics such as 'rw' or 'simp'. \
To avoid tactics, make use of functions such as \
'{MessageData.ofConstName ``inferInstanceAs}' or '{MessageData.ofConstName ``decidable_of_decidable_of_iff}' \
to alter a proposition."
else if reason.isAppOf ``Classical.choice then
m!"\n\n\
Hint: Reduction got stuck on '{MessageData.ofConstName ``Classical.choice}', \
which indicates that a '{MessageData.ofConstName ``Decidable}' instance \
is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
The 'decide' tactic works by evaluating a decision procedure via reduction, and it cannot make progress with such instances. \
This can occur due to the 'opened scoped Classical' command, which enables the instance \
'{MessageData.ofConstName ``Classical.propDecidable}'."
else
MessageData.nil
return m!"\
tactic 'decide' failed for proposition\
{indentExpr expectedType}\n\
since its '{MessageData.ofConstName ``Decidable}' instance\
{indentExpr s}\n\
did not reduce to '{MessageData.ofConstName ``isTrue}' or '{MessageData.ofConstName ``isFalse}'.\n\n\
{stuckMsg}{hint}"
private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Name := do
let auxName Term.mkAuxName baseName

View File

@@ -7,7 +7,6 @@ prelude
import Lean.Meta.Tactic.Assumption
import Lean.Meta.Tactic.TryThis
import Lean.Elab.Tactic.Simp
import Lean.Elab.App
import Lean.Linter.Basic
/--
@@ -47,43 +46,27 @@ deriving instance Repr for UseImplicitLambdaResult
return {}
g.withContext do
let stats if let some stx := usingArg then
let mvarCounterSaved := ( getMCtx).mvarCounter
setGoals [g]
g.withContext do
let e Tactic.elabTerm stx none (mayPostpone := true)
unless occursCheck g e do
throwError "occurs check failed, expression{indentExpr e}\ncontains the goal {Expr.mvar g}"
-- Copy the goal. We want to defer assigning `g := g'` to prevent `MVarId.note` from
-- partially assigning the goal in case we need to log unassigned metavariables.
-- Without deferring, this can cause `logUnassignedAndAbort` to report that `g` could not
-- be synthesized; recall that this function reports that a metavariable could not be
-- synthesized if, after mvar instantiation, it contains one of the provided mvars.
let gCopy mkFreshExprSyntheticOpaqueMVar ( g.getType) ( g.getTag)
let (h, g') gCopy.mvarId!.note `h e
let (result?, stats) simpGoal g' ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
let (h, g) if let .fvar h instantiateMVars e then
pure (h, g)
else
( g.assert `h ( inferType e) e).intro1
let (result?, stats) simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
(simplifyTarget := false) (stats := stats) (discharge? := discharge?)
match result? with
| some (xs, g') =>
let h := xs[0]?.getD h
let name mkFreshUserName `h
let g' g'.rename h name
setGoals [g']
g'.withContext do
let gType g'.getType
let h Term.elabTerm (mkIdent name) gType
Term.synthesizeSyntheticMVarsNoPostponing
let hType inferType h
unless ( withAssignableSyntheticOpaque <| isDefEq gType hType) do
-- `e` still is valid in this new local context
Term.throwTypeMismatchError gType hType h
(header? := some m!"type mismatch, term{indentExpr e}\nafter simplification")
logUnassignedAndAbort ( filterOldMVars ( getMVars e) mvarCounterSaved)
closeMainGoal `simpa (checkUnassigned := false) h
| some (xs, g) =>
let h := match xs with | #[h] | #[] => h | _ => unreachable!
let name mkFreshBinderNameForTactic `h
let g g.rename h name
g.assign <| g.withContext do
Tactic.elabTermEnsuringType (mkIdent name) ( g.getType)
| none =>
if getLinterUnnecessarySimpa ( getOptions) then
if let .fvar h := e then
if ( getLCtx).getRoundtrippingUserName? h |>.isSome then
logLint linter.unnecessarySimpa ( getRef)
m!"try 'simp at {Expr.fvar h}' instead of 'simpa using {Expr.fvar h}'"
g.assign gCopy
if ( getLCtx).getRoundtrippingUserName? h |>.isSome then
logLint linter.unnecessarySimpa ( getRef)
m!"try 'simp at {Expr.fvar h}' instead of 'simpa using {Expr.fvar h}'"
pure stats
else if let some ldecl := ( getLCtx).findFromUserName? `this then
if let (some (_, g), stats) simpGoal g ctx (simprocs := simprocs)

View File

@@ -80,9 +80,8 @@ structure SyntheticMVarDecl where
We have three different kinds of error context.
-/
inductive MVarErrorKind where
/-- Metavariable for implicit arguments. `ctx` is the parent application,
`lctx` is a local context where it is valid (necessary for eta feature for named arguments). -/
| implicitArg (lctx : LocalContext) (ctx : Expr)
/-- Metavariable for implicit arguments. `ctx` is the parent application. -/
| implicitArg (ctx : Expr)
/-- Metavariable for explicit holes provided by the user (e.g., `_` and `?m`) -/
| hole
/-- "Custom", `msgData` stores the additional error messages. -/
@@ -91,7 +90,7 @@ inductive MVarErrorKind where
instance : ToString MVarErrorKind where
toString
| .implicitArg _ _ => "implicitArg"
| .implicitArg _ => "implicitArg"
| .hole => "hole"
| .custom _ => "custom"
@@ -736,7 +735,7 @@ def registerMVarErrorHoleInfo (mvarId : MVarId) (ref : Syntax) : TermElabM Unit
registerMVarErrorInfo { mvarId, ref, kind := .hole }
def registerMVarErrorImplicitArgInfo (mvarId : MVarId) (ref : Syntax) (app : Expr) : TermElabM Unit := do
registerMVarErrorInfo { mvarId, ref, kind := .implicitArg ( getLCtx) app }
registerMVarErrorInfo { mvarId, ref, kind := .implicitArg app }
def registerMVarErrorCustomInfo (mvarId : MVarId) (ref : Syntax) (msgData : MessageData) : TermElabM Unit := do
registerMVarErrorInfo { mvarId, ref, kind := .custom msgData }
@@ -762,7 +761,7 @@ def throwMVarError (m : MessageData) : TermElabM α := do
def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) (extraMsg? : Option MessageData) : TermElabM Unit := do
match mvarErrorInfo.kind with
| MVarErrorKind.implicitArg lctx app => withLCtx lctx {} do
| MVarErrorKind.implicitArg app => do
let app instantiateMVars app
let msg addArgName "don't know how to synthesize implicit argument"
let msg := msg ++ m!"{indentExpr app.setAppPPExplicitForExposingMVars}" ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId
@@ -947,13 +946,13 @@ def applyAttributesAt (declName : Name) (attrs : Array Attribute) (applicationTi
def applyAttributes (declName : Name) (attrs : Array Attribute) : TermElabM Unit :=
applyAttributesCore declName attrs none
def mkTypeMismatchError (header? : Option MessageData) (e : Expr) (eType : Expr) (expectedType : Expr) : TermElabM MessageData := do
def mkTypeMismatchError (header? : Option String) (e : Expr) (eType : Expr) (expectedType : Expr) : TermElabM MessageData := do
let header : MessageData := match header? with
| some header => m!"{header} "
| none => m!"type mismatch{indentExpr e}\n"
return m!"{header}{← mkHasTypeButIsExpectedMsg eType expectedType}"
def throwTypeMismatchError (header? : Option MessageData) (expectedType : Expr) (eType : Expr) (e : Expr)
def throwTypeMismatchError (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr)
(f? : Option Expr := none) (_extraMsg? : Option MessageData := none) : TermElabM α := do
/-
We ignore `extraMsg?` for now. In all our tests, it contained no useful information. It was
@@ -2048,6 +2047,13 @@ def TermElabM.toIO (x : TermElabM α)
let ((a, s), sCore, sMeta) (x.run ctx s).toIO ctxCore sCore ctxMeta sMeta
return (a, sCore, sMeta, s)
instance [MetaEval α] : MetaEval (TermElabM α) where
eval env opts x _ := do
let x : TermElabM α := do
try x finally
( Core.getMessageLog).forM fun msg => do IO.println ( msg.toString)
MetaEval.eval env opts (hideUnit := true) <| x.run' {}
/--
Execute `x` and then tries to solve pending universe constraints.
Note that, stuck constraints will not be discarded.

27
src/Lean/Eval.lean Normal file
View File

@@ -0,0 +1,27 @@
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Lean.Environment
namespace Lean
universe u
/--
`Eval` extension that gives access to the current environment & options.
The basic `Eval` class is in the prelude and should not depend on these
types.
-/
class MetaEval (α : Type u) where
eval : Environment Options α (hideUnit : Bool) IO Environment
instance {α : Type u} [Eval α] : MetaEval α :=
fun env _ a hideUnit => do Eval.eval (fun _ => a) hideUnit; pure env
def runMetaEval {α : Type u} [MetaEval α] (env : Environment) (opts : Options) (a : α) : IO (String × Except IO.Error Environment) :=
IO.FS.withIsolatedStreams (MetaEval.eval env opts a false |>.toBaseIO)
end Lean

View File

@@ -120,7 +120,7 @@ instance [BEq α] [Hashable α] [Monad m] [STWorld ω m] [MonadRecDepth m] : Mon
Throw a "maximum recursion depth has been reached" exception using the given reference syntax.
-/
def throwMaxRecDepthAt [MonadError m] (ref : Syntax) : m α :=
throw <| .error ref (.tagged `runtime.maxRecDepth <| MessageData.ofFormat (Std.Format.text maxRecDepthErrorMessage))
throw <| .error ref (MessageData.ofFormat (Std.Format.text maxRecDepthErrorMessage))
/--
Return true if `ex` was generated by `throwMaxRecDepthAt`.
@@ -129,7 +129,9 @@ but it is also produced by `MacroM` which implemented in the prelude, and intern
been defined yet.
-/
def Exception.isMaxRecDepth (ex : Exception) : Bool :=
ex matches error _ (.tagged `runtime.maxRecDepth _)
match ex with
| error _ (MessageData.ofFormatWithInfos Std.Format.text msg, _) => msg == maxRecDepthErrorMessage
| _ => false
/--
Increment the current recursion depth and then execute `x`.

View File

@@ -23,14 +23,8 @@ def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
let disable := m!"note: this linter can be disabled with `set_option {linterOption.name} false`"
logWarningAt stx (.tagged linterOption.name m!"{msg}\n{disable}")
/--
If `linterOption` is enabled, print a linter warning message at the position determined by `stx`.
Whether a linter option is enabled or not is determined by the following sequence:
1. If it is set, then the value determines whether or not it is enabled.
2. Otherwise, if `linter.all` is set, then its value determines whether or not the option is enabled.
3. Otherwise, the default value determines whether or not it is enabled.
/-- If `linterOption` is true, print a linter warning message at the position determined by `stx`.
-/
def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
(linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do
if getLinterValue linterOption ( getOptions) then logLint linterOption stx msg
if linterOption.get ( getOptions) then logLint linterOption stx msg

View File

@@ -255,6 +255,10 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
(stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) ||
(stx.isOfKind ``Lean.Parser.Tactic.inductionAltLHS && pos == 2))
/-- `#guard_msgs in cmd` itself runs linters in `cmd` (via `elabCommandTopLevel`), so do not run them again. -/
builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
stack.any fun (stx, _) => stx.isOfKind ``Lean.guardMsgsCmd)
/-- Get the current list of `IgnoreFunction`s. -/
def getUnusedVariablesIgnoreFns : CommandElabM (Array IgnoreFunction) := do
return (unusedVariablesIgnoreFnsExt.getState ( getEnv)).2

View File

@@ -246,20 +246,12 @@ structure DefEqCache where
all : PersistentHashMap (Expr × Expr) Bool := {}
deriving Inhabited
/--
A cache for `inferType` at transparency levels `.default` an `.all`.
-/
structure InferTypeCaches where
default : InferTypeCache
all : InferTypeCache
deriving Inhabited
/--
Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
-/
structure Cache where
inferType : InferTypeCaches := {}, {}
funInfo : FunInfoCache := {}
inferType : InferTypeCache := {}
funInfo : FunInfoCache := {}
synthInstance : SynthInstanceCache := {}
whnfDefault : WhnfCache := {} -- cache for closed terms and `TransparencyMode.default`
whnfAll : WhnfCache := {} -- cache for closed terms and `TransparencyMode.all`
@@ -456,6 +448,9 @@ instance : MonadBacktrack SavedState MetaM where
let ((a, s), sCore) (x.run ctx s).toIO ctxCore sCore
pure (a, sCore, s)
instance [MetaEval α] : MetaEval (MetaM α) :=
fun env opts x _ => MetaEval.eval env opts x.run' true
protected def throwIsDefEqStuck : MetaM α :=
throw <| Exception.internal isDefEqStuckExceptionId
@@ -483,11 +478,8 @@ variable [MonadControlT MetaM n] [Monad n]
@[inline] def modifyCache (f : Cache Cache) : MetaM Unit :=
modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag }
@[inline] def modifyInferTypeCacheDefault (f : InferTypeCache InferTypeCache) : MetaM Unit :=
modifyCache fun icd, ica, c1, c2, c3, c4, c5, c6 => f icd, ica, c1, c2, c3, c4, c5, c6
@[inline] def modifyInferTypeCacheAll (f : InferTypeCache InferTypeCache) : MetaM Unit :=
modifyCache fun icd, ica, c1, c2, c3, c4, c5, c6 => icd, f ica, c1, c2, c3, c4, c5, c6
@[inline] def modifyInferTypeCache (f : InferTypeCache InferTypeCache) : MetaM Unit :=
modifyCache fun ic, c1, c2, c3, c4, c5, c6 => f ic, c1, c2, c3, c4, c5, c6
@[inline] def modifyDefEqTransientCache (f : DefEqCache DefEqCache) : MetaM Unit :=
modifyCache fun c1, c2, c3, c4, c5, defeqTrans, c6 => c1, c2, c3, c4, c5, f defeqTrans, c6
@@ -498,9 +490,6 @@ variable [MonadControlT MetaM n] [Monad n]
@[inline] def resetDefEqPermCaches : MetaM Unit :=
modifyDefEqPermCache fun _ => {}
@[inline] def resetSynthInstanceCache : MetaM Unit :=
modifyCache fun c => {c with synthInstance := {}}
@[inline] def modifyDiag (f : Diagnostics Diagnostics) : MetaM Unit := do
if ( isDiagnosticsEnabled) then
modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag }

View File

@@ -55,7 +55,7 @@ private def updateHasFwdDeps (pinfo : Array ParamInfo) (backDeps : Array Nat) :
private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
checkFunInfoCache fn maxArgs? do
let fnType inferType fn
withAtLeastTransparency TransparencyMode.default do
withTransparency TransparencyMode.default do
forallBoundedTelescope fnType maxArgs? fun fvars type => do
let mut paramInfo := #[]
let mut higherOrderOutParams : FVarIdSet := {}

View File

@@ -166,24 +166,13 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
| none => fvarId.throwUnknown
@[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do
match ( getTransparency) with
| .default =>
match ( get).cache.inferType.default.find? e with
| some type => return type
| none =>
let type inferType
unless e.hasMVar || type.hasMVar do
modifyInferTypeCacheDefault fun c => c.insert e type
return type
| .all =>
match ( get).cache.inferType.all.find? e with
| some type => return type
| none =>
let type inferType
unless e.hasMVar || type.hasMVar do
modifyInferTypeCacheAll fun c => c.insert e type
return type
| _ => panic! "checkInferTypeCache: transparency mode not default or all"
match ( get).cache.inferType.find? e with
| some type => return type
| none =>
let type inferType
unless e.hasMVar || type.hasMVar do
modifyInferTypeCache fun c => c.insert e type
return type
@[export lean_infer_type]
def inferTypeImp (e : Expr) : MetaM Expr :=
@@ -202,7 +191,7 @@ def inferTypeImp (e : Expr) : MetaM Expr :=
| .forallE .. => checkInferTypeCache e (inferForallType e)
| .lam .. => checkInferTypeCache e (inferLambdaType e)
| .letE .. => checkInferTypeCache e (inferLambdaType e)
withIncRecDepth <| withAtLeastTransparency TransparencyMode.default (infer e)
withIncRecDepth <| withTransparency TransparencyMode.default (infer e)
/--
Return `LBool.true` if given level is always equivalent to universe level zero.

View File

@@ -208,9 +208,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
let typeLines := ("" : MessageData).joinSep <| Array.toList <| toSynth.mapM fun i => do
let ty instantiateMVars ( inferType argMVars[i]!)
return indentExpr (ty.setPPExplicit true)
throwError m!"\
cannot find synthesization order for instance {inst} with type{indentExpr instTy}\n\
all remaining arguments have metavariables:{typeLines}"
logError m!"cannot find synthesization order for instance {inst} with type{indentExpr instTy}\nall remaining arguments have metavariables:{typeLines}"
pure toSynth[0]!
synthed := synthed.push next
toSynth := toSynth.filter (· != next)
@@ -220,10 +218,9 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
if synthInstance.checkSynthOrder.get ( getOptions) then
let ty instantiateMVars ty
if ty.hasExprMVar then
throwError m!"instance does not provide concrete values for (semi-)out-params{indentExpr (ty.setPPExplicit true)}"
logError m!"instance does not provide concrete values for (semi-)out-params{indentExpr (ty.setPPExplicit true)}"
trace[Meta.synthOrder] "synthesizing the arguments of {inst} in the order {synthed}:\
{("" : MessageData).joinSep (← synthed.mapM fun i => return indentExpr (← inferType argVars[i]!)).toList}"
trace[Meta.synthOrder] "synthesizing the arguments of {inst} in the order {synthed}:{("" : MessageData).joinSep (← synthed.mapM fun i => return indentExpr (← inferType argVars[i]!)).toList}"
return synthed

View File

@@ -33,7 +33,7 @@ register_builtin_option pp.showLetValues : Bool := {
}
private def addLine (fmt : Format) : Format :=
if fmt.isNil then fmt else fmt ++ "\n"
if fmt.isNil then fmt else fmt ++ Format.line
def getGoalPrefix (mvarDecl : MetavarDecl) : String :=
if isLHSGoal? mvarDecl.type |>.isSome then
@@ -99,6 +99,6 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
let fmt := fmt ++ getGoalPrefix mvarDecl ++ Format.nest indent typeFmt
match mvarDecl.userName with
| Name.anonymous => return fmt
| name => return "case " ++ format name.eraseMacroScopes ++ "\n" ++ fmt
| name => return "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt
end Lean.Meta

View File

@@ -67,6 +67,29 @@ instance : ToString RecursorInfo := ⟨fun info =>
end RecursorInfo
private def mkRecursorInfoForKernelRec (declName : Name) (val : RecursorVal) : MetaM RecursorInfo := do
let ival getConstInfoInduct val.getInduct
let numLParams := ival.levelParams.length
let univLevelPos := (List.range numLParams).map RecursorUnivLevelPos.majorType
let univLevelPos := if val.levelParams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos
let produceMotive := List.replicate val.numMinors true
let paramsPos := (List.range val.numParams).map some
let indicesPos := (List.range val.numIndices).map fun pos => val.numParams + pos
let numArgs := val.numIndices + val.numParams + val.numMinors + val.numMotives + 1
pure {
recursorName := declName,
typeName := val.getInduct,
univLevelPos := univLevelPos,
majorPos := val.getMajorIdx,
depElim := true,
recursive := ival.isRec,
produceMotive := produceMotive,
paramsPos := paramsPos,
indicesPos := indicesPos,
numArgs := numArgs
}
private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) : MetaM (Option Nat) :=
if majorPos?.isSome then pure majorPos?
else do
@@ -179,8 +202,8 @@ private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (m
if !motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size then
throwError "invalid user defined recursor '{declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant"
private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : MetaM RecursorInfo := do
let cinfo getConstInfo declName
private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) : MetaM RecursorInfo := do
let declName := cinfo.name
let majorPos? getMajorPosIfAuxRecursor? declName majorPos?
forallTelescopeReducing cinfo.type fun xs type => type.withApp fun motive motiveArgs => do
checkMotive declName motive motiveArgs
@@ -227,6 +250,12 @@ def Attribute.Recursor.getMajorPos (stx : Syntax) : AttrM Nat := do
else
throwErrorAt stx "unexpected attribute argument, numeral expected"
private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
let cinfo getConstInfo declName
match cinfo with
| ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
| _ => mkRecursorInfoAux cinfo majorPos?
builtin_initialize recursorAttribute : ParametricAttribute Nat
registerParametricAttribute {
name := `recursor,
@@ -240,7 +269,11 @@ def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=
recursorAttribute.getParam? env declName
def mkRecursorInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
let majorPos? := majorPos? <|> getMajorPos? ( getEnv) declName
mkRecursorInfoCore declName majorPos?
let cinfo getConstInfo declName
match cinfo with
| ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
| _ => match majorPos? with
| none => do mkRecursorInfoAux cinfo (getMajorPos? ( getEnv) declName)
| _ => mkRecursorInfoAux cinfo majorPos?
end Lean.Meta

View File

@@ -140,25 +140,6 @@ where
| .op l r => mkApp2 preContext.op (convertTarget vars l) (convertTarget vars r)
| .var x => vars[x]!
def post (e : Expr) : SimpM Simp.Step := do
let ctx Simp.getContext
match e, ctx.parent? with
| bin op₁ l r, some (bin op₂ _ _) =>
if isDefEq op₁ op₂ then
return Simp.Step.done { expr := e }
match preContext op₁ with
| some pc =>
let (proof, newTgt) buildNormProof pc l r
return Simp.Step.done { expr := newTgt, proof? := proof }
| none => return Simp.Step.done { expr := e }
| bin op l r, _ =>
match preContext op with
| some pc =>
let (proof, newTgt) buildNormProof pc l r
return Simp.Step.done { expr := newTgt, proof? := proof }
| none => return Simp.Step.done { expr := e }
| e, _ => return Simp.Step.done { expr := e }
def rewriteUnnormalized (mvarId : MVarId) : MetaM MVarId := do
let simpCtx :=
{
@@ -169,48 +150,41 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM MVarId := do
let tgt instantiateMVars ( mvarId.getType)
let (res, _) Simp.main tgt simpCtx (methods := { post })
applySimpResultToTarget mvarId tgt res
where
post (e : Expr) : SimpM Simp.Step := do
let ctx Simp.getContext
match e, ctx.parent? with
| bin op₁ l r, some (bin op₂ _ _) =>
if isDefEq op₁ op₂ then
return Simp.Step.done { expr := e }
match preContext op₁ with
| some pc =>
let (proof, newTgt) buildNormProof pc l r
return Simp.Step.done { expr := newTgt, proof? := proof }
| none => return Simp.Step.done { expr := e }
| bin op l r, _ =>
match preContext op with
| some pc =>
let (proof, newTgt) buildNormProof pc l r
return Simp.Step.done { expr := newTgt, proof? := proof }
| none => return Simp.Step.done { expr := e }
| e, _ => return Simp.Step.done { expr := e }
def rewriteUnnormalizedRefl (goal : MVarId) : MetaM Unit := do
( rewriteUnnormalized goal).refl
let newGoal rewriteUnnormalized goal
newGoal.refl
def rewriteUnnormalizedNormalForm (goal : MVarId) : TacticM Unit := do
let newGoal rewriteUnnormalized goal
replaceMainGoal [newGoal]
@[builtin_tactic acRfl] def acRflTactic : Lean.Elab.Tactic.Tactic := fun _ => do
let goal getMainGoal
goal.withContext <| rewriteUnnormalizedRefl goal
def acNfHypMeta (goal : MVarId) (fvarId : FVarId) : MetaM (Option MVarId) := do
goal.withContext do
let simpCtx :=
{
simpTheorems := {}
congrTheorems := ( getSimpCongrTheorems)
config := Simp.neutralConfig
}
let tgt instantiateMVars ( fvarId.getType)
let (res, _) Simp.main tgt simpCtx (methods := { post })
return ( applySimpResultToLocalDecl goal fvarId res false).map (·.snd)
/-- Implementation of the `ac_nf` tactic when operating on the main goal. -/
def acNfTargetTactic : TacticM Unit :=
liftMetaTactic1 fun goal => rewriteUnnormalized goal
/-- Implementation of the `ac_nf` tactic when operating on a hypothesis. -/
def acNfHypTactic (fvarId : FVarId) : TacticM Unit :=
liftMetaTactic1 fun goal => acNfHypMeta goal fvarId
@[builtin_tactic acNf0]
def evalNf0 : Tactic := fun stx => do
match stx with
| `(tactic| ac_nf0 $[$loc?]?) =>
let loc := if let some loc := loc? then expandLocation loc else Location.targets #[] true
withMainContext do
match loc with
| Location.targets hyps target =>
if target then acNfTargetTactic
( getFVarIds hyps).forM acNfHypTactic
| Location.wildcard =>
acNfTargetTactic
( ( getMainGoal).getNondepPropHyps).forM acNfHypTactic
| _ => Lean.Elab.throwUnsupportedSyntax
@[builtin_tactic acNf] def acNfTactic : Lean.Elab.Tactic.Tactic := fun _ => do
let goal getMainGoal
goal.withContext <| rewriteUnnormalizedNormalForm goal
builtin_initialize
registerTraceClass `Meta.AC

View File

@@ -82,10 +82,6 @@ structure Hypothesis where
userName : Name
type : Expr
value : Expr
/-- The hypothesis' `BinderInfo` -/
binderInfo : BinderInfo := .default
/-- The hypothesis' `LocalDeclKind` -/
kind : LocalDeclKind := .default
/--
Convert the given goal `Ctx |- target` into `Ctx, (hs[0].userName : hs[0].type) ... |-target`.
@@ -98,19 +94,11 @@ def _root_.Lean.MVarId.assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis
let tag mvarId.getTag
let target mvarId.getType
let targetNew := hs.foldr (init := target) fun h targetNew =>
.forallE h.userName h.type targetNew h.binderInfo
mkForall h.userName BinderInfo.default h.type targetNew
let mvarNew mkFreshExprSyntheticOpaqueMVar targetNew tag
let val := hs.foldl (init := mvarNew) fun val h => .app val h.value
let val := hs.foldl (init := mvarNew) fun val h => mkApp val h.value
mvarId.assign val
let (fvarIds, mvarId) mvarNew.mvarId!.introNP hs.size
mvarId.modifyLCtx fun lctx => Id.run do
let mut lctx := lctx
for h : i in [:hs.size] do
let h := hs[i]
if h.kind != .default then
lctx := lctx.setKind fvarIds[i]! h.kind
pure lctx
return (fvarIds, mvarId)
mvarNew.mvarId!.introNP hs.size
/--
Replace hypothesis `hyp` in goal `g` with `proof : typeNew`.

View File

@@ -167,7 +167,7 @@ private partial def processIndependentGoals (orig : List MVarId) (goals remainin
-- and the new subgoals generated from goals on which it is successful.
let (failed, newSubgoals') tryAllM igs fun g =>
run cfg trace next orig cfg.maxDepth [g] []
let newSubgoals := newSubgoals'.flatten
let newSubgoals := newSubgoals'.join
withTraceNode trace
(fun _ => return m!"failed: {← ppMVarIds failed}, new: {← ppMVarIds newSubgoals}") do
-- Update the list of goals with respect to which we need to check independence.

View File

@@ -43,31 +43,9 @@ def _root_.Lean.MVarId.tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVar
mvarId.clear fvarId <|> pure mvarId
/--
Try to clear the given fvars from the local context.
The fvars must be given in the order they appear in the local context.
See also `tryClearMany'` which takes care of reordering internally,
and returns the cleared hypotheses along with the new goal.
Try to erase the given free variables from the goal `mvarId`.
-/
def _root_.Lean.MVarId.tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
fvarIds.foldrM (init := mvarId) fun fvarId mvarId => mvarId.tryClear fvarId
/--
Try to clear the given fvars from the local context. Returns the new goal and
the hypotheses that were cleared.
Does not require the `hyps` to be given in the order in which they
appear in the local context.
-/
def _root_.Lean.MVarId.tryClearMany' (goal : MVarId) (fvarIds : Array FVarId) :
MetaM (MVarId × Array FVarId) :=
goal.withContext do
let fvarIds := ( getLCtx).sortFVarsByContextOrder fvarIds
fvarIds.foldrM (init := (goal, Array.mkEmpty fvarIds.size))
fun h (goal, cleared) => do
let goal' goal.tryClear h
let cleared := if goal == goal' then cleared else cleared.push h
return (goal', cleared)
end Lean.Meta

View File

@@ -662,16 +662,8 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
let varNames forallTelescope info.type fun xs _ => xs.mapM (·.fvarId!.getUserName)
-- Uses of WellFounded.fix can be partially applied. Here we eta-expand the body
-- to make sure that `target` indeed the last parameter
let e := info.value
let e lambdaTelescope e fun params body => do
if body.isAppOfArity ``WellFounded.fix 5 then
forallBoundedTelescope ( inferType body) (some 1) fun xs _ => do
unless xs.size = 1 do
throwError "functional induction: Failed to eta-expand{indentExpr e}"
mkLambdaFVars (params ++ xs) (mkAppN body xs)
else
pure e
-- to avoid dealing with this
let e lambdaTelescope info.value fun params body => do mkLambdaFVars params ( etaExpand body)
let e' lambdaTelescope e fun params funBody => MatcherApp.withUserNames params varNames do
match_expr funBody with
| fix@WellFounded.fix α _motive rel wf body target =>
@@ -718,11 +710,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
-- So for now lets just keep them around.
let e' mkLambdaFVars (binderInfoForMVars := .default) fixedParams e'
instantiateMVars e'
| _ =>
if funBody.isAppOf ``WellFounded.fix then
throwError "Function {name} defined via WellFounded.fix with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
else
throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
| _ => throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
unless ( isTypeCorrect e') do
logError m!"failed to derive a type-correct induction principle:{indentExpr e'}"

View File

@@ -164,11 +164,7 @@ does not start with a forall, lambda or let. -/
abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
intro1Core mvarId true
/--
Calculate the number of new hypotheses that would be created by `intros`,
i.e. the number of binders which can be introduced without unfolding definitions.
-/
partial def getIntrosSize : Expr Nat
private partial def getIntrosSize : Expr Nat
| .forallE _ _ b _ => getIntrosSize b + 1
| .letE _ _ _ b _ => getIntrosSize b + 1
| .mdata _ b => getIntrosSize b

View File

@@ -62,12 +62,12 @@ builtin_simproc [simp, seval] reduceNe (( _ : Fin _) ≠ _) := reduceBinPred `
builtin_dsimproc [simp, seval] reduceBEq (( _ : Fin _) == _) := reduceBoolPred ``BEq.beq 4 (. == .)
builtin_dsimproc [simp, seval] reduceBNe (( _ : Fin _) != _) := reduceBoolPred ``bne 4 (. != .)
/-- Simplification procedure for ensuring `Fin n` literals are normalized. -/
/-- Simplification procedure for ensuring `Fin` literals are normalized. -/
builtin_dsimproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
let_expr OfNat.ofNat _ m _ e | return .continue
let some n, v getFinValue? e | return .continue
let some m getNatValue? m | return .continue
if m < n then
if n == m then
-- Design decision: should we return `.continue` instead of `.done` when simplifying.
-- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
return .done e

View File

@@ -575,7 +575,7 @@ where
/--
Discharges assumptions of the form `∀ …, a = b` using `rfl`. This is particularly useful for higher
order assumptions of the form `∀ …, e = ?g x y` to instaniate a parameter `g` even if that does not
order assumptions of the form `∀ …, e = ?g x y` to instaniate a paramter `g` even if that does not
appear on the lhs of the rule.
-/
def dischargeRfl (e : Expr) : SimpM (Option Expr) := do

View File

@@ -135,9 +135,16 @@ def getIndentAndColumn (map : FileMap) (range : String.Range) : Nat × Nat :=
let body := map.source.findAux (· ' ') range.start start
((body - start).1, (range.start - start).1)
/-- Replace subexpressions like `?m.1234` with `?_` so it can be copy-pasted. -/
partial def replaceMVarsByUnderscores [Monad m] [MonadQuotation m]
(s : Syntax) : m Syntax :=
s.replaceM fun s => do
let `(?$id:ident) := s | pure none
if id.getId.hasNum || id.getId.isInternal then `(?_) else pure none
/-- Delaborate `e` into syntax suitable for use by `refine`. -/
def delabToRefinableSyntax (e : Expr) : MetaM Term :=
withOptions (pp.mvars.anonymous.set · false) do delab e
return replaceMVarsByUnderscores ( delab e)
/--
An option allowing the user to customize the ideal input width. Defaults to 100.

View File

@@ -145,7 +145,7 @@ def zetaReduce (e : Expr) : MetaM Expr := do
| none => return TransformStep.done e
| some localDecl =>
if let some value := localDecl.value? then
return TransformStep.visit ( instantiateMVars value)
return TransformStep.visit value
else
return TransformStep.done e
| _ => return .continue

View File

@@ -462,33 +462,9 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
"#check " >> termParser
@[builtin_command_parser] def check_failure := leading_parser
"#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
/--
`#eval e` evaluates the expression `e` by compiling and evaluating it.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
-/
@[builtin_command_parser, builtin_doc] def eval := leading_parser
@[builtin_command_parser] def eval := leading_parser
"#eval " >> termParser
@[builtin_command_parser, inherit_doc eval] def evalBang := leading_parser
@[builtin_command_parser] def evalBang := leading_parser
"#eval! " >> termParser
@[builtin_command_parser] def synth := leading_parser
"#synth " >> termParser

View File

@@ -125,16 +125,6 @@ example : 1 + 1 = 2 := by rfl
@[builtin_tactic_parser] def decide := leading_parser
nonReservedSymbol "decide"
/--
`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
It has the following properties:
- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
and once during kernel type checking), the `decide!` tactic reduces it exactly once.
-/
@[builtin_tactic_parser] def decideBang := leading_parser
nonReservedSymbol "decide!"
/-- `native_decide` will attempt to prove a goal of type `p` by synthesizing an instance
of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
uses `#eval` to evaluate the decidability instance.

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