## 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 (+). -/


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
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 finsets.

#### 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: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):

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):

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

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