Restricting domains of functions

Stream: Is there code for X?

[Cayden Codel]

As I'm relatively new to Lean, I'm stumped on how to proceed in a way that will prevent headaches down the line. Essentially, I want to define a function or a family of functions that maps elements belonging to a list or a set (say, of natural numbers) to a boolean. So far, I've considered optional types and providing the list in the definition:

def opt_func := nat → option bool
def dep_func (ns : list nat) := ∀ (n : nat), n ∈ ns → bool

However, I don't know which of these is preferable, or if there is a third option that is better. Any thoughts or references to similar concepts in mathlib would be very helpful.

[Eric Wieser]

Another option is the signature {n // n ∈ ns} → bool.

[Eric Wieser]

Have you considered just returning ff for elements not in the list?

[Kevin Buzzard]

In Lean it is often very convenient to just return a "random" fixed value for the output when a function is applied to a value for which our mental model is that the answer is "undefined". For example in Lean 1/0=0 and this turns out to be much more convenient than letting division take values in option X.

[Yakov Pechersky]

Whatever definition you choose, the real test for it is how easy it is for you to prove things about it. All of these definitions are in some sense isomorphic to each other, but only a few of them will lend themselves to being easily used in proofs.

[Cayden Codel]

Ooh I will take a look at {n // n ∈ ns}, that may be what I was looking for. Thank you so much!

[Cayden Codel]

I'll return to methods of "random" fixed values outside the domain I care about if subtype doesn't pan out

[Kyle Miller]

Elaborating on choosing a "random" fixed value: sort of the point of choosing a fixed value is that it gives you an extensionality property. Two of these functions are equal if they're equal on the domain you care about. If you didn't constrain the junk values like this, then there can be multiple nonequal functions that do the same thing. This can sometimes be a problem when proving or counting things.

[Kyle Miller]

Here's a possible implementation of @Eric Wieser's suggestion:

def fun_on_list (ns : list nat) : Type := {f : nat → bool // ∀ n, f n → n ∈ ns}

This gives the subtype of functions that are ff outside the values in the list.

You can prove fun_on_list ns is docs#equiv to {n // n ∈ ns} → bool