How do I add union as addition to a has_add

Stream: new members

[Lars Ericson]

I'm trying to make a has_add instance on a finset where addition is defined as set union. I know the set union operation exists because I checked it. Lean is kicking it back:

import algebra.group.defs
import data.finset.basic

def X : set ℕ := ({1, 2, 3} : finset ℕ)

#check X -- X : set ℕ
#check X ∪ X -- X ∪ X : set ℕ

instance X_has_add1 : has_add X := ⟨ λ x y, x ∪ y ⟩

with error message

failed to synthesize type class instance for
x y : ↥X
⊢ has_union ↥X

How do I do this right? I'm trying to show that {1,2,3} is an add_semigroup and this is step 1.

[Floris van Doorn]

You want to define the instance on finsets, not on elements of a particular finset X. So you want to show

instance : has_add (finset α) := ...

[Lars Ericson]

This is easy:

import data.finset.basic
instance : has_add ( finset ℕ  ) := ⟨ λ x y, x ∪ y ⟩

But what I want to do is:

• Define a finite set X={1,2,3} as a type so that if I say a : X then a can only take on values 1, 2 or 3.
• Define the power set 𝒫 X as a type, with a union operation
• Use the union operation as addition in has_add (𝒫 X).

... or the equivalent, but the idea is sets of subsets of {1,2,3}. This is my first crack at it but it doesn't work:

import data.finset.basic
instance : has_add ( finset ℕ  ) := ⟨ λ x y, x ∪ y ⟩

def X : set ℕ := ({1, 2, 3} : finset ℕ)
#check X -- X : set ℕ
#reduce X -- λ (x : ℕ), x = 1 ∨ x = 2 ∨ x = 3 ∨ false

def A := 𝒫 X
#check A -- A : set (set ℕ)
#reduce A -- λ (t : ℕ → Prop), ∀ ⦃a : ℕ⦄, t a → a = 1 ∨ a = 2 ∨ a = 3 ∨ false

def plus (x y : A) := λ (z : ℕ ), (x z) ∨ (y z) -- FAIL
/- function expected at
  x
