# Zulip Chat Archive

## Stream: new members

### Topic: finset and universes

#### Eric Meinhardt (Jan 12 2022 at 03:39):

I'd like a definition of the equalizer of two partial functions (to/from finite types) with a type useful for more than doing calculations on concrete values:

```
import data.pfun
import data.fintype.basic
import data.finset
import data.set
variables (α β : Type*) [fintype α] [fintype β]
-- Perfectly fine for doing calculations on concrete values,
-- but the return type is not very informative: can we do better?
def pfun.equalizer_comp (f : α →. β) (g : α →. β) : set α :=
{a ∈ (f.dom ∩ g.dom) | (f a) = (g a)}
-- No combination of choices of return type and function body
-- (among what's here or many other things I've tried) typechecks
def pfun.equalizer_better (f : α →. β) (g : α →. β) :
finset {a : α // (f a ≠ part.none) ∧ (f a) = (g a) }
-- {a : α // (f a ≠ part.none) ∧ (f a) = (g a) }
-- {a : α // a ∈ f.dom ∧ (f a) = (g a)}
-- ...
:=
finset {a : α | (f a ≠ part.none) ∧ (f a) = (g a)}
-- {a ∈ (f.dom ∩ g.dom) | (f a) = (g a)}
-- {a ∈ (fintype.elems α) | (f a) = (g a) ∧ (f a ≠ part.none)}
-- ...
-- Also, I'd expect this to be a usefully simple starting point,
-- but there's a universe-related error described below.
variables (X Y : Type*)
def tfun.equalizer_naive (f : X → Y) (g : X → Y) : set X := {x ∈ X | f x = g x}
/- error @ '{':
type mismatch at application
{x ∈ X | f x = g x}
term
X
has type
Type u_1 : Type (u_1+1)
but is expected to have type
set X : Type u_1
-/
```

Any suggestions?

#### Kevin Buzzard (Jan 12 2022 at 06:07):

I'm not at lean right now but your definition of `equalizer_better`

seems to say "let the equalizer be the type of all finite subsets of (some set)".

Presumably it's giving you an error?

#### Yaël Dillies (Jan 12 2022 at 06:44):

The correct definition of `equalizer_naive`

is

```
def tfun.equalizer_naive (f : X → Y) (g : X → Y) : set X := {x : X | f x = g x}
```

because `X`

is a type, not a set.

#### Yaël Dillies (Jan 12 2022 at 06:45):

I don't know what `equalizer_better`

is supposed to achieve, but using `finset`

seems wrong.

#### Adam Topaz (Jan 12 2022 at 15:30):

Just guessing here... but do you want something like this?

```
import data.pfun
import data.fintype.basic
import data.finset
import data.set
variables {α β : Type*} [fintype α] [fintype β]
def pfun.equalizer_comp (f : α →. β) (g : α →. β) : set α :=
{a ∈ (f.dom ∩ g.dom) | (f a) = (g a)}
lemma pfun.equalizer_comp_finite (f : α →. β) (g : α →. β) : (f.equalizer_comp g).finite :=
set.finite.of_fintype (pfun.equalizer_comp f g)
noncomputable def pfun.equalizer_better (f : α →. β) (g : α →. β) : finset α :=
(f.equalizer_comp_finite g).to_finset
```

#### Yury G. Kudryashov (Jan 12 2022 at 16:47):

If you have appropriate decidable instances, then you can use docs#set.to_finset

#### Eric Meinhardt (Jan 12 2022 at 20:05):

My apologies for not elaborating on my goals here - I'm partially just trying to figure out how to do what I expect might be simpler things in Lean while also formalizing in Lean some definitions that are useful for a particular problem domain of interest. The general context is theoretical linguistics - ultimately proving results about a formalism for modeling sound patterns. Without elaborating too much more, the problem domain involves reasoning about partial functions to and from sets/types (and structures or operations over those sets/types and functions) that will *always be finite*.

Examples of these finite sets/types include

1. a finite set of symbols (i.e. an "alphabet" in the sense of formal language theory).

2. a finite set of binary or ternary-valued acoustic/articulatory "features" that lets every speech sound be described as a "feature vector" (i.e. a function from feature labels to values).

Examples of functions and structures of interest include

1. extremely simple "string" rewriting functions that are actually just symbol-to-symbol maps.

2. a restricted subset of feature-vector-to-feature-vector functions that model a traditional formalism for describing sound patterns.

3. the Boolean nearlattice over `α →. β`

for choices of `α, β`

mentioned above...

4. reasoning about fixpoints, composition, and inverse relations of these functions...

I expect that working in a problem domain that extensively trucks in finite sets will sometimes make defining or proving something in Lean easier and sometimes harder.

In this case, **my main goal** here is to have a named widget (a type? a function? a theorem? ....? I'm currently indifferent, because I don't know enough about Lean and because I am currently just exploring what I can do with Lean) that says every pair of partial maps `f, g : α →. β`

(on finite `α, β`

) defines a subtype of `α`

containing just those values `a : α`

where both `f`

and `g`

are defined and where `f(a) = g(a)`

. Should this subtype be a `set`

or `finset`

or ...? Does it *have* to be one of those or make more sense for it be one of those (e.g. to compose more easily with the rest of mathlib)? I'm not sure.

From what I just said and what I understand of Lean, neither `pfun.equalizer_comp`

nor `pfun.equalizer_naive`

(my version or @Yaël Dillies 's correct version) help me accomplish my first goal *because* the 'return type' (`set X`

/`set α`

) doesn't say very much about the relationship between `f, g`

and the value `pfun.equalizer_naive(f,g)`

and hence (as I understand it) neither would be useful for doing much besides concrete calculations.

#### Eric Wieser (Jan 12 2022 at 23:57):

You don't need the return type to say much about the relationship, that's what lemmas are for

#### Eric Wieser (Jan 12 2022 at 23:58):

For example, docs#nat.add 's return type doesn't tell you it's actually addition, it could be zero everywhere!

#### Eric Rodriguez (Jan 13 2022 at 00:05):

usually the way mathlib deals with this sort of things is `_spec`

lemmas, or just lemmas about the relationship, expanding on Eric's example, there's certainly a lot of lemmas about natural addition. however, I guess docs#category_theory.limits.has_equalizers gives some bundling, but this is almost certainly not what you want

#### Eric Rodriguez (Jan 13 2022 at 00:06):

i think your best shot would be a lemma `mem_equalizer_iff`

etc, etc

#### Eric Meinhardt (Jan 13 2022 at 00:51):

Thanks!

Eric Wieser said:

You don't need the return type to say much about the relationship, that's what lemmas are for

That sounds pragmatic, and I'll take a crack at something like @Eric Rodriguez 's suggestion (`mem_equalizer_iff`

). However, I am left wondering what a good guiding philosophy might be for when to make a function's codomain type be some more precise elaborated subtype vs. something simpler (supplemented with lemmas as needed).

#### Eric Wieser (Jan 13 2022 at 01:11):

Usually the purpose of "bundling" proofs into your return type is so that you can define operators on that resulting bundle that need that proof field

#### Eric Rodriguez (Jan 13 2022 at 01:13):

see docs#finset.attach, which is useful for taking sums that require proof fields as one such example

Last updated: Dec 20 2023 at 11:08 UTC