Compare commits

..

1 Commits

Author SHA1 Message Date
Kim Morrison
a0803909e8 chore: upstream classical tactic
chore: upstream classical tactic
2024-10-16 14:16:25 +11:00
928 changed files with 3375 additions and 9658 deletions

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

@@ -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

@@ -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

@@ -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

@@ -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,4 +35,3 @@ import Init.Ext
import Init.Omega
import Init.MacroTrace
import Init.Grind
import Init.While

View File

@@ -8,28 +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.
-/
instance (priority := low) 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
@[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

@@ -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
@@ -1384,7 +1385,6 @@ gen_injective_theorems% Except
gen_injective_theorems% EStateM.Result
gen_injective_theorems% Lean.Name
gen_injective_theorems% Lean.Syntax
gen_injective_theorems% BitVec
theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ m = n :=
fun x => Nat.noConfusion x id
@@ -1936,6 +1936,15 @@ instance : Subsingleton (Squash α) where
apply Quot.sound
trivial
/-! # Relations -/
/--
`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
-/
class Antisymm {α : Sort u} (r : α α Prop) : Prop where
/-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
antisymm {a b : α} : r a b r b a a = b
namespace Lean
/-! # Kernel reduction hints -/
@@ -2111,14 +2120,4 @@ instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
instance : Commutative And := fun _ _ => propext and_comm
instance : Commutative Iff := fun _ _ => propext iff_comm
/--
`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
-/
class Antisymm (r : α α Prop) : Prop where
/-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
antisymm {a b : α} : r a b r b a a = b
@[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
abbrev _root_.Antisymm (r : α α Prop) : Prop := Std.Antisymm r
end Std

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

@@ -16,4 +16,3 @@ import Init.Data.Array.Lemmas
import Init.Data.Array.TakeDrop
import Init.Data.Array.Bootstrap
import Init.Data.Array.GetLit
import Init.Data.Array.MapIdx

View File

@@ -7,7 +7,7 @@ prelude
import Init.WFTactics
import Init.Data.Nat.Basic
import Init.Data.Fin.Basic
import Init.Data.UInt.BasicAux
import Init.Data.UInt.Basic
import Init.Data.Repr
import Init.Data.ToString.Basic
import Init.GetElem
@@ -25,8 +25,6 @@ variable {α : Type u}
namespace Array
@[deprecated toList (since := "2024-10-13")] abbrev data := @toList
/-! ### Preliminary theorems -/
@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
@@ -80,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
@@ -257,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
@@ -332,37 +291,6 @@ protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m
instance : ForIn m (Array α) α where
forIn := Array.forIn
/-- See comment at `forInUnsafe` -/
@[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 β :=
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
| 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 β :=
let rec loop (i : Nat) (h : i as.size) (b : β) : m β := do
match i, h with
| 0, _ => pure b
| i+1, h =>
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
| 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'
/-- 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 β :=
@@ -468,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
@@ -592,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)]`. -/
@@ -689,17 +607,13 @@ protected def appendList (as : Array α) (bs : List α) : Array α :=
instance : HAppend (Array α) (List α) (Array α) := Array.appendList
@[inline]
def flatMapM [Monad m] (f : α m (Array β)) (as : Array α) : m (Array β) :=
def concatMapM [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
@[inline]
def flatMap (f : α Array β) (as : Array α) : Array β :=
def concatMap (f : α Array β) (as : Array α) : Array β :=
as.foldl (init := empty) fun bs a => bs ++ f a
@[deprecated flatMap (since := "2024-10-16")] abbrev concatMap := @flatMap
/-- Joins array of array into a single array.
`flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`
@@ -899,15 +813,9 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
/-! ## Auxiliary functions used in metaprogramming.
We do not currently intend to provide verification theorems for these functions.
We do not intend to provide verification theorems for these functions.
-/
/- ### reduceOption -/
/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
@[inline] def reduceOption (as : Array (Option α)) : Array α :=
as.filterMap id
/-! ### eraseReps -/
/--

View File

@@ -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,8 +6,6 @@ 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
@@ -28,14 +26,6 @@ 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 α) :
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]
@@ -43,29 +33,6 @@ theorem rel_of_isEqv (r : αα → Bool) (a b : Array α) :
· 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 r a b, fun h, w => by
simp only [isEqv, h, reduceDIte]
exact isEqvAux_of_rel r a b h a.size (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 (fun x y => x = y) a b h
exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
@@ -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

File diff suppressed because it is too large Load Diff

View File

@@ -1,92 +0,0 @@
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Kim Morrison
-/
prelude
import Init.Data.Array.Lemmas
import Init.Data.List.MapIdx
namespace Array
/-! ### mapFinIdx -/
-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
theorem mapFinIdx_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
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
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]
| 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]
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
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
/-! ### 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 α β)
(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 :=
(mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
@[simp] theorem getElem_mapIdx (a : Array α) (f : Nat α β) (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)
@[simp] theorem getElem?_mapIdx (a : Array α) (f : Nat α β) (i : Nat) :
(a.mapIdx f)[i]? =
a[i]?.map (f i) := by
simp [getElem?_def, size_mapIdx, getElem_mapIdx]
end Array

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

@@ -8,13 +8,12 @@ import Init.Data.Fin.Basic
import Init.Data.Nat.Bitwise.Lemmas
import Init.Data.Nat.Power2
import Init.Data.Int.Bitwise
import Init.Data.BitVec.BasicAux
/-!
We define the basic algebraic structure of bitvectors. We choose the `Fin` representation over
others for its relative efficiency (Lean has special support for `Nat`), and the fact that bitwise
operations on `Fin` are already defined. Some other possible representations are `List Bool`,
`{ l : List Bool // l.length = w }`, `Fin w → Bool`.
We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
(Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
with `Fin`, and the fact that bitwise operations on `Fin` are already defined. Some other possible
representations are `List Bool`, `{ l : List Bool // l.length = w }`, `Fin w → Bool`.
We define many of the bitvector operations from the
[`QF_BV` logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).
@@ -23,12 +22,60 @@ of SMT-LIBv2.
set_option linter.missingDocs true
/--
A bitvector of the specified width.
This is represented as the underlying `Nat` number in both the runtime
and the kernel, inheriting all the special support for `Nat`.
-/
structure BitVec (w : Nat) where
/-- Construct a `BitVec w` from a number less than `2^w`.
O(1), because we use `Fin` as the internal representation of a bitvector. -/
ofFin ::
/-- Interpret a bitvector as a number less than `2^w`.
O(1), because we use `Fin` as the internal representation of a bitvector. -/
toFin : Fin (2^w)
/--
Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
-/
-- We manually derive the `DecidableEq` instances for `BitVec` because
-- we want to have builtin support for bit-vector literals, and we
-- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
def BitVec.decEq (x y : BitVec n) : Decidable (x = y) :=
match x, y with
| n, m =>
if h : n = m then
isTrue (h rfl)
else
isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h))
instance : DecidableEq (BitVec n) := BitVec.decEq
namespace BitVec
section Nat
/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
@[match_pattern]
protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2^n) : BitVec n where
toFin := i, p
/-- The `BitVec` with value `i mod 2^n`. -/
@[match_pattern]
protected def ofNat (n : Nat) (i : Nat) : BitVec n where
toFin := Fin.ofNat' (2^n) i
instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
instance natCastInst : NatCast (BitVec w) := BitVec.ofNat w
/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
(zero-cost) wrapper around a `Nat`. -/
protected def toNat (x : BitVec n) : Nat := x.toFin.val
/-- Return the bound in terms of toNat. -/
theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
@[deprecated isLt (since := "2024-03-12")]
theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
@@ -191,6 +238,22 @@ end repr_toString
section arithmetic
/--
Addition for bit vectors. This can be interpreted as either signed or unsigned addition
modulo `2^n`.
SMT-Lib name: `bvadd`.
-/
protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
instance : Add (BitVec n) := BitVec.add
/--
Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
modulo `2^n`.
-/
protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
instance : Sub (BitVec n) := BitVec.sub
/--
Negation for bit vectors. This can be interpreted as either signed or unsigned negation
modulo `2^n`.
@@ -324,6 +387,10 @@ SMT-Lib name: `bvult`.
-/
protected def ult (x y : BitVec n) : Bool := x.toNat < y.toNat
instance : LT (BitVec n) where lt := (·.toNat < ·.toNat)
instance (x y : BitVec n) : Decidable (x < y) :=
inferInstanceAs (Decidable (x.toNat < y.toNat))
/--
Unsigned less-than-or-equal-to for bit vectors.
@@ -331,6 +398,10 @@ SMT-Lib name: `bvule`.
-/
protected def ule (x y : BitVec n) : Bool := x.toNat y.toNat
instance : LE (BitVec n) where le := (·.toNat ·.toNat)
instance (x y : BitVec n) : Decidable (x y) :=
inferInstanceAs (Decidable (x.toNat y.toNat))
/--
Signed less-than for bit vectors.

View File

@@ -1,52 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed
-/
prelude
import Init.Data.Fin.Basic
set_option linter.missingDocs true
/-!
This module exists to provide the very basic `BitVec` definitions required for
`Init.Data.UInt.BasicAux`.
-/
namespace BitVec
section Nat
/-- The `BitVec` with value `i mod 2^n`. -/
@[match_pattern]
protected def ofNat (n : Nat) (i : Nat) : BitVec n where
toFin := Fin.ofNat' (2^n) i
instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
/-- Return the bound in terms of toNat. -/
theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
end Nat
section arithmetic
/--
Addition for bit vectors. This can be interpreted as either signed or unsigned addition
modulo `2^n`.
SMT-Lib name: `bvadd`.
-/
protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
instance : Add (BitVec n) := BitVec.add
/--
Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
modulo `2^n`.
-/
protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
instance : Sub (BitVec n) := BitVec.sub
end arithmetic
end BitVec

View File

