Compare commits

..

12 Commits

Author SHA1 Message Date
Kim Morrison
3be678c88a restore newly-confluence #check_simp 2024-06-18 17:00:25 +10:00
Kim Morrison
de9b419f37 line breaks 2024-06-18 16:58:33 +10:00
Kim Morrison
bfc2ac9621 adjust proofs 2024-06-18 16:54:06 +10:00
Kim Morrison
1706be284f finish #check_simp 2024-06-18 16:37:02 +10:00
Kim Morrison
188e532303 . 2024-06-18 15:11:49 +10:00
Kim Morrison
19b8c64239 much better 2024-06-18 15:10:47 +10:00
Kim Morrison
71efbdc3f9 more #check_simp 2024-06-18 14:45:46 +10:00
Kim Morrison
983054ec58 . 2024-06-18 13:12:53 +10:00
Kim Morrison
01b5d60f9a beginning to install #check_simp statements 2024-06-18 12:51:12 +10:00
Kim Morrison
322e3ea027 ... 2024-06-18 11:51:59 +10:00
Kim Morrison
7a33c9758e finish first pass 2024-06-18 11:24:26 +10:00
Kim Morrison
516e248b19 wip replicate 2024-06-18 10:49:22 +10:00
1325 changed files with 3709 additions and 22711 deletions

View File

@@ -15,7 +15,7 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4
uses: actions/checkout@v3
- name: actionlint
uses: raven-actions/actionlint@v1
with:

View File

