## Stream: new members

#### Lars Ericson (Dec 12 2020 at 01:34):

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 (Dec 12 2020 at 01:37):

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 (Dec 12 2020 at 04:21):

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 (Dec 12 2020 at 05:16):

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

#### Alex J. Best (Dec 12 2020 at 05:19):

#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 (Dec 12 2020 at 05:20):

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 (Dec 12 2020 at 05:20):

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 (Dec 12 2020 at 06:23):

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 (Dec 12 2020 at 06:24):

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 (Dec 12 2020 at 14:27):

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



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

#### Kevin Buzzard (Dec 12 2020 at 15:03):

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 (Dec 12 2020 at 15:04):

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 (Dec 12 2020 at 15:45):

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

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


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


with error

tactic.mk_instance failed to generate instance for
state:


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)



this also fails, with error:

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


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


namely

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


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
has type
(∀ (a b c : set ↥X), a + b + c = a + (b + c)) → add_semigroup (set ↥X)
but is expected to have type


I'm stuck.

#### Kevin Buzzard (Dec 12 2020 at 16:01):

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 (Dec 12 2020 at 16:03):

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

{
}


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 (Dec 12 2020 at 16:04):

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

#### Lars Ericson (Dec 12 2020 at 16:04):

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 (Dec 12 2020 at 16:05):

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

#### Kevin Buzzard (Dec 12 2020 at 16:05):

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 (Dec 12 2020 at 16:06):

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

#### Kevin Buzzard (Dec 12 2020 at 16:07):

you have to read the error messages

#### Lars Ericson (Dec 12 2020 at 16:08):

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 (Dec 12 2020 at 16:09):

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 (Dec 12 2020 at 16:10):

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


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

#### Johan Commelin (Dec 12 2020 at 16:10):

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 (Dec 12 2020 at 16:11):

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 (Dec 12 2020 at 16:12):

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

#### Lars Ericson (Dec 12 2020 at 16:12):

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 (Dec 12 2020 at 16:12):

Those messages are of the form

you gave me
X
I am expecting
Y


#### Johan Commelin (Dec 12 2020 at 16:13):

It is very important that you compare X and Y.

#### Kevin Buzzard (Dec 12 2020 at 16:13):

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

#### Kevin Buzzard (Dec 12 2020 at 16:18):

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 (Dec 12 2020 at 16:51):

#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,
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

{
}


The error message is:

type mismatch at field '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 (Dec 12 2020 at 16:58):

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)

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

{
}


#### Kevin Buzzard (Dec 12 2020 at 17:01):

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 (Dec 12 2020 at 17:02):

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)

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.