Compare commits

..

2 Commits

Author SHA1 Message Date
Kim Morrison
9b4b279ca0 update release_checklist.md 2025-01-04 12:15:49 +11:00
Kim Morrison
8cce6ac6aa feat: add script for generating release notes 2025-01-04 11:58:34 +11:00
440 changed files with 1533 additions and 12466 deletions

File diff suppressed because it is too large Load Diff

View File

@@ -33,9 +33,6 @@ Format of the commit message
- chore (maintain, ex: travis-ci)
- perf (performance improvement, optimization, ...)
Every `feat` or `fix` commit must have a `changelog-*` label, and a commit message
beginning with "This PR " that will be included in the changelog.
``<subject>`` has the following constraints:
- use imperative, present tense: "change" not "changed" nor "changes"
@@ -47,7 +44,6 @@ beginning with "This PR " that will be included in the changelog.
- just as in ``<subject>``, use imperative, present tense
- includes motivation for the change and contrasts with previous
behavior
- If a `changelog-*` label is present, the body must begin with "This PR ".
``<footer>`` is optional and may contain two items:
@@ -64,21 +60,17 @@ Examples
fix: add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel
This PR adds declarations `operator<<` for raw printing.
The actual implementation of these two operators is outside of the
kernel. They are implemented in the file 'library/printer.cpp'.
We declare them in the kernel to prevent the following problem.
Suppose there is a file 'foo.cpp' that does not include 'library/printer.h',
kernel. They are implemented in the file 'library/printer.cpp'. We
declare them in the kernel to prevent the following problem. Suppose
there is a file 'foo.cpp' that does not include 'library/printer.h',
but contains
```cpp
expr a;
...
std::cout << a << "\n";
...
```
expr a;
...
std::cout << a << "\n";
...
The compiler does not generate an error message. It silently uses the
operator bool() to coerce the expression into a Boolean. This produces
counter-intuitive behavior, and may confuse developers.

View File

@@ -49,9 +49,8 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
is represented by the representation of that parameter's type.
For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.
Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
* `Nat` and `Int` are represented by `lean_object *`.
Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
* `Nat` is represented by `lean_object *`.
Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
* Any other type is represented by `lean_object *`.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.

View File

