# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: (commutative)-semirng

#### Damiano Testa (Dec 13 2020 at 16:32):

Is there already a definition of a type with two operations, addition and multiplication, that is just like a `semiring`

, except that it does not need to have a unit for multiplication. I do not mind if multiplication is commutative, although it is in my intended application. I looked for `semirng`

(as well as `semring`

and `semrng`

), but did not find anything.

#### Damiano Testa (Dec 13 2020 at 16:41):

Nevermind, I think that `add_comm_monoid`

is what I want.

#### Adam Topaz (Dec 13 2020 at 16:41):

This doesn't have a multipication

#### Damiano Testa (Dec 13 2020 at 16:42):

Ah, so I am misunderstanding this definition:

```
/-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
@[protect_proj, ancestor add_monoid add_comm_semigroup]
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
attribute [to_additive] comm_monoid
```

I thought that the `add_monoid`

and `add_comm_semigroup`

implied different operations. Is this not the case?

#### Damiano Testa (Dec 13 2020 at 16:43):

(The doc_string seems contradicting what I think)

#### Damiano Testa (Dec 13 2020 at 16:45):

So, I guess that I would like two `add_comm`

structures, one of which is a monoid, and a distributive law.

#### Adam Topaz (Dec 13 2020 at 16:45):

the `to_additive`

thing is a metaprogramming trick that takes something like the class `comm_monoid`

and automatically makes `add_comm_monoid`

.

#### Adam Topaz (Dec 13 2020 at 16:45):

But a priori there is no relationship between `comm_monoid`

and `add_comm_monoid`

.

#### Damiano Testa (Dec 13 2020 at 16:46):

ah, so I could build one like what i want by piling up two `add`

structures and if I *do not* put the `to_additive`

they would be a `+`

and a `*`

?

#### Adam Topaz (Dec 13 2020 at 16:46):

E.g. look at the source for src#comm_monoid

#### Adam Topaz (Dec 13 2020 at 16:47):

I think what you want is a class that extends `add_comm_monoid`

and the (nonexistent, as far as I know) `semigroup_with_zero`

and the class that ensures distributivity of `+`

and `*`

that I can't remember the name of right now...

#### Damiano Testa (Dec 13 2020 at 16:48):

`distrib`

should be the distributive property:

```
/-- A typeclass stating that multiplication is left and right distributive
over addition. -/
@[protect_proj, ancestor has_mul has_add]
class distrib (R : Type*) extends has_mul R, has_add R :=
(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))
```

#### Damiano Testa (Dec 13 2020 at 16:50):

I am happy to assume comm_semigroup_with_zero, but I *really* do not have a unit for multiplication: I want to put this structure on `finset`

s.

#### Adam Topaz (Dec 13 2020 at 16:50):

Oh, BTW my explanation of `to_additive`

is probably not 100% correct. It looks like `add_comm_monoid`

is actually declared explicitly with a `to_additive`

declaration right after to connect it to `comm_monoid`

. I guess `to_additive`

makes some of the API for you.

#### Adam Topaz (Dec 13 2020 at 16:50):

semigroups don't have units IIRC

#### Damiano Testa (Dec 13 2020 at 16:51):

Ok, thanks for the correction: I know so little of this, at the moment, that I had filed it in my head as "there is a system to keep track of whether you call it `+`

or `*`

"!

#### Reid Barton (Dec 13 2020 at 16:51):

That's not `to_additive`

, that's this `add_`

stuff

#### Reid Barton (Dec 13 2020 at 16:52):

The classes with `add_`

in their name are built on top of `+`

, the ones without are built on `*`

#### Damiano Testa (Dec 13 2020 at 16:52):

ok, so by default, an operation is `*`

, unless is it declared with a `add_`

and then it is a `+`

, right?

#### Adam Topaz (Dec 13 2020 at 16:53):

I think `to_additive`

takes lemmas of the form `mul_foo`

and automatically makes lemmas of the form `add_foo`

, if I understand what Reid is saying here...

#### Damiano Testa (Dec 13 2020 at 16:53):

I was typing my comment, while you were explaining yours, thanks!)

