When updating Std, be careful that not every lemma has been upstreamed,
so we need to be careful to only delete things that have already been
declared.
Before the `zeta` / `zetaDelta` split, `dsimp` was performing `zeta`
by going inside of a `let`-expression, performing `zetaDelta`, and
then removing the unused `let`-expression.
This is pretty big PR that upstreams all of Std.Data.Int.Init in one go.
So far lemmas have seen minimal changes needed to adapt to Lean core
environment.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This upstreams NatCast and IntCast alone independent of norm_cast in
#3322.
This will allow more efficiently upstreaming parts of Std.Data.Int
relevant for omega.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
By having the `pp.proofs` feature use `⋯` when omitting proofs, when
users copy/paste terms from the InfoView the elaborator can give an
error message explaining why the term cannot be elaborated.
Also adds `pp.proofs.threshold` option to allow users to pretty print
shallow proof terms. By default, only atomic proof terms are pretty
printed.
This adjustment was suggested in PR #3201, which added `⋯` and the
related `pp.deepTerms` option.
This will collect definitions from Std.Logic
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
We previously had the syntax for `change` and `change at`, but no
implementation.
This moves Kyle's implementation from Std.
This also changes the `changeLocalDecl` function to push nodes to the
infotree about FVar aliases.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This moves the `rcases` and `obtain` tactics from Std, and makes them
built-in tactics.
We will separately move the test cases from Std after #3297
(`guard_expr`).
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
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>
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.
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 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ₖ, ⋯]`.
Adds support for `let_fun` to the `intro` and `intros` tactics. Also
adds support to `intro` for anonymous binder names, since the default
variable name for a `letFun` with an eta reduced body is anonymous.
This makes changes to the definitions of Associativity, Commutativity,
Idempotence and Identity classes to be more aligned with Mathlib's
versions.
The changes are:
* Move classes are moved from `Lean` to root namespace.
* Drop `Is` prefix from names.
* Rename `IsNeutral` to `LawfulIdentity` and add Left and Right
subclasses.
* Change neutral/identity element to outParam.
* Introduce `HasIdentity` for operations not intended for proofs to
implement
The identity changes are to make this compatible with
[Mathlib](718042db9d/Mathlib/Init/Algebra/Classes.lean)
and to enable nicer fold operations in Std that can use type classes to
infer the identity/initial element on binary operations.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