@@ -80,10 +80,3 @@ Unlike most Lean projects, all submodules of the `Lean` module begin with the
`prelude` keyword. This disables the automated import of `Init`, meaning that
developers need to figure out their own subset of `Init` to import. This is done
such that changing files in `Init` doesn't force a full rebuild of `Lean`.
### Testing against Mathlib/Batteries
You can test a Lean PR against Mathlib and Batteries by rebasing your PR
on to `nightly-with-mathlib` branch. (It is fine to force push after rebasing.)
CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN`
that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.

View File

@@ -37,32 +37,16 @@ We'll use `v4.6.0` as the intended release version as a running example.
- Create the tag `v4.6.0` from `master`/`main` and push it.
- Merge the tag `v4.6.0` into the `stable` branch and push it.
- We do this for the repositories:
- [Batteries](https://github.com/leanprover-community/batteries)
- No dependencies
- Toolchain bump PR
- Create and push the tag
- Merge the tag into `stable`
- [lean4checker](https://github.com/leanprover/lean4checker)
- No dependencies
- Toolchain bump PR
- Create and push the tag
- Merge the tag into `stable`
- [doc-gen4](https://github.com/leanprover/doc-gen4)
- Dependencies: exist, but they're not part of the release workflow
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- There is no `stable` branch; skip this step
- [Verso](https://github.com/leanprover/verso)
- Dependencies: exist, but they're not part of the release workflow
- The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- There is no `stable` branch; skip this step
- [Cli](https://github.com/leanprover/lean4-cli)
- [Batteries](https://github.com/leanprover-community/batteries)
- No dependencies
- Toolchain bump PR
- Create and push the tag
- There is no `stable` branch; skip this step
- Merge the tag into `stable`
- [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
- Dependencies: `Batteries`
- Note on versions and branches:
@@ -77,11 +61,18 @@ We'll use `v4.6.0` as the intended release version as a running example.
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- Merge the tag into `stable`
- [import-graph](https://github.com/leanprover-community/import-graph)
- [doc-gen4](https://github.com/leanprover/doc-gen4)
- Dependencies: exist, but they're not part of the release workflow
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- There is no `stable` branch; skip this step
- [plausible](https://github.com/leanprover-community/plausible)
- [Verso](https://github.com/leanprover/verso)
- Dependencies: exist, but they're not part of the release workflow
- The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- There is no `stable` branch; skip this step
- [import-graph](https://github.com/leanprover-community/import-graph)
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- There is no `stable` branch; skip this step
@@ -102,7 +93,6 @@ We'll use `v4.6.0` as the intended release version as a running example.
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- Merge the tag into `stable`
- Run `scripts/release_checklist.py v4.6.0` to check that everything is in order.
- The `v4.6.0` section of `RELEASES.md` is out of sync between
`releases/v4.6.0` and `master`. This should be reconciled:
- Replace the `v4.6.0` section on `master` with the `v4.6.0` section on `releases/v4.6.0`

View File

@@ -0,0 +1,16 @@
We replace the inductive predicate `List.lt` with an upstreamed version of `List.Lex` from Mathlib.
(Previously `Lex.lt` was defined in terms of `<`; now it is generalized to take an arbitrary relation.)
This subtely changes the notion of ordering on `List α`.
`List.lt` was a weaker relation: in particular if `l₁ < l₂`, then
`a :: l₁ < b :: l₂` may hold according to `List.lt` even if `a` and `b` are merely incomparable
(either neither `a < b` nor `b < a`), whereas according to `List.Lex` this would require `a = b`.
When `<` is total, in the sense that `¬ · < ·` is antisymmetric, then the two relations coincide.
Mathlib was already overriding the order instances for `List α`,
so this change should not be noticed by anyone already using Mathlib.
We simultaneously add the boolean valued `List.lex` function, parameterised by a `BEq` typeclass
and an arbitrary `lt` function. This will support the flexibility previously provided for `List.lt`,
via a `==` function which is weaker than strict equality.

View File

@@ -63,8 +63,8 @@ else
fi
# use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
# but do not change sysroot so users can still link against system libs
echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
# when not using the above flags, link GMP dynamically/as usual
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
# do not set `LEAN_CC` for tests

View File

@@ -48,11 +48,12 @@ if [[ -L llvm-host ]]; then
echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
gcp $GMP/lib/libgmp.a stage1/lib/
gcp $LIBUV/lib/libuv.a stage1/lib/
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv'"
else
echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/15.0.1 ${EXTRA_FLAGS:-}'"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
fi
echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
# do not set `LEAN_CC` for tests
echo -n " -DLEAN_TEST_VARS=''"

View File

@@ -43,7 +43,7 @@ echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=
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='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp $(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.
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
# do not set `LEAN_CC` for tests

View File

@@ -1,132 +0,0 @@
#!/usr/bin/env python3
import argparse
import yaml
import requests
import base64
import subprocess
import sys
import os
def parse_repos_config(file_path):
with open(file_path, "r") as f:
return yaml.safe_load(f)["repositories"]
def get_github_token():
try:
import subprocess
result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True)
if result.returncode == 0:
return result.stdout.strip()
except FileNotFoundError:
print("Warning: 'gh' CLI not found. Some API calls may be rate-limited.")
return None
def get_branch_content(repo_url, branch, file_path, github_token):
api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}"
headers = {'Authorization': f'token {github_token}'} if github_token else {}
response = requests.get(api_url, headers=headers)
if response.status_code == 200:
content = response.json().get("content", "")
content = content.replace("\n", "")
try:
return base64.b64decode(content).decode('utf-8').strip()
except Exception:
return None
return None
def tag_exists(repo_url, tag_name, github_token):
api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/git/refs/tags/{tag_name}"
headers = {'Authorization': f'token {github_token}'} if github_token else {}
response = requests.get(api_url, headers=headers)
return response.status_code == 200
def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token):
# First get the commit SHA for the tag
api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
headers = {'Authorization': f'token {github_token}'} if github_token else {}
# Get tag's commit SHA
tag_response = requests.get(f"{api_base}/git/refs/tags/{tag_name}", headers=headers)
if tag_response.status_code != 200:
return False
tag_sha = tag_response.json()['object']['sha']
# Get commits on stable branch containing this SHA
commits_response = requests.get(
f"{api_base}/commits?sha={stable_branch}&per_page=100",
headers=headers
)
if commits_response.status_code != 200:
return False
# Check if any commit in stable's history matches our tag's SHA
stable_commits = [commit['sha'] for commit in commits_response.json()]
return tag_sha in stable_commits
def parse_version(version_str):
# Remove 'v' prefix and split into components
# Handle Lean toolchain format (leanprover/lean4:v4.x.y)
if ':' in version_str:
version_str = version_str.split(':')[1]
version = version_str.lstrip('v')
# Handle release candidates by removing -rc part for comparison
version = version.split('-')[0]
return tuple(map(int, version.split('.')))
def is_version_gte(version1, version2):
"""Check if version1 >= version2"""
return parse_version(version1) >= parse_version(version2)
def is_release_candidate(version):
return "-rc" in version
def main():
github_token = get_github_token()
if len(sys.argv) != 2:
print("Usage: python3 release_checklist.py <toolchain>")
sys.exit(1)
toolchain = sys.argv[1]
with open(os.path.join(os.path.dirname(__file__), "release_repos.yml")) as f:
repos = yaml.safe_load(f)["repositories"]
for repo in repos:
name = repo["name"]
url = repo["url"]
branch = repo["branch"]
check_stable = repo["stable-branch"]
check_tag = repo.get("toolchain-tag", True)
print(f"\nRepository: {name}")
# Check if branch is on at least the target toolchain
lean_toolchain_content = get_branch_content(url, branch, "lean-toolchain", github_token)
if lean_toolchain_content is None:
print(f" ❌ No lean-toolchain file found in {branch} branch")
continue
on_target_toolchain = is_version_gte(lean_toolchain_content.strip(), toolchain)
if not on_target_toolchain:
print(f" ❌ Not on target toolchain (needs ≥ {toolchain}, but {branch} is on {lean_toolchain_content.strip()})")
continue
print(f" ✅ On compatible toolchain (>= {toolchain})")
# Only check for tag if toolchain-tag is true
if check_tag:
if not tag_exists(url, toolchain, github_token):
print(f" ❌ Tag {toolchain} does not exist")
continue
print(f" ✅ Tag {toolchain} exists")
# Only check merging into stable if stable-branch is true and not a release candidate
if check_stable and not is_release_candidate(toolchain):
if not is_merged_into_stable(url, toolchain, "stable", github_token):
print(f" ❌ Tag {toolchain} is not merged into stable")
continue
print(f" ✅ Tag {toolchain} is merged into stable")
if __name__ == "__main__":
main()

View File

@@ -1,86 +0,0 @@
repositories:
- name: Batteries
url: https://github.com/leanprover-community/batteries
toolchain-tag: true
stable-branch: true
branch: main
dependencies: []
- name: lean4checker
url: https://github.com/leanprover/lean4checker
toolchain-tag: true
stable-branch: true
branch: master
dependencies: []
- name: doc-gen4
url: https://github.com/leanprover/doc-gen4
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: Verso
url: https://github.com/leanprover/verso
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: Cli
url: https://github.com/leanprover/lean4-cli
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: ProofWidgets4
url: https://github.com/leanprover-community/ProofWidgets4
toolchain-tag: false
stable-branch: false
branch: main
dependencies:
- Batteries
- name: Aesop
url: https://github.com/leanprover-community/aesop
toolchain-tag: true
stable-branch: true
branch: master
dependencies:
- Batteries
- name: import-graph
url: https://github.com/leanprover-community/import-graph
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: plausible
url: https://github.com/leanprover-community/plausible
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: Mathlib
url: https://github.com/leanprover-community/mathlib4
toolchain-tag: true
stable-branch: true
branch: master
dependencies:
- Aesop
- ProofWidgets4
- lean4checker
- Batteries
- doc-gen4
- import-graph
- name: REPL
url: https://github.com/leanprover-community/repl
toolchain-tag: true
stable-branch: true
branch: master
dependencies:
- Mathlib

View File

@@ -37,4 +37,3 @@ import Init.MacroTrace
import Init.Grind
import Init.While
import Init.Syntax
import Init.Internal

View File

@@ -150,10 +150,6 @@ See the `simp` tactic for more information. -/
syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
that would be sufficient to close the goal. See the `simp?` tactic for more information. -/
syntax (name := simpTrace) "simp?" optConfig (discharger)? (&" only")? (simpArgs)? : conv
/--
`dsimp` is the definitional simplifier in `conv`-mode. It differs from `simp` in that it only
applies theorems that hold by reflexivity.
@@ -171,9 +167,6 @@ example (a : Nat): (0 + 0) = a - a := by
syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
(" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
@[inherit_doc simpTrace]
syntax (name := dsimpTrace) "dsimp?" optConfig (&" only")? (dsimpArgs)? : conv
/-- `simp_match` simplifies match expressions. For example,
```
match [a, b] with

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Kim Morrison
Authors: Mario Carneiro
-/
prelude
import Init.Data.Nat.Lemmas
@@ -36,8 +36,6 @@ namespace Array
@[simp] theorem mem_toList_iff (a : α) (l : Array α) : a l.toList a l := by
cases l <;> simp
@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
/-! ### empty -/
@[simp] theorem empty_eq {xs : Array α} : #[] = xs xs = #[] := by
@@ -124,8 +122,6 @@ theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a
· rintro rfl, rfl
rfl
theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
theorem exists_push_of_ne_empty {xs : Array α} (h : xs #[]) :
(ys : Array α) (a : α), xs = ys.push a := by
rcases xs with xs
@@ -958,18 +954,13 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
rw [Bool.eq_iff_iff]
simp +contextual
private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] a == b := by
intro h
have : isEqv #[a] #[b] BEq.beq = true := h
simp [isEqv, isEqvAux] at this
assumption
@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ReflBEq α := by
constructor
· intro h
constructor
intro a
apply beq_of_beq_singleton
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
@@ -982,9 +973,11 @@ private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a ==
· intro a b h
apply singleton_inj.1
apply eq_of_beq
simpa [instBEq, isEqv, isEqvAux]
simp only [instBEq, isEqv, isEqvAux]
simpa
· intro a
apply beq_of_beq_singleton
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
@@ -1003,7 +996,54 @@ private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a ==
cases l₂
simp
/-! ### map -/
/-! Content below this point has not yet been aligned with `List`. -/
theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
-- This is a duplicate of `List.toArray_toList`.
-- It's confusing to guess which namespace this theorem should live in,
-- so we provide both.
@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
@[deprecated size_toArray (since := "2024-12-11")]
theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
theorem foldrM_push [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
/--
Variant of `foldrM_push` with `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
-/
@[simp] theorem foldrM_push' [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α)
{start} (h : start = arr.size + 1) :
(arr.push a).foldrM f init start = f a init >>= arr.foldrM f := by
simp [ foldrM_push, h]
theorem foldr_push (f : α β β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
/--
Variant of `foldr_push` with the `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
-/
@[simp] theorem foldr_push' (f : α β β) (init : β) (arr : Array α) (a : α) {start}
(h : start = arr.size + 1) : (arr.push a).foldr f init start = arr.foldr f (f a init) :=
foldrM_push' _ _ _ _ h
/-- A more efficient version of `arr.toList.reverse`. -/
@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
rw [toListRev, foldl_toList, List.foldr_reverse, List.foldr_cons_nil]
theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
@@ -1027,505 +1067,15 @@ where
induction l generalizing arr <;> simp [*]
simp [H]
@[simp] theorem _root_.List.map_toArray (f : α β) (l : List α) :
l.toArray.map f = (l.map f).toArray := by
apply ext'
simp
@[simp] theorem size_map (f : α β) (arr : Array α) : (arr.map f).size = arr.size := by
simp only [ length_toList]
simp
@[simp] theorem getElem_map (f : α β) (a : Array α) (i : Nat) (hi : i < (a.map f).size) :
(a.map f)[i] = f (a[i]'(by simpa using hi)) := by
cases a
simp
@[simp] theorem getElem?_map (f : α β) (as : Array α) (i : Nat) :
(as.map f)[i]? = as[i]?.map f := by
simp [getElem?_def]
@[simp] theorem mapM_empty [Monad m] (f : α m β) : mapM f #[] = pure #[] := by
rw [mapM, mapM.map]; rfl
@[simp] theorem map_empty (f : α β) : map f #[] = #[] := mapM_empty f
@[simp] theorem map_push {f : α β} {as : Array α} {x : α} :
(as.push x).map f = (as.map f).push (f x) := by
ext
· simp
· simp only [getElem_map, getElem_push, size_map]
split <;> rfl
@[simp] theorem map_id_fun : map (id : α α) = id := by
funext l
induction l <;> simp_all
/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
theorem map_id (l : Array α) : map (id : α α) l = l := by
cases l <;> simp_all
/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
theorem map_id' (l : Array α) : map (fun (a : α) => a) l = l := map_id l
/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
theorem map_id'' {f : α α} (h : x, f x = x) (l : Array α) : map f l = l := by
simp [show f = id from funext h]
theorem map_singleton (f : α β) (a : α) : map f #[a] = #[f a] := rfl
@[simp] theorem mem_map {f : α β} {l : Array α} : b l.map f a, a l f a = b := by
simp only [mem_def, toList_map, List.mem_map]
theorem exists_of_mem_map (h : b map f l) : a, a l f a = b := mem_map.1 h
theorem mem_map_of_mem (f : α β) (h : a l) : f a map f l := mem_map.2 _, h, rfl
theorem forall_mem_map {f : α β} {l : Array α} {P : β Prop} :
( (i) (_ : i l.map f), P i) (j) (_ : j l), P (f j) := by
simp
@[simp] theorem map_inj_left {f g : α β} : map f l = map g l a l, f a = g a := by
cases l <;> simp_all
theorem map_congr_left (h : a l, f a = g a) : map f l = map g l :=
map_inj_left.2 h
theorem map_inj : map f = map g f = g := by
constructor
· intro h; ext a; replace h := congrFun h #[a]; simpa using h
· intro h; subst h; rfl
@[simp] theorem map_eq_empty_iff {f : α β} {l : Array α} : map f l = #[] l = #[] := by
cases l
simp
theorem eq_empty_of_map_eq_empty {f : α β} {l : Array α} (h : map f l = #[]) : l = #[] :=
map_eq_empty_iff.mp h
theorem map_eq_push_iff {f : α β} {l : Array α} {l₂ : Array β} {b : β} :
map f l = l₂.push b l₁ a, l = l₁.push a map f l₁ = l₂ f a = b := by
rcases l with l
rcases l₂ with l₂
simp only [List.map_toArray, List.push_toArray, mk.injEq, List.map_eq_append_iff]
constructor
· rintro l₁, l₂, rfl, rfl, h
simp only [List.map_eq_singleton_iff] at h
obtain a, rfl, rfl := h
refine l₁.toArray, a, by simp
· rintro l₁, a, h₁, h₂, rfl
refine l₁, [a], by simp_all
@[simp] theorem map_eq_singleton_iff {f : α β} {l : Array α} {b : β} :
map f l = #[b] a, l = #[a] f a = b := by
cases l
simp
theorem map_eq_map_iff {f g : α β} {l : Array α} :
map f l = map g l a l, f a = g a := by
cases l <;> simp_all
theorem map_eq_iff : map f l = l' i : Nat, l'[i]? = l[i]?.map f := by
cases l
cases l'
simp [List.map_eq_iff]
theorem map_eq_foldl (f : α β) (l : Array α) :
map f l = foldl (fun bs a => bs.push (f a)) #[] l := by
simpa using mapM_eq_foldlM (m := Id) f l
@[simp] theorem map_set {f : α β} {l : Array α} {i : Nat} {h : i < l.size} {a : α} :
(l.set i a).map f = (l.map f).set i (f a) (by simpa using h) := by
cases l
simp
@[simp] theorem map_setIfInBounds {f : α β} {l : Array α} {i : Nat} {a : α} :
(l.setIfInBounds i a).map f = (l.map f).setIfInBounds i (f a) := by
cases l
simp
@[simp] theorem map_pop {f : α β} {l : Array α} : l.pop.map f = (l.map f).pop := by
cases l
simp
@[simp] theorem back?_map {f : α β} {l : Array α} : (l.map f).back? = l.back?.map f := by
cases l
simp
@[simp] theorem map_map {f : α β} {g : β γ} {as : Array α} :
(as.map f).map g = as.map (g f) := by
cases as; simp
theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
rw [mapM_eq_foldlM, foldlM_toList, List.foldrM_reverse]
conv => rhs; rw [ List.reverse_reverse arr.toList]
induction arr.toList.reverse with
| nil => simp
| cons a l ih => simp [ih]
@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
toList <$> arr.mapM f = arr.toList.mapM f := by
simp [mapM_eq_mapM_toList]
@[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]
theorem mapM_map_eq_foldl (as : Array α) (f : α β) (i) :
mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
unfold mapM.map
split <;> rename_i h
· simp only [Id.bind_eq]
dsimp [foldl, Id.run, foldlM]
rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
-- Calling `split` here gives a bad goal.
have : size as - i = Nat.succ (size as - i - 1) := by omega
rw [this]
simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
· dsimp [foldl, Id.run, foldlM]
rw [dif_pos (by omega), foldlM.loop, dif_neg h]
rfl
termination_by as.size - i
/-! ### filter -/
@[congr]
theorem filter_congr {as bs : Array α} (h : as = bs)
{f : α Bool} {g : α Bool} (h' : f = g) {start stop start' stop' : Nat}
(h₁ : start = start') (h₂ : stop = stop') :
filter f as start stop = filter g bs start' stop' := by
congr
@[simp] theorem toList_filter' (p : α Bool) (l : Array α) (h : stop = l.size) :
(l.filter p 0 stop).toList = l.toList.filter p := by
subst h
dsimp only [filter]
rw [ foldl_toList]
generalize l.toList = l
suffices a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
a.toList ++ List.filter p l by
simpa using this #[]
induction l with simp
| cons => split <;> simp [*]
theorem toList_filter (p : α Bool) (l : Array α) :
(l.filter p).toList = l.toList.filter p := by
simp
@[simp] theorem _root_.List.filter_toArray' (p : α Bool) (l : List α) (h : stop = l.length) :
l.toArray.filter p 0 stop = (l.filter p).toArray := by
apply ext'
simp [h]
theorem _root_.List.filter_toArray (p : α Bool) (l : List α) :
l.toArray.filter p = (l.filter p).toArray := by
simp
@[simp] theorem filter_push_of_pos {p : α Bool} {a : α} {l : Array α}
(h : p a) (w : stop = l.size + 1):
(l.push a).filter p 0 stop = (l.filter p).push a := by
subst w
rcases l with l
simp [h]
@[simp] theorem filter_push_of_neg {p : α Bool} {a : α} {l : Array α}
(h : ¬p a) (w : stop = l.size + 1) :
(l.push a).filter p 0 stop = l.filter p := by
subst w
rcases l with l
simp [h]
theorem filter_push {p : α Bool} {a : α} {l : Array α} :
(l.push a).filter p = if p a then (l.filter p).push a else l.filter p := by
split <;> simp [*]
theorem size_filter_le (p : α Bool) (l : Array α) :
(l.filter p).size l.size := by
rcases l with l
simpa using List.length_filter_le p l
@[simp] theorem filter_eq_self {p : α Bool} {l : Array α} :
filter p l = l a l, p a := by
rcases l with l
simp
@[simp] theorem filter_size_eq_size {p : α Bool} {l : Array α} :
(filter p l).size = l.size a l, p a := by
rcases l with l
simp
@[simp] theorem mem_filter {p : α Bool} {l : Array α} {a : α} :
a filter p l a l p a := by
rcases l with l
simp
@[simp] theorem filter_eq_empty_iff {p : α Bool} {l : Array α} :
filter p l = #[] a, a l ¬p a := by
rcases l with l
simp
theorem forall_mem_filter {p : α Bool} {l : Array α} {P : α Prop} :
( (i) (_ : i l.filter p), P i) (j) (_ : j l), p j P j := by
simp
@[simp] theorem filter_filter (q) (l : Array α) :
filter p (filter q l) = filter (fun a => p a && q a) l := by
apply ext'
simp only [toList_filter, List.filter_filter]
theorem foldl_filter (p : α Bool) (f : β α β) (l : Array α) (init : β) :
(l.filter p).foldl f init = l.foldl (fun x y => if p y then f x y else x) init := by
rcases l with l
rw [List.filter_toArray]
simp [List.foldl_filter]
theorem foldr_filter (p : α Bool) (f : α β β) (l : Array α) (init : β) :
(l.filter p).foldr f init = l.foldr (fun x y => if p x then f x y else y) init := by
rcases l with l
rw [List.filter_toArray]
simp [List.foldr_filter]
theorem filter_map (f : β α) (l : Array β) : filter p (map f l) = map f (filter (p f) l) := by
rcases l with l
simp [List.filter_map]
theorem map_filter_eq_foldl (f : α β) (p : α Bool) (l : Array α) :
map f (filter p l) = foldl (fun y x => bif p x then y.push (f x) else y) #[] l := by
rcases l with l
apply ext'
simp only [size_toArray, List.filter_toArray', List.map_toArray, List.foldl_toArray']
rw [ List.reverse_reverse l]
generalize l.reverse = l
simp only [List.filter_reverse, List.map_reverse, List.foldl_reverse]
induction l with
| nil => rfl
| cons x l ih =>
simp only [List.filter_cons, List.foldr_cons]
split <;> simp_all
@[simp] theorem filter_append {p : α Bool} (l₁ l₂ : Array α) :
filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂ := by
rcases l₁ with l₁
rcases l₂ with l₂
simp [List.filter_append]
theorem filter_eq_append_iff {p : α Bool} :
filter p l = L₁ ++ L₂ l₁ l₂, l = l₁ ++ l₂ filter p l₁ = L₁ filter p l₂ = L₂ := by
rcases l with l
rcases L₁ with L₁
rcases L₂ with L₂
simp only [size_toArray, List.filter_toArray', List.append_toArray, mk.injEq,
List.filter_eq_append_iff]
constructor
· rintro l₁, l₂, rfl, rfl, rfl
refine l₁.toArray, l₂.toArray, by simp
· rintro l₁, l₂, h₁, h₂, h₃
refine l₁, l₂, by simp_all
theorem filter_eq_push_iff {p : α Bool} {l l' : Array α} {a : α} :
filter p l = l'.push a
l₁ l₂, l = l₁.push a ++ l₂ filter p l₁ = l' p a ( x, x l₂ ¬p x) := by
rcases l with l
rcases l' with l'
simp only [size_toArray, List.filter_toArray', List.push_toArray, mk.injEq, Bool.not_eq_true]
rw [ List.reverse_inj]
simp only [ List.filter_reverse]
simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
List.singleton_append]
rw [List.filter_eq_cons_iff]
constructor
· rintro l₁, l₂, h₁, h₂, h₃, h₄
refine l₂.reverse.toArray, l₁.reverse.toArray, by simp_all
· rintro l₁, l₂, h₁, h₂, h₃, h₄
refine l₂.reverse, l₁.reverse, by simp_all
@[deprecated filter_map (since := "2024-06-15")] abbrev map_filter := @filter_map
theorem mem_of_mem_filter {a : α} {l} (h : a filter p l) : a l :=
(mem_filter.mp h).1
/-! ### filterMap -/
@[congr]
theorem filterMap_congr {as bs : Array α} (h : as = bs)
{f : α Option β} {g : α Option β} (h' : f = g) {start stop start' stop' : Nat}
(h₁ : start = start') (h₂ : stop = stop') :
filterMap f as start stop = filterMap g bs start' stop' := by
congr
@[simp] theorem toList_filterMap' (f : α Option β) (l : Array α) (w : stop = l.size) :
(l.filterMap f 0 stop).toList = l.toList.filterMap f := by
subst w
dsimp only [filterMap, filterMapM]
rw [ foldlM_toList]
generalize l.toList = l
have this : a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
a.toList ++ List.filterMap f l := ?_
exact this #[]
induction l
· simp_all [Id.run]
· simp_all [Id.run, List.filterMap_cons]
split <;> simp_all
theorem toList_filterMap (f : α Option β) (l : Array α) :
(l.filterMap f).toList = l.toList.filterMap f := by
simp [toList_filterMap']
@[simp] theorem _root_.List.filterMap_toArray' (f : α Option β) (l : List α) (h : stop = l.length) :
l.toArray.filterMap f 0 stop = (l.filterMap f).toArray := by
apply ext'
simp [h]
theorem _root_.List.filterMap_toArray (f : α Option β) (l : List α) :
l.toArray.filterMap f = (l.filterMap f).toArray := by
simp
@[simp] theorem filterMap_push_none {f : α Option β} {a : α} {l : Array α}
(h : f a = none) (w : stop = l.size + 1) :
filterMap f (l.push a) 0 stop = filterMap f l := by
subst w
rcases l with l
simp [h]
@[simp] theorem filterMap_push_some {f : α Option β} {a : α} {l : Array α} {b : β}
(h : f a = some b) (w : stop = l.size + 1) :
filterMap f (l.push a) 0 stop = (filterMap f l).push b := by
subst w
rcases l with l
simp [h]
@[simp] theorem filterMap_eq_map (f : α β) : filterMap (some f) = map f := by
funext l
cases l
simp
theorem filterMap_some_fun : filterMap (some : α Option α) = id := by
funext l
cases l
simp
@[simp] theorem filterMap_some (l : Array α) : filterMap some l = l := by
cases l
simp
theorem map_filterMap_some_eq_filterMap_isSome (f : α Option β) (l : Array α) :
(l.filterMap f).map some = (l.map f).filter fun b => b.isSome := by
cases l
simp [List.map_filterMap_some_eq_filter_map_isSome]
theorem size_filterMap_le (f : α Option β) (l : Array α) :
(filterMap f l).size l.size := by
cases l
simp [List.length_filterMap_le]
@[simp] theorem filterMap_size_eq_size {l} :
(filterMap f l).size = l.size a, a l (f a).isSome := by
cases l
simp [List.filterMap_length_eq_length]
@[simp]
theorem filterMap_eq_filter (p : α Bool) :
filterMap (Option.guard (p ·)) = filter p := by
funext l
cases l
simp
theorem filterMap_filterMap (f : α Option β) (g : β Option γ) (l : Array α) :
filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l := by
cases l
simp [List.filterMap_filterMap]
theorem map_filterMap (f : α Option β) (g : β γ) (l : Array α) :
map g (filterMap f l) = filterMap (fun x => (f x).map g) l := by
cases l
simp [List.map_filterMap]
@[simp] theorem filterMap_map (f : α β) (g : β Option γ) (l : Array α) :
filterMap g (map f l) = filterMap (g f) l := by
cases l
simp [List.filterMap_map]
theorem filter_filterMap (f : α Option β) (p : β Bool) (l : Array α) :
filter p (filterMap f l) = filterMap (fun x => (f x).filter p) l := by
cases l
simp [List.filter_filterMap]
theorem filterMap_filter (p : α Bool) (f : α Option β) (l : Array α) :
filterMap f (filter p l) = filterMap (fun x => if p x then f x else none) l := by
cases l
simp [List.filterMap_filter]
@[simp] theorem mem_filterMap {f : α Option β} {l : Array α} {b : β} :
b filterMap f l a, a l f a = some b := by
simp only [mem_def, toList_filterMap, List.mem_filterMap]
theorem forall_mem_filterMap {f : α Option β} {l : Array α} {P : β Prop} :
( (i) (_ : i filterMap f l), P i) (j) (_ : j l) (b), f j = some b P b := by
simp only [mem_filterMap, forall_exists_index, and_imp]
rw [forall_comm]
apply forall_congr'
intro a
rw [forall_comm]
@[simp] theorem filterMap_append {α β : Type _} (l l' : Array α) (f : α Option β) :
filterMap f (l ++ l') = filterMap f l ++ filterMap f l' := by
cases l
cases l'
simp
theorem map_filterMap_of_inv (f : α Option β) (g : β α) (H : x : α, (f x).map g = some x)
(l : Array α) : map g (filterMap f l) = l := by simp only [map_filterMap, H, filterMap_some, id]
theorem forall_none_of_filterMap_eq_empty (h : filterMap f xs = #[]) : x xs, f x = none := by
cases xs
simpa using h
@[simp] theorem filterMap_eq_nil_iff {l} : filterMap f l = #[] a, a l f a = none := by
cases l
simp
theorem filterMap_eq_push_iff {f : α Option β} {l : Array α} {l' : Array β} {b : β} :
filterMap f l = l'.push b l₁ a l₂,
l = l₁.push a ++ l₂ filterMap f l₁ = l' f a = some b ( x, x l₂ f x = none) := by
rcases l with l
rcases l' with l'
simp only [size_toArray, List.filterMap_toArray', List.push_toArray, mk.injEq]
rw [ List.reverse_inj]
simp only [ List.filterMap_reverse]
simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
List.singleton_append]
rw [List.filterMap_eq_cons_iff]
constructor
· rintro l₁, a, l₂, h₁, h₂, h₃, h₄
refine l₂.reverse.toArray, a, l₁.reverse.toArray, by simp_all
· rintro l₁, a, l₂, h₁, h₂, h₃, h₄
refine l₂.reverse, a, l₁.reverse, by simp_all
/-! Content below this point has not yet been aligned with `List`. -/
theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
-- This is a duplicate of `List.toArray_toList`.
-- It's confusing to guess which namespace this theorem should live in,
-- so we provide both.
@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
@[deprecated size_toArray (since := "2024-12-11")]
theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
/-- A more efficient version of `arr.toList.reverse`. -/
@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
rw [toListRev, foldl_toList, List.foldr_reverse, List.foldr_cons_nil]
@[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
@[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
@@ -1541,6 +1091,7 @@ theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) :
(l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G := by
induction l generalizing acc <;> simp [*]
/-! # uset -/
attribute [simp] uset
@@ -1716,16 +1267,18 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
(h : i j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
simp only [set, getElem_toList, List.getElem_set_ne h]
private theorem fin_cast_val (e : n = n') (i : Fin n) : e i = i.1, e i.2 := by cases e; rfl
theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by
simp [swap]
simp [swap, fin_cast_val]
@[simp] theorem toList_swap (a : Array α) (i j : Nat) (hi hj) :
(a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def]
theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? =
if j = k then some a[i] else if i = k then some a[j] else a[k]? := by
simp [swap_def, get?_set]
simp [swap_def, get?_set, getElem_fin_eq_getElem_toList]
@[simp] theorem swapAt_def (a : Array α) (i : Nat) (v : α) (hi) :
a.swapAt i v hi = (a[i], a.set i v) := rfl
@@ -1840,90 +1393,6 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
true_and, Nat.not_lt] at h
rw [List.getElem?_eq_none_iff.2 _, List.getElem?_eq_none_iff.2 (a.toList.length_reverse _)]
end Array
open Array
namespace List
@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
apply ext'
simp only [toList_reverse]
end List
namespace Array
/-! ### foldlM and foldrM -/
theorem foldlM_append [Monad m] [LawfulMonad m] (f : β α m β) (b) (l l' : Array α) :
(l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
cases l
cases l'
rw [List.append_toArray]
simp
/-- Variant of `foldM_append` with `h : stop = (l ++ l').size`. -/
@[simp] theorem foldlM_append' [Monad m] [LawfulMonad m] (f : β α m β) (b) (l l' : Array α)
(h : stop = (l ++ l').size) :
(l ++ l').foldlM f b 0 stop = l.foldlM f b >>= l'.foldlM f := by
subst h
rw [foldlM_append]
theorem foldrM_push [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
/--
Variant of `foldrM_push` with `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
-/
@[simp] theorem foldrM_push' [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α)
{start} (h : start = arr.size + 1) :
(arr.push a).foldrM f init start = f a init >>= arr.foldrM f := by
simp [ foldrM_push, h]
theorem foldl_eq_foldlM (f : β α β) (b) (l : Array α) :
l.foldl f b = l.foldlM (m := Id) f b := by
cases l
simp [List.foldl_eq_foldlM]
theorem foldr_eq_foldrM (f : α β β) (b) (l : Array α) :
l.foldr f b = l.foldrM (m := Id) f b := by
cases l
simp [List.foldr_eq_foldrM]
@[simp] theorem id_run_foldlM (f : β α Id β) (b) (l : Array α) :
Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
@[simp] theorem id_run_foldrM (f : α β Id β) (b) (l : Array α) :
Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
/-! ### foldl and foldr -/
theorem foldr_push (f : α β β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
/--
Variant of `foldr_push` with the `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
-/
@[simp] theorem foldr_push' (f : α β β) (init : β) (arr : Array α) (a : α) {start}
(h : start = arr.size + 1) : (arr.push a).foldr f init start = arr.foldr f (f a init) :=
foldrM_push' _ _ _ _ h
@[simp] theorem foldl_push_eq_append (l l' : Array α) : l.foldl push l' = l' ++ l := by
cases l
cases l'
simp
@[simp] theorem foldr_flip_push_eq_append (l l' : Array α) :
l.foldr (fun x y => push y x) l' = l' ++ l.reverse := by
cases l
cases l'
simp
/-! ### take -/
@[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by
@@ -2036,6 +1505,22 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β}
as.foldr f a start stop = bs.foldr g b start' stop' := by
congr
theorem foldl_eq_foldlM (f : β α β) (b) (l : Array α) :
l.foldl f b = l.foldlM (m := Id) f b := by
cases l
simp [List.foldl_eq_foldlM]
theorem foldr_eq_foldrM (f : α β β) (b) (l : Array α) :
l.foldr f b = l.foldrM (m := Id) f b := by
cases l
simp [List.foldr_eq_foldrM]
@[simp] theorem id_run_foldlM (f : β α Id β) (b) (l : Array α) :
Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
@[simp] theorem id_run_foldrM (f : α β Id β) (b) (l : Array α) :
Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
theorem foldl_hom (f : α₁ α₂) (g₁ : α₁ β α₁) (g₂ : α₂ β α₂) (l : Array β) (init : α₁)
(H : x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
cases l
@@ -2050,7 +1535,45 @@ theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ :
/-! ### map -/
@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")]
@[simp] theorem mem_map {f : α β} {l : Array α} : b l.map f a, a l f a = b := by
simp only [mem_def, toList_map, List.mem_map]
theorem exists_of_mem_map (h : b map f l) : a, a l f a = b := mem_map.1 h
theorem mem_map_of_mem (f : α β) (h : a l) : f a map f l := mem_map.2 _, h, rfl
theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
rw [mapM_eq_foldlM, foldlM_toList, List.foldrM_reverse]
conv => rhs; rw [ List.reverse_reverse arr.toList]
induction arr.toList.reverse with
| nil => simp
| cons a l ih => simp [ih]
@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
toList <$> arr.mapM f = arr.toList.mapM f := by
simp [mapM_eq_mapM_toList]
theorem mapM_map_eq_foldl (as : Array α) (f : α β) (i) :
mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
unfold mapM.map
split <;> rename_i h
· simp only [Id.bind_eq]
dsimp [foldl, Id.run, foldlM]
rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
-- Calling `split` here gives a bad goal.
have : size as - i = Nat.succ (size as - i - 1) := by omega
rw [this]
simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
· dsimp [foldl, Id.run, foldlM]
rw [dif_pos (by omega), foldlM.loop, dif_neg h]
rfl
termination_by as.size - i
theorem map_eq_foldl (as : Array α) (f : α β) :
as.map f = as.foldl (fun r a => r.push (f a)) #[] :=
mapM_map_eq_foldl _ _ _
theorem map_induction (as : Array α) (f : α β) (motive : Nat Prop) (h0 : motive 0)
(p : Fin as.size β Prop) (hs : i, motive i.1 p i (f as[i]) motive (i+1)) :
motive as.size
@@ -2078,13 +1601,36 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
simp only [show j = i by omega]
exact (hs _ m).1
set_option linter.deprecated false in
@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")]
theorem map_spec (as : Array α) (f : α β) (p : Fin as.size β Prop)
(hs : i, p i (f as[i])) :
eq : (as.map f).size = as.size, i h, p i, h ((as.map f)[i]) := by
simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
@[simp] theorem getElem_map (f : α β) (as : Array α) (i : Nat) (h) :
(as.map f)[i] = f (as[i]'(size_map .. h)) := by
have := map_spec as f (fun i b => b = f (as[i]))
simp only [implies_true, true_implies] at this
obtain eq, w := this
apply w
simp_all
@[simp] theorem getElem?_map (f : α β) (as : Array α) (i : Nat) :
(as.map f)[i]? = as[i]?.map f := by
simp [getElem?_def]
@[simp] theorem map_push {f : α β} {as : Array α} {x : α} :
(as.push x).map f = (as.map f).push (f x) := by
ext
· simp
· simp only [getElem_map, getElem_push, size_map]
split <;> rfl
@[simp] theorem map_pop {f : α β} {as : Array α} :
as.pop.map f = (as.map f).pop := by
ext
· simp
· simp only [getElem_map, getElem_pop, size_map]
/-! ### modify -/
@[simp] theorem size_modify (a : Array α) (i : Nat) (f : α α) : (a.modify i f).size = a.size := by
@@ -2118,12 +1664,71 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : αα} {j : Nat} :
simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
split <;> split <;> rfl
/-! ### filter -/
@[simp] theorem toList_filter (p : α Bool) (l : Array α) :
(l.filter p).toList = l.toList.filter p := by
dsimp only [filter]
rw [ foldl_toList]
generalize l.toList = l
suffices a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
a.toList ++ List.filter p l by
simpa using this #[]
induction l with simp
| cons => split <;> simp [*]
@[simp] theorem filter_filter (q) (l : Array α) :
filter p (filter q l) = filter (fun a => p a && q a) l := by
apply ext'
simp only [toList_filter, List.filter_filter]
@[simp] theorem mem_filter : x filter p as x as p x := by
simp only [mem_def, toList_filter, List.mem_filter]
theorem mem_of_mem_filter {a : α} {l} (h : a filter p l) : a l :=
(mem_filter.mp h).1
@[congr]
theorem filter_congr {as bs : Array α} (h : as = bs)
{f : α Bool} {g : α Bool} (h' : f = g) {start stop start' stop' : Nat}
(h₁ : start = start') (h₂ : stop = stop') :
filter f as start stop = filter g bs start' stop' := by
congr
/-! ### filterMap -/
@[simp] theorem toList_filterMap (f : α Option β) (l : Array α) :
(l.filterMap f).toList = l.toList.filterMap f := by
dsimp only [filterMap, filterMapM]
rw [ foldlM_toList]
generalize l.toList = l
have this : a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
a.toList ++ List.filterMap f l := ?_
exact this #[]
induction l
· simp_all [Id.run]
· simp_all [Id.run, List.filterMap_cons]
split <;> simp_all
@[simp] theorem mem_filterMap {f : α Option β} {l : Array α} {b : β} :
b filterMap f l a, a l f a = some b := by
simp only [mem_def, toList_filterMap, List.mem_filterMap]
@[congr]
theorem filterMap_congr {as bs : Array α} (h : as = bs)
{f : α Option β} {g : α Option β} (h' : f = g) {start stop start' stop' : Nat}
(h₁ : start = start') (h₂ : stop = stop') :
filterMap f as start stop = filterMap g bs start' stop' := by
congr
/-! ### empty -/
theorem size_empty : (#[] : Array α).size = 0 := rfl
/-! ### append -/
theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
@[simp] theorem mem_append {a : α} {s t : Array α} : a s ++ t a s a t := by
simp only [mem_def, toList_append, List.mem_append]
@@ -2512,6 +2117,10 @@ theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
rw [size_toArray, mapM'_cons, foldlM_toArray]
simp [ih]
@[simp] theorem map_toArray (f : α β) (l : List α) : l.toArray.map f = (l.map f).toArray := by
apply ext'
simp
theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) :
l.toArray.uset i a h = (l.set i.toNat a).toArray := by simp
@@ -2520,11 +2129,35 @@ theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray
apply ext'
simp
@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
apply ext'
simp
@[simp] theorem modify_toArray (f : α α) (l : List α) :
l.toArray.modify i f = (l.modify f i).toArray := by
apply ext'
simp
@[simp] theorem filter_toArray' (p : α Bool) (l : List α) (h : stop = l.toArray.size) :
l.toArray.filter p 0 stop = (l.filter p).toArray := by
subst h
apply ext'
rw [toList_filter]
@[simp] theorem filterMap_toArray' (f : α Option β) (l : List α) (h : stop = l.toArray.size) :
l.toArray.filterMap f 0 stop = (l.filterMap f).toArray := by
subst h
apply ext'
rw [toList_filterMap]
theorem filter_toArray (p : α Bool) (l : List α) :
l.toArray.filter p = (l.filter p).toArray := by
simp
theorem filterMap_toArray (f : α Option β) (l : List α) :
l.toArray.filterMap f = (l.filterMap f).toArray := by
simp
@[simp] theorem flatten_toArray (l : List (List α)) :
(l.toArray.map List.toArray).flatten = l.flatten.toArray := by
apply ext'
@@ -2593,6 +2226,29 @@ namespace Array
/-! ### map -/
@[simp] theorem map_map {f : α β} {g : β γ} {as : Array α} :
(as.map f).map g = as.map (g f) := by
cases as; simp
@[simp] theorem map_id_fun : map (id : α α) = id := by
funext l
induction l <;> simp_all
/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
theorem map_id (as : Array α) : map (id : α α) as = as := by
cases as <;> simp_all
/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
theorem map_id' (as : Array α) : map (fun (a : α) => a) as = as := map_id as
/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
theorem map_id'' {f : α α} (h : x, f x = x) (as : Array α) : map f as = as := by
simp [show f = id from funext h]
theorem array_array_induction (P : Array (Array α) Prop) (h : (xss : List (List α)), P (xss.map List.toArray).toArray)
(ass : Array (Array α)) : P ass := by
specialize h (ass.toList.map toList)
@@ -2646,12 +2302,6 @@ theorem foldr_map' (g : α → β) (f : ααα) (f' : β → β → β
| nil => simp
| cons xs xss ih => simp [ih]
/-! ### mkArray -/
@[simp] theorem mem_mkArray (a : α) (n : Nat) : b mkArray n a n 0 b = a := by
rw [mkArray, mem_toArray]
simp
/-! ### reverse -/
@[simp] theorem mem_reverse {x : α} {as : Array α} : x as.reverse x as := by

View File

@@ -17,8 +17,8 @@ namespace Array
@[simp] theorem lt_toList [LT α] (l₁ l₂ : Array α) : l₁.toList < l₂.toList l₁ < l₂ := Iff.rfl
@[simp] theorem le_toList [LT α] (l₁ l₂ : Array α) : l₁.toList l₂.toList l₁ l₂ := Iff.rfl
protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ l₂ l₁ := Iff.rfl
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ l₂ l₁ := Iff.rfl
theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
¬ l₁ l₂ l₂ < l₁ :=
Decidable.not_not
@@ -135,7 +135,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
{l₁ l₂ : Array α} (h : l₁ < l₂) : l₁ l₂ :=
List.le_of_lt h
protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
[Std.Total (¬ · < · : α α Prop)]
@@ -211,7 +211,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : αα
cases l₂
simp_all [List.lex_eq_false_iff_exists]
protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Array α} :
theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Array α} :
l₁ < l₂
(l₁ = l₂.take l₁.size l₁.size < l₂.size)
( (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size),
@@ -221,7 +221,7 @@ protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁
cases l₂
simp [List.lt_iff_exists]
protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α α Prop)]
[Std.Asymm (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)] {l₁ l₂ : Array α} :
@@ -258,14 +258,14 @@ theorem le_append_left [LT α] [Std.Irrefl (· < · : αα → Prop)]
cases l₂
simpa using List.le_append_left
protected theorem map_lt [LT α] [LT β]
theorem map_lt [LT α] [LT β]
{l₁ l₂ : Array α} {f : α β} (w : x y, x < y f x < f y) (h : l₁ < l₂) :
map f l₁ < map f l₂ := by
cases l₁
cases l₂
simpa using List.map_lt w h
protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
[Std.Irrefl (· < · : α α Prop)]
[Std.Asymm (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]

View File

@@ -9,9 +9,7 @@ import Init.Data.Bool
import Init.Data.BitVec.Basic
import Init.Data.Fin.Lemmas
import Init.Data.Nat.Lemmas
import Init.Data.Nat.Div.Lemmas
import Init.Data.Nat.Mod
import Init.Data.Nat.Div.Lemmas
import Init.Data.Int.Bitwise.Lemmas
import Init.Data.Int.Pow
@@ -100,12 +98,6 @@ theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
theorem eq_of_toNat_eq {n} : {x y : BitVec n}, x.toNat = y.toNat x = y
| _, _, _, _, rfl => rfl
/-- Prove nonequality of bitvectors in terms of nat operations. -/
theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat y.toNat x y := by
constructor
· rintro h rfl; apply h rfl
· intro h h_eq; apply h <| eq_of_toNat_eq h_eq
@[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
@[bv_toNat] theorem toNat_eq {x y : BitVec n} : x = y x.toNat = y.toNat :=
@@ -450,10 +442,6 @@ theorem toInt_eq_toNat_cond (x : BitVec n) :
(x.toNat : Int) - (2^n : Nat) :=
rfl
theorem toInt_eq_toNat_of_lt {x : BitVec n} (h : 2 * x.toNat < 2^n) :
x.toInt = x.toNat := by
simp [toInt_eq_toNat_cond, h]
theorem msb_eq_false_iff_two_mul_lt {x : BitVec w} : x.msb = false 2 * x.toNat < 2^w := by
cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide, toNat_of_zero_length]
@@ -466,9 +454,6 @@ theorem toInt_eq_msb_cond (x : BitVec w) :
simp only [BitVec.toInt, msb_eq_false_iff_two_mul_lt]
cases x.msb <;> rfl
theorem toInt_eq_toNat_of_msb {x : BitVec w} (h : x.msb = false) :
x.toInt = x.toNat := by
simp [toInt_eq_msb_cond, h]
theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
simp only [toInt_eq_toNat_cond]
@@ -800,19 +785,6 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
unfold allOnes
simp
@[simp] theorem toInt_allOnes : (allOnes w).toInt = if 0 < w then -1 else 0 := by
norm_cast
by_cases h : w = 0
· subst h
simp
· have : 1 < 2 ^ w := by simp [h]
simp [BitVec.toInt]
omega
@[simp] theorem toFin_allOnes : (allOnes w).toFin = Fin.ofNat' (2^w) (2^w - 1) := by
ext
simp
@[simp] theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v) := by
simp [allOnes]
@@ -1170,16 +1142,11 @@ theorem getMsb_not {x : BitVec w} :
/-! ### shiftLeft -/
@[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
(x <<< n).toNat = x.toNat <<< n % 2^v :=
BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v :=
BitVec.toNat_ofNat _ _
@[simp] theorem toInt_shiftLeft {x : BitVec w} :
(x <<< n).toInt = (x.toNat <<< n : Int).bmod (2^w) := by
rw [toInt_eq_toNat_bmod, toNat_shiftLeft, Nat.shiftLeft_eq]
simp
@[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
(x <<< n).toFin = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
@[simp]
theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by
@@ -2315,12 +2282,6 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
@[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
simp [Neg.neg, BitVec.neg]
theorem toNat_neg_of_pos {x : BitVec n} (h : 0#n < x) :
(- x).toNat = 2^n - x.toNat := by
change 0 < x.toNat at h
rw [toNat_neg, Nat.mod_eq_of_lt]
omega
theorem toInt_neg {x : BitVec w} :
(-x).toInt = (-x.toInt).bmod (2 ^ w) := by
rw [ BitVec.zero_sub, toInt_sub]
@@ -2416,54 +2377,6 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
omega
/-! ### fill -/
@[simp]
theorem getLsbD_fill {w i : Nat} {v : Bool} :
(fill w v).getLsbD i = (v && decide (i < w)) := by
by_cases h : v
<;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
@[simp]
theorem getMsbD_fill {w i : Nat} {v : Bool} :
(fill w v).getMsbD i = (v && decide (i < w)) := by
by_cases h : v
<;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
@[simp]
theorem getElem_fill {w i : Nat} {v : Bool} (h : i < w) :
(fill w v)[i] = v := by
by_cases h : v
<;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
@[simp]
theorem msb_fill {w : Nat} {v : Bool} :
(fill w v).msb = (v && decide (0 < w)) := by
simp [BitVec.msb]
theorem fill_eq {w : Nat} {v : Bool} : fill w v = if v = true then allOnes w else 0#w := by
by_cases h : v <;> (simp only [h] ; ext ; simp)
@[simp]
theorem fill_true {w : Nat} : fill w true = allOnes w := by
simp [fill_eq]
@[simp]
theorem fill_false {w : Nat} : fill w false = 0#w := by
simp [fill_eq]
@[simp] theorem fill_toNat {w : Nat} {v : Bool} :
(fill w v).toNat = if v = true then 2^w - 1 else 0 := by
by_cases h : v <;> simp [h]
@[simp] theorem fill_toInt {w : Nat} {v : Bool} :
(fill w v).toInt = if v = true && 0 < w then -1 else 0 := by
by_cases h : v <;> simp [h]
@[simp] theorem fill_toFin {w : Nat} {v : Bool} :
(fill w v).toFin = if v = true then (allOnes w).toFin else Fin.ofNat' (2 ^ w) 0 := by
by_cases h : v <;> simp [h]
/-! ### mul -/
theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
@@ -2607,13 +2520,13 @@ theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) :
rw [ udiv_eq]
simp [udiv, bv_toNat, h, Nat.mod_eq_of_lt]
@[simp]
theorem toFin_udiv {x y : BitVec n} : (x / y).toFin = x.toFin / y.toFin := by
rfl
@[simp, bv_toNat]
theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat := by
rfl
rw [udiv_def]
by_cases h : y = 0
· simp [h]
· rw [toNat_ofNat, Nat.mod_eq_of_lt]
exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
@[simp]
theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w := by
@@ -2649,45 +2562,6 @@ theorem udiv_self {x : BitVec w} :
reduceIte, toNat_udiv]
rw [Nat.div_self (by omega), Nat.mod_eq_of_lt (by omega)]
theorem msb_udiv (x y : BitVec w) :
(x / y).msb = (x.msb && y == 1#w) := by
cases msb_x : x.msb
· suffices x.toNat / y.toNat < 2 ^ (w - 1) by simpa [msb_eq_decide]
calc
x.toNat / y.toNat x.toNat := by apply Nat.div_le_self
_ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x
. rcases w with _|w
· contradiction
· have : (y == 1#_) = decide (y.toNat = 1) := by
simp [(· == ·), toNat_eq]
simp only [this, Bool.true_and]
match hy : y.toNat with
| 0 =>
obtain rfl : y = 0#_ := eq_of_toNat_eq hy
simp
| 1 =>
obtain rfl : y = 1#_ := eq_of_toNat_eq (by simp [hy])
simpa using msb_x
| y + 2 =>
suffices x.toNat / (y + 2) < 2 ^ w by
simp_all [msb_eq_decide, hy]
calc
x.toNat / (y + 2)
x.toNat / 2 := by apply Nat.div_add_le_right (by omega)
_ < 2 ^ w := by omega
theorem msb_udiv_eq_false_of {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
(x / y).msb = false := by
simp [msb_udiv, h]
/--
If `x` is nonnegative (i.e., does not have its msb set),
then `x / y` is nonnegative, thus `toInt` and `toNat` coincide.
-/
theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
(x / y).toInt = x.toNat / y.toNat := by
simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h]
/-! ### umod -/
theorem umod_def {x y : BitVec n} :
@@ -2700,10 +2574,6 @@ theorem umod_def {x y : BitVec n} :
theorem toNat_umod {x y : BitVec n} :
(x % y).toNat = x.toNat % y.toNat := rfl
@[simp]
theorem toFin_umod {x y : BitVec w} :
(x % y).toFin = x.toFin % y.toFin := rfl
@[simp]
theorem umod_zero {x : BitVec n} : x % 0#n = x := by
simp [umod_def]
@@ -2731,55 +2601,6 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
rcases hy with rfl | rfl <;>
rfl
theorem umod_eq_of_lt {x y : BitVec w} (h : x < y) :
x % y = x := by
apply eq_of_toNat_eq
simp [Nat.mod_eq_of_lt h]
@[simp]
theorem msb_umod {x y : BitVec w} :
(x % y).msb = (x.msb && (x < y || y == 0#w)) := by
rw [msb_eq_decide, toNat_umod]
cases msb_x : x.msb
· suffices x.toNat % y.toNat < 2 ^ (w - 1) by simpa
calc
x.toNat % y.toNat x.toNat := by apply Nat.mod_le
_ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x
. by_cases hy : y = 0
· simp_all [msb_eq_decide]
· suffices 2 ^ (w - 1) x.toNat % y.toNat x < y by simp_all
by_cases x_lt_y : x < y
. simp_all [Nat.mod_eq_of_lt x_lt_y, msb_eq_decide]
· suffices x.toNat % y.toNat < 2 ^ (w - 1) by
simpa [x_lt_y]
have y_le_x : y.toNat x.toNat := by
simpa using x_lt_y
replace hy : y.toNat 0 :=
toNat_ne_iff_ne.mpr hy
by_cases msb_y : y.toNat < 2 ^ (w - 1)
· have : x.toNat % y.toNat < y.toNat := Nat.mod_lt _ (by omega)
omega
· rcases w with _|w
· contradiction
simp only [Nat.add_one_sub_one]
replace msb_y : 2 ^ w y.toNat := by
simpa using msb_y
have : y.toNat y.toNat * (x.toNat / y.toNat) := by
apply Nat.le_mul_of_pos_right
apply Nat.div_pos y_le_x
omega
have : x.toNat % y.toNat x.toNat - y.toNat := by
rw [Nat.mod_eq_sub]; omega
omega
theorem toInt_umod {x y : BitVec w} :
(x % y).toInt = (x.toNat % y.toNat : Int).bmod (2 ^ w) := by
simp [toInt_eq_toNat_bmod]
theorem toInt_umod_of_msb {x y : BitVec w} (h : x.msb = false) :
(x % y).toInt = x.toInt % y.toNat := by
simp [toInt_eq_msb_cond, h]
/-! ### smtUDiv -/
theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
@@ -2936,12 +2757,7 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
/-! # Rotate Left -/
/--`rotateLeft` is defined in terms of left and right shifts. -/
theorem rotateLeft_def {x : BitVec w} {r : Nat} :
x.rotateLeft r = (x <<< (r % w)) ||| (x >>> (w - r % w)) := by
simp only [rotateLeft, rotateLeftAux]
/-- `rotateLeft` is invariant under `mod` by the bitwidth. -/
/-- rotateLeft is invariant under `mod` by the bitwidth. -/
@[simp]
theorem rotateLeft_mod_eq_rotateLeft {x : BitVec w} {r : Nat} :
x.rotateLeft (r % w) = x.rotateLeft r := by
@@ -3085,18 +2901,8 @@ theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
· simp
omega
@[simp]
theorem toNat_rotateLeft {x : BitVec w} {r : Nat} :
(x.rotateLeft r).toNat = (x.toNat <<< (r % w)) % (2^w) ||| x.toNat >>> (w - r % w) := by
simp only [rotateLeft_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
/-! ## Rotate Right -/
/-- `rotateRight` is defined in terms of left and right shifts. -/
theorem rotateRight_def {x : BitVec w} {r : Nat} :
x.rotateRight r = (x >>> (r % w)) ||| (x <<< (w - r % w)) := by
simp only [rotateRight, rotateRightAux]
/--
Accessing bits in `x.rotateRight r` the range `[0, w-r)` is equal to
accessing bits `x` in the range `[r, w)`.
@@ -3232,11 +3038,6 @@ theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
simp [h₁]
· simp [show w = 0 by omega]
@[simp]
theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
(x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by
simp only [rotateRight_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
/- ## twoPow -/
theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by

View File

@@ -534,13 +534,6 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
@[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
conv => rhs; rw [ emod_add_ediv a b, add_mul_emod_self_left]
@[simp] theorem emod_sub_emod (m n k : Int) : (m % n - k) % n = (m - k) % n :=
Int.emod_add_emod m n (-k)
@[simp] theorem sub_emod_emod (m n k : Int) : (m - n % k) % k = (m - n) % k := by
apply (emod_add_cancel_right (n % k)).mp
rw [Int.sub_add_cancel, Int.add_emod_emod, Int.sub_add_cancel]
theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
apply (emod_add_cancel_right b).mp
rw [Int.sub_add_cancel, Int.add_emod_emod, Int.sub_add_cancel, emod_emod]
@@ -1105,32 +1098,6 @@ theorem bmod_def (x : Int) (m : Nat) : bmod x m =
(x % m) - m :=
rfl
theorem bdiv_add_bmod (x : Int) (m : Nat) : m * bdiv x m + bmod x m = x := by
unfold bdiv bmod
split
· simp_all only [Nat.cast_ofNat_Int, Int.mul_zero, emod_zero, Int.zero_add, Int.sub_zero,
ite_self]
· dsimp only
split
· exact ediv_add_emod x m
· rw [Int.mul_add, Int.mul_one, Int.add_assoc, Int.add_comm m, Int.sub_add_cancel]
exact ediv_add_emod x m
theorem bmod_add_bdiv (x : Int) (m : Nat) : bmod x m + m * bdiv x m = x := by
rw [Int.add_comm]; exact bdiv_add_bmod x m
theorem bdiv_add_bmod' (x : Int) (m : Nat) : bdiv x m * m + bmod x m = x := by
rw [Int.mul_comm]; exact bdiv_add_bmod x m
theorem bmod_add_bdiv' (x : Int) (m : Nat) : bmod x m + bdiv x m * m = x := by
rw [Int.add_comm]; exact bdiv_add_bmod' x m
theorem bmod_eq_self_sub_mul_bdiv (x : Int) (m : Nat) : bmod x m = x - m * bdiv x m := by
rw [ Int.add_sub_cancel (bmod x m), bmod_add_bdiv]
theorem bmod_eq_self_sub_bdiv_mul (x : Int) (m : Nat) : bmod x m = x - bdiv x m * m := by
rw [ Int.add_sub_cancel (bmod x m), bmod_add_bdiv']
theorem bmod_pos (x : Int) (m : Nat) (p : x % m < (m + 1) / 2) : bmod x m = x % m := by
simp [bmod_def, p]

View File

@@ -1,8 +1,7 @@
/-
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,
Kim Morrison
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
-/
prelude
import Init.Data.Bool
@@ -758,6 +757,207 @@ theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l
| nil => simp
| cons b l₂ => simp [isEqv, ih]
/-! ### foldlM and foldrM -/
@[simp] theorem foldlM_reverse [Monad m] (l : List α) (f : β α m β) (b) :
l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b := rfl
@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β α m β) (b) (l l' : List α) :
(l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
induction l generalizing b <;> simp [*]
@[simp] theorem foldrM_cons [Monad m] [LawfulMonad m] (a : α) (l) (f : α β m β) (b) :
(a :: l).foldrM f b = l.foldrM f b >>= f a := by
simp only [foldrM]
induction l <;> simp_all
theorem foldl_eq_foldlM (f : β α β) (b) (l : List α) :
l.foldl f b = l.foldlM (m := Id) f b := by
induction l generalizing b <;> simp [*, foldl]
theorem foldr_eq_foldrM (f : α β β) (b) (l : List α) :
l.foldr f b = l.foldrM (m := Id) f b := by
induction l <;> simp [*, foldr]
@[simp] theorem id_run_foldlM (f : β α Id β) (b) (l : List α) :
Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
@[simp] theorem id_run_foldrM (f : α β Id β) (b) (l : List α) :
Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
/-! ### foldl and foldr -/
@[simp] theorem foldr_cons_eq_append (l : List α) : l.foldr cons l' = l ++ l' := by
induction l <;> simp [*]
@[deprecated foldr_cons_eq_append (since := "2024-08-22")] abbrev foldr_self_append := @foldr_cons_eq_append
@[simp] theorem foldl_flip_cons_eq_append (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l' := by
induction l generalizing l' <;> simp [*]
theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l := by simp
@[deprecated foldr_cons_nil (since := "2024-09-04")] abbrev foldr_self := @foldr_cons_nil
theorem foldl_map (f : β₁ β₂) (g : α β₂ α) (l : List β₁) (init : α) :
(l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
induction l generalizing init <;> simp [*]
theorem foldr_map (f : α₁ α₂) (g : α₂ β β) (l : List α₁) (init : β) :
(l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
induction l generalizing init <;> simp [*]
theorem foldl_filterMap (f : α Option β) (g : γ β γ) (l : List α) (init : γ) :
(l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
induction l generalizing init with
| nil => rfl
| cons a l ih =>
simp only [filterMap_cons, foldl_cons]
cases f a <;> simp [ih]
theorem foldr_filterMap (f : α Option β) (g : β γ γ) (l : List α) (init : γ) :
(l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
induction l generalizing init with
| nil => rfl
| cons a l ih =>
simp only [filterMap_cons, foldr_cons]
cases f a <;> simp [ih]
theorem foldl_map' (g : α β) (f : α α α) (f' : β β β) (a : α) (l : List α)
(h : x y, f' (g x) (g y) = g (f x y)) :
(l.map g).foldl f' (g a) = g (l.foldl f a) := by
induction l generalizing a
· simp
· simp [*, h]
theorem foldr_map' (g : α β) (f : α α α) (f' : β β β) (a : α) (l : List α)
(h : x y, f' (g x) (g y) = g (f x y)) :
(l.map g).foldr f' (g a) = g (l.foldr f a) := by
induction l generalizing a
· simp
· simp [*, h]
theorem foldl_assoc {op : α α α} [ha : Std.Associative op] :
{l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)
| [], a₁, a₂ => rfl
| a :: l, a₁, a₂ => by
simp only [foldl_cons, ha.assoc]
rw [foldl_assoc]
theorem foldr_assoc {op : α α α} [ha : Std.Associative op] :
{l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂
| [], a₁, a₂ => rfl
| a :: l, a₁, a₂ => by
simp only [foldr_cons, ha.assoc]
rw [foldr_assoc]
theorem foldl_hom (f : α₁ α₂) (g₁ : α₁ β α₁) (g₂ : α₂ β α₂) (l : List β) (init : α₁)
(H : x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
induction l generalizing init <;> simp [*, H]
theorem foldr_hom (f : β₁ β₂) (g₁ : α β₁ β₁) (g₂ : α β₂ β₂) (l : List α) (init : β₁)
(H : x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by
induction l <;> simp [*, H]
/--
Prove a proposition about the result of `List.foldl`,
by proving it for the initial data,
and the implication that the operation applied to any element of the list preserves the property.
The motive can take values in `Sort _`, so this may be used to construct data,
as well as to prove propositions.
-/
def foldlRecOn {motive : β Sort _} : (l : List α) (op : β α β) (b : β) (_ : motive b)
(_ : (b : β) (_ : motive b) (a : α) (_ : a l), motive (op b a)), motive (List.foldl op b l)
| [], _, _, hb, _ => hb
| hd :: tl, op, b, hb, hl =>
foldlRecOn tl op (op b hd) (hl b hb hd (mem_cons_self hd tl))
fun y hy x hx => hl y hy x (mem_cons_of_mem hd hx)
@[simp] theorem foldlRecOn_nil {motive : β Sort _} (hb : motive b)
(hl : (b : β) (_ : motive b) (a : α) (_ : a []), motive (op b a)) :
foldlRecOn [] op b hb hl = hb := rfl
@[simp] theorem foldlRecOn_cons {motive : β Sort _} (hb : motive b)
(hl : (b : β) (_ : motive b) (a : α) (_ : a x :: l), motive (op b a)) :
foldlRecOn (x :: l) op b hb hl =
foldlRecOn l op (op b x) (hl b hb x (mem_cons_self x l))
(fun b c a m => hl b c a (mem_cons_of_mem x m)) :=
rfl
/--
Prove a proposition about the result of `List.foldr`,
by proving it for the initial data,
and the implication that the operation applied to any element of the list preserves the property.
The motive can take values in `Sort _`, so this may be used to construct data,
as well as to prove propositions.
-/
def foldrRecOn {motive : β Sort _} : (l : List α) (op : α β β) (b : β) (_ : motive b)
(_ : (b : β) (_ : motive b) (a : α) (_ : a l), motive (op a b)), motive (List.foldr op b l)
| nil, _, _, hb, _ => hb
| x :: l, op, b, hb, hl =>
hl (foldr op b l)
(foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m)) x (mem_cons_self x l)
@[simp] theorem foldrRecOn_nil {motive : β Sort _} (hb : motive b)
(hl : (b : β) (_ : motive b) (a : α) (_ : a []), motive (op a b)) :
foldrRecOn [] op b hb hl = hb := rfl
@[simp] theorem foldrRecOn_cons {motive : β Sort _} (hb : motive b)
(hl : (b : β) (_ : motive b) (a : α) (_ : a x :: l), motive (op a b)) :
foldrRecOn (x :: l) op b hb hl =
hl _ (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m))
x (mem_cons_self x l) :=
rfl
/--
We can prove that two folds over the same list are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the list,
preserves the relation.
-/
theorem foldl_rel {l : List α} {f g : β α β} {a b : β} (r : β β Prop)
(h : r a b) (h' : (a : α), a l (c c' : β), r c c' r (f c a) (g c' a)) :
r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
induction l generalizing a b with
| nil => simp_all
| cons a l ih =>
simp only [foldl_cons]
apply ih
· simp_all
· exact fun a m c c' h => h' _ (by simp_all) _ _ h
/--
We can prove that two folds over the same list are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the list,
preserves the relation.
-/
theorem foldr_rel {l : List α} {f g : α β β} {a b : β} (r : β β Prop)
(h : r a b) (h' : (a : α), a l (c c' : β), r c c' r (f a c) (g a c')) :
r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
induction l generalizing a b with
| nil => simp_all
| cons a l ih =>
simp only [foldr_cons]
apply h'
· simp
· exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h
@[simp] theorem foldl_add_const (l : List α) (a b : Nat) :
l.foldl (fun x _ => x + a) b = b + a * l.length := by
induction l generalizing b with
| nil => simp
| cons y l ih =>
simp only [foldl_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc,
Nat.add_comm a]
@[simp] theorem foldr_add_const (l : List α) (a b : Nat) :
l.foldr (fun _ x => x + a) b = b + a * l.length := by
induction l generalizing b with
| nil => simp
| cons y l ih =>
simp only [foldr_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc]
/-! ### getLast -/
theorem getLast_eq_getElem : (l : List α) (h : l []),
@@ -1016,6 +1216,27 @@ theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then n
/-! ### map -/
@[simp] theorem map_id_fun : map (id : α α) = id := by
funext l
induction l <;> simp_all
/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
theorem map_id (l : List α) : map (id : α α) l = l := by
induction l <;> simp_all
/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
theorem map_id' (l : List α) : map (fun (a : α) => a) l = l := map_id l
/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
theorem map_id'' {f : α α} (h : x, f x = x) (l : List α) : map f l = l := by
simp [show f = id from funext h]
theorem map_singleton (f : α β) (a : α) : map f [a] = [f a] := rfl
@[simp] theorem length_map (as : List α) (f : α β) : (as.map f).length = as.length := by
induction as with
| nil => simp [List.map]
@@ -1041,27 +1262,6 @@ theorem get_map (f : α → β) {l i} :
get (map f l) i = f (get l i, length_map l f i.2) := by
simp
@[simp] theorem map_id_fun : map (id : α α) = id := by
funext l
induction l <;> simp_all
/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
theorem map_id (l : List α) : map (id : α α) l = l := by
induction l <;> simp_all
/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
theorem map_id' (l : List α) : map (fun (a : α) => a) l = l := map_id l
/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
theorem map_id'' {f : α α} (h : x, f x = x) (l : List α) : map f l = l := by
simp [show f = id from funext h]
theorem map_singleton (f : α β) (a : α) : map f [a] = [f a] := rfl
@[simp] theorem mem_map {f : α β} : {l : List α}, b l.map f a, a l f a = b
| [] => by simp
| _ :: l => by simp [mem_map (l := l), eq_comm (a := b)]
@@ -1115,10 +1315,6 @@ theorem map_eq_cons_iff' {f : α → β} {l : List α} :
@[deprecated map_eq_cons' (since := "2024-09-05")] abbrev map_eq_cons' := @map_eq_cons_iff'
@[simp] theorem map_eq_singleton_iff {f : α β} {l : List α} {b : β} :
map f l = [b] a, l = [a] f a = b := by
simp [map_eq_cons_iff]
theorem map_eq_map_iff : map f l = map g l a l, f a = g a := by
induction l <;> simp
@@ -1285,7 +1481,7 @@ theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
@[simp] theorem filter_append {p : α Bool} :
(l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
| [], _ => rfl
| a :: l₁, l₂ => by simp only [cons_append, filter]; split <;> simp [filter_append l₁]
| a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
theorem filter_eq_cons_iff {l} {a} {as} :
filter p l = a :: as
@@ -1765,6 +1961,16 @@ theorem set_append {s t : List α} :
(s ++ t).set i x = s ++ t.set (i - s.length) x := by
rw [set_append, if_neg (by simp_all)]
@[simp] theorem foldrM_append [Monad m] [LawfulMonad m] (f : α β m β) (b) (l l' : List α) :
(l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by
induction l <;> simp [*]
@[simp] theorem foldl_append {β : Type _} (f : β α β) (b) (l l' : List α) :
(l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
@[simp] theorem foldr_append (f : α β β) (b) (l l' : List α) :
(l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
theorem filterMap_eq_append_iff {f : α Option β} :
filterMap f l = L₁ ++ L₂ l₁ l₂, l = l₁ ++ l₂ filterMap f l₁ = L₁ filterMap f l₂ = L₂ := by
constructor
@@ -1913,6 +2119,14 @@ theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun
-- `getLast?_flatten` is proved later, after the `reverse` section.
-- `head_flatten` and `getLast_flatten` are proved in `Init.Data.List.Find`.
theorem foldl_flatten (f : β α β) (b : β) (L : List (List α)) :
(flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
induction L generalizing b <;> simp_all
theorem foldr_flatten (f : α β β) (b : β) (L : List (List α)) :
(flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
induction L <;> simp_all
@[simp] theorem map_flatten (f : α β) (L : List (List α)) : map f (flatten L) = flatten (map (map f) L) := by
induction L <;> simp_all
@@ -2485,114 +2699,10 @@ theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.fla
@[simp] theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
reverseAux_eq_append ..
@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
eq_replicate_iff.2
by rw [length_reverse, length_replicate],
fun _ h => eq_of_mem_replicate (mem_reverse.1 h)
/-! ### foldlM and foldrM -/
@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β α m β) (b) (l l' : List α) :
(l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
induction l generalizing b <;> simp [*]
@[simp] theorem foldrM_cons [Monad m] [LawfulMonad m] (a : α) (l) (f : α β m β) (b) :
(a :: l).foldrM f b = l.foldrM f b >>= f a := by
simp only [foldrM]
induction l <;> simp_all
theorem foldl_eq_foldlM (f : β α β) (b) (l : List α) :
l.foldl f b = l.foldlM (m := Id) f b := by
induction l generalizing b <;> simp [*, foldl]
theorem foldr_eq_foldrM (f : α β β) (b) (l : List α) :
l.foldr f b = l.foldrM (m := Id) f b := by
induction l <;> simp [*, foldr]
@[simp] theorem id_run_foldlM (f : β α Id β) (b) (l : List α) :
Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
@[simp] theorem id_run_foldrM (f : α β Id β) (b) (l : List α) :
Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
@[simp] theorem foldlM_reverse [Monad m] (l : List α) (f : β α m β) (b) :
l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b := rfl
@[simp] theorem foldrM_reverse [Monad m] (l : List α) (f : α β m β) (b) :
l.reverse.foldrM f b = l.foldlM (fun x y => f y x) b :=
(foldlM_reverse ..).symm.trans <| by simp
/-! ### foldl and foldr -/
@[simp] theorem foldr_cons_eq_append (l : List α) : l.foldr cons l' = l ++ l' := by
induction l <;> simp [*]
@[deprecated foldr_cons_eq_append (since := "2024-08-22")] abbrev foldr_self_append := @foldr_cons_eq_append
@[simp] theorem foldl_flip_cons_eq_append (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l' := by
induction l generalizing l' <;> simp [*]
theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l := by simp
@[deprecated foldr_cons_nil (since := "2024-09-04")] abbrev foldr_self := @foldr_cons_nil
theorem foldl_map (f : β₁ β₂) (g : α β₂ α) (l : List β₁) (init : α) :
(l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
induction l generalizing init <;> simp [*]
theorem foldr_map (f : α₁ α₂) (g : α₂ β β) (l : List α₁) (init : β) :
(l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
induction l generalizing init <;> simp [*]
theorem foldl_filterMap (f : α Option β) (g : γ β γ) (l : List α) (init : γ) :
(l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
induction l generalizing init with
| nil => rfl
| cons a l ih =>
simp only [filterMap_cons, foldl_cons]
cases f a <;> simp [ih]
theorem foldr_filterMap (f : α Option β) (g : β γ γ) (l : List α) (init : γ) :
(l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
induction l generalizing init with
| nil => rfl
| cons a l ih =>
simp only [filterMap_cons, foldr_cons]
cases f a <;> simp [ih]
theorem foldl_map' (g : α β) (f : α α α) (f' : β β β) (a : α) (l : List α)
(h : x y, f' (g x) (g y) = g (f x y)) :
(l.map g).foldl f' (g a) = g (l.foldl f a) := by
induction l generalizing a
· simp
· simp [*, h]
theorem foldr_map' (g : α β) (f : α α α) (f' : β β β) (a : α) (l : List α)
(h : x y, f' (g x) (g y) = g (f x y)) :
(l.map g).foldr f' (g a) = g (l.foldr f a) := by
induction l generalizing a
· simp
· simp [*, h]
@[simp] theorem foldrM_append [Monad m] [LawfulMonad m] (f : α β m β) (b) (l l' : List α) :
(l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by
induction l <;> simp [*]
@[simp] theorem foldl_append {β : Type _} (f : β α β) (b) (l l' : List α) :
(l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
@[simp] theorem foldr_append (f : α β β) (b) (l l' : List α) :
(l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
theorem foldl_flatten (f : β α β) (b : β) (L : List (List α)) :
(flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
induction L generalizing b <;> simp_all
theorem foldr_flatten (f : α β β) (b : β) (L : List (List α)) :
(flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
induction L <;> simp_all
@[simp] theorem foldl_reverse (l : List α) (f : β α β) (b) :
l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
@@ -2606,127 +2716,10 @@ theorem foldl_eq_foldr_reverse (l : List α) (f : β → α → β) (b) :
theorem foldr_eq_foldl_reverse (l : List α) (f : α β β) (b) :
l.foldr f b = l.reverse.foldl (fun x y => f y x) b := by simp
theorem foldl_assoc {op : α α α} [ha : Std.Associative op] :
{l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)
| [], a₁, a₂ => rfl
| a :: l, a₁, a₂ => by
simp only [foldl_cons, ha.assoc]
rw [foldl_assoc]
theorem foldr_assoc {op : α α α} [ha : Std.Associative op] :
{l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂
| [], a₁, a₂ => rfl
| a :: l, a₁, a₂ => by
simp only [foldr_cons, ha.assoc]
rw [foldr_assoc]
theorem foldl_hom (f : α₁ α₂) (g₁ : α₁ β α₁) (g₂ : α₂ β α₂) (l : List β) (init : α₁)
(H : x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
induction l generalizing init <;> simp [*, H]
theorem foldr_hom (f : β₁ β₂) (g₁ : α β₁ β₁) (g₂ : α β₂ β₂) (l : List α) (init : β₁)
(H : x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by
induction l <;> simp [*, H]
/--
Prove a proposition about the result of `List.foldl`,
by proving it for the initial data,
and the implication that the operation applied to any element of the list preserves the property.
The motive can take values in `Sort _`, so this may be used to construct data,
as well as to prove propositions.
-/
def foldlRecOn {motive : β Sort _} : (l : List α) (op : β α β) (b : β) (_ : motive b)
(_ : (b : β) (_ : motive b) (a : α) (_ : a l), motive (op b a)), motive (List.foldl op b l)
| [], _, _, hb, _ => hb
| hd :: tl, op, b, hb, hl =>
foldlRecOn tl op (op b hd) (hl b hb hd (mem_cons_self hd tl))
fun y hy x hx => hl y hy x (mem_cons_of_mem hd hx)
@[simp] theorem foldlRecOn_nil {motive : β Sort _} (hb : motive b)
(hl : (b : β) (_ : motive b) (a : α) (_ : a []), motive (op b a)) :
foldlRecOn [] op b hb hl = hb := rfl
@[simp] theorem foldlRecOn_cons {motive : β Sort _} (hb : motive b)
(hl : (b : β) (_ : motive b) (a : α) (_ : a x :: l), motive (op b a)) :
foldlRecOn (x :: l) op b hb hl =
foldlRecOn l op (op b x) (hl b hb x (mem_cons_self x l))
(fun b c a m => hl b c a (mem_cons_of_mem x m)) :=
rfl
/--
Prove a proposition about the result of `List.foldr`,
by proving it for the initial data,
and the implication that the operation applied to any element of the list preserves the property.
The motive can take values in `Sort _`, so this may be used to construct data,
as well as to prove propositions.
-/
def foldrRecOn {motive : β Sort _} : (l : List α) (op : α β β) (b : β) (_ : motive b)
(_ : (b : β) (_ : motive b) (a : α) (_ : a l), motive (op a b)), motive (List.foldr op b l)
| nil, _, _, hb, _ => hb
| x :: l, op, b, hb, hl =>
hl (foldr op b l)
(foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m)) x (mem_cons_self x l)
@[simp] theorem foldrRecOn_nil {motive : β Sort _} (hb : motive b)
(hl : (b : β) (_ : motive b) (a : α) (_ : a []), motive (op a b)) :
foldrRecOn [] op b hb hl = hb := rfl
@[simp] theorem foldrRecOn_cons {motive : β Sort _} (hb : motive b)
(hl : (b : β) (_ : motive b) (a : α) (_ : a x :: l), motive (op a b)) :
foldrRecOn (x :: l) op b hb hl =
hl _ (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m))
x (mem_cons_self x l) :=
rfl
/--
We can prove that two folds over the same list are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the list,
preserves the relation.
-/
theorem foldl_rel {l : List α} {f g : β α β} {a b : β} (r : β β Prop)
(h : r a b) (h' : (a : α), a l (c c' : β), r c c' r (f c a) (g c' a)) :
r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
induction l generalizing a b with
| nil => simp_all
| cons a l ih =>
simp only [foldl_cons]
apply ih
· simp_all
· exact fun a m c c' h => h' _ (by simp_all) _ _ h
/--
We can prove that two folds over the same list are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the list,
preserves the relation.
-/
theorem foldr_rel {l : List α} {f g : α β β} {a b : β} (r : β β Prop)
(h : r a b) (h' : (a : α), a l (c c' : β), r c c' r (f a c) (g a c')) :
r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
induction l generalizing a b with
| nil => simp_all
| cons a l ih =>
simp only [foldr_cons]
apply h'
· simp
· exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h
@[simp] theorem foldl_add_const (l : List α) (a b : Nat) :
l.foldl (fun x _ => x + a) b = b + a * l.length := by
induction l generalizing b with
| nil => simp
| cons y l ih =>
simp only [foldl_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc,
Nat.add_comm a]
@[simp] theorem foldr_add_const (l : List α) (a b : Nat) :
l.foldr (fun _ x => x + a) b = b + a * l.length := by
induction l generalizing b with
| nil => simp
| cons y l ih =>
simp only [foldr_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc]
@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
eq_replicate_iff.2
by rw [length_reverse, length_replicate],
fun _ h => eq_of_mem_replicate (mem_reverse.1 h)
/-! #### Further results about `getLast` and `getLast?` -/

View File

@@ -14,8 +14,8 @@ namespace List
@[simp] theorem lex_lt [LT α] (l₁ l₂ : List α) : Lex (· < ·) l₁ l₂ l₁ < l₂ := Iff.rfl
@[simp] theorem not_lex_lt [LT α] (l₁ l₂ : List α) : ¬ Lex (· < ·) l₁ l₂ l₂ l₁ := Iff.rfl
protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ l₂ l₁ := Iff.rfl
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ l₂ l₁ := Iff.rfl
theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
¬ l₁ l₂ l₂ < l₁ :=
Decidable.not_not
@@ -260,7 +260,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
· exfalso
exact h' h
protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
[Std.Total (¬ · < · : α α Prop)]
@@ -333,7 +333,7 @@ theorem lex_eq_true_iff_exists [BEq α] (lt : αα → Bool) :
cases l₂ with
| nil => simp [lex]
| cons b l₂ =>
simp [lex_cons_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
simp only [lex_cons_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
constructor
· rintro (hab | hab, h₁, h₂ | i, h₁, h₂, w₁, w₂)
· exact .inr 0, by simp [hab]
@@ -397,7 +397,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : αα
cases l₂ with
| nil => simp [lex]
| cons b l₂ =>
simp [lex_cons_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
simp only [lex_cons_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
Bool.and_eq_true, length_cons]
constructor
· rintro hab, h
@@ -435,7 +435,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : αα
simpa using w₁ (j + 1) (by simpa)
· simpa using w₂
protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
l₁ < l₂
(l₁ = l₂.take l₁.length l₁.length < l₂.length)
( (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
@@ -444,7 +444,7 @@ protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁
rw [ lex_eq_true_iff_lt, lex_eq_true_iff_exists]
simp
protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α α Prop)]
[Std.Asymm (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)] {l₁ l₂ : List α} :
@@ -489,7 +489,7 @@ theorem IsPrefix.le [LT α] [Std.Irrefl (· < · : αα → Prop)]
rcases h with _, rfl
apply le_append_left
protected theorem map_lt [LT α] [LT β]
theorem map_lt [LT α] [LT β]
{l₁ l₂ : List α} {f : α β} (w : x y, x < y f x < f y) (h : l₁ < l₂) :
map f l₁ < map f l₂ := by
match l₁, l₂, h with
@@ -497,11 +497,11 @@ protected theorem map_lt [LT α] [LT β]
| nil, cons b l₂, h => simp
| cons a l₁, nil, h => simp at h
| cons a l₁, cons _ l₂, .cons h =>
simp [cons_lt_cons_iff, List.map_lt w (by simpa using h)]
simp [cons_lt_cons_iff, map_lt w (by simpa using h)]
| cons a l₁, cons b l₂, .rel h =>
simp [cons_lt_cons_iff, w, h]
protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
[Std.Irrefl (· < · : α α Prop)]
[Std.Asymm (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
@@ -510,7 +510,7 @@ protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq
[Std.Antisymm (¬ · < · : β β Prop)]
{l₁ l₂ : List α} {f : α β} (w : x y, x < y f x < f y) (h : l₁ l₂) :
map f l₁ map f l₂ := by
rw [List.le_iff_exists] at h
rw [le_iff_exists] at h
obtain (h | i, h₁, h₂, w₁, w₂) := h
· left
rw [h]

View File

@@ -510,18 +510,4 @@ theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
exact fun h h₁ h₂ => h h₂ h₁
theorem perm_insertIdx {α} (x : α) (l : List α) {n} (h : n l.length) :
insertIdx n x l ~ x :: l := by
induction l generalizing n with
| nil =>
cases n with
| zero => rfl
| succ => cases h
| cons _ _ ih =>
cases n with
| zero => simp [insertIdx]
| succ =>
simp only [insertIdx, modifyTailIdx]
refine .trans (.cons _ (ih (Nat.le_of_succ_le_succ h))) (.swap ..)
end List

View File

@@ -253,10 +253,6 @@ theorem merge_perm_append : ∀ {xs ys : List α}, merge xs ys le ~ xs ++ ys
· exact (merge_perm_append.cons y).trans
((Perm.swap x y _).trans (perm_middle.symm.cons x))
theorem Perm.merge (s₁ s₂ : α α Bool) (hl : l₁ ~ l₂) (hr : r₁ ~ r₂) :
merge l₁ r₁ s₁ ~ merge l₂ r₂ s₂ :=
Perm.trans (merge_perm_append ..) <| Perm.trans (Perm.append hl hr) <| Perm.symm (merge_perm_append ..)
/-! ### mergeSort -/
@[simp] theorem mergeSort_nil : [].mergeSort r = [] := by rw [List.mergeSort]

View File

@@ -259,7 +259,7 @@ theorem zip_map (f : αγ) (g : β → δ) :
| [], _ => rfl
| _, [] => by simp only [map, zip_nil_right]
| _ :: _, _ :: _ => by
simp only [map, zip_cons_cons, zip_map, Prod.map]; try constructor -- TODO: remove try constructor after update stage0
simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
theorem zip_map_left (f : α γ) (l₁ : List α) (l₂ : List β) :
zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [ zip_map, map_id]

View File

@@ -49,17 +49,4 @@ theorem lt_div_mul_self (h : 0 < k) (w : k ≤ x) : x - k < x / k * k := by
have : x % k < k := mod_lt x h
omega
theorem div_pos (hba : b a) (hb : 0 < b) : 0 < a / b := by
cases b
· contradiction
· simp [Nat.pos_iff_ne_zero, div_eq_zero_iff_lt, hba]
theorem div_le_div_left (hcb : c b) (hc : 0 < c) : a / b a / c :=
(Nat.le_div_iff_mul_le hc).2 <|
Nat.le_trans (Nat.mul_le_mul_left _ hcb) (Nat.div_mul_le_self a b)
theorem div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) :
x / (y + z) x / z :=
div_le_div_left (Nat.le_add_left z y) h
end Nat

View File

@@ -159,8 +159,6 @@ def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
def UInt32.shiftLeft (a b : UInt32) : UInt32 := a.toBitVec <<< (mod b 32).toBitVec
@[extern "lean_uint32_shift_right"]
def UInt32.shiftRight (a b : UInt32) : UInt32 := a.toBitVec >>> (mod b 32).toBitVec
def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
def UInt32.le (a b : UInt32) : Prop := a.toBitVec b.toBitVec
instance : Add UInt32 := UInt32.add
instance : Sub UInt32 := UInt32.sub
@@ -171,8 +169,6 @@ set_option linter.deprecated false in
instance : HMod UInt32 Nat UInt32 := UInt32.modn
instance : Div UInt32 := UInt32.div
instance : LT UInt32 := UInt32.lt
instance : LE UInt32 := UInt32.le
@[extern "lean_uint32_complement"]
def UInt32.complement (a : UInt32) : UInt32 := ~~~a.toBitVec

View File

@@ -103,7 +103,7 @@ of bounds.
@[inline] def head [NeZero n] (v : Vector α n) := v[0]'(Nat.pos_of_neZero n)
/-- Push an element `x` to the end of a vector. -/
@[inline] def push (v : Vector α n) (x : α) : Vector α (n + 1) :=
@[inline] def push (x : α) (v : Vector α n) : Vector α (n + 1) :=
v.toArray.push x, by simp
/-- Remove the last element of a vector. -/
@@ -136,18 +136,6 @@ This will perform the update destructively provided that the vector has a refere
@[inline] def set! (v : Vector α n) (i : Nat) (x : α) : Vector α n :=
v.toArray.set! i x, by simp
@[inline] def foldlM [Monad m] (f : β α m β) (b : β) (v : Vector α n) : m β :=
v.toArray.foldlM f b
@[inline] def foldrM [Monad m] (f : α β m β) (b : β) (v : Vector α n) : m β :=
v.toArray.foldrM f b
@[inline] def foldl (f : β α β) (b : β) (v : Vector α n) : β :=
v.toArray.foldl f b
@[inline] def foldr (f : α β β) (b : β) (v : Vector α n) : β :=
v.toArray.foldr f b
/-- Append two vectors. -/
@[inline] def append (v : Vector α n) (w : Vector α m) : Vector α (n + m) :=
v.toArray ++ w.toArray, by simp

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2024 Shreyas Srinivas. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison
Authors: Shreyas Srinivas, Francois Dorais
-/
prelude
import Init.Data.Vector.Basic
@@ -66,18 +66,6 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
@[simp] theorem back?_mk (a : Array α) (h : a.size = n) :
(Vector.mk a h).back? = a.back? := rfl
@[simp] theorem foldlM_mk [Monad m] (f : β α m β) (b : β) (a : Array α) (h : a.size = n) :
(Vector.mk a h).foldlM f b = a.foldlM f b := rfl
@[simp] theorem foldrM_mk [Monad m] (f : α β m β) (b : β) (a : Array α) (h : a.size = n) :
(Vector.mk a h).foldrM f b = a.foldrM f b := rfl
@[simp] theorem foldl_mk (f : β α β) (b : β) (a : Array α) (h : a.size = n) :
(Vector.mk a h).foldl f b = a.foldl f b := rfl
@[simp] theorem foldr_mk (f : α β β) (b : β) (a : Array α) (h : a.size = n) :
(Vector.mk a h).foldr f b = a.foldr f b := rfl
@[simp] theorem drop_mk (a : Array α) (h : a.size = n) (m) :
(Vector.mk a h).drop m = Vector.mk (a.extract m a.size) (by simp [h]) := rfl
@@ -153,14 +141,6 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
@[simp] theorem all_mk (p : α Bool) (a : Array α) (h : a.size = n) :
(Vector.mk a h).all p = a.all p := rfl
@[simp] theorem eq_mk : v = Vector.mk a h v.toArray = a := by
cases v
simp
@[simp] theorem mk_eq : Vector.mk a h = v a = v.toArray := by
cases v
simp
/-! ### toArray lemmas -/
@[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
@@ -1043,12 +1023,11 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
cases l₂
simp
/-! ### map -/
/-! Content below this point has not yet been aligned with `List` and `Array`. -/
@[simp] theorem getElem_map (f : α β) (a : Vector α n) (i : Nat) (hi : i < n) :
(a.map f)[i] = f a[i] := by
cases a
simp
@[simp] theorem getElem_ofFn {α n} (f : Fin n α) (i : Nat) (h : i < n) :
(Vector.ofFn f)[i] = f i, by simpa using h := by
simp [ofFn]
/-- The empty vector maps to the empty vector. -/
@[simp]
@@ -1056,123 +1035,6 @@ theorem map_empty (f : α → β) : map f #v[] = #v[] := by
rw [map, mk.injEq]
exact Array.map_empty f
@[simp] theorem map_push {f : α β} {as : Vector α n} {x : α} :
(as.push x).map f = (as.map f).push (f x) := by
cases as
simp
@[simp] theorem map_id_fun : map (n := n) (id : α α) = id := by
funext l
induction l <;> simp_all
/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
@[simp] theorem map_id_fun' : map (n := n) (fun (a : α) => a) = id := map_id_fun
-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
theorem map_id (l : Vector α n) : map (id : α α) l = l := by
cases l <;> simp_all
/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
theorem map_id' (l : Vector α n) : map (fun (a : α) => a) l = l := map_id l
/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
theorem map_id'' {f : α α} (h : x, f x = x) (l : Vector α n) : map f l = l := by
simp [show f = id from funext h]
theorem map_singleton (f : α β) (a : α) : map f #v[a] = #v[f a] := rfl
@[simp] theorem mem_map {f : α β} {l : Vector α n} : b l.map f a, a l f a = b := by
cases l
simp
theorem exists_of_mem_map (h : b map f l) : a, a l f a = b := mem_map.1 h
theorem mem_map_of_mem (f : α β) (h : a l) : f a map f l := mem_map.2 _, h, rfl
theorem forall_mem_map {f : α β} {l : Vector α n} {P : β Prop} :
( (i) (_ : i l.map f), P i) (j) (_ : j l), P (f j) := by
simp
@[simp] theorem map_inj_left {f g : α β} : map f l = map g l a l, f a = g a := by
cases l <;> simp_all
theorem map_congr_left (h : a l, f a = g a) : map f l = map g l :=
map_inj_left.2 h
theorem map_inj [NeZero n] : map (n := n) f = map g f = g := by
constructor
· intro h
ext a
replace h := congrFun h (mkVector n a)
simp only [mkVector, map_mk, mk.injEq, Array.map_inj_left, Array.mem_mkArray, and_imp,
forall_eq_apply_imp_iff] at h
exact h (NeZero.ne n)
· intro h; subst h; rfl
theorem map_eq_push_iff {f : α β} {l : Vector α (n + 1)} {l₂ : Vector β n} {b : β} :
map f l = l₂.push b l₁ a, l = l₁.push a map f l₁ = l₂ f a = b := by
rcases l with l, h
rcases l₂ with l₂, rfl
simp only [map_mk, push_mk, mk.injEq, Array.map_eq_push_iff]
constructor
· rintro l₁, a, rfl, rfl, rfl
refine l₁, by simp, a, by simp
· rintro l₁, a, h₁, h₂, rfl
refine l₁.toArray, a, by simp_all
@[simp] theorem map_eq_singleton_iff {f : α β} {l : Vector α 1} {b : β} :
map f l = #v[b] a, l = #v[a] f a = b := by
cases l
simp
theorem map_eq_map_iff {f g : α β} {l : Vector α n} :
map f l = map g l a l, f a = g a := by
cases l <;> simp_all
theorem map_eq_iff {f : α β} {l : Vector α n} {l' : Vector β n} :
map f l = l' i (h : i < n), l'[i] = f l[i] := by
rcases l with l, rfl
rcases l' with l', h'
simp only [map_mk, eq_mk, Array.map_eq_iff, getElem_mk]
constructor
· intro w i h
simpa [h, h'] using w i
· intro w i
if h : i < l.size then
simpa [h, h'] using w i h
else
rw [getElem?_neg, getElem?_neg, Option.map_none'] <;> omega
@[simp] theorem map_set {f : α β} {l : Vector α n} {i : Nat} {h : i < n} {a : α} :
(l.set i a).map f = (l.map f).set i (f a) (by simpa using h) := by
cases l
simp
@[simp] theorem map_setIfInBounds {f : α β} {l : Vector α n} {i : Nat} {a : α} :
(l.setIfInBounds i a).map f = (l.map f).setIfInBounds i (f a) := by
cases l
simp
@[simp] theorem map_pop {f : α β} {l : Vector α n} : l.pop.map f = (l.map f).pop := by
cases l
simp
@[simp] theorem back?_map {f : α β} {l : Vector α n} : (l.map f).back? = l.back?.map f := by
cases l
simp
@[simp] theorem map_map {f : α β} {g : β γ} {as : Vector α n} :
(as.map f).map g = as.map (g f) := by
cases as
simp
/-! Content below this point has not yet been aligned with `List` and `Array`. -/
@[simp] theorem getElem_ofFn {α n} (f : Fin n α) (i : Nat) (h : i < n) :
(Vector.ofFn f)[i] = f i, by simpa using h := by
simp [ofFn]
@[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
rcases v with data, rfl
simp
@@ -1226,6 +1088,13 @@ theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h :
cases a
simp
/-! ### map -/
@[simp] theorem getElem_map (f : α β) (a : Vector α n) (i : Nat) (hi : i < n) :
(a.map f)[i] = f a[i] := by
cases a
simp
/-! ### zipWith -/
@[simp] theorem getElem_zipWith (f : α β γ) (a : Vector α n) (b : Vector β n) (i : Nat)
@@ -1234,37 +1103,6 @@ theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h :
cases b
simp
/-! ### foldlM and foldrM -/
@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β α m β) (b) (l : Vector α n) (l' : Vector α n') :
(l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
cases l
cases l'
simp
@[simp] theorem foldrM_push [Monad m] (f : α β m β) (init : β) (l : Vector α n) (a : α) :
(l.push a).foldrM f init = f a init >>= l.foldrM f := by
cases l
simp
theorem foldl_eq_foldlM (f : β α β) (b) (l : Vector α n) :
l.foldl f b = l.foldlM (m := Id) f b := by
cases l
simp [Array.foldl_eq_foldlM]
theorem foldr_eq_foldrM (f : α β β) (b) (l : Vector α n) :
l.foldr f b = l.foldrM (m := Id) f b := by
cases l
simp [Array.foldr_eq_foldrM]
@[simp] theorem id_run_foldlM (f : β α Id β) (b) (l : Vector α n) :
Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
@[simp] theorem id_run_foldrM (f : α β Id β) (b) (l : Vector α n) :
Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
/-! ### foldl and foldr -/
/-! ### take -/
@[simp] theorem take_size (a : Vector α n) : a.take n = a.cast (by simp) := by

View File

@@ -19,11 +19,6 @@ namespace Vector
@[simp] theorem lt_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList < l₂.toList l₁ < l₂ := Iff.rfl
@[simp] theorem le_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList l₂.toList l₁ l₂ := Iff.rfl
protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : Vector α n) : ¬ l₁ < l₂ l₂ l₁ := Iff.rfl
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : Vector α n) :
¬ l₁ l₂ l₂ < l₁ :=
Decidable.not_not
@[simp] theorem mk_lt_mk [LT α] :
Vector.mk (α := α) (n := n) data₁ size₁ < Vector.mk data₂ size₂ data₁ < data₂ := Iff.rfl
@@ -138,7 +133,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
{l₁ l₂ : Vector α n} (h : l₁ < l₂) : l₁ l₂ :=
Array.le_of_lt h
protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]
[Std.Total (¬ · < · : α α Prop)]
@@ -205,14 +200,14 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : αα
rcases l₂ with l₂, n₂
simp_all [Array.lex_eq_false_iff_exists, n₂]
protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} :
theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} :
l₁ < l₂
( (i : Nat) (h : i < n), ( j, (hj : j < i) l₁[j] = l₂[j]) l₁[i] < l₂[i]) := by
cases l₁
cases l₂
simp_all [Array.lt_iff_exists]
protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α α Prop)]
[Std.Asymm (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)] {l₁ l₂ : Vector α n} :
@@ -235,12 +230,12 @@ theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
l₁ ++ l₂ l₁ ++ l₃ := by
simpa using Array.append_left_le h
protected theorem map_lt [LT α] [LT β]
theorem map_lt [LT α] [LT β]
{l₁ l₂ : Vector α n} {f : α β} (w : x y, x < y f x < f y) (h : l₁ < l₂) :
map f l₁ < map f l₂ := by
simpa using Array.map_lt w h
protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
[Std.Irrefl (· < · : α α Prop)]
[Std.Asymm (· < · : α α Prop)]
[Std.Antisymm (¬ · < · : α α Prop)]

View File

@@ -8,6 +8,3 @@ import Init.Grind.Norm
import Init.Grind.Tactics
import Init.Grind.Lemmas
import Init.Grind.Cases
import Init.Grind.Propagator
import Init.Grind.Util
import Init.Grind.Offset

View File

@@ -5,96 +5,10 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Core
import Init.SimpLemmas
import Init.Classical
import Init.ByCases
import Init.Grind.Util
namespace Lean.Grind
theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' q) : p q :=
fun hp => h (he.mp hp)
/-! And -/
theorem and_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a b) = b := by simp [h]
theorem and_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a b) = a := by simp [h]
theorem and_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a b) = False := by simp [h]
theorem and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a b) = False := by simp [h]
theorem eq_true_of_and_eq_true_left {a b : Prop} (h : (a b) = True) : a = True := by simp_all
theorem eq_true_of_and_eq_true_right {a b : Prop} (h : (a b) = True) : b = True := by simp_all
theorem or_of_and_eq_false {a b : Prop} (h : (a b) = False) : (¬a ¬b) := by
by_cases a <;> by_cases b <;> simp_all
/-! Or -/
theorem or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a b) = True := by simp [h]
theorem or_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a b) = True := by simp [h]
theorem or_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a b) = b := by simp [h]
theorem or_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a b) = a := by simp [h]
theorem eq_false_of_or_eq_false_left {a b : Prop} (h : (a b) = False) : a = False := by simp_all
theorem eq_false_of_or_eq_false_right {a b : Prop} (h : (a b) = False) : b = False := by simp_all
/-! Implies -/
theorem imp_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a b) = True := by simp [h]
theorem imp_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a b) = True := by simp [h]
theorem imp_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a b) = b := by simp [h]
theorem eq_true_of_imp_eq_false {a b : Prop} (h : (a b) = False) : a = True := by simp_all
theorem eq_false_of_imp_eq_false {a b : Prop} (h : (a b) = False) : b = False := by simp_all
/-! Not -/
theorem not_eq_of_eq_true {a : Prop} (h : a = True) : (Not a) = False := by simp [h]
theorem not_eq_of_eq_false {a : Prop} (h : a = False) : (Not a) = True := by simp [h]
theorem eq_false_of_not_eq_true {a : Prop} (h : (Not a) = True) : a = False := by simp_all
theorem eq_true_of_not_eq_false {a : Prop} (h : (Not a) = False) : a = True := by simp_all
theorem false_of_not_eq_self {a : Prop} (h : (Not a) = a) : False := by
by_cases a <;> simp_all
/-! Eq -/
theorem eq_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a = b) = b := by simp [h]
theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by simp [h]
theorem eq_congr {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂) := by simp [*]
theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂) := by rw [h₁, h₂, Eq.comm (a := a₂)]
/-! Forall -/
theorem forall_propagator (p : Prop) (q : p Prop) (q' : Prop) (h₁ : p = True) (h₂ : q (of_eq_true h₁) = q') : ( hp : p, q hp) = q' := by
apply propext; apply Iff.intro
· intro h'; exact Eq.mp h₂ (h' (of_eq_true h₁))
· intro h'; intros; exact Eq.mpr h₂ h'
theorem of_forall_eq_false (α : Sort u) (p : α Prop) (h : ( x : α, p x) = False) : x : α, ¬ p x := by simp_all
/-! dite -/
theorem dite_cond_eq_true' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c α} {b : ¬ c α} {r : α} (h₁ : c = True) (h₂ : a (of_eq_true h₁) = r) : (dite c a b) = r := by simp [h₁, h₂]
theorem dite_cond_eq_false' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c α} {b : ¬ c α} {r : α} (h₁ : c = False) (h₂ : b (of_eq_false h₁) = r) : (dite c a b) = r := by simp [h₁, h₂]
/-! Casts -/
theorem eqRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
{motive : (x : α) a = x Sort u_1} (v : motive a (Eq.refl a)) {b : α} (h : a = b)
: HEq (@Eq.rec α a motive v b h) v := by
subst h; rfl
theorem eqRecOn_heq.{u_1, u_2} {α : Sort u_2} {a : α}
{motive : (x : α) a = x Sort u_1} {b : α} (h : a = b) (v : motive a (Eq.refl a))
: HEq (@Eq.recOn α a motive b h v) v := by
subst h; rfl
theorem eqNDRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
{motive : α Sort u_1} (v : motive a) {b : α} (h : a = b)
: HEq (@Eq.ndrec α a motive v b h) v := by
subst h; rfl
end Lean.Grind

View File

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
-/
prelude
import Init.SimpLemmas
import Init.PropLemmas
import Init.Classical
import Init.ByCases
@@ -41,10 +40,9 @@ attribute [grind_norm] not_true
-- False
attribute [grind_norm] not_false_eq_true
-- Remark: we disabled the following normalization rule because we want this information when implementing splitting heuristics
-- Implication as a clause
-- @[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p q) := by
-- by_cases p <;> by_cases q <;> simp [*]
@[grind_norm] theorem imp_eq (p q : Prop) : (p q) = (¬ p q) := by
by_cases p <;> by_cases q <;> simp [*]
-- And
@[grind_norm] theorem not_and (p q : Prop) : (¬(p q)) = (¬p ¬q) := by
@@ -60,19 +58,13 @@ attribute [grind_norm] ite_true ite_false
@[grind_norm] theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
by_cases p <;> simp [*]
@[grind_norm] theorem ite_true_false {_ : Decidable p} : (ite p True False) = p := by
by_cases p <;> simp
@[grind_norm] theorem ite_false_true {_ : Decidable p} : (ite p False True) = ¬p := by
by_cases p <;> simp
-- Forall
@[grind_norm] theorem not_forall (p : α Prop) : (¬ x, p x) = x, ¬p x := by simp
attribute [grind_norm] forall_and
-- Exists
@[grind_norm] theorem not_exists (p : α Prop) : (¬ x, p x) = x, ¬p x := by simp
attribute [grind_norm] exists_const exists_or exists_prop exists_and_left exists_and_right
attribute [grind_norm] exists_const exists_or
-- Bool cond
@[grind_norm] theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
@@ -115,7 +107,4 @@ attribute [grind_norm] Nat.le_zero_eq
-- GT GE
attribute [grind_norm] GT.gt GE.ge
-- Succ
attribute [grind_norm] Nat.succ_eq_add_one
end Lean.Grind

View File

@@ -1,165 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Core
import Init.Omega
namespace Lean.Grind.Offset
abbrev Var := Nat
abbrev Context := Lean.RArray Nat
def fixedVar := 100000000 -- Any big number should work here
def Var.denote (ctx : Context) (v : Var) : Nat :=
bif v == fixedVar then 1 else ctx.get v
structure Cnstr where
x : Var
y : Var
k : Nat := 0
l : Bool := true
deriving Repr, DecidableEq, Inhabited
def Cnstr.denote (c : Cnstr) (ctx : Context) : Prop :=
if c.l then
c.x.denote ctx + c.k c.y.denote ctx
else
c.x.denote ctx c.y.denote ctx + c.k
def trivialCnstr : Cnstr := { x := 0, y := 0, k := 0, l := true }
@[simp] theorem denote_trivial (ctx : Context) : trivialCnstr.denote ctx := by
simp [Cnstr.denote, trivialCnstr]
def Cnstr.trans (c₁ c₂ : Cnstr) : Cnstr :=
if c₁.y = c₂.x then
let { x, k := k₁, l := l₁, .. } := c₁
let { y, k := k₂, l := l₂, .. } := c₂
match l₁, l₂ with
| false, false =>
{ x, y, k := k₁ + k₂, l := false }
| false, true =>
if k₁ < k₂ then
{ x, y, k := k₂ - k₁, l := true }
else
{ x, y, k := k₁ - k₂, l := false }
| true, false =>
if k₁ < k₂ then
{ x, y, k := k₂ - k₁, l := false }
else
{ x, y, k := k₁ - k₂, l := true }
| true, true =>
{ x, y, k := k₁ + k₂, l := true }
else
trivialCnstr
@[simp] theorem Cnstr.denote_trans_easy (ctx : Context) (c₁ c₂ : Cnstr) (h : c₁.y c₂.x) : (c₁.trans c₂).denote ctx := by
simp [*, Cnstr.trans]
@[simp] theorem Cnstr.denote_trans (ctx : Context) (c₁ c₂ : Cnstr) : c₁.denote ctx c₂.denote ctx (c₁.trans c₂).denote ctx := by
by_cases c₁.y = c₂.x
case neg => simp [*]
simp [trans, *]
let { x, k := k₁, l := l₁, .. } := c₁
let { y, k := k₂, l := l₂, .. } := c₂
simp_all; split
· simp [denote]; omega
· split <;> simp [denote] <;> omega
· split <;> simp [denote] <;> omega
· simp [denote]; omega
def Cnstr.isTrivial (c : Cnstr) : Bool := c.x == c.y && c.k == 0
theorem Cnstr.of_isTrivial (ctx : Context) (c : Cnstr) : c.isTrivial = true c.denote ctx := by
cases c; simp [isTrivial]; intros; simp [*, denote]
def Cnstr.isFalse (c : Cnstr) : Bool := c.x == c.y && c.k != 0 && c.l == true
theorem Cnstr.of_isFalse (ctx : Context) {c : Cnstr} : c.isFalse = true ¬c.denote ctx := by
cases c; simp [isFalse]; intros; simp [*, denote]; omega
def Cnstrs := List Cnstr
def Cnstrs.denoteAnd' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : Prop :=
match c₂ with
| [] => c₁.denote ctx
| c::cs => c₁.denote ctx Cnstrs.denoteAnd' ctx c cs
theorem Cnstrs.denote'_trans (ctx : Context) (c₁ c : Cnstr) (cs : Cnstrs) : c₁.denote ctx denoteAnd' ctx c cs denoteAnd' ctx (c₁.trans c) cs := by
induction cs
next => simp [denoteAnd', *]; apply Cnstr.denote_trans
next c cs ih => simp [denoteAnd']; intros; simp [*]
def Cnstrs.trans' (c₁ : Cnstr) (c₂ : Cnstrs) : Cnstr :=
match c₂ with
| [] => c₁
| c::c₂ => trans' (c₁.trans c) c₂
@[simp] theorem Cnstrs.denote'_trans' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : denoteAnd' ctx c₁ c₂ (trans' c₁ c₂).denote ctx := by
induction c₂ generalizing c₁
next => intros; simp_all [trans', denoteAnd']
next c cs ih => simp [denoteAnd']; intros; simp [trans']; apply ih; apply denote'_trans <;> assumption
def Cnstrs.denoteAnd (ctx : Context) (c : Cnstrs) : Prop :=
match c with
| [] => True
| c::cs => denoteAnd' ctx c cs
def Cnstrs.trans (c : Cnstrs) : Cnstr :=
match c with
| [] => trivialCnstr
| c::cs => trans' c cs
theorem Cnstrs.of_denoteAnd_trans {ctx : Context} {c : Cnstrs} : c.denoteAnd ctx c.trans.denote ctx := by
cases c <;> simp [*, trans, denoteAnd] <;> intros <;> simp [*]
def Cnstrs.isFalse (c : Cnstrs) : Bool :=
c.trans.isFalse
theorem Cnstrs.unsat' (ctx : Context) (c : Cnstrs) : c.isFalse = true ¬ c.denoteAnd ctx := by
simp [isFalse]; intro h₁ h₂
have := of_denoteAnd_trans h₂
have := Cnstr.of_isFalse ctx h₁
contradiction
/-- `denote ctx [c_1, ..., c_n] C` is `c_1.denote ctx → ... → c_n.denote ctx → C` -/
def Cnstrs.denote (ctx : Context) (cs : Cnstrs) (C : Prop) : Prop :=
match cs with
| [] => C
| c::cs => c.denote ctx denote ctx cs C
theorem Cnstrs.not_denoteAnd'_eq (ctx : Context) (c : Cnstr) (cs : Cnstrs) (C : Prop) : (denoteAnd' ctx c cs C) = denote ctx (c::cs) C := by
simp [denote]
induction cs generalizing c
next => simp [denoteAnd', denote]
next c' cs ih =>
simp [denoteAnd', denote, *]
theorem Cnstrs.not_denoteAnd_eq (ctx : Context) (cs : Cnstrs) (C : Prop) : (denoteAnd ctx cs C) = denote ctx cs C := by
cases cs
next => simp [denoteAnd, denote]
next c cs => apply not_denoteAnd'_eq
def Cnstr.isImpliedBy (cs : Cnstrs) (c : Cnstr) : Bool :=
cs.trans == c
/-! Main theorems used by `grind`. -/
/-- Auxiliary theorem used by `grind` to prove that a system of offset inequalities is unsatisfiable. -/
theorem Cnstrs.unsat (ctx : Context) (cs : Cnstrs) : cs.isFalse = true cs.denote ctx False := by
intro h
rw [ not_denoteAnd_eq]
apply unsat'
assumption
/-- Auxiliary theorem used by `grind` to prove an implied offset inequality. -/
theorem Cnstrs.imp (ctx : Context) (cs : Cnstrs) (c : Cnstr) (h : c.isImpliedBy cs = true) : cs.denote ctx (c.denote ctx) := by
rw [ eq_of_beq h]
rw [ not_denoteAnd_eq]
apply of_denoteAnd_trans
end Lean.Grind.Offset

View File

@@ -1,27 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.NotationExtra
namespace Lean.Parser
/-- A user-defined propagator for the `grind` tactic. -/
-- TODO: not implemented yet
syntax (docComment)? "grind_propagator " (Tactic.simpPre <|> Tactic.simpPost) ident " (" ident ")" " := " term : command
/-- A builtin propagator for the `grind` tactic. -/
syntax (docComment)? "builtin_grind_propagator " ident (Tactic.simpPre <|> Tactic.simpPost) ident " := " term : command
/-- Auxiliary attribute for builtin `grind` propagators. -/
syntax (name := grindPropagatorBuiltinAttr) "builtin_grind_propagator" (Tactic.simpPre <|> Tactic.simpPost) ident : attr
macro_rules
| `($[$doc?:docComment]? builtin_grind_propagator $propagatorName:ident $direction $op:ident := $body) => do
let propagatorType := `Lean.Meta.Grind.Propagator
`($[$doc?:docComment]? def $propagatorName:ident : $(mkIdent propagatorType) := $body
attribute [builtin_grind_propagator $direction $op] $propagatorName)
end Lean.Parser

View File

@@ -6,56 +6,20 @@ Authors: Leonardo de Moura
prelude
import Init.Tactics
namespace Lean.Parser.Attr
syntax grindEq := "="
syntax grindEqBoth := atomic("_" "=" "_")
syntax grindEqRhs := atomic("=" "_")
syntax grindBwd := ""
syntax grindFwd := ""
syntax (name := grind) "grind" (grindEqBoth <|> grindEqRhs <|> grindEq <|> grindBwd <|> grindFwd)? : attr
end Lean.Parser.Attr
namespace Lean.Grind
/--
The configuration for `grind`.
Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
Passed to `grind` using, for example, the `grind (config := { eager := true })` syntax.
-/
structure Config where
/-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
splits : Nat := 5
/-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
ematch : Nat := 5
/--
Maximum term generation.
The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain. -/
gen : Nat := 5
/-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
instances : Nat := 1000
/-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
matchEqs : Bool := true
/-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
splitMatch : Bool := true
/-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
splitIte : Bool := true
/--
If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
Otherwise, it performs case-splitting only on types marked with `[grind_split]` attribute. -/
splitIndPred : Bool := true
When `eager` is true (default: `false`), `grind` eagerly splits `if-then-else` and `match`
expressions.
-/
eager : Bool := false
deriving Inhabited, BEq
end Lean.Grind
namespace Lean.Parser.Tactic
/-!
`grind` tactic and related tactics.
-/
-- TODO: parameters
syntax (name := grind) "grind" optConfig ("on_failure " term)? : tactic
end Lean.Parser.Tactic
end Lean.Grind

View File

@@ -1,34 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Core
namespace Lean.Grind
/-- A helper gadget for annotating nested proofs in goals. -/
def nestedProof (p : Prop) (h : p) : p := h
/--
Gadget for marking terms that should not be normalized by `grind`s simplifier.
`grind` uses a simproc to implement this feature.
We use it when adding instances of `match`-equations to prevent them from being simplified to true.
-/
def doNotSimp {α : Sort u} (a : α) : α := a
/-- Gadget for representing offsets `t+k` in patterns. -/
def offset (a b : Nat) : Nat := a + b
/--
Gadget for annotating the equalities in `match`-equations conclusions.
`_origin` is the term used to instantiate the `match`-equation using E-matching.
When `EqMatch a b origin` is `True`, we mark `origin` as a resolved case-split.
-/
def EqMatch (a b : α) {_origin : α} : Prop := a = b
theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (nestedProof p hp) (nestedProof q hq) := by
subst h; apply HEq.refl
end Lean.Grind

View File

@@ -1,13 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner
-/
prelude
import Init.Internal.Order
/-!
This directory is used for components of the standard library that are either considered
implementation details or not yet ready for public consumption, and that should be available
without explicit import (in contrast to `Std.Internal`)
-/

View File

@@ -1,8 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner
-/
prelude
import Init.Internal.Order.Basic
import Init.Internal.Order.Tactic

View File

@@ -1,693 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner
-/
prelude
import Init.ByCases
import Init.RCases
/-!
This module contains some basic definitions and results from domain theory, intended to be used as
the underlying construction of the `partial_fixpoint` feature. It is not meant to be used as a
general purpose library for domain theory, but can be of interest to users who want to extend
the `partial_fixpoint` machinery (e.g. mark more functions as monotone or register more monads).
This follows the corresponding
[Isabelle development](https://isabelle.in.tum.de/library/HOL/HOL/Partial_Function.html), as also
described in [Alexander Krauss: Recursive Definitions of Monadic Functions](https://www21.in.tum.de/~krauss/papers/mrec.pdf).
-/
universe u v w
namespace Lean.Order
/--
A partial order is a reflexive, transitive and antisymmetric relation.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
class PartialOrder (α : Sort u) where
/--
A “less-or-equal-to” or “approximates” relation.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
rel : α α Prop
rel_refl : {x}, rel x x
rel_trans : {x y z}, rel x y rel y z rel x z
rel_antisymm : {x y}, rel x y rel y x x = y
@[inherit_doc] scoped infix:50 "" => PartialOrder.rel
section PartialOrder
variable {α : Sort u} [PartialOrder α]
theorem PartialOrder.rel_of_eq {x y : α} (h : x = y) : x y := by cases h; apply rel_refl
/--
A chain is a totally ordered set (representing a set as a predicate).
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
def chain (c : α Prop) : Prop := x y , c x c y x y y x
end PartialOrder
section CCPO
/--
A chain-complete partial order (CCPO) is a partial order where every chain a least upper bound.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
class CCPO (α : Sort u) extends PartialOrder α where
/--
The least upper bound of a chain.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
csup : (α Prop) α
csup_spec {c : α Prop} (hc : chain c) : csup c x ( y, c y y x)
open PartialOrder CCPO
variable {α : Sort u} [CCPO α]
theorem csup_le {c : α Prop} (hchain : chain c) : ( y, c y y x) csup c x :=
(csup_spec hchain).mpr
theorem le_csup {c : α Prop} (hchain : chain c) {y : α} (hy : c y) : y csup c :=
(csup_spec hchain).mp rel_refl y hy
/--
The bottom element is the least upper bound of the empty chain.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
def bot : α := csup (fun _ => False)
scoped notation "" => bot
theorem bot_le (x : α) : x := by
apply csup_le
· intro x y hx hy; contradiction
· intro x hx; contradiction
end CCPO
section monotone
variable {α : Sort u} [PartialOrder α]
variable {β : Sort v} [PartialOrder β]
/--
A function is monotone if if it maps related elements to releated elements.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
def monotone (f : α β) : Prop := x y, x y f x f y
theorem monotone_const (c : β) : monotone (fun (_ : α) => c) :=
fun _ _ _ => PartialOrder.rel_refl
theorem monotone_id : monotone (fun (x : α) => x) :=
fun _ _ hxy => hxy
theorem monotone_compose
{γ : Sort w} [PartialOrder γ]
{f : α β} {g : β γ}
(hf : monotone f) (hg : monotone g) :
monotone (fun x => g (f x)) := fun _ _ hxy => hg _ _ (hf _ _ hxy)
end monotone
section admissibility
variable {α : Sort u} [CCPO α]
open PartialOrder CCPO
/--
A predicate is admissable if it can be transferred from the elements of a chain to the chains least
upper bound. Such predicates can be used in fixpoint induction.
This definition implies `P ⊥`. Sometimes (e.g. in Isabelle) the empty chain is excluded
from this definition, and `P ⊥` is a separate condition of the induction predicate.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
def admissible (P : α Prop) :=
(c : α Prop), chain c ( x, c x P x) P (csup c)
theorem admissible_const_true : admissible (fun (_ : α) => True) :=
fun _ _ _ => trivial
theorem admissible_and (P Q : α Prop)
(hadm₁ : admissible P) (hadm₂ : admissible Q) : admissible (fun x => P x Q x) :=
fun c hchain h =>
hadm₁ c hchain fun x hx => (h x hx).1,
hadm₂ c hchain fun x hx => (h x hx).2
theorem chain_conj (c P : α Prop) (hchain : chain c) : chain (fun x => c x P x) := by
intro x y hcx, _ hcy, _
exact hchain x y hcx hcy
theorem csup_conj (c P : α Prop) (hchain : chain c) (h : x, c x y, c y x y P y) :
csup c = csup (fun x => c x P x) := by
apply rel_antisymm
· apply csup_le hchain
intro x hcx
obtain y, hcy, hxy, hPy := h x hcx
apply rel_trans hxy; clear x hcx hxy
apply le_csup (chain_conj _ _ hchain) hcy, hPy
· apply csup_le (chain_conj _ _ hchain)
intro x hcx, hPx
apply le_csup hchain hcx
theorem admissible_or (P Q : α Prop)
(hadm₁ : admissible P) (hadm₂ : admissible Q) : admissible (fun x => P x Q x) := by
intro c hchain h
have : ( x, c x y, c y x y P y) ( x, c x y, c y x y Q y) := by
open Classical in
apply Decidable.or_iff_not_imp_left.mpr
intro h'
simp only [not_forall, not_imp, not_exists, not_and] at h'
obtain x, hcx, hx := h'
intro y hcy
cases hchain x y hcx hcy with
| inl hxy =>
refine y, hcy, rel_refl, ?_
cases h y hcy with
| inl hPy => exfalso; apply hx y hcy hxy hPy
| inr hQy => assumption
| inr hyx =>
refine x, hcx, hyx , ?_
cases h x hcx with
| inl hPx => exfalso; apply hx x hcx rel_refl hPx
| inr hQx => assumption
cases this with
| inl hP =>
left
rw [csup_conj (h := hP) (hchain := hchain)]
apply hadm₁ _ (chain_conj _ _ hchain)
intro x hcx, hPx
exact hPx
| inr hQ =>
right
rw [csup_conj (h := hQ) (hchain := hchain)]
apply hadm₂ _ (chain_conj _ _ hchain)
intro x hcx, hQx
exact hQx
def admissible_pi (P : α β Prop)
(hadm₁ : y, admissible (fun x => P x y)) : admissible (fun x => y, P x y) :=
fun c hchain h y => hadm₁ y c hchain fun x hx => h x hx y
end admissibility
section fix
open PartialOrder CCPO
variable {α : Sort u} [CCPO α]
variable {c : α Prop} (hchain : chain c)
/--
The transfinite iteration of a function `f` is a set that is `⊥ ` and is closed under application
of `f` and `csup`.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
inductive iterates (f : α α) : α Prop where
| step : iterates f x iterates f (f x)
| sup {c : α Prop} (hc : chain c) (hi : x, c x iterates f x) : iterates f (csup c)
theorem chain_iterates {f : α α} (hf : monotone f) : chain (iterates f) := by
intros x y hx hy
induction hx generalizing y
case step x hx ih =>
induction hy
case step y hy _ =>
cases ih y hy
· left; apply hf; assumption
· right; apply hf; assumption
case sup c hchain hi ih2 =>
show f x csup c csup c f x
by_cases h : z, c z f x z
· left
obtain z, hz, hfz := h
apply rel_trans hfz
apply le_csup hchain hz
· right
apply csup_le hchain _
intro z hz
rw [not_exists] at h
specialize h z
rw [not_and] at h
specialize h hz
cases ih2 z hz
next => contradiction
next => assumption
case sup c hchain hi ih =>
show rel (csup c) y rel y (csup c)
by_cases h : z, c z rel y z
· right
obtain z, hz, hfz := h
apply rel_trans hfz
apply le_csup hchain hz
· left
apply csup_le hchain _
intro z hz
rw [not_exists] at h
specialize h z
rw [not_and] at h
specialize h hz
cases ih z hz y hy
next => assumption
next => contradiction
theorem rel_f_of_iterates {f : α α} (hf : monotone f) {x : α} (hx : iterates f x) : x f x := by
induction hx
case step ih =>
apply hf
assumption
case sup c hchain hi ih =>
apply csup_le hchain
intro y hy
apply rel_trans (ih y hy)
apply hf
apply le_csup hchain hy
set_option linter.unusedVariables false in
/--
The least fixpoint of a monotone function is the least upper bound of its transfinite iteration.
The `monotone f` assumption is not strictly necessarily for the definition, but without this the
definition is not very meaningful and it simplifies applying theorems like `fix_eq` if every use of
`fix` already has the monotonicty requirement.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
def fix (f : α α) (hmono : monotone f) := csup (iterates f)
/--
The main fixpoint theorem for fixedpoints of monotone functions in chain-complete partial orders.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
theorem fix_eq {f : α α} (hf : monotone f) : fix f hf = f (fix f hf) := by
apply rel_antisymm
· apply rel_f_of_iterates hf
apply iterates.sup (chain_iterates hf)
exact fun _ h => h
· apply le_csup (chain_iterates hf)
apply iterates.step
apply iterates.sup (chain_iterates hf)
intro y hy
exact hy
/--
The fixpoint induction theme: An admissible predicate holds for a least fixpoint if it is preserved
by the fixpoint's function.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
theorem fix_induct {f : α α} (hf : monotone f)
(motive : α Prop) (hadm: admissible motive)
(h : x, motive x motive (f x)) : motive (fix f hf) := by
apply hadm _ (chain_iterates hf)
intro x hiterates
induction hiterates with
| @step x hiter ih => apply h x ih
| @sup c hchain hiter ih => apply hadm c hchain ih
end fix
section fun_order
open PartialOrder
variable {α : Sort u}
variable {β : α Sort v}
variable {γ : Sort w}
instance instOrderPi [ x, PartialOrder (β x)] : PartialOrder ( x, β x) where
rel f g := x, f x g x
rel_refl _ := rel_refl
rel_trans hf hg x := rel_trans (hf x) (hg x)
rel_antisymm hf hg := funext (fun x => rel_antisymm (hf x) (hg x))
theorem monotone_of_monotone_apply [PartialOrder γ] [ x, PartialOrder (β x)] (f : γ ( x, β x))
(h : y, monotone (fun x => f x y)) : monotone f :=
fun x y hxy z => h z x y hxy
theorem monotone_apply [PartialOrder γ] [ x, PartialOrder (β x)] (a : α) (f : γ x, β x)
(h : monotone f) :
monotone (fun x => f x a) := fun _ _ hfg => h _ _ hfg a
theorem chain_apply [ x, PartialOrder (β x)] {c : ( x, β x) Prop} (hc : chain c) (x : α) :
chain (fun y => f, c f f x = y) := by
intro _ _ f, hf, hfeq g, hg, hgeq
subst hfeq; subst hgeq
cases hc f g hf hg
next h => left; apply h x
next h => right; apply h x
def fun_csup [ x, CCPO (β x)] (c : ( x, β x) Prop) (x : α) :=
CCPO.csup (fun y => f, c f f x = y)
instance instCCPOPi [ x, CCPO (β x)] : CCPO ( x, β x) where
csup := fun_csup
csup_spec := by
intro f c hc
constructor
next =>
intro hf g hg x
apply rel_trans _ (hf x); clear hf
apply le_csup (chain_apply hc x)
exact g, hg, rfl
next =>
intro h x
apply csup_le (chain_apply hc x)
intro y z, hz, hyz
subst y
apply h z hz
def admissible_apply [ x, CCPO (β x)] (P : x, β x Prop) (x : α)
(hadm : admissible (P x)) : admissible (fun (f : x, β x) => P x (f x)) := by
intro c hchain h
apply hadm _ (chain_apply hchain x)
rintro _ f, hcf, rfl
apply h _ hcf
def admissible_pi_apply [ x, CCPO (β x)] (P : x, β x Prop) (hadm : x, admissible (P x)) :
admissible (fun (f : x, β x) => x, P x (f x)) := by
apply admissible_pi
intro
apply admissible_apply
apply hadm
end fun_order
section monotone_lemmas
theorem monotone_letFun
{α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β]
(v : γ) (k : α γ β)
(hmono : y, monotone (fun x => k x y)) :
monotone fun (x : α) => letFun v (k x) := hmono v
theorem monotone_ite
{α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β]
(c : Prop) [Decidable c]
(k₁ : α β) (k₂ : α β)
(hmono₁ : monotone k₁) (hmono₂ : monotone k₂) :
monotone fun x => if c then k₁ x else k₂ x := by
split
· apply hmono₁
· apply hmono₂
theorem monotone_dite
{α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β]
(c : Prop) [Decidable c]
(k₁ : α c β) (k₂ : α ¬ c β)
(hmono₁ : monotone k₁) (hmono₂ : monotone k₂) :
monotone fun x => dite c (k₁ x) (k₂ x) := by
split
· apply monotone_apply _ _ hmono₁
· apply monotone_apply _ _ hmono₂
end monotone_lemmas
section pprod_order
open PartialOrder
variable {α : Sort u}
variable {β : Sort v}
variable {γ : Sort w}
instance [PartialOrder α] [PartialOrder β] : PartialOrder (α ×' β) where
rel a b := a.1 b.1 a.2 b.2
rel_refl := rel_refl, rel_refl
rel_trans ha hb := rel_trans ha.1 hb.1, rel_trans ha.2 hb.2
rel_antisymm := fun {a} {b} ha hb => by
cases a; cases b;
dsimp at *
rw [rel_antisymm ha.1 hb.1, rel_antisymm ha.2 hb.2]
theorem monotone_pprod [PartialOrder α] [PartialOrder β] [PartialOrder γ]
{f : γ α} {g : γ β} (hf : monotone f) (hg : monotone g) :
monotone (fun x => PProd.mk (f x) (g x)) :=
fun _ _ h12 => hf _ _ h12, hg _ _ h12
theorem monotone_pprod_fst [PartialOrder α] [PartialOrder β] [PartialOrder γ]
{f : γ α ×' β} (hf : monotone f) : monotone (fun x => (f x).1) :=
fun _ _ h12 => (hf _ _ h12).1
theorem monotone_pprod_snd [PartialOrder α] [PartialOrder β] [PartialOrder γ]
{f : γ α ×' β} (hf : monotone f) : monotone (fun x => (f x).2) :=
fun _ _ h12 => (hf _ _ h12).2
def chain_pprod_fst [CCPO α] [CCPO β] (c : α ×' β Prop) : α Prop := fun a => b, c a, b
def chain_pprod_snd [CCPO α] [CCPO β] (c : α ×' β Prop) : β Prop := fun b => a, c a, b
theorem chain.pprod_fst [CCPO α] [CCPO β] (c : α ×' β Prop) (hchain : chain c) :
chain (chain_pprod_fst c) := by
intro a₁ a₂ b₁, h₁ b₂, h₂
cases hchain a₁, b₁ a₂, b₂ h₁ h₂
case inl h => left; exact h.1
case inr h => right; exact h.1
theorem chain.pprod_snd [CCPO α] [CCPO β] (c : α ×' β Prop) (hchain : chain c) :
chain (chain_pprod_snd c) := by
intro b₁ b₂ a₁, h₁ a₂, h₂
cases hchain a₁, b₁ a₂, b₂ h₁ h₂
case inl h => left; exact h.2
case inr h => right; exact h.2
instance [CCPO α] [CCPO β] : CCPO (α ×' β) where
csup c := CCPO.csup (chain_pprod_fst c), CCPO.csup (chain_pprod_snd c)
csup_spec := by
intro a, b c hchain
dsimp
constructor
next =>
intro h₁, h₂ a', b' cab
constructor <;> dsimp at *
· apply rel_trans ?_ h₁
apply le_csup hchain.pprod_fst
exact b', cab
· apply rel_trans ?_ h₂
apply le_csup hchain.pprod_snd
exact a', cab
next =>
intro h
constructor <;> dsimp
· apply csup_le hchain.pprod_fst
intro a' b', hcab
apply (h _ hcab).1
· apply csup_le hchain.pprod_snd
intro b' a', hcab
apply (h _ hcab).2
theorem admissible_pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : α Prop)
(hadm : admissible P) : admissible (fun (x : α ×' β) => P x.1) := by
intro c hchain h
apply hadm _ hchain.pprod_fst
intro x y, hxy
apply h x,y hxy
theorem admissible_pprod_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : β Prop)
(hadm : admissible P) : admissible (fun (x : α ×' β) => P x.2) := by
intro c hchain h
apply hadm _ hchain.pprod_snd
intro y x, hxy
apply h x,y hxy
end pprod_order
section flat_order
variable {α : Sort u}
set_option linter.unusedVariables false in
/--
`FlatOrder b` wraps the type `α` with the flat partial order generated by `∀ x, b ⊑ x`.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
def FlatOrder {α : Sort u} (b : α) := α
variable {b : α}
/--
The flat partial order generated by `∀ x, b ⊑ x`.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
inductive FlatOrder.rel : (x y : FlatOrder b) Prop where
| bot : rel b x
| refl : rel x x
instance FlatOrder.instOrder : PartialOrder (FlatOrder b) where
rel := rel
rel_refl := .refl
rel_trans {x y z : α} (hxy : rel x y) (hyz : rel y z) := by
cases hxy <;> cases hyz <;> constructor
rel_antisymm {x y : α} (hxy : rel x y) (hyz : rel y x) : x = y := by
cases hxy <;> cases hyz <;> constructor
open Classical in
private theorem Classical.some_spec₂ {α : Sort _} {p : α Prop} {h : a, p a} (q : α Prop)
(hpq : a, p a q a) : q (choose h) := hpq _ <| choose_spec _
noncomputable def flat_csup (c : FlatOrder b Prop) : FlatOrder b := by
by_cases h : (x : FlatOrder b), c x x b
· exact Classical.choose h
· exact b
noncomputable instance FlatOrder.instCCPO : CCPO (FlatOrder b) where
csup := flat_csup
csup_spec := by
intro x c hc
unfold flat_csup
split
next hex =>
apply Classical.some_spec₂ (q := (· x ( y, c y y x)))
clear hex
intro z hz, hnb
constructor
· intro h y hy
apply PartialOrder.rel_trans _ h; clear h
cases hc y z hy hz
next => assumption
next h =>
cases h
· contradiction
· constructor
· intro h
cases h z hz
· contradiction
· constructor
next hnotex =>
constructor
· intro h y hy; clear h
suffices y = b by rw [this]; exact rel.bot
rw [not_exists] at hnotex
specialize hnotex y
rw [not_and] at hnotex
specialize hnotex hy
rw [@Classical.not_not] at hnotex
assumption
· intro; exact rel.bot
theorem admissible_flatOrder (P : FlatOrder b Prop) (hnot : P b) : admissible P := by
intro c hchain h
by_cases h' : (x : FlatOrder b), c x x b
· simp [CCPO.csup, flat_csup, h']
apply Classical.some_spec₂ (q := (P ·))
intro x hcx, hneb
apply h x hcx
· simp [CCPO.csup, flat_csup, h', hnot]
end flat_order
section mono_bind
/--
The class `MonoBind m` indicates that every `m α` has a `PartialOrder`, and that the bind operation
on `m` is monotone in both arguments with regard to that order.
This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
-/
class MonoBind (m : Type u Type v) [Bind m] [ α, PartialOrder (m α)] where
bind_mono_left {a₁ a₂ : m α} {f : α m b} (h : a₁ a₂) : a₁ >>= f a₂ >>= f
bind_mono_right {a : m α} {f₁ f₂ : α m b} (h : x, f₁ x f₂ x) : a >>= f₁ a >>= f₂
theorem monotone_bind
(m : Type u Type v) [Bind m] [ α, PartialOrder (m α)] [MonoBind m]
{α β : Type u}
{γ : Type w} [PartialOrder γ]
(f : γ m α) (g : γ α m β)
(hmono₁ : monotone f)
(hmono₂ : monotone g) :
monotone (fun (x : γ) => f x >>= g x) := by
intro x₁ x₂ hx₁₂
apply PartialOrder.rel_trans
· apply MonoBind.bind_mono_left (hmono₁ _ _ hx₁₂)
· apply MonoBind.bind_mono_right (fun y => monotone_apply y _ hmono₂ _ _ hx₁₂)
instance : PartialOrder (Option α) := inferInstanceAs (PartialOrder (FlatOrder none))
noncomputable instance : CCPO (Option α) := inferInstanceAs (CCPO (FlatOrder none))
noncomputable instance : MonoBind Option where
bind_mono_left h := by
cases h
· exact FlatOrder.rel.bot
· exact FlatOrder.rel.refl
bind_mono_right h := by
cases Option _
· exact FlatOrder.rel.refl
· exact h _
theorem admissible_eq_some (P : Prop) (y : α) :
admissible (fun (x : Option α) => x = some y P) := by
apply admissible_flatOrder; simp
instance [Monad m] [inst : α, PartialOrder (m α)] : PartialOrder (ExceptT ε m α) := inst _
instance [Monad m] [ α, PartialOrder (m α)] [inst : α, CCPO (m α)] : CCPO (ExceptT ε m α) := inst _
instance [Monad m] [ α, PartialOrder (m α)] [ α, CCPO (m α)] [MonoBind m] : MonoBind (ExceptT ε m) where
bind_mono_left h₁₂ := by
apply MonoBind.bind_mono_left (m := m)
exact h₁₂
bind_mono_right h₁₂ := by
apply MonoBind.bind_mono_right (m := m)
intro x
cases x
· apply PartialOrder.rel_refl
· apply h₁₂
end mono_bind
namespace Example
def findF (P : Nat Bool) (rec : Nat Option Nat) (x : Nat) : Option Nat :=
if P x then
some x
else
rec (x + 1)
noncomputable def find (P : Nat Bool) : Nat Option Nat := fix (findF P) <| by
unfold findF
apply monotone_of_monotone_apply
intro n
split
· apply monotone_const
· apply monotone_apply
apply monotone_id
theorem find_eq : find P = findF P (find P) := fix_eq ..
theorem find_spec : n m, find P n = some m n m P m := by
unfold find
refine fix_induct (motive := fun (f : Nat Option Nat) => n m, f n = some m n m P m) _ ?hadm ?hstep
case hadm =>
-- apply admissible_pi_apply does not work well, hard to infer everything
exact admissible_pi_apply _ (fun n => admissible_pi _ (fun m => admissible_eq_some _ m))
case hstep =>
intro f ih n m heq
simp only [findF] at heq
split at heq
· simp_all
· obtain ih1, ih2 := ih _ _ heq
constructor
· exact Nat.le_trans (Nat.le_add_right _ _ ) ih1
· exact ih2
end Example
end Lean.Order

View File

@@ -1,20 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner
-/
prelude
import Init.Notation
namespace Lean.Order
/--
`monotonicity` performs one compositional step solving `monotone` goals,
using lemma tagged with `@[partial_fixpoint_monotone]`.
This tactic is mostly used internally by lean in `partial_fixpoint` definitions, but
can be useful on its own for debugging or when proving new `@[partial_fixpoint_monotone]` lemmas.
-/
scoped syntax (name := monotonicity) "monotonicity" : tactic
end Lean.Order

View File

@@ -4170,16 +4170,6 @@ def withRef [Monad m] [MonadRef m] {α} (ref : Syntax) (x : m α) : m α :=
let ref := replaceRef ref oldRef
MonadRef.withRef ref x
/--
If `ref? = some ref`, run `x : m α` with a modified value for the `ref` by calling `withRef`.
Otherwise, run `x` directly.
-/
@[always_inline, inline]
def withRef? [Monad m] [MonadRef m] {α} (ref? : Option Syntax) (x : m α) : m α :=
match ref? with
| some ref => withRef ref x
| _ => x
/-- A monad that supports syntax quotations. Syntax quotations (in term
position) are monadic values that when executed retrieve the current "macro
scope" from the monad and apply it to every identifier they introduce

View File

@@ -818,7 +818,7 @@ syntax inductionAlt := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> synth
After `with`, there is an optional tactic that runs on all branches, and
then a list of alternatives.
-/
syntax inductionAlts := " with" (ppSpace colGt tactic)? withPosition((colGe inductionAlt)*)
syntax inductionAlts := " with" (ppSpace colGt tactic)? withPosition((colGe inductionAlt)+)
/--
Assuming `x` is a variable in the local context with an inductive type,

View File

@@ -18,7 +18,6 @@ inductive ExternEntry where
| inline (backend : Name) (pattern : String)
| standard (backend : Name) (fn : String)
| foreign (backend : Name) (fn : String)
deriving BEq, Hashable
/--
- `@[extern]`
@@ -37,7 +36,7 @@ inductive ExternEntry where
structure ExternAttrData where
arity? : Option Nat := none
entries : List ExternEntry
deriving Inhabited, BEq, Hashable
deriving Inhabited
-- def externEntry := leading_parser optional ident >> optional (nonReservedSymbol "inline ") >> strLit
-- @[builtin_attr_parser] def extern := leading_parser nonReservedSymbol "extern " >> optional numLit >> many externEntry

View File

@@ -7,7 +7,6 @@ prelude
import Init.Data.List.BasicAux
import Lean.Expr
import Lean.Meta.Instances
import Lean.Compiler.ExternAttr
import Lean.Compiler.InlineAttrs
import Lean.Compiler.Specialize
import Lean.Compiler.LCNF.Types
@@ -430,80 +429,6 @@ where
| .cases c => c.alts.forM fun alt => go alt.getCode
| .unreach .. | .return .. | .jmp .. => return ()
partial def Code.instantiateValueLevelParams (code : Code) (levelParams : List Name) (us : List Level) : Code :=
instCode code
where
instLevel (u : Level) :=
u.instantiateParams levelParams us
instExpr (e : Expr) :=
e.instantiateLevelParamsNoCache levelParams us
instParams (ps : Array Param) :=
ps.mapMono fun p => p.updateCore (instExpr p.type)
instAlt (alt : Alt) :=
match alt with
| .default k => alt.updateCode (instCode k)
| .alt _ ps k => alt.updateAlt! (instParams ps) (instCode k)
instArg (arg : Arg) : Arg :=
match arg with
| .type e => arg.updateType! (instExpr e)
| .fvar .. | .erased => arg
instLetValue (e : LetValue) : LetValue :=
match e with
| .const declName vs args => e.updateConst! declName (vs.mapMono instLevel) (args.mapMono instArg)
| .fvar fvarId args => e.updateFVar! fvarId (args.mapMono instArg)
| .proj .. | .value .. | .erased => e
instLetDecl (decl : LetDecl) :=
decl.updateCore (instExpr decl.type) (instLetValue decl.value)
instFunDecl (decl : FunDecl) :=
decl.updateCore (instExpr decl.type) (instParams decl.params) (instCode decl.value)
instCode (code : Code) :=
match code with
| .let decl k => code.updateLet! (instLetDecl decl) (instCode k)
| .jp decl k | .fun decl k => code.updateFun! (instFunDecl decl) (instCode k)
| .cases c => code.updateCases! (instExpr c.resultType) c.discr (c.alts.mapMono instAlt)
| .jmp fvarId args => code.updateJmp! fvarId (args.mapMono instArg)
| .return .. => code
| .unreach type => code.updateUnreach! (instExpr type)
inductive DeclValue where
| code (code : Code)
| extern (externAttrData : ExternAttrData)
deriving Inhabited, BEq
partial def DeclValue.size : DeclValue Nat
| .code c => c.size
| .extern .. => 0
def DeclValue.mapCode (f : Code Code) : DeclValue DeclValue :=
fun
| .code c => .code (f c)
| .extern e => .extern e
def DeclValue.mapCodeM [Monad m] (f : Code m Code) : DeclValue m DeclValue :=
fun v => do
match v with
| .code c => return .code ( f c)
| .extern .. => return v
def DeclValue.forCodeM [Monad m] (f : Code m Unit) : DeclValue m Unit :=
fun v => do
match v with
| .code c => f c
| .extern .. => return ()
def DeclValue.isCodeAndM [Monad m] (v : DeclValue) (f : Code m Bool) : m Bool :=
match v with
| .code c => f c
| .extern .. => pure false
/--
Declaration being processed by the Lean to Lean compiler passes.
-/
@@ -530,7 +455,7 @@ structure Decl where
The body of the declaration, usually changes as it progresses
through compiler passes.
-/
value : DeclValue
value : Code
/--
We set this flag to true during LCNF conversion. When we receive
a block of functions to be compiled, we set this flag to `true`
@@ -611,9 +536,7 @@ We use this function to decide whether we should inline a declaration tagged wit
`[inline_if_reduce]` or not.
-/
def Decl.isCasesOnParam? (decl : Decl) : Option Nat :=
match decl.value with
| .code c => go c
| .extern .. => none
go decl.value
where
go (code : Code) : Option Nat :=
match code with
@@ -627,6 +550,49 @@ def Decl.instantiateTypeLevelParams (decl : Decl) (us : List Level) : Expr :=
def Decl.instantiateParamsLevelParams (decl : Decl) (us : List Level) : Array Param :=
decl.params.mapMono fun param => param.updateCore (param.type.instantiateLevelParamsNoCache decl.levelParams us)
partial def Decl.instantiateValueLevelParams (decl : Decl) (us : List Level) : Code :=
instCode decl.value
where
instLevel (u : Level) :=
u.instantiateParams decl.levelParams us
instExpr (e : Expr) :=
e.instantiateLevelParamsNoCache decl.levelParams us
instParams (ps : Array Param) :=
ps.mapMono fun p => p.updateCore (instExpr p.type)
instAlt (alt : Alt) :=
match alt with
| .default k => alt.updateCode (instCode k)
| .alt _ ps k => alt.updateAlt! (instParams ps) (instCode k)
instArg (arg : Arg) : Arg :=
match arg with
| .type e => arg.updateType! (instExpr e)
| .fvar .. | .erased => arg
instLetValue (e : LetValue) : LetValue :=
match e with
| .const declName vs args => e.updateConst! declName (vs.mapMono instLevel) (args.mapMono instArg)
| .fvar fvarId args => e.updateFVar! fvarId (args.mapMono instArg)
| .proj .. | .value .. | .erased => e
instLetDecl (decl : LetDecl) :=
decl.updateCore (instExpr decl.type) (instLetValue decl.value)
instFunDecl (decl : FunDecl) :=
decl.updateCore (instExpr decl.type) (instParams decl.params) (instCode decl.value)
instCode (code : Code) :=
match code with
| .let decl k => code.updateLet! (instLetDecl decl) (instCode k)
| .jp decl k | .fun decl k => code.updateFun! (instFunDecl decl) (instCode k)
| .cases c => code.updateCases! (instExpr c.resultType) c.discr (c.alts.mapMono instAlt)
| .jmp fvarId args => code.updateJmp! fvarId (args.mapMono instArg)
| .return .. => code
| .unreach type => code.updateUnreach! (instExpr type)
/--
Return `true` if the arrow type contains an instance implicit argument.
-/
@@ -727,7 +693,7 @@ where
visit k
go : StateM NameSet Unit :=
decls.forM (·.value.forCodeM visit)
decls.forM fun decl => visit decl.value
def instantiateRangeArgs (e : Expr) (beginIdx endIdx : Nat) (args : Array Arg) : Expr :=
if !e.hasLooseBVars then

View File

@@ -123,10 +123,7 @@ def FunDeclCore.etaExpand (decl : FunDecl) : CompilerM FunDecl := do
decl.update decl.type params value
def Decl.etaExpand (decl : Decl) : CompilerM Decl := do
match decl.value with
| .code code =>
let some (params, newCode) etaExpandCore? decl.type decl.params code | return decl
return { decl with params, value := .code newCode}
| .extern .. => return decl
let some (params, value) etaExpandCore? decl.type decl.params decl.value | return decl
return { decl with params, value }
end Lean.Compiler.LCNF

View File

@@ -102,7 +102,7 @@ end CSE
Common sub-expression elimination
-/
def Decl.cse (decl : Decl) : CompilerM Decl := do
let value decl.value.mapCodeM (·.cse)
let value decl.value.cse
return { decl with value }
def cse (phase : Phase := .base) (occurrence := 0) : Pass :=

View File

@@ -261,7 +261,7 @@ def run (x : CheckM α) : CompilerM α :=
end Check
def Decl.check (decl : Decl) : CompilerM Unit := do
Check.run do decl.value.forCodeM (Check.checkFunDeclCore decl.name decl.params decl.type)
Check.run do Check.checkFunDeclCore decl.name decl.params decl.type decl.value
/--
Check whether every local declaration in the local context is used in one of given `decls`.
@@ -299,7 +299,7 @@ where
visitDecl (decl : Decl) : StateM FVarIdHashSet Unit := do
visitParams decl.params
decl.value.forCodeM visitCode
visitCode decl.value
visitDecls (decls : Array Decl) : StateM FVarIdHashSet Unit :=
decls.forM visitDecl

View File

@@ -148,7 +148,7 @@ def eraseCodeDecls (decls : Array CodeDecl) : CompilerM Unit := do
def eraseDecl (decl : Decl) : CompilerM Unit := do
eraseParams decl.params
decl.value.forCodeM eraseCode
eraseCode decl.value
abbrev Decl.erase (decl : Decl) : CompilerM Unit :=
eraseDecl decl

View File

@@ -38,7 +38,6 @@ end
instance : Hashable Code where
hash c := hashCode c
deriving instance Hashable for DeclValue
deriving instance Hashable for Decl
end Lean.Compiler.LCNF
end Lean.Compiler.LCNF

View File

@@ -95,6 +95,6 @@ def Code.elimDead (code : Code) : CompilerM Code :=
ElimDead.elimDead code |>.run' {}
def Decl.elimDead (decl : Decl) : CompilerM Decl := do
return { decl with value := ( decl.value.mapCodeM Code.elimDead) }
return { decl with value := ( decl.value.elimDead) }
end Lean.Compiler.LCNF

View File

@@ -513,7 +513,7 @@ def inferStep : InterpM Bool := do
let currentVal getFunVal idx
withReader (fun ctx => { ctx with currFnIdx := idx }) do
decl.params.forM fun p => updateVarAssignment p.fvarId .top
decl.value.forCodeM interpCode
interpCode decl.value
let newVal getFunVal idx
if currentVal != newVal then
return true
@@ -538,7 +538,7 @@ Use the information produced by the abstract interpreter to:
-/
partial def elimDead (assignment : Assignment) (decl : Decl) : CompilerM Decl := do
trace[Compiler.elimDeadBranches] s!"Eliminating {decl.name} with {repr (← assignment.toArray |>.mapM (fun (name, val) => do return (toString (← getBinderName name), val)))}"
return { decl with value := ( decl.value.mapCodeM go) }
return { decl with value := ( go decl.value) }
where
go (code : Code) : CompilerM Code := do
match code with

View File

@@ -141,9 +141,8 @@ partial def evalApp (declName : Name) (args : Array Arg) : FixParamM Unit := do
let key := (declName, values)
unless ( get).visited.contains key do
modify fun s => { s with visited := s.visited.insert key }
decl.value.forCodeM fun c =>
let assignment := mkAssignment decl values
withReader (fun ctx => { ctx with assignment }) <| evalCode c
let assignment := mkAssignment decl values
withReader (fun ctx => { ctx with assignment }) <| evalCode decl.value
end
@@ -170,12 +169,8 @@ def mkFixedParamsMap (decls : Array Decl) : NameMap (Array Bool) := Id.run do
let values := mkInitialValues decl.params.size
let assignment := mkAssignment decl values
let fixed := Array.mkArray decl.params.size true
match decl.value with
| .code c =>
match evalCode c |>.run { main := decl, decls, assignment } |>.run { fixed } with
| .ok _ s | .error _ s => result := result.insert decl.name s.fixed
| .extern .. =>
result := result.insert decl.name fixed
match evalCode decl.value |>.run { main := decl, decls, assignment } |>.run { fixed } with
| .ok _ s | .error _ s => result := result.insert decl.name s.fixed
return result
end Lean.Compiler.LCNF

View File

@@ -239,7 +239,7 @@ Iterate through `decl`, pushing local declarations that are only used in one
control flow arm into said arm in order to avoid useless computations.
-/
partial def floatLetIn (decl : Decl) : CompilerM Decl := do
let newValue decl.value.mapCodeM go |>.run {}
let newValue go decl.value |>.run {}
return { decl with value := newValue }
where
/--

View File

@@ -108,7 +108,7 @@ where
go (decl : Decl) : InternalizeM Decl := do
let type normExpr decl.type
let params decl.params.mapM internalizeParam
let value decl.value.mapCodeM internalizeCode
let value internalizeCode decl.value
return { decl with type, params, value }
/--

View File

@@ -133,7 +133,7 @@ this. This is because otherwise the calls to `myjp` in `f` and `g` would
produce out of scope join point jumps.
-/
partial def find (decl : Decl) : CompilerM FindState := do
let (_, candidates) decl.value.forCodeM go |>.run none |>.run {} |>.run' {}
let (_, candidates) go decl.value |>.run none |>.run {} |>.run' {}
return candidates
where
go : Code FindM Unit
@@ -178,7 +178,7 @@ and all calls to them with `jmp`s.
partial def replace (decl : Decl) (state : FindState) : CompilerM Decl := do
let mapper := fun acc cname _ => do return acc.insert cname ( mkFreshJpName)
let replaceCtx : ReplaceCtx state.candidates.foldM (init := .empty) mapper
let newValue decl.value.mapCodeM go |>.run replaceCtx
let newValue go decl.value |>.run replaceCtx
return { decl with value := newValue }
where
go (code : Code) : ReplaceM Code := do
@@ -389,7 +389,7 @@ position within the code so we can pull them out as far as possible, hopefully
enabling new inlining possibilities in the next simplifier run.
-/
partial def extend (decl : Decl) : CompilerM Decl := do
let newValue decl.value.mapCodeM go |>.run {} |>.run' {} |>.run' {}
let newValue go decl.value |>.run {} |>.run' {} |>.run' {}
let decl := { decl with value := newValue }
decl.pullFunDecls
where
@@ -510,8 +510,8 @@ After we have performed all of these optimizations we can take away the
code that has as little arguments as possible in the join points.
-/
partial def reduce (decl : Decl) : CompilerM Decl := do
let (_, analysis) decl.value.forCodeM goAnalyze |>.run {} |>.run {} |>.run' {}
let newValue decl.value.mapCodeM goReduce |>.run analysis
let (_, analysis) goAnalyze decl.value |>.run {} |>.run {} |>.run' {}
let newValue goReduce decl.value |>.run analysis
return { decl with value := newValue }
where
goAnalyzeFunDecl (fn : FunDecl) : ReduceAnalysisM Unit := do

View File

@@ -108,10 +108,9 @@ def mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl := do
where
go (nameNew : Name) (safe : Bool) (inlineAttr? : Option InlineAttributeKind) : InternalizeM Decl := do
let params := ( closure.mapM internalizeParam) ++ ( decl.params.mapM internalizeParam)
let code internalizeCode decl.value
let type code.inferType
let value internalizeCode decl.value
let type value.inferType
let type mkForallParams params type
let value := .code code
let decl := { name := nameNew, levelParams := [], params, type, value, safe, inlineAttr?, recursive := false : Decl }
return decl.setLevelParams
@@ -150,7 +149,7 @@ mutual
end
def main (decl : Decl) : LiftM Decl := do
let value withParams decl.params <| decl.value.mapCodeM visitCode
let value withParams decl.params <| visitCode decl.value
return { decl with value }
end LambdaLifting

View File

@@ -139,10 +139,6 @@ mutual
| .jmp _ args => visitArgs args
end
def visitDeclValue : DeclValue Visitor
| .code c => visitCode c
| .extern .. => id
end CollectLevelParams
open Lean.CollectLevelParams
@@ -153,7 +149,7 @@ Collect universe level parameters collecting in the type, parameters, and value,
set `decl.levelParams` with the resulting value.
-/
def Decl.setLevelParams (decl : Decl) : Decl :=
let levelParams := (visitDeclValue decl.value visitParams decl.params visitType decl.type) {} |>.params.toList
let levelParams := (visitCode decl.value visitParams decl.params visitType decl.type) {} |>.params.toList
{ decl with levelParams }
end Lean.Compiler.LCNF

View File

@@ -28,10 +28,10 @@ and `[specialize]` since they can be partially applied.
-/
def shouldGenerateCode (declName : Name) : CoreM Bool := do
if ( isCompIrrelevant |>.run') then return false
let env getEnv
if isExtern env declName then return true
let some info getDeclInfo? declName | return false
unless info.hasValue (allowOpaque := true) do return false
let env getEnv
if isExtern env declName then return false
if hasMacroInlineAttribute env declName then return false
if ( Meta.isMatcher declName) then return false
if isCasesOnRecursor env declName then return false

View File

@@ -105,11 +105,6 @@ mutual
return f!"⊥ : {← ppExpr type}"
else
return ""
partial def ppDeclValue (b : DeclValue) : M Format := do
match b with
| .code c => ppCode c
| .extern .. => return "extern"
end
def run (x : M α) : CompilerM α :=
@@ -126,7 +121,7 @@ def ppLetValue (e : LetValue) : CompilerM Format :=
def ppDecl (decl : Decl) : CompilerM Format :=
PP.run do
return f!"def {decl.name}{← PP.ppParams decl.params} : {← PP.ppExpr (← PP.getFunType decl.params decl.type)} :={indentD (← PP.ppDeclValue decl.value)}"
return f!"def {decl.name}{← PP.ppParams decl.params} : {← PP.ppExpr (← PP.getFunType decl.params decl.type)} :={indentD (← PP.ppCode decl.value)}"
def ppFunDecl (decl : FunDecl) : CompilerM Format :=
PP.run do

View File

@@ -57,7 +57,7 @@ where
| .cases (cases : CasesCore Code) => cases.alts.forM (go ·.getCode)
| .jmp .. | .return .. | .unreach .. => return ()
start (decls : Array Decl) : StateRefT (Array LetValue) CompilerM Unit :=
decls.forM (·.value.forCodeM go)
decls.forM (go ·.value)
partial def getJps : Probe Decl FunDecl := fun decls => do
let (_, res) start decls |>.run #[]
@@ -72,10 +72,10 @@ where
| .jmp .. | .return .. | .unreach .. => return ()
start (decls : Array Decl) : StateRefT (Array FunDecl) CompilerM Unit :=
decls.forM (·.value.forCodeM go)
decls.forM fun decl => go decl.value
partial def filterByLet (f : LetDecl CompilerM Bool) : Probe Decl Decl :=
filter (·.value.isCodeAndM go)
filter (fun decl => go decl.value)
where
go : Code CompilerM Bool
| .let decl k => do if ( f decl) then return true else go k
@@ -84,7 +84,7 @@ where
| .jmp .. | .return .. | .unreach .. => return false
partial def filterByFun (f : FunDecl CompilerM Bool) : Probe Decl Decl :=
filter (·.value.isCodeAndM go)
filter (fun decl => go decl.value)
where
go : Code CompilerM Bool
| .let _ k | .jp _ k => go k
@@ -93,7 +93,7 @@ where
| .jmp .. | .return .. | .unreach .. => return false
partial def filterByJp (f : FunDecl CompilerM Bool) : Probe Decl Decl :=
filter (·.value.isCodeAndM go)
filter (fun decl => go decl.value)
where
go : Code CompilerM Bool
| .let _ k => go k
@@ -103,7 +103,7 @@ where
| .jmp .. | .return .. | .unreach .. => return false
partial def filterByFunDecl (f : FunDecl CompilerM Bool) : Probe Decl Decl :=
filter (·.value.isCodeAndM go)
filter (fun decl => go decl.value)
where
go : Code CompilerM Bool
| .let _ k => go k
@@ -112,7 +112,7 @@ where
| .jmp .. | .return .. | .unreach .. => return false
partial def filterByCases (f : Cases CompilerM Bool) : Probe Decl Decl :=
filter (·.value.isCodeAndM go)
filter (fun decl => go decl.value)
where
go : Code CompilerM Bool
| .let _ k => go k
@@ -121,7 +121,7 @@ where
| .jmp .. | .return .. | .unreach .. => return false
partial def filterByJmp (f : FVarId Array Arg CompilerM Bool) : Probe Decl Decl :=
filter (·.value.isCodeAndM go)
filter (fun decl => go decl.value)
where
go : Code CompilerM Bool
| .let _ k => go k
@@ -131,7 +131,7 @@ where
| .return .. | .unreach .. => return false
partial def filterByReturn (f : FVarId CompilerM Bool) : Probe Decl Decl :=
filter (·.value.isCodeAndM go)
filter (fun decl => go decl.value)
where
go : Code CompilerM Bool
| .let _ k => go k
@@ -141,7 +141,7 @@ where
| .return var => f var
partial def filterByUnreach (f : Expr CompilerM Bool) : Probe Decl Decl :=
filter (·.value.isCodeAndM go)
filter (fun decl => go decl.value)
where
go : Code CompilerM Bool
| .let _ k => go k

View File

@@ -172,8 +172,8 @@ open PullFunDecls
Pull local function declarations and join points in the given declaration.
-/
def Decl.pullFunDecls (decl : Decl) : CompilerM Decl := do
let (value, ps) decl.value.mapCodeM pull |>.run []
let value := value.mapCode (attach ps.toArray)
let (value, ps) pull decl.value |>.run []
let value := attach ps.toArray value
return { decl with value }
def pullFunDecls : Pass :=

View File

@@ -96,8 +96,8 @@ open PullLetDecls
def Decl.pullLetDecls (decl : Decl) (isCandidateFn : LetDecl FVarIdSet CompilerM Bool) : CompilerM Decl := do
PullM.run (isCandidateFn := isCandidateFn) do
withParams decl.params do
let value decl.value.mapCodeM pullDecls
let value value.mapCodeM attachToPull
let value pullDecls decl.value
let value attachToPull value
return { decl with value }
def Decl.pullInstances (decl : Decl) : CompilerM Decl :=

View File

@@ -108,7 +108,7 @@ partial def visit (code : Code) : FindUsedM Unit := do
def collectUsedParams (decl : Decl) : CompilerM FVarIdSet := do
let params := decl.params.foldl (init := {}) fun s p => s.insert p.fvarId
let (_, { used, .. }) decl.value.forCodeM visit |>.run { decl, params } |>.run {}
let (_, { used, .. }) visit decl.value |>.run { decl, params } |>.run {}
return used
end FindUsed
@@ -146,40 +146,37 @@ end ReduceArity
open FindUsed ReduceArity Internalize
def Decl.reduceArity (decl : Decl) : CompilerM (Array Decl) := do
match decl.value with
| .code code =>
let used collectUsedParams decl
if used.size == decl.params.size then
return #[decl] -- Declarations uses all parameters
else
trace[Compiler.reduceArity] "{decl.name}, used params: {used.toList.map mkFVar}"
let mask := decl.params.map fun param => used.contains param.fvarId
let auxName := decl.name ++ `_redArg
let mkAuxDecl : CompilerM Decl := do
let params := decl.params.filter fun param => used.contains param.fvarId
let value decl.value.mapCodeM reduce |>.run { declName := decl.name, auxDeclName := auxName, paramMask := mask }
let type code.inferType
let type mkForallParams params type
let auxDecl := { decl with name := auxName, levelParams := [], type, params, value }
auxDecl.saveMono
return auxDecl
let updateDecl : InternalizeM Decl := do
let params decl.params.mapM internalizeParam
let mut args := #[]
for used in mask, param in params do
if used then
args := args.push param.toArg
let letDecl mkAuxLetDecl (.const auxName [] args)
let value := .code (.let letDecl (.return letDecl.fvarId))
let decl := { decl with params, value, inlineAttr? := some .inline, recursive := false }
decl.saveMono
return decl
let unusedParams := decl.params.filter fun param => !used.contains param.fvarId
let auxDecl mkAuxDecl
let decl updateDecl |>.run' {}
eraseParams unusedParams
return #[auxDecl, decl]
| .extern .. => return #[decl]
let used collectUsedParams decl
if used.size == decl.params.size then
return #[decl] -- Declarations uses all parameters
else
trace[Compiler.reduceArity] "{decl.name}, used params: {used.toList.map mkFVar}"
let mask := decl.params.map fun param => used.contains param.fvarId
let auxName := decl.name ++ `_redArg
let mkAuxDecl : CompilerM Decl := do
let params := decl.params.filter fun param => used.contains param.fvarId
let value reduce decl.value |>.run { declName := decl.name, auxDeclName := auxName, paramMask := mask }
let type value.inferType
let type mkForallParams params type
let auxDecl := { decl with name := auxName, levelParams := [], type, params, value }
auxDecl.saveMono
return auxDecl
let updateDecl : InternalizeM Decl := do
let params decl.params.mapM internalizeParam
let mut args := #[]
for used in mask, param in params do
if used then
args := args.push param.toArg
let letDecl mkAuxLetDecl (.const auxName [] args)
let value := .let letDecl (.return letDecl.fvarId)
let decl := { decl with params, value, inlineAttr? := some .inline, recursive := false }
decl.saveMono
return decl
let unusedParams := decl.params.filter fun param => !used.contains param.fvarId
let auxDecl mkAuxDecl
let decl updateDecl |>.run' {}
eraseParams unusedParams
return #[auxDecl, decl]
def reduceArity : Pass where
phase := .mono
@@ -190,4 +187,4 @@ def reduceArity : Pass where
builtin_initialize
registerTraceClass `Compiler.reduceArity (inherited := true)
end Lean.Compiler.LCNF
end Lean.Compiler.LCNF

View File

@@ -68,7 +68,7 @@ open ReduceJpArity
Try to reduce arity of join points
-/
def Decl.reduceJpArity (decl : Decl) : CompilerM Decl := do
let value decl.value.mapCodeM reduce |>.run {}
let value reduce decl.value |>.run {}
return { decl with value }
def reduceJpArity (phase := Phase.base) : Pass :=

View File

@@ -55,7 +55,7 @@ def Decl.applyRenaming (decl : Decl) (r : Renaming) : CompilerM Decl := do
return decl
else
let params decl.params.mapMonoM (·.applyRenaming r)
let value decl.value.mapCodeM (·.applyRenaming r)
let value decl.value.applyRenaming r
return { decl with params, value }
end Lean.Compiler.LCNF
end Lean.Compiler.LCNF

View File

@@ -22,20 +22,19 @@ namespace Lean.Compiler.LCNF
open Simp
def Decl.simp? (decl : Decl) : SimpM (Option Decl) := do
let .code code := decl.value | return none
updateFunDeclInfo code
updateFunDeclInfo decl.value
traceM `Compiler.simp.inline.info do return m!"{decl.name}:{Format.nest 2 (← (← get).funDeclInfoMap.format)}"
traceM `Compiler.simp.step do ppDecl decl
let code simp code
let value simp decl.value
let s get
let code code.applyRenaming s.binderRenaming
traceM `Compiler.simp.step.new do return m!"{decl.name} :=\n{← ppCode code}"
trace[Compiler.simp.stat] "{decl.name}, size: {code.size}, # visited: {s.visited}, # inline: {s.inline}, # inline local: {s.inlineLocal}"
if let some code simpJpCases? code then
let decl := { decl with value := .code code }
let value value.applyRenaming s.binderRenaming
traceM `Compiler.simp.step.new do return m!"{decl.name} :=\n{← ppCode value}"
trace[Compiler.simp.stat] "{decl.name}, size: {value.size}, # visited: {s.visited}, # inline: {s.inline}, # inline local: {s.inlineLocal}"
if let some value simpJpCases? value then
let decl := { decl with value }
decl.reduceJpArity
else if ( get).simplified then
return some { decl with value := .code code }
return some { decl with value }
else
return none

View File

@@ -43,7 +43,6 @@ def inlineCandidate? (e : LetValue) : SimpM (Option InlineCandidateInfo) := do
unless ( read).config.inlineDefs do
return none
let some decl getDecl? declName | return none
let .code code := decl.value | return none
let shouldInline : SimpM Bool := do
if !decl.inlineIfReduceAttr && decl.recursive then return false
if mustInline then return true
@@ -64,8 +63,9 @@ def inlineCandidate? (e : LetValue) : SimpM (Option InlineCandidateInfo) := do
if decl.alwaysInlineAttr then return true
-- TODO: check inlining quota
if decl.inlineAttr || decl.inlineIfReduceAttr then return true
if decl.noinlineAttr then return false
isSmall code
unless decl.noinlineAttr do
if ( isSmall decl.value) then return true
return false
unless ( shouldInline) do return none
/- check arity -/
let arity := decl.getArity
@@ -77,7 +77,7 @@ def inlineCandidate? (e : LetValue) : SimpM (Option InlineCandidateInfo) := do
let arg := args[paramIdx]!
unless ( arg.isConstructorApp) do return none
let params := decl.instantiateParamsLevelParams us
let value := code.instantiateValueLevelParams decl.levelParams us
let value := decl.instantiateValueLevelParams us
let type := decl.instantiateTypeLevelParams us
incInline
return some {

View File

@@ -69,14 +69,11 @@ where
visit fvarId projs
else
let some decl getDecl? declName | failure
match decl.value with
| .code code =>
guard (decl.getArity == args.size)
let params := decl.instantiateParamsLevelParams us
let code := code.instantiateValueLevelParams decl.levelParams us
let code betaReduce params code args (mustInline := true)
visitCode code projs
| .extern .. => failure
guard (decl.getArity == args.size)
let params := decl.instantiateParamsLevelParams us
let code := decl.instantiateValueLevelParams us
let code betaReduce params code args (mustInline := true)
visitCode code projs
visitCode (code : Code) (projs : List Nat) : OptionT (StateRefT (Array CodeDecl) SimpM) FVarId := do
match code with

View File

@@ -222,7 +222,6 @@ def mkSpecDecl (decl : Decl) (us : List Level) (argMask : Array (Option Arg)) (p
eraseDecl decl
where
go (decl : Decl) (nameNew : Name) : InternalizeM Decl := do
let .code code := decl.value | panic! "can only specialize decls with code"
let mut params params.mapM internalizeParam
let decls decls.mapM internalizeCodeDecl
for param in decl.params, arg in argMask do
@@ -236,12 +235,11 @@ where
for param in decl.params[argMask.size:] do
let param := { param with type := param.type.instantiateLevelParamsNoCache decl.levelParams us }
params := params.push ( internalizeParam param)
let code := code.instantiateValueLevelParams decl.levelParams us
let code internalizeCode code
let code := attachCodeDecls decls code
let type code.inferType
let value := decl.instantiateValueLevelParams us
let value internalizeCode value
let value := attachCodeDecls decls value
let type value.inferType
let type mkForallParams params type
let value := .code code
let safe := decl.safe
let recursive := decl.recursive
let decl := { name := nameNew, levelParams := levelParamsNew, params, type, value, safe, recursive, inlineAttr? := none : Decl }
@@ -270,7 +268,6 @@ mutual
let some paramsInfo getSpecParamInfo? declName | return none
unless ( shouldSpecialize paramsInfo args) do return none
let some decl getDecl? declName | return none
let .code _ := decl.value | return none
trace[Compiler.specialize.candidate] "{e.toExpr}, {paramsInfo}"
let (argMask, params, decls) Collector.collect paramsInfo args
let keyBody := .const declName us (argMask.filterMap id)
@@ -293,7 +290,7 @@ mutual
let specDecl specDecl.simp {}
let specDecl specDecl.simp { etaPoly := true, inlinePartial := true, implementedBy := true }
let value withReader (fun _ => { declName := specDecl.name }) do
withParams specDecl.params <| specDecl.value.mapCodeM visitCode
withParams specDecl.params <| visitCode specDecl.value
let specDecl := { specDecl with value }
modify fun s => { s with decls := s.decls.push specDecl }
return some (.const specDecl.name usNew argsNew)
@@ -328,7 +325,7 @@ def main (decl : Decl) : SpecializeM Decl := do
if ( decl.isTemplateLike) then
return decl
else
let value withParams decl.params <| decl.value.mapCodeM visitCode
let value withParams decl.params <| visitCode decl.value
return { decl with value }
end Specialize

View File

@@ -235,17 +235,12 @@ Assert that the pass under test produces `Decl`s that do not contain
`Expr.const constName` in their `Code.let` values anymore.
-/
def assertDoesNotContainConstAfter (constName : Name) (msg : String) : TestInstaller :=
assertForEachDeclAfterEachOccurrence
fun _ decl =>
match decl.value with
| .code c => !c.containsConst constName
| .extern .. => true
msg
assertForEachDeclAfterEachOccurrence (fun _ decl => !decl.value.containsConst constName) msg
def assertNoFun : TestInstaller :=
assertAfter do
for decl in ( getDecls) do
decl.value.forCodeM fun
decl.value.forM fun
| .fun .. => throwError "declaration `{decl.name}` contains a local function declaration"
| _ => return ()

View File

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
prelude
import Lean.Meta.Transform
import Lean.Meta.Match.MatcherInfo
import Lean.Compiler.ExternAttr
import Lean.Compiler.ImplementedByAttr
import Lean.Compiler.LCNF.ToLCNF
@@ -97,48 +96,31 @@ The steps for this are roughly:
def toDecl (declName : Name) : CompilerM Decl := do
let declName := if let some name := isUnsafeRecName? declName then name else declName
let some info getDeclInfo? declName | throwError "declaration `{declName}` not found"
let some value := info.value? (allowOpaque := true) | throwError "declaration `{declName}` does not have a value"
let (type, value) Meta.MetaM.run' do
let type toLCNFType info.type
let value Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs ( Meta.etaExpand body)
let value replaceUnsafeRecNames value
let value macroInline value
/- Recall that some declarations tagged with `macro_inline` contain matchers. -/
let value inlineMatchers value
/- Recall that `inlineMatchers` may have exposed `ite`s and `dite`s which are tagged as `[macro_inline]`. -/
let value macroInline value
/-
Remark: we have disabled the following transformatbion, we will perform it at phase 2, after code specialization.
It prevents many optimizations (e.g., "cases-of-ctor").
-/
-- let value ← applyCasesOnImplementedBy value
return (type, value)
let value toLCNF value
let safe := !info.isPartial && !info.isUnsafe
let inlineAttr? := getInlineAttribute? ( getEnv) declName
if let some externAttrData := getExternAttrData? ( getEnv) declName then
let paramsFromTypeBinders (expr : Expr) : CompilerM (Array Param) := do
let mut params := #[]
let mut currentExpr := expr
repeat
match currentExpr with
| .forallE binderName type body _ =>
let borrow := isMarkedBorrowed type
params := params.push ( mkParam binderName type borrow)
currentExpr := body
| _ => break
return params
let type Meta.MetaM.run' (toLCNFType info.type)
let params paramsFromTypeBinders type
return { name := declName, params, type, value := .extern externAttrData, levelParams := info.levelParams, safe, inlineAttr? }
let decl if let .fun decl (.return _) := value then
eraseFunDecl decl (recursive := false)
pure { name := declName, params := decl.params, type, value := decl.value, levelParams := info.levelParams, safe, inlineAttr? : Decl }
else
let some value := info.value? (allowOpaque := true) | throwError "declaration `{declName}` does not have a value"
let (type, value) Meta.MetaM.run' do
let type toLCNFType info.type
let value Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs ( Meta.etaExpand body)
let value replaceUnsafeRecNames value
let value macroInline value
/- Recall that some declarations tagged with `macro_inline` contain matchers. -/
let value inlineMatchers value
/- Recall that `inlineMatchers` may have exposed `ite`s and `dite`s which are tagged as `[macro_inline]`. -/
let value macroInline value
/-
Remark: we have disabled the following transformatbion, we will perform it at phase 2, after code specialization.
It prevents many optimizations (e.g., "cases-of-ctor").
-/
-- let value ← applyCasesOnImplementedBy value
return (type, value)
let code toLCNF value
let decl if let .fun decl (.return _) := code then
eraseFunDecl decl (recursive := false)
pure { name := declName, params := decl.params, type, value := .code decl.value, levelParams := info.levelParams, safe, inlineAttr? : Decl }
else
pure { name := declName, params := #[], type, value := .code code, levelParams := info.levelParams, safe, inlineAttr? }
/- `toLCNF` may eta-reduce simple declarations. -/
decl.etaExpand
pure { name := declName, params := #[], type, value, levelParams := info.levelParams, safe, inlineAttr? }
/- `toLCNF` may eta-reduce simple declarations. -/
decl.etaExpand
end Lean.Compiler.LCNF

View File

@@ -110,4 +110,7 @@ def Code.toExpr (code : Code) (xs : Array FVarId := #[]) : Expr :=
def FunDeclCore.toExpr (decl : FunDecl) (xs : Array FVarId := #[]) : Expr :=
run' decl.toExprM xs
def Decl.toExpr (decl : Decl) : Expr :=
run do withParams decl.params do mkLambdaM decl.params ( decl.value.toExprM)
end Lean.Compiler.LCNF

View File

@@ -143,7 +143,7 @@ where
go : ToMonoM Decl := do
let type toMonoType decl.type
let params decl.params.mapM (·.toMono)
let value decl.value.mapCodeM (·.toMono)
let value decl.value.toMono
let decl := { decl with type, params, value, levelParams := [] }
decl.saveMono
return decl

View File

@@ -11,22 +11,6 @@ import Init.Data.List.Impl
namespace Lean
namespace Json
set_option maxRecDepth 1024 in
/--
This table contains for each UTF-8 byte whether we need to escape a string that contains it.
-/
private def escapeTable : { xs : ByteArray // xs.size = 256 } :=
ByteArray.mk #[
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,1, 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1
], by rfl
private def escapeAux (acc : String) (c : Char) : String :=
-- escape ", \, \n and \r, keep all other characters ≥ 0x20 and render characters < 0x20 with \u
if c = '"' then -- hack to prevent emacs from regarding the rest of the file as a string: "
@@ -55,27 +39,8 @@ private def escapeAux (acc : String) (c : Char) : String :=
let d4 := Nat.digitChar (n % 16)
acc ++ "\\u" |>.push d1 |>.push d2 |>.push d3 |>.push d4
private def needEscape (s : String) : Bool :=
go s 0
where
go (s : String) (i : Nat) : Bool :=
if h : i < s.utf8ByteSize then
let byte := s.getUtf8Byte i h
have h1 : byte.toNat < 256 := UInt8.toNat_lt_size byte
have h2 : escapeTable.val.size = 256 := escapeTable.property
if escapeTable.val.get byte.toNat (Nat.lt_of_lt_of_eq h1 h2.symm) == 0 then
go s (i + 1)
else
true
else
false
def escape (s : String) (acc : String := "") : String :=
-- If we don't have any characters that need to be escaped we can just append right away.
if needEscape s then
s.foldl escapeAux acc
else
acc ++ s
s.foldl escapeAux acc
def renderString (s : String) (acc : String := "") : String :=
let acc := acc ++ "\""

View File

@@ -6,7 +6,6 @@ Authors: Marc Huisinga, Wojciech Nawrocki
-/
prelude
import Lean.Data.Lsp.Basic
import Lean.Data.Lsp.CancelParams
import Lean.Data.Lsp.Capabilities
import Lean.Data.Lsp.Client
import Lean.Data.Lsp.Communication

View File

@@ -6,6 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki
-/
prelude
import Lean.Data.Json
import Lean.Data.JsonRpc
/-! Defines most of the 'Basic Structures' in the LSP specification
(https://microsoft.github.io/language-server-protocol/specifications/specification-current/),
@@ -18,6 +19,10 @@ namespace Lsp
open Json
structure CancelParams where
id : JsonRpc.RequestID
deriving Inhabited, BEq, ToJson, FromJson
abbrev DocumentUri := String
/-- We adopt the convention that zero-based UTF-16 positions as sent by LSP clients

View File

@@ -1,25 +0,0 @@
/-
Copyright (c) 2020 Marc Huisinga. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Marc Huisinga, Wojciech Nawrocki
-/
prelude
import Lean.Data.JsonRpc
/-! # Defines `Lean.Lsp.CancelParams`.
This is separate from `Lean.Data.Lsp.Basic` to reduce transitive dependencies.
-/
namespace Lean
namespace Lsp
open Json
structure CancelParams where
id : JsonRpc.RequestID
deriving Inhabited, BEq, ToJson, FromJson
end Lsp
end Lean

View File

@@ -6,6 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki
-/
prelude
import Init.Data.String
import Init.Data.Array
import Lean.Data.Lsp.Basic
import Lean.Data.Position
import Lean.DeclarationRange

View File

@@ -49,8 +49,3 @@ variable {_ : BEq α} {_ : Hashable α}
@[inline] def fold {β : Type v} (f : β α β) (init : β) (s : PersistentHashSet α) : β :=
Id.run $ s.foldM f init
def toList (s : PersistentHashSet α) : List α :=
s.set.toList.map (·.1)
end PersistentHashSet

View File

@@ -131,18 +131,14 @@ def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) :
if isDefEqGuarded r er then
let mut failed := false
unless isDefEqGuarded lhs elhs do
let (lhs, elhs) addPPExplicitToExposeDiff lhs elhs
let (lhsTy, elhsTy) addPPExplicitToExposeDiff ( inferType lhs) ( inferType elhs)
logErrorAt steps[0]!.term m!"\
invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {lhsTy}"}\n\
but is expected to be{indentD m!"{elhs} : {elhsTy}"}"
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
let (rhs, erhs) addPPExplicitToExposeDiff rhs erhs
let (rhsTy, erhsTy) addPPExplicitToExposeDiff ( inferType rhs) ( inferType erhs)
logErrorAt steps.back!.term m!"\
invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {rhsTy}"}\n\
but is expected to be{indentD m!"{erhs} : {erhsTy}"}"
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

View File

@@ -38,7 +38,6 @@ def elabCheckTactic : CommandElab := fun stx => do
| [next] => do
let (val, _, _) matchCheckGoalType stx (next.getType)
if !( Meta.withReducible <| isDefEq val expTerm) then
let (val, expTerm) addPPExplicitToExposeDiff val expTerm
throwErrorAt stx
m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
| _ => do

View File

@@ -16,4 +16,3 @@ import Lean.Elab.Deriving.FromToJson
import Lean.Elab.Deriving.SizeOf
import Lean.Elab.Deriving.Hashable
import Lean.Elab.Deriving.Ord
import Lean.Elab.Deriving.ToExpr

View File

@@ -1,237 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kyle Miller
-/
prelude
import Lean.Meta.Transform
import Lean.Elab.Deriving.Basic
import Lean.Elab.Deriving.Util
import Lean.ToLevel
import Lean.ToExpr
/-!
# `ToExpr` deriving handler
This module defines a `ToExpr` deriving handler for inductive types.
It supports mutually inductive types as well.
The `ToExpr` deriving handlers support universe level polymorphism, via the `Lean.ToLevel` class.
To use `ToExpr` in places where there is universe polymorphism, make sure a `[ToLevel.{u}]` instance is available,
though be aware that the `ToLevel` mechanism does not support `max` or `imax` expressions.
Implementation note: this deriving handler was initially modeled after the `Repr` deriving handler, but
1. we need to account for universe levels,
2. the `ToExpr` class has two fields rather than one, and
3. we don't handle structures specially.
-/
namespace Lean.Elab.Deriving.ToExpr
open Lean Elab Parser.Term
open Meta Command Deriving
/--
Given `args := #[e₁, e₂, …, eₙ]`, constructs the syntax `Expr.app (… (Expr.app (Expr.app f e₁) e₂) …) eₙ`.
-/
def mkAppNTerm (f : Term) (args : Array Term) : MetaM Term :=
args.foldlM (fun a b => ``(Expr.app $a $b)) f
/-- Fixes the output of `mkInductiveApp` to explicitly reference universe levels. -/
def updateIndType (indVal : InductiveVal) (t : Term) : TermElabM Term :=
let levels := indVal.levelParams.toArray.map mkIdent
match t with
| `(@$f $args*) => `(@$f.{$levels,*} $args*)
| _ => throwError "(internal error) expecting output of `mkInductiveApp`"
/--
Creates a term that evaluates to an expression representing the inductive type.
Uses `toExpr` and `toTypeExpr` for the arguments to the type constructor.
-/
def mkToTypeExpr (indVal : InductiveVal) (argNames : Array Name) : TermElabM Term := do
let levels indVal.levelParams.toArray.mapM (fun u => `(Lean.toLevel.{$(mkIdent u)}))
forallTelescopeReducing indVal.type fun xs _ => do
let mut args : Array Term := #[]
for argName in argNames, x in xs do
let a := mkIdent argName
if Meta.isType x then
args := args.push <| ``(toTypeExpr $a)
else
args := args.push <| ``(toExpr $a)
mkAppNTerm ( ``(Expr.const $(quote indVal.name) [$levels,*])) args
/--
Creates the body of the `toExpr` function for the `ToExpr` instance, which is a `match` expression
that calls `toExpr` and `toTypeExpr` to assemble an expression for a given term.
For recursive inductive types, `auxFunName` refers to the `ToExpr` instance for the current type.
For mutually recursive types, we rely on the local instances set up by `mkLocalInstanceLetDecls`.
-/
def mkToExprBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) (levelInsts : Array Term) :
TermElabM Term := do
let discrs mkDiscrs header indVal
let alts mkAlts
`(match $[$discrs],* with $alts:matchAlt*)
where
/-- Create the `match` cases, one per constructor. -/
mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do
let levels levelInsts.mapM fun inst => `($(inst).toLevel)
let mut alts := #[]
for ctorName in indVal.ctors do
let ctorInfo getConstInfoCtor ctorName
let alt forallTelescopeReducing ctorInfo.type fun xs _ => do
let mut patterns := #[]
-- add `_` pattern for indices, before the constructor's pattern
for _ in [:indVal.numIndices] do
patterns := patterns.push ( `(_))
let mut ctorArgs := #[]
let mut rhsArgs : Array Term := #[]
let mkArg (x : Expr) (a : Term) : TermElabM Term := do
if ( inferType x).isAppOf indVal.name then
`($(mkIdent auxFunName) $levelInsts* $a)
else if Meta.isType x then
``(toTypeExpr $a)
else
``(toExpr $a)
-- add `_` pattern for inductive parameters, which are inaccessible
for i in [:ctorInfo.numParams] do
let a := mkIdent header.argNames[i]!
ctorArgs := ctorArgs.push ( `(_))
rhsArgs := rhsArgs.push <| mkArg xs[i]! a
for i in [:ctorInfo.numFields] do
let a := mkIdent ( mkFreshUserName `a)
ctorArgs := ctorArgs.push a
rhsArgs := rhsArgs.push <| mkArg xs[ctorInfo.numParams + i]! a
patterns := patterns.push ( `(@$(mkIdent ctorName):ident $ctorArgs:term*))
let rhs : Term mkAppNTerm ( ``(Expr.const $(quote ctorInfo.name) [$levels,*])) rhsArgs
`(matchAltExpr| | $[$patterns:term],* => $rhs)
alts := alts.push alt
return alts
/--
For nested and mutually recursive inductive types, we define `partial` instances,
and the strategy is to have local `ToExpr` instances in scope for the body of each instance.
This way, each instance can freely use `toExpr` and `toTypeExpr` for each of the types in `ctx`.
This is a modified copy of `Lean.Elab.Deriving.mkLocalInstanceLetDecls`,
since we need to include the `toTypeExpr` field in the `letDecl`
Note that, for simplicity, each instance gets its own definition of each others' `toTypeExpr` fields.
These are very simple fields, so avoiding the duplication is not worth it.
-/
def mkLocalInstanceLetDecls (ctx : Deriving.Context) (argNames : Array Name) (levelInsts : Array Term) :
TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do
let mut letDecls := #[]
for indVal in ctx.typeInfos, auxFunName in ctx.auxFunNames do
let currArgNames mkInductArgNames indVal
let numParams := indVal.numParams
let currIndices := currArgNames[numParams:]
let binders mkImplicitBinders currIndices
let argNamesNew := argNames[:numParams] ++ currIndices
let indType mkInductiveApp indVal argNamesNew
let instName mkFreshUserName `localinst
let toTypeExpr mkToTypeExpr indVal argNames
-- Recall that mutually inductive types all use the same universe levels, hence we pass the same ToLevel instances to each aux function.
let letDecl `(Parser.Term.letDecl| $(mkIdent instName):ident $binders:implicitBinder* : ToExpr $indType :=
{ toExpr := $(mkIdent auxFunName) $levelInsts*,
toTypeExpr := $toTypeExpr })
letDecls := letDecls.push letDecl
return letDecls
open TSyntax.Compat in
/--
Makes a `toExpr` function for the given inductive type.
The implementation of each `toExpr` function for a (mutual) inductive type is given as top-level private definitions.
These are assembled into `ToExpr` instances in `mkInstanceCmds`.
For mutual/nested inductive types, then each of the types' `ToExpr` instances are provided as local instances,
to wire together the recursion (necessitating these auxiliary definitions being `partial`).
-/
def mkAuxFunction (ctx : Deriving.Context) (i : Nat) : TermElabM Command := do
let auxFunName := ctx.auxFunNames[i]!
let indVal := ctx.typeInfos[i]!
let header mkHeader ``ToExpr 1 indVal
/- We make the `ToLevel` instances be explicit here so that we can pass the instances from the instances to the
aux functions. This lets us ensure universe level variables are being lined up,
without needing to use `ident.{u₁,…,uₙ}` syntax, which could conditionally be incorrect
depending on the ambient CommandElabM scope state.
TODO(kmill): deriving handlers should run in a scope with no `universes` or `variables`. -/
let (toLevelInsts, levelBinders) := Array.unzip <| indVal.levelParams.toArray.mapM fun u => do
let inst := mkIdent ( mkFreshUserName `inst)
return (inst, `(explicitBinderF| ($inst : ToLevel.{$(mkIdent u)})))
let mut body mkToExprBody header indVal auxFunName toLevelInsts
if ctx.usePartial then
let letDecls mkLocalInstanceLetDecls ctx header.argNames toLevelInsts
body mkLet letDecls body
/- We need to alter the last binder (the one for the "target") to have explicit universe levels
so that the `ToLevel` instance arguments can use them. -/
let addLevels binder :=
match binder with
| `(bracketedBinderF| ($a : $ty)) => do `(bracketedBinderF| ($a : $( updateIndType indVal ty)))
| _ => throwError "(internal error) expecting inst binder"
let binders := header.binders.pop ++ levelBinders ++ #[ addLevels header.binders.back!]
if ctx.usePartial then
`(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Expr := $body:term)
else
`(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Expr := $body:term)
/--
Creates all the auxiliary functions (using `mkAuxFunction`) for the (mutual) inductive type(s).
Wraps the resulting definition commands in `mutual ... end`.
-/
def mkAuxFunctions (ctx : Deriving.Context) : TermElabM Syntax := do
let mut auxDefs := #[]
for i in [:ctx.typeInfos.size] do
auxDefs := auxDefs.push ( mkAuxFunction ctx i)
`(mutual $auxDefs:command* end)
open TSyntax.Compat in
/--
Assuming all of the auxiliary definitions exist,
creates all the `instance` commands for the `ToExpr` instances for the (mutual) inductive type(s).
This is a modified copy of `Lean.Elab.Deriving.mkInstanceCmds` to account for `ToLevel` instances.
-/
def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
TermElabM (Array Command) := do
let mut instances := #[]
for indVal in ctx.typeInfos, auxFunName in ctx.auxFunNames do
if typeNames.contains indVal.name then
let argNames mkInductArgNames indVal
let binders mkImplicitBinders argNames
let binders := binders ++ ( mkInstImplicitBinders ``ToExpr indVal argNames)
let (toLevelInsts, levelBinders) := Array.unzip <| indVal.levelParams.toArray.mapM fun u => do
let inst := mkIdent ( mkFreshUserName `inst)
return (inst, `(instBinderF| [$inst : ToLevel.{$(mkIdent u)}]))
let binders := binders ++ levelBinders
let indType updateIndType indVal ( mkInductiveApp indVal argNames)
let toTypeExpr mkToTypeExpr indVal argNames
let instCmd `(instance $binders:implicitBinder* : ToExpr $indType where
toExpr := $(mkIdent auxFunName) $toLevelInsts*
toTypeExpr := $toTypeExpr)
instances := instances.push instCmd
return instances
/--
Returns all the commands necessary to construct the `ToExpr` instances.
-/
def mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
let ctx mkContext "toExpr" declNames[0]!
let cmds := #[ mkAuxFunctions ctx] ++ ( mkInstanceCmds ctx declNames)
trace[Elab.Deriving.toExpr] "\n{cmds}"
return cmds
/--
The main entry point to the `ToExpr` deriving handler.
-/
def mkToExprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
if ( declNames.allM isInductive) && declNames.size > 0 then
let cmds withFreshMacroScope <| liftTermElabM <| mkToExprInstanceCmds declNames
-- Enable autoimplicits, used for universe levels.
withScope (fun scope => { scope with opts := autoImplicit.set scope.opts true }) do
elabCommand (mkNullNode cmds)
return true
else
return false
builtin_initialize
registerDerivingHandler ``Lean.ToExpr mkToExprInstanceHandler
registerTraceClass `Elab.Deriving.toExpr
end Lean.Elab.Deriving.ToExpr

View File

@@ -691,9 +691,6 @@ private def addProjections (r : ElabHeaderResult) (fieldInfos : Array StructFiel
let env getEnv
let env ofExceptKernelException (mkProjections env r.view.declName projNames.toList r.view.isClass)
setEnv env
for fieldInfo in fieldInfos do
if fieldInfo.isSubobject then
addDeclarationRangesFromSyntax fieldInfo.declName r.view.ref fieldInfo.ref
private def registerStructure (structName : Name) (infos : Array StructFieldInfo) : TermElabM Unit := do
let fields infos.filterMapM fun info => do
@@ -778,14 +775,14 @@ private def setSourceInstImplicit (type : Expr) : Expr :=
/--
Creates a projection function to a non-subobject parent.
-/
private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (source : Expr) (parent : StructParentInfo) (parentType : Expr) : MetaM StructureParentInfo := do
private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (source : Expr) (parentStructName : Name) (parentType : Expr) : MetaM StructureParentInfo := do
let isProp Meta.isProp parentType
let env getEnv
let structName := view.declName
let sourceFieldNames := getStructureFieldsFlattened env structName
let binfo := if view.isClass && isClass env parent.structName then BinderInfo.instImplicit else BinderInfo.default
let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
let mut declType instantiateMVars ( mkForallFVars params ( mkForallFVars #[source] parentType))
if view.isClass && isClass env parent.structName then
if view.isClass && isClass env parentStructName then
declType := setSourceInstImplicit declType
declType := declType.inferImplicit params.size true
let rec copyFields (parentType : Expr) : MetaM Expr := do
@@ -826,8 +823,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
-- (Instances will get instance reducibility in `Lean.Elab.Command.addParentInstances`.)
if !binfo.isInstImplicit && !( Meta.isProp parentType) then
setReducibleAttribute declName
addDeclarationRangesFromSyntax declName view.ref parent.ref
return { structName := parent.structName, subobject := false, projFn := declName }
return { structName := parentStructName, subobject := false, projFn := declName }
private def mkRemainingProjections (levelParams : List Name) (params : Array Expr) (view : StructView)
(parents : Array StructParentInfo) (fieldInfos : Array StructFieldInfo) : TermElabM (Array StructureParentInfo) := do
@@ -848,7 +844,7 @@ private def mkRemainingProjections (levelParams : List Name) (params : Array Exp
pure { structName := parent.structName, subobject := true, projFn := info.declName }
else
let parent_type := ( instantiateMVars parent.type).replace fun e => parentFVarToConst[e]?
mkCoercionToCopiedParent levelParams params view source parent parent_type)
mkCoercionToCopiedParent levelParams params view source parent.structName parent_type)
parentInfos := parentInfos.push parentInfo
if let some fvar := parent.fvar? then
parentFVarToConst := parentFVarToConst.insert fvar <|

View File

@@ -44,5 +44,3 @@ import Lean.Elab.Tactic.DiscrTreeKey
import Lean.Elab.Tactic.BVDecide
import Lean.Elab.Tactic.BoolToPropSimps
import Lean.Elab.Tactic.Classical
import Lean.Elab.Tactic.Grind
import Lean.Elab.Tactic.Monotonicity

View File

@@ -82,7 +82,7 @@ instance : ToExpr Gate where
| .and => mkConst ``Gate.and
| .xor => mkConst ``Gate.xor
| .beq => mkConst ``Gate.beq
| .or => mkConst ``Gate.or
| .imp => mkConst ``Gate.imp
toTypeExpr := mkConst ``Gate
instance : ToExpr BVPred where

View File

@@ -91,7 +91,7 @@ where
| .and => ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
| .xor => ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
| .beq => ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
| .or => ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
| .imp => ``Std.Tactic.BVDecide.Reflect.Bool.imp_congr
/--
Construct the reified version of `Bool.not subExpr`.
@@ -136,7 +136,7 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr)
lhsEvalExpr lhsProof?
rhsEvalExpr rhsProof? | return none
return mkApp9
(mkConst ``Std.Tactic.BVDecide.Reflect.Bool.cond_congr)
(mkConst ``Std.Tactic.BVDecide.Reflect.Bool.ite_congr)
discrExpr lhsExpr rhsExpr
discrEvalExpr lhsEvalExpr rhsEvalExpr
discrProof lhsProof rhsProof

View File

@@ -22,70 +22,67 @@ This function adds the two lemmas:
- `discrExpr = false → atomExpr = rhsExpr`
It assumes that `discrExpr`, `lhsExpr` and `rhsExpr` are the expressions corresponding to `discr`,
`lhs` and `rhs`. Furthermore it assumes that `atomExpr` is of the form
`bif discrExpr then lhsExpr else rhsExpr`.
`if discrExpr = true then lhsExpr else rhsExpr`.
-/
def addCondLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
def addIfLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
(discrExpr atomExpr lhsExpr rhsExpr : Expr) : LemmaM Unit := do
let some trueLemma mkCondTrueLemma discr atom lhs discrExpr atomExpr lhsExpr rhsExpr | return ()
let some trueLemma mkIfTrueLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
LemmaM.addLemma trueLemma
let some falseLemma mkCondFalseLemma discr atom rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
let some falseLemma mkIfFalseLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
LemmaM.addLemma falseLemma
where
mkCondTrueLemma (discr : ReifiedBVLogical) (atom lhs : ReifiedBVExpr)
mkIfTrueLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
(discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
mkIfLemma true discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
mkIfFalseLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
(discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
mkIfLemma false discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
mkIfLemma (discrVal : Bool) (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
(discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
let resExpr := lhsExpr
let resValExpr := lhs
let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_true
let resExpr := if discrVal then lhsExpr else rhsExpr
let resValExpr := if discrVal then lhs else rhs
let lemmaName :=
if discrVal then
``Std.Tactic.BVDecide.Reflect.BitVec.if_true
else
``Std.Tactic.BVDecide.Reflect.BitVec.if_false
let discrValExpr := toExpr discrVal
let discrVal ReifiedBVLogical.mkBoolConst discrVal
let notDiscrExpr := mkApp (mkConst ``Bool.not) discrExpr
let notDiscr ReifiedBVLogical.mkNot discr discrExpr
let eqDiscrExpr mkAppM ``BEq.beq #[discrExpr, discrValExpr]
let eqDiscr ReifiedBVLogical.mkGate discr discrVal discrExpr discrValExpr .beq
let eqBVExpr mkAppM ``BEq.beq #[atomExpr, resExpr]
let some eqBVPred ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
let eqBV ReifiedBVLogical.ofPred eqBVPred
let imp ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or
let imp ReifiedBVLogical.mkGate eqDiscr eqBV eqDiscrExpr eqBVExpr .imp
let proof := do
let evalExpr ReifiedBVLogical.mkEvalExpr imp.expr
let congrProof := ( imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr)
let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr
-- !discr || (atom == rhs)
let impExpr := mkApp2 (mkConst ``Bool.or) notDiscrExpr eqBVExpr
let trueExpr := mkConst ``Bool.true
let eqDiscrTrueExpr mkEq eqDiscrExpr trueExpr
let eqBVExprTrueExpr mkEq eqBVExpr trueExpr
let impExpr mkArrow eqDiscrTrueExpr eqBVExprTrueExpr
-- construct a `Decidable` instance for the implication using forall_prop_decidable
let decEqDiscrTrue := mkApp2 (mkConst ``instDecidableEqBool) eqDiscrExpr trueExpr
let decEqBVExprTrue := mkApp2 (mkConst ``instDecidableEqBool) eqBVExpr trueExpr
let impDecidable := mkApp4 (mkConst ``forall_prop_decidable)
eqDiscrTrueExpr
(.lam .anonymous eqDiscrTrueExpr eqBVExprTrueExpr .default)
decEqDiscrTrue
(.lam .anonymous eqDiscrTrueExpr decEqBVExprTrue .default)
let decideImpExpr := mkApp2 (mkConst ``Decidable.decide) impExpr impDecidable
return mkApp4
(mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
impExpr
evalExpr
congrProof
lemmaProof
return some imp.bvExpr, proof, imp.expr
mkCondFalseLemma (discr : ReifiedBVLogical) (atom rhs : ReifiedBVExpr)
(discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
let resExpr := rhsExpr
let resValExpr := rhs
let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_false
let eqBVExpr mkAppM ``BEq.beq #[atomExpr, resExpr]
let some eqBVPred ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
let eqBV ReifiedBVLogical.ofPred eqBVPred
let imp ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or
let proof := do
let evalExpr ReifiedBVLogical.mkEvalExpr imp.expr
let congrProof := ( imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr)
let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr rhs.width) discrExpr lhsExpr rhsExpr
-- discr || (atom == rhs)
let impExpr := mkApp2 (mkConst ``Bool.or) discrExpr eqBVExpr
return mkApp4
(mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
impExpr
decideImpExpr
evalExpr
congrProof
lemmaProof

View File

@@ -220,12 +220,15 @@ where
.rotateRight
``BVUnOp.rotateRight
``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
| cond _ discrExpr lhsExpr rhsExpr =>
| ite _ discrExpr _ lhsExpr rhsExpr =>
let_expr Eq α discrExpr val := discrExpr | return none
let_expr Bool := α | return none
let_expr Bool.true := val | return none
let some atom ReifiedBVExpr.bitVecAtom x true | return none
let some discr ReifiedBVLogical.of discrExpr | return none
let some lhs goOrAtom lhsExpr | return none
let some rhs goOrAtom rhsExpr | return none
addCondLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
addIfLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
return some atom
| _ => return none
@@ -389,7 +392,10 @@ where
| Bool => gateReflection lhsExpr rhsExpr .beq
| BitVec _ => goPred t
| _ => return none
| cond _ discrExpr lhsExpr rhsExpr =>
| ite _ discrExpr _ lhsExpr rhsExpr =>
let_expr Eq α discrExpr val := discrExpr | return none
let_expr Bool := α | return none
let_expr Bool.true := val | return none
let some discr goOrAtom discrExpr | return none
let some lhs goOrAtom lhsExpr | return none
let some rhs goOrAtom rhsExpr | return none

View File

@@ -28,18 +28,6 @@ namespace Frontend.Normalize
open Lean.Meta
open Std.Tactic.BVDecide.Normalize
builtin_simproc [bv_normalize] reduceCond (cond _ _ _) := fun e => do
let_expr f@cond α c tb eb := e | return .continue
let r Simp.simp c
if r.expr.cleanupAnnotations.isConstOf ``Bool.true then
let pr := mkApp (mkApp4 (mkConst ``Bool.cond_pos f.constLevels!) α c tb eb) ( r.getProof)
return .visit { expr := tb, proof? := pr }
else if r.expr.cleanupAnnotations.isConstOf ``Bool.false then
let pr := mkApp (mkApp4 (mkConst ``Bool.cond_neg f.constLevels!) α c tb eb) ( r.getProof)
return .visit { expr := eb, proof? := pr }
else
return .continue
builtin_simproc [bv_normalize] eqToBEq (((_ : Bool) = (_ : Bool))) := fun e => do
let_expr Eq _ lhs rhs := e | return .continue
match_expr rhs with
@@ -139,6 +127,8 @@ builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _))
else
return .continue
attribute [builtin_bv_normalize_proc] reduceIte
/-- Return a number `k` such that `2^k = n`. -/
private def Nat.log2Exact (n : Nat) : Option Nat := do
guard <| n 0

View File

@@ -362,9 +362,9 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
| `(tactic| intro $h:term $hs:term*) => evalTactic ( `(tactic| intro $h:term; intro $hs:term*))
| _ => throwUnsupportedSyntax
where
introStep (ref? : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do
introStep (ref : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do
let fvarId liftMetaTacticAux fun mvarId => do
let (fvarId, mvarId) withRef? ref? <| mvarId.intro n
let (fvarId, mvarId) mvarId.intro n
pure (fvarId, [mvarId])
if let some typeStx := typeStx? then
withMainContext do
@@ -374,9 +374,9 @@ where
unless ( isDefEqGuarded type fvarType) do
throwError "type mismatch at `intro {fvar}`{← mkHasTypeButIsExpectedMsg fvarType type}"
liftMetaTactic fun mvarId => return [ mvarId.replaceLocalDeclDefEq fvarId type]
if let some ref := ref? then
if let some stx := ref then
withMainContext do
Term.addLocalVarInfo ref (mkFVar fvarId)
Term.addLocalVarInfo stx (mkFVar fvarId)
@[builtin_tactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do
let matchAlts := stx[1]

View File

@@ -24,8 +24,11 @@ def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t :
finally
modifyEnv Meta.instanceExtension.popScope
@[builtin_tactic Lean.Parser.Tactic.classical, builtin_incremental]
def evalClassical : Tactic := fun stx =>
classical <| Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx
@[builtin_tactic Lean.Parser.Tactic.classical]
def evalClassical : Tactic := fun stx => do
match stx with
| `(tactic| classical $tacs:tacticSeq) =>
classical <| Elab.Tactic.evalTactic tacs
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic

View File

@@ -7,10 +7,9 @@ prelude
import Lean.Elab.Tactic.Simp
import Lean.Elab.Tactic.Split
import Lean.Elab.Tactic.Conv.Basic
import Lean.Elab.Tactic.SimpTrace
namespace Lean.Elab.Tactic.Conv
open Meta Tactic TryThis
open Meta
def applySimpResult (result : Simp.Result) : TacticM Unit := do
if result.proof?.isNone then
@@ -24,19 +23,6 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
let (result, _) dischargeWrapper.with fun d? => simp lhs ctx (simprocs := simprocs) (discharge? := d?)
applySimpResult result
@[builtin_tactic Lean.Parser.Tactic.Conv.simpTrace] def evalSimpTrace : Tactic := fun stx => withMainContext do
match stx with
| `(conv| simp?%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => do
let stx `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]?)
let { ctx, simprocs, dischargeWrapper, .. } mkSimpContext stx (eraseLocal := false)
let lhs getLhs
let (result, stats) dischargeWrapper.with fun d? =>
simp lhs ctx (simprocs := simprocs) (discharge? := d?)
applySimpResult result
let stx mkSimpCallStx stx stats.usedTheorems
addSuggestion tk stx (origSpan? := getRef)
| _ => throwUnsupportedSyntax
@[builtin_tactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do
applySimpResult ( Split.simpMatch ( getLhs))
@@ -44,15 +30,4 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
let { ctx, .. } mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
changeLhs ( Lean.Meta.dsimp ( getLhs) ctx).1
@[builtin_tactic Lean.Parser.Tactic.Conv.dsimpTrace] def evalDSimpTrace : Tactic := fun stx => withMainContext do
match stx with
| `(conv| dsimp?%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?) =>
let stx `(tactic| dsimp%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?)
let { ctx, .. } mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
let (result, stats) Lean.Meta.dsimp ( getLhs) ctx
changeLhs result
let stx mkSimpCallStx stx stats.usedTheorems
addSuggestion tk stx (origSpan? := getRef)
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.Conv

View File

@@ -1,69 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Grind.Tactics
import Lean.Meta.Tactic.Grind
import Lean.Elab.Command
import Lean.Elab.Tactic.Basic
import Lean.Elab.Tactic.Config
namespace Lean.Elab.Tactic
open Meta
declare_config_elab elabGrindConfig Grind.Config
open Command Term in
@[builtin_command_elab Lean.Parser.Command.grindPattern]
def elabGrindPattern : CommandElab := fun stx => do
match stx with
| `(grind_pattern $thmName:ident => $terms,*) => do
liftTermElabM do
let declName resolveGlobalConstNoOverload thmName
discard <| addTermInfo thmName ( mkConstWithLevelParams declName)
let info getConstInfo declName
forallTelescope info.type fun xs _ => do
let patterns terms.getElems.mapM fun term => do
let pattern elabTerm term none
synthesizeSyntheticMVarsUsingDefault
let pattern instantiateMVars pattern
let pattern Grind.preprocessPattern pattern
return pattern.abstract xs
Grind.addEMatchTheorem declName xs.size patterns.toList
| _ => throwUnsupportedSyntax
def grind (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
let mvarIds Grind.main mvarId config mainDeclName fallback
unless mvarIds.isEmpty do
throwError "`grind` failed\n{goalsToMessageData mvarIds}"
private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
let some fallback := fallback? | return (pure ())
let type := mkApp (mkConst ``Grind.GoalM) (mkConst ``Unit)
let value withLCtx {} {} do Term.elabTermAndSynthesize fallback type
let auxDeclName if let .const declName _ := value then
pure declName
else
let auxDeclName Term.mkAuxName `_grind_fallback
let decl := Declaration.defnDecl {
name := auxDeclName
levelParams := []
type, value, hints := .opaque, safety := .safe
}
addAndCompile decl
pure auxDeclName
unsafe evalConst (Grind.GoalM Unit) auxDeclName
@[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do
match stx with
| `(tactic| grind $config:optConfig $[on_failure $fallback?]?) =>
let fallback elabFallback fallback?
logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
let declName := ( Term.getDeclName?).getD `_grind
let config elabGrindConfig config
withMainContext do liftMetaFinishingTactic (grind · config declName fallback)
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic

View File

@@ -258,11 +258,11 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
i := i + 1
open Language in
def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax))
def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs : Array Syntax)
(initialInfo : Info)
(numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[])
(toTag : Array (Ident × FVarId) := #[]) : TacticM Unit := do
let hasAlts := altStxs?.isSome
let hasAlts := altStxs.size > 0
if hasAlts then
-- default to initial state outside of alts
-- HACK: because this node has the same span as the original tactic,
@@ -274,7 +274,9 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altS
where
-- continuation in the correct info context
goWithInfo := do
if let some altStxs := altStxs? then
let hasAlts := altStxs.size > 0
if hasAlts then
if let some tacSnap := ( readThe Term.Context).tacSnap? then
-- incrementality: create a new promise for each alternative, resolve current snapshot to
-- them, eventually put each of them back in `Context.tacSnap?` in `applyAltStx`
@@ -307,8 +309,7 @@ where
-- continuation in the correct incrementality context
goWithIncremental (tacSnaps : Array (SnapshotBundle TacticParsedSnapshot)) := do
let hasAlts := altStxs?.isSome
let altStxs := altStxs?.getD #[]
let hasAlts := altStxs.size > 0
let mut alts := alts
-- initial sanity checks: named cases should be known, wildcards should be last
@@ -342,12 +343,12 @@ where
let altName := getAltName altStx
if let some i := alts.findFinIdx? (·.1 == altName) then
-- cover named alternative
applyAltStx tacSnaps altStxs altStxIdx altStx alts[i]
applyAltStx tacSnaps altStxIdx altStx alts[i]
alts := alts.eraseIdx i
else if !alts.isEmpty && isWildcard altStx then
-- cover all alternatives
for alt in alts do
applyAltStx tacSnaps altStxs altStxIdx altStx alt
applyAltStx tacSnaps altStxIdx altStx alt
alts := #[]
else
throwErrorAt altStx "unused alternative '{altName}'"
@@ -378,7 +379,7 @@ where
altMVarIds.forM fun mvarId => admitGoal mvarId
/-- Applies syntactic alternative to alternative goal. -/
applyAltStx tacSnaps altStxs altStxIdx altStx alt := withRef altStx do
applyAltStx tacSnaps altStxIdx altStx alt := withRef altStx do
let { name := altName, info, mvarId := altMVarId } := alt
-- also checks for unknown alternatives
let numFields getAltNumFields elimInfo altName
@@ -475,7 +476,7 @@ private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Exp
/--
Given `inductionAlts` of the form
```
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
```
Return an array containing its alternatives.
-/
@@ -485,30 +486,21 @@ private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
/--
Given `inductionAlts` of the form
```
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
```
runs `cont (some alts)` where `alts` is an array containing all `inductionAlt`s while disabling incremental
reuse if any other syntax changed. If there's no `with` clause, then runs `cont none`.
runs `cont alts` where `alts` is an array containing all `inductionAlt`s while disabling incremental
reuse if any other syntax changed.
-/
private def withAltsOfOptInductionAlts (optInductionAlts : Syntax)
(cont : Option (Array Syntax) TacticM α) : TacticM α :=
(cont : Array Syntax TacticM α) : TacticM α :=
Term.withNarrowedTacticReuse (stx := optInductionAlts) (fun optInductionAlts =>
if optInductionAlts.isNone then
-- if there are no alternatives, what to compare is irrelevant as there will be no reuse
(mkNullNode #[], mkNullNode #[])
else
-- if there are no alts, then use the `with` token for `inner` for a ref for messages
let altStxs := optInductionAlts[0].getArg 2
let inner := if altStxs.getNumArgs > 0 then altStxs else optInductionAlts[0][0]
-- `with` and tactic applied to all branches must be unchanged for reuse
(mkNullNode optInductionAlts[0].getArgs[:2], inner))
(fun alts? =>
if optInductionAlts.isNone then -- no `with` clause
cont none
else if alts?.isOfKind nullKind then -- has alts
cont (some alts?.getArgs)
else -- has `with` clause, but no alts
cont (some #[]))
(mkNullNode optInductionAlts[0].getArgs[:2], optInductionAlts[0].getArg 2))
(fun alts => cont alts.getArgs)
private def getOptPreTacOfOptInductionAlts (optInductionAlts : Syntax) : Syntax :=
if optInductionAlts.isNone then mkNullNode else optInductionAlts[0][1]
@@ -526,7 +518,7 @@ private def expandMultiAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do
/--
Given `inductionAlts` of the form
```
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
```
Return `some inductionAlts'` if one of the alternatives have multiple LHSs, in the new `inductionAlts'`
all alternatives have a single LHS.
@@ -587,25 +579,12 @@ private def checkAltsOfOptInductionAlts (optInductionAlts : Syntax) : TacticM Un
throwErrorAt alt "more than one wildcard alternative '| _ => ...' used"
found := true
def getInductiveValFromMajor (induction : Bool) (major : Expr) : TacticM InductiveVal :=
def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
liftMetaMAtMain fun mvarId => do
let majorType inferType major
let majorType whnf majorType
matchConstInduct majorType.getAppFn
(fun _ => do
let tacticName := if induction then `induction else `cases
let mut hint := m!"\n\nExplanation: the '{tacticName}' tactic is for constructor-based reasoning \
as well as for applying custom {tacticName} principles with a 'using' clause or a registered '@[{tacticName}_eliminator]' theorem. \
The above type neither is an inductive type nor has a registered theorem."
if majorType.isProp then
hint := m!"{hint}\n\n\
Consider using the 'by_cases' tactic, which does true/false reasoning for propositions."
else if majorType.isType then
hint := m!"{hint}\n\n\
Type universes are not inductive types, and type-constructor-based reasoning is not possible. \
This is a strong limitation. According to Lean's underlying theory, the only provable distinguishing \
feature of types is their cardinalities."
Meta.throwTacticEx tacticName mvarId m!"major premise type is not an inductive type{indentExpr majorType}{hint}")
(fun _ => Meta.throwTacticEx `induction mvarId m!"major premise type is not an inductive type {indentExpr majorType}")
(fun val _ => pure val)
/--
@@ -648,7 +627,7 @@ private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (inducti
return getElimInfo elimName
unless targets.size == 1 do
throwError "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>'), and no default eliminator has been registered using attribute `[eliminator]`"
let indVal getInductiveValFromMajor induction targets[0]!
let indVal getInductiveValFromMajor targets[0]!
if induction && indVal.all.length != 1 then
throwError "'induction' tactic does not support mutually inductive types, the eliminator '{mkRecName indVal.name}' has multiple motives"
if induction && indVal.isNested then
@@ -708,10 +687,10 @@ def evalInduction : Tactic := fun stx =>
-- unchanged
-- everything up to the alternatives must be unchanged for reuse
Term.withNarrowedArgTacticReuse (stx := stx) (argIdx := 4) fun optInductionAlts => do
withAltsOfOptInductionAlts optInductionAlts fun alts? => do
withAltsOfOptInductionAlts optInductionAlts fun alts => do
let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
mvarId.assign result.elimApp
ElimApp.evalAlts elimInfo result.alts optPreTac alts? initInfo (numGeneralized := n) (toClear := targetFVarIds)
ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numGeneralized := n) (toClear := targetFVarIds)
appendGoals result.others.toList
where
checkTargets (targets : Array Expr) : MetaM Unit := do

View File

@@ -1,223 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner
-/
prelude
import Lean.Meta.Tactic.Split
import Lean.Elab.RecAppSyntax
import Lean.Elab.Tactic.Basic
import Init.Internal.Order
namespace Lean.Meta.Monotonicity
open Lean Meta
open Lean.Order
partial def headBetaUnderLambda (f : Expr) : Expr := Id.run do
let mut f := f.headBeta
if f.isLambda then
while f.bindingBody!.isHeadBetaTarget do
f := f.updateLambda! f.bindingInfo! f.bindingDomain! f.bindingBody!.headBeta
return f
/-- Environment extensions for monotonicity lemmas -/
builtin_initialize monotoneExt :
SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name)
registerSimpleScopedEnvExtension {
addEntry := fun dt (n, ks) => dt.insertCore ks n
initial := {}
}
builtin_initialize registerBuiltinAttribute {
name := `partial_fixpoint_monotone
descr := "monotonicity theorem"
add := fun decl _ kind => MetaM.run' do
let declTy := ( getConstInfo decl).type
let (xs, _, targetTy) withReducible <| forallMetaTelescopeReducing declTy
let_expr monotone α inst_α β inst_β f := targetTy |
throwError "@[partial_fixpoint_monotone] attribute only applies to lemmas proving {.ofConstName ``monotone}"
let f := f.headBeta
let f if f.isLambda then pure f else etaExpand f
let f := headBetaUnderLambda f
lambdaBoundedTelescope f 1 fun _ e => do
let key withReducible <| DiscrTree.mkPath e
monotoneExt.add (decl, key) kind
}
/--
Finds tagged monotonicity theorems of the form `monotone (fun x => e)`.
-/
def findMonoThms (e : Expr) : MetaM (Array Name) := do
(monotoneExt.getState ( getEnv)).getMatch e
private def defaultFailK (f : Expr) (monoThms : Array Name) : MetaM α :=
let extraMsg := if monoThms.isEmpty then m!"" else
m!"Tried to apply {.andList (monoThms.toList.map (m!"'{·}'"))}, but failed."
throwError "Failed to prove monotonicity of:{indentExpr f}\n{extraMsg}"
private def applyConst (goal : MVarId) (name : Name) : MetaM (List MVarId) := do
mapError (f := (m!"Could not apply {.ofConstName name}:{indentD ·}")) do
goal.applyConst name (cfg := { synthAssignedInstances := false})
/--
Base case for solveMonoStep: Handles goals of the form
```
monotone (fun f => f.1.2 x y)
```
It's tricky to solve them compositionally from the outside in, so here we construct the proof
from the inside out.
-/
partial def solveMonoCall (α inst_α : Expr) (e : Expr) : MetaM (Option Expr) := do
if e.isApp && !e.appArg!.hasLooseBVars then
let some hmono solveMonoCall α inst_α e.appFn! | return none
let hmonoType inferType hmono
let_expr monotone _ _ _ inst _ := hmonoType | throwError "solveMonoCall {e}: unexpected type {hmonoType}"
let some inst whnfUntil inst ``instOrderPi | throwError "solveMonoCall {e}: unexpected instance {inst}"
let_expr instOrderPi γ δ inst inst | throwError "solveMonoCall {e}: whnfUntil failed?{indentExpr inst}"
return mkAppOptM ``monotone_apply #[γ, δ, α, inst_α, inst, e.appArg!, none, hmono]
if e.isProj then
let some hmono solveMonoCall α inst_α e.projExpr! | return none
let hmonoType inferType hmono
let_expr monotone _ _ _ inst _ := hmonoType | throwError "solveMonoCall {e}: unexpected type {hmonoType}"
let some inst whnfUntil inst ``instPartialOrderPProd | throwError "solveMonoCall {e}: unexpected instance {inst}"
let_expr instPartialOrderPProd β γ inst_β inst_γ inst | throwError "solveMonoCall {e}: whnfUntil failed?{indentExpr inst}"
let n := if e.projIdx! == 0 then ``monotone_pprod_fst else ``monotone_pprod_snd
return mkAppOptM n #[β, γ, α, inst_β, inst_γ, inst_α, none, hmono]
if e == .bvar 0 then
let hmono mkAppOptM ``monotone_id #[α, inst_α]
return some hmono
return none
def solveMonoStep (failK : {α}, Expr Array Name MetaM α := @defaultFailK) (goal : MVarId) : MetaM (List MVarId) :=
goal.withContext do
trace[Elab.Tactic.monotonicity] "monotonicity at\n{goal}"
let type goal.getType
if type.isForall then
let (_, goal) goal.intro1P
return [goal]
match_expr type with
| monotone α inst_α β inst_β f =>
-- Ensure f is not headed by a redex and headed by at least one lambda, and clean some
-- redexes left by some of the lemmas we tend to apply
let f instantiateMVars f
let f := f.headBeta
let f if f.isLambda then pure f else etaExpand f
let f := headBetaUnderLambda f
let e := f.bindingBody!
-- No recursive calls left
if !e.hasLooseBVars then
return applyConst goal ``monotone_const
-- NB: `e` is now an open term.
-- Look through mdata
if e.isMData then
let f' := f.updateLambdaE! f.bindingDomain! e.mdataExpr!
let goal' mkFreshExprSyntheticOpaqueMVar (mkApp type.appFn! f')
goal.assign goal'
return [goal'.mvarId!]
-- Float letE to the environment
if let .letE n t v b _nonDep := e then
if t.hasLooseBVars || v.hasLooseBVars then
failK f #[]
let goal' withLetDecl n t v fun x => do
let b' := f.updateLambdaE! f.bindingDomain! (b.instantiate1 x)
let goal' mkFreshExprSyntheticOpaqueMVar (mkApp type.appFn! b')
goal.assign ( mkLetFVars #[x] goal')
pure goal'
return [goal'.mvarId!]
-- Float `letFun` to the environment.
-- `applyConst` tends to reduce the redex
match_expr e with
| letFun γ _ v b =>
if γ.hasLooseBVars || v.hasLooseBVars then
failK f #[]
let b' := f.updateLambdaE! f.bindingDomain! b
let p mkAppOptM ``monotone_letFun #[α, β, γ, inst_α, inst_β, v, b']
let new_goals mapError (f := (m!"Could not apply {p}:{indentD ·}")) do
goal.apply p
let [new_goal] := new_goals
| throwError "Unexpected number of goals after {.ofConstName ``monotone_letFun}."
let (_, new_goal)
if b.isLambda then
new_goal.intro b.bindingName!
else
new_goal.intro1
return [new_goal]
| _ => pure ()
-- Handle lambdas, preserving the name of the binder
if e.isLambda then
let [new_goal] applyConst goal ``monotone_of_monotone_apply
| throwError "Unexpected number of goals after {.ofConstName ``monotone_of_monotone_apply}."
let (_, new_goal) new_goal.intro e.bindingName!
return [new_goal]
-- A recursive call directly here
if e.isBVar then
return applyConst goal ``monotone_id
-- A recursive call
if let some hmono solveMonoCall α inst_α e then
trace[Elab.Tactic.monotonicity] "Found recursive call {e}:{indentExpr hmono}"
unless goal.checkedAssign hmono do
trace[Elab.Tactic.monotonicity] "Failed to assign {hmono} : {← inferType hmono} to goal"
failK f #[]
return []
let monoThms withLocalDeclD `f f.bindingDomain! fun f =>
-- The discrimination tree does not like open terms
findMonoThms (e.instantiate1 f)
trace[Elab.Tactic.monotonicity] "Found monoThms: {monoThms.map MessageData.ofConstName}"
for monoThm in monoThms do
let new_goals? try
let new_goals applyConst goal monoThm
trace[Elab.Tactic.monotonicity] "Succeeded with {.ofConstName monoThm}"
pure (some new_goals)
catch e =>
trace[Elab.Tactic.monotonicity] "{e.toMessageData}"
pure none
if let some new_goals := new_goals? then
return new_goals
-- Split match-expressions
if let some info := isMatcherAppCore? ( getEnv) e then
let candidate id do
let args := e.getAppArgs
for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
if args[i]!.hasLooseBVars then
return false
return true
if candidate then
-- We could be even more deliberate here and use the `lifter` lemmas
-- for the match statements instead of the `split` tactic.
-- For now using `splitMatch` works fine.
return Split.splitMatch goal e
failK f monoThms
| _ =>
throwError "Unexpected goal:{goal}"
partial def solveMono (failK : {α}, Expr Array Name MetaM α := defaultFailK) (goal : MVarId) : MetaM Unit := do
let new_goals solveMonoStep failK goal
new_goals.forM (solveMono failK)
open Elab Tactic in
@[builtin_tactic Lean.Order.monotonicity]
def evalMonotonicity : Tactic := fun _stx =>
liftMetaTactic Lean.Meta.Monotonicity.solveMonoStep
end Lean.Meta.Monotonicity
builtin_initialize Lean.registerTraceClass `Elab.Tactic.monotonicity

View File

@@ -63,7 +63,7 @@ def isNumeral? (e : Expr) : Option (Expr × Nat) :=
if e.isConstOf ``Nat.zero then
(mkConst ``Nat, 0)
else if let Expr.app (Expr.app (Expr.app (Expr.const ``OfNat.ofNat ..) α ..)
(Expr.lit (Literal.natVal n) ..) ..) .. := e.consumeMData then
(Expr.lit (Literal.natVal n) ..) ..) .. := e then
some (α, n)
else
none

View File

@@ -680,7 +680,7 @@ def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
/-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
`TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via
the tactic call `aesop (add 50% tactic Lean.Elab.Tactic.Omega.omegaDefault)`. -/
the tactic call `aesop (add 50% tactic Lean.Omega.omegaDefault)`. -/
def omegaDefault : TacticM Unit := omegaTactic {}
@[builtin_tactic Lean.Parser.Tactic.omega]

View File

@@ -507,7 +507,7 @@ partial def rintroCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (a
match pat with
| `(rintroPat| $pat:rcasesPat) =>
let pat := ( RCasesPatt.parse pat).typed? ref ty?
let (v, g) withRef pat.ref <| g.intro (pat.name?.getD `_)
let (v, g) g.intro (pat.name?.getD `_)
rcasesCore g fs clears (.fvar v) a pat cont
| `(rintroPat| ($(pats)* $[: $ty?']?)) =>
let ref := if pats.size == 1 then pat.raw else .missing

View File

@@ -769,11 +769,6 @@ opaque quickLt (a : @& Expr) (b : @& Expr) : Bool
@[extern "lean_expr_lt"]
opaque lt (a : @& Expr) (b : @& Expr) : Bool
def quickComp (a b : Expr) : Ordering :=
if quickLt a b then .lt
else if quickLt b a then .gt
else .eq
/--
Return true iff `a` and `b` are alpha equivalent.
Binder annotations are ignored.
@@ -1648,23 +1643,6 @@ def isFalse (e : Expr) : Bool :=
def isTrue (e : Expr) : Bool :=
e.cleanupAnnotations.isConstOf ``True
/--
`getForallArity type` returns the arity of a `forall`-type. This function consumes nested annotations,
and performs pending beta reductions. It does **not** use whnf.
Examples:
- If `a` is `Nat`, `getForallArity a` returns `0`
- If `a` is `Nat → Bool`, `getForallArity a` returns `1`
-/
partial def getForallArity : Expr Nat
| .mdata _ b => getForallArity b
| .forallE _ _ b _ => getForallArity b + 1
| e =>
if e.isHeadBetaTarget then
getForallArity e.headBeta
else
let e' := e.cleanupAnnotations
if e != e' then getForallArity e' else 0
/--
Checks if an expression is a "natural number numeral in normal form",
i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`

View File

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
prelude
import Lean.Parser.Syntax
import Lean.Meta.Tactic.Simp.RegisterCommand
import Lean.Elab.Command
import Lean.Elab.SetOption

View File

@@ -176,14 +176,6 @@ def mkEqOfHEq (h : Expr) : MetaM Expr := do
| _ =>
throwAppBuilderException ``eq_of_heq m!"heterogeneous equality proof expected{indentExpr h}"
/-- Given `h : Eq a b`, returns a proof of `HEq a b`. -/
def mkHEqOfEq (h : Expr) : MetaM Expr := do
let hType infer h
let some (α, a, b) := hType.eq?
| throwAppBuilderException ``heq_of_eq m!"equality proof expected{indentExpr h}"
let u getLevel α
return mkApp4 (mkConst ``heq_of_eq [u]) α a b h
/--
If `e` is `@Eq.refl α a`, return `a`.
-/

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