finset and universes

Stream: new members

[Eric Meinhardt]

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]

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]

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]

I don't know what equalizer_better is supposed to achieve, but using finset seems wrong.

[Adam Topaz]

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]

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

[Eric Meinhardt]

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]

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

[Eric Wieser]

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

[Eric Rodriguez]

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]

i think your best shot would be a lemma mem_equalizer_iff etc, etc

[Eric Meinhardt]

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]

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]

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