Compare commits

...

50 Commits

Author SHA1 Message Date
Kim Morrison
e9efd52f22 feat: add @[grind ext] attributes for extensional maps 2025-10-28 16:13:47 +11:00
Kim Morrison
1981c62604 feat: make grind +premises more robust to bad suggestions (#10992)
This PR ensures that `grind +premises` silently drops warnings and
errors about bad suggestions.
2025-10-28 03:22:42 +00:00
Leonardo de Moura
bb3dd13f72 feat: set_config for setting grind configuration options (#10990)
This PR adds the `set_config` tactic for setting `grind` configuration
options. It uses the same syntax used for setting configuration options
in the `grind` main tactic.
2025-10-28 02:25:01 +00:00
Joachim Breitner
808d123e6f doc: typo in grindDef docstring (#10988)
This PR fixes a typo in the `grindDef` docstring.
2025-10-27 15:59:06 +00:00
Joachim Breitner
14d76cc062 fix: decreasing_by: preserve variable names of match alts (#10980)
This PR tries to preserve names of pattern variables in match
alternatives in `decreasing_by`, by telescoping into the concrete
alternative rather than the type of the matcher's alt. Fixes #10976.
2025-10-27 14:00:36 +00:00
Markus Himmel
d2f76ade61 fix: search for empty string (#10985)
This PR ensures that searching for an empty string returns the expected
pattern of alternating size-zero matches and size-one rejects.

In particular, splitting by an empty string returns an array formed of
the empty string, all of the string's characters as singleton strings,
followed by another empty string. This matches the [Rust
behavior](https://doc.rust-lang.org/std/primitive.str.html#method.split),
for example.
2025-10-27 13:05:33 +00:00
Rob23oba
12750d25b5 perf: inline decidable instances (#10934)
This PR adds inline annotations to several `Decidable` instances.
Additionally, it removes the `Decidable` instance for `p → q` which is
made redundant by `forall_prop_decidable`.
2025-10-27 12:05:01 +00:00
Henrik Böving
334fa475b4 fix: use general allocator for closures (#10982)
This PR changes the closure allocator to use the general allocator
instead of the small object one.
This is because users may create closures with a gigantic amount of
closed variables which in turn
boost the size of the closure beyond the small object threshold.

This issue was uncovered by #10979. Detecting that the small object
threshold is at fault requires
building mimalloc in debug mode at which point it yields:
```
mimalloc: assertion failed: at "/home/henrik/lean4/build/debug/mimalloc/src/mimalloc/src/alloc.c":132, mi_heap_malloc_small_zero
  assertion: "size <= MI_SMALL_SIZE_MAX"
```
The generated code at fault here looks as follows:
```c
LEAN_EXPORT lean_object* l_initExec___at___00res_spec__0(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_2 = lean_alloc_closure((void*)(l_initializer_ext___at___00initExec___at___00res_spec__0_spec__0___lam__0___boxed), 3, 0);
x_3 = l_initExec___redArg___closed__0;
x_4 = l_initExec___redArg___closed__1;
x_5 = l_instMonadLiftNonDetT___closed__0;
x_6 = l_initExec___redArg___closed__2;
x_7 = l_initExec___at___00res_spec__0___closed__0;
lean_inc_ref(x_2);
x_8 = lean_alloc_closure((void*)(l_initExec___at___00res_spec__0___lam__29___boxed), 213, 212);
lean_closure_set(x_8, 0, x_3);
lean_closure_set(x_8, 1, x_2);
lean_closure_set(x_8, 2, x_4);
lean_closure_set(x_8, 3, x_3);
lean_closure_set(x_8, 4, x_4);
lean_closure_set(x_8, 5, x_3);
lean_closure_set(x_8, 6, x_4);
lean_closure_set(x_8, 7, x_3);
lean_closure_set(x_8, 8, x_4);
lean_closure_set(x_8, 9, x_3);
lean_closure_set(x_8, 10, x_4);
lean_closure_set(x_8, 11, x_3);
lean_closure_set(x_8, 12, x_4);
lean_closure_set(x_8, 13, x_3);
lean_closure_set(x_8, 14, x_4);
lean_closure_set(x_8, 15, x_5);
lean_closure_set(x_8, 16, x_6);
lean_closure_set(x_8, 17, x_5);
lean_closure_set(x_8, 18, x_5);
lean_closure_set(x_8, 19, x_5);
lean_closure_set(x_8, 20, x_5);
lean_closure_set(x_8, 21, x_5);
lean_closure_set(x_8, 22, x_5);
...
```
With the crash happening in `lean_alloc_closure` where we
unconditionally invoke the small allocator
which cannot cope with closures this large. Hopefully changing this to
the general purpose allocator
doesn't have too much of an impact on performance.

Closes: #10979
2025-10-27 10:16:59 +00:00
Markus Himmel
8fe260de55 feat: termination arguments for String.ValidPos and String.Slice.Pos (#10933)
This PR adds the basic infrastructure to perform termination proofs
about `String.ValidPos` and `String.Slice.Pos`.

We choose approach where the intended way to do termination arguments is
to argue about the position itself rather than some projection of it
like `remainingBytes`.

The types `String.ValidPos` and `String.Slice.Pos` are equipped with a
`WellFoundedRelation` instance given by the greater-than relation. This
means that if a function takes a position `p` and performs a recursive
call on `q`, then the decreasing obligation will be `p < q`. This works
well in the common case where `q` is `p.next h`, in which case the goal
`p < p.next h` is solved by the simplifier.

For stepping through a string backwards, we introduce a type synonym
with a `WellFoundedRelation` instance given by the less-than relation.
This means that if a function takes a position `p` and performs a
recursive call on `q` and specifies `termination_by p.down`, then the
decreasing obligation will be `q < p`. This works well in the case where
`q` is `p.prev h`, in which case the goal `p.prev h < p` is solved by
the simplifier.

For termination arguments invoving multiple strings, the lower-level
primitive `p.remainingBytes` (landing in `Nat`) is also available.

In a future PR, we will additionally provide the necessary typeclasses
instances to register `String.ValidPos` and `String.Slice.Pos` with
`grind` to make complex termination arguments more convenient in user
code.
2025-10-27 10:05:44 +00:00
Henrik Böving
7e1be20317 perf: widen more in ElimDeadBranches (#10856)
This PR performs more widening in ElimDeadBranches in an attempt to
improve performance in situations with a lot of local precision.

While this is not enough to make the compilation instant it pushes
compilation time from 12s to 3s for the example in #10857 and barely
introduces regressions so it seems like a good first step in this
direction.

Closes: #10857
2025-10-27 09:12:16 +00:00
Leonardo de Moura
3a42ee0c30 feat: grind tactic mode improvements (#10978)
This PR implements the following `grind` improvements:
1. `set_option` can now be used to set `grind` configuration options in
the interactive mode.
2. Fixes a bug in the repeated theorem instantiation detection.
3. Adds the macro `use [...]` as a shorthand for `instantiate only
[...]`.
2025-10-27 04:47:02 +00:00
Kim Morrison
30ecacd625 feat: add LawfulOfScientific class (#10971)
This PR adds a `LawfulOfScientific` class, providing compatibility with
a `Lean.Grind.Field` structure.
2025-10-27 04:18:55 +00:00
Kim Morrison
a0e742be5e chore: >6 month old deprecations (#10969) 2025-10-26 22:48:41 +00:00
Leonardo de Moura
50e2fdaa74 feat: add cdot combinator in grind tactic mode (#10975)
This PR adds the combinator ` · t_1 ... t_n` to the `grind` interactive
mode. The `finish?` tactic now generates scripts using this combinator
to conform to Mathlib coding standards. The new format is also more
compact. Example:
```lean
/--
info: Try this:
  [apply] ⏎
    instantiate only [= mem_indices_of_mem, insert, = getElem_def]
    instantiate only [= getElem?_neg, = getElem?_pos]
    cases #f590
    · cases #ffdf
      · instantiate only
        instantiate only [= Array.getElem_set]
      · instantiate only
        instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
    · instantiate only [= mem_indices_of_mem, = getElem_def]
      instantiate only [usr getElem_indices_lt]
      instantiate only [size]
      cases #ffdf
      · instantiate only [=_ WF]
        instantiate only [= getElem?_neg, = getElem?_pos, = Array.getElem_set]
        instantiate only [WF']
      · instantiate only
        instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
-/
#guard_msgs in
example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
    (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
  grind => finish?
```
2025-10-26 21:27:00 +00:00
Sebastian Ullrich
77ddfd49e6 chore: further shake improvements (#10947) 2025-10-26 11:27:19 +00:00
Kim Morrison
4887eeb77c chore: remove >6 month old deprecations (#10968) 2025-10-26 10:01:30 +00:00
Kim Morrison
9cf2877945 fix: mis-stated lemmas about empty raw maps (#10966)
This PR fixes some mis-stated lemmas which should have been about the
`.Raw` variants of maps.
2025-10-26 07:51:39 +00:00
Leonardo de Moura
97d63db52c fix: mbtc for nonlinear terms in grind cutsat (#10965)
This PR ensures that model-based theory combination in `grind cutsat`
considers nonlinear terms. Nonlinear multiplications such as `x * y` are
treated as uninterpreted symbols in `cutsat`.

Closes #10885
2025-10-26 04:35:34 +00:00
Leonardo de Moura
f8b0beeba9 fix: propagator for a^(n+m) in grind (#10964)
This PR adds a propagator for `a^(n+m)` and removes its normalizer. This
change was motivated by issue #10661

Closes #10661
2025-10-26 03:52:28 +00:00
Leonardo de Moura
93c5bd0fdd chore: use realizeGlobalConstNoOverloadWithInfo (#10963)
closes #10427
closes #10426
2025-10-26 02:45:46 +00:00
Leonardo de Moura
feb864712f fix: spurious warning message in grind (#10962)
This PR fixes a spurious warning message in `grind`.

Closes #10670
2025-10-26 02:40:12 +00:00
Leonardo de Moura
2f3211028b feat: support for Rat scientific literals (#10961)
This PR adds support for scientific literals for `Rat` in `grind`.
`grind` does not yet add support for this kind of literal in arbitrary
fields.

closes #10489
2025-10-26 02:05:26 +00:00
Leonardo de Moura
cdaa827b2a fix: grind linarith counterexample (#10960)
This PR fixes a bug in the `grind linarith` model/counterexample
construction.

Closes #10500
2025-10-26 00:27:47 +00:00
Kim Morrison
a9d6bc60d0 chore: update stage0 2025-10-26 10:29:47 +11:00
Kim Morrison
9166c71e08 feat: don't count symbols in instances and proofs 2025-10-26 10:29:47 +11:00
Kim Morrison
43b2d41e81 chore: add test file 2025-10-26 10:29:47 +11:00
Kim Morrison
e8620255a0 feat: symbol frequency environment extension 2025-10-26 10:29:47 +11:00
Leonardo de Moura
48f0eb206c test: rationals in grind linarith (#10958) 2025-10-25 21:48:43 +00:00
Leonardo de Moura
962e7d5a30 test: for #10317 (#10957)
This PR adds tests for issue that has been fixed by previous commits.

closes #10317
2025-10-25 21:42:56 +00:00
Leonardo de Moura
aa59c01742 fix: equality propagation in grind order (#10956)
This PR fixes a bug in the equality propagation procedure in
`grind.order`. Specifically, it affects the procedure that asserts
equalities in the `grind` core state that are implied by (ring)
inequalities in the `grind.order` module.

closes #10622
2025-10-25 20:12:04 +00:00
Leonardo de Moura
cd60d9c14a fix: grind order regression (#10955)
This PR fixes a regression in the `grind order` module introduced by

Closes #10953
2025-10-25 16:12:28 +00:00
Eric Wieser
b3ef7c9f25 chore: add an assertion about mkValueTypeClosure (#10954)
This is a guard against #10705; if a kernel error is raised when the
return value of this function is eventually checked, it is often
silenced downstream, making it hard to spot the failure.
If we panic here via `assert!`, then the diagnostic cannot be missed.
2025-10-25 12:59:17 +00:00
Lean stage0 autoupdater
be2c2bcf9b chore: update stage0 2025-10-25 11:32:01 +00:00
Leonardo de Moura
d5ca0c7032 fix: bug in cutsat model construction (#10951)
This PR fixes a bug in the `cutsat` incremental model construction. The
model was not being reset when new (unsatisfied) equalities were
asserted.
2025-10-25 04:16:32 +00:00
Leonardo de Moura
3c2ab0fefa feat: model-based theory combination tactic and action (#10950)
This PR adds the `mbtc` tactic to the `grind` interactive mode. It
implements model-based theory combination. It also ensures `finish?` is
capable of generating it.
2025-10-25 03:35:19 +00:00
Leonardo de Moura
1643fd7532 fix: finish? checks whether solver propagation steps are needed (#10949)
This PR ensures that solver propagation steps are necessary in the
generated tactic script to close the goal.

It produces more compact proof scripts, but this is not just an
optimization, if we include an unnecessary step, we may fail to replay
the generated script when `cases` steps are pruned using
non-chronological backtracking (NCB). For example, when executing
`finish?`, we may have performed a `cases #<anchor>` step that enabled
`ring` to propagate a new fact. If this fact is not used in the final
proof, and the corresponding `cases #<anchor>` step is pruned by NCB,
the `ring` step will fail during replay.
2025-10-25 02:27:44 +00:00
Leonardo de Moura
53442d48f5 feat: finish? produces partial tactic scripts with sorry (#10948)
This PR ensures that `finish?` produces partial tactic scripts
containing `sorry`s.
We may add an option to disable this feature in the future.
It is enabled by default because it provides a useful way to debug
`grind` failures.
2025-10-24 23:47:30 +00:00
Joachim Breitner
96bace56fa fix: run enableRealizationsForConst on sizeOf decls (#10944)
This PR runs enableRealizationsForConst on sizeOf declarations. Fixes
#10573.
2025-10-24 16:15:38 +00:00
Sebastian Ullrich
b0127e01e3 chore: final module system fixes and refinements for initial Mathlib porting (#10869) 2025-10-24 15:53:49 +00:00
Joachim Breitner
e71d0abc7d test: test case for #10775 (#10943) 2025-10-24 14:54:36 +00:00
Joachim Breitner
a6d50a61b3 fix: Meta.Closure: topologically sort abstracted vars (#10926)
This PR topologically sorts abstracted vars in
`Meta.Closure.mkValueTypeClosure` if MVars are being abstracted.
Fixes #10705

---------

Co-authored-by: Eric Wieser <efw@google.com>
2025-10-24 12:07:16 +00:00
Sebastian Ullrich
dec007693a chore: fix C++ warning (#10922) 2025-10-24 11:09:08 +00:00
Henrik Böving
1145498521 fix: regression from ST redefinition (#10940)
This PR fixes a regression introduced by the `ST` redefinition by making
the definition of `ST` as
reducible as previously. The key issue here is that in the previous
state it would reduce to a
function at which point the monad lifting mechanisms don't kick in in
the same fashion anymore.
2025-10-24 08:50:56 +00:00
Leonardo de Moura
2f07b70870 fix: default parameter value in constructor footgun at cases tactic (#10939)
This PR fixes another instance of the “default parameter value in
constructor” footgun, which was affecting the `cases` tactic in the
`grind` interactive mode.
2025-10-24 00:56:15 +00:00
Leonardo de Moura
09b36c332a fix: missing processNewFacts at solver tactics (#10938)
This PR ensures solver `grind` tactics (e.g., `ac`, `ring`, `lia`, etc)
process pending facts after making progress.
2025-10-24 00:08:06 +00:00
Leonardo de Moura
955fff52c5 fix: missing reset ematch.num at cases (#10937)
This PR fixes a missing counter reset at the `cases` tactic in `grind`
interactive mode.
2025-10-23 23:58:36 +00:00
Leonardo de Moura
6d665f3e91 fix: bugs at grind => finish? (#10936)
This PR fixes issues in `grind => finish?` that were preventing
generated `grind` tactic scripts from being successfully replayed.
2025-10-23 22:35:20 +00:00
Joachim Breitner
74fd46894f fix: deprecation warning location with field notation (#10826)
This PR fixes the location of the “deprecated constant” and similar
error messages on field notation (`e.f`, `(e).f`, `e |>. f`). Fixes
#10821.
2025-10-23 20:55:25 +00:00
Joachim Breitner
ffaadcc990 doc: warning for wf_preprocess (#10897)
This PR adds a warning to `wf_preproces` that these lemmas can be used
to introduce hidden partiality.

---------

Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
2025-10-23 20:54:40 +00:00
Joachim Breitner
54175f3b99 fix: decreasing_by: remove mdata (#10931)
This PR strips the `Expr.mdata` that `WF.Fix` uses to associate goal
with recursive calls from the goal presented to the tactics.
Fixes #10895.
2025-10-23 20:54:32 +00:00
1360 changed files with 3133 additions and 3142 deletions

View File

@@ -200,8 +200,8 @@ jobs:
"test": true,
// NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
"test-speedcenter": large && level >= 2,
// made explicit until it can be assumed to have propagated to PRs
"CMAKE_OPTIONS": "-DUSE_LAKE=ON",
// We are not warning-free yet on all platforms, start here
"CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
},
{
"name": "Linux Reldebug",

View File

@@ -131,10 +131,11 @@ structure State where
`transDeps[i]` is the (non-reflexive) transitive closure of `mods[i].imports`. More specifically,
* `j ∈ transDeps[i].pub` if `i -(public import)->+ j`
* `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
* `j ∈ transDeps[i].priv` if `i -(import all)->+ -(public import ...)-> _ -(public import)->* j`
* `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import ...)->* j`
* `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import ...)->* j`
* `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ -(public meta import ...)-> _ -(public (meta)? import ...)->* j`
* `j ∈ transDeps[i].priv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].pub/priv`
* `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import)->* j`
* `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import)->* j`
* `j ∈ transDeps[i].metaPriv` if `i -(import ...)-> i'` and `j ∈ transDeps[i'].metaPub`
* `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].metaPub/metaPriv`
-/
transDeps : Array Needs := #[]
/--
@@ -162,10 +163,10 @@ def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps
-- `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
transImps := transImps.union .priv {j} |>.union .priv (impTransImps.get .pub)
if imp.importAll then
-- `j ∈ transDeps[i].priv` if `i -(import all)->+ -(public import ...)-> _ -(public import)->* j`
transImps := transImps.union .priv (impTransImps.get .pub)
-- `j ∈ transDeps[i].priv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].pub/priv`
transImps := transImps.union .priv (impTransImps.get .pub impTransImps.get .priv)
-- `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import ...)->* j`
-- `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import)->* j`
if imp.isExported then
transImps := transImps.union .metaPub (impTransImps.get .metaPub)
if imp.isMeta then
@@ -173,10 +174,13 @@ def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps
if !imp.isExported then
if imp.isMeta then
-- `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import ...)->* j`
-- `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import)->* j`
transImps := transImps.union .metaPriv {j} |>.union .metaPriv (impTransImps.get .pub impTransImps.get .metaPub)
if imp.importAll then
-- `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ -(public meta import ...)-> _ -(public (meta)? import ...)->* j`
-- `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].metaPub/metaPriv`
transImps := transImps.union .metaPriv (impTransImps.get .metaPub impTransImps.get .metaPriv)
else
-- `j ∈ transDeps[i].metaPriv` if `i -(import ...)-> i'` and `j ∈ transDeps[i'].metaPub`
transImps := transImps.union .metaPriv (impTransImps.get .metaPub)
transImps
@@ -185,7 +189,8 @@ def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps
def calcNeeds (env : Environment) (i : ModuleIdx) : Needs := Id.run do
let mut needs := default
for ci in env.header.moduleData[i]!.constants do
let pubCI? := env.setExporting true |>.find? ci.name
-- Added guard for cases like `structure` that are still exported even if private
let pubCI? := guard (!isPrivateName ci.name) *> (env.setExporting true).find? ci.name
let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
needs := visitExpr k ci.type needs
if let some e := ci.value? (allowOpaque := true) then
@@ -216,7 +221,8 @@ def getExplanations (env : Environment) (i : ModuleIdx) :
Std.HashMap (ModuleIdx × NeedsKind) (Option (Name × Name)) := Id.run do
let mut deps := default
for ci in env.header.moduleData[i]!.constants do
let pubCI? := env.setExporting true |>.find? ci.name
-- Added guard for cases like `structure` that are still exported even if private
let pubCI? := guard (!isPrivateName ci.name) *> (env.setExporting true).find? ci.name
let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
deps := visitExpr k ci.name ci.type deps
if let some e := ci.value? (allowOpaque := true) then
@@ -286,7 +292,7 @@ and `endPos` is the position of the end of the header.
-/
def parseHeaderFromString (text path : String) :
IO (System.FilePath × Parser.InputContext ×
TSyntaxArray ``Parser.Module.import × String.Pos) := do
TSyntax ``Parser.Module.header × String.Pos.Raw) := do
let inputCtx := Parser.mkInputContext text path
let (header, parserState, msgs) Parser.parseHeader inputCtx
if !msgs.toList.isEmpty then -- skip this file if there are parse errors
@@ -294,8 +300,8 @@ def parseHeaderFromString (text path : String) :
throw <| .userError "parse errors in file"
-- the insertion point for `add` is the first newline after the imports
let insertion := header.raw.getTailPos?.getD parserState.pos
let insertion := text.findAux (· == '\n') text.endPos insertion + 1
pure (path, inputCtx, .mk header.raw[2].getArgs, insertion)
let insertion := text.findAux (· == '\n') text.endPos insertion + '\n'
pure (path, inputCtx, header, insertion)
/-- Parse a source file to extract the location of the import lines, for edits and error messages.
@@ -304,13 +310,18 @@ and `endPos` is the position of the end of the header.
-/
def parseHeader (srcSearchPath : SearchPath) (mod : Name) :
IO (System.FilePath × Parser.InputContext ×
TSyntaxArray ``Parser.Module.import × String.Pos) := do
TSyntax ``Parser.Module.header × String.Pos.Raw) := do
-- Parse the input file
let some path srcSearchPath.findModuleWithExt "lean" mod
| throw <| .userError s!"error: failed to find source file for {mod}"
let text IO.FS.readFile path
parseHeaderFromString text path.toString
def decodeHeader : TSyntax ``Parser.Module.header Option (TSyntax `module) × Option (TSyntax `prelude) × TSyntaxArray ``Parser.Module.import
| `(Parser.Module.header| $[module%$moduleTk?]? $[prelude%$preludeTk?]? $imports*) =>
(moduleTk?.map .mk, preludeTk?.map .mk, imports)
| _ => unreachable!
def decodeImport : TSyntax ``Parser.Module.import Import
| `(Parser.Module.import| $[public%$pubTk?]? $[meta%$metaTk?]? import $[all%$allTk?]? $id) =>
{ module := id.getId, isExported := pubTk?.isSome, isMeta := metaTk?.isSome, importAll := allTk?.isSome }
@@ -326,11 +337,20 @@ def decodeImport : TSyntax ``Parser.Module.import → Import
* `addOnly`: if true, only add missing imports, do not remove unused ones
-/
def visitModule (srcSearchPath : SearchPath)
(i : Nat) (needs : Needs) (preserve : Needs) (edits : Edits)
(i : Nat) (needs : Needs) (preserve : Needs) (edits : Edits) (headerStx : TSyntax ``Parser.Module.header)
(addOnly := false) (githubStyle := false) (explain := false) : StateT State IO Edits := do
let s get
-- Do transitive reduction of `needs` in `deps`.
let mut deps := needs
let (_, prelude?, imports) := decodeHeader headerStx
if prelude?.isNone then
deps := deps.union .pub {s.env.getModuleIdx? `Init |>.get!}
for imp in imports do
if addOnly || imp.raw.getTrailing?.any (·.toString.toSlice.contains "shake: keep") then
let imp := decodeImport imp
let j := s.env.getModuleIdx? imp.module |>.get!
let k := NeedsKind.ofImport imp
deps := deps.union k {j}
for j in [0:s.mods.size] do
let transDeps := s.transDeps[j]!
for k in NeedsKind.all do
@@ -354,7 +374,8 @@ def visitModule (srcSearchPath : SearchPath)
newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
else
let k := NeedsKind.ofImport imp
if !addOnly && !deps.has k j && !deps.has { k with isExported := false } j then
-- A private import should also be removed if the public version is needed
if !deps.has k j || !k.isExported && deps.has { k with isExported := true } j then
toRemove := toRemove.push imp
else
newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
@@ -385,7 +406,8 @@ def visitModule (srcSearchPath : SearchPath)
if githubStyle then
try
let (path, inputCtx, imports, endHeader) parseHeader srcSearchPath s.modNames[i]!
let (path, inputCtx, stx, endHeader) parseHeader srcSearchPath s.modNames[i]!
let (_, _, imports) := decodeHeader stx
for stx in imports do
if toRemove.any fun imp => imp == decodeImport stx then
let pos := inputCtx.fileMap.toPosition stx.raw.getPos?.get!
@@ -529,33 +551,43 @@ def main (args : List String) : IO UInt32 := do
let needs := s.mods.mapIdx fun i _ =>
Task.spawn fun _ => calcNeeds s.env i
-- Parse headers in parallel
let headers s.mods.mapIdxM fun i _ =>
BaseIO.asTask (parseHeader srcSearchPath s.modNames[i]! |>.toBaseIO)
if args.fix then
println! "The following changes will be made automatically:"
-- Check all selected modules
let mut edits : Edits :=
let mut revNeeds : Needs := default
for i in [0:s.mods.size], t in needs do
edits visitModule (addOnly := !pkg.isPrefixOf s.modNames[i]!) srcSearchPath i t.get revNeeds edits args.githubStyle args.explain
if isExtraRevModUse s.env i then
revNeeds := revNeeds.union .priv {i}
for i in [0:s.mods.size], t in needs, header in headers do
match header.get with
| .ok (_, _, stx, _) =>
edits visitModule (addOnly := !pkg.isPrefixOf s.modNames[i]!)
srcSearchPath i t.get revNeeds edits stx args.githubStyle args.explain
if isExtraRevModUse s.env i then
revNeeds := revNeeds.union .priv {i}
| .error e =>
println! e.toString
if !args.fix then
-- return error if any issues were found
return if edits.isEmpty then 0 else 1
-- Apply the edits to existing files
let count edits.foldM (init := 0) fun count mod (remove, add) => do
let mut count := 0
for mod in s.modNames, header? in headers do
let some (remove, add) := edits[mod]? | continue
let add : Array Import := add.qsortOrd
-- Parse the input file
let (path, inputCtx, imports, insertion)
try parseHeader srcSearchPath mod
catch e => println! e.toString; return count
let .ok (path, inputCtx, stx, insertion) := header?.get | continue
let (_, _, imports) := decodeHeader stx
let text := inputCtx.fileMap.source
-- Calculate the edit result
let mut pos : String.Pos := 0
let mut pos : String.Pos.Raw := 0
let mut out : String := ""
let mut seen : Std.HashSet Import := {}
for stx in imports do
@@ -563,7 +595,7 @@ def main (args : List String) : IO UInt32 := do
if remove.contains mod || seen.contains mod then
out := out ++ text.extract pos stx.raw.getPos?.get!
-- We use the end position of the syntax, but include whitespace up to the first newline
pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + 1
pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + '\n'
seen := seen.insert mod
out := out ++ text.extract pos insertion
for mod in add do
@@ -573,7 +605,7 @@ def main (args : List String) : IO UInt32 := do
out := out ++ text.extract insertion text.rawEndPos
IO.FS.writeFile path out
return count + 1
count := count + 1
-- Since we throw an error upon encountering issues, we can be sure that everything worked
-- if we reach this point of the script.

View File

@@ -181,9 +181,6 @@ theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff
theorem not_and_iff_not_or_not : ¬(a b) ¬a ¬b := Decidable.not_and_iff_not_or_not
@[deprecated not_and_iff_not_or_not (since := "2025-03-18")]
abbrev not_and_iff_or_not_not := @not_and_iff_not_or_not
theorem not_iff : ¬(a b) (¬a b) := Decidable.not_iff
@[simp] theorem imp_iff_left_iff : (b a b) a b := Decidable.imp_iff_left_iff

View File

@@ -45,9 +45,6 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
rfl
@[deprecated forIn_eq_forIn' (since := "2025-04-04")]
abbrev forIn_eq_forin' := @forIn_eq_forIn'
/--
Extracts the value from a `ForInStep`, ignoring whether it is `ForInStep.done` or `ForInStep.yield`.
-/

View File

@@ -255,11 +255,6 @@ instance : LawfulMonad Id := by
@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
@[simp] theorem run_seq (f : Id (α β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
-- These lemmas are bad as they abuse the defeq of `Id α` and `α`
@[deprecated run_map (since := "2025-03-05")] theorem map_eq (x : Id α) (f : α β) : f <$> x = f x := rfl
@[deprecated run_bind (since := "2025-03-05")] theorem bind_eq (x : Id α) (f : α id β) : x >>= f = f x := rfl
@[deprecated run_pure (since := "2025-03-05")] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
end Id
/-! # Option -/

View File

@@ -600,17 +600,6 @@ export LawfulSingleton (insert_empty_eq)
attribute [simp] insert_empty_eq
@[deprecated insert_empty_eq (since := "2025-03-12")]
theorem insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
[LawfulSingleton α β] (x : α) : (insert x : β) = singleton x :=
insert_empty_eq _
@[deprecated insert_empty_eq (since := "2025-03-12")]
theorem LawfulSingleton.insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
[LawfulSingleton α β] (x : α) : (insert x : β) = singleton x :=
insert_empty_eq _
/-- Type class used to implement the notation `{ a ∈ c | p a }` -/
class Sep (α : outParam <| Type u) (γ : Type v) where
/-- Computes `{ a ∈ c | p a }`. -/
@@ -1095,14 +1084,6 @@ theorem of_toBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d =
theorem of_toBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p :=
of_decide_eq_false h
set_option linter.missingDocs false in
@[deprecated of_toBoolUsing_eq_true (since := "2025-04-04")]
abbrev ofBoolUsing_eq_true := @of_toBoolUsing_eq_true
set_option linter.missingDocs false in
@[deprecated of_toBoolUsing_eq_false (since := "2025-04-04")]
abbrev ofBoolUsing_eq_false := @of_toBoolUsing_eq_false
instance : Decidable True :=
isTrue trivial
@@ -1159,12 +1140,21 @@ variable {p q : Prop}
decidable_of_decidable_of_iff (p := p) (h Iff.rfl)
end
@[macro_inline] instance {p q} [Decidable p] [Decidable q] : Decidable (p q) :=
if hp : p then
if hq : q then isTrue (fun _ => hq)
else isFalse (fun h => absurd (h hp) hq)
else isTrue (fun h => absurd h hp)
@[inline]
instance exists_prop_decidable {p} (P : p Prop)
[Decidable p] [ h, Decidable (P h)] : Decidable (Exists P) :=
if h : p then
decidable_of_decidable_of_iff fun h2 => h, h2, fun _, h2 => h2
else isFalse fun h', _ => h h'
@[inline]
instance forall_prop_decidable {p} (P : p Prop)
[Decidable p] [ h, Decidable (P h)] : Decidable ( h, P h) :=
if h : p then
decidable_of_decidable_of_iff fun h2 _ => h2, fun al => al h
else isTrue fun h2 => absurd h2 h
@[inline]
instance {p q} [Decidable p] [Decidable q] : Decidable (p q) :=
if hp : p then
if hq : q then
@@ -1212,11 +1202,13 @@ theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) :
| isTrue _ => rfl
| isFalse _ => rfl
@[macro_inline]
instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
match dC with
| isTrue _ => dT
| isFalse _ => dE
@[inline]
instance {c : Prop} {t : c Prop} {e : ¬c Prop} [dC : Decidable c] [dT : h, Decidable (t h)] [dE : h, Decidable (e h)] : Decidable (if h : c then t h else e h) :=
match dC with
| isTrue hc => dT hc
@@ -1367,10 +1359,6 @@ namespace Subtype
theorem exists_of_subtype {α : Type u} {p : α Prop} : { x // p x } Exists (fun x => p x)
| a, h => a, h
set_option linter.missingDocs false in
@[deprecated exists_of_subtype (since := "2025-04-04")]
abbrev existsOfSubtype := @exists_of_subtype
variable {α : Type u} {p : α Prop}
protected theorem eq : {a1 a2 : {x // p x}}, val a1 = val a2 a1 = a2

View File

@@ -749,9 +749,6 @@ and simplifies these to the function directly taking the value.
(Array.replicate n x).unattach = Array.replicate n x.1 := by
simp [unattach]
@[deprecated unattach_replicate (since := "2025-03-18")]
abbrev unattach_mkArray := @unattach_replicate
/-! ### Well-founded recursion preprocessing setup -/
@[wf_preprocess] theorem map_wfParam {xs : Array α} {f : α β} :

View File

@@ -209,20 +209,6 @@ Examples:
def replicate {α : Type u} (n : Nat) (v : α) : Array α where
toList := List.replicate n v
/--
Creates an array that contains `n` repetitions of `v`.
The corresponding `List` function is `List.replicate`.
Examples:
* `Array.mkArray 2 true = #[true, true]`
* `Array.mkArray 3 () = #[(), (), ()]`
* `Array.mkArray 0 "anything" = #[]`
-/
@[extern "lean_mk_array", deprecated replicate (since := "2025-03-18")]
def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
toList := List.replicate n v
/--
Swaps two elements of an array. The modification is performed in-place when the reference to the
array is unique.
@@ -2147,5 +2133,3 @@ instance [ToString α] : ToString (Array α) where
toString xs := String.Internal.append "#" (toString xs.toList)
end Array
export Array (mkArray)

View File

@@ -99,9 +99,6 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a then n else 0 := by
simp [ List.toArray_replicate, List.countP_replicate]
@[deprecated countP_replicate (since := "2025-03-18")]
abbrev countP_mkArray := @countP_replicate
theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
(if p xs[i] then 1 else 0) xs.countP p := by
rcases xs with xs
@@ -262,15 +259,9 @@ theorem count_eq_size {xs : Array α} : count a xs = xs.size ↔ ∀ b ∈ xs, a
@[simp] theorem count_replicate_self {a : α} {n : Nat} : count a (replicate n a) = n := by
simp [ List.toArray_replicate]
@[deprecated count_replicate_self (since := "2025-03-18")]
abbrev count_mkArray_self := @count_replicate_self
theorem count_replicate {a b : α} {n : Nat} : count a (replicate n b) = if b == a then n else 0 := by
simp [ List.toArray_replicate, List.count_replicate]
@[deprecated count_replicate (since := "2025-03-18")]
abbrev count_mkArray := @count_replicate
theorem filter_beq {xs : Array α} (a : α) : xs.filter (· == a) = replicate (count a xs) a := by
rcases xs with xs
simp [List.filter_beq]
@@ -284,9 +275,6 @@ theorem replicate_count_eq_of_count_eq_size {xs : Array α} (h : count a xs = xs
rw [ toList_inj]
simp [List.replicate_count_eq_of_count_eq_length (by simpa using h)]
@[deprecated replicate_count_eq_of_count_eq_size (since := "2025-03-18")]
abbrev mkArray_count_eq_of_count_eq_size := @replicate_count_eq_of_count_eq_size
@[simp] theorem count_filter {xs : Array α} (h : p a) : count a (filter p xs) = count a xs := by
rcases xs with xs
simp [List.count_filter, h]

View File

@@ -139,25 +139,16 @@ theorem eraseP_replicate {n : Nat} {a : α} {p : α → Bool} :
simp only [ List.toArray_replicate, List.eraseP_toArray, List.eraseP_replicate]
split <;> simp
@[deprecated eraseP_replicate (since := "2025-03-18")]
abbrev eraseP_mkArray := @eraseP_replicate
@[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) :
(replicate n a).eraseP p = replicate (n - 1) a := by
simp only [ List.toArray_replicate, List.eraseP_toArray]
simp [h]
@[deprecated eraseP_replicate_of_pos (since := "2025-03-18")]
abbrev eraseP_mkArray_of_pos := @eraseP_replicate_of_pos
@[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) :
(replicate n a).eraseP p = replicate n a := by
simp only [ List.toArray_replicate, List.eraseP_toArray]
simp [h]
@[deprecated eraseP_replicate_of_neg (since := "2025-03-18")]
abbrev eraseP_mkArray_of_neg := @eraseP_replicate_of_neg
theorem eraseP_eq_iff {p} {xs : Array α} :
xs.eraseP p = ys
(( a xs, ¬ p a) xs = ys)
@@ -278,9 +269,6 @@ theorem erase_replicate [LawfulBEq α] {n : Nat} {a b : α} :
simp only [List.erase_replicate, beq_iff_eq, List.toArray_replicate]
split <;> simp
@[deprecated erase_replicate (since := "2025-03-18")]
abbrev erase_mkArray := @erase_replicate
-- The arguments `a b` are explicit,
-- so they can be specified to prevent `simp` repeatedly applying the lemma.
@[grind =]
@@ -308,17 +296,11 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {xs : Array α} :
simp only [ List.toArray_replicate, List.erase_toArray]
simp
@[deprecated erase_replicate_self (since := "2025-03-18")]
abbrev erase_mkArray_self := @erase_replicate_self
@[simp] theorem erase_replicate_ne [LawfulBEq α] {a b : α} (h : !b == a) :
(replicate n a).erase b = replicate n a := by
rw [erase_of_not_mem]
simp_all
@[deprecated erase_replicate_ne (since := "2025-03-18")]
abbrev erase_mkArray_ne := @erase_replicate_ne
end erase
/-! ### eraseIdxIfInBounds -/
@@ -429,9 +411,6 @@ theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
simp only [ List.toArray_replicate, List.eraseIdx_toArray]
simp [List.eraseIdx_replicate, h]
@[deprecated eraseIdx_replicate (since := "2025-03-18")]
abbrev eraseIdx_mkArray := @eraseIdx_replicate
theorem mem_eraseIdx_iff_getElem {x : α} {xs : Array α} {k} {h} : x xs.eraseIdx k h i w, i k xs[i]'w = x := by
rcases xs with xs
simp [List.mem_eraseIdx_iff_getElem, *]

View File

@@ -289,9 +289,6 @@ theorem extract_append_right {as bs : Array α} :
· simp only [size_extract, size_replicate] at h₁ h₂
simp only [getElem_extract, getElem_replicate]
@[deprecated extract_replicate (since := "2025-03-18")]
abbrev extract_mkArray := @extract_replicate
theorem extract_eq_extract_right {as : Array α} {i j j' : Nat} :
as.extract i j = as.extract i j' min (j - i) (as.size - i) = min (j' - i) (as.size - i) := by
rcases as with as
@@ -429,32 +426,20 @@ theorem popWhile_append {xs ys : Array α} :
(replicate n a).takeWhile p = (replicate n a).filter p := by
simp [ List.toArray_replicate]
@[deprecated takeWhile_replicate_eq_filter (since := "2025-03-18")]
abbrev takeWhile_mkArray_eq_filter := @takeWhile_replicate_eq_filter
theorem takeWhile_replicate {p : α Bool} :
(replicate n a).takeWhile p = if p a then replicate n a else #[] := by
simp [takeWhile_replicate_eq_filter, filter_replicate]
@[deprecated takeWhile_replicate (since := "2025-03-18")]
abbrev takeWhile_mkArray := @takeWhile_replicate
@[simp] theorem popWhile_replicate_eq_filter_not {p : α Bool} :
(replicate n a).popWhile p = (replicate n a).filter (fun a => !p a) := by
simp [ List.toArray_replicate, List.filter_reverse]
@[deprecated popWhile_replicate_eq_filter_not (since := "2025-03-18")]
abbrev popWhile_mkArray_eq_filter_not := @popWhile_replicate_eq_filter_not
theorem popWhile_replicate {p : α Bool} :
(replicate n a).popWhile p = if p a then #[] else replicate n a := by
simp only [popWhile_replicate_eq_filter_not, size_replicate, filter_replicate, Bool.not_eq_eq_eq_not,
Bool.not_true]
split <;> simp_all
@[deprecated popWhile_replicate (since := "2025-03-18")]
abbrev popWhile_mkArray := @popWhile_replicate
theorem extract_takeWhile {as : Array α} {i : Nat} :
(as.takeWhile p).extract 0 i = (as.extract 0 i).takeWhile p := by
rcases as with as

View File

@@ -129,31 +129,19 @@ theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
simp [ List.toArray_replicate, List.findSome?_replicate]
@[deprecated findSome?_replicate (since := "2025-03-18")]
abbrev findSome?_mkArray := @findSome?_replicate
@[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
simp [findSome?_replicate, Nat.ne_of_gt h]
@[deprecated findSome?_replicate_of_pos (since := "2025-03-18")]
abbrev findSome?_mkArray_of_pos := @findSome?_replicate_of_pos
-- Argument is unused, but used to decide whether `simp` should unfold.
@[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
findSome? f (replicate n a) = if n = 0 then none else f a := by
simp [findSome?_replicate]
@[deprecated findSome?_replicate_of_isSome (since := "2025-03-18")]
abbrev findSome?_mkArray_of_isSome := @findSome?_replicate_of_isSome
@[simp] theorem findSome?_replicate_of_isNone (h : (f a).isNone) :
findSome? f (replicate n a) = none := by
rw [Option.isNone_iff_eq_none] at h
simp [findSome?_replicate, h]
@[deprecated findSome?_replicate_of_isNone (since := "2025-03-18")]
abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
/-! ### find? -/
@[simp, grind =] theorem find?_empty : find? p #[] = none := rfl
@@ -318,16 +306,10 @@ theorem find?_replicate :
find? p (replicate n a) = if p a then some a else none := by
simp [find?_replicate, Nat.ne_of_gt h]
@[deprecated find?_replicate_of_size_pos (since := "2025-03-18")]
abbrev find?_mkArray_of_length_pos := @find?_replicate_of_size_pos
@[simp] theorem find?_replicate_of_pos (h : p a) :
find? p (replicate n a) = if n = 0 then none else some a := by
simp [find?_replicate, h]
@[deprecated find?_replicate_of_pos (since := "2025-03-18")]
abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
@[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
simp [find?_replicate, h]
@@ -583,9 +565,6 @@ theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
simp only [List.findIdx?_toArray]
simp
@[deprecated findIdx?_replicate (since := "2025-03-18")]
abbrev findIdx?_mkArray := @findIdx?_replicate
theorem findIdx?_eq_findSome?_zipIdx {xs : Array α} {p : α Bool} :
xs.findIdx? p = xs.zipIdx.findSome? fun a, i => if p a then some i else none := by
rcases xs with xs

View File

@@ -317,41 +317,23 @@ theorem singleton_inj : #[a] = #[b] ↔ a = b := by
@[simp, grind =] theorem size_replicate {n : Nat} {v : α} : (replicate n v).size = n :=
List.length_replicate ..
@[deprecated size_replicate (since := "2025-03-18")]
abbrev size_mkArray := @size_replicate
@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := by
simp only [replicate]
@[deprecated toList_replicate (since := "2025-03-18")]
abbrev toList_mkArray := @toList_replicate
@[simp, grind =] theorem replicate_zero : replicate 0 a = #[] := rfl
@[deprecated replicate_zero (since := "2025-03-18")]
abbrev mkArray_zero := @replicate_zero
@[grind =]
theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
apply toList_inj.1
simp [List.replicate_succ']
@[deprecated replicate_succ (since := "2025-03-18")]
abbrev mkArray_succ := @replicate_succ
@[simp, grind =] theorem getElem_replicate {n : Nat} {v : α} {i : Nat} (h : i < (replicate n v).size) :
(replicate n v)[i] = v := by simp [ getElem_toList]
@[deprecated getElem_replicate (since := "2025-03-18")]
abbrev getElem_mkArray := @getElem_replicate
@[grind =] theorem getElem?_replicate {n : Nat} {v : α} {i : Nat} :
(replicate n v)[i]? = if i < n then some v else none := by
simp [getElem?_def]
@[deprecated getElem?_replicate (since := "2025-03-18")]
abbrev getElem?_mkArray := @getElem?_replicate
/-! ### mem -/
@[grind ]
@@ -1074,12 +1056,6 @@ theorem mem_or_eq_of_mem_setIfInBounds
cases xs
simp
@[deprecated beq_empty_eq (since := "2025-04-04")]
abbrev beq_empty_iff := @beq_empty_eq
@[deprecated empty_beq_eq (since := "2025-04-04")]
abbrev empty_beq_iff := @empty_beq_eq
@[simp, grind =] theorem push_beq_push [BEq α] {a b : α} {xs ys : Array α} :
(xs.push a == ys.push b) = (xs == ys && a == b) := by
cases xs
@@ -1100,9 +1076,6 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
rw [Bool.eq_iff_iff]
simp +contextual
@[deprecated replicate_beq_replicate (since := "2025-03-18")]
abbrev mkArray_beq_mkArray := @replicate_beq_replicate
private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] a == b := by
intro h
have : isEqv #[a] #[b] BEq.beq = true := h
@@ -1718,9 +1691,6 @@ theorem forall_none_of_filterMap_eq_empty (h : filterMap f xs = #[]) : ∀ x ∈
cases xs
simp
@[deprecated filterMap_eq_empty_iff (since := "2025-04-04")]
abbrev filterMap_eq_nil_iff := @filterMap_eq_empty_iff
theorem filterMap_eq_push_iff {f : α Option β} {xs : Array α} {ys : Array β} {b : β} :
filterMap f xs = ys.push b as a bs,
xs = as.push a ++ bs filterMap f as = ys f a = some b ( x, x bs f x = none) := by
@@ -2390,77 +2360,44 @@ theorem flatMap_eq_foldl {f : α → Array β} {xs : Array α} :
@[simp] theorem replicate_one : replicate 1 a = #[a] := rfl
@[deprecated replicate_one (since := "2025-03-18")]
abbrev mkArray_one := @replicate_one
/-- Variant of `replicate_succ` that prepends `a` at the beginning of the array. -/
theorem replicate_succ' : replicate (n + 1) a = #[a] ++ replicate n a := by
apply Array.ext'
simp [List.replicate_succ]
@[deprecated replicate_succ' (since := "2025-03-18")]
abbrev mkArray_succ' := @replicate_succ'
@[simp, grind =] theorem mem_replicate {a b : α} {n} : b replicate n a n 0 b = a := by
unfold replicate
simp only [List.mem_toArray, List.mem_replicate]
@[deprecated mem_replicate (since := "2025-03-18")]
abbrev mem_mkArray := @mem_replicate
@[grind ] theorem eq_of_mem_replicate {a b : α} {n} (h : b replicate n a) : b = a := (mem_replicate.1 h).2
@[deprecated eq_of_mem_mkArray (since := "2025-03-18")]
abbrev eq_of_mem_mkArray := @eq_of_mem_replicate
theorem forall_mem_replicate {p : α Prop} {a : α} {n} :
( b, b replicate n a p b) n = 0 p a := by
cases n <;> simp [mem_replicate]
@[deprecated forall_mem_replicate (since := "2025-03-18")]
abbrev forall_mem_mkArray := @forall_mem_replicate
@[simp] theorem replicate_succ_ne_empty {n : Nat} {a : α} : replicate (n+1) a #[] := by
simp [replicate_succ]
@[deprecated replicate_succ_ne_empty (since := "2025-03-18")]
abbrev mkArray_succ_ne_empty := @replicate_succ_ne_empty
@[simp] theorem replicate_eq_empty_iff {n : Nat} {a : α} : replicate n a = #[] n = 0 := by
cases n <;> simp
@[deprecated replicate_eq_empty_iff (since := "2025-03-18")]
abbrev mkArray_eq_empty_iff := @replicate_eq_empty_iff
@[simp] theorem replicate_inj : replicate n a = replicate m b n = m (n = 0 a = b) := by
rw [ toList_inj]
simp
@[deprecated replicate_inj (since := "2025-03-18")]
abbrev mkArray_inj := @replicate_inj
theorem eq_replicate_of_mem {a : α} {xs : Array α} (h : (b) (_ : b xs), b = a) : xs = replicate xs.size a := by
rw [ toList_inj]
simpa using List.eq_replicate_of_mem (by simpa using h)
@[deprecated eq_replicate_of_mem (since := "2025-03-18")]
abbrev eq_mkArray_of_mem := @eq_replicate_of_mem
theorem eq_replicate_iff {a : α} {n} {xs : Array α} :
xs = replicate n a xs.size = n (b) (_ : b xs), b = a := by
rw [ toList_inj]
simpa using List.eq_replicate_iff (l := xs.toList)
@[deprecated eq_replicate_iff (since := "2025-03-18")]
abbrev eq_mkArray_iff := @eq_replicate_iff
theorem map_eq_replicate_iff {xs : Array α} {f : α β} {b : β} :
xs.map f = replicate xs.size b x xs, f x = b := by
simp [eq_replicate_iff]
@[deprecated map_eq_replicate_iff (since := "2025-03-18")]
abbrev map_eq_mkArray_iff := @map_eq_replicate_iff
@[simp] theorem map_const {xs : Array α} {b : β} : map (Function.const α b) xs = replicate xs.size b :=
map_eq_replicate_iff.mpr fun _ _ => rfl
@@ -2477,143 +2414,86 @@ theorem map_const' {xs : Array α} {b : β} : map (fun _ => b) xs = replicate xs
apply Array.ext'
simp
@[deprecated set_replicate_self (since := "2025-03-18")]
abbrev set_mkArray_self := @set_replicate_self
@[simp] theorem setIfInBounds_replicate_self : (replicate n a).setIfInBounds i a = replicate n a := by
apply Array.ext'
simp
@[deprecated setIfInBounds_replicate_self (since := "2025-03-18")]
abbrev setIfInBounds_mkArray_self := @setIfInBounds_replicate_self
@[simp] theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
apply Array.ext'
simp
@[deprecated replicate_append_replicate (since := "2025-03-18")]
abbrev mkArray_append_mkArray := @replicate_append_replicate
theorem append_eq_replicate_iff {xs ys : Array α} {a : α} :
xs ++ ys = replicate n a
xs.size + ys.size = n xs = replicate xs.size a ys = replicate ys.size a := by
simp [ toList_inj, List.append_eq_replicate_iff]
@[deprecated append_eq_replicate_iff (since := "2025-03-18")]
abbrev append_eq_mkArray_iff := @append_eq_replicate_iff
theorem replicate_eq_append_iff {xs ys : Array α} {a : α} :
replicate n a = xs ++ ys
xs.size + ys.size = n xs = replicate xs.size a ys = replicate ys.size a := by
rw [eq_comm, append_eq_replicate_iff]
@[deprecated replicate_eq_append_iff (since := "2025-03-18")]
abbrev replicate_eq_mkArray_iff := @replicate_eq_append_iff
@[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
apply Array.ext'
simp
@[deprecated map_replicate (since := "2025-03-18")]
abbrev map_mkArray := @map_replicate
@[grind =] theorem filter_replicate (w : stop = n) :
(replicate n a).filter p 0 stop = if p a then replicate n a else #[] := by
apply Array.ext'
simp only [w]
split <;> simp_all
@[deprecated filter_replicate (since := "2025-03-18")]
abbrev filter_mkArray := @filter_replicate
@[simp] theorem filter_replicate_of_pos (w : stop = n) (h : p a) :
(replicate n a).filter p 0 stop = replicate n a := by
simp [filter_replicate, h, w]
@[deprecated filter_replicate_of_pos (since := "2025-03-18")]
abbrev filter_mkArray_of_pos := @filter_replicate_of_pos
@[simp] theorem filter_replicate_of_neg (w : stop = n) (h : ¬ p a) :
(replicate n a).filter p 0 stop = #[] := by
simp [filter_replicate, h, w]
@[deprecated filter_replicate_of_neg (since := "2025-03-18")]
abbrev filter_mkArray_of_neg := @filter_replicate_of_neg
theorem filterMap_replicate {f : α Option β} (w : stop = n := by simp) :
(replicate n a).filterMap f 0 stop = match f a with | none => #[] | .some b => replicate n b := by
apply Array.ext'
simp only [w, size_replicate, toList_filterMap', toList_replicate, List.filterMap_replicate]
split <;> simp_all
@[deprecated filterMap_replicate (since := "2025-03-18")]
abbrev filterMap_mkArray := @filterMap_replicate
-- This is not a useful `simp` lemma because `b` is unknown.
theorem filterMap_replicate_of_some {f : α Option β} (h : f a = some b) :
(replicate n a).filterMap f = replicate n b := by
simp [filterMap_replicate, h]
@[deprecated filterMap_replicate_of_some (since := "2025-03-18")]
abbrev filterMap_mkArray_of_some := @filterMap_replicate_of_some
@[simp] theorem filterMap_replicate_of_isSome {f : α Option β} (h : (f a).isSome) :
(replicate n a).filterMap f = replicate n (Option.get _ h) := by
match w : f a, h with
| some b, _ => simp [filterMap_replicate, w]
@[deprecated filterMap_replicate_of_isSome (since := "2025-03-18")]
abbrev filterMap_mkArray_of_isSome := @filterMap_replicate_of_isSome
@[simp] theorem filterMap_replicate_of_none {f : α Option β} (h : f a = none) :
(replicate n a).filterMap f = #[] := by
simp [filterMap_replicate, h]
@[deprecated filterMap_replicate_of_none (since := "2025-03-18")]
abbrev filterMap_mkArray_of_none := @filterMap_replicate_of_none
@[simp] theorem flatten_replicate_empty : (replicate n (#[] : Array α)).flatten = #[] := by
rw [ toList_inj]
simp
@[deprecated flatten_replicate_empty (since := "2025-03-18")]
abbrev flatten_mkArray_empty := @flatten_replicate_empty
@[simp] theorem flatten_replicate_singleton : (replicate n #[a]).flatten = replicate n a := by
rw [ toList_inj]
simp
@[deprecated flatten_replicate_singleton (since := "2025-03-18")]
abbrev flatten_mkArray_singleton := @flatten_replicate_singleton
@[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a := by
rw [ toList_inj]
simp
@[deprecated flatten_replicate_replicate (since := "2025-03-18")]
abbrev flatten_mkArray_replicate := @flatten_replicate_replicate
theorem flatMap_replicate {f : α Array β} : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
rw [ toList_inj]
simp [List.flatMap_replicate]
@[deprecated flatMap_replicate (since := "2025-03-18")]
abbrev flatMap_mkArray := @flatMap_replicate
@[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
rw [ List.toArray_replicate, List.isEmpty_toArray]
simp
@[deprecated isEmpty_replicate (since := "2025-03-18")]
abbrev isEmpty_mkArray := @isEmpty_replicate
@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
rw [ List.toArray_replicate, List.sum_toArray]
simp
@[deprecated sum_replicate_nat (since := "2025-03-18")]
abbrev sum_mkArray_nat := @sum_replicate_nat
/-! ### Preliminaries about `swap` needed for `reverse`. -/
@[grind =]
@@ -2800,9 +2680,6 @@ theorem flatten_reverse {xss : Array (Array α)} :
rw [ toList_inj]
simp
@[deprecated reverse_replicate (since := "2025-03-18")]
abbrev reverse_mkArray := @reverse_replicate
/-! ### extract -/
theorem extract_loop_zero {xs ys : Array α} {start : Nat} : extract.loop xs 0 start ys = ys := by
@@ -3712,15 +3589,9 @@ theorem back?_replicate {a : α} {n : Nat} :
rw [replicate_eq_toArray_replicate]
simp only [List.back?_toArray, List.getLast?_replicate]
@[deprecated back?_replicate (since := "2025-03-18")]
abbrev back?_mkArray := @back?_replicate
@[simp] theorem back_replicate {xs : Array α} (w : 0 < n) : (replicate n xs).back (by simpa using w) = xs := by
simp [back_eq_getElem]
@[deprecated back_replicate (since := "2025-03-18")]
abbrev back_mkArray := @back_replicate
/-! ## Additional operations -/
/-! ### leftpad -/
@@ -3738,9 +3609,6 @@ theorem size_rightpad {n : Nat} {a : α} {xs : Array α} :
theorem elem_push_self [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.push a).elem a = true := by simp
@[deprecated elem_push_self (since := "2025-04-04")]
abbrev elem_cons_self := @elem_push_self
theorem contains_eq_any_beq [BEq α] {xs : Array α} {a : α} : xs.contains a = xs.any (a == ·) := by
rcases xs with xs
simp [List.contains_eq_any_beq]
@@ -3818,9 +3686,6 @@ theorem pop_append {xs ys : Array α} :
@[simp, grind =] theorem pop_replicate {n : Nat} {a : α} : (replicate n a).pop = replicate (n - 1) a := by
ext <;> simp
@[deprecated pop_replicate (since := "2025-03-18")]
abbrev pop_mkArray := @pop_replicate
/-! ## Logic -/
/-! ### any / all -/
@@ -4050,16 +3915,10 @@ theorem all_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
(replicate n a).any f = if n = 0 then false else f a := by
induction n <;> simp_all [replicate_succ']
@[deprecated any_replicate (since := "2025-03-18")]
abbrev any_mkArray := @any_replicate
@[simp] theorem all_replicate {n : Nat} {a : α} :
(replicate n a).all f = if n = 0 then true else f a := by
induction n <;> simp_all +contextual [replicate_succ']
@[deprecated all_replicate (since := "2025-03-18")]
abbrev all_mkArray := @all_replicate
/-! ### modify -/
@[simp, grind =] theorem size_modify {xs : Array α} {i : Nat} {f : α α} : (xs.modify i f).size = xs.size := by
@@ -4234,17 +4093,11 @@ theorem replace_extract {xs : Array α} {i : Nat} :
(replicate n a).replace a b = #[b] ++ replicate (n - 1) a := by
cases n <;> simp_all [replicate_succ', replace_append]
@[deprecated replace_replicate_self (since := "2025-03-18")]
abbrev replace_mkArray_self := @replace_replicate_self
@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
(replicate n a).replace b c = replicate n a := by
rw [replace_of_not_mem]
simp_all
@[deprecated replace_replicate_ne (since := "2025-03-18")]
abbrev replace_mkArray_ne := @replace_replicate_ne
end replace
/-! ### toListRev -/
@@ -4412,9 +4265,6 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i
@[deprecated mem_toList_iff (since := "2025-05-26")]
theorem mem_toList {a : α} {xs : Array α} : a xs.toList a xs := mem_def.symm
@[deprecated not_mem_empty (since := "2025-03-25")]
theorem not_mem_nil (a : α) : ¬ a #[] := nofun
/-! # get lemmas -/
theorem lt_of_getElem {x : α} {xs : Array α} {i : Nat} {hidx : i < xs.size} (_ : xs[i] = x) :
@@ -4463,12 +4313,6 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
cases xs
simp
/-! ### contains -/
@[deprecated contains_iff (since := "2025-04-07")]
abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a a xs :=
contains_iff
/-! ### isPrefixOf -/
@[simp, grind =] theorem isPrefixOf_toList [BEq α] {xs ys : Array α} :

View File

@@ -296,9 +296,6 @@ theorem mapFinIdx_eq_replicate_iff {xs : Array α} {f : (i : Nat) → α → (h
rw [ toList_inj]
simp [List.mapFinIdx_eq_replicate_iff]
@[deprecated mapFinIdx_eq_replicate_iff (since := "2025-03-18")]
abbrev mapFinIdx_eq_mkArray_iff := @mapFinIdx_eq_replicate_iff
@[simp, grind =] theorem mapFinIdx_reverse {xs : Array α} {f : (i : Nat) α (h : i < xs.reverse.size) β} :
xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (xs.size - 1 - i) a (by simp; omega))).reverse := by
rcases xs with l
@@ -438,9 +435,6 @@ theorem mapIdx_eq_replicate_iff {xs : Array α} {f : Nat → α → β} {b : β}
rw [ toList_inj]
simp [List.mapIdx_eq_replicate_iff]
@[deprecated mapIdx_eq_replicate_iff (since := "2025-03-18")]
abbrev mapIdx_eq_mkArray_iff := @mapIdx_eq_replicate_iff
@[simp, grind =] theorem mapIdx_reverse {xs : Array α} {f : Nat α β} :
xs.reverse.mapIdx f = (mapIdx (fun i => f (xs.size - 1 - i)) xs).reverse := by
rcases xs with xs

View File

@@ -84,9 +84,6 @@ theorem Perm.size_eq {xs ys : Array α} (p : xs ~ ys) : xs.size = ys.size := by
simp only [perm_iff_toList_perm] at p
simpa using p.length_eq
@[deprecated Perm.size_eq (since := "2025-04-17")]
abbrev Perm.length_eq := @Perm.size_eq
theorem Perm.mem_iff {a : α} {xs ys : Array α} (p : xs ~ ys) : a xs a ys := by
rcases xs with xs
rcases ys with ys

View File

@@ -166,9 +166,6 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {as : Array α} {bs : Array
zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by
simp [ List.toArray_replicate]
@[deprecated zipWith_replicate (since := "2025-03-18")]
abbrev zipWith_mkArray := @zipWith_replicate
theorem map_uncurry_zip_eq_zipWith {f : α β γ} {as : Array α} {bs : Array β} :
map (Function.uncurry f) (as.zip bs) = zipWith f as bs := by
cases as
@@ -294,9 +291,6 @@ theorem zip_eq_append_iff {as : Array α} {bs : Array β} :
zip (replicate m a) (replicate n b) = replicate (min m n) (a, b) := by
simp [ List.toArray_replicate]
@[deprecated zip_replicate (since := "2025-03-18")]
abbrev zip_mkArray := @zip_replicate
theorem zip_eq_zip_take_min {as : Array α} {bs : Array β} :
zip as bs = zip (as.take (min as.size bs.size)) (bs.take (min as.size bs.size)) := by
cases as
@@ -348,9 +342,6 @@ theorem map_zipWithAll {δ : Type _} {f : α → β} {g : Option γ → Option
zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b)) := by
simp [ List.toArray_replicate]
@[deprecated zipWithAll_replicate (since := "2025-03-18")]
abbrev zipWithAll_mkArray := @zipWithAll_replicate
/-! ### zipWithM -/
@[simp, grind =]
@@ -408,7 +399,4 @@ theorem zip_of_prod {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl
unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
ext1 <;> simp
@[deprecated unzip_replicate (since := "2025-03-18")]
abbrev unzip_mkArray := @unzip_replicate
end Array

View File

@@ -34,14 +34,6 @@ namespace BitVec
simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
omega
set_option linter.missingDocs false in
@[deprecated getLsbD_of_ge (since := "2025-04-04")]
abbrev getLsbD_ge := @getLsbD_of_ge
set_option linter.missingDocs false in
@[deprecated getMsbD_of_ge (since := "2025-04-04")]
abbrev getMsbD_ge := @getMsbD_of_ge
theorem lt_of_getLsbD {x : BitVec w} {i : Nat} : getLsbD x i = true i < w := by
if h : i < w then
simp [h]
@@ -175,12 +167,6 @@ theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i <
@[simp] theorem getMsb?_of_ge (x : BitVec w) (i : Nat) (ge : w i) : getMsb? x i = none := by
simp [getMsb?_eq_getLsb?]; omega
set_option linter.missingDocs false in
@[deprecated getElem?_of_ge (since := "2025-04-04")] abbrev getLsb?_ge := @getElem?_of_ge
set_option linter.missingDocs false in
@[deprecated getMsb?_of_ge (since := "2025-04-04")] abbrev getMsb?_ge := @getMsb?_of_ge
theorem lt_of_getElem?_eq_some (x : BitVec w) (i : Nat) : x[i]? = some b i < w := by
cases h : x[i]? with
| none => simp
@@ -203,18 +189,6 @@ theorem lt_of_isSome_getMsb? (x : BitVec w) (i : Nat) : (getMsb? x i).isSome →
else
simp [Nat.ge_of_not_lt h]
set_option linter.missingDocs false in
@[deprecated lt_of_getElem?_eq_some (since := "2025-04-04")]
abbrev lt_of_getLsb?_eq_some := @lt_of_getElem?_eq_some
set_option linter.missingDocs false in
@[deprecated lt_of_isSome_getElem? (since := "2025-04-04")]
abbrev lt_of_getLsb?_isSome := @lt_of_isSome_getElem?
set_option linter.missingDocs false in
@[deprecated lt_of_isSome_getMsb? (since := "2025-04-04")]
abbrev lt_of_getMsb?_isSome := @lt_of_isSome_getMsb?
theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
x.getMsbD i = (x.getMsb? i).getD false := by
rw [getMsbD_eq_getLsbD]
@@ -1750,9 +1724,6 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
rw [h]
simp
set_option linter.missingDocs false in
@[deprecated getMsbD_not (since := "2025-04-04")] abbrev getMsb_not := @getMsbD_not
@[simp] theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by
simp [BitVec.msb]
@@ -2572,10 +2543,6 @@ theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) :
ext i h
simp [getElem_signExtend, show i < w by omega]
@[deprecated signExtend_eq_setWidth_of_le (since := "2025-03-07")]
theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v w) :
x.signExtend v = x.setWidth v := signExtend_eq_setWidth_of_le x hv
/-- Sign extending to the same bitwidth is a no op. -/
@[simp] theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
rw [signExtend_eq_setWidth_of_le _ (Nat.le_refl _), setWidth_eq]
@@ -3635,9 +3602,6 @@ theorem sub_eq_add_neg {n} (x y : BitVec n) : x - y = x + - y := by
simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod]
rw [Nat.add_comm]
set_option linter.missingDocs false in
@[deprecated sub_eq_add_neg (since := "2025-04-04")] abbrev sub_toAdd := @sub_eq_add_neg
theorem add_left_neg (x : BitVec w) : -x + x = 0#w := by
apply toInt_inj.mp
simp [toInt_neg, Int.add_left_neg]
@@ -3677,10 +3641,6 @@ theorem neg_one_eq_allOnes : -1#w = allOnes w := by
have r : (2^w - 1) < 2^w := by omega
simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
set_option linter.missingDocs false in
@[deprecated neg_one_eq_allOnes (since := "2025-04-04")]
abbrev negOne_eq_allOnes := @neg_one_eq_allOnes
theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1#w := by
apply eq_of_toNat_eq
simp only [toNat_neg, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]
@@ -4682,9 +4642,6 @@ theorem zero_smod {x : BitVec w} : (0#w).smod x = 0#w := by
@[simp, grind =] theorem getLsbD_ofBoolListLE : (ofBoolListLE bs).getLsbD i = bs.getD i false := by
induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
set_option linter.missingDocs false in
@[deprecated getLsbD_ofBoolListLE (since := "2025-04-04")] abbrev getLsb_ofBoolListLE := @getLsbD_ofBoolListLE
@[simp, grind =] theorem getMsbD_ofBoolListLE :
(ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
simp [getMsbD_eq_getLsbD]
@@ -4755,14 +4712,6 @@ theorem getLsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i
apply getLsbD_of_ge
omega
set_option linter.missingDocs false in
@[deprecated getLsbD_rotateLeftAux_of_lt (since := "2025-04-04")]
abbrev getLsbD_rotateLeftAux_of_le := @getLsbD_rotateLeftAux_of_lt
set_option linter.missingDocs false in
@[deprecated getLsbD_rotateLeftAux_of_ge (since := "2025-04-04")]
abbrev getLsbD_rotateLeftAux_of_geq := @getLsbD_rotateLeftAux_of_ge
/-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/
theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
(x.rotateLeft r).getLsbD i =
@@ -4919,14 +4868,6 @@ theorem getLsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i
apply getLsbD_of_ge
omega
set_option linter.missingDocs false in
@[deprecated getLsbD_rotateRightAux_of_lt (since := "2025-04-04")]
abbrev getLsbD_rotateRightAux_of_le := @getLsbD_rotateRightAux_of_lt
set_option linter.missingDocs false in
@[deprecated getLsbD_rotateRightAux_of_ge (since := "2025-04-04")]
abbrev getLsbD_rotateRightAux_of_geq := @getLsbD_rotateRightAux_of_ge
/-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is
smaller than the bitwidth. -/
theorem rotateRight_eq_rotateRightAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) :

View File

@@ -111,35 +111,11 @@ Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` v
@[simp] theorem eq_self_and : {a b : Bool}, (a = (a && b)) (a b) := by decide
@[simp] theorem eq_and_self : {a b : Bool}, (b = (a && b)) (b a) := by decide
@[deprecated and_eq_left_iff_imp (since := "2025-04-04")]
abbrev and_iff_left_iff_imp := @and_eq_left_iff_imp
@[deprecated and_eq_right_iff_imp (since := "2025-04-04")]
abbrev and_iff_right_iff_imp := @and_eq_right_iff_imp
@[deprecated eq_self_and (since := "2025-04-04")]
abbrev iff_self_and := @eq_self_and
@[deprecated eq_and_self (since := "2025-04-04")]
abbrev iff_and_self := @eq_and_self
@[simp] theorem not_and_eq_left_iff_and : {a b : Bool}, ((!a && b) = a) !a !b := by decide
@[simp] theorem and_not_eq_right_iff_and : {a b : Bool}, ((a && !b) = b) !a !b := by decide
@[simp] theorem eq_not_self_and : {a b : Bool}, (a = (!a && b)) !a !b := by decide
@[simp] theorem eq_and_not_self : {a b : Bool}, (b = (a && !b)) !a !b := by decide
@[deprecated not_and_eq_left_iff_and (since := "2025-04-04")]
abbrev not_and_iff_left_iff_imp := @not_and_eq_left_iff_and
@[deprecated and_not_eq_right_iff_and (since := "2025-04-04")]
abbrev and_not_iff_right_iff_imp := @and_not_eq_right_iff_and
@[deprecated eq_not_self_and (since := "2025-04-04")]
abbrev iff_not_self_and := @eq_not_self_and
@[deprecated eq_and_not_self (since := "2025-04-04")]
abbrev iff_and_not_self := @eq_and_not_self
/-! ### or -/
@[simp] theorem or_self_left : (a b : Bool), (a || (a || b)) = (a || b) := by decide
@@ -169,35 +145,11 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v
@[simp] theorem eq_self_or : {a b : Bool}, (a = (a || b)) (b a) := by decide
@[simp] theorem eq_or_self : {a b : Bool}, (b = (a || b)) (a b) := by decide
@[deprecated or_eq_left_iff_imp (since := "2025-04-04")]
abbrev or_iff_left_iff_imp := @or_eq_left_iff_imp
@[deprecated or_eq_right_iff_imp (since := "2025-04-04")]
abbrev or_iff_right_iff_imp := @or_eq_right_iff_imp
@[deprecated eq_self_or (since := "2025-04-04")]
abbrev iff_self_or := @eq_self_or
@[deprecated eq_or_self (since := "2025-04-04")]
abbrev iff_or_self := @eq_or_self
@[simp] theorem not_or_eq_left_iff_and : {a b : Bool}, ((!a || b) = a) a b := by decide
@[simp] theorem or_not_eq_right_iff_and : {a b : Bool}, ((a || !b) = b) a b := by decide
@[simp] theorem eq_not_self_or : {a b : Bool}, (a = (!a || b)) a b := by decide
@[simp] theorem eq_or_not_self : {a b : Bool}, (b = (a || !b)) a b := by decide
@[deprecated not_or_eq_left_iff_and (since := "2025-04-04")]
abbrev not_or_iff_left_iff_imp := @not_or_eq_left_iff_and
@[deprecated or_not_eq_right_iff_and (since := "2025-04-04")]
abbrev or_not_iff_right_iff_imp := @or_not_eq_right_iff_and
@[deprecated eq_not_self_or (since := "2025-04-04")]
abbrev iff_not_self_or := @eq_not_self_or
@[deprecated eq_or_not_self (since := "2025-04-04")]
abbrev iff_or_not_self := @eq_or_not_self
theorem or_comm : (x y : Bool), (x || y) = (y || x) := by decide
instance : Std.Commutative (· || ·) := or_comm
@@ -621,11 +573,6 @@ protected theorem cond_false {α : Sort u} {a b : α} : cond false a b = b := co
@[simp] theorem cond_then_self : (c b : Bool), cond c c b = (c || b) := by decide
@[simp] theorem cond_else_self : (c b : Bool), cond c b c = (c && b) := by decide
@[deprecated cond_then_not_self (since := "2025-04-04")] abbrev cond_true_not_same := @cond_then_not_self
@[deprecated cond_else_not_self (since := "2025-04-04")] abbrev cond_false_not_same := @cond_else_not_self
@[deprecated cond_then_self (since := "2025-04-04")] abbrev cond_true_same := @cond_then_self
@[deprecated cond_else_self (since := "2025-04-04")] abbrev cond_false_same := @cond_else_self
theorem cond_pos {b : Bool} {a a' : α} (h : b = true) : (bif b then a else a') = a := by
rw [h, cond_true]

View File

@@ -24,9 +24,6 @@ attribute [ext] ByteArray
instance : DecidableEq ByteArray :=
fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm
@[deprecated emptyWithCapacity (since := "2025-03-12")]
abbrev mkEmpty := emptyWithCapacity
instance : Inhabited ByteArray where
default := empty

View File

@@ -281,4 +281,9 @@ theorem append_toByteArray_singleton {as : ByteArray} {a : UInt8} :
ext1
simp
@[simp]
theorem extract_zero_max_size {a : ByteArray} {i : Nat} : a.extract 0 (max i a.size) = a := by
ext1
simp [Nat.le_max_right]
end ByteArray

View File

@@ -29,9 +29,6 @@ attribute [ext] FloatArray
def emptyWithCapacity (c : @& Nat) : FloatArray :=
{ data := #[] }
@[deprecated emptyWithCapacity (since := "2025-03-12")]
abbrev mkEmpty := emptyWithCapacity
def empty : FloatArray :=
emptyWithCapacity 0

View File

@@ -369,9 +369,6 @@ def toNat? : Int → Option Nat
| (n : Nat) => some n
| -[_+1] => none
@[deprecated toNat? (since := "2025-03-11"), inherit_doc toNat?]
abbrev toNat' := toNat?
/-! ## divisibility -/
/--

View File

@@ -118,9 +118,6 @@ instance : Mod Int where
@[simp, norm_cast] theorem natCast_ediv (m n : Nat) : ((m / n) : Int) = m / n := rfl
@[deprecated natCast_ediv (since := "2025-04-17")]
theorem ofNat_ediv (m n : Nat) : ((m / n) : Int) = m / n := natCast_ediv m n
theorem ofNat_ediv_ofNat {a b : Nat} : (a / b : Int) = (a / b : Nat) := rfl
@[norm_cast]
theorem negSucc_ediv_ofNat_succ {a b : Nat} : ((-[a+1]) / (b+1) : Int) = -[a / succ b +1] := rfl

View File

@@ -92,9 +92,6 @@ theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) z ↔ n z.natA
@[simp, norm_cast] theorem natCast_emod (m n : Nat) : ((m % n) : Int) = m % n := rfl
@[deprecated natCast_emod (since := "2025-04-17")]
theorem ofNat_emod (m n : Nat) : ((m % n) : Int) = m % n := natCast_emod m n
/-! ### mod definitions -/
theorem emod_add_mul_ediv : a b : Int, a % b + b * (a / b) = a
@@ -233,10 +230,6 @@ theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
@[simp] theorem mul_add_emod_self_left (a b c : Int) : (a * b + c) % a = c % a := by
rw [Int.add_comm, add_mul_emod_self_left]
@[deprecated add_mul_emod_self_right (since := "2025-04-11")]
theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
add_mul_emod_self_right ..
@[simp] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm
rwa [Int.add_right_comm, emod_add_mul_ediv] at this

View File

@@ -510,9 +510,6 @@ theorem ediv_neg_of_neg_of_pos {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0
match a, b, eq_negSucc_of_lt_zero Ha, eq_succ_of_zero_lt Hb with
| _, _, _, rfl, _, rfl => negSucc_lt_zero _
@[deprecated ediv_neg_of_neg_of_pos (since := "2025-03-04")]
abbrev ediv_neg' := @ediv_neg_of_neg_of_pos
theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(ediv m b + 1) :=
match b, eq_succ_of_zero_lt H with
| _, _, rfl => rfl
@@ -545,9 +542,6 @@ theorem ediv_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a / b
theorem ediv_nonpos_of_nonneg_of_nonpos {a b : Int} (Ha : 0 a) (Hb : b 0) : a / b 0 :=
Int.nonpos_of_neg_nonneg <| Int.ediv_neg .. Int.ediv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
@[deprecated ediv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
abbrev ediv_nonpos := @ediv_nonpos_of_nonneg_of_nonpos
theorem ediv_eq_zero_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) : a / b = 0 :=
match a, b, eq_ofNat_of_zero_le H1, eq_succ_of_zero_lt (Int.lt_of_le_of_lt H1 H2) with
| _, _, _, rfl, _, rfl => congrArg Nat.cast <| Nat.div_eq_of_lt <| ofNat_lt.1 H2
@@ -678,25 +672,15 @@ theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = ↑(m % n) := rfl
@[simp] theorem add_neg_mul_emod_self_right (a b c : Int) : (a + -(b * c)) % c = a % c := by
rw [Int.neg_mul_eq_neg_mul, add_mul_emod_self_right]
@[deprecated add_neg_mul_emod_self_right (since := "2025-04-11")]
theorem add_neg_mul_emod_self {a b c : Int} : (a + -(b * c)) % c = a % c :=
add_neg_mul_emod_self_right ..
@[simp] theorem add_neg_mul_emod_self_left (a b c : Int) : (a + -(b * c)) % b = a % b := by
rw [Int.neg_mul_eq_mul_neg, add_mul_emod_self_left]
@[simp] theorem add_emod_right (a b : Int) : (a + b) % b = a % b := by
have := add_mul_emod_self_left a b 1; rwa [Int.mul_one] at this
@[deprecated add_emod_right (since := "2025-04-11")]
theorem add_emod_self {a b : Int} : (a + b) % b = a % b := add_emod_right ..
@[simp] theorem add_emod_left (a b : Int) : (a + b) % a = b % a := by
rw [Int.add_comm, add_emod_right]
@[deprecated add_emod_left (since := "2025-04-11")]
theorem add_emod_self_left {a b : Int} : (a + b) % a = b % a := add_emod_left ..
@[simp] theorem sub_mul_emod_self_right (a b c : Int) : (a - b * c) % c = a % c := by
simp [Int.sub_eq_add_neg]
@@ -937,9 +921,6 @@ where
| -[_+1], 0 => Nat.zero_le _
| -[_+1], succ _ => Nat.succ_le_succ (Nat.div_le_self _ _)
@[deprecated natAbs_ediv_le_natAbs (since := "2025-03-05")]
abbrev natAbs_div_le_natAbs := natAbs_ediv_le_natAbs
theorem ediv_le_self {a : Int} (b : Int) (Ha : 0 a) : a / b a := by
have := Int.le_trans le_natAbs (ofNat_le.2 <| natAbs_ediv_le_natAbs a b)
rwa [natAbs_of_nonneg Ha] at this
@@ -972,14 +953,6 @@ theorem emod_eq_iff {a b c : Int} (hb : b ≠ 0) : a % b = c ↔ 0 ≤ c ∧ c <
rw [ dvd_iff_emod_eq_zero, Int.dvd_neg]
exact Int.dvd_mul_right a b
@[deprecated mul_ediv_cancel (since := "2025-03-05")]
theorem neg_mul_ediv_cancel (a b : Int) (h : b 0) : -(a * b) / b = -a := by
rw [neg_ediv_of_dvd (Int.dvd_mul_left a b), mul_ediv_cancel _ h]
@[deprecated mul_ediv_cancel (since := "2025-03-05")]
theorem neg_mul_ediv_cancel_left (a b : Int) (h : a 0) : -(a * b) / a = -b := by
rw [neg_ediv_of_dvd (Int.dvd_mul_right a b), mul_ediv_cancel_left _ h]
@[simp] theorem ediv_one : a : Int, a / 1 = a
| (_:Nat) => congrArg Nat.cast (Nat.div_one _)
| -[_+1] => congrArg negSucc (Nat.div_one _)
@@ -993,10 +966,6 @@ theorem ediv_minus_one (a : Int) : a / (-1) = -a := by
theorem emod_minus_one (a : Int) : a % (-1) = 0 := by
simp
@[deprecated sub_emod_right (since := "2025-04-11")]
theorem emod_sub_cancel (x y : Int) : (x - y) % y = x % y :=
sub_emod_right ..
@[simp] theorem add_neg_emod_self (a b : Int) : (a + -b) % b = a % b := by
rw [Int.add_neg_eq_sub, sub_emod_right]
@@ -1007,10 +976,6 @@ theorem emod_sub_cancel (x y : Int) : (x - y) % y = x % y :=
theorem dvd_self_sub_of_emod_eq {a b : Int} : {c : Int} a % b = c b a - c
| _, rfl => dvd_self_sub_emod
@[deprecated dvd_self_sub_of_emod_eq (since := "2025-04-12")]
theorem dvd_sub_of_emod_eq {a b : Int} : {c : Int} a % b = c b a - c :=
dvd_self_sub_of_emod_eq
theorem dvd_sub_self_of_emod_eq {a b : Int} : {c : Int} a % b = c b c - a
| _, rfl => dvd_emod_sub_self
@@ -1329,9 +1294,6 @@ theorem tdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0
protected theorem tdiv_nonpos_of_nonneg_of_nonpos {a b : Int} (Ha : 0 a) (Hb : b 0) : a.tdiv b 0 :=
Int.nonpos_of_neg_nonneg <| Int.tdiv_neg .. Int.tdiv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
@[deprecated Int.tdiv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
abbrev tdiv_nonpos := @Int.tdiv_nonpos_of_nonneg_of_nonpos
theorem tdiv_eq_zero_of_lt {a b : Int} (H1 : 0 a) (H2 : a < b) : a.tdiv b = 0 :=
match a, b, eq_ofNat_of_zero_le H1, eq_succ_of_zero_lt (Int.lt_of_le_of_lt H1 H2) with
| _, _, _, rfl, _, rfl => congrArg Nat.cast <| Nat.div_eq_of_lt <| ofNat_lt.1 H2
@@ -1890,10 +1852,6 @@ theorem le_emod_self_add_one_iff {a b : Int} (h : 0 < b) : b ≤ a % b + 1 ↔ b
sign_eq_one_of_pos (by omega), Int.mul_add]
omega
@[deprecated le_emod_self_add_one_iff (since := "2025-04-12")]
theorem le_mod_self_add_one_iff {a b : Int} (h : 0 < b) : b a % b + 1 b a + 1 :=
le_emod_self_add_one_iff h
theorem add_one_tdiv_of_pos {a b : Int} (h : 0 < b) :
(a + 1).tdiv b = a.tdiv b + if (0 < a + 1 b a + 1) (a < 0 b a) then 1 else 0 := by
match b, h with
@@ -2029,9 +1987,6 @@ theorem fdiv_nonpos_of_nonneg_of_nonpos : ∀ {a b : Int}, 0 ≤ a → b ≤ 0
| 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => by
simp [fdiv, negSucc_le_zero]
@[deprecated fdiv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
abbrev fdiv_nonpos := @fdiv_nonpos_of_nonneg_of_nonpos
theorem fdiv_neg_of_neg_of_pos : {a b : Int}, a < 0 0 < b a.fdiv b < 0
| -[_+1], succ _, _, _ => negSucc_lt_zero _
@@ -2150,9 +2105,6 @@ theorem fmod_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a.fmod b :
theorem fmod_nonneg_of_pos (a : Int) {b : Int} (hb : 0 < b) : 0 a.fmod b :=
fmod_eq_emod_of_nonneg _ (Int.le_of_lt hb) emod_nonneg _ (Int.ne_of_lt hb).symm
@[deprecated fmod_nonneg_of_pos (since := "2025-03-04")]
abbrev fmod_nonneg' := @fmod_nonneg_of_pos
theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
fmod_eq_emod_of_nonneg _ (Int.le_of_lt H) emod_lt_of_pos a H
@@ -2162,10 +2114,6 @@ theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
rw [fmod_eq_emod, add_mul_emod_self_right, fmod_eq_emod]
simp
@[deprecated add_mul_fmod_self_right (since := "2025-04-11")]
theorem add_mul_fmod_self {a b c : Int} : (a + b * c).fmod c = a.fmod c :=
add_mul_fmod_self_right ..
@[simp] theorem add_mul_fmod_self_left (a b c : Int) : (a + b * c).fmod b = a.fmod b := by
rw [Int.mul_comm, Int.add_mul_fmod_self_right]
@@ -2464,20 +2412,12 @@ theorem dvd_sub_self_of_fmod_eq {a b c : Int} (h : a.fmod b = c) :
@[simp] theorem fmod_one (a : Int) : a.fmod 1 = 0 := by
simp [fmod_def, Int.one_mul, Int.sub_self]
@[deprecated sub_fmod_right (since := "2025-04-12")]
theorem fmod_sub_cancel (x y : Int) : (x - y).fmod y = x.fmod y :=
sub_fmod_right _ _
@[simp] theorem add_neg_fmod_self (a b : Int) : (a + -b).fmod b = a.fmod b := by
rw [Int.add_neg_eq_sub, sub_fmod_right]
@[simp] theorem neg_add_fmod_self (a b : Int) : (-a + b).fmod a = b.fmod a := by
rw [Int.add_comm, add_neg_fmod_self]
@[deprecated dvd_self_sub_of_fmod_eq (since := "2025-04-12")]
theorem dvd_sub_of_fmod_eq {a b c : Int} (h : a.fmod b = c) : b a - c :=
dvd_self_sub_of_fmod_eq h
theorem fdiv_sign {a b : Int} : a.fdiv (sign b) = a * sign b := by
rw [fdiv_eq_ediv]
rcases sign_trichotomy b with h | h | h <;> simp [h]
@@ -2511,10 +2451,6 @@ theorem lt_mul_fdiv_self_add {x k : Int} (h : 0 < k) : x < k * (x.fdiv k) + k :=
theorem emod_bmod (x : Int) (n : Nat) : Int.bmod (x%n) n = Int.bmod x n := by
simp [bmod]
@[deprecated emod_bmod (since := "2025-04-11")]
theorem emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n) n = Int.bmod x n :=
emod_bmod ..
theorem bdiv_add_bmod (x : Int) (m : Nat) : m * bdiv x m + bmod x m = x := by
unfold bdiv bmod
split
@@ -2556,9 +2492,6 @@ theorem bmod_eq_emod (x : Int) (m : Nat) : bmod x m = x % m - if x % m ≥ (m +
theorem bmod_one (x : Int) : Int.bmod x 1 = 0 := by
simp [Int.bmod]
@[deprecated bmod_one (since := "2025-04-10")]
abbrev bmod_one_is_zero := @bmod_one
@[simp] theorem add_bmod_right (a : Int) (b : Nat) : (a + b).bmod b = a.bmod b := by
simp [bmod_def]
@@ -2601,76 +2534,36 @@ abbrev bmod_one_is_zero := @bmod_one
@[simp] theorem add_neg_mul_bmod_self_left (a : Int) (b : Nat) (c : Int) : (a + -(b * c)).bmod b = a.bmod b := by
simp [bmod_def]
@[deprecated add_bmod_right (since := "2025-04-10")]
theorem bmod_add_cancel {x : Int} {n : Nat} : Int.bmod (x + n) n = Int.bmod x n :=
add_bmod_right ..
@[deprecated add_mul_bmod_self_left (since := "2025-04-10")]
theorem bmod_add_mul_cancel (x : Int) (n : Nat) (k : Int) : Int.bmod (x + n * k) n = Int.bmod x n :=
add_mul_bmod_self_left ..
@[deprecated sub_bmod_right (since := "2025-04-10")]
theorem bmod_sub_cancel (x : Int) (n : Nat) : Int.bmod (x - n) n = Int.bmod x n :=
sub_bmod_right ..
@[deprecated sub_mul_bmod_self_left (since := "2025-04-10")]
theorem Int.bmod_sub_mul_cancel (x : Int) (n : Nat) (k : Int) : (x - n * k).bmod n = x.bmod n :=
sub_mul_bmod_self_left ..
@[simp]
theorem emod_add_bmod (x : Int) (n : Nat) : Int.bmod (x % n + y) n = Int.bmod (x + y) n := by
simp [Int.emod_def, Int.sub_eq_add_neg]
rw [Int.mul_neg, Int.add_right_comm, Int.add_mul_bmod_self_left]
@[deprecated emod_add_bmod (since := "2025-04-11")]
theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x % n + y) n = Int.bmod (x + y) n :=
emod_add_bmod ..
@[simp]
theorem emod_sub_bmod (x : Int) (n : Nat) : Int.bmod (x % n - y) n = Int.bmod (x - y) n := by
simp only [emod_def, Int.sub_eq_add_neg]
rw [Int.mul_neg, Int.add_right_comm, Int.add_mul_bmod_self_left]
@[deprecated emod_sub_bmod (since := "2025-04-11")]
theorem emod_sub_bmod_congr (x : Int) (n : Nat) : Int.bmod (x % n - y) n = Int.bmod (x - y) n :=
emod_sub_bmod ..
@[simp]
theorem sub_emod_bmod (x : Int) (n : Nat) : Int.bmod (x - y % n) n = Int.bmod (x - y) n := by
simp only [emod_def]
rw [Int.sub_eq_add_neg, Int.neg_sub, Int.sub_eq_add_neg, Int.add_assoc, Int.add_right_comm,
Int.add_mul_bmod_self_left, Int.sub_eq_add_neg]
@[deprecated sub_emod_bmod (since := "2025-04-11")]
theorem sub_emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x - y % n) n = Int.bmod (x - y) n :=
sub_emod_bmod ..
@[simp]
theorem emod_mul_bmod (x : Int) (n : Nat) : Int.bmod (x % n * y) n = Int.bmod (x * y) n := by
simp [Int.emod_def, Int.sub_eq_add_neg]
rw [Int.mul_neg, Int.add_mul, Int.mul_assoc, Int.add_mul_bmod_self_left]
@[deprecated emod_mul_bmod (since := "2025-04-11")]
theorem emod_mul_bmod_congr (x : Int) (n : Nat) : Int.bmod (x % n * y) n = Int.bmod (x * y) n :=
emod_mul_bmod ..
@[simp]
theorem bmod_add_bmod : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n := by
have := (@add_mul_bmod_self_left (Int.bmod x n + y) n (bdiv x n)).symm
rwa [Int.add_right_comm, bmod_add_bdiv] at this
@[deprecated bmod_add_bmod (since := "2025-04-11")]
theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n :=
bmod_add_bmod ..
@[simp]
theorem bmod_sub_bmod : Int.bmod (Int.bmod x n - y) n = Int.bmod (x - y) n :=
@bmod_add_bmod x n (-y)
@[deprecated bmod_sub_bmod (since := "2025-04-11")]
theorem bmod_sub_bmod_congr : Int.bmod (Int.bmod x n - y) n = Int.bmod (x - y) n :=
bmod_sub_bmod ..
theorem add_bmod_eq_add_bmod_right (i : Int)
(H : bmod x n = bmod y n) : bmod (x + i) n = bmod (y + i) n := by
rw [ bmod_add_bmod, @bmod_add_bmod y, H]
@@ -2863,9 +2756,6 @@ theorem bmod_natAbs_add_one (x : Int) (w : x ≠ -1) : x.bmod (x.natAbs + 1) = -
· rw [sign_eq_one_iff_pos.2 hx]
exact by omega, by omega, -1, by omega
@[deprecated bmod_natAbs_add_one (since := "2025-04-04")]
abbrev bmod_natAbs_plus_one := @bmod_natAbs_add_one
theorem bmod_self_add_one {x : Nat} : (x : Int).bmod (x + 1) = if x = 0 then 0 else -1 := by
have := bmod_natAbs_add_one x (by omega)
simp only [natAbs_natCast] at this
@@ -2986,11 +2876,6 @@ theorem bmod_eq_of_le {n : Int} {m : Nat} (hn' : -(m / 2) ≤ n) (hn : n < (m +
n.bmod m = n :=
(Nat.eq_zero_or_pos m).elim (by rintro rfl; simp) (fun hm => by simp_all [bmod_eq_iff])
@[deprecated bmod_eq_of_le (since := "2025-04-11")]
theorem bmod_eq_self_of_le {n : Int} {m : Nat} (hn' : -(m / 2) n) (hn : n < (m + 1) / 2) :
n.bmod m = n :=
bmod_eq_of_le hn' hn
theorem bmod_bmod_of_dvd {a : Int} {n m : Nat} (hnm : n m) :
(a.bmod m).bmod n = a.bmod n := by
rw [ Int.sub_eq_iff_eq_add.2 (bmod_add_bdiv a m).symm]
@@ -3001,11 +2886,6 @@ theorem bmod_eq_of_le_mul_two {x : Int} {y : Nat} (hle : -y ≤ x * 2) (hlt : x
x.bmod y = x := by
apply bmod_eq_of_le (by omega) (by omega)
@[deprecated bmod_eq_of_le_mul_two (since := "2025-04-11")]
theorem bmod_eq_self_of_le_mul_two {x : Int} {y : Nat} (hle : -y x * 2) (hlt : x * 2 < y) :
x.bmod y = x :=
bmod_eq_of_le_mul_two hle hlt
/- ### ediv -/
theorem ediv_lt_self_of_pos_of_ne_one {x y : Int} (hx : 0 < x) (hy : y 1) :

View File

@@ -74,9 +74,6 @@ theorem negSucc_inj : negSucc m = negSucc n ↔ m = n := ⟨negSucc.inj, fun H =
theorem negSucc_eq (n : Nat) : -[n+1] = -((n : Int) + 1) := rfl
@[deprecated negSucc_eq (since := "2025-03-11")]
theorem negSucc_coe (n : Nat) : -[n+1] = -(n + 1) := rfl
@[simp] theorem negSucc_ne_zero (n : Nat) : -[n+1] 0 := nofun
@[simp] theorem zero_ne_negSucc (n : Nat) : 0 -[n+1] := nofun
@@ -353,10 +350,6 @@ protected theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c) := by
change ofNat (n - succ m) = subNatNat n (succ m)
rw [subNatNat, Nat.sub_eq_zero_of_le h]
@[deprecated negSucc_eq (since := "2025-03-11")]
theorem negSucc_coe' (n : Nat) : -[n+1] = -n - 1 := by
rw [Int.sub_eq_add_neg, Int.neg_add]; rfl
protected theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = m - n := by
apply subNatNat_elim m n fun m n i => i = m - n
· intro i n

View File

@@ -118,14 +118,8 @@ theorem pos_iff_toNat_pos {n : Int} : 0 < n ↔ 0 < n.toNat := by
theorem natCast_toNat_eq_self {a : Int} : a.toNat = a 0 a := by omega
@[deprecated natCast_toNat_eq_self (since := "2025-04-16")]
theorem ofNat_toNat_eq_self {a : Int} : a.toNat = a 0 a := natCast_toNat_eq_self
theorem eq_natCast_toNat {a : Int} : a = a.toNat 0 a := by omega
@[deprecated eq_natCast_toNat (since := "2025-04-16")]
theorem eq_ofNat_toNat {a : Int} : a = a.toNat 0 a := eq_natCast_toNat
theorem toNat_le_toNat {n m : Int} (h : n m) : n.toNat m.toNat := by omega
theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat n < m := by omega

View File

@@ -234,9 +234,6 @@ theorem eq_natAbs_of_nonneg {a : Int} (h : 0 ≤ a) : a = natAbs a := by
let n, e := eq_ofNat_of_zero_le h
rw [e]; rfl
@[deprecated eq_natAbs_of_nonneg (since := "2025-03-11")]
abbrev eq_natAbs_of_zero_le := @eq_natAbs_of_nonneg
theorem le_natAbs {a : Int} : a natAbs a :=
match Int.le_total 0 a with
| .inl h => by rw [eq_natAbs_of_nonneg h]; apply Int.le_refl
@@ -554,9 +551,6 @@ protected theorem mul_le_mul_of_nonpos_left {a b c : Int}
@[simp, norm_cast] theorem natAbs_natCast (n : Nat) : natAbs n = n := rfl
@[deprecated natAbs_natCast (since := "2025-04-16")]
theorem natAbs_ofNat (n : Nat) : natAbs n = n := natAbs_natCast n
/-
TODO: rename `natAbs_ofNat'` to `natAbs_ofNat` once the current deprecated alias
`natAbs_ofNat := natAbs_natCast` is removed
@@ -646,17 +640,11 @@ theorem toNat_of_nonneg {a : Int} (h : 0 ≤ a) : (toNat a : Int) = a := by
@[simp] theorem toNat_natCast (n : Nat) : toNat n = n := rfl
@[deprecated toNat_natCast (since := "2025-04-16")]
theorem toNat_ofNat (n : Nat) : toNat n = n := rfl
@[simp] theorem toNat_negSucc (n : Nat) : (Int.negSucc n).toNat = 0 := by
simp [toNat]
@[simp] theorem toNat_natCast_add_one {n : Nat} : ((n : Int) + 1).toNat = n + 1 := rfl
@[deprecated toNat_natCast_add_one (since := "2025-04-16")]
theorem toNat_ofNat_add_one {n : Nat} : ((n : Int) + 1).toNat = n + 1 := toNat_natCast_add_one
@[simp] theorem ofNat_toNat (a : Int) : (a.toNat : Int) = max a 0 := by
match a with
| (n : Nat) => simp
@@ -717,9 +705,6 @@ theorem mem_toNat? : ∀ {a : Int} {n : Nat}, toNat? a = some n ↔ a = n
| (m : Nat), n => by simp [toNat?, Int.ofNat_inj]
| -[m+1], n => by constructor <;> nofun
@[deprecated mem_toNat? (since := "2025-03-11")]
abbrev mem_toNat' := @mem_toNat?
/-! ## Order properties of the integers -/
protected theorem le_of_not_le {a b : Int} : ¬ a b b a := (Int.le_total a b).resolve_left
@@ -1259,18 +1244,10 @@ theorem natAbs_sign (z : Int) : z.sign.natAbs = if z = 0 then 0 else 1 :=
theorem natAbs_sign_of_ne_zero {z : Int} (hz : z 0) : z.sign.natAbs = 1 := by
rw [Int.natAbs_sign, if_neg hz]
@[deprecated natAbs_sign_of_ne_zero (since := "2025-04-16")]
theorem natAbs_sign_of_nonzero {z : Int} (hz : z 0) : z.sign.natAbs = 1 :=
natAbs_sign_of_ne_zero hz
theorem sign_natCast_of_ne_zero {n : Nat} (hn : n 0) : Int.sign n = 1 :=
match n, Nat.exists_eq_succ_of_ne_zero hn with
| _, n, rfl => Int.sign_of_add_one n
@[deprecated sign_natCast_of_ne_zero (since := "2025-04-16")]
theorem sign_ofNat_of_nonzero {n : Nat} (hn : n 0) : Int.sign n = 1 :=
sign_natCast_of_ne_zero hn
@[simp] theorem sign_neg (z : Int) : Int.sign (-z) = -Int.sign z := by
match z with | 0 | succ _ | -[_+1] => rfl
@@ -1325,8 +1302,6 @@ theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0
exact Int.le_add_one (natCast_nonneg _)
| .negSucc _ => simp +decide [sign]
@[deprecated sign_nonneg_iff (since := "2025-03-11")] abbrev sign_nonneg := @sign_nonneg_iff
@[simp] theorem sign_pos_iff : 0 < sign x 0 < x := by
match x with
| 0
@@ -1409,9 +1384,6 @@ theorem natAbs_add_of_nonpos {a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) :
natAbs_add_of_nonneg (Int.neg_nonneg_of_nonpos ha) (Int.neg_nonneg_of_nonpos hb),
natAbs_neg (-a), natAbs_neg (-b)]
@[deprecated negSucc_eq (since := "2025-03-11")]
theorem negSucc_eq' (m : Nat) : -[m+1] = -m - 1 := by simp only [negSucc_eq, Int.neg_add]; rfl
theorem natAbs_lt_natAbs_of_nonneg_of_lt {a b : Int}
(w₁ : 0 a) (w₂ : a < b) : a.natAbs < b.natAbs :=
match a, b, eq_ofNat_of_zero_le w₁, eq_ofNat_of_zero_le (Int.le_trans w₁ (Int.le_of_lt w₂)) with
@@ -1420,9 +1392,6 @@ theorem natAbs_lt_natAbs_of_nonneg_of_lt {a b : Int}
theorem natAbs_eq_iff_mul_eq_zero : natAbs a = n (a - n) * (a + n) = 0 := by
rw [natAbs_eq_iff, Int.mul_eq_zero, Int.sub_neg, Int.sub_eq_zero, Int.sub_eq_zero]
@[deprecated natAbs_eq_iff_mul_eq_zero (since := "2025-03-11")]
abbrev eq_natAbs_iff_mul_eq_zero := @natAbs_eq_iff_mul_eq_zero
instance instIsLinearOrder : IsLinearOrder Int := by
apply IsLinearOrder.of_le
case le_antisymm => constructor; apply Int.le_antisymm

View File

@@ -49,10 +49,6 @@ protected theorem pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0 := b
instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := Int.pow_ne_zero (NeZero.ne _)
-- This can't be removed until the next update-stage0
@[deprecated Nat.pow_pos (since := "2025-02-17")]
abbrev _root_.Nat.pos_pow_of_pos := @Nat.pow_pos
@[simp, norm_cast]
protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
match n with

View File

@@ -1038,9 +1038,6 @@ def dropLast {α} : List α → List α
@[simp, grind =] theorem dropLast_nil : ([] : List α).dropLast = [] := rfl
@[simp, grind =] theorem dropLast_singleton : [x].dropLast = [] := rfl
@[deprecated dropLast_singleton (since := "2025-04-16")]
theorem dropLast_single : [x].dropLast = [] := dropLast_singleton
@[simp, grind =] theorem dropLast_cons₂ :
(x::y::zs).dropLast = x :: (y::zs).dropLast := rfl

View File

@@ -705,12 +705,6 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {i : Nat} {a b : α}, a ∈ l.s
@[simp, grind =] theorem nil_beq_eq [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
cases l <;> rfl
@[deprecated beq_nil_eq (since := "2025-04-04")]
abbrev beq_nil_iff := @beq_nil_eq
@[deprecated nil_beq_eq (since := "2025-04-04")]
abbrev nil_beq_iff := @nil_beq_eq
@[simp, grind =] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
(a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
@@ -933,9 +927,6 @@ theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys
@[simp] theorem isSome_head? : l.head?.isSome l [] := by
cases l <;> simp
@[deprecated isSome_head? (since := "2025-03-18")]
abbrev head?_isSome := @isSome_head?
@[simp] theorem head_mem : {l : List α} (h : l []), head l h l
| [], h => absurd rfl h
| _::_, _ => .head ..
@@ -1266,9 +1257,6 @@ theorem length_filter_eq_length_iff {l} : (filter p l).length = l.length ↔ ∀
· have := Nat.ne_of_lt (Nat.lt_succ.mpr (length_filter_le p l))
simp_all
@[deprecated length_filter_eq_length_iff (since := "2025-04-04")]
abbrev filter_length_eq_length := @length_filter_eq_length_iff
@[simp, grind =] theorem mem_filter : x filter p as x as p x := by
induction as with
| nil => simp

View File

@@ -548,9 +548,6 @@ theorem _root_.Array.replicate_eq_toArray_replicate :
Array.replicate n v = (List.replicate n v).toArray := by
simp
@[deprecated _root_.Array.replicate_eq_toArray_replicate (since := "2025-03-18")]
abbrev _root_.Array.mkArray_eq_toArray_replicate := @_root_.Array.replicate_eq_toArray_replicate
@[simp, grind =] theorem flatMap_empty {β} (f : α Array β) : (#[] : Array α).flatMap f = #[] := rfl
theorem flatMap_toArray_cons {β} (f : α Array β) (a : α) (as : List α) :

View File

@@ -627,9 +627,6 @@ theorem eq_zero_or_eq_succ_pred : ∀ n, n = 0 n = succ (pred n)
theorem succ_inj : succ a = succ b a = b := (Nat.succ.injEq a b).to_iff
@[deprecated succ_inj (since := "2025-04-14")]
theorem succ_inj' : succ a = succ b a = b := succ_inj
theorem succ_le_succ_iff : succ a succ b a b := le_of_succ_le_succ, succ_le_succ
theorem succ_lt_succ_iff : succ a < succ b a < b := lt_of_succ_lt_succ, succ_lt_succ

View File

@@ -132,9 +132,6 @@ theorem testBit_eq_decide_div_mod_eq {x : Nat} : testBit x i = decide (x / 2^i %
| succ i hyp =>
simp [hyp, Nat.div_div_eq_div_mul, Nat.pow_succ']
@[deprecated testBit_eq_decide_div_mod_eq (since := "2025-04-04")]
abbrev testBit_to_div_mod := @testBit_eq_decide_div_mod_eq
theorem toNat_testBit (x i : Nat) :
(x.testBit i).toNat = x / 2 ^ i % 2 := by
rw [testBit_eq_decide_div_mod_eq]
@@ -155,9 +152,6 @@ theorem exists_testBit_of_ne_zero {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i
apply Exists.intro 0
simp_all
@[deprecated exists_testBit_of_ne_zero (since := "2025-04-04")]
abbrev ne_zero_implies_bit_true := @exists_testBit_of_ne_zero
theorem exists_testBit_ne_of_ne {x y : Nat} (p : x y) : i, testBit x i testBit y i := by
induction y using Nat.div2Induction generalizing x with
| ind y hyp =>
@@ -183,9 +177,6 @@ theorem exists_testBit_ne_of_ne {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i
cases mod_two_eq_zero_or_one x with
| _ p => cases mod_two_eq_zero_or_one y with | _ q => simp [p,q]
@[deprecated exists_testBit_ne_of_ne (since := "2025-04-04")]
abbrev ne_implies_bit_diff := @exists_testBit_ne_of_ne
/--
`eq_of_testBit_eq` allows proving two natural numbers are equal
if their bits are all equal.
@@ -218,9 +209,6 @@ theorem exists_ge_and_testBit_of_ge_two_pow {x : Nat} (p : x ≥ 2^n) : ∃ i
case right =>
simpa using jp.right
@[deprecated exists_ge_and_testBit_of_ge_two_pow (since := "2025-04-04")]
abbrev ge_two_pow_implies_high_bit_true := @exists_ge_and_testBit_of_ge_two_pow
theorem ge_two_pow_of_testBit {x : Nat} (p : testBit x i = true) : x 2^i := by
simp only [Nat.testBit_eq_decide_div_mod_eq] at p
apply Decidable.by_contra
@@ -228,9 +216,6 @@ theorem ge_two_pow_of_testBit {x : Nat} (p : testBit x i = true) : x ≥ 2^i :=
have x_lt : x < 2^i := Nat.lt_of_not_le not_ge
simp [div_eq_of_lt x_lt] at p
@[deprecated ge_two_pow_of_testBit (since := "2025-04-04")]
abbrev testBit_implies_ge := @ge_two_pow_of_testBit
theorem testBit_lt_two_pow {x i : Nat} (lt : x < 2^i) : x.testBit i = false := by
match p : x.testBit i with
| false => trivial
@@ -529,16 +514,10 @@ theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n
simp only [testBit_and, testBit_mod_two_pow]
cases testBit x i <;> simp
@[deprecated and_two_pow_sub_one_eq_mod (since := "2025-03-18")]
abbrev and_pow_two_sub_one_eq_mod := @and_two_pow_sub_one_eq_mod
theorem and_two_pow_sub_one_of_lt_two_pow {x : Nat} (lt : x < 2^n) : x &&& 2^n - 1 = x := by
rw [and_two_pow_sub_one_eq_mod]
apply Nat.mod_eq_of_lt lt
@[deprecated and_two_pow_sub_one_of_lt_two_pow (since := "2025-03-18")]
abbrev and_pow_two_sub_one_of_lt_two_pow := @and_two_pow_sub_one_of_lt_two_pow
@[simp] theorem and_mod_two_eq_one : (a &&& b) % 2 = 1 a % 2 = 1 b % 2 = 1 := by
simp only [mod_two_eq_one_iff_testBit_zero]
rw [testBit_and]
@@ -728,9 +707,6 @@ theorem testBit_two_pow_mul_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat)
Nat.div_eq_of_lt b_lt,
Nat.two_pow_pos i]
@[deprecated testBit_two_pow_mul_add (since := "2025-03-18")]
abbrev testBit_mul_pow_two_add := @testBit_two_pow_mul_add
@[grind =]
theorem testBit_two_pow_mul :
testBit (2 ^ i * a) j = (decide (j i) && testBit a (j-i)) := by
@@ -745,9 +721,6 @@ theorem testBit_mul_two_pow (x j i : Nat) :
(x * 2 ^ i).testBit j = (decide (i j) && x.testBit (j - i)) := by
rw [Nat.mul_comm, testBit_two_pow_mul]
@[deprecated testBit_two_pow_mul (since := "2025-03-18")]
abbrev testBit_mul_pow_two := @testBit_two_pow_mul
theorem two_pow_add_eq_or_of_lt {b : Nat} (b_lt : b < 2^i) (a : Nat) :
2^i * a + b = 2^i * a ||| b := by
apply eq_of_testBit_eq
@@ -763,9 +736,6 @@ theorem two_pow_add_eq_or_of_lt {b : Nat} (b_lt : b < 2^i) (a : Nat) :
_ 2 ^ j := Nat.pow_le_pow_right Nat.zero_lt_two i_le
simp [i_le, j_lt, testBit_lt_two_pow, b_lt_j]
@[deprecated two_pow_add_eq_or_of_lt (since := "2025-03-18")]
abbrev mul_add_lt_is_or := @two_pow_add_eq_or_of_lt
/-! ### shiftLeft and shiftRight -/
@[simp, grind =] theorem testBit_shiftLeft (x : Nat) : testBit (x <<< i) j =

View File

@@ -30,9 +30,6 @@ theorem compare_eq_ite_lt (a b : Nat) :
| .inl h => simp [h, Nat.ne_of_gt h]
| .inr rfl => simp
@[deprecated compare_eq_ite_lt (since := "2025-03_28")]
def compare_def_lt := compare_eq_ite_lt
theorem compare_eq_ite_le (a b : Nat) :
compare a b = if a b then if b a then .eq else .lt else .gt := by
rw [compare_eq_ite_lt]
@@ -43,9 +40,6 @@ theorem compare_eq_ite_le (a b : Nat) :
next hgt => simp [Nat.not_le.2 hgt]
next hle => simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle]
@[deprecated compare_eq_ite_le (since := "2025-03_28")]
def compare_def_le := compare_eq_ite_le
protected theorem compare_swap (a b : Nat) : (compare a b).swap = compare b a := by
simp only [compare_eq_ite_le]; (repeat' split) <;> try rfl
next h1 h2 => cases h1 (Nat.le_of_not_le h2)

View File

@@ -182,17 +182,9 @@ theorem gcd_dvd_gcd_of_dvd_right {m k : Nat} (n : Nat) (H : m k) : gcd n m
theorem gcd_dvd_gcd_mul_left_left (m n k : Nat) : gcd m n gcd (k * m) n :=
gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_left _ _)
@[deprecated gcd_dvd_gcd_mul_left_left (since := "2025-04-01")]
theorem gcd_dvd_gcd_mul_left (m n k : Nat) : gcd m n gcd (k * m) n :=
gcd_dvd_gcd_mul_left_left m n k
theorem gcd_dvd_gcd_mul_right_left (m n k : Nat) : gcd m n gcd (m * k) n :=
gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_right _ _)
@[deprecated gcd_dvd_gcd_mul_right_left (since := "2025-04-01")]
theorem gcd_dvd_gcd_mul_right (m n k : Nat) : gcd m n gcd (m * k) n :=
gcd_dvd_gcd_mul_right_left m n k
theorem gcd_dvd_gcd_mul_left_right (m n k : Nat) : gcd m n gcd m (k * n) :=
gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_left _ _)
@@ -242,10 +234,6 @@ theorem gcd_left_eq_iff {m m' n : Nat} : gcd m n = gcd m' n ↔ ∀ k, k n
@[simp] theorem gcd_add_mul_right_right (m n k : Nat) : gcd m (n + k * m) = gcd m n := by
simp [gcd_rec m (n + k * m), gcd_rec m n]
@[deprecated gcd_add_mul_right_right (since := "2025-03-31")]
theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n :=
gcd_add_mul_right_right _ _ _
@[simp] theorem gcd_add_mul_left_right (m n k : Nat) : gcd m (n + m * k) = gcd m n := by
rw [Nat.mul_comm, gcd_add_mul_right_right]
@@ -389,11 +377,6 @@ def dvdProdDvdOfDvdProd {k m n : Nat} (h : k m * n) :
rw [hd, gcd_mul_right]
exact Nat.dvd_gcd (Nat.dvd_mul_right _ _) h
@[inherit_doc dvdProdDvdOfDvdProd, deprecated dvdProdDvdOfDvdProd (since := "2025-04-01")]
def prod_dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k m * n) :
{d : {m' // m' m} × {n' // n' n} // k = d.1.val * d.2.val} :=
dvdProdDvdOfDvdProd H
protected theorem dvd_mul {k m n : Nat} : k m * n k₁ k₂, k₁ m k₂ n k₁ * k₂ = k := by
refine fun h => ?_, ?_
· obtain k₁, hk₁, k₂, hk₂, rfl := dvdProdDvdOfDvdProd h
@@ -410,10 +393,6 @@ theorem gcd_mul_right_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) gcd k m * gc
(dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_right m' n') h') hm')
(dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_left n' m') h') hn')
@[deprecated gcd_mul_right_dvd_mul_gcd (since := "2025-04-02")]
theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) gcd k m * gcd k n :=
gcd_mul_right_dvd_mul_gcd k m n
theorem gcd_mul_left_dvd_mul_gcd (k m n : Nat) : gcd (m * n) k gcd m k * gcd n k := by
simpa [gcd_comm, Nat.mul_comm] using gcd_mul_right_dvd_mul_gcd _ _ _

View File

@@ -220,15 +220,6 @@ protected theorem add_right_inj {n : Nat} : n + m = n + k ↔ m = k := Nat.add_l
@[simp high] protected theorem left_eq_add {a b : Nat} : a = a + b b = 0 := by omega
@[simp high] protected theorem right_eq_add {a b : Nat} : b = a + b a = 0 := by omega
@[deprecated Nat.add_eq_right (since := "2025-04-15")]
protected theorem add_left_eq_self {a b : Nat} : a + b = b a = 0 := Nat.add_eq_right
@[deprecated Nat.add_eq_left (since := "2025-04-15")]
protected theorem add_right_eq_self {a b : Nat} : a + b = a b = 0 := Nat.add_eq_left
@[deprecated Nat.left_eq_add (since := "2025-04-15")]
protected theorem self_eq_add_right {a b : Nat} : a = a + b b = 0 := Nat.left_eq_add
@[deprecated Nat.right_eq_add (since := "2025-04-15")]
protected theorem self_eq_add_left {a b : Nat} : a = b + a b = 0 := Nat.right_eq_add
protected theorem lt_of_add_lt_add_right : {n : Nat}, k + n < m + n k < m
| 0, h => h
| _+1, h => Nat.lt_of_add_lt_add_right (Nat.lt_of_succ_lt_succ h)

View File

@@ -46,16 +46,10 @@ def isPowerOfTwo (n : Nat) := ∃ k, n = 2 ^ k
theorem isPowerOfTwo_one : isPowerOfTwo 1 :=
0, by decide
@[deprecated isPowerOfTwo_one (since := "2025-03-18")]
abbrev one_isPowerOfTwo := isPowerOfTwo_one
theorem isPowerOfTwo_mul_two_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n * 2) :=
have k, h := h
k+1, by simp [h, Nat.pow_succ]
@[deprecated isPowerOfTwo_mul_two_of_isPowerOfTwo (since := "2025-04-04")]
abbrev mul2_isPowerOfTwo_of_isPowerOfTwo := @isPowerOfTwo_mul_two_of_isPowerOfTwo
theorem pos_of_isPowerOfTwo (h : isPowerOfTwo n) : n > 0 := by
have k, h := h
rw [h]

View File

@@ -390,27 +390,6 @@ Examples:
| none => List.toArray .nil
| some a => List.toArray (.cons a .nil)
/--
Applies a function to a two optional values if both are present. Otherwise, if one value is present,
it is returned and the function is not used.
The value is `some (f a b)` if the inputs are `some a` and `some b`. Otherwise, the behavior is
equivalent to `Option.orElse`. If only one input is `some x`, then the value is `some x`. If both
are `none`, then the value is `none`.
Examples:
* `Option.liftOrGet (· + ·) none (some 3) = some 3`
* `Option.liftOrGet (· + ·) (some 2) (some 3) = some 5`
* `Option.liftOrGet (· + ·) (some 2) none = some 2`
* `Option.liftOrGet (· + ·) none none = none`
-/
@[deprecated merge (since := "2025-04-04")]
def liftOrGet (f : α α α) : Option α Option α Option α
| none, none => none
| some a, none => some a
| none, some b => some b
| some a, some b => some (f a b)
/-- Lifts a relation `α → β → Prop` to a relation `Option α → Option β → Prop` by just adding
`none ~ none`. -/
inductive Rel (r : α β Prop) : Option α Option β Prop

View File

@@ -46,10 +46,6 @@ Try to use the Boolean comparisons `Option.isNone` or `Option.isSome` instead.
@[inline] def decidableEqNone {o : Option α} : Decidable (o = none) :=
decidable_of_decidable_of_iff isNone_iff_eq_none
@[deprecated decidableEqNone (since := "2025-04-10"), inline]
def decidable_eq_none {o : Option α} : Decidable (o = none) :=
decidableEqNone
instance decidableForallMem {p : α Prop} [DecidablePred p] :
o : Option α, Decidable ( a, a o p a)
| none => isTrue nofun

View File

@@ -19,9 +19,6 @@ namespace Option
@[grind =] theorem default_eq_none : (default : Option α) = none := rfl
@[deprecated mem_def (since := "2025-04-07")]
theorem mem_iff {a : α} {b : Option α} : a b b = some a := .rfl
@[grind =] theorem mem_some {a b : α} : a some b b = a := by simp
theorem mem_some_iff {a b : α} : a some b b = a := mem_some
@@ -177,10 +174,6 @@ theorem exists_ne_none {p : Option α → Prop} : (∃ x, x ≠ none ∧ p x)
fun x, hx, hp => x.get <| ne_none_iff_isSome.1 hx, by rwa [some_get],
fun x, hx => some x, some_ne_none x, hx
@[deprecated exists_ne_none (since := "2025-04-04")]
theorem bex_ne_none {p : Option α Prop} : ( x, (_ : x none), p x) x, p (some x) := by
simp only [exists_prop, exists_ne_none]
theorem forall_ne_none {p : Option α Prop} : ( x (_ : x none), p x) x, p (some x) :=
fun h x => h (some x) (some_ne_none x),
fun h x hx => by
@@ -188,9 +181,6 @@ theorem forall_ne_none {p : Option α → Prop} : (∀ x (_ : x ≠ none), p x)
simp [some_get] at this
exact this
@[deprecated forall_ne_none (since := "2025-04-04")]
abbrev ball_ne_none := @forall_ne_none
@[simp] theorem pure_def : pure = @some α := rfl
@[grind =] theorem pure_apply : pure x = some x := rfl
@@ -207,15 +197,9 @@ abbrev ball_ne_none := @forall_ne_none
theorem bind_eq_some_iff : x.bind f = some b a, x = some a f a = some b := by
cases x <;> simp
@[deprecated bind_eq_some_iff (since := "2025-04-10")]
abbrev bind_eq_some := @bind_eq_some_iff
@[simp] theorem bind_eq_none_iff {o : Option α} {f : α Option β} :
o.bind f = none a, o = some a f a = none := by cases o <;> simp
@[deprecated bind_eq_none_iff (since := "2025-04-10")]
abbrev bind_eq_none := @bind_eq_none_iff
theorem bind_eq_none' {o : Option α} {f : α Option β} :
o.bind f = none b a, o = some a f a some b := by
cases o <;> simp [eq_none_iff_forall_ne_some]
@@ -272,9 +256,6 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α
theorem join_eq_some_iff : x.join = some a x = some (some a) := by
simp [ bind_id_eq_join, bind_eq_some_iff]
@[deprecated join_eq_some_iff (since := "2025-04-10")]
abbrev join_eq_some := @join_eq_some_iff
theorem join_ne_none : x.join none z, x = some (some z) := by
simp only [ne_none_iff_exists', join_eq_some_iff, iff_self]
@@ -284,9 +265,6 @@ theorem join_ne_none' : ¬x.join = none ↔ ∃ z, x = some (some z) :=
theorem join_eq_none_iff : o.join = none o = none o = some none :=
match o with | none | some none | some (some _) => by simp
@[deprecated join_eq_none_iff (since := "2025-04-10")]
abbrev join_eq_none := @join_eq_none_iff
theorem bind_join {f : α Option β} {o : Option (Option α)} :
o.join.bind f = o.bind (·.bind f) := by
cases o <;> simp
@@ -295,36 +273,15 @@ theorem bind_join {f : α → Option β} {o : Option (Option α)} :
@[grind =] theorem map_apply : Functor.map f x = Option.map f x := rfl
@[deprecated map_none (since := "2025-04-10")]
abbrev map_none' := @map_none
@[deprecated map_some (since := "2025-04-10")]
abbrev map_some' := @map_some
@[simp] theorem map_eq_some_iff : x.map f = some b a, x = some a f a = b := by
cases x <;> simp
@[deprecated map_eq_some_iff (since := "2025-04-10")]
abbrev map_eq_some := @map_eq_some_iff
@[deprecated map_eq_some_iff (since := "2025-04-10")]
abbrev map_eq_some' := @map_eq_some_iff
@[simp] theorem map_eq_none_iff : x.map f = none x = none := by
cases x <;> simp [map_none, map_some]
@[deprecated map_eq_none_iff (since := "2025-04-10")]
abbrev map_eq_none := @map_eq_none_iff
@[deprecated map_eq_none_iff (since := "2025-04-10")]
abbrev map_eq_none' := @map_eq_none_iff
@[simp, grind =] theorem isSome_map {x : Option α} : (x.map f).isSome = x.isSome := by
cases x <;> simp
@[deprecated isSome_map (since := "2025-04-10")]
abbrev isSome_map' := @isSome_map
@[simp, grind =] theorem isNone_map {x : Option α} : (x.map f).isNone = x.isNone := by
cases x <;> simp
@@ -396,16 +353,10 @@ theorem isSome_of_isSome_filter (p : α → Bool) (o : Option α) (h : (o.filter
o.isSome := by
cases o <;> simp at h
@[deprecated isSome_of_isSome_filter (since := "2025-03-18")]
abbrev isSome_filter_of_isSome := @isSome_of_isSome_filter
@[simp] theorem filter_eq_none_iff {o : Option α} {p : α Bool} :
o.filter p = none a, o = some a ¬ p a := by
cases o <;> simp [filter_some]
@[deprecated filter_eq_none_iff (since := "2025-04-10")]
abbrev filter_eq_none := @filter_eq_none_iff
@[simp] theorem filter_eq_some_iff {o : Option α} {p : α Bool} :
o.filter p = some a o = some a p a := by
cases o with
@@ -420,9 +371,6 @@ abbrev filter_eq_none := @filter_eq_none_iff
rintro rfl
simpa using h
@[deprecated filter_eq_some_iff (since := "2025-04-10")]
abbrev filter_eq_some := @filter_eq_some_iff
theorem filter_some_eq_some : Option.filter p (some a) = some a p a := by simp
theorem filter_some_eq_none : Option.filter p (some a) = none ¬p a := by simp
@@ -610,15 +558,9 @@ theorem join_eq_get {x : Option (Option α)} {h} : x.join = x.get h := by
@[simp] theorem guard_eq_some_iff : guard p a = some b a = b p a :=
if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
@[deprecated guard_eq_some_iff (since := "2025-04-10")]
abbrev guard_eq_some := @guard_eq_some_iff
@[simp, grind =] theorem isSome_guard : (Option.guard p a).isSome = p a :=
if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
@[deprecated isSome_guard (since := "2025-03-18")]
abbrev guard_isSome := @isSome_guard
@[simp, grind =] theorem isNone_guard : (Option.guard p a).isNone = !p a := by
rw [ not_isSome, isSome_guard]
@@ -724,23 +666,6 @@ theorem merge_eq_or_eq {f : ααα} (h : ∀ a b, f a b = a f a b
@[simp, grind =] theorem merge_some_some {f} {a b : α} :
merge f (some a) (some b) = some (f a b) := rfl
@[deprecated merge_eq_or_eq (since := "2025-04-04")]
theorem liftOrGet_eq_or_eq {f : α α α} (h : a b, f a b = a f a b = b) :
o₁ o₂, merge f o₁ o₂ = o₁ merge f o₁ o₂ = o₂ :=
merge_eq_or_eq h
@[deprecated merge_none_left (since := "2025-04-04")]
theorem liftOrGet_none_left {f} {b : Option α} : merge f none b = b :=
merge_none_left
@[deprecated merge_none_right (since := "2025-04-04")]
theorem liftOrGet_none_right {f} {a : Option α} : merge f a none = a :=
merge_none_right
@[deprecated merge_some_some (since := "2025-04-04")]
theorem liftOrGet_some_some {f} {a b : α} : merge f (some a) (some b) = some (f a b) :=
merge_some_some
instance commutative_merge (f : α α α) [Std.Commutative f] :
Std.Commutative (merge f) :=
fun a b by cases a <;> cases b <;> simp [merge, Std.Commutative.comm]
@@ -861,9 +786,6 @@ grind_pattern isSome_choice_iff_nonempty => (choice α).isSome
theorem isSome_choice [Nonempty α] : (choice α).isSome :=
isSome_choice_iff_nonempty.2 inferInstance
@[deprecated isSome_choice_iff_nonempty (since := "2025-03-18")]
abbrev choice_isSome_iff_nonempty := @isSome_choice_iff_nonempty
@[simp]
theorem isNone_choice_eq_false [Nonempty α] : (choice α).isNone = false := by
simp [ not_isSome]
@@ -915,15 +837,9 @@ theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
@[simp] theorem or_eq_none_iff : or o o' = none o = none o' = none := by
cases o <;> simp
@[deprecated or_eq_none_iff (since := "2025-04-10")]
abbrev or_eq_none := @or_eq_none_iff
@[simp] theorem or_eq_some_iff : or o o' = some a o = some a (o = none o' = some a) := by
cases o <;> simp
@[deprecated or_eq_some_iff (since := "2025-04-10")]
abbrev or_eq_some := @or_eq_some_iff
@[grind _=_] theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
cases o₁ <;> cases o₂ <;> rfl
instance : Std.Associative (or (α := α)) := @or_assoc _
@@ -943,9 +859,6 @@ instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩
@[grind _=_] theorem map_or : (or o o').map f = (o.map f).or (o'.map f) := by
cases o <;> rfl
@[deprecated map_or (since := "2025-04-10")]
abbrev map_or' := @map_or
theorem or_of_isSome {o o' : Option α} (h : o.isSome) : o.or o' = o := by
match o, h with
| some _, _ => simp
@@ -1227,11 +1140,6 @@ theorem isNone_pbind_iff {o : Option α} {f : (a : α) → o = some a → Option
(o.pbind f).isNone o = none a h, f a h = none := by
cases o <;> simp
@[deprecated "isSome_pbind_iff" (since := "2025-04-01")]
theorem pbind_isSome {o : Option α} {f : (a : α) o = some a Option β} :
(o.pbind f).isSome = a h, (f a h).isSome := by
exact propext isSome_pbind_iff
theorem pbind_eq_some_iff {o : Option α} {f : (a : α) o = some a Option β} {b : β} :
o.pbind f = some b a h, f a h = some b := by
cases o <;> simp
@@ -1281,8 +1189,6 @@ theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h
(pmap f o h).isNone = o.isNone := by
cases o <;> simp
@[deprecated isSome_pmap (since := "2025-04-01")] abbrev pmap_isSome := @isSome_pmap
@[simp] theorem pmap_eq_some_iff {p : α Prop} {f : (a : α), p a β} {o : Option α} {h} :
pmap f o h = some b (a : α) (h : p a), o = some a b = f a h := by
cases o with

View File

@@ -1011,7 +1011,6 @@ theorem intCast_neg_iff {a : Int} :
/--
Alternative statement of `ofScientific_def`.
-/
@[grind =]
theorem ofScientific_def' :
(OfScientific.ofScientific m s e : Rat) = m * (10 ^ (if s then -e else e : Int)) := by
change Rat.ofScientific _ _ _ = _
@@ -1023,6 +1022,13 @@ theorem ofScientific_def' :
· push_cast
rfl
theorem ofScientific_def_eq_if :
(OfScientific.ofScientific m s e : Rat) = if s then (m : Rat) / (10 : Rat) ^ e else (m : Rat) * (10 : Rat) ^ e := by
simp [ofScientific_def']
split
next => rw [Rat.zpow_neg, Rat.div_def, Rat.zpow_natCast]
next => rw [Rat.zpow_natCast]
/-!
# min and max
-/

View File

@@ -59,28 +59,6 @@ declare_int_theorems Int32 32
declare_int_theorems Int64 64
declare_int_theorems ISize System.Platform.numBits
@[deprecated Int8.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem Int8.le_def {a b : Int8} : a b a.toBitVec.sle b.toBitVec := Iff.rfl
@[deprecated Int16.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem Int16.le_def {a b : Int16} : a b a.toBitVec.sle b.toBitVec := Iff.rfl
@[deprecated Int32.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem Int32.le_def {a b : Int32} : a b a.toBitVec.sle b.toBitVec := Iff.rfl
@[deprecated Int64.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem Int64.le_def {a b : Int64} : a b a.toBitVec.sle b.toBitVec := Iff.rfl
@[deprecated ISize.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem ISize.le_def {a b : ISize} : a b a.toBitVec.sle b.toBitVec := Iff.rfl
@[deprecated Int8.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem Int8.lt_def {a b : Int8} : a < b a.toBitVec.slt b.toBitVec := Iff.rfl
@[deprecated Int16.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem Int16.lt_def {a b : Int16} : a < b a.toBitVec.slt b.toBitVec := Iff.rfl
@[deprecated Int32.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem Int32.lt_def {a b : Int32} : a < b a.toBitVec.slt b.toBitVec := Iff.rfl
@[deprecated Int64.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem Int64.lt_def {a b : Int64} : a < b a.toBitVec.slt b.toBitVec := Iff.rfl
@[deprecated ISize.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem ISize.lt_def {a b : ISize} : a < b a.toBitVec.slt b.toBitVec := Iff.rfl
theorem Int8.toInt.inj {x y : Int8} (h : x.toInt = y.toInt) : x = y := Int8.toBitVec.inj (BitVec.eq_of_toInt_eq h)
theorem Int8.toInt_inj {x y : Int8} : x.toInt = y.toInt x = y := Int8.toInt.inj, fun h => h rfl
theorem Int16.toInt.inj {x y : Int16} (h : x.toInt = y.toInt) : x = y := Int16.toBitVec.inj (BitVec.eq_of_toInt_eq h)

View File

@@ -21,3 +21,4 @@ public import Init.Data.String.PosRaw
public import Init.Data.String.Substring
public import Init.Data.String.TakeDrop
public import Init.Data.String.Modify
public import Init.Data.String.Termination

View File

@@ -468,6 +468,7 @@ theorem Pos.Raw.isValid_iff_exists_append {s : String} {p : Pos.Raw} :
· rintro s₁, s₂, rfl, rfl
refine isValid_iff_isValidUTF8_extract_zero.2 by simp [Pos.Raw.le_iff], ?_
simpa [ByteArray.extract_append_eq_left] using s₁.isValidUTF8
theorem Pos.Raw.isValid_asString {l : List Char} {p : Pos.Raw} :
p.IsValid l.asString i, p.byteIdx = (l.take i).asString.utf8ByteSize := by
rw [isValid_iff_exists_append]
@@ -757,6 +758,10 @@ theorem Slice.utf8ByteSize_copy {s : Slice} :
theorem Slice.rawEndPos_copy {s : Slice} : s.copy.rawEndPos = s.rawEndPos := by
simp [Pos.Raw.ext_iff, utf8ByteSize_eq]
@[simp]
theorem copy_toSlice {s : String} : s.toSlice.copy = s := by
simp [ bytes_inj, Slice.bytes_copy, size_bytes]
theorem Slice.getUTF8Byte_eq_getUTF8Byte_copy {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} :
s.getUTF8Byte p h = s.copy.getUTF8Byte p (by simpa) := by
simp [getUTF8Byte, String.getUTF8Byte, bytes_copy, ByteArray.getElem_extract]
@@ -1056,19 +1061,6 @@ position. -/
def Slice.Pos.get! {s : Slice} (pos : s.Pos) : Char :=
if h : pos = s.endPos then panic! "Cannot retrieve character at end position" else pos.get h
@[simp]
theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startValidPos := rfl
@[simp]
theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endValidPos := rfl
@[simp]
theorem str_toSlice {s : String} : s.toSlice.str = s := rfl
@[simp]
theorem copy_toSlice {s : String} : s.toSlice.copy = s := by
simp [ bytes_inj, Slice.bytes_copy, size_bytes]
@[simp]
theorem Pos.Raw.isValidForSlice_toSlice_iff {s : String} {p : Pos.Raw} :
p.IsValidForSlice s.toSlice p.IsValid s := by
@@ -1121,6 +1113,38 @@ theorem ValidPos.ofSlice_toSlice {s : String} (pos : s.ValidPos) : pos.toSlice.o
theorem Slice.Pos.toSlice_ofSlice {s : String} (pos : s.toSlice.Pos) : pos.ofSlice.toSlice = pos :=
Slice.Pos.ext (by simp)
@[simp]
theorem Slice.Pos.toSlice_comp_ofSlice {s : String} :
ValidPos.toSlice (ofSlice (s := s)) = id := by ext; simp
@[simp]
theorem ValidPos.ofSlice_comp_toSlice {s : String} :
Slice.Pos.ofSlice (toSlice (s := s)) = id := by ext; simp
theorem ValidPos.toSlice_inj {s : String} {p q : s.ValidPos} : p.toSlice = q.toSlice p = q :=
fun h => by simpa using congrArg Slice.Pos.ofSlice h, (· rfl)
theorem Slice.Pos.ofSlice_inj {s : String} {p q : s.toSlice.Pos} : p.ofSlice = q.ofSlice p = q :=
fun h => by simpa using congrArg ValidPos.toSlice h, (· rfl)
@[simp]
theorem ValidPos.toSlice_le {s : String} {p q : s.ValidPos} : p.toSlice q.toSlice p q := by
simp [le_iff, Slice.Pos.le_iff]
@[simp]
theorem Slice.Pos.ofSlice_le {s : String} {p q : s.toSlice.Pos} :
p.ofSlice q.ofSlice p q := by
simp [ValidPos.le_iff, le_iff]
@[simp]
theorem ValidPos.toSlice_lt {s : String} {p q : s.ValidPos} : p.toSlice < q.toSlice p < q := by
simp [lt_iff, Slice.Pos.lt_iff]
@[simp]
theorem Slice.Pos.ofSlice_lt {s : String} {p q : s.toSlice.Pos} :
p.ofSlice < q.ofSlice p < q := by
simp [ValidPos.lt_iff, lt_iff]
/--
Returns the character at the position `pos` of a string, taking a proof that `p` is not the
past-the-end position.
@@ -1548,6 +1572,10 @@ theorem ValidPos.offset_cast {s t : String} {pos : s.ValidPos} {h : s = t} :
theorem ValidPos.cast_rfl {s : String} {pos : s.ValidPos} : pos.cast rfl = pos :=
ValidPos.ext (by simp)
theorem ValidPos.toCopy_toSlice_eq_cast {s : String} (p : s.ValidPos) :
p.toSlice.toCopy = p.cast copy_toSlice.symm :=
ValidPos.ext (by simp)
/-- Given a byte position within a string slice, obtains the smallest valid position that is
strictly greater than the given byte position. -/
@[inline]
@@ -1613,6 +1641,10 @@ theorem Slice.Pos.prev_ne_endPos {s : Slice} {p : s.Pos} {h} : p.prev h ≠ s.en
theorem ValidPos.prev_ne_endValidPos {s : String} {p : s.ValidPos} {h} : p.prev h s.endValidPos :=
mt (congrArg (·.toSlice)) (Slice.Pos.prev_ne_endPos (h := mt (congrArg (·.ofSlice)) h))
theorem ValidPos.toSlice_prev {s : String} {p : s.ValidPos} {h} :
(p.prev h).toSlice = p.toSlice.prev (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)) := by
simp [prev]
theorem Slice.Pos.offset_prev_lt_offset {s : Slice} {p : s.Pos} {h} : (p.prev h).offset < p.offset := by
simpa [prev] using prevAux_lt_self
@@ -1620,6 +1652,10 @@ theorem Slice.Pos.offset_prev_lt_offset {s : Slice} {p : s.Pos} {h} : (p.prev h)
theorem Slice.Pos.prev_lt {s : Slice} {p : s.Pos} {h} : p.prev h < p :=
lt_iff.2 offset_prev_lt_offset
@[simp]
theorem ValidPos.prev_lt {s : String} {p : s.ValidPos} {h} : p.prev h < p := by
simp [ toSlice_lt, toSlice_prev]
/-- Advances the position `p` `n` times, saturating at `s.endPos` if necessary. -/
def Slice.Pos.nextn {s : Slice} (p : s.Pos) (n : Nat) : s.Pos :=
match n with
@@ -1752,12 +1788,20 @@ theorem ValidPos.byteIdx_offset_next {s : String} (p : s.ValidPos) (h : p ≠ s.
(p.next h).offset.byteIdx = p.offset.byteIdx + (p.get h).utf8Size := by
simp
theorem ValidPos.toSlice_next {s : String} {p : s.ValidPos} {h} :
(p.next h).toSlice = p.toSlice.next (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)) := by
simp [next]
theorem ValidPos.byteIdx_lt_utf8ByteSize {s : String} (p : s.ValidPos) (h : p s.endValidPos) :
p.offset.byteIdx < s.utf8ByteSize := by
have := byteIdx_rawEndPos Pos.Raw.le_iff.1 p.isValid.le_rawEndPos
simp only [ne_eq, ValidPos.ext_iff, offset_endValidPos, Pos.Raw.ext_iff, byteIdx_rawEndPos] at h
omega
@[simp]
theorem ValidPos.lt_next {s : String} (p : s.ValidPos) {h} : p < p.next h := by
simp [ ValidPos.toSlice_lt, toSlice_next]
@[simp]
theorem ValidPos.str_toSlice {s : String} {p : s.ValidPos} : p.toSlice.str = p := by
ext
@@ -1781,6 +1825,11 @@ theorem endExclusive_replaceEnd {s : String} {p : s.ValidPos} :
(s.replaceEnd p).endExclusive = p := by
simp [replaceEnd]
@[simp]
theorem rawEndPos_replaceEnd {s : String} {p : s.ValidPos} :
(s.replaceEnd p).rawEndPos = p.offset := by
simp [replaceEnd]
theorem Pos.Raw.isValidForSlice_stringReplaceEnd {s : String} {p : s.ValidPos} {q : Pos.Raw} :
q.IsValidForSlice (s.replaceEnd p) q p.offset q.IsValid s := by
rw [replaceEnd, isValidForSlice_replaceEnd, ValidPos.offset_toSlice, isValidForSlice_toSlice_iff]

View File

@@ -312,6 +312,11 @@ theorem Pos.Raw.isValid_rawEndPos {s : String} : s.rawEndPos.IsValid s where
le_rawEndPos := by simp
isValidUTF8_extract_zero := by simp [ size_bytes, s.isValidUTF8]
theorem Pos.Raw.isValid_of_eq_rawEndPos {s : String} {p : Pos.Raw} (h : p = s.rawEndPos) :
p.IsValid s := by
subst h
exact isValid_rawEndPos
@[simp]
theorem Pos.Raw.isValid_empty_iff {p : Pos.Raw} : p.IsValid "" p = 0 := by
refine ?_, ?_
@@ -406,6 +411,15 @@ def toSlice (s : String) : Slice where
endExclusive := s.endValidPos
startInclusive_le_endExclusive := by simp [ValidPos.le_iff, Pos.Raw.le_iff]
@[simp]
theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startValidPos := rfl
@[simp]
theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endValidPos := rfl
@[simp]
theorem str_toSlice {s : String} : s.toSlice.str = s := rfl
/-- The number of bytes of the UTF-8 encoding of the string slice. -/
@[expose]
def Slice.utf8ByteSize (s : Slice) : Nat :=
@@ -526,11 +540,20 @@ theorem Pos.Raw.offsetBy_sliceRawEndPos_right {p : Pos.Raw} {s : Slice} :
p.offsetBy s.rawEndPos = s + p := by
simp [Pos.Raw.ext_iff]
@[simp]
theorem Pos.Raw.isValidForSlice_rawEndPos {s : Slice} : (s.rawEndPos).IsValidForSlice s where
le_rawEndPos := by simp
isValid_offsetBy := by simpa using s.endExclusive.isValid
theorem Pos.Raw.isValidForSlice_of_eq_rawEndPos {p : Pos.Raw} {s : Slice} (h : p = s.rawEndPos) :
p.IsValidForSlice s := by
subst h; simp
/-- The past-the-end position of `s`, as an `s.Pos`. -/
@[inline, expose]
def Slice.endPos (s : Slice) : s.Pos where
offset := s.rawEndPos
isValidForSlice := by simp, by simpa using s.endExclusive.isValid
isValidForSlice := Pos.Raw.isValidForSlice_rawEndPos
@[simp]
theorem Slice.offset_endPos {s : Slice} : s.endPos.offset = s.rawEndPos := (rfl)

View File

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
module
prelude
public import Init.Data.String.Lemmas.Splits
public import Init.Data.Char.Order
public import Init.Data.Char.Lemmas
public import Init.Data.List.Lex

View File

@@ -0,0 +1,92 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Markus Himmel
-/
module
prelude
public import Init.Data.String.Basic
import Init.Data.ByteArray.Lemmas
/-!
# `Splits` predicates on `String.ValidPos` and `String.Slice.Pos`.
We introduce the predicate `p.Splits t₁ t₂` for a position `p` on a string or slice `s`, which means
that `s = t₁ ++ t₂` with `p` lying between the two parts. This is a useful primitive when verifying
string operations.
-/
public section
namespace String
/--
We say that `p` splits `s` into `t₁` and `t₂` if `s = t₁ ++ t₂` and `p` is the position between `t₁`
and `t₂`.
-/
structure ValidPos.Splits {s : String} (p : s.ValidPos) (t₁ t₂ : String) : Prop where
eq_append : s = t₁ ++ t₂
offset_eq_rawEndPos : p.offset = t₁.rawEndPos
/--
We say that `p` splits `s` into `t₁` and `t₂` if `s = t₁ ++ t₂` and `p` is the position between `t₁`
and `t₂`.
-/
structure Slice.Pos.Splits {s : Slice} (p : s.Pos) (t₁ t₂ : String) : Prop where
eq_append : s.copy = t₁ ++ t₂
offset_eq_rawEndPos : p.offset = t₁.rawEndPos
@[simp]
theorem ValidPos.splits_cast_iff {s₁ s₂ : String} {h : s₁ = s₂} {p : s₁.ValidPos} {t₁ t₂ : String} :
(p.cast h).Splits t₁ t₂ p.Splits t₁ t₂ := by
subst h; simp
theorem ValidPos.Splits.cast {s₁ s₂ : String} {p : s₁.ValidPos} {t₁ t₂ : String} (h : s₁ = s₂) :
p.Splits t₁ t₂ (p.cast h).Splits t₁ t₂ :=
splits_cast_iff.mpr
@[simp]
theorem Slice.Pos.splits_cast_iff {s₁ s₂ : Slice} {h : s₁ = s₂} {p : s₁.Pos} {t₁ t₂ : String} :
(p.cast h).Splits t₁ t₂ p.Splits t₁ t₂ := by
subst h; simp
theorem Slice.Pos.Splits.cast {s₁ s₂ : Slice} {p : s₁.Pos} {t₁ t₂ : String} (h : s₁ = s₂) :
p.Splits t₁ t₂ (p.cast h).Splits t₁ t₂ :=
splits_cast_iff.mpr
theorem Slice.Pos.Splits.toCopy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
(h : p.Splits t₁ t₂) : p.toCopy.Splits t₁ t₂ where
eq_append := h.eq_append
offset_eq_rawEndPos := by simpa using h.offset_eq_rawEndPos
theorem Slice.Pos.splits_of_splits_toCopy {s : Slice} {p : s.Pos} {t₁ t₂ : String}
(h : p.toCopy.Splits t₁ t₂) : p.Splits t₁ t₂ where
eq_append := h.eq_append
offset_eq_rawEndPos := by simpa using h.offset_eq_rawEndPos
@[simp]
theorem Slice.Pos.splits_toCopy_iff {s : Slice} {p : s.Pos} {t₁ t₂ : String} :
p.toCopy.Splits t₁ t₂ p.Splits t₁ t₂ :=
splits_of_splits_toCopy, (·.toCopy)
@[simp]
theorem ValidPos.splits_toSlice_iff {s : String} {p : s.ValidPos} {t₁ t₂ : String} :
p.toSlice.Splits t₁ t₂ p.Splits t₁ t₂ := by
rw [ Slice.Pos.splits_toCopy_iff, p.toCopy_toSlice_eq_cast, splits_cast_iff]
theorem ValidPos.Splits.toSlice {s : String} {p : s.ValidPos} {t₁ t₂ : String}
(h : p.Splits t₁ t₂) : p.toSlice.Splits t₁ t₂ :=
splits_toSlice_iff.mpr h
theorem ValidPos.splits {s : String} (p : s.ValidPos) :
p.Splits (s.replaceEnd p).copy (s.replaceStart p).copy where
eq_append := by simp [ bytes_inj, Slice.bytes_copy, size_bytes]
offset_eq_rawEndPos := by simp
theorem Slice.Pos.splits {s : Slice} (p : s.Pos) :
p.Splits (s.replaceEnd p).copy (s.replaceStart p).copy where
eq_append := copy_eq_copy_replaceEnd
offset_eq_rawEndPos := by simp
end String

View File

@@ -7,6 +7,7 @@ module
prelude
public import Init.Data.String.Basic
public import Init.Data.String.Termination
import Init.Data.ByteArray.Lemmas
import Init.Data.Char.Lemmas
@@ -70,6 +71,34 @@ def ValidPos.toSetOfLE {s : String} (q p : s.ValidPos) (c : Char) (hp : p ≠ s.
theorem ValidPos.offset_toSetOfLE {s : String} {q p : s.ValidPos} {c : Char} {hp : p s.endValidPos}
{hpq : q p} : (q.toSetOfLE p c hp hpq).offset = q.offset := (rfl)
theorem Pos.Raw.isValid_add_char_set {s : String} {p : s.ValidPos} {c : Char} {hp} :
(p.offset + c).IsValid (p.set c hp) :=
ValidPos.set_eq_append IsValid.append_right (isValid_of_eq_rawEndPos (by simp [Pos.Raw.ext_iff])) _
/-- The position just after the position that changed in a `ValidPos.set` call. -/
@[inline]
def ValidPos.pastSet {s : String} (p : s.ValidPos) (c : Char) (hp) : (p.set c hp).ValidPos where
offset := p.offset + c
isValid := Pos.Raw.isValid_add_char_set
@[simp]
theorem ValidPos.offset_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
(p.pastSet c hp).offset = p.offset + c := (rfl)
@[inline]
def ValidPos.appendRight {s : String} (p : s.ValidPos) (t : String) : (s ++ t).ValidPos where
offset := p.offset
isValid := p.isValid.append_right t
theorem ValidPos.splits_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
(p.pastSet c hp).Splits ((s.replaceEnd p).copy ++ singleton c) (s.replaceStart (p.next hp)).copy where
eq_append := set_eq_append
offset_eq_rawEndPos := by simp [Pos.Raw.ext_iff]
theorem remainingBytes_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
(p.pastSet c hp).remainingBytes = (p.next hp).remainingBytes := by
rw [(p.next hp).splits.remainingBytes_eq, p.splits_pastSet.remainingBytes_eq]
/--
Replaces the character at position `p` in the string `s` with the result of applying `f` to that
character.
@@ -80,6 +109,7 @@ string is not shared, then it is updated in-place and not copied.
Examples:
* `("abc".pos ⟨1⟩ (by decide)).modify Char.toUpper (by decide) = "aBc"`
-/
@[inline]
def ValidPos.modify {s : String} (p : s.ValidPos) (f : Char Char) (hp : p s.endValidPos) :
String :=
p.set (f <| p.get hp) hp
@@ -91,6 +121,7 @@ theorem Pos.Raw.IsValid.modify_of_le {s : String} {p : s.ValidPos} {f : Char →
/-- Given a valid position in a string, obtain the corresponding position after modifying a character
in that string, provided that the position was before the changed position. -/
@[inline]
def ValidPos.toModifyOfLE {s : String} (q p : s.ValidPos) (f : Char Char)
(hp : p s.endValidPos) (hpq : q p) : (p.modify f hp).ValidPos where
offset := q.offset
@@ -100,6 +131,16 @@ def ValidPos.toModifyOfLE {s : String} (q p : s.ValidPos) (f : Char → Char)
theorem ValidPos.offset_toModifyOfLE {s : String} {q p : s.ValidPos} {f : Char Char}
{hp : p s.endValidPos} {hpq : q p} : (q.toModifyOfLE p f hp hpq).offset = q.offset := (rfl)
/-- The position just after the position that was modified in a `ValidPos.modify` call. -/
@[inline]
def ValidPos.pastModify {s : String} (p : s.ValidPos) (f : Char Char)
(hp : p s.endValidPos) : (p.modify f hp).ValidPos :=
p.pastSet _ _
theorem remainingBytes_pastModify {s : String} {p : s.ValidPos} {f : Char Char} {hp} :
(p.pastModify f hp).remainingBytes = (p.next hp).remainingBytes :=
remainingBytes_pastSet
/--
Replaces the character at a specified position in a string with a new character. If the position is
invalid, the string is returned unchanged.
@@ -147,66 +188,14 @@ def Pos.Raw.modify (s : String) (i : Pos.Raw) (f : Char → Char) : String :=
def modify (s : String) (i : Pos.Raw) (f : Char Char) : String :=
i.set s (f (i.get s))
-- This is just to keep the proof of `set_next_add` below from breaking; if that lemma goes away
-- or the proof is rewritten, it can be removed.
private noncomputable def utf8ByteSize' : String Nat
| s => go s.data
where
go : List Char Nat
| [] => 0
| c::cs => go cs + c.utf8Size
private theorem utf8ByteSize'_eq (s : String) : s.utf8ByteSize' = s.utf8ByteSize := by
suffices l, utf8ByteSize'.go l = l.asString.utf8ByteSize by
obtain m, rfl := s.exists_eq_asString
rw [utf8ByteSize', this, asString_data]
intro l
induction l with
| nil => simp [utf8ByteSize'.go]
| cons c cs ih =>
rw [utf8ByteSize'.go, ih, List.singleton_append, List.asString_append,
utf8ByteSize_append, Nat.add_comm]
congr
rw [ size_bytes, List.bytes_asString, List.utf8Encode_singleton,
List.size_toByteArray, length_utf8EncodeChar]
theorem set_next_add (s : String) (i : Pos.Raw) (c : Char) (b₁ b₂)
(h : (i.next s).1 + b₁ = s.rawEndPos.1 + b₂) :
(i.next (i.set s c)).1 + b₁ = (i.set s c).rawEndPos.1 + b₂ := by
simp [Pos.Raw.next, Pos.Raw.get, Pos.Raw.set, rawEndPos, utf8ByteSize'_eq, utf8ByteSize'] at h
rw [Nat.add_comm i.1, Nat.add_assoc] at h
let rec foo : cs a b₁ b₂,
(Pos.Raw.utf8GetAux cs a i).utf8Size + b₁ = utf8ByteSize'.go cs + b₂
(Pos.Raw.utf8GetAux (Pos.Raw.utf8SetAux c cs a i) a i).utf8Size + b₁ = utf8ByteSize'.go (Pos.Raw.utf8SetAux c cs a i) + b₂
| [], _, _, _, h => h
| c'::cs, a, b₁, b₂, h => by
unfold Pos.Raw.utf8SetAux
apply iteInduction (motive := fun p => (Pos.Raw.utf8GetAux p a i).utf8Size + b₁ = utf8ByteSize'.go p + b₂) <;>
intro h' <;> simp [Pos.Raw.utf8GetAux, h', utf8ByteSize'.go] at h
next =>
rw [Nat.add_assoc, Nat.add_left_comm] at h ; rw [Nat.add_left_cancel h]
next =>
rw [Nat.add_assoc] at h
refine foo cs (a + c') b₁ (c'.utf8Size + b₂) h
exact foo s.data 0 _ _ h
theorem mapAux_lemma (s : String) (i : Pos.Raw) (c : Char) (h : ¬i.atEnd s) :
(i.set s c).rawEndPos.1 - (i.next (i.set s c)).1 < s.rawEndPos.1 - i.1 := by
suffices (i.set s c).rawEndPos.1 - (i.next (i.set s c)).1 = s.rawEndPos.1 - (i.next s).1 by
rw [this]
apply Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (Pos.Raw.lt_next ..)
have := set_next_add s i c (s.rawEndPos.byteIdx - (i.next s).byteIdx) 0
have := set_next_add s i c 0 ((i.next s).byteIdx - s.rawEndPos.byteIdx)
omega
@[specialize] def mapAux (f : Char Char) (i : Pos.Raw) (s : String) : String :=
if h : i.atEnd s then s
@[specialize] def mapAux (f : Char Char) (s : String) (p : s.ValidPos) : String :=
if h : p = s.endValidPos then
s
else
let c := f (i.get s)
have := mapAux_lemma s i c h
let s := i.set s c
mapAux f (i.next s) s
termination_by s.rawEndPos.1 - i.1
mapAux f (p.modify f h) (p.pastModify f h)
termination_by p.remainingBytes
decreasing_by
simp [remainingBytes_pastModify, ValidPos.lt_iff_remainingBytes_lt]
/--
Applies the function `f` to every character in a string, returning a string that contains the
@@ -217,7 +206,7 @@ Examples:
* `"".map Char.toUpper = ""`
-/
@[inline] def map (f : Char Char) (s : String) : String :=
mapAux f 0 s
mapAux f s s.startValidPos
/--
In the string `s`, replaces all occurrences of `pattern` with `replacement`.

View File

@@ -38,7 +38,7 @@ inductive SearchStep (s : Slice) where
The subslice starting at {name}`startPos` and ending at {name}`endPos` matches the pattern.
-/
| matched (startPos endPos : s.Pos)
deriving Inhabited
deriving Inhabited, BEq
/--
Provides a conversion from a pattern to an iterator of {name}`SearchStep` that searches for matches

View File

@@ -9,6 +9,7 @@ prelude
public import Init.Data.String.Pattern.Basic
public import Init.Data.Iterators.Internal.Termination
public import Init.Data.Iterators.Consumers.Monadic.Loop
import Init.Data.String.Termination
set_option doc.verso true
@@ -60,8 +61,7 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardCharSearcher s) Id (Search
pure (.deflate .yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextIt, nextPos])
def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s) Id where
rel := InvImage WellFoundedRelation.rel
(fun it => s.utf8ByteSize - it.internalState.currPos.offset.byteIdx)
rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp_wf
@@ -69,10 +69,7 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s
cases step
· cases h
obtain _, h1, h2, _ := h'
have h3 := Char.utf8Size_pos (it.internalState.currPos.get h1)
have h4 := it.internalState.currPos.isValidForSlice.le_utf8ByteSize
simp [Pos.ext_iff, String.Pos.Raw.ext_iff] at h1 h2 h4
omega
simp [h2]
· cases h'
· cases h
@@ -129,8 +126,7 @@ instance (s : Slice) : Std.Iterators.Iterator (BackwardCharSearcher s) Id (Searc
pure (.deflate .yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos])
def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharSearcher s) Id where
rel := InvImage WellFoundedRelation.rel
(fun it => it.internalState.currPos.offset.byteIdx)
rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos.down)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp_wf
@@ -138,9 +134,7 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharSearcher
cases step
· cases h
obtain _, h1, h2, _ := h'
have h3 := Pos.offset_prev_lt_offset (h := h1)
simp [Pos.ext_iff, String.Pos.Raw.ext_iff, String.Pos.Raw.lt_iff] at h2 h3
omega
simp [h2]
· cases h'
· cases h

View File

@@ -9,6 +9,7 @@ prelude
public import Init.Data.String.Pattern.Basic
public import Init.Data.Iterators.Internal.Termination
public import Init.Data.Iterators.Consumers.Monadic.Loop
import Init.Data.String.Termination
set_option doc.verso true
@@ -62,8 +63,7 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardCharPredSearcher s) Id (Se
def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher s) Id where
rel := InvImage WellFoundedRelation.rel
(fun it => s.utf8ByteSize - it.internalState.currPos.offset.byteIdx)
rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
wf := InvImage.wf _ WellFoundedRelation.wf
subrelation {it it'} h := by
simp_wf
@@ -71,10 +71,7 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearch
cases step
· cases h
obtain _, h1, h2, _ := h'
have h3 := Char.utf8Size_pos (it.internalState.currPos.get h1)
have h4 := it.internalState.currPos.isValidForSlice.le_utf8ByteSize
simp [Pos.ext_iff, String.Pos.Raw.ext_iff] at h1 h2 h4
omega
simp [h2]
· cases h'
· cases h

View File

@@ -9,6 +9,7 @@ prelude
public import Init.Data.String.Pattern.Basic
public import Init.Data.Iterators.Internal.Termination
public import Init.Data.Iterators.Consumers.Monadic.Loop
import Init.Data.String.Termination
set_option doc.verso true
@@ -22,7 +23,8 @@ public section
namespace String.Slice.Pattern
inductive ForwardSliceSearcher (s : Slice) where
| empty (pos : s.Pos)
| emptyBefore (pos : s.Pos)
| emptyAt (pos : s.Pos) (h : pos s.endPos)
| proper (needle : Slice) (table : Array String.Pos.Raw) (stackPos : String.Pos.Raw) (needlePos : String.Pos.Raw)
| atEnd
deriving Inhabited
@@ -56,7 +58,7 @@ where
@[inline]
def iter (s : Slice) (pat : Slice) : Std.Iter (α := ForwardSliceSearcher s) (SearchStep s) :=
if pat.utf8ByteSize == 0 then
{ internalState := .empty s.startPos }
{ internalState := .emptyBefore s.startPos }
else
{ internalState := .proper pat (buildTable pat) s.startPos.offset pat.startPos.offset }
@@ -71,9 +73,8 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
IsPlausibleStep it
| .yield it' out =>
match it.internalState with
| .empty pos =>
( newPos, pos < newPos it'.internalState = .empty newPos)
it'.internalState = .atEnd
| .emptyBefore pos => ( h, it'.internalState = .emptyAt pos h) it'.internalState = .atEnd
| .emptyAt pos h => newPos, pos < newPos it'.internalState = .emptyBefore newPos
| .proper needle table stackPos needlePos =>
( newStackPos newNeedlePos,
stackPos < newStackPos
@@ -85,12 +86,15 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
| .done => True
step := fun iter =>
match iter with
| .empty pos =>
| .emptyBefore pos =>
let res := .matched pos pos
if h : pos s.endPos then
pure (.deflate .yield .empty (pos.next h) res, by simp)
pure (.deflate .yield .emptyAt pos h res, by simp [h])
else
pure (.deflate .yield .atEnd res, by simp)
| .emptyAt pos h =>
let res := .rejected pos (pos.next h)
pure (.deflate .yield .emptyBefore (pos.next h) res, by simp)
| .proper needle table stackPos needlePos =>
let rec findNext (startPos : String.Pos.Raw)
(currStackPos : String.Pos.Raw) (needlePos : String.Pos.Raw) (h : stackPos currStackPos) :=
@@ -148,15 +152,17 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
findNext stackPos stackPos needlePos (by simp)
| .atEnd => pure (.deflate .done, by simp)
private def toPair : ForwardSliceSearcher s (Nat × Nat)
| .empty pos => (1, s.utf8ByteSize - pos.offset.byteIdx)
| .proper _ _ sp _ => (1, s.utf8ByteSize - sp.byteIdx)
| .atEnd => (0, 0)
private def toOption : ForwardSliceSearcher s Option (Nat × Nat)
| .emptyBefore pos => some (pos.remainingBytes, 1)
| .emptyAt pos _ => some (pos.remainingBytes, 0)
| .proper _ _ sp _ => some (s.utf8ByteSize - sp.byteIdx, 0)
| .atEnd => none
private instance : WellFoundedRelation (ForwardSliceSearcher s) where
rel s1 s2 := Prod.Lex (· < ·) (· < ·) s1.toPair s2.toPair
rel := InvImage (Option.lt (Prod.Lex (· < ·) (· < ·))) ForwardSliceSearcher.toOption
wf := by
apply InvImage.wf
apply Option.wellFounded_lt
apply (Prod.lex _ _).wf
private def finitenessRelation :
@@ -168,30 +174,24 @@ private def finitenessRelation :
obtain step, h, h' := h
cases step
· cases h
simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
split at h'
· next heq =>
rw [heq]
rcases h' with np, h1', h2' | h'
· rw [h2']
apply Prod.Lex.right'
· simp
· have haux := np.isValidForSlice.le_utf8ByteSize
simp [Slice.Pos.lt_iff, String.Pos.Raw.lt_iff] at h1' haux
omega
· apply Prod.Lex.left
simp [h']
· next heq =>
rw [heq]
rcases h' with np, sp, h1', h2', h3' | h'
· rw [h3']
apply Prod.Lex.right'
· simp
· simp [String.Pos.Raw.le_iff, String.Pos.Raw.lt_iff] at h1' h2'
omega
· apply Prod.Lex.left
simp [h']
· contradiction
revert h'
simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep]
match it.internalState with
| .emptyBefore pos =>
rintro (h, h'|h') <;> simp [h', ForwardSliceSearcher.toOption, Option.lt, Prod.lex_def]
| .emptyAt pos h =>
simp only [forall_exists_index, and_imp]
intro x hx h
simpa [h, ForwardSliceSearcher.toOption, Option.lt, Prod.lex_def,
Pos.lt_iff_remainingBytes_lt]
| .proper needle table stackPos needlePos =>
simp only [exists_and_left]
rintro (newStackPos, h₁, h, x, hx|h)
· simp [hx, ForwardSliceSearcher.toOption, Option.lt, Prod.lex_def, Pos.Raw.lt_iff,
Pos.Raw.le_iff] at h₁ h₂
omega
· simp [h, ForwardSliceSearcher.toOption, Option.lt]
| .atEnd .. => simp
· cases h'
· cases h

View File

@@ -322,9 +322,6 @@ theorem ne_of_gt {i₁ i₂ : Pos.Raw} (h : i₁ < i₂) : i₂ ≠ i₁ := (ne_
theorem byteIdx_addString (p : Pos.Raw) (s : String) :
(p + s).byteIdx = p.byteIdx + s.utf8ByteSize := byteIdx_add_string
@[deprecated byteIdx_addString (since := "2025-03-18")]
abbrev addString_byteIdx := @byteIdx_add_string
theorem addString_eq (p : Pos.Raw) (s : String) : p + s = p.byteIdx + s.utf8ByteSize := rfl
theorem byteIdx_zero_add_string (s : String) : ((0 : Pos.Raw) + s).byteIdx = s.utf8ByteSize := by
@@ -334,9 +331,6 @@ theorem byteIdx_zero_add_string (s : String) : ((0 : Pos.Raw) + s).byteIdx = s.u
theorem byteIdx_zero_addString (s : String) : ((0 : Pos.Raw) + s).byteIdx = s.utf8ByteSize :=
byteIdx_zero_add_string s
@[deprecated byteIdx_zero_addString (since := "2025-03-18")]
abbrev zero_addString_byteIdx := @byteIdx_zero_add_string
theorem zero_add_string_eq (s : String) : (0 : Pos.Raw) + s = s.utf8ByteSize := by
rw [ byteIdx_zero_add_string]

View File

@@ -0,0 +1,257 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Markus Himmel
-/
module
prelude
public import Init.Data.String.Basic
public import Init.Data.String.Lemmas.Splits
/-!
# Helpers for termination arguments about functions operating on strings
-/
public section
namespace String
namespace Slice.Pos
/-- The number of bytes between `p` and the end position. This number decreases as `p` advances. -/
def remainingBytes {s : Slice} (p : s.Pos) : Nat :=
p.offset.byteDistance s.endPos.offset
theorem remainingBytes_eq_byteDistance {s : Slice} {p : s.Pos} :
p.remainingBytes = p.offset.byteDistance s.endPos.offset := (rfl)
theorem remainingBytes_eq {s : Slice} {p : s.Pos} :
p.remainingBytes = s.utf8ByteSize - p.offset.byteIdx := by
simp [remainingBytes_eq_byteDistance, Pos.Raw.byteDistance_eq]
theorem remainingBytes_inj {s : Slice} {p q : s.Pos} :
p.remainingBytes = q.remainingBytes p = q := by
have := p.isValidForSlice.le_utf8ByteSize
have := q.isValidForSlice.le_utf8ByteSize
simp only [remainingBytes_eq, Pos.ext_iff, Pos.Raw.ext_iff]
omega
theorem le_iff_remainingBytes_le {s : Slice} (p q : s.Pos) :
p q q.remainingBytes p.remainingBytes := by
have := p.isValidForSlice.le_utf8ByteSize
have := q.isValidForSlice.le_utf8ByteSize
simp only [remainingBytes_eq, Slice.Pos.le_iff, Pos.Raw.le_iff]
omega
theorem lt_iff_remainingBytes_lt {s : Slice} (p q : s.Pos) :
p < q q.remainingBytes < p.remainingBytes := by
have := p.isValidForSlice.le_utf8ByteSize
have := q.isValidForSlice.le_utf8ByteSize
simp only [remainingBytes_eq, Slice.Pos.lt_iff, Pos.Raw.lt_iff]
omega
theorem wellFounded_lt {s : Slice} : WellFounded (fun (p : s.Pos) q => p < q) := by
simpa [lt_iff, Pos.Raw.lt_iff] using
InvImage.wf (Pos.Raw.byteIdx Slice.Pos.offset) Nat.lt_wfRel.wf
theorem wellFounded_gt {s : Slice} : WellFounded (fun (p : s.Pos) q => q < p) := by
simpa [lt_iff_remainingBytes_lt] using
InvImage.wf Slice.Pos.remainingBytes Nat.lt_wfRel.wf
instance {s : Slice} : WellFoundedRelation s.Pos where
rel p q := q < p
wf := Slice.Pos.wellFounded_gt
/-- Type alias for `String.Slice.Pos` representing that the given position is expected to decrease
in recursive calls. -/
structure Down (s : Slice) : Type where
inner : s.Pos
/-- Use `termination_by pos.down` to signify that in a recursive call, the parameter `pos` is
expected to decrease. -/
def down {s : Slice} (p : s.Pos) : Pos.Down s where
inner := p
@[simp]
theorem inner_down {s : Slice} {p : s.Pos} : p.down.inner = p := (rfl)
instance {s : Slice} : WellFoundedRelation (Pos.Down s) where
rel p q := p.inner < q.inner
wf := InvImage.wf Down.inner wellFounded_lt
theorem ne_endPos_of_next?_eq_some {s : Slice} {p q : s.Pos} :
p.next? = some q p s.endPos := by
simpa [next?] using fun h _ => h
theorem eq_next_of_next?_eq_some {s : Slice} {p q : s.Pos} :
(h : p.next? = some q) q = p.next (ne_endPos_of_next?_eq_some h) := by
simpa [next?] using fun _ h => h.symm
theorem ne_startPos_of_prev?_eq_some {s : Slice} {p q : s.Pos} :
p.prev? = some q p s.startPos := by
simpa [prev?] using fun h _ => h
theorem eq_prev_of_prev?_eq_some {s : Slice} {p q : s.Pos} :
(h : p.prev? = some q) q = p.prev (ne_startPos_of_prev?_eq_some h) := by
simpa [prev?] using fun _ h => h.symm
@[simp]
theorem le_refl {s : Slice} (p : s.Pos) : p p := by
simp [le_iff]
theorem lt_trans {s : Slice} {p q r : s.Pos} : p < q q < r p < r := by
simpa [Pos.lt_iff, Pos.Raw.lt_iff] using Nat.lt_trans
@[simp]
theorem lt_next_next {s : Slice} {p : s.Pos} {h h'} : p < (p.next h).next h' :=
lt_trans p.lt_next (p.next h).lt_next
@[simp]
theorem prev_prev_lt {s : Slice} {p : s.Pos} {h h'} : (p.prev h).prev h' < p :=
lt_trans (p.prev h).prev_lt p.prev_lt
end Slice.Pos
namespace ValidPos
/-- The number of bytes between `p` and the end position. This number decreases as `p` advances. -/
def remainingBytes {s : String} (p : s.ValidPos) : Nat :=
p.toSlice.remainingBytes
@[simp]
theorem remainingBytes_toSlice {s : String} {p : s.ValidPos} :
p.toSlice.remainingBytes = p.remainingBytes := (rfl)
theorem remainingBytes_eq_byteDistance {s : String} {p : s.ValidPos} :
p.remainingBytes = p.offset.byteDistance s.endValidPos.offset := (rfl)
theorem remainingBytes_eq {s : String} {p : s.ValidPos} :
p.remainingBytes = s.utf8ByteSize - p.offset.byteIdx := by
simp [remainingBytes_eq_byteDistance, Pos.Raw.byteDistance_eq]
theorem remainingBytes_inj {s : String} {p q : s.ValidPos} :
p.remainingBytes = q.remainingBytes p = q := by
simp [ remainingBytes_toSlice, ValidPos.toSlice_inj, Slice.Pos.remainingBytes_inj]
theorem le_iff_remainingBytes_le {s : String} (p q : s.ValidPos) :
p q q.remainingBytes p.remainingBytes := by
simp [ remainingBytes_toSlice, Slice.Pos.le_iff_remainingBytes_le]
theorem lt_iff_remainingBytes_lt {s : String} (p q : s.ValidPos) :
p < q q.remainingBytes < p.remainingBytes := by
simp [ remainingBytes_toSlice, Slice.Pos.lt_iff_remainingBytes_lt]
theorem wellFounded_lt {s : String} : WellFounded (fun (p : s.ValidPos) q => p < q) := by
simpa [lt_iff, Pos.Raw.lt_iff] using
InvImage.wf (Pos.Raw.byteIdx ValidPos.offset) Nat.lt_wfRel.wf
theorem wellFounded_gt {s : String} : WellFounded (fun (p : s.ValidPos) q => q < p) := by
simpa [lt_iff_remainingBytes_lt] using
InvImage.wf ValidPos.remainingBytes Nat.lt_wfRel.wf
instance {s : String} : WellFoundedRelation s.ValidPos where
rel p q := q < p
wf := ValidPos.wellFounded_gt
/-- Type alias for `String.ValidPos` representing that the given position is expected to decrease
in recursive calls. -/
structure Down (s : String) : Type where
inner : s.ValidPos
/-- Use `termination_by pos.down` to signify that in a recursive call, the parameter `pos` is
expected to decrease. -/
def down {s : String} (p : s.ValidPos) : ValidPos.Down s where
inner := p
@[simp]
theorem inner_down {s : String} {p : s.ValidPos} : p.down.inner = p := (rfl)
instance {s : String} : WellFoundedRelation (ValidPos.Down s) where
rel p q := p.inner < q.inner
wf := InvImage.wf ValidPos.Down.inner ValidPos.wellFounded_lt
theorem map_toSlice_next? {s : String} {p : s.ValidPos} :
p.next?.map ValidPos.toSlice = p.toSlice.next? := by
simp [next?]
theorem map_toSlice_prev? {s : String} {p : s.ValidPos} :
p.prev?.map ValidPos.toSlice = p.toSlice.prev? := by
simp [prev?]
theorem ne_endValidPos_of_next?_eq_some {s : String} {p q : s.ValidPos}
(h : p.next? = some q) : p s.endValidPos :=
ne_of_apply_ne ValidPos.toSlice (Slice.Pos.ne_endPos_of_next?_eq_some
(by simpa only [ValidPos.map_toSlice_next?, Option.map_some] using congrArg (·.map toSlice) h))
theorem eq_next_of_next?_eq_some {s : String} {p q : s.ValidPos} (h : p.next? = some q) :
q = p.next (ne_endValidPos_of_next?_eq_some h) := by
simpa only [ toSlice_inj, toSlice_next] using Slice.Pos.eq_next_of_next?_eq_some
(by simpa [ValidPos.map_toSlice_next?] using congrArg (·.map toSlice) h)
theorem ne_startValidPos_of_prev?_eq_some {s : String} {p q : s.ValidPos}
(h : p.prev? = some q) : p s.startValidPos :=
ne_of_apply_ne ValidPos.toSlice (Slice.Pos.ne_startPos_of_prev?_eq_some
(by simpa only [ValidPos.map_toSlice_prev?, Option.map_some] using congrArg (·.map toSlice) h))
theorem eq_prev_of_prev?_eq_some {s : String} {p q : s.ValidPos} (h : p.prev? = some q) :
q = p.prev (ne_startValidPos_of_prev?_eq_some h) := by
simpa only [ toSlice_inj, toSlice_prev] using Slice.Pos.eq_prev_of_prev?_eq_some
(by simpa [ValidPos.map_toSlice_prev?] using congrArg (·.map toSlice) h)
@[simp]
theorem le_refl {s : String} (p : s.ValidPos) : p p := by
simp [ValidPos.le_iff]
theorem lt_trans {s : String} {p q r : s.ValidPos} : p < q q < r p < r := by
simpa [ValidPos.lt_iff, Pos.Raw.lt_iff] using Nat.lt_trans
@[simp]
theorem lt_next_next {s : String} {p : s.ValidPos} {h h'} : p < (p.next h).next h' :=
lt_trans p.lt_next (p.next h).lt_next
@[simp]
theorem prev_prev_lt {s : String} {p : s.ValidPos} {h h'} : (p.prev h).prev h' < p :=
lt_trans (p.prev h).prev_lt p.prev_lt
theorem Splits.remainingBytes_eq {s : String} {p : s.ValidPos} {t₁ t₂}
(h : p.Splits t₁ t₂) : p.remainingBytes = t₂.utf8ByteSize := by
simp [ValidPos.remainingBytes_eq, h.eq_append, h.offset_eq_rawEndPos]
end ValidPos
namespace Slice.Pos
@[simp]
theorem remainingBytes_toCopy {s : Slice} {p : s.Pos} :
p.toCopy.remainingBytes = p.remainingBytes := by
simp [remainingBytes_eq, ValidPos.remainingBytes_eq, Slice.utf8ByteSize_eq]
theorem Splits.remainingBytes_eq {s : Slice} {p : s.Pos} {t₁ t₂} (h : p.Splits t₁ t₂) :
p.remainingBytes = t₂.utf8ByteSize := by
simpa using h.toCopy.remainingBytes_eq
end Slice.Pos
macro_rules | `(tactic| decreasing_trivial) => `(tactic|
(with_reducible change (_ : Slice.Pos _) < _
simp [
Slice.Pos.eq_next_of_next?_eq_some (by assumption),
]) <;> done)
macro_rules | `(tactic| decreasing_trivial) => `(tactic|
(with_reducible change (_ : Slice.Pos _) < _
simp [
Slice.Pos.eq_prev_of_prev?_eq_some (by assumption),
]) <;> done)
macro_rules | `(tactic| decreasing_trivial) => `(tactic|
(with_reducible change (_ : String.ValidPos _) < _
simp [
ValidPos.eq_next_of_next?_eq_some (by assumption),
]) <;> done)
macro_rules | `(tactic| decreasing_trivial) => `(tactic|
(with_reducible change (_ : String.ValidPos _) < _
simp [
ValidPos.eq_prev_of_prev?_eq_some (by assumption),
]) <;> done)
end String

View File

@@ -60,14 +60,8 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
@[int_toBitVec] theorem le_iff_toBitVec_le {a b : $typeName} : a b a.toBitVec b.toBitVec := .rfl
@[deprecated le_iff_toBitVec_le (since := "2025-03-20")]
protected theorem le_def {a b : $typeName} : a b a.toBitVec b.toBitVec := .rfl
@[int_toBitVec] theorem lt_iff_toBitVec_lt {a b : $typeName} : a < b a.toBitVec < b.toBitVec := .rfl
@[deprecated lt_iff_toBitVec_lt (since := "2025-03-20")]
protected theorem lt_def {a b : $typeName} : a < b a.toBitVec < b.toBitVec := .rfl
theorem le_iff_toNat_le {a b : $typeName} : a b a.toNat b.toNat := .rfl
theorem lt_iff_toNat_lt {a b : $typeName} : a < b a.toNat < b.toNat := .rfl
@@ -304,22 +298,6 @@ theorem UInt32.le_ofNat_iff {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat
theorem UInt32.ofNat_le_iff {n : UInt32} {m : Nat} (h : m < size) : ofNat m n m n.toNat := by
rw [le_iff_toNat_le, toNat_ofNat_of_lt' h]
@[deprecated UInt32.lt_ofNat_iff (since := "2025-03-18")]
theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m n.toNat < m :=
(UInt32.lt_ofNat_iff h).1
@[deprecated UInt32.ofNat_lt_iff (since := "2025-03-18")]
theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n m < n.toNat :=
(UInt32.ofNat_lt_iff h).1
@[deprecated UInt32.le_ofNat_iff (since := "2025-03-18")]
theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ofNat m n.toNat m :=
(UInt32.le_ofNat_iff h).1
@[deprecated UInt32.ofNat_le_iff (since := "2025-03-18")]
theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m n m n.toNat :=
(UInt32.ofNat_le_iff h).1
theorem UInt64.lt_ofNat_iff {n : UInt64} {m : Nat} (h : m < size) : n < ofNat m n.toNat < m := by
rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h]
theorem UInt64.ofNat_lt_iff {n : UInt64} {m : Nat} (h : m < size) : ofNat m < n m < n.toNat := by

View File

@@ -603,7 +603,4 @@ and simplifies these to the function directly taking the value.
(replicate n x).unattach = replicate n x.1 := by
simp [unattach]
@[deprecated unattach_replicate (since := "2025-03-18")]
abbrev unattach_mkVector := @unattach_replicate
end Vector

View File

@@ -80,15 +80,9 @@ def elimAsList {motive : Vector α n → Sort u}
/-- Make an empty vector with pre-allocated capacity. -/
@[inline, expose] def emptyWithCapacity (capacity : Nat) : Vector α 0 := .emptyWithCapacity capacity, by simp
@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
abbrev mkEmpty := @emptyWithCapacity
/-- Makes a vector of size `n` with all cells containing `v`. -/
@[inline, expose] def replicate (n) (v : α) : Vector α n := Array.replicate n v, by simp
@[deprecated replicate (since := "2025-03-18")]
abbrev mkVector := @replicate
instance : Nonempty (Vector α 0) := #v[]
instance [Nonempty α] : Nonempty (Vector α n) := replicate _ Classical.ofNonempty

View File

@@ -82,9 +82,6 @@ theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a
simp only [replicate_eq_mk_replicate, countP_mk]
simp [Array.countP_replicate]
@[deprecated countP_replicate (since := "2025-03-18")]
abbrev countP_mkVector := @countP_replicate
theorem boole_getElem_le_countP {p : α Bool} {xs : Vector α n} (h : i < n) :
(if p xs[i] then 1 else 0) xs.countP p := by
rcases xs with xs, rfl
@@ -227,16 +224,10 @@ theorem count_eq_size {xs : Vector α n} : count a xs = n ↔ ∀ b ∈ xs, a =
simp only [replicate_eq_mk_replicate, count_mk]
simp
@[deprecated count_replicate_self (since := "2025-03-18")]
abbrev count_mkVector_self := @count_replicate_self
theorem count_replicate {a b : α} {n : Nat} : count a (replicate n b) = if b == a then n else 0 := by
simp only [replicate_eq_mk_replicate, count_mk]
simp [Array.count_replicate]
@[deprecated count_replicate (since := "2025-03-18")]
abbrev count_mkVector := @count_replicate
theorem count_le_count_map [BEq β] [LawfulBEq β] {xs : Vector α n} {f : α β} {x : α} :
count x xs count (f x) (map f xs) := by
rcases xs with xs, rfl

View File

@@ -93,9 +93,6 @@ theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
rw [replicate_eq_mk_replicate, eraseIdx_mk]
simp [Array.eraseIdx_replicate, *]
@[deprecated eraseIdx_replicate (since := "2025-03-18")]
abbrev eraseIdx_mkVector := @eraseIdx_replicate
theorem mem_eraseIdx_iff_getElem {x : α} {xs : Vector α n} {k} {h} : x xs.eraseIdx k h i w, i k xs[i]'w = x := by
rcases xs with xs
simp [Array.mem_eraseIdx_iff_getElem, *]

View File

@@ -156,9 +156,6 @@ theorem extract_append_left {xs : Vector α n} {ys : Vector α m} :
ext i h
simp
@[deprecated extract_mkVector (since := "2025-03-18")]
abbrev extract_mkVector := @extract_replicate
theorem extract_add_left {xs : Vector α n} {i j k : Nat} :
xs.extract (i + j) k = ((xs.extract i k).extract j (k - i)).cast (by omega) := by
rcases xs with xs, rfl

View File

@@ -130,31 +130,19 @@ theorem getElem_zero_flatten {xss : Vector (Vector α m) n} (h : 0 < n * m) :
theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
rw [replicate_eq_mk_replicate, findSome?_mk, Array.findSome?_replicate]
@[deprecated findSome?_replicate (since := "2025-03-18")]
abbrev findSome?_mkVector := @findSome?_replicate
@[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
simp [findSome?_replicate, Nat.ne_of_gt h]
@[deprecated findSome?_replicate_of_pos (since := "2025-03-18")]
abbrev findSome?_mkVector_of_pos := @findSome?_replicate_of_pos
-- Argument is unused, but used to decide whether `simp` should unfold.
@[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
findSome? f (replicate n a) = if n = 0 then none else f a := by
simp [findSome?_replicate]
@[deprecated findSome?_replicate_of_isSome (since := "2025-03-18")]
abbrev findSome?_mkVector_of_isSome := @findSome?_replicate_of_isSome
@[simp] theorem findSome?_replicate_of_isNone (h : (f a).isNone) :
findSome? f (replicate n a) = none := by
rw [Option.isNone_iff_eq_none] at h
simp [findSome?_replicate, h]
@[deprecated findSome?_replicate_of_isNone (since := "2025-03-18")]
abbrev findSome?_mkVector_of_isNone := @findSome?_replicate_of_isNone
/-! ### find? -/
@[simp, grind =] theorem find?_empty : find? p #v[] = none := rfl
@@ -263,53 +251,32 @@ theorem find?_replicate :
find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
rw [replicate_eq_mk_replicate, find?_mk, Array.find?_replicate]
@[deprecated find?_replicate (since := "2025-03-18")]
abbrev find?_mkVector := @find?_replicate
@[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
find? p (replicate n a) = if p a then some a else none := by
simp [find?_replicate, Nat.ne_of_gt h]
@[deprecated find?_replicate_of_size_pos (since := "2025-03-18")]
abbrev find?_mkVector_of_length_pos := @find?_replicate_of_size_pos
@[simp] theorem find?_replicate_of_pos (h : p a) :
find? p (replicate n a) = if n = 0 then none else some a := by
simp [find?_replicate, h]
@[deprecated find?_replicate_of_pos (since := "2025-03-18")]
abbrev find?_mkVector_of_pos := @find?_replicate_of_pos
@[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
simp [find?_replicate, h]
@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
abbrev find?_mkVector_of_neg := @find?_replicate_of_neg
-- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α Bool} :
(replicate n a).find? p = none n = 0 !p a := by
simp [Classical.or_iff_not_imp_left]
@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
abbrev find?_mkVector_eq_none_iff := @find?_replicate_eq_none_iff
@[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α Bool} :
(replicate n a).find? p = some b n 0 p a a = b := by
rw [replicate_eq_mk_replicate, find?_mk]
simp
@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
abbrev find?_mkVector_eq_some_iff := @find?_replicate_eq_some_iff
@[simp] theorem get_find?_replicate {n : Nat} {a : α} {p : α Bool} (h) :
((replicate n a).find? p).get h = a := by
simp only [replicate_eq_mk_replicate, find?_mk]
simp
@[deprecated get_find?_replicate (since := "2025-03-18")]
abbrev get_find?_mkVector := @get_find?_replicate
@[grind =]
theorem find?_pmap {P : α Prop} {f : (a : α) P a β} {xs : Vector α n}
(H : (a : α), a xs P a) {p : β Bool} :

View File

@@ -287,9 +287,6 @@ set_option linter.indexVariables false in
@[simp, grind =] theorem toArray_emptyWithCapacity {cap} :
(Vector.emptyWithCapacity (α := α) cap).toArray = Array.emptyWithCapacity cap := rfl
@[deprecated toArray_emptyWithCapacity (since := "2025-03-12")]
abbrev toArray_mkEmpty := @toArray_emptyWithCapacity
@[simp, grind =] theorem toArray_eraseIdx {xs : Vector α n} {i} (h) :
(xs.eraseIdx i h).toArray = xs.toArray.eraseIdx i (by simp [h]) := rfl
@@ -474,9 +471,6 @@ theorem toArray_swapAt! {xs : Vector α n} {i x} :
@[simp, grind =] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl
@[deprecated toArray_replicate (since := "2025-03-18")]
abbrev toArray_mkVector := @toArray_replicate
@[simp] theorem toArray_inj {xs ys : Vector α n} : xs.toArray = ys.toArray xs = ys := by
cases xs
cases ys
@@ -531,9 +525,6 @@ theorem toList_empty : (#v[] : Vector α 0).toList = [] := rfl
theorem toList_emptyWithCapacity {cap} :
(Vector.emptyWithCapacity (α := α) cap).toList = [] := rfl
@[deprecated toList_emptyWithCapacity (since := "2025-03-12")]
abbrev toList_mkEmpty := @toList_emptyWithCapacity
theorem toList_eraseIdx {xs : Vector α n} {i} (h) :
(xs.eraseIdx i h).toList = xs.toList.eraseIdx i := by simp [toList]
@@ -663,9 +654,6 @@ theorem toList_swap {xs : Vector α n} {i j} (hi hj) :
@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := rfl
@[deprecated toList_replicate (since := "2025-03-18")]
abbrev toList_mkVector := @toList_replicate
theorem toList_inj {xs ys : Vector α n} : xs.toList = ys.toList xs = ys := by
cases xs
cases ys
@@ -676,9 +664,6 @@ theorem toList_inj {xs ys : Vector α n} : xs.toList = ys.toList ↔ xs = ys :=
simp only [toList, Array.toList_eq_nil_iff]
exact by rintro rfl; simp_all, by rintro rfl; simpa using h
@[deprecated toList_eq_nil_iff (since := "2025-04-04")]
abbrev toList_eq_empty_iff {α n} (xs) := @toList_eq_nil_iff α n xs
@[simp] theorem mem_toList_iff {a : α} {xs : Vector α n} : a xs.toList a xs := by
simp [toList]
@@ -784,35 +769,20 @@ theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
@[simp, grind =] theorem replicate_zero : replicate 0 a = #v[] := rfl
@[deprecated replicate_zero (since := "2025-03-18")]
abbrev replicate_mkVector := @replicate_zero
@[grind =]
theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
simp [replicate, Array.replicate_succ]
@[deprecated replicate_succ (since := "2025-03-18")]
abbrev replicate_mkVector_succ := @replicate_succ
@[simp] theorem replicate_inj : replicate n a = replicate n b n = 0 a = b := by
simp [ toArray_inj, toArray_replicate, Array.replicate_inj]
@[deprecated replicate_inj (since := "2025-03-18")]
abbrev mkVector_inj := @replicate_inj
@[simp] theorem _root_.Array.vector_mk_replicate {a : α} {n : Nat} :
mk (n := n) (Array.replicate n a) (by simp) = replicate n a := rfl
@[deprecated _root_.Array.vector_mk_replicate (since := "2025-03-18")]
abbrev _root_.Array.mk_mkArray := @_root_.Array.vector_mk_replicate
theorem replicate_eq_mk_replicate {a : α} {n : Nat} :
replicate n a = mk (n := n) (Array.replicate n a) (by simp) := by
simp
@[deprecated replicate_eq_mk_replicate (since := "2025-03-18")]
abbrev mkVector_eq_mk_mkArray := @replicate_eq_mk_replicate
/-! ## L[i] and L[i]? -/
theorem getElem?_eq_none_iff {xs : Vector α n} : xs[i]? = none n i := by
@@ -1373,9 +1343,6 @@ theorem mem_setIfInBounds {xs : Vector α n} {a : α} (hi : i < n) :
rw [Bool.eq_iff_iff]
simp +contextual
@[deprecated replicate_beq_replicate (since := "2025-03-18")]
abbrev mkVector_beq_mkVector := @replicate_beq_replicate
@[simp] theorem reflBEq_iff [BEq α] [NeZero n] : ReflBEq (Vector α n) ReflBEq α := by
match n, NeZero.ne n with
| n + 1, _ =>
@@ -2074,78 +2041,45 @@ theorem map_eq_flatMap {f : α → β} {xs : Vector α n} :
@[simp] theorem replicate_one : replicate 1 a = #v[a] := rfl
@[deprecated replicate_one (since := "2025-03-18")]
abbrev replicate_mkVector_one := @replicate_one
/-- Variant of `replicate_succ` that prepends `a` at the beginning of the vector. -/
theorem replicate_succ' : replicate (n + 1) a = (#v[a] ++ replicate n a).cast (by omega) := by
rw [ toArray_inj]
simp [Array.replicate_succ']
@[deprecated replicate_succ' (since := "2025-03-18")]
abbrev mkVector_succ' := @replicate_succ'
@[simp, grind =] theorem mem_replicate {a b : α} {n} : b replicate n a n 0 b = a := by
unfold replicate
simp only [mem_mk]
simp
@[deprecated mem_replicate (since := "2025-03-18")]
abbrev mem_mkVector := @mem_replicate
@[grind ] theorem eq_of_mem_replicate {a b : α} {n} (h : b replicate n a) : b = a := (mem_replicate.1 h).2
@[deprecated eq_of_mem_replicate (since := "2025-03-18")]
abbrev eq_of_mem_mkVector := @eq_of_mem_replicate
theorem forall_mem_replicate {p : α Prop} {a : α} {n} :
( b, b replicate n a p b) n = 0 p a := by
cases n <;> simp [mem_replicate]
@[deprecated forall_mem_replicate (since := "2025-03-18")]
abbrev forall_mem_mkVector := @forall_mem_replicate
@[simp, grind =] theorem getElem_replicate {a : α} (h : i < n) : (replicate n a)[i] = a := by
rw [replicate_eq_mk_replicate, getElem_mk]
simp
@[deprecated getElem_replicate (since := "2025-03-18")]
abbrev getElem_mkVector := @getElem_replicate
@[grind =] theorem getElem?_replicate {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none := by
simp [getElem?_def]
@[deprecated getElem?_replicate (since := "2025-03-18")]
abbrev getElem?_mkVector := @getElem?_replicate
@[simp] theorem getElem?_replicate_of_lt {n : Nat} {i : Nat} (h : i < n) : (replicate n a)[i]? = some a := by
simp [h]
@[deprecated getElem?_replicate_of_lt (since := "2025-03-18")]
abbrev getElem?_mkVector_of_lt := @getElem?_replicate_of_lt
theorem eq_replicate_of_mem {a : α} {xs : Vector α n} (h : (b) (_ : b xs), b = a) : xs = replicate n a := by
rw [ toArray_inj]
simpa using Array.eq_replicate_of_mem (xs := xs.toArray) (by simpa using h)
@[deprecated eq_replicate_of_mem (since := "2025-03-18")]
abbrev eq_mkVector_of_mem := @eq_replicate_of_mem
theorem eq_replicate_iff {a : α} {n} {xs : Vector α n} :
xs = replicate n a (b) (_ : b xs), b = a := by
rw [ toArray_inj]
simpa using Array.eq_replicate_iff (xs := xs.toArray) (n := n)
@[deprecated eq_replicate_iff (since := "2025-03-18")]
abbrev eq_mkVector_iff := @eq_replicate_iff
theorem map_eq_replicate_iff {xs : Vector α n} {f : α β} {b : β} :
xs.map f = replicate n b x xs, f x = b := by
simp [eq_replicate_iff]
@[deprecated map_eq_replicate_iff (since := "2025-03-18")]
abbrev map_eq_mkVector_iff := @map_eq_replicate_iff
@[simp] theorem map_const {xs : Vector α n} {b : β} : map (Function.const α b) xs = replicate n b :=
map_eq_replicate_iff.mpr fun _ _ => rfl
@@ -2162,78 +2096,45 @@ theorem map_const' {xs : Vector α n} {b : β} : map (fun _ => b) xs = replicate
rw [ toArray_inj]
simp
@[deprecated set_replicate_self (since := "2025-03-18")]
abbrev set_mkVector_self := @set_replicate_self
@[simp] theorem setIfInBounds_replicate_self : (replicate n a).setIfInBounds i a = replicate n a := by
rw [ toArray_inj]
simp
@[deprecated setIfInBounds_replicate_self (since := "2025-03-18")]
abbrev setIfInBounds_mkVector_self := @setIfInBounds_replicate_self
@[simp] theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
rw [ toArray_inj]
simp
@[deprecated replicate_append_replicate (since := "2025-03-18")]
abbrev mkVector_append_mkVector := @replicate_append_replicate
theorem append_eq_replicate_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
xs ++ ys = replicate (n + m) a xs = replicate n a ys = replicate m a := by
simp [ toArray_inj, Array.append_eq_replicate_iff]
@[deprecated append_eq_replicate_iff (since := "2025-03-18")]
abbrev append_eq_mkVector_iff := @append_eq_replicate_iff
theorem replicate_eq_append_iff {xs : Vector α n} {ys : Vector α m} {a : α} :
replicate (n + m) a = xs ++ ys xs = replicate n a ys = replicate m a := by
rw [eq_comm, append_eq_replicate_iff]
@[deprecated replicate_eq_append_iff (since := "2025-03-18")]
abbrev mkVector_eq_append_iff := @replicate_eq_append_iff
@[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
rw [ toArray_inj]
simp
@[deprecated map_replicate (since := "2025-03-18")]
abbrev map_mkVector := @map_replicate
@[simp] theorem flatten_replicate_empty : (replicate n (#v[] : Vector α 0)).flatten = #v[] := by
rw [ toArray_inj]
simp
@[deprecated flatten_replicate_empty (since := "2025-03-18")]
abbrev flatten_mkVector_empty := @flatten_replicate_empty
@[simp] theorem flatten_replicate_singleton : (replicate n #v[a]).flatten = (replicate n a).cast (by simp) := by
ext i h
simp
@[deprecated flatten_replicate_singleton (since := "2025-03-18")]
abbrev flatten_mkVector_singleton := @flatten_replicate_singleton
@[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a := by
ext i h
simp
@[deprecated flatten_replicate_replicate (since := "2025-03-18")]
abbrev flatten_mkVector_mkVector := @flatten_replicate_replicate
theorem flatMap_replicate {f : α Vector β m} : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
ext i h
simp
@[deprecated flatMap_replicate (since := "2025-03-18")]
abbrev flatMap_mkVector := @flatMap_replicate
@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
simp [sum, toArray_replicate]
@[deprecated sum_replicate_nat (since := "2025-03-18")]
abbrev sum_mkVector := @sum_replicate_nat
/-! ### reverse -/
theorem reverse_empty : reverse (#v[] : Vector α 0) = #v[] := rfl
@@ -2335,9 +2236,6 @@ theorem flatMap_reverse {xs : Vector α n} {f : α → Vector β m} :
rw [ toArray_inj]
simp
@[deprecated reverse_replicate (since := "2025-03-18")]
abbrev reverse_mkVector := @reverse_replicate
/-! ### extract -/
@[simp] theorem getElem_extract {as : Vector α n} {start stop : Nat}
@@ -2662,15 +2560,9 @@ theorem back?_replicate {a : α} {n : Nat} :
rw [replicate_eq_mk_replicate]
simp only [back?_mk, Array.back?_replicate]
@[deprecated back?_replicate (since := "2025-03-18")]
abbrev back?_mkVector := @back?_replicate
@[simp] theorem back_replicate [NeZero n] : (replicate n a).back = a := by
simp [back_eq_getElem]
@[deprecated back_replicate (since := "2025-03-18")]
abbrev back_mkVector := @back_replicate
/-! ### leftpad and rightpad -/
@[simp] theorem leftpad_mk {n : Nat} {a : α} {xs : Array α} (h : xs.size = m) :
@@ -2811,9 +2703,6 @@ theorem pop_append {xs : Vector α n} {ys : Vector α m} :
@[simp] theorem pop_replicate {n : Nat} {a : α} : (replicate n a).pop = replicate (n - 1) a := by
ext <;> simp
@[deprecated pop_replicate (since := "2025-03-18")]
abbrev pop_mkVector := @pop_replicate
/-! ## Logic -/
/-! ### any / all -/
@@ -2969,16 +2858,10 @@ theorem all_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool
(replicate n a).any f = if n = 0 then false else f a := by
induction n <;> simp_all [replicate_succ']
@[deprecated any_replicate (since := "2025-03-18")]
abbrev any_mkVector := @any_replicate
@[simp] theorem all_replicate {n : Nat} {a : α} :
(replicate n a).all f = if n = 0 then true else f a := by
induction n <;> simp_all +contextual [replicate_succ']
@[deprecated all_replicate (since := "2025-03-18")]
abbrev all_mkVector := @all_replicate
/-! ### replace -/
section replace
@@ -3053,17 +2936,11 @@ theorem replace_extract {xs : Vector α n} {i : Nat} :
match n, h with
| n + 1, _ => simp_all [replicate_succ', replace_append]
@[deprecated replace_replicate_self (since := "2025-03-18")]
abbrev replace_mkArray_self := @replace_replicate_self
@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
(replicate n a).replace b c = replicate n a := by
rw [replace_of_not_mem]
simp_all
@[deprecated replace_replicate_ne (since := "2025-03-18")]
abbrev replace_mkArray_ne := @replace_replicate_ne
end replace
/-! Content below this point has not yet been aligned with `List` and `Array`. -/

View File

@@ -216,9 +216,6 @@ theorem mapFinIdx_eq_replicate_iff {xs : Vector α n} {f : (i : Nat) → α
rcases xs with xs, rfl
simp [Array.mapFinIdx_eq_replicate_iff]
@[deprecated mapFinIdx_eq_replicate_iff (since := "2025-03-18")]
abbrev mapFinIdx_eq_mkVector_iff := @mapFinIdx_eq_replicate_iff
@[simp, grind =] theorem mapFinIdx_reverse {xs : Vector α n} {f : (i : Nat) α (h : i < n) β} :
xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (n - 1 - i) a (by omega))).reverse := by
rcases xs with xs, rfl
@@ -351,9 +348,6 @@ theorem mapIdx_eq_replicate_iff {xs : Vector α n} {f : Nat → α → β} {b :
rcases xs with xs, rfl
simp [Array.mapIdx_eq_replicate_iff]
@[deprecated mapIdx_eq_replicate_iff (since := "2025-03-18")]
abbrev mapIdx_eq_mkVector_iff := @mapIdx_eq_replicate_iff
@[simp, grind =] theorem mapIdx_reverse {xs : Vector α n} {f : Nat α β} :
xs.reverse.mapIdx f = (mapIdx (fun i => f (n - 1 - i)) xs).reverse := by
rcases xs with xs, rfl

View File

@@ -163,9 +163,6 @@ theorem zipWith_replicate {a : α} {b : β} {n : Nat} :
ext
simp
@[deprecated zipWith_replicate (since := "2025-03-18")]
abbrev zipWith_mkVector := @zipWith_replicate
theorem map_uncurry_zip_eq_zipWith {f : α β γ} {as : Vector α n} {bs : Vector β n} :
map (Function.uncurry f) (as.zip bs) = zipWith f as bs := by
rcases as with as, rfl
@@ -268,9 +265,6 @@ theorem zip_replicate {a : α} {b : β} {n : Nat} :
zip (replicate n a) (replicate n b) = replicate n (a, b) := by
ext <;> simp
@[deprecated zip_replicate (since := "2025-03-18")]
abbrev zip_mkVector := @zip_replicate
/-! ### unzip -/
@[simp, grind =]
@@ -320,7 +314,4 @@ theorem unzip_replicate {a : α} {b : β} {n : Nat} :
unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
ext1 <;> simp
@[deprecated unzip_replicate (since := "2025-03-18")]
abbrev unzip_mkVector := @unzip_replicate
end Vector

View File

@@ -130,7 +130,7 @@ If `grind!` is used, then only minimal indexable subexpressions are considered.
syntax grindLR := patternIgnore("" <|> "=>")
/--
The `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
theorem, and then the hypotheses from eft to right. We say this is the default modifier.
theorem, and then the hypotheses from left to right. We say this is the default modifier.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.

216
src/Init/Grind/Config.lean Normal file
View File

@@ -0,0 +1,216 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Core
public section
namespace Lean.Grind
/--
The configuration for `grind`.
Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
-/
structure Config where
/-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
trace : Bool := false
/-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
or for which no patterns can be generated. -/
lax : Bool := false
/-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
premises : Bool := false
/-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
splits : Nat := 9
/-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
ematch : Nat := 5
/--
Maximum term generation.
The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain. -/
gen : Nat := 8
/-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
instances : Nat := 1000
/-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
matchEqs : Bool := true
/-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
splitMatch : Bool := true
/-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
splitIte : Bool := true
/--
If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
Otherwise, it performs case-splitting only on types marked with `[grind cases]` attribute. -/
splitIndPred : Bool := false
/--
If `splitImp` is `true`, then given an implication `p → q` or `(h : p) → q h`, `grind` splits on `p`
if the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
-/
splitImp : Bool := false
/-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
canonHeartbeats : Nat := 1000
/-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`. -/
ext : Bool := true
/-- If `extAll` is `true`, `grind` uses any extensionality theorems available in the environment. -/
extAll : Bool := false
/--
If `etaStruct` is `true`, then for each term `t : S` such that `S` is a structure,
and is tagged with `[grind ext]`, `grind` adds the equation `t = ⟨t.1, ..., t.n⟩`
which holds by reflexivity. Moreover, the extensionality theorem for `S` is not used.
-/
etaStruct : Bool := true
/--
If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
on equalities between lambda expressions.
-/
funext : Bool := true
/-- TODO -/
lookahead : Bool := true
/-- If `verbose` is `false`, additional diagnostics information is not collected. -/
verbose : Bool := true
/-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/
clean : Bool := true
/--
If `qlia` is `true`, `grind` may generate counterexamples for integer constraints
using rational numbers, and ignoring divisibility constraints.
This approach is cheaper but incomplete. -/
qlia : Bool := false
/--
If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
See paper "Model-based Theory Combination" for details.
-/
mbtc : Bool := true
/--
When set to `true` (default: `true`), local definitions are unfolded during normalization and internalization.
In other words, given a local context with an entry `x : t := e`, the free variable `x` is reduced to `e`.
Note that this behavior is also available in `simp`, but there its default is `false` because `simp` is not
always used as a terminal tactic, and it important to preserve the abstractions introduced by users.
Additionally, in `grind` we observed that `zetaDelta` is particularly important when combined with function induction.
In such scenarios, the same let-expressions can be introduced by function induction and also by unfolding the
corresponding definition. We want to avoid a situation in which `zetaDelta` is not applied to let-declarations
introduced by function induction while `zeta` unfolds the definition, causing a mismatch.
Finally, note that congruence closure is less effective on terms containing many binders such as
`lambda` and `let` expressions.
-/
zetaDelta := true
/--
When `true` (default: `true`), performs zeta reduction of let expressions during normalization.
That is, `let x := v; e[x]` reduces to `e[v]`. See also `zetaDelta`.
-/
zeta := true
/--
When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
This solver also support commutative semirings, fields, and normalizer non-commutative rings and
semirings.
-/
ring := true
/--
Maximum number of steps performed by the `ring` solver.
A step is counted whenever one polynomial is used to simplify another.
For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
used to simplify the second to `-1 * y^3 + x * y`.
-/
ringSteps := 10000
/--
When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
`CommRing`.
-/
linarith := true
/--
When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`.
-/
cutsat := true
/--
When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
-/
ac := true
/--
Maximum number of steps performed by the `ac` solver.
A step is counted whenever one AC equation is used to simplify another.
For example, given `ma x z = w` and `max x (max y z) = x`, the first can be
used to simplify the second to `max w y = x`.
-/
acSteps := 1000
/--
Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
the characteristic of a ring.
-/
exp : Nat := 2^20
/--
When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
-/
abstractProof := true
/--
When `true` (default: `true`), enables the procedure for handling injective functions.
In this mode, `grind` takes into account theorems such as:
```
@[grind inj] theorem double_inj : Function.Injective double
```
-/
inj := true
/--
When `true` (default: `true`), enables the procedure for handling orders that implement
at least `Std.IsPreorder`
-/
order := true
/--
When `true` (default: `true`), enables the legacy module `offset`. This module will be deleted in
the future.
-/
offset := true
deriving Inhabited, BEq
/--
Configuration for interactive mode.
We disable `clean := false`.
-/
structure ConfigInteractive extends Config where
clean := false
/--
A minimal configuration, with ematching and splitting disabled, and all solver modules turned off.
`grind` will not do anything in this configuration,
which can be used a starting point for minimal configurations.
-/
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
structure NoopConfig extends Config where
-- Disable splitting
splits := 0
-- We don't override the various `splitMatch` / `splitIte` settings separately.
-- Disable e-matching
ematch := 0
-- We don't override `matchEqs` separately.
-- Disable extensionality
ext := false
extAll := false
etaStruct := false
funext := false
-- Disable all solver modules
ring := false
linarith := false
cutsat := false
ac := false
/--
A `grind` configuration that only uses `cutsat` and splitting.
Note: `cutsat` benefits from some amount of instantiation, e.g. `Nat.max_def`.
We don't currently have a mechanism to enable only a small set of lemmas.
-/
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
structure CutsatConfig extends NoopConfig where
cutsat := true
-- Allow the default number of splits.
splits := ({} : Config).splits
/--
A `grind` configuration that only uses `ring`.
-/
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
structure GrobnerConfig extends NoopConfig where
ring := true
end Lean.Grind

View File

@@ -16,6 +16,16 @@ when selecting patterns.
-/
syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
/-!
`grind` tactic and related tactics.
-/
syntax grindErase := "-" ident
/--
The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
when selecting patterns.
-/
syntax grindParam := grindErase <|> grindLemma <|> grindLemmaMin
namespace Grind
declare_syntax_cat grind_filter (behavior := both)
@@ -73,6 +83,10 @@ that may have redundant arguments.
-/
syntax (name := instantiate) "instantiate" (&" only")? (&" approx")? (" [" withoutPosition(thm,*,?) "]")? : grind
/-- Shorthand for `instantiate only` -/
syntax (name := use) "use" " [" withoutPosition(thm,*,?) "]" : grind
macro_rules | `(grind| use%$u [$ts:thm,*]) => `(grind| instantiate%$u only [$ts,*])
-- **Note**: Should we rename the following tactics to `trace_`?
/-- Shows asserted facts. -/
syntax (name := showAsserted) "show_asserted" ppSpace grindFilter : grind
@@ -98,8 +112,17 @@ declare_syntax_cat grind_ref (behavior := both)
syntax:max anchor : grind_ref
syntax term : grind_ref
/--
Performs a case-split on a logical connective, `match`-expression, `if-then-else`-expression,
or inductive predicate. The argument is an anchor referencing one of the case-split candidates
in the `grind` state. You can use `cases?` to select a specific candidate using a code action.
-/
syntax (name := cases) "cases " grind_ref : grind
/--
A variant of `cases` that provides a code-action for selecting one of the candidate case-splits
available in the `grind` state.
-/
syntax (name := casesTrace) "cases?" grindFilter : grind
/-- `done` succeeds iff there are no remaining goals. -/
@@ -111,6 +134,14 @@ syntax (name := finish) "finish" : grind
/-- `finish?` tries to close the current goal using `grind`'s default strategy and suggests a tactic script. -/
syntax (name := finishTrace) "finish?" : grind
/--
The `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded.
* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
-/
syntax (name := «have») "have" letDecl : grind
/-- Executes the given tactic block to close the current goal. -/
@@ -128,8 +159,19 @@ Usually `· tac`, which enforces that the goal is closed by `tac`, should be pre
-/
syntax (name := focus) "focus " grindSeq : grind
/--
`next => tac` focuses on the next goal and solves it using `tac`, or else fails.
`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
inaccessible names to the given names.
-/
syntax (name := next) "next " binderIdent* " => " grindSeq : grind
/--
`· grindSeq` focuses on the main `grind` goal and tries to solve it using the given
sequence of `grind` tactics.
-/
macro dot:patternIgnore("· " <|> ". ") s:grindSeq : grind => `(grind| next%$dot =>%$dot $s:grindSeq )
/--
`any_goals tac` applies the tactic `tac` to every goal,
concatenating the resulting goals for successful tactic applications.
@@ -198,10 +240,20 @@ syntax (name := exposeNames) "expose_names" : grind
but it sets the option only within the tactics `tacs`. -/
syntax (name := setOption) "set_option " (ident (noWs "." noWs ident)?) ppSpace optionValue " in " grindSeq : grind
/--
`set_config configItem+ in tacs` executes `tacs` with the updated configuration options `configItem+`
-/
syntax (name := setConfig) "set_config " configItem+ " in " grindSeq : grind
/--
Proves `<term>` using the current `grind` state and default search strategy.
-/
syntax (name := haveSilent) "have" (ppSpace ident)? ppSpace ": " term : grind
/--
Adds new case-splits using model-based theory combination.
-/
syntax (name := mbtc) "mbtc" : grind
end Grind
end Lean.Parser.Tactic

View File

@@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Data.Int.Linear
public import Init.Grind.Ring.Field
public import Init.Data.Rat.Lemmas
public section
namespace Lean.Grind
@@ -153,7 +152,7 @@ init_grind_norm
/- Pre theorems -/
|
/- Post theorems -/
iff_eq heq_eq_eq
iff_eq heq_eq_eq eq_self
-- And
and_true true_and and_false false_and and_assoc
-- ite
@@ -208,5 +207,7 @@ init_grind_norm
Ring.intCast_mul
Ring.intCast_pow
Ring.intCast_sub
-- Rationals
Rat.ofScientific_def_eq_if Rat.zpow_neg
end Lean.Grind

View File

@@ -107,6 +107,11 @@ Helper theorem for equality propagation
theorem eq_of_le_of_le {α} [LE α] [Std.IsPartialOrder α] {a b : α} : a b b a a = b :=
Std.IsPartialOrder.le_antisymm _ _
theorem eq_of_le_of_le_0 {α} [LE α] [Std.IsPartialOrder α] [Ring α]
{a b : α} : a b + Int.cast (R := α) 0 b a + Int.cast (R := α) 0 a = b := by
simp [Ring.intCast_zero, Semiring.add_zero]
apply Std.IsPartialOrder.le_antisymm
/-!
Transitivity
-/

View File

@@ -7,6 +7,7 @@ module
prelude
public import Init.Grind.Ring.Basic
public import Init.Grind.Ring.Field
public import Init.Grind.Ring.OfScientific
public import Init.Grind.Ring.Envelope
public import Init.Grind.Ring.CommSolver
public import Init.Grind.Ring.CommSemiringAdapter

View File

@@ -201,6 +201,9 @@ theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂
next => simp [pow_zero, mul_one]
next k₂ ih => rw [Nat.add_succ, pow_succ, pow_succ, ih, mul_assoc]
theorem pow_add_congr (a r : α) (k k₁ k₂ : Nat) : k = k₁ + k₂ a^k₁ * a^k₂ = r a ^ k = r := by
intros; subst k r; rw [pow_add]
theorem natCast_pow (x : Nat) (k : Nat) : ((x ^ k : Nat) : α) = (x : α) ^ k := by
induction k
next => simp [pow_zero, Nat.pow_zero, natCast_one]

View File

@@ -0,0 +1,29 @@
/-
Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
module
prelude
public import Init.Grind.Ring.Field
public import Init.Data.OfScientific
public section
namespace Lean.Grind
attribute [local instance] Semiring.natCast
/--
A type class that ensures that `OfScientific.ofScientific` is properly defined with respect to
the field structure.
-/
class LawfulOfScientific (α : Type u) [Field α] [OfScientific α] : Prop where
/--
`OfScientific.ofScientific` is properly defined with respect to the field structure.
-/
ofScientific_def :
OfScientific.ofScientific m s e = if s then (Nat.cast m : α) / 10^e else (Nat.cast m : α) * 10^e
end Lean.Grind

View File

@@ -7,227 +7,9 @@ module
prelude
public import Init.Core
public import Init.Grind.Interactive
public import Init.Grind.Config
public section
namespace Lean.Grind
/--
The configuration for `grind`.
Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
-/
structure Config where
/-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
trace : Bool := false
/-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
or for which no patterns can be generated. -/
lax : Bool := false
/-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
premises : Bool := false
/-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
splits : Nat := 9
/-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
ematch : Nat := 5
/--
Maximum term generation.
The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain. -/
gen : Nat := 8
/-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
instances : Nat := 1000
/-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
matchEqs : Bool := true
/-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
splitMatch : Bool := true
/-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
splitIte : Bool := true
/--
If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
Otherwise, it performs case-splitting only on types marked with `[grind cases]` attribute. -/
splitIndPred : Bool := false
/--
If `splitImp` is `true`, then given an implication `p → q` or `(h : p) → q h`, `grind` splits on `p`
if the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
-/
splitImp : Bool := false
/-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
canonHeartbeats : Nat := 1000
/-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`. -/
ext : Bool := true
/-- If `extAll` is `true`, `grind` uses any extensionality theorems available in the environment. -/
extAll : Bool := false
/--
If `etaStruct` is `true`, then for each term `t : S` such that `S` is a structure,
and is tagged with `[grind ext]`, `grind` adds the equation `t = ⟨t.1, ..., t.n⟩`
which holds by reflexivity. Moreover, the extensionality theorem for `S` is not used.
-/
etaStruct : Bool := true
/--
If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
on equalities between lambda expressions.
-/
funext : Bool := true
/-- TODO -/
lookahead : Bool := true
/-- If `verbose` is `false`, additional diagnostics information is not collected. -/
verbose : Bool := true
/-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/
clean : Bool := true
/--
If `qlia` is `true`, `grind` may generate counterexamples for integer constraints
using rational numbers, and ignoring divisibility constraints.
This approach is cheaper but incomplete. -/
qlia : Bool := false
/--
If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
See paper "Model-based Theory Combination" for details.
-/
mbtc : Bool := true
/--
When set to `true` (default: `true`), local definitions are unfolded during normalization and internalization.
In other words, given a local context with an entry `x : t := e`, the free variable `x` is reduced to `e`.
Note that this behavior is also available in `simp`, but there its default is `false` because `simp` is not
always used as a terminal tactic, and it important to preserve the abstractions introduced by users.
Additionally, in `grind` we observed that `zetaDelta` is particularly important when combined with function induction.
In such scenarios, the same let-expressions can be introduced by function induction and also by unfolding the
corresponding definition. We want to avoid a situation in which `zetaDelta` is not applied to let-declarations
introduced by function induction while `zeta` unfolds the definition, causing a mismatch.
Finally, note that congruence closure is less effective on terms containing many binders such as
`lambda` and `let` expressions.
-/
zetaDelta := true
/--
When `true` (default: `true`), performs zeta reduction of let expressions during normalization.
That is, `let x := v; e[x]` reduces to `e[v]`. See also `zetaDelta`.
-/
zeta := true
/--
When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
This solver also support commutative semirings, fields, and normalizer non-commutative rings and
semirings.
-/
ring := true
/--
Maximum number of steps performed by the `ring` solver.
A step is counted whenever one polynomial is used to simplify another.
For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
used to simplify the second to `-1 * y^3 + x * y`.
-/
ringSteps := 10000
/--
When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
`CommRing`.
-/
linarith := true
/--
When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`.
-/
cutsat := true
/--
When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
-/
ac := true
/--
Maximum number of steps performed by the `ac` solver.
A step is counted whenever one AC equation is used to simplify another.
For example, given `ma x z = w` and `max x (max y z) = x`, the first can be
used to simplify the second to `max w y = x`.
-/
acSteps := 1000
/--
Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
the characteristic of a ring.
-/
exp : Nat := 2^20
/--
When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
-/
abstractProof := true
/--
When `true` (default: `true`), enables the procedure for handling injective functions.
In this mode, `grind` takes into account theorems such as:
```
@[grind inj] theorem double_inj : Function.Injective double
```
-/
inj := true
/--
When `true` (default: `true`), enables the procedure for handling orders that implement
at least `Std.IsPreorder`
-/
order := true
/--
When `true` (default: `true`), enables the legacy module `offset`. This module will be deleted in
the future.
-/
offset := true
deriving Inhabited, BEq
/--
Configuration for interactive mode.
We disable `clean := false`.
-/
structure ConfigInteractive extends Config where
clean := false
/--
A minimal configuration, with ematching and splitting disabled, and all solver modules turned off.
`grind` will not do anything in this configuration,
which can be used a starting point for minimal configurations.
-/
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
structure NoopConfig extends Config where
-- Disable splitting
splits := 0
-- We don't override the various `splitMatch` / `splitIte` settings separately.
-- Disable e-matching
ematch := 0
-- We don't override `matchEqs` separately.
-- Disable extensionality
ext := false
extAll := false
etaStruct := false
funext := false
-- Disable all solver modules
ring := false
linarith := false
cutsat := false
ac := false
/--
A `grind` configuration that only uses `cutsat` and splitting.
Note: `cutsat` benefits from some amount of instantiation, e.g. `Nat.max_def`.
We don't currently have a mechanism to enable only a small set of lemmas.
-/
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
structure CutsatConfig extends NoopConfig where
cutsat := true
-- Allow the default number of splits.
splits := ({} : Config).splits
/--
A `grind` configuration that only uses `ring`.
-/
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
structure GrobnerConfig extends NoopConfig where
ring := true
end Lean.Grind
namespace Lean.Parser.Tactic
/-!
`grind` tactic and related tactics.
-/
syntax grindErase := "-" ident
/--
The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
when selecting patterns.
-/
syntax grindParam := grindErase <|> grindLemma <|> grindLemmaMin
open Parser.Tactic.Grind
/--

View File

@@ -6,7 +6,7 @@ Authors: Robin Arnez
module
prelude
public import Init.Grind.Ring.Field
public import Init.Grind.Ring.OfScientific
public import Init.Data.Rat.Lemmas
public section
@@ -56,4 +56,7 @@ instance : NoNatZeroDivisors Rat where
change k * a = k * b at h₂
simpa [ Rat.mul_assoc, Rat.inv_mul_cancel, h₁] using congrArg ((k : Rat)⁻¹ * ·) h₂
instance : LawfulOfScientific Rat where
ofScientific_def {m s e} := by rw [Rat.ofScientific_def_eq_if]
end Lean.Grind

View File

@@ -1099,6 +1099,7 @@ until `c` is known.
| Or.inl h => hp h
| Or.inr h => hq h
@[inline]
instance [dp : Decidable p] : Decidable (Not p) :=
match dp with
| isTrue hp => isFalse (absurd hp)

View File

@@ -447,18 +447,6 @@ theorem Decidable.by_contra [Decidable p] : (¬p → False) → p := of_not_not
@[expose] protected def Or.by_cases' [Decidable q] {α : Sort u} (h : p q) (h₁ : p α) (h₂ : q α) : α :=
if hq : q then h₂ hq else h₁ (h.resolve_right hq)
instance exists_prop_decidable {p} (P : p Prop)
[Decidable p] [ h, Decidable (P h)] : Decidable ( h, P h) :=
if h : p then
decidable_of_decidable_of_iff fun h2 => h, h2, fun _, h2 => h2
else isFalse fun h', _ => h h'
instance forall_prop_decidable {p} (P : p Prop)
[Decidable p] [ h, Decidable (P h)] : Decidable ( h, P h) :=
if h : p then
decidable_of_decidable_of_iff fun h2 _ => h2, fun al => al h
else isTrue fun h2 => absurd h2 h
@[bool_to_prop] theorem decide_eq_true_iff {p : Prop} [Decidable p] : (decide p = true) p := by simp
@[simp, bool_to_prop] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
@@ -543,31 +531,15 @@ theorem Decidable.not_and_not_right [Decidable b] : ¬(a ∧ ¬b) ↔ (a → b)
theorem Decidable.not_and_iff_not_or_not [Decidable a] : ¬(a b) ¬a ¬b :=
fun h => if ha : a then .inr (h ha, ·) else .inl ha, not_and_of_not_or_not
set_option linter.missingDocs false in
@[deprecated Decidable.not_and_iff_not_or_not (since := "2025-03-18")]
abbrev Decidable.not_and_iff_or_not_not := @Decidable.not_and_iff_not_or_not
theorem Decidable.not_and_iff_not_or_not' [Decidable b] : ¬(a b) ¬a ¬b :=
fun h => if hb : b then .inl (h ·, hb) else .inr hb, not_and_of_not_or_not
set_option linter.missingDocs false in
@[deprecated Decidable.not_and_iff_not_or_not' (since := "2025-03-18")]
abbrev Decidable.not_and_iff_or_not_not' := @Decidable.not_and_iff_not_or_not'
theorem Decidable.or_iff_not_not_and_not [Decidable a] [Decidable b] : a b ¬(¬a ¬b) := by
rw [ not_or, not_not]
set_option linter.missingDocs false in
@[deprecated Decidable.or_iff_not_not_and_not (since := "2025-03-18")]
abbrev Decidable.or_iff_not_and_not := @Decidable.or_iff_not_not_and_not
theorem Decidable.and_iff_not_not_or_not [Decidable a] [Decidable b] : a b ¬(¬a ¬b) := by
rw [ not_and_iff_not_or_not, not_not]
set_option linter.missingDocs false in
@[deprecated Decidable.and_iff_not_not_or_not (since := "2025-03-18")]
abbrev Decidable.and_iff_not_or_not := @Decidable.and_iff_not_not_or_not
theorem Decidable.imp_iff_right_iff [Decidable a] : (a b b) a b :=
Iff.intro
(fun h => (Decidable.em a).imp_right fun ha' => h.mp fun ha => (ha' ha).elim)

View File

@@ -31,7 +31,7 @@ A restricted version of `IO` in which mutable state is the only side effect.
It is possible to run `ST` computations in a non-monadic context using `runST`.
-/
abbrev ST (σ : Type) (α : Type) := Void σ ST.Out σ α
@[expose] def ST (σ : Type) (α : Type) := Void σ ST.Out σ α
namespace ST

View File

@@ -2317,6 +2317,12 @@ Theorems tagged with the `wf_preprocess` attribute are used during the processin
by well-founded recursion. They are applied to the function's body to add additional hypotheses,
such as replacing `if c then _ else _` with `if h : c then _ else _` or `xs.map` with
`xs.attach.map`. Also see `wfParam`.
Warning: These rewrites are only applied to the declaration for the purpose of the logical
definition, but do not affect the compiled code. In particular they can cause a function definition
that diverges as compiled to be accepted without an explicit `partial` keyword, for example if they
remove irrelevant subterms or change the evaluation order by hiding terms under binders. Therefore
avoid tagging theorems with `[wf_preprocess]` unless they preserve also operational behavior.
-/
syntax (name := wf_preprocess) "wf_preprocess" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("" <|> "<- ")? (ppSpace prio)? : attr

View File

@@ -102,9 +102,6 @@ theorem fixF_eq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p :
induction acx with
| intro x r _ => exact rfl
@[deprecated fixF_eq (since := "2025-04-04")]
abbrev fixFEq := @fixF_eq
end
variable {α : Sort u} {C : α Sort v} {r : α α Prop}

View File

@@ -48,5 +48,26 @@ partial def inferMeta (decls : Array Decl) : CompilerM Unit := do
modifyEnv (setDeclMeta · decl.name)
setClosureMeta decl
/--
Checks meta availability just before `evalConst`. This is a "last line of defense" as accesses
should have been checked at declaration time in case of attributes. We do not solely want to rely on
errors from the interpreter itself as those depend on whether we are running in the server.
-/
@[export lean_eval_check_meta]
private partial def evalCheckMeta (env : Environment) (declName : Name) : Except String Unit := do
if !env.header.isModule then
return
go declName |>.run' {}
where go (ref : Name) : StateT NameSet (Except String) Unit := do
if ( get).contains ref then
return
modify (·.insert ref)
if let some localDecl := declMapExt.getState env |>.find? ref then
for ref in collectUsedFDecls localDecl do
go ref
else
if getIRPhases env ref == .runtime then
throw s!"Cannot evaluate constant `{declName}` as it uses `{ref}` which is neither marked nor imported as `meta`"
builtin_initialize
registerTraceClass `compiler.ir.inferMeta

View File

@@ -173,9 +173,9 @@ def ofLCNFLit : LCNF.LitValue → Value
-- TODO: We could make this much more precise but the payoff is questionable
| .str .. => .top
partial def proj : Value Nat Value
partial def proj (env : Environment) : Value Nat Value
| .ctor _ vs , i => vs.getD i bot
| .choice vs, i => vs.foldl (fun r v => merge r (proj v i)) bot
| .choice vs, i => vs.foldl (fun r v => widening env r (proj env v i)) bot
| v, _ => v
/--
@@ -351,8 +351,9 @@ def findArgValue (arg : Arg) : InterpM Value := do
Update the assignment of `var` by merging the current value with `newVal`.
-/
def updateVarAssignment (var : FVarId) (newVal : Value) : InterpM Unit := do
let env getEnv
let val findVarValue var
let updatedVal := .merge val newVal
let updatedVal := .widening env val newVal
modifyAssignment (·.insert var updatedVal)
/--
@@ -378,10 +379,11 @@ a partial application and set the values of the remaining parameters to
-/
def updateFunDeclParamsAssignment (params : Array Param) (args : Array Arg) : InterpM Bool := do
let mut ret := false
let env getEnv
for param in params, arg in args do
let paramVal findVarValue param.fvarId
let argVal findArgValue arg
let newVal := .merge paramVal argVal
let newVal := .widening env paramVal argVal
if newVal != paramVal then
modifyAssignment (·.insert param.fvarId newVal)
ret := true
@@ -460,7 +462,9 @@ where
interpLetValue (letVal : LetValue) : InterpM Value := do
match letVal with
| .lit val => return .ofLCNFLit val
| .proj _ idx struct => return ( findVarValue struct).proj idx
| .proj _ idx struct =>
let env getEnv
return ( findVarValue struct).proj env idx
| .const declName _ args =>
let env getEnv
args.forM handleFunArg

View File

@@ -113,30 +113,6 @@ where go (isMeta isPublic : Bool) (decl : Decl) : StateT NameSet CompilerM Unit
if let some refDecl getLocalDecl? ref then
go isMeta isPublic refDecl
/--
Checks meta availability just before `evalConst`. This is a "last line of defense" as accesses
should have been checked at declaration time in case of attributes. We do not solely want to rely on
errors from the interpreter itself as those depend on whether we are running in the server.
-/
@[export lean_eval_check_meta]
private partial def evalCheckMeta (env : Environment) (declName : Name) : Except String Unit := do
if !env.header.isModule then
return
let some decl := getDeclCore? env baseExt declName
| return -- We might not have the LCNF available, in which case there's nothing we can do
go decl |>.run' {}
where go (decl : Decl) : StateT NameSet (Except String) Unit :=
decl.value.forCodeM fun code =>
for ref in collectUsedDecls code do
if ( get).contains ref then
continue
modify (·.insert ref)
if let some localDecl := baseExt.getState env |>.find? ref then
go localDecl
else
if getIRPhases env ref == .runtime then
throw s!"Cannot evaluate constant `{declName}` as it uses `{ref}` which is neither marked nor imported as `meta`"
/--
Checks that imports necessary for inlining/specialization are public as otherwise we may run into
unknown declarations at the point of inlining/specializing. This is a limitation that we want to

View File

@@ -7,7 +7,7 @@ module
prelude
public import Init.Prelude
import Init.Data.String.Basic
import Init.Data.String.Termination
namespace String
@@ -28,24 +28,6 @@ where finally
simp only [Nat.reducePow, Nat.add_one_sub_one] at this
simp [i, UInt32.lt_iff_toNat_lt, this]; omega
def ValidPos.remainingBytes (pos : String.ValidPos s) : Nat :=
s.utf8ByteSize - pos.offset.byteIdx
theorem ValidPos.remainingBytes_next_lt_of_lt {p p' : String.ValidPos s} (h' : p' < p) :
p.remainingBytes < p'.remainingBytes := by
simp only [ValidPos.lt_iff, Pos.Raw.lt_iff] at h'
simp only [remainingBytes]
have : p.offset.byteIdx s.utf8ByteSize := p.isValid.le_rawEndPos
omega
theorem ValidPos.lt_next {p : String.ValidPos s} (h) : p < p.next h := by
simp only [next, lt_iff, Slice.Pos.offset_ofSlice, Pos.Raw.lt_iff, Slice.Pos.byteIdx_offset_next,
offset_toSlice, Nat.lt_add_right_iff_pos]
exact Char.utf8Size_pos _
theorem ValidPos.remainingBytes_next_lt (pos : String.ValidPos s) (h) :
(pos.next h).remainingBytes < pos.remainingBytes :=
remainingBytes_next_lt_of_lt (pos.lt_next h)
def mangleAux (s : String) (pos : s.ValidPos) (r : String) : String :=
if h : pos = s.endValidPos then r else
@@ -61,8 +43,7 @@ def mangleAux (s : String) (pos : s.ValidPos) (r : String) : String :=
mangleAux s pos (pushHex 4 c.val (r ++ "_u"))
else
mangleAux s pos (pushHex 8 c.val (r ++ "_U"))
termination_by pos.remainingBytes
decreasing_by all_goals apply ValidPos.remainingBytes_next_lt
termination_by pos
public def mangle (s : String) : String :=
mangleAux s s.startValidPos ""
@@ -81,41 +62,35 @@ def checkLowerHex : Nat → (s : String) → s.ValidPos → Bool
(ch.isDigit || (ch.val >= 97 && ch.val <= 102)) && -- 0-9a-f
checkLowerHex k s (pos.next h)
theorem valid_of_checkLowerHex (h : checkLowerHex n s p) :
(String.Pos.Raw.mk (p.offset.byteIdx + n)).IsValid s := by
fun_induction checkLowerHex
· rename_i p
exact p.isValid
· contradiction
· rename_i k s p hp ch ih
simp only [Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq] at h
specialize ih h.2
refine cast ?_ ih
congr 2
simp only [String.ValidPos.next, String.Slice.Pos.offset_ofSlice,
String.Slice.Pos.byteIdx_offset_next, String.ValidPos.offset_toSlice, Nat.succ_eq_add_one]
change p.offset.byteIdx + ch.utf8Size + k = _
rw [Char.utf8Size_eq_one_iff.mpr, Nat.add_assoc, Nat.add_comm 1]
rcases h.1 with h | h
· simp only [Char.isDigit, Bool.and_eq_true, decide_eq_true_eq] at h
exact UInt32.le_trans h.2 (by decide)
· exact UInt32.le_trans h.2 (by decide)
def fromHex? (c : Char) : Option Nat :=
if c.isDigit then
some (c.val - 48).toNat
else if c.val >= 97 && c.val <= 102 then
some (c.val - 87).toNat
else none
def parseLowerHex : (n : Nat) (s : String) (p : s.ValidPos)
checkLowerHex n s p Nat Nat
| 0, _, _, _, n => n
| k + 1, s, pos, h, n =>
have hpos : pos s.endValidPos := by
rw [checkLowerHex] at h
split at h <;> trivial
let ch := pos.get hpos
let pos := pos.next hpos
have h' : checkLowerHex k s pos := by
simp only [checkLowerHex, hpos, reduceDIte, ge_iff_le, Bool.and_eq_true, Bool.or_eq_true,
decide_eq_true_eq, pos] at h
exact h.2
if ch.isDigit then parseLowerHex k s pos h' (n <<< 4 ||| (ch.val - 48).toNat)
else parseLowerHex k s pos h' (n <<< 4 ||| (ch.val - 87).toNat)
def parseLowerHex? (k : Nat) (s : String) (p : s.ValidPos) (acc : Nat) :
Option (s.ValidPos × Nat) :=
match k with
| 0 => some (p, acc)
| k + 1 =>
if h : p = s.endValidPos then
none
else
match fromHex? (p.get h) with
| some d => parseLowerHex? k s (p.next h) (acc <<< 4 ||| d)
| none => none
theorem lt_of_parseLowerHex?_eq_some {k : Nat} {s : String} {p q : s.ValidPos} {acc : Nat}
{r : Nat} (hk : 0 < k) : parseLowerHex? k s p acc = some (q, r) p < q := by
fun_induction parseLowerHex? with
| case1 => simp at hk
| case2 => simp
| case3 p acc k h d x ih =>
match k with
| 0 => simpa [parseLowerHex?] using fun h _ => h p.lt_next
| k + 1 => exact fun h => String.ValidPos.lt_trans p.lt_next (ih (by simp) h)
| case4 => simp
def checkDisambiguation (s : String) (p : s.ValidPos) : Bool :=
if h : _ then
@@ -132,8 +107,7 @@ def checkDisambiguation (s : String) (p : s.ValidPos) : Bool :=
true
else false
else true
termination_by p.remainingBytes
decreasing_by apply p.remainingBytes_next_lt
termination_by p
def needDisambiguation (prev : Name) (next : String) : Bool :=
(match prev with
@@ -165,11 +139,11 @@ public def mkModuleInitializationFunctionName (moduleName : Name) : String :=
"initialize_" ++ moduleName.mangle ""
-- assumes `s` has been generated `Name.mangle n ""`
def Name.demangleAux (s : String) (p : s.ValidPos) (res : Name)
def Name.demangleAux (s : String) (p : s.ValidPos) (res : Name)
(acc : String) (ucount : Nat) : Name :=
if h : p = s.endValidPos then res.str (acc.pushn '_' (ucount / 2)) else
let ch := p.get h
let p := p.next h
if hp₀ : p = s.endValidPos then res.str (acc.pushn '_' (ucount / 2)) else
let ch := p.get hp₀
let p := p.next hp₀
if ch = '_' then demangleAux s p res acc (ucount + 1) else
if ucount % 2 = 0 then
demangleAux s p res (acc.pushn '_' (ucount / 2) |>.push ch) 0
@@ -179,31 +153,26 @@ def Name.demangleAux (s : String) (p : s.ValidPos) (res : Name)
demangleAux s (p.next h.2.1) res "" 0
else
decodeNum s p res (ch.val - 48).toNat
else if h : ch = 'x' checkLowerHex 2 s p then
let acc := acc.pushn '_' (ucount / 2)
demangleAux s _, valid_of_checkLowerHex h.2 res (acc.push (Char.ofNat (parseLowerHex 2 s p h.2 0))) 0
else if h : ch = 'u' checkLowerHex 4 s p then
let acc := acc.pushn '_' (ucount / 2)
demangleAux s _, valid_of_checkLowerHex h.2 res (acc.push (Char.ofNat (parseLowerHex 4 s p h.2 0))) 0
else if h : ch = 'U' checkLowerHex 8 s p then
let acc := acc.pushn '_' (ucount / 2)
demangleAux s _, valid_of_checkLowerHex h.2 res (acc.push (Char.ofNat (parseLowerHex 8 s p h.2 0))) 0
else
demangleAux s p (res.str acc) ("".pushn '_' (ucount / 2) |>.push ch) 0
termination_by p.remainingBytes
decreasing_by
· apply String.ValidPos.remainingBytes_next_lt
· apply String.ValidPos.remainingBytes_next_lt
· apply String.ValidPos.remainingBytes_next_lt_of_lt
(Nat.lt_trans (String.ValidPos.lt_next _) (String.ValidPos.lt_next _))
· apply String.ValidPos.remainingBytes_next_lt
· apply String.ValidPos.remainingBytes_next_lt_of_lt
(Nat.lt_trans (String.ValidPos.lt_next _) (Nat.lt_add_of_pos_right (by decide)))
· apply String.ValidPos.remainingBytes_next_lt_of_lt
(Nat.lt_trans (String.ValidPos.lt_next _) (Nat.lt_add_of_pos_right (by decide)))
· apply String.ValidPos.remainingBytes_next_lt_of_lt
(Nat.lt_trans (String.ValidPos.lt_next _) (Nat.lt_add_of_pos_right (by decide)))
· apply String.ValidPos.remainingBytes_next_lt
match ch, h₁ : parseLowerHex? 2 s p 0 with
| 'x', some (q, v) =>
let acc := acc.pushn '_' (ucount / 2)
have : p₀ < q := String.ValidPos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₁)
demangleAux s q res (acc.push (Char.ofNat v)) 0
| _, _ =>
match ch, h₂ : parseLowerHex? 4 s p 0 with
| 'u', some (q, v) =>
let acc := acc.pushn '_' (ucount / 2)
have : p₀ < q := String.ValidPos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₂)
demangleAux s q res (acc.push (Char.ofNat v)) 0
| _, _ =>
match ch, h₃ : parseLowerHex? 8 s p 0 with
| 'U', some (q, v) =>
let acc := acc.pushn '_' (ucount / 2)
have : p₀ < q := String.ValidPos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₃)
demangleAux s q res (acc.push (Char.ofNat v)) 0
| _, _ => demangleAux s p (res.str acc) ("".pushn '_' (ucount / 2) |>.push ch) 0
termination_by p₀
where
decodeNum (s : String) (p : s.ValidPos) (res : Name) (n : Nat) : Name :=
if h : p = s.endValidPos then res.num n else
@@ -215,11 +184,7 @@ where
let res := res.num n
if h : p = s.endValidPos then res else
nameStart s (p.next h) res -- assume s.get' p h = '_'
termination_by p.remainingBytes
decreasing_by
· apply String.ValidPos.remainingBytes_next_lt
· apply String.ValidPos.remainingBytes_next_lt_of_lt
(Nat.lt_trans (String.ValidPos.lt_next _) (String.ValidPos.lt_next _))
termination_by p
nameStart (s : String) (p : s.ValidPos) (res : Name) : Name :=
if h : p = s.endValidPos then res else
let ch := p.get h
@@ -233,11 +198,7 @@ where
demangleAux s p res "" 1
else
demangleAux s p res (String.singleton ch) 0
termination_by p.remainingBytes
decreasing_by
· apply String.ValidPos.remainingBytes_next_lt_of_lt
(Nat.lt_trans (String.ValidPos.lt_next _) (String.ValidPos.lt_next _))
all_goals apply String.ValidPos.remainingBytes_next_lt
termination_by p
/-- Assuming `s` has been produced by `Name.mangle _ ""`, return the original name. -/
public def Name.demangle (s : String) : Name :=

View File

@@ -508,11 +508,6 @@ def isDefinition : ConstantInfo → Bool
| .defnInfo _ => true
| _ => false
@[deprecated "May be inaccurate for theorems imported under the module system, use `Lean.getOriginalConstKind?` instead" (since := "2025-04-24")]
def isTheorem : ConstantInfo Bool
| .thmInfo _ => true
| _ => false
def inductiveVal! : ConstantInfo InductiveVal
| .inductInfo val => val
| _ => panic! "Expected a `ConstantInfo.inductInfo`."

View File

@@ -1340,7 +1340,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
throwErrorAt ref m!"{msg}{.nil}"
if eType.isForall then
match lval with
| LVal.fieldName _ fieldName suffix? fullRef =>
| LVal.fieldName ref fieldName suffix? _fullRef =>
let fullName := Name.str `Function fieldName
if ( getEnv).contains fullName then
return LValResolution.const `Function `Function fullName
@@ -1349,7 +1349,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
been a field in the `Function` namespace, so we needn't wait to check if this is actually
a constant. If `suffix?` is non-`none`, we prefer to throw the "unknown constant" error
(because of monad namespaces like `IO` and auxiliary declarations like `mutual_induct`) -/
throwInvalidFieldAt fullRef fieldName fullName
throwInvalidFieldAt ref fieldName fullName
| .fieldIdx .. =>
throwLValError e eType "Invalid projection: Projections cannot be used on functions"
else if eType.getAppFn.isMVar then
@@ -1386,7 +1386,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; {bounds}"
++ .note m!"The expression{inlineExpr e}has type{inlineExpr eType}which has only {numFields} {fields}"
++ tupleHint
| some structName, LVal.fieldName _ fieldName _ fullRef =>
| some structName, LVal.fieldName ref fieldName _ _ => withRef ref do
let env getEnv
if isStructure env structName then
if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
@@ -1402,15 +1402,15 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
-- Then search the environment
if let some (baseStructName, fullName) findMethod? structName (.mkSimple fieldName) then
return LValResolution.const baseStructName structName fullName
throwInvalidFieldAt fullRef fieldName fullName
throwInvalidFieldAt ref fieldName fullName
-- Suggest a potential unreachable private name as hint. This does not cover structure
-- inheritance, nor `import all`.
(declHint := (mkPrivateName env structName).mkStr fieldName)
| none, LVal.fieldName _ _ (some suffix) fullRef =>
| none, LVal.fieldName ref _ (some suffix) _fullRef =>
-- This may be a function constant whose implicit arguments have already been filled in:
let c := e.getAppFn
if c.isConst then
throwUnknownConstantAt fullRef (c.constName! ++ suffix)
throwUnknownConstantAt ref (c.constName! ++ suffix)
else
throwInvalidFieldNotation e eType
| _, _ => throwInvalidFieldNotation e eType
@@ -1619,7 +1619,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
let some info := getFieldInfo? ( getEnv) baseStructName fieldName | unreachable!
if ( isInaccessiblePrivateName info.projFn) then
throwError "Field `{fieldName}` from structure `{structName}` is private"
let projFn mkConst info.projFn
let projFn withRef lval.getRef <| 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 }
@@ -1629,7 +1629,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
loop f lvals
| LValResolution.const baseStructName structName constName =>
let f if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
let projFn mkConst constName
let projFn withRef lval.getRef <| mkConst constName
let projFn addProjTermInfo lval.getRef projFn
if lvals.isEmpty then
let (args, namedArgs) addLValArg baseStructName f args namedArgs projFn explicit

View File

@@ -240,9 +240,10 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
@[builtin_term_elab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ => do
-- Always allow quoting private names.
let n withoutExporting <| realizeGlobalConstNoOverloadWithInfo stx[2]
recordExtraModUseFromDecl (isMeta := false) n
return toExpr n
withoutExporting do
let n realizeGlobalConstNoOverloadWithInfo stx[2]
recordExtraModUseFromDecl (isMeta := false) n
return toExpr n
@[builtin_term_elab declName] def elabDeclName : TermElab := adaptExpander fun _ => do
let some declName getDeclName?

View File

@@ -330,11 +330,6 @@ def elabMutual : CommandElab := fun stx => do
Term.applyAttributes declName attrs
for attrName in toErase do
Attribute.erase declName attrName
if ( getEnv).isImportedConst declName && attrs.any (·.kind == .global) then
-- If an imported declaration is marked with a global attribute, there is no good way to track
-- its use generally and so Shake should conservatively preserve imports of the current
-- module.
recordExtraRevUseOfCurrentModule
@[builtin_command_elab Lean.Parser.Command.«initialize»] def elabInitialize : CommandElab
| stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ]? $doSeq) => do

View File

@@ -1087,7 +1087,7 @@ def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers :
if mainHeaders.any (·.modifiers.isNoncomputable) then .noncomputable
else if mainHeaders.any (·.modifiers.isMeta) then .meta
else .regular
recKind := if mainHeaders.any fun h => h.modifiers.isInferredPartial then RecKind.partial else RecKind.default
recKind := if mainHeaders.any fun h => h.modifiers.isPartial then RecKind.partial else RecKind.default
isUnsafe := mainHeaders.any fun h => h.modifiers.isUnsafe
}

View File

@@ -332,9 +332,8 @@ def addPreDefinitions (docCtx : LocalContext × LocalInstances) (preDefs : Array
else
-- Consider partial if `partial` was given explicitly, or implied and no termination hint
-- was given
if preDefs.any fun preDef =>
preDef.modifiers.isPartial ||
preDef.modifiers.isInferredPartial && !preDef.termination.isNotNone then
if preDefs.any (·.modifiers.isPartial) ||
preDefs.any (·.modifiers.isInferredPartial) && !preDefs.any (·.termination.isNotNone) then
let mut isPartial := true
for preDef in preDefs do
if !( whnfD preDef.type).isForall then

View File

@@ -221,8 +221,10 @@ def solveDecreasingGoals (funNames : Array Name) (argsPacker : ArgsPacker) (decr
let type goal.getType
let some ref := getRecAppSyntax? ( goal.getType)
| throwError "MVar not annotated as a recursive call:{indentExpr type}"
goal.setType type.mdataExpr!
withRef ref <| applyDefaultDecrTactic goal
| some decrTactic => withRef decrTactic.ref do
goals.forM fun goal => do goal.setType ( goal.getType).mdataExpr!
unless goals.isEmpty do -- unlikely to be empty
-- make info from `runTactic` available
goals.forM fun goal => pushInfoTree (.hole goal)

View File

@@ -130,8 +130,6 @@ private partial def quoteSyntax : Syntax → TermElabM Term
-- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation).
-- See the paper for details.
let consts resolveGlobalName val
-- Record all constants to make sure they can still be resolved after shaking imports
consts.forM fun (n, _) => recordExtraModUseFromDecl (isMeta := false) n
-- extension of the paper algorithm: also store unique section variable names as top-level scopes
-- so they can be captured and used inside the section, but not outside
let sectionVars := resolveSectionVariable ( read).sectionVars val

View File

@@ -0,0 +1,65 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Elab.Command
meta import Lean.Elab.Command
public import Lean.Data.KVMap
public section
namespace Lean.Elab
open Command Meta
/--
Generates a function `setterName` for updating the `Bool` and `Nat` fields
of the structure `struct`.
This is a very simple implementation. There is no support for subobjects.
-/
meta def mkConfigSetter (doc? : Option (TSyntax ``Parser.Command.docComment))
(setterName struct : Ident) : CommandElabM Unit := do
let structName resolveGlobalConstNoOverload struct
let .inductInfo val getConstInfo structName
| throwErrorAt struct "`{structName}` is not s structure"
unless val.levelParams.isEmpty do
throwErrorAt struct "`{structName}` is universe polymorphic"
unless val.numIndices == 0 && val.numParams == 0 do
throwErrorAt struct "`{structName}` must not be parametric"
let env getEnv
let some structInfo := getStructureInfo? env structName
| throwErrorAt struct "`{structName}` is not a structure"
let code : Term liftTermElabM do
let mut code : Term `(throwError "invalid configuration option `{fieldName}`")
for fieldInfo in structInfo.fieldInfo do
if fieldInfo.subobject?.isSome then continue -- ignore subobject's
let projInfo getConstInfo fieldInfo.projFn
let fieldType forallTelescope projInfo.type fun _ body => pure body
-- **Note**: We only support `Nat` and `Bool` fields
let fieldIdent : Ident := mkCIdent fieldInfo.fieldName
if fieldType.isConstOf ``Nat then
code `(if fieldName == $(quote fieldInfo.fieldName) then
return { s with $fieldIdent:ident := ( getNatField) }
else $code)
else if fieldType.isConstOf ``Bool then
code `(if fieldName == $(quote fieldInfo.fieldName) then
return { s with $fieldIdent:ident := ( getBoolField) }
else $code)
return code
let cmd `(command|
$[$doc?:docComment]?
def $setterName (s : $struct) (fieldName : Name) (val : DataValue) : CoreM $struct :=
let getBoolField : CoreM Bool := do
let .ofBool b := val | throwError "`{fieldName}` is a Boolean"
return b
let getNatField : CoreM Nat := do
let .ofNat n := val | throwError "`{fieldName}` is a natural number"
return n
$code
)
elabCommand cmd
elab (name := elabConfigGetter) doc?:(docComment)? "declare_config_getter" setterName:ident type:ident : command => do
mkConfigSetter doc? setterName type
end Lean.Elab

View File

@@ -11,3 +11,4 @@ public import Lean.Elab.Tactic.Grind.BuiltinTactic
public import Lean.Elab.Tactic.Grind.ShowState
public import Lean.Elab.Tactic.Grind.Have
public import Lean.Elab.Tactic.Grind.Trace
public import Lean.Elab.Tactic.Grind.Config

View File

@@ -379,7 +379,7 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM
-- **Note**: We use `withCheapCasesOnly` to ensure multiple goals are not created.
-- We will add support for this case in the future.
let (goal, _) withCheapCasesOnly <| SearchM.run goal do
intros 0
intros 0; discard <| assertAll
getGoal
let goals := if goal.inconsistent then [] else [goal]
let ctx readThe Meta.Grind.Context

View File

@@ -25,6 +25,7 @@ import Lean.Elab.Tactic.Basic
import Lean.Elab.Tactic.RenameInaccessibles
import Lean.Elab.Tactic.Grind.Filter
import Lean.Elab.Tactic.Grind.ShowState
import Lean.Elab.Tactic.Grind.Config
import Lean.Elab.SetOption
namespace Lean.Elab.Tactic.Grind
@@ -102,6 +103,7 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
let progress k
unless progress do
throwError "`{tacticName}` failed"
processNewFacts
unless ( Grind.getConfig).verbose do
return ()
if ( get).inconsistent then
@@ -280,8 +282,9 @@ def logAnchor (e : Expr) : TermElabM Unit := do
throwError "`cases` tactic failed, invalid anchor"
goal.withContext <| withRef anchor <| logAnchor e
let goals goals.filterMapM fun goal => do
let goal := { goal with ematch.num := 0 }
let (goal, _) liftGrindM <| SearchM.run goal do
intros genNew
intros genNew; discard <| assertAll
getGoal
if goal.inconsistent then
return none
@@ -427,4 +430,20 @@ where
let options Elab.elabSetOption stx[1] stx[3]
withOptions (fun _ => options) do evalGrindTactic stx[5]
@[builtin_grind_tactic setConfig] def elabSetConfig : GrindTactic := fun stx => do
let `(grind| set_config $[$items:configItem]* in $seq:grindSeq) := stx | throwUnsupportedSyntax
let config := ( read).ctx.config
let config elabConfigItems config items
withReader (fun c => { c with ctx.config := config }) do
evalGrindTactic seq
@[builtin_grind_tactic mbtc] def elabMBTC : GrindTactic := fun _ => do
liftGoalM do
discard <| Solvers.check
if ( get).inconsistent then
return ()
let progress Solvers.mbtc
unless progress do
throwError "`mbtc` tactic failed to generate new candidate case-splits."
end Lean.Elab.Tactic.Grind

View File

@@ -0,0 +1,32 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.CoreM
meta import Lean.Elab.Tactic.ConfigSetter
public section
namespace Lean.Elab.Tactic.Grind
/-- Sets a field of the `grind` configuration object. -/
declare_config_getter setConfigField Grind.Config
def elabConfigItems (init : Grind.Config) (items : Array (TSyntax `Lean.Parser.Tactic.configItem))
: CoreM Grind.Config := do
let mut config := init
for item in items do
match item with
| `(Lean.Parser.Tactic.configItem| ($fieldName:ident := true))
| `(Lean.Parser.Tactic.configItem| +$fieldName:ident) =>
config setConfigField config fieldName.getId true
| `(Lean.Parser.Tactic.configItem| ($fieldName:ident := false))
| `(Lean.Parser.Tactic.configItem| -$fieldName:ident) =>
config setConfigField config fieldName.getId false
| `(Lean.Parser.Tactic.configItem| ($fieldName:ident := $val:num)) =>
config setConfigField config fieldName.getId (.ofNat val.getNat)
| _ => throwErrorAt item "unexpected configuration option"
return config
end Lean.Elab.Tactic.Grind

View File

@@ -6,18 +6,10 @@ Authors: Leonardo de Moura
module
prelude
public import Lean.Elab.Tactic.Grind.Basic
public import Lean.Meta.Tactic.Grind.Filter
import Init.Grind.Interactive
namespace Lean.Elab.Tactic.Grind
open Meta
public inductive Filter where
| true
| const (declName : Name)
| fvar (fvarId : FVarId)
| gen (pred : Nat Bool)
| or (a b : Filter)
| and (a b : Filter)
| not (a : Filter)
open Meta Grind
public partial def elabFilter (filter? : Option (TSyntax `grind_filter)) : GrindTacticM Filter := do
let some filter := filter? | return .true
@@ -44,27 +36,4 @@ where
| `(grind_filter| gen != $n:num) => let n := n.getNat; return .gen fun x => x != n
| _ => throwUnsupportedSyntax
open Meta.Grind
-- **Note**: facts may not have been internalized if they are equalities.
def getGen (e : Expr) : GoalM Nat := do
if ( alreadyInternalized e) then
getGeneration e
else match_expr e with
| Eq _ lhs rhs => return max ( getGeneration lhs) ( getGeneration rhs)
| _ => return 0
public def Filter.eval (filter : Filter) (e : Expr) : GoalM Bool := do
go filter
where
go (filter : Filter) : GoalM Bool := do
match filter with
| .true => return .true
| .and a b => go a <&&> go b
| .or a b => go a <||> go b
| .not a => return !( go a)
| .const declName => return Option.isSome <| e.find? fun e => e.isConstOf declName
| .fvar fvarId => return Option.isSome <| e.find? fun e => e.isFVar && e.fvarId! == fvarId
| .gen pred => let gen getGen e; return pred gen
end Lean.Elab.Tactic.Grind

View File

@@ -35,8 +35,7 @@ def elabGrindPattern : CommandElab := fun stx => do
| _ => throwUnsupportedSyntax
where
go (thmName : TSyntax `ident) (terms : Syntax.TSepArray `term ",") (kind : AttributeKind) : CommandElabM Unit := liftTermElabM do
let declName resolveGlobalConstNoOverload thmName
discard <| addTermInfo thmName ( mkConstWithLevelParams declName)
let declName realizeGlobalConstNoOverloadWithInfo thmName
let info getConstVal declName
forallTelescope info.type fun xs _ => do
let patterns terms.getElems.mapM fun term => do
@@ -121,7 +120,9 @@ def elabGrindParams
| none => pure <| .ematch (.default false)
match attr with
| .ematch kind =>
params addEMatchTheorem params (mkIdent p.name) p.name kind false
try
params addEMatchTheorem params (mkIdent p.name) p.name kind false (warn := false)
catch _ => pure () -- Don't worry if premise suggestion gave bad suggetions.
| _ =>
-- We could actually support arbitrary grind modifiers,
-- and call `processParam` rather than `addEMatchTheorem`,
@@ -185,7 +186,8 @@ where
-- If it is an inductive predicate,
-- we also add the constructors (intro rules) as E-matching rules
for ctor in info.ctors do
params withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
-- **Note**: We should not warn if `declName` is an inductive
params withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False)
else
params withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
| .symbol prio =>
@@ -195,7 +197,7 @@ where
addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name)
(kind : Grind.EMatchTheoremKind)
(minIndexable : Bool) (suggest : Bool := false) : MetaM Grind.Params := do
(minIndexable : Bool) (suggest : Bool := false) (warn := true) : MetaM Grind.Params := do
let info getAsyncConstInfo declName
match info.kind with
| .thm | .axiom | .ctor =>
@@ -204,7 +206,8 @@ where
ensureNoMinIndexable minIndexable
let thm₁ Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios
let thm₂ Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios
if params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
if warn &&
params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then
warnRedundantEMatchArg params.ematch declName
return { params with extra := params.extra.push thm₁ |>.push thm₂ }
@@ -215,7 +218,7 @@ where
Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
else
Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
if params.ematch.containsWithSamePatterns thm.origin thm.patterns then
if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns then
warnRedundantEMatchArg params.ematch declName
return { params with extra := params.extra.push thm }
| .defn =>
@@ -356,6 +359,8 @@ private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (
elabGrindConfig config
@[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
-- Preserve this import in core; all others import `Init` anyway
recordExtraModUse (isMeta := false) `Init.Grind.Tactics
match stx with
| `(tactic| grind $config:optConfig $[only%$only]? $[ [$params:grindParam,*] ]? $[=> $seq:grindSeq]?) =>
let interactive := seq.isSome

View File

@@ -20,7 +20,8 @@ def withTracing (x : GrindTacticM α) : GrindTacticM α := do
def mkFinish (maxIterations : Nat) : IO Action := do
let solvers Solvers.mkAction
return Action.checkTactic >> (Action.done <|> solvers <|> Action.instantiate <|> Action.splitNext).loop maxIterations
let step : Action := Action.done <|> solvers <|> Action.instantiate <|> Action.splitNext <|> Action.mbtc
return Action.checkTactic (warnOnly := true) >> step.loop maxIterations
def maxIterations := 1000 -- **TODO**: Add option

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