Zulip Chat Archive

Stream: general

Topic: Diamond problem in mv_polynomial

Devon Tuma (Dec 27 2020 at 20:35):

I'm running into problems trying to use theorems about polynomial (mv_polynomial (fin n) R) when R is a comm_ring instead of just a comm_semiring. The issue seems to be that the semiring instance inferred on mv_polynomial (fin n) R is different depending on the context of the terms, and these instances aren't definitionally equal. This should be a mwe of the type of thing I'm running into:

import data.mv_polynomial.equiv
-- The issue only appears if `ring_theory.polynomial.basic` has been imported
import ring_theory.polynomial.basic

noncomputable example {R : Type*} [hR : comm_ring R] (n : ℕ) :
  mv_polynomial (option (fin n)) R ≃+* polynomial (mv_polynomial (fin n) R) :=
begin
  -- This instance is what is synthesized in the polynomial in the goal
  -- let sr2 : semiring (mv_polynomial (fin n) R) := ring.to_semiring,

  have := mv_polynomial.option_equiv_left R (fin n),
  -- This instance is what is synthesized in the above expression
  -- let sr1 : semiring (mv_polynomial (fin n) R) := comm_semiring.to_semiring,

  -- the below expression times out, unless `hR` is replaced with `comm_semiring R`
  exact this,
end

I've found a couple work-arounds for the specific use cases I have, but they seem like hacks and I feel there should probably be a better solution for this.

Eric Wieser (Dec 27 2020 at 21:17):

Is something marked irreducible here? Perhaps mv_polynomial or polynomial?

Devon Tuma (Dec 27 2020 at 21:36):

It doesn't seem like anything is irreducible as far as I can tell, both definitions are just in terms of finsupp, but I'm not sure how to check for sure

Eric Wieser (Dec 27 2020 at 21:39):

So the code runs without error without the second import?

Devon Tuma (Dec 27 2020 at 21:42):

Yes, I think you can go a step further and only import data.mv_polynomial.comm_ring and get the same error, since that is what gives the comm_ring instance on mv_polynomial, which I think is what gives the distinct semiring structure on the mv_polynomial

Eric Wieser (Dec 27 2020 at 21:44):

I would guess this line causes the trouble: https://github.com/leanprover-community/mathlib/blob/5c8c122226776201eba48f45a991e86084d77375/src/ring_theory/polynomial/basic.lean#L32

Devon Tuma (Dec 27 2020 at 21:44):

But yes if data.mv_polynomial.equiv is the only import then there isn't any issue

Eric Wieser (Dec 27 2020 at 21:45):

I would guess this line causes the trouble: https://github.com/leanprover-community/mathlib/blob/5c8c122226776201eba48f45a991e86084d77375/src/ring_theory/polynomial/basic.lean#L32

Eric Wieser (Dec 27 2020 at 21:46):

Where's the docs#mv_polynomial.comm_semiring instance?

Devon Tuma (Dec 27 2020 at 21:46):

