## Stream: general

### Topic: partial functions

#### Victor Porton (Jul 07 2018 at 15:43):

Why this does not work?

-- Switch from a function on a subset to a function to option monad
def subfunc_to_option {α β: Type} {c: α → Prop} (f: {x:α // c x} → β) : α → option β :=
λ y: α, if c y then some (f (subtype.mk y (arbitrary (c y) [true_inhabited (c y)]))) else none

#### Kenny Lau (Jul 07 2018 at 15:43):

put [decidable_pred c] in the list of assumptions (before the colon)

#### Victor Porton (Jul 07 2018 at 15:45):

Kenny, I did what you say. Moreover open classical is already in effect. But it does not work now too

#### Chris Hughes (Jul 07 2018 at 15:53):

def subfunc_to_option {α β: Type} {c: α → Prop} [decidable_pred c]
(f: {x:α // c x} → β) : α → option β :=
λ y: α, if h : c y then some (f (subtype.mk y h)) else none


#### Chris Hughes (Jul 07 2018 at 15:55):

if h : c y instead of if c y gives you access to the proof.

#### Victor Porton (Jul 07 2018 at 15:56):

Chris, Thanks it works now. But I am curious why my old code (with arbitrary) didn't work.

#### Chris Hughes (Jul 07 2018 at 15:57):

Because there was no way of telling that the type c y was inhabited.

#### Chris Hughes (Jul 07 2018 at 15:59):

It's actually very unusual to use inhabited on Props.

#### Chris Hughes (Jul 07 2018 at 16:00):

Also open classical only opens the classical namespace, it doesn't give you decidability. You need local attribute [instance] classical.prop_decidable for that.

#### Victor Porton (Jul 07 2018 at 16:11):

I tried to synthesize the function in another direction. Now I know where is my error but don't know how to fix it:

-- Switch from function to option monad to a function on a subset
def option_to_subfunc {α β: Type} (f: α → (option β)) :=
λ y: {x:α // f x ≠ none},
match f y with
| some x := y
| none := sorry

#### Chris Hughes (Jul 07 2018 at 16:15):

You needed to give the type, and write end at the end of your match

def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // f x ≠ none} → {x:α // f x ≠ none} :=
λ y: {x:α // f x ≠ none},
match f y with
| some x := y
| none := sorry
end


#### Johan Commelin (Jul 07 2018 at 16:15):

@Victor Porton If you surround your code between three backticks, then it will be typeset in a codeblock. If you append "lean" to the first 3 backticks, then it will get highlighting!

#### Kevin Buzzard (Jul 07 2018 at 16:16):

Again f y does not make sense because alpha is not equal to the subtype you are using. f wants an input of type alpha and you are feeding it y. Did you read about subtypes in Theorem in Lean?

#### Victor Porton (Jul 07 2018 at 16:16):

@Chris Hughes Your code does not validate. What I really wanted to ask is what to do instead of sorry. I am lost about this

#### Chris Hughes (Jul 07 2018 at 16:17):

It does make sense because there's a coercion

#### Victor Porton (Jul 07 2018 at 16:17):

Yes, I knew that here there is a coercion

#### Kevin Buzzard (Jul 07 2018 at 16:17):

Oh -- it does make sense in this context because there's a coercion!

:-)

#### Chris Hughes (Jul 07 2018 at 16:21):

In response to a question in (no topic) that should have been here.

def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // f x ≠ none} → {x:α // f x ≠ none} :=
λ y: {x:α // f x ≠ none},
have hfy : f y ≠ none := y.2,
match f y, hfy with
| some x := λ hfy, y
| none := λ hfy, (hfy rfl).elim
end


#### Victor Porton (Jul 07 2018 at 16:25):

@Chris Hughes 1. The values type of your option_to_subfunc is wrong; it should be \beta not {x:α // f x ≠ none}. 2. Do I understand correctly that the values in have are "ignored" (not included into the result) when building the value of the defined object? 3. What this elimination do? (I am a very novice and understand your code partially.)

#### Victor Porton (Jul 07 2018 at 16:26):

@Chris Hughes Sorry for a stupid question but I do not understand what := after have means

#### Chris Hughes (Jul 07 2018 at 16:27):

It's the same as from

#### Victor Porton (Jul 07 2018 at 16:29):

Sorry, what is λ hfy, y?

#### Chris Hughes (Jul 07 2018 at 16:29):

I put hfy after the match so I would have access to the fact that f y ≠ none. In the none cases hfy has type none ≠ none which is obviously false, so I can use false.elim to define the function

#### Chris Hughes (Jul 07 2018 at 16:30):

hfy is just a proof that f y = none or in the some case that some ≠ none

#### Chris Hughes (Jul 07 2018 at 16:32):

I think this is the function you want

def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // f x ≠ none} → β :=
λ y: {x:α // f x ≠ none},
have hfy : f y ≠ none := y.2,
match f y, hfy with
| some x := λ hfy, x
| none := λ hfy, (hfy rfl).elim
end


#### Victor Porton (Jul 07 2018 at 16:33):

what is (hfy rfl).elim?

#### Chris Hughes (Jul 07 2018 at 16:33):

match f y, hfy with means I now have to define a function with type Π x : option β, x ≠ none → β

#### Chris Hughes (Jul 07 2018 at 16:34):

hfy rfl is a proof of false

#### Chris Hughes (Jul 07 2018 at 16:34):

(hfy rfl).elim is another way of writing false.elim (hfy rfl).

#### Victor Porton (Jul 07 2018 at 16:35):

I need to time to review all you wrote

#### Chris Hughes (Jul 07 2018 at 16:35):

false.elim is a function that gives you a term of any type given a proof of false

#### Victor Porton (Jul 07 2018 at 16:39):

What I don't understand: Why is it | some x := λ hfy, x not | some x := x. It should be a value in \b, right? But λ hfy, x is a function and so it looks for me that it can't be in \b

err.. wrong

#### Chris Hughes (Jul 07 2018 at 16:43):

match f y, hfy with means I now have to define a function with type Π x : option β, x ≠ none → β, not option β → β any more. Even though I'm not using the fact that x ≠ none in the some case, I still have access to it.

#### Victor Porton (Jul 07 2018 at 16:46):

Hm, it is harder than I expected, I yet do not understand the details of this simple construct. I initially started to learn Lean to rewrite my English book in Lean. Now I suspect that it would take me too much time to master Lean. What is your advice: learn Lean or just to keep writing math in English?

#### Chris Hughes (Jul 07 2018 at 16:47):

What field of maths is your book on?

#### Chris Hughes (Jul 07 2018 at 16:48):

I think maybe a good way to think about the function is that the output of type β is the function of type Π x : option β, x ≠ none → β applied to f y and hfy

#### Victor Porton (Jul 07 2018 at 16:48):

@Chris Hughes I discovered a new subfield of general topology (though some man expressed that he does not consider it a subfield of general topology). For example the formula $f\circ\mu \leq \nu\circ f$ means that $f$ is a continuous morphisms from $\mu$ to $\nu$.

#### Chris Hughes (Jul 07 2018 at 16:50):

I don't really know much about topology (I'm a first year undergraduate). I think @Patrick Massot and @Johannes Hölzl know about topology in lean.

#### Victor Porton (Jul 07 2018 at 16:50):

Honestly, I am somehow lost in your Lean discussion. I may re-read it again

#### Victor Porton (Jul 07 2018 at 16:51):

@Chris Hughes This does not matter, as I build my version of topology from scratch, without using the classical GT

#### Victor Porton (Jul 07 2018 at 16:54):

Is match f y, hfy the same as match \<f y, hfy\>?

#### Chris Hughes (Jul 07 2018 at 17:01):

more or less

def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // f x ≠ none} → β :=
λ y: {x:α // f x ≠ none},
have hfy : f y ≠ none := y.2,
match (⟨f y, hfy⟩ : Σ' x : option β, x ≠ none) with
| ⟨some x, hfy⟩ := x
| ⟨none, hfy⟩ := (hfy rfl).elim
end


#### Chris Hughes (Jul 07 2018 at 17:03):

I think that might be more confusing though.

#### Victor Porton (Jul 07 2018 at 17:06):

It seems that I do (or almost do) understand your last ("more confusing") code. But why the "less confusing" code (which I don't understand) uses some x := λ hfy, x not some x := x?

#### Victor Porton (Jul 07 2018 at 17:06):

oh, it seems I got the idea

#### Victor Porton (Jul 07 2018 at 17:09):

I have yet a question. How does the following work?

match f y, hfy with
| some x := λ hfy, x
| none := λ hfy, (hfy rfl).elim
end


We have two expressions in match arguments and just one in the math conditions. How do they match?

#### Chris Hughes (Jul 07 2018 at 17:16):

I don't really understand enough about the equation compiler to answer the question properly.

#### Victor Porton (Jul 07 2018 at 17:17):

@Chris Hughes Anyway much thanks for your support. Also what does $\Sigma'$ mean? It has added apostrophe

#### Victor Porton (Jul 07 2018 at 17:18):

Now I "almost" understand. Thanks

#### Chris Hughes (Jul 07 2018 at 17:18):

It's just like Sigma, except the constructors can be either proofs or data, whereas Sigma only takes data.

#### Chris Hughes (Jul 07 2018 at 17:22):

This is perhaps a better way of writing the function

def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // f x ≠ none} → β :=
λ y : {x:α // f x ≠ none},
let g : Π x : option β, x ≠ none → β :=
λ x, match x with
| (some x) := λ h, x
| none := λ h, (h rfl).elim
end in
g (f y) y.property


#### Victor Porton (Jul 07 2018 at 17:23):

@Chris Hughes It gets better as I rewrote it more understandably

def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // f x ≠ none} → β :=
λ y: {x:α // f x ≠ none},
have hfy : f y ≠ none := y.2,
match f y, hfy with
| some x, hfy := x
| none  , hfy := (hfy rfl).elim
end


#### Victor Porton (Jul 07 2018 at 17:24):

I don't understand your last code. For example, what is property?

#### Chris Hughes (Jul 07 2018 at 17:25):

Another way of writing y.2

#### Victor Porton (Jul 07 2018 at 17:26):

Why do you think the the second way is better?

#### Chris Hughes (Jul 07 2018 at 17:30):

I had to try out a few things to get the first way to work. For example this didn't work. I don't really have a good reason why the second way is better other than that.

def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // f x ≠ none} → β :=
λ y: {x:α // f x ≠ none},
match f y, y.2 with
| some x, hfy := x
| none  , hfy := (hfy rfl).elim
end


#### Chris Hughes (Jul 07 2018 at 17:33):

It's clearer what's going on, because in the first method, it's not obvious that hfy will have type some x ≠ none or none ≠ none, and not f y ≠ none in the match expression.

#### Mario Carneiro (Jul 07 2018 at 18:10):

In that last one, y.2 has the type f y.1 ≠ none, so it is important that you write f y.1 instead of f (\u y)

#### Patrick Massot (Jul 07 2018 at 18:26):

def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // option.is_some (f x)} → β | ⟨x, h⟩ := option.get h


#### Chris Hughes (Jul 07 2018 at 18:27):

I thought the function probably already existed, but I couldn't find it.

#### Patrick Massot (Jul 07 2018 at 18:27):

option.is_some is directly about what you care about instead of its negation

#### Patrick Massot (Jul 07 2018 at 18:28):

I don't know if it already exists

#### Chris Hughes (Jul 07 2018 at 18:30):

I think I saw it before, but I was thrown off by the fact is_some is bool rather than Prop

#### Patrick Massot (Jul 07 2018 at 18:30):

Oh, you mean is_some already existed.

#### Patrick Massot (Jul 07 2018 at 18:31):

I thought you were referring to option_to_subfunc

#### Chris Hughes (Jul 07 2018 at 18:32):

I was referring to option_to_subfunc or things like it, and I saw option.get but I didn't like it because is_some is bool

#### Victor Porton (Jul 07 2018 at 20:02):

@Patrick Massot What is this |?

#### Victor Porton (Jul 07 2018 at 20:03):

@Patrick Massot Oh, it is pattern matching, I got

#### Victor Porton (Jul 07 2018 at 20:12):

weird, I can't find def option in Lean library

#### Victor Porton (Jul 07 2018 at 20:12):

got: inductive option

#### Victor Porton (Jul 07 2018 at 20:14):

@Patrick Massot Where is option.get defined?

#### Victor Porton (Jul 07 2018 at 20:15):

found: basic.lean

#### Victor Porton (Jul 07 2018 at 20:22):

I also don't understand (hfy rfl).elim. Does it contain hfy applied to rfl? I would be not surprised if rfl were applied to an equality, but I see inequality applied to rfl what looks for me the "opposite" of what can be done. What is it?

#### Chris Hughes (Jul 07 2018 at 20:26):

hfy has type none ≠ none which is definitionally equal to none = none → false. rfl is a proof that none = none so hfy rfl has type false

#### Victor Porton (Jul 07 2018 at 21:46):

How having a function f determine its domain?

#### Kenny Lau (Jul 07 2018 at 21:46):

it's in the type of the function

#### Victor Porton (Jul 07 2018 at 21:47):

@Kenny Lau So use match?

#### Victor Porton (Jul 07 2018 at 21:47):

I have f: (Σ c:α → Prop, {x:α // c x}) and want to get the c

#### Kenny Lau (Jul 07 2018 at 21:48):

I... don't think that's how this works

#### Victor Porton (Jul 07 2018 at 21:48):

What I try is like:

noncomputable def subfunc_to_option2 {α β: Type} --[decidable_pred c]
(f: (Σ c:α → Prop, {x:α // c x}) → β) : α → option β :=
λ y: α, if h : f.1 y then some (f (subtype.mk y h)) else none


#### Victor Porton (Jul 07 2018 at 21:52):

is this possible?

#### Victor Porton (Jul 07 2018 at 22:11):

This does not compile (types of sides equality in inv1 do not match). How to fix the error?

local attribute [instance] classical.prop_decidable

-- Switch from a function on a subset to a function to option monad
noncomputable def subfunc_to_option {α β: Type} {c: α → Prop} --[decidable_pred c]
(f: {x:α // c x} → β) : α → option β :=
λ y: α, if h : c y then some (f (subtype.mk y h)) else none

-- Switch from function to option monad to a function on a subset
def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // option.is_some (f x)} → β | ⟨x, h⟩ := option.get h

theorem inv1 {α β: Type} {c: α → Prop} (f) : option_to_subfunc (@subfunc_to_option α β c f) = f := sorry


#### Chris Hughes (Jul 07 2018 at 22:12):

I'm not sure what you're trying to do. I don't think the type of f is what you want it to be. You cannot do f.1 because f is not a sigma type.

#### Victor Porton (Jul 07 2018 at 22:14):

@Chris Hughes I tried to eliminate {c: α → Prop} from my definition. I tried it for completeness, but probably the proper way to do it is using an implicit argument (as in your code) instead

#### Victor Porton (Jul 07 2018 at 22:14):

@Chris Hughes Note that the issue in my very last question was different

#### Victor Porton (Jul 07 2018 at 22:19):

Side question: I subscribed to desktop notifications for this chat, but I get no notifications. Will I receive the notifications, if I close the browser window?

#### Chris Hughes (Jul 07 2018 at 22:21):

One way to fix the error is to use == instead of = which allows you to state equality when the types are different (your types are different, but they should be equal). This can be unwieldy however. Another way would be to prove that they are equal when applied to an argument, something like this

theorem inv1 {α β: Type} {c: α → Prop} (f: {x:α // c x} → β) [decidable_pred c] :
∀ y : {x // c x}, option_to_subfunc (@subfunc_to_option α β c _ f) ⟨y.1, sorry⟩ = f y := sorry


#### Victor Porton (Jul 07 2018 at 22:23):

@Chris Hughes "unwieldy"? What is particularly bad with ==? the second way (to write y explicitly) seems even worse for me.

#### Victor Porton (Jul 07 2018 at 22:35):

Can the following be proved?

theorem eq_xxx (t: Type) (a b: t) := (a==b -> a=b)


(that is if values of the same type are == then they are =)

#### Chris Hughes (Jul 07 2018 at 22:55):

eq_of_heq

#### Victor Porton (Jul 07 2018 at 23:00):

hm, it looks now I am really stalled to fill the sorryies in my source:

local attribute [instance] classical.prop_decidable

-- Switch from a function on a subset to a function to option monad
noncomputable def subfunc_to_option {α β: Type} {c: α → Prop} --[decidable_pred c]
(f: {x:α // c x} → β) : α → option β :=
λ y: α, if h : c y then some (f (subtype.mk y h)) else none

-- Switch from function to option monad to a function on a subset
def option_to_subfunc {α β: Type} (f: α → (option β)) :
{x : α // option.is_some (f x)} → β | ⟨x, h⟩ := option.get h

theorem inv1 {α β: Type} {c: α → Prop} (f) : option_to_subfunc (@subfunc_to_option α β c f) == f := sorry

theorem inv2 {α β: Type} {c: α → Prop} (f): subfunc_to_option (@option_to_subfunc β α f) = f := sorry


How to learn to use ==? Maybe I should read Coq docs on this?

#### Mario Carneiro (Jul 07 2018 at 23:01):

To address the larger goal of the definitions you are making, I think you want to use roption (in data.pfun) and the isomorphism theorems between roption and option. A function A -> roption B is the same as a partial function (from a subset of A to B)

#### Victor Porton (Jul 08 2018 at 13:16):

@Mario Carneiro First, how roption would be better for my purposes than option? My project uses classical logic. (However someone suggested me to mark which theorems need axiom of choice explicitly.) Now we have three isomorphic objects (and thus three isomorphisms): a partial function, A->option B and A->roption B. I do not see how it could be better than my initial idea.

#### Mario Carneiro (Jul 08 2018 at 17:01):

Because a function A -> roption B is a "subfunc" as you call it. It is literally a pair of a domain and a partial function on that domain

#### Mario Carneiro (Jul 08 2018 at 17:02):

so you can leverage the proofs of isomorphism there to obtain an isomorphism from A -> option B to a partial function

#### Victor Porton (Jul 08 2018 at 17:05):

@Mario Carneiro Either you don't understand me, or I do not understand you. The "subfunc" by definition is a function on a _subtype_ of A. But A -> roption B is a function on the type A, not on its arbitrary subtype as I want. It may be isomorphic, but they are _not_ the same.

#### Mario Carneiro (Jul 08 2018 at 17:05):

The isomorphism is almost trivial though, unlike the one from option

#### Mario Carneiro (Jul 08 2018 at 17:06):

And furthermore there is already a definition which gives this isomorphism, as_subtype

#### Victor Porton (Jul 08 2018 at 17:15):

@Mario Carneiro Thanks. As there is undocumented things like == which I may need for my Lean-related project, I prefer to lay it aside for an indefinite future. Moreover, I am going to lay aside abstract math research and get busy myself writing a free Python program (for an applied computer science, not abstract mathematics) now

#### Mario Carneiro (Jul 08 2018 at 17:15):

It's not undocumented, but it's a pain to work with

Last updated: May 15 2021 at 22:14 UTC