#### Reid Barton (Dec 13 2020 at 16:53):

right, `to_additive`

is some automation which means we don't have to duplicate everything between the additive and multiplicative versions by hand

#### Adam Topaz (Dec 13 2020 at 16:54):

so you have to tell lean that it should generate the `add_foo`

lemmas for `add_comm_monoid`

using the `mul_foo`

lemmas for `comm_monoid`

, and that's the `to_additive`

declaration that we noticed above.

#### Reid Barton (Dec 13 2020 at 16:54):

So, I think you want to extend `add_comm_group`

, `semigroup`

and `distrib`

... that will imply `0 * x = x * 0 = 0`

already, right?

#### Reid Barton (Dec 13 2020 at 16:55):

I guess you can also add `monoid_with_zero`

just in case

#### Adam Topaz (Dec 13 2020 at 16:55):

Yes. but he doesn't have negation and that's not true for additive monoids

#### Reid Barton (Dec 13 2020 at 16:55):

oh I missed "semi"

#### Damiano Testa (Dec 13 2020 at 16:55):

Yes, negation I also want to avoid.

#### Reid Barton (Dec 13 2020 at 16:55):

oh then there might not be any combination which does exactly what you want

#### Reid Barton (Dec 13 2020 at 16:56):

You can't actually use `monoid_with_zero`

because it implies `monoid`

#### Adam Topaz (Dec 13 2020 at 16:56):

Yeah, this is why I was suggesting the `semigroup_with_zero`

class :rofl:

#### Reid Barton (Dec 13 2020 at 16:56):

`semigroup`

is such a hard name for category theorists :head_bandage:

#### Damiano Testa (Dec 13 2020 at 16:57):

well, if it is only the `with_zero`

part that is missing, I can add the two axioms `zero_mul`

and `mul_zero`

, right?

#### Reid Barton (Dec 13 2020 at 16:57):

#### Reid Barton (Dec 13 2020 at 16:58):

What goofy names... `mul_zero_class`

and `distrib`

#### Damiano Testa (Dec 13 2020 at 16:58):

so, `extends add_comm_monoid, semigroup, distrib, mul_zero_class`

?

#### Damiano Testa (Dec 13 2020 at 16:58):

I will try it and see if I can pull it off!

#### Damiano Testa (Dec 13 2020 at 17:03):

Just to avoid being stuck for silly reasons: proving the `instance`

should simply be a matter of following my nose, right?

```
import algebra.algebra.basic
set_option old_structure_cmd true
variables {α : Type*}
class semirng (α : Type*) extends add_comm_monoid α, semigroup α, distrib α, mul_zero_class α
instance : semirng (finset α) :=
```

#### Kevin Buzzard (Dec 13 2020 at 17:05):

If all the other structures are on `finset`

then it might be a matter of `by apply_instance`

. If it isn't then you can make the other structures first. But this might be one of those places where some people don't want those instances, so maybe it should be a `def`

instead.

#### Adam Topaz (Dec 13 2020 at 17:05):

I assume this is the semiring structure given by the lattice structure?

#### Damiano Testa (Dec 13 2020 at 17:05):

Yes, union=+ and intersection=*.

#### Adam Topaz (Dec 13 2020 at 17:06):

Umm... addition is symmetric difference no?

#### Damiano Testa (Dec 13 2020 at 17:06):

Ah, I had union in mind...

#### Damiano Testa (Dec 13 2020 at 17:06):

It is not the boolean-ish algebra that I want

#### Kevin Buzzard (Dec 13 2020 at 17:07):

If there are two natural choices for addition then probably you don't want anything to be an instance, because then everyone who wants the other one is stuck with it

#### Adam Topaz (Dec 13 2020 at 17:07):

This is essentially a direct sum of $\mathbf{Z}/2$ indexed by the type

#### Adam Topaz (Dec 13 2020 at 17:07):

where you identify a finite set with its indicator function.

#### Damiano Testa (Dec 13 2020 at 17:08):

In what I want, once an element is in, it will never go out

#### Damiano Testa (Dec 13 2020 at 17:08):

(with addition, you can remove it with intersections, of course)