@@ -267,21 +267,6 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
/-! ### add -/
theorem getMsbD_add {i : Nat} {i_lt : i < w} {x y : BitVec w} :
getMsbD (x + y) i =
Bool.xor (getMsbD x i) (Bool.xor (getMsbD y i) (carry (w - 1 - i) x y false)) := by
simp [getMsbD, getLsbD_add, i_lt, show w - 1 - i < w by omega]
theorem msb_add {w : Nat} {x y: BitVec w} :
(x + y).msb =
Bool.xor x.msb (Bool.xor y.msb (carry (w - 1) x y false)) := by
simp only [BitVec.msb, BitVec.getMsbD]
by_cases h : w 0
· simp [h, show w = 0 by omega]
· rw [getLsbD_add (x := x)]
simp [show w > 0 by omega]
omega
/-- Adding a bitvector to its own complement yields the all ones bitpattern -/
@[simp] theorem add_not_self (x : BitVec w) : x + ~~~x = allOnes w := by
rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (allOnes w)]
@@ -307,26 +292,6 @@ theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
simp_all [hx]
· by_cases hx : x.getLsbD i <;> simp_all [hx]
/-! ### Sub-/
theorem getLsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
(x - y).getLsbD i
= (x.getLsbD i ^^ ((~~~y + 1#w).getLsbD i ^^ carry i x (~~~y + 1#w) false)) := by
rw [sub_toAdd, BitVec.neg_eq_not_add, getLsbD_add]
omega
theorem getMsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
(x - y).getMsbD i =
(x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false)) := by
rw [sub_toAdd, neg_eq_not_add, getMsbD_add]
· rfl
· omega
theorem msb_sub {x y: BitVec w} :
(x - y).msb
= (x.msb ^^ ((~~~y + 1#w).msb ^^ carry (w - 1 - 0) x (~~~y + 1#w) false)) := by
simp [sub_toAdd, BitVec.neg_eq_not_add, msb_add]
/-! ### Negation -/
theorem bit_not_testBit (x : BitVec w) (i : Fin w) :

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
@@ -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) :=
@@ -2148,8 +2113,6 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
/-! ### 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]
@@ -2186,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
@@ -2383,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`. -/
@@ -2444,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`. -/
@@ -2739,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
@@ -3244,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

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.Data.UInt.BasicAux
import Init.Data.UInt.Basic
/-- Determines if the given integer is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).
@@ -42,10 +42,8 @@ theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by
theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
match h with
| Or.inl h =>
Or.inl (UInt32.ofNat'_lt_of_lt _ (by decide) h)
| Or.inr h₁, h₂ =>
Or.inr UInt32.lt_ofNat'_of_lt _ (by decide) h₁, UInt32.ofNat'_lt_of_lt _ (by decide) h₂
| Or.inl h => Or.inl h
| Or.inr h₁, h₂ => Or.inr h₁, h
theorem isValidChar_zero : isValidChar 0 :=
Or.inl (by decide)
@@ -59,7 +57,7 @@ theorem isValidChar_zero : isValidChar 0 :=
c.val.toUInt8
/-- The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other. -/
def ofUInt8 (n : UInt8) : Char := n.toUInt32, .inl (Nat.lt_trans n.toBitVec.isLt (by decide))
def ofUInt8 (n : UInt8) : Char := n.toUInt32, .inl (Nat.lt_trans n.1.2 (by decide))
instance : Inhabited Char where
default := 'A'

View File

@@ -51,9 +51,6 @@ instance : Hashable USize where
instance : Hashable (Fin n) where
hash v := v.val.toUInt64
instance : Hashable Char where
hash c := c.val.toUInt64
instance : Hashable Int where
hash
| Int.ofNat n => UInt64.ofNat (2 * n)

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]

View File

@@ -639,16 +639,14 @@ and simplifies these to the function directly taking the value.
| nil => simp
| cons a l ih => simp [ih, hf, filterMap_cons]
@[simp] theorem flatMap_subtype {p : α Prop} {l : List { x // p x }}
@[simp] theorem bind_subtype {p : α Prop} {l : List { x // p x }}
{f : { x // p x } List β} {g : α List β} {hf : x h, f x, h = g x} :
(l.flatMap f) = l.unattach.flatMap g := by
(l.bind f) = l.unattach.bind g := by
unfold unattach
induction l with
| nil => simp
| cons a l ih => simp [ih, hf]
@[deprecated flatMap_subtype (since := "2024-10-16")] abbrev bind_subtype := @flatMap_subtype
@[simp] theorem unattach_filter {p : α Prop} {l : List { x // p x }}
{f : { x // p x } Bool} {g : α Bool} {hf : x h, f x, h = g x} :
(l.filter f).unattach = l.unattach.filter g := by

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,7 +38,7 @@ 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`.
@@ -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
@@ -563,38 +558,28 @@ def flatten : List (List α) → List α
@[deprecated flatten (since := "2024-10-14"), inherit_doc flatten] abbrev join := @flatten
/-! ### singleton -/
/-! ### pure -/
/-- `singleton x = [x]`. -/
@[inline] protected def singleton {α : Type u} (a : α) : List α := [a]
/-- `pure x = [x]` is the `pure` operation of the list monad. -/
@[inline] protected def pure {α : Type u} (a : α) : List α := [a]
set_option linter.missingDocs false in
@[deprecated singleton (since := "2024-10-16")] protected abbrev pure := @singleton
/-! ### flatMap -/
/-! ### bind -/
/--
`flatMap xs f` applies `f` to each element of `xs`
`bind xs f` is the bind operation of the list monad. It applies `f` to each element of `xs`
to get a list of lists, and then concatenates them all together.
* `[2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]`
-/
@[inline] def flatMap {α : Type u} {β : Type v} (a : List α) (b : α List β) : List β := flatten (map b a)
@[inline] protected def bind {α : Type u} {β : Type v} (a : List α) (b : α List β) : List β := flatten (map b a)
@[simp] theorem flatMap_nil (f : α List β) : List.flatMap [] f = [] := by simp [flatten, List.flatMap]
@[simp] theorem flatMap_cons x xs (f : α List β) :
List.flatMap (x :: xs) f = f x ++ List.flatMap xs f := by simp [flatten, List.flatMap]
@[simp] theorem bind_nil (f : α List β) : List.bind [] f = [] := by simp [flatten, List.bind]
@[simp] theorem bind_cons x xs (f : α List β) :
List.bind (x :: xs) f = f x ++ List.bind xs f := by simp [flatten, List.bind]
set_option linter.missingDocs false in
@[deprecated flatMap (since := "2024-10-16")] abbrev bind := @flatMap
@[deprecated bind_nil (since := "2024-06-15")] abbrev nil_bind := @bind_nil
set_option linter.missingDocs false in
@[deprecated flatMap_nil (since := "2024-10-16")] abbrev nil_flatMap := @flatMap_nil
set_option linter.missingDocs false in
@[deprecated flatMap_cons (since := "2024-10-16")] abbrev cons_flatMap := @flatMap_cons
set_option linter.missingDocs false in
@[deprecated flatMap_nil (since := "2024-06-15")] abbrev nil_bind := @flatMap_nil
set_option linter.missingDocs false in
@[deprecated flatMap_cons (since := "2024-06-15")] abbrev cons_bind := @flatMap_cons
@[deprecated bind_cons (since := "2024-06-15")] abbrev cons_bind := @bind_cons
/-! ### replicate -/
@@ -1119,35 +1104,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 +1408,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 -/

View File

@@ -232,8 +232,7 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
apply Nat.lt_trans ih
simp_arith
theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α α Prop)]
{as bs : List α} (h₁ : as bs) (h₂ : bs as) : as = bs :=
theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α α Prop)] {as bs : List α} (h₁ : as bs) (h₂ : bs as) : as = bs :=
match as, bs with
| [], [] => rfl
| [], _::_ => False.elim <| h₂ (List.lt.nil ..)
@@ -249,8 +248,7 @@ theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : αα → Prop)]
have : a = b := s.antisymm hab hba
simp [this, ih]
instance [LT α] [Std.Antisymm (¬ · < · : α α Prop)] :
Std.Antisymm (· · : List α List α Prop) where
instance [LT α] [Antisymm (¬ · < · : α α Prop)] : Antisymm (· · : List α List α Prop) where
antisymm h₁ h₂ := le_antisymm h₁ h₂
end List

View File

@@ -254,8 +254,6 @@ instance : ForIn m (List α) α where
instance : ForIn' m (List α) α inferInstance where
forIn' := List.forIn'
@[simp] theorem forIn'_eq_forIn' [Monad m] : @List.forIn' α β m _ = forIn' := 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

View File

@@ -378,18 +378,14 @@ theorem find?_flatten_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
· exact h₁ l ml a m
· exact h₂ a m
@[simp] theorem find?_flatMap (xs : List α) (f : α List β) (p : β Bool) :
(xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
simp [flatMap_def, findSome?_map]; rfl
@[simp] theorem find?_bind (xs : List α) (f : α List β) (p : β Bool) :
(xs.bind f).find? p = xs.findSome? (fun x => (f x).find? p) := by
simp [bind_def, findSome?_map]; rfl
@[deprecated find?_flatMap (since := "2024-10-16")] abbrev find?_bind := @find?_flatMap
theorem find?_flatMap_eq_none {xs : List α} {f : α List β} {p : β Bool} :
(xs.flatMap f).find? p = none x xs, y f x, !p y := by
theorem find?_bind_eq_none {xs : List α} {f : α List β} {p : β Bool} :
(xs.bind f).find? p = none x xs, y f x, !p y := by
simp
@[deprecated find?_flatMap_eq_none (since := "2024-10-16")] abbrev find?_bind_eq_none := @find?_flatMap_eq_none
theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
cases n
· simp
@@ -595,14 +591,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

@@ -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`.
-/
@@ -93,29 +93,29 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
/-! ### flatMap -/
/-! ### bind -/
/-- Tail recursive version of `List.flatMap`. -/
@[inline] def flatMapTR (as : List α) (f : α List β) : List β := go as #[] where
/-- Auxiliary for `flatMap`: `flatMap.go f as = acc.toList ++ bind f as` -/
/-- Tail recursive version of `List.bind`. -/
@[inline] def bindTR (as : List α) (f : α List β) : List β := go as #[] where
/-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/
@[specialize] go : List α Array β List β
| [], acc => acc.toList
| x::xs, acc => go xs (acc ++ f x)
@[csimp] theorem flatMap_eq_flatMapTR : @List.flatMap = @flatMapTR := by
@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
funext α β as f
let rec go : as acc, flatMapTR.go f as acc = acc.toList ++ as.flatMap f
| [], acc => by simp [flatMapTR.go, flatMap]
| x::xs, acc => by simp [flatMapTR.go, flatMap, go xs]
let rec go : as acc, bindTR.go f as acc = acc.toList ++ as.bind f
| [], acc => by simp [bindTR.go, bind]
| x::xs, acc => by simp [bindTR.go, bind, go xs]
exact (go as #[]).symm
/-! ### flatten -/
/-- Tail recursive version of `List.flatten`. -/
@[inline] def flattenTR (l : List (List α)) : List α := flatMapTR l id
@[inline] def flattenTR (l : List (List α)) : List α := bindTR l id
@[csimp] theorem flatten_eq_flattenTR : @flatten = @flattenTR := by
funext α l; rw [ List.flatMap_id, List.flatMap_eq_flatMapTR]; rfl
funext α l; rw [ List.bind_id, List.bind_eq_bindTR]; rfl
/-! ## Sublists -/
@@ -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 -/
@@ -2105,8 +2097,8 @@ theorem forall_mem_flatten {p : α → Prop} {L : List (List α)} :
simp only [mem_flatten, forall_exists_index, and_imp]
constructor <;> (intros; solve_by_elim)
theorem flatten_eq_flatMap {L : List (List α)} : flatten L = L.flatMap id := by
induction L <;> simp [List.flatMap]
theorem flatten_eq_bind {L : List (List α)} : flatten L = L.bind id := by
induction L <;> simp [List.bind]
theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun l => l.head? := by
induction L with
@@ -2223,86 +2215,86 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
obtain rfl, h := append_inj h₁ h₂
exact rfl, h, h₃
/-! ### flatMap -/
/-! ### bind -/
theorem flatMap_def (l : List α) (f : α List β) : l.flatMap f = flatten (map f l) := by rfl
theorem bind_def (l : List α) (f : α List β) : l.bind f = flatten (map f l) := by rfl
@[simp] theorem flatMap_id (l : List (List α)) : List.flatMap l id = l.flatten := by simp [flatMap_def]
@[simp] theorem bind_id (l : List (List α)) : List.bind l id = l.flatten := by simp [bind_def]
@[simp] theorem mem_flatMap {f : α List β} {b} {l : List α} : b l.flatMap f a, a l b f a := by
simp [flatMap_def, mem_flatten]
@[simp] theorem mem_bind {f : α List β} {b} {l : List α} : b l.bind f a, a l b f a := by
simp [bind_def, mem_flatten]
exact fun _, a, h₁, rfl, h₂ => a, h₁, h₂, fun a, h₁, h₂ => _, a, h₁, rfl, h₂
theorem exists_of_mem_flatMap {b : β} {l : List α} {f : α List β} :
b l.flatMap f a, a l b f a := mem_flatMap.1
theorem exists_of_mem_bind {b : β} {l : List α} {f : α List β} :
b l.bind f a, a l b f a := mem_bind.1
theorem mem_flatMap_of_mem {b : β} {l : List α} {f : α List β} {a} (al : a l) (h : b f a) :
b l.flatMap f := mem_flatMap.2 a, al, h
theorem mem_bind_of_mem {b : β} {l : List α} {f : α List β} {a} (al : a l) (h : b f a) :
b l.bind f := mem_bind.2 a, al, h
@[simp]
theorem flatMap_eq_nil_iff {l : List α} {f : α List β} : List.flatMap l f = [] x l, f x = [] :=
theorem bind_eq_nil_iff {l : List α} {f : α List β} : List.bind l f = [] x l, f x = [] :=
flatten_eq_nil_iff.trans <| by
simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
@[deprecated flatMap_eq_nil_iff (since := "2024-09-05")] abbrev bind_eq_nil := @flatMap_eq_nil_iff
@[deprecated bind_eq_nil_iff (since := "2024-09-05")] abbrev bind_eq_nil := @bind_eq_nil_iff
theorem forall_mem_flatMap {p : β Prop} {l : List α} {f : α List β} :
( (x) (_ : x l.flatMap f), p x) (a) (_ : a l) (b) (_ : b f a), p b := by
simp only [mem_flatMap, forall_exists_index, and_imp]
theorem forall_mem_bind {p : β Prop} {l : List α} {f : α List β} :
( (x) (_ : x l.bind f), p x) (a) (_ : a l) (b) (_ : b f a), p b := by
simp only [mem_bind, forall_exists_index, and_imp]
constructor <;> (intros; solve_by_elim)
theorem flatMap_singleton (f : α List β) (x : α) : [x].flatMap f = f x :=
theorem bind_singleton (f : α List β) (x : α) : [x].bind f = f x :=
append_nil (f x)
@[simp] theorem flatMap_singleton' (l : List α) : (l.flatMap fun x => [x]) = l := by
@[simp] theorem bind_singleton' (l : List α) : (l.bind fun x => [x]) = l := by
induction l <;> simp [*]
theorem head?_flatMap {l : List α} {f : α List β} :
(l.flatMap f).head? = l.findSome? fun a => (f a).head? := by
theorem head?_bind {l : List α} {f : α List β} :
(l.bind f).head? = l.findSome? fun a => (f a).head? := by
induction l with
| nil => rfl
| cons =>
simp only [findSome?_cons]
split <;> simp_all
@[simp] theorem flatMap_append (xs ys : List α) (f : α List β) :
(xs ++ ys).flatMap f = xs.flatMap f ++ ys.flatMap f := by
induction xs; {rfl}; simp_all [flatMap_cons, append_assoc]
@[simp] theorem bind_append (xs ys : List α) (f : α List β) :
(xs ++ ys).bind f = xs.bind f ++ ys.bind f := by
induction xs; {rfl}; simp_all [bind_cons, append_assoc]
@[deprecated flatMap_append (since := "2024-07-24")] abbrev append_bind := @flatMap_append
@[deprecated bind_append (since := "2024-07-24")] abbrev append_bind := @bind_append
theorem flatMap_assoc {α β} (l : List α) (f : α List β) (g : β List γ) :
(l.flatMap f).flatMap g = l.flatMap fun x => (f x).flatMap g := by
theorem bind_assoc {α β} (l : List α) (f : α List β) (g : β List γ) :
(l.bind f).bind g = l.bind fun x => (f x).bind g := by
induction l <;> simp [*]
theorem map_flatMap (f : β γ) (g : α List β) :
l : List α, (l.flatMap g).map f = l.flatMap fun a => (g a).map f
theorem map_bind (f : β γ) (g : α List β) :
l : List α, (l.bind g).map f = l.bind fun a => (g a).map f
| [] => rfl
| a::l => by simp only [flatMap_cons, map_append, map_flatMap _ _ l]
| a::l => by simp only [bind_cons, map_append, map_bind _ _ l]
theorem flatMap_map (f : α β) (g : β List γ) (l : List α) :
(map f l).flatMap g = l.flatMap (fun a => g (f a)) := by
induction l <;> simp [flatMap_cons, *]
theorem bind_map (f : α β) (g : β List γ) (l : List α) :
(map f l).bind g = l.bind (fun a => g (f a)) := by
induction l <;> simp [bind_cons, *]
theorem map_eq_flatMap {α β} (f : α β) (l : List α) : map f l = l.flatMap fun x => [f x] := by
theorem map_eq_bind {α β} (f : α β) (l : List α) : map f l = l.bind fun x => [f x] := by
simp only [ map_singleton]
rw [ flatMap_singleton' l, map_flatMap, flatMap_singleton']
rw [ bind_singleton' l, map_bind, bind_singleton']
theorem filterMap_flatMap {β γ} (l : List α) (g : α List β) (f : β Option γ) :
(l.flatMap g).filterMap f = l.flatMap fun a => (g a).filterMap f := by
theorem filterMap_bind {β γ} (l : List α) (g : α List β) (f : β Option γ) :
(l.bind g).filterMap f = l.bind fun a => (g a).filterMap f := by
induction l <;> simp [*]
theorem filter_flatMap (l : List α) (g : α List β) (f : β Bool) :
(l.flatMap g).filter f = l.flatMap fun a => (g a).filter f := by
theorem filter_bind (l : List α) (g : α List β) (f : β Bool) :
(l.bind g).filter f = l.bind fun a => (g a).filter f := by
induction l <;> simp [*]
theorem flatMap_eq_foldl (f : α List β) (l : List α) :
l.flatMap f = l.foldl (fun acc a => acc ++ f a) [] := by
suffices l', l' ++ l.flatMap f = l.foldl (fun acc a => acc ++ f a) l' by simpa using this []
theorem bind_eq_foldl (f : α List β) (l : List α) :
l.bind f = l.foldl (fun acc a => acc ++ f a) [] := by
suffices l', l' ++ l.bind f = l.foldl (fun acc a => acc ++ f a) l' by simpa using this []
intro l'
induction l generalizing l'
· simp
· next ih => rw [flatMap_cons, append_assoc, ih, foldl_cons]
· next ih => rw [bind_cons, append_assoc, ih, foldl_cons]
/-! ### replicate -/
@@ -2492,10 +2484,10 @@ theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
simp only [replicate_succ, flatten_cons, ih, append_replicate_replicate, replicate_inj, or_true,
and_true, add_one_mul, Nat.add_comm]
theorem flatMap_replicate {β} (f : α List β) : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
theorem bind_replicate {β} (f : α List β) : (replicate n a).bind f = (replicate n (f a)).flatten := by
induction n with
| zero => simp
| succ n ih => simp only [replicate_succ, flatMap_cons, ih, flatten_cons]
| succ n ih => simp only [replicate_succ, bind_cons, ih, flatten_cons]
@[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
cases n <;> simp [replicate_succ]
@@ -2680,10 +2672,10 @@ theorem flatten_reverse (L : List (List α)) :
L.reverse.flatten = (L.map reverse).flatten.reverse := by
induction L <;> simp_all
theorem reverse_flatMap {β} (l : List α) (f : α List β) : (l.flatMap f).reverse = l.reverse.flatMap (reverse f) := by
theorem reverse_bind {β} (l : List α) (f : α List β) : (l.bind f).reverse = l.reverse.bind (reverse f) := by
induction l <;> simp_all
theorem flatMap_reverse {β} (l : List α) (f : α List β) : (l.reverse.flatMap f) = (l.flatMap (reverse f)).reverse := by
theorem bind_reverse {β} (l : List α) (f : α List β) : (l.reverse.bind f) = (l.bind (reverse f)).reverse := by
induction l <;> simp_all
@[simp] theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
@@ -2791,15 +2783,15 @@ theorem getLast_filterMap_of_eq_some {f : α → Option β} {l : List α} {w : l
rw [head_filterMap_of_eq_some (by simp_all)]
simp_all
theorem getLast?_flatMap {L : List α} {f : α List β} :
(L.flatMap f).getLast? = L.reverse.findSome? fun a => (f a).getLast? := by
simp only [ head?_reverse, reverse_flatMap]
rw [head?_flatMap]
theorem getLast?_bind {L : List α} {f : α List β} :
(L.bind f).getLast? = L.reverse.findSome? fun a => (f a).getLast? := by
simp only [ head?_reverse, reverse_bind]
rw [head?_bind]
rfl
theorem getLast?_flatten {L : List (List α)} :
(flatten L).getLast? = L.reverse.findSome? fun l => l.getLast? := by
simp [ flatMap_id, getLast?_flatMap]
simp [ bind_id, getLast?_bind]
theorem getLast?_replicate (a : α) (n : Nat) : (replicate n a).getLast? = if n = 0 then none else some a := by
simp only [ head?_reverse, reverse_replicate, head?_replicate]
@@ -3308,12 +3300,12 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
@[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
@[simp] theorem any_flatMap {l : List α} {f : α List β} :
(l.flatMap f).any p = l.any fun a => (f a).any p := by
@[simp] theorem any_bind {l : List α} {f : α List β} :
(l.bind f).any p = l.any fun a => (f a).any p := by
induction l <;> simp_all
@[simp] theorem all_flatMap {l : List α} {f : α List β} :
(l.flatMap f).all p = l.all fun a => (f a).all p := by
@[simp] theorem all_bind {l : List α} {f : α List β} :
(l.bind f).all p = l.all fun a => (f a).all p := by
induction l <;> simp_all
@[simp] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
@@ -3353,7 +3345,7 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
@[deprecated exists_of_mem_flatten (since := "2024-10-14")] abbrev exists_of_mem_join := @exists_of_mem_flatten
@[deprecated mem_flatten_of_mem (since := "2024-10-14")] abbrev mem_join_of_mem := @mem_flatten_of_mem
@[deprecated forall_mem_flatten (since := "2024-10-14")] abbrev forall_mem_join := @forall_mem_flatten
@[deprecated flatten_eq_flatMap (since := "2024-10-14")] abbrev join_eq_bind := @flatten_eq_flatMap
@[deprecated flatten_eq_bind (since := "2024-10-14")] abbrev join_eq_bind := @flatten_eq_bind
@[deprecated head?_flatten (since := "2024-10-14")] abbrev head?_join := @head?_flatten
@[deprecated foldl_flatten (since := "2024-10-14")] abbrev foldl_join := @foldl_flatten
@[deprecated foldr_flatten (since := "2024-10-14")] abbrev foldr_join := @foldr_flatten
@@ -3380,30 +3372,5 @@ theorem join_map_filter (p : α → Bool) (l : List (List α)) :
@[deprecated reverse_flatten (since := "2024-10-14")] abbrev reverse_join := @reverse_flatten
@[deprecated flatten_reverse (since := "2024-10-14")] abbrev join_reverse := @flatten_reverse
@[deprecated getLast?_flatten (since := "2024-10-14")] abbrev getLast?_join := @getLast?_flatten
@[deprecated flatten_eq_flatMap (since := "2024-10-16")] abbrev flatten_eq_bind := @flatten_eq_flatMap
@[deprecated flatMap_def (since := "2024-10-16")] abbrev bind_def := @flatMap_def
@[deprecated flatMap_id (since := "2024-10-16")] abbrev bind_id := @flatMap_id
@[deprecated mem_flatMap (since := "2024-10-16")] abbrev mem_bind := @mem_flatMap
@[deprecated exists_of_mem_flatMap (since := "2024-10-16")] abbrev exists_of_mem_bind := @exists_of_mem_flatMap
@[deprecated mem_flatMap_of_mem (since := "2024-10-16")] abbrev mem_bind_of_mem := @mem_flatMap_of_mem
@[deprecated flatMap_eq_nil_iff (since := "2024-10-16")] abbrev bind_eq_nil_iff := @flatMap_eq_nil_iff
@[deprecated forall_mem_flatMap (since := "2024-10-16")] abbrev forall_mem_bind := @forall_mem_flatMap
@[deprecated flatMap_singleton (since := "2024-10-16")] abbrev bind_singleton := @flatMap_singleton
@[deprecated flatMap_singleton' (since := "2024-10-16")] abbrev bind_singleton' := @flatMap_singleton'
@[deprecated head?_flatMap (since := "2024-10-16")] abbrev head_bind := @head?_flatMap
@[deprecated flatMap_append (since := "2024-10-16")] abbrev bind_append := @flatMap_append
@[deprecated flatMap_assoc (since := "2024-10-16")] abbrev bind_assoc := @flatMap_assoc
@[deprecated map_flatMap (since := "2024-10-16")] abbrev map_bind := @map_flatMap
@[deprecated flatMap_map (since := "2024-10-16")] abbrev bind_map := @flatMap_map
@[deprecated map_eq_flatMap (since := "2024-10-16")] abbrev map_eq_bind := @map_eq_flatMap
@[deprecated filterMap_flatMap (since := "2024-10-16")] abbrev filterMap_bind := @filterMap_flatMap
@[deprecated filter_flatMap (since := "2024-10-16")] abbrev filter_bind := @filter_flatMap
@[deprecated flatMap_eq_foldl (since := "2024-10-16")] abbrev bind_eq_foldl := @flatMap_eq_foldl
@[deprecated flatMap_replicate (since := "2024-10-16")] abbrev bind_replicate := @flatMap_replicate
@[deprecated reverse_flatMap (since := "2024-10-16")] abbrev reverse_bind := @reverse_flatMap
@[deprecated flatMap_reverse (since := "2024-10-16")] abbrev bind_reverse := @flatMap_reverse
@[deprecated getLast?_flatMap (since := "2024-10-16")] abbrev getLast?_bind := @getLast?_flatMap
@[deprecated any_flatMap (since := "2024-10-16")] abbrev any_bind := @any_flatMap
@[deprecated all_flatMap (since := "2024-10-16")] abbrev all_bind := @all_flatMap
end List

View File

@@ -75,7 +75,7 @@ theorem le_min?_iff [Min α] [LE α]
-- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
-- and `le_min_iff`.
theorem min?_eq_some_iff [Min α] [LE α] [anti : Std.Antisymm ((· : α) ·)]
theorem min?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ·)]
(le_refl : a : α, a a)
(min_eq_or : a b : α, min a b = a min a b = b)
(le_min_iff : a b c : α, a min b c a b a c) {xs : List α} :
@@ -146,7 +146,7 @@ theorem max?_le_iff [Max α] [LE α]
-- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
-- and `le_min_iff`.
theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm ((· : α) ·)]
theorem max?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ·)]
(le_refl : a : α, a a)
(max_eq_or : a b : α, max a b = a max a b = b)
(max_le_iff : a b c : α, max b c a b a c a) {xs : List α} :

View File

@@ -87,68 +87,6 @@ theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β)
(l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by
induction l₁ <;> simp [*]
/-! ### forIn' -/
@[simp] theorem forIn'_nil [Monad m] (f : (a : α) a [] β m (ForInStep β)) (b : β) : forIn' [] b f = pure b :=
rfl
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
@[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
/-! ### allM -/
theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α m Bool) (as : List α) :
@@ -161,14 +99,4 @@ 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

@@ -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

@@ -173,12 +173,10 @@ theorem pairwise_flatten {L : List (List α)} :
@[deprecated pairwise_flatten (since := "2024-10-14")] abbrev pairwise_join := @pairwise_flatten
theorem pairwise_flatMap {R : β β Prop} {l : List α} {f : α List β} :
List.Pairwise R (l.flatMap f)
theorem pairwise_bind {R : β β Prop} {l : List α} {f : α List β} :
List.Pairwise R (l.bind f)
( a l, Pairwise R (f a)) Pairwise (fun a₁ a₂ => x f a₁, y f a₂, R x y) l := by
simp [List.flatMap, pairwise_flatten, pairwise_map]
@[deprecated pairwise_flatMap (since := "2024-10-14")] abbrev pairwise_bind := @pairwise_flatMap
simp [List.bind, pairwise_flatten, pairwise_map]
theorem pairwise_reverse {l : List α} :
l.reverse.Pairwise R l.Pairwise (fun a b => R b a) := by

View File

@@ -470,11 +470,9 @@ theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatt
@[deprecated Perm.flatten (since := "2024-10-14")] abbrev Perm.join := @Perm.flatten
theorem Perm.flatMap_right {l₁ l₂ : List α} (f : α List β) (p : l₁ ~ l₂) : l₁.flatMap f ~ l₂.flatMap f :=
theorem Perm.bind_right {l₁ l₂ : List α} (f : α List β) (p : l₁ ~ l₂) : l₁.bind f ~ l₂.bind f :=
(p.map _).flatten
@[deprecated Perm.flatMap_right (since := "2024-10-16")] abbrev Perm.bind_right := @Perm.flatMap_right
theorem Perm.eraseP (f : α Bool) {l₁ l₂ : List α}
(H : Pairwise (fun a b => f a f b False) l₁) (p : l₁ ~ l₂) : eraseP f l₁ ~ eraseP f l₂ := by
induction p with

View File

@@ -131,7 +131,7 @@ theorem or_exists_add_one : p 0 (Exists fun n => p (n + 1)) ↔ Exists p :=
@[simp] theorem blt_eq : (Nat.blt x y = true) = (x < y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
instance : LawfulBEq Nat where
eq_of_beq h := by simpa using h
eq_of_beq h := Nat.eq_of_beq_eq_true h
rfl := by simp [BEq.beq]
theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp
@@ -490,10 +490,10 @@ protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
(fun hle, hge => Nat.le_antisymm hle hge)
protected theorem eq_iff_le_and_ge : {a b : Nat}, a = b a b b a := @Nat.le_antisymm_iff
instance : Std.Antisymm ( . . : Nat Nat Prop) where
instance : Antisymm ( . . : Nat Nat Prop) where
antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂
instance : Std.Antisymm (¬ . < . : Nat Nat Prop) where
instance : Antisymm (¬ . < . : Nat Nat Prop) where
antisymm h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
protected theorem add_le_add_left {n m : Nat} (h : n m) (k : Nat) : k + n k + m :=
@@ -796,8 +796,6 @@ theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
| zero => cases h
| succ n => simp [Nat.pow_succ]
protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
Nat.ne_zero_iff_zero_lt.mpr (Nat.pos_pow_of_pos m (pos_of_neZero _))

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
@@ -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

@@ -8,6 +8,8 @@ import Init.Data.Nat.Linear
namespace Nat
protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
have : power * 2 = power + power := by simp_arith
rw [this, Nat.sub_add_eq]

View File

@@ -10,10 +10,8 @@ import Init.Data.Nat.Log2
/-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
Examples:
- `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
- `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`
Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
- `OfScientific.ofScientific 123 true 2` represents `1.23`
- `OfScientific.ofScientific 121 false 100` represents `121e100`
-/
class OfScientific (α : Type u) where
ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : α

View File

@@ -44,7 +44,7 @@ theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
simp
theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α Prop} {H : x o₁, P x} :
o₁.attachWith P H = o₂.attachWith P fun _ h => H _ (w h) := by
o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w h) := by
subst w
simp
@@ -128,12 +128,12 @@ theorem attach_map {o : Option α} (f : α → β) :
cases o <;> simp
theorem attachWith_map {o : Option α} (f : α β) {P : β Prop} {H : (b : β), b o.map f P b} :
(o.map f).attachWith P H = (o.attachWith (P f) (fun _ h => H _ (mem_map_of_mem f h))).map
(o.map f).attachWith P H = (o.attachWith (P f) (fun a h => H _ (mem_map_of_mem f h))).map
fun x, h => f x, h := by
cases o <;> simp
theorem map_attach {o : Option α} (f : { x // x o } β) :
o.attach.map f = o.pmap (fun a (h : a o) => f a, h) (fun _ h => h) := by
o.attach.map f = o.pmap (fun a (h : a o) => f a, h) (fun a h => h) := by
cases o <;> simp
theorem map_attachWith {o : Option α} {P : α Prop} {H : (a : α), a o P a}

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

@@ -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

@@ -7,8 +7,6 @@ prelude
import Init.SimpLemmas
import Init.NotationExtra
namespace Prod
instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
eq_of_beq {a b} (h : a.1 == b.1 && a.2 == b.2) := by
cases a; cases b
@@ -16,65 +14,9 @@ instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β)
rfl {a} := by cases a; simp [BEq.beq, LawfulBEq.rfl]
@[simp]
protected theorem «forall» {p : α × β Prop} : ( x, p x) a b, p (a, b) :=
protected theorem Prod.forall {p : α × β Prop} : ( x, p x) a b, p (a, b) :=
fun h a b h (a, b), fun h a, b h a b
@[simp]
protected theorem «exists» {p : α × β Prop} : ( x, p x) a b, p (a, b) :=
protected theorem Prod.exists {p : α × β Prop} : ( x, p x) a b, p (a, b) :=
fun a, b, h a, b, h, fun a, b, h a, b, h
@[simp] theorem map_id : Prod.map (@id α) (@id β) = id := rfl
@[simp] theorem map_id' : Prod.map (fun a : α => a) (fun b : β => b) = fun x x := rfl
/--
Composing a `Prod.map` with another `Prod.map` is equal to
a single `Prod.map` of composed functions.
-/
theorem map_comp_map (f : α β) (f' : γ δ) (g : β ε) (g' : δ ζ) :
Prod.map g g' Prod.map f f' = Prod.map (g f) (g' f') :=
rfl
/--
Composing a `Prod.map` with another `Prod.map` is equal to
a single `Prod.map` of composed functions, fully applied.
-/
theorem map_map (f : α β) (f' : γ δ) (g : β ε) (g' : δ ζ) (x : α × γ) :
Prod.map g g' (Prod.map f f' x) = Prod.map (g f) (g' f') x :=
rfl
/-- Swap the factors of a product. `swap (a, b) = (b, a)` -/
def swap : α × β β × α := fun p => (p.2, p.1)
@[simp]
theorem swap_swap : x : α × β, swap (swap x) = x
| _, _ => rfl
@[simp]
theorem fst_swap {p : α × β} : (swap p).1 = p.2 :=
rfl
@[simp]
theorem snd_swap {p : α × β} : (swap p).2 = p.1 :=
rfl
@[simp]
theorem swap_prod_mk {a : α} {b : β} : swap (a, b) = (b, a) :=
rfl
@[simp]
theorem swap_swap_eq : swap swap = @id (α × β) :=
funext swap_swap
@[simp]
theorem swap_inj {p q : α × β} : swap p = swap q p = q := by
cases p; cases q; simp [and_comm]
/--
For two functions `f` and `g`, the composition of `Prod.map f g` with `Prod.swap`
is equal to the composition of `Prod.swap` with `Prod.map g f`.
-/
theorem map_comp_swap (f : α β) (g : γ δ) :
Prod.map f g Prod.swap = Prod.swap Prod.map g f := rfl
end Prod

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.Basic
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
@@ -1147,23 +1148,23 @@ namespace String
/--
If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
-/
def dropPrefix? (s : String) (pre : String) : Option Substring :=
s.toSubstring.dropPrefix? pre.toSubstring
def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
s.toSubstring.dropPrefix? pre
/--
If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
-/
def dropSuffix? (s : String) (suff : String) : Option Substring :=
s.toSubstring.dropSuffix? suff.toSubstring
def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
s.toSubstring.dropSuffix? suff
/-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
or otherwise return `s`. -/
def stripPrefix (s : String) (pre : String) : String :=
def stripPrefix (s : String) (pre : Substring) : String :=
s.dropPrefix? pre |>.map Substring.toString |>.getD s
/-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
or otherwise return `s`. -/
def stripSuffix (s : String) (suff : String) : String :=
def stripSuffix (s : String) (suff : Substring) : String :=
s.dropSuffix? suff |>.map Substring.toString |>.getD s
end String

View File

@@ -5,7 +5,6 @@ Author: Leonardo de Moura
-/
prelude
import Init.Data.ByteArray
import Init.Data.UInt.Lemmas
namespace String
@@ -21,14 +20,14 @@ def toNat! (s : String) : Nat :=
def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
let c a[i]?
if c &&& 0x80 == 0 then
some c.toUInt32, .inl (Nat.lt_trans c.toBitVec.isLt (by decide))
some c.toUInt32, .inl (Nat.lt_trans c.1.2 (by decide))
else if c &&& 0xe0 == 0xc0 then
let c1 a[i+1]?
guard (c1 &&& 0xc0 == 0x80)
let r := ((c &&& 0x1f).toUInt32 <<< 6) ||| (c1 &&& 0x3f).toUInt32
guard (0x80 r)
-- TODO: Prove h from the definition of r once we have the necessary lemmas
if h : r < 0xd800 then some r, .inl (UInt32.toNat_lt_of_lt (by decide) h) else none
if h : r < 0xd800 then some r, .inl h else none
else if c &&& 0xf0 == 0xe0 then
let c1 a[i+1]?
let c2 a[i+2]?
@@ -39,14 +38,7 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
(c2 &&& 0x3f).toUInt32
guard (0x800 r)
-- TODO: Prove `r < 0x110000` from the definition of r once we have the necessary lemmas
if h : r < 0xd800 0xdfff < r r < 0x110000 then
have :=
match h with
| .inl h => Or.inl (UInt32.toNat_lt_of_lt (by decide) h)
| .inr h => Or.inr UInt32.lt_toNat_of_lt (by decide) h.left, UInt32.toNat_lt_of_lt (by decide) h.right
some r, this
else
none
if h : r < 0xd800 0xdfff < r r < 0x110000 then some r, h else none
else if c &&& 0xf8 == 0xf0 then
let c1 a[i+1]?
let c2 a[i+2]?
@@ -58,7 +50,7 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
((c2 &&& 0x3f).toUInt32 <<< 6) |||
(c3 &&& 0x3f).toUInt32
if h : 0x10000 r r < 0x110000 then
some r, .inr Nat.lt_of_lt_of_le (by decide) (UInt32.le_toNat_of_le (by decide) h.left), UInt32.toNat_lt_of_lt (by decide) h.right
some r, .inr Nat.lt_of_lt_of_le (by decide) h.1, h.2
else none
else
none
@@ -125,10 +117,10 @@ def utf8EncodeChar (c : Char) : List UInt8 :=
/-- Converts the given `String` to a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded byte array. -/
@[extern "lean_string_to_utf8"]
def toUTF8 (a : @& String) : ByteArray :=
a.data.flatMap utf8EncodeChar
a.data.bind utf8EncodeChar
@[simp] theorem size_toUTF8 (s : String) : s.toUTF8.size = s.utf8ByteSize := by
simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.flatMap]
simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.bind]
induction s.data <;> simp [List.map, List.flatten, utf8ByteSize.go, Nat.add_comm, *]
/-- Accesses a byte in the UTF-8 encoding of the `String`. O(1) -/

View File

@@ -4,5 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Yury G. Kudryashov
-/
prelude
import Init.Data.Sum.Basic
import Init.Data.Sum.Lemmas
import Init.Core
namespace Sum
deriving instance DecidableEq for Sum
deriving instance BEq for Sum
/-- Check if a sum is `inl` and if so, retrieve its contents. -/
def getLeft? : α β Option α
| inl a => some a
| inr _ => none
/-- Check if a sum is `inr` and if so, retrieve its contents. -/
def getRight? : α β Option β
| inr b => some b
| inl _ => none
end Sum

View File

@@ -1,178 +0,0 @@
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Yury G. Kudryashov
-/
prelude
import Init.PropLemmas
/-!
# Disjoint union of types
This file defines basic operations on the the sum type `α ⊕ β`.
`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
## Main declarations
* `Sum.isLeft`: Returns whether `x : α ⊕ β` comes from the left component or not.
* `Sum.isRight`: Returns whether `x : α ⊕ β` comes from the right component or not.
* `Sum.getLeft`: Retrieves the left content of a `x : α ⊕ β` that is known to come from the left.
* `Sum.getRight`: Retrieves the right content of `x : α ⊕ β` that is known to come from the right.
* `Sum.getLeft?`: Retrieves the left content of `x : α ⊕ β` as an option type or returns `none`
if it's coming from the right.
* `Sum.getRight?`: Retrieves the right content of `x : α ⊕ β` as an option type or returns `none`
if it's coming from the left.
* `Sum.map`: Maps `α ⊕ β` to `γ ⊕ δ` component-wise.
* `Sum.elim`: Nondependent eliminator/induction principle for `α ⊕ β`.
* `Sum.swap`: Maps `α ⊕ β` to `β ⊕ α` by swapping components.
* `Sum.LiftRel`: The disjoint union of two relations.
* `Sum.Lex`: Lexicographic order on `α ⊕ β` induced by a relation on `α` and a relation on `β`.
## Further material
See `Batteries.Data.Sum.Lemmas` for theorems about these definitions.
## Notes
The definition of `Sum` takes values in `Type _`. This effectively forbids `Prop`- valued sum types.
To this effect, we have `PSum`, which takes value in `Sort _` and carries a more complicated
universe signature in consequence. The `Prop` version is `Or`.
-/
namespace Sum
deriving instance DecidableEq for Sum
deriving instance BEq for Sum
section get
/-- Check if a sum is `inl`. -/
def isLeft : α β Bool
| inl _ => true
| inr _ => false
/-- Check if a sum is `inr`. -/
def isRight : α β Bool
| inl _ => false
| inr _ => true
/-- Retrieve the contents from a sum known to be `inl`.-/
def getLeft : (ab : α β) ab.isLeft α
| inl a, _ => a
/-- Retrieve the contents from a sum known to be `inr`.-/
def getRight : (ab : α β) ab.isRight β
| inr b, _ => b
/-- Check if a sum is `inl` and if so, retrieve its contents. -/
def getLeft? : α β Option α
| inl a => some a
| inr _ => none
/-- Check if a sum is `inr` and if so, retrieve its contents. -/
def getRight? : α β Option β
| inr b => some b
| inl _ => none
@[simp] theorem isLeft_inl : (inl x : α β).isLeft = true := rfl
@[simp] theorem isLeft_inr : (inr x : α β).isLeft = false := rfl
@[simp] theorem isRight_inl : (inl x : α β).isRight = false := rfl
@[simp] theorem isRight_inr : (inr x : α β).isRight = true := rfl
@[simp] theorem getLeft_inl (h : (inl x : α β).isLeft) : (inl x).getLeft h = x := rfl
@[simp] theorem getRight_inr (h : (inr x : α β).isRight) : (inr x).getRight h = x := rfl
@[simp] theorem getLeft?_inl : (inl x : α β).getLeft? = some x := rfl
@[simp] theorem getLeft?_inr : (inr x : α β).getLeft? = none := rfl
@[simp] theorem getRight?_inl : (inl x : α β).getRight? = none := rfl
@[simp] theorem getRight?_inr : (inr x : α β).getRight? = some x := rfl
end get
/-- Define a function on `α ⊕ β` by giving separate definitions on `α` and `β`. -/
protected def elim {α β γ} (f : α γ) (g : β γ) : α β γ :=
fun x => Sum.casesOn x f g
@[simp] theorem elim_inl (f : α γ) (g : β γ) (x : α) :
Sum.elim f g (inl x) = f x := rfl
@[simp] theorem elim_inr (f : α γ) (g : β γ) (x : β) :
Sum.elim f g (inr x) = g x := rfl
/-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
protected def map (f : α α') (g : β β') : α β α' β' :=
Sum.elim (inl f) (inr g)
@[simp] theorem map_inl (f : α α') (g : β β') (x : α) : (inl x).map f g = inl (f x) := rfl
@[simp] theorem map_inr (f : α α') (g : β β') (x : β) : (inr x).map f g = inr (g x) := rfl
/-- Swap the factors of a sum type -/
def swap : α β β α := Sum.elim inr inl
@[simp] theorem swap_inl : swap (inl x : α β) = inr x := rfl
@[simp] theorem swap_inr : swap (inr x : α β) = inl x := rfl
section LiftRel
/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
`α ⊕ β` and `γ ⊕ δ`. -/
inductive LiftRel (r : α γ Prop) (s : β δ Prop) : α β γ δ Prop
/-- `inl a` and `inl c` are related via `LiftRel r s` if `a` and `c` are related via `r`. -/
| protected inl {a c} : r a c LiftRel r s (inl a) (inl c)
/-- `inr b` and `inr d` are related via `LiftRel r s` if `b` and `d` are related via `s`. -/
| protected inr {b d} : s b d LiftRel r s (inr b) (inr d)
@[simp] theorem liftRel_inl_inl : LiftRel r s (inl a) (inl c) r a c :=
fun h => by cases h; assumption, LiftRel.inl
@[simp] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun
@[simp] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun
@[simp] theorem liftRel_inr_inr : LiftRel r s (inr b) (inr d) s b d :=
fun h => by cases h; assumption, LiftRel.inr
instance {r : α γ Prop} {s : β δ Prop}
[ a c, Decidable (r a c)] [ b d, Decidable (s b d)] :
(ab : α β) (cd : γ δ), Decidable (LiftRel r s ab cd)
| inl _, inl _ => decidable_of_iff' _ liftRel_inl_inl
| inl _, inr _ => Decidable.isFalse not_liftRel_inl_inr
| inr _, inl _ => Decidable.isFalse not_liftRel_inr_inl
| inr _, inr _ => decidable_of_iff' _ liftRel_inr_inr
end LiftRel
section Lex
/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
respective order on `α` or `β`. -/
inductive Lex (r : α α Prop) (s : β β Prop) : α β α β Prop
/-- `inl a₁` and `inl a₂` are related via `Lex r s` if `a₁` and `a₂` are related via `r`. -/
| protected inl {a₁ a₂} (h : r a₁ a₂) : Lex r s (inl a₁) (inl a₂)
/-- `inr b₁` and `inr b₂` are related via `Lex r s` if `b₁` and `b₂` are related via `s`. -/
| protected inr {b₁ b₂} (h : s b₁ b₂) : Lex r s (inr b₁) (inr b₂)
/-- `inl a` and `inr b` are always related via `Lex r s`. -/
| sep (a b) : Lex r s (inl a) (inr b)
attribute [simp] Lex.sep
@[simp] theorem lex_inl_inl : Lex r s (inl a₁) (inl a₂) r a₁ a₂ :=
fun h => by cases h; assumption, Lex.inl
@[simp] theorem lex_inr_inr : Lex r s (inr b₁) (inr b₂) s b₁ b₂ :=
fun h => by cases h; assumption, Lex.inr
@[simp] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun
instance instDecidableRelSumLex [DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)
| inl _, inl _ => decidable_of_iff' _ lex_inl_inl
| inl _, inr _ => Decidable.isTrue (Lex.sep _ _)
| inr _, inl _ => Decidable.isFalse lex_inr_inl
| inr _, inr _ => decidable_of_iff' _ lex_inr_inr
end Lex
end Sum

View File

@@ -1,251 +0,0 @@
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Yury G. Kudryashov
-/
prelude
import Init.Data.Sum.Basic
import Init.Ext
/-!
# Disjoint union of types
Theorems about the definitions introduced in `Init.Data.Sum.Basic`.
-/
open Function
namespace Sum
@[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₂
@[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
| inr b, h => Or.inr b, h,
fun
| Or.inl a, h => inl a, h
| Or.inr b, h => inr b, h
theorem forall_sum {γ : α β Sort _} (p : ( ab, γ ab) Prop) :
( fab, p fab) ( fa fb, p (Sum.rec fa fb)) := by
refine fun h fa fb => h _, fun h fab => ?_
have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by
apply funext
rintro (_ | _) <;> rfl
rw [h1]; exact h _ _
section get
@[simp] theorem inl_getLeft : (x : α β) (h : x.isLeft), inl (x.getLeft h) = x
| inl _, _ => rfl
@[simp] theorem inr_getRight : (x : α β) (h : x.isRight), inr (x.getRight h) = x
| inr _, _ => rfl
@[simp] theorem getLeft?_eq_none_iff {x : α β} : x.getLeft? = none x.isRight := by
cases x <;> simp only [getLeft?, isRight, eq_self_iff_true, reduceCtorEq]
@[simp] theorem getRight?_eq_none_iff {x : α β} : x.getRight? = none x.isLeft := by
cases x <;> simp only [getRight?, isLeft, eq_self_iff_true, reduceCtorEq]
theorem eq_left_getLeft_of_isLeft : {x : α β} (h : x.isLeft), x = inl (x.getLeft h)
| inl _, _ => rfl
@[simp] theorem getLeft_eq_iff (h : x.isLeft) : x.getLeft h = a x = inl a := by
cases x <;> simp at h
theorem eq_right_getRight_of_isRight : {x : α β} (h : x.isRight), x = inr (x.getRight h)
| inr _, _ => rfl
@[simp] theorem getRight_eq_iff (h : x.isRight) : x.getRight h = b x = inr b := by
cases x <;> simp at h
@[simp] theorem getLeft?_eq_some_iff : x.getLeft? = some a x = inl a := by
cases x <;> simp only [getLeft?, Option.some.injEq, inl.injEq, reduceCtorEq]
@[simp] theorem getRight?_eq_some_iff : x.getRight? = some b x = inr b := by
cases x <;> simp only [getRight?, Option.some.injEq, inr.injEq, reduceCtorEq]
@[simp] theorem bnot_isLeft (x : α β) : !x.isLeft = x.isRight := by cases x <;> rfl
@[simp] theorem isLeft_eq_false {x : α β} : x.isLeft = false x.isRight := by cases x <;> simp
theorem not_isLeft {x : α β} : ¬x.isLeft x.isRight := by simp
@[simp] theorem bnot_isRight (x : α β) : !x.isRight = x.isLeft := by cases x <;> rfl
@[simp] theorem isRight_eq_false {x : α β} : x.isRight = false x.isLeft := by cases x <;> simp
theorem not_isRight {x : α β} : ¬x.isRight x.isLeft := by simp
theorem isLeft_iff : x.isLeft y, x = Sum.inl y := by cases x <;> simp
theorem isRight_iff : x.isRight y, x = Sum.inr y := by cases x <;> simp
end get
theorem inl.inj_iff : (inl a : α β) = inl b a = b := inl.inj, congrArg _
theorem inr.inj_iff : (inr a : α β) = inr b a = b := inr.inj, congrArg _
theorem inl_ne_inr : inl a inr b := nofun
theorem inr_ne_inl : inr b inl a := nofun
/-! ### `Sum.elim` -/
@[simp] theorem elim_comp_inl (f : α γ) (g : β γ) : Sum.elim f g inl = f :=
rfl
@[simp] theorem elim_comp_inr (f : α γ) (g : β γ) : Sum.elim f g inr = g :=
rfl
@[simp] theorem elim_inl_inr : @Sum.elim α β _ inl inr = id :=
funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
theorem comp_elim (f : γ δ) (g : α γ) (h : β γ) :
f Sum.elim g h = Sum.elim (f g) (f h) :=
funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
@[simp] theorem elim_comp_inl_inr (f : α β γ) :
Sum.elim (f inl) (f inr) = f :=
funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
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.map` -/
@[simp] theorem map_map (f' : α' α'') (g' : β' β'') (f : α α') (g : β β') :
x : Sum α β, (x.map f g).map f' g' = x.map (f' f) (g' g)
| inl _ => rfl
| inr _ => rfl
@[simp] theorem map_comp_map (f' : α' α'') (g' : β' β'') (f : α α') (g : β β') :
Sum.map f' g' Sum.map f g = Sum.map (f' f) (g' g) :=
funext <| map_map f' g' f g
@[simp] theorem map_id_id : Sum.map (@id α) (@id β) = id :=
funext fun x => Sum.recOn x (fun _ => rfl) fun _ => rfl
theorem elim_map {f₁ : α β} {f₂ : β ε} {g₁ : γ δ} {g₂ : δ ε} {x} :
Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ f₁) (g₂ g₁) x := by
cases x <;> rfl
theorem elim_comp_map {f₁ : α β} {f₂ : β ε} {g₁ : γ δ} {g₂ : δ ε} :
Sum.elim f₂ g₂ Sum.map f₁ g₁ = Sum.elim (f₂ f₁) (g₂ g₁) :=
funext fun _ => elim_map
@[simp] theorem isLeft_map (f : α β) (g : γ δ) (x : α γ) :
isLeft (x.map f g) = isLeft x := by
cases x <;> rfl
@[simp] theorem isRight_map (f : α β) (g : γ δ) (x : α γ) :
isRight (x.map f g) = isRight x := by
cases x <;> rfl
@[simp] theorem getLeft?_map (f : α β) (g : γ δ) (x : α γ) :
(x.map f g).getLeft? = x.getLeft?.map f := by
cases x <;> rfl
@[simp] theorem getRight?_map (f : α β) (g : γ δ) (x : α γ) :
(x.map f g).getRight? = x.getRight?.map g := by cases x <;> rfl
/-! ### `Sum.swap` -/
@[simp] theorem swap_swap (x : α β) : swap (swap x) = x := by cases x <;> rfl
@[simp] theorem swap_swap_eq : swap swap = @id (α β) := funext <| swap_swap
@[simp] theorem isLeft_swap (x : α β) : x.swap.isLeft = x.isRight := by cases x <;> rfl
@[simp] theorem isRight_swap (x : α β) : x.swap.isRight = x.isLeft := by cases x <;> rfl
@[simp] theorem getLeft?_swap (x : α β) : x.swap.getLeft? = x.getRight? := by cases x <;> rfl
@[simp] theorem getRight?_swap (x : α β) : x.swap.getRight? = x.getLeft? := by cases x <;> rfl
section LiftRel
theorem LiftRel.mono (hr : a b, r₁ a b r₂ a b) (hs : a b, s₁ a b s₂ a b)
(h : LiftRel r₁ s₁ x y) : LiftRel r₂ s₂ x y := by
cases h
· exact LiftRel.inl (hr _ _ _)
· exact LiftRel.inr (hs _ _ _)
theorem LiftRel.mono_left (hr : a b, r₁ a b r₂ a b) (h : LiftRel r₁ s x y) :
LiftRel r₂ s x y :=
(h.mono hr) fun _ _ => id
theorem LiftRel.mono_right (hs : a b, s₁ a b s₂ a b) (h : LiftRel r s₁ x y) :
LiftRel r s₂ x y :=
h.mono (fun _ _ => id) hs
protected theorem LiftRel.swap (h : LiftRel r s x y) : LiftRel s r x.swap y.swap := by
cases h
· exact LiftRel.inr _
· exact LiftRel.inl _
@[simp] theorem liftRel_swap_iff : LiftRel s r x.swap y.swap LiftRel r s x y :=
fun h => by rw [ swap_swap x, swap_swap y]; exact h.swap, LiftRel.swap
end LiftRel
section Lex
protected theorem LiftRel.lex {a b : α β} (h : LiftRel r s a b) : Lex r s a b := by
cases h
· exact Lex.inl _
· exact Lex.inr _
theorem liftRel_subrelation_lex : Subrelation (LiftRel r s) (Lex r s) := LiftRel.lex
theorem Lex.mono (hr : a b, r₁ a b r₂ a b) (hs : a b, s₁ a b s₂ a b) (h : Lex r₁ s₁ x y) :
Lex r₂ s₂ x y := by
cases h
· exact Lex.inl (hr _ _ _)
· exact Lex.inr (hs _ _ _)
· exact Lex.sep _ _
theorem Lex.mono_left (hr : a b, r₁ a b r₂ a b) (h : Lex r₁ s x y) : Lex r₂ s x y :=
(h.mono hr) fun _ _ => id
theorem Lex.mono_right (hs : a b, s₁ a b s₂ a b) (h : Lex r s₁ x y) : Lex r s₂ x y :=
h.mono (fun _ _ => id) hs
theorem lex_acc_inl (aca : Acc r a) : Acc (Lex r s) (inl a) := by
induction aca with
| intro _ _ IH =>
constructor
intro y h
cases h with
| inl h' => exact IH _ h'
theorem lex_acc_inr (aca : a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) :
Acc (Lex r s) (inr b) := by
induction acb with
| intro _ _ IH =>
constructor
intro y h
cases h with
| inr h' => exact IH _ h'
| sep => exact aca _
theorem lex_wf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s) :=
have aca : a, Acc (Lex r s) (inl a) := fun a => lex_acc_inl (ha.apply a)
fun x => Sum.recOn x aca fun b => lex_acc_inr aca (hb.apply b)
end Lex
theorem elim_const_const (c : γ) :
Sum.elim (const _ c : α γ) (const _ c : β γ) = const _ c := by
apply funext
rintro (_ | _) <;> rfl
@[simp] theorem elim_lam_const_lam_const (c : γ) :
Sum.elim (fun _ : α => c) (fun _ : β => c) = fun _ => c :=
Sum.elim_const_const c

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.Basic
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

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Init.Data.UInt.BasicAux
import Init.Data.UInt.Basic
import Init.Data.UInt.Log2
import Init.Data.UInt.Lemmas

View File

@@ -4,50 +4,52 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Data.UInt.BasicAux
import Init.Data.BitVec.Basic
import Init.Data.Fin.Basic
open Nat
@[extern "lean_uint8_of_nat"]
def UInt8.ofNat (n : @& Nat) : UInt8 := Fin.ofNat n
abbrev Nat.toUInt8 := UInt8.ofNat
@[extern "lean_uint8_to_nat"]
def UInt8.toNat (n : UInt8) : Nat := n.val.val
@[extern "lean_uint8_add"]
def UInt8.add (a b : UInt8) : UInt8 := a.toBitVec + b.toBitVec
def UInt8.add (a b : UInt8) : UInt8 := a.val + b.val
@[extern "lean_uint8_sub"]
def UInt8.sub (a b : UInt8) : UInt8 := a.toBitVec - b.toBitVec
def UInt8.sub (a b : UInt8) : UInt8 := a.val - b.val
@[extern "lean_uint8_mul"]
def UInt8.mul (a b : UInt8) : UInt8 := a.toBitVec * b.toBitVec
def UInt8.mul (a b : UInt8) : UInt8 := a.val * b.val
@[extern "lean_uint8_div"]
def UInt8.div (a b : UInt8) : UInt8 := BitVec.udiv a.toBitVec b.toBitVec
def UInt8.div (a b : UInt8) : UInt8 := a.val / b.val
@[extern "lean_uint8_mod"]
def UInt8.mod (a b : UInt8) : UInt8 := BitVec.umod a.toBitVec b.toBitVec
@[extern "lean_uint8_modn", deprecated UInt8.mod (since := "2024-09-23")]
def UInt8.mod (a b : UInt8) : UInt8 := a.val % b.val
@[extern "lean_uint8_modn"]
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
def UInt8.land (a b : UInt8) : UInt8 := Fin.land a.val b.val
@[extern "lean_uint8_lor"]
def UInt8.lor (a b : UInt8) : UInt8 := a.toBitVec ||| b.toBitVec
def UInt8.lor (a b : UInt8) : UInt8 := Fin.lor a.val b.val
@[extern "lean_uint8_xor"]
def UInt8.xor (a b : UInt8) : UInt8 := a.toBitVec ^^^ b.toBitVec
def UInt8.xor (a b : UInt8) : UInt8 := Fin.xor a.val b.val
@[extern "lean_uint8_shift_left"]
def UInt8.shiftLeft (a b : UInt8) : UInt8 := a.toBitVec <<< (mod b 8).toBitVec
def UInt8.shiftLeft (a b : UInt8) : UInt8 := a.val <<< (modn b 8).val
@[extern "lean_uint8_shift_right"]
def UInt8.shiftRight (a b : UInt8) : UInt8 := a.toBitVec >>> (mod b 8).toBitVec
def UInt8.lt (a b : UInt8) : Prop := a.toBitVec < b.toBitVec
def UInt8.le (a b : UInt8) : Prop := a.toBitVec b.toBitVec
def UInt8.shiftRight (a b : UInt8) : UInt8 := a.val >>> (modn b 8).val
def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
def UInt8.le (a b : UInt8) : Prop := a.val b.val
instance UInt8.instOfNat : OfNat UInt8 n := UInt8.ofNat n
instance : Add UInt8 := UInt8.add
instance : Sub UInt8 := UInt8.sub
instance : Mul UInt8 := UInt8.mul
instance : Mod UInt8 := UInt8.mod
set_option linter.deprecated false in
instance : HMod UInt8 Nat UInt8 := UInt8.modn
instance : Div UInt8 := UInt8.div
instance : LT UInt8 := UInt8.lt
instance : LE UInt8 := UInt8.le
@[extern "lean_uint8_complement"]
def UInt8.complement (a : UInt8) : UInt8 := ~~~a.toBitVec
def UInt8.complement (a:UInt8) : UInt8 := 0-(a+1)
instance : Complement UInt8 := UInt8.complement
instance : AndOp UInt8 := UInt8.land
@@ -56,58 +58,69 @@ instance : Xor UInt8 := ⟨UInt8.xor⟩
instance : ShiftLeft UInt8 := UInt8.shiftLeft
instance : ShiftRight UInt8 := UInt8.shiftRight
set_option bootstrap.genMatcherCode false in
@[extern "lean_uint8_dec_lt"]
def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
match a, b with
| n, m => inferInstanceAs (Decidable (n < m))
set_option bootstrap.genMatcherCode false in
@[extern "lean_uint8_dec_le"]
def UInt8.decLe (a b : UInt8) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec b.toBitVec))
match a, b with
| n, m => inferInstanceAs (Decidable (n <= m))
instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
instance (a b : UInt8) : Decidable (a b) := UInt8.decLe a b
instance : Max UInt8 := maxOfLe
instance : Min UInt8 := minOfLe
@[extern "lean_uint16_of_nat"]
def UInt16.ofNat (n : @& Nat) : UInt16 := Fin.ofNat n
abbrev Nat.toUInt16 := UInt16.ofNat
@[extern "lean_uint16_to_nat"]
def UInt16.toNat (n : UInt16) : Nat := n.val.val
@[extern "lean_uint16_add"]
def UInt16.add (a b : UInt16) : UInt16 := a.toBitVec + b.toBitVec
def UInt16.add (a b : UInt16) : UInt16 := a.val + b.val
@[extern "lean_uint16_sub"]
def UInt16.sub (a b : UInt16) : UInt16 := a.toBitVec - b.toBitVec
def UInt16.sub (a b : UInt16) : UInt16 := a.val - b.val
@[extern "lean_uint16_mul"]
def UInt16.mul (a b : UInt16) : UInt16 := a.toBitVec * b.toBitVec
def UInt16.mul (a b : UInt16) : UInt16 := a.val * b.val
@[extern "lean_uint16_div"]
def UInt16.div (a b : UInt16) : UInt16 := BitVec.udiv a.toBitVec b.toBitVec
def UInt16.div (a b : UInt16) : UInt16 := a.val / b.val
@[extern "lean_uint16_mod"]
def UInt16.mod (a b : UInt16) : UInt16 := BitVec.umod a.toBitVec b.toBitVec
@[extern "lean_uint16_modn", deprecated UInt16.mod (since := "2024-09-23")]
def UInt16.mod (a b : UInt16) : UInt16 := a.val % b.val
@[extern "lean_uint16_modn"]
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
def UInt16.land (a b : UInt16) : UInt16 := Fin.land a.val b.val
@[extern "lean_uint16_lor"]
def UInt16.lor (a b : UInt16) : UInt16 := a.toBitVec ||| b.toBitVec
def UInt16.lor (a b : UInt16) : UInt16 := Fin.lor a.val b.val
@[extern "lean_uint16_xor"]
def UInt16.xor (a b : UInt16) : UInt16 := a.toBitVec ^^^ b.toBitVec
def UInt16.xor (a b : UInt16) : UInt16 := Fin.xor a.val b.val
@[extern "lean_uint16_shift_left"]
def UInt16.shiftLeft (a b : UInt16) : UInt16 := a.toBitVec <<< (mod b 16).toBitVec
def UInt16.shiftLeft (a b : UInt16) : UInt16 := a.val <<< (modn b 16).val
@[extern "lean_uint16_to_uint8"]
def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
@[extern "lean_uint8_to_uint16"]
def UInt8.toUInt16 (a : UInt8) : UInt16 := a.val, Nat.lt_trans a.1.2 (by decide)
@[extern "lean_uint16_shift_right"]
def UInt16.shiftRight (a b : UInt16) : UInt16 := a.toBitVec >>> (mod b 16).toBitVec
def UInt16.lt (a b : UInt16) : Prop := a.toBitVec < b.toBitVec
def UInt16.le (a b : UInt16) : Prop := a.toBitVec b.toBitVec
def UInt16.shiftRight (a b : UInt16) : UInt16 := a.val >>> (modn b 16).val
def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
def UInt16.le (a b : UInt16) : Prop := a.val b.val
instance UInt16.instOfNat : OfNat UInt16 n := UInt16.ofNat n
instance : Add UInt16 := UInt16.add
instance : Sub UInt16 := UInt16.sub
instance : Mul UInt16 := UInt16.mul
instance : Mod UInt16 := UInt16.mod
set_option linter.deprecated false in
instance : HMod UInt16 Nat UInt16 := UInt16.modn
instance : Div UInt16 := UInt16.div
instance : LT UInt16 := UInt16.lt
instance : LE UInt16 := UInt16.le
@[extern "lean_uint16_complement"]
def UInt16.complement (a : UInt16) : UInt16 := ~~~a.toBitVec
def UInt16.complement (a:UInt16) : UInt16 := 0-(a+1)
instance : Complement UInt16 := UInt16.complement
instance : AndOp UInt16 := UInt16.land
@@ -119,53 +132,74 @@ instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
set_option bootstrap.genMatcherCode false in
@[extern "lean_uint16_dec_lt"]
def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
match a, b with
| n, m => inferInstanceAs (Decidable (n < m))
set_option bootstrap.genMatcherCode false in
@[extern "lean_uint16_dec_le"]
def UInt16.decLe (a b : UInt16) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec b.toBitVec))
match a, b with
| n, m => inferInstanceAs (Decidable (n <= m))
instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
instance (a b : UInt16) : Decidable (a b) := UInt16.decLe a b
instance : Max UInt16 := maxOfLe
instance : Min UInt16 := minOfLe
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat (n : @& Nat) : UInt32 := Fin.ofNat n
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := n, h
/--
Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
-/
def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
if h : n < UInt32.size then
UInt32.ofNat' n h
else
UInt32.ofNat' (UInt32.size - 1) (by decide)
abbrev Nat.toUInt32 := UInt32.ofNat
@[extern "lean_uint32_add"]
def UInt32.add (a b : UInt32) : UInt32 := a.toBitVec + b.toBitVec
def UInt32.add (a b : UInt32) : UInt32 := a.val + b.val
@[extern "lean_uint32_sub"]
def UInt32.sub (a b : UInt32) : UInt32 := a.toBitVec - b.toBitVec
def UInt32.sub (a b : UInt32) : UInt32 := a.val - b.val
@[extern "lean_uint32_mul"]
def UInt32.mul (a b : UInt32) : UInt32 := a.toBitVec * b.toBitVec
def UInt32.mul (a b : UInt32) : UInt32 := a.val * b.val
@[extern "lean_uint32_div"]
def UInt32.div (a b : UInt32) : UInt32 := BitVec.udiv a.toBitVec b.toBitVec
def UInt32.div (a b : UInt32) : UInt32 := a.val / b.val
@[extern "lean_uint32_mod"]
def UInt32.mod (a b : UInt32) : UInt32 := BitVec.umod a.toBitVec b.toBitVec
@[extern "lean_uint32_modn", deprecated UInt32.mod (since := "2024-09-23")]
def UInt32.mod (a b : UInt32) : UInt32 := a.val % b.val
@[extern "lean_uint32_modn"]
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
def UInt32.land (a b : UInt32) : UInt32 := Fin.land a.val b.val
@[extern "lean_uint32_lor"]
def UInt32.lor (a b : UInt32) : UInt32 := a.toBitVec ||| b.toBitVec
def UInt32.lor (a b : UInt32) : UInt32 := Fin.lor a.val b.val
@[extern "lean_uint32_xor"]
def UInt32.xor (a b : UInt32) : UInt32 := a.toBitVec ^^^ b.toBitVec
def UInt32.xor (a b : UInt32) : UInt32 := Fin.xor a.val b.val
@[extern "lean_uint32_shift_left"]
def UInt32.shiftLeft (a b : UInt32) : UInt32 := a.toBitVec <<< (mod b 32).toBitVec
def UInt32.shiftLeft (a b : UInt32) : UInt32 := a.val <<< (modn b 32).val
@[extern "lean_uint32_shift_right"]
def UInt32.shiftRight (a b : UInt32) : UInt32 := a.toBitVec >>> (mod b 32).toBitVec
def UInt32.shiftRight (a b : UInt32) : UInt32 := a.val >>> (modn b 32).val
@[extern "lean_uint32_to_uint8"]
def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
@[extern "lean_uint32_to_uint16"]
def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
@[extern "lean_uint8_to_uint32"]
def UInt8.toUInt32 (a : UInt8) : UInt32 := a.val, Nat.lt_trans a.1.2 (by decide)
@[extern "lean_uint16_to_uint32"]
def UInt16.toUInt32 (a : UInt16) : UInt32 := a.val, Nat.lt_trans a.1.2 (by decide)
instance UInt32.instOfNat : OfNat UInt32 n := UInt32.ofNat n
instance : Add UInt32 := UInt32.add
instance : Sub UInt32 := UInt32.sub
instance : Mul UInt32 := UInt32.mul
instance : Mod UInt32 := UInt32.mod
set_option linter.deprecated false in
instance : HMod UInt32 Nat UInt32 := UInt32.modn
instance : Div UInt32 := UInt32.div
@[extern "lean_uint32_complement"]
def UInt32.complement (a : UInt32) : UInt32 := ~~~a.toBitVec
def UInt32.complement (a:UInt32) : UInt32 := 0-(a+1)
instance : Complement UInt32 := UInt32.complement
instance : AndOp UInt32 := UInt32.land
@@ -174,45 +208,60 @@ instance : Xor UInt32 := ⟨UInt32.xor⟩
instance : ShiftLeft UInt32 := UInt32.shiftLeft
instance : ShiftRight UInt32 := UInt32.shiftRight
@[extern "lean_uint64_of_nat"]
def UInt64.ofNat (n : @& Nat) : UInt64 := Fin.ofNat n
abbrev Nat.toUInt64 := UInt64.ofNat
@[extern "lean_uint64_to_nat"]
def UInt64.toNat (n : UInt64) : Nat := n.val.val
@[extern "lean_uint64_add"]
def UInt64.add (a b : UInt64) : UInt64 := a.toBitVec + b.toBitVec
def UInt64.add (a b : UInt64) : UInt64 := a.val + b.val
@[extern "lean_uint64_sub"]
def UInt64.sub (a b : UInt64) : UInt64 := a.toBitVec - b.toBitVec
def UInt64.sub (a b : UInt64) : UInt64 := a.val - b.val
@[extern "lean_uint64_mul"]
def UInt64.mul (a b : UInt64) : UInt64 := a.toBitVec * b.toBitVec
def UInt64.mul (a b : UInt64) : UInt64 := a.val * b.val
@[extern "lean_uint64_div"]
def UInt64.div (a b : UInt64) : UInt64 := BitVec.udiv a.toBitVec b.toBitVec
def UInt64.div (a b : UInt64) : UInt64 := a.val / b.val
@[extern "lean_uint64_mod"]
def UInt64.mod (a b : UInt64) : UInt64 := BitVec.umod a.toBitVec b.toBitVec
@[extern "lean_uint64_modn", deprecated UInt64.mod (since := "2024-09-23")]
def UInt64.mod (a b : UInt64) : UInt64 := a.val % b.val
@[extern "lean_uint64_modn"]
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
def UInt64.land (a b : UInt64) : UInt64 := Fin.land a.val b.val
@[extern "lean_uint64_lor"]
def UInt64.lor (a b : UInt64) : UInt64 := a.toBitVec ||| b.toBitVec
def UInt64.lor (a b : UInt64) : UInt64 := Fin.lor a.val b.val
@[extern "lean_uint64_xor"]
def UInt64.xor (a b : UInt64) : UInt64 := a.toBitVec ^^^ b.toBitVec
def UInt64.xor (a b : UInt64) : UInt64 := Fin.xor a.val b.val
@[extern "lean_uint64_shift_left"]
def UInt64.shiftLeft (a b : UInt64) : UInt64 := a.toBitVec <<< (mod b 64).toBitVec
def UInt64.shiftLeft (a b : UInt64) : UInt64 := a.val <<< (modn b 64).val
@[extern "lean_uint64_shift_right"]
def UInt64.shiftRight (a b : UInt64) : UInt64 := a.toBitVec >>> (mod b 64).toBitVec
def UInt64.lt (a b : UInt64) : Prop := a.toBitVec < b.toBitVec
def UInt64.le (a b : UInt64) : Prop := a.toBitVec b.toBitVec
def UInt64.shiftRight (a b : UInt64) : UInt64 := a.val >>> (modn b 64).val
def UInt64.lt (a b : UInt64) : Prop := a.val < b.val
def UInt64.le (a b : UInt64) : Prop := a.val b.val
@[extern "lean_uint64_to_uint8"]
def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
@[extern "lean_uint64_to_uint16"]
def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
@[extern "lean_uint64_to_uint32"]
def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
@[extern "lean_uint8_to_uint64"]
def UInt8.toUInt64 (a : UInt8) : UInt64 := a.val, Nat.lt_trans a.1.2 (by decide)
@[extern "lean_uint16_to_uint64"]
def UInt16.toUInt64 (a : UInt16) : UInt64 := a.val, Nat.lt_trans a.1.2 (by decide)
@[extern "lean_uint32_to_uint64"]
def UInt32.toUInt64 (a : UInt32) : UInt64 := a.val, Nat.lt_trans a.1.2 (by decide)
instance UInt64.instOfNat : OfNat UInt64 n := UInt64.ofNat n
instance : Add UInt64 := UInt64.add
instance : Sub UInt64 := UInt64.sub
instance : Mul UInt64 := UInt64.mul
instance : Mod UInt64 := UInt64.mod
set_option linter.deprecated false in
instance : HMod UInt64 Nat UInt64 := UInt64.modn
instance : Div UInt64 := UInt64.div
instance : LT UInt64 := UInt64.lt
instance : LE UInt64 := UInt64.le
@[extern "lean_uint64_complement"]
def UInt64.complement (a : UInt64) : UInt64 := ~~~a.toBitVec
def UInt64.complement (a:UInt64) : UInt64 := 0-(a+1)
instance : Complement UInt64 := UInt64.complement
instance : AndOp UInt64 := UInt64.land
@@ -224,52 +273,79 @@ instance : ShiftRight UInt64 := ⟨UInt64.shiftRight⟩
@[extern "lean_bool_to_uint64"]
def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
set_option bootstrap.genMatcherCode false in
@[extern "lean_uint64_dec_lt"]
def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
match a, b with
| n, m => inferInstanceAs (Decidable (n < m))
set_option bootstrap.genMatcherCode false in
@[extern "lean_uint64_dec_le"]
def UInt64.decLe (a b : UInt64) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec b.toBitVec))
match a, b with
| n, m => inferInstanceAs (Decidable (n <= m))
instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
instance (a b : UInt64) : Decidable (a b) := UInt64.decLe a b
instance : Max UInt64 := maxOfLe
instance : Min UInt64 := minOfLe
-- This instance would interfere with the global instance `NeZero (n + 1)`,
-- so we only enable it locally.
@[local instance]
private def instNeZeroUSizeSize : NeZero USize.size := add_one_ne_zero _
@[deprecated (since := "2024-09-16")]
theorem usize_size_gt_zero : USize.size > 0 :=
Nat.zero_lt_succ ..
@[extern "lean_usize_of_nat"]
def USize.ofNat (n : @& Nat) : USize := Fin.ofNat' _ n
abbrev Nat.toUSize := USize.ofNat
@[extern "lean_usize_to_nat"]
def USize.toNat (n : USize) : Nat := n.val.val
@[extern "lean_usize_add"]
def USize.add (a b : USize) : USize := a.val + b.val
@[extern "lean_usize_sub"]
def USize.sub (a b : USize) : USize := a.val - b.val
@[extern "lean_usize_mul"]
def USize.mul (a b : USize) : USize := a.toBitVec * b.toBitVec
def USize.mul (a b : USize) : USize := a.val * b.val
@[extern "lean_usize_div"]
def USize.div (a b : USize) : USize := a.toBitVec / b.toBitVec
def USize.div (a b : USize) : USize := a.val / b.val
@[extern "lean_usize_mod"]
def USize.mod (a b : USize) : USize := a.toBitVec % b.toBitVec
@[extern "lean_usize_modn", deprecated USize.mod (since := "2024-09-23")]
def USize.mod (a b : USize) : USize := a.val % b.val
@[extern "lean_usize_modn"]
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
def USize.land (a b : USize) : USize := Fin.land a.val b.val
@[extern "lean_usize_lor"]
def USize.lor (a b : USize) : USize := a.toBitVec ||| b.toBitVec
def USize.lor (a b : USize) : USize := Fin.lor a.val b.val
@[extern "lean_usize_xor"]
def USize.xor (a b : USize) : USize := a.toBitVec ^^^ b.toBitVec
def USize.xor (a b : USize) : USize := Fin.xor a.val b.val
@[extern "lean_usize_shift_left"]
def USize.shiftLeft (a b : USize) : USize := a.toBitVec <<< (mod b (USize.ofNat System.Platform.numBits)).toBitVec
def USize.shiftLeft (a b : USize) : USize := a.val <<< (modn b System.Platform.numBits).val
@[extern "lean_usize_shift_right"]
def USize.shiftRight (a b : USize) : USize := a.toBitVec >>> (mod b (USize.ofNat System.Platform.numBits)).toBitVec
def USize.shiftRight (a b : USize) : USize := a.val >>> (modn b System.Platform.numBits).val
@[extern "lean_uint32_to_usize"]
def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.val a.1.2
@[extern "lean_usize_to_uint32"]
def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
def USize.lt (a b : USize) : Prop := a.val < b.val
def USize.le (a b : USize) : Prop := a.val b.val
instance USize.instOfNat : OfNat USize n := USize.ofNat n
instance : Add USize := USize.add
instance : Sub USize := USize.sub
instance : Mul USize := USize.mul
instance : Mod USize := USize.mod
set_option linter.deprecated false in
instance : HMod USize Nat USize := USize.modn
instance : Div USize := USize.div
instance : LT USize := USize.lt
instance : LE USize := USize.le
@[extern "lean_usize_complement"]
def USize.complement (a : USize) : USize := ~~~a.toBitVec
def USize.complement (a:USize) : USize := 0-(a+1)
instance : Complement USize := USize.complement
instance : AndOp USize := USize.land
@@ -278,5 +354,19 @@ instance : Xor USize := ⟨USize.xor⟩
instance : ShiftLeft USize := USize.shiftLeft
instance : ShiftRight USize := USize.shiftRight
set_option bootstrap.genMatcherCode false in
@[extern "lean_usize_dec_lt"]
def USize.decLt (a b : USize) : Decidable (a < b) :=
match a, b with
| n, m => inferInstanceAs (Decidable (n < m))
set_option bootstrap.genMatcherCode false in
@[extern "lean_usize_dec_le"]
def USize.decLe (a b : USize) : Decidable (a b) :=
match a, b with
| n, m => inferInstanceAs (Decidable (n <= m))
instance (a b : USize) : Decidable (a < b) := USize.decLt a b
instance (a b : USize) : Decidable (a b) := USize.decLe a b
instance : Max USize := maxOfLe
instance : Min USize := minOfLe

View File

@@ -1,132 +0,0 @@
/-
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Data.Fin.Basic
import Init.Data.BitVec.BasicAux
/-!
This module exists to provide the very basic `UInt8` etc. definitions required for
`Init.Data.Char.Basic` and `Init.Data.Array.Basic`. These are very important as they are used in
meta code that is then (transitively) used in `Init.Data.UInt.Basic` and `Init.Data.BitVec.Basic`.
This file thus breaks the import cycle that would be created by this dependency.
-/
open Nat
def UInt8.val (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
@[extern "lean_uint8_of_nat"]
def UInt8.ofNat (n : @& Nat) : UInt8 := BitVec.ofNat 8 n
abbrev Nat.toUInt8 := UInt8.ofNat
@[extern "lean_uint8_to_nat"]
def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat
instance UInt8.instOfNat : OfNat UInt8 n := UInt8.ofNat n
def UInt16.val (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin
@[extern "lean_uint16_of_nat"]
def UInt16.ofNat (n : @& Nat) : UInt16 := BitVec.ofNat 16 n
abbrev Nat.toUInt16 := UInt16.ofNat
@[extern "lean_uint16_to_nat"]
def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat
@[extern "lean_uint16_to_uint8"]
def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
@[extern "lean_uint8_to_uint16"]
def UInt8.toUInt16 (a : UInt8) : UInt16 := a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)
instance UInt16.instOfNat : OfNat UInt16 n := UInt16.ofNat n
def UInt32.val (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat (n : @& Nat) : UInt32 := BitVec.ofNat 32 n
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := BitVec.ofNatLt n h
/--
Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
-/
def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
if h : n < UInt32.size then
UInt32.ofNat' n h
else
UInt32.ofNat' (UInt32.size - 1) (by decide)
abbrev Nat.toUInt32 := UInt32.ofNat
@[extern "lean_uint32_to_uint8"]
def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
@[extern "lean_uint32_to_uint16"]
def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
@[extern "lean_uint8_to_uint32"]
def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)
@[extern "lean_uint16_to_uint32"]
def UInt16.toUInt32 (a : UInt16) : UInt32 := a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)
instance UInt32.instOfNat : OfNat UInt32 n := UInt32.ofNat n
theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
n < m UInt32.ofNat' n h1 < UInt32.ofNat m := by
simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
Nat.mod_eq_of_lt h2, imp_self]
theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
m < n UInt32.ofNat m < UInt32.ofNat' n h1 := by
simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
Nat.mod_eq_of_lt h2, imp_self]
def UInt64.val (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin
@[extern "lean_uint64_of_nat"]
def UInt64.ofNat (n : @& Nat) : UInt64 := BitVec.ofNat 64 n
abbrev Nat.toUInt64 := UInt64.ofNat
@[extern "lean_uint64_to_nat"]
def UInt64.toNat (n : UInt64) : Nat := n.toBitVec.toNat
@[extern "lean_uint64_to_uint8"]
def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
@[extern "lean_uint64_to_uint16"]
def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
@[extern "lean_uint64_to_uint32"]
def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
@[extern "lean_uint8_to_uint64"]
def UInt8.toUInt64 (a : UInt8) : UInt64 := a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)
@[extern "lean_uint16_to_uint64"]
def UInt16.toUInt64 (a : UInt16) : UInt64 := a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)
@[extern "lean_uint32_to_uint64"]
def UInt32.toUInt64 (a : UInt32) : UInt64 := a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)
instance UInt64.instOfNat : OfNat UInt64 n := UInt64.ofNat n
theorem usize_size_gt_zero : USize.size > 0 := by
cases usize_size_eq with
| inl h => rw [h]; decide
| inr h => rw [h]; decide
def USize.val (x : USize) : Fin USize.size := x.toBitVec.toFin
@[extern "lean_usize_of_nat"]
def USize.ofNat (n : @& Nat) : USize := BitVec.ofNat _ n
abbrev Nat.toUSize := USize.ofNat
@[extern "lean_usize_to_nat"]
def USize.toNat (n : USize) : Nat := n.toBitVec.toNat
@[extern "lean_usize_add"]
def USize.add (a b : USize) : USize := a.toBitVec + b.toBitVec
@[extern "lean_usize_sub"]
def USize.sub (a b : USize) : USize := a.toBitVec - b.toBitVec
def USize.lt (a b : USize) : Prop := a.toBitVec < b.toBitVec
def USize.le (a b : USize) : Prop := a.toBitVec b.toBitVec
instance USize.instOfNat : OfNat USize n := USize.ofNat n
instance : Add USize := USize.add
instance : Sub USize := USize.sub
instance : LT USize := USize.lt
instance : LE USize := USize.le
@[extern "lean_usize_dec_lt"]
def USize.decLt (a b : USize) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
@[extern "lean_usize_dec_le"]
def USize.decLe (a b : USize) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec b.toBitVec))
instance (a b : USize) : Decidable (a < b) := USize.decLt a b
instance (a b : USize) : Decidable (a b) := USize.decLe a b

View File

@@ -6,14 +6,13 @@ Authors: Markus Himmel
prelude
import Init.Data.UInt.Basic
import Init.Data.Fin.Bitwise
import Init.Data.BitVec.Lemmas
set_option hygiene false in
macro "declare_bitwise_uint_theorems" typeName:ident : command =>
`(
namespace $typeName
@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := Fin.and_val ..
end $typeName
)

View File

@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
prelude
import Init.Data.UInt.Basic
import Init.Data.Fin.Lemmas
import Init.Data.BitVec.Lemmas
import Init.Data.BitVec.Bitblast
set_option hygiene false in
macro "declare_uint_theorems" typeName:ident : command =>
@@ -19,111 +17,50 @@ instance : Inhabited $typeName where
theorem zero_def : (0 : $typeName) = 0 := rfl
theorem one_def : (1 : $typeName) = 1 := rfl
theorem sub_def (a b : $typeName) : a - b = a.toBitVec - b.toBitVec := rfl
theorem mul_def (a b : $typeName) : a * b = a.toBitVec * b.toBitVec := rfl
theorem mod_def (a b : $typeName) : a % b = a.toBitVec % b.toBitVec := rfl
theorem add_def (a b : $typeName) : a + b = a.toBitVec + b.toBitVec := rfl
theorem sub_def (a b : $typeName) : a - b = a.val - b.val := rfl
theorem mul_def (a b : $typeName) : a * b = a.val * b.val := rfl
theorem mod_def (a b : $typeName) : a % b = a.val % b.val := rfl
theorem add_def (a b : $typeName) : a + b = a.val + b.val := rfl
@[simp] theorem mk_toBitVec_eq : (a : $typeName), mk a.toBitVec = a
@[simp] theorem mk_val_eq : (a : $typeName), mk a.val = a
| _, _ => rfl
theorem toBitVec_eq_of_lt {a : Nat} : a < size (ofNat a).toBitVec.toNat = a :=
theorem val_eq_of_lt {a : Nat} : a < size ((ofNat a).val : Nat) = a :=
Nat.mod_eq_of_lt
theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
rw [toNat, toBitVec_eq_of_lt h]
theorem le_def {a b : $typeName} : a b a.toBitVec b.toBitVec := .rfl
theorem lt_def {a b : $typeName} : a < b a.toBitVec < b.toBitVec := .rfl
@[simp] protected theorem not_le {a b : $typeName} : ¬ a b b < a := by simp [le_def, lt_def]
@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b b a := by simp [le_def, lt_def]
rw [toNat, val_eq_of_lt h]
theorem le_def {a b : $typeName} : a b a.1 b.1 := .rfl
theorem lt_def {a b : $typeName} : a < b a.1 < b.1 := .rfl
theorem lt_iff_val_lt_val {a b : $typeName} : a < b a.val < b.val := .rfl
@[simp] protected theorem not_le {a b : $typeName} : ¬ a b b < a := Fin.not_le
@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b b a := Fin.not_lt
@[simp] protected theorem le_refl (a : $typeName) : a a := by simp [le_def]
@[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
protected theorem le_trans {a b c : $typeName} : a b b c a c := BitVec.le_trans
protected theorem lt_trans {a b c : $typeName} : a < b b < c a < c := BitVec.lt_trans
protected theorem le_total (a b : $typeName) : a b b a := BitVec.le_total ..
protected theorem lt_asymm {a b : $typeName} : a < b ¬ b < a := BitVec.lt_asymm
protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h rfl
protected theorem eq_of_toBitVec_eq {a b : $typeName} (h : a.toBitVec = b.toBitVec) : a = b := by
cases a; cases b; simp_all
open $typeName (eq_of_toBitVec_eq) in
protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
rcases a with _; rcases b with _; simp_all [val]
open $typeName (toBitVec_eq_of_eq) in
protected theorem ne_of_toBitVec_ne {a b : $typeName} (h : a.toBitVec b.toBitVec) : a b :=
fun h' => absurd (toBitVec_eq_of_eq h') h
open $typeName (ne_of_toBitVec_ne) in
protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a b := by
apply ne_of_toBitVec_ne
apply BitVec.ne_of_lt
simpa [lt_def] using h
protected theorem le_trans {a b c : $typeName} : a b b c a c := Fin.le_trans
protected theorem lt_trans {a b c : $typeName} : a < b b < c a < c := Fin.lt_trans
protected theorem le_total (a b : $typeName) : a b b a := Fin.le_total a.1 b.1
protected theorem lt_asymm {a b : $typeName} (h : a < b) : ¬ b < a := Fin.lt_asymm h
protected theorem val_eq_of_eq {a b : $typeName} (h : a = b) : a.val = b.val := h rfl
protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by cases a; cases b; simp at h; simp [h]
open $typeName (val_eq_of_eq) in
protected theorem ne_of_val_ne {a b : $typeName} (h : a.val b.val) : a b := fun h' => absurd (val_eq_of_eq h') h
open $typeName (ne_of_val_ne) in
protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a b := ne_of_val_ne (Fin.ne_of_lt h)
@[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := BitVec.toNat_umod ..
@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := BitVec.toNat_udiv ..
@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b a (a - b).toNat = a.toNat - b.toNat := BitVec.toNat_sub_of_le
protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.toBitVec.isLt
open $typeName (toNat_mod toNat_lt_size) in
protected theorem toNat_mod_lt {m : Nat} : (u : $typeName), m > 0 toNat (u % ofNat m) < m := by
intro u h1
by_cases h2 : m < size
· rw [toNat_mod, toNat_ofNat_of_lt h2]
apply Nat.mod_lt _ h1
· apply Nat.lt_of_lt_of_le
· apply toNat_lt_size
· simpa using h2
open $typeName (toNat_mod_lt) in
set_option linter.deprecated false in
@[deprecated toNat_mod_lt (since := "2024-09-24")]
protected theorem modn_lt {m : Nat} : (u : $typeName), m > 0 toNat (u % m) < m := by
intro u
simp only [(· % ·)]
simp only [gt_iff_lt, toNat, modn, Fin.modn_val, BitVec.natCast_eq_ofNat, BitVec.toNat_ofNat,
Nat.reducePow]
rw [Nat.mod_eq_of_lt]
· apply Nat.mod_lt
· apply Nat.lt_of_le_of_lt
· apply Nat.mod_le
· apply Fin.is_lt
protected theorem mod_lt (a : $typeName) {b : $typeName} : 0 < b a % b < b := by
simp only [lt_def, mod_def]
apply BitVec.umod_lt
@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b a (a - b).toNat = a.toNat - b.toNat := Fin.sub_val_of_le
@[simp] protected theorem toNat_modn (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
protected theorem modn_lt {m : Nat} : (u : $typeName), m > 0 toNat (u % m) < m
| u, h => Fin.modn_lt u h
open $typeName (modn_lt) in
protected theorem mod_lt (a b : $typeName) (h : 0 < b) : a % b < b := modn_lt _ (by simp [lt_def] at h; exact h)
protected theorem toNat.inj : {a b : $typeName}, a.toNat = b.toNat a = b
| _, _, _, _, rfl => rfl
protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.1.2
@[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
@[simp]
theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
@[simp]
theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
@[simp]
theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
end $typeName
)
@@ -133,34 +70,27 @@ declare_uint_theorems UInt32
declare_uint_theorems UInt64
declare_uint_theorems USize
theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m n.toNat < m := by
simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n m < n.toNat := by
simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ofNat m n.toNat m := by
simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m n m n.toNat := by
simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
@[deprecated (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero
@[deprecated (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div
@[deprecated (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod
@[deprecated (since := "2024-06-23")] protected abbrev UInt8.modn_toNat := @UInt8.toNat_modn
@[deprecated (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero
@[deprecated (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div
@[deprecated (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod
@[deprecated (since := "2024-06-23")] protected abbrev UInt16.modn_toNat := @UInt16.toNat_modn
@[deprecated (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero
@[deprecated (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div
@[deprecated (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod
@[deprecated (since := "2024-06-23")] protected abbrev UInt32.modn_toNat := @UInt32.toNat_modn
@[deprecated (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero
@[deprecated (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div
@[deprecated (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod
@[deprecated (since := "2024-06-23")] protected abbrev UInt64.modn_toNat := @UInt64.toNat_modn
@[deprecated (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero
@[deprecated (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div
@[deprecated (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod
@[deprecated (since := "2024-06-23")] protected abbrev USize.modn_toNat := @USize.toNat_modn

View File

@@ -7,16 +7,16 @@ prelude
import Init.Data.Fin.Log2
@[extern "lean_uint8_log2"]
def UInt8.log2 (a : UInt8) : UInt8 := Fin.log2 a.val
def UInt8.log2 (a : UInt8) : UInt8 := Fin.log2 a.val
@[extern "lean_uint16_log2"]
def UInt16.log2 (a : UInt16) : UInt16 := Fin.log2 a.val
def UInt16.log2 (a : UInt16) : UInt16 := Fin.log2 a.val
@[extern "lean_uint32_log2"]
def UInt32.log2 (a : UInt32) : UInt32 := Fin.log2 a.val
def UInt32.log2 (a : UInt32) : UInt32 := Fin.log2 a.val
@[extern "lean_uint64_log2"]
def UInt64.log2 (a : UInt64) : UInt64 := Fin.log2 a.val
def UInt64.log2 (a : UInt64) : UInt64 := Fin.log2 a.val
@[extern "lean_usize_log2"]
def USize.log2 (a : USize) : USize := Fin.log2 a.val
def USize.log2 (a : USize) : USize := Fin.log2 a.val

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

@@ -224,7 +224,11 @@ structure Config where
-/
index : Bool := true
/--
This option does not have any effect (yet).
When `true` (default: `true`), `simp` will **not** create a proof for a rewriting rule associated
with an `rfl`-theorem.
Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
will **not** create a proof term which is an application of the annotated theorem.
-/
implicitDefEqProofs : Bool := true
deriving Inhabited, BEq

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

@@ -1592,6 +1592,9 @@ def Nat.beq : (@& Nat) → (@& Nat) → Bool
| succ _, zero => false
| succ n, succ m => beq n m
instance : BEq Nat where
beq := Nat.beq
theorem Nat.eq_of_beq_eq_true : {n m : Nat} Eq (beq n m) true Eq n m
| zero, zero, _ => rfl
| zero, succ _, h => Bool.noConfusion h
@@ -1866,52 +1869,6 @@ instance {n} : LE (Fin n) where
instance Fin.decLt {n} (a b : Fin n) : Decidable (LT.lt a b) := Nat.decLt ..
instance Fin.decLe {n} (a b : Fin n) : Decidable (LE.le a b) := Nat.decLe ..
/--
A bitvector of the specified width.
This is represented as the underlying `Nat` number in both the runtime
and the kernel, inheriting all the special support for `Nat`.
-/
structure BitVec (w : Nat) where
/-- Construct a `BitVec w` from a number less than `2^w`.
O(1), because we use `Fin` as the internal representation of a bitvector. -/
ofFin ::
/-- Interpret a bitvector as a number less than `2^w`.
O(1), because we use `Fin` as the internal representation of a bitvector. -/
toFin : Fin (hPow 2 w)
/--
Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
-/
-- We manually derive the `DecidableEq` instances for `BitVec` because
-- we want to have builtin support for bit-vector literals, and we
-- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
def BitVec.decEq (x y : BitVec n) : Decidable (Eq x y) :=
match x, y with
| n, m =>
dite (Eq n m)
(fun h => isTrue (h rfl))
(fun h => isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h)))
instance : DecidableEq (BitVec n) := BitVec.decEq
/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
@[match_pattern]
protected def BitVec.ofNatLt {n : Nat} (i : Nat) (p : LT.lt i (hPow 2 n)) : BitVec n where
toFin := i, p
/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
(zero-cost) wrapper around a `Nat`. -/
protected def BitVec.toNat (x : BitVec n) : Nat := x.toFin.val
instance : LT (BitVec n) where lt := (LT.lt ·.toNat ·.toNat)
instance (x y : BitVec n) : Decidable (LT.lt x y) :=
inferInstanceAs (Decidable (LT.lt x.toNat y.toNat))
instance : LE (BitVec n) where le := (LE.le ·.toNat ·.toNat)
instance (x y : BitVec n) : Decidable (LE.le x y) :=
inferInstanceAs (Decidable (LE.le x.toNat y.toNat))
/-- The size of type `UInt8`, that is, `2^8 = 256`. -/
abbrev UInt8.size : Nat := 256
@@ -1920,12 +1877,12 @@ The type of unsigned 8-bit integers. This type has special support in the
compiler to make it actually 8 bits rather than wrapping a `Nat`.
-/
structure UInt8 where
/-- Unpack a `UInt8` as a `BitVec 8`.
/-- Unpack a `UInt8` as a `Nat` less than `2^8`.
This function is overridden with a native implementation. -/
toBitVec : BitVec 8
val : Fin UInt8.size
attribute [extern "lean_uint8_of_nat_mk"] UInt8.mk
attribute [extern "lean_uint8_to_nat"] UInt8.toBitVec
attribute [extern "lean_uint8_to_nat"] UInt8.val
/--
Pack a `Nat` less than `2^8` into a `UInt8`.
@@ -1933,7 +1890,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint8_of_nat"]
def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
toBitVec := BitVec.ofNatLt n h
val := { val := n, isLt := h }
set_option bootstrap.genMatcherCode false in
/--
@@ -1944,9 +1901,7 @@ This function is overridden with a native implementation.
def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
match a, b with
| n, m =>
dite (Eq n m)
(fun h => isTrue (h rfl))
(fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
dite (Eq n m) (fun h => isTrue (h rfl)) (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
instance : DecidableEq UInt8 := UInt8.decEq
@@ -1961,12 +1916,12 @@ The type of unsigned 16-bit integers. This type has special support in the
compiler to make it actually 16 bits rather than wrapping a `Nat`.
-/
structure UInt16 where
/-- Unpack a `UInt16` as a `BitVec 16`.
/-- Unpack a `UInt16` as a `Nat` less than `2^16`.
This function is overridden with a native implementation. -/
toBitVec : BitVec 16
val : Fin UInt16.size
attribute [extern "lean_uint16_of_nat_mk"] UInt16.mk
attribute [extern "lean_uint16_to_nat"] UInt16.toBitVec
attribute [extern "lean_uint16_to_nat"] UInt16.val
/--
Pack a `Nat` less than `2^16` into a `UInt16`.
@@ -1974,7 +1929,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint16_of_nat"]
def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
toBitVec := BitVec.ofNatLt n h
val := { val := n, isLt := h }
set_option bootstrap.genMatcherCode false in
/--
@@ -1985,9 +1940,7 @@ This function is overridden with a native implementation.
def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
match a, b with
| n, m =>
dite (Eq n m)
(fun h => isTrue (h rfl))
(fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
dite (Eq n m) (fun h => isTrue (h rfl)) (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
instance : DecidableEq UInt16 := UInt16.decEq
@@ -2002,12 +1955,12 @@ The type of unsigned 32-bit integers. This type has special support in the
compiler to make it actually 32 bits rather than wrapping a `Nat`.
-/
structure UInt32 where
/-- Unpack a `UInt32` as a `BitVec 32.
/-- Unpack a `UInt32` as a `Nat` less than `2^32`.
This function is overridden with a native implementation. -/
toBitVec : BitVec 32
val : Fin UInt32.size
attribute [extern "lean_uint32_of_nat_mk"] UInt32.mk
attribute [extern "lean_uint32_to_nat"] UInt32.toBitVec
attribute [extern "lean_uint32_to_nat"] UInt32.val
/--
Pack a `Nat` less than `2^32` into a `UInt32`.
@@ -2015,14 +1968,14 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint32_of_nat"]
def UInt32.ofNatCore (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
toBitVec := BitVec.ofNatLt n h
val := { val := n, isLt := h }
/--
Unpack a `UInt32` as a `Nat`.
This function is overridden with a native implementation.
-/
@[extern "lean_uint32_to_nat"]
def UInt32.toNat (n : UInt32) : Nat := n.toBitVec.toNat
def UInt32.toNat (n : UInt32) : Nat := n.val.val
set_option bootstrap.genMatcherCode false in
/--
@@ -2041,26 +1994,30 @@ instance : Inhabited UInt32 where
default := UInt32.ofNatCore 0 (by decide)
instance : LT UInt32 where
lt a b := LT.lt a.toBitVec b.toBitVec
lt a b := LT.lt a.val b.val
instance : LE UInt32 where
le a b := LE.le a.toBitVec b.toBitVec
le a b := LE.le a.val b.val
set_option bootstrap.genMatcherCode false in
/--
Decides less-equal on `UInt32`.
This function is overridden with a native implementation.
-/
@[extern "lean_uint32_dec_lt"]
def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
match a, b with
| n, m => inferInstanceAs (Decidable (LT.lt n m))
set_option bootstrap.genMatcherCode false in
/--
Decides less-than on `UInt32`.
This function is overridden with a native implementation.
-/
@[extern "lean_uint32_dec_le"]
def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
match a, b with
| n, m => inferInstanceAs (Decidable (LE.le n m))
instance (a b : UInt32) : Decidable (LT.lt a b) := UInt32.decLt a b
instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b
@@ -2074,12 +2031,12 @@ The type of unsigned 64-bit integers. This type has special support in the
compiler to make it actually 64 bits rather than wrapping a `Nat`.
-/
structure UInt64 where
/-- Unpack a `UInt64` as a `BitVec 64`.
/-- Unpack a `UInt64` as a `Nat` less than `2^64`.
This function is overridden with a native implementation. -/
toBitVec: BitVec 64
val : Fin UInt64.size
attribute [extern "lean_uint64_of_nat_mk"] UInt64.mk
attribute [extern "lean_uint64_to_nat"] UInt64.toBitVec
attribute [extern "lean_uint64_to_nat"] UInt64.val
/--
Pack a `Nat` less than `2^64` into a `UInt64`.
@@ -2087,7 +2044,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint64_of_nat"]
def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
toBitVec := BitVec.ofNatLt n h
val := { val := n, isLt := h }
set_option bootstrap.genMatcherCode false in
/--
@@ -2098,20 +2055,36 @@ This function is overridden with a native implementation.
def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
match a, b with
| n, m =>
dite (Eq n m)
(fun h => isTrue (h rfl))
(fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
dite (Eq n m) (fun h => isTrue (h rfl)) (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
instance : DecidableEq UInt64 := UInt64.decEq
instance : Inhabited UInt64 where
default := UInt64.ofNatCore 0 (by decide)
/-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
/--
The size of type `USize`, that is, `2^System.Platform.numBits`, which may
be either `2^32` or `2^64` depending on the platform's architecture.
Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the
Lean unifier can solve constraints such as `?m + 1 = USize.size`. Recall that
`numBits` does not reduce to a numeral in the Lean kernel since it is platform
specific. Without this trick, the following definition would be rejected by the
Lean type checker.
```
def one: Fin USize.size := 1
```
Because Lean would fail to synthesize instance `OfNat (Fin USize.size) 1`.
Recall that the `OfNat` instance for `Fin` is
```
instance : OfNat (Fin (n+1)) i where
ofNat := Fin.ofNat i
```
-/
abbrev USize.size : Nat := hAdd (hSub (hPow 2 System.Platform.numBits) 1) 1
theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
show Or (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 4294967296) (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 18446744073709551616) from
match System.Platform.numBits, System.Platform.numBits_eq with
| _, Or.inl rfl => Or.inl (by decide)
| _, Or.inr rfl => Or.inr (by decide)
@@ -2124,20 +2097,21 @@ For example, if running on a 32-bit machine, USize is equivalent to UInt32.
Or on a 64-bit machine, UInt64.
-/
structure USize where
/-- Unpack a `USize` as a `BitVec System.Platform.numBits`.
/-- Unpack a `USize` as a `Nat` less than `USize.size`.
This function is overridden with a native implementation. -/
toBitVec : BitVec System.Platform.numBits
val : Fin USize.size
attribute [extern "lean_usize_of_nat_mk"] USize.mk
attribute [extern "lean_usize_to_nat"] USize.toBitVec
attribute [extern "lean_usize_to_nat"] USize.val
/--
Pack a `Nat` less than `USize.size` into a `USize`.
This function is overridden with a native implementation.
-/
@[extern "lean_usize_of_nat"]
def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize where
toBitVec := BitVec.ofNatLt n h
def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize := {
val := { val := n, isLt := h }
}
set_option bootstrap.genMatcherCode false in
/--
@@ -2148,9 +2122,7 @@ This function is overridden with a native implementation.
def USize.decEq (a b : USize) : Decidable (Eq a b) :=
match a, b with
| n, m =>
dite (Eq n m)
(fun h => isTrue (h rfl))
(fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
dite (Eq n m) (fun h =>isTrue (h rfl)) (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
instance : DecidableEq USize := USize.decEq
@@ -2166,12 +2138,12 @@ This function is overridden with a native implementation.
-/
@[extern "lean_usize_of_nat"]
def USize.ofNat32 (n : @& Nat) (h : LT.lt n 4294967296) : USize where
toBitVec :=
BitVec.ofNatLt n (
match System.Platform.numBits, System.Platform.numBits_eq with
val := {
val := n
isLt := match USize.size, usize_size_eq with
| _, Or.inl rfl => h
| _, Or.inr rfl => Nat.lt_trans h (by decide)
)
}
/--
A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and
@@ -2206,7 +2178,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint32_of_nat"]
def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
{ val := BitVec.ofNatLt n (isValidChar_UInt32 h), valid := h }
{ val := { val := n, isLt := isValidChar_UInt32 h }, valid := h }
/--
Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scalar value,
@@ -2216,7 +2188,7 @@ Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scal
def Char.ofNat (n : Nat) : Char :=
dite (n.isValidChar)
(fun h => Char.ofNatAux n h)
(fun _ => { val := BitVec.ofNatLt 0 (by decide), valid := Or.inl (by decide) })
(fun _ => { val := { val := 0, isLt := by decide }, valid := Or.inl (by decide) })
theorem Char.eq_of_val_eq : {c d : Char}, Eq c.val d.val Eq c d
| _, _, _, _, rfl => rfl
@@ -3476,13 +3448,15 @@ This function is overridden with a native implementation.
-/
@[extern "lean_usize_to_uint64"]
def USize.toUInt64 (u : USize) : UInt64 where
toBitVec := BitVec.ofNatLt u.toBitVec.toNat (
let n, h := u
show LT.lt n _ from
match System.Platform.numBits, System.Platform.numBits_eq, h with
| _, Or.inl rfl, h => Nat.lt_trans h (by decide)
| _, Or.inr rfl, h => h
)
val := {
val := u.val.val
isLt :=
let n, h := u
show LT.lt n _ from
match USize.size, usize_size_eq, h with
| _, Or.inl rfl, h => Nat.lt_trans h (by decide)
| _, Or.inr rfl, h => h
}
/-- An opaque hash mixing operation, used to implement hashing for tuples. -/
@[extern "lean_uint64_mix_hash"]

View File

@@ -135,10 +135,6 @@ Both reduce to `b = false ∧ c = false` via `not_or`.
theorem not_and_of_not_or_not (h : ¬a ¬b) : ¬(a b) := h.elim (mt (·.1)) (mt (·.2))
/-! ## not equal -/
theorem ne_of_apply_ne {α β : Sort _} (f : α β) {x y : α} : f x f y x y :=
mt <| congrArg _
/-! ## Ite -/
@@ -388,17 +384,6 @@ theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' :
end quantifiers
/-! ## membership -/
section Mem
variable [Membership α β] {s t : β} {a b : α}
theorem ne_of_mem_of_not_mem (h : a s) : b s a b := mt fun e => e h
theorem ne_of_mem_of_not_mem' (h : a s) : a t s t := mt fun e => e h
end Mem
/-! ## Nonempty -/
@[simp] theorem nonempty_prop {p : Prop} : Nonempty p p :=

View File

@@ -67,7 +67,6 @@ deriving instance SizeOf for PLift
deriving instance SizeOf for ULift
deriving instance SizeOf for Decidable
deriving instance SizeOf for Fin
deriving instance SizeOf for BitVec
deriving instance SizeOf for UInt8
deriving instance SizeOf for UInt16
deriving instance SizeOf for UInt32

View File

@@ -11,25 +11,22 @@ import Init.Data.Nat.Linear
@[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
cases a; simp_arith
@[simp] protected theorem BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1 := by
cases a; simp_arith
@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by
cases a; simp_arith [UInt8.toNat]
@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt8.toNat, BitVec.toNat]
@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by
cases a; simp_arith [UInt16.toNat]
@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt16.toNat, BitVec.toNat]
@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by
cases a; simp_arith [UInt32.toNat]
@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt32.toNat, BitVec.toNat]
@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by
cases a; simp_arith [UInt64.toNat]
@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt64.toNat, BitVec.toNat]
@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by
cases a; simp_arith [USize.toNat]
@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [USize.toNat, BitVec.toNat]
@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4 := by
@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [Char.toNat]
@[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by

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

@@ -268,9 +268,9 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
inaccessible names to the given names.
-/
macro nextTk:"next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
-- Limit ref variability for incrementality; see Note [Incremental Macros]
withRef arrowTk `(tactic| case%$nextTk _ $args* =>%$arrowTk $tac)
withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
syntax (name := allGoals) "all_goals " tacticSeq : tactic
@@ -495,7 +495,7 @@ macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
`(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))
@@ -1490,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:
@@ -1506,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.

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

@@ -29,6 +29,7 @@ import Lean.Server
import Lean.ScopedEnvExtension
import Lean.DocString
import Lean.DeclarationRange
import Lean.LazyInitExtension
import Lean.LoadDynlib
import Lean.Widget
import Lean.Log

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

@@ -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

@@ -46,7 +46,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
if h' : u.toNat < sz then
u, h'
else
0, by simp; apply Nat.pos_of_isPowerOfTwo h
0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h
@[inline] def reinsertAux (hashFn : α UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
let i, h := mkIdx (hashFn a) data.property

View File

@@ -42,7 +42,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
if h' : u.toNat < sz then
u, h'
else
0, by simp; apply Nat.pos_of_isPowerOfTwo h
0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h
@[inline] def reinsertAux (hashFn : α UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
let i, h := mkIdx (hashFn a) data.property

View File

@@ -54,7 +54,7 @@ structure WorkspaceEditClientCapabilities where
deriving ToJson, FromJson
structure WorkspaceClientCapabilities where
applyEdit? : Option Bool := none
applyEdit: Bool
workspaceEdit? : Option WorkspaceEditClientCapabilities := none
deriving ToJson, FromJson

View File

@@ -7,7 +7,6 @@ prelude
import Init.Data.Array.Basic
import Init.NotationExtra
import Init.Data.ToString.Macro
import Init.Data.UInt.Basic
universe u v w

View File

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
prelude
import Init.Data.Array.BasicAux
import Init.Data.ToString.Macro
import Init.Data.UInt.Basic
namespace Lean
universe u v w w'

View File

@@ -459,7 +459,7 @@ mutual
let z optional (Content.Character <$> CharData)
pure #[y, z]
let xs := #[x] ++ xs.flatMap id |>.filterMap id
let xs := #[x] ++ xs.concatMap id |>.filterMap id
let mut res := #[]
for x in xs do
if res.size > 0 then

View File

@@ -369,13 +369,8 @@ def RecursorVal.getFirstIndexIdx (v : RecursorVal) : Nat :=
def RecursorVal.getFirstMinorIdx (v : RecursorVal) : Nat :=
v.numParams + v.numMotives
/-- The inductive type of the major argument of the recursor. -/
def RecursorVal.getMajorInduct (v : RecursorVal) : Name :=
go v.getMajorIdx v.type
where
go
| 0, e => e.bindingDomain!.getAppFn.constName!
| n+1, e => go n e.bindingBody!
def RecursorVal.getInduct (v : RecursorVal) : Name :=
v.name.getPrefix
inductive QuotKind where
| type -- `Quot`
@@ -472,10 +467,6 @@ def isInductive : ConstantInfo → Bool
| inductInfo _ => true
| _ => false
def isTheorem : ConstantInfo Bool
| thmInfo _ => true
| _ => false
def inductiveVal! : ConstantInfo InductiveVal
| .inductInfo val => val
| _ => panic! "Expected a `ConstantInfo.inductInfo`."

View File

@@ -1150,7 +1150,7 @@ private partial def findMethod? (env : Environment) (structName fieldName : Name
| some _ => some (structName, fullNamePrv)
| none =>
if isStructure env structName then
(getStructureSubobjects env structName).findSome? fun parentStructName => findMethod? env parentStructName fieldName
(getParentStructures env structName).findSome? fun parentStructName => findMethod? env parentStructName fieldName
else
none

View File

@@ -12,18 +12,16 @@ import Lean.Elab.Eval
import Lean.Elab.Command
import Lean.Elab.Open
import Lean.Elab.SetOption
import Init.System.Platform
namespace Lean.Elab.Command
@[builtin_command_elab moduleDoc] def elabModuleDoc : CommandElab := fun stx => do
match stx[1] with
| Syntax.atom _ val =>
let doc := val.extract 0 (val.endPos - 2)
let some range Elab.getDeclarationRange? stx
| return -- must be from partial syntax, ignore
modifyEnv fun env => addMainModuleDoc env doc, range
| _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
match stx[1] with
| Syntax.atom _ val =>
let doc := val.extract 0 (val.endPos - 2)
let range Elab.getDeclarationRange stx
modifyEnv fun env => addMainModuleDoc env doc, range
| _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
modify fun s => { s with
@@ -231,7 +229,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
@[builtin_command_elab «variable»] def elabVariable : CommandElab
| `(variable $binders*) => do
let binders binders.flatMapM replaceBinderAnnotation
let binders binders.concatMapM replaceBinderAnnotation
-- Try to elaborate `binders` for sanity checking
runTermElabM fun _ => Term.withSynthesize <| Term.withAutoBoundImplicit <|
Term.elabBinders binders fun _ => pure ()
@@ -343,14 +341,14 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
if let .none findDeclarationRangesCore? declName then
-- this is only relevant for declarations added without a declaration range
-- in particular `Quot.mk` et al which are added by `init_quot`
addDeclarationRangesFromSyntax declName stx id
addAuxDeclarationRanges declName stx id
addDocString declName ( getDocStringText doc)
| _ => throwUnsupportedSyntax
@[builtin_command_elab Lean.Parser.Command.include] def elabInclude : CommandElab
| `(Lean.Parser.Command.include| include $ids*) => do
let sc getScope
let vars sc.varDecls.flatMapM getBracketedBinderIds
let vars sc.varDecls.concatMapM getBracketedBinderIds
let mut uids := #[]
for id in ids do
if let some idx := vars.findIdx? (· == id.getId) then
@@ -405,16 +403,6 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
includedVars := sc.includedVars.filter (!omittedVars.contains ·) }
| _ => throwUnsupportedSyntax
@[builtin_command_elab version] def elabVersion : CommandElab := fun _ => do
let mut target := System.Platform.target
if target.isEmpty then target := "unknown"
-- Only one should be set, but good to know if multiple are set in error.
let platforms :=
(if System.Platform.isWindows then [" Windows"] else [])
++ (if System.Platform.isOSX then [" macOS"] else [])
++ (if System.Platform.isEmscripten then [" Emscripten"] else [])
logInfo m!"Lean {Lean.versionString}\nTarget: {target}{String.join platforms}"
@[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>
logWarning "using 'exit' to interrupt Lean"

View File

@@ -136,7 +136,7 @@ private def mkFormat (e : Expr) : MetaM Expr := do
if eval.derive.repr.get ( getOptions) then
if let .const name _ := ( whnf ( inferType e)).getAppFn then
try
trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{.ofConstName name}'"
trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{MessageData.ofConstName name}'"
liftCommandElabM do applyDerivingHandlers ``Repr #[name] none
resetSynthInstanceCache
return mkRepr e
@@ -201,9 +201,9 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
discard <| withLocalDeclD `x ty fun x => mkT x
catch _ =>
throw ex
throwError m!"unable to synthesize '{.ofConstName ``MonadEval}' instance \
throwError m!"unable to synthesize '{MessageData.ofConstName ``MonadEval}' instance \
to adapt{indentExpr (← inferType e)}\n\
to '{.ofConstName ``IO}' or '{.ofConstName ``CommandElabM}'."
to '{MessageData.ofConstName ``IO}' or '{MessageData.ofConstName ``CommandElabM}'."
addAndCompileExprForEval declName r (allowSorry := bang)
-- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below.
let r toMessageData <$> evalConst t declName

View File

@@ -135,21 +135,13 @@ open Meta
| _ => Macro.throwUnsupported
@[builtin_macro Lean.Parser.Term.suffices] def expandSuffices : Macro
| `(suffices%$tk $x:ident : $type from $val; $body) => `(have%$tk $x : $type := $body; $val)
| `(suffices%$tk _%$x : $type from $val; $body) => `(have%$tk _%$x : $type := $body; $val)
| `(suffices%$tk $hy:hygieneInfo $type from $val; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
| `(suffices%$tk $x:ident : $type $b:byTactic'; $body) =>
-- Pass on `SourceInfo` of `b` to `have`. This is necessary to display the goal state in the
-- trailing whitespace of `by` and sound since `byTactic` and `byTactic'` are identical.
let b := b.raw.setKind `Lean.Parser.Term.byTactic
`(have%$tk $x : $type := $body; $b:byTactic)
| `(suffices%$tk _%$x : $type $b:byTactic'; $body) =>
let b := b.raw.setKind `Lean.Parser.Term.byTactic
`(have%$tk _%$x : $type := $body; $b:byTactic)
| `(suffices%$tk $hy:hygieneInfo $type $b:byTactic'; $body) =>
let b := b.raw.setKind `Lean.Parser.Term.byTactic
`(have%$tk $hy:hygieneInfo : $type := $body; $b:byTactic)
| _ => Macro.throwUnsupported
| `(suffices%$tk $x:ident : $type from $val; $body) => `(have%$tk $x : $type := $body; $val)
| `(suffices%$tk _%$x : $type from $val; $body) => `(have%$tk _%$x : $type := $body; $val)
| `(suffices%$tk $hy:hygieneInfo $type from $val; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
| `(suffices%$tk $x:ident : $type by%$b $tac:tacticSeq; $body) => `(have%$tk $x : $type := $body; by%$b $tac)
| `(suffices%$tk _%$x : $type by%$b $tac:tacticSeq; $body) => `(have%$tk _%$x : $type := $body; by%$b $tac)
| `(suffices%$tk $hy:hygieneInfo $type by%$b $tac:tacticSeq; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; by%$b $tac)
| _ => Macro.throwUnsupported
open Lean.Parser in
private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do

View File

@@ -10,11 +10,10 @@ namespace Lean.Elab.Term
open Meta
/--
Decompose `e` into `(r, a, b)`.
Decompose `e` into `(r, a, b)`.
Remark: it assumes the last two arguments are explicit.
-/
def getCalcRelation? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
Remark: it assumes the last two arguments are explicit. -/
def getCalcRelation? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
if e.getAppNumArgs < 2 then
return none
else
@@ -69,102 +68,56 @@ where
| .node i k as => return .node i k ( as.mapM go)
| _ => set false; return t
/-- View of a `calcStep`. -/
structure CalcStepView where
ref : Syntax
/-- A relation term like `a ≤ b` -/
term : Term
/-- A proof of `term` -/
proof : Term
deriving Inhabited
def mkCalcFirstStepView (step0 : TSyntax ``calcFirstStep) : TermElabM CalcStepView :=
def getCalcFirstStep (step0 : TSyntax ``calcFirstStep) : TermElabM (TSyntax ``calcStep) :=
withRef step0 do
match step0 with
| `(calcFirstStep| $term:term) => return { ref := step0, term := `($term = _), proof := ``(rfl)}
| `(calcFirstStep| $term := $proof) => return { ref := step0, term, proof}
| `(calcFirstStep| $term:term) =>
`(calcStep| $term = _ := rfl)
| `(calcFirstStep| $term := $proof) =>
`(calcStep| $term := $proof)
| _ => throwUnsupportedSyntax
def mkCalcStepViews (steps : TSyntax ``calcSteps) : TermElabM (Array CalcStepView) :=
def getCalcSteps (steps : TSyntax ``calcSteps) : TermElabM (Array (TSyntax ``calcStep)) :=
match steps with
| `(calcSteps|
$step0:calcFirstStep
$rest*) => do
let mut steps := #[ mkCalcFirstStepView step0]
for step in rest do
let `(calcStep| $term := $proof) := step | throwUnsupportedSyntax
steps := steps.push { ref := step, term, proof }
return steps
| _ => throwUnsupportedSyntax
let step0 getCalcFirstStep step0
pure (#[step0] ++ rest)
| _ => unreachable!
def elabCalcSteps (steps : Array CalcStepView) : TermElabM (Expr × Expr) := do
def elabCalcSteps (steps : TSyntax ``calcSteps) : TermElabM Expr := do
let mut result? := none
let mut prevRhs? := none
for step in steps do
for step in getCalcSteps steps do
let `(calcStep| $pred := $proofTerm) := step | unreachable!
let type elabType <| do
if let some prevRhs := prevRhs? then
annotateFirstHoleWithType step.term ( inferType prevRhs)
annotateFirstHoleWithType pred ( inferType prevRhs)
else
pure step.term
pure pred
let some (_, lhs, rhs) getCalcRelation? type |
throwErrorAt step.term "invalid 'calc' step, relation expected{indentExpr type}"
throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr type}"
if let some prevRhs := prevRhs? then
unless ( isDefEqGuarded lhs prevRhs) do
throwErrorAt step.term "\
invalid 'calc' step, left-hand side is{indentD m!"{lhs} : { inferType lhs}"}\n\
but previous right-hand side is{indentD m!"{prevRhs} : { inferType prevRhs}"}"
let proof withFreshMacroScope do elabTermEnsuringType step.proof type
throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : { inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : { inferType prevRhs}"}" -- "
let proof withFreshMacroScope do elabTermEnsuringType proofTerm type
result? := some <| do
if let some (result, resultType) := result? then
synthesizeSyntheticMVarsUsingDefault
withRef step.term do mkCalcTrans result resultType proof type
withRef pred do mkCalcTrans result resultType proof type
else
pure (proof, type)
prevRhs? := rhs
synthesizeSyntheticMVarsUsingDefault
return result?.get!
def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) : MetaM α := do
let resultType := ( instantiateMVars ( inferType result)).headBeta
let some (r, lhs, rhs) getCalcRelation? resultType | unreachable!
if let some (er, elhs, erhs) getCalcRelation? expectedType then
if isDefEqGuarded r er then
let mut failed := false
unless isDefEqGuarded lhs elhs do
logErrorAt steps[0]!.term m!"\
invalid 'calc' step, left-hand side is{indentD m!"{lhs} : { inferType lhs}"}\n\
but is expected to be{indentD m!"{elhs} : { inferType elhs}"}"
failed := true
unless isDefEqGuarded rhs erhs do
logErrorAt steps.back.term m!"\
invalid 'calc' step, right-hand side is{indentD m!"{rhs} : { inferType rhs}"}\n\
but is expected to be{indentD m!"{erhs} : { inferType erhs}"}"
failed := true
if failed then
throwAbortTerm
throwTypeMismatchError "'calc' expression" expectedType resultType result
/-!
Warning! It is *very* tempting to try to improve `calc` so that it makes use of the expected type
to unify with the LHS and RHS.
Two people have already re-implemented `elabCalcSteps` trying to do so and then reverted the changes,
not being aware of examples like https://github.com/leanprover/lean4/issues/2073
The problem is that the expected type might need to be unfolded to get an accurate LHS and RHS.
(Consider `≤` vs `≥`. Users expect to be able to use `calc` to prove `≥` using chained `≤`!)
Furthermore, the types of the LHS and RHS do not need to be the same (consider `x ∈ S` as a relation),
so we also cannot use the expected LHS and RHS as type hints.
-/
return result?.get!.1
/-- Elaborator for the `calc` term mode variant. -/
@[builtin_term_elab Lean.calc]
def elabCalc : TermElab
| `(calc%$tk $steps:calcSteps), expectedType? => withRef tk do
let steps mkCalcStepViews steps
let (result, _) elabCalcSteps steps
ensureHasTypeWithErrorMsgs expectedType? result
(mkImmedErrorMsg := fun _ => throwCalcFailure steps)
(mkErrorMsg := fun _ => throwCalcFailure steps)
| _, _ => throwUnsupportedSyntax
def elabCalc : TermElab := fun stx expectedType? => do
let steps : TSyntax ``calcSteps := stx[1]
let result elabCalcSteps steps
synthesizeSyntheticMVarsUsingDefault
let result ensureHasType expectedType? result
return result
end Lean.Elab.Term

View File

@@ -532,12 +532,11 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
let mut msgs := ( get).messages
for tree in ( getInfoTrees) do
trace[Elab.info] ( tree.format)
if ( isTracingEnabledFor `Elab.snapshotTree) then
if let some snap := ( read).snap? then
-- We can assume that the root command snapshot is not involved in parallelism yet, so this
-- should be true iff the command supports incrementality
if ( IO.hasFinished snap.new.result) then
liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
if let some snap := ( read).snap? then
-- We can assume that the root command snapshot is not involved in parallelism yet, so this
-- should be true iff the command supports incrementality
if ( IO.hasFinished snap.new.result) then
liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
modify fun st => { st with
messages := initMsgs ++ msgs
infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }
@@ -572,7 +571,7 @@ def getBracketedBinderIds : Syntax → CommandElabM (Array Name)
private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Context := do
let scope := s.scopes.head!
let mut sectionVars := {}
for id in ( scope.varDecls.flatMapM getBracketedBinderIds), uid in scope.varUIds do
for id in ( scope.varDecls.concatMapM getBracketedBinderIds), uid in scope.varUIds do
sectionVars := sectionVars.insert id uid
return {
macroStack := ctx.macroStack
@@ -711,54 +710,21 @@ def addUnivLevel (idStx : Syntax) : CommandElabM Unit := withRef idStx do
else
modifyScope fun scope => { scope with levelNames := id :: scope.levelNames }
def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM ExpandDeclIdResult := do
let currNamespace getCurrNamespace
let currLevelNames getLevelNames
let r Elab.expandDeclId currNamespace currLevelNames declId modifiers
for id in ( ( getScope).varDecls.concatMapM getBracketedBinderIds) do
if id == r.shortName then
throwError "invalid declaration name '{r.shortName}', there is a section variable with the same name"
return r
end Elab.Command
open Elab Command MonadRecDepth
private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) : CoreM α := do
let s : Core.State get
let ctx : Core.Context read
let (a, commandState)
cmd.run {
fileName := ctx.fileName
fileMap := ctx.fileMap
currRecDepth := ctx.currRecDepth
currMacroScope := ctx.currMacroScope
ref := ctx.ref
tacticCache? := none
snap? := none
cancelTk? := ctx.cancelTk?
suppressElabErrors := ctx.suppressElabErrors
} |>.run {
env := s.env
nextMacroScope := s.nextMacroScope
maxRecDepth := ctx.maxRecDepth
ngen := s.ngen
scopes := [{ header := "", opts := ctx.options }]
infoState.enabled := s.infoState.enabled
}
modify fun coreState => { coreState with
env := commandState.env
nextMacroScope := commandState.nextMacroScope
ngen := commandState.ngen
traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
}
if throwOnError then
if let some err := commandState.messages.toArray.find? (·.severity matches .error) then
throwError err.data
modify fun coreState => { coreState with
infoState.trees := coreState.infoState.trees.append commandState.infoState.trees
messages := coreState.messages ++ commandState.messages
}
return a
/--
Lifts an action in `CommandElabM` into `CoreM`, updating the environment,
messages, info trees, traces, the name generator, and macro scopes.
The action is run in a context with an empty message log, empty trace state, and empty info trees.
If `throwOnError` is true, then if the command produces an error message, it is converted into an exception.
In this case, info trees and messages are not carried over.
Lifts an action in `CommandElabM` into `CoreM`, updating the traces and the environment.
Commands that modify the processing of subsequent commands,
such as `open` and `namespace` commands,
@@ -771,9 +737,27 @@ to reset the instance cache.
While the `modifyEnv` function for `MetaM` clears its caches entirely,
`liftCommandElabM` has no way to reset these caches.
-/
def liftCommandElabM (cmd : CommandElabM α) (throwOnError : Bool := true) : CoreM α := do
-- `observing` ensures that if `cmd` throws an exception we still thread state back to `CoreM`.
MonadExcept.ofExcept ( liftCommandElabMCore (observing cmd) throwOnError)
def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
let (a, commandState)
cmd.run {
fileName := getFileName
fileMap := getFileMap
ref := getRef
tacticCache? := none
snap? := none
cancelTk? := ( read).cancelTk?
} |>.run {
env := getEnv
maxRecDepth := getMaxRecDepth
scopes := [{ header := "", opts := getOptions }]
}
modify fun coreState => { coreState with
traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
env := commandState.env
}
if let some err := commandState.messages.toArray.find? (·.severity matches .error) then
throwError err.data
pure a
/--
Given a command elaborator `cmd`, returns a new command elaborator that

View File

@@ -25,19 +25,19 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
if env.contains declName then
addInfo declName
match privateToUserName? declName with
| none => throwError "'{.ofConstName declName true}' has already been declared"
| some declName => throwError "private declaration '{.ofConstName declName true}' has already been declared"
| none => throwError "'{declName}' has already been declared"
| some declName => throwError "private declaration '{declName}' has already been declared"
if isReservedName env declName then
throwError "'{declName}' is a reserved name"
if env.contains (mkPrivateName env declName) then
addInfo (mkPrivateName env declName)
throwError "a private declaration '{.ofConstName declName true}' has already been declared"
throwError "a private declaration '{declName}' has already been declared"
match privateToUserName? declName with
| none => pure ()
| some declName =>
if env.contains declName then
addInfo declName
throwError "a non-private declaration '{.ofConstName declName true}' has already been declared"
throwError "a non-private declaration '{declName}' has already been declared"
/-- Declaration visibility modifier. That is, whether a declaration is regular, protected or private. -/
inductive Visibility where
@@ -57,8 +57,6 @@ inductive RecKind where
/-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/
structure Modifiers where
/-- Input syntax, used for adjusting declaration range (unless missing) -/
stx : TSyntax ``Parser.Command.declModifiers := .missing
docString? : Option String := none
visibility : Visibility := Visibility.regular
isNoncomputable : Bool := false
@@ -123,16 +121,16 @@ section Methods
variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/
def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers := do
let docCommentStx := stx.raw[0]
let attrsStx := stx.raw[1]
let visibilityStx := stx.raw[2]
let noncompStx := stx.raw[3]
let unsafeStx := stx.raw[4]
def elabModifiers (stx : Syntax) : m Modifiers := do
let docCommentStx := stx[0]
let attrsStx := stx[1]
let visibilityStx := stx[2]
let noncompStx := stx[3]
let unsafeStx := stx[4]
let recKind :=
if stx.raw[5].isNone then
if stx[5].isNone then
RecKind.default
else if stx.raw[5][0].getKind == ``Parser.Command.partial then
else if stx[5][0].getKind == ``Parser.Command.partial then
RecKind.partial
else
RecKind.nonrec
@@ -150,7 +148,7 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
| none => pure #[]
| some attrs => elabDeclAttrs attrs
return {
stx, docString?, visibility, recKind, attrs,
docString?, visibility, recKind, attrs,
isUnsafe := !unsafeStx.isNone
isNoncomputable := !noncompStx.isNone
}

View File

@@ -102,16 +102,14 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-- leading_parser "axiom " >> declId >> declSig
let declId := stx[1]
let (binders, typeStx) := expandDeclSig stx[2]
runTermElabM fun vars => do
let scopeLevelNames Term.getLevelNames
let shortName, declName, allUserLevelNames Term.expandDeclId ( getCurrNamespace) scopeLevelNames declId modifiers
addDeclarationRangesForBuiltin declName modifiers.stx stx
Term.withAutoBoundImplicitForbiddenPred (fun n => shortName == n) do
let scopeLevelNames getLevelNames
let _, declName, allUserLevelNames expandDeclId declId modifiers
addDeclarationRanges declName stx
runTermElabM fun vars =>
Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
let type Term.elabType typeStx
Term.synthesizeSyntheticMVarsNoPostponing
let xs Term.addAutoBoundImplicits xs
let type instantiateMVars type
let type mkForallFVars xs type
let type mkForallFVars vars type (usedOnly := true)
@@ -137,6 +135,63 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
compileDecl decl
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
/-
leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
-/
private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
checkValidInductiveModifier modifiers
let (binders, type?) := expandOptDeclSig decl[2]
let declId := decl[1]
let name, declName, levelNames expandDeclId declId modifiers
addDeclarationRanges declName decl
let ctors decl[4].getArgs.mapM fun ctor => withRef ctor do
-- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
let mut ctorModifiers elabModifiers ctor[2]
if let some leadingDocComment := ctor[0].getOptional? then
if ctorModifiers.docString?.isSome then
logErrorAt leadingDocComment "duplicate doc string"
ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString leadingDocComment }
if ctorModifiers.isPrivate && modifiers.isPrivate then
throwError "invalid 'private' constructor in a 'private' inductive datatype"
if ctorModifiers.isProtected && modifiers.isPrivate then
throwError "invalid 'protected' constructor in a 'private' inductive datatype"
checkValidCtorModifier ctorModifiers
let ctorName := ctor.getIdAt 3
let ctorName := declName ++ ctorName
let ctorName withRef ctor[3] <| applyVisibility ctorModifiers.visibility ctorName
let (binders, type?) := expandOptDeclSig ctor[4]
addDocString' ctorName ctorModifiers.docString?
addAuxDeclarationRanges ctorName ctor ctor[3]
return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
let computedFields (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := cf[3], matchAlts := cf[4] }
let classes liftCoreM <| getOptDerivingClasses decl[6]
if decl[3][0].isToken ":=" then
-- https://github.com/leanprover/lean4/issues/5236
withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
"'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
return {
ref := decl
shortDeclName := name
derivingClasses := classes
declId, modifiers, declName, levelNames
binders, type?, ctors
computedFields
}
private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView :=
inductiveSyntaxToView modifiers decl
def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
let v inductiveSyntaxToView modifiers stx
elabInductiveViews #[v]
def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
let modifiers := modifiers.addAttr { name := `class }
let v classInductiveSyntaxToView modifiers stx
elabInductiveViews #[v]
/--
Macro that expands a declaration with a complex name into an explicit `namespace` block.
Implementing this step as a macro means that reuse checking is handled by `elabCommand`.
@@ -159,22 +214,34 @@ def elabDeclaration : CommandElab := fun stx => do
-- only case implementing incrementality currently
elabMutualDef #[stx]
else withoutCommandIncrementality true do
let modifiers : TSyntax ``Parser.Command.declModifiers := stx[0]
if declKind == ``Lean.Parser.Command.«axiom» then
let modifiers elabModifiers modifiers
let modifiers elabModifiers stx[0]
elabAxiom modifiers decl
else if declKind == ``Lean.Parser.Command.«inductive» then
let modifiers elabModifiers modifiers
let modifiers elabModifiers stx[0]
elabInductive modifiers decl
else if declKind == ``Lean.Parser.Command.classInductive then
let modifiers elabModifiers modifiers
let modifiers elabModifiers stx[0]
elabClassInductive modifiers decl
else if declKind == ``Lean.Parser.Command.«structure» then
let modifiers elabModifiers modifiers
let modifiers elabModifiers stx[0]
elabStructure modifiers decl
else
throwError "unexpected declaration"
/-- Return true if all elements of the mutual-block are inductive declarations. -/
private def isMutualInductive (stx : Syntax) : Bool :=
stx[1].getArgs.all fun elem =>
let decl := elem[1]
let declKind := decl.getKind
declKind == `Lean.Parser.Command.inductive
private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
let views elems.mapM fun stx => do
let modifiers elabModifiers stx[0]
inductiveSyntaxToView modifiers stx[1]
elabInductiveViews views
/-- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/
private def isMutualDef (stx : Syntax) : Bool :=
stx[1].getArgs.all fun elem =>
@@ -332,7 +399,7 @@ def elabMutual : CommandElab := fun stx => do
-- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
-- otherwise the info context created by `with_decl_name` will be incomplete and break the
-- call hierarchy
addDeclarationRangesForBuiltin fullId defStx.raw[0] defStx.raw[1]
addDeclarationRanges fullId defStx
elabCommand ( `(
$[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
$defStx:command))

View File

@@ -11,14 +11,12 @@ import Lean.Data.Lsp.Utf16
namespace Lean.Elab
def getDeclarationRange? [Monad m] [MonadFileMap m] (stx : Syntax) : m (Option DeclarationRange) := do
let some range := stx.getRange?
| return none
def getDeclarationRange [Monad m] [MonadFileMap m] (stx : Syntax) : m DeclarationRange := do
let fileMap getFileMap
--let range := fileMap.utf8RangeToLspRange
let pos := fileMap.toPosition range.start
let endPos := fileMap.toPosition range.stop
return some {
let pos := stx.getPos?.getD 0
let endPos := stx.getTailPos?.getD pos |> fileMap.toPosition
let pos := pos |> fileMap.toPosition
return {
pos := pos
charUtf16 := fileMap.leanPosToLspPos pos |>.character
endPos := endPos
@@ -49,31 +47,25 @@ def getDeclarationSelectionRef (stx : Syntax) : Syntax :=
else
stx[0]
/--
Derives and adds declaration ranges from given syntax trees. If `rangeStx` does not have a range,
nothing is added. If `selectionRangeStx` does not have a range, it is defaulted to that of
`rangeStx`.
-/
def addDeclarationRangesFromSyntax [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
(rangeStx : Syntax) (selectionRangeStx : Syntax := .missing) : m Unit := do
-- may fail on partial syntax, ignore in that case
let some range getDeclarationRange? rangeStx | return
let selectionRange (·.getD range) <$> getDeclarationRange? selectionRangeStx
Lean.addDeclarationRanges declName { range, selectionRange }
/--
Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and
`cmdStx` the remaining part of the syntax tree for `declName`.
This method is for the builtin declarations only. User-defined commands should use
`Lean.Elab.addDeclarationRangesFromSyntax` or `Lean.addDeclarationRanges` to store this information
for their commands.
-/
def addDeclarationRangesForBuiltin [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
(modsStx : TSyntax ``Parser.Command.declModifiers) (declStx : Syntax) : m Unit := do
if declStx.getKind == ``Parser.Command.«example» then
Store the `range` and `selectionRange` for `declName` where `stx` is the whole syntax object describing `declName`.
This method is for the builtin declarations only.
User-defined commands should use `Lean.addDeclarationRanges` to store this information for their commands. -/
def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) : m Unit := do
if stx.getKind == ``Parser.Command.«example» then
return ()
let stx := mkNullNode #[modsStx, declStx]
addDeclarationRangesFromSyntax declName stx (getDeclarationSelectionRef declStx)
else
Lean.addDeclarationRanges declName {
range := ( getDeclarationRange stx)
selectionRange := ( getDeclarationRange (getDeclarationSelectionRef stx))
}
/-- Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc. -/
def addAuxDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) (header : Syntax) : m Unit := do
Lean.addDeclarationRanges declName {
range := ( getDeclarationRange stx)
selectionRange := ( getDeclarationRange header)
}
end Lean.Elab

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