Zulip Chat Archive

Stream: general

Topic: neg diamond


Yaël Dillies (Sep 09 2021 at 08:44):

I think I just encountered a diamond:
real.linear_ordered_field.to_linear_ordered_ring.to_ordered_ring.to_ordered_add_comm_group.to_add_comm_group.to_add_group.to_sub_neg_monoid.to_has_neg vs real.has_neg
I don't really know how to diagnose that further, but refl failed on abs a = abs a. I'm trying to write a MWE.

Eric Rodriguez (Sep 09 2021 at 08:51):

i think this may be related to leanprover-community/lean#609

Eric Rodriguez (Sep 09 2021 at 08:52):

lean just needs a release to catch up with this (would be nice if leanprover-community/lean#612 was in there too :])

Yaël Dillies (Sep 09 2021 at 08:53):

Ah yes, probably!

Yury G. Kudryashov (Sep 10 2021 at 00:16):

I don't understand why lean#609 is relevant here.

Yury G. Kudryashov (Sep 10 2021 at 00:17):

@Yaël Dillies Did you try convert or congr to see what instances are not defeq?

Yury G. Kudryashov (Sep 10 2021 at 00:18):

lean#609 makes it possible to have definitional equality between two different has_sup.sups (one from a linear_order, one from somewhere else).

Yaël Dillies (Sep 10 2021 at 07:56):

It's because I had two abs that weren't defeq, which is exactly what lean#609 is about. One of them was inferred from linear_ordered_ring ℤ, the other one (partly) from has_neg ℤ.

Eric Wieser (Sep 10 2021 at 08:15):

You should unfold abs once you hit that point, then apply congr (docs#abs)

Eric Wieser (Sep 10 2021 at 08:16):

Then you'll probably be told that the has_neg is irrelevant and it's the has_sup that is the problem

Yaël Dillies (Sep 10 2021 at 08:17):

Yeah, probably

Yury G. Kudryashov (Sep 11 2021 at 06:36):

Indeed, abs switched from max to has_sup some time ago. I missed this fact.

Yury G. Kudryashov (Sep 11 2021 at 06:37):

So, indeed this is a lattice diamond that we can solve once we have a Lean release with lean#609

Ruben Van de Velde (Sep 11 2021 at 06:43):

Quite recently: https://github.com/leanprover-community/mathlib/commit/74373b8132f58b7c9223e2e32d852629261c02dc


Last updated: Dec 20 2023 at 11:08 UTC