Zulip Chat Archive

Stream: new members

Topic: functions with finite support


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

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

view this post on Zulip Kenny Lau (Apr 30 2020 at 22:14):

data.finsupp

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

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

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

view this post on Zulip Jalex Stark (Apr 30 2020 at 22:25):

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

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

view this post on Zulip Reid Barton (Apr 30 2020 at 22:28):

Are you doing it only for countable orders then?

view this post on Zulip Reid Barton (Apr 30 2020 at 22:29):

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

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

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

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

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

view this post on Zulip Jalex Stark (Apr 30 2020 at 22:37):

yeah I agree

view this post on Zulip Jalex Stark (Apr 30 2020 at 22:37):

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

view this post on Zulip Jalex Stark (Apr 30 2020 at 22:46):

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

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

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

view this post on Zulip Mario Carneiro (May 01 2020 at 00:57):

that is, the safely_apply function is called get

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

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

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

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

view this post on Zulip Jalex Stark (May 01 2020 at 02:15):

Thank you!

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

view this post on Zulip Jalex Stark (May 01 2020 at 02:16):

dot notation is great

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

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

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

view this post on Zulip Jalex Stark (May 02 2020 at 02:43):

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

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

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

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

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

view this post on Zulip Mario Carneiro (May 02 2020 at 03:05):

#mwe

view this post on Zulip Jalex Stark (May 02 2020 at 03:08):

fixed, thanks

view this post on Zulip Mario Carneiro (May 02 2020 at 03:08):

what is (set.finite dom f) doing?

view this post on Zulip Mario Carneiro (May 02 2020 at 03:09):

That looks like a malformed binder

view this post on Zulip Mario Carneiro (May 02 2020 at 03:09):

in any case set.finite isn't imported

view this post on Zulip Mario Carneiro (May 02 2020 at 03:09):

and dom doesn't exist either

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

view this post on Zulip Reid Barton (May 02 2020 at 03:14):

I think more newlines might help.

view this post on Zulip Jalex Stark (May 02 2020 at 03:14):

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

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

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

view this post on Zulip Mario Carneiro (May 02 2020 at 03:18):

put fields one per line, and skip mk ::

view this post on Zulip Jalex Stark (May 02 2020 at 03:19):

okay, thanks. Is there a style guide somewhere?

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

view this post on Zulip Mario Carneiro (May 02 2020 at 03:20):

mk :: is unnecessary since mk is the default

view this post on Zulip Mario Carneiro (May 02 2020 at 03:20):

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

view this post on Zulip Mario Carneiro (May 02 2020 at 03:21):

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

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

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

view this post on Zulip Jalex Stark (May 02 2020 at 03:22):

hmm okay

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

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

view this post on Zulip Mario Carneiro (May 02 2020 at 03:24):

anyway, I missed what the question is

view this post on Zulip Mario Carneiro (May 02 2020 at 03:25):

the code you sent seems to work

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

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

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