Defining a function

Stream: new members

[King Arthur]

Say you have a type X and a proof that x : X can only take on n distinct cases. Is it then possible to define a function from X to some type Y using each of those cases without necessarily making X an inductive type?

[Anne Baanen]

The way to do this depends a lot on the way you prove that x : X can only take on n distinct values. For example, we have the notation ![1, 2, 3] for writing a function fin 3 → ℤ. So if you have a surjective function f : fin n → X then you can take the section of f and compose it with a function like ![...].

[King Arthur]

Good to know! But for the sake of simplicity, let's say there are only two cases: like, maybe x : X is either some object e : X or anything else that isn't e. How would I approach making f : X → Y using these two cases?

[Anne Baanen]

You can use an if expression: def f (x : X) := if h : x = e then _ else _ (see docs#ite or docs#dite)

[King Arthur]

I see, thanks!

[King Arthur]

Also, is it possible to define a function from a set of ordered pairs, given a proof that it passes the vertical line test?

[Kevin Buzzard]

Not without classical.some but yes

[King Arthur]

I'm fine with classical.some haha. is there any specific API for this task? or is this a lot more complicated than I'm thinking it is

[Yakov Pechersky]

Not complicated. What's the set you have? What if the caller of the function gives you a term that isn't in any of the pairs?

[King Arthur]

right, fair. but let's say you do also have a proof that there's a unique pair for every single object in the domain. would that be enough?

[Yakov Pechersky]

I imagine the expression of that assumption is "H : forall x : X, exists p in s, p.1 = x", then your function is "lambda x, (classical.some (H x)).2"

[Yakov Pechersky]

You don't even need a unique pair to define the function, just a pair.

[King Arthur]

oh neat, thanks!

[Yakov Pechersky]

Or you can phrase it like "H : forall x : X, exists y : Y, (x, y) in s", and the function is "lambda x, classical.some (H x)"