out_param

Stream: general

[Sebastien Gouezel]

I thought that out_param should have disappeared from modules, but in analysis.normed_space.basic there are the following lines:

class normed_space (α : out_param $ Type*) (β : Type*) [out_param $ normed_field α]
  extends normed_group β, vector_space α β :=

I don't understand them, which is not a big deal, but I wanted to check that they should not be changed.

[Patrick Massot]

I asked the same question last week...

[Sebastien Gouezel]

And what answer did you get?

[Patrick Massot]

none

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/out_param.20again/near/160275177

[Sebastien Gouezel]

Thansk for the pointer. Indeed, this is the very same question!

[Sebastien Gouezel]

I am having problems with out_param in the following situation. Suppose M is a C^1 manifold, with respect to a base field k and a model vector space E. I want to define the tangent space at a point x, by taking equivalence classes of vectors in charts. The maths are not important. The point is that k is relevant (you may want to consider a complex manifold as a real manifold), so just as for linear maps it should be explicit in the definition of the tangent space. However, there will always be one single model space E, so I don't want to have it as an explicit parameter in the definition: it should rather be inferred from the manifold instance in the context. I tried to write this as (with everything in Type to avoid potential universe issues):

def tangent_space_unfolded (k : Type) [nondiscrete_normed_field k] {E : out_param $ Type}
  [out_param $ normed_space k E]
  {M : Type} [topological_space M] [manifold E (times_cont_diff_groupoid 1 k E) M]
  (x : M) : Type :=
  {e : local_homeomorph M E // e ∈ chart (times_cont_diff_groupoid 1 k E) M ∧ x ∈ e.source} × E

(notice the out_param on E and normed_space k E). However, when I try to use this definition, E is not inferred. For instance, with

def tangent_vector_equiv_rel {k : Type} [nondiscrete_normed_field k] {E : Type} [normed_space k E]
  {M : Type} [topological_space M] [manifold E (times_cont_diff_groupoid 1 k E) M]
  (x : M) (p : tangent_space_unfolded k x) : Prop :=
true

I get the red squiggle under p : tangent_space_unfolded k x with the complaint

don't know how to synthesize placeholder
context:
k : Type,
_inst_1 : nondiscrete_normed_field k,
E : Type,
_inst_2 : normed_space k E,
M : Type,
_inst_3 : topological_space M,
_inst_4 : manifold E (times_cont_diff_groupoid 1 k E) M,
x : M
⊢ out_param Type

If I make the parameter E explicit, on the other hand, everything is fine.

There are very few places in the library where out_param is used, so I don't have enough examples (or documentation) to understand what the right syntax should be. Is it impossible to do what I would like?

[Mario Carneiro]

out_param goes on instances and class definitions

[Mario Carneiro]

you can't just put it on a single definition, it's tied in to the whole instance search problem for that typeclass

[Mario Carneiro]

In this case, if you want k to determine E in normed_space, you would need to mark E as out_param in the definition of normed_space. I guess that's not what you want

[Sebastien Gouezel]

I don't want k to determine E, I want the manifold instance together with k to determine E.

[Mario Carneiro]

but the manifold instance already mentions E

[Mario Carneiro]

So you want to trigger the search manifold ?E (times_cont_diff_groupoid 1 k ?E) M?

[Sebastien Gouezel]

Yes. I guess I don't understand at all what out_param does. What I would like to happen when Lean encounters tangent_space k x: it looks in the context for a instance of manifold ?m1 (times_cont_diff_groupoid 1 k ?m1) M, and if it finds one it picks it at E.

[Mario Carneiro]

or is it manifold ?E ?X M

[Mario Carneiro]

what is that second argument?

[Sebastien Gouezel]

It is really manifold ?m1 (times_cont_diff_groupoid 1 k ?m1) M that it should look for.

[Sebastien Gouezel]

It is a groupoid, i.e., a set of local homeomorphisms between M and E.

[Mario Carneiro]

can you make another class?

[Mario Carneiro]

like model_space M ?E or something

[Mario Carneiro]

that implies manifold ?E (times_cont_diff_groupoid 1 k ?E) M

[Mario Carneiro]

I am wary of that typeclass arg. You can probably make lean search for it because lean typeclass search has no hygiene, but that's also why typeclass search is starting to fall over in mathlib

[Sebastien Gouezel]

What I could do is mark E as out_param in the definition of manifold. Except that this is not OK as there can be different model spaces depending on whether one considers a space as a real or complex manifold. So, it would really have to depend on both k and M. I can build a new class smooth_manifold k ?E M with E as an out_param, and see how this goes.

[Sebastien Gouezel]

Being a manifold is definitely a type class, just as good as being a ring or a topological space. The only difference is that it has more structure built in, so it depends on more stuff but that's the way math is.

[Mario Carneiro]

The problem isn't the math, it's the use of (times_cont_diff_groupoid 1 k ?E) as one of the arguments to the class. It's too dependent for my liking (it's not even a type IIUC)