#### Adam Topaz (Dec 13 2020 at 17:08):

Is that distributive?

#### Damiano Testa (Dec 13 2020 at 17:09):

I thought that it was distributive "both ways"

#### Adam Topaz (Dec 13 2020 at 17:09):

Yeah you're probably right

#### Reid Barton (Dec 13 2020 at 17:09):

This already basically exists as `distrib_lattice`

#### Damiano Testa (Dec 13 2020 at 17:09):

it is according to wikipedia:

https://en.wikipedia.org/wiki/Algebra_of_sets

#### Damiano Testa (Dec 13 2020 at 17:10):

Ah, I will look at distributive lattice then!

#### Damiano Testa (Dec 13 2020 at 17:10):

(the name sounds good)

#### Adam Topaz (Dec 13 2020 at 17:11):

Yeah it's clearly distribute. But I agree with what Kevin said above, because as far as I know the "standard" way to define a (semi)ring structure from a boolean algebra is by letting addition be the symmetric difference.

#### Damiano Testa (Dec 13 2020 at 17:13):

Ok, it is simply that for doing "induction", unions is what I need, rather than symmetric differences

#### Damiano Testa (Dec 13 2020 at 17:13):

I will not make an instance, and I will check out `distrib_lattice`

#### Kevin Buzzard (Dec 13 2020 at 17:18):

@Damiano Testa $\cup$ and $\cap$ are "builtin" notation for mathematicians when using sets, but lattice theory is a generalisation of this stuff and the notation used is these square $\sqcup$ and $\sqcap$ stuff. It is actually a **pain** that set theory in Lean sticks to this set union and intersection notation. When ideals were defined and given a lattice structure, the lattice notation was used, and initially I was shocked that I was supposed to write $I\leq J$ instead of $I\subseteq J$, but now actually I see the benefits of this: we are using lots of different notations for lattice notation in various situations when we're dealing with lattices which we don't perceive as lattices, e.g. the subgroup generated by $H$ and $K$ is just $H\sqcup K$ in Lean. Sticking to lattice notation everywhere is a good convention, I think.

#### Damiano Testa (Dec 13 2020 at 17:19):

Good, I will follow the convention! How do I type the square union and intersection?

#### Damiano Testa (Dec 13 2020 at 17:19):

(hovering in VSCode answers my question \lub)

#### Damiano Testa (Dec 13 2020 at 17:21):

~~So, I should define inclusion of sets, rather than union. Have I understood correctly?~~ I am slightly confused.

#### Adam Topaz (Dec 13 2020 at 17:24):

I agree with what Kevin said about the union intersection notation, but just one small comment. I would argue that addition being defined as symmetric difference is the only reasonable choice. For example if you work in a finite type, then the structure you get is a ring if you use symmetric difference, but not if you use union.

#### Damiano Testa (Dec 13 2020 at 17:27):

I thought that this would have worked, but Lean does not want me to use neither ⊔ nor ∪. I suspect that you already told me what I should do, but I did not understand it...

```
import algebra.algebra.basic
def finset_lattice (X : Type*) : distrib_lattice (finset X) :=
begin
refine ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, _, _⟩,
use (λ a b, a ⊔ b), -- failed to instantiate goal with fun (a : 4._.40) (b : 4._.41), ((frozen_name has_sup.sup) a b)
end
```

#### Mario Carneiro (Dec 13 2020 at 17:27):

ooh, what a fun error message

#### Damiano Testa (Dec 13 2020 at 17:28):

Adam Topaz said:

I agree with what Kevin said about the union intersection notation, but just one small comment. I would argue that addition being defined as symmetric difference is the only reasonable choice. For example if you work in a finite type, then the structure you get is a ring if you use symmetric difference, but not if you use union.

Ok, I will use this "simple-minded union" structure sparingly!

#### Adam Topaz (Dec 13 2020 at 17:31):

Don't we have this? docs#finset.distrib_lattice

#### Mario Carneiro (Dec 13 2020 at 17:31):

note the `decidable_eq`

requirement

#### Damiano Testa (Dec 13 2020 at 17:32):