I think that is too high in the dependency tree to be the culprit, since just data.mv_polynomial.comm_ring causes the timeout without importing anything from ring_theory/*

Eric Wieser (Dec 27 2020 at 21:48):

Somehow my clipboard had the wrong thing in it. I meant to link to the file you mentioned...

Devon Tuma (Dec 27 2020 at 21:50):

I don't think there is just a ring instance on mv_polynomial, the derived ring instance just seems to come from the comm_ring instance

Devon Tuma (Dec 27 2020 at 21:51):

Oh sorry, I see your edit, the comm_semiring comes from data.mv_polynomial.basic

Eric Wieser (Dec 27 2020 at 21:54):

Seems odd that they'd form a diamond

Eric Wieser (Dec 27 2020 at 21:55):

Does convert this give any more helpful output than exact this? Or perhaps convert this using 1

Devon Tuma (Dec 27 2020 at 21:57):

Both still just timeout (although they take much longer to timeout than exact)

Devon Tuma (Dec 27 2020 at 21:58):

I'm not 100% sure it is a diamond problem but the different semiring instances were the only differences I could find between the terms.

Kevin Buzzard (Dec 27 2020 at 22:06):

If you change {R : Type*} to {R : Type u} then it works fine.

Kevin Buzzard (Dec 27 2020 at 22:08):

There are other times when this sort of thing has happened and I'm not entirely sure that people have got to the bottom of it. Type* means "Lean, solve this universe problem for me in the most general way possible automatically"; Type u means "Lean, I claim this choice works".

Devon Tuma (Dec 27 2020 at 22:11):

Ah, thank you, I hadn't even thought to try changing that, I didn't realize Type* could be dangerous to use.

Kevin Buzzard (Dec 27 2020 at 22:12):

It's just one of those things you pick up if you hang around here. I don't know why it's dangerous but you've got a pretty neat example here, I'm trying to minimise. Reid once told me he never used Type*. Right now I don't know whether the issue was that you just asked Lean to solve a super-hard universe unification question or whether it's something else.

Eric Wieser (Dec 27 2020 at 22:13):

Is this a problem that goes away if you use lemma instead of example?

Eric Wieser (Dec 27 2020 at 22:14):

Since I've seen def look at the body to determine it's type, but I haven't seen lemma do that

Kevin Buzzard (Dec 27 2020 at 22:14):

Yes

Devon Tuma (Dec 27 2020 at 22:15):

Although I can replicate it inside of a lemma in a much less minimized version (since I came across this while trying to prove a lemma)

Kevin Buzzard (Dec 27 2020 at 22:21):

import data.mv_polynomial.equiv

universes u v

-- uncomment this and the first example times out and the second two take much longer to compile

--noncomputable instance {R : Type u} [comm_ring R] {σ : Type v} : comm_ring (mv_polynomial σ R) :=
--add_monoid_algebra.comm_ring

noncomputable example {R : Type*} [comm_ring R] (n : ℕ) :
  mv_polynomial (option (fin n)) R ≃+* polynomial (mv_polynomial (fin n) R) :=
mv_polynomial.option_equiv_left R (fin n)

noncomputable lemma foo {R : Type*} [comm_ring R] (n : ℕ) :
  mv_polynomial (option (fin n)) R ≃+* polynomial (mv_polynomial (fin n) R) :=
mv_polynomial.option_equiv_left R (fin n)

noncomputable example {R : Type u} [comm_ring R] (n : ℕ) :
  mv_polynomial (option (fin n)) R ≃+* polynomial (mv_polynomial (fin n) R) :=
mv_polynomial.option_equiv_left R (fin n)

Devon Tuma (Dec 27 2020 at 22:28):

I still get a timeout when I'm trying to use some of these things internally to a lemma though:

import data.mv_polynomial.equiv
-- The issue only appears if `ring_theory.polynomial.basic` has been imported
import data.mv_polynomial.comm_ring

universe u

noncomputable lemma ex {R : Type u} [hR : comm_ring R] (n : ℕ) : ℕ :=
begin
  -- This times out unless `hR` is switched to `comm_semiring`
  have : mv_polynomial (fin (n + 1)) R ≃+* polynomial (mv_polynomial (fin n) R) :=
    mv_polynomial.fin_succ_equiv R n,

  exact 0
end

Eric Wieser (Dec 27 2020 at 22:57):

I think this might be a bug feature I don't understand in tactic#have?

Eric Wieser (Dec 27 2020 at 22:57):

The problem doesn't exist in term-mode have

Eric Wieser (Dec 27 2020 at 22:58):

noncomputable lemma ex {R : Type u} [hR : comm_ring R] (n : ℕ) : ℕ :=
have mv_polynomial (fin (n + 1)) R ≃+* polynomial (mv_polynomial (fin n) R) :=
    mv_polynomial.fin_succ_equiv R n,
begin
  exact 0
end

Devon Tuma (Dec 27 2020 at 23:37):

Thanks, jumping in and out of term-mode seems to solve all the time-outs I was getting with tactic#have and tactic#let, although it does make the proofs look a bit strange

Kevin Buzzard (Dec 27 2020 at 23:57):

Does making universes explicit solve any problems?

Devon Tuma (Dec 28 2020 at 00:10):

I've made all the proofs I'm writing explicit about universes and still have the issue. And data.mv_polynomial.equiv already uses explicit universes. I'll have to do some digging to see if any of the definitions I'm importing might still have implicit universes though, and see if modifying those helps.

Kevin Buzzard (Dec 28 2020 at 00:14):

I think the universe thing all happens at compile time, I don't think changing *s to us in other theorems will change anything -- it might change what happens when it compiles, but it won't change the type of the term at all I don't think.

Mario Carneiro (Dec 28 2020 at 00:16):

I don't think using * instead of u has any detrimental effects unless you can see the type of the theorem change

Mario Carneiro (Dec 28 2020 at 00:16):

I still think it is best to prefer * when possible, because lean's automatic universe handling is generally the right thing to do

Kevin Buzzard (Dec 28 2020 at 00:23):

We have here an explicit example of where lean's automatic universe handling is timing out and telling it "Type u works fine" doesn't time out :-/

Mario Carneiro (Dec 28 2020 at 00:25):

It's not clear to me that universe handling is the problem though, it seems typeclass inference is to blame here

Mario Carneiro (Dec 28 2020 at 00:25):

you are saying it works better if you are more explicit about things and yes that's probably true but it doesn't mean we shouldn't make the normal inference work

Kevin Buzzard (Dec 28 2020 at 00:26):

@ring_equiv.{u_1 u_1} (@mv_polynomial.{0 u_1} (option.{0} (fin n)) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
  (@polynomial.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
     (@ring.to_semiring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
        (@comm_ring.to_ring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
           (@mv_polynomial.comm_ring.{u_1 0} R _inst_2 (fin n)))))
  (@distrib.to_has_mul.{u_1}
     (@mv_polynomial.{0 u_1} (option.{0} (fin n)) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
     (@ring.to_distrib.{u_1}
        (@mv_polynomial.{0 u_1} (option.{0} (fin n)) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
        (@comm_ring.to_ring.{u_1}
           (@mv_polynomial.{0 u_1} (option.{0} (fin n)) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
           (@mv_polynomial.comm_ring.{u_1 0} R _inst_2 (option.{0} (fin n))))))
  (@distrib.to_has_add.{u_1}
     (@mv_polynomial.{0 u_1} (option.{0} (fin n)) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
     (@ring.to_distrib.{u_1}
        (@mv_polynomial.{0 u_1} (option.{0} (fin n)) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
        (@comm_ring.to_ring.{u_1}
           (@mv_polynomial.{0 u_1} (option.{0} (fin n)) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
           (@mv_polynomial.comm_ring.{u_1 0} R _inst_2 (option.{0} (fin n))))))
  (@distrib.to_has_mul.{u_1}
     (@polynomial.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
        (@ring.to_semiring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
           (@comm_ring.to_ring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
              (@mv_polynomial.comm_ring.{u_1 0} R _inst_2 (fin n)))))
     (@ring.to_distrib.{u_1}
        (@polynomial.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
           (@ring.to_semiring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
              (@comm_ring.to_ring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
                 (@mv_polynomial.comm_ring.{u_1 0} R _inst_2 (fin n)))))
        (@polynomial.ring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
           (@comm_ring.to_ring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
              (@mv_polynomial.comm_ring.{u_1 0} R _inst_2 (fin n))))))
  (@distrib.to_has_add.{u_1}
     (@polynomial.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
        (@ring.to_semiring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
           (@comm_ring.to_ring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
              (@mv_polynomial.comm_ring.{u_1 0} R _inst_2 (fin n)))))
     (@ring.to_distrib.{u_1}
        (@polynomial.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
           (@ring.to_semiring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
              (@comm_ring.to_ring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
                 (@mv_polynomial.comm_ring.{u_1 0} R _inst_2 (fin n)))))
        (@polynomial.ring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
           (@comm_ring.to_ring.{u_1} (@mv_polynomial.{0 u_1} (fin n) R (@comm_ring.to_comm_semiring.{u_1} R _inst_2))
              (@mv_polynomial.comm_ring.{u_1 0} R _inst_2 (fin n))))))

is the problem, I suspect.

Mario Carneiro (Dec 28 2020 at 00:26):

Why do these goals always make me weep

Kevin Buzzard (Dec 28 2020 at 00:26):

That's what maths actually looks like when you do it this way

Mario Carneiro (Dec 28 2020 at 00:27):

This is not something that ever happens in metamath, and the problems that are dealt with are around the same level of complexity

Mario Carneiro (Dec 28 2020 at 00:27):

so I don't buy the "this is reality" argument

Kevin Buzzard (Dec 28 2020 at 00:27):

right, I'm not saying maths is wrong, I'm saying the way this is all set up in Lean 3 is somehow wrong

Eric Wieser (Dec 28 2020 at 00:28):

Isn't there an issue here that we train people to use example instead of lemma, but example fails above and lemma doesn't?

Eric Wieser (Dec 28 2020 at 00:28):

Do we need a lemma_example?

Mario Carneiro (Dec 28 2020 at 00:29):

The reason that makes a difference is that example is like def in that the value of the definition affects the inference of the statement

Kevin Buzzard (Dec 28 2020 at 00:29):

lemma example does that, I think

Mario Carneiro (Dec 28 2020 at 00:29):

wait what?

Kevin Buzzard (Dec 28 2020 at 00:29):

I mean just call the lemma example

Eric Wieser (Dec 28 2020 at 00:29):

Well, right now I assume #mwe tells people to use example

Mario Carneiro (Dec 28 2020 at 00:30):

oh, I thought you had discovered some long lost keyword combination

Mario Carneiro (Dec 28 2020 at 00:30):

incidentally, you can't name a lemma example because it's a keyword

Eric Wieser (Dec 28 2020 at 00:30):

Huh, it doesn't actually recommend example

Mario Carneiro (Dec 28 2020 at 00:31):

There is nothing wrong with example per se, it's just one part of the confluence that leads to the bug here

Mario Carneiro (Dec 28 2020 at 00:31):

It's useful to have example perform inference of the statement from the value because otherwise you wouldn't be able to do e.g. example := 1

Mario Carneiro (Dec 28 2020 at 00:32):

with a lemma that would have to be lemma foo : nat := 1 where nat is required

Mario Carneiro (Dec 28 2020 at 00:32):

So somehow mv_polynomial.option_equiv_left is implicated in this issue

Eric Wieser (Dec 28 2020 at 00:34):

Sure, I'm not saying example is broken - just that encouraging people to use example : some_prop := sorry in zulip is setting an unnecessary trap that would be resolved if we had the hypothetical lemma example

Eric Wieser (Dec 28 2020 at 00:35):

Do you know where the part of lean is that defines theorem / lemma etc?

Mario Carneiro (Dec 28 2020 at 00:35):

I don't think it's a trap either

Mario Carneiro (Dec 28 2020 at 00:36):

I think Kevin found a bug that involves example and Type*

Mario Carneiro (Dec 28 2020 at 00:36):

and it doesn't on its own mean that example and/or Type* should be avoided

Kevin Buzzard (Dec 28 2020 at 00:36):

Where is that list of useful options? I want to see what typeclass stuff is happening

Mario Carneiro (Dec 28 2020 at 00:37):

set_option trace.class_instances true

Kevin Buzzard (Dec 28 2020 at 00:39):

First we get lots of these:

[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @submodule.quotient.has_add ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @linear_map.has_add ?x_7 ?x_8 ?x_9 ?x_10 ?x_11 ?x_12 ?x_13 ?x_14
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @finsupp.has_add ?x_15 ?x_16 ?x_17
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @finset.has_add ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @set.has_add ?x_21 ?x_22
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := enat.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := ?x_28.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := ?x_31.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @matrix.has_add ?x_32 ?x_33 ?x_34 ?x_35 ?x_36 ?x_37
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := ?x_40.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := ?x_43.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @multiset.has_add ?x_44
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @opposite.has_add ?x_45 ?x_46
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := rat.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @with_top.has_add ?x_47 ?x_48
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @prod.has_add ?x_49 ?x_50 ?x_51 ?x_52
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @additive.has_add ?x_53 ?x_54
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @with_zero.has_add ?x_55 ?x_56
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @add_monoid_hom.has_add ?x_57 ?x_58 ?x_59 ?x_60
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @pi.has_add ?x_61 ?x_62 ?x_63
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := native.float.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := unsigned.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @fin.has_add ?x_64
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := int.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := options.has_add

Kevin Buzzard (Dec 28 2020 at 00:40):

Then all of a sudden, the breakthrough:

[class_instances] (0) ?x_0 : has_add
  (@polynomial (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
     (@ring.to_semiring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
        (@comm_ring.to_ring (@mv_polynomial (fin n) R (@comm_ring.to_comm_semiring R _inst_2))
           (@baz R _inst_2 (fin n))))) := @distrib.to_has_add ?x_65 ?x_66

Could polynomials be a distrib?

Mario Carneiro (Dec 28 2020 at 00:45):

I think this is the core problem:

example {R : Type*} [comm_ring R] (n : ℕ) :
  @comm_semiring.to_semiring _ (@mv_polynomial.comm_semiring R (fin n) (@comm_ring.to_comm_semiring R _inst_1)) =
  (@ring.to_semiring _ (@comm_ring.to_ring _ (@mv_polynomial.comm_ring R _inst_1 (fin n)))) :=
rfl

this is slow exactly in the same cases as the original

Mario Carneiro (Dec 28 2020 at 00:47):

I think that this sums up the problems with the diamond problems in lean 3. This rfl is true but lean has to do a stupid amount of work to prove it

Mario Carneiro (Dec 28 2020 at 00:48):

because it basically has to completely unfold the definition of mv_polynomials, look at all of the fields and note that they are the same

Mario Carneiro (Dec 28 2020 at 00:49):

If only we could prove these definitional equalities and maybe hint to the unifier to use them

Kevin Buzzard (Dec 28 2020 at 00:49):

Lean 4 has unification hints! As does Lean 3, right?

Mario Carneiro (Dec 28 2020 at 00:52):

I don't know how well lean (or even DTT in general) can handle "proofs of defeq" though. Especially hypothetical defeq theorems, i.e. "if A = B is defeq then C = D is defeq" don't exist in DTT proper, even though they are as important as lemmas in regular mathematics in theory, providing super-exponential speedups in some problems

Last updated: Dec 20 2023 at 11:08 UTC