Zulip Chat Archive

Stream: general

Topic: algebra.semiring_to_ring breaks semimodule typeclass lookup

Eric Wieser (Oct 07 2020 at 16:12):

Which is consistent with haveI : semimodule ℕ (tensor_algebra R M) := infer_instance, succeeding and haveI : semimodule R (tensor_algebra R M) := infer_instance, failing. I can only assume this failure is very related to #4289, which is unfortunate, because it means that we can't do subtraction in the tensor / free / clifford /... algebras

Johan Commelin (Oct 07 2020 at 16:15):

this is beyond my pay grade :sad:

Eric Wieser (Oct 07 2020 at 16:17):

Perhaps a better #mwe:

import linear_algebra.tensor_algebra

variables (R : Type*) (M : Type*) [add_comm_group M] [comm_ring R] [semimodule R M]

example (a b : tensor_algebra R M) : sorry := begin
  -- this poisons the instance cache somehow and makes the next line fail
  haveI : ring (tensor_algebra R M) := algebra.semiring_to_ring R,
  haveI : semimodule R (tensor_algebra R M) := infer_instance,
  sorry
end

Eric Wieser (Oct 07 2020 at 16:17):

Whose pay grade might this be within? It's certainly well beyond mine...

Reid Barton (Oct 07 2020 at 16:18):

haveI : ring ... is almost always wrong, should be letI at least

Reid Barton (Oct 07 2020 at 16:18):

without any other idea of what is happening here

Eric Wieser (Oct 07 2020 at 16:20):

Behavior is the same either way

Eric Wieser (Oct 07 2020 at 16:30):

To take tactics out of the equation, this also fails:

import linear_algebra.tensor_algebra

variables (R : Type*) (M : Type*) [add_comm_group M] [comm_ring R] [semimodule R M]

-- this poisons the instance cache somehow and makes the next line fail
instance : ring (tensor_algebra R M) := algebra.semiring_to_ring R

instance : semimodule R (tensor_algebra R M) := infer_instance

Unfortunately I can't ask the author of docs#algebra.semiring_to_ring what the problem is, as that's me...

Reid Barton (Oct 07 2020 at 16:31):

what's the error

Eric Wieser (Oct 07 2020 at 16:32):

Unhelpful:

failed to synthesize type class instance for
R : Type u_1,
M : Type u_2,
_inst_1 : add_comm_group M,
_inst_2 : comm_ring R,
_inst_3 : semimodule R M
⊢ semimodule R (tensor_algebra R M)

Eric Wieser (Oct 07 2020 at 16:33):

The tactic state showed by vs-code is identical with and without the poisoned line, the only difference is whether it succeeds or fails

Reid Barton (Oct 07 2020 at 16:35):

What happens if in semiring_to_ring you swap the two .. lines?

Eric Wieser (Oct 07 2020 at 16:37):

Will try that. FWIW, with verbose printing the difference between good and bad is

--- bad
+++ good
@@ -7,10 +7,9 @@
R : Type u_1,
M : Type u_2,
_inst_1 : add_comm_group M,
_inst_2 : comm_ring R,
_inst_3 :
  @semimodule R M (@ring.to_semiring R (@comm_ring.to_ring R _inst_2)) (@add_comm_group.to_add_comm_monoid M _inst_1)
 ⊢ @semimodule R
     (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1) _inst_3)
     (@ring.to_semiring R (@comm_ring.to_ring R _inst_2))
-    (@add_comm_group.to_add_comm_monoid
+    (@semiring.to_add_comm_monoid
        (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
           _inst_3)
-       (@ring.to_add_comm_group
-          (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
-             _inst_3)
-          (@tensor_algebra.ring R M _inst_1 _inst_2 _inst_3)))
+       (@tensor_algebra.semiring R (@comm_ring.to_comm_semiring R _inst_2) M
+          (@add_comm_group.to_add_comm_monoid M _inst_1)
+          _inst_3))

Reid Barton (Oct 07 2020 at 16:39):

Currently my theory, which may or may not be possible, is that finding the semimodule R (tensor_algebra R M) instance requires the entire semiring (tensor_algebra R M) instance to match (not just match fieldwise, because of a lack of eta expansion for structures) and that the way that algebra.semiring_to_ring is implemented causes the underlying semiring to be broken up and reassembled rather than preserved as a unit.

