eta ftw

Stream: mathlib4

[Johan Commelin]

The new etaExperiment option is crucial for certain linear algebra files.

[Johan Commelin]

You can do some awesome juggling with it.

[Johan Commelin]

Before (pretty broken):

/-- `R^n/I^n` is isomorphic to `(R/I)^n` as an `R/I`-module. -/
noncomputable def piQuotEquiv : ((ι → R) ⧸ I.pi ι) ≃ₗ[R ⧸ I] ι → (R ⧸ I) where
  toFun x :=
    Quotient.liftOn' x (fun f i => Ideal.Quotient.mk I (f i)) fun a b hab =>
      funext fun i => (Submodule.Quotient.eq' _).2 (QuotientAddGroup.leftRel_apply.mp hab i)
  invFun x := Ideal.Quotient.mk (I.pi ι) fun i => Quotient.out' (x i)
  map_add' := by rintro ⟨_⟩ ⟨_⟩; rfl
  map_smul' := by rintro ⟨_⟩ ⟨_⟩; rfl
  left_inv := by
    rintro ⟨x⟩
    exact Ideal.Quotient.eq.2 fun i => Ideal.Quotient.eq.1 (Quotient.out_eq' _)
  right_inv := by
    intro x
    ext i
    obtain ⟨r, hr⟩ := @Quot.exists_rep _ _ (x i)
    simp_rw [← hr]
    convert Quotient.out_eq' _
#align ideal.pi_quot_equiv Ideal.piQuotEquiv

[Johan Commelin]

After:

set_option synthInstance.etaExperiment false in -- needed, otherwise the type times out
/-- `R^n/I^n` is isomorphic to `(R/I)^n` as an `R/I`-module. -/
noncomputable def piQuotEquiv : ((ι → R) ⧸ I.pi ι) ≃ₗ[R ⧸ I] ι → (R ⧸ I) := by
  refine' ⟨⟨⟨?toFun, _⟩, _⟩, ?invFun, _, _⟩
  case toFun => set_option synthInstance.etaExperiment true in -- needed otherwise we don't have `Module R R`
    exact fun x ↦
      Quotient.liftOn' x (fun f i => Ideal.Quotient.mk I (f i)) fun a b hab =>
        funext fun i => (Submodule.Quotient.eq' _).2 (QuotientAddGroup.leftRel_apply.mp hab i)
  case invFun =>
    exact fun x ↦ Ideal.Quotient.mk (I.pi ι) fun i ↦ Quotient.out' (x i)
  · rintro ⟨_⟩ ⟨_⟩; rfl
  · rintro ⟨_⟩ ⟨_⟩; rfl
  · rintro ⟨x⟩
    exact Ideal.Quotient.eq.2 fun i => Ideal.Quotient.eq.1 (Quotient.out_eq' _)
  · intro x
    ext i
    obtain ⟨r, hr⟩ := @Quot.exists_rep _ _ (x i)
    convert Quotient.out_eq' (x i)
#align ideal.pi_quot_equiv Ideal.piQuotEquiv

[Kevin Buzzard]

So what happens when someone makes a PR with etaExperiment in?

[Jireh Loreaux]

I think Gabriel has said etaExperiment is for testing purposes only, so I would say we should not have any PRs merge with it present.

[Gabriel Ebner]

Yes, it's not completely clear to me when/if we can enable eta by default. I'd like to avoid a situation where we have etaExperiment enabled in every file (because it's obviously the right choice), and then run into the performance issues that prevent us from enabling it by default in the first place.

[Johan Commelin]

So the RingTheory.Ideal.Quotient PR is pretty stuck. Because this decl needs the option turned off for the type, but turned on for the term...

[Kevin Buzzard]

Dare I ask why we didn't have this problem in lean 3?

[Johan Commelin]

I think it is because we now use new structures everywhere.

[Johan Commelin]

But take that with a grain of salt. I don't know what I'm talking about.

[Eric Wieser]

Is reverting to manual old style structures in mathlib 4 a reasonable thing to do?

[Eric Wieser]

Or will that have all the same performance problems as enabling the eta mode and sticking with new-style structures?

[Jireh Loreaux]

Isn't the problem with old structures that it makes proof terms huge?

[Gabriel Ebner]

Is reverting to manual old style structures in mathlib 4 a reasonable thing to do?

It might be a good workaround for the algebraic hierarchy. But I'm not sure if we can get a set_option oldStructure true into core. :-/ (And monkeypatching that in mathlib4 is--while possible--pretty awful as it requires copy-pasting a couple hundred lines from Elab/Structure.lean) I'd really like to avoid extends Add α, Mul α, .. because that's hard to revert once we get a proper solution.

[Gabriel Ebner]

Or will that have all the same performance problems as enabling the eta mode and sticking with new-style structures?

The general issue is that the unifier is a performance shitshow with new-style structures since it tries to reduce A.toPartialOrder =?= B.toPartialOrder to A =?= B, so we end up comparing group structures when all we need to know is that 0 is the same. This isn't such a huge issue with old-style structures because at least there we've only got a single layer of nested structures.

[Gabriel Ebner]

Eta can feed into this issue. It reduces A =?= @LinearOrder.mk _ po .. to A.toPartialOrder =?= po and then it can happen that po is also a ...toPartialOrder. (And on top of it the eta implementation is pretty new and produces different projections than WHNF returns, so we even circumvent the defeq cache..)

[Gabriel Ebner]

Isn't the problem with old structures that it makes proof terms huge?

I don't think new structures have a significant effect on term size in the algebraic hierarchy. The term size reduction only works for the first parent. That is, in class Lattice P extends SemilatticeSup P, SemilatticeInf P only the SemilatticeSup P is "faster" (benchmarks needed). The SemilatticeInf P side looks just like old-style structures.

[Johan Commelin]

Eric Wieser said:

Is reverting to manual old style structures in mathlib 4 a reasonable thing to do?

If we make huge refactors to the hierarchy, I would rather do it only once. The other day we a discussion about moving in a mixin direction. If that is the future, I would prefer working towards that refactor.

[Mario Carneiro]

Gabriel Ebner said:

Is reverting to manual old style structures in mathlib 4 a reasonable thing to do?

It might be a good workaround for the algebraic hierarchy. But I'm not sure if we can get a set_option oldStructure true into core. :-/

I think that it would actually reasonable to have not a set_option for this - that's obviously a hack - but rather a @[flat] annotation that goes on parents of a structure a la struct Foo A extends Bar A, @[flat] Baz A. The reason is that the structure command is using a heuristic to decide what should be flattened and what should not be, and it is not unreasonable to have a way to have more direct control over this.

[Gabriel Ebner]

The problem is not the surface syntax, but getting it into core. FWIW, I like the term attribute suggestion. Not just for this but also for @[outParam], @[unused], and @[borrowed].

[Gabriel Ebner]

To contribute to the bikeshed, a long time ago I thought we should call this class Foo A extends Bar A with Baz A (like Scala, where the with indicates indirect inheritance).

[Mario Carneiro]

I think the version I suggested is potentially viable for core. set_option oldStructure is absolutely the wrong message by comparison

[Mario Carneiro]

This is already something the structure elaborator can do, it just doesn't surface a syntax for it

[Moritz Doll]

I think we might want to have the eta:

import Mathlib.LinearAlgebra.Basic

variable [Ring k] [AddCommGroup V] [Module k V]
variable (σ : k →+* k) (f : V →ₛₗ[σ] V) (x : V)

#check f x --fails

set_option synthInstance.etaExperiment true

#check f x -- no problem

[Johan Commelin]

@Moritz Doll At the top of the thread, I show an example where you need to switch between having the option true and false within one declaration.

[Moritz Doll]

I saw that. My point is that we need a midterm-solution to that issue, because otherwise all linear algebra is blocked.

[Johan Commelin]

Sure, a lot of the port is blocked

[Johan Commelin]

@Moritz Doll Is

-- Porting note: added the following line, fails to be inferred otherwise. Probably lean4#2074
instance : Module R R := Semiring.toModule

a workaround in your file?

[Johan Commelin]

If you search for 2074 in mathlib4, you'll find a handful of workarounds that people use to keep the port moving.

[Moritz Doll]

Ah thanks, I was only aware of the 'remove attribute' workaround.

[Sebastien Gouezel]

As a temporary workaround to guarantee that all our base algebraic classes are flat, would it work to start all of them with hasZero, so that the other classes that also have a zero would be flattened by the current heuristics? Something like class Ring R extends hasZero R, Semiring R, hasNeg R...

[Eric Wieser]

That won't ensure flatness for MonoidWithZero I don't think

[Eric Wieser]

Lots of possible workarounds (including a similar one) were already discussed in a previous thread I think

[Sebastien Gouezel]

Eric Wieser said:

That won't ensure flatness for MonoidWithZero I don't think

Sure, for this one we would need extends hasZero R, hasOneR, .... Do you have pointers for where this was discussed?

[Eric Wieser]

The original thread is linked from the GitHub issue I think. When I'm not on mobile I could look for it

[Eric Wieser]

But yes, in general listing all the notation base classes explicitly would do the trick

[Eric Wieser]

As would adding an empty structure EnsureClash base class to the start of every algebraic and notation class