term has type
  {x // x ∈ A} -/

instance : has_add A := ⟨ plus ⟩

[Alex J. Best]

The standard explicit finite set type is docs#fin with fin n being the subtype of natural numbers below n.

[Alex J. Best]

#check fin 3
#reduce fin 3

@[reducible]
def A := set (fin 3)
#check A
#reduce A

def plus (x y : A) := x ∪ y

might be what you're looking for

[Alex J. Best]

In this situation it might be best not to define types with names to be explicit things, I had to add the reducible attribute here so that lean still knows how to define a union of terms of type A.

[Alex J. Best]

I.e. rather than writing def plus (x y : A) := x ∪ y write def plus (x y : set (fin 3)) := x ∪ y if you're playing around with things.

[Floris van Doorn]

In that case you want instance : has_add (set X) := ... (which is equally easy to define, and uses nothing special about X).
I also agree with everything Alex said, though if you just want some example code, your X would work fine as well.

[Floris van Doorn]

Here is a code snippet that works:

import data.finset.basic
instance : has_add ( finset ℕ  ) := ⟨ λ x y, x ∪ y ⟩

def X : set ℕ := ({1, 2, 3} : finset ℕ)
#check X -- X : set ℕ
#reduce X -- λ (x : ℕ), x = 1 ∨ x = 2 ∨ x = 3 ∨ false

def A := set X
#check A -- A : set (set ℕ)
#reduce A -- λ (t : ℕ → Prop), ∀ ⦃a : ℕ⦄, t a → a = 1 ∨ a = 2 ∨ a = 3 ∨ false

def plus (x y : A) : A := (x ∪ y : set X)
example (x y : A) : A := set.union x y -- alternative

instance : has_add A := ⟨ plus ⟩

However, I strongly encourage you to not define A (or define it as local notation or something), and just use set X instead.

[Lars Ericson]

Thank you @Floris van Doorn and @Alex J. Best. For self-training I am trying fill out a bunch of these intermediary concepts with countable and concrete finite examples. This really helps me get started on the concrete finite ones. I got this far and then I got stuck on the case above:

import algebra.group.defs
import data.finset.basic
import data.nat.basic

instance X_is_nontrivial : nontrivial (fin 3) := fin.nontrivial
#check X_is_nontrivial --X_is_nontrivial : nontrivial X

instance X_has_add : has_add (fin 3):= fin.has_add
#check X_has_add -- X_has_add : has_add X

instance X_has_add_semigroup : add_semigroup ℕ := nat.add_semigroup
#check X_has_add_semigroup -- X_has_add_semigroup : add_semigroup X

where the whole homework is:
Screenshot-from-2020-12-12-09-15-45.png

[Kevin Buzzard]

import algebra.group.defs
import data.finset.basic
import data.nat.basic

example : nontrivial (fin 3) := by apply_instance

example : has_add (fin 3):= by apply_instance

example : add_semigroup ℕ := by apply_instance

The point of the type class inference framework is that the end user shouldn't have to worry about what these instances are called or where they are. Lean will fill in the "square bracket inputs" to functions automatically. Your #check outputs aren't the same as mine, I don't know what X is, but this is the reason why def X := fin 3 might be a bad idea -- because then apply_instance won't work any more when applied to X and you have to unfold the definition to get it working again.

[Kevin Buzzard]

import algebra.group.defs
import data.finset.basic
import data.nat.basic

@[derive nontrivial] def X := fin 3

example : nontrivial X := by apply_instance

example : has_add X := by unfold X; apply_instance -- apply_instance by itself won't work

[Lars Ericson]

Thanks @Kevin Buzzard. I will replace my uses of instance with lemma:

import algebra.group.defs
import data.nat.basic
lemma X_add_semigroup : add_semigroup ℕ := nat.add_semigroup
#check X_add_semigroup -- X_has_add_semigroup : add_semigroup ℕ

I like being able to #check the result because it gives me a little extra positive feedback.

For fin 3, even though it has_add, it doesn't appear to be an add_semigroup. This fails:

import data.finset.basic
lemma fin3_has_add : has_add (fin 3) := by apply_instance -- OK
instance fin3_add_semigroup : add_semigroup (fin 3) := by apply_instance -- FAIL

with error

tactic.mk_instance failed to generate instance for
  add_semigroup (fin 3)
state:
⊢ add_semigroup (fin 3)

Tactic library_search! also fails.

I tried a slightly different route:

def X : set ℕ := ({1, 2, 3} : finset ℕ)
def plus (x y : set X) : set X := (x ∪ y : set X)
lemma X_has_add : has_add (set X) := ⟨ plus ⟩
#check X_has_add : X_has_add : has_add (set ↥X)

lemma X_add_semigroup: add_semigroup (set X) := ⟨ plus ⟩

this also fails, with error:

type mismatch, term
  add_semigroup.mk plus
has type
  (∀ (a b c : set ↥X), a + b + c = a + (b + c)) → add_semigroup (set ↥X)
but is expected to have type
  add_semigroup (set ↥X)

So now I'm confused again. ∪ on sets should give me add_semigroup. Should I be working with power sets? That's where I started at the beginning of this thread. But this also fails with a similar error:

import data.finset.basic
instance : has_add ( finset ℕ  ) := ⟨ λ x y, x ∪ y ⟩
def X : set ℕ := ({1, 2, 3} : finset ℕ)
def A := set X
def plus (x y : A) : A := (x ∪ y : set X)
example (x y : A) : A := set.union x y -- alternative
lemma A_has_add : has_add A := ⟨ plus ⟩ -- OK
lemma A_add_semigroup : add_semigroup A := ⟨ plus ⟩ -- ERROR

namely

type mismatch, term
  add_semigroup.mk plus
has type
  (∀ (a b c : A), a + b + c = a + (b + c)) → add_semigroup A
but is expected to have type
  add_semigroup A

If I take the def A out, I still get an error:

import data.finset.basic
instance : has_add ( finset ℕ  ) := ⟨ λ x y, x ∪ y ⟩

def X : set ℕ := ({1, 2, 3} : finset ℕ)

def plus (x y : set X) : set X := (x ∪ y : set X)
example (x y : set X) : set X := set.union x y -- alternative

lemma A_has_add : has_add (set X) := ⟨ plus ⟩ -- OK

lemma A_add_semigroup : add_semigroup (set X) := ⟨ plus ⟩ -- ERROR

of

type mismatch, term
  add_semigroup.mk plus
has type
  (∀ (a b c : set ↥X), a + b + c = a + (b + c)) → add_semigroup (set ↥X)
but is expected to have type
  add_semigroup (set ↥X)

I'm stuck.

[Kevin Buzzard]

You shouldn't call them lemmas, the instances contain data and if you call them lemmas then the data will be forgotten and things will break

[Lars Ericson]

I can scope it out a little bit like this (which makes this a pretty good exercise):

import data.finset.basic
instance : has_add ( finset ℕ  ) := ⟨ λ x y, x ∪ y ⟩

def X : set ℕ := ({1, 2, 3} : finset ℕ)

def plus (x y : set X) : set X := (x ∪ y : set X)

instance set123_has_add : has_add (set X) := ⟨ plus ⟩ -- OK

lemma set123_add_assoc : ∀ a b c : set X, a + b + c = a + (b + c) :=
begin
  intro h1,
  exact sup_assoc, -- FAIL
end

instance A_add_semigroup : add_semigroup (set X) :=
{
  add := plus,
  add_assoc := set123_add_assoc
}

the exact sup_assoc came from library_search!. It fails, but gives a clue maybe as to a sub-lemma to prove (modelled after sup_assoc):

invalid type ascription, term has type
  ?m_3 ⊔ ?m_4 ⊔ ?m_5 = ?m_3 ⊔ (?m_4 ⊔ ?m_5)
but is expected to have type
  ∀ (b c : set ↥X), h1 + b + c = h1 + (b + c)
state:
h1 : set ↥X
⊢ ∀ (b c : set ↥X), h1 + b + c = h1 + (b + c)

[Kevin Buzzard]

Do you understand the error message? It gives you enough information about how to try and fix it.

[Lars Ericson]

It seems like I will have to copy all the sup_assoc machinery and textually replace the ⊔ with a ∪, is that correct?

theorem sup_assoc : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) :=
le_antisymm
  (sup_le
    (sup_le le_sup_left (le_sup_right_of_le le_sup_left))
    (le_sup_right_of_le le_sup_right))
  (sup_le
    (le_sup_left_of_le le_sup_left)
    (sup_le (le_sup_left_of_le le_sup_right) le_sup_right))

