Zulip Chat Archive

Stream: new members

Topic: sum of sets


view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:15):

I am trying to understand why this fails and how to fix it:

import data.real.basic

def set_sum : set   set   set 
| (X : set ) (Y : set ) := {x + y | x  X  y  Y}

view this post on Zulip Alex J. Best (Jul 23 2020 at 01:21):

It fails because lean's set notation doesn't support this, specifically the thing left of the | must just be an identifier like x.
This definition already exists in algebra/pointwise.lean

view this post on Zulip Alex J. Best (Jul 23 2020 at 01:22):

The definition there is as:

instance [has_add α] : has_add (set α) := image2 has_add.add

view this post on Zulip Alex J. Best (Jul 23 2020 at 01:22):

And image2 is

def image2 (f : α  β  γ) (s : set α) (t : set β) : set γ :=
{c |  a b, a  s  b  t  f a b = c }

view this post on Zulip Alex J. Best (Jul 23 2020 at 01:23):

There were some interesting related threads to do with changing this notation earlier today btw, https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23402.3A.20set.20builder.20notation/near/204661344

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:27):

Thank you.

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:32):

So I need to do this?

def set_sum : set   set   set 
| (X : set ) (Y : set ) := {z |  x  X,  y  Y, z = x + y}

view this post on Zulip Alex J. Best (Jul 23 2020 at 01:35):

Yeah that looks like it should work, does it?

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:36):

Yeah.

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:38):

Does the existing definition allow for writing something like X + Y?

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:39):

I tried that, but no luck. Not sure if I have it right though.

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:39):

For example:
def set_sum : set ℝ → set ℝ → set ℝ
| (X : set ℝ) (Y : set ℝ) := X + Y

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:40):

Not sure how to read the definition exactly.

view this post on Zulip Alex J. Best (Jul 23 2020 at 01:40):

Yes, because it is registered as a has_add instance. It works for me, are you importing algebra.pointwise

view this post on Zulip Reid Barton (Jul 23 2020 at 01:40):

Do you have it imported?

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:40):

Ah. Right. Sorry.

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:42):

Hmm. No, this does not work for me.

import data.real.basic
import data.set
import algebra.pointwise

def set_sum : set   set   set 
| (X : set ) (Y : set ) := X + Y

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:44):

I get:

failed to synthesize type class instance for
set_sum : set   set   set ,
X Y : set 
 has_add (set )

view this post on Zulip Bryan Gin-ge Chen (Jul 23 2020 at 01:53):

What version of mathlib are you using? Try leanproject up to get a more recent version.

view this post on Zulip Bryan Gin-ge Chen (Jul 23 2020 at 01:53):

Also note that you can get nice syntax highlighting on Zulip using #backticks.

view this post on Zulip Patrick Thomas (Jul 23 2020 at 01:56):

I'm not sure I have the command leanproject.

view this post on Zulip Bryan Gin-ge Chen (Jul 23 2020 at 01:59):

The community Lean tooling has been revamped in the past few months: try going through the #install instructions for your OS again. There's even tutorial videos!

view this post on Zulip Patrick Thomas (Jul 23 2020 at 02:01):

It has been a while since I used it. I'll give it a try. Thank you.


Last updated: May 10 2021 at 18:22 UTC