Zulip Chat Archive

Stream: general

Topic: partial functions


view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 07 2018 at 15:43):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Jul 07 2018 at 15:55):

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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jul 07 2018 at 15:57):

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

view this post on Zulip Chris Hughes (Jul 07 2018 at 15:59):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Chris Hughes (Jul 07 2018 at 16:17):

It does make sense because there's a coercion

view this post on Zulip Victor Porton (Jul 07 2018 at 16:17):

Yes, I knew that here there is a coercion

view this post on Zulip Kevin Buzzard (Jul 07 2018 at 16:17):

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

view this post on Zulip Kevin Buzzard (Jul 07 2018 at 16:17):

:-)

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip Victor Porton (Jul 07 2018 at 16:26):

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

view this post on Zulip Chris Hughes (Jul 07 2018 at 16:27):

It's the same as from

view this post on Zulip Victor Porton (Jul 07 2018 at 16:27):

I am trying to read your code

view this post on Zulip Victor Porton (Jul 07 2018 at 16:29):

Sorry, what is λ hfy, y?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Victor Porton (Jul 07 2018 at 16:33):

what is (hfy rfl).elim?

view this post on Zulip 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 → β

view this post on Zulip Chris Hughes (Jul 07 2018 at 16:34):

hfy rfl is a proof of false

view this post on Zulip Chris Hughes (Jul 07 2018 at 16:34):

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

view this post on Zulip Victor Porton (Jul 07 2018 at 16:35):

I need to time to review all you wrote

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Victor Porton (Jul 07 2018 at 16:39):

err.. wrong

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Jul 07 2018 at 16:47):

What field of maths is your book on?

view this post on Zulip 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

view this post on Zulip 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$.

view this post on Zulip 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.

view this post on Zulip Victor Porton (Jul 07 2018 at 16:50):

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

view this post on Zulip 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

view this post on Zulip Victor Porton (Jul 07 2018 at 16:54):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Jul 07 2018 at 17:03):

I think that might be more confusing though.

view this post on Zulip 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?

view this post on Zulip Victor Porton (Jul 07 2018 at 17:06):

oh, it seems I got the idea

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Jul 07 2018 at 17:16):

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

view this post on Zulip 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

view this post on Zulip Victor Porton (Jul 07 2018 at 17:18):

Now I "almost" understand. Thanks

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Victor Porton (Jul 07 2018 at 17:24):

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

view this post on Zulip Chris Hughes (Jul 07 2018 at 17:25):

Another way of writing y.2

view this post on Zulip Victor Porton (Jul 07 2018 at 17:26):

Why do you think the the second way is better?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Jul 07 2018 at 18:26):

What about

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

view this post on Zulip Chris Hughes (Jul 07 2018 at 18:27):

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

view this post on Zulip Patrick Massot (Jul 07 2018 at 18:27):

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

view this post on Zulip Patrick Massot (Jul 07 2018 at 18:28):

I don't know if it already exists

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 07 2018 at 18:30):

Oh, you mean is_some already existed.

view this post on Zulip Patrick Massot (Jul 07 2018 at 18:31):

I thought you were referring to option_to_subfunc

view this post on Zulip 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

view this post on Zulip Victor Porton (Jul 07 2018 at 20:02):

@Patrick Massot What is this |?

view this post on Zulip Victor Porton (Jul 07 2018 at 20:03):

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

view this post on Zulip Victor Porton (Jul 07 2018 at 20:12):

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

view this post on Zulip Victor Porton (Jul 07 2018 at 20:12):

got: inductive option

view this post on Zulip Victor Porton (Jul 07 2018 at 20:14):

@Patrick Massot Where is option.get defined?

view this post on Zulip Victor Porton (Jul 07 2018 at 20:15):

found: basic.lean

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Victor Porton (Jul 07 2018 at 21:46):

How having a function f determine its domain?

view this post on Zulip Kenny Lau (Jul 07 2018 at 21:46):

it's in the type of the function

view this post on Zulip Victor Porton (Jul 07 2018 at 21:47):

@Kenny Lau So use match?

view this post on Zulip Victor Porton (Jul 07 2018 at 21:47):

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

view this post on Zulip Kenny Lau (Jul 07 2018 at 21:48):

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

view this post on Zulip 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

view this post on Zulip Victor Porton (Jul 07 2018 at 21:52):

is this possible?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Victor Porton (Jul 07 2018 at 22:14):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 =)

view this post on Zulip Chris Hughes (Jul 07 2018 at 22:55):

eq_of_heq

view this post on Zulip Mario Carneiro (Jul 07 2018 at 22:58):

@Victor Porton You should receive notifications if you are directly addressed, like this

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 08 2018 at 17:05):

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

view this post on Zulip Mario Carneiro (Jul 08 2018 at 17:06):

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

view this post on Zulip 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

view this post on Zulip 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