Eric Wieser (Oct 07 2020 at 16:41):

Yeah, the idea seems sensible to me

Reid Barton (Oct 07 2020 at 16:46):

actually, wait. These are old_structure_cmd structures, right? So the semiring instance is never preserved as a unit

Reid Barton (Oct 07 2020 at 16:46):

I'm confused how this doesn't cause more problems in general

Eric Wieser (Oct 07 2020 at 16:47):

Yes, they are. I don't know what this refers to, but semiring_to_ring is currently used in only one place

Eric Wieser (Oct 07 2020 at 16:51):

Finallly tested your idea - it made no difference unfortunately

Eric Wieser (Oct 07 2020 at 16:56):

An even further reduced example without infer_instance, that gives a better error message:

import linear_algebra.tensor_algebra

variables (R : Type*) (M : Type*) [add_comm_group M] [comm_ring R] [semimodule R M]

instance working_instance : semimodule R (tensor_algebra R M) := infer_instance

-- this poisons the instance cache somehow and makes the next line fail
instance : ring (tensor_algebra R M) := algebra.semiring_to_ring R

instance : semimodule R (tensor_algebra R M) := working_instance R M

Error message

Reid Barton (Oct 07 2020 at 17:02):

OK, now I understand why what I was worried about before isn't a problem. Both semiring.to_add_comm_monoid and add_comm_group.to_add_comm_monoid are going to return constructors of the form { add := ..., zero := ..., ... } so they will be defeq as soon as the add and zero fields are defeq.
So, that suggests that the add and/or zero fields must not be defeq for some reason...

Eric Wieser (Oct 07 2020 at 17:09):

I'll have a go at proving the types are equal...

Reid Barton (Oct 07 2020 at 17:14):

I managed to reproduce the error in whatever version of mathlib I have lying around so I no longer have to pester you with things to try.

Reid Barton (Oct 07 2020 at 17:16):

Curiously Lean does seem to think both the add and zero fields of those instances are defeq even though the instances are not.
It would be nice to have a #whnf user command...

Eric Wieser (Oct 07 2020 at 17:16):

I was at least able to get to the point where the definitions looked almost equal:

Long code...

Reid Barton (Oct 07 2020 at 17:20):

Curiously Lean also thinks both instances reduce to constructors--sorry for atrocious formatting:

#check (rfl : (@semiring.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@tensor_algebra.semiring R (@comm_ring.to_comm_semiring R _inst_2) M
          (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)) = @add_comm_monoid.mk _ _ _ _ _ _ _)

#check (rfl : (@add_comm_group.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@ring.to_add_comm_group
          (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
             _inst_3)
          (@tensor_algebra.ring R M _inst_1 _inst_2 _inst_3))) = @add_comm_monoid.mk _ _ _ _ _ _ _)

Reid Barton (Oct 07 2020 at 17:24):

Curiously congr closes your goal that refl can't, and looking at the term is not illuminating...

Reid Barton (Oct 07 2020 at 17:38):

Well this is something, Lean apparently doesn't think the add_assoc fields of these two instance are equal, even though they are proofs of the same proposition. Same for the other proof fields I tested.

Reid Barton (Oct 07 2020 at 17:42):

import linear_algebra.tensor_algebra

variables (R : Type*) (M : Type*) [_inst_1 : add_comm_group M] [_inst_2 : comm_ring R] [_inst_3 : semimodule R M]

instance working_instance : semimodule R (tensor_algebra R M) := infer_instance

instance : ring (tensor_algebra R M) := algebra.semiring_to_ring R

def x :
  @add_comm_monoid.add_assoc _
    (@semiring.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@tensor_algebra.semiring R (@comm_ring.to_comm_semiring R _inst_2) M
          (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3))
  =
  @add_comm_monoid.add_assoc _
    (@add_comm_group.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@ring.to_add_comm_group
          (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
             _inst_3)
          (@tensor_algebra.ring R M _inst_1 _inst_2 _inst_3))) :=
