nontrivial LinearOrder.compare

Stream: mathlib4

[Johan Commelin]

LinearOrder has a field compare. How can I find instances of LinearOrder that do not use the default argument compareOfLessAndEq?

[Adam Topaz]

git grep compareOfLessAndEq?

[Adam Topaz]

using that it seems that there are no such instances?

[Adam Topaz]

That wouldn't account for instances defined using angle brackets, of course.

[Adam Topaz]

oh sorry, I misunderstood

[Adam Topaz]

compare doesn't have a default value?

[Adam Topaz]

no, it does as you said. I'm an idiot. sorry for the noise

[Adam Topaz]

I guess you could write a metaprogram that looks at all such instances, picks out the compare projection, looks at its value, and use something like docs#Lean.Expr.getUsedConstants to check whether it uses compareOfLessandEq.

[Johan Commelin]

Yes, probably, if only I knew how to actually do that :sad:

[Adam Topaz]

I'm hacking something together now

[Adam Topaz]

import Mathlib
import Lean

open Lean

#eval show MetaM Unit from do
  let cs := (← getEnv).constants
  for (n,c) in cs.toList do
    if let .app (.const `LinearOrder _) _ := c.type then
      let some val := c.value? | continue
      unless val.getUsedConstantsAsSet.contains `compareOfLessAndEq do
        IO.println n

[Adam Topaz]

just an initial approximation. I didn't debug or think too carefully about whether this actually does what you want.

[Adam Topaz]

The result is

instPNatLinearOrder
instENatLinearOrder
String.instLinearOrderString
Int.instLinearOrderInt
instPNatLinearOrder._cstage1
instLinearOrderChar
Prop.linearOrder
Nat.linearOrder._cstage1
Int.instLinearOrderInt._cstage1
Real.linearOrder
NONote.instLinearOrderNONote._cstage1
NatOrdinal.linearOrder
NONote.instLinearOrderNONote
instENatLinearOrder._cstage1
Bool.linearOrder
Nat.linearOrder

[Johan Commelin]

Merci!

[Adam Topaz]

Well, I don't think that's the right answer.

[Adam Topaz]

For example, I guess Bool.linearOrder shouldn't be in there.

[Adam Topaz]

Oh, no maybe it's ok, since the ord instance for bool is defined as docs#instOrdBool

[Johan Commelin]

But if I look up Nat.linearOrder, then I don't see a custom compare field.

[Adam Topaz]

right, that comes from docs#instOrdNat which does actually use that lemma, so the code above doesn't quite do what you want.

[Adam Topaz]

Probably just need to unfold a bit... how about this?

#eval show MetaM Unit from do
  let cs := (← getEnv).constants
  for (n,c) in cs.toList do
    if let .app (.const `LinearOrder [u]) α := c.type then
      let some val := c.value? | continue
      let ordInst : Expr := .app (.app (.const `LinearOrder.toOrd [u]) α) val
      let compare : Expr := .app (.app (.const `Ord.compare [u]) α) ordInst
      unless (← Meta.whnf compare).getUsedConstantsAsSet.contains `compareOfLessAndEq do
        IO.println n

[Johan Commelin]

That prints some things, but I still don't find any nontrivial compare field

[Adam Topaz]

look at the one for bool

[Adam Topaz]

it comes from docs#instOrdBool

[Adam Topaz]

compare is part of Ord.

[Adam Topaz]

it seems that docs#instPNatLinearOrder might be another one?

[Adam Topaz]

for some reason I can't seem to go to that definition, but #check instPNatLinearOrder throws no errors.

[Adam Topaz]

Oh, I think it's because this is derived from the following line: https://github.com/leanprover-community/mathlib4/blob/bbf2206016a67e7d54812dcf76f830c704df378c/Mathlib/Data/PNat/Basic.lean#L24