neg diamond

Stream: general

[Yaël Dillies]

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]

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

[Eric Rodriguez]

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]

Ah yes, probably!

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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]

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]

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

[Eric Wieser]

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]

Yeah, probably

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Ruben Van de Velde]

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