rfl                             -- doesn't work
/-     -- works
begin
  have : ∀ (P : Prop) (p q : P), p = q := λ P p q, rfl,
  apply this,
end  -/

Eric Wieser (Oct 07 2020 at 17:51):

Well that's bizarre

Eric Wieser (Oct 07 2020 at 17:57):

attribute [semireducible] tensor_algebra fixes your example, and some but not all of the ones in this thread

Eric Wieser (Oct 07 2020 at 17:57):

cc @Scott Morrison, who suggested that it should be irreducible (which without that line it currently is)

Reid Barton (Oct 07 2020 at 18:02):

OK, well, that makes a tiny bit more sense I guess. The two sides really are defeq but the elaborator thinks they aren't?
It's worth noting that you do have to do some work to see that the two proofs are proofs of the same proposition (because they are about syntactically different +s). I don't see what making the type tensor_algebra not irreducible would have to do with this, though.

Reid Barton (Oct 07 2020 at 18:05):

Even with this irreducible business it's still really weird. The elaborator knows the two sides have the same type because there is no type error if you put _ as the definition (or indeed the begin...end block in the comment).

Reid Barton (Oct 07 2020 at 18:08):

It also makes me wonder how much work Lean does in general checking that proofs are defeq

Mario Carneiro (Oct 07 2020 at 19:58):

Oh, the conclusion of this thread is not good at all

Mario Carneiro (Oct 07 2020 at 19:59):

Lean should definitely have an early out checking that proofs are defeq

Reid Barton (Oct 07 2020 at 20:25):

I guess it would be good to create a self-contained reproducer.

Eric Wieser (Oct 07 2020 at 21:18):

Without mathlib, you mean?

Patrick Massot (Oct 07 2020 at 21:20):

Yes.

Wojciech Nawrocki (Oct 08 2020 at 04:46):

Fwiw I experimented with proof reduction a little back when it became known that it can loop in Lean's type theory. It's been a while so I'm very fuzzy on the details, but as far as I remember, there are checks to exit reduction early if the term is a proof since at least for typechecking, irrelevance applies. However life is not so simple, mainly due to unification. It turns out that things sometimes have to be reduced to infer some metas.

Mario Carneiro (Oct 08 2020 at 07:05):

I recall there being a recent crackdown on such unifications in 3.14 or so, it broke a bunch of proofs that were doing just that. Are you sure this is still the case?

Gabriel Ebner (Oct 08 2020 at 07:51):

We only removed support to unfold theorems (i.e. δ-reduction). Nothing changed about the unification algorithm otherwise. Though there is a big "if both sides are proofs and the types are defeq, exit" statement at the top.

Wojciech Nawrocki (Oct 08 2020 at 14:22):

Indeed, there is a check, but it's more at the bottom.

Eric Wieser (Oct 13 2020 at 11:58):

Do we think this can be fixed by just moving that check?

Oliver Nash (Oct 14 2020 at 13:28):

Eric Wieser said:

Do we think this can be fixed by just moving that check?

