dsimp took 83.3s

Stream: mathlib4

[Matthew Ballard]

After the salacious lede, !4#3067 currently builds (allowing infinite time) but is extremely slow in two places. (If you thought !4#2364 was bad...) Any perf whisperers are very welcome to take a look. I will keep poking at it with my primitive instruments.

[Kyle Miller]

I'm looking at prime_rename_iff, and one thing I've found is that this partial proof elaborates almost instantly

theorem prime_rename_iff (s : Set σ) {p : MvPolynomial s R} :
    Prime (rename ((↑) : s → σ) p) ↔ Prime p := by
  classical
  symm
  let eqv1 := (sumAlgEquiv R (↥(sᶜ)) s)
  sorry

but this one times out

theorem prime_rename_iff (s : Set σ) {p : MvPolynomial s R} :
    Prime (rename ((↑) : s → σ) p) ↔ Prime p := by
  classical
  symm
  let eqv1 := (sumAlgEquiv R (↥(sᶜ)) s).symm
  sorry

[Matthew Ballard]

I noticed that also. I tried feeding it things with @ and I think it did help a bit.

[Matthew Ballard]

I think you if also change from s^c to just some t is also helps (if memory serves)

[Kyle Miller]

It looks like it has something to do with how [...] binders get resynthesized from scratch even if they're available from unification?

This is instant:

def _root_.AlgEquiv.symm' {inst : CommSemiring R} {_ : Semiring A₁} {_ : Semiring A₂}
  {_ : Algebra R A₁} {_ : Algebra R A₂} (e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁ := e.symm

theorem prime_rename_iff (s : Set σ) {p : MvPolynomial s R} :
    Prime (rename ((↑) : s → σ) p) ↔ Prime p := by
  classical
  symm
  have eqv1 := (sumAlgEquiv R (↥(sᶜ)) s).symm'
  sorry

[Kyle Miller]

Perhaps AlgEquiv.symm should have only implicit arguments since they can all be inferred from e.

[Matthew Ballard]

I assume the same problem afflicts trans?

[Kyle Miller]

Untested theory: they get resynthesized and they're slightly different, in a way where unification slowly but surely eventually succeeds.

[Kyle Miller]

(And if anyone's following along, the classical isn't the culprit. It's slow with or without it.)

[Kyle Miller]

Matthew Ballard said:

I assume the same problem afflicts trans?

Yeah, I'd guess so.

[Matthew Ballard]

Doesrefine and ?_ achieve this effect? (With @)

[Kyle Miller]

Yeah, I noticed that porting note and couldn't immediately think of what might cause that, but looking at it again, it seems like using (_) instead of ?_ works too. Could you test it on your computer?

[Kyle Miller]

My understanding is that (_) causes Lean to interpret this as a placeholder for an expression that goes into that argument, rather than a placeholder for an instance argument. (A "natural metavariable" vs a "synthetic metavariable" -- these are filled in by typeclass inference.)

[Gabriel Ebner]

Kyle Miller said:

Untested theory: they get resynthesized and they're slightly different, in a way where unification slowly but surely eventually succeeds.

I think that's accurate:

[Meta.isDefEq] [1.903590s] 💥 CommSemiring.toSemiring =?= Ring.toSemiring ▶

[Matthew Ballard]

I think this gives me a sense of how to work around the issue. I will test it out later (unless someone beats me to it!) Thanks for the (_) tip

[Matthew Ballard]

Though I guess we should ask whether the signature of AlgEquiv.symm, AlgEquiv.trans... should change

[Kyle Miller]

Just to summarize some things I've sort of figured out recently, regarding (_) vs ?_, I think neither create synthetic metavariables, but in refine the (_) metavariables must be solved for and the ?_ are allowed to not be solved for. The ?_ metavariables are also special in that once they get through refine, they get turned into metavariables that can't be solved for via unification anymore, since they're marked as being unassignable (though tactics can override this using docs4#Lean.Meta.withAssignableSyntheticOpaque).

[Matthew Ballard]

(_) is new behavior for refine in Lean 4 right?

[Kyle Miller]

I don't think the (_) is refine-specific -- it's just alters how the elaborator deals with placeholders.

[Kyle Miller]

I also think it's new to Lean 4, since Lean 3 didn't have a way to represent (_) before it got to the elaborator.

[Kyle Miller]

AlgEquiv.trans is tricky, since if you use the transitivity tactic you want to synthesize typeclasses for the middle term.

[Matthew Ballard]

The problem also crops up for MulEquiv.symm in uniqueFactorizationMonoid_of_fintype later on I think

[Matthew Ballard]

Eg

refine @IsDomain.toCancelCommMonoidWithZero _ _ ?_
infer_instance

is fine but the condensed version is not

[Matthew Ballard]

!4#3067 no longer requires infinite time. Ultimately there were some diamonds that Lean could resolve given time. Removing appropriate instances sped things up significantly. Thanks to @Kyle Miller, @Eric Wieser , and @Gabriel Ebner for the help