@@ -9,17 +9,6 @@ on:
merge_group:
schedule:
- cron: '0 7 * * *' # 8AM CET/11PM PT
# for manual re-release of a nightly
workflow_dispatch:
inputs:
action:
description: 'Action'
required: true
default: 'release nightly'
type: choice
options:
- release nightly
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}-${{ github.event_name }}
@@ -52,11 +41,11 @@ jobs:
steps:
- name: Checkout
uses: actions/checkout@v4
uses: actions/checkout@v3
# don't schedule nightlies on forks
if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
- name: Set Nightly
if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
id: set-nightly
run: |
if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
@@ -397,7 +386,7 @@ jobs:
else
${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
fi
- uses: actions/upload-artifact@v4
- uses: actions/upload-artifact@v3
if: matrix.release
with:
name: build-${{ matrix.name }}
@@ -470,7 +459,7 @@ jobs:
runs-on: ubuntu-latest
needs: build
steps:
- uses: actions/download-artifact@v4
- uses: actions/download-artifact@v3
with:
path: artifacts
- name: Release
@@ -478,14 +467,8 @@ jobs:
with:
files: artifacts/*/*
fail_on_unmatched_files: true
prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- name: Update release.lean-lang.org
run: |
gh workflow -R leanprover/release-index run update-index.yml
env:
GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
# This job creates nightly releases during the cron job.
# It is responsible for creating the tag, and automatically generating a changelog.
@@ -495,12 +478,12 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4
uses: actions/checkout@v3
with:
# needed for tagging
fetch-depth: 0
token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
- uses: actions/download-artifact@v4
- uses: actions/download-artifact@v3
with:
path: artifacts
- name: Prepare Nightly Release
@@ -528,8 +511,3 @@ jobs:
repository: ${{ github.repository_owner }}/lean4-nightly
env:
GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
- name: Update release.lean-lang.org
run: |
gh workflow -R leanprover/release-index run update-index.yml
env:
GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}

View File

@@ -50,7 +50,7 @@ jobs:
NIX_BUILD_ARGS: --print-build-logs --fallback
steps:
- name: Checkout
uses: actions/checkout@v4
uses: actions/checkout@v3
with:
# the default is to use a virtual merge commit between the PR and master: just use the PR
ref: ${{ github.event.pull_request.head.sha }}

View File

@@ -234,7 +234,7 @@ jobs:
# Checkout the Batteries repository with all branches
- name: Checkout Batteries repository
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
uses: actions/checkout@v4
uses: actions/checkout@v3
with:
repository: leanprover-community/batteries
token: ${{ secrets.MATHLIB4_BOT }}
@@ -291,7 +291,7 @@ jobs:
# Checkout the mathlib4 repository with all branches
- name: Checkout mathlib4 repository
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
uses: actions/checkout@v4
uses: actions/checkout@v3
with:
repository: leanprover-community/mathlib4
token: ${{ secrets.MATHLIB4_BOT }}
@@ -328,7 +328,7 @@ jobs:
git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
git add lean-toolchain
sed -i 's,require "leanprover-community" / "batteries" @ ".\+",require "leanprover-community" / "batteries" @ "git#nightly-testing-'"${MOST_RECENT_NIGHTLY}"'",' lakefile.lean
sed -i "s/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \".\+\"/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
lake update batteries
git add lakefile.lean lake-manifest.json
git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"

View File

@@ -20,12 +20,10 @@ jobs:
gh run view "$run_id"
echo "Cancelling (just in case)"
gh run cancel "$run_id" || echo "(failed)"
echo "Waiting for 30s"
sleep 30
gh run view "$run_id"
echo "Waiting for 10s"
sleep 10
echo "Rerunning"
gh run rerun "$run_id"
gh run view "$run_id"
shell: bash
env:
head_ref: ${{ github.head_ref }}

View File

@@ -23,7 +23,7 @@ jobs:
# This action should push to an otherwise protected branch, so it
# uses a deploy key with write permissions, as suggested at
# https://stackoverflow.com/a/76135647/946226
- uses: actions/checkout@v4
- uses: actions/checkout@v3
with:
ssh-key: ${{secrets.STAGE0_SSH_KEY}}
- run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"

View File

@@ -42,4 +42,4 @@
/src/Lean/Elab/Tactic/Guard.lean @digama0
/src/Init/Guard.lean @digama0
/src/Lean/Server/CodeActions/ @digama0
/src/Std/ @TwoFX

View File

@@ -8,326 +8,13 @@ This file contains work-in-progress notes for the upcoming release, as well as p
Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
of each version.
v4.11.0
v4.10.0
----------
Development in progress.
v4.10.0
----------
Release candidate, release notes will be copied from branch `releases/v4.10.0` once completed.
v4.9.0
----------
### Language features, tactics, and metaprograms
* **Definition transparency**
* [#4053](https://github.com/leanprover/lean4/pull/4053) adds the `seal` and `unseal` commands, which make definitions locally be irreducible or semireducible.
* [#4061](https://github.com/leanprover/lean4/pull/4061) marks functions defined by well-founded recursion with `@[irreducible]` by default,
which should prevent the expensive and often unfruitful unfolding of such definitions (see breaking changes below).
* **Incrementality**
* [#3940](https://github.com/leanprover/lean4/pull/3940) extends incremental elaboration into various steps inside of declarations:
definition headers, bodies, and tactics.
![Recording 2024-05-10](https://github.com/leanprover/lean4/assets/109126/c9d67b6f-c131-4bc3-a0de-7d63eaf1bfc9).
* [250994](https://github.com/leanprover/lean4/commit/250994166ce036ab8644e459129f51ea79c1c2d2)
and [67338b](https://github.com/leanprover/lean4/commit/67338bac2333fa39a8656e8f90574784e4c23d3d)
add `@[incremental]` attribute to mark an elaborator as supporting incremental elaboration.
* [#4259](https://github.com/leanprover/lean4/pull/4259) improves resilience by ensuring incremental commands and tactics are reached only in supported ways.
* [#4268](https://github.com/leanprover/lean4/pull/4268) adds special handling for `:= by` so that stray tokens in tactic blocks do not inhibit incrementality.
* [#4308](https://github.com/leanprover/lean4/pull/4308) adds incremental `have` tactic.
* [#4340](https://github.com/leanprover/lean4/pull/4340) fixes incorrect info tree reuse.
* [#4364](https://github.com/leanprover/lean4/pull/4364) adds incrementality for careful command macros such as `set_option in theorem`, `theorem foo.bar`, and `lemma`.
* [#4395](https://github.com/leanprover/lean4/pull/4395) adds conservative fix for whitespace handling to avoid incremental reuse leading to goals in front of the text cursor being shown.
* [#4407](https://github.com/leanprover/lean4/pull/4407) fixes non-incremental commands in macros blocking further incremental reporting.
* [#4436](https://github.com/leanprover/lean4/pull/4436) fixes incremental reporting when there are nested tactics in terms.
* **Functional induction**
* [#4135](https://github.com/leanprover/lean4/pull/4135) ensures that the names used for functional induction are reserved.
* [#4327](https://github.com/leanprover/lean4/pull/4327) adds support for structural recursion on reflexive types.
For example,
```lean4
inductive Many (α : Type u) where
| none : Many α
| more : α → (Unit → Many α) → Many α
def Many.map {α β : Type u} (f : α → β) : Many α → Many β
| .none => .none
| .more x xs => .more (f x) (fun _ => (xs ()).map f)
#check Many.map.induct
/-
Many.map.induct {α β : Type u} (f : α → β) (motive : Many α → Prop)
(case1 : motive Many.none)
(case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) :
∀ (a : Many α), motive a
-/
```
* [#3903](https://github.com/leanprover/lean4/pull/3903) makes the Lean frontend normalize all line endings to LF before processing.
This lets Lean be insensitive to CRLF vs LF line endings, improving the cross-platform experience and making Lake hashes be faithful to what Lean processes.
* [#4130](https://github.com/leanprover/lean4/pull/4130) makes the tactic framework be able to recover from runtime errors (for example, deterministic timeouts or maximum recursion depth errors).
* `split` tactic
* [#4211](https://github.com/leanprover/lean4/pull/4211) fixes `split at h` when `h` has forward dependencies.
* [#4349](https://github.com/leanprover/lean4/pull/4349) allows `split` for `if`-expressions to work on non-propositional goals.
* `apply` tactic
* [#3929](https://github.com/leanprover/lean4/pull/3929) makes error message for `apply` show implicit arguments in unification errors as needed.
Modifies `MessageData` type (see breaking changes below).
* `cases` tactic
* [#4224](https://github.com/leanprover/lean4/pull/4224) adds support for unification of offsets such as `x + 20000 = 20001` in `cases` tactic.
* `omega` tactic
* [#4073](https://github.com/leanprover/lean4/pull/4073) lets `omega` fall back to using classical `Decidable` instances when setting up contradiction proofs.
* [#4141](https://github.com/leanprover/lean4/pull/4141) and [#4184](https://github.com/leanprover/lean4/pull/4184) fix bugs.
* [#4264](https://github.com/leanprover/lean4/pull/4264) improves `omega` error message if no facts found in local context.
* [#4358](https://github.com/leanprover/lean4/pull/4358) improves expression matching in `omega` by using `match_expr`.
* `simp` tactic
* [#4176](https://github.com/leanprover/lean4/pull/4176) makes names of erased lemmas clickable.
* [#4208](https://github.com/leanprover/lean4/pull/4208) adds a pretty printer for discrimination tree keys.
* [#4202](https://github.com/leanprover/lean4/pull/4202) adds `Simp.Config.index` configuration option,
which controls whether to use the full discrimination tree when selecting candidate simp lemmas.
When `index := false`, only the head function is taken into account, like in Lean 3.
This feature can help users diagnose tricky simp failures or issues in code from libraries
developed using Lean 3 and then ported to Lean 4.
In the following example, it will report that `foo` is a problematic theorem.
```lean
opaque f : Nat → Nat → Nat
@[simp] theorem foo : f x (x, y).2 = y := by sorry
example : f a b ≤ b := by
set_option diagnostics true in
simp (config := { index := false })
/-
[simp] theorems with bad keys
foo, key: f _ (@Prod.mk _ _).2
-/
```
With the information above, users can annotate theorems such as `foo` using `no_index` for problematic subterms. Example:
```lean
opaque f : Nat → Nat → Nat
@[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry
example : f a b ≤ b := by
simp -- `foo` is still applied with `index := true`
```
* [#4274](https://github.com/leanprover/lean4/pull/4274) prevents internal `match` equational theorems from appearing in simp trace.
* [#4177](https://github.com/leanprover/lean4/pull/4177) and [#4359](https://github.com/leanprover/lean4/pull/4359) make `simp` continue even if a simp lemma does not elaborate, if the tactic state is in recovery mode.
* [#4341](https://github.com/leanprover/lean4/pull/4341) fixes panic when applying `@[simp]` to malformed theorem syntax.
* [#4345](https://github.com/leanprover/lean4/pull/4345) fixes `simp` so that it does not use the forward version of a user-specified backward theorem.
* [#4352](https://github.com/leanprover/lean4/pull/4352) adds missing `dsimp` simplifications for fixed parameters of generated congruence theorems.
* [#4362](https://github.com/leanprover/lean4/pull/4362) improves trace messages for `simp` so that constants are hoverable.
* **Elaboration**
* [#4046](https://github.com/leanprover/lean4/pull/4046) makes subst notation (`he ▸ h`) try rewriting in both directions even when there is no expected type available.
* [#3328](https://github.com/leanprover/lean4/pull/3328) adds support for identifiers in autoparams (for example, `rfl` in `(h : x = y := by exact rfl)`).
* [#4096](https://github.com/leanprover/lean4/pull/4096) changes how the type in `let` and `have` is elaborated, requiring that any tactics in the type be evaluated before proceeding, improving performance.
* [#4215](https://github.com/leanprover/lean4/pull/4215) ensures the expression tree elaborator commits to the computed "max type" for the entire arithmetic expression.
* [#4267](https://github.com/leanprover/lean4/pull/4267) cases signature elaboration errors to show even if there are parse errors in the body.
* [#4368](https://github.com/leanprover/lean4/pull/4368) improves error messages when numeric literals fail to synthesize an `OfNat` instance,
including special messages warning when the expected type of the numeral can be a proposition.
* **Metaprogramming**
* [#4167](https://github.com/leanprover/lean4/pull/4167) adds `Lean.MVarId.revertAll` to revert all free variables.
* [#4169](https://github.com/leanprover/lean4/pull/4169) adds `Lean.MVarId.ensureNoMVar` to ensure the goal's target contains no expression metavariables.
* [#4180](https://github.com/leanprover/lean4/pull/4180) adds `cleanupAnnotations` parameter to `forallTelescope` methods.
* [#4307](https://github.com/leanprover/lean4/pull/4307) adds support for parser aliases in syntax quotations.
* Work toward implementing `grind` tactic
* [0a515e](https://github.com/leanprover/lean4/commit/0a515e2ec939519dafb4b99daa81d6bf3c411404)
and [#4164](https://github.com/leanprover/lean4/pull/4164)
add `grind_norm` and `grind_norm_proc` attributes and `@[grind_norm]` theorems.
* [#4170](https://github.com/leanprover/lean4/pull/4170), [#4221](https://github.com/leanprover/lean4/pull/4221),
and [#4249](https://github.com/leanprover/lean4/pull/4249) create `grind` preprocessor and core module.
* [#4235](https://github.com/leanprover/lean4/pull/4235) and [d6709e](https://github.com/leanprover/lean4/commit/d6709eb1576c5d40fc80462637dc041f970e4d9f)
add special `cases` tactic to `grind` along with `@[grind_cases]` attribute to mark types that this `cases` tactic should automatically apply to.
* [#4243](https://github.com/leanprover/lean4/pull/4243) adds special `injection?` tactic to `grind`.
* **Other fixes or improvements**
* [#4065](https://github.com/leanprover/lean4/pull/4065) fixes a bug in the `Nat.reduceLeDiff` simproc.
* [#3969](https://github.com/leanprover/lean4/pull/3969) makes deprecation warnings activate even for generalized field notation ("dot notation").
* [#4132](https://github.com/leanprover/lean4/pull/4132) fixes the `sorry` term so that it does not activate the implicit lambda feature
* [9803c5](https://github.com/leanprover/lean4/commit/9803c5dd63dc993628287d5f998525e74af03839)
and [47c8e3](https://github.com/leanprover/lean4/commit/47c8e340d65b01f4d9f011686e3dda0d4bb30a20)
move `cdot` and `calc` parsers to `Lean` namespace.
* [#4252](https://github.com/leanprover/lean4/pull/4252) fixes the `case` tactic so that it is usable in macros by having it erase macro scopes from the tag.
* [26b671](https://github.com/leanprover/lean4/commit/26b67184222e75529e1b166db050aaebee323d2d)
and [cc33c3](https://github.com/leanprover/lean4/commit/cc33c39cb022d8a3166b1e89677c78835ead1fc7)
extract `haveId` syntax.
* [#4335](https://github.com/leanprover/lean4/pull/4335) fixes bugs in partial `calc` tactic when there is mdata or metavariables.
* [#4329](https://github.com/leanprover/lean4/pull/4329) makes `termination_by?` report unused each unused parameter as `_`.
* **Docs:** [#4238](https://github.com/leanprover/lean4/pull/4238), [#4294](https://github.com/leanprover/lean4/pull/4294),
[#4338](https://github.com/leanprover/lean4/pull/4338).
### Language server, widgets, and IDE extensions
* [#4066](https://github.com/leanprover/lean4/pull/4066) fixes features like "Find References" when browsing core Lean sources.
* [#4254](https://github.com/leanprover/lean4/pull/4254) allows embedding user widgets in structured messages.
Companion PR is [vscode-lean4#449](https://github.com/leanprover/vscode-lean4/pull/449).
* [#4445](https://github.com/leanprover/lean4/pull/4445) makes watchdog more resilient against badly behaving clients.
### Library
* [#4059](https://github.com/leanprover/lean4/pull/4059) upstreams many `List` and `Array` operations and theorems from Batteries.
* [#4055](https://github.com/leanprover/lean4/pull/4055) removes the unused `Inhabited` instance for `Subtype`.
* [#3967](https://github.com/leanprover/lean4/pull/3967) adds dates in existing `@[deprecated]` attributes.
* [#4231](https://github.com/leanprover/lean4/pull/4231) adds boilerplate `Char`, `UInt`, and `Fin` theorems.
* [#4205](https://github.com/leanprover/lean4/pull/4205) fixes the `MonadStore` type classes to use `semiOutParam`.
* [#4350](https://github.com/leanprover/lean4/pull/4350) renames `IsLawfulSingleton` to `LawfulSingleton`.
* `Nat`
* [#4094](https://github.com/leanprover/lean4/pull/4094) swaps `Nat.zero_or` and `Nat.or_zero`.
* [#4098](https://github.com/leanprover/lean4/pull/4098) and [#4145](https://github.com/leanprover/lean4/pull/4145)
change the definition of `Nat.mod` so that `n % (m + n)` reduces when `n` is literal without relying on well-founded recursion,
which becomes irreducible by default in [#4061](https://github.com/leanprover/lean4/pull/4061).
* [#4188](https://github.com/leanprover/lean4/pull/4188) redefines `Nat.testBit` to be more performant.
* Theorems: [#4199](https://github.com/leanprover/lean4/pull/4199).
* `Array`
* [#4074](https://github.com/leanprover/lean4/pull/4074) improves the functional induction principle `Array.feraseIdx.induct`.
* `List`
* [#4172](https://github.com/leanprover/lean4/pull/4172) removes `@[simp]` from `List.length_pos`.
* `Option`
* [#4037](https://github.com/leanprover/lean4/pull/4037) adds theorems to simplify `Option`-valued dependent if-then-else.
* [#4314](https://github.com/leanprover/lean4/pull/4314) removes `@[simp]` from `Option.bind_eq_some`.
* `BitVec`
* Theorems: [#3920](https://github.com/leanprover/lean4/pull/3920), [#4095](https://github.com/leanprover/lean4/pull/4095),
[#4075](https://github.com/leanprover/lean4/pull/4075), [#4148](https://github.com/leanprover/lean4/pull/4148),
[#4165](https://github.com/leanprover/lean4/pull/4165), [#4178](https://github.com/leanprover/lean4/pull/4178),
[#4200](https://github.com/leanprover/lean4/pull/4200), [#4201](https://github.com/leanprover/lean4/pull/4201),
[#4298](https://github.com/leanprover/lean4/pull/4298), [#4299](https://github.com/leanprover/lean4/pull/4299),
[#4257](https://github.com/leanprover/lean4/pull/4257), [#4179](https://github.com/leanprover/lean4/pull/4179),
[#4321](https://github.com/leanprover/lean4/pull/4321), [#4187](https://github.com/leanprover/lean4/pull/4187).
* [#4193](https://github.com/leanprover/lean4/pull/4193) adds simprocs for reducing `x >>> i` and `x <<< i` where `i` is a bitvector literal.
* [#4194](https://github.com/leanprover/lean4/pull/4194) adds simprocs for reducing `(x <<< i) <<< j` and `(x >>> i) >>> j` where `i` and `j` are natural number literals.
* [#4229](https://github.com/leanprover/lean4/pull/4229) redefines `rotateLeft`/`rotateRight` to use modulo reduction of shift offset.
* [0d3051](https://github.com/leanprover/lean4/commit/0d30517dca094a07bcb462252f718e713b93ffba) makes `<num>#<term>` bitvector literal notation global.
* `Char`/`String`
* [#4143](https://github.com/leanprover/lean4/pull/4143) modifies `String.substrEq` to avoid linter warnings in downstream code.
* [#4233](https://github.com/leanprover/lean4/pull/4233) adds simprocs for `Char` and `String` inequalities.
* [#4348](https://github.com/leanprover/lean4/pull/4348) upstreams Mathlib lemmas.
* [#4354](https://github.com/leanprover/lean4/pull/4354) upstreams basic `String` lemmas.
* `HashMap`
* [#4248](https://github.com/leanprover/lean4/pull/4248) fixes implicitness of typeclass arguments in `HashMap.ofList`.
* `IO`
* [#4036](https://github.com/leanprover/lean4/pull/4036) adds `IO.Process.getCurrentDir` and `IO.Process.setCurrentDir` for adjusting the current process's working directory.
* **Cleanup:** [#4077](https://github.com/leanprover/lean4/pull/4077), [#4189](https://github.com/leanprover/lean4/pull/4189),
[#4304](https://github.com/leanprover/lean4/pull/4304).
* **Docs:** [#4001](https://github.com/leanprover/lean4/pull/4001), [#4166](https://github.com/leanprover/lean4/pull/4166),
[#4332](https://github.com/leanprover/lean4/pull/4332).
### Lean internals
* **Defeq and WHNF algorithms**
* [#4029](https://github.com/leanprover/lean4/pull/4029) remove unnecessary `checkpointDefEq`
* [#4206](https://github.com/leanprover/lean4/pull/4206) fixes `isReadOnlyOrSyntheticOpaque` to respect metavariable depth.
* [#4217](https://github.com/leanprover/lean4/pull/4217) fixes missing occurs check for delayed assignments.
* **Definition transparency**
* [#4052](https://github.com/leanprover/lean4/pull/4052) adds validation to application of `@[reducible]`/`@[semireducible]`/`@[irreducible]` attributes (with `local`/`scoped` modifiers as well).
Setting `set_option allowUnsafeReductibility true` turns this validation off.
* **Inductive types**
* [#3591](https://github.com/leanprover/lean4/pull/3591) fixes a bug where indices could be incorrectly promoted to parameters.
* [#3398](https://github.com/leanprover/lean4/pull/3398) fixes a bug in the injectivity theorem generator.
* [#4342](https://github.com/leanprover/lean4/pull/4342) fixes elaboration of mutual inductives with instance parameters.
* **Diagnostics and profiling**
* [#3986](https://github.com/leanprover/lean4/pull/3986) adds option `trace.profiler.useHeartbeats` to switch `trace.profiler.threshold` to being in terms of heartbeats instead of milliseconds.
* [#4082](https://github.com/leanprover/lean4/pull/4082) makes `set_option diagnostics true` report kernel diagnostic information.
* **Typeclass resolution**
* [#4119](https://github.com/leanprover/lean4/pull/4119) fixes multiple issues with TC caching interacting with `synthPendingDepth`, adds `maxSynthPendingDepth` option with default value `1`.
* [#4210](https://github.com/leanprover/lean4/pull/4210) ensures local instance cache does not contain multiple copies of the same instance.
* [#4216](https://github.com/leanprover/lean4/pull/4216) fix handling of metavariables, to avoid needing to set the option `backward.synthInstance.canonInstances` to `false`.
* **Other fixes or improvements**
* [#4080](https://github.com/leanprover/lean4/pull/4080) fixes propagation of state for `Lean.Elab.Command.liftCoreM` and `Lean.Elab.Command.liftTermElabM`.
* [#3944](https://github.com/leanprover/lean4/pull/3944) makes the `Repr` deriving handler be consistent between `structure` and `inductive` for how types and proofs are erased.
* [#4113](https://github.com/leanprover/lean4/pull/4113) propagates `maxHeartbeats` to kernel to control "(kernel) deterministic timeout" error.
* [#4125](https://github.com/leanprover/lean4/pull/4125) reverts [#3970](https://github.com/leanprover/lean4/pull/3970) (monadic generalization of `FindExpr`).
* [#4128](https://github.com/leanprover/lean4/pull/4128) catches stack overflow in auto-bound implicits feature.
* [#4129](https://github.com/leanprover/lean4/pull/4129) adds `tryCatchRuntimeEx` combinator to replace `catchRuntimeEx` reader state.
* [#4155](https://github.com/leanprover/lean4/pull/4155) simplifies the expression canonicalizer.
* [#4151](https://github.com/leanprover/lean4/pull/4151) and [#4369](https://github.com/leanprover/lean4/pull/4369)
add many missing trace classes.
* [#4185](https://github.com/leanprover/lean4/pull/4185) makes congruence theorem generators clean up type annotations of argument types.
* [#4192](https://github.com/leanprover/lean4/pull/4192) fixes restoration of infotrees when auto-bound implicit feature is activated,
fixing a pretty printing error in hovers and strengthening the unused variable linter.
* [dfb496](https://github.com/leanprover/lean4/commit/dfb496a27123c3864571aec72f6278e2dad1cecf) fixes `declareBuiltin` to allow it to be called multiple times per declaration.
* Cleanup: [#4112](https://github.com/leanprover/lean4/pull/4112), [#4126](https://github.com/leanprover/lean4/pull/4126), [#4091](https://github.com/leanprover/lean4/pull/4091), [#4139](https://github.com/leanprover/lean4/pull/4139), [#4153](https://github.com/leanprover/lean4/pull/4153).
* Tests: [030406](https://github.com/leanprover/lean4/commit/03040618b8f9b35b7b757858483e57340900cdc4), [#4133](https://github.com/leanprover/lean4/pull/4133).
### Compiler, runtime, and FFI
* [#4100](https://github.com/leanprover/lean4/pull/4100) improves reset/reuse algorithm; it now runs a second pass relaxing the constraint that reused memory cells must only be for the exact same constructor.
* [#2903](https://github.com/leanprover/lean4/pull/2903) fixes segfault in old compiler from mishandling `noConfusion` applications.
* [#4311](https://github.com/leanprover/lean4/pull/4311) fixes bug in constant folding.
* [#3915](https://github.com/leanprover/lean4/pull/3915) documents the runtime memory layout for inductive types.
### Lake
* [#4057](https://github.com/leanprover/lean4/pull/4057) adds support for docstrings on `require` commands.
* [#4088](https://github.com/leanprover/lean4/pull/4088) improves hovers for `family_def` and `library_data` commands.
* [#4147](https://github.com/leanprover/lean4/pull/4147) adds default `README.md` to package templates
* [#4261](https://github.com/leanprover/lean4/pull/4261) extends `lake test` help page, adds help page for `lake check-test`,
adds `lake lint` and tag `@[lint_driver]`, adds support for specifying test and lint drivers from dependencies,
adds `testDriverArgs` and `lintDriverArgs` options, adds support for library test drivers,
makes `lake check-test` and `lake check-lint` only load the package without dependencies.
* [#4270](https://github.com/leanprover/lean4/pull/4270) adds `lake pack` and `lake unpack` for packing and unpacking Lake build artifacts from an archive.
* [#4083](https://github.com/leanprover/lean4/pull/4083)
Switches the manifest format to use `major.minor.patch` semantic
versions. Major version increments indicate breaking changes (e.g., new
required fields and semantic changes to existing fields). Minor version
increments (after `0.x`) indicate backwards-compatible extensions (e.g.,
adding optional fields, removing fields). This change is backwards
compatible. Lake will still successfully read old manifests with numeric
versions. It will treat the numeric version `N` as semantic version
`0.N.0`. Lake will also accept manifest versions with `-` suffixes
(e.g., `x.y.z-foo`) and then ignore the suffix.
* [#4273](https://github.com/leanprover/lean4/pull/4273) adds a lift from `JobM` to `FetchM` for backwards compatibility reasons.
* [#4351](https://github.com/leanprover/lean4/pull/4351) fixes `LogIO`-to-`CliM`-lifting performance issues.
* [#4343](https://github.com/leanprover/lean4/pull/4343) make Lake store the dependency trace for a build in
the cached build long and then verifies that it matches the trace of the current build before replaying the log.
* [#4402](https://github.com/leanprover/lean4/pull/4402) moves the cached log into the trace file (no more `.log.json`).
This means logs are no longer cached on fatal errors and this ensures that an out-of-date log is not associated with an up-to-date trace.
Separately, `.hash` file generation was changed to be more reliable as well.
The `.hash` files are deleted as part of the build and always regenerate with `--rehash`.
* **Other fixes or improvements**
* [#4056](https://github.com/leanprover/lean4/pull/4056) cleans up tests
* [#4244](https://github.com/leanprover/lean4/pull/4244) fixes `noRelease` test when Lean repo is tagged
* [#4346](https://github.com/leanprover/lean4/pull/4346) improves `tests/serve`
* [#4356](https://github.com/leanprover/lean4/pull/4356) adds build log path to the warning for a missing or invalid build log.
### DevOps
* [#3984](https://github.com/leanprover/lean4/pull/3984) adds a script (`script/rebase-stage0.sh`) for `git rebase -i` that automatically updates each stage0.
* [#4108](https://github.com/leanprover/lean4/pull/4108) finishes renamings from transition to Std to Batteries.
* [#4109](https://github.com/leanprover/lean4/pull/4109) adjusts the Github bug template to mention testing using [live.lean-lang.org](https://live.lean-lang.org).
* [#4136](https://github.com/leanprover/lean4/pull/4136) makes CI rerun only when `full-ci` label is added or removed.
* [#4175](https://github.com/leanprover/lean4/pull/4175) and [72b345](https://github.com/leanprover/lean4/commit/72b345c621a9a06d3a5a656da2b793a5eea5f168)
switch to using `#guard_msgs` to run tests as much as possible.
* [#3125](https://github.com/leanprover/lean4/pull/3125) explains the Lean4 `pygments` lexer.
* [#4247](https://github.com/leanprover/lean4/pull/4247) sets up a procedure for preparing release notes.
* [#4032](https://github.com/leanprover/lean4/pull/4032) modernizes build instructions and workflows.
* [#4255](https://github.com/leanprover/lean4/pull/4255) moves some expensive checks from merge queue to releases.
* [#4265](https://github.com/leanprover/lean4/pull/4265) adds aarch64 macOS as native compilation target for CI.
* [f05a82](https://github.com/leanprover/lean4/commit/f05a82799a01569edeb5e2594cd7d56282320f9e) restores macOS aarch64 install suffix in CI
* [#4317](https://github.com/leanprover/lean4/pull/4317) updates build instructions for macOS.
* [#4333](https://github.com/leanprover/lean4/pull/4333) adjusts workflow to update Batteries in manifest when creating `lean-pr-testing-NNNN` Mathlib branches.
* [#4355](https://github.com/leanprover/lean4/pull/4355) simplifies `lean4checker` step of release checklist.
* [#4361](https://github.com/leanprover/lean4/pull/4361) adds installing elan to `pr-release` CI step.
### Breaking changes
While most changes could be considered to be a breaking change, this section makes special note of API changes.
* `Nat.zero_or` and `Nat.or_zero` have been swapped ([#4094](https://github.com/leanprover/lean4/pull/4094)).
* `IsLawfulSingleton` is now `LawfulSingleton` ([#4350](https://github.com/leanprover/lean4/pull/4350)).
* `BitVec.rotateLeft` and `BitVec.rotateRight` now take the shift modulo the bitwidth ([#4229](https://github.com/leanprover/lean4/pull/4229)).
* These are no longer simp lemmas:
`List.length_pos` ([#4172](https://github.com/leanprover/lean4/pull/4172)),
`Option.bind_eq_some` ([#4314](https://github.com/leanprover/lean4/pull/4314)).
* Types in `let` and `have` (both the expressions and tactics) may fail to elaborate due to new restrictions on what sorts of elaboration problems may be postponed ([#4096](https://github.com/leanprover/lean4/pull/4096)).
In particular, tactics embedded in the type will no longer make use of the type of `value` in expressions such as `let x : type := value; body`.
* Now functions defined by well-founded recursion are marked with `@[irreducible]` by default ([#4061](https://github.com/leanprover/lean4/pull/4061)).
Existing proofs that hold by definitional equality (e.g. `rfl`) can be
rewritten to explictly unfold the function definition (using `simp`,
`unfold`, `rw`), or the recursive function can be temporarily made
semireducible (using `unseal f in` before the command), or the function
definition itself can be marked as `@[semireducible]` to get the previous
behavior.
* Due to [#3929](https://github.com/leanprover/lean4/pull/3929):
* The `MessageData.ofPPFormat` constructor has been removed.
Its functionality has been split into two:
- for lazy structured messages, please use `MessageData.lazy`;
- for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
* The `MessageData.ofFormat` constructor has been turned into a function.
If you need to inspect `MessageData`, you can pattern-match on `MessageData.ofFormatWithInfos`.
Release candidate, release notes will be copied from branch `releases/v4.9.0` once completed.
v4.8.0
---------

View File

@@ -5,8 +5,7 @@ See below for the checklist for release candidates.
We'll use `v4.6.0` as the intended release version as a running example.
- One week before the planned release, ensure that (1) someone has written the release notes and (2) someone has written the first draft of the release blog post.
If there is any material in `./releases_drafts/`, then the release notes are not done. (See the section "Writing the release notes".)
- One week before the planned release, ensure that someone has written the first draft of the release blog post
- `git checkout releases/v4.6.0`
(This branch should already exist, from the release candidates.)
- `git pull`
@@ -14,6 +13,13 @@ We'll use `v4.6.0` as the intended release version as a running example.
- `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
- `set(LEAN_VERSION_IS_RELEASE 1)`
- (both of these should already be in place from the release candidates)
- It is possible that the `v4.6.0` section of `RELEASES.md` is out of sync between
`releases/v4.6.0` and `master`. This should be reconciled:
- Run `git diff master RELEASES.md`.
- You should expect to see additons on `master` in the `v4.7.0-rc1` section; ignore these.
(i.e. the new release notes for the upcoming release candidate).
- Reconcile discrepancies in the `v4.6.0` section,
usually via copy and paste and a commit to `releases/v4.6.0`.
- `git tag v4.6.0`
- `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
- Now wait, while CI runs.
@@ -24,9 +30,8 @@ We'll use `v4.6.0` as the intended release version as a running example.
you may want to start on the release candidate checklist now.
- Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
- Edit the release notes on Github to select the "Set as the latest release".
- Follow the instructions in creating a release candidate for the "GitHub release notes" step,
now that we have a written `RELEASES.md` section.
Do a quick sanity check.
- Copy and paste the Github release notes from the previous releases candidate for this version
(e.g. `v4.6.0-rc1`), and quickly sanity check.
- Next, we will move a curated list of downstream repos to the latest stable release.
- For each of the repositories listed below:
- Make a PR to `master`/`main` changing the toolchain to `v4.6.0`
@@ -89,10 +94,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`
- 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`
and commit this to `master`.
- Merge the release announcement PR for the Lean website - it will be deployed automatically
- Finally, make an announcement!
This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.6.0`.
@@ -103,6 +104,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
## Optimistic(?) time estimates:
- Initial checks and push the tag: 30 minutes.
- Note that if `RELEASES.md` has discrepancies this could take longer!
- Waiting for the release: 60 minutes.
- Fixing release notes: 10 minutes.
- Bumping toolchains in downstream repositories, up to creating the Mathlib PR: 30 minutes.
@@ -129,26 +131,29 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
git checkout nightly-2024-02-29
git checkout -b releases/v4.7.0
```
- In `RELEASES.md` replace `Development in progress` in the `v4.7.0` section with `Release notes to be written.`
- We will rely on automatically generated release notes for release candidates,
and the written release notes will be used for stable versions only.
It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion.
- In `RELEASES.md` remove `(development in progress)` from the `v4.7.0` section header.
- Our current goal is to have written release notes only about major language features or breaking changes,
and to rely on automatically generated release notes for bugfixes and minor changes.
- Do not wait on `RELEASES.md` being perfect before creating the `release/v4.7.0` branch. It is essential to choose the nightly which will become the release candidate as early as possible, to avoid confusion.
- If there are major changes not reflected in `RELEASES.md` already, you may need to solicit help from the authors.
- Minor changes and bug fixes do not need to be documented in `RELEASES.md`: they will be added automatically on the Github release page.
- Commit your changes to `RELEASES.md`, and push.
- Remember that changes to `RELEASES.md` after you have branched `releases/v4.7.0` should also be cherry-picked back to `master`.
- In `src/CMakeLists.txt`,
- verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.
- `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`).
- Commit your changes to `src/CMakeLists.txt`, and push.
- `git tag v4.7.0-rc1`
- `git push origin v4.7.0-rc1`
- Ping the FRO Zulip that release notes need to be written. The release notes do not block completing the rest of this checklist.
- Now wait, while CI runs.
- You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
- This step can take up to an hour.
- (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/
- Once the release appears at https://github.com/leanprover/lean4/releases/
- Edit the release notes on Github to select the "Set as a pre-release box".
- If release notes have been written already, copy the section of `RELEASES.md` for this version into the Github release notes
and use the title "Changes since v4.6.0 (from RELEASES.md)".
- Otherwise, in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
This will add a list of all the commits since the last stable version.
- Copy the section of `RELEASES.md` for this version into the Github release notes.
- Use the title "Changes since v4.6.0 (from RELEASES.md)"
- Then in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
- This will add a list of all the commits since the last stable version.
- Delete anything already mentioned in the hand-written release notes above.
- Delete "update stage0" commits, and anything with a completely inscrutable commit message.
- Briefly rearrange the remaining items by category (e.g. `simp`, `lake`, `bug fixes`),
@@ -174,9 +179,6 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
- We do this for the same list of repositories as for stable releases, see above.
As above, there are dependencies between these, and so the process above is iterative.
It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
It is essential for Mathlib CI that you then create the next `bump/v4.8.0` branch
for the next development cycle.
Set the `lean-toolchain` file on this branch to same `nightly` you used for this release.
- For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
`nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
(create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
@@ -187,17 +189,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
Please also make sure that whoever is handling social media knows the release is out.
- Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
- Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
- Replaces the "development in progress" in the `v4.7.0` section of `RELEASES.md` with
```
Release candidate, release notes will be copied from `branch releases/v4.7.0` once completed.
```
and inserts the following section before that section:
```
v4.8.0
----------
Development in progress.
```
- Removes all the entries from the `./releases_drafts/` folder.
- Removes `(in development)` from the section heading in `RELEASES.md` for `v4.7.0`,
and creates a new `v4.8.0 (in development)` section heading.
## Time estimates:
Slightly longer than the corresponding steps for a stable release.
@@ -231,18 +224,3 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
* It is always okay to merge in the following directions:
`master` -> `bump/v4.7.0` -> `bump/nightly-2024-02-15` -> `nightly-testing`.
Please remember to push any merges you make to intermediate steps!
# Writing the release notes
We are currently trying a system where release notes are compiled all at once from someone looking through the commit history.
The exact steps are a work in progress.
Here is the general idea:
* The work is done right on the `releases/v4.6.0` branch sometime after it is created but before the stable release is made.
The release notes for `v4.6.0` will be copied to `master`.
* There can be material for release notes entries in commit messages.
* There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
See `./releases_drafts/README.md` for more information.
* The release notes should be written from a downstream expert user's point of view.
This section will be updated when the next release notes are written (for `v4.10.0`).

View File

@@ -35,28 +35,27 @@
lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
devShellWithDist = pkgsDist: pkgs.mkShell.override {
stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
} ({
buildInputs = with pkgs; [
cmake gmp ccache
lean-packages.llvmPackages.llvm # llvm-symbolizer for asan/lsan
gdb
# TODO: only add when proven to not affect the flakification
#pkgs.python3
tree # for CI
];
# https://github.com/NixOS/nixpkgs/issues/60919
hardeningDisable = [ "all" ];
# more convenient `ctest` output
CTEST_OUTPUT_ON_FAILURE = 1;
} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
GMP = pkgsDist.gmp.override { withStatic = true; };
GLIBC = pkgsDist.glibc;
GLIBC_DEV = pkgsDist.glibc.dev;
GCC_LIB = pkgsDist.gcc.cc.lib;
ZLIB = pkgsDist.zlib;
GDB = pkgsDist.gdb;
});
stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
} ({
buildInputs = with pkgs; [
cmake gmp ccache
lean-packages.llvmPackages.llvm # llvm-symbolizer for asan/lsan
# TODO: only add when proven to not affect the flakification
#pkgs.python3
tree # for CI
];
# https://github.com/NixOS/nixpkgs/issues/60919
hardeningDisable = [ "all" ];
# more convenient `ctest` output
CTEST_OUTPUT_ON_FAILURE = 1;
} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
GMP = pkgsDist.gmp.override { withStatic = true; };
GLIBC = pkgsDist.glibc;
GLIBC_DEV = pkgsDist.glibc.dev;
GCC_LIB = pkgsDist.gcc.cc.lib;
ZLIB = pkgsDist.zlib;
GDB = pkgsDist.gdb;
});
in {
packages = lean-packages // rec {
debug = lean-packages.override { debug = true; };

View File

@@ -87,8 +87,7 @@ rec {
leanFlags = [ "-DwarningAsError=true" ];
} // args);
Init' = build { name = "Init"; deps = []; };
Std' = build { name = "Std"; deps = [ Init' ]; };
Lean' = build { name = "Lean"; deps = [ Std' ]; };
Lean' = build { name = "Lean"; deps = [ Init' ]; };
attachSharedLib = sharedLib: pkg: pkg // {
inherit sharedLib;
mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
@@ -96,8 +95,7 @@ rec {
in (all: all // all.lean) rec {
inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
Init = attachSharedLib leanshared Init';
Std = attachSharedLib leanshared Std' // { allExternalDeps = [ Init ]; };
Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init ]; };
Lake = build {
name = "Lake";
src = src + "/src/lake";
@@ -111,24 +109,23 @@ rec {
linkFlags = lib.optional stdenv.isLinux "-rdynamic";
src = src + "/src/lake";
};
stdlib = [ Init Std Lean Lake ];
stdlib = [ Init Lean Lake ];
modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
mkdir $out
touch empty.c
${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
-Wl,--whole-archive -lInit ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
$(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
-o $out/$libName
'';
leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
mkdir $out
LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
${if stdenv.isDarwin
then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Std.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} \
-lm ${stdlibLinkFlags} \
LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
${libInit_shared}/* -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
$(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
-o $out/$libName
'';
@@ -154,9 +151,11 @@ rec {
'';
meta.mainProgram = "lean";
};
cacheRoots = linkFarmFromDrvs "cacheRoots" ([
cacheRoots = linkFarmFromDrvs "cacheRoots" [
stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
] ++ map (lib: lib.oTree) stdlib);
# .o files are not a runtime dependency on macOS because of lack of thin archives
Lean.oTree Lake.oTree
];
test = buildCMake {
name = "lean-test-${desc}";
realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
@@ -179,7 +178,7 @@ rec {
'';
};
update-stage0 =
let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) stdlib; }; in
let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree Lake.cTree ]; }; in
writeShellScriptBin "update-stage0" ''
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
'';

View File

@@ -5,7 +5,7 @@ let lean-final' = lean-final; in
lib.makeOverridable (
{ name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
# Lean dependencies. Each entry should be an output of buildLeanPackage.
deps ? [ lean.Init lean.Std lean.Lean ],
deps ? [ lean.Lean ],
# Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
staticLibDeps ? [],
# Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
@@ -224,8 +224,7 @@ with builtins; let
allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
objects = mapAttrs (_: m: m.obj) mods';
bintools = if stdenv.isDarwin then darwin.cctools else stdenv.cc.bintools.bintools;
staticLib = runCommand "${name}-lib" { buildInputs = [ bintools ]; } ''
staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } ''
mkdir -p $out
ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
'';
@@ -250,7 +249,7 @@ in rec {
${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.libInit_shared}/* ${lean-final.leanshared}/*";
in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
mkdir -p $out/bin
leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \

View File

@@ -9,7 +9,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 11)
set(LEAN_VERSION_MINOR 10)
set(LEAN_VERSION_PATCH 0)
set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -300,11 +300,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH)
string(APPEND LEANSHARED_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
endif()
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lleanrt")
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt")
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lnodefs.js -lleanrt")
else()
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
endif()
set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
@@ -510,15 +510,15 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
# set up libInit_shared only on Windows; see also stdlib.make.in
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
else()
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
endif()
if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@@ -540,7 +540,7 @@ add_custom_target(make_stdlib ALL
# The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
# for a parallelized nested build, but CMake doesn't let us do that.
# We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Lean
VERBATIM)
# if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode

View File

@@ -131,7 +131,7 @@ protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → Exc
end ExceptT
@[always_inline]
instance (m : Type u Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
instance (m : Type u Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
throw e := ExceptT.mk <| throwThe ε₁ e
tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle

View File

@@ -9,7 +9,7 @@ import Init.Meta
open Function
@[simp] theorem monadLift_self {m : Type u Type v} (x : m α) : monadLift x = x :=
@[simp] theorem monadLift_self [Monad m] (x : m α) : monadLift x = x :=
rfl
/--

View File

@@ -14,7 +14,7 @@ open Function
namespace ExceptT
theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
theorem ext [Monad m] {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
simp [run] at h
assumption
@@ -50,7 +50,7 @@ theorem run_bind [Monad m] (x : ExceptT ε m α)
protected theorem seq_eq {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α β)) (x : ExceptT ε m α) : mf <*> x = mf >>= fun f => f <$> x :=
rfl
protected theorem bind_pure_comp [Monad m] (f : α β) (x : ExceptT ε m α) : x >>= pure f = f <$> x := by
protected theorem bind_pure_comp [Monad m] [LawfulMonad m] (f : α β) (x : ExceptT ε m α) : x >>= pure f = f <$> x := by
intros; rfl
protected theorem seqLeft_eq {α β ε : Type u} {m : Type u Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y := by
@@ -188,23 +188,23 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
@[simp] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
@[simp] theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
simp [StateT.lift, StateT.run, bind, StateT.bind]
@[simp] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
@[simp] theorem run_monadMap [MonadFunctor n m] (f : {β : Type u} n β n β) (x : StateT σ m α) (s : σ) :
(monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
@[simp] theorem run_monadMap [Monad m] [MonadFunctor n m] (f : {β : Type u} n β n β) (x : StateT σ m α) (s : σ)
: (monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
@[simp] theorem run_seq {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = (f.run s >>= fun fs => (fun (p : α × σ) => (fs.1 p.1, p.2)) <$> x.run fs.2) := by
show (f >>= fun g => g <$> x).run s = _
simp
@[simp] theorem run_seqRight [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
show (x >>= fun _ => y).run s = _
simp
@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
show (x >>= fun a => y >>= fun _ => pure a).run s = _
simp

View File

@@ -67,7 +67,7 @@ instance : MonadExceptOf Unit (OptionT m) where
throw := fun _ => OptionT.fail
tryCatch := OptionT.tryCatch
instance (ε : Type u) [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
instance (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
throw e := OptionT.mk <| throwThe ε e
tryCatch x handle := OptionT.mk <| tryCatchThe ε x handle

View File

@@ -32,7 +32,7 @@ instance : MonadControl m (ReaderT ρ m) where
restoreM x _ := x
@[always_inline]
instance ReaderT.tryFinally [MonadFinally m] : MonadFinally (ReaderT ρ m) where
instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
@[reducible] def ReaderM (ρ : Type u) := ReaderT ρ Id

View File

@@ -87,7 +87,7 @@ protected def lift {α : Type u} (t : m α) : StateT σ m α :=
instance : MonadLift m (StateT σ m) := StateT.lift
@[always_inline]
instance (σ m) : MonadFunctor m (StateT σ m) := fun f x s => f (x s)
instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) := fun f x s => f (x s)
@[always_inline]
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {

View File

@@ -14,18 +14,16 @@ def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type
namespace StateCpsT
variable {α σ : Type u} {m : Type u Type v}
@[always_inline, inline]
def runK (x : StateCpsT σ m α) (s : σ) (k : α σ m β) : m β :=
def runK {α σ : Type u} {m : Type u Type v} (x : StateCpsT σ m α) (s : σ) (k : α σ m β) : m β :=
x _ s k
@[always_inline, inline]
def run [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
def run {α σ : Type u} {m : Type u Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
runK x s (fun a s => pure (a, s))
@[always_inline, inline]
def run' [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
def run' {α σ : Type u} {m : Type u Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
runK x s (fun a _ => pure a)
@[always_inline]
@@ -50,29 +48,29 @@ protected def lift [Monad m] (x : m α) : StateCpsT σ m α :=
instance [Monad m] : MonadLift m (StateCpsT σ m) where
monadLift := StateCpsT.lift
@[simp] theorem runK_pure (a : α) (s : σ) (k : α σ m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
@[simp] theorem runK_pure {m : Type u Type v} (a : α) (s : σ) (k : α σ m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
@[simp] theorem runK_get (s : σ) (k : σ σ m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
@[simp] theorem runK_get {m : Type u Type v} (s : σ) (k : σ σ m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
@[simp] theorem runK_set (s s' : σ) (k : PUnit σ m β) : (set s' : StateCpsT σ m PUnit).runK s k = k s' := rfl
@[simp] theorem runK_set {m : Type u Type v} (s s' : σ) (k : PUnit σ m β) : (set s' : StateCpsT σ m PUnit).runK s k = k s' := rfl
@[simp] theorem runK_modify (f : σ σ) (s : σ) (k : PUnit σ m β) : (modify f : StateCpsT σ m PUnit).runK s k = k (f s) := rfl
@[simp] theorem runK_modify {m : Type u Type v} (f : σ σ) (s : σ) (k : PUnit σ m β) : (modify f : StateCpsT σ m PUnit).runK s k = k (f s) := rfl
@[simp] theorem runK_lift [Monad m] (x : m α) (s : σ) (k : α σ m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
@[simp] theorem runK_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) (k : α σ m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
@[simp] theorem runK_monadLift [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α σ m β)
@[simp] theorem runK_monadLift {σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α σ m β)
: (monadLift x : StateCpsT σ m α).runK s k = (monadLift x : m α) >>= (k . s) := rfl
@[simp] theorem runK_bind_pure (a : α) (f : α StateCpsT σ m β) (s : σ) (k : β σ m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
@[simp] theorem runK_bind_pure {α σ : Type u} [Monad m] (a : α) (f : α StateCpsT σ m β) (s : σ) (k : β σ m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
@[simp] theorem runK_bind_lift [Monad m] (x : m α) (f : α StateCpsT σ m β) (s : σ) (k : β σ m γ)
@[simp] theorem runK_bind_lift {α σ : Type u} [Monad m] (x : m α) (f : α StateCpsT σ m β) (s : σ) (k : β σ m γ)
: (StateCpsT.lift x >>= f).runK s k = x >>= fun a => (f a).runK s k := rfl
@[simp] theorem runK_bind_get (f : σ StateCpsT σ m β) (s : σ) (k : β σ m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
@[simp] theorem runK_bind_get {σ : Type u} [Monad m] (f : σ StateCpsT σ m β) (s : σ) (k : β σ m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
@[simp] theorem runK_bind_set (f : PUnit StateCpsT σ m β) (s s' : σ) (k : β σ m γ) : (set s' >>= f).runK s k = (f ).runK s' k := rfl
@[simp] theorem runK_bind_set {σ : Type u} [Monad m] (f : PUnit StateCpsT σ m β) (s s' : σ) (k : β σ m γ) : (set s' >>= f).runK s k = (f ).runK s' k := rfl
@[simp] theorem runK_bind_modify (f : σ σ) (g : PUnit StateCpsT σ m β) (s : σ) (k : β σ m γ) : (modify f >>= g).runK s k = (g ).runK (f s) k := rfl
@[simp] theorem runK_bind_modify {σ : Type u} [Monad m] (f : σ σ) (g : PUnit StateCpsT σ m β) (s : σ) (k : β σ m γ) : (modify f >>= g).runK s k = (g ).runK (f s) k := rfl
@[simp] theorem run_eq [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run s = x.runK s (fun a s => pure (a, s)) := rfl

View File

@@ -34,22 +34,22 @@ protected def lift (x : m α) : StateRefT' ω σ m α :=
instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
instance : MonadLift m (StateRefT' ω σ m) := StateRefT'.lift
instance (σ m) : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
@[inline]
protected def get [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
fun ref => ref.get
@[inline]
protected def set [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
protected def set [Monad m] [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
fun ref => ref.set s
@[inline]
protected def modifyGet [MonadLiftT (ST ω) m] (f : σ α × σ) : StateRefT' ω σ m α :=
protected def modifyGet [Monad m] [MonadLiftT (ST ω) m] (f : σ α × σ) : StateRefT' ω σ m α :=
fun ref => ref.modifyGet f
instance [MonadLiftT (ST ω) m] : MonadStateOf σ (StateRefT' ω σ m) where
instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) where
get := StateRefT'.get
set := StateRefT'.set
modifyGet := StateRefT'.modifyGet
@@ -64,5 +64,5 @@ end StateRefT'
instance (ω σ : Type) (m : Type Type) : MonadControl m (StateRefT' ω σ m) :=
inferInstanceAs (MonadControl m (ReaderT _ _))
instance {m : Type Type} {ω σ : Type} [MonadFinally m] : MonadFinally (StateRefT' ω σ m) :=
instance {m : Type Type} {ω σ : Type} [MonadFinally m] [Monad m] : MonadFinally (StateRefT' ω σ m) :=
inferInstanceAs (MonadFinally (ReaderT _ _))

View File

@@ -642,7 +642,7 @@ instance : LawfulBEq String := inferInstance
/-! # Logical connectives and equality -/
@[inherit_doc True.intro] theorem trivial : True :=
@[inherit_doc True.intro] def trivial : True :=
theorem mt {a b : Prop} (h₁ : a b) (h₂ : ¬b) : ¬a :=
fun ha => h₂ (h₁ ha)
@@ -1089,18 +1089,15 @@ def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β
fun a₁ a₂ => r (f a₁) (f a₂)
/--
The transitive closure `TransGen r` of a relation `r` is the smallest relation which is
transitive and contains `r`. `TransGen r a z` if and only if there exists a sequence
The transitive closure `r` of a relation `r` is the smallest relation which is
transitive and contains `r`. `r a z` if and only if there exists a sequence
`a r b r ... r z` of length at least 1 connecting `a` to `z`.
-/
inductive Relation.TransGen {α : Sort u} (r : α α Prop) : α α Prop
/-- If `r a b` then `TransGen r a b`. This is the base case of the transitive closure. -/
| single {a b} : r a b TransGen r a b
inductive TC {α : Sort u} (r : α α Prop) : α α Prop where
/-- If `r a b` then `r a b`. This is the base case of the transitive closure. -/
| base : a b, r a b TC r a b
/-- The transitive closure is transitive. -/
| tail {a b c} : TransGen r a b r b c TransGen r a c
/-- Deprecated synonym for `Relation.TransGen`. -/
@[deprecated Relation.TransGen (since := "2024-07-16")] abbrev TC := @Relation.TransGen
| trans : a b c, TC r a b TC r b c TC r a c
/-! # Subtype -/
@@ -1176,7 +1173,7 @@ def Prod.lexLt [LT α] [LT β] (s : α × β) (t : α × β) : Prop :=
s.1 < t.1 (s.1 = t.1 s.2 < t.2)
instance Prod.lexLtDec
[LT α] [LT β] [DecidableEq α]
[LT α] [LT β] [DecidableEq α] [DecidableEq β]
[(a b : α) Decidable (a < b)] [(a b : β) Decidable (a < b)]
: (s t : α × β) Decidable (Prod.lexLt s t) :=
fun _ _ => inferInstanceAs (Decidable (_ _))
@@ -1194,11 +1191,6 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
(f : α₁ α₂) (g : β₁ β₂) : α₁ × β₁ α₂ × β₂
| (a, b) => (f a, g b)
@[simp] theorem Prod.map_apply (f : α β) (g : γ δ) (x) (y) :
Prod.map f g (x, y) = (f x, g y) := rfl
@[simp] theorem Prod.map_fst (f : α β) (g : γ δ) (x) : (Prod.map f g x).1 = f x.1 := rfl
@[simp] theorem Prod.map_snd (f : α β) (g : γ δ) (x) : (Prod.map f g x).2 = g x.2 := rfl
/-! # Dependent products -/
theorem ex_of_PSigma {α : Type u} {p : α Prop} : (PSigma (fun x => p x)) Exists (fun x => p x)
@@ -1365,9 +1357,6 @@ theorem iff_false_right (ha : ¬a) : (b ↔ a) ↔ ¬b := Iff.comm.trans (iff_fa
theorem of_iff_true (h : a True) : a := h.mpr trivial
theorem iff_true_intro (h : a) : a True := iff_of_true h trivial
theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y True :=
iff_true_intro (Subsingleton.elim ..)
theorem not_of_iff_false : (p False) ¬p := Iff.mp
theorem iff_false_intro (h : ¬a) : a False := iff_of_false h id
@@ -1873,7 +1862,7 @@ instance : Subsingleton (Squash α) where
/--
`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
-/
class Antisymm {α : Sort u} (r : α α Prop) : Prop where
class Antisymm {α : Sort u} (r : α α Prop) where
/-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
antisymm {a b : α} : r a b r b a a = b

View File

@@ -35,4 +35,3 @@ import Init.Data.Queue
import Init.Data.Channel
import Init.Data.Cast
import Init.Data.Sum
import Init.Data.BEq

View File

@@ -10,7 +10,5 @@ import Init.Data.Array.BinSearch
import Init.Data.Array.InsertionSort
import Init.Data.Array.DecidableEq
import Init.Data.Array.Mem
import Init.Data.Array.Attach
import Init.Data.Array.BasicAux
import Init.Data.Array.Lemmas
import Init.Data.Array.TakeDrop

View File

@@ -1,29 +0,0 @@
/-
Copyright (c) 2021 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner, Mario Carneiro
-/
prelude
import Init.Data.Array.Mem
import Init.Data.List.Attach
namespace Array
/--
Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
`Array {x // P x}` is the same as the input `Array α`.
-/
@[inline] private unsafe def attachWithImpl
(xs : Array α) (P : α Prop) (_ : x xs, P x) : Array {x // P x} := unsafeCast xs
/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array
with the same elements but in the type `{x // P x}`. -/
@[implemented_by attachWithImpl] def attachWith
(xs : Array α) (P : α Prop) (H : x xs, P x) : Array {x // P x} :=
xs.data.attachWith P fun x h => H x (Array.Mem.mk h)
/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
with the same elements but in the type `{x // x ∈ xs}`. -/
@[inline] def attach (xs : Array α) : Array {x // x xs} := xs.attachWith _ fun _ => id
end Array

View File

@@ -60,6 +60,8 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
getElem xs i h := xs.uget i h
instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
def back [Inhabited α] (a : Array α) : α :=
a.get! (a.size - 1)

View File

@@ -51,7 +51,7 @@ theorem foldlM_eq_foldlM_data.aux [Monad m]
simp [foldlM_eq_foldlM_data.aux f arr i (j+1) H]
rw (config := {occs := .pos [2]}) [ List.get_drop_eq_drop _ _ _]
rfl
· rw [List.drop_of_length_le (Nat.ge_of_not_lt _)]; rfl
· rw [List.drop_length_le (Nat.ge_of_not_lt _)]; rfl
theorem foldlM_eq_foldlM_data [Monad m]
(f : β α m β) (init : β) (arr : Array α) :
@@ -141,7 +141,7 @@ where
· rw [ List.get_drop_eq_drop _ i _]
simp only [aux (i + 1), map_eq_pure_bind, data_length, List.foldlM_cons, bind_assoc, pure_bind]
rfl
· rw [List.drop_of_length_le (Nat.ge_of_not_lt _)]; rfl
· rw [List.drop_length_le (Nat.ge_of_not_lt _)]; rfl
termination_by arr.size - i
decreasing_by decreasing_trivial_pre_omega
@@ -220,7 +220,7 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
theorem getD_get? (a : Array α) (i : Nat) (d : α) :
Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
if h : i < a.size then
simp [setD, h, getElem?_def]
simp [setD, h, getElem?]
else
have p : i a.size := Nat.le_of_not_gt h
simp [setD, getElem?_len_le _ p, h]
@@ -383,18 +383,18 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
| Or.inl g =>
have h1 : i < a.size + 1 := by omega
have h2 : i a.size := by omega
simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
simp [getElem?, size_push, g, h1, h2, get_push_lt]
| Or.inr (Or.inl heq) =>
simp [heq, getElem?_pos, get_push_eq]
| Or.inr (Or.inr g) =>
simp only [getElem?_def, size_push]
simp only [getElem?, size_push]
have h1 : ¬ (i < a.size) := by omega
have h2 : ¬ (i < a.size + 1) := by omega
have h3 : i a.size := by omega
simp [h1, h2, h3]
@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
simp only [getElem?_def, Nat.lt_irrefl, dite_false]
simp only [getElem?, Nat.lt_irrefl, dite_false]
@[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl

View File

@@ -23,7 +23,7 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
cases as with | _ as =>
exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)
theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
@[simp] theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
cases as with | _ as =>
exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)

View File

@@ -47,6 +47,8 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
getElem xs i h := xs.get i, h
instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
@[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
if h : i < s.size then s.get i, h else v₀

View File

@@ -1,17 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
prelude
import Init.Data.Array.Lemmas
import Init.Data.List.TakeDrop
namespace Array
theorem exists_of_uset (self : Array α) (i d h) :
l₁ l₂, self.data = l₁ ++ self[i] :: l₂ List.length l₁ = i.toNat
(self.uset i d h).data = l₁ ++ d :: l₂ := by
simpa [Array.getElem_eq_data_getElem] using List.exists_of_set _
end Array

View File

@@ -1,60 +0,0 @@
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Markus Himmel
-/
prelude
import Init.Data.Bool
set_option linter.missingDocs true
/-- `PartialEquivBEq α` says that the `BEq` implementation is a
partial equivalence relation, that is:
* it is symmetric: `a == b → b == a`
* it is transitive: `a == b → b == c → a == c`.
-/
class PartialEquivBEq (α) [BEq α] : Prop where
/-- Symmetry for `BEq`. If `a == b` then `b == a`. -/
symm : (a : α) == b b == a
/-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
trans : (a : α) == b b == c a == c
/-- `ReflBEq α` says that the `BEq` implementation is reflexive. -/
class ReflBEq (α) [BEq α] : Prop where
/-- Reflexivity for `BEq`. -/
refl : (a : α) == a
/-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
class EquivBEq (α) [BEq α] extends PartialEquivBEq α, ReflBEq α : Prop
@[simp]
theorem BEq.refl [BEq α] [ReflBEq α] {a : α} : a == a :=
ReflBEq.refl
theorem beq_of_eq [BEq α] [ReflBEq α] {a b : α} : a = b a == b
| rfl => BEq.refl
theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b b == a :=
PartialEquivBEq.symm
theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
Bool.eq_iff_iff.2 BEq.symm, BEq.symm
theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false (b == a) = false :=
BEq.comm (α := α) id
theorem BEq.trans [BEq α] [PartialEquivBEq α] {a b c : α} : a == b b == c a == c :=
PartialEquivBEq.trans
theorem BEq.neq_of_neq_of_beq [BEq α] [PartialEquivBEq α] {a b c : α} :
(a == b) = false b == c (a == c) = false :=
fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₁ (BEq.trans h₃ (BEq.symm h₂))
theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
a == b (b == c) = false (a == c) = false :=
fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₂ (BEq.trans (BEq.symm h₁) h₃)
instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
refl := LawfulBEq.rfl
symm h := (beq_iff_eq _ _).2 <| Eq.symm <| (beq_iff_eq _ _).1 h
trans hab hbc := (beq_iff_eq _ _).2 <| ((beq_iff_eq _ _).1 hab).trans <| (beq_iff_eq _ _).1 hbc

View File

@@ -614,13 +614,6 @@ theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..) :=
rfl
/--
`twoPow w i` is the bitvector `2^i` if `i < w`, and `0` otherwise.
That is, 2 to the power `i`.
For the bitwise point of view, it has the `i`th bit as `1` and all other bits as `0`.
-/
def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w <<< i
end bitwise
section normalization_eqs

View File

@@ -159,21 +159,6 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
rw [ add_not_self x, BitVec.add_comm, add_sub_cancel]
/-- Addition of bitvectors is the same as bitwise or, if bitwise and is zero. -/
theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
(h : x &&& y = 0#w) : x + y = x ||| y := by
rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (x ||| y)]
· rfl
· simp only [adcb, atLeastTwo, Bool.and_false, Bool.or_false, bne_false, getLsb_or,
Prod.mk.injEq, and_eq_false_imp]
intros i
replace h : (x &&& y).getLsb i = (0#w).getLsb i := by rw [h]
simp only [getLsb_and, getLsb_zero, and_eq_false_imp] at h
constructor
· intros hx
simp_all [hx]
· by_cases hx : x.getLsb i <;> simp_all [hx]
/-! ### Negation -/
theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
@@ -250,80 +235,4 @@ theorem sle_eq_carry (x y : BitVec w) :
x.sle y = !((x.msb == y.msb).xor (carry w y (~~~x) true)) := by
rw [sle_eq_not_slt, slt_eq_not_carry, beq_comm]
/-! ### mul recurrence for bitblasting -/
/--
A recurrence that describes multiplication as repeated addition.
Is useful for bitblasting multiplication.
-/
def mulRec (l r : BitVec w) (s : Nat) : BitVec w :=
let cur := if r.getLsb s then (l <<< s) else 0
match s with
| 0 => cur
| s + 1 => mulRec l r s + cur
theorem mulRec_zero_eq (l r : BitVec w) :
mulRec l r 0 = if r.getLsb 0 then l else 0 := by
simp [mulRec]
theorem mulRec_succ_eq (l r : BitVec w) (s : Nat) :
mulRec l r (s + 1) = mulRec l r s + if r.getLsb (s + 1) then (l <<< (s + 1)) else 0 := rfl
/--
Recurrence lemma: truncating to `i+1` bits and then zero extending to `w`
equals truncating upto `i` bits `[0..i-1]`, and then adding the `i`th bit of `x`.
-/
theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w) (i : Nat) :
zeroExtend w (x.truncate (i + 1)) =
zeroExtend w (x.truncate i) + (x &&& twoPow w i) := by
rw [add_eq_or_of_and_eq_zero]
· ext k
simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
by_cases hik : i = k
· subst hik
simp
· simp only [getLsb_twoPow, hik, decide_False, Bool.and_false, Bool.or_false]
by_cases hik' : k < (i + 1)
· have hik'' : k < i := by omega
simp [hik', hik'']
· have hik'' : ¬ (k < i) := by omega
simp [hik', hik'']
· ext k
simp
omega
/--
Recurrence lemma: multiplying `l` with the first `s` bits of `r` is the
same as truncating `r` to `s` bits, then zero extending to the original length,
and performing the multplication. -/
theorem mulRec_eq_mul_signExtend_truncate (l r : BitVec w) (s : Nat) :
mulRec l r s = l * ((r.truncate (s + 1)).zeroExtend w) := by
induction s
case zero =>
simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
by_cases r.getLsb 0
case pos hr =>
simp only [hr, reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero,
hr, ofBool_true, ofNat_eq_ofNat]
rw [zeroExtend_ofNat_one_eq_ofNat_one_of_lt (by omega)]
simp
case neg hr =>
simp [hr, zeroExtend_one_eq_ofBool_getLsb_zero]
case succ s' hs =>
rw [mulRec_succ_eq, hs]
have heq :
(if r.getLsb (s' + 1) = true then l <<< (s' + 1) else 0) =
(l * (r &&& (BitVec.twoPow w (s' + 1)))) := by
simp only [ofNat_eq_ofNat, and_twoPow_eq]
by_cases hr : r.getLsb (s' + 1) <;> simp [hr]
rw [heq, BitVec.mul_add, zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow]
theorem getLsb_mul (x y : BitVec w) (i : Nat) :
(x * y).getLsb i = (mulRec x y w).getLsb i := by
simp only [mulRec_eq_mul_signExtend_truncate]
rw [truncate, truncate_eq_zeroExtend, truncate_eq_zeroExtend,
truncate_truncate_of_le]
· simp
· omega
end BitVec

View File

@@ -110,8 +110,8 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
@[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp
theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp
@[simp] theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp [of_length_zero]
@[simp] theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp [of_length_zero]
@[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
theorem eq_of_toFin_eq : {x y : BitVec w}, x.toFin = y.toFin x = y
@@ -163,13 +163,6 @@ theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m n) : x < 2 ^ n :=
Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
@[simp]
theorem getLsb_ofBool (b : Bool) (i : Nat) : (BitVec.ofBool b).getLsb i = ((i = 0) && b) := by
rcases b with rfl | rfl
· simp [ofBool]
· simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsb_ofNat, Bool.and_true]
by_cases hi : i = 0 <;> simp [hi] <;> omega
/-! ### msb -/
@[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsb]
@@ -191,7 +184,8 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
· simp only [h]
rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
· decide
· omega
· have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
omega
@[bv_toNat] theorem getLsb_succ_last (x : BitVec (w + 1)) :
x.getLsb w = decide (2 ^ w x.toNat) := getLsb_last x
@@ -293,9 +287,6 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
/-! ### zeroExtend and truncate -/
theorem truncate_eq_zeroExtend {v : Nat} {x : BitVec w} :
truncate v x = zeroExtend v x := rfl
@[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m n) (x : BitVec m) :
(zeroExtend' p x).toNat = x.toNat := by
unfold zeroExtend'
@@ -329,7 +320,7 @@ theorem zeroExtend'_eq {x : BitVec w} (h : w ≤ v) : x.zeroExtend' h = x.zeroEx
apply eq_of_toNat_eq
simp [toNat_zeroExtend]
theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
@[simp] theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = truncate m x := by
apply eq_of_toNat_eq
@@ -340,7 +331,10 @@ theorem toNat_eq_nat (x : BitVec w) (y : Nat)
: (x.toNat = y) (y < 2^w (x = BitVec.ofNat w y)) := by
apply Iff.intro
· intro eq
simp [eq, x.isLt]
simp at eq
have lt := x.isLt
simp [eq] at lt
simp [eq, lt, x.isLt]
· intro eq
simp [Nat.mod_eq_of_lt, eq]
@@ -383,7 +377,7 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
all_goals (first | apply getLsb_ge | apply Eq.symm; apply getLsb_ge)
<;> omega
theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
@[simp] theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
getLsb (truncate m x) i = (decide (i < m) && getLsb x i) :=
getLsb_zeroExtend m x i
@@ -402,12 +396,6 @@ theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsb k := b
(x.truncate l).truncate k = x.truncate k :=
zeroExtend_zeroExtend_of_le x h
/--Truncating by the bitwidth has no effect. -/
@[simp]
theorem truncate_eq_self {x : BitVec w} : x.truncate w = x := by
ext i
simp [getLsb_zeroExtend]
@[simp] theorem truncate_cast {h : w = v} : (cast h x).truncate k = x.truncate k := by
apply eq_of_getLsb_eq
simp
@@ -420,22 +408,6 @@ theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) &
theorem msb_zeroExtend' (x : BitVec w) (h : w v) : (x.zeroExtend' h).msb = (decide (0 < v) && x.getLsb (v - 1)) := by
rw [zeroExtend'_eq, msb_zeroExtend]
/-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
theorem zeroExtend_one_eq_ofBool_getLsb_zero (x : BitVec w) :
x.zeroExtend 1 = BitVec.ofBool (x.getLsb 0) := by
ext i
simp [getLsb_zeroExtend, Fin.fin_one_eq_zero i]
/-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/
theorem zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
(BitVec.ofNat v 1).zeroExtend w = BitVec.ofNat w 1 := by
ext i, hilt
simp only [getLsb_zeroExtend, hilt, decide_True, getLsb_ofNat, Bool.true_and,
Bool.and_iff_right_iff_imp, decide_eq_true_eq]
intros hi₁
have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
omega
/-! ## extractLsb -/
@[simp]
@@ -608,7 +580,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
ext
simp_all [lt_of_getLsb]
@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x ^^^ cast h y = cast h (x ^^^ y) := by
@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
ext
simp_all [lt_of_getLsb]
@@ -621,11 +593,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
BitVec.toFin (x <<< n) = Fin.ofNat' (x.toNat <<< n) (Nat.two_pow_pos w) := rfl
@[simp]
theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
apply eq_of_toNat_eq
simp
@[simp] theorem getLsb_shiftLeft (x : BitVec m) (n) :
getLsb (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsb x (i - n)) := by
rw [ testBit_toNat, getLsb]
@@ -1080,16 +1047,8 @@ theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
@[simp] theorem toNat_sub {n} (x y : BitVec n) :
(x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
-- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
-- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
-- results in `omega` generating proof terms that are very slow in the kernel.
@[bv_toNat] theorem toNat_sub' {n} (x y : BitVec n) :
(x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := by
rw [toNat_sub, Nat.add_comm]
@[simp, bv_toNat] theorem toNat_sub {n} (x y : BitVec n) :
(x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
@[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
@[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
@@ -1181,18 +1140,6 @@ instance : Std.Associative (fun (x y : BitVec w) => x * y) := ⟨BitVec.mul_asso
instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
right_id := BitVec.mul_one
@[simp]
theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by
apply eq_of_toNat_eq
simp [toNat_mul]
theorem BitVec.mul_add {x y z : BitVec w} :
x * (y + z) = x * y + x * z := by
apply eq_of_toNat_eq
simp only [toNat_mul, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod]
rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
Nat.mul_mod, Nat.mul_add]
@[simp, bv_toNat] theorem toInt_mul (x y : BitVec w) :
(x * y).toInt = (x.toInt * y.toInt).bmod (2^w) := by
simp [toInt_eq_toNat_bmod]
@@ -1293,7 +1240,11 @@ x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
theorem getLsb_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
(x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i) := by
rw [rotateLeftAux, getLsb_or, getLsb_ushiftRight]
simp; omega
suffices (x <<< r).getLsb i = false by
simp; omega
simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
omega
/--
Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to
@@ -1424,84 +1375,4 @@ theorem getLsb_rotateRight {x : BitVec w} {r i : Nat} :
· simp
· rw [ rotateRight_mod_eq_rotateRight, getLsb_rotateRight_of_le (Nat.mod_lt _ (by omega))]
/- ## twoPow -/
@[simp, bv_toNat]
theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
rcases w with rfl | w
· simp [Nat.mod_one]
· simp only [twoPow, toNat_shiftLeft, toNat_ofNat]
have h1 : 1 < 2 ^ (w + 1) := Nat.one_lt_two_pow (by omega)
rw [Nat.mod_eq_of_lt h1, Nat.shiftLeft_eq, Nat.one_mul]
@[simp]
theorem getLsb_twoPow (i j : Nat) : (twoPow w i).getLsb j = ((i < w) && (i = j)) := by
rcases w with rfl | w
· simp
· simp only [twoPow, getLsb_shiftLeft, getLsb_ofNat]
by_cases hj : j < i
· simp only [hj, decide_True, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,
Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not]
omega
· by_cases hi : Nat.testBit 1 (j - i)
· obtain hi' := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi
have hij : j = i := by omega
simp_all
· have hij : i j := by
intro h; subst h
simp at hi
simp_all
theorem and_twoPow_eq (x : BitVec w) (i : Nat) :
x &&& (twoPow w i) = if x.getLsb i then twoPow w i else 0#w := by
ext j
simp only [getLsb_and, getLsb_twoPow]
by_cases hj : i = j <;> by_cases hx : x.getLsb i <;> simp_all
@[simp]
theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
x * (twoPow w i) = x <<< i := by
apply eq_of_toNat_eq
simp only [toNat_mul, toNat_twoPow, toNat_shiftLeft, Nat.shiftLeft_eq]
by_cases hi : i < w
· have hpow : 2^i < 2^w := Nat.pow_lt_pow_of_lt (by omega) (by omega)
rw [Nat.mod_eq_of_lt hpow]
· have hpow : 2 ^ i % 2 ^ w = 0 := by
rw [Nat.mod_eq_zero_of_dvd]
apply Nat.pow_dvd_pow 2 (by omega)
simp [Nat.mul_mod, hpow]
/- ### zeroExtend, truncate, and bitwise operations -/
/--
When the `(i+1)`th bit of `x` is false,
keeping the lower `(i + 1)` bits of `x` equals keeping the lower `i` bits.
-/
theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false
{x : BitVec w} {i : Nat} (hx : x.getLsb i = false) :
zeroExtend w (x.truncate (i + 1)) =
zeroExtend w (x.truncate i) := by
ext k
simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
by_cases hik : i = k
· subst hik
simp [hx]
· by_cases hik' : k < i + 1 <;> simp [hik'] <;> omega
/--
When the `(i+1)`th bit of `x` is true,
keeping the lower `(i + 1)` bits of `x` equalsk eeping the lower `i` bits
and then performing bitwise-or with `twoPow i = (1 << i)`,
-/
theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true
{x : BitVec w} {i : Nat} (hx : x.getLsb i = true) :
zeroExtend w (x.truncate (i + 1)) =
zeroExtend w (x.truncate i) ||| (twoPow w i) := by
ext k
simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
by_cases hik : i = k
· subst hik
simp [hx]
· by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
end BitVec

View File

@@ -52,8 +52,8 @@ theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
@[simp] theorem decide_eq_true {b : Bool} [Decidable (b = true)] : decide (b = true) = b := by cases b <;> simp
@[simp] theorem decide_eq_false {b : Bool} [Decidable (b = false)] : decide (b = false) = !b := by cases b <;> simp
theorem decide_true_eq {b : Bool} [Decidable (true = b)] : decide (true = b) = b := by cases b <;> simp
theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp
@[simp] theorem decide_true_eq {b : Bool} [Decidable (true = b)] : decide (true = b) = b := by cases b <;> simp
@[simp] theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp
/-! ### and -/
@@ -163,7 +163,7 @@ Consider the term: `¬((b && c) = true)`:
-/
@[simp] theorem and_eq_false_imp : (x y : Bool), (x && y) = false (x = true y = false) := by decide
theorem or_eq_true_iff : (x y : Bool), (x || y) = true x = true y = true := by simp
@[simp] theorem or_eq_true_iff : (x y : Bool), (x || y) = true x = true y = true := by decide
@[simp] theorem or_eq_false_iff : (x y : Bool), (x || y) = false x = false y = false := by decide
@@ -187,9 +187,11 @@ in false_eq and true_eq.
@[simp] theorem true_beq : b, (true == b) = b := by decide
@[simp] theorem false_beq : b, (false == b) = !b := by decide
@[simp] theorem beq_true : b, (b == true) = b := by decide
instance : Std.LawfulIdentity (· == ·) true where
left_id := true_beq
right_id := beq_true
@[simp] theorem beq_false : b, (b == false) = !b := by decide
@[simp] theorem true_bne : (b : Bool), (true != b) = !b := by decide
@[simp] theorem false_bne : (b : Bool), (false != b) = b := by decide
@@ -351,7 +353,7 @@ theorem and_or_inj_left_iff :
/-! ## toNat -/
/-- convert a `Bool` to a `Nat`, `false -> 0`, `true -> 1` -/
def toNat (b : Bool) : Nat := cond b 1 0
def toNat (b:Bool) : Nat := cond b 1 0
@[simp] theorem toNat_false : false.toNat = 0 := rfl
@@ -494,16 +496,6 @@ protected theorem cond_false {α : Type u} {a b : α} : cond false a b = b := co
@[simp] theorem cond_true_same : (c b : Bool), cond c c b = (c || b) := by decide
@[simp] theorem cond_false_same : (c b : Bool), cond c b c = (c && b) := by decide
theorem cond_pos {b : Bool} {a a' : α} (h : b = true) : (bif b then a else a') = a := by
rw [h, cond_true]
theorem cond_neg {b : Bool} {a a' : α} (h : b = false) : (bif b then a else a') = a' := by
rw [h, cond_false]
theorem apply_cond (f : α β) {b : Bool} {a a' : α} :
f (bif b then a else a') = bif b then f a else f a' := by
cases b <;> simp
/-# decidability -/
protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b := decide_eq_true

View File

@@ -52,9 +52,13 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
getElem xs i h := xs.get i, h
instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
getElem xs i h := xs.uget i h
instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
@[extern "lean_byte_array_set"]
def set! : ByteArray (@& Nat) UInt8 ByteArray
| bs, i, b => bs.set! i b
@@ -92,24 +96,20 @@ protected def append (a : ByteArray) (b : ByteArray) : ByteArray :=
instance : Append ByteArray := ByteArray.append
def toList (bs : ByteArray) : List UInt8 :=
partial def toList (bs : ByteArray) : List UInt8 :=
let rec loop (i : Nat) (r : List UInt8) :=
if i < bs.size then
loop (i+1) (bs.get! i :: r)
else
r.reverse
termination_by bs.size - i
decreasing_by decreasing_trivial_pre_omega
loop 0 []
@[inline] def findIdx? (a : ByteArray) (p : UInt8 Bool) (start := 0) : Option Nat :=
@[inline] partial def findIdx? (a : ByteArray) (p : UInt8 Bool) (start := 0) : Option Nat :=
let rec @[specialize] loop (i : Nat) :=
if i < a.size then
if p (a.get! i) then some i else loop (i+1)
else
none
termination_by a.size - i
decreasing_by decreasing_trivial_pre_omega
loop start
/--

View File

@@ -31,9 +31,11 @@ theorem utf8Size_eq (c : Char) : c.utf8Size = 1 c.utf8Size = 2 c.utf8Siz
rw [Char.ofNat, dif_pos]
rfl
@[ext] protected theorem ext : {a b : Char} a.val = b.val a = b
@[ext] theorem Char.ext : {a b : Char} a.val = b.val a = b
| _,_, _,_, rfl => rfl
theorem Char.ext_iff {x y : Char} : x = y x.val = y.val := congrArg _, Char.ext
end Char
@[deprecated Char.utf8Size (since := "2024-06-04")] abbrev String.csize := Char.utf8Size

View File

@@ -1,15 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
prelude
import Init.Data.Nat.Bitwise
import Init.Data.Fin.Basic
namespace Fin
@[simp] theorem and_val (a b : Fin n) : (a &&& b).val = a.val &&& b.val :=
Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt Nat.and_le_left a.isLt)
end Fin

View File

@@ -37,7 +37,9 @@ theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
@[simp] protected theorem eta (a : Fin n) (h : a < n) : (a, h : Fin n) = a := rfl
@[ext] protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
@[ext] theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
theorem ext_iff {a b : Fin n} : a = b a.1 = b.1 := val_inj.symm
theorem val_ne_iff {a b : Fin n} : a.1 b.1 a b := not_congr val_inj
@@ -45,12 +47,12 @@ theorem forall_iff {p : Fin n → Prop} : (∀ i, p i) ↔ ∀ i h, p ⟨i, h⟩
fun h i hi => h i, hi, fun h i, hi => h i hi
protected theorem mk.inj_iff {n a b : Nat} {ha : a < n} {hb : b < n} :
(a, ha : Fin n) = b, hb a = b := Fin.ext_iff
(a, ha : Fin n) = b, hb a = b := ext_iff
theorem val_mk {m n : Nat} (h : m < n) : (m, h : Fin n).val = m := rfl
theorem eq_mk_iff_val_eq {a : Fin n} {k : Nat} {hk : k < n} :
a = k, hk (a : Nat) = k := Fin.ext_iff
a = k, hk (a : Nat) = k := ext_iff
theorem mk_val (i : Fin n) : (i, i.isLt : Fin n) = i := Fin.eta ..
@@ -143,7 +145,7 @@ theorem eq_succ_of_ne_zero {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) : ∃ j :
@[simp] theorem val_rev (i : Fin n) : rev i = n - (i + 1) := rfl
@[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := Fin.ext <| by
@[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := ext <| by
rw [val_rev, val_rev, Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
@[simp] theorem rev_le_rev {i j : Fin n} : rev i rev j j i := by
@@ -169,12 +171,12 @@ theorem le_last (i : Fin (n + 1)) : i ≤ last n := Nat.le_of_lt_succ i.is_lt
theorem last_pos : (0 : Fin (n + 2)) < last (n + 1) := Nat.succ_pos _
theorem eq_last_of_not_lt {i : Fin (n + 1)} (h : ¬(i : Nat) < n) : i = last n :=
Fin.ext <| Nat.le_antisymm (le_last i) (Nat.not_lt.1 h)
ext <| Nat.le_antisymm (le_last i) (Nat.not_lt.1 h)
theorem val_lt_last {i : Fin (n + 1)} : i last n (i : Nat) < n :=
Decidable.not_imp_comm.1 eq_last_of_not_lt
@[simp] theorem rev_last (n : Nat) : rev (last n) = 0 := Fin.ext <| by simp
@[simp] theorem rev_last (n : Nat) : rev (last n) = 0 := ext <| by simp
@[simp] theorem rev_zero (n : Nat) : rev 0 = last n := by
rw [ rev_rev (last _), rev_last]
@@ -242,11 +244,11 @@ theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt one_pos
@[simp] theorem succ_lt_succ_iff {a b : Fin n} : a.succ < b.succ a < b := Nat.succ_lt_succ_iff
@[simp] theorem succ_inj {a b : Fin n} : a.succ = b.succ a = b := by
refine fun h => Fin.ext ?_, congrArg _
refine fun h => ext ?_, congrArg _
apply Nat.le_antisymm <;> exact succ_le_succ_iff.1 (h Nat.le_refl _)
theorem succ_ne_zero {n} : k : Fin n, Fin.succ k 0
| k, _, heq => Nat.succ_ne_zero k <| congrArg Fin.val heq
| k, _, heq => Nat.succ_ne_zero k <| ext_iff.1 heq
@[simp] theorem succ_zero_eq_one : Fin.succ (0 : Fin (n + 1)) = 1 := rfl
@@ -265,7 +267,7 @@ theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
rw [ succ_zero_eq_one, succ_lt_succ_iff]; exact succ_pos a
@[simp] theorem add_one_lt_iff {n : Nat} {k : Fin (n + 2)} : k + 1 < k k = last _ := by
simp only [lt_def, val_add, val_last, Fin.ext_iff]
simp only [lt_def, val_add, val_last, ext_iff]
let k, hk := k
match Nat.eq_or_lt_of_le (Nat.le_of_lt_succ hk) with
| .inl h => cases h; simp [Nat.succ_pos]
@@ -283,7 +285,7 @@ theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
split <;> simp [*, (Nat.succ_ne_zero _).symm, Nat.ne_of_gt (Nat.lt_succ_self _)]
@[simp] theorem last_le_iff {n : Nat} {k : Fin (n + 1)} : last n k k = last n := by
rw [Fin.ext_iff, Nat.le_antisymm_iff, le_def, and_iff_right (by apply le_last)]
rw [ext_iff, Nat.le_antisymm_iff, le_def, and_iff_right (by apply le_last)]
@[simp] theorem lt_add_one_iff {n : Nat} {k : Fin (n + 1)} : k < k + 1 k < last n := by
rw [ Decidable.not_iff_not]; simp
@@ -304,10 +306,10 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
@[simp] theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n m) :
castLE h i, hn = i, Nat.lt_of_lt_of_le hn h := rfl
@[simp] theorem castLE_zero {n m : Nat} (h : n.succ m.succ) : castLE h 0 = 0 := by simp [Fin.ext_iff]
@[simp] theorem castLE_zero {n m : Nat} (h : n.succ m.succ) : castLE h 0 = 0 := by simp [ext_iff]
@[simp] theorem castLE_succ {m n : Nat} (h : m + 1 n + 1) (i : Fin m) :
castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by simp [Fin.ext_iff]
castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by simp [ext_iff]
@[simp] theorem castLE_castLE {k m n} (km : k m) (mn : m n) (i : Fin k) :
Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i :=
@@ -320,7 +322,7 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
@[simp] theorem coe_cast (h : n = m) (i : Fin n) : (cast h i : Nat) = i := rfl
@[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : cast h (last n) = last n' :=
Fin.ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
@[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : cast h i, hn = i, h hn := rfl
@@ -346,7 +348,7 @@ theorem castAdd_lt {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m :=
/-- For rewriting in the reverse direction, see `Fin.cast_castAdd_left`. -/
theorem castAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := Fin.ext rfl
castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := ext rfl
theorem cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
cast h (castAdd m i) = castAdd m (cast (Nat.add_right_cancel h) i) := rfl
@@ -395,7 +397,7 @@ theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
@[simp] theorem castSucc_lt_castSucc_iff {a b : Fin n} :
Fin.castSucc a < Fin.castSucc b a < b := .rfl
theorem castSucc_inj {a b : Fin n} : castSucc a = castSucc b a = b := by simp [Fin.ext_iff]
theorem castSucc_inj {a b : Fin n} : castSucc a = castSucc b a = b := by simp [ext_iff]
theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt
@@ -407,7 +409,7 @@ theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt
theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < castSucc i := by
simpa [lt_def] using h
@[simp] theorem castSucc_eq_zero_iff (a : Fin (n + 1)) : castSucc a = 0 a = 0 := by simp [Fin.ext_iff]
@[simp] theorem castSucc_eq_zero_iff (a : Fin (n + 1)) : castSucc a = 0 a = 0 := by simp [ext_iff]
theorem castSucc_ne_zero_iff (a : Fin (n + 1)) : castSucc a 0 a 0 :=
not_congr <| castSucc_eq_zero_iff a
@@ -419,7 +421,7 @@ theorem castSucc_fin_succ (n : Nat) (j : Fin n) :
theorem coeSucc_eq_succ {a : Fin n} : castSucc a + 1 = a.succ := by
cases n
· exact a.elim0
· simp [Fin.ext_iff, add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ a.is_lt)]
· simp [ext_iff, add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ a.is_lt)]
theorem lt_succ {a : Fin n} : castSucc a < a.succ := by
rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
@@ -452,7 +454,7 @@ theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
@[simp] theorem cast_addNat_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
cast h (addNat i m') = addNat i m :=
Fin.ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
@[simp] theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
@@ -472,7 +474,7 @@ theorem cast_natAdd_right {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
@[simp] theorem cast_natAdd_left {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
cast h (natAdd m' i) = natAdd m i :=
Fin.ext <| (congrArg (· + (i : Nat)) (Nat.add_right_cancel h) : _)
ext <| (congrArg (· + (i : Nat)) (Nat.add_right_cancel h) : _)
theorem castAdd_natAdd (p m : Nat) {n : Nat} (i : Fin n) :
castAdd p (natAdd m i) = cast (Nat.add_assoc ..).symm (natAdd m (castAdd p i)) := rfl
@@ -482,27 +484,27 @@ theorem natAdd_castAdd (p m : Nat) {n : Nat} (i : Fin n) :
theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
natAdd m (natAdd n i) = cast (Nat.add_assoc ..) (natAdd (m + n) i) :=
Fin.ext <| (Nat.add_assoc ..).symm
ext <| (Nat.add_assoc ..).symm
@[simp]
theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
cast h (natAdd 0 i) = cast ((Nat.zero_add _).symm.trans h) i :=
Fin.ext <| Nat.zero_add _
ext <| Nat.zero_add _
@[simp]
theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :
cast (Nat.add_comm ..) (natAdd n i) = addNat i n := Fin.ext <| Nat.add_comm ..
cast (Nat.add_comm ..) (natAdd n i) = addNat i n := ext <| Nat.add_comm ..
@[simp]
theorem cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
cast (Nat.add_comm ..) (addNat i m) = natAdd m i := Fin.ext <| Nat.add_comm ..
cast (Nat.add_comm ..) (addNat i m) = natAdd m i := ext <| Nat.add_comm ..
@[simp] theorem natAdd_last {m n : Nat} : natAdd n (last m) = last (n + m) := rfl
theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) :=
rfl
theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := Fin.ext <| by
theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := ext <| by
rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by
@@ -532,7 +534,7 @@ theorem pred_eq_iff_eq_succ {n : Nat} (i : Fin (n + 1)) (hi : i ≠ 0) (j : Fin
theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
Fin.pred i + 1, Nat.add_lt_add_right h 1 (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
i, h := by
simp only [Fin.ext_iff, coe_pred, Nat.add_sub_cancel]
simp only [ext_iff, coe_pred, Nat.add_sub_cancel]
@[simp] theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
Fin.pred i + 1, h₁ h₂ = i, Nat.lt_of_succ_lt_succ h₁ := pred_mk_succ i _
@@ -552,14 +554,14 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
{a b : Fin (n + 1)} {ha : a 0} {hb : b 0}, a.pred ha = b.pred hb a = b
| 0, _, _, ha, _ => by simp only [mk_zero, ne_eq, not_true] at ha
| i + 1, _, 0, _, _, hb => by simp only [mk_zero, ne_eq, not_true] at hb
| i + 1, hi, j + 1, hj, ha, hb => by simp [Fin.ext_iff, Nat.succ.injEq]
| i + 1, hi, j + 1, hj, ha, hb => by simp [ext_iff, Nat.succ.injEq]
@[simp] theorem pred_one {n : Nat} :
Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := rfl
theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by
rw [Fin.ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
rw [ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
exact Nat.add_lt_add_right h 1
@[simp] theorem coe_subNat (i : Fin (n + m)) (h : m i) : (i.subNat m h : Nat) = i - m := rfl
@@ -571,10 +573,10 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := rfl
@[simp] theorem addNat_subNat {i : Fin (n + m)} (h : m i) : addNat (subNat m i h) m = i :=
Fin.ext <| Nat.sub_add_cancel h
ext <| Nat.sub_add_cancel h
@[simp] theorem subNat_addNat (i : Fin n) (m : Nat) (h : m addNat i m := le_coe_addNat m i) :
subNat m (addNat i m) h = i := Fin.ext <| Nat.add_sub_cancel i m
subNat m (addNat i m) h = i := ext <| Nat.add_sub_cancel i m
@[simp] theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n i) :
natAdd n (subNat n (cast (Nat.add_comm ..) i) h) = i := by simp [ cast_addNat]; rfl
@@ -784,9 +786,6 @@ theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a :=
rw [Nat.mod_eq_of_lt]
all_goals omega
theorem sub_val_of_le {a b : Fin n} : b a (a - b).val = a.val - b.val :=
coe_sub_iff_le.2
theorem coe_sub_iff_lt {a b : Fin n} : ((a - b) : Nat) = n + a - b a < b := by
rw [sub_def, lt_def]
dsimp only
@@ -808,10 +807,10 @@ theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
match n with
| 0 => exact Subsingleton.elim (α := Fin 1) ..
| n+1 => simp [Fin.ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
| n+1 => simp [ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
Fin.ext <| by rw [mul_def, mul_def, Nat.mul_comm]
ext <| by rw [mul_def, mul_def, Nat.mul_comm]
instance : Std.Commutative (α := Fin n) (· * ·) := Fin.mul_comm
protected theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by
@@ -827,9 +826,9 @@ instance : Std.LawfulIdentity (α := Fin (n + 1)) (· * ·) 1 where
left_id := Fin.one_mul
right_id := Fin.mul_one
protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [Fin.ext_iff, mul_def]
protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [ext_iff, mul_def]
protected theorem zero_mul (k : Fin (n + 1)) : (0 : Fin (n + 1)) * k = 0 := by
simp [Fin.ext_iff, mul_def]
simp [ext_iff, mul_def]
end Fin

View File

@@ -101,13 +101,13 @@ Returns an undefined value if `x` is not finite.
instance : ToString Float where
toString := Float.toString
@[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
instance : Repr Float where
reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
reprPrec n _ := Float.toString n
instance : ReprAtom Float :=
@[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
@[extern "sin"] opaque Float.sin : Float Float
@[extern "cos"] opaque Float.cos : Float Float
@[extern "tan"] opaque Float.tan : Float Float

View File

@@ -58,9 +58,13 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
getElem xs i h := xs.get i, h
instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
getElem xs i h := xs.uget i h
instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
@[extern "lean_float_array_uset"]
def uset : (a : FloatArray) (i : USize) Float i.toNat < a.size FloatArray
| ds, i, v, h => ds.uset i v h

View File

@@ -62,16 +62,3 @@ instance (P : Prop) : Hashable P where
/-- An opaque (low-level) hash operation used to implement hashing for pointers. -/
@[always_inline, inline] def hash64 (u : UInt64) : UInt64 :=
mixHash u 11
/-- `LawfulHashable α` says that the `BEq α` and `Hashable α` instances on `α` are compatible, i.e.,
that `a == b` implies `hash a = hash b`. This is automatic if the `BEq` instance is lawful.
-/
class LawfulHashable (α : Type u) [BEq α] [Hashable α] where
/-- If `a == b`, then `hash a = hash b`. -/
hash_eq (a b : α) : a == b hash a = hash b
theorem hash_eq [BEq α] [Hashable α] [LawfulHashable α] {a b : α} : a == b hash a = hash b :=
LawfulHashable.hash_eq a b
instance (priority := low) [BEq α] [Hashable α] [LawfulBEq α] : LawfulHashable α where
hash_eq _ _ h := eq_of_beq h rfl

View File

@@ -636,7 +636,7 @@ theorem sub_ediv_of_dvd (a : Int) {b c : Int}
have := Int.mul_ediv_cancel 1 H; rwa [Int.one_mul] at this
@[simp]
theorem emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
theorem Int.emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
by_cases h : y = 0
· simp [h]
· simp only [Int.emod_def, Int.sub_ediv_of_dvd, Int.dvd_refl, Int.ediv_self h, Int.mul_sub]

View File

@@ -127,14 +127,9 @@ protected theorem lt_iff_le_not_le {a b : Int} : a < b ↔ a ≤ b ∧ ¬b ≤ a
· exact Int.le_antisymm h h'
· subst h'; apply Int.le_refl
protected theorem lt_of_not_ge {a b : Int} (h : ¬a b) : b < a :=
Int.lt_iff_le_not_le.mpr (Int.le_total ..).resolve_right h, h
protected theorem not_le_of_gt {a b : Int} (h : b < a) : ¬a b :=
(Int.lt_iff_le_not_le.mp h).right
protected theorem not_le {a b : Int} : ¬a b b < a :=
Iff.intro Int.lt_of_not_ge Int.not_le_of_gt
fun h => Int.lt_iff_le_not_le.2 (Int.le_total ..).resolve_right h, h,
fun h => (Int.lt_iff_le_not_le.1 h).2
protected theorem not_lt {a b : Int} : ¬a < b b a :=
by rw [ Int.not_le, Decidable.not_not]
@@ -514,6 +509,9 @@ theorem mem_toNat' : ∀ (a : Int) (n : Nat), toNat' a = some n ↔ a = n
/-! ## Order properties of the integers -/
protected theorem lt_of_not_ge {a b : Int} : ¬a b b < a := Int.not_le.mp
protected theorem not_le_of_gt {a b : Int} : b < a ¬a b := Int.not_le.mpr
protected theorem le_of_not_le {a b : Int} : ¬ a b b a := (Int.le_total a b).resolve_left
@[simp] theorem negSucc_not_pos (n : Nat) : 0 < -[n+1] False := by
@@ -588,10 +586,7 @@ theorem add_one_le_iff {a b : Int} : a + 1 ≤ b ↔ a < b := .rfl
theorem lt_add_one_iff {a b : Int} : a < b + 1 a b := Int.add_le_add_iff_right _
@[simp] theorem succ_ofNat_pos (n : Nat) : 0 < (n : Int) + 1 :=
lt_add_one_iff.mpr (ofNat_zero_le _)
theorem not_ofNat_neg (n : Nat) : ¬((n : Int) < 0) :=
Int.not_lt.mpr (ofNat_zero_le ..)
lt_add_one_iff.2 (ofNat_zero_le _)
theorem le_add_one {a b : Int} (h : a b) : a b + 1 :=
Int.le_of_lt (Int.lt_add_one_iff.2 h)
@@ -806,12 +801,6 @@ protected theorem lt_add_of_neg_lt_sub_right {a b c : Int} (h : -b < a - c) : c
protected theorem neg_lt_sub_right_of_lt_add {a b c : Int} (h : c < a + b) : -b < a - c :=
Int.lt_sub_left_of_add_lt (Int.sub_right_lt_of_lt_add h)
protected theorem add_lt_iff (a b c : Int) : a + b < c a < -b + c := by
rw [ Int.add_lt_add_iff_left (-b), Int.add_comm (-b), Int.add_neg_cancel_right]
protected theorem sub_lt_iff (a b c : Int) : a - b < c a < c + b :=
Iff.intro Int.lt_add_of_sub_right_lt Int.sub_right_lt_of_lt_add
protected theorem sub_lt_of_sub_lt {a b c : Int} (h : a - b < c) : a - c < b :=
Int.sub_left_lt_of_lt_add (Int.lt_add_of_sub_right_lt h)

View File

@@ -8,7 +8,6 @@ import Init.Data.List.Basic
import Init.Data.List.BasicAux
import Init.Data.List.Control
import Init.Data.List.Lemmas
import Init.Data.List.Attach
import Init.Data.List.Impl
import Init.Data.List.TakeDrop
import Init.Data.List.Notation

View File

@@ -1,46 +0,0 @@
/-
Copyright (c) 2023 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
prelude
import Init.Data.List.Lemmas
namespace List
/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
`a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
but is defined only when all members of `l` satisfy `P`, using the proof
to apply `f`. -/
@[simp] def pmap {P : α Prop} (f : a, P a β) : l : List α, (H : a l, P a) List β
| [], _ => []
| a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2
/--
Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
`List {x // P x}` is the same as the input `List α`.
(Someday, the compiler might do this optimization automatically, but until then...)
-/
@[inline] private unsafe def attachWithImpl
(l : List α) (P : α Prop) (_ : x l, P x) : List {x // P x} := unsafeCast l
/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `l` to produce a new list
with the same elements but in the type `{x // P x}`. -/
@[implemented_by attachWithImpl] def attachWith
(l : List α) (P : α Prop) (H : x l, P x) : List {x // P x} := pmap Subtype.mk l H
/-- `O(1)`. "Attach" the proof that the elements of `l` are in `l` to produce a new list
with the same elements but in the type `{x // x ∈ l}`. -/
@[inline] def attach (l : List α) : List {x // x l} := attachWith l _ fun _ => id
/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
@[inline] private def pmapImpl {P : α Prop} (f : a, P a β) (l : List α) (H : a l, P a) :
List β := (l.attachWith _ H).map fun x, h' => f x h'
@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
funext α β p f L h'
let rec go : L' (hL' : x, x L' p x),
pmap f L' hL' = map (fun x, hx => f x hx) (pmap Subtype.mk L' hL')
| nil, hL' => rfl
| cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx)
exact go L h'

View File

@@ -22,7 +22,7 @@ along with `@[csimp]` lemmas,
In `Init.Data.List.Lemmas` we develop the full API for these functions.
Recall that `length`, `get`, `set`, `foldl`, and `concat` have already been defined in `Init.Prelude`.
Recall that `length`, `get`, `set`, `fold`, and `concat` have already been defined in `Init.Prelude`.
The operations are organized as follow:
* Equality: `beq`, `isEqv`.
@@ -32,8 +32,8 @@ The operations are organized as follow:
* List membership: `isEmpty`, `elem`, `contains`, `mem` (and the `∈` notation),
and decidability for predicates quantifying over membership in a `List`.
* Sublists: `take`, `drop`, `takeWhile`, `dropWhile`, `partition`, `dropLast`,
`isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `Subset`, `Sublist`, `rotateLeft` and `rotateRight`.
* Manipulating elements: `replace`, `insert`, `erase`, `eraseP`, `eraseIdx`, `find?`, `findSome?`, and `lookup`.
`isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `rotateLeft` and `rotateRight`.
* Manipulating elements: `replace`, `insert`, `erase`, `eraseIdx`, `find?`, `findSome?`, and `lookup`.
* Logic: `any`, `all`, `or`, and `and`.
* Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
* Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
@@ -67,9 +67,6 @@ namespace List
@[simp 1100] theorem length_singleton (a : α) : length [a] = 1 := rfl
@[simp] theorem length_cons {α} (a : α) (as : List α) : (cons a as).length = as.length + 1 :=
rfl
/-! ### set -/
@[simp] theorem length_set (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length := by
@@ -88,7 +85,7 @@ namespace List
/-! ### concat -/
@[simp high] theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by
@[simp] theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by
induction as with
| nil => rfl
| cons _ xs ih => simp [concat, ih]
@@ -817,8 +814,6 @@ def dropLast {α} : List α → List α
@[simp] theorem dropLast_cons₂ :
(x::y::zs).dropLast = x :: (y::zs).dropLast := rfl
-- Later this can be proved by `simp` via `[List.length_dropLast, List.length_cons, Nat.add_sub_cancel]`,
-- but we need this while bootstrapping `Array`.
@[simp] theorem length_dropLast_cons (a : α) (as : List α) : (a :: as).dropLast.length = as.length := by
match as with
| [] => rfl
@@ -866,40 +861,6 @@ def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
def isSuffixOf? [BEq α] (l₁ l₂ : List α) : Option (List α) :=
Option.map List.reverse <| isPrefixOf? l₁.reverse l₂.reverse
/-! ### Subset -/
/--
`l₁ ⊆ l₂` means that every element of `l₁` is also an element of `l₂`, ignoring multiplicity.
-/
protected def Subset (l₁ l₂ : List α) := a : α, a l₁ a l₂
instance : HasSubset (List α) := List.Subset
instance [DecidableEq α] : DecidableRel (Subset : List α List α Prop) :=
fun _ _ => decidableBAll _ _
/-! ### Sublist and isSublist -/
/-- `l₁ <+ l₂`, or `Sublist l₁ l₂`, says that `l₁` is a (non-contiguous) subsequence of `l₂`. -/
inductive Sublist {α} : List α List α Prop
/-- the base case: `[]` is a sublist of `[]` -/
| slnil : Sublist [] []
/-- If `l₁` is a subsequence of `l₂`, then it is also a subsequence of `a :: l₂`. -/
| cons a : Sublist l₁ l₂ Sublist l₁ (a :: l₂)
/-- If `l₁` is a subsequence of `l₂`, then `a :: l₁` is a subsequence of `a :: l₂`. -/
| cons₂ a : Sublist l₁ l₂ Sublist (a :: l₁) (a :: l₂)
@[inherit_doc] scoped infixl:50 " <+ " => Sublist
/-- True if the first list is a potentially non-contiguous sub-sequence of the second list. -/
def isSublist [BEq α] : List α List α Bool
| [], _ => true
| _, [] => false
| l₁@(hd₁::tl₁), hd₂::tl₂ =>
if hd₁ == hd₂
then tl₁.isSublist tl₂
else l₁.isSublist tl₂
/-! ### rotateLeft -/
/--
@@ -919,8 +880,6 @@ def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
let e := xs.drop n
e ++ b
@[simp] theorem rotateLeft_nil : ([] : List α).rotateLeft n = [] := rfl
/-! ### rotateRight -/
/--
@@ -940,57 +899,6 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α :=
let e := xs.drop n
e ++ b
@[simp] theorem rotateRight_nil : ([] : List α).rotateRight n = [] := rfl
/-! ## Pairwise, Nodup -/
section Pairwise
variable (R : α α Prop)
/--
`Pairwise R l` means that all the elements with earlier indexes are
`R`-related to all the elements with later indexes.
```
Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
```
For example if `R = (·≠·)` then it asserts `l` has no duplicates,
and if `R = (·<·)` then it asserts that `l` is (strictly) sorted.
-/
inductive Pairwise : List α Prop
/-- All elements of the empty list are vacuously pairwise related. -/
| nil : Pairwise []
/-- `a :: l` is `Pairwise R` if `a` `R`-relates to every element of `l`,
and `l` is `Pairwise R`. -/
| cons : {a : α} {l : List α}, ( a', a' l R a a') Pairwise l Pairwise (a :: l)
attribute [simp] Pairwise.nil
variable {R}
@[simp] theorem pairwise_cons : Pairwise R (a::l) ( a', a' l R a a') Pairwise R l :=
fun | .cons h₁ h₂ => h₁, h₂, fun h₁, h₂ => h₂.cons h₁
instance instDecidablePairwise [DecidableRel R] :
(l : List α) Decidable (Pairwise R l)
| [] => isTrue .nil
| hd :: tl =>
match instDecidablePairwise tl with
| isTrue ht =>
match decidableBAll (R hd) tl with
| isFalse hf => isFalse fun hf' => hf (pairwise_cons.1 hf').1
| isTrue ht' => isTrue <| pairwise_cons.mpr (And.intro ht' ht)
| isFalse hf => isFalse fun | .cons _ ih => hf ih
end Pairwise
/-- `Nodup l` means that `l` has no duplicates, that is, any element appears at most
once in the List. It is defined as `Pairwise (≠)`. -/
def Nodup : List α Prop := Pairwise (· ·)
instance nodupDecidable [DecidableEq α] : l : List α, Decidable (Nodup l) :=
instDecidablePairwise
/-! ## Manipulating elements -/
/-! ### replace -/
@@ -1036,11 +944,6 @@ theorem erase_cons [BEq α] (a b : α) (l : List α) :
(b :: l).erase a = if b == a then l else b :: l.erase a := by
simp only [List.erase]; split <;> simp_all
/-- `eraseP p l` removes the first element of `l` satisfying the predicate `p`. -/
def eraseP (p : α Bool) : List α List α
| [] => []
| a :: l => bif p a then l else a :: eraseP p l
/-! ### eraseIdx -/
/--

View File

@@ -295,24 +295,6 @@ theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++
· rw [IH] <;> simp_all
· simp
/-- Tail-recursive version of `eraseP`. -/
@[inline] def erasePTR (p : α Bool) (l : List α) : List α := go l #[] where
/-- Auxiliary for `erasePTR`: `erasePTR.go p l xs acc = acc.toList ++ eraseP p xs`,
unless `xs` does not contain any elements satisfying `p`, where it returns `l`. -/
@[specialize] go : List α Array α List α
| [], _ => l
| a :: l, acc => bif p a then acc.toListAppend l else go l (acc.push a)
@[csimp] theorem eraseP_eq_erasePTR : @eraseP = @erasePTR := by
funext α p l; simp [erasePTR]
let rec go (acc) : xs, l = acc.data ++ xs
erasePTR.go p l xs acc = acc.data ++ xs.eraseP p
| [] => fun h => by simp [erasePTR.go, eraseP, h]
| x::xs => by
simp [erasePTR.go, eraseP]; cases p x <;> simp
· intro h; rw [go _ xs]; {simp}; simp [h]
exact (go #[] _ rfl).symm
/-! ### eraseIdx -/
/-- Tail recursive version of `List.eraseIdx`. -/

File diff suppressed because it is too large Load Diff

View File

@@ -120,43 +120,6 @@ theorem get?_take_eq_if {l : List α} {n m : Nat} :
(l.take n).get? m = if m < n then l.get? m else none := by
simp [getElem?_take_eq_if]
theorem head?_take {l : List α} {n : Nat} :
(l.take n).head? = if n = 0 then none else l.head? := by
simp [head?_eq_getElem?, getElem?_take_eq_if]
split
· rw [if_neg (by omega)]
· rw [if_pos (by omega)]
theorem head_take {l : List α} {n : Nat} (h : l.take n []) :
(l.take n).head h = l.head (by simp_all) := by
apply Option.some_inj.1
rw [ head?_eq_head, head?_eq_head, head?_take, if_neg]
simp_all
theorem getLast?_take {l : List α} : (l.take n).getLast? = if n = 0 then none else l[n - 1]?.or l.getLast? := by
rw [getLast?_eq_getElem?, getElem?_take_eq_if, length_take]
split
· rw [if_neg (by omega)]
rw [Nat.min_def]
split
· rw [getElem?_eq_getElem (by omega)]
simp
· rw [ getLast?_eq_getElem?, getElem?_eq_none (by omega)]
simp
· rw [if_pos]
omega
theorem getLast_take {l : List α} (h : l.take n []) :
(l.take n).getLast h = l[n - 1]?.getD (l.getLast (by simp_all)) := by
rw [getLast_eq_getElem, getElem_take']
simp [length_take, Nat.min_def]
simp at h
split
· rw [getElem?_eq_getElem (by omega)]
simp
· rw [getElem?_eq_none (by omega), getLast_eq_getElem]
simp
@[simp]
theorem take_eq_take :
{l : List α} {m n : Nat}, l.take m = l.take n min m l.length = min n l.length
@@ -282,31 +245,6 @@ theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? :=
theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
simp
theorem head?_drop (l : List α) (n : Nat) :
(l.drop n).head? = l[n]? := by
rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]
theorem head_drop {l : List α} {n : Nat} (h : l.drop n []) :
(l.drop n).head h = l[n]'(by simp_all) := by
have w : n < l.length := length_lt_of_drop_ne_nil h
simpa [head?_eq_head, getElem?_eq_getElem, h, w] using head?_drop l n
theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length n then none else l.getLast? := by
rw [getLast?_eq_getElem?, getElem?_drop]
rw [length_drop]
split
· rw [getElem?_eq_none (by omega)]
· rw [getLast?_eq_getElem?]
congr
omega
theorem getLast_drop {l : List α} (h : l.drop n []) :
(l.drop n).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
simp only [ne_eq, drop_eq_nil_iff_le] at h
apply Option.some_inj.1
simp only [ getLast?_eq_getLast, getLast?_drop, ite_eq_right_iff]
omega
theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} :
l.set n a = if n < l.length then l.take n ++ a :: l.drop (n + 1) else l := by
split <;> rename_i h
@@ -334,15 +272,6 @@ theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} :
· rw [set_eq_of_length_le]
omega
theorem exists_of_set {n : Nat} {a' : α} {l : List α} (h : n < l.length) :
l₁ l₂, l = l₁ ++ l[n] :: l₂ l₁.length = n l.set n a' = l₁ ++ a' :: l₂ := by
refine l.take n, l.drop (n + 1), by simp, length_take_of_le (Nat.le_of_lt h), ?_
simp [set_eq_take_append_cons_drop, h]
theorem drop_set_of_lt (a : α) {n m : Nat} (l : List α)
(hnm : n < m) : drop m (l.set n a) = l.drop m :=
ext_getElem? fun k => by simpa only [getElem?_drop] using getElem?_set_ne (by omega)
theorem drop_take : (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
| 0, _, _ => by simp
| _, 0, _ => by simp
@@ -387,7 +316,7 @@ theorem take_reverse {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
omega
/-! ### rotateRight -/
/-! ### rotateLeft -/
@[simp] theorem rotateRight_replicate (n) (a : α) : rotateRight (replicate m a) n = replicate m a := by
cases n with
@@ -435,70 +364,4 @@ theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β),
rw [zip_eq_zip_take_min]
simp
/-! ### minimum? -/
-- A specialization of `minimum?_eq_some_iff` to Nat.
theorem minimum?_eq_some_iff' {xs : List Nat} :
xs.minimum? = some a (a xs b xs, a b) :=
minimum?_eq_some_iff
(le_refl := Nat.le_refl)
(min_eq_or := fun _ _ => by omega)
(le_min_iff := fun _ _ _ => by omega)
-- This could be generalized,
-- but will first require further work on order typeclasses in the core repository.
theorem minimum?_cons' {a : Nat} {l : List Nat} :
(a :: l).minimum? = some (match l.minimum? with
| none => a
| some m => min a m) := by
rw [minimum?_eq_some_iff']
split <;> rename_i h m
· simp_all
· rw [minimum?_eq_some_iff'] at m
obtain m, le := m
rw [Nat.min_def]
constructor
· split
· exact mem_cons_self a l
· exact mem_cons_of_mem a m
· intro b m
cases List.mem_cons.1 m with
| inl => split <;> omega
| inr h =>
specialize le b h
split <;> omega
/-! ### maximum? -/
-- A specialization of `maximum?_eq_some_iff` to Nat.
theorem maximum?_eq_some_iff' {xs : List Nat} :
xs.maximum? = some a (a xs b xs, b a) :=
maximum?_eq_some_iff
(le_refl := Nat.le_refl)
(max_eq_or := fun _ _ => by omega)
(max_le_iff := fun _ _ _ => by omega)
-- This could be generalized,
-- but will first require further work on order typeclasses in the core repository.
theorem maximum?_cons' {a : Nat} {l : List Nat} :
(a :: l).maximum? = some (match l.maximum? with
| none => a
| some m => max a m) := by
rw [maximum?_eq_some_iff']
split <;> rename_i h m
· simp_all
· rw [maximum?_eq_some_iff'] at m
obtain m, le := m
rw [Nat.max_def]
constructor
· split
· exact mem_cons_of_mem a m
· exact mem_cons_self a l
· intro b m
cases List.mem_cons.1 m with
| inl => split <;> omega
| inr h =>
specialize le b h
split <;> omega
end List

View File

@@ -100,7 +100,6 @@ def blt (a b : Nat) : Bool :=
ble a.succ b
attribute [simp] Nat.zero_le
attribute [simp] Nat.not_lt_zero
/-! # Helper "packing" theorems -/
@@ -125,8 +124,13 @@ instance : LawfulBEq Nat where
eq_of_beq h := Nat.eq_of_beq_eq_true h
rfl := by simp [BEq.beq]
theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp
theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) := by simp
@[simp] theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := propext <| Iff.intro eq_of_beq (fun h => by subst h; apply LawfulBEq.rfl)
@[simp] theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) :=
propext <| Iff.intro
(fun h₁ h₂ => by subst h₂; rw [LawfulBEq.rfl] at h₁; contradiction)
(fun h =>
have : ¬ ((a == b) = true) := fun h' => absurd (eq_of_beq h') h
by simp [this])
/-! # Nat.add theorems -/
@@ -274,7 +278,7 @@ theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
| zero => exact rfl
| succ m ih => apply congrArg pred ih
theorem pred_le : (n : Nat), pred n n
@[simp] theorem pred_le : (n : Nat), pred n n
| zero => Nat.le.refl
| succ _ => le_succ _
@@ -284,7 +288,7 @@ theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
theorem sub_one_lt : {n : Nat}, n 0 n - 1 < n := pred_lt
@[simp] theorem sub_le (n m : Nat) : n - m n := by
theorem sub_le (n m : Nat) : n - m n := by
induction m with
| zero => exact Nat.le_refl (n - 0)
| succ m ih => apply Nat.le_trans (pred_le (n - m)) ih
@@ -351,7 +355,7 @@ protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_po
theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
@[simp] theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
@[simp] protected theorem lt_add_one (n : Nat) : n < n + 1 := lt.base n
@@ -634,10 +638,6 @@ theorem succ_lt_succ_iff : succ a < succ b ↔ a < b := ⟨lt_of_succ_lt_succ, s
theorem add_one_inj : a + 1 = b + 1 a = b := succ_inj'
theorem ne_add_one (n : Nat) : n n + 1 := fun h => by cases h
theorem add_one_ne (n : Nat) : n + 1 n := fun h => by cases h
theorem add_one_le_add_one_iff : a + 1 b + 1 a b := succ_le_succ_iff
theorem add_one_lt_add_one_iff : a + 1 < b + 1 a < b := succ_lt_succ_iff
@@ -705,7 +705,8 @@ protected theorem one_ne_zero : 1 ≠ (0 : Nat) :=
protected theorem zero_ne_one : 0 (1 : Nat) :=
fun h => Nat.noConfusion h
theorem succ_ne_zero (n : Nat) : succ n 0 := by simp
@[simp] theorem succ_ne_zero (n : Nat) : succ n 0 :=
fun h => Nat.noConfusion h
/-! # mul + order -/
@@ -813,14 +814,8 @@ theorem sub_one_lt_of_lt {n m : Nat} (h : m < n) : n - 1 < n :=
/-! # pred theorems -/
protected theorem pred_zero : pred 0 = 0 := rfl
protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
@[simp] protected theorem zero_sub_one : 0 - 1 = 0 := rfl
@[simp] protected theorem add_one_sub_one (n : Nat) : n + 1 - 1 = n := rfl
theorem sub_one_eq_self (n : Nat) : n - 1 = n n = 0 := by cases n <;> simp [ne_add_one]
theorem eq_self_sub_one (n : Nat) : n = n - 1 n = 0 := by cases n <;> simp [add_one_ne]
@[simp] protected theorem pred_zero : pred 0 = 0 := rfl
@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
theorem succ_pred {a : Nat} (h : a 0) : a.pred.succ = a := by
induction a with

View File

@@ -86,7 +86,7 @@ noncomputable def div2Induction {motive : Nat → Sort u}
@[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
@[simp] theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
unfold testBit
simp [shiftRight_succ_inside]
@@ -310,11 +310,6 @@ theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
Nat.div_div_eq_div_mul _ 2, one_div_two,
Nat.mod_eq_of_lt]
/-- `testBit 1 i` is true iff the index `i` equals 0. -/
theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
Nat.testBit 1 i = true i = 0 := by
cases i <;> simp
/-! ### bitwise -/
theorem testBit_bitwise
@@ -504,27 +499,3 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
@[simp] theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j) := by
simp [testBit, shiftRight_add]
/-! ### le -/
theorem le_of_testBit {n m : Nat} (h : i, n.testBit i = true m.testBit i = true) : n m := by
induction n using div2Induction generalizing m
next n ih =>
have : n / 2 m / 2 := by
rcases n with (_|n)
· simp
· exact ih (Nat.succ_pos _) fun i => by simpa using h (i + 1)
rw [ div_add_mod n 2, div_add_mod m 2]
cases hn : n.testBit 0
· have hn2 : n % 2 = 0 := by simp at hn; omega
rw [hn2]
omega
· have hn2 : n % 2 = 1 := by simpa using hn
have hm2 : m % 2 = 1 := by simpa using h _ hn
omega
theorem and_le_left {n m : Nat} : n &&& m n :=
le_of_testBit (by simpa using fun i x _ => x)
theorem and_le_right {n m : Nat} : n &&& m m :=
le_of_testBit (by simp)

View File

@@ -251,10 +251,10 @@ theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m
theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y x < y * k := by
rw [ Nat.not_le, Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk)
@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = (x / z) + 1 := by
@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = succ (x / z) := by
rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]
@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = (x / z) + 1 := by
@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = succ (x / z) := by
rw [Nat.add_comm, add_div_right x H]
theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z := by
@@ -285,7 +285,7 @@ theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z =
@[simp] theorem mul_mod_left (m n : Nat) : (m * n) % n = 0 := by
rw [Nat.mul_comm, mul_mod_right]
protected theorem div_eq_of_lt_le (lo : k * n m) (hi : m < (k + 1) * n) : m / n = k :=
protected theorem div_eq_of_lt_le (lo : k * n m) (hi : m < succ k * n) : m / n = k :=
have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by
rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi)
Nat.le_antisymm
@@ -307,7 +307,7 @@ theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p
rw [sub_succ, IH h₂, div_eq_sub_div h₀ h₃]
simp [Nat.pred_succ, mul_succ, Nat.sub_sub]
theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - (x + 1)) / n = p - ((x / n) + 1) := by
theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁
apply Nat.div_eq_of_lt_le

View File

@@ -115,6 +115,8 @@ protected theorem add_sub_cancel_right (n m : Nat) : (n + m) - m = n := Nat.add_
theorem succ_sub_one (n) : succ n - 1 = n := rfl
protected theorem add_one_sub_one (n : Nat) : (n + 1) - 1 = n := rfl
protected theorem one_add_sub_one (n : Nat) : (1 + n) - 1 = n := Nat.add_sub_cancel_left 1 _
protected theorem sub_sub_self {n m : Nat} (h : m n) : n - (n - m) = m :=

View File

@@ -583,6 +583,8 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
have : k 0 k + 1 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]
have : ¬ (k == 0) (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
have : ¬ ((k + 1 == 0) = true) := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
have : (1 == (0 : Nat)) = false := rfl
have : (1 == (1 : Nat)) = true := rfl
by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
<;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h
· exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h

View File

@@ -19,7 +19,6 @@ def getM [Alternative m] : Option α → m α
| some a => pure a
@[deprecated getM (since := "2024-04-17")]
-- `[Monad m]` is not needed here.
def toMonad [Monad m] [Alternative m] : Option α m α := getM
/-- Returns `true` on `some x` and `false` on `none`. -/
@@ -27,7 +26,7 @@ def toMonad [Monad m] [Alternative m] : Option α → m α := getM
| some _ => true
| none => false
@[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α Bool := isSome
@[deprecated isSome, inline] def toBool : Option α Bool := isSome
/-- Returns `true` on `none` and `false` on `some x`. -/
@[inline] def isNone : Option α Bool
@@ -81,9 +80,7 @@ theorem map_id : (Option.map id : Option α → Option α) = id :=
| none => false
/--
Implementation of `OrElse`'s `<|>` syntax for `Option`. If the first argument is `some a`, returns
`some a`, otherwise evaluates and returns the second argument. See also `or` for a version that is
strict in the second argument.
Implementation of `OrElse`'s `<|>` syntax for `Option`.
-/
@[always_inline, macro_inline] protected def orElse : Option α (Unit Option α) Option α
| some a, _ => some a
@@ -92,12 +89,6 @@ strict in the second argument.
instance : OrElse (Option α) where
orElse := Option.orElse
/-- If the first argument is `some a`, returns `some a`, otherwise returns the second argument.
This is similar to `<|>`/`orElse`, but it is strict in the second argument. -/
@[always_inline, macro_inline] def or : Option α Option α Option α
| some a, _ => some a
| none, b => b
@[inline] protected def lt (r : α α Prop) : Option α Option α Prop
| none, some _ => True
| some x, some y => r x y
@@ -128,7 +119,7 @@ def merge (fn : ααα) : Option α → Option α → Option α
/-- An elimination principle for `Option`. It is a nondependent version of `Option.recOn`. -/
@[inline] protected def elim : Option α β (α β) β
@[simp, inline] protected def elim : Option α β (α β) β
| some x, _, f => f x
| none, y, _ => y

View File

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
prelude
import Init.Data.Option.BasicAux
import Init.Data.Option.Instances
import Init.Classical
import Init.Ext
@@ -42,21 +41,6 @@ theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.get
theorem getD_eq_iff {o : Option α} {a b} : o.getD a = b (o = some b o = none a = b) := by
cases o <;> simp
@[simp] theorem get!_none [Inhabited α] : (none : Option α).get! = default := rfl
@[simp] theorem get!_some [Inhabited α] {a : α} : (some a).get! = a := rfl
theorem get_eq_get! [Inhabited α] : (o : Option α) {h : o.isSome} o.get h = o.get!
| some _, _ => rfl
theorem get_eq_getD {fallback : α} : (o : Option α) {h : o.isSome} o.get h = o.getD fallback
| some _, _ => rfl
theorem some_get! [Inhabited α] : (o : Option α) o.isSome some (o.get!) = o
| some _, _ => rfl
theorem get!_eq_getD_default [Inhabited α] (o : Option α) : o.get! = o.getD default := rfl
theorem mem_unique {o : Option α} {a b : α} (ha : a o) (hb : b o) : a = b :=
some.inj <| ha hb
@@ -82,7 +66,7 @@ theorem isSome_iff_exists : isSome x ↔ ∃ a, x = some a := by cases x <;> sim
cases a <;> simp
theorem eq_some_iff_get_eq : o = some a h : o.isSome, o.get h = a := by
cases o <;> simp
cases o <;> simp; nofun
theorem eq_some_of_isSome : {o : Option α} (h : o.isSome), o = some (o.get h)
| some _, _ => rfl
@@ -161,12 +145,6 @@ theorem map_eq_some : f <$> x = some b ↔ ∃ a, x = some a ∧ f a = b := map_
@[simp] theorem map_eq_none' : x.map f = none x = none := by
cases x <;> simp only [map_none', map_some', eq_self_iff_true]
theorem isSome_map {x : Option α} : (f <$> x).isSome = x.isSome := by
cases x <;> simp
@[simp] theorem isSome_map' {x : Option α} : (x.map f).isSome = x.isSome := by
cases x <;> simp
theorem map_eq_none : f <$> x = none x = none := map_eq_none'
theorem map_eq_bind {x : Option α} : x.map f = x.bind (some f) := by
@@ -190,9 +168,6 @@ theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘
theorem mem_map_of_mem (g : α β) (h : a x) : g a Option.map g x := h.symm map_some' ..
@[simp] theorem filter_none (p : α Bool) : none.filter p = none := rfl
theorem filter_some : Option.filter p (some a) = if p a then some a else none := rfl
theorem bind_map_comm {α β} {x : Option (Option α)} {f : α β} :
x.bind (Option.map f) = (x.map (Option.map f)).bind id := by cases x <;> simp
@@ -233,9 +208,9 @@ theorem liftOrGet_eq_or_eq {f : ααα} (h : ∀ a b, f a b = a f
@[simp] theorem liftOrGet_some_some {f} {a b : α} :
liftOrGet f (some a) (some b) = f a b := rfl
@[simp] theorem elim_none (x : β) (f : α β) : none.elim x f = x := rfl
theorem elim_none (x : β) (f : α β) : none.elim x f = x := rfl
@[simp] theorem elim_some (x : β) (f : α β) (a : α) : (some a).elim x f = f a := rfl
theorem elim_some (x : β) (f : α β) (a : α) : (some a).elim x f = f a := rfl
@[simp] theorem getD_map (f : α β) (x : α) (o : Option α) :
(o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl
@@ -261,46 +236,3 @@ end
@[simp] theorem toList_some (a : α) : (a : Option α).toList = [a] := rfl
@[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
@[simp] theorem or_some : (some a).or o = some a := rfl
@[simp] theorem none_or : none.or o = o := rfl
theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
cases o <;> rfl
@[simp] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
cases o <;> rfl
@[simp] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
cases o <;> rfl
@[simp] theorem or_eq_none : or o o' = none o = none o' = none := by
cases o <;> simp
theorem or_eq_some : or o o' = some a o = some a (o = none o' = some a) := by
cases o <;> simp
theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
cases o₁ <;> cases o₂ <;> rfl
instance : Std.Associative (or (α := α)) := @or_assoc _
@[simp]
theorem or_none : or o none = o := by
cases o <;> rfl
instance : Std.LawfulIdentity (or (α := α)) none where
left_id := @none_or _
right_id := @or_none _
@[simp]
theorem or_self : or o o = o := by
cases o <;> rfl
instance : Std.IdempotentOp (or (α := α)) := @or_self _
theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
cases o <;> rfl
theorem map_or : f <$> or o o' = (f <$> o).or (f <$> o') := by
cases o <;> rfl
theorem map_or' : (or o o').map f = (o.map f).or (o'.map f) := by
cases o <;> rfl

View File

@@ -230,7 +230,7 @@ protected def Int.repr : Int → String
| negSucc m => "-" ++ Nat.repr (succ m)
instance : Repr Int where
reprPrec i prec := if i < 0 then Repr.addAppParen i.repr prec else i.repr
reprPrec i _ := i.repr
def hexDigitRepr (n : Nat) : String :=
String.singleton <| Nat.digitChar n

View File

@@ -69,7 +69,7 @@ where
decreasing_by exact Nat.sub_lt_sub_left _ (Nat.lt_add_of_pos_right c.utf8Size_pos)
/-- Converts a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded `ByteArray` string to `String`. -/
@[extern "lean_string_from_utf8_unchecked"]
@[extern "lean_string_from_utf8"]
def fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String :=
loop 0 ""
where

View File

@@ -7,4 +7,3 @@ prelude
import Init.Data.UInt.Basic
import Init.Data.UInt.Log2
import Init.Data.UInt.Lemmas
import Init.Data.UInt.Bitwise

View File

@@ -1,24 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
prelude
import Init.Data.UInt.Basic
import Init.Data.Fin.Bitwise
set_option hygiene false in
macro "declare_bitwise_uint_theorems" typeName:ident : command =>
`(
namespace $typeName
@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := Fin.and_val ..
end $typeName
)
declare_bitwise_uint_theorems UInt8
declare_bitwise_uint_theorems UInt16
declare_bitwise_uint_theorems UInt32
declare_bitwise_uint_theorems UInt64
declare_bitwise_uint_theorems USize

View File

@@ -26,8 +26,6 @@ theorem add_def (a b : $typeName) : a + b = ⟨a.val + b.val⟩ := rfl
| _, _ => rfl
theorem val_eq_of_lt {a : Nat} : a < size ((ofNat a).val : Nat) = a :=
Nat.mod_eq_of_lt
theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
rw [toNat, val_eq_of_lt h]
theorem le_def {a b : $typeName} : a b a.1 b.1 := .rfl
theorem lt_def {a b : $typeName} : a < b a.1 < b.1 := .rfl
@@ -50,7 +48,6 @@ protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := ne_of_val_
@[simp] protected theorem zero_toNat : (0 : $typeName).toNat = 0 := Nat.zero_mod _
@[simp] protected theorem mod_toNat (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
@[simp] protected theorem div_toNat (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
@[simp] protected theorem sub_toNat_of_le (a b : $typeName) : b a (a - b).toNat = a.toNat - b.toNat := Fin.sub_val_of_le
@[simp] protected theorem modn_toNat (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
protected theorem modn_lt {m : Nat} : (u : $typeName), m > 0 toNat (u % m) < m
| u, h => Fin.modn_lt u h
@@ -58,8 +55,6 @@ open $typeName (modn_lt) in
protected theorem mod_lt (a b : $typeName) (h : 0 < b) : a % b < b := modn_lt _ (by simp [lt_def] at h; exact h)
protected theorem toNat.inj : {a b : $typeName}, a.toNat = b.toNat a = b
| _, _, _, _, rfl => rfl
protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.1.2
@[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
end $typeName
)

View File

@@ -10,38 +10,58 @@ import Init.RCases
namespace Lean
namespace Parser.Attr
/--
The flag `(iff := false)` prevents `ext` from generating an `ext_iff` lemma.
-/
syntax extIff := atomic("(" &"iff" " := " &"false" ")")
/--
The flag `(flat := false)` causes `ext` to not flatten parents' fields when generating an `ext` lemma.
-/
syntax extFlat := atomic("(" &"flat" " := " &"false" ")")
/--
Registers an extensionality theorem.
/-- Registers an extensionality theorem.
* When `@[ext]` is applied to a structure, it generates `.ext` and `.ext_iff` theorems and registers
them for the `ext` tactic.
* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an `ext_iff` theorem.
The name of the theorem is from adding the suffix `_iff` to the theorem name.
* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic.
* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the lemma. Higher-priority lemmas are chosen first, and the default is `1000`.
* The flag `@[ext (iff := false)]` prevents it from generating an `ext_iff` theorem.
* The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation,
rather than flattening the parents' fields into the lemma's equality hypotheses.
-/
syntax (name := ext) "ext" (ppSpace extIff)? (ppSpace extFlat)? (ppSpace prio)? : attr
structures in the generated extensionality theorems. -/
syntax (name := ext) "ext" (" (" &"flat" " := " term ")")? (ppSpace prio)? : attr
end Parser.Attr
-- TODO: rename this namespace?
-- Remark: `ext` has scoped syntax, Mathlib may depend on the actual namespace name.
namespace Elab.Tactic.Ext
/--
Creates the type of the extensionality theorem for the given structure,
elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
-/
scoped syntax (name := extType) "ext_type% " term:max ppSpace ident : term
/--
Creates the type of the iff-variant of the extensionality theorem for the given structure,
elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
-/
scoped syntax (name := extIffType) "ext_iff_type% " term:max ppSpace ident : term
/--
`declare_ext_theorems_for A` declares the extensionality theorems for the structure `A`.
These theorems state that two expressions with the structure type are equal if their fields are equal.
-/
syntax (name := declareExtTheoremFor) "declare_ext_theorems_for " ("(" &"flat" " := " term ") ")? ident (ppSpace prio)? : command
macro_rules | `(declare_ext_theorems_for $[(flat := $f)]? $struct:ident $(prio)?) => do
let flat := f.getD (mkIdent `true)
let names Macro.resolveGlobalName struct.getId.eraseMacroScopes
let name match names.filter (·.2.isEmpty) with
| [] => Macro.throwError s!"unknown constant {struct.getId}"
| [(name, _)] => pure name
| _ => Macro.throwError s!"ambiguous name {struct.getId}"
let extName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext"
let extIffName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext_iff"
`(@[ext $(prio)?] protected theorem $extName:ident : ext_type% $flat $struct:ident :=
fun {..} {..} => by intros; subst_eqs; rfl
protected theorem $extIffName:ident : ext_iff_type% $flat $struct:ident :=
fun {..} {..} =>
fun h => by cases h; and_intros <;> rfl,
fun _ => by (repeat cases _ _); subst_eqs; rfl)
/--
Applies extensionality lemmas that are registered with the `@[ext]` attribute.
@@ -76,8 +96,19 @@ macro "ext1" xs:(colGt ppSpace rintroPat)* : tactic =>
end Elab.Tactic.Ext
end Lean
attribute [ext] Prod PProd Sigma PSigma
attribute [ext] funext propext Subtype.eq
@[ext] theorem Prod.ext : {x y : Prod α β} x.fst = y.fst x.snd = y.snd x = y
| _,_, _,_, rfl, rfl => rfl
@[ext] theorem PProd.ext : {x y : PProd α β} x.fst = y.fst x.snd = y.snd x = y
| _,_, _,_, rfl, rfl => rfl
@[ext] theorem Sigma.ext : {x y : Sigma β} x.fst = y.fst HEq x.snd y.snd x = y
| _,_, _,_, rfl, .rfl => rfl
@[ext] theorem PSigma.ext : {x y : PSigma β} x.fst = y.fst HEq x.snd y.snd x = y
| _,_, _,_, rfl, .rfl => rfl
@[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
protected theorem Unit.ext (x y : Unit) : x = y := rfl

View File

@@ -7,57 +7,22 @@ prelude
import Init.Util
@[never_extract]
def outOfBounds [Inhabited α] : α :=
private def outOfBounds [Inhabited α] : α :=
panic! "index out of bounds"
theorem outOfBounds_eq_default [Inhabited α] : (outOfBounds : α) = default := rfl
/--
The classes `GetElem` and `GetElem?` implement lookup notation,
specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.
Both classes are indexed by types `coll`, `idx`, and `elem` which are
the collection, the index, and the element types.
A single collection may support lookups with multiple index
types. The relation `valid` determines when the index is guaranteed to be
valid; lookups of valid indices are guaranteed not to fail.
For example, an instance for arrays looks like
`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
holds, which is true when `i` is less than the size of the array. `Array`
additionally supports indexing with `USize` instead of `Nat`.
In either case, because the bounds are checked at compile time,
no runtime check is required.
The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
`GetElem coll idx elem valid` and uses this to infer the type of the return
value `elem` and side condition `valid` required to ensure `xs[i]` yields
a valid value of type `elem`. The tactic `get_elem_tactic` is
invoked to prove validity automatically. The `xs[i]'p` notation uses the
proof `p` to satisfy the validity condition.
If the proof `p` is long, it is often easier to place the
proof in the context using `have`, because `get_elem_tactic` tries
`assumption`.
`GetElem coll idx elem valid` and uses this to infer the type of return
value `elem` and side conditions `valid` required to ensure `xs[i]` yields
a valid value of type `elem`.
For example, the instance for arrays looks like
`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
The proof side-condition `valid xs i` is automatically dispatched by the
`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
`get_elem_tactic_trivial` using `macro_rules`.
`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
an `Option elem`, with `none` signalling that the value isn't present, and
the latter returns `elem` but panics if the value isn't there, returning
`default : elem` based on the `Inhabited elem` instance.
These are provided by the `GetElem?` class, for which there is a default instance
generated from a `GetElem` class as long as `valid xs i` is always decidable.
Important instances include:
* `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
indexing with no runtime bounds check and a proof side goal `i < arr.size`.
* `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
side goal `i < l.length`.
`get_elem_tactic` tactic, which can be extended by adding more clauses to
`get_elem_tactic_trivial`.
-/
class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
(valid : outParam (coll idx Prop)) where
@@ -65,10 +30,33 @@ class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
are proof side conditions to the application, they will be automatically
inferred by the `get_elem_tactic` tactic.
The actual behavior of this class is type-dependent, but here are some
important implementations:
* `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
indexing with no bounds check and a proof side goal `i < arr.size`.
* `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
side goal `i < l.length`.
* `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
no side goal (returns `.missing` out of range)
There are other variations on this syntax:
* `arr[i]!` is syntax for `getElem! arr i` which should panic and return
`default : α` if the index is not valid.
* `arr[i]?` is syntax for `getElem?` which should return `none` if the index
is not valid.
* `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
index is valid.
-/
getElem (xs : coll) (i : idx) (h : valid xs i) : elem
export GetElem (getElem)
getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
if h : _ then some (getElem xs i h) else none
getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
match getElem? xs i with | some e => e | none => outOfBounds
export GetElem (getElem getElem! getElem?)
@[inherit_doc getElem]
syntax:max term noWs "[" withoutPosition(term) "]" : term
@@ -78,30 +66,6 @@ macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
syntax term noWs "[" withoutPosition(term) "]'" term:max : term
macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
/-- Helper function for implementation of `GetElem?.getElem?`. -/
abbrev decidableGetElem? [GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] :
Option elem :=
if h : valid xs i then some xs[i] else none
@[inherit_doc GetElem]
class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w))
(valid : outParam (coll idx Prop)) extends GetElem coll idx elem valid where
/--
The syntax `arr[i]?` gets the `i`'th element of the collection `arr`,
if it is present (and wraps it in `some`), and otherwise returns `none`.
-/
getElem? : coll idx Option elem
/--
The syntax `arr[i]!` gets the `i`'th element of the collection `arr`,
if it is present, and otherwise panics at runtime and returns the `default` term
from `Inhabited elem`.
-/
getElem! [Inhabited elem] (xs : coll) (i : idx) : elem :=
match getElem? xs i with | some e => e | none => outOfBounds
export GetElem? (getElem? getElem!)
/--
The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
returns `none` if `i` is out of bounds.
@@ -114,51 +78,32 @@ panics `i` is out of bounds.
-/
macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
instance (priority := low) [GetElem coll idx elem valid] [ xs i, Decidable (valid xs i)] :
GetElem? coll idx elem valid where
getElem? xs i := decidableGetElem? xs i
theorem getElem_congr_coll [GetElem coll idx elem valid] {c d : coll} {i : idx} {h : valid c i}
(h' : c = d) : c[i] = d[i]'(h' h) := by
cases h'; rfl
theorem getElem_congr [GetElem coll idx elem valid] {c : coll} {i j : idx} {h : valid c i}
(h' : i = j) : c[i] = c[j]'(h' h) := by
cases h'; rfl
class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
(dom : outParam (cont idx Prop)) [ge : GetElem? cont idx elem dom] : Prop where
(dom : outParam (cont idx Prop)) [ge : GetElem cont idx elem dom] : Prop where
getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
c[i]? = if h : dom c i then some (c[i]'h) else none := by
intros
try simp only [getElem?] <;> congr
getElem!_def [Inhabited elem] (c : cont) (i : idx) :
c[i]! = match c[i]? with | some e => e | none => default := by
intros
simp only [getElem!, getElem?, outOfBounds_eq_default]
c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
export LawfulGetElem (getElem?_def getElem!_def)
instance (priority := low) [GetElem coll idx elem valid] [ xs i, Decidable (valid xs i)] :
LawfulGetElem coll idx elem valid where
theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
rw [getElem?_def]
exact dif_pos h
theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
rw [getElem?_def]
exact dif_neg h
theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
[Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
c[i]! = c[i]'h := by
simp only [getElem!_def, getElem?_def, h]
theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
[Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
simp only [getElem!_def, getElem?_def, h]
@@ -166,22 +111,23 @@ namespace Fin
instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
getElem xs i h := getElem xs i.1 h
instance instGetElem?FinVal [GetElem? cont Nat elem dom] : GetElem? cont (Fin n) elem fun xs i => dom xs i where
getElem? xs i := getElem? xs i.val
getElem! xs i := getElem! xs i.val
instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
getElem?_def _c _i _d := h.getElem?_def ..
getElem!_def _c _i := h.getElem!_def ..
@[simp] theorem getElem_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
getElem?_def _c _i _d := h.getElem?_def ..
getElem!_def _c _i _d := h.getElem!_def ..
@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
a[i] = a[i.1] := rfl
@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[i.1]? := by rfl
@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
[Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[i.1]! := rfl
@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
[Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
macro_rules
| `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)
@@ -193,15 +139,17 @@ namespace List
instance : GetElem (List α) Nat α fun as i => i < as.length where
getElem as i h := as.get i, h
instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
@[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
rfl
@[deprecated (since := "2024-06-12")] abbrev cons_getElem_zero := @getElem_cons_zero
@[deprecated (since := "2024-6-12")] abbrev cons_getElem_zero := @getElem_cons_zero
@[simp] theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
rfl
@[deprecated (since := "2024-06-12")] abbrev cons_getElem_succ := @getElem_cons_succ
@[deprecated (since := "2024-6-12")] abbrev cons_getElem_succ := @getElem_cons_succ
theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
match as, i with
@@ -215,6 +163,8 @@ namespace Array
instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
getElem xs i h := xs.get i, h
instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
end Array
namespace Lean.Syntax
@@ -222,4 +172,6 @@ namespace Lean.Syntax
instance : GetElem Syntax Nat Syntax fun _ _ => True where
getElem stx i _ := stx.getArg i
instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
end Lean.Syntax

View File

@@ -1278,46 +1278,12 @@ def Occurrences.isAll : Occurrences → Bool
| all => true
| _ => false
/--
Controls which new mvars are turned in to goals by the `apply` tactic.
- `nonDependentFirst` mvars that don't depend on other goals appear first in the goal list.
- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list.
- `all` all unassigned mvars are added to the goal list.
-/
-- TODO: Consider renaming to `Apply.NewGoals`
inductive ApplyNewGoals where
| nonDependentFirst | nonDependentOnly | all
/-- Configures the behaviour of the `apply` tactic. -/
-- TODO: Consider renaming to `Apply.Config`
structure ApplyConfig where
newGoals := ApplyNewGoals.nonDependentFirst
/--
If `synthAssignedInstances` is `true`, then `apply` will synthesize instance implicit arguments
even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
one inferred. The `congr` tactic sets this flag to false.
-/
synthAssignedInstances := true
/--
If `allowSynthFailures` is `true`, then `apply` will return instance implicit arguments
for which typeclass search failed as new goals.
-/
allowSynthFailures := false
/--
If `approx := true`, then we turn on `isDefEq` approximations. That is, we use
the `approxDefEq` combinator.
-/
approx : Bool := true
namespace Rewrite
abbrev NewGoals := ApplyNewGoals
structure Config where
transparency : TransparencyMode := .reducible
transparency : TransparencyMode := TransparencyMode.reducible
offsetCnstrs : Bool := true
occs : Occurrences := .all
newGoals : NewGoals := .nonDependentFirst
occs : Occurrences := Occurrences.all
end Rewrite

View File

@@ -42,67 +42,23 @@ inductive EtaStructMode where
namespace DSimp
/--
The configuration for `dsimp`.
Passed to `dsimp` using, for example, the `dsimp (config := {zeta := false})` syntax.
Implementation note: this structure is only used for processing the `(config := ...)` syntax, and it is not used internally.
It is immediately converted to `Lean.Meta.Simp.Config` by `Lean.Elab.Tactic.elabSimpConfig`.
-/
structure Config where
/--
When `true` (default: `true`), performs zeta reduction of let expressions.
That is, `let x := v; e[x]` reduces to `e[v]`.
See also `zetaDelta`.
-/
/-- `let x := v; e[x]` reduces to `e[v]`. -/
zeta : Bool := true
/--
When `true` (default: `true`), performs beta reduction of applications of `fun` expressions.
That is, `(fun x => e[x]) v` reduces to `e[v]`.
-/
beta : Bool := true
/--
TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions.
That is, `(fun x => f x)` reduces to `f`.
-/
eta : Bool := true
/--
Configures how to determine definitional equality between two structure instances.
See documentation for `Lean.Meta.EtaStructMode`.
-/
etaStruct : EtaStructMode := .all
/--
When `true` (default: `true`), reduces `match` expressions applied to constructors.
-/
iota : Bool := true
/--
When `true` (default: `true`), reduces projections of structure constructors.
-/
proj : Bool := true
/--
When `true` (default: `false`), rewrites a proposition `p` to `True` or `False` by inferring
a `Decidable p` instance and reducing it.
-/
decide : Bool := false
/--
When `true` (default: `false`), unfolds definitions.
This can be enabled using the `simp!` syntax.
-/
autoUnfold : Bool := false
/--
If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all`
will fail if they do not make progress.
-/
/-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
will fail if they do not make progress. -/
failIfUnchanged : Bool := true
/--
If `unfoldPartialApp` is `true` (default: `false`), then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded.
-/
/-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded. -/
unfoldPartialApp : Bool := false
/--
When `true` (default: `false`), local definitions are unfolded.
That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
-/
/-- Given a local context containing entry `x : t := e`, free variable `x` reduces to `e`. -/
zetaDelta : Bool := false
deriving Inhabited, BEq
@@ -116,7 +72,7 @@ def defaultMaxSteps := 100000
The configuration for `simp`.
Passed to `simp` using, for example, the `simp (config := {contextual := true})` syntax.
See also `Lean.Meta.Simp.neutralConfig` and `Lean.Meta.DSimp.Config`.
See also `Lean.Meta.Simp.neutralConfig`.
-/
structure Config where
/--
@@ -218,14 +174,6 @@ structure Config where
to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
-/
index : Bool := true
/--
When `true` (default: `false`), `simp` will **not** create a proof for a rewriting rule associated
with an `rfl`-theorem.
Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
will **not** create a proof term which is an application of the annotated theorem.
-/
implicitDefEqProofs : Bool := false
deriving Inhabited, BEq
-- Configuration object for `simp_all`

View File

@@ -267,7 +267,6 @@ syntax (name := rawNatLit) "nat_lit " num : term
@[inherit_doc] infixr:90 "" => Function.comp
@[inherit_doc] infixr:35 " × " => Prod
@[inherit_doc] infixr:35 " ×' " => PProd
@[inherit_doc] infix:50 " " => Dvd.dvd
@[inherit_doc] infixl:55 " ||| " => HOr.hOr
@@ -704,28 +703,6 @@ syntax (name := checkSimp) "#check_simp " term "~>" term : command
-/
syntax (name := checkSimpFailure) "#check_simp " term "!~>" : command
/--
`#discr_tree_key t` prints the discrimination tree keys for a term `t` (or, if it is a single identifier, the type of that constant).
It uses the default configuration for generating keys.
For example,
```
#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
-- bar _ (@OfNat.ofNat Nat _ _)
#discr_tree_simp_key Nat.add_assoc
-- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _
```
`#discr_tree_simp_key` is similar to `#discr_tree_key`, but treats the underlying type
as one of a simp lemma, i.e. transforms it into an equality and produces the key of the
left-hand side.
-/
syntax (name := discrTreeKeyCmd) "#discr_tree_key " term : command
@[inherit_doc discrTreeKeyCmd]
syntax (name := discrTreeSimpKeyCmd) "#discr_tree_simp_key" term : command
/--
The `seal foo` command ensures that the definition of `foo` is sealed, meaning it is marked as `[irreducible]`.
This command is particularly useful in contexts where you want to prevent the reduction of `foo` in proofs.

View File

@@ -173,7 +173,7 @@ theorem mul_neg_left (xs ys : IntList) : (-xs) * ys = -(xs * ys) := by
attribute [local simp] add_def neg_def sub_def in
theorem sub_eq_add_neg (xs ys : IntList) : xs - ys = xs + (-ys) := by
induction xs generalizing ys with
| nil => simp
| nil => simp; rfl
| cons x xs ih =>
cases ys with
| nil => simp

View File

@@ -38,10 +38,6 @@ theorem ext {a b : LinearCombo} (w₁ : a.const = b.const) (w₂ : a.coeffs = b.
subst w₁; subst w₂
congr
/-- Check if a linear combination is an atom, i.e. the constant term is zero and there is exactly one nonzero coefficient, which is one. -/
def isAtom (a : LinearCombo) : Bool :=
a.const == 0 && (a.coeffs.filter (· == 1)).length == 1 && a.coeffs.all fun c => c == 0 || c == 1
/--
Evaluate a linear combination `⟨r, [c_1, …, c_k]⟩` at values `[v_1, …, v_k]` to obtain
`r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0))))`.

View File

@@ -488,9 +488,9 @@ attribute [unbox] Prod
/--
Similar to `Prod`, but `α` and `β` can be propositions.
You can use `α ×' β` as notation for `PProd α β`.
We use this type internally to automatically generate the `brecOn` recursor.
-/
@[pp_using_anonymous_constructor]
structure PProd (α : Sort u) (β : Sort v) where
/-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
fst : α
@@ -740,7 +740,7 @@ prove `p` given any element `x : α`, then `p` holds. Note that it is essential
that `p` is a `Prop` here; the version with `p` being a `Sort u` is equivalent
to `Classical.choice`.
-/
protected theorem Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α p) : p :=
protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α p) : p :=
match h₁ with
| intro a => h₂ a
@@ -2329,6 +2329,9 @@ without running out of stack space.
def List.lengthTR (as : List α) : Nat :=
lengthTRAux as 0
@[simp] theorem List.length_cons {α} (a : α) (as : List α) : Eq (cons a as).length as.length.succ :=
rfl
/--
`as.get i` returns the `i`'th element of the list `as`.
This version of the function uses `i : Fin as.length` to ensure that it will
@@ -2973,7 +2976,7 @@ def MonadExcept.ofExcept [Monad m] [MonadExcept ε m] : Except ε α → m α
export MonadExcept (throw tryCatch ofExcept)
instance (ε : Type u) (m : Type v Type w) [MonadExceptOf ε m] : MonadExcept ε m where
instance (ε : outParam (Type u)) (m : Type v Type w) [MonadExceptOf ε m] : MonadExcept ε m where
throw := throwThe ε
tryCatch := tryCatchThe ε
@@ -3147,7 +3150,7 @@ instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadW
instance {ρ : Type u} {m : Type u Type v} {n : Type u Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ n where
withReader f := monadMap (m := m) (withTheReader ρ f)
instance {ρ : Type u} {m : Type u Type v} : MonadWithReaderOf ρ (ReaderT ρ m) where
instance {ρ : Type u} {m : Type u Type v} [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) where
withReader f x := fun ctx => x (f ctx)
/--
@@ -3172,8 +3175,8 @@ class MonadStateOf (σ : semiOutParam (Type u)) (m : Type u → Type v) where
export MonadStateOf (set)
/--
Like `get`, but with `σ` explicit. This is useful if a monad supports
`MonadStateOf` for multiple different types `σ`.
Like `withReader`, but with `ρ` explicit. This is useful if a monad supports
`MonadWithReaderOf` for multiple different types `ρ`.
-/
abbrev getThe (σ : Type u) {m : Type u Type v} [MonadStateOf σ m] : m σ :=
MonadStateOf.get
@@ -3230,7 +3233,7 @@ def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ
of the state. It is equivalent to `get <* modify f` but may be more efficient.
-/
@[always_inline, inline]
def getModify {σ : Type u} {m : Type u Type v} [MonadState σ m] (f : σ σ) : m σ :=
def getModify {σ : Type u} {m : Type u Type v} [MonadState σ m] [Monad m] (f : σ σ) : m σ :=
modifyGet fun s => (s, f s)
-- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer

View File

@@ -253,9 +253,6 @@ end forall_congr
@[simp] theorem not_exists : (¬ x, p x) x, ¬p x := exists_imp
theorem forall_not_of_not_exists (h : ¬ x, p x) : x, ¬p x := not_exists.mp h
theorem not_exists_of_forall_not (h : x, ¬p x) : ¬ x, p x := not_exists.mpr h
theorem forall_and : ( x, p x q x) ( x, p x) ( x, q x) :=
fun h => fun x => (h x).1, fun x => (h x).2, fun h₁, h₂ x => h₁ x, h₂ x
@@ -295,8 +292,6 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x,
@[simp] theorem exists_eq_left' : ( a, a' = a p a) p a' := by simp [@eq_comm _ a']
@[simp] theorem exists_eq_right' : ( a, p a a' = a) p a' := by simp [@eq_comm _ a']
@[simp] theorem forall_eq_or_imp : ( a, a = a' q a p a) p a' a, q a p a := by
simp only [or_imp, forall_and, forall_eq]
@@ -373,6 +368,9 @@ else isTrue fun h2 => absurd h2 h
theorem decide_eq_true_iff (p : Prop) [Decidable p] : (decide p = true) p := by simp
@[simp] theorem decide_eq_false_iff_not (p : Prop) {_ : Decidable p} : (decide p = false) ¬p :=
of_decide_eq_false, decide_eq_false
@[simp] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
decide p = decide q (p q) :=
fun h => by rw [ decide_eq_true_iff p, h, decide_eq_true_iff], fun h => by simp [h]

View File

@@ -102,11 +102,3 @@ instance ShareCommonT.monadShareCommon [Monad m] : MonadShareCommon (ShareCommon
@[inline] def ShareCommonT.run [Monad m] (x : ShareCommonT σ m α) : m α := x.run' default
@[inline] def ShareCommonM.run (x : ShareCommonM σ α) : α := ShareCommonT.run x
/--
A more restrictive but efficient max sharing primitive.
Remark: it optimizes the number of RC operations, and the strategy for caching results.
-/
@[extern "lean_sharecommon_quick"]
def ShareCommon.shareCommon' (a : α) : α := a

View File

@@ -129,7 +129,6 @@ instance : Std.LawfulIdentity Or False where
@[simp] theorem iff_false (p : Prop) : (p False) = ¬p := propext (·.1), (·, False.elim)
@[simp] theorem false_iff (p : Prop) : (False p) = ¬p := propext (·.2), (False.elim, ·)
@[simp] theorem false_implies (p : Prop) : (False p) = True := eq_true False.elim
@[simp] theorem forall_false (p : False Prop) : ( h : False, p h) = True := eq_true (False.elim ·)
@[simp] theorem implies_true (α : Sort u) : (α True) = True := eq_true fun _ => trivial
@[simp] theorem true_implies (p : Prop) : (True p) = p := propext (· trivial), (fun _ => ·)
@[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim
@@ -229,22 +228,25 @@ instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
@[simp] theorem Bool.not_not (b : Bool) : (!!b) = b := by cases b <;> rfl
@[simp] theorem Bool.not_true : (!true) = false := by decide
@[simp] theorem Bool.not_false : (!false) = true := by decide
@[simp] theorem beq_true (b : Bool) : (b == true) = b := by cases b <;> rfl
@[simp] theorem beq_false (b : Bool) : (b == false) = !b := by cases b <;> rfl
@[simp] theorem Bool.not_beq_true (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
@[simp] theorem Bool.not_beq_false (b : Bool) : (!(b == false)) = (b == true) := by cases b <;> rfl
@[simp] theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
@[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
@[simp] theorem Bool.beq_to_eq (a b : Bool) :
(a == b) = (a = b) := by cases a <;> cases b <;> decide
@[simp] theorem Bool.not_beq_to_not_eq (a b : Bool) :
(!(a == b)) = ¬(a = b) := by cases a <;> cases b <;> decide
@[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
@[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide
@[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p :=
propext <| Iff.intro of_decide_eq_true decide_eq_true
@[simp] theorem decide_eq_false_iff_not {_ : Decidable p} : (decide p = false) ¬p :=
of_decide_eq_false, decide_eq_false
@[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by
cases g <;> (rename_i gp; simp [gp]; rfl)
@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp
@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by
cases h <;> (rename_i hp; simp [decide, hp])
@[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
@@ -252,10 +254,10 @@ instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
@[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
@[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl
theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp
@[simp] theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp [BEq.beq]
@[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne]
theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp
@[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
@[simp] theorem decide_False : decide False = false := rfl
@[simp] theorem decide_True : decide True = true := rfl
@@ -281,10 +283,7 @@ These will both normalize to `a = b` with the first via `bne_eq_false_iff_eq`.
rw [bne, beq_iff_eq a b]
cases a == b <;> decide
theorem Bool.beq_to_eq (a b : Bool) : (a == b) = (a = b) := by simp
theorem Bool.not_beq_to_not_eq (a b : Bool) : (!(a == b)) = ¬(a = b) := by simp
/- # Nat -/
/-# Nat -/
@[simp] theorem Nat.le_zero_eq (a : Nat) : (a 0) = (a = 0) :=
propext fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide

View File

@@ -712,17 +712,8 @@ structure Child (cfg : StdioConfig) where
@[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)
/--
Block until the child process has exited and return its exit code.
-/
@[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg IO UInt32
/--
Check whether the child has exited yet. If it hasn't return none, otherwise its exit code.
-/
@[extern "lean_io_process_child_try_wait"] opaque Child.tryWait {cfg : @& StdioConfig} : @& Child cfg
IO (Option UInt32)
/-- Terminates the child process using the SIGTERM signal or a platform analogue.
If the process was started using `SpawnArgs.setsid`, terminates the entire process group instead. -/
@[extern "lean_io_process_child_kill"] opaque Child.kill {cfg : @& StdioConfig} : @& Child cfg IO Unit
@@ -823,10 +814,6 @@ def set (tk : CancelToken) : BaseIO Unit :=
def isSet (tk : CancelToken) : BaseIO Bool :=
tk.ref.get
-- separate definition as otherwise no unboxed version is generated
@[export lean_io_cancel_token_is_set]
private def isSetExport := @isSet
end CancelToken
namespace FS

View File

@@ -267,9 +267,7 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
inaccessible names to the given names.
-/
macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
-- Limit ref variability for incrementality; see Note [Incremental Macros]
withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
macro "next " args:binderIdent* " => " tac:tacticSeq : tactic => `(tactic| case _ $args* => $tac)
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
syntax (name := allGoals) "all_goals " tacticSeq : tactic
@@ -373,8 +371,7 @@ reflexivity theorems (e.g., `Iff.rfl`).
macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
`exact HEq.rfl` etc.")
Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)

View File

@@ -31,19 +31,15 @@ private def expandIfThenElse
pure (hole, #[case])
let (posHole, posCase) mkCase thenTk pos `(?pos)
let (negHole, negCase) mkCase elseTk neg `(?neg)
`(tactic| ((open Classical in refine%$ifTk $( mkIf posHole negHole)); $[$(posCase ++ negCase)]*))
`(tactic| (open Classical in refine%$ifTk $( mkIf posHole negHole); $[$(posCase ++ negCase)]*))
macro_rules
| `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) =>
-- Limit ref variability for incrementality; see Note [Incremental Macros]
withRef tk do
expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
macro_rules
| `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
-- Limit ref variability for incrementality; see Note [Incremental Macros]
withRef tk do
expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
/--
`iterate n tac` runs `tac` exactly `n` times.

View File

@@ -45,13 +45,6 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
@[extern "lean_ptr_addr"]
unsafe opaque ptrAddrUnsafe {α : Type u} (a : @& α) : USize
/--
Returns `true` if `a` is an exclusive object.
We say an object is exclusive if it is single-threaded and its reference counter is 1.
-/
@[extern "lean_is_exclusive_obj"]
unsafe opaque isExclusiveUnsafe {α : Type u} (a : @& α) : Bool
set_option linter.unusedVariables.funArgs false in
@[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize β) (h : u₁ u₂, k u₁ = k u₂) : β :=
k (ptrAddrUnsafe a)

View File

@@ -37,7 +37,7 @@ noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : αα → Prop
namespace Acc
variable {α : Sort u} {r : α α Prop}
theorem inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
end Acc
@@ -58,7 +58,7 @@ class WellFoundedRelation (α : Sort u) where
wf : WellFounded rel
namespace WellFounded
theorem apply {α : Sort u} {r : α α Prop} (wf : WellFounded r) (a : α) : Acc r a :=
def apply {α : Sort u} {r : α α Prop} (wf : WellFounded r) (a : α) : Acc r a :=
wf.rec (fun p => p) a
section
@@ -78,7 +78,7 @@ noncomputable def fixF (x : α) (a : Acc r x) : C x := by
induction a with
| intro x₁ _ ih => exact F x₁ ih
theorem fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
induction acx with
| intro x r _ => exact rfl
@@ -112,14 +112,14 @@ def emptyWf {α : Sort u} : WellFoundedRelation α where
namespace Subrelation
variable {α : Sort u} {r q : α α Prop}
theorem accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
induction ac with
| intro x _ ih =>
apply Acc.intro
intro y h
exact ih y (h₁ h)
theorem wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
def wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
fun a => accessible @h₁ (apply h₂ a)
end Subrelation
@@ -136,10 +136,10 @@ private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x =
subst x
apply ih (f y) lt y rfl
theorem accessible {a : α} (f : α β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
def accessible {a : α} (f : α β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
accAux f ac a rfl
theorem wf (f : α β) (h : WellFounded r) : WellFounded (InvImage r f) :=
def wf (f : α β) (h : WellFounded r) : WellFounded (InvImage r f) :=
fun a => accessible f (apply h (f a))
end InvImage
@@ -148,26 +148,22 @@ end InvImage
wf := InvImage.wf f h.wf
-- The transitive closure of a well-founded relation is well-founded
open Relation
namespace TC
variable {α : Sort u} {r : α α Prop}
theorem Acc.transGen (h : Acc r a) : Acc (TransGen r) a := by
induction h with
| intro x _ H =>
refine Acc.intro x fun y hy ?_
cases hy with
| single hyx =>
exact H y hyx
| tail hyz hzx =>
exact (H _ hzx).inv hyz
def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
induction ac with
| intro x acx ih =>
apply Acc.intro x
intro y rel
induction rel with
| base a b rab => exact ih a rab
| trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
theorem acc_transGen_iff : Acc (TransGen r) a Acc r a :=
Subrelation.accessible TransGen.single, Acc.transGen
def wf (h : WellFounded r) : WellFounded (TC r) :=
fun a => accessible (apply h a)
end TC
theorem WellFounded.transGen (h : WellFounded r) : WellFounded (TransGen r) :=
fun a (h.apply a).transGen
@[deprecated Acc.transGen (since := "2024-07-16")] abbrev TC.accessible := @Acc.transGen
@[deprecated WellFounded.transGen (since := "2024-07-16")] abbrev TC.wf := @WellFounded.transGen
namespace Nat
-- less-than is well-founded
@@ -255,7 +251,7 @@ instance [αeqDec : DecidableEq α] {r : αα → Prop} [rDec : DecidableRe
apply isFalse; intro contra; cases contra <;> contradiction
-- TODO: generalize
theorem right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
def right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
match Nat.eq_or_lt_of_le h₁ with
| Or.inl h => h Prod.Lex.right a₁ h₂
| Or.inr h => Prod.Lex.left b₁ _ h
@@ -272,7 +268,7 @@ section
variable {α : Type u} {β : Type v}
variable {ra : α α Prop} {rb : β β Prop}
theorem lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
def lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
induction aca generalizing b with
| intro xa _ iha =>
induction (acb b) with
@@ -292,7 +288,7 @@ instance [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] : WellFound
lex ha hb
-- relational product is a Subrelation of the Lex
theorem RProdSubLex (a : α × β) (b : α × β) (h : RProd ra rb a b) : Prod.Lex ra rb a b := by
def RProdSubLex (a : α × β) (b : α × β) (h : RProd ra rb a b) : Prod.Lex ra rb a b := by
cases h with
| intro h₁ h₂ => exact Prod.Lex.left _ _ h₁
@@ -324,7 +320,7 @@ section
variable {α : Sort u} {β : α Sort v}
variable {r : α α Prop} {s : (a : α), β a β a Prop}
theorem lexAccessible {a} (aca : Acc r a) (acb : (a : α) WellFounded (s a)) (b : β a) : Acc (Lex r s) a, b := by
def lexAccessible {a} (aca : Acc r a) (acb : (a : α) WellFounded (s a)) (b : β a) : Acc (Lex r s) a, b := by
induction aca with
| intro xa _ iha =>
induction (WellFounded.apply (acb xa) b) with
@@ -351,7 +347,7 @@ variable {α : Sort u} {β : Sort v}
def lexNdep (r : α α Prop) (s : β β Prop) :=
Lex r (fun _ => s)
theorem lexNdepWf {r : α α Prop} {s : β β Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
def lexNdepWf {r : α α Prop} {s : β β Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
WellFounded.intro fun a, b => lexAccessible (WellFounded.apply ha a) (fun _ => hb) b
end
@@ -369,7 +365,7 @@ open WellFounded
variable {α : Sort u} {β : Sort v}
variable {r : α α Prop} {s : β β Prop}
theorem revLexAccessible {b} (acb : Acc s b) (aca : (a : α) Acc r a): (a : α) Acc (RevLex r s) a, b := by
def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) Acc r a): (a : α) Acc (RevLex r s) a, b := by
induction acb with
| intro xb _ ihb =>
intro a
@@ -381,7 +377,7 @@ theorem revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a :
| left => apply iha; assumption
| right => apply ihb; assumption
theorem revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
def revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
WellFounded.intro fun a, b => revLexAccessible (apply hb b) (WellFounded.apply ha) a
end
@@ -393,7 +389,7 @@ def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFou
rel := SkipLeft α hb.rel
wf := revLex emptyWf.wf hb.wf
theorem mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β β Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s a₁, b₁ a₂, b₂ :=
def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β β Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s a₁, b₁ a₂, b₂ :=
RevLex.right _ _ h
end

View File

@@ -8,22 +8,11 @@ import Lean.CoreM
namespace Lean
register_builtin_option debug.skipKernelTC : Bool := {
defValue := false
group := "debug"
descr := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
}
def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
(cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment :=
if debug.skipKernelTC.get opts then
addDeclWithoutChecking env decl
else
addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration)
(cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment := do
let env addDecl env opts decl cancelTk?
def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
let env addDecl env opts decl
compileDecl env opts decl
def addDecl (decl : Declaration) : CoreM Unit := do
@@ -31,7 +20,7 @@ def addDecl (decl : Declaration) : CoreM Unit := do
withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
if !( MonadLog.hasErrors) && decl.hasSorry then
logWarning "declaration uses 'sorry'"
match ( getEnv).addDecl ( getOptions) decl ( read).cancelTk? with
match ( getEnv).addDecl ( getOptions) decl with
| .ok env => setEnv env
| .error ex => throwKernelException ex

View File

@@ -53,7 +53,7 @@ structure AttributeImpl extends AttributeImplCore where
erase (decl : Name) : AttrM Unit := throwError "attribute cannot be erased"
deriving Inhabited
builtin_initialize attributeMapRef : IO.Ref (HashMap Name AttributeImpl) IO.mkRef {}
builtin_initialize attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) IO.mkRef {}
/-- Low level attribute registration function. -/
def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do
@@ -185,7 +185,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
afterSet : Name α AttrM Unit := fun _ _ _ => pure ()
afterImport : Array (Array (Name × α)) ImportM Unit := fun _ => pure ()
def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
def registerParametricAttribute [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) registerPersistentEnvExtension {
name := impl.ref
mkInitial := pure {}
@@ -239,7 +239,7 @@ structure EnumAttributes (α : Type) where
ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
deriving Inhabited
def registerEnumAttributes (attrDescrs : List (Name × String × α))
def registerEnumAttributes [Inhabited α] (attrDescrs : List (Name × String × α))
(validate : Name α AttrM Unit := fun _ _ => pure ())
(applicationTime := AttributeApplicationTime.afterTypeChecking)
(ref : Name := by exact decl_name%) : IO (EnumAttributes α) := do
@@ -317,7 +317,7 @@ inductive AttributeExtensionOLeanEntry where
structure AttributeExtensionState where
newEntries : List AttributeExtensionOLeanEntry := []
map : HashMap Name AttributeImpl
map : PersistentHashMap Name AttributeImpl
deriving Inhabited
abbrev AttributeExtension := PersistentEnvExtension AttributeExtensionOLeanEntry (AttributeExtensionOLeanEntry × AttributeImpl) AttributeExtensionState
@@ -348,7 +348,7 @@ private def AttributeExtension.addImported (es : Array (Array AttributeExtension
let map es.foldlM
(fun map entries =>
entries.foldlM
(fun (map : HashMap Name AttributeImpl) entry => do
(fun (map : PersistentHashMap Name AttributeImpl) entry => do
let attrImpl mkAttributeImplOfEntry ctx.env ctx.opts entry
return map.insert attrImpl.name attrImpl)
map)
@@ -374,7 +374,7 @@ def isBuiltinAttribute (n : Name) : IO Bool := do
/-- Return the name of all registered attributes. -/
def getBuiltinAttributeNames : IO (List Name) :=
return ( attributeMapRef.get).fold (init := []) fun r n _ => n::r
return ( attributeMapRef.get).foldl (init := []) fun r n _ => n::r
def getBuiltinAttributeImpl (attrName : Name) : IO AttributeImpl := do
let m attributeMapRef.get
@@ -392,7 +392,7 @@ def isAttribute (env : Environment) (attrName : Name) : Bool :=
def getAttributeNames (env : Environment) : List Name :=
let m := (attributeExtension.getState env).map
m.fold (fun r n _ => n::r) []
m.foldl (fun r n _ => n::r) []
def getAttributeImpl (env : Environment) (attrName : Name) : Except String AttributeImpl :=
let m := (attributeExtension.getState env).map
@@ -427,7 +427,7 @@ def Attribute.erase (declName : Name) (attrName : Name) : AttrM Unit := do
def updateEnvAttributesImpl (env : Environment) : IO Environment := do
let map attributeMapRef.get
let s := attributeExtension.getState env
let s := map.fold (init := s) fun s attrName attrImpl =>
let s := map.foldl (init := s) fun s attrName attrImpl =>
if s.map.contains attrName then
s
else

View File

@@ -13,17 +13,16 @@ def recOnSuffix := "recOn"
def brecOnSuffix := "brecOn"
def binductionOnSuffix := "binductionOn"
def belowSuffix := "below"
def ibelowSuffix := "ibelow"
def mkCasesOnName (indDeclName : Name) : Name := Name.mkStr indDeclName casesOnSuffix
def mkRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName recOnSuffix
def mkBRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName brecOnSuffix
def mkBInductionOnName (indDeclName : Name) : Name := Name.mkStr indDeclName binductionOnSuffix
def mkBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName belowSuffix
def mkIBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName ibelowSuffix
builtin_initialize auxRecExt : TagDeclarationExtension mkTagDeclarationExtension
@[export lean_mark_aux_recursor]
def markAuxRecursor (env : Environment) (declName : Name) : Environment :=
auxRecExt.tag env declName
@@ -51,6 +50,7 @@ def isBRecOnRecursor (env : Environment) (declName : Name) : Bool :=
builtin_initialize noConfusionExt : TagDeclarationExtension mkTagDeclarationExtension
@[export lean_mark_no_confusion]
def markNoConfusion (env : Environment) (n : Name) : Environment :=
noConfusionExt.tag env n

View File

@@ -5,12 +5,12 @@ Authors: Mario Carneiro
-/
prelude
import Lean.Compiler.InitAttr
import Lean.DocString.Extension
import Lean.DocString
namespace Lean
def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
if let some doc findSimpleDocString? ( getEnv) declName (includeBuiltin := false) then
if let some doc findDocString? ( getEnv) declName (includeBuiltin := false) then
declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
if let some declRanges findDeclarationRanges? declName then
declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])

View File

@@ -18,13 +18,6 @@ private opaque getLeancExtraFlags : Unit → String
def getCFlags (leanSysroot : FilePath) : Array String :=
#["-I", (leanSysroot / "include").toString] ++ (getLeancExtraFlags ()).trim.splitOn
@[extern "lean_get_leanc_internal_flags"]
private opaque getLeancInternalFlags : Unit String
/-- Return C compiler flags needed to use the C compiler bundled with the Lean toolchain. -/
def getInternalCFlags (leanSysroot : FilePath) : Array String :=
(getLeancInternalFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
@[extern "lean_get_linker_flags"]
private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
@@ -32,11 +25,4 @@ private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String :=
#["-L", (leanSysroot / "lib" / "lean").toString] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn
@[extern "lean_get_internal_linker_flags"]
private opaque getBuiltinInternalLinkerFlags : Unit String
/-- Return linker flags needed to use the linker bundled with the Lean toolchain. -/
def getInternalLinkerFlags (leanSysroot : FilePath) : Array String :=
(getBuiltinInternalLinkerFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
end Lean.Compiler.FFI

View File

@@ -94,7 +94,7 @@ def emitCInitName (n : Name) : M Unit :=
def shouldExport (n : Name) : Bool :=
-- HACK: exclude symbols very unlikely to be used by the interpreter or other consumers of
-- libleanshared to avoid Windows symbol limit
!(`Lean.Compiler.LCNF).isPrefixOf n && !(`Lean.IR).isPrefixOf n && !(`Lean.Server).isPrefixOf n
!(`Lean.Compiler.LCNF).isPrefixOf n
def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
let ps := decl.params
@@ -499,11 +499,7 @@ def emitLit (z : VarId) (t : IRType) (v : LitVal) : M Unit := do
emitLhs z;
match v with
| LitVal.num v => emitNumLit t v; emitLn ";"
| LitVal.str v =>
emit "lean_mk_string_unchecked(";
emit (quoteString v); emit ", ";
emit v.utf8ByteSize; emit ", ";
emit v.length; emitLn ");"
| LitVal.str v => emit "lean_mk_string_from_bytes("; emit (quoteString v); emit ", "; emit v.utf8ByteSize; emitLn ");"
def emitVDecl (z : VarId) (t : IRType) (v : Expr) : M Unit :=
match v with

View File

@@ -178,14 +178,14 @@ def callLeanUnsignedToNatFn (builder : LLVM.Builder llvmctx)
let nv constIntUnsigned n
LLVM.buildCall2 builder fnty f #[nv] name
def callLeanMkStringUncheckedFn (builder : LLVM.Builder llvmctx)
(strPtr nBytes nChars : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
let fnName := "lean_mk_string_unchecked"
def callLeanMkStringFromBytesFn (builder : LLVM.Builder llvmctx)
(strPtr nBytes : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
let fnName := "lean_mk_string_from_bytes"
let retty LLVM.voidPtrType llvmctx
let argtys := #[ LLVM.voidPtrType llvmctx, LLVM.size_tType llvmctx, LLVM.size_tType llvmctx]
let argtys := #[ LLVM.voidPtrType llvmctx, LLVM.size_tType llvmctx]
let fn getOrCreateFunctionPrototype ( getLLVMModule) retty fnName argtys
let fnty LLVM.functionType retty argtys
LLVM.buildCall2 builder fnty fn #[strPtr, nBytes, nChars] name
LLVM.buildCall2 builder fnty fn #[strPtr, nBytes] name
def callLeanMkString (builder : LLVM.Builder llvmctx)
(strPtr : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
@@ -772,8 +772,7 @@ def emitLit (builder : LLVM.Builder llvmctx)
( LLVM.opaquePointerTypeInContext llvmctx)
str_global #[zero] ""
let nbytes constIntSizeT v.utf8ByteSize
let nchars constIntSizeT v.length
callLeanMkStringUncheckedFn builder strPtr nbytes nchars ""
callLeanMkStringFromBytesFn builder strPtr nbytes ""
LLVM.buildStore builder zv zslot
return zslot

View File

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
-/
prelude
import Lean.Compiler.Options
import Lean.Compiler.ExternAttr
import Lean.Compiler.LCNF.PassManager
import Lean.Compiler.LCNF.Passes
import Lean.Compiler.LCNF.PrettyPrinter

View File

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.PrettyPrinter.Delaborator.Options
import Lean.PrettyPrinter
import Lean.Compiler.LCNF.CompilerM
import Lean.Compiler.LCNF.Internalize

View File

@@ -211,12 +211,12 @@ instance : MonadTrace CoreM where
structure SavedState extends State where
/-- Number of heartbeats passed inside `withRestoreOrSaveFull`, not used otherwise. -/
passedHeartbeats : Nat
passedHearbeats : Nat
deriving Nonempty
def saveState : CoreM SavedState := do
let s get
return { toState := s, passedHeartbeats := 0 }
return { toState := s, passedHearbeats := 0 }
/--
Incremental reuse primitive: if `reusableResult?` is `none`, runs `act` and returns its result
@@ -236,14 +236,14 @@ itself after calling `act` as well as by reuse-handling code such as the one sup
(act : CoreM α) : CoreM (α × SavedState) := do
if let some (val, state) := reusableResult? then
set state.toState
IO.addHeartbeats state.passedHeartbeats.toUInt64
IO.addHeartbeats state.passedHearbeats.toUInt64
return (val, state)
let startHeartbeats IO.getNumHeartbeats
let a act
let s get
let stopHeartbeats IO.getNumHeartbeats
return (a, { toState := s, passedHeartbeats := stopHeartbeats - startHeartbeats })
return (a, { toState := s, passedHearbeats := stopHeartbeats - startHeartbeats })
/-- Restore backtrackable parts of the state. -/
def SavedState.restore (b : SavedState) : CoreM Unit :=
@@ -472,30 +472,23 @@ def Exception.isInterrupt : Exception → Bool
/--
Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
exceptions" these monads, but on `CommandElabM` or, in specific cases, using `tryCatchRuntimeEx`.
See issues #2775 and #2744 as well as `MonadAlwaysExcept`. Also, we never want to catch interrupt
exceptions inside the elaborator.
exceptions" these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as
`MonadAlwaysExcept`. Also, we never want to catch interrupt exceptions inside the elaborator.
-/
@[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception CoreM α) : CoreM α := do
try
x
catch ex =>
if ex.isInterrupt || ex.isRuntime then
throw ex
throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
else
h ex
/--
A variant of `tryCatch` that also catches runtime exception (see also `tryCatch` documentation).
Like `tryCatch`, this function does not catch interrupt exceptions, which are not considered runtime
exceptions.
-/
@[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception CoreM α) : CoreM α := do
try
x
catch ex =>
if ex.isInterrupt then
throw ex
h ex
instance : MonadExceptOf Exception CoreM where
@@ -519,16 +512,4 @@ instance : MonadRuntimeException CoreM where
@[inline] def mapCoreM [MonadControlT CoreM m] [Monad m] (f : forall {α}, CoreM α CoreM α) {α} (x : m α) : m α :=
controlAt CoreM fun runInBase => f <| runInBase x
/--
Returns `true` if the given message kind has not been reported in the message log,
and then mark it as reported. Otherwise, returns `false`.
We use this API to ensure we don't report the same kind of warning multiple times.
-/
def reportMessageKind (kind : Name) : CoreM Bool := do
if ( get).messages.reportedKinds.contains kind then
return false
else
modify fun s => { s with messages.reportedKinds := s.messages.reportedKinds.insert kind }
return true
end Lean

View File

@@ -223,6 +223,8 @@ def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option
instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
getElem m k _ := m.find? k
instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
@[inline] def contains (m : HashMap α β) (a : α) : Bool :=
match m with
| m, _ => m.contains a

View File

@@ -72,6 +72,8 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
getElem xs i _ := xs.get! i
instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
partial def setAux : PersistentArrayNode α USize USize α PersistentArrayNode α
| node cs, i, shift, a =>
let j := div2Shift i shift

View File

@@ -23,13 +23,6 @@ inductive Node (α : Type u) (β : Type v) : Type (max u v) where
| entries (es : Array (Entry α β (Node α β))) : Node α β
| collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node α β
partial def Node.isEmpty : Node α β Bool
| .collision .. => false
| .entries es => es.all fun
| .entry .. => false
| .ref n => n.isEmpty
| .null => true
instance {α β} : Inhabited (Node α β) := Node.entries #[]
abbrev shift : USize := 5
@@ -43,7 +36,8 @@ def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) :=
end PersistentHashMap
structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
root : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
root : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
size : Nat := 0
abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β
@@ -51,8 +45,8 @@ namespace PersistentHashMap
def empty [BEq α] [Hashable α] : PersistentHashMap α β := {}
def isEmpty {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β Bool
| { root } => root.isEmpty
def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool :=
m.size == 0
instance [BEq α] [Hashable α] : Inhabited (PersistentHashMap α β) := {}
@@ -136,7 +130,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
else Entry.ref $ mkCollisionNode k' v' k v
def insert {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β α β PersistentHashMap α β
| { root }, k, v => { root := insertAux root (hash k |>.toUSize) 1 k v }
| { root := n, size := sz }, k, v => { root := insertAux n (hash k |>.toUSize) 1 k v, size := sz + 1 }
partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option β :=
if h : i < keys.size then
@@ -156,11 +150,13 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β
| Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β α Option β
| { root }, k => findAux root (hash k |>.toUSize) k
| { root := n, .. }, k => findAux n (hash k |>.toUSize) k
instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
getElem m i _ := m.find? i
instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
@[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
(m.find? a).getD b₀
@@ -187,7 +183,7 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α
| Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β α Option (α × β)
| { root }, k => findEntryAux root (hash k |>.toUSize) k
| { root := n, .. }, k => findEntryAux n (hash k |>.toUSize) k
partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool :=
if h : i < keys.size then
@@ -206,7 +202,7 @@ partial def containsAux [BEq α] : Node α β → USize → α → Bool
| Node.collision keys vals heq, _, k => containsAtAux keys vals heq 0 k
def contains [BEq α] [Hashable α] : PersistentHashMap α β α Bool
| { root }, k => containsAux root (hash k |>.toUSize) k
| { root := n, .. }, k => containsAux n (hash k |>.toUSize) k
partial def isUnaryEntries (a : Array (Entry α β (Node α β))) (i : Nat) (acc : Option (α × β)) : Option (α × β) :=
if h : i < a.size then
@@ -229,7 +225,7 @@ def isUnaryNode : Node α β → Option (α × β)
else
none
partial def eraseAux [BEq α] : Node α β USize α Node α β
partial def eraseAux [BEq α] : Node α β USize α Node α β × Bool
| n@(Node.collision keys vals heq), _, k =>
match keys.indexOf? k with
| some idx =>
@@ -238,26 +234,28 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
let vals' := vals.feraseIdx (Eq.ndrec idx heq)
have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
have : keys.size - 1 = vals.size - 1 := by rw [heq]
Node.collision keys' vals' (keq.trans (this.trans veq.symm))
| none => n
(Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
| none => (n, false)
| n@(Node.entries entries), h, k =>
let j := (mod2Shift h shift).toNat
let entry := entries.get! j
match entry with
| Entry.null => n
| Entry.null => (n, false)
| Entry.entry k' _ =>
if k == k' then Node.entries (entries.set! j Entry.null) else n
if k == k' then (Node.entries (entries.set! j Entry.null), true) else (n, false)
| Entry.ref node =>
let entries := entries.set! j Entry.null
let newNode := eraseAux node (div2Shift h shift) k
match isUnaryNode newNode with
| none => Node.entries (entries.set! j (Entry.ref newNode))
| some (k, v) => Node.entries (entries.set! j (Entry.entry k v))
let (newNode, deleted) := eraseAux node (div2Shift h shift) k
if !deleted then (n, false)
else match isUnaryNode newNode with
| none => (Node.entries (entries.set! j (Entry.ref newNode)), true)
| some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true)
def erase {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β α PersistentHashMap α β
| { root }, k =>
| { root := n, size := sz }, k =>
let h := hash k |>.toUSize
{ root := eraseAux root h k }
let (n, del) := eraseAux n h k
{ root := n, size := if del then sz - 1 else sz }
section
variable {m : Type w Type w'} [Monad m]
@@ -319,7 +317,7 @@ partial def mapMAux {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Ty
def mapM {α : Type u} {β : Type v} {σ : Type u} {m : Type u Type w} [Monad m] {_ : BEq α} {_ : Hashable α} (pm : PersistentHashMap α β) (f : β m σ) : m (PersistentHashMap α σ) := do
let root mapMAux f pm.root
return { root }
return { pm with root }
def map {α : Type u} {β : Type v} {σ : Type u} {_ : BEq α} {_ : Hashable α} (pm : PersistentHashMap α β) (f : β σ) : PersistentHashMap α σ :=
Id.run <| pm.mapM f

View File

@@ -44,6 +44,9 @@ variable {_ : BEq α} {_ : Hashable α}
@[inline] def contains (s : PersistentHashSet α) (a : α) : Bool :=
s.set.contains a
@[inline] def size (s : PersistentHashSet α) : Nat :=
s.set.size
@[inline] def foldM {β : Type v} {m : Type v Type v} [Monad m] (f : β α m β) (init : β) (s : PersistentHashSet α) : m β :=
s.set.foldlM (init := init) fun d a _ => f d a

View File

@@ -80,10 +80,6 @@ protected def max : RBNode α β → Option (Sigma (fun k => β k))
def singleton (k : α) (v : β k) : RBNode α β :=
node red leaf k v leaf
def isSingleton : RBNode α β Bool
| node _ leaf _ _ leaf => true
| _ => false
-- the first half of Okasaki's `balance`, concerning red-red sequences in the left child
@[inline] def balance1 : RBNode α β (a : α) β a RBNode α β RBNode α β
| node red (node red a kx vx b) ky vy c, kz, vz, d
@@ -273,9 +269,6 @@ variable {α : Type u} {β : Type v} {σ : Type w} {cmp : αα → Ordering
def depth (f : Nat Nat Nat) (t : RBMap α β cmp) : Nat :=
t.val.depth f
def isSingleton (t : RBMap α β cmp) : Bool :=
t.val.isSingleton
@[inline] def fold (f : σ α β σ) : (init : σ) RBMap α β cmp σ
| b, t, _ => t.fold f b

View File

@@ -87,14 +87,15 @@ def switch (m : SMap α β) : SMap α β :=
@[inline] def foldStage2 {σ : Type w} (f : σ α β σ) (s : σ) (m : SMap α β) : σ :=
m.map₂.foldl f s
/-- Monadic fold over a staged map. -/
def foldM {m : Type w Type w} [Monad m]
(f : σ α β m σ) (init : σ) (map : SMap α β) : m σ := do
map.map₂.foldlM f ( map.map₁.foldM f init)
def fold {σ : Type w} (f : σ α β σ) (init : σ) (m : SMap α β) : σ :=
m.map₂.foldl f $ m.map₁.fold f init
def size (m : SMap α β) : Nat :=
m.map₁.size + m.map₂.size
def stageSizes (m : SMap α β) : Nat × Nat :=
(m.map₁.size, m.map₂.size)
def numBuckets (m : SMap α β) : Nat :=
m.map₁.numBuckets

View File

@@ -34,6 +34,9 @@ abbrev switch (s : SSet α) : SSet α :=
abbrev fold (f : σ α σ) (init : σ) (s : SSet α) : σ :=
SMap.fold (fun d a _ => f d a) init s
abbrev size (s : SSet α) : Nat :=
SMap.size s
def toList (m : SSet α) : List α :=
m.fold (init := []) fun es a => a::es

View File

@@ -35,7 +35,7 @@ inductive ReducibilityHints where
| opaque : ReducibilityHints
| abbrev : ReducibilityHints
| regular : UInt32 ReducibilityHints
deriving Inhabited, BEq
deriving Inhabited
@[export lean_mk_reducibility_hints_regular]
def mkReducibilityHintsRegularEx (h : UInt32) : ReducibilityHints :=
@@ -117,7 +117,7 @@ structure DefinitionVal extends ConstantVal where
are compiled using recursors and `WellFounded.fix`.
-/
all : List Name := [name]
deriving Inhabited, BEq
deriving Inhabited
@[export lean_mk_definition_val]
def mkDefinitionValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) (all : List Name) : DefinitionVal := {
@@ -161,13 +161,13 @@ def mkOpaqueValEx (name : Name) (levelParams : List Name) (type : Expr) (value :
structure Constructor where
name : Name
type : Expr
deriving Inhabited, BEq
deriving Inhabited
structure InductiveType where
name : Name
type : Expr
ctors : List Constructor
deriving Inhabited, BEq
deriving Inhabited
/-- Declaration object that can be sent to the kernel. -/
inductive Declaration where
@@ -178,7 +178,7 @@ inductive Declaration where
| quotDecl
| mutualDefnDecl (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` or `partial`
| inductDecl (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool)
deriving Inhabited, BEq
deriving Inhabited
@[export lean_mk_inductive_decl]
def mkInductiveDeclEs (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) : Declaration :=
@@ -189,10 +189,6 @@ def Declaration.isUnsafeInductiveDeclEx : Declaration → Bool
| Declaration.inductDecl _ _ _ isUnsafe => isUnsafe
| _ => false
def Declaration.definitionVal! : Declaration DefinitionVal
| .defnDecl val => val
| _ => panic! "Expected a `Declaration.defnDecl`."
@[specialize] def Declaration.foldExprM {α} {m : Type Type} [Monad m] (d : Declaration) (f : α Expr m α) (a : α) : m α :=
match d with
| Declaration.quotDecl => pure a
@@ -239,10 +235,6 @@ structure InductiveVal extends ConstantVal where
all : List Name
/-- List of the names of the constructors for this inductive datatype. -/
ctors : List Name
/-- Number of auxillary data types produced from nested occurrences.
An inductive definition `T` is nested when there is a constructor with an argument `x : F T`,
where `F : Type → Type` is some suitably behaved (ie strictly positive) function (Eg `Array T`, `List T`, `T × T`, ...). -/
numNested : Nat
/-- `true` when recursive (that is, the inductive type appears as an argument in a constructor). -/
isRec : Bool
/-- Whether the definition is flagged as unsafe. -/
@@ -261,12 +253,14 @@ structure InductiveVal extends ConstantVal where
Section 2.2, Definition 3
-/
isReflexive : Bool
/-- An inductive definition `T` is nested when there is a constructor with an argument `x : F T`,
where `F : Type → Type` is some suitably behaved (ie strictly positive) function (Eg `Array T`, `List T`, `T × T`, ...). -/
isNested : Bool
deriving Inhabited
@[export lean_mk_inductive_val]
def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numParams numIndices : Nat)
(all ctors : List Name) (numNested : Nat) (isRec isUnsafe isReflexive : Bool) : InductiveVal := {
(all ctors : List Name) (isRec isUnsafe isReflexive isNested : Bool) : InductiveVal := {
name := name
levelParams := levelParams
type := type
@@ -274,19 +268,18 @@ def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numP
numIndices := numIndices
all := all
ctors := ctors
numNested := numNested
isRec := isRec
isUnsafe := isUnsafe
isReflexive := isReflexive
isNested := isNested
}
@[export lean_inductive_val_is_rec] def InductiveVal.isRecEx (v : InductiveVal) : Bool := v.isRec
@[export lean_inductive_val_is_unsafe] def InductiveVal.isUnsafeEx (v : InductiveVal) : Bool := v.isUnsafe
@[export lean_inductive_val_is_reflexive] def InductiveVal.isReflexiveEx (v : InductiveVal) : Bool := v.isReflexive
@[export lean_inductive_val_is_nested] def InductiveVal.isNestedEx (v : InductiveVal) : Bool := v.isNested
def InductiveVal.numCtors (v : InductiveVal) : Nat := v.ctors.length
def InductiveVal.isNested (v : InductiveVal) : Bool := v.numNested > 0
def InductiveVal.numTypeFormers (v : InductiveVal) : Nat := v.all.length + v.numNested
structure ConstructorVal extends ConstantVal where
/-- Inductive type this constructor is a member of -/

View File

@@ -4,26 +4,58 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.DocString.Extension
import Lean.Parser.Tactic.Doc
set_option linter.missingDocs true
-- This module contains the main query interface for docstrings, which assembles user-visible
-- docstrings.
-- The module `Lean.DocString.Extension` contains the underlying data.
import Lean.DeclarationRange
import Lean.MonadEnv
import Init.Data.String.Extra
namespace Lean
open Lean.Parser.Tactic.Doc
/--
Finds the docstring for a name, taking tactic alternate forms and documentation extensions into
account.
private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) IO.mkRef {}
private builtin_initialize docStringExt : MapDeclarationExtension String mkMapDeclarationExtension
Use `Lean.findSimpleDocString?` to look up the raw docstring without resolving alternate forms or
including extensions.
-/
def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
let declName := alternativeOfTactic env declName |>.getD declName
let exts := getTacticExtensionString env declName
return ( findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts)
def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
unless ( getEnv).getModuleIdxFor? declName |>.isNone do
throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
match docString? with
| some docString => addDocString declName docString
| none => return ()
def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
if let some docStr := docStringExt.find? env declName then
return some docStr
else if includeBuiltin then
return ( builtinDocStrings.get).find? declName
else
return none
structure ModuleDoc where
doc : String
declarationRange : DeclarationRange
private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) registerSimplePersistentEnvExtension {
addImportedFn := fun _ => {}
addEntryFn := fun s e => s.push e
toArrayFn := fun es => es.toArray
}
def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
moduleDocExt.addEntry env doc
def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
moduleDocExt.getState env
def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
def getDocStringText [Monad m] [MonadError m] [MonadRef m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
match stx.raw[1] with
| Syntax.atom _ val => return val.extract 0 (val.endPos - 2)
| _ => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
end Lean

View File

@@ -1,69 +0,0 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.DeclarationRange
import Lean.MonadEnv
import Init.Data.String.Extra
-- This module contains the underlying data for docstrings, with as few imports as possible, so that
-- docstrings can be saved in as much of the compiler as possible.
-- The module `Lean.DocString` contains the query interface, which needs to look at additional data
-- to construct user-visible docstrings.
namespace Lean
private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) IO.mkRef {}
private builtin_initialize docStringExt : MapDeclarationExtension String mkMapDeclarationExtension
def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
unless ( getEnv).getModuleIdxFor? declName |>.isNone do
throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
match docString? with
| some docString => addDocString declName docString
| none => return ()
/--
Finds a docstring without performing any alias resolution or enrichment with extra metadata.
Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
-/
def findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
if let some docStr := docStringExt.find? env declName then
return some docStr
else if includeBuiltin then
return ( builtinDocStrings.get).find? declName
else
return none
structure ModuleDoc where
doc : String
declarationRange : DeclarationRange
private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) registerSimplePersistentEnvExtension {
addImportedFn := fun _ => {}
addEntryFn := fun s e => s.push e
toArrayFn := fun es => es.toArray
}
def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
moduleDocExt.addEntry env doc
def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
moduleDocExt.getState env
def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
match stx.raw[1] with
| Syntax.atom _ val => return val.extract 0 (val.endPos - 2)
| _ => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"

View File

@@ -50,4 +50,3 @@ import Lean.Elab.ParseImportsFast
import Lean.Elab.GuardMsgs
import Lean.Elab.CheckTactic
import Lean.Elab.MatchExpr
import Lean.Elab.Tactic.Doc

View File

@@ -1292,7 +1292,6 @@ private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level)
funLVals.foldlM (init := acc) fun acc (f, fIdent, fields) => do
let lvals' := toLVals fields (first := true)
let s observing do
checkDeprecated fIdent f
let f addTermInfo fIdent f expectedType?
let e elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit ellipsis
if overloaded then ensureHasType expectedType? e else return e
@@ -1425,27 +1424,8 @@ private def getSuccesses (candidates : Array (TermElabResult Expr)) : TermElabM
return false
return true
| _ => return false
if r₂.size == 0 then
return r₁
if r₂.size == 1 then
return r₂
/-
If there are still more than one solution, discard solutions that have pending metavariables.
We added this extra filter to address regressions introduced after fixing
`isDefEqStuckEx` behavior at `ExprDefEq.lean`.
-/
let r₂ candidates.filterM fun
| .ok _ s => do
try
s.restore
synthesizeSyntheticMVars (postpone := .no)
return true
catch _ =>
return false
| _ => return false
if r₂.size == 0 then
return r₁
return r₂
if r₂.size == 0 then return r₁ else return r₂
/--
Throw an error message that describes why each possible interpretation for the overloaded notation and symbols did not work.
We use a nested error message to aggregate the exceptions produced by each failure.

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