[Lars Ericson]

I.e. prove all the sup_assoc theorems and supporting lemmas in a union context.

[Kevin Buzzard]

All these questions you're asking -- all the errors you're posting are of the form "Lean expected a term of type X and you gave it a term of a completely different type". The errors are telling you what you did wrong.

[Lars Ericson]

I have to prove set union is associative, is the clue.

[Kevin Buzzard]

you have to read the error messages

[Lars Ericson]

That is, library_search! seems to be looking for something that fits the bill, but I don't know in Lean how to instantiate ⊔ with ∪. I am not willfully ignoring the error messages, I am trying to figure out why library_search! took me here and what I need to do next. Naively, it's a copy and replace of all of sup_assoc.

[Kevin Buzzard]

invalid type ascription, term has type
  ?m_3 ⊔ ?m_4 ⊔ ?m_5 = ?m_3 ⊔ (?m_4 ⊔ ?m_5)
but is expected to have type
  ∀ (b c : set ↥X), h1 + b + c = h1 + (b + c)
state:
h1 : set ↥X
⊢ ∀ (b c : set ↥X), h1 + b + c = h1 + (b + c)

says "the term you gave me does not start with "for all" but the term I want starts with "for all".

[Kevin Buzzard]

type mismatch, term
  add_semigroup.mk plus
has type
  (∀ (a b c : set ↥X), a + b + c = a + (b + c)) → add_semigroup (set ↥X)
but is expected to have type
  add_semigroup (set ↥X)

says "the term you gave me is of the form X -> Y but I was expecting a term of type Y"

[Johan Commelin]

Kevin Buzzard said:

you have to read the error messages

@Lars Ericson I get this sort of error messages all the time. And they help me figure out my next step.
Learning how to read these error messages is not hard and crucial for a happy Lean experience.

[Johan Commelin]

Basically, these particular error messages are telling you: hey, your answer is almost right, but not quite. If you change it a little bit, I'll be happy.

[Johan Commelin]

And it gives you very good clues about how you need to change your code.

[Lars Ericson]

Thank you. I didn't know how to fix the → message which is why I broke down the problem more. When I looked at the ⊔ message I saw the ⊔ versus + and didn't focus on the ∀. I will focus on the ∀.

[Johan Commelin]

Those messages are of the form

you gave me
  X
I am expecting
  Y

[Johan Commelin]

It is very important that you compare X and Y.

[Kevin Buzzard]

⊔ and + are probably definitionally the same in your situation.

[Kevin Buzzard]

