## Stream: new members

### Topic: functions with finite support

#### Jalex Stark (Apr 30 2020 at 21:58):

I want to talk about an object which in my head has either type f : M →. N  with A : finset M and support f = a (I don't actually know what I mean by support) or else has type f : A → N the latter doesn't work because A is not a type. I thought about trying to make A a subtype of M with an insteance fintype A, but I want to have m : M and reason about m ∈ A : Prop. Any advice? "Go read all of this particular file and you'll figure it out" would be fine.

#### Jalex Stark (Apr 30 2020 at 22:03):

Maybe the answer is "read fintype.basic", since fintype.of_finset looks like a good place for me to start.

#### Kenny Lau (Apr 30 2020 at 22:14):

data.finsupp

#### Chris Hughes (Apr 30 2020 at 22:17):

I don't think finsupp is really the right thing. finsupp is basically just free module, or direct sum, and requires M to have a zero.

#### Chris Hughes (Apr 30 2020 at 22:19):

I also don't think there are any examples of this really in mathlib, other than by making A the domain of the function. There is data.pfun for partial functions, but the best approach probably depends on what you want to do with it.

#### Jalex Stark (Apr 30 2020 at 22:23):

the big goal is to prove categoricity of dense linear orders without endpoints. (this was the nuke that came to mind for one of Kenny's kata, and it seemed like a good exercise regardless of whether it was appropriate)
the small goal is to talk about extending a finitely supported function by one point

#### Jalex Stark (Apr 30 2020 at 22:25):

is pfun supposed to be finsupp but replacing 0 with none?

#### Jalex Stark (Apr 30 2020 at 22:26):

that seems like a step in the right direction, I was about to enrich my target type with a "zero" by wrapping it in option and setting 0 = none

#### Reid Barton (Apr 30 2020 at 22:28):

Are you doing it only for countable orders then?

#### Reid Barton (Apr 30 2020 at 22:29):

"Finite" is not really the condition you need, right?

#### Reid Barton (Apr 30 2020 at 22:30):

Like, it's automatically finite because you've only picked finitely many things so far. So you don't also need to remember it's a finset.

#### Jalex Stark (Apr 30 2020 at 22:35):

yeah i just want to do it for countable orders (which should be like 80% of the work of doing it for orders in bijection with an arbitrary ordinal)

#### Jalex Stark (Apr 30 2020 at 22:35):

my plan was to do a mutual induction on two maps forth : M \to N and back : N \to M

#### Reid Barton (Apr 30 2020 at 22:37):

I think you will find this tricky, and I'm curious to see what you come up with

yeah I agree

#### Jalex Stark (Apr 30 2020 at 22:37):

(my hope is that it ends up being a decent kata)

#### Jalex Stark (Apr 30 2020 at 22:46):

i guess it's time to see if I know how the option monad works...

#### Jalex Stark (Apr 30 2020 at 23:07):

okay, I think this is the API that I want into roption (as in, I think after I know this I don't have to think about the guts of roption)

import data.pfun
open pfun

variables {M N : Type u}
structure safely_applied
{f : M →. N} {a : M} (ha : a ∈ dom f)
:= mk :: (val : N) (h_val : f a = roption.some val)

def safely_apply
(f : M →. N) {a : M}(ha : a ∈ dom f)
: safely_applied ha
:= sorry


edit: now it's an MWE instead of an ME

#### Mario Carneiro (May 01 2020 at 00:56):

I don't get this api at all. The structure safely_applied is useless, you may as well have {val // f a = roption.some val} as the target type of safely_apply, which is more conventionally written {val // val \in f a}, and the proof is <(f a).get ha, (f a).get_mem ha>

#### Mario Carneiro (May 01 2020 at 00:57):

that is, the safely_apply function is called get

#### Jalex Stark (May 01 2020 at 02:12):

hmm now I realize I don't know how to do what I want with either safely_apply or get. How would you fix this?

variables {M N : Type u}
def partial_embedding (f : M →. N) {a b : M} (ha : a ∈ dom f) (hb : b ∈ dom f) : Prop
:= ( a ≤ b ↔ f a ≤ f b )


#### Jalex Stark (May 01 2020 at 02:13):

where the problem is that i've asked about the order between two terms of type roption N instead of N

#### Mario Carneiro (May 01 2020 at 02:15):

variables {M N : Type u}
def partial_embedding (f : M →. N) {a b : M} (ha : a ∈ dom f) (hb : b ∈ dom f) : Prop
:= ( a ≤ b ↔ (f a).get ha ≤ (f b).get hb )


#### Jalex Stark (May 01 2020 at 02:15):

I wanted to replace f a with something like get (f a) ha or (safely_apply f a).val, but I didn't seem to understand the error messages when I tried using each of those

Thank you!

#### Mario Carneiro (May 01 2020 at 02:16):

If you don't use dot notation you have to write roption.get (f a) ha or open roption

#### Jalex Stark (May 01 2020 at 02:16):

dot notation is great

#### Jalex Stark (May 01 2020 at 02:19):

I'll have to study the definition of roption.get to figure out why my attempt to call .val on my structure failed

#### Jalex Stark (May 02 2020 at 02:43):

Okay I think I'm still missing something fundamental. I want to define a term def partial_embedding (f : M →. N) : Prop  which morally means "whenever f a and f b are defined, we have a \le b \iff f a \le f b"

#### Jalex Stark (May 02 2020 at 02:43):

This is what I came up with, and I think it is bad in a way that means I'm missing something fundamental

import data.pfun
open pfun

variables {M N : Type u} [DLO M] [DLO N]

def partial_embedding_at_points (f : M →. N) {a b : M} (ha : a ∈ dom f) (hb : b ∈ dom f) : Prop
:= ( a ≤ b ↔ (f a).get ha ≤ (f b).get hb )

def partial_embedding_aux (f : M →. N) (a b : M) : Prop :=
begin
by_cases a ∈ dom f,
swap, exact true, rename h ha,
by_cases b ∈ dom f,
swap, exact true, rename h hb,
exact partial_embedding_at_points f ha hb,
end

def partial_embedding (f : M →. N) : Prop := ∀ a b : M, partial_embedding_aux f a b


#### Jalex Stark (May 02 2020 at 02:43):

(oof I did not mean to have "press enter to send" checked)

#### Mario Carneiro (May 02 2020 at 02:46):

def partial_embedding (f : M →. N) : Prop :=
∀ a b ha hb, @partial_embedding_at_points _ _ _ _ f a b ha hb


#### Jalex Stark (May 02 2020 at 02:47):

oh i didn't know you could leave the type unspecified in a quantifier. that's great!

#### Mario Carneiro (May 02 2020 at 02:48):

import data.pfun
open pfun

universe u
variables {M N : Type u} [preorder M] [preorder N]

def partial_embedding (f : M →. N) : Prop :=
∀ a b ha hb, a ≤ b ↔ (f a).get ha ≤ (f b).get hb


#### Jalex Stark (May 02 2020 at 02:54):

The next broken bit is this:

structure embedding_extension (f : M →. N) (hf : partial_embedding f) (x : M) := mk :: (F : M →. N) (embedding : partial_embedding F) (extension : dom f ≤ dom F) (supports_x : x ∈ dom F)

def finite_embedding_extension (f : M →. N) (hf : partial_embedding f) (x : M) (set.finite dom f) : embedding_extension f hf x := sorry


The problem is that the type signature of the second term doesn't compile. The error message looks to me like it says it doesn't know partial_embedding f = partial_embedding f

type mismatch at application
embedding_extension f hf
term
hf
has type
@partial_embedding M N _inst_1 _inst_2 f
but is expected to have type
@partial_embedding ?m_1 ?m_2 ?m_3 ?m_4 f


or maybe like it's upset that it got concrete variables when it expected metavariables?

#mwe

fixed, thanks

#### Mario Carneiro (May 02 2020 at 03:08):

what is (set.finite dom f) doing?

#### Mario Carneiro (May 02 2020 at 03:09):

That looks like a malformed binder

#### Mario Carneiro (May 02 2020 at 03:09):

in any case set.finite isn't imported

#### Mario Carneiro (May 02 2020 at 03:09):

and dom doesn't exist either

#### Jalex Stark (May 02 2020 at 03:13):

added an import for set.

#check dom works for me? it's pfun.dom which comes from import data.pfun

#### Reid Barton (May 02 2020 at 03:14):

I think more newlines might help.

#### Jalex Stark (May 02 2020 at 03:14):

ah, the malformed binder is why I couldn't tell that set.finite was missing

#### Jalex Stark (May 02 2020 at 03:16):

Okay, this works now. I guess I will try to recognize malformed binders in the future.

import data.pfun
import data.set
open pfun

universe u
variables {M N : Type u} [preorder M] [preorder N]

def partial_embedding (f : M →. N) : Prop :=
∀ a b ha hb, a ≤ b ↔ (f a).get ha ≤ (f b).get hb

structure embedding_extension (f : M →. N) (hf : partial_embedding f) (x : M) := mk :: (F : M →. N) (embedding : partial_embedding F) (extension : dom f ≤ dom F) (supports_x : x ∈ dom F)
#check dom

def finite_embedding_extension (f : M →. N) (hf : partial_embedding f) (x : M) (h : set.finite (dom f) ) : embedding_extension f hf x := sorry


#### Mario Carneiro (May 02 2020 at 03:18):

structure embedding_extension (f : M →. N) (hf : partial_embedding f) (x : M) :=
(F : M →. N)
(embedding : partial_embedding F)
(extension : dom f ≤ dom F)
(supports_x : x ∈ dom F)


#### Mario Carneiro (May 02 2020 at 03:18):

put fields one per line, and skip mk ::

#### Jalex Stark (May 02 2020 at 03:19):

okay, thanks. Is there a style guide somewhere?

#### Mario Carneiro (May 02 2020 at 03:20):

https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/style.md but I wouldn't be surprised if it's missing something

#### Mario Carneiro (May 02 2020 at 03:20):

mk :: is unnecessary since mk is the default

#### Mario Carneiro (May 02 2020 at 03:20):

Mostly, look at mathlib sources to get a feel for the style

#### Mario Carneiro (May 02 2020 at 03:21):

also be kind to people who have 80-100 character wide screens

#### Jalex Stark (May 02 2020 at 03:21):

Mario Carneiro said:

mk :: is unnecessary since mk is the default

I have no idea what that means, I just copied structure  blocks from other places enough times for me to memorize that mk :: is a thing to type

#### Mario Carneiro (May 02 2020 at 03:22):

the name :: at the beginning of a structure is a (rarely used) feature to allow you to change the name of the single constructor for the structure

hmm okay

#### Mario Carneiro (May 02 2020 at 03:22):

the default is mk and most structures go with that, but sometimes you might want a custom constructor with that name so you will see mk' :: sometimes

#### Mario Carneiro (May 02 2020 at 03:23):

it's because a structure is sugar for an inductive type like this:

inductive embedding_extension (f : M →. N) (hf : partial_embedding f) (x : M)
| mk : ∀
(F : M →. N)
(embedding : partial_embedding F)
(extension : dom f ≤ dom F)
(supports_x : x ∈ dom F),
embedding_extension


#### Mario Carneiro (May 02 2020 at 03:24):

anyway, I missed what the question is

#### Mario Carneiro (May 02 2020 at 03:25):

the code you sent seems to work

#### Jalex Stark (May 02 2020 at 03:27):

Yeah, I agree, I was just trying to express that I incorporated the solution. I prefaced it with "this works now". Sorry for causing extra copy-paste-compiles.

#### David Wärn (May 02 2020 at 07:59):

$\kappa$-categoricity is false for uncountable $\kappa$, right? Consider something like "rationals union negative reals" vs "rationals union positive reals". The interesting thing is that you get completeness from just $\omega$-categoricity.

Anyway, this is definitely a nice exercise! :-)

#### Reid Barton (May 02 2020 at 11:06):

Oh, nice example, thanks. I must have been mixing up this with something else then.

Last updated: May 10 2021 at 00:31 UTC