Compare commits

..

1 Commits

Author SHA1 Message Date
Kim Morrison
10bdf8a9d8 chore: upstream Array.reduceOption 2024-10-18 11:21:17 +11:00
949 changed files with 3171 additions and 10836 deletions

View File

@@ -39,7 +39,7 @@ Please put an X between the brackets as you perform the following steps:
### Versions
[Output of `#version` or `#eval Lean.versionString`]
[Output of `#eval Lean.versionString`]
[OS version, if not using live.lean-lang.org.]
### Additional Information

View File

@@ -11,9 +11,7 @@ jobs:
with:
# the default is to use a virtual merge commit between the PR and master: just use the PR
ref: ${{ github.event.pull_request.head.sha }}
sparse-checkout: |
src/Lean
src/Std
sparse-checkout: src/Lean
- name: Check Prelude
run: |
failed_files=""
@@ -21,8 +19,8 @@ jobs:
if ! grep -q "^prelude$" "$file"; then
failed_files="$failed_files$file\n"
fi
done < <(find src/Lean src/Std -name '*.lean' -print0)
done < <(find src/Lean -name '*.lean' -print0)
if [ -n "$failed_files" ]; then
echo -e "The following files should use 'prelude':\n$failed_files"
exit 1
fi
fi

View File

@@ -217,7 +217,7 @@ jobs:
"release": true,
"check-level": 2,
"shell": "msys2 {0}",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
// for reasons unknown, interactivetests are flaky on Windows
"CTEST_OPTIONS": "--repeat until-pass:2",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -227,7 +227,7 @@ jobs:
{
"name": "Linux aarch64",
"os": "nscloud-ubuntu-22.04-arm64-4x8",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"release": true,
"check-level": 2,
"shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",

View File

@@ -96,7 +96,7 @@ jobs:
nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
- name: Test
run: |
nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/build/source/src/build ./push-test; false)
nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/source/src/build/ ./push-test; false)
- name: Test Summary
uses: test-summary/action@v2
with:

View File

@@ -4,14 +4,14 @@
# Listed persons will automatically be asked by GitHub to review a PR touching these paths.
# If multiple names are listed, a review by any of them is considered sufficient by default.
/.github/ @Kha @kim-em
/RELEASES.md @kim-em
/.github/ @Kha @semorrison
/RELEASES.md @semorrison
/src/kernel/ @leodemoura
/src/lake/ @tydeu
/src/Lean/Compiler/ @leodemoura
/src/Lean/Data/Lsp/ @mhuisi
/src/Lean/Elab/Deriving/ @kim-em
/src/Lean/Elab/Tactic/ @kim-em
/src/Lean/Elab/Deriving/ @semorrison
/src/Lean/Elab/Tactic/ @semorrison
/src/Lean/Language/ @Kha
/src/Lean/Meta/Tactic/ @leodemoura
/src/Lean/Parser/ @Kha
@@ -19,7 +19,7 @@
/src/Lean/PrettyPrinter/Delaborator/ @kmill
/src/Lean/Server/ @mhuisi
/src/Lean/Widget/ @Vtec234
/src/Init/Data/ @kim-em
/src/Init/Data/ @semorrison
/src/Init/Data/Array/Lemmas.lean @digama0
/src/Init/Data/List/Lemmas.lean @digama0
/src/Init/Data/List/BasicAux.lean @digama0
@@ -45,4 +45,3 @@
/src/Std/ @TwoFX
/src/Std/Tactic/BVDecide/ @hargoniX
/src/Lean/Elab/Tactic/BVDecide/ @hargoniX
/src/Std/Sat/ @hargoniX

View File

@@ -8,21 +8,6 @@ This file contains work-in-progress notes for the upcoming release, as well as p
Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
of each version.
v4.15.0
----------
Development in progress.
v4.14.0
----------
Release candidate, release notes will be copied from the branch `releases/v4.14.0` once completed.
v4.13.0
----------
Release candidate, release notes will be copied from the branch `releases/v4.13.0` once completed.
v4.12.0
----------

View File