Thanks! I opened the classical locale and now Lean is having more `fun`

: thanks!

#### Damiano Testa (Dec 13 2020 at 17:33):

Adam Topaz said:

Don't we have this? docs#finset.distrib_lattice

I will try to do it by hand first, and then compare with what is already in mathlib, just to get some practice. Thanks for the pointer, though!

#### Adam Topaz (Dec 13 2020 at 17:47):

My only issue with lattice notation is that $\sqcup$ is disjoint union in my mind. But I got used to $\oplus$

#### Damiano Testa (Dec 13 2020 at 18:47):

Is it possible to see the name of each field that I am trying to prove? For instance, the first one asks to produce something with type `finset X \to finset X \to finset X`

. I "guessed" that it was the union. Others later on are similarly ambiguous. Is there a way to know what name each property has?

#### Damiano Testa (Dec 13 2020 at 18:47):

(instead of type-checking myself and second guessing what I see that I will need to prove later on!)

#### Sebastien Gouezel (Dec 13 2020 at 18:49):

If you type `{! }`

where you are supposed to construct a structure, a little light bulb will show on. If you click on the light bulb and select `generate a skeleton for the structure under construction`

, it will give you the name of the different fields.

#### Damiano Testa (Dec 13 2020 at 18:52):

Wow: this is great!!! Thank you @Sebastien Gouezel !

#### Mario Carneiro (Dec 13 2020 at 18:58):

Actually you can just use `_`

#### Damiano Testa (Dec 13 2020 at 19:04):

I had never thought of clickling the yellow light-bulbs

:light_bulb:

#### Damiano Testa (Dec 14 2020 at 08:13):

To get some practice, I thought that I would define a new structure `sus`

on subsets of a set, just like `topological_space`

, except that I drop the requirement of arbitrary unions and only allow finite unions. (The definition only involves pairwise unions, although, as a mathematician, I still feel a bit funny having to specify this! As a consequence, for those who, like me, think often about the empty set, this implies that I need to add the hypothesis that `∅`

is in my collection of sets, since I can no longer take the empty union.)

Thus, `sus`

with `+ = ∪`

and `* = ∩`

is a `comm_semiring`

, which is where I am headed. This `comm_semiring`

structure is also the structure that I want to put on "`finsets with univ`

".

I copied the beginning of the `topology/basic`

file and started changing as needed. When I got to

```
@[ext]
lemma topological_space_eq : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g
| ⟨a, _, _, _⟩ ⟨b, _, _, _⟩ rfl := rfl
```

I got completely stuck. I can understand the statement: if two instances of topological space on the same type have the same open sets, then they agree. However, the proof in indecipherable to me. Can anyone give me some guidance or even simply a proof? Below is the code that I have so far. Feel free to give more advice!

```
import order.filter.ultrafilter
import order.filter.partial
open set filter classical
open_locale classical filter
/-- A `sus` on `α`. -/
@[protect_proj] structure sus (α : Type*) :=
(is_su : set α → Prop)
(is_su_univ : is_su univ)
(is_su_empty : is_su ∅)
(is_su_inter : ∀s t, is_su s → is_su t → is_su (s ∩ t))
(is_su_union : ∀s t, is_su s → is_su t → is_su (s ∪ t))
attribute [class] sus --I do not know what this does, but it was there
/-- A constructor for `sus` using complements of the given `sus` structure. -/
-- this definition is not relevant to what I care about: I simply say that if I have a ```sus```, then the collection of complements also forms a ```sus```
def sus.comp {α : Type*} (f : sus α) : sus α :=
{ is_su := λ X, f.is_su Xᶜ,
is_su_univ := by simp [sus.is_su_empty],
is_su_empty := by simp [sus.is_su_univ],
is_su_inter := λ s t hs ht, by { rw compl_inter, exact sus.is_su_union f sᶜ tᶜ hs ht },
is_su_union := λ s t hs ht, by { rw compl_union, exact sus.is_su_inter f sᶜ tᶜ hs ht },
}
section sus
variables {α : Type*} {β : Type*} {ι : Sort*} {a : α} {s s₁ s₂ : set α} {p p₁ p₂ : α → Prop}
@[ext]
lemma sus_eq : ∀ {f g : sus α}, f.is_su = g.is_su → f = g :=
-- this was the proof for topological spaces
-- | ⟨a, _, _, _, _⟩ ⟨b, _, _, _, _⟩ rfl := rfl
begin
sorry
end
```

