Moves the `@[coe]` attribute and associated elaborators/delaborators
from Std to Lean.
---------
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.
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.
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`.
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.
Encouraged by the performance gains from making `rewrite` produce
smaller proof objects
(#3121) I am here looking for low-hanging fruit in `simp`.
Consider this typical example:
```
set_option pp.explicit true
theorem test
(a : Nat)
(b : Nat)
(c : Nat)
(heq : a = b)
(h : (c.add (c.add ((c.add b).add c))).add c = c)
: (c.add (c.add ((c.add a).add c))).add c = c
```
We get a rather nice proof term when using
```
:= by rw [heq]; assumption
```
namely
```
theorem test : ∀ (a b c : Nat),
@Eq Nat a b →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c :=
fun a b c heq h =>
@Eq.mpr (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c)
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c)
(@congrArg Nat Prop a b (fun _a => @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c _a) c))) c) c) heq) h
```
(this is with #3121).
But with `by simp only [heq]; assumption`, it looks rather different:
```
theorem test : ∀ (a b c : Nat),
@Eq Nat a b →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c :=
fun a b c heq h =>
@Eq.mpr (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c)
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c)
(@id
(@Eq Prop (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c)
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c))
(@congrFun Nat (fun a => Prop) (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c))
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c))
(@congrArg Nat (Nat → Prop) (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c)
(Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) (@Eq Nat)
(@congrFun Nat (fun a => Nat) (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))))
(Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))))
(@congrArg Nat (Nat → Nat) (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c)))
(Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) Nat.add
(@congrArg Nat Nat (Nat.add c (Nat.add (Nat.add c a) c)) (Nat.add c (Nat.add (Nat.add c b) c)) (Nat.add c)
(@congrArg Nat Nat (Nat.add (Nat.add c a) c) (Nat.add (Nat.add c b) c) (Nat.add c)
(@congrFun Nat (fun a => Nat) (Nat.add (Nat.add c a)) (Nat.add (Nat.add c b))
(@congrArg Nat (Nat → Nat) (Nat.add c a) (Nat.add c b) Nat.add
(@congrArg Nat Nat a b (Nat.add c) heq))
c))))
c))
c))
h
```
Since simp uses only single-step `congrArg`/`congrFun` congruence lemmas
here, the proof
term grows very large, likely quadratic in this case.
Can we do better? Every nesting of `congrArg` (and it's little brother
`congrFun`) can be
turned into a single `congrArg` call.
In this PR I make making the smart app builders `Meta.mkCongrArg` and
`Meta.mkCongrFun` a bit
smarter and not only fuse with `Eq.refl`, but also with
`congrArg`/`congrFun`.
Now we get, in this simple example,
```
theorem test : ∀ (a b c : Nat),
@Eq Nat a b →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c →
@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c :=
fun a b c heq h =>
@Eq.mpr (@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c a) c))) c) c)
(@Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c b) c))) c) c)
(@congrArg Nat Prop a b (fun x => @Eq Nat (Nat.add (Nat.add c (Nat.add c (Nat.add (Nat.add c x) c))) c) c) heq) h
```
Let’s see if it works and how much we gain.
right now, the `induction` tactic accepts a custom eliminator using the
`using <ident>` syntax, but is restricted to identifiers. This
limitation becomes annoying when the elminator has explicit parameters
that are not targets, and the user (naturally) wants to be able to write
```
induction a, b, c using foo (x := …)
```
This generalizes the syntax to expressions and changes the code
accordingly.
This can be used to instantiate a multi-motive induction:
```
example (a : A) : True := by
induction a using A.rec (motive_2 := fun b => True)
case mkA b IH => exact trivial
case A => exact trivial
case mkB b IH => exact trivial
```
For this to work the term elaborator learned the `heedElabAsElim` flag,
`true` by default. But in the default setting, `A.rec (motive_2 := fun b
=> True)`
would fail to elaborate, because there is no expected type. So the
induction
tactic will elaborate in a mode where that attribute is simply ignored.
As a side effect, the “failed to infer implicit target” error message
is improved and prints the name of the implicit target that could not be
instantiated.
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>
Consider
```
import Std.Tactic.ShowTerm
opaque a : Nat
opaque b : Nat
axiom a_eq_b : a = b
opaque P : Nat → Prop
set_option pp.explicit true
-- Using rw
example (h : P b) : P a := by show_term rw [a_eq_b]; assumption
```
Before, a typical proof term for `rewrite` looked like this:
```
-- Using the proof term that rw produces
example (h : P b) : P a :=
@Eq.mpr (P a) (P b)
(@id (@Eq Prop (P a) (P b))
(@Eq.ndrec Nat a (fun _a => @Eq Prop (P a) (P _a))
(@Eq.refl Prop (P a)) b a_eq_b))
h
```
which is rather round-about, applying `ndrec` to `refl`. It would be
more direct to write
```
example (h : P b) : P a :=
@Eq.mpr (P a) (P b)
(@id (@Eq Prop (P a) (P b))
(@congrArg Nat Prop a b (fun _a => (P _a)) a_eq_b))
h
```
which this change does.
This makes proof terms smaller, causing mild general speed up throughout
the code; if the brenchmarks don’t lie the highlights are
* olean size -2.034 %
* lint wall-clock -3.401 %
* buildtactic execution s -10.462 %
H'T to @digama0 for advice and help.
NB: One might even expect the even simpler
```
-- Using the proof term that I would have expected
example (h : P b) : P a :=
@Eq.ndrec Nat b (fun _a => P _a) h a a_eq_b.symm
```
but that would require non-local changes to the source code, so one step
at a time.
