set of pre-images given a set of sets

Stream: new members

[Logan Murphy]

Having some difficulty formalizing what should be a simple mathematical intuition. Suppose I have a structure which organizes
1) a set X of type α
2) a set D of type β
3) a function f : α → β
4) a finite set of sets {D₁, D₂... Dₙ} such that each Dᵢ ⊆ D

and I want to create a set of pre-images of f, a set of sets {X₁, X₂... Xₙ} where Xᵢ = {x ∈ X | f(x) ∈ Dᵢ}

The structure for points 1-4 I've defined as

structure foo (α β : Type) :=
(X : set α)
(D : set β)
(f : α → β)
(Ds : finset (set β))
(subs_D : ∀ s ∈ Ds, s ⊆ D)

But I have been struggling to come up with a way to write something like

def pre_images (f : foo α β) : finset (set α) := sorry

I haven't been able to work out how set.preimage should fit in to this picture. I'm also wondering if it would be better to use a (finite?) indexed set instead of finset for this purpose. Any suggestions would be appreciated!

[Kyle Miller]

This might be it:

def pre_images {α β} (f : foo α β) [decidable_eq (set α)] : finset (set α) :=
finset.image (set.preimage f.f) f.Ds

The decidable_eq instance refers to how you need to be able to tell whether two given sets are equal to be able to do deduplication. If you already are in the classical locale, then I don't think you need this.

[Logan Murphy]

cool, I will try it out. Thank you very much!

[Logan Murphy]

Trying out a small example without using finset just to observe the behaviour, I'm not sure how to parse the type error I've gotten.

import  data.set.basic
open set
variables α  β: Type

structure foo (α β : Type) :=
(X : set α)
(D : set β)
(f : α → β)
(Ds : set (set β))

def pre_images (bar : foo α β) [decidable_eq (set α)] : set (set α) :=
image (preimage bar.f) bar.Ds

def fun1 (b : bool) : ℕ := begin cases b, {exact 5}, {exact 7} end

def struct : foo bool ℕ := foo.mk {tt, ff} {5,7} fun1 {{5},{7}}

def test : set (set ℕ) := pre_images  struct -- error here

Err :

type mismatch, term
pre_images ?m_1
has type
Π (β : Type), foo ?m_1 β → Π [_inst_1 : decidable_eq (set ?m_1)], set (set ?m_1) : Type 1
but is expected to have type
set (set ℕ) : Type

[Yakov Pechersky]

I expanded the pre_images defn:

def test : set (set ℕ) := let struct := (foo.mk {tt, ff} {5,7} fun1 {{5},{7}}) in
  image (preimage _) struct.Ds -- you need an ℕ → ℕ

[Yakov Pechersky]

The α β : Type variables were being explicit. Now, with this syntax, you just need to know that your test was typed wrong initially. This works:

import  data.set.basic
open set
variables {α β: Type}

structure foo (α β : Type) :=
(X : set α)
(D : set β)
(f : α → β)
(Ds : set (set β))

def pre_images (bar : foo α β) : set (set α) :=
image (preimage bar.f) bar.Ds

def fun1 (b : bool) : ℕ := begin cases b, {exact 5}, {exact 7} end

def test : set (set bool) := let struct := (foo.mk {tt, ff} {5,7} fun1 {{5},{7}}) in
  pre_images struct

[Kyle Miller]

For one, you should see what #check pre_images is. Because your variables declaration involves non-implicit arguments, the first two arguments to pre_images are α and β. For another, you might have meant test : set (set bool).

Since you won't have a decidable_eq instance most of the time, you may as well do this:

import  data.set.basic
open set

noncomputable theory
open_locale classical

variables {α β: Type}

structure foo (α β : Type) :=
(X : set α)
(D : set β)
(f : α → β)
(Ds : set (set β))

def pre_images (bar : foo α β) : set (set α) :=
image (preimage bar.f) bar.Ds

def fun1 (b : bool) : ℕ := begin cases b, {exact 5}, {exact 7} end

def struct : foo bool ℕ := foo.mk {tt, ff} {5,7} fun1 {{5},{7}}

def test : set (set bool) := pre_images struct

[Kyle Miller]

Oh right, these are set and not finset, so no need for the noncomputable theory and open_locale classical here.

[Yakov Pechersky]

You can also do this:

def fun1 (b : bool) : ℕ := cond b 5 7

[Yakov Pechersky]

As it is right now, nothing required any decidable_eq

[Logan Murphy]

Thanks to you both!