Zulip Chat Archive

Stream: new members

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Lars Ericson (Dec 12 2020 at 16:05):

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

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

view this post on Zulip Lars Ericson (Dec 12 2020 at 16:06):

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

view this post on Zulip Kevin Buzzard (Dec 12 2020 at 16:07):

you have to read the error messages

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

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

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

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

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

view this post on Zulip Johan Commelin (Dec 12 2020 at 16:12):

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

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

view this post on Zulip Johan Commelin (Dec 12 2020 at 16:12):

Those messages are of the form

you gave me
  X
I am expecting
  Y

view this post on Zulip Johan Commelin (Dec 12 2020 at 16:13):

It is very important that you compare X and Y.

view this post on Zulip Kevin Buzzard (Dec 12 2020 at 16:13):

and + are probably definitionally the same in your situation.

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

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

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

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

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

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