I doubt it will be that easy (though I'd love to be corrected!). I think the way to make progress here is for us to produce a version of this apparent bug that is independent of Mathlib. I spent a little time on this yesterday evening but could not even eliminate tensor_algebra. I'll try again this evening.

Eric Wieser (Oct 19 2020 at 13:54):

I assume you made no progress, @Oliver Nash?

Oliver Nash (Oct 19 2020 at 13:55):

Correct. About another hour spent on it last week but didn't really get anywhere.

Oliver Nash (Oct 19 2020 at 13:55):

I think with a sufficiently-big block of time, I could do it.

Eric Wieser (Oct 19 2020 at 13:57):

There was some related discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Can't.20find.20algebra.20instance/near/213566642, just to keep things connected together.

Eric Wieser (Oct 19 2020 at 15:36):

I think I've made some progress here, we shouldn't be using algebra.semiring_to_ring for tensor_algebra, as that clashes with ring_quot.ring

Adam Topaz (Oct 19 2020 at 15:38):

I think that will at least solve my issues from https://github.com/leanprover-community/mathlib/tree/tensor_algebra_adjunction

Eric Wieser (Oct 19 2020 at 15:39):

I think adding

instance {S : Type*} [comm_ring S] [semimodule S M] : ring (tensor_algebra S M) :=
ring_quot.ring (tensor_algebra.rel S M)

is a good start. I'm still struggling to make clifford_algebra happy with a similar definition though.

Adam Topaz (Oct 19 2020 at 15:39):

But ring_quot.ring is an instance, so why do we need to add it in the first place?

Eric Wieser (Oct 19 2020 at 15:40):

Because tensor_algebra = ring_quot only while the former is reducible

Eric Wieser (Oct 19 2020 at 15:40):

So we need to explictly re-export it

Adam Topaz (Oct 19 2020 at 15:40):

Oh right.

Eric Wieser (Oct 19 2020 at 15:40):

This would be a lot easier if @derive could handle instances with dependencies

Eric Wieser (Oct 19 2020 at 15:41):

But essentially I think we need to copy across all the ring_quot instances (that we care about) in tensor_algebra

Adam Topaz (Oct 19 2020 at 15:41):

Is there a ring instance for free_algebra?

Eric Wieser (Oct 19 2020 at 15:41):

Yes

Eric Wieser (Oct 19 2020 at 15:41):

Oh, wait

Eric Wieser (Oct 19 2020 at 15:41):

Yes, in the PR that this thread started with (#4289)

Eric Wieser (Oct 19 2020 at 15:41):

Let's check: docs#free_algebra.ring

Adam Topaz (Oct 19 2020 at 15:42):

Oh ok, so not in mathlib then. I've used algebra.semiring_to_ring for the free_algebra ajunction.

Eric Wieser (Oct 19 2020 at 15:44):

I'll update the PR shortly if I get this working

Eric Wieser (Oct 19 2020 at 16:51):

(I did not get this working)

Oliver Nash (Oct 19 2020 at 16:53):

I'm _delighted_ to see a possible resolution of this issue but are you sure this is the root cause? I was convinced that there was a serious bug in Lean based on @Reid Barton 's example. Have you tried removing ring_quot.ring and seeing if the problems disappear?

Mario Carneiro (Oct 19 2020 at 16:58):

I don't think there is a serious bug in lean (in the sense of anything compromising soundness), just one more elaborator edge case

Mario Carneiro (Oct 19 2020 at 16:58):

you can probably give that term straight to the kernel and it will work

Mario Carneiro (Oct 19 2020 at 16:59):

but it should really be minimized to make it appropriate for study

Oliver Nash (Oct 19 2020 at 17:02):

Mario Carneiro said:

I don't think there is a serious bug in lean (in the sense of anything compromising soundness), just one more elaborator edge case

Right! Thanks for clearing up my sloppy use of the phrase "serious bug"; indeed I had not intended to suggest there was anything approaching a soundness bug.

Oliver Nash (Oct 19 2020 at 17:03):

And minimizing that example is something I'd like to do. It's somewhat unglamorous work but I will try again.

Eric Wieser (Oct 19 2020 at 17:30):

I've put up a PR that at least adds the ring instances for free_algebra and tensor_algebra in #4692. I run into problems trying to extend to clifford_algebra or exterior_algebra, so I've left those until we get a better understanding of what's going on. @Oliver Nash's universal_enveloping_algebra manages to survive because it isn't marked irreducible!

Eric Wieser (Oct 20 2020 at 13:49):

exterior_algebra I could get with some rewrites in an instance definition: #4714

Eric Wieser (Oct 20 2020 at 14:01):

... which upon rebasing, leaves me with a 0 = 0 goal that refl can't close

Eric Wieser (Oct 20 2020 at 14:13):

I get the feeling that most of the difficulty here comes from the fact that ring does not extend semiring

Johan Commelin (Oct 21 2020 at 20:45):

import linear_algebra.tensor_product
import deprecated.subring

-- swap these ↑ two imports, and then `foo` will be happy
-- otherwise, get a timeout

import algebra.module.submodule

variables {R M N P Q : Type*} [comm_ring R]
variables [add_comm_group M] [module R M]
variables [add_comm_group N] [module R N]

open function

lemma injective_iff (f : M →ₗ[R] N) : function.injective f ↔ ∀ m, f m = 0 → m = 0 :=
add_monoid_hom.injective_iff f.to_add_monoid_hom

lemma foo (L : submodule R (unit → R)) :
  injective (tensor_product.map L.subtype L.subtype) :=
(injective_iff _).mpr (sorry)

Johan Commelin (Oct 21 2020 at 20:46):

(Thanks to Reid for helping me figure this out.)

Reid Barton (Oct 21 2020 at 20:48):

which mathlib commit are you on, in case it matters?

Johan Commelin (Oct 21 2020 at 20:52):

src/foo.lean on branch crazy

Johan Commelin (Oct 21 2020 at 20:53):

Which has 1 commit on top of commit df4500242eb6aa6ee20b315b185b0f97a9b359c

Kevin Buzzard (Oct 21 2020 at 20:53):

Is this related to the earlier rfl weirdness or is this some all-new weirdness?

Reid Barton (Oct 21 2020 at 21:11):

Good question!

Kevin Buzzard (Oct 21 2020 at 21:12):

I tried to unmathlibify the bad rfl but there was so much stuff which needed to be copy-pasted in :-/

Eric Wieser (Oct 21 2020 at 23:59):

I don't immediately see the connection to the rest of this thread

Johan Commelin (Oct 22 2020 at 03:28):

Neither do I, but note that the problem goes away if you remove any of the following three ingredients:

  • change unit -> R to a module like M
  • change L.subtype to some hom f
  • remove the tensor_product.map L.subtype, and just ask for injectivity of L.subtype.

Johan Commelin (Oct 22 2020 at 09:22):

#4735 fixes this particular problem. Once the oleans are there, I will test if it also solves it in the bigger context that I was working in.

Johan Commelin (Oct 22 2020 at 09:23):

@Eric Wieser It would be interesting to test if it also helps in your setting. (I don't expect so, but you never know.)

Johan Commelin (Oct 22 2020 at 09:42):

I can confirm that on the flat-module branch, the following snippet no longer times out:

lemma injective_rtensor_aux₁ [hM : flat R M] {n : ℕ} (L : submodule R (fin n → R)) :
  injective (L.subtype.rtensor M) :=
begin
  -- refine (injective_iff _).mpr _,
  -- rw [show M = M, from rfl],
  rw injective_iff,
  -- induction n with n IH,
  { sorry },
end

Johan Commelin (Oct 22 2020 at 09:42):

However, if I change the (fin n → R) into finsupps, then it still times out :sad: :cry: :angry_cat:

Johan Commelin (Oct 22 2020 at 09:54):

@Gabriel Ebner FYI, the PR #4735 is quasi-related to this thread.

Gabriel Ebner (Oct 22 2020 at 10:11):

Ok, then my preferred solution is just to remove the suspicious group/monoid/etc. instances. May I push to your branch?

Johan Commelin (Oct 22 2020 at 10:12):

Yes, certainly

Johan Commelin (Oct 22 2020 at 10:12):

@Gabriel Ebner Feel free to play around with flat-module as well

Johan Commelin (Oct 22 2020 at 10:12):

Although there is quite a lot going on there

Reid Barton (Oct 22 2020 at 11:54):

Do we have an explanation for why #4735 affects the behavior here at all?

Gabriel Ebner (Oct 22 2020 at 12:05):

docs#tensor_product.add_comm_group makes Lean construct a add_comm_group ↥L via is_add_subgroup, while we want submodule.semimodule instead.

Reid Barton (Oct 22 2020 at 12:10):

Oh right. I thought that when Johan and I were minimizing the example it didn't fail with deprecated.subring replaced by deprecated.subgroup though.

Reid Barton (Oct 22 2020 at 12:13):

Does this example involve actually non-defeq instances then? The only place I could see there being a problem is with neg

Gabriel Ebner (Oct 22 2020 at 13:52):

It definitely is about subtype.add_comm_group (you can check with local attribute [-instance]). I'm also not sure what is going on exactly (the type of linear_map is several lines long....).
My rationale for removing these instances is that we already want to get away from unbundled substructures, so when in doubt remove the already deprecated instances.

Johan Commelin (Oct 23 2020 at 07:54):

@maintainers anyone wants to look at #4735? Gabriel kindly fix some bad instances, but this is now touching 14 files, so it would be sad to let this bitrot.

Eric Wieser (Nov 05 2020 at 16:42):

I think my plan here is just to remove the irreducible attribute, unless something has changed in master to make this go away - having a nicely isolated "black box" definition seems less important than having a ring instance

Eric Wieser (Nov 05 2020 at 18:15):

Done in #4916 - I've err'd on the side of making all the involved types semireducible, to avoid running into any similar headaches later. I think it's fine to just make "don't directly use the inductive construction of the algebra" something that we check by eye in review, rather than trying to enforce it with attribute and creating unification problems.

Reid Barton (Nov 27 2020 at 21:51):

Did anyone ever figure out what was going on with this weird elaborator issue (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algebra.2Esemiring_to_ring.20breaks.20semimodule.20typeclass.20lookup/near/212593885)?

Kevin Buzzard (Nov 27 2020 at 22:16):

import linear_algebra.tensor_algebra

variables (R : Type*) (M : Type*) [add_comm_group M] [comm_ring R] [semimodule R M]

instance working_instance : semimodule R (tensor_algebra R M) := infer_instance

-- this poisons the instance cache somehow and makes the next line fail
instance foo : ring (tensor_algebra R M) := algebra.semiring_to_ring R

-- ...except that the issue is that `tensor_algebra` is irreducible
local attribute [semireducible] tensor_algebra

-- now works
instance : semimodule R (tensor_algebra R M) := working_instance R M

Kevin Buzzard (Nov 27 2020 at 22:18):

Amelia and I were talking about tensor_algebra on Thursday and she was having some crazy problems with things not unifying, and then we discovered that tensor_algebra was marked irreducible (or at least it was in the branch we were working on). Does this explain some stuff?

Adam Topaz (Nov 27 2020 at 22:25):

Oh no... more of this irreducible stuff @Eric Wieser

Kevin Buzzard (Nov 27 2020 at 22:30):

Now Yury is back with us I must get back to making with_top and with_bot irreducible...

Reid Barton (Nov 27 2020 at 22:31):

I think we knew about it being irreducible but the behavior is still really weird

Kevin Buzzard (Nov 27 2020 at 22:34):

import linear_algebra.tensor_algebra

variables (R : Type*) (M : Type*) [_inst_1 : add_comm_group M] [_inst_2 : comm_ring R] [_inst_3 : semimodule R M]

instance working_instance : semimodule R (tensor_algebra R M) := infer_instance

instance foo : ring (tensor_algebra R M) := algebra.semiring_to_ring R

-- this makes it work
local attribute [semireducible] tensor_algebra


def x :
  @add_comm_monoid.add_assoc _
    (@semiring.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@tensor_algebra.semiring R (@comm_ring.to_comm_semiring R _inst_2) M
          (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3))
  =
  @add_comm_monoid.add_assoc _
    (@add_comm_group.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@ring.to_add_comm_group
          (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
             _inst_3)
          (@foo R M _inst_1 _inst_2 _inst_3))) :=
          rfl -- now works

Kevin Buzzard (Nov 27 2020 at 22:35):

(I had to change an instance name presumably because of some recent Lean changes).

Kevin Buzzard (Nov 27 2020 at 22:36):

Oh I see, Eric already spotted this. And this doesn't explain everything?

Kevin Buzzard (Nov 27 2020 at 22:49):

import linear_algebra.tensor_algebra

variables (R : Type*) (M : Type*) [_inst_1 : add_comm_group M] [_inst_2 : comm_ring R] [_inst_3 : semimodule R M]

instance working_instance : semimodule R (tensor_algebra R M) := infer_instance

instance foo : ring (tensor_algebra R M) := algebra.semiring_to_ring R

--local attribute [semireducible] tensor_algebra

lemma add_comm_monoid.ext (α : Type*) (a b : add_comm_monoid α)
  (h : @add_comm_monoid.add _ a = @add_comm_monoid.add _ b) : a = b :=
begin
  tactic.unfreeze_local_instances,
  cases a,
  cases b,
  change a_add = b_add at h,
  congr',
  -- too lazy to prove zeros coincide
  sorry
end


def x :
  @add_comm_monoid.add_assoc _
    (@semiring.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@tensor_algebra.semiring R (@comm_ring.to_comm_semiring R _inst_2) M
          (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3))
  =
  @add_comm_monoid.add_assoc _
    (@add_comm_group.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@ring.to_add_comm_group
          (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
             _inst_3)
          (@foo R M _inst_1 _inst_2 _inst_3))) :=
begin
  congr',
  /-
  ⊢ semiring.to_add_comm_monoid (tensor_algebra R M) =
    add_comm_group.to_add_comm_monoid (tensor_algebra R M)
  -/
  apply add_comm_monoid.ext,
  refl,
end

There's a proof which keeps everything irreducible. Is the answer not just something like "these things are not unfolding because tensor_algebra is irreducible" or something? I don't really understand the problem properly.

Kevin Buzzard (Nov 27 2020 at 22:51):

Sorry-free:

import linear_algebra.tensor_algebra

variables (R : Type*) (M : Type*) [_inst_1 : add_comm_group M] [_inst_2 : comm_ring R] [_inst_3 : semimodule R M]

instance working_instance : semimodule R (tensor_algebra R M) := infer_instance

instance foo : ring (tensor_algebra R M) := algebra.semiring_to_ring R

--local attribute [semireducible] tensor_algebra

lemma add_comm_monoid.ext (α : Type*) (a b : add_comm_monoid α)
  (h_add : @add_comm_monoid.add _ a = @add_comm_monoid.add _ b)
  (h_zero : @add_comm_monoid.zero _ a = @add_comm_monoid.zero _ b) : a = b :=
begin
  tactic.unfreeze_local_instances,
  cases a,
  cases b,
  congr',
end


def x :
  @add_comm_monoid.add_assoc _
    (@semiring.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@tensor_algebra.semiring R (@comm_ring.to_comm_semiring R _inst_2) M
          (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3))
  =
  @add_comm_monoid.add_assoc _
    (@add_comm_group.to_add_comm_monoid
       (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
          _inst_3)
       (@ring.to_add_comm_group
          (@tensor_algebra R (@comm_ring.to_comm_semiring R _inst_2) M (@add_comm_group.to_add_comm_monoid M _inst_1)
             _inst_3)
          (@foo R M _inst_1 _inst_2 _inst_3))) :=
begin
  congr',
  /-
  ⊢ semiring.to_add_comm_monoid (tensor_algebra R M) =
    add_comm_group.to_add_comm_monoid (tensor_algebra R M)
  -/
  apply add_comm_monoid.ext,
  { refl },
  { refl }
end

Kevin Buzzard (Nov 27 2020 at 22:51):

This was exactly the sort of problem Amelia was having.

Kevin Buzzard (Nov 27 2020 at 22:54):

I see -- the point is that rfl is failing because some part of the system has convinced itself that the types of the proofs are equal, but some other part of the system cannot convince itself of this, because of irreducibility. Is that the issue?

Eric Wieser (Nov 27 2020 at 23:13):

I thought I removed all the offending irreducibles from mathlib

Eric Wieser (Nov 27 2020 at 23:14):

At least, the ones relating to free algebra

Kevin Buzzard (Nov 27 2020 at 23:15):

oh you're right, my mathlib was on some other branch which hadn't been merged with master for a while.

Eric Wieser (Nov 27 2020 at 23:16):

I made sure to add a test to prevent someone undoing this by accident

Kevin Buzzard (Nov 27 2020 at 23:16):

meh. You have to add local attribute [irreducible] tensor_algebra to get my code running.

Eric Wieser (Nov 27 2020 at 23:23):

Wait, for your code you have to make it _not_ reducible?

Kevin Buzzard (Nov 28 2020 at 07:47):

Otherwise the proof finishes sooner

Kevin Buzzard (Nov 28 2020 at 23:42):

set_option old_structure_cmd true

class foo (α : Type) :=
(bar : α)
(prop : bar = bar)

class foo' (α : Type) extends foo α :=
(prop' : bar = bar)

instance nat.foo : foo ℕ :=
{ bar := 0,
  prop := rfl }

instance nat.foo' : foo' ℕ :=
{ prop' := rfl,
  .. nat.foo }

class foo'' (α β : Type) [foo β] :=
(bar'' : β)

instance nat.foo'' : foo'' ℕ ℕ :=
{ bar'' := 1 }

def foo''.foo_to_foo' (α : Type) {β : Type} [foo β] [foo'' α β] : foo' β :=
{ prop' := rfl,
  .. (infer_instance : foo β) }

def typealias := ℕ

instance baz : foo' typealias := nat.foo'
instance typealias.foo'' : foo'' ℕ typealias := nat.foo''

def baz' : foo' typealias := foo''.foo_to_foo' ℕ

local attribute [irreducible] typealias

example : @foo'.bar _ baz = @foo'.bar _ baz' := rfl

/-
run_cmd tactic.add_decl
  (declaration.thm `X []  `(@foo'.prop _ baz = @foo'.prop _ baz')
  (pure `(eq.refl (@foo'.prop _ baz))))

#print X
-/

-- works if `typealias` is not made irreducible
example : @foo'.prop _ baz = @foo'.prop _ baz' := rfl -- fails

@Reid Barton @Gabriel Ebner

Bhavik Mehta (Nov 28 2020 at 23:42):

I feel like it's important to note that proof_irrel _ _ works in place of rfl

Kevin Buzzard (Nov 28 2020 at 23:43):

def they_are_equal {P : Prop} {h1 h2 : P} : h1 = h2 := rfl

example : @foo'.prop _ baz = @foo'.prop _ baz' := they_are_equal -- works

Kevin Buzzard (Nov 28 2020 at 23:43):

The run_cmd (which Chris wrote) also works

Kevin Buzzard (Nov 28 2020 at 23:45):

(ps thanks to Shing, Chris, Kenny and Bhavik for being foolhardy enough to watch the discord livestream and between them helping a lot)

Kevin Buzzard (Nov 28 2020 at 23:50):

Title needs to be changed to foo''.foo_to_foo' breaks foo' typeclass lookup

Kenny Lau (Nov 29 2020 at 14:41):

set_option old_structure_cmd true

class foo (α : Type) :=
(bar : α)
(prop : bar = bar)

def foo_to_foo (α : Type) [foo α] : foo α :=
{ .. (infer_instance : foo α) }

instance nat.foo : foo ℕ :=
{ bar := 0,
  prop := rfl }

def typealias := ℕ

instance baz : foo typealias := nat.foo
instance baz' : foo typealias := foo_to_foo typealias

local attribute [irreducible] typealias

example : @foo.bar _ baz = @foo.bar _ baz' := rfl
example : @foo.prop _ baz = @foo.prop _ baz' := rfl

Kenny Lau (Nov 29 2020 at 14:41):

@Kevin Buzzard

Kevin Buzzard (Nov 29 2020 at 14:44):

Nice!

Kenny Lau (Nov 29 2020 at 20:04):

who do we ping for this? @Kevin Buzzard

Kevin Buzzard (Nov 29 2020 at 21:51):

Maybe it's just worth restating what's going on: over the weekend we minimised (in the sense of removing mathlib imports) the issue discovered at the top of this thread. The last line of the code above is a proof that two proofs of a proposition are equal, but rfl fails. If Lean didn't think that it was two proofs of the same proposition, then the term @foo.prop _ baz = @foo.prop _ baz' itself wouldn't typecheck. The term does typecheck, but the proof fails anyway. The example can be proved with they_are_equal, or with the tactic.add_decl trick above.

Floris van Doorn (Nov 29 2020 at 23:08):

they_are_equal is in the library under the name docs#proof_irrel.

Floris van Doorn (Nov 29 2020 at 23:08):

Oh, Bhavik already mentioned that.

Kevin Buzzard (Nov 29 2020 at 23:39):

Oh! I hadn't appreciated that this was what he was saying!

Eric Wieser (Nov 29 2020 at 23:44):

Now that we have the reproducer, presumably we can attempt to change the line of C++ code linked up-thread and see if it fixes it

Last updated: Dec 20 2023 at 11:08 UTC