Slow rfl (timeout) with `Algebra.adjoin`

Stream: mathlib4

[Junyan Xu]

I think it's connected to an earlier slow rfl question, but here even destructing the subtype doesn't work outright, I had to insert a show too.

import Mathlib.RingTheory.Adjoin.Basic

variable {R A B} [CommSemiring R] [CommSemiring A] [CommSemiring B]
  [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
  (s : Set B)

open Algebra

set_option quotPrecheck false
local notation "Rs" => adjoin R s
local notation "As" => (adjoin A s).restrictScalars R

instance : Algebra Rs As :=
  (Subalgebra.inclusion <| adjoin_le <| by exact subset_adjoin).toAlgebra

-- slow (timeout)
-- instance : IsScalarTower Rs As B := .of_algebraMap_eq fun _ ↦ rfl
-- instance : IsScalarTower Rs As B := .of_algebraMap_eq fun ⟨_, _⟩ ↦ rfl
-- instance : IsScalarTower Rs As B := .of_algebraMap_eq fun x ↦ show x.1 = x.1 from rfl

-- fast
instance : IsScalarTower Rs As B := .of_algebraMap_eq fun ⟨x, _⟩ ↦ show x = x from rfl

[Kevin Buzzard]

When you say "slow" do you actually mean "slow" or do you mean "always times out"? I've never got a "slow" one to terminate (which makes debugging much harder)

[Junyan Xu]

Yeah, I edited to say "timeout"

[Junyan Xu]

Definitely feels like kernel entering infinite loop

[Kevin Buzzard]

instance : IsScalarTower Rs As B := .of_algebraMap_eq fun x ↦ by
  rcases x with ⟨a, ha⟩
  change a = _ -- comment out one and you're still fine
  change _ = a -- comment out both and you're dead
  rfl

[Junyan Xu]

Good observation. Indeed both show _ = x and show x = _ work.

[Kevin Buzzard]

I'm not sure my observation helps. Here's what might be happening: maybe if both are commented out then rfl says "OK so this is algebraMap something something = algebraMap something something so let's see if I can equate the somethings" and now it might be in big trouble. But changing either of them to a makes it stop doing this.

[Junyan Xu]

That can't quite explain why

instance : IsScalarTower Rs As B := .of_algebraMap_eq fun x ↦ show x.1 = x.1 from rfl

doesn't work. So maybe the need of show is a new issue (due to Lean trying to equate the somethings), and the need to destruct the subtype is the old issue? (A difference with the old issue is that there we're checking equality in a subtype, but here we're not.)

[Kevin Buzzard]

have foo : (↥Rs) = (↥(Subalgebra.restrictScalars R (adjoin A s))) := rfl -- fails quickly

so I can't find evidence for my guess above.

[Kevin Buzzard]

set_option maxHeartbeats 0 in
-- slow (timeout)
-- instance : IsScalarTower Rs As B := .of_algebraMap_eq fun _ ↦ rfl
-- instance : IsScalarTower Rs As B := .of_algebraMap_eq fun ⟨_, _⟩ ↦ rfl
instance : IsScalarTower Rs As B := .of_algebraMap_eq fun x ↦ by
  rcases x with ⟨a, ha⟩
  congr
  -- 15 goals (after a very long pause)

I would imagine that rfl is going down this path before you tell it that it's just a = a. Examples of goals:

⊢ (fun x ↦ x ∈ Rs) = fun x ↦ x ∈ Subalgebra.restrictScalars R (adjoin A s)
⊢ Rs = Subalgebra.restrictScalars R (adjoin A s)
⊢ HEq (fun x ↦ B) fun x ↦ B
⊢ HEq ha ⋯

In fact that's all the goals, the first one shows up 9 times and the second one shows up 4 times. The algorithm gets it wrong and never recovers.

[Junyan Xu]

congr might create HEq goals, but might rfl? rfl would first check the types are defeq, right?

[Kevin Buzzard]

I'm afraid I have absolutely no idea what the rfl tactic does under the hood

[Junyan Xu]

In my original post there's no use of the rfl tactic, only the rfl term. (Is show a tactic? Or just a hint to the kernel?)

[Kevin Buzzard]

Oh I thought one should prefer the tactic to the term

[Anne Baanen]

So I see the message "(kernel) deterministic timeout" on the show-less instances. A kernel timeout means that the elaborator already accepted your definition but the kernel is taking too long to check. The elaborator and the kernel both have an algorithm for checking definitional equalities, and the one in the elaborator has quite a few more features and options. For example, only the elaborator cares about reducibility settings, the kernel will just unfold everything.

Unfortunately, the kernel does not do any tracing for equality checking, so unless you fire up a debugger with a breakpoint on is_def_eq_core we'll have to do with guessing.

[Junyan Xu]

Thanks! What difference does show make? Does it break one equality into two or three equalities for the kernel to check?

[Anne Baanen]

We can follow along what happens in the elaborator if we set_option trace.Meta.isDefEq true, and try to see if the kernel will do the same.

What happens when we have a goal of

(algebraMap (↥Rs) B) x =
    (algebraMap (↥(Subalgebra.restrictScalars R (adjoin A s))) B)
      ((algebraMap ↥Rs ↥(Subalgebra.restrictScalars R (adjoin A s))) x)

that gets solved by rfl (whether term or tactic) is that the elaborator will check that this term has the expected type. Which is basically just defeq checking

(algebraMap (↥Rs) B) x =
    (algebraMap (↥(Subalgebra.restrictScalars R (adjoin A s))) B)
      ((algebraMap ↥Rs ↥(Subalgebra.restrictScalars R (adjoin A s))) x)
=?=
?m.55479 = ?m.55479

Since = is an inductive type, the only solution is that the LHS equals the other LHS and the RHS equals the other RHS (this is done in the kernel by is_def_eq_app). Assigning ?m.55479 as (algebraMap (↥Rs) B) x solves the LHS, so the RHS now looks like:

((algebraMap ↥Rs ↥(Subalgebra.restrictScalars R (adjoin A s))) x✝) =?= (algebraMap (↥Rs) B) x✝

What's interesting is that the elaborator now starts unfolding the function applications:

(↑↑(algebraMap (↥Rs) B)).toFun x✝
=?=
(↑↑(algebraMap (↥(Subalgebra.restrictScalars R (adjoin A s))) B)).toFun
      ((algebraMap ↥Rs ↥(Subalgebra.restrictScalars R (adjoin A s))) x✝)

The kernel does its unfolding during defeq checks in lazy_delta_reduction_step, which gets called before trying to match up functions and arguments one by one. So this should still work the same between elaborator and kernel I think?

With a bit of unfolding the elaborator gets to:

(algebraMap B B)
      ((Subalgebra.restrictScalars R (adjoin A s)).subtype
        ((algebraMap ↥Rs ↥(Subalgebra.restrictScalars R (adjoin A s))) x✝))
=?=
(algebraMap B B) (Rs.subtype x✝)

which becomes

(Subalgebra.restrictScalars R (adjoin A s)).subtype
      ((algebraMap ↥Rs ↥(Subalgebra.restrictScalars R (adjoin A s))) x✝)
=?=
Rs.subtype x✝

and then

↑((algebraMap ↥Rs ↥(Subalgebra.restrictScalars R (adjoin A s))) x✝) =?= ↑x✝

Now here something interesting happens: the up arrow is a structure projection, and there the elaborator does decide to first try unifying the structures being projected:

((algebraMap ↥Rs ↥(Subalgebra.restrictScalars R (adjoin A s))) x✝).1 =?= x✝.1

becomes

⟨↑x✝, ⋯⟩ =?= x✝

and this actually fails on the check { x // x ∈ ↑(Subalgebra.restrictScalars R (adjoin A s)) } =?= ↥Rs.

So instead the elaborator unfolds the LHS one final time getting ↑x✝ =?= x✝.1 which finally succeeds.

[Anne Baanen]

Although looking at the definition of Rs, I'm not sure why it is not equal to (Subalgebra.restrictScalars R (adjoin A s))...

[Anne Baanen]

Ah nevermind, I was looking at the definition of As instead of Rs. It makes perfect sense again!

[Anne Baanen]

There are some ways to get definitions kernel checked without the elaborator failing, so maybe we could try to see if the kernel also times out on example : As = Rs := rfl. But that's probably a project for another time.

[Anne Baanen]

(Just a side note: the rfl tactic essentially tries exact rfl on equalities, and searches for a @[refl]-tagged proof for other relations. rfl and by rfl should not behave differently except if some weird goal order issues come up.)

[Anne Baanen]

Junyan Xu said:

In my original post there's no use of the rfl tactic, only the rfl term. (Is show a tactic? Or just a hint to the kernel?)

Junyan Xu said:

Thanks! What difference does show make? Does it break one equality into two or three equalities for the kernel to check?

Let's first try to explain the difference between (rfl : x = x) and show x = x from rfl. (rfl : x = x) is a hint to the elaborator to first typecheck that rfl has type x = x, and then to unify the hinted type with the goal type:

x = x
=?=
(algebraMap (↥Rs) B) ⟨x, property✝⟩ =
      (algebraMap (↥(Subalgebra.restrictScalars R (adjoin A s))) B)
        ((algebraMap ↥Rs ↥(Subalgebra.restrictScalars R (adjoin A s))) ⟨x, property✝⟩)

So essentially this does the same as explicitly writing out @rfl _ x. The kernel will see that @rfl _ x and should therefore perform basically the same defeq check as above. And indeed,

instance : IsScalarTower Rs As B := .of_algebraMap_eq fun ⟨x, _⟩ ↦ (rfl : x = x)
instance : IsScalarTower Rs As B := .of_algebraMap_eq fun ⟨x, _⟩ ↦ @rfl _ x

do not time out in the kernel!

What show x = x from rfl does is defined in docs#Lean.Elab.Term.elabShow: it comes down to inserting a term let this : x = x := rfl; this. This whole term is passed to the kernel which will end up checking that this : x = x has the expected type and so we get essentially the same unification goal again.

Crucially, show explicitly shows up in the term passed to the kernel, while the type ascription (rfl : x = x) just so happens to set up the implicit variables correctly. This is why show is sometimes more powerful than type ascription: it keeps the expected type around explicitly.