Zulip Chat Archive

Stream: Is there code for X?

Topic: evaluation map from sets to sets


view this post on Zulip Xavier Xarles (Feb 03 2021 at 12:41):

Dear all,
I need to define something quite easy like
def foo (A : Type*)(B : Type*) : A → set(A → B)→ set B
where it send (a:A) and a set s : set(A → B) the set " { f(a) for f in s}". It is already defined something like this, or can somebody help me with the code?

view this post on Zulip Johan Commelin (Feb 03 2021 at 12:44):

You can either define it explicitly as {x | \exists a : A, \exists f \in s, x = f a}.
Another option is to define it as the union of the ranges of the f \in s:

\bigcup f \in s, set.range f

view this post on Zulip Johan Commelin (Feb 03 2021 at 12:44):

I don't think this is in mathlib yet.

view this post on Zulip Xavier Xarles (Feb 03 2021 at 13:07):

So the first solution will be to write something like
def foo (A : Type*)(B : Type*) : A → set(A → B)→ set B := λ a s, {x | ∃ a : A, ∃ f ∈ s, x = f a}
but it gives me an strange error, complaining about the f.

view this post on Zulip Johan Commelin (Feb 03 2021 at 13:11):

What happens if you write \exists (f : A \to B) (h : f \in s), x = f a?

view this post on Zulip Xavier Xarles (Feb 03 2021 at 13:16):

nice, it works, thank you

view this post on Zulip Adam Topaz (Feb 03 2021 at 14:47):

@Xavier Xarles You can also use do notation, as follows:

import data.set

def foo (A : Type*)(B : Type*) : A  set(A  B) set B := λ a fs, do {f  fs, return (f a)}

I think this is quite intuitive.

view this post on Zulip Floris van Doorn (Feb 03 2021 at 19:09):

There are a lot of set operations that are really applications of set.image and set.preimage. I recommend using those, so that you can use all the properties about them. In this case, you can use:

import data.set.basic
def foo (A B : Type*) : A  set (A  B)  set B :=
λ x s, (λ f : A  B, f x) '' s

view this post on Zulip Floris van Doorn (Feb 03 2021 at 19:10):

A lot of properties about set.image (notation '') are here: https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.mem_image_iff_bex

view this post on Zulip Johan Commelin (Feb 03 2021 at 19:13):

Whoops... @Xavier Xarles I now realise that my answers are maths-incorrect. You have a fixed a, whereas I gave answers that range over all a.

view this post on Zulip Adam Topaz (Feb 03 2021 at 19:19):

Just in case it helps:

import data.set

@[simp]
def foo {A B : Type*} : A  set (A  B)  set B := λ x s, (λ f : A  B, f x) '' s

@[simp]
def bar {A B : Type*} : A  set (A  B)  set B := λ a fs, do {f  fs, return (f a)}

example {A B : Type*} (a : A) (fs : set (A  B)) : foo a fs = bar a fs := by tidy

view this post on Zulip Floris van Doorn (Feb 03 2021 at 19:20):

Also, (λ f : A → B, f x) is function.eval x, and there are already a few properties about images of function.eval in the file I linked, like docs#set.eval_image_pi.

view this post on Zulip Kyle Miller (Feb 03 2021 at 22:24):

This can also be done with applicative functors rather than the full monad:

def foo (A : Type*) (B : Type*) : A  set (A  B)  set B := λ a fs, fs <*> pure a

Unfolding some definitions, it turns out that set.seq applies a set of functions to a set of values and forms the set of all values:

def foo (A : Type*) (B : Type*) : A  set (A  B)  set B := λ a fs, fs.seq {a}

view this post on Zulip Adam Topaz (Feb 03 2021 at 22:32):

Yeah, pure a for the monad set is the singleton {a}, and bind is given by a big union.

view this post on Zulip Adam Topaz (Feb 03 2021 at 22:33):

docs#set.bind_def

view this post on Zulip Kyle Miller (Feb 03 2021 at 23:07):

I should have looked at your first example more closely -- it only uses that set is a functor. Point-free style using set.image, which is set's functor.map:

def foo (A : Type*) (B : Type*) : A  set (A  B)  set B := set.image  function.eval

The generalized version:

def foo (F) [functor F] (A : Type*) (B : Type*) : A  F (A  B)  F B := functor.map  function.eval

I found a Haskell library where they call this function flap, which is maybe a play on how function.eval is equivalently flip ($)?


Last updated: May 07 2021 at 22:14 UTC