If you give it a term of type X and it was expecting a term of type Y, and X and Y are definitionally equal, this will be fine.

[Lars Ericson]

#print notation tells me that

_ `⊔`:65 _:65 := has_sup.sup
_ `+`:65 _:65 := has_add.add

Knowing a little now about mathlib naming conventions, this tells me that I should instead be using add_assoc. If the proofs of add_assoc and sup_assoc are identical up to notation, maybe there is some code factoring that could be done to make one theorem apply to both notations. There is a proof for sup_assoc:

theorem sup_assoc : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) :=
le_antisymm
  (sup_le
    (sup_le le_sup_left (le_sup_right_of_le le_sup_left))
    (le_sup_right_of_le le_sup_right))
  (sup_le
    (le_sup_left_of_le le_sup_left)
    (sup_le (le_sup_left_of_le le_sup_right) le_sup_right))

The definition of add_assoc is a little more mysterious. It shows as a theorem in the docs:

theorem add_assoc {G : Type u} [add_semigroup G] (a b c : G) : a + b + c = a + (b + c)

but the source is hard to interpret. This is the only thing I see in the file:

attribute [no_rsimp] add_assoc -- TODO(Mario): find out why this isn't copying

Game theory has it's own definition:

theorem add_assoc : ∀ (x y z : game), (x + y) + z = x + (y + z) :=
begin
  rintros ⟨x⟩ ⟨y⟩ ⟨z⟩,
  apply quot.sound,
  exact add_assoc_equiv
end

This is fairly compact (unlike the sup definition which relies on a lot of lemmas), so maybe I can just copy this one over and give it a try, if add_assoc on it's own doesn't work.

And actually this comes a lot closer:

import data.finset.basic
instance : has_add ( finset ℕ  ) := ⟨ λ x y, x ∪ y ⟩

def X : set ℕ := ({1, 2, 3} : finset ℕ)

def plus (x y : set X) : set X := (x ∪ y : set X)

instance X_has_add : has_add (set X) := ⟨ plus ⟩ -- OK

instance A_add_semigroup : add_semigroup (set X) :=
{
  add := plus,
  add_assoc := add_assoc -- ERROR
}

The error message is:

type mismatch at field 'add_assoc'
  add_assoc
has type
  ∀ (a b c : ?m_1), a + b + c = a + (b + c)
but is expected to have type
  ∀ (a b c : set ↥X), a + b + c = a + (b + c)

Now once again I am stumped. I am looking at the error message. It says I am really close. It just doesn't know how to match a type metavariable ?m_1 with a concrete type set ↥X.

What do I do in this case? I'm guess I need to use @add_assoc instead

add_assoc : ∀ {G : Type u_1} [_inst_1 : add_semigroup G] (a b c : G), a + b + c = a + (b + c)

and fill out each implicit argument explicitly.

[Lars Ericson]

DONE (with a hybrid approach of copying the technique in the game theory version to fix the ∀ and then finally applying sup_assoc even though ⊔ and + map to different types):

import data.finset.basic

def X : set ℕ := ({1, 2, 3} : finset ℕ)

def plus (x y : set X) : set X := (x ∪ y : set X)

instance X_has_add : has_add (set X) := ⟨ plus ⟩

theorem X_add_assoc : ∀ (x y z : set X), (x + y) + z = x + (y + z) :=
begin
  rintro x y z,
  exact sup_assoc,
end

instance X_add_semigroup : add_semigroup (set X) :=
{
  add := plus,
  add_assoc := X_add_assoc
}

[Kevin Buzzard]

theorem X_add_assoc (x y z : set X) : (x + y) + z = x + (y + z) := sup_assoc

Why not move x,y,z before the colon and then just go full term mode?

[Lars Ericson]

Thank you. Shortest version:

import data.finset.basic
def X : set ℕ := ({1, 2, 3} : finset ℕ)
def plus (x y : set X) : set X := (x ∪ y : set X)
instance X_has_add : has_add (set X) := ⟨ plus ⟩
theorem X_add_assoc (x y z : set X) :  (x + y) + z = x + (y + z) := sup_assoc
instance X_add_semigroup : add_semigroup (set X) := ⟨ plus, X_add_assoc ⟩

[Kevin Buzzard]

I usually stick with the { ... } notation for making structure instances such as X_add_semigroup, because it's more readable. Note that you don't have to name the instances either -- Lean will find them automatically. The very fact that (x + y) + z typechecks demonstrates this.