This PR add instances showing that the Grothendieck (i.e. additive)
envelope of a semiring is an ordered ring if the original semiring is
ordered (and satisfies ExistsAddOfLE), and in this case the embedding is
monotone.
This PR improves the case splitting strategy used in `grind`, and
ensures `grind` also considers simple `match`-conditions for
case-splitting. Example:
```lean
example (x y : Nat)
: 0 < match x, y with
| 0, 0 => 1
| _, _ => x + y := by -- x or y must be greater than 0
grind
```
This PR changes `toLCNF` to stop caching translations of expressions
upon seeing an expression marked `never_extract`. This is more
coarse-grained than it needs to be, but it is difficult to do any
better, as the new compiler's `Expr` cache is based on structural
identity (rather than the pointer identity of the old compiler).
The newly added `tests/compiler/never_extract.lean` is also converted
into a `run` tests, because during development I found the order of the
output to `stderr` to be a bit finicky. The reason for making it a
`compiler` test in the first place is that closed term decls work
slightly differently between native code and the interpreter, and it
would be good to test both, but we already have separate tests for
`never_extract` and closed term extraction.
Fixes#8944.
This PR adds a procedure that efficiently transforms `let` expressions
into `have` expressions (`Meta.letToHave`). This is exposed as the
`let_to_have` tactic.
It uses the `withTrackingZetaDelta` technique: the expression is
typechecked, and any `let` variables that don't enter the zeta delta set
are nondependent. The procedure uses a number of heuristics to limit the
amount of typechecking performed. For example, it is ok to skip
subexpressions that do not contain fvars, mvars, or `let`s.
This PR implements support for normalization for commutative semirings
that do not implement `AddRightCancel`. Examples:
```lean
variable (R : Type u) [CommSemiring R]
example (a b c : R) : a * (b + c) = a * c + b * a := by grind
example (a b : R) : (a + b)^2 = a^2 + 2 * a * b + b^2 := by grind
example (a b : R) : (a + 2 * b)^2 = a^2 + 4 * a * b + 4 * b^2 := by grind
example (a b : R) : (a + 2 * b)^2 = 4 * b^2 + b * 4 * a + a^2 := by grind
```
This PR fixes the handling of the `never_extract` attribute in the
compiler's CSE pass. There is an interesting debate to be had about
exactly how hard the compiler should try to avoid duplicating anything
that transitively uses `never_extract`, but this is the simplest form
and roughly matches the check in the old compiler (although due to
different handling of local function decls in the two compilers, the
consequences might be slightly different).
This gets half of the way to #8944.
This PR adds support to the server for the new module setup process by
changing how `lake setup-file` is used.
In the new server setup, `lake setup-file` is invoked with the file name
of the edited module passed as a CLI argument and with the parsed header
passed to standard input in JSON form. Standard input is used to avoid
potentially exceeding the CLI length limits on Windows. Lake will build
the module's imports along with any other dependencies and then return
the module's workspace configuration via JSON (now in the form of
`ModuleSetup`). The server then post-processes this configuration a bit
and returns it back to the Lean language processor.
The server's header is currently only fully respected by Lake for
external modules (files that are not part of any workspace library). For
workspace modules, the saved module header is currently used to build
imports (as has been done since #7909). A follow-up Lake PR will align
both cases to follow the server's header.
Lean search paths (e.g., `LEAN_PATH`, `LEAN_SRC_PATH`) are no longer
negotiated between the server and Lake. These environment variables are
already configured during sever setup by `lake serve` and do not change
on a per-file basis. Lake can also pre-resolve the `.olean` files of
imports via the `importArts` field of `ModuleSetup`, limiting the
potential utility of communicating `LEAN_PATH`.
This PR skips attempting to compute a module name from the file name and
root directory (i.e., `lean -R`) if a name is already provided via `lean
--setup`.
This is accomplished by porting the rest of the frontend code in the
`try` block to Lean.
This PR adds explanations for a few errors concerning noncomputability,
redundant match alternatives, and invalid inductive declarations.
These adopt a lower-case error naming style, which is also applied to
existing error explanation tests.
This PR allows `simp` to recognize and warn about simp lemmas that are
likely looping in the current simp set. It does so automatically
whenever simplification fails with the dreaded “max recursion depth”
error fails, but it can be made to do it always with `set_option
linter.loopingSimpArgs true`. This check is not on by default because it
is somewhat costly, and can warn about simp calls that still happen to
work.
This closes#5111. In the end, this implemented much simpler logic than
described there (and tried in the abandoned #8688; see that PR
description for more background information), but it didn’t work as well
as I thought. The current logic is:
“Simplify the RHS of the simp theorem, complain if that fails”.
It is a reasonable policy for a Lean project to say that all simp
invocation should be so that this linter does not complain. Often it is
just a matter of explicitly disabling some simp theorems from the
default simp set, to make it clear and robust that in this call, we do
not want them to trigger. But given that often such simp call happen to
work, it’s too pedantic to impose it on everyone.
This PR adds the `+generalize` option to the `let` and `have` syntaxes.
For example, `have +generalize n := a + b; body` replaces all instances
of `a + b` in the expected type with `n` when elaborating `body`. This
can be likened to a term version of the `generalize` tactic. One can
combine this with `eq` in `have +generalize (eq := h) n := a + b; body`
as an analogue of `generalize h : n = a + b`.
This PR finishes post-stage0-cleanup after #8914 and #8929. Also:
- adds configuration options for `haveI` and `letI` terms.
- adds `letConfig` parser alias
This PR implements first-class support for nondependent let expressions
in the elaborator; recall that a let expression `let x : t := v; b` is
called *nondependent* if `fun x : t => b` typechecks, and the notation
for a nondependent let expression is `have x := v; b`. Previously we
encoded `have` using the `letFun` function, but now we make use of the
`nondep` flag in the `Expr.letE` constructor for the encoding. This has
been given full support throughout the metaprogramming interface and the
elaborator. Key changes to the metaprogramming interface:
- Local context `ldecl`s with `nondep := true` are generally treated as
`cdecl`s. This is because in the body of a `have` expression the
variable is opaque. Functions like `LocalDecl.isLet` by default return
`false` for nondependent `ldecl`s. In the rare case where it is needed,
they take an additional optional `allowNondep : Bool` flag (defaults to
`false`) if the variable is being processed in a context where the value
is relevant.
- Functions such as `mkLetFVars` by default generalize nondependent let
variables and create lambda expressions for them. The
`generalizeNondepLet` flag (default true) can be set to false if `have`
expressions should be produced instead. **Breaking change:** Uses of
`letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet :=
false`. See the next item.
- There are now some mapping functions to make telescoping operations
more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`.
There is also `mapLetDecl` as a counterpart to `withLetDecl` for
creating `let`/`have` expressions.
- Important note about the `generalizeNondepLet` flag: it should only be
used for variables in a local context that the metaprogram "owns". Since
nondependent let variables are treated as constants in most cases, the
`value` field might refer to variables that do not exist, if for example
those variables were cleared or reverted. Using `mapLetDecl` is always
fine.
- The simplifier will cache its let dependence calculations in the
nondep field of let expressions.
- The `intro` tactic still produces *dependent* local variables. Given
that the simplifier will transform lets into haves, it would be
surprising if that would prevent `intro` from creating a local variable
whose value cannot be used.
Note that nondependence of lets is not checked by the kernel. To
external checker authors: If the elaborator gets the nondep flag wrong,
we consider this to be an elaborator error. Feel free to typecheck `letE
n t v b true` as if it were `app (lam n t b default) v` and please
report issues.
This PR follows up from #8751, which made sure the nondep flag was
preserved in the C++ interface.
This PR is a followup to #8914, fixing an oversight where
`letIdDeclBinders` is was not updated with the new format. This relies
on some bootstrapping code to stay in place, but we do bootstrap cleanup
that is currently possible.
This PR adds a linter (`linter.unusedSimpArgs`) that complains when a
simp argument (`simp [foo]`) is unused. It should do the right thing if
the `simp` invocation is run multiple times, e.g. inside `all_goals`. It
does not trigger when the `simp` call is inside a macro. The linter
message contains a clickable hint to remove the simp argument.
I chose to display a separate warning for each unused argument. This
means that the user has to click multiple times to remove all of them
(and wait for re-elaboration in between). But this just means multiple
endorphine kicks, and the main benefit over a single warning that would
have to span the whole argument list is that already the squigglies tell
the users about unused arguments.
This closes#4483.
Making Init and Std clean wrt to this linter revealed close to 1000
unused simp args, a pleasant experience for anyone enjoying tidying
things: #8905
The `.impure` LCNF `Phase` is not currently used, but was intended for a
potential future where the current `IR` passes (which operate on a
highly impure representation) were rewritten to operate on LCNF instead.
For several reasons, I don't think this is very likely to happen, and
instead we are more likely to remove some of the unnecessary differences
between LCNF and IR while keeping them distinct.
This PR modifies `let` and `have` term syntaxes to be consistent with
each other. Adds configuration options; for example, `have` is
equivalent to `let +nondep`, for *nondependent* lets. Other options
include `+usedOnly` (for `let_tmp`), `+zeta` (for `letI`/`haveI`), and
`+postponeValue` (for `let_delayed)`. There is also `let (eq := h) x :=
v; b` for introducing `h : x = v` when elaborating `b`. The `eq` option
works for pattern matching as well, for example `let (eq := h) (x, y) :=
p; b`.
Future PRs will add these options to tactic syntax, once a stage0 update
has been done.
This PR implements support for (commutative) semirings in `grind`. It
uses the Grothendieck completion to construct a (commutative) ring
`Lean.Grind.Ring.OfSemiring.Q α` from a (commutative) semiring `α`. This
construction is mostly useful for semirings that implement
`AddRightCancel α`. Otherwise, the function `toQ` is not injective.
Examples:
```lean
example (x y : Nat) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
grind
example [CommSemiring α] [AddRightCancel α] (x y : α) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
grind
example (a b : Nat) : 3 * a * b = a * b * 3 := by grind
example (k z : Nat) : k * (z * 2 * (z * 2 + 1)) = z * (k * (2 * (z * 2 + 1))) := by grind
example [CommSemiring α] [AddRightCancel α] [IsCharP α 0] (x y : α)
: x^2*y = 1 → x*y^2 = y → x + y = 1 → False := by
grind
```
This PR makes `simp` consult its own cache more often, to avoid
replicating work.
Before, the simp cache was checked upon entry of `simpImpl` only, which
then calls `simpLoop`, which recursively iterates the `pre`-lemmas,
without checking the cache again.
Now, `simpLoop` itself checks the cache. This seems more principled,
given that `simpLoop` is actually putting entries into the cache for
each of its calls, so it’s more uniform if it checks the cache itself.
This avoids repeated rewrites. For example given
```
theorem ab : a = b := testSorry
theorem bc : b = c := testSorry
example (h : P c) : P b ∧ P a := by simp [ab, bc, h]
```
simp would rewrite `b ==> c` twice (once as part of `b ==> c` and then
again as part of `a ==> b ==> c`). And it’d be order dependent: With
```
example (h : P c) : P a ∧ P b := by simp [ab, bc, h]
```
the `a ==> b ==> c` chain would insert `b ==> c` into the cache, and
picked up by `simpImpl` when rewriting `P b`.
With this change, `b ==> c` is performed only once in both examples.
Instruction counts on stdlib and mathlib both show a mild improvement
across the board (0.5%), with individual modules improving by up to 4%
in stdlib and even more in mathlib.
(This does not check the cache before applying `post`, which explains
where there are still some repeated rewrites in the trace logs. But I’m
less sure about inserting a cache check here and so I am treading
carefully here. It’s also going to be at most one `post` application
that’s duplicated, because if `post` returns `.visit`, we go back to
`pre` and thus a cache check.)
This PR refactors the way simp arguments are elaborated: Instead of
changing the `SimpTheorems` structure as we go, this elaborates each
argument to a more declarative description of what it does, and then
apply those. This enables more interesting checks of simp arguments that
need to happen in the context of the eventually constructed simp context
(the checks in #8688), or after simp has run (unused argument linter
#8901).
The new data structure describing an elaborated simp argument isn’t the
most elegant, but follows from the code.
While I am at it, move handling of `[*]` into `elabSimpArgs`. Downstream
adaption branches exist (but may not be fully up to date because of the
permission changes).
While I am at it, I cleaned up `SimpTheorems.lean` file a bit (sorting
declarations, mild renaming) and added documentation.
This PR make sure that the local instance cache calculation applies more
reductions. In #2199 there was an issue where metavariables could
prevent local variables from being considered as local instances. We use
a slightly different approach that ensures that, for example, `let`s at
the ends of telescopes do not cause similar problems. These reductions
were already being calculated, so this does not require any additional
work to be done.
Metaprogramming interface addition: the various forall telescope
functions that do reduction now have a `whnfType` flag (default false).
If it's true, then the callback `k` is given the WHNF of the type. This
is a free operation, since the telescope function already computes it.
This PR refactors `Lean.Grind.NatModule/IntModule/Ring.IsOrdered`.
We ensure the the diamond from `Ring` to `NatModule` via either
`Semiring` or `IntModule` is defeq, which was not previously the case.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This PR corrects the pretty printing of `grind` modifiers. Previously
`@[grind →]` was being pretty printed as `@[grind→ ]` (Space on the
right of the symbol, rather than left.) This fixes the pretty printing
of attributes, and preserves the presence of spaces after the symbol in
the output of `grind?`.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This PR implements a `finally` section following a (potentially empty)
`where` block. `where ... finally` opens a tactic sequence block in
which the goals are the unassigned metavariables from the definition
body and its auxiliary definitions that arise from use of `let rec` and
`where`.
This can be useful for discharging multiple proof obligations in the
definition body by a single invocation of a tactic such as `all_goals`:
```lean
example (i j : Nat) (xs : Array Nat) (hi : i < xs.size) (hj: j < xs.size) :=
match i with
| 0 => x
| _ => xs[i]'?_ + xs[j]'?_
where x := 13
finally all_goals assumption
```
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR adds a logic of stateful predicates `SPred` to `Std.Do` in order
to support reasoning about monadic programs. It comes with a dedicated
proof mode the tactics of which are accessible by importing
`Std.Tactic.Do`.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
Although `HEq` was abbreviated as `≍` in #8503, many instances of the
form `HEq x y` still remain.
Therefore, I searched for occurrences of `HEq x y` using the regular
expression `(?<![A-Za-z/@]|``)HEq(?![A-Za-z.])` and replaced as many as
possible with the form `x ≍ y`.
This PR improves the error messages produced by `end` and prevents
invalid `end` commands from closing scopes on failure.
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR adds support for throwing named errors with associated error
explanations. In particular, it adds elaborators for the syntax defined
in #8649, which use the error-explanation infrastructure added in #8651.
This includes completions, hovers, and jump-to-definition for error
names.
Note that another stage0 rebuild will be required to define explanations
using `register_error_explanation`.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
