RingTheory.Subring.Basic !4#1945

Stream: mathlib4

[Johan Commelin]

This is a massive red carpet. I guess not so surprising, since there is Basic in the filename.

[Johan Commelin]

It starts with all sorts of TC timeouts.

[Kevin Buzzard]

First timeout is:

    [tryResolve] [5.509188s] 💥 NoZeroDivisors { x // x ∈ s } ≟ NoZeroDivisors { x // x ∈ ?m.11435 } ▼
      [] [0.000336s] ✅ NonAssocSemiring R ▶
      [] [0.000433s] ✅ SubsemiringClass S R ▶

and this is hard to diagnose because this says "I'm taking 5 seconds to do something, but all I'm going to tell you about what I did was two things which happened super-quickly

[Gabriel Ebner]

If you turn on set_option trace.Meta.isDefEq true you will see what's going on.

[Gabriel Ebner]

Wow this is a ride. In order to check that * is *, we check that the two semirings are the same. In order to do that, we check that the types of the distributivity axioms match (!!). In order to check the distributivity axioms, we check that + is + (presumably also * but we never get there). In order to check +, we check that the two additive monoids are the same. And in order to check the additive monoids, ... I think you get the idea.

[Reid Barton]

Related: https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/isDefEq.20on.20structures/near/324548803

[Mario Carneiro]

Surely lean4#2003 will solve that?

[Johan Commelin]

In cases like this, is it possible for Lean to detect that it only needs to check that the data fields are defeq?

[Johan Commelin]

That's not what 2003 does, right? I thought it fixed a different issue.

[Mario Carneiro]

no, that's reid's proposal in the related thread

[Mario Carneiro]

2003 fixes the "In order to check that * is *, we check that the two semirings are the same." part

[Jireh Loreaux]

Per the lean4#2003 meme, does it also fix the issue described here? I assume not because I think that's about unification.

[Kevin Buzzard]

That issue is now lean4#2074 BTW.

[Johan Commelin]

This PR is now moving again!

[Johan Commelin]

I need to do something else for a bit. But the amount of red errors left is now really small

[Eric Wieser]

port-status#ring_theory/subring/basic says the PR is already out of sync; can we pull in the latest mathport?

[Eric Wieser]

I think the change in question was a backport specifically to fix this file, so it might be as simple as updating the SHA

[Johan Commelin]

1 error left, which is quite mysterious to me

[Johan Commelin]

-- Porting note: Lean can find this instance already
/-- The action by a subring is the action by the underlying ring. -/
instance [Zero α] [SMulWithZero R α] (S : Subring R) : SMulWithZero S α :=
  inferInstanceAs (SMulWithZero S.toSubsemiring α) -- works

-- Porting note: Lean can *not* find this instance already
/-- The action by a subring is the action by the underlying ring. -/
instance [Zero α] [MulActionWithZero R α] (S : Subring R) : MulActionWithZero S α :=
  Subsemiring.mulActionWithZero S.toSubsemiring -- works
  -- inferInstanceAs (MulActionWithZero S.toSubsemiring α) -- Porting note: does not work

-- Porting note: Lean can *not* find this instance already
/-- The action by a subring is the action by the underlying ring. -/
instance [AddCommMonoid α] [Module R α] (S : Subring R) : Module S α :=
  inferInstanceAs (Module S.toSubsemiring α) -- Porting note: does not work

[Johan Commelin]

Incoming hack

[Johan Commelin]

/-- The action by a subring is the action by the underlying ring. -/
instance [AddCommMonoid α] [Module R α] (S : Subring R) : Module S α :=
  -- inferInstanceAs (Module S.toSubsemiring α) -- Porting note: does not work
  let aux : ∀ {R : Type _} {M : Type _} [Semiring R] [AddCommMonoid M] [Module R M]
      (S : Subsemiring R), Module S M := by
    intro R M _ _ _ S
    infer_instance
  aux S.toSubsemiring

[Johan Commelin]

This works :see_no_evil:

[Johan Commelin]

The file is error free, the linter seems happy

[Adam Topaz]

It seems that let can help with a lot of the silly unification issues that pop up in lean4 which did not happen in lean3

[Kevin Buzzard]

Looking at the trace for the first failure, Lean wants to use Subsemiring.mulActionWithZero but it can't solve x ∈ S =?= x ∈ ?m.260191 because ?m.260191 : Subsemiring ?m.260186 and S : Subring R. I would go on a minimisation binge but I need to get a bunch of marking done urgently.

[Eric Wieser]

I think naming the instance directly like you do in your first code block is better than the aux hack

[Johan Commelin]

The aux hack is localised

[Johan Commelin]

My impression was that naming instances is considered evil.

[Eric Wieser]

Isn't adding extra terms to unfold in an instance more evil?

[Eric Wieser]

It certainly was considered so in lean 3

[Johan Commelin]

Eric Wieser said:

I think naming the instance directly like you do in your first code block is better than the aux hack

Done

[Eric Wieser]

A related problem is that a lot of our docstrings say Foo.semiring is a main result; if we don't name our instances they're hard to link from docstrings

[Johan Commelin]

We could mention Semiring Foo as the main result. But it wouldn't result in a hyperlink in the docs.

[Yaël Dillies]

Naming instances was considered evil in Lean 3 because the automatic naming algorithm was usually doing a better job at it than us. I'm not sure we can pretend the same about the Lean 4 one :grinning_face_with_smiling_eyes:

[Eric Wieser]

The hyperlink is often pretty valuable given the instance usually holds under assumptions not mentioned in the module docstring.