extending `RCLike` and `LinearOrder`

Stream: mathlib4

[Tomas Skrivan]

I have a class

import Mathlib.Analysis.RCLike.Basic

class RealScalar (R : Type*) extends RCLike R, LinearOrder R where
  is_real : RCLike.I = 0

  exp : R → R
  sin : R → R
  -- ...

which on v4.19.0-rc2 breaks with

field 'toPartialOrder' from 'RCLike' has a name conflict with parent projection for 'PartialOrder'

The 'toParent : P' syntax can be used to adjust the name for the parent projection

What is going on? How do I fix this?

Following the suggestion

class RealScalar (R :(Type _)) extends Scalar R R, toOrder : LinearOrder R where

does not work.

[Aaron Liu]

Why are you extending RCLike and LinearOrder?

[Tomas Skrivan]

I want to work with real numbers without actually working with real numbers and making my code noncomputable everywhere. I write most of my code parameterized over this calss and only at the and provide an inconsistent instance of this class for Float to execute the code.

[Aaron Liu]

I think SciLean had a solution for this that didn't involve extending RCLike and LinearOrder.

[Aaron Liu]

I don't know how it works though, you'll have to see for yourself.

[Tomas Skrivan]

This is in SciLean :)

[Tomas Skrivan]

https://github.com/lecopivo/SciLean/blob/53f112d9c99068a8231454c078525facd4ca2404/SciLean/Analysis/Scalar/Basic.lean#L109

[Aaron Liu]

oh, well... hmm...

[Aaron Liu]

What if you extend docs#ConditionallyCompleteLinearOrderedField and add an instance of RCLike

[Kevin Buzzard]

The job of RCLike is to axiomatise "the reals or complexes". If you want to axiomatise the reals then we have just the class for you in mathlib: docs#ConditionallyCompleteLinearOrderedField .

[Tomas Skrivan]

My current hierarchy is actually

-- `K` models complex numbers over `R` which should model reals
class Scalar (R : outParam Type*) (K : Type*) extends RCLike K where

-- `R` models reals
class RealScalar (R : Type*) extends Scalar R R, LinearOder K where

I feel that to use ConditionallyCompleteLinearOrderedField I would have to do substantial refactoring. Which might be the right thing to do as I'm not completely satisfy with my current set up, but in a short term In not going to do that.

[Aaron Liu]

Well I managed to get a different error...

import Mathlib.Analysis.RCLike.Basic

class RealScalar (R : Type*) extends LinearOrder R, RCLike R where
  is_real : RCLike.I = (0 : R)

  exp : R → R
  sin : R → R
  -- ...

[Tomas Skrivan]

Interesting, if you swap RCLike and LinearOrder it gives you very different error.

[Tomas Skrivan]

Anyway, simply doing

class RealScalar (R : Type*) extends Scalar R R where
  [order : LinearOrder R]

  is_real : ∀ x : R, im x = 0

instance {R : Type*} [RealScalar R] : LinearOrder R := RealScalar.order

seems to work for now.

[Kevin Buzzard]

Are you sure that this isn't just a "random" linear order on R rather than the one you want? (i.e. the one where x^2>=0)?

[Aaron Liu]

import Mathlib.Analysis.RCLike.Basic

-- shut up the error
set_option synthInstance.checkSynthOrder false in
class RealScalar (R : Type*) extends LinearOrder R, RCLike R where
  is_real : RCLike.I = (0 : R)

  exp : R → R
  sin : R → R
  -- ...


variable (R : Type*) [RealScalar R]

-- synthesis still seems to work fine
#synth RCLike R
#synth LinearOrder R

example :
    (inferInstanceAs (RCLike R)).toPartialOrder =
    (inferInstanceAs (LinearOrder R)).toPartialOrder :=
  -- no diamonds either
  rfl

[Tomas Skrivan]

Kevin Buzzard said:

Are you sure that this isn't just a "random" linear order on R rather than the one you want? (i.e. the one where x^2>=0)?

Ohh yes that is true, the class should contain some compatibility of those structures.

[Aaron Liu]

If you extend LinearOrder R, RCLike R and shut up the error, the toPartialOrder fields get merged, so the compatibility is free

[Kevin Buzzard]

The checkSynthOrder error is surprising (to me). Is it a regression?

[Kevin Buzzard]

In v4.18.0 you get an error on RCLike.I with the complaint that it can't synthesiz RCLike R and if you delete this field then you get the synthesization order error again.

[Eric Wieser]

-- no diamonds either

There is a diamond in the decidableEq instance, since this creates both decidableEq and toDecidableEq fields

[Aaron Liu]

We could rename the field in RCLike to also be called decidableEq

[Eric Wieser]

I'd argue vice versa is more consistent

[Aaron Liu]

Then we should have toDecidableEq, toDecidableLE, and toDecidableLT on LinearOrder?

[Matt Diamond]

The checkSynthOrder error is surprising (to me). Is it a regression?

@Kevin Buzzard I saw that error recently as well:

import Mathlib

variable {R S : Type} [CommGroup R] [Group S] (f : S ≃ R)

instance : CommGroup S := f.commGroup

it seemed like a straightforward application of docs#Equiv.commGroup so I figured I was making some dumb mistake

[Matt Diamond]

looks like there was a recent thread about this: #lean4 > projection instance binderinfo problem @ 💬

[Aaron Liu]

Matt Diamond said:

The checkSynthOrder error is surprising (to me). Is it a regression?

Kevin Buzzard I saw that error recently as well:

import Mathlib

variable {R S : Type} [CommGroup R] [Group S] (f : S ≃ R)

instance : CommGroup S := f.commGroup

it seemed like a straightforward application of docs#Equiv.commGroup so I figured I was making some dumb mistake

No in that one the error seems reasonable

[Aaron Liu]

Since Equiv isn't a typeclass

[Aaron Liu]

Typeclass search will not infer the Equiv, so you're asking it to do CommGroup ?R → CommGroup S, which does not solve for ?R

[Matt Diamond]

(deleted)

[Matt Diamond]

(deleted)

[Matt Diamond]

wait, but I'm not asking it to infer the Equiv, I'm providing it explicitly...

[Matt Diamond]

I don't get why that wouldn't work... it has all the information it needs

[Matt Diamond]

oh I think I get it... the arguments to a class instance must themselves be classes for typeclass inference to work (you can't just say "if this equiv exists...")

[Matt Diamond]

so I guess the point of Equiv.commGroup is for when you need a CommGroup instance in a specific proof, not as a general instance

[Eric Wieser]

Aaron Liu said:

Then we should have toDecidableEq, toDecidableLE, and toDecidableLT on LinearOrder?

I don't see it mentioned here; this is #23976