#### Alex J. Best (Dec 14 2020 at 08:22):

```
@[ext]
lemma sus_eq : ∀ {f g : sus α}, f.is_su = g.is_su → f = g :=
-- this was the proof for topological spaces
-- | ⟨a, _, _, _, _⟩ ⟨b, _, _, _, _⟩ rfl := rfl
begin
rintro ⟨f_is_su, f_is_su_univ, f_is_su_empty, f_is_su_inter, f_is_su_union⟩ ⟨g_is_su,
g_is_su_univ,
g_is_su_empty,
g_is_su_inter,
g_is_su_union⟩ ⟨⟩,refl,
end
```

#### Alex J. Best (Dec 14 2020 at 08:22):

The first part was generated by `rintros?`

#### Damiano Testa (Dec 14 2020 at 08:23):

Thanks! I will try it!

#### Damiano Testa (Dec 14 2020 at 08:25):

I am not sure if this makes it clearer or opaquer, but also what is below works.

```
@[ext]
lemma sus_eq : ∀ {f g : sus α}, f.is_su = g.is_su → f = g :=
begin
rintro ⟨_⟩ ⟨_⟩ ⟨⟩,
refl,
end
```

#### Alex J. Best (Dec 14 2020 at 08:28):

If you do

```
@[protect_proj, ext] structure sus (α : Type*) :=
```

lean will generate a lemma `sus.ext`

and `sus.ext_iff`

for you

#### Kevin Buzzard (Dec 14 2020 at 08:30):

To prove two instances of a structure are equal, do cases on them. Look at how I prove the ext lemma for complex numbers in the complex number game. The equation compiler proof is just doing cases.

#### Damiano Testa (Dec 14 2020 at 08:33):

Thank you both!

Indeed, with

`@[protect_proj, ext] structure sus (α : Type*) :=`

the proof is simply `sus.ext`

.

Otherwise, `cases`

all the way reduces the proof to `refl`

:

```
@[ext]
lemma sus_eq : ∀ {f g : sus α}, f.is_su = g.is_su → f = g :=
begin
intros f g h,
cases f,
cases g,
cases h,
refl,
end
```

#### Damiano Testa (Dec 14 2020 at 08:34):

Kevin Buzzard said:

To prove two instances of a structure are equal, do cases on them. Look at how I prove the ext lemma for complex numbers in the complex number game. The equation compiler proof is just doing cases.

What does "equation compiler" mean? Is it what you see when you use `show_term`

?

#### Alex J. Best (Dec 14 2020 at 08:40):

The equation compiler proof is the first one you mentioned:

```
@[ext]
lemma topological_space_eq : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g
| ⟨a, _, _, _⟩ ⟨b, _, _, _⟩ rfl := rfl
```

#### Damiano Testa (Dec 14 2020 at 08:48):

Ah, thanks! I am also seeing through this proof more. However, now I do not understand why is what is below not a proof?

```
@[ext]
lemma sus_eq : ∀ {f g : sus α}, f.is_su = g.is_su → f = g :=
| ⟨_, _, _, _, _⟩ ⟨_, _, _, _, _⟩ ⟨⟩ := rfl -- invalid expression\\ command expected
```

While this one is?

```
@[ext]
lemma sus_eq : ∀ {f g : sus α}, f.is_su = g.is_su → f = g :=
begin
rintros ⟨_⟩ ⟨_⟩ ⟨⟩,
refl,
end
```

#### Mario Carneiro (Dec 14 2020 at 08:52):

you probably need `rfl`

instead of `⟨⟩`

in the first version

#### Mario Carneiro (Dec 14 2020 at 08:54):

you can also use `⟨_⟩`

#### Mario Carneiro (Dec 14 2020 at 08:54):

because the constructor of `eq`

is `eq.refl`

