Foo extends BarCast

Stream: mathlib4

[Martin Dvořák]

I am confused by frequently reading class Foo extends BarCast in Mathlib.
For example, docs#DivisionRing extends docs#NNRatCast and docs#RatCast .
I find it weird that BarCast is part of the definition.
Why isn't it just an instance for given class?

[Yaël Dillies]

Why wouldn't it just extend it?

[Filippo A. E. Nuccio]

A nice explanation is in this chapter of the Lean Manual, for instance.

[Filippo A. E. Nuccio]

If you don't "extend", you need to define all the fields again from scratch (plus you loose some nice automatic instance creation, but even without this the extension mechanism is great).

[Filippo A. E. Nuccio]

Another advantage is that otherwise you need to call all these instances before being allowed to insert the one you're defining: see the examples:

import Mathlib

class foo (α : Type) extends CommRing α, CommGroup α :=
another_plus : α → α → α

example (α : Type) [foo α] (x y : α) : x + y = y + x := by
  exact AddCommMagma.add_comm x y

class bar (α : Type) [CommRing α] [Group α] :=
another_plus : α → α → α

example (α : Type) [CommRing α] [CommGroup α] [bar α] (x y : α) : x + y = y + x := by --cannot simply put [bar α]
   exact AddCommMagma.add_comm x y

[Filippo A. E. Nuccio]

Another advantage is that the extension mechanism helps in checking that fields with the same name are actually the same field: see the examples below

import Mathlib

class foo (α : Type) extends CommRing α, One α :=
another_plus : α → α → α

example (α : Type) [foo α] (x y : α) : x * 1 = x := by
  exact MulOneClass.mul_one x

class bar (α : Type) [CommRing α] [One α] :=
another_plus : α → α → α

example (α : Type) [CommRing α] [One α] [bar α] (x y : α) : x * 1 = x := by
    exact MulOneClass.mul_one x --gets an error, Lean is confused whether * is the CommRing one or the One one.

[Martin Dvořák]

I didn't mean Foo having an instance argument of type BarCast.
I meant Foo having an instance of type BarCast.
In the following example, imagine that the One instance does not exist yet...

import Mathlib

class foo (α : Type) extends CommRing α :=
another_plus : α → α → α

instance foo.toOne' (α : Type) [foo α] : One α := inferInstance

[Filippo A. E. Nuccio]

I am not sure to follow what you want to say. How would you suggest to define DivisionRing without extend?

[Martin Dvořák]

Yaël Dillies said:

Why wouldn't it just extend it?

It makes it harder to check that the formal definition corresponds to the informal definition.

[Martin Dvořák]

Filippo A. E. Nuccio said:

I am not sure to follow what you want to say. How would you suggest to define DivisionRing without extend?

Why doesn't Mathlib do something along these lines?

import Mathlib

class DivisionRing' (α : Type*) extends Ring α, DivInvMonoid α, Nontrivial α where
  protected mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
  protected inv_zero : (0 : α)⁻¹ = 0

instance DivisionRing'.hasNNRatCast (α : Type*) [DivisionRing' α] : NNRatCast α := sorry

instance DivisionRing'.hasRatCast (α : Type*) [DivisionRing' α] : RatCast α := sorry

[Yaël Dillies]

That's to allow NNRat.cast q = q definitionally when q : ℚ≥0

[Filippo A. E. Nuccio]

See the doc of docs#Field.

[Martin Dvořák]

What is the note [forgetful inheritance] please?

[Martin Dvořák]

Yaël Dillies said:

That's to allow NNRat.cast q = q definitionally when q : ℚ≥0

I still don't get it. Is it extends NNRatCast in order to prevent diamonds that would occur if the NNRatCast instance was synthesized instead of being a part of the definitions?

[Eric Wieser]

Just to be clear, there are three possibility here:

class DivisionRing extends RatCast where
  ...

class DivisionRing where
  ratCast : _
  ...

instance DivisionRing.toRatCast [DivisionRing K] : RatCast K where
  ratCast := DIvisionRing.ratCast

class DivisionRing where

instance DivisionRing.toRatCast [DivisionRing K] : RatCast K where
  ratCast q := q.num / q.den

