Simp claims not defeq but rfl works

Stream: lean4

[Matthew Ballard]

Why would I see a failure like

[Meta.Tactic.simp.discharge] @Pi.smul_apply, failed to assign instance
      ℝ × ℝ → SMul ℝ ℝ
    sythesized value
      fun i ↦ Algebra.toSMul
    is not definitionally equal to
      fun i ↦ SMulZeroClass.toSMul

with the following working fine?

def foo : ℝ × ℝ → SMul ℝ ℝ := fun _ => Algebra.toSMul
def bar : ℝ × ℝ → SMul ℝ ℝ := fun _ => SMulZeroClass.toSMul
example : foo = bar := rfl

(also synthesized is mis-spelled)

[Kyle Miller]

I just checked the source (the spelling error made it quick to find), and when it does the check it does reducible-and-instances defeq. Maybe that's too strict in this case?

[Matthew Ballard]

Indeed, this fails

example : Algebra.toSMul = SMulZeroClass.toSMul (M := ℝ) (A := ℝ) := by with_reducible_and_instances rfl

[Matthew Ballard]

Note this is in #9007 and not on master

[Matthew Ballard]

For a follow up, how does simp [Pi.smul_apply _, ...] bypass this?

[Matthew Ballard]

Does this short-circuit synthesis?

[Kyle Miller]

It looks like the normal isDefEq check for instances does it at default transparency

[Kyle Miller]

I'm guessing _ is a bypass since it switches from having simp deal with the instance argument to having the main elaborator deal with it.

[Matthew Ballard]

And this fills in something from the cache instead of resynthesizing?

[Kyle Miller]

No, I don't think so. I think both with and without _ it will use a cache. The question is who is responsible for making sure the metavariable associated to the instance argument ends up being filled in. I believe putting a _ causes the main elaborator to handle the implicit arguments to Pi.smul_apply, but not including it means simp will decide it will take responsibility. In both cases the instance argument might be filled in via unification, but in the first the usual method checks that the filled-in value is defeq to what the synthesized value would be, but in the second simp does that check with reducible-and-instances defeq.

[Kyle Miller]

Here's how instance arguments work in the main elaborator:

1. The instance argument is filled in with a fresh metavariable.
2. This metavariable is added to a table of pending instance synthesis problems. This makes it be a "synthetic metavariable".
3. Periodically, the elaborator tries to synthesize pending instance synthesis problems. The synthesis either succeeds, fails, or remains indeterminate. On failure (which happens if it can tell there are no instances no matter what), it throws an error.
4. On success, it checks if the metavariable has already been independently assigned. If it hasn't, then it assigns the metavariable. If it has, then it does an isDefEq check; if that check fails, it throws an error.

[Kyle Miller]

The way simp works is

1. The LHS of the simp lemma is unified against the target.
2. If that succeeds, then it goes on to try to synthesize the instance arguments to the simp lemma. There's some logic about if arguments have a class as a type, it still tries to synthesize if possible, and if the argument is a prop, it tries to use simp on it.

[Kyle Miller]

There's an interesting comment in here:

    -- Note that the binderInfo may be misleading here:
    -- `simp [foo _]` uses `abstractMVars` to turn the elaborated term with
    -- mvars into the lambda expression `fun α x inst => foo x`, and all
    -- its bound variables have default binderInfo!

[Matthew Ballard]

Huh

[Kyle Miller]

I guess actually foo _ causes all the arguments to become explicit, so it becomes less picky about the usual instance rules. (I'm pretty sure instance arguments will still be handled by the main elaborator's system. This is just about causing simp to not try using the pickier method on top of that.)

[Kyle Miller]

I didn't know that simp was happy to fill in non-[...] typeclass arguments. Maybe we should use {...} instead of [...] a lot more frequently for simp lemmas, since that means (1) it should pick up these arguments via unification (skipping potentially expensive instance synthesis) and (2) do instance synthesis if that wasn't sufficient

[Kyle Miller]

If that's a problem for using these as rw lemmas, maybe rw could use the same logic?

[Matthew Ballard]

What are the disadvantages in principal of prioritizing unification over synthesis here?

[Kyle Miller]

There's nothing making sure that instances remain canonical, and maybe it could be a problem that unification might only half solve for an instance? (i.e., the instance it picks up might contain metavariables that a full instance synthesis could fill in)

[Kyle Miller]

That second point doesn't seem like a real problem, since those metavariables would still be goals or should otherwise be accounted for.

[Kyle Miller]

Here's the line in rewrite that causes arguments to a rewrite lemma to be synthesized: https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Rewrite.lean#L50 (in particular, docs#Lean.Meta.synthAppInstances)

Here's the logic in simp for synthesizing simp lemma arguments: https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/Rewrite.lean#L22-L65

[Kyle Miller]

Upgrading that logic for rewrite would also affect apply

[Jannis Limperg]

Kyle Miller said:

I just checked the source (the spelling error made it quick to find), and when it does the check it does reducible-and-instances defeq. Maybe that's too strict in this case?

