Instance diamond in DecidableEq Fin

Stream: mathlib4

[Eric Wieser]

@Joseph Myers' #29418 led me to discover this diamond:

example : Fin.instLinearOrder.toDecidableEq = instDecidableEqFin n := rfl -- fails

set_option smartUnfolding false in
example : Fin.instLinearOrder.toDecidableEq = instDecidableEqFin n := rfl -- works

I guess we decided "this will obviously be defeq to the instance in core" without actually reusing the core instance, but then the meaning of "defeq" changed

[Aaron Liu]

interesting

[Aaron Liu]

I guess it's time to pull out

import Mahtlib

/-- Replace decidable equality in a `LinearOrder` instance with a propositionally (but possibly not
definitionally) equal one. -/
abbrev LinearOrder.replaceDecEq {α : Type*} [decEq : DecidableEq α]
    (l : LinearOrder α) : LinearOrder α where
  __ := l
  toDecidableEq := decEq
  compare_eq_compareOfLessAndEq :=
    Subsingleton.elim l.toDecidableEq decEq ▸ l.compare_eq_compareOfLessAndEq

and friends

[Eric Wieser]

I think really docs#LinearOrder.lift and family are to blame

[Aaron Liu]

Do you think we should have versions which don't synthesize the decidability fields?

[Kevin Buzzard]

Can someone remind me why we have all this constructivist nonsense in docs#LinearOrder ? My instinct with these things is that the moment they start causing trouble, rip them out, but presumably there's a good reason that they're there in the first place?

[Kevin Buzzard]

Perhaps related (but perhaps not): it seems that core is adding predicates to LE to get things like partial orders (sorry for no link, on mobile, but I thought I saw a recent core PR). Should we switch to this model? (edit: it was lean4#9908 which was going on about IsPartialOrder, IsLinearOrder etc)

[Eric Wieser]

Aaron Liu said:

Do you think we should have versions which don't synthesize the decidability fields?

Yes, I've started writing these in #29436

[Eric Wieser]

Kevin Buzzard said:

My instinct with these things is that the moment they start causing trouble, rip them out

In this case the problem is mostly docs#LinearOrder.lift, which completely ignores the pattern set by docs#Function.Injective.ring etc

[Kevin Buzzard]

Aah OK, let's see if this solves it.

[Eric Wieser]

It definitely solves it, you can't construct diamonds if you don't construct any data in the first place!

[Eric Wieser]

One thing that #29436 raises is what to do about this and similar theorems):

 lemma Function.Injective.isOrderedMonoid [IsOrderedMonoid α]
-    [One β] [Mul β] [Pow β ℕ]
+    [CommMonoid β] [PartialOrder β]
     (f : β → α)
-    (hf : Function.Injective f) (one : f 1 = 1) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
+    (le : ∀ {x y}, f x ≤ f y ↔ x ≤ y)
     (mul : ∀ x y, f (x * y) = f x * f y) :
-    let _ : CommMonoid β := hf.commMonoid f one mul npow
-    let _ : PartialOrder β := PartialOrder.lift f hf
     IsOrderedMonoid β :=

after changing the arguments, the name no longer makes any sense!