This PR adds a benchmark for the persistent hashmap, in particular also
covering the non
linear insert case which is often hit in practical uses. Furthermore the
same test case is also
added to the treemap benchmark.
This PR makes `mframe`, `mspec` and `mvcgen` respect hygiene.
Inaccessible stateful hypotheses can now be named with a new tactic
`mrename_i` that works analogously to `rename_i`.
This PR surfaces kernel diagnostics even in `example`.
The problem was that the kernel checking happens asynchronously. We
cannot use `reportDiag` in `addDecl`, which spawns that task, due to the
module hierarchy. For non `example`-declaration, `reportDiag` is called
somewhere else later, but for `example`, the `withoutModifyingEnv` in
`elabMutualDef` hid the kernel diagnostics. (But only the kernel
diagnostics; they are in the `Environment`, while the others are in the
`State`).
I also observed that the `reportDiag` in `elabAsync` (but not in
`elabSync`) duplicated the reporting, so without `elab.Async true` you
get the message twice. To fix this, `reportDiag` now resets the
diagnostics. This should avoid reporting counts twice in general (at
least within a linear use of the state).
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR removes vestigial syntax definitions in
`Lean.Elab.Tactic.Do.VCGen` that when imported undefine the `mvcgen`
tactic. Now it should be possible to import Mathlib and still use
`mvcgen`.
This PR adds a few more `*.by_wp` "adequacy theorems" that allows to
prove facts about programs in `ReaderM` and `ExceptM` using the `Std.Do`
framework.
This PR adds a `HPow \a Int \a` field to `Lean.Grind.Field`, and
sufficient axioms to connect it to the operations, so that in future we
can reason about exponents in `grind`. To avoid collisions, we also move
the `HPow \a Nat \a` field in `Semiring` from the extends clause to a
field. Finally, we add some failing tests about normalizing exponents.
This PR makes cdot function expansion take hygiene information into
account, fixing "parenthesis capturing" errors that can make erroneous
cdots trigger cdot expansion in conjunction with macros. For example,
given
```lean
macro "baz% " t:term : term => `(1 + ($t))
```
it used to be that `baz% ·` would expand to `1 + fun x => x`, but now
the parentheses in `($t)` do not capture the cdot. We also fix an
oversight where cdot function expansion ignored the fact that type
ascriptions and tuples were supposed to delimit expansion, and also now
the quotation prechecker ignores the identifier in `hygieneInfo`. (#9491
added the hygiene information to the parenthesis and cdot syntaxes.)
This fixes a bug discovered by [Google
DeepMind](https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html),
which made use of `useλy . x=>y.rec λS p=>?_`. The `use` tactic from
Mathlib wrapped the provided term in a type ascription, and so this was
equivalent to `use fun x => λy x x=>y.rec λS p=>?_`. (Note that cdot
function expansion is not able to take into account *where* the cdots
are located, and it is syntactically valid to insert an identifier into
the binder list like this. If we ever want to address this in the
future, we could have cdots expand into a special term that wraps an
identifier that evaluates to a local, but which would cause errors in
other contexts.)
Design note: we put the `hygieneInfo` on the open parenthesis rather
than at the end, since that way the hygiene information is available
even when there are parsing errors. This is important since we rely on
being able to elaborate partial syntax to get elab info (e.g. in `(a.`
to get completion info). Note that syntax matchers check that the
`hygieneInfo` is actually present, so such partial syntax would not be
matched.
This PR adds a feature where `structure` constructors can override the
inferred binder kinds of the type's parameters. In the following, the
`(p)` binder on `toLp` causes `p` to be an explicit parameter to
`WithLp.toLp`:
```lean
structure WithLp (p : Nat) (V : Type) where toLp (p) ::
ofLp : V
```
This reflects the syntax of the feature added in #7742 for overriding
binder kinds of structure projections. Similarly, only those parameters
in the header of the `structure` may be updated; it is an error to try
to update binder kinds of parameters included via `variable`.
Closes#9072.
Fixes a possible bug from stale caches when creating the type of the
constructor.
This PR resolves an issue where the `Meta.Context.configKey` field is
private but we still want to use the constructor of the structure for
setting other fields, which would be prevented by the module system
checks:
```lean
structure Context where
private config : Config := {}
private configKey : UInt64 := config.toKey
...
def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
-- cannot call private constructor of `Meta.Context`!
(·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })
```
Instead, the private field is extracted into an (existing) structure
that applies its default value:
```lean
/-- Configuration with key produced by `Config.toKey`. -/
structure ConfigWithKey where
private mk ::
config : Config := {}
key : UInt64 := config.toKey
structure Context where
keyedConfig : ConfigWithKey := default
```
Thus `Context`'s constructor remains public without exposing a way to
set `key` directly.
This PR fixes a kernel type mismatch that occurs when using `grind` on
goals containing non-standard `OfNat.ofNat` terms. For example, in issue
#9477, the `0` in the theorem `range_lower` has the form:
```lean
(@OfNat.ofNat
(Std.PRange.Bound (Std.PRange.RangeShape.lower (Std.PRange.RangeShape.mk Std.PRange.BoundShape.closed Std.PRange.BoundShape.open)) Nat)
(nat_lit 0)
(instOfNatNat (nat_lit 0)))
```
instead of the more standard form:
```lean
(@OfNat.ofNat
Nat
(nat_lit 0)
(instOfNatNat (nat_lit 0)))
```
Closes#9477
This PR improves the `evalInt?` function, which is used to evaluate
configuration parameters from the `ToInt` type class. This PR also adds
a new `evalNat?` function for handling the `IsCharP` type class, and
introduces a configuration option:
```
grind (exp := <num>)
```
This option controls the maximum exponent size considered during
expression evaluation. Previously, `evalInt?` used `whnf`, which could
run out of stack space when reducing terms such as `2^1024`.
closes#9427
This PR adds `binrel%` macros for `!=` and `≠` notation defined in
`Init.Core`. This allows the elaborator to insert coercions on both
sides of the relation, instead of committing to the type on the left
hand side.
I first discovered this bug while working on Brouwer's fixed point
theorem. See the discussion on Zulip at [#lean4 > Elaboration of
`≠` @
💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elaboration.20of.20.60.E2.89.A0.60/near/526236907).
This PR replaces the proof of the simplification lemma `Nat.zero_mod`
with
`rfl` since it is, by design, a definitional equality. This solves an
issue
whereby the lemma could not be used by the simplifier when in 'dsimp'
mode.
Closes#9389
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR introduces tactic `mleave` that leaves the `SPred` proof mode by
eta expanding through its abstractions and applying some mild
simplifications. This is useful to apply automation such as `grind`
afterwards.
Relates to #9363.
This PR adds support in the `mintro` tactic for introducing `let`/`have`
binders in stateful targets, akin to `intro`. This is useful when
specifications introduce such let bindings.
Closes#9365.
This PR makes `PProdN.reduceProjs` also look for projection functions.
Previously, all redexes were created by the functions in `PProdN`, which
used primitive projections. But with `mkAdmProj` the projection
functions creep in via the types of the `admissible_pprod_fst` theorem.
So let's just reduce both of them.
Fixes#9462.
