(commutative)-semirng

Stream: Is there code for X?

[Damiano Testa]

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]

Nevermind, I think that add_comm_monoid is what I want.

[Adam Topaz]

This doesn't have a multipication

[Damiano Testa]

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]

(The doc_string seems contradicting what I think)

[Damiano Testa]

So, I guess that I would like two add_comm structures, one of which is a monoid, and a distributive law.

[Adam Topaz]

the to_additive thing is a metaprogramming trick that takes something like the class comm_monoid and automatically makes add_comm_monoid.

[Adam Topaz]

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

[Damiano Testa]

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]

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

[Adam Topaz]

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]

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]

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]

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]

semigroups don't have units IIRC

[Damiano Testa]

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]

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

[Reid Barton]

The classes with add_ in their name are built on top of +, the ones without are built on *

[Damiano Testa]

ok, so by default, an operation is *, unless is it declared with a add_ and then it is a +, right?

[Adam Topaz]

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]

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

[Reid Barton]

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]

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]

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]

I guess you can also add monoid_with_zero just in case

[Adam Topaz]

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

[Reid Barton]

oh I missed "semi"

[Damiano Testa]

Yes, negation I also want to avoid.

[Reid Barton]

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

[Reid Barton]

You can't actually use monoid_with_zero because it implies monoid

[Adam Topaz]

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

[Reid Barton]

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

[Damiano Testa]

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]

oh docs#mul_zero_class

[Reid Barton]

What goofy names... mul_zero_class and distrib

[Damiano Testa]

so, extends add_comm_monoid, semigroup, distrib, mul_zero_class?

[Damiano Testa]

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

[Damiano Testa]

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]

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]

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

[Damiano Testa]

Yes, union=+ and intersection=*.

[Adam Topaz]

Umm... addition is symmetric difference no?

[Damiano Testa]

Ah, I had union in mind...

[Damiano Testa]

It is not the boolean-ish algebra that I want

[Kevin Buzzard]

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]

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

[Adam Topaz]

where you identify a finite set with its indicator function.

[Damiano Testa]

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

[Damiano Testa]

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

[Adam Topaz]

Is that distributive?

[Damiano Testa]

I thought that it was distributive "both ways"

[Adam Topaz]

Yeah you're probably right

[Reid Barton]

This already basically exists as distrib_lattice

[Damiano Testa]

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

[Damiano Testa]

Ah, I will look at distributive lattice then!

[Damiano Testa]

(the name sounds good)

[Adam Topaz]

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]

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

[Damiano Testa]

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

[Kevin Buzzard]

@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]

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

[Damiano Testa]

(hovering in VSCode answers my question \lub)

[Damiano Testa]

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

[Adam Topaz]

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]

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]

ooh, what a fun error message

[Damiano Testa]

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]

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

[Mario Carneiro]

note the decidable_eq requirement

[Damiano Testa]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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

[Sebastien Gouezel]

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]

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

[Mario Carneiro]

Actually you can just use _

[Damiano Testa]

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

[Damiano Testa]

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]

@[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]

The first part was generated by rintros?

[Damiano Testa]

Thanks! I will try it!

[Damiano Testa]

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]

If you do

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

lean will generate a lemma sus.ext and sus.ext_iff for you

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

you can also use ⟨_⟩

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Damiano Testa]

so then, why the a and b?

[Mario Carneiro]

it makes the intermediate state display a little nicer

[Damiano Testa]

I see

[Mario Carneiro]

it's totally optional here

[Damiano Testa]

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]

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]

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