@@ -15,13 +15,6 @@ Mode](https://docs.microsoft.com/en-us/windows/apps/get-started/enable-your-devi
which will allow Lean to create symlinks that e.g. enable go-to-definition in
the stdlib.
## Installing the Windows SDK
Install the Windows SDK from [Microsoft](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
The oldest supported version is 10.0.18362.0. If you installed the Windows SDK to the default location,
then there should be a directory with the version number at `C:\Program Files (x86)\Windows Kits\10\Include`.
If there are multiple directories, only the highest version number matters.
## Installing dependencies
[The official webpage of MSYS2][msys2] provides one-click installers.

View File

@@ -138,8 +138,8 @@ definition:
-/
instance : Applicative List where
pure := List.singleton
seq f x := List.flatMap f fun y => Functor.map y (x ())
pure := List.pure
seq f x := List.bind f fun y => Functor.map y (x ())
/-!
Notice you can now sequence a _list_ of functions and a _list_ of items.

View File

@@ -128,8 +128,8 @@ Applying the identity function through an applicative structure should not chang
values or structure. For example:
-/
instance : Applicative List where
pure := List.singleton
seq f x := List.flatMap f fun y => Functor.map y (x ())
pure := List.pure
seq f x := List.bind f fun y => Functor.map y (x ())
#eval pure id <*> [1, 2, 3] -- [1, 2, 3]
/-!
@@ -235,8 +235,8 @@ structure or its values.
Left identity is `x >>= pure = x` and is demonstrated by the following examples on a monadic `List`:
-/
instance : Monad List where
pure := List.singleton
bind := List.flatMap
pure := List.pure
bind := List.bind
def a := ["apple", "orange"]

View File

@@ -192,8 +192,8 @@ implementation of `pure` and `bind`.
-/
instance : Monad List where
pure := List.singleton
bind := List.flatMap
pure := List.pure
bind := List.bind
/-!
Like you saw with the applicative `seq` operator, the `bind` operator applies the given function

View File

@@ -7,7 +7,7 @@ Platforms built & tested by our CI, available as binary releases via elan (see b
* x86-64 Linux with glibc 2.27+
* x86-64 macOS 10.15+
* aarch64 (Apple Silicon) macOS 10.15+
* x86-64 Windows 11 (any version), Windows 10 (version 1903 or higher), Windows Server 2022
* x86-64 Windows 10+
### Tier 2

View File

@@ -38,11 +38,7 @@
# more convenient `ctest` output
CTEST_OUTPUT_ON_FAILURE = 1;
} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
GMP = (pkgsDist.gmp.override { withStatic = true; }).overrideAttrs (attrs:
pkgs.lib.optionalAttrs (pkgs.stdenv.system == "aarch64-linux") {
# would need additional linking setup on Linux aarch64, we don't use it anywhere else either
hardeningDisable = [ "stackprotector" ];
});
GMP = pkgsDist.gmp.override { withStatic = true; };
LIBUV = pkgsDist.libuv.overrideAttrs (attrs: {
configureFlags = ["--enable-static"];
hardeningDisable = [ "stackprotector" ];

View File

@@ -31,20 +31,14 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
# runtime
(cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1)
# further dependencies
# Note: even though we're linking against libraries like `libbcrypt.a` which appear to be static libraries from the file name,
# we're not actually linking statically against the code.
# Rather, `libbcrypt.a` is an import library (see https://en.wikipedia.org/wiki/Dynamic-link_library#Import_libraries) that just
# tells the compiler how to dynamically link against `bcrypt.dll` (which is located in the System32 folder).
# This distinction is relevant specifically for `libicu.a`/`icu.dll` because there we want updates to the time zone database to
# be delivered to users via Windows Update without having to recompile Lean or Lean programs.
cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu}.* /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,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/
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'"
# when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
# when not using the above flags, link GMP dynamically/as usual
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
# do not set `LEAN_CC` for tests
echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"

View File

@@ -10,7 +10,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 15)
set(LEAN_VERSION_MINOR 12)
set(LEAN_VERSION_PATCH 0)
set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -155,10 +155,6 @@ endif ()
# We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
string(APPEND LEANC_EXTRA_FLAGS " -fstack-clash-protection")
# This makes signed integer overflow guaranteed to match 2's complement.
string(APPEND CMAKE_CXX_FLAGS " -fwrapv")
string(APPEND LEANC_EXTRA_FLAGS " -fwrapv")
if(NOT MULTI_THREAD)
message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
set(AUTO_THREAD_FINALIZATION OFF)
@@ -301,23 +297,6 @@ if(NOT LEAN_STANDALONE)
string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LIBRARIES}")
endif()
# Windows SDK (for ICU)
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
# Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
find_package(WindowsSDK REQUIRED COMPONENTS tools)
# This will give a semicolon-separated list of include directories
get_windowssdk_include_dirs(${WINDOWSSDK_LATEST_DIR} WINDOWSSDK_INCLUDE_DIRS)
# To successfully build against Windows SDK headers, the Windows SDK headers must have lower
# priority than other system headers, so use `-idirafter`. Unfortunately, CMake does not
# support this using `include_directories`.
string(REPLACE ";" "\" -idirafter \"" WINDOWSSDK_INCLUDE_DIRS "${WINDOWSSDK_INCLUDE_DIRS}")
string(APPEND CMAKE_CXX_FLAGS " -idirafter \"${WINDOWSSDK_INCLUDE_DIRS}\"")
string(APPEND LEAN_EXTRA_LINKER_FLAGS " -licu")
endif()
# ccache
if(CCACHE AND NOT CMAKE_CXX_COMPILER_LAUNCHER AND NOT CMAKE_C_COMPILER_LAUNCHER)
find_program(CCACHE_PATH ccache)
@@ -501,7 +480,7 @@ endif()
# Git HASH
if(USE_GITHASH)
include(GetGitRevisionDescription)
get_git_head_revision(GIT_REFSPEC GIT_SHA1 ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR)
get_git_head_revision(GIT_REFSPEC GIT_SHA1)
if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
message(STATUS "Failed to read git_sha1")
set(GIT_SHA1 "")

View File

@@ -35,5 +35,3 @@ import Init.Ext
import Init.Omega
import Init.MacroTrace
import Init.Grind
import Init.While
import Init.Syntax

View File

@@ -8,42 +8,6 @@ import Init.Core
universe u v w
/--
A `ForIn'` instance, which handles `for h : x in c do`,
can also handle `for x in x do` by ignoring `h`, and so provides a `ForIn` instance.
Note that this instance will cause a potentially non-defeq duplication if both `ForIn` and `ForIn'`
instances are provided for the same type.
-/
-- We set the priority to 500 so it is below the default,
-- but still above the low priority instance from `Stream`.
instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
forIn x b f := forIn' x b fun a _ => f a
@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
(f : (a : α) a x β m (ForInStep β)) (g : (a : α) β m (ForInStep β))
(h : a m b, f a m b = g a b) :
forIn' x b f = forIn x b g := by
simp [instForInOfForIn']
congr
apply funext
intro a
apply funext
intro m
apply funext
intro b
simp [h]
rfl
/-- Extract the value from a `ForInStep`, ignoring whether it is `done` or `yield`. -/
def ForInStep.value (x : ForInStep α) : α :=
match x with
| ForInStep.done b => b
| ForInStep.yield b => b
@[simp] theorem ForInStep.value_done (b : β) : (ForInStep.done b).value = b := rfl
@[simp] theorem ForInStep.value_yield (b : β) : (ForInStep.yield b).value = b := rfl
@[reducible]
def Functor.mapRev {f : Type u Type v} [Functor f] {α β : Type u} : f α (α β) f β :=
fun a f => f <$> a

View File

@@ -6,7 +6,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
The State monad transformer using IO references.
-/
prelude
import Init.System.ST
import Init.System.IO
import Init.Control.State
def StateRefT' (ω : Type) (σ : Type) (m : Type Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α

View File

@@ -7,7 +7,6 @@ Notation for operators defined at Prelude.lean
-/
prelude
import Init.Tactics
import Init.Meta
namespace Lean.Parser.Tactic.Conv
@@ -47,20 +46,12 @@ scoped syntax (name := withAnnotateState)
/-- `skip` does nothing. -/
syntax (name := skip) "skip" : conv
/--
Traverses into the left subterm of a binary operator.
In general, for an `n`-ary operator, it traverses into the second to last argument.
It is a synonym for `arg -2`.
-/
/-- Traverses into the left subterm of a binary operator.
(In general, for an `n`-ary operator, it traverses into the second to last argument.) -/
syntax (name := lhs) "lhs" : conv
/--
Traverses into the right subterm of a binary operator.
In general, for an `n`-ary operator, it traverses into the last argument.
It is a synonym for `arg -1`.
-/
/-- Traverses into the right subterm of a binary operator.
(In general, for an `n`-ary operator, it traverses into the last argument.) -/
syntax (name := rhs) "rhs" : conv
/-- Traverses into the function of a (unary) function application.
@@ -83,17 +74,13 @@ subgoals for all the function arguments. For example, if the target is `f x y` t
`congr` produces two subgoals, one for `x` and one for `y`. -/
syntax (name := congr) "congr" : conv
syntax argArg := "@"? "-"? num
/--
* `arg i` traverses into the `i`'th argument of the target. For example if the
target is `f a b c d` then `arg 1` traverses to `a` and `arg 3` traverses to `c`.
The index may be negative; `arg -1` traverses into the last argument,
`arg -2` into the second-to-last argument, and so on.
* `arg @i` is the same as `arg i` but it counts all arguments instead of just the
explicit arguments.
* `arg 0` traverses into the function. If the target is `f a b c d`, `arg 0` traverses into `f`. -/
syntax (name := arg) "arg " argArg : conv
syntax (name := arg) "arg " "@"? num : conv
/-- `ext x` traverses into a binder (a `fun x => e` or `∀ x, e` expression)
to target `e`, introducing name `x` in the process. -/
@@ -143,11 +130,11 @@ For example, if we are searching for `f _` in `f (f a) = f b`:
syntax (name := pattern) "pattern " (occs)? term : conv
/-- `rw [thm]` rewrites the target using `thm`. See the `rw` tactic for more information. -/
syntax (name := rewrite) "rewrite" optConfig rwRuleSeq : conv
syntax (name := rewrite) "rewrite" (config)? rwRuleSeq : conv
/-- `simp [thm]` performs simplification using `thm` and marked `@[simp]` lemmas.
See the `simp` tactic for more information. -/
syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
/--
@@ -164,7 +151,7 @@ example (a : Nat): (0 + 0) = a - a := by
rw [← Nat.sub_self a]
```
-/
syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
(" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
/-- `simp_match` simplifies match expressions. For example,
@@ -260,12 +247,12 @@ macro (name := failIfSuccess) tk:"fail_if_success " s:convSeq : conv =>
/-- `rw [rules]` applies the given list of rewrite rules to the target.
See the `rw` tactic for more information. -/
macro "rw" c:optConfig s:rwRuleSeq : conv => `(conv| rewrite $c:optConfig $s)
macro "rw" c:(config)? s:rwRuleSeq : conv => `(conv| rewrite $[$c]? $s)
/-- `erw [rules]` is a shorthand for `rw (transparency := .default) [rules]`.
/-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
which only unfolds `@[reducible]` definitions). -/
macro "erw" c:optConfig s:rwRuleSeq : conv => `(conv| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq)
macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s)
/-- `args` traverses into all arguments. Synonym for `congr`. -/
macro "args" : conv => `(conv| congr)
@@ -276,7 +263,7 @@ macro "right" : conv => `(conv| rhs)
/-- `intro` traverses into binders. Synonym for `ext`. -/
macro "intro" xs:(ppSpace colGt ident)* : conv => `(conv| ext $xs*)
syntax enterArg := ident <|> argArg
syntax enterArg := ident <|> ("@"? num)
/-- `enter [arg, ...]` is a compact way to describe a path to a subterm.
It is a shorthand for other conv tactics as follows:
@@ -285,7 +272,12 @@ It is a shorthand for other conv tactics as follows:
* `enter [x]` (where `x` is an identifier) is equivalent to `ext x`.
For example, given the target `f (g a (fun x => x b))`, `enter [1, 2, x, 1]`
will traverse to the subterm `b`. -/
syntax (name := enter) "enter" " [" withoutPosition(enterArg,+) "]" : conv
syntax "enter" " [" withoutPosition(enterArg,+) "]" : conv
macro_rules
| `(conv| enter [$i:num]) => `(conv| arg $i)
| `(conv| enter [@$i]) => `(conv| arg @$i)
| `(conv| enter [$id:ident]) => `(conv| ext $id)
| `(conv| enter [$arg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
/-- The `apply thm` conv tactic is the same as `apply thm` the tactic.
There are no restrictions on `thm`, but strange results may occur if `thm`

View File

@@ -324,6 +324,7 @@ class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)
export ForIn' (forIn')
/--
Auxiliary type used to compile `do` notation. It is used when compiling a do block
nested inside a combinator like `tryCatch`. It encodes the possible ways the

View File

@@ -19,7 +19,6 @@ import Init.Data.ByteArray
import Init.Data.FloatArray
import Init.Data.Fin
import Init.Data.UInt
import Init.Data.SInt
import Init.Data.Float
import Init.Data.Option
import Init.Data.Ord

View File

@@ -17,4 +17,3 @@ import Init.Data.Array.TakeDrop
import Init.Data.Array.Bootstrap
import Init.Data.Array.GetLit
import Init.Data.Array.MapIdx
import Init.Data.Array.Set

View File

@@ -12,7 +12,6 @@ import Init.Data.Repr
import Init.Data.ToString.Basic
import Init.GetElem
import Init.Data.List.ToArray
import Init.Data.Array.Set
universe u v w
/-! ### Array literal syntax -/
@@ -26,12 +25,9 @@ variable {α : Type u}
namespace Array
@[deprecated toList (since := "2024-10-13")] abbrev data := @toList
/-! ### Preliminary theorems -/
@[simp] theorem size_set (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
(set a i v h).size = a.size :=
@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
List.length_set ..
@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
@@ -82,42 +78,6 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
/-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
-- NB: This is defined as a structure rather than a plain def so that a lemma
-- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
structure Mem (as : Array α) (a : α) : Prop where
val : a as.toList
instance : Membership α (Array α) where
mem := Mem
theorem mem_def {a : α} {as : Array α} : a as a as.toList :=
fun | .mk h => h, Array.Mem.mk
@[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] l := by
rw [Array.mem_def, getElem_toList]
apply List.getElem_mem
end Array
namespace List
@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
a.toArray[i] = a[i]'(by simpa using h) := rfl
@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
@[simp] theorem getElem!_toArray [Inhabited α] {a : List α} {i : Nat} :
a.toArray[i]! = a[i]! := rfl
end List
namespace Array
@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
@[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
@@ -143,7 +103,7 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
`fset` may be slightly slower than `uset`. -/
@[extern "lean_array_uset"]
def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
a.set i.toNat v h
a.set i.toNat, h v
@[extern "lean_array_pop"]
def pop (a : Array α) : Array α where
@@ -169,10 +129,10 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
let v₁ := a.get i
let v₂ := a.get j
let a' := a.set i v₂
a'.set j v₁ (Nat.lt_of_lt_of_eq j.isLt (size_set a i v₂ _).symm)
a'.set (size_set a i v₂ j) v₁
@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
show ((a.set i (a.get j)).set j (a.get i) (Nat.lt_of_lt_of_eq j.isLt (size_set a i (a.get j) _).symm)).size = a.size
show ((a.set i (a.get j)).set (size_set a i _ j) (a.get i)).size = a.size
rw [size_set, size_set]
/--
@@ -237,11 +197,9 @@ def range (n : Nat) : Array Nat :=
def singleton (v : α) : Array α :=
mkArray 1 v
def back! [Inhabited α] (a : Array α) : α :=
def back [Inhabited α] (a : Array α) : α :=
a.get! (a.size - 1)
@[deprecated back! (since := "2024-10-31")] abbrev back := @back!
def get? (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some a[i] else none
@@ -261,15 +219,12 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
have : Inhabited (α × Array α) := (v, a)
panic! ("index " ++ toString i ++ " out of bounds")
/-- `take a n` returns the first `n` elements of `a`. -/
def take (a : Array α) (n : Nat) : Array α :=
def shrink (a : Array α) (n : Nat) : Array α :=
let rec loop
| 0, a => a
| n+1, a => loop n a.pop
loop (a.size - n) a
@[deprecated take (since := "2024-10-22")] abbrev shrink := @take
@[inline]
unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α m α) : m (Array α) := do
if h : i < a.size then
@@ -280,7 +235,7 @@ unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α → m α) :
-- of the element type, and that it is valid to store `box(0)` in any array.
let a' := a.set idx (unsafeCast ())
let v f v
pure <| a'.set idx v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
pure <| a'.set (size_set a .. idx) v
else
pure a
@@ -306,21 +261,21 @@ def modifyOp (self : Array α) (idx : Nat) (f : αα) : Array α :=
We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < usizeSz` to true. -/
@[inline] unsafe def forIn'Unsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) a as β m (ForInStep β)) : m β :=
@[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (b : β) (f : α β m (ForInStep β)) : m β :=
let sz := as.usize
let rec @[specialize] loop (i : USize) (b : β) : m β := do
if i < sz then
let a := as.uget i lcProof
match ( f a lcProof b) with
match ( f a b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop (i+1) b
else
pure b
loop 0 b
/-- Reference implementation for `forIn'` -/
@[implemented_by Array.forIn'Unsafe]
protected def forIn' {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) a as β m (ForInStep β)) : m β :=
/-- Reference implementation for `forIn` -/
@[implemented_by Array.forInUnsafe]
protected def forIn {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (b : β) (f : α β m (ForInStep β)) : m β :=
let rec loop (i : Nat) (h : i as.size) (b : β) : m β := do
match i, h with
| 0, _ => pure b
@@ -328,17 +283,15 @@ protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
have h' : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
have : as.size - 1 < as.size := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
match ( f as[as.size - 1 - i] (getElem_mem this) b) with
match ( f as[as.size - 1 - i] b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop i (Nat.le_of_lt h') b
loop as.size (Nat.le_refl _) b
instance : ForIn' m (Array α) α inferInstance where
forIn' := Array.forIn'
instance : ForIn m (Array α) α where
forIn := Array.forIn
-- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
/-- See comment at `forIn'Unsafe` -/
/-- See comment at `forInUnsafe` -/
@[inline]
unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (f : β α m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β :=
let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do
@@ -373,7 +326,7 @@ def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β
else
fold as.size (Nat.le_refl _)
/-- See comment at `forIn'Unsafe` -/
/-- See comment at `forInUnsafe` -/
@[inline]
unsafe def foldrMUnsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (f : α β m β) (init : β) (as : Array α) (start := as.size) (stop := 0) : m β :=
let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do
@@ -412,7 +365,7 @@ def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
else
pure init
/-- See comment at `forIn'Unsafe` -/
/-- See comment at `forInUnsafe` -/
@[inline]
unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (f : α m β) (as : Array α) : m (Array β) :=
let sz := as.usize
@@ -443,25 +396,20 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
decreasing_by simp_wf; decreasing_trivial_pre_omega
map 0 (mkEmpty as.size)
/-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
@[inline]
def mapFinIdxM {α : Type u} {β : Type v} {m : Type v Type w} [Monad m]
(as : Array α) (f : Fin as.size α m β) : m (Array β) :=
def mapIdxM {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (f : Fin as.size α m β) : m (Array β) :=
let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do
match i, inv with
| 0, _ => pure bs
| i+1, inv =>
have j_lt : j < as.size := by
have : j < as.size := by
rw [ inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
apply Nat.le_add_right
let idx : Fin as.size := j, this
have : i + (j + 1) = as.size := by rw [ inv, Nat.add_comm j 1, Nat.add_assoc]
map i (j+1) this (bs.push ( f j, j_lt (as.get j, j_lt)))
map i (j+1) this (bs.push ( f idx (as.get idx)))
map as.size 0 rfl (mkEmpty as.size)
@[inline]
def mapIdxM {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (f : Nat α m β) : m (Array β) :=
as.mapFinIdxM fun i a => f i a
@[inline]
def findSomeM? {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (f : α m (Option β)) : m (Option β) := do
for a in as do
@@ -567,13 +515,8 @@ def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : A
def map {α : Type u} {β : Type v} (f : α β) (as : Array α) : Array β :=
Id.run <| as.mapM f
/-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
@[inline]
def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size α β) : Array β :=
Id.run <| as.mapFinIdxM f
@[inline]
def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat α β) : Array β :=
def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size α β) : Array β :=
Id.run <| as.mapIdxM f
/-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
@@ -667,7 +610,7 @@ instance : HAppend (Array α) (List α) (Array α) := ⟨Array.appendList⟩
def flatMapM [Monad m] (f : α m (Array β)) (as : Array α) : m (Array β) :=
as.foldlM (init := empty) fun bs a => do return bs ++ ( f a)
@[deprecated flatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
@[deprecated concatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
@[inline]
def flatMap (f : α Array β) (as : Array α) : Array β :=

View File

@@ -60,7 +60,7 @@ where
if ptrEq a b then
go (i+1) as
else
go (i+1) (as.set i b h)
go (i+1) (as.set i, h b)
else
return as

View File

@@ -69,8 +69,8 @@ namespace Array
if as.isEmpty then do let v add (); pure <| as.push v
else if lt k (as.get! 0) then do let v add (); pure <| as.insertAt! 0 v
else if !lt (as.get! 0) k then as.modifyM 0 <| merge
else if lt as.back! k then do let v add (); pure <| as.push v
else if !lt k as.back! then as.modifyM (as.size - 1) <| merge
else if lt as.back k then do let v add (); pure <| as.push v
else if !lt k as.back then as.modifyM (as.size - 1) <| merge
else binInsertAux lt merge add as k 0 (as.size - 1)
@[inline] def binInsert {α : Type u} (lt : α α Bool) (as : Array α) (k : α) : Array α :=

View File

@@ -23,7 +23,7 @@ theorem foldlM_eq_foldlM_toList.aux [Monad m]
· cases Nat.not_le_of_gt _ (Nat.zero_add _ H)
· rename_i i; rw [Nat.succ_add] at H
simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
rw (occs := .pos [2]) [ List.get_drop_eq_drop _ _ _]
rw (config := {occs := .pos [2]}) [ List.get_drop_eq_drop _ _ _]
rfl
· rw [List.drop_of_length_le (Nat.ge_of_not_lt _)]; rfl
@@ -42,7 +42,7 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
unfold foldrM.fold
match i with
| 0 => simp [List.foldlM, List.take]
| i+1 => rw [ List.take_concat_get _ _ h]; simp [ (aux f arr · i)]
| i+1 => rw [ List.take_concat_get _ _ h]; simp [ (aux f arr · i)]; rfl
theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α β m β) (init : β) (arr : Array α) :
arr.foldrM f init = arr.toList.reverse.foldlM (fun x y => f y x) init := by

View File

@@ -6,16 +6,14 @@ Authors: Leonardo de Moura
prelude
import Init.Data.Array.Basic
import Init.Data.BEq
import Init.Data.Nat.Lemmas
import Init.Data.List.Nat.BEq
import Init.ByCases
namespace Array
theorem rel_of_isEqvAux
{r : α α Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i a.size)
(r : α α Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i a.size)
(heqv : Array.isEqvAux a b hsz r i hi)
{j : Nat} (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz hi))) := by
(j : Nat) (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz hi))) := by
induction i with
| zero => contradiction
| succ i ih =>
@@ -28,46 +26,15 @@ theorem rel_of_isEqvAux
subst hj'
exact heqv.left
theorem isEqvAux_of_rel {r : α α Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i a.size)
(w : j, (hj : j < i) r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz hi)))) : Array.isEqvAux a b hsz r i hi := by
induction i with
| zero => simp [Array.isEqvAux]
| succ i ih =>
simp only [isEqvAux, Bool.and_eq_true]
exact w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)
theorem rel_of_isEqv {r : α α Bool} {a b : Array α} :
theorem rel_of_isEqv (r : α α Bool) (a b : Array α) :
Array.isEqv a b r h : a.size = b.size, (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h h')) := by
simp only [isEqv]
split <;> rename_i h
· exact fun h' => h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'
· exact fun h' => h, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'
· intro; contradiction
theorem isEqv_iff_rel (a b : Array α) (r) :
Array.isEqv a b r h : a.size = b.size, (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h h')) :=
rel_of_isEqv, fun h, w => by
simp only [isEqv, h, reduceDIte]
exact isEqvAux_of_rel h (by simp [h]) w
theorem isEqv_eq_decide (a b : Array α) (r) :
Array.isEqv a b r =
if h : a.size = b.size then decide ( (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h h'))) else false := by
by_cases h : Array.isEqv a b r
· simp only [h, Bool.true_eq]
simp only [isEqv_iff_rel] at h
obtain h, w := h
simp [h, w]
· let h' := h
simp only [Bool.not_eq_true] at h
simp only [h, Bool.false_eq, dite_eq_right_iff, decide_eq_false_iff_not, Classical.not_forall,
Bool.not_eq_true]
simpa [isEqv_iff_rel] using h'
@[simp] theorem isEqv_toList [BEq α] (a b : Array α) : (a.toList.isEqv b.toList r) = (a.isEqv b r) := by
simp [isEqv_eq_decide, List.isEqv_eq_decide]
theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
have h, h' := rel_of_isEqv h
have h, h' := rel_of_isEqv (fun x y => x = y) a b h
exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
theorem isEqvAux_self (r : α α Bool) (hr : a, r a a) (a : Array α) (i : Nat) (h : i a.size) :
@@ -89,22 +56,4 @@ instance [DecidableEq α] : DecidableEq (Array α) :=
| true => isTrue (eq_of_isEqv a b h)
| false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
theorem beq_eq_decide [BEq α] (a b : Array α) :
(a == b) = if h : a.size = b.size then
decide ( (i : Nat) (h' : i < a.size), a[i] == b[i]'(h h')) else false := by
simp [BEq.beq, isEqv_eq_decide]
@[simp] theorem beq_toList [BEq α] (a b : Array α) : (a.toList == b.toList) = (a == b) := by
simp [beq_eq_decide, List.beq_eq_decide]
end Array
namespace List
@[simp] theorem isEqv_toArray [BEq α] (a b : List α) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r) := by
simp [isEqv_eq_decide, Array.isEqv_eq_decide]
@[simp] theorem beq_toArray [BEq α] (a b : List α) : (a.toArray == b.toArray) = (a == b) := by
simp [beq_eq_decide, Array.beq_eq_decide]
end List

View File

@@ -41,6 +41,6 @@ where
getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) h₂) :=
rfl
go (i : Nat) (hi : i as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.get_drop_eq_drop, *]
induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
end Array

View File

@@ -8,12 +8,7 @@ import Init.Data.Nat.Lemmas
import Init.Data.List.Impl
import Init.Data.List.Monadic
import Init.Data.List.Range
import Init.Data.List.Nat.TakeDrop
import Init.Data.List.Nat.Modify
import Init.Data.List.Monadic
import Init.Data.List.OfFn
import Init.Data.Array.Mem
import Init.Data.Array.DecidableEq
import Init.TacticsExtra
/-!
@@ -22,9 +17,12 @@ import Init.TacticsExtra
namespace Array
@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := rfl
theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
by_cases i < a.size <;> (try simp [*]) <;> rfl
theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] :=
getElem?_pos ..
@@ -45,35 +43,21 @@ theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[
rw [getElem?_eq]
split <;> simp_all
theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
(a.push x)[i] = a[i] := by
simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
@[simp] theorem getElem_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
@[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]
theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
(a.push x)[i] = if h : i < a.size then a[i] else x := by
by_cases h' : i < a.size
· simp [getElem_push_lt, h']
· simp [get_push_lt, h']
· simp at h
simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
@[deprecated getElem_push (since := "2024-10-21")] abbrev get_push := @getElem_push
@[deprecated getElem_push_lt (since := "2024-10-21")] abbrev get_push_lt := @getElem_push_lt
@[deprecated getElem_push_eq (since := "2024-10-21")] abbrev get_push_eq := @getElem_push_eq
@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
simp [getElem!_def, get!, getD]
split <;> rename_i h
· simp [getElem?_eq_getElem h]
rfl
· simp [getElem?_eq_none_iff.2 (by simpa using h)]
theorem singleton_inj : #[a] = #[b] a = b := by
simp
simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
end Array
@@ -90,8 +74,12 @@ We prefer to pull `List.toArray` outwards.
(a.toArrayAux b).size = b.size + a.length := by
simp [size]
@[simp] theorem mem_toArray {a : α} {l : List α} : a l.toArray a l := by
simp [mem_def]
@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
a.toArray[i] = a[i]'(by simpa using h) := rfl
@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
apply ext'
@@ -102,42 +90,6 @@ We prefer to pull `List.toArray` outwards.
funext a
simp
@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
cases l <;> simp
@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) a l.toArray β m (ForInStep β)) (i : Nat)
(h : i l.length) (b : β) :
Array.forIn'.loop l.toArray f i h b =
forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b) := by
induction i generalizing l b with
| zero =>
simp [Array.forIn'.loop]
| succ i ih =>
simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]
have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
simp only [Nat.sub_add_eq]
rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
simp only [Option.toList_some, singleton_append]
simp [t]
have t : l.length - 1 - i = l.length - i - 1 := by omega
simp only [t]
congr
@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) a l.toArray β m (ForInStep β)) :
forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
change Array.forIn' _ _ _ = List.forIn' _ _ _
rw [Array.forIn', forIn'_loop_toArray]
simp
@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α β m (ForInStep β)) :
forIn l.toArray b f = forIn l b f := by
simpa using forIn'_toArray l b fun a m b => f a b
theorem foldrM_toArray [Monad m] (f : α β m β) (init : β) (l : List α) :
l.toArray.foldrM f init = l.foldrM f init := by
rw [foldrM_eq_reverse_foldlM_toList]
@@ -195,9 +147,6 @@ namespace Array
@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
-- This is a duplicate of `List.toArray_toList`.
-- It's confusing to guess which namespace this theorem should live in,
-- so we provide both.
@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
@@ -206,32 +155,21 @@ namespace Array
@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
@[simp] theorem isEmpty_toList {l : Array α} : l.toList.isEmpty = l.isEmpty := by
rcases l with _ | _ <;> simp
theorem foldrM_push [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
simp [foldrM_eq_reverse_foldlM_toList, -size_push]
/--
Variant of `foldrM_push` with `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
-/
@[simp] theorem foldrM_push' [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α)
{start} (h : start = arr.size + 1) :
(arr.push a).foldrM f init start = f a init >>= arr.foldrM f := by
simp [ foldrM_push, h]
/-- Variant of `foldrM_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
@[simp] theorem foldrM_push' [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
simp [ foldrM_push]
theorem foldr_push (f : α β β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
/--
Variant of `foldr_push` with the `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
-/
@[simp] theorem foldr_push' (f : α β β) (init : β) (arr : Array α) (a : α) {start}
(h : start = arr.size + 1) : (arr.push a).foldr f init start = arr.foldr f (f a init) :=
foldrM_push' _ _ _ _ h
/-- Variant of `foldr_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
@[simp] theorem foldr_push' (f : α β β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
/-- A more efficient version of `arr.toList.reverse`. -/
@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
@@ -293,6 +231,9 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
(h : min stop as.size start) : anyM p as start stop = pure false := by
rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
theorem mem_def {a : α} {as : Array α} : a as a as.toList :=
fun | .mk h => h, Array.Mem.mk
@[simp] theorem not_mem_empty (a : α) : ¬(a #[]) := by
simp [mem_def]
@@ -307,7 +248,7 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
theorem getElem?_lt
(a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
(a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some (a[i]) := dif_pos h
theorem getElem?_ge
(a : Array α) {i : Nat} (h : i a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
@@ -330,33 +271,30 @@ theorem getD_get? (a : Array α) (i : Nat) (d : α) :
theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
a.get! i = (a.get? i).getD default := by
by_cases p : i < a.size <;>
simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]
@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
/-! # set -/
@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
(eq : i = j) (p : j < (a.set i v).size) :
@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
(eq : i.val = j) (p : j < (a.set i v).size) :
(a.set i v)[j]'p = v := by
simp [set, getElem_eq_getElem_toList, eq]
@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
(pj : j < (a.set i v).size) (h : i j) :
(a.set i v)[j]'pj = a[j]'(size_set a i v _ pj) := by
@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
(h : i.val j) : (a.set i v)[j]'pj = a[j]'(size_set a i v pj) := by
simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
(h : j < (a.set i v).size) :
(a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ h) := by
by_cases p : i = j <;> simp [p]
(a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v h) := by
by_cases p : i.1 = j <;> simp [p]
@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
(a.set i v)[i]? = v := by simp [getElem?_lt, h]
@[simp] theorem getElem?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1]? = v := by simp [getElem?_lt, i.2]
@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
(ne : i j) : (a.set i v)[j]? = a[j]? := by
@[simp] theorem getElem?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
(ne : i.val j) : (a.set i v)[j]? = a[j]? := by
by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
/-! # setD -/
@@ -373,7 +311,7 @@ theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat
@[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
(setD a i v)[i]'h = v := by
simp at h
simp only [setD, h, reduceDIte, getElem_set_eq]
simp only [setD, h, dite_true, getElem_set, ite_true]
@[simp]
theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
@@ -414,8 +352,8 @@ theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
simp only [dif_pos hin]
rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
| inl hj => simp [getElem_push, hj, hacc j hj]
| inr hj => simp [getElem_push, *]
| inl hj => simp [get_push, hj, hacc j hj]
| inr hj => simp [get_push, *]
else
simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi hin)))]
termination_by n - i
@@ -483,16 +421,18 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
idx < a.size :=
hidx
theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] l := by
erw [Array.mem_def, getElem_eq_getElem_toList]
apply List.get_mem
theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a.toList[i] := rfl
@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
a[i] = a[i.toNat] := rfl
theorem getElem?_size_le (a : Array α) (i : Nat) (h : a.size i) : a[i]? = none := by
theorem get?_len_le (a : Array α) (i : Nat) (h : a.size i) : a[i]? = none := by
simp [getElem?_neg, h]
@[deprecated getElem?_size_le (since := "2024-10-21")] abbrev get?_len_le := @getElem?_size_le
theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] a.toList := by
simp only [getElem_eq_getElem_toList, List.getElem_mem]
@@ -500,40 +440,35 @@ theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get?
simp [getElem?_eq_getElem?_toList]
theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
simp only [get!_eq_getElem?, get?_eq_getElem?]
simp [get!_eq_getD]
theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a h : n < as.size, as[n] = a := by
cases as
simp [List.getElem?_eq_some_iff]
theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by
simp only [back!, get!_eq_getElem?, get?_eq_getElem?, back?]
@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
simp [back, back?]
@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
simp [back?, getElem?_eq_getElem?_toList]
@[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
simp [back!_eq_back?]
theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
(a.push x)[i]? = some a[i] := by
rw [getElem?_pos, getElem_push_lt]
rw [getElem?_pos, get_push_lt]
@[deprecated getElem?_push_lt (since := "2024-10-21")] abbrev get?_push_lt := @getElem?_push_lt
theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
rw [getElem?_pos, get_push_eq]
theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
rw [getElem?_pos, getElem_push_eq]
@[deprecated getElem?_push_eq (since := "2024-10-21")] abbrev get?_push_eq := @getElem?_push_eq
theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
match Nat.lt_trichotomy i a.size with
| Or.inl g =>
have h1 : i < a.size + 1 := by omega
have h2 : i a.size := by omega
simp [getElem?_def, size_push, g, h1, h2, getElem_push_lt]
simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
| Or.inr (Or.inl heq) =>
simp [heq, getElem?_pos, getElem_push_eq]
simp [heq, getElem?_pos, get_push_eq]
| Or.inr (Or.inr g) =>
simp only [getElem?_def, size_push]
have h1 : ¬ (i < a.size) := by omega
@@ -541,50 +476,46 @@ theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some
have h3 : i a.size := by omega
simp [h1, h2, h3]
@[deprecated getElem?_push (since := "2024-10-21")] abbrev get?_push := @getElem?_push
@[simp] theorem getElem?_size {a : Array α} : a[a.size]? = none := by
@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
simp only [getElem?_def, Nat.lt_irrefl, dite_false]
@[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
@[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
@[simp] theorem toList_set (a : Array α) (i v h) : (a.set i v).toList = a.toList.set i v := rfl
theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
(a.set i v h)[i]'(by simp [h]) = v := by
theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1] = v := by
simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
theorem get?_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
(a.set i v)[i]? = v := by simp [getElem?_pos, h]
theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
@[simp] theorem get?_set_ne (a : Array α) (i : Nat) (h' : i < a.size) {j : Nat} (v : α)
(h : i j) : (a.set i v)[j]? = a[j]? := by
@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
(h : i.1 j) : (a.set i v)[j]? = a[j]? := by
by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
theorem get?_set (a : Array α) (i : Nat) (h : i < a.size) (j : Nat) (v : α) :
(a.set i v)[j]? = if i = j then some v else a[j]? := by
if h : i = j then subst j; simp [*] else simp [*]
theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
(a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
if h : i.1 = j then subst j; simp [*] else simp [*]
theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a.size) (v : α) :
theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
(a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
if h : i = j then subst j; simp [*] else simp [*]
if h : i.1 = j then subst j; simp [*] else simp [*]
@[simp] theorem get_set_ne (a : Array α) (i : Nat) (hi : i < a.size) {j : Nat} (v : α) (hj : j < a.size)
(h : i j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
(h : i.1 j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
(setD a i v)[i] = v := by
simp at h
simp only [setD, h, reduceDIte, getElem_set_eq]
simp only [setD, h, dite_true, get_set, ite_true]
theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
(a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
(a.set i v).set i, by simp [i.2] v' = a.set i v' := by simp [set, List.set_set]
private theorem fin_cast_val (e : n = n') (i : Fin n) : e i = i.1, e i.2 := by cases e; rfl
theorem swap_def (a : Array α) (i j : Fin a.size) :
a.swap i j = (a.set i (a.get j)).set j (a.get i) := by
a.swap i j = (a.set i (a.get j)).set j.1, by simp [j.2] (a.get i) := by
simp [swap, fin_cast_val]
@[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
@@ -597,12 +528,9 @@ theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)
@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
a.swapAt i v = (a[i.1], a.set i v) := rfl
@[simp] theorem size_swapAt (a : Array α) (i : Fin a.size) (v : α) :
(a.swapAt i v).2.size = a.size := by simp [swapAt_def]
@[simp]
theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
a.swapAt! i v = (a[i], a.set i v) := by simp [swapAt!, h]
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
@@ -626,22 +554,22 @@ theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] :=
· simp [h]
· intros; contradiction
theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size 0) :
as = as.pop.push as.back! := by
theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size 0) :
as = as.pop.push as.back := by
apply ext
· simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
· intros i h h'
if hlt : i < as.pop.size then
rw [getElem_push_lt (h:=hlt), getElem_pop]
rw [get_push_lt (h:=hlt), getElem_pop]
else
have heq : i = as.pop.size :=
Nat.le_antisymm (size_pop .. Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
cases heq; rw [getElem_push_eq, back!, size_pop, get!_eq_getD, getD, dif_pos h]; rfl
cases heq; rw [get_push_eq, back, size_pop, get!_eq_getD, getD, dif_pos h]; rfl
theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size 0) :
(bs : Array α) (c : α), as = bs.push c :=
let _ : Inhabited α := as[0]
as.pop, as.back!, eq_push_pop_back!_of_size_ne_zero h
as.pop, as.back, eq_push_pop_back_of_size_ne_zero h
theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl
@@ -714,82 +642,6 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
true_and, Nat.not_lt] at h
rw [List.getElem?_eq_none_iff.2 _, List.getElem?_eq_none_iff.2 (a.toList.length_reverse _)]
/-! ### BEq -/
@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ReflBEq α := by
constructor
· intro h
constructor
intro a
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
apply Array.isEqv_self_beq
@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) LawfulBEq α := by
constructor
· intro h
constructor
· intro a b h
apply singleton_inj.1
apply eq_of_beq
simp only [instBEq, isEqv, isEqvAux]
simpa
· intro a
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
· intro a b h
obtain hs, hi := rel_of_isEqv h
ext i h₁ h₂
· exact hs
· simpa using hi _ h₁
· intro a
apply Array.isEqv_self_beq
/-! ### take -/
@[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by
induction n generalizing a with
| zero => simp [take.loop]
| succ n ih =>
simp [take.loop, ih]
omega
@[simp] theorem getElem_take_loop (a : Array α) (n : Nat) (i : Nat) (h : i < (take.loop n a).size) :
(take.loop n a)[i] = a[i]'(by simp at h; omega) := by
induction n generalizing a i with
| zero => simp [take.loop]
| succ n ih =>
simp [take.loop, ih]
@[simp] theorem size_take (a : Array α) (n : Nat) : (a.take n).size = min n a.size := by
simp [take]
omega
@[simp] theorem getElem_take (a : Array α) (n : Nat) (i : Nat) (h : i < (a.take n).size) :
(a.take n)[i] = a[i]'(by simp at h; omega) := by
simp [take]
@[simp] theorem toList_take (a : Array α) (n : Nat) : (a.take n).toList = a.toList.take n := by
apply List.ext_getElem <;> simp
/-! ### forIn -/
@[simp] theorem forIn_toList [Monad m] (as : Array α) (b : β) (f : α β m (ForInStep β)) :
forIn as.toList b f = forIn as b f := by
cases as
simp
@[simp] theorem forIn'_toList [Monad m] (as : Array α) (b : β) (f : (a : α) a as.toList β m (ForInStep β)) :
forIn' as.toList b f = forIn' as b (fun a m b => f a (mem_toList.mpr m) b) := by
cases as
simp
/-! ### foldl / foldr -/
@[simp] theorem foldlM_loop_empty [Monad m] (f : β α m β) (init : β) (i j : Nat) :
@@ -910,7 +762,7 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
obtain m, eq, w := t
· refine m, by simpa [map_eq_foldl] using eq, ?_
intro i h
simp only [eq] at w
simp [eq] at w
specialize w i, h h
simpa [map_eq_foldl] using w
· exact h0, rfl, nofun
@@ -921,9 +773,9 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
· intro j h
simp at h
by_cases h' : j < size b
· rw [getElem_push]
· rw [get_push]
simp_all
· rw [getElem_push, dif_neg h']
· rw [get_push, dif_neg h']
simp only [show j = i by omega]
exact (hs _ m).1
@@ -948,7 +800,7 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
(as.push x).map f = (as.map f).push (f x) := by
ext
· simp
· simp only [getElem_map, getElem_push, size_map]
· simp only [getElem_map, get_push, size_map]
split <;> rfl
@[simp] theorem map_pop {f : α β} {as : Array α} :
@@ -967,15 +819,9 @@ theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
(as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by
simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
split
· simp only [Id.bind_eq, get_set _ _ _ _ (by simpa using h)]; split <;> simp [*]
· simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
· rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
@[simp] theorem toList_modify (as : Array α) (f : α α) :
(as.modify x f).toList = as.toList.modify f x := by
apply List.ext_getElem
· simp
· simp [getElem_modify, List.getElem_modify]
theorem getElem_modify_self {as : Array α} {i : Nat} (f : α α) (h : i < (as.modify i f).size) :
(as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
simp [getElem_modify h]
@@ -985,11 +831,6 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
(as.modify i f)[j] = as[j]'(by simpa using hj) := by
simp [getElem_modify hj, h]
theorem getElem?_modify {as : Array α} {i : Nat} {f : α α} {j : Nat} :
(as.modify i f)[j]? = if i = j then as[j]?.map f else as[j]? := by
simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
split <;> split <;> rfl
/-! ### filter -/
@[simp] theorem toList_filter (p : α Bool) (l : Array α) :
@@ -1051,7 +892,7 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
theorem size_empty : (#[] : Array α).size = 0 := rfl
@[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
theorem toList_empty : (#[] : Array α).toList = [] := rfl
/-! ### append -/
@@ -1083,38 +924,18 @@ theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle :
conv => rhs; rw [ List.getElem_append_right (h₁ := hle) (h₂ := h')]
apply List.get_of_eq; rw [toList_append]
theorem getElem?_append_left {as bs : Array α} {n : Nat} (hn : n < as.size) :
(as ++ bs)[n]? = as[n]? := by
have hn' : n < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
size_append .. Nat.le_add_right ..
simp_all [getElem?_eq_getElem, getElem_append]
theorem getElem?_append_right {as bs : Array α} {n : Nat} (h : as.size n) :
(as ++ bs)[n]? = bs[n - as.size]? := by
cases as
cases bs
simp at h
simp [List.getElem?_append_right, h]
theorem getElem?_append {as bs : Array α} {n : Nat} :
(as ++ bs)[n]? = if n < as.size then as[n]? else bs[n - as.size]? := by
split <;> rename_i h
· exact getElem?_append_left h
· exact getElem?_append_right (by simpa using h)
@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
apply ext'; simp only [toList_append, toList_empty, List.append_nil]
@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
apply ext'; simp only [toList_append, toList_empty, List.nil_append]
@[simp] theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
apply ext'; simp only [toList_append, List.append_assoc]
/-! ### 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).flatten := by
dsimp [flatten]
simp only [foldl_eq_foldl_toList]
generalize l.toList = l
@@ -1229,7 +1050,7 @@ theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i
have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, getElem_push_eq]
rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
rw [h]; congr; rw [Nat.add_sub_cancel]
else
have hge : bs.size + 1 i := Nat.lt_of_le_of_ne hge hi
@@ -1256,14 +1077,6 @@ theorem getElem?_extract {as : Array α} {start stop : Nat} :
· omega
· rfl
@[simp] theorem toList_extract (as : Array α) (start stop : Nat) :
(as.extract start stop).toList = (as.toList.drop start).take (stop - start) := by
apply List.ext_getElem
· simp only [length_toList, size_extract, List.length_take, List.length_drop]
omega
· intros n h₁ h₂
simp
@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
apply ext
· rw [size_extract, Nat.min_self, Nat.sub_zero]
@@ -1407,18 +1220,33 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
open Fin
@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.1] = a[i] := by
simp [swap_def, getElem_set]
@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.1] = a[j] := by
simp +contextual [swap_def, getElem_set]
@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
if he : ((Array.size_set _ _ _).symm j).val = i.val then by
simp only [he, fin_cast_val, getElem_swap_right, getElem_fin]
else by
apply Eq.trans
· apply Array.get_set_ne
· simp only [size_set, Fin.isLt]
· assumption
· simp [get_set_ne]
@[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
(hi : p i) (hj : p j) : (a.swap i j)[p]'(a.size_swap .. |>.symm hp) = a[p] := by
simp [swap_def, getElem_set, hi.symm, hj.symm]
apply Eq.trans
· have : ((a.size_set i (a.get j)).symm j).val = j.val := by simp only [fin_cast_val]
apply Array.get_set_ne
· simp only [this]
apply Ne.symm
· assumption
· apply Array.get_set_ne
· apply Ne.symm
· assumption
theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
(a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
(a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
split
· simp_all only [getElem_swap_left]
· split <;> simp_all
@@ -1428,7 +1256,7 @@ theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.sw
apply getElem_swap'
@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
(a.swap i j).swap i.1, (a.size_swap ..).symm i.2 j.1, (a.size_swap ..).symm j.2 = a := by
(a.swap i j).swap i.1, (a.size_swap ..).symm i.2 j.1, (a.size_swap ..).symm j.2 = a := by
apply ext
· simp only [size_swap]
· intros
@@ -1458,6 +1286,9 @@ namespace List
Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
-/
@[simp] theorem mem_toArray {a : α} {l : List α} : a l.toArray a l := by
simp [mem_def]
@[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
simp
@@ -1466,10 +1297,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
apply ext'
simp
@[simp] theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray := by
apply ext'
simp
@[simp] theorem mapM_toArray [Monad m] [LawfulMonad m] (f : α m β) (l : List α) :
l.toArray.mapM f = List.toArray <$> l.mapM f := by
simp only [ mapM'_eq_mapM, mapM_eq_foldlM]
@@ -1564,11 +1391,6 @@ theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p
apply ext'
simp
@[simp] theorem modify_toArray (f : α α) (l : List α) :
l.toArray.modify i f = (l.modify f i).toArray := by
apply ext'
simp
@[simp] theorem filter_toArray' (p : α Bool) (l : List α) (h : stop = l.toArray.size) :
l.toArray.filter p 0 stop = (l.filter p).toArray := by
subst h
@@ -1597,26 +1419,8 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
apply ext'
simp
@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
apply ext'
simp
@[simp] theorem toArray_ofFn (f : Fin n α) : (ofFn f).toArray = Array.ofFn f := by
ext <;> simp
end List
namespace Array
@[simp] theorem mapM_id {l : Array α} {f : α Id β} : l.mapM f = l.map f := by
induction l; simp_all
@[simp] theorem toList_ofFn (f : Fin n α) : (Array.ofFn f).toList = List.ofFn f := by
apply List.ext_getElem <;> simp
end Array
/-! ### Deprecations -/
namespace List
@@ -1630,8 +1434,6 @@ theorem toArray_concat {as : List α} {x : α} :
apply ext'
simp
@[deprecated back!_toArray (since := "2024-10-31")] abbrev back_toArray := @back!_toArray
end List
namespace Array
@@ -1772,9 +1574,4 @@ abbrev get_swap := @getElem_swap
@[deprecated getElem_swap' (since := "2024-09-30")]
abbrev get_swap' := @getElem_swap'
@[deprecated back!_eq_back? (since := "2024-10-31")] abbrev back_eq_back? := @back!_eq_back?
@[deprecated back!_push (since := "2024-10-31")] abbrev back_push := @back!_push
@[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
end Array

View File

@@ -9,104 +9,56 @@ import Init.Data.List.MapIdx
namespace Array
/-! ### mapFinIdx -/
/-! ### mapIdx -/
-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
theorem mapFinIdx_induction (as : Array α) (f : Fin as.size α β)
theorem mapIdx_induction (as : Array α) (f : Fin as.size α β)
(motive : Nat Prop) (h0 : motive 0)
(p : Fin as.size β Prop)
(hs : i, motive i.1 p i (f i as[i]) motive (i + 1)) :
motive as.size eq : (Array.mapFinIdx as f).size = as.size,
i h, p i, h ((Array.mapFinIdx as f)[i]) := by
motive as.size eq : (Array.mapIdx as f).size = as.size,
i h, p i, h ((Array.mapIdx as f)[i]) := by
let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : i h h', p i, h bs[i]) (hm : motive j) :
let arr : Array β := Array.mapFinIdxM.map (m := Id) as f i j h bs
let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
motive as.size eq : arr.size = as.size, i h, p i, h arr[i] := by
induction i generalizing j bs with simp [mapFinIdxM.map]
induction i generalizing j bs with simp [mapIdxM.map]
| zero =>
have := (Nat.zero_add _).symm.trans h
exact this hm, h₁ this, fun _ _ => h₂ ..
| succ i ih =>
apply @ih (bs.push (f j, by omega as[j])) (j + 1) (by omega) (by simp; omega)
· intro i i_lt h'
rw [getElem_push]
rw [get_push]
split
· apply h₂
· simp only [size_push] at h'
obtain rfl : i = j := by omega
apply (hs i, by omega hm).1
· exact (hs j, by omega hm).2
simp [mapFinIdx, mapFinIdxM]; exact go rfl nofun h0
simp [mapIdx, mapIdxM]; exact go rfl nofun h0
theorem mapFinIdx_spec (as : Array α) (f : Fin as.size α β)
(p : Fin as.size β Prop) (hs : i, p i (f i as[i])) :
eq : (Array.mapFinIdx as f).size = as.size,
i h, p i, h ((Array.mapFinIdx as f)[i]) :=
(mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ => hs .., trivial).2
@[simp] theorem size_mapFinIdx (a : Array α) (f : Fin a.size α β) : (a.mapFinIdx f).size = a.size :=
(mapFinIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
Array.size_mapFinIdx _ _
@[simp] theorem getElem_mapFinIdx (a : Array α) (f : Fin a.size α β) (i : Nat)
(h : i < (mapFinIdx a f).size) :
(a.mapFinIdx f)[i] = f i, by simp_all (a[i]'(by simp_all)) :=
(mapFinIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : Fin a.size α β) (i : Nat) :
(a.mapFinIdx f)[i]? =
a[i]?.pbind fun b h => f i, (getElem?_eq_some_iff.1 h).1 b := by
simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
split <;> simp_all
@[simp] theorem toList_mapFinIdx (a : Array α) (f : Fin a.size α β) :
(a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a => f i, by simp a) := by
apply List.ext_getElem <;> simp
/-! ### mapIdx -/
theorem mapIdx_induction (as : Array α) (f : Nat α β)
(motive : Nat Prop) (h0 : motive 0)
(p : Fin as.size β Prop)
(hs : i, motive i.1 p i (f i as[i]) motive (i + 1)) :
motive as.size eq : (Array.mapIdx as f).size = as.size,
i h, p i, h ((Array.mapIdx as f)[i]) :=
mapFinIdx_induction as (fun i a => f i a) motive h0 p hs
theorem mapIdx_spec (as : Array α) (f : Nat α β)
theorem mapIdx_spec (as : Array α) (f : Fin as.size α β)
(p : Fin as.size β Prop) (hs : i, p i (f i as[i])) :
eq : (Array.mapIdx as f).size = as.size,
i h, p i, h ((Array.mapIdx as f)[i]) :=
(mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => hs .., trivial).2
@[simp] theorem size_mapIdx (a : Array α) (f : Nat α β) : (a.mapIdx f).size = a.size :=
@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size α β) : (a.mapIdx f).size = a.size :=
(mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
@[simp] theorem getElem_mapIdx (a : Array α) (f : Nat α β) (i : Nat)
@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
Array.size_mapIdx _ _
@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size α β) (i : Nat)
(h : i < (mapIdx a f).size) :
(a.mapIdx f)[i] = f i (a[i]'(by simp_all)) :=
(mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i (by simp_all)
(a.mapIdx f)[i] = f i, by simp_all (a[i]'(by simp_all)) :=
(mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
@[simp] theorem getElem?_mapIdx (a : Array α) (f : Nat α β) (i : Nat) :
@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size α β) (i : Nat) :
(a.mapIdx f)[i]? =
a[i]?.map (f i) := by
simp [getElem?_def, size_mapIdx, getElem_mapIdx]
@[simp] theorem toList_mapIdx (a : Array α) (f : Nat α β) :
(a.mapIdx f).toList = a.toList.mapIdx (fun i a => f i a) := by
apply List.ext_getElem <;> simp
a[i]?.pbind fun b h => f i, (getElem?_eq_some_iff.1 h).1 b := by
simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
split <;> simp_all
end Array
namespace List
@[simp] theorem mapFinIdx_toArray (l : List α) (f : Fin l.length α β) :
l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
ext <;> simp
@[simp] theorem mapIdx_toArray (l : List α) (f : Nat α β) :
l.toArray.mapIdx f = (l.mapIdx f).toArray := by
ext <;> simp
end List

View File

@@ -10,6 +10,15 @@ import Init.Data.List.BasicAux
namespace Array
/-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
-- NB: This is defined as a structure rather than a plain def so that a lemma
-- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
structure Mem (as : Array α) (a : α) : Prop where
val : a as.toList
instance : Membership α (Array α) where
mem := Mem
theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a as) : sizeOf a < sizeOf as := by
cases as with | _ as =>
exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)

View File

@@ -1,39 +0,0 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Tactics
/--
Set an element in an array, using a proof that the index is in bounds.
(This proof can usually be omitted, and will be synthesized automatically.)
This will perform the update destructively provided that `a` has a reference
count of 1 when called.
-/
@[extern "lean_array_fset"]
def Array.set (a : Array α) (i : @& Nat) (v : α) (h : i < a.size := by get_elem_tactic) :
Array α where
toList := a.toList.set i v
/--
Set an element in an array, or do nothing if the index is out of bounds.
This will perform the update destructively provided that `a` has a reference
count of 1 when called.
-/
@[inline] def Array.setD (a : Array α) (i : Nat) (v : α) : Array α :=
dite (LT.lt i a.size) (fun h => a.set i v h) (fun _ => a)
/--
Set an element in an array, or panic if the index is out of bounds.
This will perform the update destructively provided that `a` has a reference
count of 1 when called.
-/
@[extern "lean_array_set"]
def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
Array.setD a i v

View File

@@ -634,16 +634,6 @@ def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w <<< i
end bitwise
/-- Compute a hash of a bitvector, combining 64-bit words using `mixHash`. -/
def hash (bv : BitVec n) : UInt64 :=
if n 64 then
bv.toFin.val.toUInt64
else
mixHash (bv.toFin.val.toUInt64) (hash ((bv >>> 64).setWidth (n - 64)))
instance : Hashable (BitVec n) where
hash := hash
section normalization_eqs
/-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
@[simp] theorem append_eq (x : BitVec w) (y : BitVec v) : BitVec.append x y = x ++ y := rfl

View File

@@ -174,30 +174,6 @@ theorem carry_succ (i : Nat) (x y : BitVec w) (c : Bool) :
exact mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ ..
cases x.toNat.testBit i <;> cases y.toNat.testBit i <;> (simp; omega)
theorem carry_succ_one (i : Nat) (x : BitVec w) (h : 0 < w) :
carry (i+1) x (1#w) false = decide ( j i, x.getLsbD j = true) := by
induction i with
| zero => simp [carry_succ, h]
| succ i ih =>
rw [carry_succ, ih]
simp only [getLsbD_one, add_one_ne_zero, decide_False, Bool.and_false, atLeastTwo_false_mid]
cases hx : x.getLsbD (i+1)
case false =>
have : j i + 1, x.getLsbD j = false :=
i+1, by omega, hx
simpa
case true =>
suffices
( (j : Nat), j i x.getLsbD j = true)
( (j : Nat), j i + 1 x.getLsbD j = true) by
simpa
constructor
· intro h j hj
rcases Nat.le_or_eq_of_le_succ hj with (hj' | rfl)
· apply h; assumption
· exact hx
· intro h j hj; apply h; omega
/--
If `x &&& y = 0`, then the carry bit `(x + y + 0)` is always `false` for any index `i`.
Intuitively, this is because a carry is only produced when at least two of `x`, `y`, and the
@@ -376,117 +352,6 @@ theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c
simp [ sub_toAdd, BitVec.sub_add_cancel]
· simp [bit_not_testBit x _]
/--
Remember that negating a bitvector is equal to incrementing the complement
by one, i.e., `-x = ~~~x + 1`. See also `neg_eq_not_add`.
This computation has two crucial properties:
- The least significant bit of `-x` is the same as the least significant bit of `x`, and
- The `i+1`-th least significant bit of `-x` is the complement of the `i+1`-th bit of `x`, unless
all of the preceding bits are `false`, in which case the bit is equal to the `i+1`-th bit of `x`
-/
theorem getLsbD_neg {i : Nat} {x : BitVec w} :
getLsbD (-x) i =
(getLsbD x i ^^ decide (i < w) && decide ( j < i, getLsbD x j = true)) := by
rw [neg_eq_not_add]
by_cases hi : i < w
· rw [getLsbD_add hi]
have : 0 < w := by omega
simp only [getLsbD_not, hi, decide_True, Bool.true_and, getLsbD_one, this, not_bne,
_root_.true_and, not_eq_eq_eq_not]
cases i with
| zero =>
have carry_zero : carry 0 ?x ?y false = false := by
simp [carry]; omega
simp [hi, carry_zero]
| succ =>
rw [carry_succ_one _ _ (by omega), Bool.xor_not, decide_not]
simp only [add_one_ne_zero, decide_False, getLsbD_not, and_eq_true, decide_eq_true_eq,
not_eq_eq_eq_not, Bool.not_true, false_bne, not_exists, _root_.not_and, not_eq_true,
bne_left_inj, decide_eq_decide]
constructor
· rintro h j hj; exact And.right <| h j (by omega)
· rintro h j hj; exact by omega, h j (by omega)
· have h_ge : w i := by omega
simp [getLsbD_ge _ _ h_ge, h_ge, hi]
theorem getMsbD_neg {i : Nat} {x : BitVec w} :
getMsbD (-x) i =
(getMsbD x i ^^ decide ( j < w, i < j getMsbD x j = true)) := by
simp only [getMsbD, getLsbD_neg, Bool.decide_and, Bool.and_eq_true, decide_eq_true_eq]
by_cases hi : i < w
case neg =>
simp [hi]; omega
case pos =>
have h₁ : w - 1 - i < w := by omega
simp only [hi, decide_True, h₁, Bool.true_and, Bool.bne_left_inj, decide_eq_decide]
constructor
· rintro j, hj, h
refine w - 1 - j, by omega, by omega, by omega, _root_.cast ?_ h
congr; omega
· rintro j, hj₁, hj₂, -, h
exact w - 1 - j, by omega, h
theorem msb_neg {w : Nat} {x : BitVec w} :
(-x).msb = ((x != 0#w && x != intMin w) ^^ x.msb) := by
simp only [BitVec.msb, getMsbD_neg]
by_cases hmin : x = intMin _
case pos =>
have : ( j, j < w 0 < j 0 < w j = 0) False := by
simp; omega
simp [hmin, getMsbD_intMin, this]
case neg =>
by_cases hzero : x = 0#w
case pos => simp [hzero]
case neg =>
have w_pos : 0 < w := by
cases w
· rw [@of_length_zero x] at hzero
contradiction
· omega
suffices j, j < w 0 < j x.getMsbD j = true
by simp [show x != 0#w by simpa, show x != intMin w by simpa, this]
false_or_by_contra
rename_i getMsbD_x
simp only [not_exists, _root_.not_and, not_eq_true] at getMsbD_x
/- `getMsbD` says that all bits except the msb are `false` -/
cases hmsb : x.msb
case true =>
apply hmin
apply eq_of_getMsbD_eq
rintro i, hi
simp only [getMsbD_intMin, w_pos, decide_True, Bool.true_and]
cases i
case zero => exact hmsb
case succ => exact getMsbD_x _ hi (by omega)
case false =>
apply hzero
apply eq_of_getMsbD_eq
rintro i, hi
simp only [getMsbD_zero]
cases i
case zero => exact hmsb
case succ => exact getMsbD_x _ hi (by omega)
/-! ### abs -/
theorem msb_abs {w : Nat} {x : BitVec w} :
x.abs.msb = (decide (x = intMin w) && decide (0 < w)) := by
simp only [BitVec.abs, getMsbD_neg, ne_eq, decide_not, Bool.not_bne]
by_cases h₀ : 0 < w
· by_cases h₁ : x = intMin w
· simp [h₁, msb_intMin]
· simp only [neg_eq, h₁, decide_False]
by_cases h₂ : x.msb
· simp [h₂, msb_neg]
and_intros
· by_cases h₃ : x = 0#w
· simp [h₃] at h₂
· simp [h₃]
· simp [h₁]
· simp [h₂]
· simp [BitVec.msb, show w = 0 by omega]
/-! ### Inequalities (le / lt) -/
theorem ult_eq_not_carry (x y : BitVec w) : x.ult y = !carry w x (~~~y) true := by

View File

@@ -316,12 +316,6 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
simp [Nat.sub_sub_eq_min, Nat.min_eq_right]
omega
@[simp] theorem sub_add_bmod_cancel {x y : BitVec w} :
((((2 ^ w : Nat) - y.toNat) : Int) + x.toNat).bmod (2 ^ w) =
((x.toNat : Int) - y.toNat).bmod (2 ^ w) := by
rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm, Int.bmod_add_cancel, Int.add_comm,
Int.sub_eq_add_neg]
private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m n) : x < 2 ^ n :=
Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
@@ -1062,7 +1056,7 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
@[simp]
theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by
theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
apply eq_of_toNat_eq
simp
@@ -1232,11 +1226,7 @@ theorem ushiftRight_or_distrib (x y : BitVec w) (n : Nat) :
simp
@[simp]
theorem ushiftRight_zero (x : BitVec w) : x >>> 0 = x := by
simp [bv_toNat]
@[simp]
theorem zero_ushiftRight {n : Nat} : 0#w >>> n = 0#w := by
theorem ushiftRight_zero_eq (x : BitVec w) : x >>> 0 = x := by
simp [bv_toNat]
/--
@@ -1391,10 +1381,6 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
ext i
simp [getLsbD_sshiftRight]
@[simp] theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by
ext i
simp [getLsbD_sshiftRight]
theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
ext i
@@ -1792,7 +1778,7 @@ theorem setWidth_succ (x : BitVec w) :
· simp_all
· omega
@[deprecated "Use the reverse direction of `cons_msb_setWidth`" (since := "2024-09-23")]
@[deprecated "Use the reverse direction of `cons_msb_setWidth`"]
theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
simp
@@ -1917,31 +1903,6 @@ theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat}
ext
simp [getLsbD_concat]
@[simp]
theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} :
(x.concat b).getMsbD i = if i < w then x.getMsbD i else decide (i = w) && b := by
simp only [getMsbD_eq_getLsbD, Nat.add_sub_cancel, getLsbD_concat]
by_cases h₀ : i = w
· simp [h₀]
· by_cases h₁ : i < w
· simp [h₀, h₁, show ¬ w - i = 0 by omega, show i < w + 1 by omega, Nat.sub_sub, Nat.add_comm]
· simp only [show w - i = 0 by omega, reduceIte, h₁, h₀, decide_False, Bool.false_and,
Bool.and_eq_false_imp, decide_eq_true_eq]
intro
omega
@[simp]
theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
(x.concat b).msb = if 0 < w then x.msb else b := by
simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_True, Nat.add_one_sub_one,
Nat.sub_zero, Bool.true_and]
by_cases h₀ : 0 < w
· simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, reduceIte, decide_True,
Bool.true_and, ite_eq_right_iff]
intro
omega
· simp [h₀, show w = 0 by omega]
/-! ### add -/
theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
@@ -2013,10 +1974,6 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
@[simp] theorem toNat_sub {n} (x y : BitVec n) :
(x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
@[simp, bv_toNat] theorem toInt_sub {x y : BitVec w} :
(x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w) := by
simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
-- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
-- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
-- results in `omega` generating proof terms that are very slow in the kernel.
@@ -2039,8 +1996,6 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
@[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp
@[simp] protected theorem zero_sub (x : BitVec n) : 0#n - x = -x := rfl
@[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by
apply eq_of_toNat_eq
simp only [toNat_sub]
@@ -2053,8 +2008,18 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
theorem toInt_neg {x : BitVec w} :
(-x).toInt = (-x.toInt).bmod (2 ^ w) := by
rw [ BitVec.zero_sub, toInt_sub]
simp [BitVec.toInt_ofNat]
simp only [toInt_eq_toNat_bmod, toNat_neg, Int.ofNat_emod, Int.emod_bmod_congr]
rw [ Int.subNatNat_of_le (by omega), Int.subNatNat_eq_coe, Int.sub_eq_add_neg, Int.add_comm,
Int.bmod_add_cancel]
by_cases h : x.toNat < ((2 ^ w) + 1) / 2
· rw [Int.bmod_pos (x := x.toNat)]
all_goals simp only [toNat_mod_cancel']
norm_cast
· rw [Int.bmod_neg (x := x.toNat)]
· simp only [toNat_mod_cancel']
rw_mod_cast [Int.neg_sub, Int.sub_eq_add_neg, Int.add_comm, Int.bmod_add_cancel]
· norm_cast
simp_all
@[simp] theorem toFin_neg (x : BitVec n) :
(-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=
@@ -2146,6 +2111,17 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
omega
/-! ### abs -/
@[simp, bv_toNat]
theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
simp only [BitVec.abs, neg_eq]
by_cases h : x.msb = true
· simp only [h, reduceIte, toNat_neg]
have : 2 * x.toNat 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
rw [Nat.mod_eq_of_lt (by omega)]
· simp [h]
/-! ### mul -/
theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
@@ -2173,23 +2149,18 @@ instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
right_id := BitVec.mul_one
@[simp]
theorem mul_zero {x : BitVec w} : x * 0#w = 0#w := by
theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by
apply eq_of_toNat_eq
simp [toNat_mul]
@[simp]
theorem zero_mul {x : BitVec w} : 0#w * x = 0#w := by
apply eq_of_toNat_eq
simp [toNat_mul]
theorem mul_add {x y z : BitVec w} :
theorem BitVec.mul_add {x y z : BitVec w} :
x * (y + z) = x * y + x * z := by
apply eq_of_toNat_eq
simp only [toNat_mul, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod]
rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
Nat.mul_mod, Nat.mul_add]
theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [mul_add]
theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [BitVec.mul_add]
theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add]
theorem mul_two {x : BitVec w} : x * 2#w = x + x := by
@@ -2370,11 +2341,6 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
rcases hy with rfl | rfl <;>
rfl
/-! ### smtUDiv -/
theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
simp [smtUDiv]
/-! ### sdiv -/
/-- Equation theorem for `sdiv` in terms of `udiv`. -/
@@ -2431,28 +2397,6 @@ theorem sdiv_self {x : BitVec w} :
rcases x.msb with msb | msb <;> simp
· rcases x.msb with msb | msb <;> simp [h]
/-! ### smtSDiv -/
theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
match x.msb, y.msb with
| false, false => smtUDiv x y
| false, true => -(smtUDiv x (-y))
| true, false => -(smtUDiv (-x) y)
| true, true => smtUDiv (-x) (-y) := by
rw [BitVec.smtSDiv]
rcases x.msb <;> rcases y.msb <;> simp
/-! ### srem -/
theorem srem_eq (x y : BitVec w) : srem x y =
match x.msb, y.msb with
| false, false => x % y
| false, true => x % (-y)
| true, false => - ((-x) % y)
| true, true => -((-x) % (-y)) := by
rw [BitVec.srem]
rcases x.msb <;> rcases y.msb <;> simp
/-! ### smod -/
/-- Equation theorem for `smod` in terms of `umod`. -/
@@ -2726,21 +2670,6 @@ theorem getElem_twoPow {i j : Nat} (h : j < w) : (twoPow w i)[j] = decide (j = i
simp [eq_comm]
omega
@[simp]
theorem getMsbD_twoPow {i j w: Nat} :
(twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1)) := by
simp only [getMsbD_eq_getLsbD, getLsbD_twoPow]
by_cases h₀ : i < w <;> by_cases h₁ : j < w <;>
simp [h₀, h₁] <;> omega
@[simp]
theorem msb_twoPow {i w: Nat} :
(twoPow w i).msb = (decide (i < w) && decide (i = w - 1)) := by
simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.sub_zero, getLsbD_twoPow,
Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp]
intros
omega
theorem and_twoPow (x : BitVec w) (i : Nat) :
x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by
ext j
@@ -2886,14 +2815,6 @@ theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) :=
simp only [intMin, getLsbD_twoPow, boolToPropSimps]
omega
theorem getMsbD_intMin {w i : Nat} :
(intMin w).getMsbD i = (decide (0 < w) && decide (i = 0)) := by
simp only [getMsbD, getLsbD_intMin]
match w, i with
| 0, _ => simp
| w+1, 0 => simp
| w+1, i+1 => simp; omega
/--
The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
-/
@@ -2916,21 +2837,6 @@ theorem toInt_intMin {w : Nat} :
rw [Nat.mul_comm]
simp [w_pos]
theorem toInt_intMin_le (x : BitVec w) :
(intMin w).toInt x.toInt := by
cases w
case zero => simp [@of_length_zero x]
case succ w =>
simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
have : 0 < 2 ^ w := Nat.two_pow_pos w
rw [Int.emod_eq_of_lt (by omega) (by omega)]
rw [BitVec.toInt_eq_toNat_bmod]
rw [show (2 ^ w : Nat) = ((2 ^ (w + 1) : Nat) : Int) / 2 by omega]
apply Int.le_bmod (by omega)
theorem intMin_sle (x : BitVec w) : (intMin w).sle x := by
simp only [BitVec.sle, toInt_intMin_le x, decide_True]
@[simp]
theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
by_cases h : 0 < w
@@ -2938,10 +2844,6 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
· simp only [Nat.not_lt, Nat.le_zero_eq] at h
simp [bv_toNat, h]
@[simp]
theorem abs_intMin {w : Nat} : (intMin w).abs = intMin w := by
simp [BitVec.abs, bv_toNat]
theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x intMin w) :
(-x).toInt = -(x.toInt) := by
simp only [ne_eq, toNat_eq, toNat_intMin] at rs
@@ -2958,10 +2860,6 @@ theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
have := @Nat.two_pow_pred_mul_two w (by omega)
split <;> split <;> omega
theorem msb_intMin {w : Nat} : (intMin w).msb = decide (0 < w) := by
simp only [msb_eq_decide, toNat_intMin, decide_eq_decide]
by_cases h : 0 < w <;> simp_all
/-! ### intMax -/
/-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
@@ -3054,38 +2952,6 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
omega
/-! ### neg -/
theorem msb_eq_toInt {x : BitVec w}:
x.msb = decide (x.toInt < 0) := by
by_cases h : x.msb <;>
· simp [h, toInt_eq_msb_cond]
omega
theorem msb_eq_toNat {x : BitVec w}:
x.msb = decide (x.toNat 2 ^ (w - 1)) := by
simp only [msb_eq_decide, ge_iff_le]
/-! ### abs -/
theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
@[simp, bv_toNat]
theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
simp only [BitVec.abs, neg_eq]
by_cases h : x.msb = true
· simp only [h, reduceIte, toNat_neg]
have : 2 * x.toNat 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
rw [Nat.mod_eq_of_lt (by omega)]
· simp [h]
theorem getLsbD_abs {i : Nat} {x : BitVec w} :
getLsbD x.abs i = if x.msb then getLsbD (-x) i else getLsbD x i := by
by_cases h : x.msb <;> simp [BitVec.abs, h]
theorem getMsbD_abs {i : Nat} {x : BitVec w} :
getMsbD (x.abs) i = if x.msb then getMsbD (-x) i else getMsbD x i := by
by_cases h : x.msb <;> simp [BitVec.abs, h]
/-! ### Decidable quantifiers -/
@@ -3294,10 +3160,4 @@ abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLs
@[deprecated msb_sshiftRight (since := "2024-10-03")]
abbrev sshiftRight_msb_eq_msb := @msb_sshiftRight
@[deprecated shiftLeft_zero (since := "2024-10-27")]
abbrev shiftLeft_zero_eq := @shiftLeft_zero
@[deprecated ushiftRight_zero (since := "2024-10-27")]
abbrev ushiftRight_zero_eq := @ushiftRight_zero
end BitVec

View File

@@ -65,7 +65,7 @@ def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
@[extern "lean_byte_array_fset"]
def set : (a : ByteArray) (@& Fin a.size) UInt8 ByteArray
| bs, i, b => bs.set i.1 b i.2
| bs, i, b => bs.set i b
@[extern "lean_byte_array_uset"]
def uset : (a : ByteArray) (i : USize) UInt8 i.toNat < a.size ByteArray

View File

@@ -5,8 +5,6 @@ Authors: François G. Dorais
-/
prelude
import Init.Data.Nat.Linear
import Init.Control.Lawful.Basic
import Init.Data.Fin.Lemmas
namespace Fin
@@ -25,195 +23,4 @@ namespace Fin
| 0, _, x => x
| i+1, h, x => loop i, Nat.le_of_lt h (f i, h x)
/--
Folds a monadic function over `Fin n` from left to right:
```
Fin.foldlM n f x₀ = do
let x₁ ← f x₀ 0
let x₂ ← f x₁ 1
...
let xₙ ← f xₙ₋₁ (n-1)
pure xₙ
```
-/
@[inline] def foldlM [Monad m] (n) (f : α Fin n m α) (init : α) : m α := loop init 0 where
/--
Inner loop for `Fin.foldlM`.
```
Fin.foldlM.loop n f xᵢ i = do
let xᵢ₊₁ ← f xᵢ i
...
let xₙ ← f xₙ₋₁ (n-1)
pure xₙ
```
-/
loop (x : α) (i : Nat) : m α := do
if h : i < n then f x i, h >>= (loop · (i+1)) else pure x
termination_by n - i
decreasing_by decreasing_trivial_pre_omega
/--
Folds a monadic function over `Fin n` from right to left:
```
Fin.foldrM n f xₙ = do
let xₙ₋₁ ← f (n-1) xₙ
let xₙ₋₂ ← f (n-2) xₙ₋₁
...
let x₀ ← f 0 x₁
pure x₀
```
-/
@[inline] def foldrM [Monad m] (n) (f : Fin n α m α) (init : α) : m α :=
loop n, Nat.le_refl n init where
/--
Inner loop for `Fin.foldrM`.
```
Fin.foldrM.loop n f i xᵢ = do
let xᵢ₋₁ ← f (i-1) xᵢ
...
let x₁ ← f 1 x₂
let x₀ ← f 0 x₁
pure x₀
```
-/
loop : {i // i n} α m α
| 0, _, x => pure x
| i+1, h, x => f i, h x >>= loop i, Nat.le_of_lt h
/-! ### foldlM -/
theorem foldlM_loop_lt [Monad m] (f : α Fin n m α) (x) (h : i < n) :
foldlM.loop n f x i = f x i, h >>= (foldlM.loop n f . (i+1)) := by
rw [foldlM.loop, dif_pos h]
theorem foldlM_loop_eq [Monad m] (f : α Fin n m α) (x) : foldlM.loop n f x n = pure x := by
rw [foldlM.loop, dif_neg (Nat.lt_irrefl _)]
theorem foldlM_loop [Monad m] (f : α Fin (n+1) m α) (x) (h : i < n+1) :
foldlM.loop (n+1) f x i = f x i, h >>= (foldlM.loop n (fun x j => f x j.succ) . i) := by
if h' : i < n then
rw [foldlM_loop_lt _ _ h]
congr; funext
rw [foldlM_loop_lt _ _ h', foldlM_loop]; rfl
else
cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
rw [foldlM_loop_lt]
congr; funext
rw [foldlM_loop_eq, foldlM_loop_eq]
termination_by n - i
@[simp] theorem foldlM_zero [Monad m] (f : α Fin 0 m α) (x) : foldlM 0 f x = pure x :=
foldlM_loop_eq ..
theorem foldlM_succ [Monad m] (f : α Fin (n+1) m α) (x) :
foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop ..
/-! ### foldrM -/
theorem foldrM_loop_zero [Monad m] (f : Fin n α m α) (x) :
foldrM.loop n f 0, Nat.zero_le _ x = pure x := by
rw [foldrM.loop]
theorem foldrM_loop_succ [Monad m] (f : Fin n α m α) (x) (h : i < n) :
foldrM.loop n f i+1, h x = f i, h x >>= foldrM.loop n f i, Nat.le_of_lt h := by
rw [foldrM.loop]
theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) α m α) (x) (h : i+1 n+1) :
foldrM.loop (n+1) f i+1, h x =
foldrM.loop n (fun j => f j.succ) i, Nat.le_of_succ_le_succ h x >>= f 0 := by
induction i generalizing x with
| zero =>
rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
conv => rhs; rw [bind_pure (f 0 x)]
congr; funext; exact foldrM_loop_zero ..
| succ i ih =>
rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
congr; funext; exact ih ..
@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 α m α) (x) : foldrM 0 f x = pure x :=
foldrM_loop_zero ..
theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) α m α) (x) :
foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..
/-! ### foldl -/
theorem foldl_loop_lt (f : α Fin n α) (x) (h : i < n) :
foldl.loop n f x i = foldl.loop n f (f x i, h) (i+1) := by
rw [foldl.loop, dif_pos h]
theorem foldl_loop_eq (f : α Fin n α) (x) : foldl.loop n f x n = x := by
rw [foldl.loop, dif_neg (Nat.lt_irrefl _)]
theorem foldl_loop (f : α Fin (n+1) α) (x) (h : i < n+1) :
foldl.loop (n+1) f x i = foldl.loop n (fun x j => f x j.succ) (f x i, h) i := by
if h' : i < n then
rw [foldl_loop_lt _ _ h]
rw [foldl_loop_lt _ _ h', foldl_loop]; rfl
else
cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
rw [foldl_loop_lt]
rw [foldl_loop_eq, foldl_loop_eq]
@[simp] theorem foldl_zero (f : α Fin 0 α) (x) : foldl 0 f x = x :=
foldl_loop_eq ..
theorem foldl_succ (f : α Fin (n+1) α) (x) :
foldl (n+1) f x = foldl n (fun x i => f x i.succ) (f x 0) :=
foldl_loop ..
theorem foldl_succ_last (f : α Fin (n+1) α) (x) :
foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by
rw [foldl_succ]
induction n generalizing x with
| zero => simp [foldl_succ, Fin.last]
| succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
theorem foldl_eq_foldlM (f : α Fin n α) (x) :
foldl n f x = foldlM (m:=Id) n f x := by
induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
/-! ### foldr -/
theorem foldr_loop_zero (f : Fin n α α) (x) :
foldr.loop n f 0, Nat.zero_le _ x = x := by
rw [foldr.loop]
theorem foldr_loop_succ (f : Fin n α α) (x) (h : i < n) :
foldr.loop n f i+1, h x = foldr.loop n f i, Nat.le_of_lt h (f i, h x) := by
rw [foldr.loop]
theorem foldr_loop (f : Fin (n+1) α α) (x) (h : i+1 n+1) :
foldr.loop (n+1) f i+1, h x =
f 0 (foldr.loop n (fun j => f j.succ) i, Nat.le_of_succ_le_succ h x) := by
induction i generalizing x <;> simp [foldr_loop_zero, foldr_loop_succ, *]
@[simp] theorem foldr_zero (f : Fin 0 α α) (x) : foldr 0 f x = x :=
foldr_loop_zero ..
theorem foldr_succ (f : Fin (n+1) α α) (x) :
foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop ..
theorem foldr_succ_last (f : Fin (n+1) α α) (x) :
foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
induction n generalizing x with
| zero => simp [foldr_succ, Fin.last]
| succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
theorem foldr_eq_foldrM (f : Fin n α α) (x) :
foldr n f x = foldrM (m:=Id) n f x := by
induction n <;> simp [foldr_succ, foldrM_succ, *]
theorem foldl_rev (f : Fin n α α) (x) :
foldl n (fun x i => f i.rev x) x = foldr n f x := by
induction n generalizing x with
| zero => simp
| succ n ih => rw [foldl_succ, foldr_succ_last, ih]; simp [rev_succ]
theorem foldr_rev (f : α Fin n α) (x) :
foldr n (fun i x => f x i.rev) x = foldl n f x := by
induction n generalizing x with
| zero => simp
| succ n ih => rw [foldl_succ_last, foldr_succ, ih]; simp [rev_succ]
end Fin

View File

@@ -71,7 +71,7 @@ def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → F
@[extern "lean_float_array_fset"]
def set : (ds : FloatArray) (@& Fin ds.size) Float FloatArray
| ds, i, d => ds.set i.1 d i.2
| ds, i, d => ds.set i d
@[extern "lean_float_array_set"]
def set! : FloatArray (@& Nat) Float FloatArray

View File

@@ -48,9 +48,6 @@ instance : Hashable UInt64 where
instance : Hashable USize where
hash n := n.toUInt64
instance : Hashable ByteArray where
hash as := as.foldl (fun r a => mixHash r (hash a)) 7
instance : Hashable (Fin n) where
hash v := v.val.toUInt64

View File

@@ -1125,17 +1125,6 @@ theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n + y) n = Int.bmo
simp [Int.emod_def, Int.sub_eq_add_neg]
rw [Int.mul_neg, Int.add_right_comm, Int.bmod_add_mul_cancel]
@[simp]
theorem emod_sub_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n - y) n = Int.bmod (x - y) n := by
simp only [emod_def, Int.sub_eq_add_neg]
rw [Int.mul_neg, Int.add_right_comm, Int.bmod_add_mul_cancel]
@[simp]
theorem sub_emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x - y%n) n = Int.bmod (x - y) n := by
simp only [emod_def]
rw [Int.sub_eq_add_neg, Int.neg_sub, Int.sub_eq_add_neg, Int.add_assoc, Int.add_right_comm,
Int.bmod_add_mul_cancel, Int.sub_eq_add_neg]
@[simp]
theorem emod_mul_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n * y) n = Int.bmod (x * y) n := by
simp [Int.emod_def, Int.sub_eq_add_neg]
@@ -1151,28 +1140,9 @@ theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n
rw [Int.sub_eq_add_neg, Int.add_right_comm, Int.sub_eq_add_neg]
simp
@[simp]
theorem bmod_sub_bmod_congr : Int.bmod (Int.bmod x n - y) n = Int.bmod (x - y) n := by
rw [Int.bmod_def x n]
split
next p =>
simp only [emod_sub_bmod_congr]
next p =>
rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_right_comm, Int.sub_eq_add_neg, Int.sub_eq_add_neg]
simp [emod_sub_bmod_congr]
@[simp] theorem add_bmod_bmod : Int.bmod (x + Int.bmod y n) n = Int.bmod (x + y) n := by
rw [Int.add_comm x, Int.bmod_add_bmod_congr, Int.add_comm y]
@[simp] theorem sub_bmod_bmod : Int.bmod (x - Int.bmod y n) n = Int.bmod (x - y) n := by
rw [Int.bmod_def y n]
split
next p =>
simp [sub_emod_bmod_congr]
next p =>
rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, Int.add_assoc, Int.sub_eq_add_neg]
simp [sub_emod_bmod_congr]
@[simp]
theorem bmod_mul_bmod : Int.bmod (Int.bmod x n * y) n = Int.bmod (x * y) n := by
rw [bmod_def x n]
@@ -1267,7 +1237,7 @@ theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2 := by
_ = ((m + 1 - 2) + 2)/2 := by simp
_ = (m - 1) / 2 + 1 := by
rw [add_ediv_of_dvd_right]
· simp +decide only [Int.ediv_self]
· simp (config := {decide := true}) only [Int.ediv_self]
congr 2
rw [Int.add_sub_assoc, Int.sub_neg]
congr
@@ -1285,7 +1255,7 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
simp only [bmod, ofNat_eq_coe, natAbs_ofNat, natCast_add, ofNat_one,
emod_self_add_one (ofNat_nonneg x)]
match x with
| 0 => rw [if_pos] <;> simp +decide
| 0 => rw [if_pos] <;> simp (config := {decide := true})
| (x+1) =>
rw [if_neg]
· simp [ Int.sub_sub]

View File

@@ -1007,9 +1007,9 @@ theorem sign_eq_neg_one_iff_neg {a : Int} : sign a = -1 ↔ a < 0 :=
match x with
| 0 => rfl
| .ofNat (_ + 1) =>
simp +decide only [sign, true_iff]
simp (config := { decide := true }) only [sign, true_iff]
exact Int.le_add_one (ofNat_nonneg _)
| .negSucc _ => simp +decide [sign]
| .negSucc _ => simp (config := { decide := true }) [sign]
theorem mul_sign : i : Int, i * sign i = natAbs i
| succ _ => Int.mul_one _

View File

@@ -25,4 +25,3 @@ import Init.Data.List.Perm
import Init.Data.List.Sort
import Init.Data.List.ToArray
import Init.Data.List.MapIdx
import Init.Data.List.OfFn

View File

@@ -29,7 +29,7 @@ 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`, `flatMap`, `replicate`, and
`map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `bind`, `replicate`, and
`reverse`.
* Additional functions defined in terms of these: `leftpad`, `rightPad`, and `reduceOption`.
* Operations using indexes: `mapIdx`.
@@ -38,14 +38,14 @@ The operations are organized as follow:
* Sublists: `take`, `drop`, `takeWhile`, `dropWhile`, `partition`, `dropLast`,
`isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `Subset`, `Sublist`,
`rotateLeft` and `rotateRight`.
* Manipulating elements: `replace`, `insert`, `modify`, `erase`, `eraseP`, `eraseIdx`.
* Manipulating elements: `replace`, `insert`, `erase`, `eraseP`, `eraseIdx`.
* Finding elements: `find?`, `findSome?`, `findIdx`, `indexOf`, `findIdx?`, `indexOf?`,
`countP`, `count`, and `lookup`.
* Logic: `any`, `all`, `or`, and `and`.
* Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
* Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
* Minima and maxima: `min?` and `max?`.
* Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `splitBy`,
* Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `groupBy`,
`removeAll`
(currently these functions are mostly only used in meta code,
and do not have API suitable for verification).
@@ -122,11 +122,6 @@ protected def beq [BEq α] : List α → List α → Bool
| a::as, b::bs => a == b && List.beq as bs
| _, _ => false
@[simp] theorem beq_nil_nil [BEq α] : List.beq ([] : List α) ([] : List α) = true := rfl
@[simp] theorem beq_cons_nil [BEq α] (a : α) (as : List α) : List.beq (a::as) [] = false := rfl
@[simp] theorem beq_nil_cons [BEq α] (a : α) (as : List α) : List.beq [] (a::as) = false := rfl
theorem beq_cons₂ [BEq α] (a b : α) (as bs : List α) : List.beq (a::as) (b::bs) = (a == b && List.beq as bs) := rfl
instance [BEq α] : BEq (List α) := List.beq
instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
@@ -1119,35 +1114,6 @@ theorem replace_cons [BEq α] {a : α} :
@[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
if l.elem a then l else a :: l
/-! ### modify -/
/--
Apply a function to the nth tail of `l`. Returns the input without
using `f` if the index is larger than the length of the List.
```
modifyTailIdx f 2 [a, b, c] = [a, b] ++ f [c]
```
-/
@[simp] def modifyTailIdx (f : List α List α) : Nat List α List α
| 0, l => f l
| _+1, [] => []
| n+1, a :: l => a :: modifyTailIdx f n l
/-- Apply `f` to the head of the list, if it exists. -/
@[inline] def modifyHead (f : α α) : List α List α
| [] => []
| a :: l => f a :: l
@[simp] theorem modifyHead_nil (f : α α) : [].modifyHead f = [] := by rw [modifyHead]
@[simp] theorem modifyHead_cons (a : α) (l : List α) (f : α α) :
(a :: l).modifyHead f = f a :: l := by rw [modifyHead]
/--
Apply `f` to the nth element of the list, if it exists, replacing that element with the result.
-/
def modify (f : α α) : Nat List α List α :=
modifyTailIdx (modifyHead f)
/-! ### erase -/
/--
@@ -1452,15 +1418,11 @@ def sum {α} [Add α] [Zero α] : List αα :=
@[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
/-- Sum of a list of natural numbers. -/
@[deprecated List.sum (since := "2024-10-17")]
-- We intend to subsequently deprecate this in favor of `List.sum`.
protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
set_option linter.deprecated false in
@[simp, deprecated sum_nil (since := "2024-10-17")]
theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
set_option linter.deprecated false in
@[simp, deprecated sum_cons (since := "2024-10-17")]
theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
@[simp] theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
@[simp] theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
Nat.sum (a::l) = a + Nat.sum l := rfl
/-! ### range -/
@@ -1639,23 +1601,23 @@ where
| true => loop as (a::rs)
| false => (rs.reverse, a::as)
/-! ### splitBy -/
/-! ### groupBy -/
/--
`O(|l|)`. `splitBy R l` splits `l` into chains of elements
`O(|l|)`. `groupBy R l` splits `l` into chains of elements
such that adjacent elements are related by `R`.
* `splitBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
* `splitBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
* `groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
* `groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
-/
@[specialize] def splitBy (R : α α Bool) : List α List (List α)
@[specialize] def groupBy (R : α α Bool) : List α List (List α)
| [] => []
| a::as => loop as a [] []
where
/--
The arguments of `splitBy.loop l ag g gs` represent the following:
The arguments of `groupBy.loop l ag g gs` represent the following:
- `l : List α` are the elements which we still need to split.
- `l : List α` are the elements which we still need to group.
- `ag : α` is the previous element for which a comparison was performed.
- `g : List α` is the group currently being assembled, in **reverse order**.
- `gs : List (List α)` is all of the groups that have been completed, in **reverse order**.
@@ -1666,8 +1628,6 @@ where
| false => loop as a [] ((ag::g).reverse::gs)
| [], ag, g, gs => ((ag::g).reverse::gs).reverse
@[deprecated splitBy (since := "2024-10-30"), inherit_doc splitBy] abbrev groupBy := @splitBy
/-! ### removeAll -/
/-- `O(|xs|)`. Computes the "set difference" of lists,

View File

@@ -215,6 +215,27 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
| some b => pure (some b)
| none => findSomeM? f as
@[inline] protected def forIn {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : List α) (init : β) (f : α β m (ForInStep β)) : m β :=
let rec @[specialize] loop
| [], b => pure b
| a::as, b => do
match ( f a b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop as b
loop as init
instance : ForIn m (List α) α where
forIn := List.forIn
@[simp] theorem forIn_eq_forIn [Monad m] : @List.forIn α β m _ = forIn := rfl
@[simp] theorem forIn_nil [Monad m] (f : α β m (ForInStep β)) (b : β) : forIn [] b f = pure b :=
rfl
@[simp] theorem forIn_cons [Monad m] (f : α β m (ForInStep β)) (a : α) (as : List α) (b : β)
: forIn (a::as) b f = f a b >>= fun | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f :=
rfl
@[inline] protected def forIn' {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : List α) (init : β) (f : (a : α) a as β m (ForInStep β)) : m β :=
let rec @[specialize] loop : (as' : List α) (b : β) Exists (fun bs => bs ++ as' = as) m β
| [], b, _ => pure b
@@ -233,15 +254,14 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
instance : ForIn' m (List α) α inferInstance where
forIn' := List.forIn'
-- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@[simp] theorem forIn'_eq_forIn' [Monad m] : @List.forIn' α β m _ = forIn' := rfl
@[simp] theorem forIn'_nil [Monad m] (f : (a : α) a [] β m (ForInStep β)) (b : β) : forIn' [] b f = pure b :=
rfl
@[simp] theorem forIn_nil [Monad m] (f : α β m (ForInStep β)) (b : β) : forIn [] b f = pure b :=
rfl
@[simp] theorem forIn'_eq_forIn {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : List α) (init : β) (f : α β m (ForInStep β)) : forIn' as init (fun a _ b => f a b) = forIn as init f := by
simp [forIn', forIn, List.forIn, List.forIn']
have : cs h, List.forIn'.loop cs (fun a _ b => f a b) as init h = List.forIn.loop f as init := by
intro cs h
induction as generalizing cs init with
| nil => intros; rfl
| cons a as ih => intros; simp [List.forIn.loop, List.forIn'.loop, ih]
apply this
instance : ForM m (List α) α where
forM := List.forM

View File

@@ -153,7 +153,7 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
simp only [length_filterMap_eq_countP]
congr
ext a
simp +contextual [Option.getD_eq_iff, Option.isSome_eq_isSome]
simp (config := { contextual := true }) [Option.getD_eq_iff, Option.isSome_eq_isSome]
@[simp] theorem countP_flatten (l : List (List α)) :
countP p l.flatten = (l.map (countP p)).sum := by
@@ -315,7 +315,7 @@ theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = len
theorem count_le_count_map [DecidableEq β] (l : List α) (f : α β) (x : α) :
count x l count (f x) (map f l) := by
rw [count, count, countP_map]
apply countP_mono_left; simp +contextual
apply countP_mono_left; simp (config := { contextual := true })
theorem count_filterMap {α} [BEq β] (b : β) (f : α Option β) (l : List α) :
count b (filterMap f l) = countP (fun a => f a == some b) l := by

View File

@@ -179,7 +179,7 @@ theorem IsPrefix.findSome?_eq_some {l₁ l₂ : List α} {f : α → Option β}
List.findSome? f l₁ = some b List.findSome? f l₂ = some b := by
rw [IsPrefix] at h
obtain t, rfl := h
simp +contextual [findSome?_append]
simp (config := {contextual := true}) [findSome?_append]
theorem IsPrefix.findSome?_eq_none {l₁ l₂ : List α} {f : α Option β} (h : l₁ <+: l₂) :
List.findSome? f l₂ = none List.findSome? f l₁ = none :=
@@ -436,7 +436,7 @@ theorem IsPrefix.find?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁
List.find? p l₁ = some b List.find? p l₂ = some b := by
rw [IsPrefix] at h
obtain t, rfl := h
simp +contextual [find?_append]
simp (config := {contextual := true}) [find?_append]
theorem IsPrefix.find?_eq_none {l₁ l₂ : List α} {p : α Bool} (h : l₁ <+: l₂) :
List.find? p l₂ = none List.find? p l₁ = none :=
@@ -562,7 +562,7 @@ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs
| inr e =>
have ipm := Nat.succ_pred_eq_of_pos e
have ilt := Nat.le_trans ho (findIdx_le_length p)
simp +singlePass only [ ipm, getElem_cons_succ]
simp (config := { singlePass := true }) only [ ipm, getElem_cons_succ]
rw [ ipm, Nat.succ_lt_succ_iff] at h
simpa using ih h
@@ -595,14 +595,15 @@ theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length
theorem findIdx_append (p : α Bool) (l₁ l₂ : List α) :
(l₁ ++ l₂).findIdx p =
if l₁.findIdx p < l₁.length then l₁.findIdx p else l₂.findIdx p + l₁.length := by
if x, x l₁ p x = true then l₁.findIdx p else l₂.findIdx p + l₁.length := by
induction l₁ with
| nil => simp
| cons x xs ih =>
simp only [findIdx_cons, length_cons, cons_append]
by_cases h : p x
· simp [h]
· simp only [h, ih, cond_eq_if, Bool.false_eq_true, reduceIte, add_one_lt_add_one_iff]
· simp only [h, ih, cond_eq_if, Bool.false_eq_true, reduceIte, mem_cons, exists_eq_or_imp,
false_or]
split <;> simp [Nat.add_assoc]
theorem IsPrefix.findIdx_le {l₁ l₂ : List α} {p : α Bool} (h : l₁ <+: l₂) :

View File

@@ -23,7 +23,7 @@ namespace List
The following operations are already tail-recursive, and do not need `@[csimp]` replacements:
`get`, `foldl`, `beq`, `isEqv`, `reverse`, `elem` (and hence `contains`), `drop`, `dropWhile`,
`partition`, `isPrefixOf`, `isPrefixOf?`, `find?`, `findSome?`, `lookup`, `any` (and hence `or`),
`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `splitBy`.
`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `groupBy`.
The following operations are still missing `@[csimp]` replacements:
`concat`, `zipWithAll`.
@@ -38,7 +38,7 @@ The following operations were already given `@[csimp]` replacements in `Init/Dat
The following operations are given `@[csimp]` replacements below:
`set`, `filterMap`, `foldr`, `append`, `bind`, `join`,
`take`, `takeWhile`, `dropLast`, `replace`, `modify`, `erase`, `eraseIdx`, `zipWith`,
`take`, `takeWhile`, `dropLast`, `replace`, `erase`, `eraseIdx`, `zipWith`,
`enumFrom`, and `intercalate`.
-/
@@ -197,24 +197,6 @@ The following operations are given `@[csimp]` replacements below:
· simp [*]
· intro h; rw [IH] <;> simp_all
/-! ### modify -/
/-- Tail-recursive version of `modify`. -/
def modifyTR (f : α α) (n : Nat) (l : List α) : List α := go l n #[] where
/-- Auxiliary for `modifyTR`: `modifyTR.go f l n acc = acc.toList ++ modify f n l`. -/
go : List α Nat Array α List α
| [], _, acc => acc.toList
| a :: l, 0, acc => acc.toListAppend (f a :: l)
| a :: l, n+1, acc => go l n (acc.push a)
theorem modifyTR_go_eq : l n, modifyTR.go f l n acc = acc.toList ++ modify f n l
| [], n => by cases n <;> simp [modifyTR.go, modify]
| a :: l, 0 => by simp [modifyTR.go, modify]
| a :: l, n+1 => by simp [modifyTR.go, modify, modifyTR_go_eq l]
@[csimp] theorem modify_eq_modifyTR : @modify = @modifyTR := by
funext α f n l; simp [modifyTR, modifyTR_go_eq]
/-! ### erase -/
/-- Tail recursive version of `List.erase`. -/

View File

@@ -492,6 +492,10 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
theorem get?_of_mem {a} {l : List α} (h : a l) : n, l.get? n = some a :=
let n, _, e := get_of_mem h; n, e get?_eq_get _
@[simp] theorem getElem_mem : {l : List α} {n} (h : n < l.length), l[n]'h l
| _ :: _, 0, _ => .head ..
| _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
theorem get_mem : (l : List α) n h, get l n, h l
| _ :: _, 0, _ => .head ..
| _ :: l, _+1, _ => .tail _ (get_mem l ..)
@@ -1043,6 +1047,9 @@ theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
@[simp] theorem getLast?_singleton (a : α) : getLast? [a] = a := rfl
theorem getLast!_of_getLast? [Inhabited α] : {l : List α}, getLast? l = some a getLast! l = a
| _ :: _, rfl => rfl
theorem getLast?_eq_getLast : l h, @getLast? α l = some (getLast l h)
| [], h => nomatch h rfl
| _ :: _, _ => rfl
@@ -1076,21 +1083,6 @@ theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
rw [getLastD_eq_getLast?, getLast?_concat]; rfl
/-! ### getLast! -/
@[simp] theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
theorem getLast!_of_getLast? [Inhabited α] : {l : List α}, getLast? l = some a getLast! l = a
| _ :: _, rfl => rfl
theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]! := by
cases l with
| nil => simp
| cons _ _ =>
apply getLast!_of_getLast?
rw [getElem!_pos, getElem_cons_length (h := by simp)]
rfl
/-! ## Head and tail -/
/-! ### head -/
@@ -3328,7 +3320,7 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
@[simp] theorem all_replicate {n : Nat} {a : α} :
(replicate n a).all f = if n = 0 then true else f a := by
cases n <;> simp +contextual [replicate_succ]
cases n <;> simp (config := {contextual := true}) [replicate_succ]
@[simp] theorem any_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
(l.insert a).any f = (f a || l.any f) := by

View File

@@ -7,9 +7,6 @@ Authors: Kim Morrison, Mario Carneiro
prelude
import Init.Data.Array.Lemmas
import Init.Data.List.Nat.Range
import Init.Data.List.OfFn
import Init.Data.Fin.Lemmas
import Init.Data.Option.Attach
namespace List
@@ -17,21 +14,8 @@ namespace List
/-! ### mapIdx -/
/--
Given a list `as = [a₀, a₁, ...]` function `f : Fin as.length → α → β`, returns the list
`[f 0 a₀, f 1 a₁, ...]`.
-/
@[inline] def mapFinIdx (as : List α) (f : Fin as.length α β) : List β := go as #[] (by simp) where
/-- Auxiliary for `mapFinIdx`:
`mapFinIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀, f 1 a₁, ...]` -/
@[specialize] go : (bs : List α) (acc : Array β) bs.length + acc.size = as.length List β
| [], acc, h => acc.toList
| a :: as, acc, h =>
go as (acc.push (f acc.size, by simp at h; omega a)) (by simp at h ; omega)
/--
Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁, ...]`, returns the list
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
@@ -41,177 +25,34 @@ Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁,
| [], acc => acc.toList
| a :: as, acc => go as (acc.push (f acc.size a))
/-! ### mapFinIdx -/
@[simp]
theorem mapFinIdx_nil {f : Fin 0 α β} : mapFinIdx [] f = [] :=
rfl
@[simp] theorem length_mapFinIdx_go :
(mapFinIdx.go as f bs acc h).length = as.length := by
induction bs generalizing acc with
| nil => simpa using h
| cons _ _ ih => simp [mapFinIdx.go, ih]
@[simp] theorem length_mapFinIdx {as : List α} {f : Fin as.length α β} :
(as.mapFinIdx f).length = as.length := by
simp [mapFinIdx, length_mapFinIdx_go]
theorem getElem_mapFinIdx_go {as : List α} {f : Fin as.length α β} {i : Nat} {h} {w} :
(mapFinIdx.go as f bs acc h)[i] =
if w' : i < acc.size then acc[i] else f i, by simp at w; omega (bs[i - acc.size]'(by simp at w; omega)) := by
induction bs generalizing acc with
| nil =>
simp only [length_mapFinIdx_go, length_nil, Nat.zero_add] at w h
simp only [mapFinIdx.go, Array.getElem_toList]
rw [dif_pos]
| cons _ _ ih =>
simp [mapFinIdx.go]
rw [ih]
simp
split <;> rename_i h₁ <;> split <;> rename_i h₂
· rw [Array.getElem_push_lt]
· have h₃ : i = acc.size := by omega
subst h₃
simp
· omega
· have h₃ : i - acc.size = (i - (acc.size + 1)) + 1 := by omega
simp [h₃]
@[simp] theorem getElem_mapFinIdx {as : List α} {f : Fin as.length α β} {i : Nat} {h} :
(as.mapFinIdx f)[i] = f i, by simp at h; omega (as[i]'(by simp at h; omega)) := by
simp [mapFinIdx, getElem_mapFinIdx_go]
theorem mapFinIdx_eq_ofFn {as : List α} {f : Fin as.length α β} :
as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] := by
apply ext_getElem <;> simp
@[simp] theorem getElem?_mapFinIdx {l : List α} {f : Fin l.length α β} {i : Nat} :
(l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f i, by simp [getElem?_eq_some] at m; exact m.1 x := by
simp only [getElem?_eq, length_mapFinIdx, getElem_mapFinIdx]
split <;> simp
@[simp]
theorem mapFinIdx_cons {l : List α} {a : α} {f : Fin (l.length + 1) α β} :
mapFinIdx (a :: l) f = f 0 a :: mapFinIdx l (fun i => f i.succ) := by
apply ext_getElem
· simp
· rintro (_|i) h₁ h₂ <;> simp
theorem mapFinIdx_append {K L : List α} {f : Fin (K ++ L).length α β} :
(K ++ L).mapFinIdx f =
K.mapFinIdx (fun i => f (i.castLE (by simp))) ++ L.mapFinIdx (fun i => f ((i.natAdd K.length).cast (by simp))) := by
apply ext_getElem
· simp
· intro i h₁ h₂
rw [getElem_append]
simp only [getElem_mapFinIdx, length_mapFinIdx]
split <;> rename_i h
· rw [getElem_append_left]
congr
· simp only [Nat.not_lt] at h
rw [getElem_append_right h]
congr
simp
omega
@[simp] theorem mapFinIdx_concat {l : List α} {e : α} {f : Fin (l ++ [e]).length α β}:
(l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i => f (i.castLE (by simp))) ++ [f l.length, by simp e] := by
simp [mapFinIdx_append]
congr
theorem mapFinIdx_singleton {a : α} {f : Fin 1 α β} :
[a].mapFinIdx f = [f 0, by simp a] := by
simp
theorem mapFinIdx_eq_enum_map {l : List α} {f : Fin l.length α β} :
l.mapFinIdx f = l.enum.attach.map
fun i, x, m => f i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some] at m; exact m.1 x := by
apply ext_getElem <;> simp
@[simp]
theorem mapFinIdx_eq_nil_iff {l : List α} {f : Fin l.length α β} :
l.mapFinIdx f = [] l = [] := by
rw [mapFinIdx_eq_enum_map, map_eq_nil_iff, attach_eq_nil_iff, enum_eq_nil_iff]
theorem mapFinIdx_ne_nil_iff {l : List α} {f : Fin l.length α β} :
l.mapFinIdx f [] l [] := by
simp
theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : Fin l.length α β}
(h : b l.mapFinIdx f) : (i : Fin l.length), f i l[i] = b := by
rw [mapFinIdx_eq_enum_map] at h
replace h := exists_of_mem_map h
simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_enum_iff_getElem?] 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_mapFinIdx {b : β} {l : List α} {f : Fin l.length α β} :
b l.mapFinIdx f (i : Fin l.length), f i l[i] = b := by
constructor
· intro h
exact exists_of_mem_mapFinIdx h
· rintro i, h, rfl
rw [mem_iff_getElem]
exact i, by simp
theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : Fin l.length α β} :
l.mapFinIdx f = b :: l₂
(a : α) (l₁ : List α) (h : l = a :: l₁),
f 0, by simp [h] a = b l₁.mapFinIdx (fun i => f (i.succ.cast (by simp [h]))) = l₂ := by
cases l with
| nil => simp
| cons x l' =>
simp only [mapFinIdx_cons, cons.injEq, length_cons, Fin.zero_eta, Fin.cast_succ_eq,
exists_and_left]
constructor
· rintro rfl, rfl
refine x, rfl, l', by simp
· rintro a, rfl, h, _, rfl, rfl, h
exact rfl, h
theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : Fin l.length α β} :
l.mapFinIdx f = b :: l₂
l.head?.pbind (fun x m => (f 0, by cases l <;> simp_all x)) = some b
l.tail?.attach.map (fun t, m => t.mapFinIdx fun i => f (i.succ.cast (by cases l <;> simp_all))) = some l₂ := by
cases l <;> simp
theorem mapFinIdx_eq_iff {l : List α} {f : Fin l.length α β} :
l.mapFinIdx f = l' h : l'.length = l.length, (i : Nat) (h : i < l.length), l'[i] = f i, h l[i] := by
constructor
· rintro rfl
simp
· rintro h, w
apply ext_getElem <;> simp_all
theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : Fin l.length α β} :
l.mapFinIdx f = l.mapFinIdx g (i : Fin l.length), f i l[i] = g i l[i] := by
rw [eq_comm, mapFinIdx_eq_iff]
simp [Fin.forall_iff]
@[simp] theorem mapFinIdx_mapFinIdx {l : List α} {f : Fin l.length α β} {g : Fin _ β γ} :
(l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i => g (i.cast (by simp)) f i) := by
simp [mapFinIdx_eq_iff]
theorem mapFinIdx_eq_replicate_iff {l : List α} {f : Fin l.length α β} {b : β} :
l.mapFinIdx f = replicate l.length b (i : Fin l.length), f i l[i] = b := by
simp [eq_replicate_iff, length_mapFinIdx, mem_mapFinIdx, forall_exists_index, true_and]
@[simp] theorem mapFinIdx_reverse {l : List α} {f : Fin l.reverse.length α β} :
l.reverse.mapFinIdx f = (l.mapFinIdx (fun i => f l.length - 1 - i, by simp; omega)).reverse := by
simp [mapFinIdx_eq_iff]
intro i h
congr
omega
/-! ### mapIdx -/
@[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
@@ -219,6 +60,16 @@ theorem mapIdx_go_length {arr : Array β} :
| 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]
@@ -261,15 +112,6 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat},
rw [ getElem?_eq_getElem, getElem?_mapIdx, getElem?_eq_getElem (by simpa using h)]
simp
@[simp] theorem mapFinIdx_eq_mapIdx {l : List α} {f : Fin l.length α β} {g : Nat α β}
(h : (i : Fin l.length), f i l[i] = g i l[i]) :
l.mapFinIdx f = l.mapIdx g := by
simp_all [mapFinIdx_eq_iff]
theorem mapIdx_eq_mapFinIdx {l : List α} {f : Nat α β} :
l.mapIdx f = l.mapFinIdx (fun i => f i) := by
simp [mapFinIdx_eq_mapIdx]
theorem mapIdx_eq_enum_map {l : List α} :
l.mapIdx f = l.enum.map (Function.uncurry f) := by
ext1 i
@@ -288,16 +130,9 @@ theorem mapIdx_append {K L : List α} :
| nil => rfl
| cons _ _ ih => simp [ih (f := fun i => f (i + 1)), Nat.add_assoc]
@[simp] theorem mapIdx_concat {l : List α} {e : α} :
mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e] := by
simp [mapIdx_append]
theorem mapIdx_singleton {a : α} : mapIdx f [a] = [f 0 a] := by
simp
@[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_iff]
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
@@ -305,8 +140,13 @@ theorem mapIdx_ne_nil_iff {l : List α} :
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_mapFinIdx] at h
simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx h
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

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.List.Attach
/-!
# Lemmas about `List.mapM` and `List.forM`.
@@ -49,9 +48,6 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
@[simp] theorem mapM_cons [Monad m] [LawfulMonad m] (f : α m β) :
(a :: l).mapM f = (return ( f a) :: ( l.mapM f)) := by simp [ mapM'_eq_mapM, mapM']
@[simp] theorem mapM_id {l : List α} {f : α Id β} : l.mapM f = l.map f := by
induction l <;> simp_all
@[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α m β) {l₁ l₂ : List α} :
(l₁ ++ l₂).mapM f = (return ( l₁.mapM f) ++ ( l₂.mapM f)) := by induction l₁ <;> simp [*]
@@ -76,16 +72,6 @@ theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β)
reverse_cons, reverse_nil, nil_append, singleton_append]
simp [bind_pure_comp]
/-! ### foldlM and foldrM -/
theorem foldlM_map [Monad m] (f : β₁ β₂) (g : α β₂ m α) (l : List β₁) (init : α) :
(l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
induction l generalizing g init <;> simp [*]
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ β₂) (g : β₂ α m α) (l : List β₁)
(init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
induction l generalizing g init <;> simp [*]
/-! ### forM -/
-- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
@@ -101,129 +87,6 @@ theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂
(l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by
induction l₁ <;> simp [*]
/-! ### forIn' -/
theorem forIn'_loop_congr [Monad m] {as bs : List α}
{f : (a' : α) a' as β m (ForInStep β)}
{g : (a' : α) a' bs β m (ForInStep β)}
{b : β} (ha : ys, ys ++ xs = as) (hb : ys, ys ++ xs = bs)
(h : a m m' b, f a m b = g a m' b) : forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb := by
induction xs generalizing b with
| nil => simp [forIn'.loop]
| cons a xs ih =>
simp only [forIn'.loop] at *
congr 1
· rw [h]
· funext s
obtain b | b := s
· rfl
· simp
rw [ih]
@[simp] theorem forIn'_cons [Monad m] {a : α} {as : List α}
(f : (a' : α) a' a :: as β m (ForInStep β)) (b : β) :
forIn' (a::as) b f = f a (mem_cons_self a as) b >>=
fun | ForInStep.done b => pure b | ForInStep.yield b => forIn' as b fun a' m b => f a' (mem_cons_of_mem a m) b := by
simp only [forIn', List.forIn', forIn'.loop]
congr 1
funext s
obtain b | b := s
· rfl
· apply forIn'_loop_congr
intros
rfl
@[simp] theorem forIn_cons [Monad m] (f : α β m (ForInStep β)) (a : α) (as : List α) (b : β) :
forIn (a::as) b f = f a b >>= fun | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f := by
have := forIn'_cons (a := a) (as := as) (fun a' _ b => f a' b) b
simpa only [forIn'_eq_forIn]
@[congr] theorem forIn'_congr [Monad m] {as bs : List α} (w : as = bs)
{b b' : β} (hb : b = b')
{f : (a' : α) a' as β m (ForInStep β)}
{g : (a' : α) a' bs β m (ForInStep β)}
(h : a m b, f a (by simpa [w] using m) b = g a m b) :
forIn' as b f = forIn' bs b' g := by
induction bs generalizing as b b' with
| nil =>
subst w
simp [hb, forIn'_nil]
| cons b bs ih =>
cases as with
| nil => simp at w
| cons a as =>
simp only [cons.injEq] at w
obtain rfl, rfl := w
simp only [forIn'_cons]
congr 1
· simp [h, hb]
· funext s
obtain b | b := s
· rfl
· simp
rw [ih rfl rfl]
intro a m b
exact h a (mem_cons_of_mem _ m) b
/--
We can express a for loop over a list as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
(l : List α) (f : (a : α) a l β m (ForInStep β)) (init : β) :
forIn' l init f = ForInStep.value <$>
l.attach.foldlM (fun b a => match b with
| .yield b => f a.1 a.2 b
| .done b => pure (.done b)) (ForInStep.yield init) := by
induction l generalizing init with
| nil => simp
| cons a as ih =>
simp only [forIn'_cons, attach_cons, foldlM_cons, _root_.map_bind]
congr 1
funext x
match x with
| .done b =>
clear ih
dsimp
induction as with
| nil => simp
| cons a as ih =>
simp only [attach_cons, map_cons, map_map, Function.comp_def, foldlM_cons, pure_bind]
specialize ih (fun a m b => f a (by
simp only [mem_cons] at m
rcases m with rfl|m
· apply mem_cons_self
· exact mem_cons_of_mem _ (mem_cons_of_mem _ m)) b)
simp [ih, List.foldlM_map]
| .yield b =>
simp [ih, List.foldlM_map]
/--
We can express a for loop over a list as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
(f : α β m (ForInStep β)) (init : β) (l : List α) :
forIn l init f = ForInStep.value <$>
l.foldlM (fun b a => match b with
| .yield b => f a b
| .done b => pure (.done b)) (ForInStep.yield init) := by
induction l generalizing init with
| nil => simp
| cons a as ih =>
simp only [foldlM_cons, bind_pure_comp, forIn_cons, _root_.map_bind]
congr 1
funext x
match x with
| .done b =>
clear ih
dsimp
induction as with
| nil => simp
| cons a as ih => simp [ih]
| .yield b =>
simp [ih]
/-! ### allM -/
theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α m Bool) (as : List α) :
@@ -236,4 +99,14 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
funext b
split <;> simp_all
/-! ### foldlM and foldrM -/
theorem foldlM_map [Monad m] (f : β₁ β₂) (g : α β₂ m α) (l : List β₁) (init : α) :
(l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
induction l generalizing g init <;> simp [*]
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ β₂) (g : β₂ α m α) (l : List β₁)
(init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
induction l generalizing g init <;> simp [*]
end List

View File

@@ -12,5 +12,3 @@ import Init.Data.List.Nat.TakeDrop
import Init.Data.List.Nat.Count
import Init.Data.List.Nat.Erase
import Init.Data.List.Nat.Find
import Init.Data.List.Nat.BEq
import Init.Data.List.Nat.Modify

View File

@@ -1,47 +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.Data.Nat.Lemmas
import Init.Data.List.Basic
namespace List
/-! ### isEqv-/
theorem isEqv_eq_decide (a b : List α) (r) :
isEqv a b r = if h : a.length = b.length then
decide ( (i : Nat) (h' : i < a.length), r (a[i]'(h h')) (b[i]'(h h'))) else false := by
induction a generalizing b with
| nil =>
cases b <;> simp
| cons a as ih =>
cases b with
| nil => simp
| cons b bs =>
simp only [isEqv, ih, length_cons, Nat.add_right_cancel_iff]
split <;> simp [Nat.forall_lt_succ_left']
/-! ### beq -/
theorem beq_eq_isEqv [BEq α] (a b : List α) : a.beq b = isEqv a b (· == ·) := by
induction a generalizing b with
| nil =>
cases b <;> simp
| cons a as ih =>
cases b with
| nil => simp
| cons b bs =>
simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff,
Nat.forall_lt_succ_left', getElem_cons_zero, getElem_cons_succ, Bool.decide_and,
Bool.decide_eq_true]
split <;> simp
theorem beq_eq_decide [BEq α] (a b : List α) :
(a == b) = if h : a.length = b.length then
decide ( (i : Nat) (h' : i < a.length), a[i] == b[i]'(h h')) else false := by
simp [BEq.beq, beq_eq_isEqv, isEqv_eq_decide]
end List

View File

@@ -1,295 +0,0 @@
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
-/
prelude
import Init.Data.List.Nat.TakeDrop
import Init.Data.List.Nat.Erase
namespace List
/-! ### modifyHead -/
@[simp] theorem length_modifyHead {f : α α} {l : List α} : (l.modifyHead f).length = l.length := by
cases l <;> simp [modifyHead]
theorem modifyHead_eq_set [Inhabited α] (f : α α) (l : List α) :
l.modifyHead f = l.set 0 (f (l[0]?.getD default)) := by cases l <;> simp [modifyHead]
@[simp] theorem modifyHead_eq_nil_iff {f : α α} {l : List α} :
l.modifyHead f = [] l = [] := by cases l <;> simp [modifyHead]
@[simp] theorem modifyHead_modifyHead {l : List α} {f g : α α} :
(l.modifyHead f).modifyHead g = l.modifyHead (g f) := by cases l <;> simp [modifyHead]
theorem getElem_modifyHead {l : List α} {f : α α} {n} (h : n < (l.modifyHead f).length) :
(l.modifyHead f)[n] = if h' : n = 0 then f (l[0]'(by simp at h; omega)) else l[n]'(by simpa using h) := by
cases l with
| nil => simp at h
| cons hd tl => cases n <;> simp
@[simp] theorem getElem_modifyHead_zero {l : List α} {f : α α} {h} :
(l.modifyHead f)[0] = f (l[0]'(by simpa using h)) := by simp [getElem_modifyHead]
@[simp] theorem getElem_modifyHead_succ {l : List α} {f : α α} {n} (h : n + 1 < (l.modifyHead f).length) :
(l.modifyHead f)[n + 1] = l[n + 1]'(by simpa using h) := by simp [getElem_modifyHead]
theorem getElem?_modifyHead {l : List α} {f : α α} {n} :
(l.modifyHead f)[n]? = if n = 0 then l[n]?.map f else l[n]? := by
cases l with
| nil => simp
| cons hd tl => cases n <;> simp
@[simp] theorem getElem?_modifyHead_zero {l : List α} {f : α α} :
(l.modifyHead f)[0]? = l[0]?.map f := by simp [getElem?_modifyHead]
@[simp] theorem getElem?_modifyHead_succ {l : List α} {f : α α} {n} :
(l.modifyHead f)[n + 1]? = l[n + 1]? := by simp [getElem?_modifyHead]
@[simp] theorem head_modifyHead (f : α α) (l : List α) (h) :
(l.modifyHead f).head h = f (l.head (by simpa using h)) := by
cases l with
| nil => simp at h
| cons hd tl => simp
@[simp] theorem head?_modifyHead {l : List α} {f : α α} :
(l.modifyHead f).head? = l.head?.map f := by cases l <;> simp
@[simp] theorem tail_modifyHead {f : α α} {l : List α} :
(l.modifyHead f).tail = l.tail := by cases l <;> simp
@[simp] theorem take_modifyHead {f : α α} {l : List α} {n} :
(l.modifyHead f).take n = (l.take n).modifyHead f := by
cases l <;> cases n <;> simp
@[simp] theorem drop_modifyHead_of_pos {f : α α} {l : List α} {n} (h : 0 < n) :
(l.modifyHead f).drop n = l.drop n := by
cases l <;> cases n <;> simp_all
@[simp] theorem eraseIdx_modifyHead_zero {f : α α} {l : List α} :
(l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by cases l <;> simp
@[simp] theorem eraseIdx_modifyHead_of_pos {f : α α} {l : List α} {n} (h : 0 < n) :
(l.modifyHead f).eraseIdx n = (l.eraseIdx n).modifyHead f := by cases l <;> cases n <;> simp_all
@[simp] theorem modifyHead_id : modifyHead (id : α α) = id := by funext l; cases l <;> simp
/-! ### modifyTailIdx -/
@[simp] theorem modifyTailIdx_id : n (l : List α), l.modifyTailIdx id n = l
| 0, _ => rfl
| _+1, [] => rfl
| n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)
theorem eraseIdx_eq_modifyTailIdx : n (l : List α), eraseIdx l n = modifyTailIdx tail n l
| 0, l => by cases l <;> rfl
| _+1, [] => rfl
| _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
@[simp] theorem length_modifyTailIdx (f : List α List α) (H : l, length (f l) = length l) :
n l, length (modifyTailIdx f n l) = length l
| 0, _ => H _
| _+1, [] => rfl
| _+1, _ :: _ => congrArg (·+1) (length_modifyTailIdx _ H _ _)
theorem modifyTailIdx_add (f : List α List α) (n) (l₁ l₂ : List α) :
modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂ := by
induction l₁ <;> simp [*, Nat.succ_add]
theorem modifyTailIdx_eq_take_drop (f : List α List α) (H : f [] = []) :
n l, modifyTailIdx f n l = take n l ++ f (drop n l)
| 0, _ => rfl
| _ + 1, [] => H.symm
| n + 1, b :: l => congrArg (cons b) (modifyTailIdx_eq_take_drop f H n l)
theorem exists_of_modifyTailIdx (f : List α List α) {n} {l : List α} (h : n l.length) :
l₁ l₂, l = l₁ ++ l₂ l₁.length = n modifyTailIdx f n l = l₁ ++ f l₂ :=
have _, _, eq, hl : l₁ l₂, l = l₁ ++ l₂ l₁.length = n :=
_, _, (take_append_drop n l).symm, length_take_of_le h
_, _, eq, hl, hl eq modifyTailIdx_add (n := 0) ..
/-! ### modify -/
@[simp] theorem modify_nil (f : α α) (n) : [].modify f n = [] := by cases n <;> rfl
@[simp] theorem modify_zero_cons (f : α α) (a : α) (l : List α) :
(a :: l).modify f 0 = f a :: l := rfl
@[simp] theorem modify_succ_cons (f : α α) (a : α) (l : List α) (n) :
(a :: l).modify f (n + 1) = a :: l.modify f n := by rfl
theorem modifyHead_eq_modify_zero (f : α α) (l : List α) :
l.modifyHead f = l.modify f 0 := by cases l <;> simp
@[simp] theorem modify_eq_nil_iff (f : α α) (n) (l : List α) :
l.modify f n = [] l = [] := by cases l <;> cases n <;> simp
theorem getElem?_modify (f : α α) :
n (l : List α) m, (modify f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
| n, l, 0 => by cases l <;> cases n <;> simp
| n, [], _+1 => by cases n <;> rfl
| 0, _ :: l, m+1 => by cases h : l[m]? <;> simp [h, modify, m.succ_ne_zero.symm]
| n+1, a :: l, m+1 => by
simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
refine (getElem?_modify f n l m).trans ?_
cases h' : l[m]? <;> by_cases h : n = m <;>
simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']
@[simp] theorem length_modify (f : α α) : n l, length (modify f n l) = length l :=
length_modifyTailIdx _ fun l => by cases l <;> rfl
@[simp] theorem getElem?_modify_eq (f : α α) (n) (l : List α) :
(modify f n l)[n]? = f <$> l[n]? := by
simp only [getElem?_modify, if_pos]
@[simp] theorem getElem?_modify_ne (f : α α) {m n} (l : List α) (h : m n) :
(modify f m l)[n]? = l[n]? := by
simp only [getElem?_modify, if_neg h, id_map']
theorem getElem_modify (f : α α) (n) (l : List α) (m) (h : m < (modify f n l).length) :
(modify f n l)[m] =
if n = m then f (l[m]'(by simp at h; omega)) else l[m]'(by simp at h; omega) := by
rw [getElem_eq_iff, getElem?_modify]
simp at h
simp [h]
@[simp] theorem getElem_modify_eq (f : α α) (n) (l : List α) (h) :
(modify f n l)[n] = f (l[n]'(by simpa using h)) := by simp [getElem_modify]
@[simp] theorem getElem_modify_ne (f : α α) {m n} (l : List α) (h : m n) (h') :
(modify f m l)[n] = l[n]'(by simpa using h') := by simp [getElem_modify, h]
theorem modify_eq_self {f : α α} {n} {l : List α} (h : l.length n) :
l.modify f n = l := by
apply ext_getElem
· simp
· intro m h₁ h₂
simp only [getElem_modify, ite_eq_right_iff]
intro h
omega
theorem modify_modify_eq (f g : α α) (n) (l : List α) :
(modify f n l).modify g n = modify (g f) n l := by
apply ext_getElem
· simp
· intro m h₁ h₂
simp only [getElem_modify, Function.comp_apply]
split <;> simp
theorem modify_modify_ne (f g : α α) {m n} (l : List α) (h : m n) :
(modify f m l).modify g n = (l.modify g n).modify f m := by
apply ext_getElem
· simp
· intro m' h₁ h₂
simp only [getElem_modify, getElem_modify_ne, h₂]
split <;> split <;> first | rfl | omega
theorem modify_eq_set [Inhabited α] (f : α α) (n) (l : List α) :
modify f n l = l.set n (f (l[n]?.getD default)) := by
apply ext_getElem
· simp
· intro m h₁ h₂
simp [getElem_modify, getElem_set, h₂]
split <;> rename_i h
· subst h
simp only [length_modify] at h₁
simp [h₁]
· rfl
theorem modify_eq_take_drop (f : α α) :
n l, modify f n l = take n l ++ modifyHead f (drop n l) :=
modifyTailIdx_eq_take_drop _ rfl
theorem modify_eq_take_cons_drop {f : α α} {n} {l : List α} (h : n < l.length) :
modify f n l = take n l ++ f l[n] :: drop (n + 1) l := by
rw [modify_eq_take_drop, drop_eq_getElem_cons h]; rfl
theorem exists_of_modify (f : α α) {n} {l : List α} (h : n < l.length) :
l₁ a l₂, l = l₁ ++ a :: l₂ l₁.length = n modify f n l = l₁ ++ f a :: l₂ :=
match exists_of_modifyTailIdx _ (Nat.le_of_lt h) with
| _, _::_, eq, hl, H => _, _, _, eq, hl, H
| _, [], eq, hl, _ => nomatch Nat.ne_of_gt h (eq append_nil _ hl)
@[simp] theorem modify_id (n) (l : List α) : l.modify id n = l := by
simp [modify]
theorem take_modify (f : α α) (n m) (l : List α) :
(modify f m l).take n = (take n l).modify f m := by
induction n generalizing l m with
| zero => simp
| succ n ih =>
cases l with
| nil => simp
| cons hd tl =>
cases m with
| zero => simp
| succ m => simp [ih]
theorem drop_modify_of_lt (f : α α) (n m) (l : List α) (h : n < m) :
(modify f n l).drop m = l.drop m := by
apply ext_getElem
· simp
· intro m' h₁ h₂
simp only [getElem_drop, getElem_modify, ite_eq_right_iff]
intro h'
omega
theorem drop_modify_of_ge (f : α α) (n m) (l : List α) (h : n m) :
(modify f n l).drop m = modify f (n - m) (drop m l) := by
apply ext_getElem
· simp
· intro m' h₁ h₂
simp [getElem_drop, getElem_modify, ite_eq_right_iff]
split <;> split <;> first | rfl | omega
theorem eraseIdx_modify_of_eq (f : α α) (n) (l : List α) :
(modify f n l).eraseIdx n = l.eraseIdx n := by
apply ext_getElem
· simp [length_eraseIdx]
· intro m h₁ h₂
simp only [getElem_eraseIdx, getElem_modify]
split <;> split <;> first | rfl | omega
theorem eraseIdx_modify_of_lt (f : α α) (i j) (l : List α) (h : j < i) :
(modify f i l).eraseIdx j = (l.eraseIdx j).modify f (i - 1) := by
apply ext_getElem
· simp [length_eraseIdx]
· intro k h₁ h₂
simp only [getElem_eraseIdx, getElem_modify]
by_cases h' : i - 1 = k
repeat' split
all_goals (first | rfl | omega)
theorem eraseIdx_modify_of_gt (f : α α) (i j) (l : List α) (h : j > i) :
(modify f i l).eraseIdx j = (l.eraseIdx j).modify f i := by
apply ext_getElem
· simp [length_eraseIdx]
· intro k h₁ h₂
simp only [getElem_eraseIdx, getElem_modify]
by_cases h' : i = k
repeat' split
all_goals (first | rfl | omega)
theorem modify_eraseIdx_of_lt (f : α α) (i j) (l : List α) (h : j < i) :
(l.eraseIdx i).modify f j = (l.modify f j).eraseIdx i := by
apply ext_getElem
· simp [length_eraseIdx]
· intro k h₁ h₂
simp only [getElem_eraseIdx, getElem_modify]
by_cases h' : j = k + 1
repeat' split
all_goals (first | rfl | omega)
theorem modify_eraseIdx_of_ge (f : α α) (i j) (l : List α) (h : j i) :
(l.eraseIdx i).modify f j = (l.modify f (j + 1)).eraseIdx i := by
apply ext_getElem
· simp [length_eraseIdx]
· intro k h₁ h₂
simp only [getElem_eraseIdx, getElem_modify]
by_cases h' : j + 1 = k + 1
repeat' split
all_goals (first | rfl | omega)
end List

View File

@@ -169,7 +169,7 @@ theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp
theorem self_mem_range_succ (n : Nat) : n range (n + 1) := by simp
theorem pairwise_lt_range (n : Nat) : Pairwise (· < ·) (range n) := by
simp +decide only [range_eq_range', pairwise_lt_range']
simp (config := {decide := true}) only [range_eq_range', pairwise_lt_range']
theorem pairwise_le_range (n : Nat) : Pairwise (· ·) (range n) :=
Pairwise.imp Nat.le_of_lt (pairwise_lt_range _)
@@ -177,10 +177,10 @@ theorem pairwise_le_range (n : Nat) : Pairwise (· ≤ ·) (range n) :=
theorem take_range (m n : Nat) : take m (range n) = range (min m n) := by
apply List.ext_getElem
· simp
· simp +contextual [getElem_take, Nat.lt_min]
· simp (config := { contextual := true }) [getElem_take, Nat.lt_min]
theorem nodup_range (n : Nat) : Nodup (range n) := by
simp +decide only [range_eq_range', nodup_range']
simp (config := {decide := true}) only [range_eq_range', nodup_range']
@[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat Bool} :
(range n).find? p = some i p i i range n j, j < i !p j := by
@@ -430,10 +430,7 @@ theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
/-! ### enum -/
@[simp]
theorem enum_eq_nil_iff {l : List α} : List.enum l = [] l = [] := enumFrom_eq_nil
@[deprecated enum_eq_nil_iff (since := "2024-11-04")]
theorem enum_eq_nil {l : List α} : List.enum l = [] l = [] := enum_eq_nil_iff
theorem enum_eq_nil {l : List α} : List.enum l = [] l = [] := enumFrom_eq_nil
@[simp] theorem enum_singleton (x : α) : enum [x] = [(0, x)] := rfl

View File

@@ -187,9 +187,6 @@ theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.dro
· apply length_take_le
· apply Nat.le_add_right
theorem take_one {l : List α} : l.take 1 = l.head?.toList := by
induction l <;> simp
theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
(l.take n).dropLast = l.take (n - 1) := by
simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, Nat.min_eq_left, take_take, sub_le]
@@ -285,14 +282,14 @@ theorem mem_drop_iff_getElem {l : List α} {a : α} :
· rintro i, hm, rfl
refine i, by simp; omega, by rw [getElem_drop]
@[simp] theorem head?_drop (l : List α) (n : Nat) :
theorem head?_drop (l : List α) (n : Nat) :
(l.drop n).head? = l[n]? := by
rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]
@[simp] theorem head_drop {l : List α} {n : Nat} (h : l.drop n []) :
theorem head_drop {l : List α} {n : Nat} (h : l.drop n []) :
(l.drop n).head h = l[n]'(by simp_all) := by
have w : n < l.length := length_lt_of_drop_ne_nil h
simp [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some]
simpa [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some] using head?_drop l n
theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length n then none else l.getLast? := by
rw [getLast?_eq_getElem?, getElem?_drop]
@@ -303,7 +300,7 @@ theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n th
congr
omega
@[simp] theorem getLast_drop {l : List α} (h : l.drop n []) :
theorem getLast_drop {l : List α} (h : l.drop n []) :
(l.drop n).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
simp only [ne_eq, drop_eq_nil_iff] at h
apply Option.some_inj.1
@@ -452,26 +449,6 @@ theorem reverse_drop {l : List α} {n : Nat} :
rw [w, take_zero, drop_of_length_le, reverse_nil]
omega
theorem take_add_one {l : List α} {n : Nat} :
l.take (n + 1) = l.take n ++ l[n]?.toList := by
simp [take_add, take_one]
theorem drop_eq_getElem?_toList_append {l : List α} {n : Nat} :
l.drop n = l[n]?.toList ++ l.drop (n + 1) := by
induction l generalizing n with
| nil => simp
| cons hd tl ih =>
cases n
· simp
· simp only [drop_succ_cons, getElem?_cons_succ]
rw [ih]
theorem drop_sub_one {l : List α} {n : Nat} (h : 0 < n) :
l.drop (n - 1) = l[n - 1]?.toList ++ l.drop n := by
rw [drop_eq_getElem?_toList_append]
congr
omega
/-! ### findIdx -/
theorem false_of_mem_take_findIdx {xs : List α} {p : α Bool} (h : x xs.take (xs.findIdx p)) :

View File

@@ -1,55 +0,0 @@
/-
Copyright (c) 2024 Lean FRO. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Kim Morrison
-/
prelude
import Init.Data.List.Basic
import Init.Data.Fin.Fold
/-!
# Theorems about `List.ofFn`
-/
namespace List
/--
`ofFn f` with `f : fin n → α` returns the list whose ith element is `f i`
```
ofFn f = [f 0, f 1, ... , f (n - 1)]
```
-/
def ofFn {n} (f : Fin n α) : List α := Fin.foldr n (f · :: ·) []
@[simp]
theorem length_ofFn (f : Fin n α) : (ofFn f).length = n := by
simp only [ofFn]
induction n with
| zero => simp
| succ n ih => simp [Fin.foldr_succ, ih]
@[simp]
protected theorem getElem_ofFn (f : Fin n α) (i : Nat) (h : i < (ofFn f).length) :
(ofFn f)[i] = f i, by simp_all := by
simp only [ofFn]
induction n generalizing i with
| zero => simp at h
| succ n ih =>
match i with
| 0 => simp [Fin.foldr_succ]
| i+1 =>
simp only [Fin.foldr_succ]
apply ih
simp_all
@[simp]
protected theorem getElem?_ofFn (f : Fin n α) (i) : (ofFn f)[i]? = if h : i < n then some (f i, h) else none :=
if h : i < (ofFn f).length
then by
rw [getElem?_eq_getElem h, List.getElem_ofFn]
· simp only [length_ofFn] at h; simp [h]
else by
rw [dif_neg] <;>
simpa using h
end List

View File

@@ -76,11 +76,11 @@ theorem pairwise_of_forall {l : List α} (H : ∀ x y, R x y) : Pairwise R l :=
theorem Pairwise.and_mem {l : List α} :
Pairwise R l Pairwise (fun x y => x l y l R x y) l :=
Pairwise.iff_of_mem <| by simp +contextual
Pairwise.iff_of_mem <| by simp (config := { contextual := true })
theorem Pairwise.imp_mem {l : List α} :
Pairwise R l Pairwise (fun x y => x l y l R x y) l :=
Pairwise.iff_of_mem <| by simp +contextual
Pairwise.iff_of_mem <| by simp (config := { contextual := true })
theorem Pairwise.forall_of_forall_of_flip (h₁ : x l, R x x) (h₂ : Pairwise R l)
(h₃ : l.Pairwise (flip R)) : x, x l y, y l R x y := by

View File

@@ -116,7 +116,7 @@ fun s => Subset.trans s <| subset_append_right _ _
theorem replicate_subset {n : Nat} {a : α} {l : List α} : replicate n a l n = 0 a l := by
induction n with
| zero => simp
| succ n ih => simp +contextual [replicate_succ, ih, cons_subset]
| succ n ih => simp (config := {contextual := true}) [replicate_succ, ih, cons_subset]
theorem subset_replicate {n : Nat} {a : α} {l : List α} (h : n 0) : l replicate n a x l, x = a := by
induction l with
@@ -835,7 +835,7 @@ theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? =
simpa using 0, by simp
| cons b l₂ =>
simp only [cons_append, cons_prefix_cons, ih]
rw (occs := .pos [2]) [ Nat.and_forall_add_one]
rw (config := {occs := .pos [2]}) [ Nat.and_forall_add_one]
simp [Nat.succ_lt_succ_iff, eq_comm]
theorem isPrefix_iff_getElem {l₁ l₂ : List α} :

View File

@@ -92,7 +92,7 @@ protected theorem div_mul_cancel {n m : Nat} (H : n m) : m / n * n = m := by
rw [Nat.mul_comm, Nat.mul_div_cancel' H]
@[simp] theorem mod_mod_of_dvd (a : Nat) (h : c b) : a % b % c = a % c := by
rw (occs := .pos [2]) [ mod_add_div a b]
rw (config := {occs := .pos [2]}) [ mod_add_div a b]
have x, h := h
subst h
rw [Nat.mul_assoc, add_mul_mod_self_left]

View File

@@ -32,77 +32,6 @@ namespace Nat
@[simp] theorem exists_add_one_eq : ( n, n + 1 = a) 0 < a :=
fun n, h => by omega, fun h => a - 1, by omega
/-- Dependent variant of `forall_lt_succ_right`. -/
theorem forall_lt_succ_right' {p : (m : Nat) (m < n + 1) Prop} :
( m (h : m < n + 1), p m h) ( m (h : m < n), p m (by omega)) p n (by omega) := by
simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
constructor
· intro w
constructor
· intro m h
exact w _ (.inl h)
· exact w _ (.inr rfl)
· rintro w m (h|rfl)
· exact w.1 _ h
· exact w.2
/-- See `forall_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
theorem forall_lt_succ_right {p : Nat Prop} :
( m, m < n + 1 p m) ( m, m < n p m) p n := by
simpa using forall_lt_succ_right' (p := fun m _ => p m)
/-- Dependent variant of `forall_lt_succ_left`. -/
theorem forall_lt_succ_left' {p : (m : Nat) (m < n + 1) Prop} :
( m (h : m < n + 1), p m h) p 0 (by omega) ( m (h : m < n), p (m + 1) (by omega)) := by
constructor
· intro w
constructor
· exact w 0 (by omega)
· intro m h
exact w (m + 1) (by omega)
· rintro h₀, h₁ m h
cases m with
| zero => exact h₀
| succ m => exact h₁ m (by omega)
/-- See `forall_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
theorem forall_lt_succ_left {p : Nat Prop} :
( m, m < n + 1 p m) p 0 ( m, m < n p (m + 1)) := by
simpa using forall_lt_succ_left' (p := fun m _ => p m)
/-- Dependent variant of `exists_lt_succ_right`. -/
theorem exists_lt_succ_right' {p : (m : Nat) (m < n + 1) Prop} :
( m, (h : m < n + 1), p m h) ( m, (h : m < n), p m (by omega)) p n (by omega) := by
simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
constructor
· rintro m, (h|rfl), w
· exact .inl m, h, w
· exact .inr w
· rintro (m, h, w | w)
· exact m, by omega, w
· exact n, by omega, w
/-- See `exists_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
theorem exists_lt_succ_right {p : Nat Prop} :
( m, m < n + 1 p m) ( m, m < n p m) p n := by
simpa using exists_lt_succ_right' (p := fun m _ => p m)
/-- Dependent variant of `exists_lt_succ_left`. -/
theorem exists_lt_succ_left' {p : (m : Nat) (m < n + 1) Prop} :
( m, (h : m < n + 1), p m h) p 0 (by omega) ( m, (h : m < n), p (m + 1) (by omega)) := by
constructor
· rintro _|m, h, w
· exact .inl w
· exact .inr m, by omega, w
· rintro (w|m, h, w)
· exact 0, by omega, w
· exact m + 1, by omega, w
/-- See `exists_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
theorem exists_lt_succ_left {p : Nat Prop} :
( m, m < n + 1 p m) p 0 ( m, m < n p (m + 1)) := by
simpa using exists_lt_succ_left' (p := fun m _ => p m)
/-! ## add -/
protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by
@@ -651,8 +580,8 @@ theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
| .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)
theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
rw (occs := .pos [1]) [ mod_add_div a n]
rw (occs := .pos [1]) [ mod_add_div b n]
rw (config := {occs := .pos [1]}) [ mod_add_div a n]
rw (config := {occs := .pos [1]}) [ mod_add_div b n]
rw [Nat.add_mul, Nat.mul_add, Nat.mul_add,
Nat.mul_assoc, Nat.mul_assoc, Nat.mul_add n, add_mul_mod_self_left,
Nat.mul_comm _ (n * (b / n)), Nat.mul_assoc, add_mul_mod_self_left]
@@ -873,10 +802,6 @@ theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
theorem log2_lt (h : n 0) : n.log2 < k n < 2 ^ k := by
rw [ Nat.not_le, Nat.not_le, le_log2 h]
@[simp]
theorem log2_two_pow : (2 ^ n).log2 = n := by
apply Nat.eq_of_le_of_lt_succ <;> simp [le_log2, log2_lt, NeZero.ne, Nat.pow_lt_pow_iff_right]
theorem log2_self_le (h : n 0) : 2 ^ n.log2 n := (le_log2 h).1 (Nat.le_refl _)
theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=

View File

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Core
import Init.Control.Basic
import Init.Coe
namespace Option

View File

@@ -86,6 +86,4 @@ instance : ForIn' m (Option α) α inferInstance where
match f a rfl init with
| .done r | .yield r => return r
-- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
end Option

View File

@@ -11,28 +11,4 @@ namespace Option
@[simp] theorem mem_toList {a : α} {o : Option α} : a o.toList a o := by
cases o <;> simp [eq_comm]
@[simp] theorem forIn'_none [Monad m] (b : β) (f : (a : α) a none β m (ForInStep β)) :
forIn' none b f = pure b := by
rfl
@[simp] theorem forIn'_some [Monad m] (a : α) (b : β) (f : (a' : α) a' some a β m (ForInStep β)) :
forIn' (some a) b f = bind (f a rfl b) (fun | .done r | .yield r => pure r) := by
rfl
@[simp] theorem forIn_none [Monad m] (b : β) (f : α β m (ForInStep β)) :
forIn none b f = pure b := by
rfl
@[simp] theorem forIn_some [Monad m] (a : α) (b : β) (f : α β m (ForInStep β)) :
forIn (some a) b f = bind (f a b) (fun | .done r | .yield r => pure r) := by
rfl
@[simp] theorem forIn'_toList [Monad m] (o : Option α) (b : β) (f : (a : α) a o.toList β m (ForInStep β)) :
forIn' o.toList b f = forIn' o b fun a m b => f a (by simpa using m) b := by
cases o <;> rfl
@[simp] theorem forIn_toList [Monad m] (o : Option α) (b : β) (f : α β m (ForInStep β)) :
forIn o.toList b f = forIn o b f := by
cases o <;> rfl
end Option

View File

@@ -20,6 +20,21 @@ instance : Membership Nat Range where
namespace Range
universe u v
@[inline] protected def forIn {β : Type u} {m : Type u Type v} [Monad m] (range : Range) (init : β) (f : Nat β m (ForInStep β)) : m β :=
-- pass `stop` and `step` separately so the `range` object can be eliminated through inlining
let rec @[specialize] loop (fuel i stop step : Nat) (b : β) : m β := do
if i stop then
return b
else match fuel with
| 0 => pure b
| fuel+1 => match ( f i b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop fuel (i + step) stop step b
loop range.stop range.start range.stop range.step init
instance : ForIn m Range Nat where
forIn := Range.forIn
@[inline] protected def forIn' {β : Type u} {m : Type u Type v} [Monad m] (range : Range) (init : β) (f : (i : Nat) i range β m (ForInStep β)) : m β :=
let rec @[specialize] loop (start stop step : Nat) (f : (i : Nat) start i i < stop β m (ForInStep β)) (fuel i : Nat) (hl : start i) (b : β) : m β := do
if hu : i < stop then
@@ -35,8 +50,6 @@ universe u v
instance : ForIn' m Range Nat inferInstance where
forIn' := Range.forIn'
-- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@[inline] protected def forM {m : Type u Type v} [Monad m] (range : Range) (f : Nat m PUnit) : m PUnit :=
let rec @[specialize] loop (fuel i stop step : Nat) : m PUnit := do
if i stop then

View File

@@ -5,6 +5,10 @@ Author: Leonardo de Moura
-/
prelude
import Init.Data.Format.Basic
import Init.Data.Int.Basic
import Init.Data.Nat.Div
import Init.Data.UInt.BasicAux
import Init.Control.Id
open Sum Subtype Nat
open Std

View File

@@ -1,11 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Init.Data.SInt.Basic
/-!
This module contains the definitions and basic theory about signed fixed width integer types.
-/

View File

@@ -1,116 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Init.Data.UInt.Basic
/-!
This module contains the definition of signed fixed width integer types as well as basic arithmetic
and bitwise operations on top of it.
-/
/--
The type of signed 8-bit integers. This type has special support in the
compiler to make it actually 8 bits rather than wrapping a `Nat`.
-/
structure Int8 where
/--
Obtain the `UInt8` that is 2's complement equivalent to the `Int8`.
-/
toUInt8 : UInt8
/-- The size of type `Int8`, that is, `2^8 = 256`. -/
abbrev Int8.size : Nat := 256
/--
Obtain the `BitVec` that contains the 2's complement representation of the `Int8`.
-/
@[inline] def Int8.toBitVec (x : Int8) : BitVec 8 := x.toUInt8.toBitVec
@[extern "lean_int8_of_int"]
def Int8.ofInt (i : @& Int) : Int8 := BitVec.ofInt 8 i
@[extern "lean_int8_of_int"]
def Int8.ofNat (n : @& Nat) : Int8 := BitVec.ofNat 8 n
abbrev Int.toInt8 := Int8.ofInt
abbrev Nat.toInt8 := Int8.ofNat
@[extern "lean_int8_to_int"]
def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt
@[inline] def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
@[extern "lean_int8_neg"]
def Int8.neg (i : Int8) : Int8 := -i.toBitVec
instance : ToString Int8 where
toString i := toString i.toInt
instance : OfNat Int8 n := Int8.ofNat n
instance : Neg Int8 where
neg := Int8.neg
@[extern "lean_int8_add"]
def Int8.add (a b : Int8) : Int8 := a.toBitVec + b.toBitVec
@[extern "lean_int8_sub"]
def Int8.sub (a b : Int8) : Int8 := a.toBitVec - b.toBitVec
@[extern "lean_int8_mul"]
def Int8.mul (a b : Int8) : Int8 := a.toBitVec * b.toBitVec
@[extern "lean_int8_div"]
def Int8.div (a b : Int8) : Int8 := BitVec.sdiv a.toBitVec b.toBitVec
@[extern "lean_int8_mod"]
def Int8.mod (a b : Int8) : Int8 := BitVec.smod a.toBitVec b.toBitVec
@[extern "lean_int8_land"]
def Int8.land (a b : Int8) : Int8 := a.toBitVec &&& b.toBitVec
@[extern "lean_int8_lor"]
def Int8.lor (a b : Int8) : Int8 := a.toBitVec ||| b.toBitVec
@[extern "lean_int8_xor"]
def Int8.xor (a b : Int8) : Int8 := a.toBitVec ^^^ b.toBitVec
@[extern "lean_int8_shift_left"]
def Int8.shiftLeft (a b : Int8) : Int8 := a.toBitVec <<< (mod b 8).toBitVec
@[extern "lean_int8_shift_right"]
def Int8.shiftRight (a b : Int8) : Int8 := BitVec.sshiftRight' a.toBitVec (mod b 8).toBitVec
@[extern "lean_int8_complement"]
def Int8.complement (a : Int8) : Int8 := ~~~a.toBitVec
@[extern "lean_int8_dec_eq"]
def Int8.decEq (a b : Int8) : Decidable (a = b) :=
match a, b with
| n, m =>
if h : n = m then
isTrue <| h rfl
else
isFalse (fun h' => Int8.noConfusion h' (fun h' => absurd h' h))
def Int8.lt (a b : Int8) : Prop := a.toBitVec.slt b.toBitVec
def Int8.le (a b : Int8) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited Int8 where
default := 0
instance : Add Int8 := Int8.add
instance : Sub Int8 := Int8.sub
instance : Mul Int8 := Int8.mul
instance : Mod Int8 := Int8.mod
instance : Div Int8 := Int8.div
instance : LT Int8 := Int8.lt
instance : LE Int8 := Int8.le
instance : Complement Int8 := Int8.complement
instance : AndOp Int8 := Int8.land
instance : OrOp Int8 := Int8.lor
instance : Xor Int8 := Int8.xor
instance : ShiftLeft Int8 := Int8.shiftLeft
instance : ShiftRight Int8 := Int8.shiftRight
instance : DecidableEq Int8 := Int8.decEq
@[extern "lean_int8_dec_lt"]
def Int8.decLt (a b : Int8) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@[extern "lean_int8_dec_le"]
def Int8.decLe (a b : Int8) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : Int8) : Decidable (a < b) := Int8.decLt a b
instance (a b : Int8) : Decidable (a b) := Int8.decLe a b
instance : Max Int8 := maxOfLe
instance : Min Int8 := minOfLe

View File

@@ -6,6 +6,7 @@ Author: Leonardo de Moura, Mario Carneiro
prelude
import Init.Data.List.Basic
import Init.Data.Char.Basic
import Init.Data.Option.Basic
universe u

View File

@@ -17,11 +17,11 @@ open Function
namespace Sum
protected theorem «forall» {p : α β Prop} :
@[simp] protected theorem «forall» {p : α β Prop} :
( x, p x) ( a, p (inl a)) b, p (inr b) :=
fun h => fun _ => h _, fun _ => h _, fun h₁, h₂ => Sum.rec h₁ h₂
protected theorem «exists» {p : α β Prop} :
@[simp] protected theorem «exists» {p : α β Prop} :
( x, p x) ( a, p (inl a)) b, p (inr b) :=
fun
| inl a, h => Or.inl a, h
@@ -116,7 +116,7 @@ theorem comp_elim (f : γ → δ) (g : αγ) (h : β → γ) :
theorem elim_eq_iff {u u' : α γ} {v v' : β γ} :
Sum.elim u v = Sum.elim u' v' u = u' v = v' := by
simp [funext_iff, Sum.forall]
simp [funext_iff]
/-! ### `Sum.map` -/

View File

@@ -4,9 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.Data.String.Basic
import Init.Data.UInt.BasicAux
import Init.Data.Nat.Div
import Init.Data.Repr
import Init.Data.Option.Basic
import Init.Data.Int.Basic
import Init.Data.Format.Basic
import Init.Control.Id
import Init.Control.Option
open Sum Subtype Nat
open Std

View File

@@ -19,8 +19,8 @@ def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
def UInt8.div (a b : UInt8) : UInt8 := BitVec.udiv a.toBitVec b.toBitVec
@[extern "lean_uint8_mod"]
def UInt8.mod (a b : UInt8) : UInt8 := BitVec.umod a.toBitVec b.toBitVec
@[deprecated UInt8.mod (since := "2024-09-23")]
def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := Fin.modn a.val n
@[extern "lean_uint8_modn", deprecated UInt8.mod (since := "2024-09-23")]
def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := Fin.modn a.val n
@[extern "lean_uint8_land"]
def UInt8.land (a b : UInt8) : UInt8 := a.toBitVec &&& b.toBitVec
@[extern "lean_uint8_lor"]
@@ -79,8 +79,8 @@ def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
def UInt16.div (a b : UInt16) : UInt16 := BitVec.udiv a.toBitVec b.toBitVec
@[extern "lean_uint16_mod"]
def UInt16.mod (a b : UInt16) : UInt16 := BitVec.umod a.toBitVec b.toBitVec
@[deprecated UInt16.mod (since := "2024-09-23")]
def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := Fin.modn a.val n
@[extern "lean_uint16_modn", deprecated UInt16.mod (since := "2024-09-23")]
def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := Fin.modn a.val n
@[extern "lean_uint16_land"]
def UInt16.land (a b : UInt16) : UInt16 := a.toBitVec &&& b.toBitVec
@[extern "lean_uint16_lor"]
@@ -141,8 +141,8 @@ def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
def UInt32.div (a b : UInt32) : UInt32 := BitVec.udiv a.toBitVec b.toBitVec
@[extern "lean_uint32_mod"]
def UInt32.mod (a b : UInt32) : UInt32 := BitVec.umod a.toBitVec b.toBitVec
@[deprecated UInt32.mod (since := "2024-09-23")]
def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := Fin.modn a.val n
@[extern "lean_uint32_modn", deprecated UInt32.mod (since := "2024-09-23")]
def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := Fin.modn a.val n
@[extern "lean_uint32_land"]
def UInt32.land (a b : UInt32) : UInt32 := a.toBitVec &&& b.toBitVec
@[extern "lean_uint32_lor"]
@@ -184,8 +184,8 @@ def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
def UInt64.div (a b : UInt64) : UInt64 := BitVec.udiv a.toBitVec b.toBitVec
@[extern "lean_uint64_mod"]
def UInt64.mod (a b : UInt64) : UInt64 := BitVec.umod a.toBitVec b.toBitVec
@[deprecated UInt64.mod (since := "2024-09-23")]
def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := Fin.modn a.val n
@[extern "lean_uint64_modn", deprecated UInt64.mod (since := "2024-09-23")]
def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := Fin.modn a.val n
@[extern "lean_uint64_land"]
def UInt64.land (a b : UInt64) : UInt64 := a.toBitVec &&& b.toBitVec
@[extern "lean_uint64_lor"]
@@ -243,8 +243,8 @@ def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
def USize.div (a b : USize) : USize := a.toBitVec / b.toBitVec
@[extern "lean_usize_mod"]
def USize.mod (a b : USize) : USize := a.toBitVec % b.toBitVec
@[deprecated USize.mod (since := "2024-09-23")]
def USize.modn (a : USize) (n : Nat) : USize := Fin.modn a.val n
@[extern "lean_usize_modn", deprecated USize.mod (since := "2024-09-23")]
def USize.modn (a : USize) (n : @& Nat) : USize := Fin.modn a.val n
@[extern "lean_usize_land"]
def USize.land (a b : USize) : USize := a.toBitVec &&& b.toBitVec
@[extern "lean_usize_lor"]

View File

@@ -144,26 +144,22 @@ instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (v
LawfulGetElem coll idx elem valid where
theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h) := by
have : Decidable (dom c i) := .isTrue h
(c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
rw [getElem?_def]
exact dif_pos h
theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none := by
have : Decidable (dom c i) := .isFalse h
(c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
rw [getElem?_def]
exact dif_neg h
theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
[Inhabited elem] (c : cont) (i : idx) (h : dom c i) :
[Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
c[i]! = c[i]'h := by
have : Decidable (dom c i) := .isTrue h
simp [getElem!_def, getElem?_def, h]
theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
[Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default := by
have : Decidable (dom c i) := .isFalse h
[Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
simp [getElem!_def, getElem?_def, h]
namespace Fin
@@ -207,10 +203,6 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where
@[deprecated (since := "2024-06-12")] abbrev cons_getElem_succ := @getElem_cons_succ
@[simp] theorem getElem_mem : {l : List α} {n} (h : n < l.length), l[n]'h l
| _ :: _, 0, _ => .head ..
| _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
match as, i with
| _::_, 0 => rfl

View File

@@ -7,7 +7,6 @@ Additional goodies for writing macros
-/
prelude
import Init.MetaTypes
import Init.Syntax
import Init.Data.Array.GetLit
import Init.Data.Option.BasicAux
@@ -443,7 +442,7 @@ def unsetTrailing (stx : Syntax) : Syntax :=
if h : i < a.size then
let v := a[i]
match f v with
| some v => some <| a.set i v h
| some v => some <| a.set i, h v
| none => updateFirst a f (i+1)
else
none
@@ -630,9 +629,6 @@ def mkStrLit (val : String) (info := SourceInfo.none) : StrLit :=
def mkNumLit (val : String) (info := SourceInfo.none) : NumLit :=
mkLit numLitKind val info
def mkNatLit (val : Nat) (info := SourceInfo.none) : NumLit :=
mkLit numLitKind (toString val) info
def mkScientificLit (val : String) (info := SourceInfo.none) : TSyntax scientificLitKind :=
mkLit scientificLitKind val info
@@ -1413,87 +1409,64 @@ namespace Parser
namespace Tactic
/--
Extracts the items from a tactic configuration,
either a `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`, or these wrapped in null nodes.
-/
partial def getConfigItems (c : Syntax) : TSyntaxArray ``configItem :=
if c.isOfKind nullKind then
c.getArgs.flatMap getConfigItems
else
match c with
| `(optConfig| $items:configItem*) => items
| `(config| (config := $_)) => #[⟨c⟩] -- handled by mkConfigItemViews
| _ => #[]
def mkOptConfig (items : TSyntaxArray ``configItem) : TSyntax ``optConfig :=
⟨Syntax.node1 .none ``optConfig (mkNullNode items)⟩
/--
Appends two tactic configurations.
The configurations can be `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`,
or these wrapped in null nodes (for example because the syntax is `(config)?`).
-/
def appendConfig (cfg cfg' : Syntax) : TSyntax ``optConfig :=
mkOptConfig <| getConfigItems cfg ++ getConfigItems cfg'
/-- `erw [rules]` is a shorthand for `rw (transparency := .default) [rules]`.
/-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
which only unfolds `@[reducible]` definitions). -/
macro "erw" c:optConfig s:rwRuleSeq loc:(location)? : tactic => do
`(tactic| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq $(loc)?)
macro "erw" s:rwRuleSeq loc:(location)? : tactic =>
`(tactic| rw (config := { transparency := .default }) $s $(loc)?)
syntax simpAllKind := atomic(" (" &"all") " := " &"true" ")"
syntax dsimpKind := atomic(" (" &"dsimp") " := " &"true" ")"
macro (name := declareSimpLikeTactic) doc?:(docComment)?
"declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?)
ppSpace tacName:ident ppSpace tacToken:str ppSpace cfg:optConfig : command => do
ppSpace tacName:ident ppSpace tacToken:str ppSpace updateCfg:term : command => do
let (kind, tkn, stx) ←
if opt.raw.isNone then
pure (← `(``simp), ← `("simp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
pure (← `(``simp), ← `("simp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
else if opt.raw[0].getKind == ``simpAllKind then
pure (← `(``simpAll), ← `("simp_all"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic))
pure (← `(``simpAll), ← `("simp_all"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic))
else
pure (← `(``dsimp), ← `("dsimp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
pure (← `(``dsimp), ← `("dsimp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
`($stx:command
@[macro $tacName] def expandSimp : Macro := fun s => do
let cfg`(optConfig| $cfg)
let c ← match s[1][0] with
| `(config| (config := $$c)) => `(config| (config := $updateCfg $$c))
| _ => `(config| (config := $updateCfg {}))
let s := s.setKind $kind
let s := s.setArg 0 (mkAtomFrom s[0] $tkn (canonical := true))
let s := s.setArg 1 (appendConfig s[1] cfg)
let s := s.mkSynthetic
return s)
let r := s.setArg 1 (mkNullNode #[c])
return r)
/-- `simp!` is shorthand for `simp` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic simpAutoUnfold "simp! " (autoUnfold := true)
declare_simp_like_tactic simpAutoUnfold "simp! " fun (c : Lean.Meta.Simp.Config) => { c with autoUnfold := true }
/-- `simp_arith` is shorthand for `simp` with `arith := true` and `decide := true`.
This enables the use of normalization by linear arithmetic. -/
declare_simp_like_tactic simpArith "simp_arith " (arith := true) (decide := true)
declare_simp_like_tactic simpArith "simp_arith " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, decide := true }
/-- `simp_arith!` is shorthand for `simp_arith` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " (arith := true) (autoUnfold := true) (decide := true)
declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, autoUnfold := true, decide := true }
/-- `simp_all!` is shorthand for `simp_all` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " (autoUnfold := true)
declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with autoUnfold := true }
/-- `simp_all_arith` combines the effects of `simp_all` and `simp_arith`. -/
declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " (arith := true) (decide := true)
declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, decide := true }
/-- `simp_all_arith!` combines the effects of `simp_all`, `simp_arith` and `simp!`. -/
declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " (arith := true) (autoUnfold := true) (decide := true)
declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, autoUnfold := true, decide := true }
/-- `dsimp!` is shorthand for `dsimp` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " (autoUnfold := true)
declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " fun (c : Lean.Meta.DSimp.Config) => { c with autoUnfold := true }
end Tactic

View File

@@ -341,19 +341,16 @@ macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)
notation:50 a:50 "" b:50 => ¬ (a b)
@[inherit_doc] infixr:67 " :: " => List.cons
@[inherit_doc] infixr:100 " <$> " => Functor.map
@[inherit_doc] infixl:55 " >>= " => Bind.bind
@[inherit_doc HOrElse.hOrElse] syntax:20 term:21 " <|> " term:20 : term
@[inherit_doc HOrElse.hOrElse] syntax:20 term:21 " <|> " term:20 : term
@[inherit_doc HAndThen.hAndThen] syntax:60 term:61 " >> " term:60 : term
@[inherit_doc Seq.seq] syntax:60 term:60 " <*> " term:61 : term
@[inherit_doc SeqLeft.seqLeft] syntax:60 term:60 " <* " term:61 : term
@[inherit_doc SeqRight.seqRight] syntax:60 term:60 " *> " term:61 : term
@[inherit_doc] infixl:55 " >>= " => Bind.bind
@[inherit_doc] notation:60 a:60 " <*> " b:61 => Seq.seq a fun _ : Unit => b
@[inherit_doc] notation:60 a:60 " <* " b:61 => SeqLeft.seqLeft a fun _ : Unit => b
@[inherit_doc] notation:60 a:60 " *> " b:61 => SeqRight.seqRight a fun _ : Unit => b
@[inherit_doc] infixr:100 " <$> " => Functor.map
macro_rules | `($x <|> $y) => `(binop_lazy% HOrElse.hOrElse $x $y)
macro_rules | `($x >> $y) => `(binop_lazy% HAndThen.hAndThen $x $y)
macro_rules | `($x <*> $y) => `(Seq.seq $x fun _ : Unit => $y)
macro_rules | `($x <* $y) => `(SeqLeft.seqLeft $x fun _ : Unit => $y)
macro_rules | `($x *> $y) => `(SeqRight.seqRight $x fun _ : Unit => $y)
namespace Lean

View File

@@ -10,7 +10,6 @@ import Init.Data.ToString.Basic
import Init.Data.Array.Subarray
import Init.Conv
import Init.Meta
import Init.While
namespace Lean
@@ -169,9 +168,9 @@ end Lean
| _ => throw ()
@[app_unexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
| `($(_) $_) => `(sorry)
| `($(_) $_ $_) => `(sorry)
| _ => throw ()
| `($(_) _) => `(sorry)
| `($(_) _ _) => `(sorry)
| _ => throw ()
@[app_unexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
| `($(_) $m $h) => `($h $m)
@@ -345,6 +344,42 @@ syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " t
macro_rules
| `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
/-! # `repeat` and `while` notation -/
inductive Loop where
| mk
@[inline]
partial def Loop.forIn {β : Type u} {m : Type u Type v} [Monad m] (_ : Loop) (init : β) (f : Unit β m (ForInStep β)) : m β :=
let rec @[specialize] loop (b : β) : m β := do
match f () b with
| ForInStep.done b => pure b
| ForInStep.yield b => loop b
loop init
instance : ForIn m Loop Unit where
forIn := Loop.forIn
syntax "repeat " doSeq : doElem
macro_rules
| `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
macro_rules
| `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
syntax "while " termBeforeDo " do " doSeq : doElem
macro_rules
| `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
macro_rules
| `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
`(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))

View File

@@ -2688,6 +2688,35 @@ def Array.mkArray7 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ : α) : Arr
def Array.mkArray8 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : α) : Array α :=
((((((((mkEmpty 8).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇).push a₈
/--
Set an element in an array without bounds checks, using a `Fin` index.
This will perform the update destructively provided that `a` has a reference
count of 1 when called.
-/
@[extern "lean_array_fset"]
def Array.set (a : Array α) (i : @& Fin a.size) (v : α) : Array α where
toList := a.toList.set i.val v
/--
Set an element in an array, or do nothing if the index is out of bounds.
This will perform the update destructively provided that `a` has a reference
count of 1 when called.
-/
@[inline] def Array.setD (a : Array α) (i : Nat) (v : α) : Array α :=
dite (LT.lt i a.size) (fun h => a.set i, h v) (fun _ => a)
/--
Set an element in an array, or panic if the index is out of bounds.
This will perform the update destructively provided that `a` has a reference
count of 1 when called.
-/
@[extern "lean_array_set"]
def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
Array.setD a i v
/-- Slower `Array.append` used in quotations. -/
protected def Array.appendCore {α : Type u} (as : Array α) (bs : Array α) : Array α :=
let rec loop (i : Nat) (j : Nat) (as : Array α) : Array α :=
@@ -3608,13 +3637,6 @@ def appendCore : Name → Name → Name
end Name
/-- The default maximum recursion depth. This is adjustable using the `maxRecDepth` option. -/
def defaultMaxRecDepth := 512
/-- The message to display on stack overflow. -/
def maxRecDepthErrorMessage : String :=
"maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
/-! # Syntax -/
/-- Source information of tokens. -/
@@ -3947,6 +3969,24 @@ def getId : Syntax → Name
| ident _ _ val _ => val
| _ => Name.anonymous
/--
Updates the argument list without changing the node kind.
Does nothing for non-`node` nodes.
-/
def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
match stx with
| node info k _ => node info k args
| stx => stx
/--
Updates the `i`'th argument of the syntax.
Does nothing for non-`node` nodes, or if `i` is out of bounds of the node list.
-/
def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
match stx with
| node info k args => node info k (args.setD i arg)
| stx => stx
/-- Retrieve the left-most node or leaf's info in the Syntax tree. -/
partial def getHeadInfo? : Syntax Option SourceInfo
| atom info _ => some info
@@ -4383,6 +4423,13 @@ main module and current macro scope.
bind getCurrMacroScope fun scp =>
pure (Lean.addMacroScope mainModule n scp)
/-- The default maximum recursion depth. This is adjustable using the `maxRecDepth` option. -/
def defaultMaxRecDepth := 512
/-- The message to display on stack overflow. -/
def maxRecDepthErrorMessage : String :=
"maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
namespace Syntax
/-- Is this syntax a null `node`? -/

View File

@@ -643,11 +643,11 @@ theorem decide_ite (u : Prop) [du : Decidable u] (p q : Prop)
(@ite _ p h q (decide p)) = (decide p && q) := by
split <;> simp_all
@[deprecated ite_then_decide_self (since := "2024-08-29")]
@[deprecated ite_then_decide_self]
theorem ite_true_decide_same (p : Prop) [Decidable p] (b : Bool) :
(if p then decide p else b) = (decide p || b) := ite_then_decide_self p b
@[deprecated ite_false_decide_same (since := "2024-08-29")]
@[deprecated ite_false_decide_same]
theorem ite_false_decide_same (p : Prop) [Decidable p] (b : Bool) :
(if p then b else decide p) = (decide p && b) := ite_else_decide_self p b

View File

@@ -54,13 +54,6 @@ theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂
: ( a : p₁, q₁ a) = ( a : p₂, q₂ a) := by
subst h₁; simp [ h₂]
theorem forall_prop_congr_dom {p₁ p₂ : Prop} (h : p₁ = p₂) (q : p₁ Prop) :
( a : p₁, q a) = ( a : p₂, q (h.substr a)) :=
h rfl
theorem pi_congr {α : Sort u} {β β' : α Sort v} (h : a, β a = β' a) : ( a, β a) = a, β' a :=
(funext h : β = β') rfl
theorem let_congr {α : Sort u} {β : Sort v} {a a' : α} {b b' : α β}
(h₁ : a = a') (h₂ : x, b x = b' x) : (let x := a; b x) = (let x := a'; b' x) :=
h₁ (funext h₂ : b = b') rfl

View File

@@ -1,36 +0,0 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Data.Array.Set
/-!
# Helper functions for `Syntax`.
These are delayed here to allow some time to bootstrap `Array`.
-/
namespace Lean.Syntax
/--
Updates the argument list without changing the node kind.
Does nothing for non-`node` nodes.
-/
def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
match stx with
| node info k _ => node info k args
| stx => stx
/--
Updates the `i`'th argument of the syntax.
Does nothing for non-`node` nodes, or if `i` is out of bounds of the node list.
-/
def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
match stx with
| node info k args => node info k (args.setD i arg)
| stx => stx
end Lean.Syntax

View File

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.System.Platform
import Init.Data.String.Basic
import Init.Data.Repr
import Init.Data.ToString.Basic
namespace System

View File

@@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone
-/
prelude
import Init.Control.Reader
import Init.Data.String
import Init.Data.ByteArray
import Init.System.IOError
import Init.System.FilePath
import Init.System.ST
import Init.Data.ToString.Macro
import Init.Data.Ord
open System

View File

@@ -5,7 +5,10 @@ Authors: Simon Hudon
-/
prelude
import Init.Core
import Init.Data.UInt.Basic
import Init.Data.ToString.Basic
import Init.Data.String.Basic
/--
Imitate the structure of IOErrorType in Haskell:

View File

@@ -417,27 +417,7 @@ It synthesizes a value of any target type by typeclass inference.
-/
macro "infer_instance" : tactic => `(tactic| exact inferInstance)
/--
`+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`.
-/
syntax posConfigItem := "+" noWs ident
/--
`-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`.
-/
syntax negConfigItem := "-" noWs ident
/--
`(opt := val)` sets the `opt` configuration option to `val`.
As a special case, `(config := ...)` sets the entire configuration.
-/
syntax valConfigItem := atomic(" (" notFollowedBy(&"discharger" <|> &"disch") (ident <|> &"config")) " := " withoutPosition(term) ")"
/-- A configuration item for a tactic configuration. -/
syntax configItem := posConfigItem <|> negConfigItem <|> valConfigItem
/-- Configuration options for tactics. -/
syntax optConfig := (colGt configItem)*
/-- Optional configuration option for tactics. (Deprecated. Replace `(config)?` with `optConfig`.) -/
/-- Optional configuration option for tactics -/
syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")"
/-- The `*` location refers to all hypotheses and the goal. -/
@@ -494,28 +474,28 @@ This provides a convenient way to unfold `e`.
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.
Using `rw (occs := .pos L) [e]`,
Using `rw (config := {occs := .pos L}) [e]`,
where `L : List Nat`, you can control which "occurrences" are rewritten.
(This option applies to each rule, so usually this will only be used with a single rule.)
Occurrences count from `1`.
At each allowed occurrence, arguments of the rewrite rule `e` may be instantiated,
restricting which later rewrites can be found.
(Disallowed occurrences do not result in instantiation.)
`(occs := .neg L)` allows skipping specified occurrences.
`{occs := .neg L}` allows skipping specified occurrences.
-/
syntax (name := rewriteSeq) "rewrite" optConfig rwRuleSeq (location)? : tactic
syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic
/--
`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
-/
macro (name := rwSeq) "rw " c:optConfig s:rwRuleSeq l:(location)? : tactic =>
macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
match s with
| `(rwRuleSeq| [$rs,*]%$rbrak) =>
-- We show the `rfl` state on `]`
`(tactic| (rewrite $c [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
`(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
| _ => Macro.throwUnsupported
/-- `rwa` is short-hand for `rw; assumption`. -/
/-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/
macro "rwa " rws:rwRuleSeq loc:(location)? : tactic =>
`(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption))
@@ -581,14 +561,14 @@ non-dependent hypotheses. It has many variants:
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
other hypotheses.
-/
syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
/--
`simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target
are simplified multiple times until no simplification is applicable.
Only non-dependent propositional hypotheses are considered.
-/
syntax (name := simpAll) "simp_all" optConfig (discharger)? (&" only")?
syntax (name := simpAll) "simp_all" (config)? (discharger)? (&" only")?
(" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? : tactic
/--
@@ -596,7 +576,7 @@ The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but o
applies theorems that hold by reflexivity. Thus, the result is guaranteed to be
definitionally equal to the input.
-/
syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
(" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
/--
@@ -618,7 +598,7 @@ def dsimpArg := simpErase.binary `orelse simpLemma
syntax dsimpArgs := " [" dsimpArg,* "]"
/-- The common arguments of `simp?` and `simp?!`. -/
syntax simpTraceArgsRest := optConfig (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
syntax simpTraceArgsRest := (config)? (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
/--
`simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
@@ -637,7 +617,7 @@ syntax (name := simpTrace) "simp?" "!"? simpTraceArgsRest : tactic
macro tk:"simp?!" rest:simpTraceArgsRest : tactic => `(tactic| simp?%$tk ! $rest)
/-- The common arguments of `simp_all?` and `simp_all?!`. -/
syntax simpAllTraceArgsRest := optConfig (discharger)? (&" only")? (dsimpArgs)?
syntax simpAllTraceArgsRest := (config)? (discharger)? (&" only")? (dsimpArgs)?
@[inherit_doc simpTrace]
syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
@@ -646,7 +626,7 @@ syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
macro tk:"simp_all?!" rest:simpAllTraceArgsRest : tactic => `(tactic| simp_all?%$tk ! $rest)
/-- The common arguments of `dsimp?` and `dsimp?!`. -/
syntax dsimpTraceArgsRest := optConfig (&" only")? (dsimpArgs)? (ppSpace location)?
syntax dsimpTraceArgsRest := (config)? (&" only")? (dsimpArgs)? (ppSpace location)?
@[inherit_doc simpTrace]
syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
@@ -655,7 +635,7 @@ syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
macro tk:"dsimp?!" rest:dsimpTraceArgsRest : tactic => `(tactic| dsimp?%$tk ! $rest)
/-- The arguments to the `simpa` family tactics. -/
syntax simpaArgsRest := optConfig (discharger)? &" only "? (simpArgs)? (" using " term)?
syntax simpaArgsRest := (config)? (discharger)? &" only "? (simpArgs)? (" using " term)?
/--
This is a "finishing" tactic modification of `simp`. It has two forms.
@@ -1168,7 +1148,8 @@ a natural subtraction appearing in a hypothesis, and try again.
The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
omega (config :=
{ splitDisjunctions := true, splitNatSub := true, splitNatAbs := true, splitMinMax := true })
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
@@ -1178,7 +1159,7 @@ can be used to:
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a min a b = b`
Currently, all of these are on by default.
-/
syntax (name := omega) "omega" optConfig : tactic
syntax (name := omega) "omega" (config)? : tactic
/--
`bv_omega` is `omega` with an additional preprocessor that turns statements about `BitVec` into statements about `Nat`.
@@ -1291,7 +1272,7 @@ example (a b : Nat)
See also `norm_cast`.
-/
syntax (name := pushCast) "push_cast" optConfig (discharger)? (&" only")?
syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
(" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
/--
@@ -1367,7 +1348,7 @@ See also the doc-comment for `Lean.Meta.Tactic.Backtrack.BacktrackConfig` for th
Both `apply_assumption` and `apply_rules` are implemented via these hooks.
-/
syntax (name := solveByElim)
"solve_by_elim" "*"? optConfig (&" only")? (args)? (using_)? : tactic
"solve_by_elim" "*"? (config)? (&" only")? (args)? (using_)? : tactic
/--
`apply_assumption` looks for an assumption of the form `... → ∀ _, ... → head`
@@ -1390,7 +1371,7 @@ You can pass a further configuration via the syntax `apply_rules (config := {...
The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).
-/
syntax (name := applyAssumption)
"apply_assumption" optConfig (&" only")? (args)? (using_)? : tactic
"apply_assumption" (config)? (&" only")? (args)? (using_)? : tactic
/--
`apply_rules [l₁, l₂, ...]` tries to solve the main goal by iteratively
@@ -1415,7 +1396,7 @@ You can bound the iteration depth using the syntax `apply_rules (config := {maxD
Unlike `solve_by_elim`, `apply_rules` does not perform backtracking, and greedily applies
a lemma from the list until it gets stuck.
-/
syntax (name := applyRules) "apply_rules" optConfig (&" only")? (args)? (using_)? : tactic
syntax (name := applyRules) "apply_rules" (config)? (&" only")? (args)? (using_)? : tactic
end SolveByElim
/--
@@ -1509,11 +1490,6 @@ have been simplified by using the modifier `↓`. Here is an example
@[simp↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ¬q) :=
```
You can instruct the simplifier to rewrite the lemma from right-to-left:
```lean
attribute @[simp ←] and_assoc
```
When multiple simp theorems are applicable, the simplifier uses the one with highest priority.
The equational theorems of function are applied at very low priority (100 and below).
If there are several with the same priority, it is uses the "most recent one". Example:
@@ -1525,7 +1501,7 @@ If there are several with the same priority, it is uses the "most recent one". E
cases d <;> rfl
```
-/
syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("" <|> "<- ")? (ppSpace prio)? : attr
syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
/--
Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
@@ -1614,7 +1590,7 @@ where `i < arr.size` is in the context) and `simp_arith` and `omega`
syntax "get_elem_tactic_trivial" : tactic
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp +arith; done)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
/--

View File

@@ -70,11 +70,11 @@ macro_rules
/--
Rewrites with the given rules, normalizing casts prior to each step.
-/
syntax "rw_mod_cast" optConfig rwRuleSeq (location)? : tactic
syntax "rw_mod_cast" (config)? rwRuleSeq (location)? : tactic
macro_rules
| `(tactic| rw_mod_cast $cfg:optConfig [$rules,*] $[$loc]?) => do
| `(tactic| rw_mod_cast $[$config]? [$rules,*] $[$loc]?) => do
let tacs rules.getElems.mapM fun rule =>
`(tactic| (norm_cast at *; rw $cfg [$rule] $[$loc]?))
`(tactic| (norm_cast at *; rw $[$config]? [$rule] $[$loc]?))
`(tactic| ($[$tacs]*))
/--

View File

@@ -16,14 +16,15 @@ user, and this tactic should no longer be necessary. Calls to `simp_wf` can be r
by plain calls to `simp`.
-/
macro "simp_wf" : tactic =>
`(tactic| try simp +unfoldPartialApp +zetaDelta [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
`(tactic| try simp (config := { unfoldPartialApp := true, zetaDelta := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
/--
This tactic is used internally by lean before presenting the proof obligations from a well-founded
definition to the user via `decreasing_by`. It is not necessary to use this tactic manually.
-/
macro "clean_wf" : tactic =>
`(tactic| simp +unfoldPartialApp +zetaDelta -failIfUnchanged
`(tactic| simp
(config := { unfoldPartialApp := true, zetaDelta := true, failIfUnchanged := false })
only [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel,
WellFoundedRelation.rel, sizeOf_nat, reduceCtorEq])
@@ -36,7 +37,7 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
-/
syntax "decreasing_trivial" : tactic
macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp +arith -failIfUnchanged) <;> done)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)

View File

@@ -1,51 +0,0 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Core
/-!
# Notation for `while` and `repeat` loops.
-/
namespace Lean
/-! # `repeat` and `while` notation -/
inductive Loop where
| mk
@[inline]
partial def Loop.forIn {β : Type u} {m : Type u Type v} [Monad m] (_ : Loop) (init : β) (f : Unit β m (ForInStep β)) : m β :=
let rec @[specialize] loop (b : β) : m β := do
match f () b with
| ForInStep.done b => pure b
| ForInStep.yield b => loop b
loop init
instance : ForIn m Loop Unit where
forIn := Loop.forIn
syntax "repeat " doSeq : doElem
macro_rules
| `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
macro_rules
| `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
syntax "while " termBeforeDo " do " doSeq : doElem
macro_rules
| `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
macro_rules
| `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
end Lean

View File

@@ -87,7 +87,7 @@ def hasOutParams (env : Environment) (declName : Name) : Bool :=
incorrect. This transformation would be counterintuitive to users since
we would implicitly treat these regular parameters as `outParam`s.
-/
private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (outParams : Array Nat) (type : Expr) : Except MessageData (Array Nat) :=
private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (outParams : Array Nat) (type : Expr) : Except String (Array Nat) :=
match type with
| .forallE _ d b bi =>
let addOutParam (_ : Unit) :=
@@ -102,7 +102,7 @@ private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (ou
/- See issue #1852 for a motivation for `bi.isInstImplicit` -/
addOutParam ()
else
Except.error m!"invalid class, parameter #{i+1} depends on `outParam`, but it is not an `outParam`"
Except.error s!"invalid class, parameter #{i+1} depends on `outParam`, but it is not an `outParam`"
else
checkOutParam (i+1) outParamFVarIds outParams b
| _ => return outParams
@@ -149,13 +149,13 @@ and it must be the name of constant in `env`.
`declName` must be a inductive datatype or axiom.
Recall that all structures are inductive datatypes.
-/
def addClass (env : Environment) (clsName : Name) : Except MessageData Environment := do
def addClass (env : Environment) (clsName : Name) : Except String Environment := do
if isClass env clsName then
throw m!"class has already been declared '{.ofConstName clsName true}'"
throw s!"class has already been declared '{clsName}'"
let some decl := env.find? clsName
| throw m!"unknown declaration '{clsName}'"
| throw s!"unknown declaration '{clsName}'"
unless decl matches .inductInfo .. | .axiomInfo .. do
throw m!"invalid 'class', declaration '{.ofConstName clsName}' must be inductive datatype, structure, or constant"
throw s!"invalid 'class', declaration '{clsName}' must be inductive datatype, structure, or constant"
let outParams checkOutParam 0 #[] #[] decl.type
return classExtension.addEntry env { name := clsName, outParams }

View File

@@ -13,7 +13,7 @@ partial def reshapeWithoutDead (bs : Array FnBody) (term : FnBody) : FnBody :=
let rec reshape (bs : Array FnBody) (b : FnBody) (used : IndexSet) :=
if bs.isEmpty then b
else
let curr := bs.back!
let curr := bs.back
let bs := bs.pop
let keep (_ : Unit) :=
let used := curr.collectFreeIndices used

View File

@@ -1075,7 +1075,7 @@ def emitSetTag (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) : M llvmct
def ensureHasDefault' (alts : Array Alt) : Array Alt :=
if alts.any Alt.isDefault then alts
else
let last := alts.back!
let last := alts.back
let alts := alts.pop
alts.push (Alt.default last.body)

View File

@@ -56,7 +56,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
if bs.size < 2 then done ()
else
let b := bs.back!
let b := bs.back
match b with
| .vdecl _ _ (.sproj _ _ _) _ => keepInstr b
| .vdecl _ _ (.uproj _ _) _ => keepInstr b

View File

@@ -13,7 +13,7 @@ namespace Lean.IR
partial def pushProjs (bs : Array FnBody) (alts : Array Alt) (altsF : Array IndexSet) (ctx : Array FnBody) (ctxF : IndexSet) : Array FnBody × Array Alt :=
if bs.isEmpty then (ctx.reverse, alts)
else
let b := bs.back!
let b := bs.back
let bs := bs.pop
let done (_ : Unit) := (bs.push b ++ ctx.reverse, alts)
let skip (_ : Unit) := pushProjs bs alts altsF (ctx.push b) (b.collectFreeIndices ctxF)

View File

@@ -13,8 +13,8 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
if alts.any Alt.isDefault then alts
else if alts.size < 2 then alts
else
let last := alts.back!
let alts := alts.pop
let last := alts.back;
let alts := alts.pop;
alts.push (Alt.default last.body)
private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do

View File

@@ -168,12 +168,13 @@ mutual
/- TODO: after we erase universe variables, we can just extract a better type using just `structName` and `idx`. -/
return erasedExpr
else
matchConstStructure structType.getAppFn failed fun structVal structLvls ctorVal =>
let structTypeArgs := structType.getAppArgs
if structVal.numParams + structVal.numIndices != structTypeArgs.size then
matchConstStruct structType.getAppFn failed fun structVal structLvls ctorVal =>
let n := structVal.numParams
let structParams := structType.getAppArgs
if n != structParams.size then
failed ()
else do
let mut ctorType inferAppType (mkAppN (mkConst ctorVal.name structLvls) structTypeArgs[:structVal.numParams])
let mut ctorType inferAppType (mkAppN (mkConst ctorVal.name structLvls) structParams)
for _ in [:idx] do
match ctorType with
| .forallE _ _ body _ =>

View File

@@ -46,7 +46,7 @@ partial def withCheckpoint (x : PullM Code) : PullM Code := do
else
return c
let (c, keep) := go toPullSizeSaved ( read).included |>.run #[]
modify fun s => { s with toPull := s.toPull.take toPullSizeSaved ++ keep }
modify fun s => { s with toPull := s.toPull.shrink toPullSizeSaved ++ keep }
return c
def attachToPull (c : Code) : PullM Code := do

View File

@@ -271,11 +271,11 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
| none => m.insert p.fst p.snd
| some v => m.insert p.fst $ f v p.snd)
attribute [deprecated Std.HashMap (since := "2024-08-08")] HashMap
attribute [deprecated Std.HashMap.Raw (since := "2024-08-08")] HashMapImp
attribute [deprecated Std.HashMap.Raw.empty (since := "2024-08-08")] mkHashMapImp
attribute [deprecated Std.HashMap.empty (since := "2024-08-08")] mkHashMap
attribute [deprecated Std.HashMap.empty (since := "2024-08-08")] HashMap.empty
attribute [deprecated Std.HashMap.ofList (since := "2024-08-08")] HashMap.ofList
attribute [deprecated Std.HashMap] HashMap
attribute [deprecated Std.HashMap.Raw] HashMapImp
attribute [deprecated Std.HashMap.Raw.empty] mkHashMapImp
attribute [deprecated Std.HashMap.empty] mkHashMap
attribute [deprecated Std.HashMap.empty] HashMap.empty
attribute [deprecated Std.HashMap.ofList] HashMap.ofList
end Lean.HashMap

View File

@@ -219,8 +219,8 @@ def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :
t.fold (init := s) fun s a => s.insert a
-- We don't use `insertMany` here because it gives weird universes.
attribute [deprecated Std.HashSet (since := "2024-08-08")] HashSet
attribute [deprecated Std.HashSet.Raw (since := "2024-08-08")] HashSetImp
attribute [deprecated Std.HashSet.Raw.empty (since := "2024-08-08")] mkHashSetImp
attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] mkHashSet
attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] HashSet.empty
attribute [deprecated Std.HashSet] HashSet
attribute [deprecated Std.HashSet.Raw] HashSetImp
attribute [deprecated Std.HashSet.Raw.empty] mkHashSetImp
attribute [deprecated Std.HashSet.empty] mkHashSet
attribute [deprecated Std.HashSet.empty] HashSet.empty

View File

@@ -177,7 +177,7 @@ def updateSyntax (m : KVMap) (k : Name) (f : Syntax → Syntax) : KVMap :=
@[inline] protected def forIn.{w, w'} {δ : Type w} {m : Type w Type w'} [Monad m]
(kv : KVMap) (init : δ) (f : Name × DataValue δ m (ForInStep δ)) : m δ :=
forIn kv.entries init f
kv.entries.forIn init f
instance : ForIn m KVMap (Name × DataValue) where
forIn := KVMap.forIn

View File

@@ -70,7 +70,7 @@ private def lineStartPos (text : FileMap) (line : Nat) : String.Pos :=
else if text.positions.isEmpty then
0
else
text.positions.back!
text.positions.back
/-- Computes an UTF-8 offset into `text.source`
from an LSP-style 0-indexed (ln, col) position. -/

View File

@@ -159,7 +159,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
let cs' := cs'.pop
if cs'.isEmpty then (some l, emptyArray) else (some l, cs')
else
(some l, cs'.set idx (node newLast) (by simp only [cs', Array.size_set]; omega))
(some l, cs'.set (Array.size_set cs idx _ idx) (node newLast))
else
(none, emptyArray)
| leaf vs => (some vs, emptyArray)

View File

@@ -66,12 +66,12 @@ partial def ofString (s : String) : FileMap :=
let i := s.next i
if c == '\n' then loop i (line+1) (ps.push i)
else loop i line ps
loop 0 1 #[0]
loop 0 1 (#[0])
partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
match fmap with
| { source := str, positions := ps } =>
if ps.size >= 2 && pos <= ps.back! then
if ps.size >= 2 && pos <= ps.back then
let rec toColumn (i : String.Pos) (c : Nat) : Nat :=
if i == pos || str.atEnd i then c
else toColumn (str.next i) (c+1)
@@ -84,14 +84,14 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
if pos == posM then { line := fmap.getLine m, column := 0 }
else if pos > posM then loop m e
else loop b m
loop 0 (ps.size - 1)
loop 0 (ps.size -1)
else if ps.isEmpty then
0, 0
else
-- Some systems like the delaborator use synthetic positions without an input file,
-- which would violate `toPositionAux`'s invariant.
-- Can also happen with EOF errors, which are not strictly inside the file.
fmap.getLastLine, (pos - ps.back!).byteIdx
fmap.getLastLine, (pos - ps.back).byteIdx
/-- Convert a `Lean.Position` to a `String.Pos`. -/
def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
@@ -101,7 +101,7 @@ def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
else if text.positions.isEmpty then
0
else
text.positions.back!
text.positions.back
String.Iterator.nextn text.source, colPos pos.column |>.pos
/--

View File

@@ -298,14 +298,9 @@ instance : ForIn m (RBMap α β cmp) (α × β) where
| leaf, _ => true
| _ => false
/-- Returns a `List` of the key/value pairs in order. -/
@[specialize] def toList : RBMap α β cmp List (α × β)
| t, _ => t.revFold (fun ps k v => (k, v)::ps) []
/-- Returns an `Array` of the key/value pairs in order. -/
@[specialize] def toArray : RBMap α β cmp Array (α × β)
| t, _ => t.fold (fun ps k v => ps.push (k, v)) #[]
/-- Returns the kv pair `(a,b)` such that `a ≤ k` for all keys in the RBMap. -/
@[inline] protected def min : RBMap α β cmp Option (α × β)
| t, _ =>

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