Moves the `@[coe]` attribute and associated elaborators/delaborators
from Std to Lean.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
The `push_cast` tactic in Std currently uses a copy-paste version of
`mkSimpContext` that allows overriding `getSimpTheorems`. However it has
been diverging from the version in Lean.
This is one way of generalizing `mkSimpContext` in Lean to allow what is
needed downstream., but I'm not at all set on this one. As far as I can
see there are no other tactics currently using this.
`push_cast` itself just replaces `getSimpTheorems` with
`pushCastExt.getTheorems`, where `pushCastExt` is a simp extension. If
there is another approach that suits that situation it would be fine.
I've tested that the change in this PR works downstream.
This is used in the "Try this:" widget machinery powering `simp?`.
There is a test file in Std, which I am not upstreaming at the same
time, as that relies on more code actions / #guard_msgs material. That
test file will still of course test things from Std, and later it can be
reunited with the code it is testing.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This does not completely empty `Std.Lean.Name`, as working out how to
document the difference between `Name.isInternalDetail` and
`Name.isImplementationDetail` requires further thought.
The induction principle used by `induction` may have explicit parameters
that are
not motive, target or “real” alternatives (that have the `motive` as
conclusion), e.g. restrictions on the `motive` or other parameters.
Previously, `induction` would treat them as normal alternatives, and try
to re-introduce the automatically reverted hypotheses. But this only
works when the `motive` is actually the conclusion in the type of that
alternative.
We now pay attention to that, thread that information through, and only
revert when needed.
Fixes#3212.
Implements the pretty printer option `pp.numericTypes` for including a
type ascription for numeric literals. For example, `(2 : Nat)`, `(-2 :
Int)`, and `(-2 / 3 : Rat)`. This is useful for debugging how arithmetic
expressions have elaborated or have been otherwise transformed. For
example, with exponentiation is is helpful knowing whether it is `x ^ (2
: Nat)` or `x ^ (2 : Real)`. This is like the Lean 3 option
`pp.numeralTypes` but it has a wider notion of a numeric literal.
Also implements the pretty printer option `pp.natLit` for including the
`nat_lit` prefix for raw natural number literals.
Closes#3021
When we declare a `simp` set using `register_simp_attr`, we
automatically create `simproc` set. However, users may create `simp`
sets programmatically, and the associated `simproc` set may be missing
and vice-versa.
Before this commit, `Simproc`s were defined as `Expr -> SimpM (Option Step)`, where `Step` is inductively defined as follows:
```
inductive Step where
| visit : Result → Step
| done : Result → Step
```
Here, `Result` is a structure containing the resulting expression and a proof demonstrating its equality to the input. Notably, the proof is optional; in its absence, `simp` assumes reflexivity.
A simproc can:
- Fail by returning `none`, indicating its inapplicability. In this case, the next suitable simproc is attempted, along with other simp extensions.
- Succeed and invoke further simplifications using the `.visit`
constructor. This action returns control to the beginning of the
simplification loop.
- Succeed and indicate that the result should not undergo further
simplifications. However, I find the current approach unsatisfactory, as it does not align with the methodology employed in `Transform.lean`, where we have the type:
```
inductive TransformStep where
/-- Return expression without visiting any subexpressions. -/
| done (e : Expr)
/--
Visit expression (which should be different from current expression) instead.
The new expression `e` is passed to `pre` again.
-/
| visit (e : Expr)
/--
Continue transformation with the given expression (defaults to current expression).
For `pre`, this means visiting the children of the expression.
For `post`, this is equivalent to returning `done`. -/
| continue (e? : Option Expr := none)
```
This type makes it clearer what is going on. The new `Simp.Step` type is similar but use `Result` instead of `Expr` because we need a proof.
Modifies the structure instance elaborator to
1. Fill in missing fields from sources in strict left-to-right order. In
`{a, b with}`, sometimes the elaborator
would ignore `a` even if both `a` and `b` provided the same field,
depending on what subobject fields they had.
2. Use the sources, or subobjects of the sources, to fill in entire
subobjects of the target structure as much as possible.
Currently, a field cannot be filled directly by a source itself
resulting in the term being eta expanded.
This change avoids this unnecessary and surprisingly costly extra eta
expansion.
Adds two new tests to illustrate the performance benefit (one courtesy
@semorrison). These are currently failing on master and succeed on this
branch.
There is one additional test to exercise the changes to the elaboration
of structure instances.
Changes to make mathlib build are in leanprover-community/mathlib4#9843
Closes#2451
This replaces the no-op `unusedVariablesIgnoreFnsExt` environment
extension with an actual environment extension which can be extended
using either `@[unused_variables_ignore_fn]` or
`@[builtin_unused_variables_ignore_fn]` (although for the present all
the builtin `unused_variables_ignore_fn`s are being added using direct
calls to `builtin_initialize addBuiltinUnusedVariablesIgnoreFn`, because
this also works and a stage0 update is required before the attribute can
be used).
We would like to use this attribute to disable unused variables in
syntaxes defined in std and mathlib, like
[`proof_wanted`](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Unused.20variables.20and.20proof_wanted/near/408554690).
This PR adds two new delaboration settings: `pp.deepTerms : Bool`
(default: `true`) and `pp.deepTerms.threshold : Nat` (default: `20`).
Setting `pp.deepTerms` to `false` will make the delaborator terminate
early after `pp.deepTerms.threshold` layers of recursion and replace the
omitted subterm with the symbol `⋯` if the subterm is deeper than
`pp.deepTerms.threshold / 4` (i.e. it is not shallow). To display the
omitted subterm in the InfoView, `⋯` can be clicked to open a popup with
the delaborated subterm.
<details>
<summary>InfoView with pp.deepTerms set to false (click to show
image)</summary>
</details>
### Implementation
- The delaborator is adjusted to use the new configuration settings and
terminate early if the threshold is exceeded and the corresponding term
to omit is shallow.
- To be able to distinguish `⋯` from regular terms, a new constructor
`Lean.Elab.Info.ofOmissionInfo` is added to `Lean.Elab.Info` that takes
a value of a new type `Lean.Elab.OmissionInfo`.
- `ofOmissionInfo` is needed in `Lean.Widget.makePopup` for the
`Lean.Widget.InteractiveDiagnostics.infoToInteractive` RPC procedure
that is used to display popups when clicking on terms in the InfoView.
It ensures that the expansion of an omitted subterm is delaborated using
`explicit := false`, which is typically set to `true` in popups for
regular terms.
- Several `Info` widget utility functions are adjusted to support
`ofOmissionInfo`.
- The list delaborator is adjusted with special support for `⋯` so that
long lists `[x₁, ..., xₖ, ..., xₙ]` are shortened to `[x₁, ..., xₖ, ⋯]`.
this way this function does not have to peek at the `altType` to see
when there are no more arguments, which makes it a bit more explicit,
and also a bit more robust should one apply this function to the type of
an alternative with the motive already instantiated.
It seems this uncovered a variable shadow bug, where the counter `i` was
accidentially reset after removing the `i`’th entry in `ys`.