which has one explicit argument

#### Mario Carneiro (Dec 14 2020 at 08:55):

`rintro`

doesn't really care if you don't give it enough arguments:

```
@[ext]
lemma sus_eq : ∀ {f g : sus α}, f.is_su = g.is_su → f = g :=
by rintro ⟨⟩ ⟨⟩ ⟨⟩; refl
```

#### Damiano Testa (Dec 14 2020 at 09:00):

I tried with

```
@[ext]
lemma sus_eq : ∀ {f g : sus α}, f.is_su = g.is_su → f = g :=
| ⟨_, _, _, _, _⟩ ⟨_, _, _, _, _⟩ rfl := rfl -- invalid expression \\ command expected
```

and it does not work. In any case, I have enough proofs of a completely trivial result that the computer can even figure out on its own! I was just curious about the proof style with `|`

that I had never seen before, hence my curiousity!

#### Mario Carneiro (Dec 14 2020 at 09:02):

The following compiles for me with no errors:

```
import order.filter.ultrafilter
import order.filter.partial
open set filter classical
open_locale classical filter
/-- A `sus` on `α`. -/
@[protect_proj] structure sus (α : Type*) :=
(is_su : set α → Prop)
(is_su_univ : is_su univ)
(is_su_empty : is_su ∅)
(is_su_inter : ∀s t, is_su s → is_su t → is_su (s ∩ t))
(is_su_union : ∀s t, is_su s → is_su t → is_su (s ∪ t))
attribute [class] sus --I do not know what this does, but it was there
/-- A constructor for `sus` using complements of the given `sus` structure. -/
-- this definition is not relevant to what I care about: I simply say that if I have a ```sus```, then the collection of complements also forms a ```sus```
def sus.comp {α : Type*} (f : sus α) : sus α :=
{ is_su := λ X, f.is_su Xᶜ,
is_su_univ := by simp [sus.is_su_empty],
is_su_empty := by simp [sus.is_su_univ],
is_su_inter := λ s t hs ht, by { rw compl_inter, exact sus.is_su_union f sᶜ tᶜ hs ht },
is_su_union := λ s t hs ht, by { rw compl_union, exact sus.is_su_inter f sᶜ tᶜ hs ht },
}
section sus
variables {α : Type*} {β : Type*} {ι : Sort*} {a : α} {s s₁ s₂ : set α} {p p₁ p₂ : α → Prop}
@[ext]
lemma sus_eq : ∀ {f g : sus α}, f.is_su = g.is_su → f = g
| ⟨a, _, _, _, _⟩ ⟨b, _, _, _, _⟩ rfl := rfl
```

#### Mario Carneiro (Dec 14 2020 at 09:02):

Oh, you still have the `:=`

on the first line

#### Mario Carneiro (Dec 14 2020 at 09:03):

when you use an equation compiler proof you have to take that off

#### Damiano Testa (Dec 14 2020 at 09:03):

Ah, I was puzzled by the fact that yours compiled, while mine did not. I had taken no notice of the `:=`

#### Damiano Testa (Dec 14 2020 at 09:04):

so then, why the `a`

and `b`

?

#### Mario Carneiro (Dec 14 2020 at 09:04):

it makes the intermediate state display a little nicer

#### Damiano Testa (Dec 14 2020 at 09:05):

I see

#### Mario Carneiro (Dec 14 2020 at 09:05):

it's totally optional here

#### Damiano Testa (Dec 14 2020 at 09:07):

Ok, I am understanding this proof a little better now. At first, it looked like non-sense, now it suggests that the statement is entirely trivial!

#### Damiano Testa (Dec 14 2020 at 09:38):

Kevin Buzzard said:

To prove two instances of a structure are equal, do cases on them. Look at how I prove the ext lemma for complex numbers in the complex number game. The equation compiler proof is just doing cases.

I am doing the Complex Numbers Game. If you are interested, I found a couple of typos in `Level_00_basic.lean`

.

#### Kevin Buzzard (Dec 14 2020 at 09:43):

Open an issue on github and I'll deal with it one day.

Last updated: May 17 2021 at 16:26 UTC