[Sebastien Gouezel]

For each groupoid G, you have a notion of manifold based on this groupoid. For instance, C^infty manifolds, or manifolds with boundary, or manifold with corners, or contact manifolds, or orientable manifolds, or whatever. Each of these structures gives you access to some objects on the manifold. My idea is to set up a set of instances between these structures, so that when you have a contact manifold then you also get automatically a smooth structure, an oriented structure, and so on, just by typeclass inference. I have the impression that this is precisely the kind of things at which typeclass inference is good, but maybe I am missing something.

[Mario Carneiro]

could you put the definition of manifold? I'm confused about the type of everything here

[Sebastien Gouezel]

structure structure_groupoid (α : Type*) [topological_space α] :=
(members      : set (local_homeomorph α α))
(comp         : ∀e e' : local_homeomorph α α, e ∈ members → e' ∈ members → e →ₕ e' ∈ members)
(inv          : ∀e : local_homeomorph α α, e ∈ members → e.symm ∈ members)
(id_mem       : local_homeomorph.refl α ∈ members)
(locality     : ∀e : local_homeomorph α α, (∀x ∈ e.source, ∃s, is_open s ∧
                  x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
(eq_on_source : ∀ e e' : local_homeomorph α α, e ∈ members → e' ≈ e → e' ∈ members)

class manifold {α : Type*} [topological_space α] (G : structure_groupoid α) (β : Type*) [topological_space β] :=
(chart  : set (local_homeomorph β α))
(compat : ∀e e' : local_homeomorph β α, e ∈ chart → e' ∈ chart → e.symm →ₕ e' ∈ G)
(cover  : ∀x, ∃e : local_homeomorph β α, e ∈ chart ∧ x ∈ e.source)

One could also go for a manifold structure just by picking the charts and the cover condition (this would be a has_chart class, say, similar to has_add and friends), and say that the manifold structure is compatible with a given groupoid if the compat condition holds (in the same way as one can add properties extending has_add making it into a group, a ring, a module, and so on).

[Mario Carneiro]

Okay, I see. I guess this definition of manifold differs from the earlier one though, since α is implicit now but the other one had three explicit args

[Mario Carneiro]

The order of inference still seems a bit weird to me. Can't manifolds have multiple model vector spaces? Like a manifold with different dimensions at different points

[Sebastien Gouezel]

Yes, you're right. I had tried to make the argument explicit to see if it made a difference, but it didn't so I came back to my original definition with alpha implicit.

[Mario Carneiro]

It seems pretty natural to me that you should say M is a C^1 R^n manifold, and both R,n,M are required args

[Sebastien Gouezel]

In the most standard definition, the model space is the same everywhere (and so the dimension is the same everywhere). If you really want to have a manifold with different local dimensions with this definition, you can by taking as a model space the union of all R^n over varying n, but this is not very natural.

[Mario Carneiro]

that's not a vector space

[Sebastien Gouezel]

The thing is that the groupoid G already contains the information about alpha.

[Sebastien Gouezel]

The model space does not need to be a vector space (and in many applications it isn't)

[Sebastien Gouezel]

An important example to keep in mind, however, is a complex manifold of dimension n, modelled over C^n, that you also want to think of as a manifold of dimension 2n modelled over R^{2n}. So not everything can be implicit.

[Mario Carneiro]

I think I want this definition to be explicit in all the args k E G M

[Mario Carneiro]

but you should keep things variable when possible. For example tangent_space_unfolded seems to be unnecessarily specializing on the groupoid

[Mario Carneiro]

Even if there is "only one" model space up to isomorphism doesn't mean there's only one up to defeq

[Mario Carneiro]

In particular I'm sure there will be ways to combine stuff in mathlib to get other isomorphic things like (R^2)^n that we also want to talk about

[Sebastien Gouezel]

You want to be able to speak of the tangent space to many manifolds, for instance to C^infty manifolds or to contact manifolds. If there is an instance saying that a C^infty manifold is a C^1 manifold, or that a contact manifold is a C^1 manifold, then you get the tangent space for all of them at once.

[Mario Carneiro]

I mean that you have specialized to C^1 but the definition works in any groupoid, or at least that part of it does

[Mario Carneiro]

Also, given that the C^1 groupoid is data here, I think that those instances you just said are going to cause diamond problems

[Mario Carneiro]

Looking at your definition of manifold, it seems like G isn't actually necessary to define the manifold itself. You can have one manifold structure and assert that it is compatible with a variety of groupoids

[Mario Carneiro]

That also solves the problem of these composite constraints in the typeclass, since you then have [manifold A B] [is_C1_manifold A B] instead of [manifold A (C1_groupoid A) B]

[Mario Carneiro]

where is_C1_manifold is a Prop

[Sebastien Gouezel]

I agree it is a good idea to separate the manifold structure, i.e., the data given by the charts, from the regularity of the charts, i.e., the fact that the charts belong to some groupoid. I'll try this route, thanks!

[Sebastien Gouezel]

In fact, I am not so sure I gain anything with this. The two options are

• Just a typeclass [manifold A G B], which contains data (the charts) and a proposition (the fact that the changes of charts belong to G)
• Two typeclasses, [manifold A B] containing the charts, and [has_smoothness_class A G B] (assuming [manifold A B]), which is only Prop, asserting that the changes of charts belong to G.

Whe one sets up instances, with the second point of view the set of charts is fixed, and one only asserts, say, that if a manifold is C^oo then it is C^1 for the same charts. In the first approach, one would get an instance from [manifold A (C^oo) B] to [manifold A C^1 B], keeping the same charts but asserting that they belong to the larger groupoid C^1. I don't see why the first approach would give rise to diamonds, as the data between the instances does not change, so whatever the path between the instances one should get defeq stuff, right?

[Mario Carneiro]

In the first approach, the manifold itself is different when it is inferred by a different route

[Mario Carneiro]

because the manifold instance depends on G

[Mario Carneiro]

I guess you are saying that the typeclass instance itself might not be defeq but the charts projection is

[Sebastien Gouezel]

I don't get it. The manifold is made of data (the charts) and Props. Whatever way you go, you get the same data (it does not change through the instances), and the props are irrelevant. How could it not be defeq?

[Mario Carneiro]

The manifold lives in a different type

[Mario Carneiro]

manifold A (C1_groupoid A (C1_of_C^oo)) B vs manifold A (C1_groupoid A (C1_of_C^2 (C^2_of_C^oo))) B or something

[Mario Carneiro]

because the dependencies are different, these can't even be propositionally equal

[Sebastien Gouezel]

I still don't get it, sorry, I am a little bit slow. Suppose you have three instances

instance C1_of_C3 [manifold (C^3_groupoid E) M] : manifold (C^1_groupoid E) M
instance C2_of_C3 [manifold (C^3_groupoid E) M] : manifold (C^2_groupoid E) M
instance C1_of_C2 [manifold (C^2_groupoid E) M] : manifold (C^1_groupoid E) M

Then the path C1_of_C3 seems to me to be completely equivalent to the composition of C2_of_C3 and C1_of_C2. And the types do not seem to depend on the chosen path.

[Mario Carneiro]

Actually I think I'm the one that's slow. Feel free to ignore my ramblings, I must be tired. I think you are right. However, this kind of instance search seems like a bad idea - there are lots and lots of values of k in C^k, and I'm sure in the right context you will be able to get some silliness like a search for has_zero nat ending up at manifold (C^57_groupoid R) nat

[Sebastien Gouezel]

I am only planning to register the ones with 0, 1 and infinity. And prove the general statement, but not register it as an instance (if necessary, it can be registered locally).

[Yury G. Kudryashov]

What is the purpose of out_param? It says something about output parameters in typeclasses but in has_insert α γ the first parameter is out_param.

[Yury G. Kudryashov]

I'm trying to turn singleton into a typeclass has_singleton + lawful_singleton.

[Yury G. Kudryashov]

So that we can have {a} = {x | x = a}

[Yury G. Kudryashov]

It seems that Lean interprets {x} as insert x ∅, not as singleton x.

[Johan Commelin]

Yup, there are plans to change this... but I don't think there's a PR yet. I think Mario has a PR related to this to core lean (about how {x,y, ..., z} is defined

[Kenny Lau]

man, a lot of proofs would break (at least those that I write, because I never use simp)

[Yury G. Kudryashov]

I thought that it already calls singleton, and we just have to change def singleton in the library. I was wrong, so let's wait for Mario (I don't want to touch C++ lean code).

[Kenny Lau]

core lean doesn't mean C++ lean code

[Yury G. Kudryashov]

If you use singleton, then you probably use mem_singleton_iff. We'll need to change its proof to iff.rfl, then most proofs should work.

[Yury G. Kudryashov]

Parsing of {x, y, ...} happens in C++.

[Yury G. Kudryashov]

https://github.com/leanprover-community/lean/pull/153/files

[Kenny Lau]

oh, interesting

[Yury G. Kudryashov]

Even more interesting: parsing of {x} calls singleton but pretty printing relies on singleton x = insert x ∅.

[Yury G. Kudryashov]

So if I redefine singleton x, then {x} in the input will parse as singleton x, then printed as singleton x while insert x ∅ will be printed as {x}.

[Yury G. Kudryashov]

@Mario Carneiro @Gabriel Ebner

[Mario Carneiro]

The C++ change is already done and in the PR queue

[Mario Carneiro]

(it's broken because C++11 but that's another matter)

[Mario Carneiro]

the change you are talking about is entirely in lean

[Mario Carneiro]

I don't know whether it should be okay to have insert x emptyget printed as {x} or not. It basically boils down to whether we think we can reliably retain that form for literals

[Yury G. Kudryashov]

It seems that you're changing the parser, not the printer.

[Mario Carneiro]

I would expect things like simp to easily break this (rewriting the inner singleton a to insert a empty in order to have a more uniform layout) and then the printer will give you the messy version

[Mario Carneiro]

The change in the PR is only about parsing

[Mario Carneiro]

Here I'm talking about the printing issue you pointed out

[Yury G. Kudryashov]

The problem is that singleton x is printed as singleton x, not {x}.

[Jasmin Blanchette]

I'm joining the conversation midway, but printing insert x empty as {x} is what Isabelle does. Likewise, insert x (insert y empty) is printed as {x, y}. It works well in practice.

[Mario Carneiro]

and I should revise my earlier statement - if you want to change the printing behavior that's a C++ change

[Mario Carneiro]

@Jasmin Blanchette the issue is the lack of consistency between parser and printer here

[Mario Carneiro]

I would bet the printer is currently "forgiving" and will use the sugared notation for either of insert ... insert singleton and insert ... insert empty

[Mario Carneiro]

but the parser can't be round-tripping in this situation

[Yury G. Kudryashov]

No, I tried to redefine singleton, and the printer is not forgiving.

[Mario Carneiro]

#check (insert 1 (insert 2 (insert 3 ∅)):set ℕ) -- {3, 2, 1} : set ℕ
#check (insert 1 (insert 2 (singleton 3)):set ℕ) -- {3, 2, 1} : set ℕ

[Yury G. Kudryashov]

Did you redefine singleton?

[Mario Carneiro]

no, this is stock lean

[Yury G. Kudryashov]

If you redefine singleton, then it stops working.

[Johan Commelin]

I wouldn't mind if insert x empty doesn't print as {x}. If {x} is meant to be singleton x and that is no longer defeq to insert x empty I think it is actually a feature if the printer doesn't hide that.

[Mario Carneiro]

Here's a MWE subset of core to demonstrate the printing behavior:

prelude
universes u v
class has_emptyc (α : Type u) := (emptyc : α)
@[reducible] def out_param (α : Sort u) : Sort u := α
class has_insert (α : out_param (Type u)) (γ : Type v) := (insert : α → γ → γ)
export has_insert (insert)
notation `∅` := has_emptyc.emptyc _
def singleton {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a : α) : γ :=
has_insert.insert a (has_emptyc.emptyc _)

variables {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a b c : α)
#check (insert a (insert b (insert c ∅)):γ) -- {c, b, a} : γ
#check (insert a (insert b (singleton c)):γ) -- {c, b, a} : γ

[Mario Carneiro]

Changing the definition of singleton doesn't affect parsing or printing:

prelude
universes u v
class has_emptyc (α : Type u) := (emptyc : α)
@[reducible] def out_param (α : Sort u) : Sort u := α
class has_insert (α : out_param (Type u)) (γ : Type v) := (insert : α → γ → γ)
export has_insert (insert)
notation `∅` := has_emptyc.emptyc _
def singleton {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a : α) : γ :=
has_insert.insert a (has_insert.insert a (has_emptyc.emptyc _))

variables {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a b c : α)
#check (insert a (insert b (insert c ∅)):γ) -- {c, b, a} : γ
#check (insert a (insert b (singleton c)):γ) -- {c, b, a} : γ

[Mario Carneiro]

Using a typeclass version breaks it:

class has_singleton (α : out_param (Type u)) (γ : Type v) := (singleton : α → γ)
def singleton {α : Type u} {γ : Type v} [has_singleton α γ] (a : α) : γ :=
has_singleton.singleton _ a

variables {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] [has_singleton α γ] (a b c : α)
#check (insert a (insert b (insert c ∅)):γ) -- {c, b, a} : γ
#check (insert a (insert b (singleton c)):γ) -- insert a (insert b (singleton c)) : γ

but this is clearly because it's counting arguments wrong:

class has_singleton (α : out_param (Type u)) (γ : Type v) := (singleton : α → γ)
def singleton {α : Type u} {γ : Type v} [has_singleton α γ] [has_singleton α γ] (a : α) : γ :=
has_singleton.singleton _ a

variables {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] [has_singleton α γ] (a b c : α)
#check (insert a (insert b (insert c ∅)):γ) -- {c, b, a} : γ
#check (insert a (insert b (singleton c)):γ) -- {c, b, a} : γ

[Mario Carneiro]

it presumably relies on the contents of the singleton to be in argument # 5

[Yury G. Kudryashov]

Thank you! I only tried the typeclass version, and didn't guess that it relies on argument index.

[Yury G. Kudryashov]

Yes, frontends/lean/pp.cpp has is_constant(get_app_fn(e), get_singleton_name()) && get_app_num_args(e) == 5

[Mario Carneiro]

I can't test it because the other bug gets in the way, but I would expect export has_singleton (singleton) to also break printing, since now the name of the singleton constructor is has_singleton.singleton instead of _root_.singleton

[Yury G. Kudryashov]

Thank you for the explanation. I think that now I know how to do it.

[Yury G. Kudryashov]

BTW, why our notation for sUnion doesn't conflict with the one from stdlib?

[Yury G. Kudryashov]

Ignore.

[Mario Carneiro]

heh, problem solved:

@[class] inductive unit | star
attribute [instance] unit.star
def singleton {α : Type u} {γ : Type v} [has_singleton α γ] [unit] (a : α) : γ :=
has_singleton.singleton _ a

variables {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] [has_singleton α γ] (a b c : α)
#check (insert a (insert b (insert c ∅)):γ) -- {c, b, a} : γ
#check (insert a (insert b (singleton c)):γ) -- {c, b, a} : γ

[Johan Commelin]

Isn't it easier to change a 5 into a 4?

[Mario Carneiro]

not from lean

[Johan Commelin]

Sure... but we are changing core Lean anyway

[Mario Carneiro]

I wonder if it is worth making unit a class for implicit dummy args like this

[Mario Carneiro]

more fun with confusing the printer:

@[class] inductive unit | star
attribute [instance] unit.star
def singleton {α : Type u} {γ : Type v} [has_singleton α γ] (a : α) [unit] : γ :=
has_singleton.singleton _ a

variables {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] [has_singleton α γ] (a b c : α)
#check (insert a (insert b (insert c ∅)):γ) -- {c, b, a} : γ
#check (insert a (insert b (singleton c)):γ) -- {(), b, a} : γ

[Mario Carneiro]

also amusing that lean already knows that unit is printed as ()

[Kenny Lau]

so the printer has access to definitions of stuffs?

[Mario Carneiro]

Thinking about this a bit more, I think I want the printer to stay the way it is w.r.t. sugaring both kinds of enumerated set. There are already a ton of places where the printer doesn't round trip, for example when there are non-canonical instances, or when you mix succ and bit0/bit1

#check nat.succ nat.zero -- 1 : ℕ
#check @has_one.one ℕ _ -- 1 : ℕ
#check nat.succ (nat.succ nat.zero) -- 2 : ℕ
#check nat.succ (@has_one.one ℕ _) -- nat.succ 1 : ℕ
#check bit1 (@has_one.one ℕ _) -- 3 : ℕ
#check bit1 (nat.succ nat.zero) -- 3 : ℕ

[Mario Carneiro]

The printer is completely dumbly going over the term thinking it knows what's up, but you can easily mislead it

[Johan Commelin]

@Mario Carneiro But if we implement the changes then singleton x is not defeq to insert x ∅, right? So {x} = {x} is not provable by rfl...

[Mario Carneiro]

did you think we had that property before?

[Yury G. Kudryashov]

Why not?

[Johan Commelin]

Mario Carneiro said:

did you think we had that property before?

Maybe not, but this one is going to trip up a lot of people

[Johan Commelin]

Why can't we just make the printer not do fancy things with insert x ∅? And have a simp-lemma that turns it into singleton x

[Yury G. Kudryashov]

I think that most people won't meet insert x empty

[Johan Commelin]

Hmmm, that's probably right

[Mario Carneiro]

I think it's fine to say "most people won't meet it" but I would prefer for the failure mode to be confusing printing rather than a 10x blowup of the printed term.

[Mario Carneiro]

import algebra.group

example : @has_one.one ℕ _ = @has_one.one (multiplicative ℕ) _ :=
begin
  -- ⊢ 1 = 1
  exact rfl, -- fail
end

[Mario Carneiro]

it's trivially easy to come up with examples along these lines

[Johan Commelin]

Of course

[Mario Carneiro]

the printer should really be viewed as a "best effort" thing

[Mario Carneiro]

at least as long as you aren't using pp.all

[Yury G. Kudryashov]

@Mario Carneiro Do you have a Lean built with your lean#153 applied?

[Mario Carneiro]

no, why?

[Mario Carneiro]

I have a pretty good idea what will happen

[Yury G. Kudryashov]

I wonder how #check ({0, 1} : set nat) will work.

[Mario Carneiro]

it will produce the term insert 0 (singleton 1)

[Yury G. Kudryashov]

And how will it be pretty-printed?

[Yury G. Kudryashov]

{0, 1} or {1, 0}?

[Mario Carneiro]

Actually, I guess I should have fixed the printer too in that PR since the printer will indeed print {1, 0}