Compare commits

..

2 Commits

Author SHA1 Message Date
Kim Morrison
737a82fc30 chore: basic functionality tests for modify/alter 2024-10-31 10:41:46 +11:00
Kim Morrison
2a85401689 feat: interim implementation of HashMap.modify/alter 2024-10-30 12:05:28 +11:00
611 changed files with 1315 additions and 6948 deletions

View File

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

View File

@@ -1,8 +0,0 @@
version: 2
updates:
- package-ecosystem: "github-actions"
directory: "/"
schedule:
interval: "monthly"
commit-message:
prefix: "chore: CI"

View File

@@ -17,6 +17,6 @@ jobs:
- name: Checkout
uses: actions/checkout@v4
- name: actionlint
uses: raven-actions/actionlint@v2
uses: raven-actions/actionlint@v1
with:
pyflakes: false # we do not use python scripts

View File

@@ -217,7 +217,7 @@ jobs:
"release": true,
"check-level": 2,
"shell": "msys2 {0}",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
// for reasons unknown, interactivetests are flaky on Windows
"CTEST_OPTIONS": "--repeat until-pass:2",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -227,7 +227,7 @@ jobs:
{
"name": "Linux aarch64",
"os": "nscloud-ubuntu-22.04-arm64-4x8",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"release": true,
"check-level": 2,
"shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
@@ -415,10 +415,6 @@ jobs:
- name: Test
id: test
run: |
# give Linux debug unlimited stack, we're not interested in its specific stack usage
if [[ '${{ matrix.name }}' == 'Linux Debug' ]]; then
ulimit -s unlimited
fi
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.check-level >= 1
- name: Test Summary
@@ -496,7 +492,7 @@ jobs:
with:
path: artifacts
- name: Release
uses: softprops/action-gh-release@v2
uses: softprops/action-gh-release@v1
with:
files: artifacts/*/*
fail_on_unmatched_files: true
@@ -540,7 +536,7 @@ jobs:
echo -e "\n*Full commit log*\n" >> diff.md
git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
- name: Release Nightly
uses: softprops/action-gh-release@v2
uses: softprops/action-gh-release@v1
with:
body_path: diff.md
prerelease: true

View File

@@ -112,7 +112,7 @@ jobs:
if: matrix.name == 'Nix Linux'
- name: Check manual for broken links
id: lychee
uses: lycheeverse/lychee-action@v2.0.2
uses: lycheeverse/lychee-action@v1.9.0
with:
fail: false # report errors but do not block CI on temporary failures
# gmplib.org consistently times out from GH actions
@@ -129,7 +129,7 @@ jobs:
python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
- name: Publish manual to Netlify
uses: nwtgck/actions-netlify@v3.0
uses: nwtgck/actions-netlify@v2.0
id: publish-manual
with:
publish-dir: ./dist

View File

@@ -34,7 +34,7 @@ jobs:
- name: Download artifact from the previous workflow.
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
id: download-artifact
uses: dawidd6/action-download-artifact@v6 # https://github.com/marketplace/actions/download-workflow-artifact
uses: dawidd6/action-download-artifact@v2 # https://github.com/marketplace/actions/download-workflow-artifact
with:
run_id: ${{ github.event.workflow_run.id }}
path: artifacts
@@ -60,7 +60,7 @@ jobs:
GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
- name: Release
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: softprops/action-gh-release@v2
uses: softprops/action-gh-release@v1
with:
name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
# There are coredumps files here as well, but all in deeper subdirectories.
@@ -75,7 +75,7 @@ jobs:
- name: Report release status
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: actions/github-script@v7
uses: actions/github-script@v6
with:
script: |
await github.rest.repos.createCommitStatus({
@@ -111,7 +111,7 @@ jobs:
- name: 'Setup jq'
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: dcarbone/install-jq-action@v2.1.0
uses: dcarbone/install-jq-action@v1.0.1
# Check that the most recently nightly coincides with 'git merge-base HEAD master'
- name: Check merge-base and nightly-testing-YYYY-MM-DD
@@ -208,7 +208,7 @@ jobs:
- name: Report mathlib base
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
uses: actions/github-script@v7
uses: actions/github-script@v6
with:
script: |
const description =

View File

@@ -11,7 +11,7 @@ jobs:
stale:
runs-on: ubuntu-latest
steps:
- uses: actions/stale@v9
- uses: actions/stale@v8
with:
days-before-stale: -1
days-before-pr-stale: 30

View File

@@ -8,329 +8,6 @@ This file contains work-in-progress notes for the upcoming release, as well as p
Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
of each version.
v4.15.0
----------
Development in progress.
v4.14.0
----------
Release candidate, release notes will be copied from the branch `releases/v4.14.0` once completed.
v4.13.0
----------
**Full Changelog**: https://github.com/leanprover/lean4/compare/v4.12.0...v4.13.0
### Language features, tactics, and metaprograms
* `structure` command
* [#5511](https://github.com/leanprover/lean4/pull/5511) allows structure parents to be type synonyms.
* [#5531](https://github.com/leanprover/lean4/pull/5531) allows default values for structure fields to be noncomputable.
* `rfl` and `apply_rfl` tactics
* [#3714](https://github.com/leanprover/lean4/pull/3714), [#3718](https://github.com/leanprover/lean4/pull/3718) improve the `rfl` tactic and give better error messages.
* [#3772](https://github.com/leanprover/lean4/pull/3772) makes `rfl` no longer use kernel defeq for ground terms.
* [#5329](https://github.com/leanprover/lean4/pull/5329) tags `Iff.refl` with `@[refl]` (@Parcly-Taxel)
* [#5359](https://github.com/leanprover/lean4/pull/5359) ensures that the `rfl` tactic tries `Iff.rfl` (@Parcly-Taxel)
* `unfold` tactic
* [#4834](https://github.com/leanprover/lean4/pull/4834) let `unfold` do zeta-delta reduction of local definitions, incorporating functionality of the Mathlib `unfold_let` tactic.
* `omega` tactic
* [#5382](https://github.com/leanprover/lean4/pull/5382) fixes spurious error in [#5315](https://github.com/leanprover/lean4/issues/5315)
* [#5523](https://github.com/leanprover/lean4/pull/5523) supports `Int.toNat`
* `simp` tactic
* [#5479](https://github.com/leanprover/lean4/pull/5479) lets `simp` apply rules with higher-order patterns.
* `induction` tactic
* [#5494](https://github.com/leanprover/lean4/pull/5494) fixes `induction`s "pre-tactic" block to always be indented, avoiding unintended uses of it.
* `ac_nf` tactic
* [#5524](https://github.com/leanprover/lean4/pull/5524) adds `ac_nf`, a counterpart to `ac_rfl`, for normalizing expressions with respect to associativity and commutativity. Tests it with `BitVec` expressions.
* `bv_decide`
* [#5211](https://github.com/leanprover/lean4/pull/5211) makes `extractLsb'` the primitive `bv_decide` understands, rather than `extractLsb` (@alexkeizer)
* [#5365](https://github.com/leanprover/lean4/pull/5365) adds `bv_decide` diagnoses.
* [#5375](https://github.com/leanprover/lean4/pull/5375) adds `bv_decide` normalization rules for `ofBool (a.getLsbD i)` and `ofBool a[i]` (@alexkeizer)
* [#5423](https://github.com/leanprover/lean4/pull/5423) enhances the rewriting rules of `bv_decide`
* [#5433](https://github.com/leanprover/lean4/pull/5433) presents the `bv_decide` counterexample at the API
* [#5484](https://github.com/leanprover/lean4/pull/5484) handles `BitVec.ofNat` with `Nat` fvars in `bv_decide`
* [#5506](https://github.com/leanprover/lean4/pull/5506), [#5507](https://github.com/leanprover/lean4/pull/5507) add `bv_normalize` rules.
* [#5568](https://github.com/leanprover/lean4/pull/5568) generalize the `bv_normalize` pipeline to support more general preprocessing passes
* [#5573](https://github.com/leanprover/lean4/pull/5573) gets `bv_normalize` up-to-date with the current `BitVec` rewrites
* Cleanups: [#5408](https://github.com/leanprover/lean4/pull/5408), [#5493](https://github.com/leanprover/lean4/pull/5493), [#5578](https://github.com/leanprover/lean4/pull/5578)
* Elaboration improvements
* [#5266](https://github.com/leanprover/lean4/pull/5266) preserve order of overapplied arguments in `elab_as_elim` procedure.
* [#5510](https://github.com/leanprover/lean4/pull/5510) generalizes `elab_as_elim` to allow arbitrary motive applications.
* [#5283](https://github.com/leanprover/lean4/pull/5283), [#5512](https://github.com/leanprover/lean4/pull/5512) refine how named arguments suppress explicit arguments. Breaking change: some previously omitted explicit arguments may need explicit `_` arguments now.
* [#5376](https://github.com/leanprover/lean4/pull/5376) modifies projection instance binder info for instances, making parameters that are instance implicit in the type be implicit.
* [#5402](https://github.com/leanprover/lean4/pull/5402) localizes universe metavariable errors to `let` bindings and `fun` binders if possible. Makes "cannot synthesize metavariable" errors take precedence over unsolved universe level errors.
* [#5419](https://github.com/leanprover/lean4/pull/5419) must not reduce `ite` in the discriminant of `match`-expression when reducibility setting is `.reducible`
* [#5474](https://github.com/leanprover/lean4/pull/5474) have autoparams report parameter/field on failure
* [#5530](https://github.com/leanprover/lean4/pull/5530) makes automatic instance names about types with hygienic names be hygienic.
* Deriving handlers
* [#5432](https://github.com/leanprover/lean4/pull/5432) makes `Repr` deriving instance handle explicit type parameters
* Functional induction
* [#5364](https://github.com/leanprover/lean4/pull/5364) adds more equalities in context, more careful cleanup.
* Linters
* [#5335](https://github.com/leanprover/lean4/pull/5335) fixes the unused variables linter complaining about match/tactic combinations
* [#5337](https://github.com/leanprover/lean4/pull/5337) fixes the unused variables linter complaining about some wildcard patterns
* Other fixes
* [#4768](https://github.com/leanprover/lean4/pull/4768) fixes a parse error when `..` appears with a `.` on the next line
* Metaprogramming
* [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)
* [#5401](https://github.com/leanprover/lean4/pull/5401) instance for `Inhabited (TacticM α)` (@alexkeizer)
* [#5412](https://github.com/leanprover/lean4/pull/5412) expose Kernel.check for debugging purposes
* [#5556](https://github.com/leanprover/lean4/pull/5556) improves the "invalid projection" type inference error in `inferType`.
* [#5587](https://github.com/leanprover/lean4/pull/5587) allows `MVarId.assertHypotheses` to set `BinderInfo` and `LocalDeclKind`.
* [#5588](https://github.com/leanprover/lean4/pull/5588) adds `MVarId.tryClearMany'`, a variant of `MVarId.tryClearMany`.
### Language server, widgets, and IDE extensions
* [#5205](https://github.com/leanprover/lean4/pull/5205) decreases the latency of auto-completion in tactic blocks.
* [#5237](https://github.com/leanprover/lean4/pull/5237) fixes symbol occurrence highlighting in VS Code not highlighting occurrences when moving the text cursor into the identifier from the right.
* [#5257](https://github.com/leanprover/lean4/pull/5257) fixes several instances of incorrect auto-completions being reported.
* [#5299](https://github.com/leanprover/lean4/pull/5299) allows auto-completion to report completions for global identifiers when the elaborator fails to provide context-specific auto-completions.
* [#5312](https://github.com/leanprover/lean4/pull/5312) fixes the server breaking when changing whitespace after the module header.
* [#5322](https://github.com/leanprover/lean4/pull/5322) fixes several instances of auto-completion reporting non-existent namespaces.
* [#5428](https://github.com/leanprover/lean4/pull/5428) makes sure to always report some recent file range as progress when waiting for elaboration.
### Pretty printing
* [#4979](https://github.com/leanprover/lean4/pull/4979) make pretty printer escape identifiers that are tokens.
* [#5389](https://github.com/leanprover/lean4/pull/5389) makes formatter use the current token table.
* [#5513](https://github.com/leanprover/lean4/pull/5513) use breakable instead of unbreakable whitespace when formatting tokens.
### Library
* [#5222](https://github.com/leanprover/lean4/pull/5222) reduces allocations in `Json.compress`.
* [#5231](https://github.com/leanprover/lean4/pull/5231) upstreams `Zero` and `NeZero`
* [#5292](https://github.com/leanprover/lean4/pull/5292) refactors `Lean.Elab.Deriving.FromToJson` (@arthur-adjedj)
* [#5415](https://github.com/leanprover/lean4/pull/5415) implements `Repr Empty` (@TomasPuverle)
* [#5421](https://github.com/leanprover/lean4/pull/5421) implements `To/FromJSON Empty` (@TomasPuverle)
* Logic
* [#5263](https://github.com/leanprover/lean4/pull/5263) allows simplifying `dite_not`/`decide_not` with only `Decidable (¬p)`.
* [#5268](https://github.com/leanprover/lean4/pull/5268) fixes binders on `ite_eq_left_iff`
* [#5284](https://github.com/leanprover/lean4/pull/5284) turns off `Inhabited (Sum α β)` instances
* [#5355](https://github.com/leanprover/lean4/pull/5355) adds simp lemmas for `LawfulBEq`
* [#5374](https://github.com/leanprover/lean4/pull/5374) add `Nonempty` instances for products, allowing more `partial` functions to elaborate successfully
* [#5447](https://github.com/leanprover/lean4/pull/5447) updates Pi instance names
* [#5454](https://github.com/leanprover/lean4/pull/5454) makes some instance arguments implicit
* [#5456](https://github.com/leanprover/lean4/pull/5456) adds `heq_comm`
* [#5529](https://github.com/leanprover/lean4/pull/5529) moves `@[simp]` from `exists_prop'` to `exists_prop`
* `Bool`
* [#5228](https://github.com/leanprover/lean4/pull/5228) fills gaps in Bool lemmas
* [#5332](https://github.com/leanprover/lean4/pull/5332) adds notation `^^` for Bool.xor
* [#5351](https://github.com/leanprover/lean4/pull/5351) removes `_root_.and` (and or/not/xor) and instead exports/uses `Bool.and` (etc.).
* `BitVec`
* [#5240](https://github.com/leanprover/lean4/pull/5240) removes BitVec simps with complicated RHS
* [#5247](https://github.com/leanprover/lean4/pull/5247) `BitVec.getElem_zeroExtend`
* [#5248](https://github.com/leanprover/lean4/pull/5248) simp lemmas for BitVec, improving confluence
* [#5249](https://github.com/leanprover/lean4/pull/5249) removes `@[simp]` from some BitVec lemmas
* [#5252](https://github.com/leanprover/lean4/pull/5252) changes `BitVec.intMin/Max` from abbrev to def
* [#5278](https://github.com/leanprover/lean4/pull/5278) adds `BitVec.getElem_truncate` (@tobiasgrosser)
* [#5281](https://github.com/leanprover/lean4/pull/5281) adds udiv/umod bitblasting for `bv_decide` (@bollu)
* [#5297](https://github.com/leanprover/lean4/pull/5297) `BitVec` unsigned order theoretic results
* [#5313](https://github.com/leanprover/lean4/pull/5313) adds more basic BitVec ordering theory for UInt
* [#5314](https://github.com/leanprover/lean4/pull/5314) adds `toNat_sub_of_le` (@bollu)
* [#5357](https://github.com/leanprover/lean4/pull/5357) adds `BitVec.truncate` lemmas
* [#5358](https://github.com/leanprover/lean4/pull/5358) introduces `BitVec.setWidth` to unify zeroExtend and truncate (@tobiasgrosser)
* [#5361](https://github.com/leanprover/lean4/pull/5361) some BitVec GetElem lemmas
* [#5385](https://github.com/leanprover/lean4/pull/5385) adds `BitVec.ofBool_[and|or|xor]_ofBool` theorems (@tobiasgrosser)
* [#5404](https://github.com/leanprover/lean4/pull/5404) more of `BitVec.getElem_*` (@tobiasgrosser)
* [#5410](https://github.com/leanprover/lean4/pull/5410) BitVec analogues of `Nat.{mul_two, two_mul, mul_succ, succ_mul}` (@bollu)
* [#5411](https://github.com/leanprover/lean4/pull/5411) `BitVec.toNat_{add,sub,mul_of_lt}` for BitVector non-overflow reasoning (@bollu)
* [#5413](https://github.com/leanprover/lean4/pull/5413) adds `_self`, `_zero`, and `_allOnes` for `BitVec.[and|or|xor]` (@tobiasgrosser)
* [#5416](https://github.com/leanprover/lean4/pull/5416) adds LawCommIdentity + IdempotentOp for `BitVec.[and|or|xor]` (@tobiasgrosser)
* [#5418](https://github.com/leanprover/lean4/pull/5418) decidable quantifers for BitVec
* [#5450](https://github.com/leanprover/lean4/pull/5450) adds `BitVec.toInt_[intMin|neg|neg_of_ne_intMin]` (@tobiasgrosser)
* [#5459](https://github.com/leanprover/lean4/pull/5459) missing BitVec lemmas
* [#5469](https://github.com/leanprover/lean4/pull/5469) adds `BitVec.[not_not, allOnes_shiftLeft_or_shiftLeft, allOnes_shiftLeft_and_shiftLeft]` (@luisacicolini)
* [#5478](https://github.com/leanprover/lean4/pull/5478) adds `BitVec.(shiftLeft_add_distrib, shiftLeft_ushiftRight)` (@luisacicolini)
* [#5487](https://github.com/leanprover/lean4/pull/5487) adds `sdiv_eq`, `smod_eq` to allow `sdiv`/`smod` bitblasting (@bollu)
* [#5491](https://github.com/leanprover/lean4/pull/5491) adds `BitVec.toNat_[abs|sdiv|smod]` (@tobiasgrosser)
* [#5492](https://github.com/leanprover/lean4/pull/5492) `BitVec.(not_sshiftRight, not_sshiftRight_not, getMsb_not, msb_not)` (@luisacicolini)
* [#5499](https://github.com/leanprover/lean4/pull/5499) `BitVec.Lemmas` - drop non-terminal simps (@tobiasgrosser)
* [#5505](https://github.com/leanprover/lean4/pull/5505) unsimps `BitVec.divRec_succ'`
* [#5508](https://github.com/leanprover/lean4/pull/5508) adds `BitVec.getElem_[add|add_add_bool|mul|rotateLeft|rotateRight…` (@tobiasgrosser)
* [#5554](https://github.com/leanprover/lean4/pull/5554) adds `Bitvec.[add, sub, mul]_eq_xor` and `width_one_cases` (@luisacicolini)
* `List`
* [#5242](https://github.com/leanprover/lean4/pull/5242) improve naming for `List.mergeSort` lemmas
* [#5302](https://github.com/leanprover/lean4/pull/5302) provide `mergeSort` comparator autoParam
* [#5373](https://github.com/leanprover/lean4/pull/5373) fix name of `List.length_mergeSort`
* [#5377](https://github.com/leanprover/lean4/pull/5377) upstream `map_mergeSort`
* [#5378](https://github.com/leanprover/lean4/pull/5378) modify signature of lemmas about `mergeSort`
* [#5245](https://github.com/leanprover/lean4/pull/5245) avoid importing `List.Basic` without List.Impl
* [#5260](https://github.com/leanprover/lean4/pull/5260) review of List API
* [#5264](https://github.com/leanprover/lean4/pull/5264) review of List API
* [#5269](https://github.com/leanprover/lean4/pull/5269) remove HashMap's duplicated Pairwise and Sublist
* [#5271](https://github.com/leanprover/lean4/pull/5271) remove @[simp] from `List.head_mem` and similar
* [#5273](https://github.com/leanprover/lean4/pull/5273) lemmas about `List.attach`
* [#5275](https://github.com/leanprover/lean4/pull/5275) reverse direction of `List.tail_map`
* [#5277](https://github.com/leanprover/lean4/pull/5277) more `List.attach` lemmas
* [#5285](https://github.com/leanprover/lean4/pull/5285) `List.count` lemmas
* [#5287](https://github.com/leanprover/lean4/pull/5287) use boolean predicates in `List.filter`
* [#5289](https://github.com/leanprover/lean4/pull/5289) `List.mem_ite_nil_left` and analogues
* [#5293](https://github.com/leanprover/lean4/pull/5293) cleanup of `List.findIdx` / `List.take` lemmas
* [#5294](https://github.com/leanprover/lean4/pull/5294) switch primes on `List.getElem_take`
* [#5300](https://github.com/leanprover/lean4/pull/5300) more `List.findIdx` theorems
* [#5310](https://github.com/leanprover/lean4/pull/5310) fix `List.all/any` lemmas
* [#5311](https://github.com/leanprover/lean4/pull/5311) fix `List.countP` lemmas
* [#5316](https://github.com/leanprover/lean4/pull/5316) `List.tail` lemma
* [#5331](https://github.com/leanprover/lean4/pull/5331) fix implicitness of `List.getElem_mem`
* [#5350](https://github.com/leanprover/lean4/pull/5350) `List.replicate` lemmas
* [#5352](https://github.com/leanprover/lean4/pull/5352) `List.attachWith` lemmas
* [#5353](https://github.com/leanprover/lean4/pull/5353) `List.head_mem_head?`
* [#5360](https://github.com/leanprover/lean4/pull/5360) lemmas about `List.tail`
* [#5391](https://github.com/leanprover/lean4/pull/5391) review of `List.erase` / `List.find` lemmas
* [#5392](https://github.com/leanprover/lean4/pull/5392) `List.fold` / `attach` lemmas
* [#5393](https://github.com/leanprover/lean4/pull/5393) `List.fold` relators
* [#5394](https://github.com/leanprover/lean4/pull/5394) lemmas about `List.maximum?`
* [#5403](https://github.com/leanprover/lean4/pull/5403) theorems about `List.toArray`
* [#5405](https://github.com/leanprover/lean4/pull/5405) reverse direction of `List.set_map`
* [#5448](https://github.com/leanprover/lean4/pull/5448) add lemmas about `List.IsPrefix` (@Command-Master)
* [#5460](https://github.com/leanprover/lean4/pull/5460) missing `List.set_replicate_self`
* [#5518](https://github.com/leanprover/lean4/pull/5518) rename `List.maximum?` to `max?`
* [#5519](https://github.com/leanprover/lean4/pull/5519) upstream `List.fold` lemmas
* [#5520](https://github.com/leanprover/lean4/pull/5520) restore `@[simp]` on `List.getElem_mem` etc.
* [#5521](https://github.com/leanprover/lean4/pull/5521) List simp fixes
* [#5550](https://github.com/leanprover/lean4/pull/5550) `List.unattach` and simp lemmas
* [#5594](https://github.com/leanprover/lean4/pull/5594) induction-friendly `List.min?_cons`
* `Array`
* [#5246](https://github.com/leanprover/lean4/pull/5246) cleanup imports of Array.Lemmas
* [#5255](https://github.com/leanprover/lean4/pull/5255) split Init.Data.Array.Lemmas for better bootstrapping
* [#5288](https://github.com/leanprover/lean4/pull/5288) rename `Array.data` to `Array.toList`
* [#5303](https://github.com/leanprover/lean4/pull/5303) cleanup of `List.getElem_append` variants
* [#5304](https://github.com/leanprover/lean4/pull/5304) `Array.not_mem_empty`
* [#5400](https://github.com/leanprover/lean4/pull/5400) reorganization in Array/Basic
* [#5420](https://github.com/leanprover/lean4/pull/5420) make `Array` functions either semireducible or use structural recursion
* [#5422](https://github.com/leanprover/lean4/pull/5422) refactor `DecidableEq (Array α)`
* [#5452](https://github.com/leanprover/lean4/pull/5452) refactor of Array
* [#5458](https://github.com/leanprover/lean4/pull/5458) cleanup of Array docstrings after refactor
* [#5461](https://github.com/leanprover/lean4/pull/5461) restore `@[simp]` on `Array.swapAt!_def`
* [#5465](https://github.com/leanprover/lean4/pull/5465) improve Array GetElem lemmas
* [#5466](https://github.com/leanprover/lean4/pull/5466) `Array.foldX` lemmas
* [#5472](https://github.com/leanprover/lean4/pull/5472) @[simp] lemmas about `List.toArray`
* [#5485](https://github.com/leanprover/lean4/pull/5485) reverse simp direction for `toArray_concat`
* [#5514](https://github.com/leanprover/lean4/pull/5514) `Array.eraseReps`
* [#5515](https://github.com/leanprover/lean4/pull/5515) upstream `Array.qsortOrd`
* [#5516](https://github.com/leanprover/lean4/pull/5516) upstream `Subarray.empty`
* [#5526](https://github.com/leanprover/lean4/pull/5526) fix name of `Array.length_toList`
* [#5527](https://github.com/leanprover/lean4/pull/5527) reduce use of deprecated lemmas in Array
* [#5534](https://github.com/leanprover/lean4/pull/5534) cleanup of Array GetElem lemmas
* [#5536](https://github.com/leanprover/lean4/pull/5536) fix `Array.modify` lemmas
* [#5551](https://github.com/leanprover/lean4/pull/5551) upstream `Array.flatten` lemmas
* [#5552](https://github.com/leanprover/lean4/pull/5552) switch obvious cases of array "bang"`[]!` indexing to rely on hypothesis (@TomasPuverle)
* [#5577](https://github.com/leanprover/lean4/pull/5577) add missing simp to `Array.size_feraseIdx`
* [#5586](https://github.com/leanprover/lean4/pull/5586) `Array/Option.unattach`
* `Option`
* [#5272](https://github.com/leanprover/lean4/pull/5272) remove @[simp] from `Option.pmap/pbind` and add simp lemmas
* [#5307](https://github.com/leanprover/lean4/pull/5307) restoring Option simp confluence
* [#5354](https://github.com/leanprover/lean4/pull/5354) remove @[simp] from `Option.bind_map`
* [#5532](https://github.com/leanprover/lean4/pull/5532) `Option.attach`
* [#5539](https://github.com/leanprover/lean4/pull/5539) fix explicitness of `Option.mem_toList`
* `Nat`
* [#5241](https://github.com/leanprover/lean4/pull/5241) add @[simp] to `Nat.add_eq_zero_iff`
* [#5261](https://github.com/leanprover/lean4/pull/5261) Nat bitwise lemmas
* [#5262](https://github.com/leanprover/lean4/pull/5262) `Nat.testBit_add_one` should not be a global simp lemma
* [#5267](https://github.com/leanprover/lean4/pull/5267) protect some Nat bitwise theorems
* [#5305](https://github.com/leanprover/lean4/pull/5305) rename Nat bitwise lemmas
* [#5306](https://github.com/leanprover/lean4/pull/5306) add `Nat.self_sub_mod` lemma
* [#5503](https://github.com/leanprover/lean4/pull/5503) restore @[simp] to upstreamed `Nat.lt_off_iff`
* `Int`
* [#5301](https://github.com/leanprover/lean4/pull/5301) rename `Int.div/mod` to `Int.tdiv/tmod`
* [#5320](https://github.com/leanprover/lean4/pull/5320) add `ediv_nonneg_of_nonpos_of_nonpos` to DivModLemmas (@sakehl)
* `Fin`
* [#5250](https://github.com/leanprover/lean4/pull/5250) missing lemma about `Fin.ofNat'`
* [#5356](https://github.com/leanprover/lean4/pull/5356) `Fin.ofNat'` uses `NeZero`
* [#5379](https://github.com/leanprover/lean4/pull/5379) remove some @[simp]s from Fin lemmas
* [#5380](https://github.com/leanprover/lean4/pull/5380) missing Fin @[simp] lemmas
* `HashMap`
* [#5244](https://github.com/leanprover/lean4/pull/5244) (`DHashMap`|`HashMap`|`HashSet`).(`getKey?`|`getKey`|`getKey!`|`getKeyD`)
* [#5362](https://github.com/leanprover/lean4/pull/5362) remove the last use of `Lean.(HashSet|HashMap)`
* [#5369](https://github.com/leanprover/lean4/pull/5369) `HashSet.ofArray`
* [#5370](https://github.com/leanprover/lean4/pull/5370) `HashSet.partition`
* [#5581](https://github.com/leanprover/lean4/pull/5581) `Singleton`/`Insert`/`Union` instances for `HashMap`/`Set`
* [#5582](https://github.com/leanprover/lean4/pull/5582) `HashSet.all`/`any`
* [#5590](https://github.com/leanprover/lean4/pull/5590) adding `Insert`/`Singleton`/`Union` instances for `HashMap`/`Set.Raw`
* [#5591](https://github.com/leanprover/lean4/pull/5591) `HashSet.Raw.all/any`
* `Monads`
* [#5463](https://github.com/leanprover/lean4/pull/5463) upstream some monad lemmas
* [#5464](https://github.com/leanprover/lean4/pull/5464) adjust simp attributes on monad lemmas
* [#5522](https://github.com/leanprover/lean4/pull/5522) more monadic simp lemmas
* Simp lemma cleanup
* [#5251](https://github.com/leanprover/lean4/pull/5251) remove redundant simp annotations
* [#5253](https://github.com/leanprover/lean4/pull/5253) remove Int simp lemmas that can't fire
* [#5254](https://github.com/leanprover/lean4/pull/5254) variables appearing on both sides of an iff should be implicit
* [#5381](https://github.com/leanprover/lean4/pull/5381) cleaning up redundant simp lemmas
### Compiler, runtime, and FFI
* [#4685](https://github.com/leanprover/lean4/pull/4685) fixes a typo in the C `run_new_frontend` signature
* [#4729](https://github.com/leanprover/lean4/pull/4729) has IR checker suggest using `noncomputable`
* [#5143](https://github.com/leanprover/lean4/pull/5143) adds a shared library for Lake
* [#5437](https://github.com/leanprover/lean4/pull/5437) removes (syntactically) duplicate imports (@euprunin)
* [#5462](https://github.com/leanprover/lean4/pull/5462) updates `src/lake/lakefile.toml` to the adjusted Lake build process
* [#5541](https://github.com/leanprover/lean4/pull/5541) removes new shared libs before build to better support Windows
* [#5558](https://github.com/leanprover/lean4/pull/5558) make `lean.h` compile with MSVC (@kant2002)
* [#5564](https://github.com/leanprover/lean4/pull/5564) removes non-conforming size-0 arrays (@eric-wieser)
### Lake
* Reservoir build cache. Lake will now attempt to fetch a pre-built copy of the package from Reservoir before building it. This is only enabled for packages in the leanprover or leanprover-community organizations on versions indexed by Reservoir. Users can force Lake to build packages from the source by passing --no-cache on the CLI or by setting the LAKE_NO_CACHE environment variable to true. [#5486](https://github.com/leanprover/lean4/pull/5486), [#5572](https://github.com/leanprover/lean4/pull/5572), [#5583](https://github.com/leanprover/lean4/pull/5583), [#5600](https://github.com/leanprover/lean4/pull/5600), [#5641](https://github.com/leanprover/lean4/pull/5641), [#5642](https://github.com/leanprover/lean4/pull/5642).
* [#5504](https://github.com/leanprover/lean4/pull/5504) lake new and lake init now produce TOML configurations by default.
* [#5878](https://github.com/leanprover/lean4/pull/5878) fixes a serious issue where Lake would delete path dependencies when attempting to cleanup a dependency required with an incorrect name.
* **Breaking changes**
* [#5641](https://github.com/leanprover/lean4/pull/5641) A Lake build of target within a package will no longer build a package's dependencies package-level extra target dependencies. At the technical level, a package's extraDep facet no longer transitively builds its dependencies extraDep facets (which include their extraDepTargets).
### Documentation fixes
* [#3918](https://github.com/leanprover/lean4/pull/3918) `@[builtin_doc]` attribute (@digama0)
* [#4305](https://github.com/leanprover/lean4/pull/4305) explains the borrow syntax (@eric-wieser)
* [#5349](https://github.com/leanprover/lean4/pull/5349) adds documentation for `groupBy.loop` (@vihdzp)
* [#5473](https://github.com/leanprover/lean4/pull/5473) fixes typo in `BitVec.mul` docstring (@llllvvuu)
* [#5476](https://github.com/leanprover/lean4/pull/5476) fixes typos in `Lean.MetavarContext`
* [#5481](https://github.com/leanprover/lean4/pull/5481) removes mention of `Lean.withSeconds` (@alexkeizer)
* [#5497](https://github.com/leanprover/lean4/pull/5497) updates documentation and tests for `toUIntX` functions (@TomasPuverle)
* [#5087](https://github.com/leanprover/lean4/pull/5087) mentions that `inferType` does not ensure type correctness
* Many fixes to spelling across the doc-strings, (@euprunin): [#5425](https://github.com/leanprover/lean4/pull/5425) [#5426](https://github.com/leanprover/lean4/pull/5426) [#5427](https://github.com/leanprover/lean4/pull/5427) [#5430](https://github.com/leanprover/lean4/pull/5430) [#5431](https://github.com/leanprover/lean4/pull/5431) [#5434](https://github.com/leanprover/lean4/pull/5434) [#5435](https://github.com/leanprover/lean4/pull/5435) [#5436](https://github.com/leanprover/lean4/pull/5436) [#5438](https://github.com/leanprover/lean4/pull/5438) [#5439](https://github.com/leanprover/lean4/pull/5439) [#5440](https://github.com/leanprover/lean4/pull/5440) [#5599](https://github.com/leanprover/lean4/pull/5599)
### Changes to CI
* [#5343](https://github.com/leanprover/lean4/pull/5343) allows addition of `release-ci` label via comment (@thorimur)
* [#5344](https://github.com/leanprover/lean4/pull/5344) sets check level correctly during workflow (@thorimur)
* [#5444](https://github.com/leanprover/lean4/pull/5444) Mathlib's `lean-pr-testing-NNNN` branches should use Batteries' `lean-pr-testing-NNNN` branches
* [#5489](https://github.com/leanprover/lean4/pull/5489) commit `lake-manifest.json` when updating `lean-pr-testing` branches
* [#5490](https://github.com/leanprover/lean4/pull/5490) use separate secrets for commenting and branching in `pr-release.yml`
v4.12.0
----------

View File

@@ -1,6 +1,6 @@
These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](../dev/index.md).
These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](doc/dev/index.md).
We strongly suggest that new users instead follow the [Quickstart](../quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
We strongly suggest that new users instead follow the [Quickstart](doc/quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
Requirements
------------

View File

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

View File

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

View File

@@ -10,7 +10,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 15)
set(LEAN_VERSION_MINOR 12)
set(LEAN_VERSION_PATCH 0)
set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

View File

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

View File

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

View File

@@ -235,11 +235,9 @@ def range (n : Nat) : Array Nat :=
def singleton (v : α) : Array α :=
mkArray 1 v
def back! [Inhabited α] (a : Array α) : α :=
def back [Inhabited α] (a : Array α) : α :=
a.get! (a.size - 1)
@[deprecated back! (since := "2024-10-31")] abbrev back := @back!
def get? (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some a[i] else none
@@ -304,6 +302,37 @@ def modifyOp (self : Array α) (idx : Nat) (f : αα) : Array α :=
We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < usizeSz` to true. -/
@[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (b : β) (f : α β m (ForInStep β)) : m β :=
let sz := as.usize
let rec @[specialize] loop (i : USize) (b : β) : m β := do
if i < sz then
let a := as.uget i lcProof
match ( f a b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop (i+1) b
else
pure b
loop 0 b
/-- Reference implementation for `forIn` -/
@[implemented_by Array.forInUnsafe]
protected def forIn {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (b : β) (f : α β m (ForInStep β)) : m β :=
let rec loop (i : Nat) (h : i as.size) (b : β) : m β := do
match i, h with
| 0, _ => pure b
| i+1, h =>
have h' : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
have : as.size - 1 < as.size := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
match ( f as[as.size - 1 - i] b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop i (Nat.le_of_lt h') b
loop as.size (Nat.le_refl _) b
instance : ForIn m (Array α) α where
forIn := Array.forIn
/-- See comment at `forInUnsafe` -/
@[inline] unsafe def forIn'Unsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) a as β m (ForInStep β)) : m β :=
let sz := as.usize
let rec @[specialize] loop (i : USize) (b : β) : m β := do
@@ -334,9 +363,7 @@ protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
instance : ForIn' m (Array α) α inferInstance where
forIn' := Array.forIn'
-- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
/-- See comment at `forIn'Unsafe` -/
/-- See comment at `forInUnsafe` -/
@[inline]
unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (f : β α m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β :=
let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do
@@ -371,7 +398,7 @@ def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β
else
fold as.size (Nat.le_refl _)
/-- See comment at `forIn'Unsafe` -/
/-- See comment at `forInUnsafe` -/
@[inline]
unsafe def foldrMUnsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (f : α β m β) (init : β) (as : Array α) (start := as.size) (stop := 0) : m β :=
let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do
@@ -410,7 +437,7 @@ def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
else
pure init
/-- See comment at `forIn'Unsafe` -/
/-- See comment at `forInUnsafe` -/
@[inline]
unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (f : α m β) (as : Array α) : m (Array β) :=
let sz := as.usize
@@ -866,7 +893,6 @@ def zip (as : Array α) (bs : Array β) : Array (α × β) :=
def unzip (as : Array (α × β)) : Array α × Array β :=
as.foldl (init := (#[], #[])) fun (as, bs) (a, b) => (as.push a, bs.push b)
@[deprecated partition (since := "2024-11-06")]
def split (as : Array α) (p : α Bool) : Array α × Array α :=
as.foldl (init := (#[], #[])) fun (as, bs) a =>
if p a then (as.push a, bs) else (as, bs.push a)

View File

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

View File

@@ -23,7 +23,7 @@ theorem foldlM_eq_foldlM_toList.aux [Monad m]
· cases Nat.not_le_of_gt _ (Nat.zero_add _ H)
· rename_i i; rw [Nat.succ_add] at H
simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
rw (occs := .pos [2]) [ List.getElem_cons_drop_succ_eq_drop _]
rw (config := {occs := .pos [2]}) [ List.get_drop_eq_drop _ _ _]
rfl
· rw [List.drop_of_length_le (Nat.ge_of_not_lt _)]; rfl

View File

@@ -13,9 +13,9 @@ import Init.ByCases
namespace Array
theorem rel_of_isEqvAux
{r : α α Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i a.size)
(r : α α Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i a.size)
(heqv : Array.isEqvAux a b hsz r i hi)
{j : Nat} (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz hi))) := by
(j : Nat) (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz hi))) := by
induction i with
| zero => contradiction
| succ i ih =>
@@ -28,7 +28,7 @@ theorem rel_of_isEqvAux
subst hj'
exact heqv.left
theorem isEqvAux_of_rel {r : α α Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i a.size)
theorem isEqvAux_of_rel (r : α α Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i a.size)
(w : j, (hj : j < i) r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz hi)))) : Array.isEqvAux a b hsz r i hi := by
induction i with
| zero => simp [Array.isEqvAux]
@@ -36,18 +36,18 @@ theorem isEqvAux_of_rel {r : αα → Bool} {a b : Array α} (hsz : a.size
simp only [isEqvAux, Bool.and_eq_true]
exact w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)
theorem rel_of_isEqv {r : α α Bool} {a b : Array α} :
theorem rel_of_isEqv (r : α α Bool) (a b : Array α) :
Array.isEqv a b r h : a.size = b.size, (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h h')) := by
simp only [isEqv]
split <;> rename_i h
· exact fun h' => h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'
· exact fun h' => h, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'
· intro; contradiction
theorem isEqv_iff_rel (a b : Array α) (r) :
Array.isEqv a b r h : a.size = b.size, (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h h')) :=
rel_of_isEqv, fun h, w => by
rel_of_isEqv r a b, fun h, w => by
simp only [isEqv, h, reduceDIte]
exact isEqvAux_of_rel h (by simp [h]) w
exact isEqvAux_of_rel r a b h a.size (by simp [h]) w
theorem isEqv_eq_decide (a b : Array α) (r) :
Array.isEqv a b r =
@@ -67,7 +67,7 @@ theorem isEqv_eq_decide (a b : Array α) (r) :
simp [isEqv_eq_decide, List.isEqv_eq_decide]
theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
have h, h' := rel_of_isEqv h
have h, h' := rel_of_isEqv (fun x y => x = y) a b h
exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
theorem isEqvAux_self (r : α α Bool) (hr : a, r a a) (a : Array α) (i : Nat) (h : i a.size) :

View File

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

View File

@@ -10,11 +10,7 @@ import Init.Data.List.Monadic
import Init.Data.List.Range
import Init.Data.List.Nat.TakeDrop
import Init.Data.List.Nat.Modify
import Init.Data.List.Nat.Erase
import Init.Data.List.Monadic
import Init.Data.List.OfFn
import Init.Data.Array.Mem
import Init.Data.Array.DecidableEq
import Init.TacticsExtra
/-!
@@ -73,9 +69,6 @@ theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size)
rfl
· simp [getElem?_eq_none_iff.2 (by simpa using h)]
theorem singleton_inj : #[a] = #[b] a = b := by
simp
end Array
namespace List
@@ -108,8 +101,27 @@ We prefer to pull `List.toArray` outwards.
@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
@[simp] theorem back_toArray [Inhabited α] (l : List α) : l.toArray.back = l.getLast! := by
simp only [back, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
@[simp] theorem forIn_loop_toArray [Monad m] (l : List α) (f : α β m (ForInStep β)) (i : Nat)
(h : i l.length) (b : β) :
Array.forIn.loop l.toArray f i h b = (l.drop (l.length - i)).forIn b f := by
induction i generalizing l b with
| zero => simp [Array.forIn.loop]
| succ i ih =>
simp only [Array.forIn.loop, size_toArray, getElem_toArray, ih, forIn_eq_forIn]
rw [Nat.sub_add_eq, List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
simp only [Option.toList_some, singleton_append, forIn_cons]
have t : l.length - 1 - i = l.length - i - 1 := by omega
simp only [t]
congr
@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α β m (ForInStep β)) :
forIn l.toArray b f = forIn l b f := by
change l.toArray.forIn b f = l.forIn b f
rw [Array.forIn, forIn_loop_toArray]
simp
@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) a l.toArray β m (ForInStep β)) (i : Nat)
(h : i l.length) (b : β) :
@@ -119,7 +131,7 @@ We prefer to pull `List.toArray` outwards.
| zero =>
simp [Array.forIn'.loop]
| succ i ih =>
simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]
simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih, forIn_eq_forIn]
have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
simp only [Nat.sub_add_eq]
rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
@@ -133,11 +145,7 @@ We prefer to pull `List.toArray` outwards.
forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
change Array.forIn' _ _ _ = List.forIn' _ _ _
rw [Array.forIn', forIn'_loop_toArray]
simp
@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α β m (ForInStep β)) :
forIn l.toArray b f = forIn l b f := by
simpa using forIn'_toArray l b fun a m b => f a b
simp [List.forIn_eq_forIn]
theorem foldrM_toArray [Monad m] (f : α β m β) (init : β) (l : List α) :
l.toArray.foldrM f init = l.foldrM f init := by
@@ -214,25 +222,17 @@ theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array
(arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
simp [foldrM_eq_reverse_foldlM_toList, -size_push]
/--
Variant of `foldrM_push` with `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
-/
@[simp] theorem foldrM_push' [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α)
{start} (h : start = arr.size + 1) :
(arr.push a).foldrM f init start = f a init >>= arr.foldrM f := by
simp [ foldrM_push, h]
/-- Variant of `foldrM_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
@[simp] theorem foldrM_push' [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
simp [ foldrM_push]
theorem foldr_push (f : α β β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
/--
Variant of `foldr_push` with the `h : start = arr.size + 1`
rather than `(arr.push a).size` as the argument.
-/
@[simp] theorem foldr_push' (f : α β β) (init : β) (arr : Array α) (a : α) {start}
(h : start = arr.size + 1) : (arr.push a).foldr f init start = arr.foldr f (f a init) :=
foldrM_push' _ _ _ _ h
/-- Variant of `foldr_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
@[simp] theorem foldr_push' (f : α β β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
/-- A more efficient version of `arr.toList.reverse`. -/
@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
@@ -247,7 +247,7 @@ where
aux (i r) :
mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
unfold mapM.map; split
· rw [ List.getElem_cons_drop_succ_eq_drop _]
· rw [ List.get_drop_eq_drop _ i _]
simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
pure_bind]
rfl
@@ -506,14 +506,13 @@ theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < a
cases as
simp [List.getElem?_eq_some_iff]
theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by
simp only [back!, get!_eq_getElem?, get?_eq_getElem?, back?]
@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
simp only [back, get!_eq_getElem?, get?_eq_getElem?, back?]
@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
simp [back?, getElem?_eq_getElem?_toList]
@[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
simp [back!_eq_back?]
theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
(a.push x)[i]? = some a[i] := by
@@ -626,8 +625,8 @@ theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] :=
· simp [h]
· intros; contradiction
theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size 0) :
as = as.pop.push as.back! := by
theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size 0) :
as = as.pop.push as.back := by
apply ext
· simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
· intros i h h'
@@ -636,12 +635,12 @@ theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as
else
have heq : i = as.pop.size :=
Nat.le_antisymm (size_pop .. Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
cases heq; rw [getElem_push_eq, back!, size_pop, get!_eq_getD, getD, dif_pos h]; rfl
cases heq; rw [getElem_push_eq, back, size_pop, get!_eq_getD, getD, dif_pos h]; rfl
theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size 0) :
(bs : Array α) (c : α), as = bs.push c :=
let _ : Inhabited α := as[0]
as.pop, as.back!, eq_push_pop_back!_of_size_ne_zero h
as.pop, as.back, eq_push_pop_back_of_size_ne_zero h
theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl
@@ -714,43 +713,6 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
true_and, Nat.not_lt] at h
rw [List.getElem?_eq_none_iff.2 _, List.getElem?_eq_none_iff.2 (a.toList.length_reverse _)]
/-! ### BEq -/
@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ReflBEq α := by
constructor
· intro h
constructor
intro a
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
apply Array.isEqv_self_beq
@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) LawfulBEq α := by
constructor
· intro h
constructor
· intro a b h
apply singleton_inj.1
apply eq_of_beq
simp only [instBEq, isEqv, isEqvAux]
simpa
· intro a
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
· intro a b h
obtain hs, hi := rel_of_isEqv h
ext i h₁ h₂
· exact hs
· simpa using hi _ h₁
· intro a
apply Array.isEqv_self_beq
/-! ### take -/
@[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by
@@ -910,7 +872,7 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
obtain m, eq, w := t
· refine m, by simpa [map_eq_foldl] using eq, ?_
intro i h
simp only [eq] at w
simp [eq] at w
specialize w i, h h
simpa [map_eq_foldl] using w
· exact h0, rfl, nofun
@@ -1461,10 +1423,6 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
· split <;> simp_all
· split <;> simp_all
theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
a.feraseIdx i = a.eraseIdx i.1 := by
simp [eraseIdx]
end Array
open Array
@@ -1616,98 +1574,13 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
apply ext'
simp
@[simp] theorem extract_toArray (l : List α) (start stop : Nat) :
@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
apply ext'
simp
@[simp] theorem toArray_ofFn (f : Fin n α) : (ofFn f).toArray = Array.ofFn f := by
ext <;> simp
theorem takeWhile_go_succ (p : α Bool) (a : α) (l : List α) (i : Nat) :
takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
rw [takeWhile.go, takeWhile.go]
simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
getElem_toArray, getElem_cons_succ]
split
rw [takeWhile_go_succ]
rfl
theorem takeWhile_go_toArray (p : α Bool) (l : List α) (i : Nat) :
Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
induction l generalizing i r with
| nil => simp [takeWhile.go]
| cons a l ih =>
rw [takeWhile.go]
cases i with
| zero =>
simp [takeWhile_go_succ, ih, takeWhile_cons]
split <;> simp
| succ i =>
simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
getElem_toArray, getElem_cons_succ, drop_succ_cons]
split <;> rename_i h₁
· rw [takeWhile_go_succ, ih]
rw [ getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
split <;> simp_all
· simp_all [drop_eq_nil_of_le]
@[simp] theorem takeWhile_toArray (p : α Bool) (l : List α) :
l.toArray.takeWhile p = (l.takeWhile p).toArray := by
simp [Array.takeWhile, takeWhile_go_toArray]
@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
rw [feraseIdx]
split <;> rename_i h
· rw [feraseIdx_toArray]
simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
simp
· rcases i with i, w
simp at h w
have t : i = l.length - 1 := by omega
simp [t]
termination_by l.length - i
decreasing_by
rename_i h
simp at h
simp
omega
@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
rw [Array.eraseIdx]
split
· simp
· simp_all [eraseIdx_eq_self.2]
end List
namespace Array
@[simp] theorem mapM_id {l : Array α} {f : α Id β} : l.mapM f = l.map f := by
induction l; simp_all
@[simp] theorem toList_ofFn (f : Fin n α) : (Array.ofFn f).toList = List.ofFn f := by
apply List.ext_getElem <;> simp
@[simp] theorem toList_takeWhile (p : α Bool) (as : Array α) :
(as.takeWhile p).toList = as.toList.takeWhile p := by
induction as; simp
@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
(as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
induction as
simp
@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
(as.eraseIdx i).toList = as.toList.eraseIdx i := by
induction as
simp
end Array
/-! ### Deprecations -/
namespace List
@@ -1721,8 +1594,6 @@ theorem toArray_concat {as : List α} {x : α} :
apply ext'
simp
@[deprecated back!_toArray (since := "2024-10-31")] abbrev back_toArray := @back!_toArray
end List
namespace Array
@@ -1863,9 +1734,4 @@ abbrev get_swap := @getElem_swap
@[deprecated getElem_swap' (since := "2024-09-30")]
abbrev get_swap' := @getElem_swap'
@[deprecated back!_eq_back? (since := "2024-10-31")] abbrev back_eq_back? := @back!_eq_back?
@[deprecated back!_push (since := "2024-10-31")] abbrev back_push := @back!_push
@[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
end Array

View File

@@ -60,10 +60,6 @@ theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
split <;> simp_all
@[simp] theorem toList_mapFinIdx (a : Array α) (f : Fin a.size α β) :
(a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a => f i, by simp a) := by
apply List.ext_getElem <;> simp
/-! ### mapIdx -/
theorem mapIdx_induction (as : Array α) (f : Nat α β)
@@ -93,20 +89,4 @@ theorem mapIdx_spec (as : Array α) (f : Nat → α → β)
a[i]?.map (f i) := by
simp [getElem?_def, size_mapIdx, getElem_mapIdx]
@[simp] theorem toList_mapIdx (a : Array α) (f : Nat α β) :
(a.mapIdx f).toList = a.toList.mapIdx (fun i a => f i a) := by
apply List.ext_getElem <;> simp
end Array
namespace List
@[simp] theorem mapFinIdx_toArray (l : List α) (f : Fin l.length α β) :
l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
ext <;> simp
@[simp] theorem mapIdx_toArray (l : List α) (f : Nat α β) :
l.toArray.mapIdx f = (l.mapIdx f).toArray := by
ext <;> simp
end List

View File

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

View File

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

View File

@@ -1792,7 +1792,7 @@ theorem setWidth_succ (x : BitVec w) :
· simp_all
· omega
@[deprecated "Use the reverse direction of `cons_msb_setWidth`" (since := "2024-09-23")]
@[deprecated "Use the reverse direction of `cons_msb_setWidth`"]
theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
simp
@@ -2026,9 +2026,9 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
@[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
@[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
rfl
theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
@[simp] theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
rfl
-- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
@@ -2146,6 +2146,19 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
omega
/-! ### abs -/
theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
@[simp, bv_toNat]
theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
simp only [BitVec.abs, neg_eq]
by_cases h : x.msb = true
· simp only [h, reduceIte, toNat_neg]
have : 2 * x.toNat 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
rw [Nat.mod_eq_of_lt (by omega)]
· simp [h]
/-! ### mul -/
theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
@@ -2886,14 +2899,6 @@ theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) :=
simp only [intMin, getLsbD_twoPow, boolToPropSimps]
omega
theorem getMsbD_intMin {w i : Nat} :
(intMin w).getMsbD i = (decide (0 < w) && decide (i = 0)) := by
simp only [getMsbD, getLsbD_intMin]
match w, i with
| 0, _ => simp
| w+1, 0 => simp
| w+1, i+1 => simp; omega
/--
The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
-/
@@ -2916,21 +2921,6 @@ theorem toInt_intMin {w : Nat} :
rw [Nat.mul_comm]
simp [w_pos]
theorem toInt_intMin_le (x : BitVec w) :
(intMin w).toInt x.toInt := by
cases w
case zero => simp [@of_length_zero x]
case succ w =>
simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
have : 0 < 2 ^ w := Nat.two_pow_pos w
rw [Int.emod_eq_of_lt (by omega) (by omega)]
rw [BitVec.toInt_eq_toNat_bmod]
rw [show (2 ^ w : Nat) = ((2 ^ (w + 1) : Nat) : Int) / 2 by omega]
apply Int.le_bmod (by omega)
theorem intMin_sle (x : BitVec w) : (intMin w).sle x := by
simp only [BitVec.sle, toInt_intMin_le x, decide_True]
@[simp]
theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
by_cases h : 0 < w
@@ -2938,10 +2928,6 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
· simp only [Nat.not_lt, Nat.le_zero_eq] at h
simp [bv_toNat, h]
@[simp]
theorem abs_intMin {w : Nat} : (intMin w).abs = intMin w := by
simp [BitVec.abs, bv_toNat]
theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x intMin w) :
(-x).toInt = -(x.toInt) := by
simp only [ne_eq, toNat_eq, toNat_intMin] at rs
@@ -2958,10 +2944,6 @@ theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
have := @Nat.two_pow_pred_mul_two w (by omega)
split <;> split <;> omega
theorem msb_intMin {w : Nat} : (intMin w).msb = decide (0 < w) := by
simp only [msb_eq_decide, toNat_intMin, decide_eq_decide]
by_cases h : 0 < w <;> simp_all
/-! ### intMax -/
/-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
@@ -3054,38 +3036,6 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
omega
/-! ### neg -/
theorem msb_eq_toInt {x : BitVec w}:
x.msb = decide (x.toInt < 0) := by
by_cases h : x.msb <;>
· simp [h, toInt_eq_msb_cond]
omega
theorem msb_eq_toNat {x : BitVec w}:
x.msb = decide (x.toNat 2 ^ (w - 1)) := by
simp only [msb_eq_decide, ge_iff_le]
/-! ### abs -/
theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
@[simp, bv_toNat]
theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
simp only [BitVec.abs, neg_eq]
by_cases h : x.msb = true
· simp only [h, reduceIte, toNat_neg]
have : 2 * x.toNat 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
rw [Nat.mod_eq_of_lt (by omega)]
· simp [h]
theorem getLsbD_abs {i : Nat} {x : BitVec w} :
getLsbD x.abs i = if x.msb then getLsbD (-x) i else getLsbD x i := by
by_cases h : x.msb <;> simp [BitVec.abs, h]
theorem getMsbD_abs {i : Nat} {x : BitVec w} :
getMsbD (x.abs) i = if x.msb then getMsbD (-x) i else getMsbD x i := by
by_cases h : x.msb <;> simp [BitVec.abs, h]
/-! ### Decidable quantifiers -/

View File

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

View File

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

View File

@@ -1267,7 +1267,7 @@ theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2 := by
_ = ((m + 1 - 2) + 2)/2 := by simp
_ = (m - 1) / 2 + 1 := by
rw [add_ediv_of_dvd_right]
· simp +decide only [Int.ediv_self]
· simp (config := {decide := true}) only [Int.ediv_self]
congr 2
rw [Int.add_sub_assoc, Int.sub_neg]
congr
@@ -1285,7 +1285,7 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
simp only [bmod, ofNat_eq_coe, natAbs_ofNat, natCast_add, ofNat_one,
emod_self_add_one (ofNat_nonneg x)]
match x with
| 0 => rw [if_pos] <;> simp +decide
| 0 => rw [if_pos] <;> simp (config := {decide := true})
| (x+1) =>
rw [if_neg]
· simp [ Int.sub_sub]

View File

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

View File

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

View File

@@ -169,13 +169,6 @@ theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Li
(H : (a : α), a xs P a) : xs.pmap f H [] xs [] := by
simp
theorem pmap_eq_self {l : List α} {p : α Prop} (hp : (a : α), a l p a)
(f : (a : α) p a α) : l.pmap f hp = l a (h : a l), f a (hp a h) = a := by
rw [pmap_eq_map_attach]
conv => lhs; rhs; rw [ attach_map_subtype_val l]
rw [map_inj_left]
simp
@[simp]
theorem attach_eq_nil_iff {l : List α} : l.attach = [] l = [] :=
pmap_eq_nil_iff

View File

@@ -45,7 +45,7 @@ The operations are organized as follow:
* Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
* Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
* Minima and maxima: `min?` and `max?`.
* Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `splitBy`,
* Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `groupBy`,
`removeAll`
(currently these functions are mostly only used in meta code,
and do not have API suitable for verification).
@@ -1639,23 +1639,23 @@ where
| true => loop as (a::rs)
| false => (rs.reverse, a::as)
/-! ### splitBy -/
/-! ### groupBy -/
/--
`O(|l|)`. `splitBy R l` splits `l` into chains of elements
`O(|l|)`. `groupBy R l` splits `l` into chains of elements
such that adjacent elements are related by `R`.
* `splitBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
* `splitBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
* `groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
* `groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
-/
@[specialize] def splitBy (R : α α Bool) : List α List (List α)
@[specialize] def groupBy (R : α α Bool) : List α List (List α)
| [] => []
| a::as => loop as a [] []
where
/--
The arguments of `splitBy.loop l ag g gs` represent the following:
The arguments of `groupBy.loop l ag g gs` represent the following:
- `l : List α` are the elements which we still need to split.
- `l : List α` are the elements which we still need to group.
- `ag : α` is the previous element for which a comparison was performed.
- `g : List α` is the group currently being assembled, in **reverse order**.
- `gs : List (List α)` is all of the groups that have been completed, in **reverse order**.
@@ -1666,8 +1666,6 @@ where
| false => loop as a [] ((ag::g).reverse::gs)
| [], ag, g, gs => ((ag::g).reverse::gs).reverse
@[deprecated splitBy (since := "2024-10-30"), inherit_doc splitBy] abbrev groupBy := @splitBy
/-! ### removeAll -/
/-- `O(|xs|)`. Computes the "set difference" of lists,

View File

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

View File

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

View File

@@ -179,7 +179,7 @@ theorem IsPrefix.findSome?_eq_some {l₁ l₂ : List α} {f : α → Option β}
List.findSome? f l₁ = some b List.findSome? f l₂ = some b := by
rw [IsPrefix] at h
obtain t, rfl := h
simp +contextual [findSome?_append]
simp (config := {contextual := true}) [findSome?_append]
theorem IsPrefix.findSome?_eq_none {l₁ l₂ : List α} {f : α Option β} (h : l₁ <+: l₂) :
List.findSome? f l₂ = none List.findSome? f l₁ = none :=
@@ -436,7 +436,7 @@ theorem IsPrefix.find?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁
List.find? p l₁ = some b List.find? p l₂ = some b := by
rw [IsPrefix] at h
obtain t, rfl := h
simp +contextual [find?_append]
simp (config := {contextual := true}) [find?_append]
theorem IsPrefix.find?_eq_none {l₁ l₂ : List α} {p : α Bool} (h : l₁ <+: l₂) :
List.find? p l₂ = none List.find? p l₁ = none :=
@@ -562,7 +562,7 @@ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs
| inr e =>
have ipm := Nat.succ_pred_eq_of_pos e
have ilt := Nat.le_trans ho (findIdx_le_length p)
simp +singlePass only [ ipm, getElem_cons_succ]
simp (config := { singlePass := true }) only [ ipm, getElem_cons_succ]
rw [ ipm, Nat.succ_lt_succ_iff] at h
simpa using ih h

View File

@@ -23,7 +23,7 @@ namespace List
The following operations are already tail-recursive, and do not need `@[csimp]` replacements:
`get`, `foldl`, `beq`, `isEqv`, `reverse`, `elem` (and hence `contains`), `drop`, `dropWhile`,
`partition`, `isPrefixOf`, `isPrefixOf?`, `find?`, `findSome?`, `lookup`, `any` (and hence `or`),
`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `splitBy`.
`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `groupBy`.
The following operations are still missing `@[csimp]` replacements:
`concat`, `zipWithAll`.

View File

@@ -3328,7 +3328,7 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
@[simp] theorem all_replicate {n : Nat} {a : α} :
(replicate n a).all f = if n = 0 then true else f a := by
cases n <;> simp +contextual [replicate_succ]
cases n <;> simp (config := {contextual := true}) [replicate_succ]
@[simp] theorem any_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
(l.insert a).any f = (f a || l.any f) := by

View File

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

View File

@@ -5,7 +5,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
-/
prelude
import Init.Data.List.TakeDrop
import Init.Data.List.Attach
/-!
# Lemmas about `List.mapM` and `List.forM`.
@@ -49,9 +48,6 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
@[simp] theorem mapM_cons [Monad m] [LawfulMonad m] (f : α m β) :
(a :: l).mapM f = (return ( f a) :: ( l.mapM f)) := by simp [ mapM'_eq_mapM, mapM']
@[simp] theorem mapM_id {l : List α} {f : α Id β} : l.mapM f = l.map f := by
induction l <;> simp_all
@[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α m β) {l₁ l₂ : List α} :
(l₁ ++ l₂).mapM f = (return ( l₁.mapM f) ++ ( l₂.mapM f)) := by induction l₁ <;> simp [*]
@@ -76,16 +72,6 @@ theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β)
reverse_cons, reverse_nil, nil_append, singleton_append]
simp [bind_pure_comp]
/-! ### foldlM and foldrM -/
theorem foldlM_map [Monad m] (f : β₁ β₂) (g : α β₂ m α) (l : List β₁) (init : α) :
(l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
induction l generalizing g init <;> simp [*]
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ β₂) (g : β₂ α m α) (l : List β₁)
(init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
induction l generalizing g init <;> simp [*]
/-! ### forM -/
-- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
@@ -103,6 +89,9 @@ theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂
/-! ### forIn' -/
@[simp] theorem forIn'_nil [Monad m] (f : (a : α) a [] β m (ForInStep β)) (b : β) : forIn' [] b f = pure b :=
rfl
theorem forIn'_loop_congr [Monad m] {as bs : List α}
{f : (a' : α) a' as β m (ForInStep β)}
{g : (a' : α) a' bs β m (ForInStep β)}
@@ -133,11 +122,6 @@ theorem forIn'_loop_congr [Monad m] {as bs : List α}
intros
rfl
@[simp] theorem forIn_cons [Monad m] (f : α β m (ForInStep β)) (a : α) (as : List α) (b : β) :
forIn (a::as) b f = f a b >>= fun | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f := by
have := forIn'_cons (a := a) (as := as) (fun a' _ b => f a' b) b
simpa only [forIn'_eq_forIn]
@[congr] theorem forIn'_congr [Monad m] {as bs : List α} (w : as = bs)
{b b' : β} (hb : b = b')
{f : (a' : α) a' as β m (ForInStep β)}
@@ -165,65 +149,6 @@ theorem forIn'_loop_congr [Monad m] {as bs : List α}
intro a m b
exact h a (mem_cons_of_mem _ m) b
/--
We can express a for loop over a list as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
(l : List α) (f : (a : α) a l β m (ForInStep β)) (init : β) :
forIn' l init f = ForInStep.value <$>
l.attach.foldlM (fun b a => match b with
| .yield b => f a.1 a.2 b
| .done b => pure (.done b)) (ForInStep.yield init) := by
induction l generalizing init with
| nil => simp
| cons a as ih =>
simp only [forIn'_cons, attach_cons, foldlM_cons, _root_.map_bind]
congr 1
funext x
match x with
| .done b =>
clear ih
dsimp
induction as with
| nil => simp
| cons a as ih =>
simp only [attach_cons, map_cons, map_map, Function.comp_def, foldlM_cons, pure_bind]
specialize ih (fun a m b => f a (by
simp only [mem_cons] at m
rcases m with rfl|m
· apply mem_cons_self
· exact mem_cons_of_mem _ (mem_cons_of_mem _ m)) b)
simp [ih, List.foldlM_map]
| .yield b =>
simp [ih, List.foldlM_map]
/--
We can express a for loop over a list as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
(f : α β m (ForInStep β)) (init : β) (l : List α) :
forIn l init f = ForInStep.value <$>
l.foldlM (fun b a => match b with
| .yield b => f a b
| .done b => pure (.done b)) (ForInStep.yield init) := by
induction l generalizing init with
| nil => simp
| cons a as ih =>
simp only [foldlM_cons, bind_pure_comp, forIn_cons, _root_.map_bind]
congr 1
funext x
match x with
| .done b =>
clear ih
dsimp
induction as with
| nil => simp
| cons a as ih => simp [ih]
| .yield b =>
simp [ih]
/-! ### allM -/
theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α m Bool) (as : List α) :
@@ -236,4 +161,14 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
funext b
split <;> simp_all
/-! ### foldlM and foldrM -/
theorem foldlM_map [Monad m] (f : β₁ β₂) (g : α β₂ m α) (l : List β₁) (init : α) :
(l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
induction l generalizing g init <;> simp [*]
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ β₂) (g : β₂ α m α) (l : List β₁)
(init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
induction l generalizing g init <;> simp [*]
end List

View File

@@ -64,82 +64,3 @@ theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.era
(l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
rw [getElem_eraseIdx, dif_neg]
omega
theorem eraseIdx_set_eq {l : List α} {i : Nat} {a : α} :
(l.set i a).eraseIdx i = l.eraseIdx i := by
apply ext_getElem
· simp [length_eraseIdx]
· intro n h₁ h₂
rw [getElem_eraseIdx, getElem_eraseIdx]
split <;>
· rw [getElem_set_ne]
omega
theorem eraseIdx_set_lt {l : List α} {i : Nat} {j : Nat} {a : α} (h : j < i) :
(l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a := by
apply ext_getElem
· simp [length_eraseIdx]
· intro n h₁ h₂
simp only [length_eraseIdx, length_set] at h₁
simp only [getElem_eraseIdx, getElem_set]
split
· split
· split
· rfl
· omega
· split
· omega
· rfl
· split
· split
· rfl
· omega
· have t : i - 1 n := by omega
simp [t]
theorem eraseIdx_set_gt {l : List α} {i : Nat} {j : Nat} {a : α} (h : i < j) :
(l.set i a).eraseIdx j = (l.eraseIdx j).set i a := by
apply ext_getElem
· simp [length_eraseIdx]
· intro n h₁ h₂
simp only [length_eraseIdx, length_set] at h₁
simp only [getElem_eraseIdx, getElem_set]
split
· rfl
· split
· split
· rfl
· omega
· have t : i n := by omega
simp [t]
@[simp] theorem set_getElem_succ_eraseIdx_succ
{l : List α} {i : Nat} (h : i + 1 < l.length) :
(l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i := by
apply ext_getElem
· simp only [length_set, length_eraseIdx, h, reduceIte]
rw [if_pos]
omega
· intro n h₁ h₂
simp [getElem_set, getElem_eraseIdx]
split
· split
· omega
· simp_all
· split
· split
· rfl
· omega
· have t : ¬ n < i := by omega
simp [t]
@[simp] theorem eraseIdx_length_sub_one (l : List α) :
(l.eraseIdx (l.length - 1)) = l.dropLast := by
apply ext_getElem
· simp [length_eraseIdx]
omega
· intro n h₁ h₂
rw [getElem_eraseIdx_of_lt, getElem_dropLast]
simp_all
end List

View File

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

View File

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

View File

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

View File

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

View File

@@ -190,7 +190,7 @@ theorem set_drop {l : List α} {n m : Nat} {a : α} :
theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
(l.take i).concat l[i] = l.take (i+1) :=
Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop]
rw [concat_eq_append, append_assoc, singleton_append, get_drop_eq_drop, take_append_drop]
@[deprecated take_succ_cons (since := "2024-07-25")]
theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl

View File

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

View File

@@ -651,8 +651,8 @@ theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
| .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)
theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
rw (occs := .pos [1]) [ mod_add_div a n]
rw (occs := .pos [1]) [ mod_add_div b n]
rw (config := {occs := .pos [1]}) [ mod_add_div a n]
rw (config := {occs := .pos [1]}) [ mod_add_div b n]
rw [Nat.add_mul, Nat.mul_add, Nat.mul_add,
Nat.mul_assoc, Nat.mul_assoc, Nat.mul_add n, add_mul_mod_self_left,
Nat.mul_comm _ (n * (b / n)), Nat.mul_assoc, add_mul_mod_self_left]

View File

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

View File

@@ -374,15 +374,9 @@ end choice
-- See `Init.Data.Option.List` for lemmas about `toList`.
@[simp] theorem some_or : (some a).or o = some a := rfl
@[simp] theorem or_some : (some a).or o = some a := rfl
@[simp] theorem none_or : none.or o = o := rfl
@[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl
/-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/
@[simp] theorem or_some' {o : Option α} : o.or (some a) = o.getD a := by
cases o <;> rfl
theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
cases o <;> rfl

View File

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

View File

@@ -22,48 +22,6 @@ structure Int8 where
-/
toUInt8 : UInt8
/--
The type of signed 16-bit integers. This type has special support in the
compiler to make it actually 16 bits rather than wrapping a `Nat`.
-/
structure Int16 where
/--
Obtain the `UInt16` that is 2's complement equivalent to the `Int16`.
-/
toUInt16 : UInt16
/--
The type of signed 32-bit integers. This type has special support in the
compiler to make it actually 32 bits rather than wrapping a `Nat`.
-/
structure Int32 where
/--
Obtain the `UInt32` that is 2's complement equivalent to the `Int32`.
-/
toUInt32 : UInt32
/--
The type of signed 64-bit integers. This type has special support in the
compiler to make it actually 64 bits rather than wrapping a `Nat`.
-/
structure Int64 where
/--
Obtain the `UInt64` that is 2's complement equivalent to the `Int64`.
-/
toUInt64 : UInt64
/--
A `ISize` is a signed integer with the size of a word for the platform's architecture.
For example, if running on a 32-bit machine, ISize is equivalent to `Int32`.
Or on a 64-bit machine, `Int64`.
-/
structure ISize where
/--
Obtain the `USize` that is 2's complement equivalent to the `ISize`.
-/
toUSize : USize
/-- The size of type `Int8`, that is, `2^8 = 256`. -/
abbrev Int8.size : Nat := 256
@@ -74,16 +32,12 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int8
@[extern "lean_int8_of_int"]
def Int8.ofInt (i : @& Int) : Int8 := BitVec.ofInt 8 i
@[extern "lean_int8_of_nat"]
@[extern "lean_int8_of_int"]
def Int8.ofNat (n : @& Nat) : Int8 := BitVec.ofNat 8 n
abbrev Int.toInt8 := Int8.ofInt
abbrev Nat.toInt8 := Int8.ofNat
@[extern "lean_int8_to_int"]
def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt
/--
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
@[extern "lean_int8_neg"]
def Int8.neg (i : Int8) : Int8 := -i.toBitVec
@@ -104,7 +58,7 @@ def Int8.mul (a b : Int8) : Int8 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
@[extern "lean_int8_div"]
def Int8.div (a b : Int8) : Int8 := BitVec.sdiv a.toBitVec b.toBitVec
@[extern "lean_int8_mod"]
def Int8.mod (a b : Int8) : Int8 := BitVec.srem a.toBitVec b.toBitVec
def Int8.mod (a b : Int8) : Int8 := BitVec.smod a.toBitVec b.toBitVec
@[extern "lean_int8_land"]
def Int8.land (a b : Int8) : Int8 := a.toBitVec &&& b.toBitVec
@[extern "lean_int8_lor"]
@@ -112,9 +66,9 @@ def Int8.lor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
@[extern "lean_int8_xor"]
def Int8.xor (a b : Int8) : Int8 := a.toBitVec ^^^ b.toBitVec
@[extern "lean_int8_shift_left"]
def Int8.shiftLeft (a b : Int8) : Int8 := a.toBitVec <<< (b.toBitVec.smod 8)
def Int8.shiftLeft (a b : Int8) : Int8 := a.toBitVec <<< (mod b 8).toBitVec
@[extern "lean_int8_shift_right"]
def Int8.shiftRight (a b : Int8) : Int8 := BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 8)
def Int8.shiftRight (a b : Int8) : Int8 := BitVec.sshiftRight' a.toBitVec (mod b 8).toBitVec
@[extern "lean_int8_complement"]
def Int8.complement (a : Int8) : Int8 := ~~~a.toBitVec
@@ -160,429 +114,3 @@ instance (a b : Int8) : Decidable (a < b) := Int8.decLt a b
instance (a b : Int8) : Decidable (a b) := Int8.decLe a b
instance : Max Int8 := maxOfLe
instance : Min Int8 := minOfLe
/-- The size of type `Int16`, that is, `2^16 = 65536`. -/
abbrev Int16.size : Nat := 65536
/--
Obtain the `BitVec` that contains the 2's complement representation of the `Int16`.
-/
@[inline] def Int16.toBitVec (x : Int16) : BitVec 16 := x.toUInt16.toBitVec
@[extern "lean_int16_of_int"]
def Int16.ofInt (i : @& Int) : Int16 := BitVec.ofInt 16 i
@[extern "lean_int16_of_nat"]
def Int16.ofNat (n : @& Nat) : Int16 := BitVec.ofNat 16 n
abbrev Int.toInt16 := Int16.ofInt
abbrev Nat.toInt16 := Int16.ofNat
@[extern "lean_int16_to_int"]
def Int16.toInt (i : Int16) : Int := i.toBitVec.toInt
/--
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int16.toNat (i : Int16) : Nat := i.toInt.toNat
@[extern "lean_int16_to_int8"]
def Int16.toInt8 (a : Int16) : Int8 := a.toBitVec.signExtend 8
@[extern "lean_int8_to_int16"]
def Int8.toInt16 (a : Int8) : Int16 := a.toBitVec.signExtend 16
@[extern "lean_int16_neg"]
def Int16.neg (i : Int16) : Int16 := -i.toBitVec
instance : ToString Int16 where
toString i := toString i.toInt
instance : OfNat Int16 n := Int16.ofNat n
instance : Neg Int16 where
neg := Int16.neg
@[extern "lean_int16_add"]
def Int16.add (a b : Int16) : Int16 := a.toBitVec + b.toBitVec
@[extern "lean_int16_sub"]
def Int16.sub (a b : Int16) : Int16 := a.toBitVec - b.toBitVec
@[extern "lean_int16_mul"]
def Int16.mul (a b : Int16) : Int16 := a.toBitVec * b.toBitVec
@[extern "lean_int16_div"]
def Int16.div (a b : Int16) : Int16 := BitVec.sdiv a.toBitVec b.toBitVec
@[extern "lean_int16_mod"]
def Int16.mod (a b : Int16) : Int16 := BitVec.srem a.toBitVec b.toBitVec
@[extern "lean_int16_land"]
def Int16.land (a b : Int16) : Int16 := a.toBitVec &&& b.toBitVec
@[extern "lean_int16_lor"]
def Int16.lor (a b : Int16) : Int16 := a.toBitVec ||| b.toBitVec
@[extern "lean_int16_xor"]
def Int16.xor (a b : Int16) : Int16 := a.toBitVec ^^^ b.toBitVec
@[extern "lean_int16_shift_left"]
def Int16.shiftLeft (a b : Int16) : Int16 := a.toBitVec <<< (b.toBitVec.smod 16)
@[extern "lean_int16_shift_right"]
def Int16.shiftRight (a b : Int16) : Int16 := BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 16)
@[extern "lean_int16_complement"]
def Int16.complement (a : Int16) : Int16 := ~~~a.toBitVec
@[extern "lean_int16_dec_eq"]
def Int16.decEq (a b : Int16) : Decidable (a = b) :=
match a, b with
| n, m =>
if h : n = m then
isTrue <| h rfl
else
isFalse (fun h' => Int16.noConfusion h' (fun h' => absurd h' h))
def Int16.lt (a b : Int16) : Prop := a.toBitVec.slt b.toBitVec
def Int16.le (a b : Int16) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited Int16 where
default := 0
instance : Add Int16 := Int16.add
instance : Sub Int16 := Int16.sub
instance : Mul Int16 := Int16.mul
instance : Mod Int16 := Int16.mod
instance : Div Int16 := Int16.div
instance : LT Int16 := Int16.lt
instance : LE Int16 := Int16.le
instance : Complement Int16 := Int16.complement
instance : AndOp Int16 := Int16.land
instance : OrOp Int16 := Int16.lor
instance : Xor Int16 := Int16.xor
instance : ShiftLeft Int16 := Int16.shiftLeft
instance : ShiftRight Int16 := Int16.shiftRight
instance : DecidableEq Int16 := Int16.decEq
@[extern "lean_int16_dec_lt"]
def Int16.decLt (a b : Int16) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@[extern "lean_int16_dec_le"]
def Int16.decLe (a b : Int16) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : Int16) : Decidable (a < b) := Int16.decLt a b
instance (a b : Int16) : Decidable (a b) := Int16.decLe a b
instance : Max Int16 := maxOfLe
instance : Min Int16 := minOfLe
/-- The size of type `Int32`, that is, `2^32 = 4294967296`. -/
abbrev Int32.size : Nat := 4294967296
/--
Obtain the `BitVec` that contains the 2's complement representation of the `Int32`.
-/
@[inline] def Int32.toBitVec (x : Int32) : BitVec 32 := x.toUInt32.toBitVec
@[extern "lean_int32_of_int"]
def Int32.ofInt (i : @& Int) : Int32 := BitVec.ofInt 32 i
@[extern "lean_int32_of_nat"]
def Int32.ofNat (n : @& Nat) : Int32 := BitVec.ofNat 32 n
abbrev Int.toInt32 := Int32.ofInt
abbrev Nat.toInt32 := Int32.ofNat
@[extern "lean_int32_to_int"]
def Int32.toInt (i : Int32) : Int := i.toBitVec.toInt
/--
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int32.toNat (i : Int32) : Nat := i.toInt.toNat
@[extern "lean_int32_to_int8"]
def Int32.toInt8 (a : Int32) : Int8 := a.toBitVec.signExtend 8
@[extern "lean_int32_to_int16"]
def Int32.toInt16 (a : Int32) : Int16 := a.toBitVec.signExtend 16
@[extern "lean_int8_to_int32"]
def Int8.toInt32 (a : Int8) : Int32 := a.toBitVec.signExtend 32
@[extern "lean_int16_to_int32"]
def Int16.toInt32 (a : Int16) : Int32 := a.toBitVec.signExtend 32
@[extern "lean_int32_neg"]
def Int32.neg (i : Int32) : Int32 := -i.toBitVec
instance : ToString Int32 where
toString i := toString i.toInt
instance : OfNat Int32 n := Int32.ofNat n
instance : Neg Int32 where
neg := Int32.neg
@[extern "lean_int32_add"]
def Int32.add (a b : Int32) : Int32 := a.toBitVec + b.toBitVec
@[extern "lean_int32_sub"]
def Int32.sub (a b : Int32) : Int32 := a.toBitVec - b.toBitVec
@[extern "lean_int32_mul"]
def Int32.mul (a b : Int32) : Int32 := a.toBitVec * b.toBitVec
@[extern "lean_int32_div"]
def Int32.div (a b : Int32) : Int32 := BitVec.sdiv a.toBitVec b.toBitVec
@[extern "lean_int32_mod"]
def Int32.mod (a b : Int32) : Int32 := BitVec.srem a.toBitVec b.toBitVec
@[extern "lean_int32_land"]
def Int32.land (a b : Int32) : Int32 := a.toBitVec &&& b.toBitVec
@[extern "lean_int32_lor"]
def Int32.lor (a b : Int32) : Int32 := a.toBitVec ||| b.toBitVec
@[extern "lean_int32_xor"]
def Int32.xor (a b : Int32) : Int32 := a.toBitVec ^^^ b.toBitVec
@[extern "lean_int32_shift_left"]
def Int32.shiftLeft (a b : Int32) : Int32 := a.toBitVec <<< (b.toBitVec.smod 32)
@[extern "lean_int32_shift_right"]
def Int32.shiftRight (a b : Int32) : Int32 := BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 32)
@[extern "lean_int32_complement"]
def Int32.complement (a : Int32) : Int32 := ~~~a.toBitVec
@[extern "lean_int32_dec_eq"]
def Int32.decEq (a b : Int32) : Decidable (a = b) :=
match a, b with
| n, m =>
if h : n = m then
isTrue <| h rfl
else
isFalse (fun h' => Int32.noConfusion h' (fun h' => absurd h' h))
def Int32.lt (a b : Int32) : Prop := a.toBitVec.slt b.toBitVec
def Int32.le (a b : Int32) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited Int32 where
default := 0
instance : Add Int32 := Int32.add
instance : Sub Int32 := Int32.sub
instance : Mul Int32 := Int32.mul
instance : Mod Int32 := Int32.mod
instance : Div Int32 := Int32.div
instance : LT Int32 := Int32.lt
instance : LE Int32 := Int32.le
instance : Complement Int32 := Int32.complement
instance : AndOp Int32 := Int32.land
instance : OrOp Int32 := Int32.lor
instance : Xor Int32 := Int32.xor
instance : ShiftLeft Int32 := Int32.shiftLeft
instance : ShiftRight Int32 := Int32.shiftRight
instance : DecidableEq Int32 := Int32.decEq
@[extern "lean_int32_dec_lt"]
def Int32.decLt (a b : Int32) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@[extern "lean_int32_dec_le"]
def Int32.decLe (a b : Int32) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : Int32) : Decidable (a < b) := Int32.decLt a b
instance (a b : Int32) : Decidable (a b) := Int32.decLe a b
instance : Max Int32 := maxOfLe
instance : Min Int32 := minOfLe
/-- The size of type `Int64`, that is, `2^64 = 18446744073709551616`. -/
abbrev Int64.size : Nat := 18446744073709551616
/--
Obtain the `BitVec` that contains the 2's complement representation of the `Int64`.
-/
@[inline] def Int64.toBitVec (x : Int64) : BitVec 64 := x.toUInt64.toBitVec
@[extern "lean_int64_of_int"]
def Int64.ofInt (i : @& Int) : Int64 := BitVec.ofInt 64 i
@[extern "lean_int64_of_nat"]
def Int64.ofNat (n : @& Nat) : Int64 := BitVec.ofNat 64 n
abbrev Int.toInt64 := Int64.ofInt
abbrev Nat.toInt64 := Int64.ofNat
@[extern "lean_int64_to_int_sint"]
def Int64.toInt (i : Int64) : Int := i.toBitVec.toInt
/--
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int64.toNat (i : Int64) : Nat := i.toInt.toNat
@[extern "lean_int64_to_int8"]
def Int64.toInt8 (a : Int64) : Int8 := a.toBitVec.signExtend 8
@[extern "lean_int64_to_int16"]
def Int64.toInt16 (a : Int64) : Int16 := a.toBitVec.signExtend 16
@[extern "lean_int64_to_int32"]
def Int64.toInt32 (a : Int64) : Int32 := a.toBitVec.signExtend 32
@[extern "lean_int8_to_int64"]
def Int8.toInt64 (a : Int8) : Int64 := a.toBitVec.signExtend 64
@[extern "lean_int16_to_int64"]
def Int16.toInt64 (a : Int16) : Int64 := a.toBitVec.signExtend 64
@[extern "lean_int32_to_int64"]
def Int32.toInt64 (a : Int32) : Int64 := a.toBitVec.signExtend 64
@[extern "lean_int64_neg"]
def Int64.neg (i : Int64) : Int64 := -i.toBitVec
instance : ToString Int64 where
toString i := toString i.toInt
instance : OfNat Int64 n := Int64.ofNat n
instance : Neg Int64 where
neg := Int64.neg
@[extern "lean_int64_add"]
def Int64.add (a b : Int64) : Int64 := a.toBitVec + b.toBitVec
@[extern "lean_int64_sub"]
def Int64.sub (a b : Int64) : Int64 := a.toBitVec - b.toBitVec
@[extern "lean_int64_mul"]
def Int64.mul (a b : Int64) : Int64 := a.toBitVec * b.toBitVec
@[extern "lean_int64_div"]
def Int64.div (a b : Int64) : Int64 := BitVec.sdiv a.toBitVec b.toBitVec
@[extern "lean_int64_mod"]
def Int64.mod (a b : Int64) : Int64 := BitVec.srem a.toBitVec b.toBitVec
@[extern "lean_int64_land"]
def Int64.land (a b : Int64) : Int64 := a.toBitVec &&& b.toBitVec
@[extern "lean_int64_lor"]
def Int64.lor (a b : Int64) : Int64 := a.toBitVec ||| b.toBitVec
@[extern "lean_int64_xor"]
def Int64.xor (a b : Int64) : Int64 := a.toBitVec ^^^ b.toBitVec
@[extern "lean_int64_shift_left"]
def Int64.shiftLeft (a b : Int64) : Int64 := a.toBitVec <<< (b.toBitVec.smod 64)
@[extern "lean_int64_shift_right"]
def Int64.shiftRight (a b : Int64) : Int64 := BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 64)
@[extern "lean_int64_complement"]
def Int64.complement (a : Int64) : Int64 := ~~~a.toBitVec
@[extern "lean_int64_dec_eq"]
def Int64.decEq (a b : Int64) : Decidable (a = b) :=
match a, b with
| n, m =>
if h : n = m then
isTrue <| h rfl
else
isFalse (fun h' => Int64.noConfusion h' (fun h' => absurd h' h))
def Int64.lt (a b : Int64) : Prop := a.toBitVec.slt b.toBitVec
def Int64.le (a b : Int64) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited Int64 where
default := 0
instance : Add Int64 := Int64.add
instance : Sub Int64 := Int64.sub
instance : Mul Int64 := Int64.mul
instance : Mod Int64 := Int64.mod
instance : Div Int64 := Int64.div
instance : LT Int64 := Int64.lt
instance : LE Int64 := Int64.le
instance : Complement Int64 := Int64.complement
instance : AndOp Int64 := Int64.land
instance : OrOp Int64 := Int64.lor
instance : Xor Int64 := Int64.xor
instance : ShiftLeft Int64 := Int64.shiftLeft
instance : ShiftRight Int64 := Int64.shiftRight
instance : DecidableEq Int64 := Int64.decEq
@[extern "lean_int64_dec_lt"]
def Int64.decLt (a b : Int64) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@[extern "lean_int64_dec_le"]
def Int64.decLe (a b : Int64) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : Int64) : Decidable (a < b) := Int64.decLt a b
instance (a b : Int64) : Decidable (a b) := Int64.decLe a b
instance : Max Int64 := maxOfLe
instance : Min Int64 := minOfLe
/-- The size of type `ISize`, that is, `2^System.Platform.numBits`. -/
abbrev ISize.size : Nat := 2^System.Platform.numBits
/--
Obtain the `BitVec` that contains the 2's complement representation of the `ISize`.
-/
@[inline] def ISize.toBitVec (x : ISize) : BitVec System.Platform.numBits := x.toUSize.toBitVec
@[extern "lean_isize_of_int"]
def ISize.ofInt (i : @& Int) : ISize := BitVec.ofInt System.Platform.numBits i
@[extern "lean_isize_of_nat"]
def ISize.ofNat (n : @& Nat) : ISize := BitVec.ofNat System.Platform.numBits n
abbrev Int.toISize := ISize.ofInt
abbrev Nat.toISize := ISize.ofNat
@[extern "lean_isize_to_int"]
def ISize.toInt (i : ISize) : Int := i.toBitVec.toInt
/--
This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
@[extern "lean_isize_to_int32"]
def ISize.toInt32 (a : ISize) : Int32 := a.toBitVec.signExtend 32
/--
Upcast `ISize` to `Int64`. This function is losless as `ISize` is either `Int32` or `Int64`.
-/
@[extern "lean_isize_to_int64"]
def ISize.toInt64 (a : ISize) : Int64 := a.toBitVec.signExtend 64
/--
Upcast `Int32` to `ISize`. This function is losless as `ISize` is either `Int32` or `Int64`.
-/
@[extern "lean_int32_to_isize"]
def Int32.toISize (a : Int32) : ISize := a.toBitVec.signExtend System.Platform.numBits
@[extern "lean_int64_to_isize"]
def Int64.toISize (a : Int64) : ISize := a.toBitVec.signExtend System.Platform.numBits
@[extern "lean_isize_neg"]
def ISize.neg (i : ISize) : ISize := -i.toBitVec
instance : ToString ISize where
toString i := toString i.toInt
instance : OfNat ISize n := ISize.ofNat n
instance : Neg ISize where
neg := ISize.neg
@[extern "lean_isize_add"]
def ISize.add (a b : ISize) : ISize := a.toBitVec + b.toBitVec
@[extern "lean_isize_sub"]
def ISize.sub (a b : ISize) : ISize := a.toBitVec - b.toBitVec
@[extern "lean_isize_mul"]
def ISize.mul (a b : ISize) : ISize := a.toBitVec * b.toBitVec
@[extern "lean_isize_div"]
def ISize.div (a b : ISize) : ISize := BitVec.sdiv a.toBitVec b.toBitVec
@[extern "lean_isize_mod"]
def ISize.mod (a b : ISize) : ISize := BitVec.srem a.toBitVec b.toBitVec
@[extern "lean_isize_land"]
def ISize.land (a b : ISize) : ISize := a.toBitVec &&& b.toBitVec
@[extern "lean_isize_lor"]
def ISize.lor (a b : ISize) : ISize := a.toBitVec ||| b.toBitVec
@[extern "lean_isize_xor"]
def ISize.xor (a b : ISize) : ISize := a.toBitVec ^^^ b.toBitVec
@[extern "lean_isize_shift_left"]
def ISize.shiftLeft (a b : ISize) : ISize := a.toBitVec <<< (b.toBitVec.smod System.Platform.numBits)
@[extern "lean_isize_shift_right"]
def ISize.shiftRight (a b : ISize) : ISize := BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod System.Platform.numBits)
@[extern "lean_isize_complement"]
def ISize.complement (a : ISize) : ISize := ~~~a.toBitVec
@[extern "lean_isize_dec_eq"]
def ISize.decEq (a b : ISize) : Decidable (a = b) :=
match a, b with
| n, m =>
if h : n = m then
isTrue <| h rfl
else
isFalse (fun h' => ISize.noConfusion h' (fun h' => absurd h' h))
def ISize.lt (a b : ISize) : Prop := a.toBitVec.slt b.toBitVec
def ISize.le (a b : ISize) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited ISize where
default := 0
instance : Add ISize := ISize.add
instance : Sub ISize := ISize.sub
instance : Mul ISize := ISize.mul
instance : Mod ISize := ISize.mod
instance : Div ISize := ISize.div
instance : LT ISize := ISize.lt
instance : LE ISize := ISize.le
instance : Complement ISize := ISize.complement
instance : AndOp ISize := ISize.land
instance : OrOp ISize := ISize.lor
instance : Xor ISize := ISize.xor
instance : ShiftLeft ISize := ISize.shiftLeft
instance : ShiftRight ISize := ISize.shiftRight
instance : DecidableEq ISize := ISize.decEq
@[extern "lean_isize_dec_lt"]
def ISize.decLt (a b : ISize) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@[extern "lean_isize_dec_le"]
def ISize.decLe (a b : ISize) : Decidable (a b) :=
inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
instance (a b : ISize) : Decidable (a < b) := ISize.decLt a b
instance (a b : ISize) : Decidable (a b) := ISize.decLe a b
instance : Max ISize := maxOfLe
instance : Min ISize := minOfLe

View File

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

View File

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

View File

@@ -211,13 +211,10 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where
| _ :: _, 0, _ => .head ..
| _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.length) :
as[i] :: as.drop (i+1) = as.drop i :=
theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
match as, i with
| _::_, 0 => rfl
| _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) _
@[deprecated (since := "2024-11-05")] abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop
| _::_, i+1 => get_drop_eq_drop _ i _
end List

View File

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

View File

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

View File

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

View File

@@ -272,20 +272,12 @@ macro nextTk:"next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
-- Limit ref variability for incrementality; see Note [Incremental Macros]
withRef arrowTk `(tactic| case%$nextTk _ $args* =>%$arrowTk $tac)
/--
`all_goals tac` runs `tac` on each goal, concatenating the resulting goals.
If the tactic fails on any goal, the entire `all_goals` tactic fails.
See also `any_goals tac`.
-/
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
syntax (name := allGoals) "all_goals " tacticSeq : tactic
/--
`any_goals tac` applies the tactic `tac` to every goal,
concating the resulting goals for successful tactic applications.
If the tactic fails on all of the goals, the entire `any_goals` tactic fails.
This tactic is like `all_goals try tac` except that it fails if none of the applications of `tac` succeeds.
`any_goals tac` applies the tactic `tac` to every goal, and succeeds if at
least one application succeeds.
-/
syntax (name := anyGoals) "any_goals " tacticSeq : tactic
@@ -425,27 +417,7 @@ It synthesizes a value of any target type by typeclass inference.
-/
macro "infer_instance" : tactic => `(tactic| exact inferInstance)
/--
`+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`.
-/
syntax posConfigItem := "+" noWs ident
/--
`-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`.
-/
syntax negConfigItem := "-" noWs ident
/--
`(opt := val)` sets the `opt` configuration option to `val`.
As a special case, `(config := ...)` sets the entire configuration.
-/
syntax valConfigItem := atomic(" (" notFollowedBy(&"discharger" <|> &"disch") (ident <|> &"config")) " := " withoutPosition(term) ")"
/-- A configuration item for a tactic configuration. -/
syntax configItem := posConfigItem <|> negConfigItem <|> valConfigItem
/-- Configuration options for tactics. -/
syntax optConfig := (colGt configItem)*
/-- Optional configuration option for tactics. (Deprecated. Replace `(config)?` with `optConfig`.) -/
/-- Optional configuration option for tactics -/
syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")"
/-- The `*` location refers to all hypotheses and the goal. -/
@@ -502,25 +474,25 @@ This provides a convenient way to unfold `e`.
list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
can also be used, to signify the target of the goal.
Using `rw (occs := .pos L) [e]`,
Using `rw (config := {occs := .pos L}) [e]`,
where `L : List Nat`, you can control which "occurrences" are rewritten.
(This option applies to each rule, so usually this will only be used with a single rule.)
Occurrences count from `1`.
At each allowed occurrence, arguments of the rewrite rule `e` may be instantiated,
restricting which later rewrites can be found.
(Disallowed occurrences do not result in instantiation.)
`(occs := .neg L)` allows skipping specified occurrences.
`{occs := .neg L}` allows skipping specified occurrences.
-/
syntax (name := rewriteSeq) "rewrite" optConfig rwRuleSeq (location)? : tactic
syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic
/--
`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
-/
macro (name := rwSeq) "rw " c:optConfig s:rwRuleSeq l:(location)? : tactic =>
macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
match s with
| `(rwRuleSeq| [$rs,*]%$rbrak) =>
-- We show the `rfl` state on `]`
`(tactic| (rewrite $c [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
`(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
| _ => Macro.throwUnsupported
/-- `rwa` is short-hand for `rw; assumption`. -/
@@ -589,14 +561,14 @@ non-dependent hypotheses. It has many variants:
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
other hypotheses.
-/
syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
/--
`simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target
are simplified multiple times until no simplification is applicable.
Only non-dependent propositional hypotheses are considered.
-/
syntax (name := simpAll) "simp_all" optConfig (discharger)? (&" only")?
syntax (name := simpAll) "simp_all" (config)? (discharger)? (&" only")?
(" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? : tactic
/--
@@ -604,7 +576,7 @@ The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but o
applies theorems that hold by reflexivity. Thus, the result is guaranteed to be
definitionally equal to the input.
-/
syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
(" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
/--
@@ -626,7 +598,7 @@ def dsimpArg := simpErase.binary `orelse simpLemma
syntax dsimpArgs := " [" dsimpArg,* "]"
/-- The common arguments of `simp?` and `simp?!`. -/
syntax simpTraceArgsRest := optConfig (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
syntax simpTraceArgsRest := (config)? (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
/--
`simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
@@ -645,7 +617,7 @@ syntax (name := simpTrace) "simp?" "!"? simpTraceArgsRest : tactic
macro tk:"simp?!" rest:simpTraceArgsRest : tactic => `(tactic| simp?%$tk ! $rest)
/-- The common arguments of `simp_all?` and `simp_all?!`. -/
syntax simpAllTraceArgsRest := optConfig (discharger)? (&" only")? (dsimpArgs)?
syntax simpAllTraceArgsRest := (config)? (discharger)? (&" only")? (dsimpArgs)?
@[inherit_doc simpTrace]
syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
@@ -654,7 +626,7 @@ syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
macro tk:"simp_all?!" rest:simpAllTraceArgsRest : tactic => `(tactic| simp_all?%$tk ! $rest)
/-- The common arguments of `dsimp?` and `dsimp?!`. -/
syntax dsimpTraceArgsRest := optConfig (&" only")? (dsimpArgs)? (ppSpace location)?
syntax dsimpTraceArgsRest := (config)? (&" only")? (dsimpArgs)? (ppSpace location)?
@[inherit_doc simpTrace]
syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
@@ -663,7 +635,7 @@ syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
macro tk:"dsimp?!" rest:dsimpTraceArgsRest : tactic => `(tactic| dsimp?%$tk ! $rest)
/-- The arguments to the `simpa` family tactics. -/
syntax simpaArgsRest := optConfig (discharger)? &" only "? (simpArgs)? (" using " term)?
syntax simpaArgsRest := (config)? (discharger)? &" only "? (simpArgs)? (" using " term)?
/--
This is a "finishing" tactic modification of `simp`. It has two forms.
@@ -1176,7 +1148,8 @@ a natural subtraction appearing in a hypothesis, and try again.
The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
omega (config :=
{ splitDisjunctions := true, splitNatSub := true, splitNatAbs := true, splitMinMax := true })
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
@@ -1186,7 +1159,7 @@ can be used to:
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a min a b = b`
Currently, all of these are on by default.
-/
syntax (name := omega) "omega" optConfig : tactic
syntax (name := omega) "omega" (config)? : tactic
/--
`bv_omega` is `omega` with an additional preprocessor that turns statements about `BitVec` into statements about `Nat`.
@@ -1299,7 +1272,7 @@ example (a b : Nat)
See also `norm_cast`.
-/
syntax (name := pushCast) "push_cast" optConfig (discharger)? (&" only")?
syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
(" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
/--
@@ -1375,7 +1348,7 @@ See also the doc-comment for `Lean.Meta.Tactic.Backtrack.BacktrackConfig` for th
Both `apply_assumption` and `apply_rules` are implemented via these hooks.
-/
syntax (name := solveByElim)
"solve_by_elim" "*"? optConfig (&" only")? (args)? (using_)? : tactic
"solve_by_elim" "*"? (config)? (&" only")? (args)? (using_)? : tactic
/--
`apply_assumption` looks for an assumption of the form `... → ∀ _, ... → head`
@@ -1398,7 +1371,7 @@ You can pass a further configuration via the syntax `apply_rules (config := {...
The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).
-/
syntax (name := applyAssumption)
"apply_assumption" optConfig (&" only")? (args)? (using_)? : tactic
"apply_assumption" (config)? (&" only")? (args)? (using_)? : tactic
/--
`apply_rules [l₁, l₂, ...]` tries to solve the main goal by iteratively
@@ -1423,7 +1396,7 @@ You can bound the iteration depth using the syntax `apply_rules (config := {maxD
Unlike `solve_by_elim`, `apply_rules` does not perform backtracking, and greedily applies
a lemma from the list until it gets stuck.
-/
syntax (name := applyRules) "apply_rules" optConfig (&" only")? (args)? (using_)? : tactic
syntax (name := applyRules) "apply_rules" (config)? (&" only")? (args)? (using_)? : tactic
end SolveByElim
/--
@@ -1622,7 +1595,7 @@ where `i < arr.size` is in the context) and `simp_arith` and `omega`
syntax "get_elem_tactic_trivial" : tactic
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp +arith; done)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
/--

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@@ -463,7 +463,7 @@ mutual
let mut res := #[]
for x in xs do
if res.size > 0 then
match res.back!, x with
match res.back, x with
| Content.Character x, Content.Character y => res := res.set! (res.size - 1) (Content.Character $ x ++ y)
| _, x => res := res.push x
else res := res.push x

View File

@@ -595,22 +595,6 @@ mutual
elabAndAddNewArg argName arg
main
| _ =>
if ( read).ellipsis && ( readThe Term.Context).inPattern then
/-
In patterns, ellipsis should always be an implicit argument, even if it is an optparam or autoparam.
This prevents examples such as the one in #4555 from failing:
```lean
match e with
| .internal .. => sorry
| .error .. => sorry
```
The `internal` has an optparam (`| internal (id : InternalExceptionId) (extra : KVMap := {})`).
We may consider having ellipsis suppress optparams and autoparams in general.
We avoid doing so for now since it's possible to opt-out of them (for example with `.internal (extra := _) ..`)
but it's not possible to opt-in.
-/
return addImplicitArg argName
let argType getArgExpectedType
match ( read).explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with
| false, some defVal, _ => addNewArg argName defVal; main
@@ -1151,29 +1135,24 @@ private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermE
throwError "{msg}{indentExpr e}\nhas type{indentExpr eType}"
/--
`findMethod? S fName` tries the following for each namespace `S'` in the resolution order for `S`:
- If `env` contains `S' ++ fName`, returns `(S', S' ++ fName)`
- Otherwise if `env` contains private name `prv` for `S' ++ fName`, returns `(S', prv)`
`findMethod? env S fName`.
- If `env` contains `S ++ fName`, return `(S, S++fName)`
- Otherwise if `env` contains private name `prv` for `S ++ fName`, return `(S, prv)`, o
- Otherwise for each parent structure `S'` of `S`, we try `findMethod? env S' fname`
-/
private partial def findMethod? (structName fieldName : Name) : MetaM (Option (Name × Name)) := do
let env getEnv
let find? structName' : MetaM (Option (Name × Name)) := do
let fullName := structName' ++ fieldName
if env.contains fullName then
return some (structName', fullName)
private partial def findMethod? (env : Environment) (structName fieldName : Name) : Option (Name × Name) :=
let fullName := structName ++ fieldName
match env.find? fullName with
| some _ => some (structName, fullName)
| none =>
let fullNamePrv := mkPrivateName env fullName
if env.contains fullNamePrv then
return some (structName', fullNamePrv)
return none
-- Optimization: the first element of the resolution order is `structName`,
-- so we can skip computing the resolution order in the common case
-- of the name resolving in the `structName` namespace.
find? structName <||> do
let resolutionOrder if isStructure env structName then getStructureResolutionOrder structName else pure #[structName]
for h : i in [1:resolutionOrder.size] do
if let some res find? resolutionOrder[i] then
return res
return none
match env.find? fullNamePrv with
| some _ => some (structName, fullNamePrv)
| none =>
if isStructure env structName then
(getStructureSubobjects env structName).findSome? fun parentStructName => findMethod? env parentStructName fieldName
else
none
/--
Return `some (structName', fullName)` if `structName ++ fieldName` is an alias for `fullName`, and
@@ -1209,23 +1188,23 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
if idx == 0 then
throwError "invalid projection, index must be greater than 0"
let env getEnv
let failK _ := throwLValError e eType "invalid projection, structure expected"
matchConstStructure eType.getAppFn failK fun _ _ ctorVal => do
let numFields := ctorVal.numFields
if idx - 1 < numFields then
if isStructure env structName then
let fieldNames := getStructureFields env structName
return LValResolution.projFn structName structName fieldNames[idx - 1]!
else
/- `structName` was declared using `inductive` command.
So, we don't projection functions for it. Thus, we use `Expr.proj` -/
return LValResolution.projIdx structName (idx - 1)
unless isStructureLike env structName do
throwLValError e eType "invalid projection, structure expected"
let numFields := getStructureLikeNumFields env structName
if idx - 1 < numFields then
if isStructure env structName then
let fieldNames := getStructureFields env structName
return LValResolution.projFn structName structName fieldNames[idx - 1]!
else
throwLValError e eType m!"invalid projection, structure has only {numFields} field(s)"
/- `structName` was declared using `inductive` command.
So, we don't projection functions for it. Thus, we use `Expr.proj` -/
return LValResolution.projIdx structName (idx - 1)
else
throwLValError e eType m!"invalid projection, structure has only {numFields} field(s)"
| some structName, LVal.fieldName _ fieldName _ _ =>
let env getEnv
let searchEnv : Unit TermElabM LValResolution := fun _ => do
if let some (baseStructName, fullName) findMethod? structName (.mkSimple fieldName) then
if let some (baseStructName, fullName) := findMethod? env structName (.mkSimple fieldName) then
return LValResolution.const baseStructName structName fullName
else if let some (structName', fullName) := findMethodAlias? env structName (.mkSimple fieldName) then
return LValResolution.const structName' structName' fullName
@@ -1411,17 +1390,19 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
loop f lvals
| LValResolution.projFn baseStructName structName fieldName =>
let f mkBaseProjections baseStructName structName f
let some info := getFieldInfo? ( getEnv) baseStructName fieldName | unreachable!
if isPrivateNameFromImportedModule ( getEnv) info.projFn then
throwError "field '{fieldName}' from structure '{structName}' is private"
let projFn mkConst info.projFn
let projFn addProjTermInfo lval.getRef projFn
if lvals.isEmpty then
let namedArgs addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
if let some info := getFieldInfo? ( getEnv) baseStructName fieldName then
if isPrivateNameFromImportedModule ( getEnv) info.projFn then
throwError "field '{fieldName}' from structure '{structName}' is private"
let projFn mkConst info.projFn
let projFn addProjTermInfo lval.getRef projFn
if lvals.isEmpty then
let namedArgs addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
else
let f elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
loop f lvals
else
let f elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
loop f lvals
unreachable!
| LValResolution.const baseStructName structName constName =>
let f if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
let projFn mkConst constName

View File

@@ -39,7 +39,7 @@ partial def expandArgs (args : Array Syntax) : MetaM (Array NamedArg × Array Ar
let (args, ellipsis) :=
if args.isEmpty then
(args, false)
else if args.back!.isOfKind ``Lean.Parser.Term.ellipsis then
else if args.back.isOfKind ``Lean.Parser.Term.ellipsis then
(args.pop, true)
else
(args, false)

View File

@@ -424,87 +424,4 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
@[builtin_command_elab Parser.Command.eoi] def elabEoi : CommandElab := fun _ =>
return
@[builtin_command_elab Parser.Command.where] def elabWhere : CommandElab := fun _ => do
let scope getScope
let mut msg : Array MessageData := #[]
-- Noncomputable
if scope.isNoncomputable then
msg := msg.push <| `(command| noncomputable section)
-- Namespace
if !scope.currNamespace.isAnonymous then
msg := msg.push <| `(command| namespace $(mkIdent scope.currNamespace))
-- Open namespaces
if let some openMsg describeOpenDecls scope.openDecls.reverse then
msg := msg.push openMsg
-- Universe levels
if !scope.levelNames.isEmpty then
let levels := scope.levelNames.reverse.map mkIdent
msg := msg.push <| `(command| universe $levels.toArray*)
-- Variables
if !scope.varDecls.isEmpty then
let varDecls : Array (TSyntax `Lean.Parser.Term.bracketedBinder) := scope.varDecls.map (·.raw.unsetTrailing)
msg := msg.push <| `(command| variable $varDecls*)
-- Included variables
if !scope.includedVars.isEmpty then
msg := msg.push <| `(command| include $(scope.includedVars.toArray.map (mkIdent ·.eraseMacroScopes))*)
-- Options
if let some optionsMsg describeOptions scope.opts then
msg := msg.push optionsMsg
if msg.isEmpty then
logInfo m!"-- In root namespace with initial scope"
else
logInfo <| MessageData.joinSep msg.toList "\n\n"
where
/--
'Delaborate' open declarations.
Current limitations:
- does not check whether or not successive namespaces need `_root_`
- does not combine commands with `renaming` clauses into a single command
-/
describeOpenDecls (ds : List OpenDecl) : CommandElabM (Option MessageData) := do
let mut lines : Array MessageData := #[]
let mut simple : Array Name := #[]
let flush (lines : Array MessageData) (simple : Array Name) : CommandElabM (Array MessageData × Array Name) := do
if simple.isEmpty then
return (lines, simple)
else
return (lines.push <| `(command| open $(simple.map mkIdent)*), #[])
for d in ds do
match d with
| .explicit id decl =>
(lines, simple) flush lines simple
let ns := decl.getPrefix
let «from» := Name.mkSimple decl.getString!
lines := lines.push <| `(command| open $(mkIdent ns) renaming $(mkIdent «from») $(mkIdent id))
| .simple ns ex =>
if ex == [] then
simple := simple.push ns
else
(lines, simple) flush lines simple
lines := lines.push <| `(command| open $(mkIdent ns) hiding $[$(ex.toArray.map mkIdent)]*)
(lines, _) flush lines simple
return if lines.isEmpty then none else MessageData.joinSep lines.toList "\n"
describeOptions (opts : Options) : CommandElabM (Option MessageData) := do
let mut lines : Array MessageData := #[]
let decls getOptionDecls
for (name, val) in opts do
let (isSet, isUnknown) :=
match decls.find? name with
| some decl => (decl.defValue != val, false)
| none => (true, true)
if isSet then
let cmd : TSyntax `command
match val with
| .ofBool true => `(set_option $(mkIdent name) true)
| .ofBool false => `(set_option $(mkIdent name) false)
| .ofString str => `(set_option $(mkIdent name) $(Syntax.mkStrLit str))
| .ofNat n => `(set_option $(mkIdent name) $(Syntax.mkNatLit n))
| _ => `(set_option $(mkIdent name) 0 /- unrepresentable value -/)
if isUnknown then
lines := lines.push m!"-- {cmd} -- unknown option"
else
lines := lines.push cmd
return if lines.isEmpty then none else MessageData.joinSep lines.toList "\n"
end Lean.Elab.Command

View File

@@ -137,7 +137,7 @@ private def mkFormat (e : Expr) : MetaM Expr := do
if let .const name _ := ( whnf ( inferType e)).getAppFn then
try
trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{.ofConstName name}'"
liftCommandElabM do applyDerivingHandlers ``Repr #[name]
liftCommandElabM do applyDerivingHandlers ``Repr #[name] none
resetSynthInstanceCache
return mkRepr e
catch ex =>

View File

@@ -226,7 +226,7 @@ partial def mkPairs (elems : Array Term) : MacroM Term :=
loop i acc
else
pure acc
loop (elems.size - 1) elems.back!
loop (elems.size - 1) elems.back
/-- Return syntax `PProd.mk elems[0] (PProd.mk elems[1] ... (PProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
partial def mkPPairs (elems : Array Term) : MacroM Term :=
@@ -238,7 +238,7 @@ partial def mkPPairs (elems : Array Term) : MacroM Term :=
loop i acc
else
pure acc
loop (elems.size - 1) elems.back!
loop (elems.size - 1) elems.back
/-- Return syntax `MProd.mk elems[0] (MProd.mk elems[1] ... (MProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
partial def mkMPairs (elems : Array Term) : MacroM Term :=
@@ -250,7 +250,7 @@ partial def mkMPairs (elems : Array Term) : MacroM Term :=
loop i acc
else
pure acc
loop (elems.size - 1) elems.back!
loop (elems.size - 1) elems.back
open Parser in

View File

@@ -136,7 +136,7 @@ def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) :
but is expected to be{indentD m!"{elhs} : { inferType elhs}"}"
failed := true
unless isDefEqGuarded rhs erhs do
logErrorAt steps.back!.term m!"\
logErrorAt steps.back.term m!"\
invalid 'calc' step, right-hand side is{indentD m!"{rhs} : { inferType rhs}"}\n\
but is expected to be{indentD m!"{erhs} : { inferType erhs}"}"
failed := true

View File

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Wojciech Nawrocki
-/
prelude
import Lean.Elab.Command
import Lean.Elab.DeclarationRange
namespace Lean.Elab
open Command
@@ -56,17 +55,13 @@ def processDefDeriving (className : Name) (declName : Name) : TermElabM Bool :=
safety := info.safety
}
addInstance instName AttributeKind.global (eval_prio default)
addDeclarationRangesFromSyntax instName ( getRef)
return true
catch _ =>
return false
end Term
def DerivingHandler := (typeNames : Array Name) CommandElabM Bool
/-- Deprecated - `DerivingHandler` no longer assumes arguments -/
@[deprecated DerivingHandler (since := "2024-09-09")]
def DerivingHandler := (typeNames : Array Name) (args? : Option (TSyntax ``Parser.Term.structInst)) CommandElabM Bool
def DerivingHandlerNoArgs := (typeNames : Array Name) CommandElabM Bool
builtin_initialize derivingHandlersRef : IO.Ref (NameMap (List DerivingHandler)) IO.mkRef {}
@@ -76,21 +71,25 @@ as well as the syntax of a `with` argument, if present.
For example, `deriving instance Foo with fooArgs for Bar, Baz` invokes
``fooHandler #[`Bar, `Baz] `(fooArgs)``. -/
def registerDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit := do
def registerDerivingHandlerWithArgs (className : Name) (handler : DerivingHandler) : IO Unit := do
unless ( initializing) do
throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")
derivingHandlersRef.modify fun m => match m.find? className with
| some handlers => m.insert className (handler :: handlers)
| none => m.insert className [handler]
/-- Like `registerBuiltinDerivingHandlerWithArgs` but ignoring any `with` argument. -/
def registerDerivingHandler (className : Name) (handler : DerivingHandlerNoArgs) : IO Unit := do
registerDerivingHandlerWithArgs className fun typeNames _ => handler typeNames
def defaultHandler (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
throwError "default handlers have not been implemented yet, class: '{className}' types: {typeNames}"
def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
def applyDerivingHandlers (className : Name) (typeNames : Array Name) (args? : Option (TSyntax ``Parser.Term.structInst)) : CommandElabM Unit := do
match ( derivingHandlersRef.get).find? className with
| some handlers =>
for handler in handlers do
if ( handler typeNames) then
if ( handler typeNames args?) then
return ()
defaultHandler className typeNames
| none => defaultHandler className typeNames
@@ -100,16 +99,16 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
Term.processDefDeriving className declName
@[builtin_command_elab «deriving»] def elabDeriving : CommandElab
| `(deriving instance $[$classes],* for $[$declNames],*) => do
| `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
let declNames liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
for cls in classes do
for cls in classes, args? in argss? do
try
let className liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
withRef cls do
if declNames.size == 1 then
if declNames.size == 1 && args?.isNone then
if ( tryApplyDefHandler className declNames[0]!) then
return ()
applyDerivingHandlers className declNames
applyDerivingHandlers className declNames args?
catch ex =>
logException ex
| _ => throwUnsupportedSyntax
@@ -117,19 +116,20 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
structure DerivingClassView where
ref : Syntax
className : Name
args? : Option (TSyntax ``Parser.Term.structInst)
def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassView) := do
match optDeriving with
| `(Parser.Command.optDeriving| deriving $[$classes],*) =>
| `(Parser.Command.optDeriving| deriving $[$classes $[with $argss?]?],*) =>
let mut ret := #[]
for cls in classes do
for cls in classes, args? in argss? do
let className realizeGlobalConstNoOverloadWithInfo cls
ret := ret.push { ref := cls, className := className }
ret := ret.push { ref := cls, className := className, args? }
return ret
| _ => return #[]
def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : CommandElabM Unit :=
withRef view.ref do applyDerivingHandlers view.className declNames
withRef view.ref do applyDerivingHandlers view.className declNames view.args?
builtin_initialize
registerTraceClass `Elab.Deriving

View File

@@ -801,7 +801,7 @@ private def mkTuple (elems : Array Syntax) : MacroM Syntax := do
else if elems.size == 1 then
return elems[0]!
else
elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back!) fun elem tuple =>
elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back) fun elem tuple =>
``(MProd.mk $elem $tuple)
/-- Return `some action` if `doElem` is a `doExpr <action>`-/

View File

@@ -60,11 +60,11 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
elabLevel (stx.getArg 1)
else if kind == ``Lean.Parser.Level.max then
let args := stx.getArg 1 |>.getArgs
args[:args.size - 1].foldrM (init := elabLevel args.back!) fun stx lvl =>
args[:args.size - 1].foldrM (init := elabLevel args.back) fun stx lvl =>
return mkLevelMax' ( elabLevel stx) lvl
else if kind == ``Lean.Parser.Level.imax then
let args := stx.getArg 1 |>.getArgs
args[:args.size - 1].foldrM (init := elabLevel args.back!) fun stx lvl =>
args[:args.size - 1].foldrM (init := elabLevel args.back) fun stx lvl =>
return mkLevelIMax' ( elabLevel stx) lvl
else if kind == ``Lean.Parser.Level.hole then
mkFreshLevelMVar

View File

@@ -957,7 +957,7 @@ where
let mut s : CollectFVars.State := {}
for discr in discrs do
s := collectFVars s ( instantiateMVars ( inferType discr))
let (indicesFVar, indicesNonFVar) := indices.partition Expr.isFVar
let (indicesFVar, indicesNonFVar) := indices.split Expr.isFVar
let indicesFVar := indicesFVar.map Expr.fvarId!
let mut toAdd := #[]
for fvarId in s.fvarSet.toList do

View File

@@ -105,6 +105,6 @@ def IndGroupInst.nestedTypeFormers (igi : IndGroupInst) : MetaM (Array Expr) :=
auxMotives.mapM fun motive =>
forallTelescopeReducing motive fun xs _ => do
assert! xs.size > 0
mkForallFVars xs.pop ( inferType xs.back!)
mkForallFVars xs.pop ( inferType xs.back)
end Lean.Elab.Structural

View File

@@ -118,7 +118,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars
-- drop trailing underscores
let mut vars := vars
while ! vars.isEmpty && vars.back!.raw.isOfKind ``hole do vars := vars.pop
while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop
if termArg.structural then
if vars.isEmpty then
`(terminationBy|termination_by structural $stxBody)

View File

@@ -190,7 +190,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
| $[some $ids:ident],* => $(quote inner)
| $[_%$ids],* => Array.empty)
| _ =>
let arr ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
let arr ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back
`(Array.map (fun $( mkTuple ids) => $(inner[0]!)) $arr)
let arr if k == `sepBy then
`(mkSepArray $arr $(getSepStxFromSplice arg))

View File

@@ -22,12 +22,7 @@ namespace Lean.Elab.Command
register_builtin_option structureDiamondWarning : Bool := {
defValue := false
descr := "if true, enable warnings when a structure has diamond inheritance"
}
register_builtin_option structure.strictResolutionOrder : Bool := {
defValue := false
descr := "if true, require a strict resolution order for structures"
descr := "enable/disable warning messages for structure diamonds"
}
open Meta
@@ -811,16 +806,9 @@ private def mkAuxConstructions (declName : Name) : TermElabM Unit := do
let hasEq := env.contains ``Eq
let hasHEq := env.contains ``HEq
let hasUnit := env.contains ``PUnit
let hasProd := env.contains ``Prod
mkRecOn declName
if hasUnit then mkCasesOn declName
if hasUnit && hasEq && hasHEq then mkNoConfusion declName
let ival getConstInfoInduct declName
if ival.isRec then
if hasUnit && hasProd then mkBelow declName
if hasUnit && hasProd then mkIBelow declName
if hasUnit && hasProd then mkBRecOn declName
if hasUnit && hasProd then mkBInductionOn declName
private def addDefaults (lctx : LocalContext) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
withLCtx lctx ( getLocalInstances) do
@@ -940,6 +928,8 @@ private def mkInductiveType (view : StructView) (indFVar : Expr) (levelNames : L
let levelParams := levelNames.map mkLevelParam
let const := mkConst view.declName levelParams
let ctorType forallBoundedTelescope ctor.type numParams fun params type => do
if type.containsFVar indFVar.fvarId! then
throwErrorAt view.ref "Recursive structures are not yet supported."
let type := type.replace fun e =>
if e == indFVar then
mkAppN const (params.extract 0 numVars)
@@ -948,23 +938,6 @@ private def mkInductiveType (view : StructView) (indFVar : Expr) (levelNames : L
instantiateMVars ( mkForallFVars params type)
return { name := view.declName, type := instantiateMVars type, ctors := [{ ctor with type := instantiateMVars ctorType }] }
/--
Precomputes the structure's resolution order.
Option `structure.strictResolutionOrder` controls whether to create a warning if the C3 algorithm failed.
-/
private def checkResolutionOrder (structName : Name) : TermElabM Unit := do
let resolutionOrderResult computeStructureResolutionOrder structName (relaxed := !structure.strictResolutionOrder.get ( getOptions))
trace[Elab.structure.resolutionOrder] "computed resolution order: {resolutionOrderResult.resolutionOrder}"
unless resolutionOrderResult.conflicts.isEmpty do
let mut defects : List MessageData := []
for conflict in resolutionOrderResult.conflicts do
let parentKind direct := if direct then "parent" else "indirect parent"
let conflicts := conflict.conflicts.map fun (isDirect, name) =>
m!"{parentKind isDirect} '{MessageData.ofConstName name}'"
defects := m!"- {parentKind conflict.isDirectParent} '{MessageData.ofConstName conflict.badParent}' \
must come after {MessageData.andList conflicts.toList}" :: defects
logWarning m!"failed to compute strict resolution order:\n{MessageData.joinSep defects.reverse "\n"}"
def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do
let scopeLevelNames Term.getLevelNames
let isUnsafe := view.modifiers.isUnsafe
@@ -1030,8 +1003,6 @@ def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit :=
else
mkCoercionToCopiedParent levelParams params view parent.structName parent.type
setStructureParents view.declName parentInfos
checkResolutionOrder view.declName
let lctx getLCtx
/- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations
The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/
@@ -1069,8 +1040,6 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
pure view
elabStructureViewPostprocessing view
builtin_initialize
registerTraceClass `Elab.structure
registerTraceClass `Elab.structure.resolutionOrder
builtin_initialize registerTraceClass `Elab.structure
end Lean.Elab.Command

View File

@@ -35,13 +35,9 @@ Reconstruct bit by bit which value expression must have had which `BitVec` value
expression - pair values.
-/
def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat))
(aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
(aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
Array (Expr × BVExpr.PackedBitVec) := Id.run do
let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {}
let filter bvBit _ :=
let (_, _, synthetic) := atomsAssignment.get! bvBit.var
!synthetic
let var2Cnf := var2Cnf.filter filter
for (bitVar, cnfVar) in var2Cnf.toArray do
/-
The setup of the variables in CNF is as follows:
@@ -74,7 +70,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
if bitValue then
value := value ||| (1 <<< currentBit)
currentBit := currentBit + 1
let (_, atomExpr, _) := atomsAssignment.get! bitVecVar
let atomExpr := atomsAssignment.get! bitVecVar |>.snd
finalMap := finalMap.push (atomExpr, BitVec.ofNat currentBit value)
return finalMap
@@ -105,7 +101,7 @@ structure UnsatProver.Result where
proof : Expr
lratCert : LratCert
abbrev UnsatProver := MVarId ReflectionResult Std.HashMap Nat (Nat × Expr × Bool)
abbrev UnsatProver := MVarId ReflectionResult Std.HashMap Nat (Nat × Expr)
MetaM (Except CounterExample UnsatProver.Result)
/--
@@ -187,7 +183,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
return err
def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult)
(atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
(atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
MetaM (Except CounterExample UnsatProver.Result) := do
let bvExpr := reflectionResult.bvExpr
let entry
@@ -257,8 +253,7 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
reflectBV g
trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
let flipper := (fun (expr, {width, atomNumber, synthetic}) => (atomNumber, (width, expr, synthetic)))
let atomsPairs := ( getThe State).atoms.toList.map flipper
let atomsPairs := ( getThe State).atoms.toList.map (fun (expr, width, ident) => (ident, (width, expr)))
let atomsAssignment := Std.HashMap.ofList atomsPairs
match unsatProver g reflectionResult atomsAssignment with
| .ok bvExprUnsat, cert =>

View File

@@ -107,25 +107,6 @@ where
open Lean.Meta
/--
A `BitVec` atom.
-/
structure Atom where
/--
The width of the `BitVec` that is being abstracted.
-/
width : Nat
/--
A unique numeric identifier for the atom.
-/
atomNumber : Nat
/--
Whether the atom is synthetic. The effect of this is that values for this atom are not considered
for the counter example deriviation. This is for example useful when we introduce an atom over
an expression, together with additional lemmas that fully describe the behavior of the atom.
-/
synthetic : Bool
/--
The state of the reflection monad
-/
@@ -134,7 +115,7 @@ structure State where
The atoms encountered so far. Saved as a map from `BitVec` expressions to a (width, atomNumber)
pair.
-/
atoms : Std.HashMap Expr Atom := {}
atoms : Std.HashMap Expr (Nat × Nat) := {}
/--
A cache for `atomsAssignment`.
-/
@@ -227,8 +208,8 @@ def run (m : M α) : MetaM α :=
Retrieve the atoms as pairs of their width and expression.
-/
def atoms : M (List (Nat × Expr)) := do
let sortedAtoms := ( getThe State).atoms.toArray.qsort (·.2.atomNumber < ·.2.atomNumber)
return sortedAtoms.map (fun (expr, {width, ..}) => (width, expr)) |>.toList
let sortedAtoms := ( getThe State).atoms.toArray.qsort (·.2.2 < ·.2.2)
return sortedAtoms.map (fun (expr, width, _) => (width, expr)) |>.toList
/--
Retrieve a `BitVec.Assignment` representing the atoms we found so far.
@@ -239,17 +220,16 @@ def atomsAssignment : M Expr := do
/--
Look up an expression in the atoms, recording it if it has not previously appeared.
-/
def lookup (e : Expr) (width : Nat) (synthetic : Bool) : M Nat := do
def lookup (e : Expr) (width : Nat) : M Nat := do
match ( getThe State).atoms[e]? with
| some atom =>
if width != atom.width then
| some (width', ident) =>
if width != width' then
panic! "The same atom occurs with different widths, this is a bug"
return atom.atomNumber
return ident
| none =>
trace[Meta.Tactic.bv] "New atom of width {width}, synthetic? {synthetic}: {e}"
trace[Meta.Tactic.bv] "New atom of width {width}: {e}"
let ident modifyGetThe State fun s =>
let newAtom := { width, synthetic, atomNumber := s.atoms.size}
(s.atoms.size, { s with atoms := s.atoms.insert e newAtom })
(s.atoms.size, { s with atoms := s.atoms.insert e (width, s.atoms.size) })
updateAtomsAssignment
return ident
where

View File

@@ -32,10 +32,10 @@ def mkBVRefl (w : Nat) (expr : Expr) : Expr :=
expr
/--
Register `e` as an atom of `width` that might potentially be `synthetic`.
Register `e` as an atom of width `width`.
-/
def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do
let ident M.lookup e width synthetic
def mkAtom (e : Expr) (width : Nat) : M ReifiedBVExpr := do
let ident M.lookup e width
let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
let proof := do
let evalExpr mkEvalExpr width expr
@@ -55,13 +55,13 @@ def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do
| _ => return none
/--
Construct an uninterpreted `BitVec` atom from `x`, potentially `synthetic`.
Construct an uninterpreted `BitVec` atom from `x`.
-/
def bitVecAtom (x : Expr) (synthetic : Bool) : M (Option ReifiedBVExpr) := do
def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do
let t instantiateMVars ( whnfR ( inferType x))
let_expr BitVec widthExpr := t | return none
let some width getNatValue? widthExpr | return none
let atom mkAtom x width synthetic
let atom mkAtom x width
return some atom
/--

View File

@@ -31,7 +31,7 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
-/
let ty inferType t
let_expr Bool := ty | return none
let atom ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1 false
let atom ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
let bvExpr : BVPred := .getLsbD atom.bvExpr 0
let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
let proof := do

View File

@@ -209,7 +209,7 @@ where
let_expr Eq α discrExpr val := discrExpr | return none
let_expr Bool := α | return none
let_expr Bool.true := val | return none
let some atom ReifiedBVExpr.bitVecAtom x true | return none
let some atom ReifiedBVExpr.bitVecAtom x | return none
let some discr ReifiedBVLogical.of discrExpr | return none
let some lhs goOrAtom lhsExpr | return none
let some rhs goOrAtom rhsExpr | return none
@@ -226,7 +226,7 @@ where
let res go x
match res with
| some exp => return some exp
| none => ReifiedBVExpr.bitVecAtom x false
| none => ReifiedBVExpr.bitVecAtom x
shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat BVUnOp)
(shiftOpName : Name) (congrThm : Name) :
@@ -316,7 +316,7 @@ where
return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
let some _, bvVal getBitVecValue? x | return ReifiedBVExpr.bitVecAtom x false
let some _, bvVal getBitVecValue? x | return ReifiedBVExpr.bitVecAtom x
ReifiedBVExpr.mkBVConst bvVal
/--

View File

@@ -112,6 +112,7 @@ builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _))
| some w', exp1Val =>
if h : w = w' then
let newLhs := exp3Val + h exp1Val
-- TODO
let expr mkAppM ``HAdd.hAdd #[toExpr newLhs, exp2]
let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_left'
return .visit { expr := expr, proof? := some proof }
@@ -177,33 +178,6 @@ def rewriteRulesPass : Pass := fun goal => do
let some (_, newGoal) := result? | return none
return newGoal
/--
Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
them to substitute occurences of `x` within other hypotheses
-/
def embeddedConstraintPass : Pass := fun goal =>
goal.withContext do
let hyps goal.getNondepPropHyps
let relevanceFilter acc hyp := do
let typ hyp.getType
let_expr Eq α _ rhs := typ | return acc
let_expr Bool := α | return acc
let_expr Bool.true := rhs | return acc
let localDecl hyp.getDecl
let proof := localDecl.toExpr
acc.addTheorem (.fvar hyp) proof
let relevantHyps : SimpTheoremsArray hyps.foldlM (init := #[]) relevanceFilter
let simpCtx : Simp.Context := {
config := { failIfUnchanged := false }
simpTheorems := relevantHyps
congrTheorems := ( getSimpCongrTheorems)
}
let result?, _ simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := hyps)
let some (_, newGoal) := result? | return none
return newGoal
/--
Normalize with respect to Associativity and Commutativity.
-/
@@ -222,7 +196,7 @@ def acNormalizePass : Pass := fun goal => do
/--
The normalization passes used by `bv_normalize` and thus `bv_decide`.
-/
def defaultPipeline : List Pass := [rewriteRulesPass, embeddedConstraintPass]
def defaultPipeline : List Pass := [rewriteRulesPass]
def passPipeline : MetaM (List Pass) := do
let opts getOptions
@@ -248,8 +222,8 @@ def evalBVNormalize : Tactic := fun
| `(tactic| bv_normalize) => do
let g getMainGoal
match bvNormalize g with
| some newGoal => replaceMainGoal [newGoal]
| none => replaceMainGoal []
| some newGoal => setGoals [newGoal]
| none => setGoals []
| _ => throwUnsupportedSyntax
end Frontend.Normalize

View File

@@ -263,26 +263,19 @@ private def getOptRotation (stx : Syntax) : Nat :=
@[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
let mvarIds getGoals
let mut mvarIdsNew := #[]
let mut abort := false
let mut mctxSaved getMCtx
for mvarId in mvarIds do
unless ( mvarId.isAssigned) do
setGoals [mvarId]
abort Tactic.tryCatch
mvarIdsNew Tactic.tryCatch
(do
evalTactic stx[1]
pure abort)
return mvarIdsNew ++ ( getUnsolvedGoals))
(fun ex => do
if ( read).recover then
logException ex
pure true
return mvarIdsNew.push mvarId
else
throw ex)
mvarIdsNew := mvarIdsNew ++ ( getUnsolvedGoals)
if abort then
setMCtx mctxSaved
mvarIds.forM fun mvarId => unless ( mvarId.isAssigned) do admitGoal mvarId
throwAbortTactic
setGoals mvarIdsNew.toList
@[builtin_tactic Parser.Tactic.anyGoals] def evalAnyGoals : Tactic := fun stx => do
@@ -472,7 +465,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
let inaccessible := !(extractMacroScopes localDecl.userName |>.equalScope callerScopes)
let shadowed := found.contains localDecl.userName
if inaccessible || shadowed then
if let `(binderIdent| $h:ident) := hs.back! then
if let `(binderIdent| $h:ident) := hs.back then
let newName := h.getId
lctx := lctx.setUserName localDecl.fvarId newName
info := info.push (localDecl.fvarId, h)

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Kyle Miller
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Eval
@@ -10,174 +10,25 @@ import Lean.Elab.SyntheticMVars
import Lean.Linter.MissingDocs
namespace Lean.Elab.Tactic
open Meta Parser.Tactic Command
private structure ConfigItemView where
ref : Syntax
option : Ident
value : Term
/-- Whether this was using `+`/`-`, to be able to give a better error message on type mismatch. -/
(bool : Bool := false)
/-- Interprets the `config` as an array of option/value pairs. -/
private def mkConfigItemViews (c : TSyntaxArray ``configItem) : Array ConfigItemView :=
c.map fun item =>
match item with
| `(configItem| ($option:ident := $value)) => { ref := item, option, value }
| `(configItem| +$option) => { ref := item, option, bool := true, value := mkCIdentFrom item ``true }
| `(configItem| -$option) => { ref := item, option, bool := true, value := mkCIdentFrom item ``false }
| `(config| (config%$tk := $value)) => { ref := item, option := mkCIdentFrom tk `config, value := value }
| _ => { ref := item, option := Syntax.missing, value := Syntax.missing }
/--
Expands a field access into full field access like `toB.toA.x`.
Returns that and the last projection function for `x` itself.
-/
private def expandFieldName (structName : Name) (fieldName : Name) : MetaM (Name × Name) := do
let env getEnv
unless isStructure env structName do throwError "'{.ofConstName structName}' is not a structure"
let some baseStructName := findField? env structName fieldName
| throwError "structure '{.ofConstName structName}' does not have a field named '{fieldName}'"
let some path := getPathToBaseStructure? env baseStructName structName
| throwError "(internal error) failed to access field '{fieldName}' in parent structure"
let field := path.foldl (init := .anonymous) (fun acc s => Name.appendCore acc <| Name.mkSimple s.getString!) ++ fieldName
let fieldInfo := (getFieldInfo? env baseStructName fieldName).get!
return (field, fieldInfo.projFn)
/--
Given a hierarchical name `field`, returns the fully resolved field access, the base struct name, and the last projection function.
-/
private partial def expandField (structName : Name) (field : Name) : MetaM (Name × Name) := do
match field with
| .num .. | .anonymous => throwError m!"invalid configuration field"
| .str .anonymous fieldName => expandFieldName structName (Name.mkSimple fieldName)
| .str field' fieldName =>
let (field', projFn) expandField structName field'
let notStructure {α} : MetaM α := throwError "field '{field'}' of structure '{.ofConstName structName}' is not a structure"
let .const structName' _ := ( getConstInfo projFn).type.getForallBody | notStructure
unless isStructure ( getEnv) structName' do notStructure
let (field'', projFn) expandFieldName structName' (Name.mkSimple fieldName)
return (field' ++ field'', projFn)
/-- Elaborates a tactic configuration. -/
private def elabConfig (recover : Bool) (structName : Name) (items : Array ConfigItemView) : TermElabM Expr :=
withoutModifyingStateWithInfoAndMessages <| withLCtx {} {} <| withSaveInfoContext do
let mkStructInst (source? : Option Term) (fields : TSyntaxArray ``Parser.Term.structInstField) : TermElabM Term :=
match source? with
| some source => `({$source with $fields* : $(mkCIdent structName)})
| none => `({$fields* : $(mkCIdent structName)})
let mut source? : Option Term := none
let mut seenFields : NameSet := {}
let mut fields : TSyntaxArray ``Parser.Term.structInstField := #[]
for item in items do
try
let option := item.option.getId.eraseMacroScopes
if option == `config then
unless fields.isEmpty do
-- Flush fields. Even though these values will not be used, we still want to elaborate them.
source? mkStructInst source? fields
seenFields := {}
fields := #[]
let valSrc withRef item.value `(($item.value : $(mkCIdent structName)))
if let some source := source? then
source? withRef item.value `({$valSrc, $source with : $(mkCIdent structName)})
else
source? := valSrc
else
addCompletionInfo <| CompletionInfo.fieldId item.option option {} structName
let (path, projFn) withRef item.option <| expandField structName option
if item.bool then
-- Verify that the type is `Bool`
unless ( getConstInfo projFn).type.bindingBody! == .const ``Bool [] do
throwErrorAt item.ref m!"option is not boolean-valued, so '({option} := ...)' syntax must be used"
let value
match item.value with
| `(by $seq:tacticSeq) =>
-- Special case: `(opt := by tacs)` uses the `tacs` syntax itself
withRef item.value <| `(Unhygienic.run `(tacticSeq| $seq))
| value => pure value
if seenFields.contains path then
-- Flush fields. There is a duplicate, but we still want to elaborate both.
source? mkStructInst source? fields
seenFields := {}
fields := #[]
fields := fields.push <| `(Parser.Term.structInstField|
$(mkCIdentFrom item.option path (canonical := true)):ident := $value)
seenFields := seenFields.insert path
catch ex =>
if recover then
logException ex
else
throw ex
let stx : Term mkStructInst source? fields
let e Term.withSynthesize <| Term.elabTermEnsuringType stx (mkConst structName)
instantiateMVars e
private def mkConfigElaborator
(doc? : Option (TSyntax ``Parser.Command.docComment)) (elabName type monadName : Ident)
(adapt recover : Term) : MacroM (TSyntax `command) := do
let empty withRef type `({ : $type})
`(unsafe def evalUnsafe (e : Expr) : TermElabM $type :=
Meta.evalExpr' (safety := .unsafe) $type ``$type e
@[implemented_by evalUnsafe] opaque eval (e : Expr) : TermElabM $type
$[$doc?:docComment]?
def $elabName (optConfig : Syntax) : $monadName $type := $adapt do
let recover := $recover
let go : TermElabM $type := withRef optConfig do
let items := mkConfigItemViews (getConfigItems optConfig)
if items.isEmpty then
return $empty
unless ( getEnv).contains ``$type do
throwError m!"error evaluating configuration, environment does not yet contain type {``$type}"
let c elabConfig recover ``$type items
if c.hasSyntheticSorry then
-- An error is already logged, return the default.
return $empty
if c.hasSorry then
throwError m!"configuration contains 'sorry'"
try
let res eval c
return res
catch ex =>
let msg := m!"error evaluating configuration\n{indentD c}\n\nException: {ex.toMessageData}"
if false then
logError msg
return $empty
else
throwError msg
go)
/-!
`declare_config_elab elabName TypeName` declares a function `elabName : Syntax → TacticM TypeName`
that elaborates a tactic configuration.
The tactic configuration can be from `Lean.Parser.Tactic.optConfig` or `Lean.Parser.Tactic.config`,
and these can also be wrapped in null nodes (for example, from `(config)?`).
The elaborator responds to the current recovery state.
For defining elaborators for commands, use `declare_command_config_elab`.
-/
macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ident type:ident : command => do
mkConfigElaborator doc? elabName type (mkCIdent ``TacticM) (mkCIdent ``id) ( `(( read).recover))
open Meta
macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ident type:ident : command =>
`(unsafe def evalUnsafe (e : Expr) : TermElabM $type :=
Meta.evalExpr' (safety := .unsafe) $type ``$type e
@[implemented_by evalUnsafe] opaque eval (e : Expr) : TermElabM $type
$[$doc?:docComment]?
def $elabName (optConfig : Syntax) : TermElabM $type := do
if optConfig.isNone then
return { : $type }
else
let c withoutModifyingStateWithInfoAndMessages <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do
let c Term.elabTermEnsuringType optConfig[0][3] (Lean.mkConst ``$type)
Term.synthesizeSyntheticMVarsNoPostponing
instantiateMVars c
eval c
)
open Linter.MissingDocs in
@[builtin_missing_docs_handler Elab.Tactic.configElab]
def checkConfigElab : SimpleHandler := mkSimpleHandler "config elab"
/-!
`declare_command_config_elab elabName TypeName` declares a function `elabName : Syntax → CommandElabM TypeName`
that elaborates a command configuration.
The configuration can be from `Lean.Parser.Tactic.optConfig` or `Lean.Parser.Tactic.config`,
and these can also be wrapped in null nodes (for example, from `(config)?`).
The elaborator has error recovery enabled.
-/
macro (name := commandConfigElab) doc?:(docComment)? "declare_command_config_elab" elabName:ident type:ident : command => do
mkConfigElaborator doc? elabName type (mkCIdent ``CommandElabM) (mkCIdent ``liftTermElabM) (mkCIdent ``true)
open Linter.MissingDocs in
@[builtin_missing_docs_handler Elab.Tactic.commandConfigElab]
def checkCommandConfigElab : SimpleHandler := mkSimpleHandler "config elab"
end Lean.Elab.Tactic

View File

@@ -11,8 +11,6 @@ import Lean.Elab.Tactic.Conv.Basic
namespace Lean.Elab.Tactic.Conv
open Meta
@[builtin_tactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun _ => pure ()
private def congrImplies (mvarId : MVarId) : MetaM (List MVarId) := do
let [mvarId₁, mvarId₂, _, _] mvarId.apply ( mkConstWithFreshMVarLevels ``implies_congr) | throwError "'apply implies_congr' unexpected result"
let mvarId₁ markAsConvGoal mvarId₁
@@ -74,14 +72,6 @@ private partial def mkCongrThm (origTag : Name) (f : Expr) (args : Array Expr) (
mvarIdsNewInsts := mvarIdsNewInsts ++ mvarIdsNewInsts'
return (proof, mvarIdsNew, mvarIdsNewInsts)
private def resolveRhs (tacticName : String) (rhs rhs' : Expr) : MetaM Unit := do
unless ( isDefEqGuarded rhs rhs') do
throwError "invalid '{tacticName}' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
private def resolveRhsFromProof (tacticName : String) (rhs proof : Expr) : MetaM Unit := do
let some (_, _, rhs') := ( whnf ( inferType proof)).eq? | throwError "'{tacticName}' conv tactic failed, equality expected"
resolveRhs tacticName rhs rhs'
def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
MetaM (List (Option MVarId)) := mvarId.withContext do
let origTag mvarId.getTag
@@ -92,7 +82,9 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
else if lhs.isApp then
let (proof, mvarIdsNew, mvarIdsNewInsts)
mkCongrThm origTag lhs.getAppFn lhs.getAppArgs addImplicitArgs nameSubgoals
resolveRhsFromProof "congr" rhs proof
let some (_, _, rhs') := ( whnf ( inferType proof)).eq? | throwError "'congr' conv tactic failed, equality expected"
unless ( isDefEqGuarded rhs rhs') do
throwError "invalid 'congr' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
mvarId.assign proof
return mvarIdsNew.toList ++ mvarIdsNewInsts.toList
else
@@ -101,7 +93,42 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
@[builtin_tactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do
replaceMainGoal <| List.filterMap id ( congr ( getMainGoal))
/-- Implementation of `arg 0`. -/
-- mvarIds is the list of goals produced by congr. We only want to change the one at position `i`
-- so this closes all other equality goals with `rfl.`. There are non-equality goals produced
-- by `congr` (e.g. dependent instances), these are kept as goals.
private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
TacticM Unit := do
if i >= 0 then
let i := i.toNat
if h : i < mvarIds.length then
let mut otherGoals := #[]
for mvarId? in mvarIds, j in [:mvarIds.length] do
match mvarId? with
| none => pure ()
| some mvarId =>
if i != j then
if ( mvarId.getType').isEq then
mvarId.refl
else
-- If its not an equality, it's likely a class constraint, to be left open
otherGoals := otherGoals.push mvarId
match mvarIds[i] with
| none => throwError "cannot select argument"
| some mvarId => replaceMainGoal (mvarId :: otherGoals.toList)
return ()
throwError "invalid '{tacticName}' conv tactic, application has only {mvarIds.length} (nondependent) argument(s)"
@[builtin_tactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun _ => pure ()
@[builtin_tactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun _ => do
let mvarIds congr ( getMainGoal) (nameSubgoals := false)
selectIdx "lhs" mvarIds ((mvarIds.length : Int) - 2)
@[builtin_tactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun _ => do
let mvarIds congr ( getMainGoal) (nameSubgoals := false)
selectIdx "rhs" mvarIds ((mvarIds.length : Int) - 1)
/-- Implementation of `arg 0` -/
def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
let (lhs, rhs) getLhsRhsCore mvarId
let lhs := ( instantiateMVars lhs).cleanupAnnotations
@@ -109,137 +136,24 @@ def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
throwError "invalid 'arg 0' conv tactic, application expected{indentExpr lhs}"
lhs.withApp fun f xs => do
let (g, mvarNew) mkConvGoalFor f
mvarId.assign ( xs.foldlM (init := mvarNew) Meta.mkCongrFun)
resolveRhs "arg 0" rhs (mkAppN g xs)
mvarId.assign ( xs.foldlM (fun mvar a => Meta.mkCongrFun mvar a) mvarNew)
let rhs' := mkAppN g xs
unless isDefEqGuarded rhs rhs' do
throwError "invalid 'arg 0' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
return mvarNew.mvarId!
private partial def mkCongrArgZeroThm (tacticName : String) (origTag : Name) (f : Expr) (args : Array Expr) :
MetaM (Expr × MVarId × Array MVarId) := do
let funInfo getFunInfoNArgs f args.size
let some congrThm mkCongrSimpCore? f funInfo ( getCongrSimpKindsForArgZero funInfo) (subsingletonInstImplicitRhs := false)
| throwError "'{tacticName}' conv tactic failed to create congruence theorem"
unless congrThm.argKinds[0]! matches .eq do
throwError "'{tacticName}' conv tactic failed, cannot select argument"
let mut eNew := f
let mut proof := congrThm.proof
let mut mvarIdNew? := none
let mut mvarIdsNewInsts := #[]
for h : i in [:congrThm.argKinds.size] do
let arg := args[i]!
let argInfo := funInfo.paramInfo[i]!
match congrThm.argKinds[i] with
| .fixed | .cast =>
eNew := mkApp eNew arg
proof := mkApp proof arg
| .eq =>
let (rhs, mvarNew) mkConvGoalFor arg origTag
eNew := mkApp eNew rhs
proof := mkApp3 proof arg rhs mvarNew
if mvarIdNew?.isSome then throwError "'{tacticName}' conv tactic failed, cannot select argument"
mvarIdNew? := some mvarNew.mvarId!
| .subsingletonInst =>
proof := mkApp proof arg
let rhs mkFreshExprMVar ( whnf ( inferType proof)).bindingDomain!
eNew := mkApp eNew rhs
proof := mkApp proof rhs
mvarIdsNewInsts := mvarIdsNewInsts.push rhs.mvarId!
| .heq | .fixedNoParam => unreachable!
let proof' args[congrThm.argKinds.size:].foldlM (init := proof) mkCongrFun
return (proof', mvarIdNew?.get!, mvarIdsNewInsts)
/--
Implements `arg` for foralls. If `domain` is true, accesses the domain, otherwise accesses the codomain.
-/
def congrArgForall (tacticName : String) (domain : Bool) (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List MVarId) := do
let .forallE n t b bi := lhs | unreachable!
if domain then
if !b.hasLooseBVars then
let (t', g) mkConvGoalFor t ( mvarId.getTag)
mvarId.assign <| mkAppM ``implies_congr #[g, mkEqRefl b]
resolveRhs tacticName rhs (.forallE n t' b bi)
return [g.mvarId!]
else if isProp b <&&> isProp lhs then
let (_rhs, g) mkConvGoalFor t ( mvarId.getTag)
let proof mkAppM ``forall_prop_congr_dom #[g, .lam n t b .default]
resolveRhsFromProof tacticName rhs proof
mvarId.assign proof
return [g.mvarId!]
else
throwError m!"'{tacticName}' conv tactic failed, cannot select domain"
else
withLocalDeclD ( mkFreshUserName n) t fun arg => do
let u getLevel t
let q := b.instantiate1 arg
let (q', g) mkConvGoalFor q ( mvarId.getTag)
let v getLevel q
let proof := mkAppN (.const ``pi_congr [u, v])
#[t, .lam n t b .default, mkLambdaFVars #[arg] q', mkLambdaFVars #[arg] g]
resolveRhsFromProof tacticName rhs proof
mvarId.assign proof
return [g.mvarId!]
/-- Implementation of `arg i`. -/
def congrArgN (tacticName : String) (mvarId : MVarId) (i : Int) (explicit : Bool) : MetaM (List MVarId) := mvarId.withContext do
let (lhs, rhs) getLhsRhsCore mvarId
let lhs := ( instantiateMVars lhs).cleanupAnnotations
if lhs.isForall then
if i < -2 || i == 0 || i > 2 then throwError "invalid '{tacticName}' conv tactic, index is out of bounds for pi type"
let domain := i == 1 || i == -2
return congrArgForall tacticName domain mvarId lhs rhs
else if lhs.isApp then
lhs.withApp fun f xs => do
let (f, xs) applyArgs f xs i
let (proof, mvarIdNew, mvarIdsNewInsts) mkCongrArgZeroThm tacticName ( mvarId.getTag) f xs
resolveRhsFromProof tacticName rhs proof
mvarId.assign proof
return mvarIdNew :: mvarIdsNewInsts.toList
else
throwError "invalid '{tacticName}' conv tactic, application or implication expected{indentExpr lhs}"
where
applyArgs (f : Expr) (xs : Array Expr) (i : Int) : MetaM (Expr × Array Expr) := do
if explicit then
let i := if i > 0 then i - 1 else i + xs.size
if i < 0 || i xs.size then
throwError "invalid '{tacticName}' tactic, application has {xs.size} arguments but the index is out of bounds"
let idx := i.natAbs
return (mkAppN f xs[0:idx], xs[idx:])
else
let mut fType inferType f
let mut j := 0
let mut explicitIdxs := #[]
for k in [0:xs.size] do
unless fType.isForall do
fType withTransparency .all <| whnf (fType.instantiateRevRange j k xs)
j := k
let .forallE _ _ b bi := fType | failure
fType := b
if bi.isExplicit then
explicitIdxs := explicitIdxs.push k
let i := if i > 0 then i - 1 else i + explicitIdxs.size
if i < 0 || i explicitIdxs.size then
throwError "invalid '{tacticName}' tactic, application has {xs.size} explicit argument(s) but the index is out of bounds"
let idx := explicitIdxs[i.natAbs]!
return (mkAppN f xs[0:idx], xs[idx:])
def evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit := do
if i == 0 then
replaceMainGoal [ congrFunN ( getMainGoal)]
else
replaceMainGoal ( congrArgN tacticName ( getMainGoal) i explicit)
@[builtin_tactic Lean.Parser.Tactic.Conv.arg] def elabArg : Tactic := fun stx => do
@[builtin_tactic Lean.Parser.Tactic.Conv.arg] def evalArg : Tactic := fun stx => do
match stx with
| `(conv| arg $[@%$tk?]? $[-%$neg?]? $i:num) =>
let i : Int := if neg?.isSome then -i.getNat else i.getNat
evalArg "arg" i (explicit := tk?.isSome)
| `(conv| arg $[@%$tk?]? $i:num) =>
let i := i.getNat
if i == 0 then
replaceMainGoal [ congrFunN ( getMainGoal)]
else
let i := i - 1
let mvarIds congr ( getMainGoal) (addImplicitArgs := tk?.isSome) (nameSubgoals := false)
selectIdx "arg" mvarIds i
| _ => throwUnsupportedSyntax
@[builtin_tactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun _ => do
evalArg "lhs" (-2) false
@[builtin_tactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun _ => do
evalArg "rhs" (-1) false
@[builtin_tactic Lean.Parser.Tactic.Conv.«fun»] def evalFun : Tactic := fun _ => do
let mvarId getMainGoal
mvarId.withContext do
@@ -249,7 +163,9 @@ def evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit :=
| throwError "invalid 'fun' conv tactic, application expected{indentExpr lhs}"
let (g, mvarNew) mkConvGoalFor f
mvarId.assign ( Meta.mkCongrFun mvarNew a)
resolveRhs "fun" rhs (.app g a)
let rhs' := .app g a
unless isDefEqGuarded rhs rhs' do
throwError "invalid 'fun' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
replaceMainGoal [mvarNew.mvarId!]
def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId) := do
@@ -293,7 +209,9 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
let (qa, mvarNew) mkConvGoalFor pa
let q mkLambdaFVars #[a] qa
let h mkLambdaFVars #[a] mvarNew
resolveRhs "ext" rhs ( mkForallFVars #[a] qa)
let rhs' mkForallFVars #[a] qa
unless ( isDefEqGuarded rhs rhs') do
throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
return (q, h, mvarNew)
let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
mvarId.assign proof
@@ -320,22 +238,4 @@ private def ext (userName? : Option Name) : TacticM Unit := do
for id in ids do
withRef id <| ext id.getId
-- syntax (name := enter) "enter" " [" enterArg,+ "]" : conv
@[builtin_tactic Lean.Parser.Tactic.Conv.enter] def evalEnter : Tactic := fun stx => do
let token := stx[0]
let lbrak := stx[1]
let enterArgsAndSeps := stx[2].getArgs
-- show initial state up to (incl.) `[`
withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
let numEnterArgs := (enterArgsAndSeps.size + 1) / 2
for i in [:numEnterArgs] do
let enterArg := enterArgsAndSeps[2 * i]!
let sep := enterArgsAndSeps.getD (2 * i + 1) .missing
-- show state up to (incl.) next `,` and show errors on `enterArg`
withTacticInfoContext (mkNullNode #[enterArg, sep]) <| withRef enterArg do
match enterArg with
| `(Parser.Tactic.Conv.enterArg| $arg:argArg) => evalTactic ( `(conv| arg $arg))
| `(Parser.Tactic.Conv.enterArg| $id:ident) => evalTactic ( `(conv| ext $id))
| _ => pure ()
end Lean.Elab.Tactic.Conv

View File

@@ -208,28 +208,15 @@ private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM N
private def isWildcard (altStx : Syntax) : Bool :=
getAltName altStx == `_
private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit := do
let mut seenNames : Array Name := #[]
private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
for h : i in [:altsSyntax.size] do
let altStx := altsSyntax[i]
if getAltName altStx == `_ && i != altsSyntax.size - 1 then
withRef altStx <| throwError "invalid occurrence of wildcard alternative, it must be the last alternative"
let altName := getAltName altStx
if altName != `_ then
if seenNames.contains altName then
throwErrorAt altStx s!"duplicate alternative name '{altName}'"
seenNames := seenNames.push altName
unless alts.any (·.name == altName) do
let unhandledAlts := alts.filter fun alt => !seenNames.contains alt.name
let msg :=
if unhandledAlts.isEmpty then
m!"invalid alternative name '{altName}', no unhandled alternatives"
else
let unhandledAltsMessages := unhandledAlts.map (m!"{·.name}")
let unhandledAlts := MessageData.orList unhandledAltsMessages.toList
m!"invalid alternative name '{altName}', expected {unhandledAlts}"
throwErrorAt altStx msg
throwErrorAt altStx "invalid alternative name '{altName}'"
/-- Given the goal `altMVarId` for a given alternative that introduces `numFields` new variables,
return the number of explicit variables. Recall that when the `@` is not used, only the explicit variables can

View File

@@ -696,9 +696,9 @@ the tactic call `aesop (add 50% tactic Lean.Omega.omegaDefault)`. -/
def omegaDefault : TacticM Unit := omegaTactic {}
@[builtin_tactic Lean.Parser.Tactic.omega]
def evalOmega : Tactic
| `(tactic| omega $cfg:optConfig) => do
let cfg elabOmegaConfig cfg
def evalOmega : Tactic := fun
| `(tactic| omega $[$cfg]?) => do
let cfg elabOmegaConfig (mkOptionalNode cfg)
omegaTactic cfg
| _ => throwUnsupportedSyntax

View File

@@ -85,7 +85,7 @@ private def mkDischargeWrapper (optDischargeSyntax : Syntax) : TacticM Simp.Disc
/-
`optConfig` is of the form `("(" "config" ":=" term ")")?`
-/
def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.Config := do
def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.Config := do
match kind with
| .simp => elabSimpConfigCore optConfig
| .simpAll => return ( elabSimpConfigCtxCore optConfig).toConfig
@@ -437,7 +437,7 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
Simp.reportDiag stats
/-
"simp" optConfig (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
"simp" (config)? (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
(location)?
-/
@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do

View File

@@ -25,11 +25,11 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
@[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
match stx with
| `(tactic|
simp?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
let stx if bang.isSome then
`(tactic| simp!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
`(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
else
`(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]? $(loc)?)
`(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
let { ctx, simprocs, dischargeWrapper } mkSimpContext stx (eraseLocal := false)
let stats dischargeWrapper.with fun discharge? =>
simpLocation ctx (simprocs := simprocs) discharge? <|
@@ -41,11 +41,11 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
@[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
match stx with
| `(tactic| simp_all?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
| `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
let stx if bang.isSome then
`(tactic| simp_all!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
`(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
else
`(tactic| simp_all%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
`(tactic| simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
let { ctx, .. } mkSimpContext stx (eraseLocal := true)
(kind := .simpAll) (ignoreStarArg := true)
let (result?, stats) simpAll ( getMainGoal) ctx
@@ -81,11 +81,11 @@ where
@[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
match stx with
| `(tactic| dsimp?%$tk $[!%$bang]? $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
| `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
let stx if bang.isSome then
`(tactic| dsimp!%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?)
`(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
else
`(tactic| dsimp%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?)
`(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
let { ctx, simprocs, .. }
withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
let stats dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)

View File

@@ -31,9 +31,9 @@ deriving instance Repr for UseImplicitLambdaResult
@[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
match stx with
| `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $cfg:optConfig $(disch)? $[only%$only]?
| `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
$[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
let stx `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
let stx `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
let { ctx, simprocs, dischargeWrapper }
withMainContext <| mkSimpContext stx (eraseLocal := false)
let ctx := if unfold.isSome then { ctx with config.autoUnfold := true } else ctx
@@ -96,11 +96,11 @@ deriving instance Repr for UseImplicitLambdaResult
g.assumption; pure stats
if tactic.simp.trace.get ( getOptions) || squeeze.isSome then
let stx match mkSimpOnly stx stats.usedTheorems with
| `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
| `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?) =>
if unfold.isSome then
`(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
`(tactic| simpa! $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
else
`(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
`(tactic| simpa $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
| _ => unreachable!
TryThis.addSuggestion tk stx (origSpan? := getRef)
return stats.diag

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