Previous thread about a similar issue: #lean4 > apply instance check fails at reducible transparency

There, the problem is that the instance check in apply is performed with the ambient transparency. So with with_reducible apply (which I'd like to use for Aesop), it can happen that a lemma is applicable at reducible transparency, but the instance check fails at reducible transparency and so apply fails.

I think we should investigate whether it would be feasible to have these instance checks use a fixed, fairly aggressive transparency (default? all even?). This would make sure that users are bothered as little as possible by these checks. Of course, we'd have to keep an eye on performance.

[Mario Carneiro]

best not to ever use all, it is an implementation detail that irreducible defs are even unfoldable

[Floris van Doorn]

Would using with_reducible_and_instances apply solve this issue, while not making the apply significantly more expensive?

[Matthew Ballard]

Kyle Miller said:

I didn't know that simp was happy to fill in non-[...] typeclass arguments. Maybe we should use {...} instead of [...] a lot more frequently for simp lemmas, since that means (1) it should pick up these arguments via unification (skipping potentially expensive instance synthesis) and (2) do instance synthesis if that wasn't sufficient

#9020 yolo

[Floris van Doorn]

Clearly this should be solved by making the instances defeq up to instances transparency.

variable (R : Type) [CommSemiring R] in
example : Algebra.toSMul (R := R) (A := R) = SMulZeroClass.toSMul (M := R) (A := R) :=
  by with_reducible_and_instances rfl

In particular RingHom.toAlgebra should be reducible (and maybe others as well). This is the library note [reducible non-instances].

[Matthew Ballard]

You need Algebra.id to be reducible.

[Matthew Ballard]

To be clear, I am not strongly advocating for anything currently. I want to check breakage and performance implications.

[Floris van Doorn]

Algebra.id is an instance, so will already be unfolded using with_reducible_and_instances

[Matthew Ballard]

It doesn't appear to be unfolded currently.

-- import Mathlib.Analysis.NormedSpace.Basic
import Mathlib.Algebra.Algebra.Pi
import Mathlib.Algebra.Algebra.RestrictScalars
import Mathlib.Analysis.Normed.Field.Basic
import Mathlib.Analysis.Normed.MulAction
import Mathlib.Data.Real.Sqrt
import Mathlib.Topology.Algebra.Module.Basic

set_option trace.Meta.isDefEq true in
def foo : Algebra.toSMul = SMulZeroClass.toSMul (M := ℝ) (A := ℝ) := by with_reducible_and_instances rfl
def bar : Algebra.toSMul = SMulZeroClass.toSMul (M := ℝ) (A := ℝ) := by rfl

set_option pp.all true in
#print foo

set_option pp.all true in
#print bar

Uncomment the first import and foo goes green. docs#NormedAlgebra.id has an extra eta expansion which unfolds Algebra.id as side-effect

instance NormedAlgebra.id : NormedAlgebra 𝕜 𝕜 :=
  { NormedField.toNormedSpace, Algebra.id 𝕜 with }

[Matthew Ballard]

@Floris van Doorn I tried to mark it as draft to express my current neutrality but the web UI is borked

[Matthew Ballard]

Ok, it seems to have taken but didn't reload the page

[Matthew Ballard]

Went through smoothly. No performance benefit/cost.

[Kyle Miller]

Floris van Doorn said:

Clearly this should be solved by making the instances defeq up to instances transparency.

I agree, but the other part of this is that making arguments for instances not be inst-implicit means simp won't try re-synthesizing them and it will trust the value obtained through unification. This might have interesting performance implications.

It's also worth thinking about improvements to how simp elaborates arguments. Anne in https://github.com/leanprover-community/lean/pull/659 made it so Lean 3's simp could handle out params, which as far as I understand Lean 4's simp doesn't -- it just processes arguments left-to-right just like how Lean 3 did before Anne's change.

[Matthew Ballard]

#9025 has the minimal amount of changes to achieve unification at appropriate transparency

[Matthew Ballard]

It builds and lints now but the benchmark is going to be painful.

[Matthew Ballard]

Benchmark                                                  Metric          Change
  =================================================================================
- build                                                      instructions      5.7%
- build                                                      simp             29.6%
- build                                                      wall-clock        8.2%

ouch

[Matthew Ballard]

So in well-studied example of Pi.smul_apply #lean4 > simp [X] fails, rw [X] works we have three options to have simp work "as expected":

1. Make the instance implicit just implicit #9020
2. Make RingHom.id (and intermediate defs reducible) #9025
3. Use simp [Pi.smul_apply _].

Option 2 follows the general principles for handling this situation but the (mind-numbed) implementation is horrifically slower overall. Option 3 muddles us along.

[Matthew Ballard]

I guess there is also

4. Change the behavior of simp in some principled way that makes it easier for end users to reason about application and failure

which is what Kyle is suggesting based on path walked in Lean 3.

[Matthew Ballard]

If someone can make 2. more performance neutral, that would be great