# Zulip Chat Archive

## Stream: new members

### Topic: How do I add union as addition to a has_add

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

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.

Last updated: May 13 2021 at 18:26 UTC