functions with finite support

Stream: new members

[Jalex Stark]

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]

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

[Kenny Lau]

data.finsupp

[Chris Hughes]

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]

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]

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]

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

[Jalex Stark]

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]

Are you doing it only for countable orders then?

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Jalex Stark]

yeah I agree

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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]

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]

that is, the safely_apply function is called get

[Jalex Stark]

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]

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

[Mario Carneiro]

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]

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

[Jalex Stark]

Thank you!

[Mario Carneiro]

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

[Jalex Stark]

dot notation is great

[Jalex Stark]

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]

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]

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]

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

[Mario Carneiro]

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

[Jalex Stark]

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

[Mario Carneiro]

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]

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?

[Mario Carneiro]

#mwe

[Jalex Stark]

fixed, thanks

[Mario Carneiro]

what is (set.finite dom f) doing?

[Mario Carneiro]

That looks like a malformed binder

[Mario Carneiro]

in any case set.finite isn't imported

[Mario Carneiro]

and dom doesn't exist either

[Jalex Stark]

added an import for set.

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

[Reid Barton]

I think more newlines might help.

[Jalex Stark]

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

[Jalex Stark]

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]

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]

put fields one per line, and skip mk ::

[Jalex Stark]

okay, thanks. Is there a style guide somewhere?

[Mario Carneiro]

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]

mk :: is unnecessary since mk is the default

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jalex Stark]

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]

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

[Jalex Stark]

hmm okay

[Mario Carneiro]

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]

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]

anyway, I missed what the question is

[Mario Carneiro]

the code you sent seems to work

[Jalex Stark]

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]

$\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]

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