Zulip Chat Archive

Stream: Is there code for X?

Topic: (commutative)-semirng


view this post on Zulip 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.

view this post on Zulip Damiano Testa (Dec 13 2020 at 16:41):

Nevermind, I think that add_comm_monoid is what I want.

view this post on Zulip Adam Topaz (Dec 13 2020 at 16:41):

This doesn't have a multipication

view this post on Zulip 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?

view this post on Zulip Damiano Testa (Dec 13 2020 at 16:43):

(The doc_string seems contradicting what I think)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Dec 13 2020 at 16:45):

But a priori there is no relationship between comm_monoid and add_comm_monoid.

view this post on Zulip 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 *?

view this post on Zulip Adam Topaz (Dec 13 2020 at 16:46):

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

view this post on Zulip 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...

view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Dec 13 2020 at 16:50):

semigroups don't have units IIRC

view this post on Zulip 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 *"!

view this post on Zulip Reid Barton (Dec 13 2020 at 16:51):

That's not to_additive, that's this add_ stuff

view this post on Zulip 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 *

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Damiano Testa (Dec 13 2020 at 16:53):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Dec 13 2020 at 16:55):

I guess you can also add monoid_with_zero just in case

view this post on Zulip Adam Topaz (Dec 13 2020 at 16:55):

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

view this post on Zulip Reid Barton (Dec 13 2020 at 16:55):

oh I missed "semi"

view this post on Zulip Damiano Testa (Dec 13 2020 at 16:55):

Yes, negation I also want to avoid.

view this post on Zulip Reid Barton (Dec 13 2020 at 16:55):

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

view this post on Zulip Reid Barton (Dec 13 2020 at 16:56):

You can't actually use monoid_with_zero because it implies monoid

view this post on Zulip Adam Topaz (Dec 13 2020 at 16:56):

Yeah, this is why I was suggesting the semigroup_with_zero class :rofl:

view this post on Zulip Reid Barton (Dec 13 2020 at 16:56):

semigroup is such a hard name for category theorists :head_bandage:

view this post on Zulip 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?

view this post on Zulip Reid Barton (Dec 13 2020 at 16:57):

oh docs#mul_zero_class

view this post on Zulip Reid Barton (Dec 13 2020 at 16:58):

What goofy names... mul_zero_class and distrib

view this post on Zulip Damiano Testa (Dec 13 2020 at 16:58):

so, extends add_comm_monoid, semigroup, distrib, mul_zero_class?

view this post on Zulip Damiano Testa (Dec 13 2020 at 16:58):

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

view this post on Zulip 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 α) :=

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Dec 13 2020 at 17:05):

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

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:05):

Yes, union=+ and intersection=*.

view this post on Zulip Adam Topaz (Dec 13 2020 at 17:06):

Umm... addition is symmetric difference no?

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:06):

Ah, I had union in mind...

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:06):

It is not the boolean-ish algebra that I want

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 13 2020 at 17:07):

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

view this post on Zulip Adam Topaz (Dec 13 2020 at 17:07):

where you identify a finite set with its indicator function.

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:08):

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

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:08):

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

view this post on Zulip Adam Topaz (Dec 13 2020 at 17:08):

Is that distributive?

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:09):

I thought that it was distributive "both ways"

view this post on Zulip Adam Topaz (Dec 13 2020 at 17:09):

Yeah you're probably right

view this post on Zulip Reid Barton (Dec 13 2020 at 17:09):

This already basically exists as distrib_lattice

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:09):

it is according to wikipedia:
https://en.wikipedia.org/wiki/Algebra_of_sets

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:10):

Ah, I will look at distributive lattice then!

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:10):

(the name sounds good)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:13):

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

view this post on Zulip 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 IJI\leq J instead of IJI\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 HH and KK is just HKH\sqcup K in Lean. Sticking to lattice notation everywhere is a good convention, I think.

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:19):

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

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:19):

(hovering in VSCode answers my question \lub)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 13 2020 at 17:27):

ooh, what a fun error message

view this post on Zulip 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!

view this post on Zulip Adam Topaz (Dec 13 2020 at 17:31):

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

view this post on Zulip Mario Carneiro (Dec 13 2020 at 17:31):

note the decidable_eq requirement

view this post on Zulip Damiano Testa (Dec 13 2020 at 17:32):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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!)

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Dec 13 2020 at 18:52):

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

view this post on Zulip Mario Carneiro (Dec 13 2020 at 18:58):

Actually you can just use _

view this post on Zulip Damiano Testa (Dec 13 2020 at 19:04):

I had never thought of clickling the yellow light-bulbs
:light_bulb:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Alex J. Best (Dec 14 2020 at 08:22):

The first part was generated by rintros?

view this post on Zulip Damiano Testa (Dec 14 2020 at 08:23):

Thanks! I will try it!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 14 2020 at 08:52):

you probably need rfl instead of ⟨⟩ in the first version

view this post on Zulip Mario Carneiro (Dec 14 2020 at 08:54):

you can also use ⟨_⟩

view this post on Zulip Mario Carneiro (Dec 14 2020 at 08:54):

because the constructor of eq is eq.refl which has one explicit argument

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 14 2020 at 09:02):

Oh, you still have the := on the first line

view this post on Zulip Mario Carneiro (Dec 14 2020 at 09:03):

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

view this post on Zulip 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 :=

view this post on Zulip Damiano Testa (Dec 14 2020 at 09:04):

so then, why the a and b?

view this post on Zulip Mario Carneiro (Dec 14 2020 at 09:04):

it makes the intermediate state display a little nicer

view this post on Zulip Damiano Testa (Dec 14 2020 at 09:05):

I see

view this post on Zulip Mario Carneiro (Dec 14 2020 at 09:05):

it's totally optional here

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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