partial functions

Stream: general

[Victor Porton]

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]

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

[Victor Porton]

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

[Chris Hughes]

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]

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

[Victor Porton]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Chris Hughes]

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]

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]

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]

@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]

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]

@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]

It does make sense because there's a coercion

[Victor Porton]

Yes, I knew that here there is a coercion

[Kevin Buzzard]

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

[Kevin Buzzard]

:-)

[Chris Hughes]

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]

@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]

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

[Chris Hughes]

It's the same as from

[Victor Porton]

I am trying to read your code

[Victor Porton]

Sorry, what is λ hfy, y?

[Chris Hughes]

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]

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

[Chris Hughes]

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]

what is (hfy rfl).elim?

[Chris Hughes]

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

[Chris Hughes]

hfy rfl is a proof of false

[Chris Hughes]

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

[Victor Porton]

I need to time to review all you wrote

[Chris Hughes]

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

[Victor Porton]

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

[Victor Porton]

err.. wrong

[Chris Hughes]

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]

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]

What field of maths is your book on?

[Chris Hughes]

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]

@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]

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]

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

[Victor Porton]

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

[Victor Porton]

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

[Chris Hughes]

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]

I think that might be more confusing though.

[Victor Porton]

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]

oh, it seems I got the idea

[Victor Porton]

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]

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

[Victor Porton]

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

[Victor Porton]

Now I "almost" understand. Thanks

[Chris Hughes]

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

[Chris Hughes]

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]

@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]

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

[Chris Hughes]

Another way of writing y.2

[Victor Porton]

Why do you think the the second way is better?

[Chris Hughes]

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]

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]

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]

What about

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

[Chris Hughes]

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

[Patrick Massot]

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

[Patrick Massot]

I don't know if it already exists

[Chris Hughes]

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

[Patrick Massot]

Oh, you mean is_some already existed.

[Patrick Massot]

I thought you were referring to option_to_subfunc

[Chris Hughes]

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]

@Patrick Massot What is this |?

[Victor Porton]

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

[Victor Porton]

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

[Victor Porton]

got: inductive option

[Victor Porton]

@Patrick Massot Where is option.get defined?

[Victor Porton]

found: basic.lean

[Victor Porton]

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]

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]

How having a function f determine its domain?

[Kenny Lau]

it's in the type of the function

[Victor Porton]

@Kenny Lau So use match?

[Victor Porton]

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

[Kenny Lau]

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

[Victor Porton]

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]

is this possible?

[Victor Porton]

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]

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]

@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]

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

[Victor Porton]

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]

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]

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

[Victor Porton]

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]

eq_of_heq

[Mario Carneiro]

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

[Victor Porton]

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]

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]

@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]

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]

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

[Victor Porton]

@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]

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

[Mario Carneiro]

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

[Victor Porton]

@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]

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