feat: use supplied structure fields left to right and eta reduce terms in structure instance elaboration #2478

mattrobball · 2023-08-29T18:10:51Z

Modifies the structure instance elaborator to

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.
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

github-actions · 2023-08-29T18:11:05Z

Thanks for your contribution! Please make sure to follow our Commit Convention.

mattrobball · 2023-08-30T00:49:56Z

awaiting-review

tests/lean/run/structWith_scott.lean

tests/lean/run/structInstFast.lean

tests/lean/structInstExtraEta.lean

src/Lean/Elab/StructInst.lean

semorrison · 2023-08-30T05:33:37Z

awaiting-author

mattrobball · 2023-08-30T10:35:11Z

Thanks for the comments. Hopefully, they are addressed with these changes.

awaiting-review

mattrobball · 2023-08-30T11:46:28Z

awaiting-author

mattrobball · 2023-08-30T17:00:08Z

awaiting-review

tests/lean/run/structInstFast.lean

tests/lean/structInstExtraEta.lean

semorrison · 2023-08-31T01:47:36Z

Can you please rebase on master so we get a mathlib-compatible release to try out?

kbuzzard · 2024-01-19T17:20:46Z

Note the substantial speedup to mathlib which comes with this PR.

kmill

Thanks for all the work getting this to this point! I'm looking forward to seeing this merged.

It looks good to me. I see it's not rebased onto the most current nightly, so please do that to be sure the CI goes through.

kmill · 2024-01-31T22:17:33Z

tests/lean/run/463.lean

@@ -4,4 +4,4 @@ structure C := (a b c : Nat)
 structure D := (toA : A) (c : Nat)

 def foo (s : C) : B := {s with} -- works in lean 4, works in lean 3
-def bar (s : D) : B := {s with} -- works in lean 4, fails in lean 3
+-- def bar (s : D) : B := {s with} -- works in lean 4, fails in lean 3


Correct me if I'm wrong, you don't need to comment this out, right?

You can add a comment that this is not necessarily meant to succeed.

Doesn’t it fail a test because this errors?

Added a comment referencing the PR number

@mattrobball

This is the adaptation PR for nightly-2024-02-01. It rolls in the branches * #9843, prepared by @mattrobball, which has the adaptations for leanprover/lean4#2478 * #10133, prepared by @semorrison, which has the adaptations for leanprover/lean4#3210 As these both landed in the same nightly, we're having to do the update in one go. Note this nightly is intended to become `v4.6.0-rc1` tomorrow. ---  [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) --------- Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

The FunLike hierarchy is very big and gets scanned through each time we need a coercion (via the `CoeFun` instance). It looks like unbundled inheritance suits Lean 4 better here. The only class that still extends `FunLike` is `EquivLike`, since that has a custom `coe_injective'` field that is easier to implement. All other classes should take `FunLike` or `EquivLike` as a parameter. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60example.20.28p.20.3A.20P.29.20.3A.20Q.20.3A.3D.20p.60.20takes.200.2E25s.20to.20fail!) ## Important changes Previously, morphism classes would be `Type`-valued and extend `FunLike`: ```lean /-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms. You should extend this class when you extend `MyHom`. -/ class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B] extends FunLike F A B := (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y)) ``` After this PR, they should be `Prop`-valued and take `FunLike` as a parameter: ```lean /-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms. You should extend this class when you extend `MyHom`. -/ class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B] [FunLike F A B] : Prop := (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y)) ``` (Note that `A B` stay marked as `outParam` even though they are not purely required to be so due to the `FunLike` parameter already filling them in. This is required to see through type synonyms, which is important in the category theory library. Also, I think keeping them as `outParam` is slightly faster.) Similarly, `MyEquivClass` should take `EquivLike` as a parameter. As a result, every mention of `[MyHomClass F A B]` should become `[FunLike F A B] [MyHomClass F A B]`. ## Remaining issues ### Slower (failing) search While overall this gives some great speedups, there are some cases that are noticeably slower. In particular, a *failing* application of a lemma such as `map_mul` is more expensive. This is due to suboptimal processing of arguments. For example: ```lean variable [FunLike F M N] [Mul M] [Mul N] (f : F) (x : M) (y : M) theorem map_mul [MulHomClass F M N] : f (x * y) = f x * f y example [AddHomClass F A B] : f (x * y) = f x * f y := map_mul f _ _ ``` Before this PR, applying `map_mul f` gives the goals `[Mul ?M] [Mul ?N] [MulHomClass F ?M ?N]`. Since `M` and `N` are `out_param`s, `[MulHomClass F ?M ?N]` is synthesized first, supplies values for `?M` and `?N` and then the `Mul M` and `Mul N` instances can be found. After this PR, the goals become `[FunLike F ?M ?N] [Mul ?M] [Mul ?N] [MulHomClass F ?M ?N]`. Now `[FunLike F ?M ?N]` is synthesized first, supplies values for `?M` and `?N` and then the `Mul M` and `Mul N` instances can be found, before trying `MulHomClass F M N` which *fails*. Since the `Mul` hierarchy is very big, this can be slow to fail, especially when there is no such `Mul` instance. A long-term but harder to achieve solution would be to specify the order in which instance goals get solved. For example, we'd like to change the arguments to `map_mul` to look like `[FunLike F M N] [Mul M] [Mul N] [highPriority <| MulHomClass F M N]` because `MulHomClass` fails or succeeds much faster than the others. As a consequence, the `simpNF` linter is much slower since by design it tries and fails to apply many `map_` lemmas. The same issue occurs a few times in existing calls to `simp [map_mul]`, where `map_mul` is tried "too soon" and fails. Thanks to the speedup of leanprover/lean4#2478 the impact is very limited, only in files that already were close to the timeout. ### `simp` not firing sometimes This affects `map_smulₛₗ` and related definitions. For `simp` lemmas Lean apparently uses a slightly different mechanism to find instances, so that `rw` can find every argument to `map_smulₛₗ` successfully but `simp` can't: leanprover/lean4#3701. ### Missing instances due to unification failing Especially in the category theory library, we might sometimes have a type `A` which is also accessible as a synonym `(Bundled A hA).1`. Instance synthesis doesn't always work if we have `f : A →* B` but `x * y : (Bundled A hA).1` or vice versa. This seems to be mostly fixed by keeping `A B` as `outParam`s in `MulHomClass F A B`. (Presumably because Lean will do a definitional check `A =?= (Bundled A hA).1` instead of using the syntax in the discrimination tree.) ## Workaround for issues The timeouts can be worked around for now by specifying which `map_mul` we mean, either as `map_mul f` for some explicit `f`, or as e.g. `MonoidHomClass.map_mul`. `map_smulₛₗ` not firing as `simp` lemma can be worked around by going back to the pre-FunLike situation and making `LinearMap.map_smulₛₗ` a `simp` lemma instead of the generic `map_smulₛₗ`. Writing `simp [map_smulₛₗ _]` also works. Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

mattrobball changed the title ~~Tweak structure instance elaboration to eliminate un-needed eta expansions of terms~~ feat: modify structure instance elaboration to eliminate un-needed eta expansions of terms Aug 29, 2023

mattrobball force-pushed the reduce_etas branch from 0c0c9d4 to 89ea1d4 Compare August 29, 2023 23:25

github-actions bot added the awaiting-review Waiting for someone to review the PR label Aug 30, 2023