I assume you understand why we prefer choice 1 to choice 2 (it's shorter and otherwise identical), and your question is really why choice 3 is bad?

[Martin Dvořák]

Please enlighten me why the 3rd option is bad.

[Daniel Weber]

Note that there's a default to ratCast, so if you create an instance of DivisionRing without changing ratCast it automatically uses q.num / q.den.
The benefit of using option 1 is that we can create the field instance of ℚ such that Rat.cast q = q holds definitionally, which doesn't work with docs#Rat.castRec, which is the default value of ratCast:

#guard_expr Rat.cast (1 / 2 : ℚ) =~ (1 / 2 : ℚ)

#guard_expr Rat.cast (K := ℚ) =~ id

/--
error: failed: Rat.castRec (1 / 2 : ℚ) =~ (1 / 2 : ℚ) is not true
-/
#guard_msgs in
#guard_expr Rat.castRec (1 / 2 : ℚ) =~ (1 / 2 : ℚ)

[Eric Wieser]

The reason we care about Rat.cast q = q being true by definition is that otherwise we end up with two different Algebra ℚ ℚ instances

[Eric Wieser]

(and similarly for Nat.cast and Int.cast)

[Violeta Hernández]

I mean, even on a basic level, def-eqs are really nice

[Violeta Hernández]

It's always satisfying to show some huge result by a single rfl

[Violeta Hernández]

This just extends that idea

[Yury G. Kudryashov]

BTW, why removing algebraMap from Algebra (and defining it in terms of smul) instead of adding all these *Cast fields is a bad idea?

[Yury G. Kudryashov]

I remember that there was a reason, but I keep forgetting it. It would be nice to add it to docs.

[Yury G. Kudryashov]

Let me write what I understand: we need nice Nat.cast defeq to avoid conflicting OfNat instances. What about the other *Casts?

[Martin Dvořák]

docs#Algebra

[Eric Wieser]

I think it's related to how we have a sub field in Ring vs deriving it from neg

[Yury G. Kudryashov]

Module docstring explains how to deal with existing instances, but doesn't explain what are the issues with different approaches.

[Yury G. Kudryashov]

Eric Wieser said:

I think it's related to how we have a sub field in Ring vs deriving it from neg

I assumed that we do it to avoid some diamonds, but I don't remember what diamonds appear if we use instance [Mul G] [Inv G] : Div G instead of the current approach. It's not Prod or Pi types. AFAIR, there was a type, where one can define Div or Sub, and under additional assumptions it becomes propeq to a * b⁻¹.

[Yury G. Kudryashov]

See !3#5303

[Yury G. Kudryashov]

@Anne Baanen Do we have an actual type, where DivInvMonoid allows us to avoid a diamond?

[Anne Baanen]

Yury G. Kudryashov said:

Anne Baanen Do we have an actual type, where DivInvMonoid allows us to avoid a diamond?

docs#FractionalIdeal has a division defined in general. But b⁻¹ (or 1/b) isn't an inverse unless some conditions hold (specifically docs#IsDedekindDomain), so we can't define a/b = a * b⁻¹.

[Yury G. Kudryashov]

Should this be in the docstring of DivInvMonoid?

[Eric Wieser]

Or maybe in the hierarchy design docstring

[Kim Morrison]

Violeta Hernández said:

It's always satisfying to show some huge result by a single rfl

This is actually a bit of a dangerous idea. :-) We should be thinking that it's even more satisfying to write a proof and know that even if someone changes an essential definition, our proof will survive unchanged (assuming they update the relevant API lemmas, and that's what we use).

"a single rfl" can hide arbitrary complexity: both what the lean kernel has to do to check the proof, and arbitrary hidden dependencies on minor implementation details.

[Violeta Hernández]

I guess I'm mostly thinking about stuff like toDual and ofDual. If anyone changes the defeqs for those, a lot of the library will just implode :stuck_out_tongue:

[Kim Morrison]

We've done some big defeq changes in the past. :-)

[Yury G. Kudryashov]

So, are there any reasons besides docs#Algebra to have *Cast fields other than Nat.cast?

[Yury G. Kudryashov]

@Anne Baanen @Eric Wieser :up: