Asserting that X is-a Y: "instance : Y X where …"?

Stream: new members

[Isak Colboubrani]

1. The following asserts that Int (ℤ, +) forms an AdditiveGroup. Is there a more succinct way to phrase it?

instance : AdditiveGroup Int where
  add := Int.add
  add_assoc := Int.add_assoc
  zero := Int.zero
  zero_add := Int.zero_add
  add_zero := Int.add_zero
  neg := Int.neg
  add_left_neg := Int.add_left_neg
  add_right_neg := Int.add_right_neg

2. I'm trying to assert that Int forms an Ring, but I'm struggling with the last two fields. What am I missing?

class Ring (R : Type) extends AdditiveCommutativeGroup R, Monoid R where
  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
instance : Ring Int where
  add := Int.add
  add_assoc := Int.add_assoc
  zero := 0
  zero_add := Int.zero_add
  add_zero := Int.add_zero
  neg := Int.neg
  add_left_neg := Int.add_left_neg
  add_right_neg := Int.add_right_neg
  add_comm := Int.add_comm
  mul := Int.mul
  mul_assoc := Int.mul_assoc
  one := 1
  one_mul := Int.one_mul
  mul_one := Int.mul_one
  left_distrib := ???
  right_distrib := ???

3. Is instance : Y X where … the idiomatic way to assert/demonstrate that X fulfils the interface of Y (X is-a Y)? Could it alternatively be stated as an example?

[Eric Wieser]

2. The ???s are docs#Int.mul_add etc

[Eric Wieser]

3. instance : Y X means that this construction is the canonical way that X is a Y.

[Eric Wieser]

1. Strictly this asserts "there is an additive group structure on ℤ, and if you look at how I build it you can see I use Int.add"; you didn't at any point write a statement that said the group operator was Int.add.

[Kevin Buzzard]

Eric is just pointing out that phrases such as "the integers are a ring", whilst commonly used in mathematics and which sound like true/false statements, are in fact missing information; in lean you have to say "this choice of addition and multiplication make the integers into a ring" (and in lean you also have to say which choice of negation, 0 and 1 you use, although a posteriori they are unique)

[Eric Wieser]

Arguably the missing information is present if you say "$(ℤ, 0, 1, -, +, \times)$ is a ring", which is effectively what Isak did above. What I was trying to convey is that while this language is precise, it is not the phrasing that mathlib uses; we say "$ℤ$ has a ring structure, I'm going to define it in terms of $(0, 1, -, +, \times)$".

[Damiano Testa]

In this specific case, you could introduce instances for each one of the data fields, since they are typeclasses in their own right.

[Isak Colboubrani]

Thanks!

Ah, I had searched for Int.mul_add and Int.add_mul in Lean core and Mathlib, but it had not occurred to me that they could live in the standard library std4 (Std.Data.Int.Init.Lemmas).

Do I understand it correctly that …


instance : Ring Int where
  add := Int.add
  add_assoc := Int.add_assoc
  zero := 0
  …

… is a one-time setup that tells Lean that the given construction is the canonical way that Int is a Ring.

And once that setup is done I can simply do …

instance : Ring Int := by infer_instance

… in the rest of my code to assert that Int is a Ring (given the canonical construction)?

Would it possible to express the same thing in an example instead like …

example … <int-is-a-ring> … := by infer_instance

… ?

[Yaël Dillies]

Isak Colboubrani said:

Ah, I had searched for Int.mul_add and Int.add_mul in Lean core and Mathlib, but it had not occurred to me that they could live in the standard library std4 (Std.Data.Int.Init.Lemmas).

Do you mean you searched by hand? :fear: You should use the docs.

[Isak Colboubrani]

@Yaël Dillies Search as in git grep mul_add! :sweat_smile: