# Zulip Chat Archive

## Stream: general

### Topic: out_param

#### Sebastien Gouezel (Mar 17 2019 at 11:05):

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 (Mar 17 2019 at 11:05):

I asked the same question last week...

#### Sebastien Gouezel (Mar 17 2019 at 11:05):

And what answer did you get?

#### Patrick Massot (Mar 17 2019 at 11:07):

none

#### Kevin Buzzard (Mar 17 2019 at 11:34):

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

#### Sebastien Gouezel (Mar 17 2019 at 11:40):

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

#### Sebastien Gouezel (May 05 2019 at 09:48):

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 (May 05 2019 at 10:01):

out_param goes on instances and class definitions

#### Mario Carneiro (May 05 2019 at 10:02):

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 (May 05 2019 at 10:04):

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 (May 05 2019 at 10:04):

I don't want `k`

to determine `E`

, I want the manifold instance together with `k`

to determine `E`

.

#### Mario Carneiro (May 05 2019 at 10:05):

but the manifold instance already mentions E

#### Mario Carneiro (May 05 2019 at 10:06):

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

?

#### Sebastien Gouezel (May 05 2019 at 10:06):

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 (May 05 2019 at 10:07):

or is it `manifold ?E ?X M`

#### Mario Carneiro (May 05 2019 at 10:08):

what is that second argument?

#### Sebastien Gouezel (May 05 2019 at 10:08):

It is really `manifold ?m1 (times_cont_diff_groupoid 1 k ?m1) M`

that it should look for.

#### Sebastien Gouezel (May 05 2019 at 10:08):

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

and `E`

.

#### Mario Carneiro (May 05 2019 at 10:10):

can you make another class?

#### Mario Carneiro (May 05 2019 at 10:10):

like `model_space M ?E`

or something

#### Mario Carneiro (May 05 2019 at 10:10):

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

#### Mario Carneiro (May 05 2019 at 10:13):

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 (May 05 2019 at 10:13):

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 (May 05 2019 at 10:15):

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 (May 05 2019 at 10:28):

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 (May 05 2019 at 10:36):

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 (May 05 2019 at 10:43):

could you put the definition of `manifold`

? I'm confused about the type of everything here

#### Sebastien Gouezel (May 05 2019 at 11:24):

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 (May 05 2019 at 13:00):

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 (May 05 2019 at 13:02):

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 (May 05 2019 at 13:02):

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 (May 05 2019 at 13:04):

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 (May 05 2019 at 13:04):

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 (May 05 2019 at 13:04):

that's not a vector space

#### Sebastien Gouezel (May 05 2019 at 13:04):

The thing is that the groupoid `G`

already contains the information about alpha.

#### Sebastien Gouezel (May 05 2019 at 13:05):

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

#### Sebastien Gouezel (May 05 2019 at 13:12):

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 (May 05 2019 at 13:13):

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

#### Mario Carneiro (May 05 2019 at 13:14):

but you should keep things variable when possible. For example `tangent_space_unfolded`

seems to be unnecessarily specializing on the groupoid

#### Mario Carneiro (May 05 2019 at 13:18):

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

#### Mario Carneiro (May 05 2019 at 13:19):

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 (May 05 2019 at 13:57):

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 (May 05 2019 at 14:59):

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 (May 05 2019 at 15:01):

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 (May 05 2019 at 15:04):

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 (May 05 2019 at 15:06):

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 (May 05 2019 at 15:07):

where `is_C1_manifold`

is a Prop

#### Sebastien Gouezel (May 05 2019 at 15:11):

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 (May 05 2019 at 15:34):

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 (May 05 2019 at 16:20):

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

#### Mario Carneiro (May 05 2019 at 16:20):

because the manifold instance depends on G

#### Mario Carneiro (May 05 2019 at 16:22):

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

projection is

#### Sebastien Gouezel (May 05 2019 at 16:22):

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 (May 05 2019 at 16:23):

The manifold lives in a different type

#### Mario Carneiro (May 05 2019 at 16:24):

`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 (May 05 2019 at 16:25):

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

#### Sebastien Gouezel (May 05 2019 at 17:03):

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 (May 05 2019 at 17:17):

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 (May 05 2019 at 17:29):

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 (Apr 08 2020 at 07:05):

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 (Apr 08 2020 at 07:06):

I'm trying to turn `singleton`

into a typeclass `has_singleton`

+ `lawful_singleton`

.

#### Yury G. Kudryashov (Apr 08 2020 at 07:06):

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

#### Yury G. Kudryashov (Apr 08 2020 at 07:15):

It seems that Lean interprets `{x}`

as `insert x ∅`

, not as `singleton x`

.

#### Johan Commelin (Apr 08 2020 at 07:19):

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 (Apr 08 2020 at 07:20):

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

)

#### Yury G. Kudryashov (Apr 08 2020 at 07:21):

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 (Apr 08 2020 at 07:22):

core lean doesn't mean C++ lean code

#### Yury G. Kudryashov (Apr 08 2020 at 07:22):

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 (Apr 08 2020 at 07:22):

Parsing of `{x, y, ...}`

happens in C++.

#### Yury G. Kudryashov (Apr 08 2020 at 07:23):

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

#### Kenny Lau (Apr 08 2020 at 07:23):

oh, interesting

#### Yury G. Kudryashov (Apr 08 2020 at 07:28):

Even more interesting: *parsing* of `{x}`

calls `singleton`

but *pretty printing* relies on `singleton x = insert x ∅`

.

#### Yury G. Kudryashov (Apr 08 2020 at 07:30):

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 (Apr 08 2020 at 07:30):

@Mario Carneiro @Gabriel Ebner

#### Mario Carneiro (Apr 08 2020 at 07:31):

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

#### Mario Carneiro (Apr 08 2020 at 07:31):

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

#### Mario Carneiro (Apr 08 2020 at 07:32):

the change you are talking about is entirely in lean

#### Mario Carneiro (Apr 08 2020 at 07:34):

I don't know whether it should be okay to have `insert x empty`

get printed as `{x}`

or not. It basically boils down to whether we think we can reliably retain that form for literals

#### Yury G. Kudryashov (Apr 08 2020 at 07:34):

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

#### Mario Carneiro (Apr 08 2020 at 07:34):

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 (Apr 08 2020 at 07:35):

The change in the PR is only about parsing

#### Mario Carneiro (Apr 08 2020 at 07:35):

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

#### Yury G. Kudryashov (Apr 08 2020 at 07:36):

The problem is that `singleton x`

is printed as `singleton x`

, not `{x}`

.

#### Jasmin Blanchette (Apr 08 2020 at 07:36):

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 (Apr 08 2020 at 07:36):

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

#### Mario Carneiro (Apr 08 2020 at 07:36):

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

#### Mario Carneiro (Apr 08 2020 at 07:37):

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 (Apr 08 2020 at 07:37):

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

#### Yury G. Kudryashov (Apr 08 2020 at 07:38):

No, I tried to redefine `singleton`

, and the printer is not forgiving.

#### Mario Carneiro (Apr 08 2020 at 07:39):

#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 (Apr 08 2020 at 07:39):

Did you redefine `singleton`

?

#### Mario Carneiro (Apr 08 2020 at 07:39):

no, this is stock lean

#### Yury G. Kudryashov (Apr 08 2020 at 07:40):

If you redefine `singleton`

, then it stops working.

#### Johan Commelin (Apr 08 2020 at 07:44):

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 (Apr 08 2020 at 07:44):

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 (Apr 08 2020 at 07:45):

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 (Apr 08 2020 at 07:49):

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 (Apr 08 2020 at 07:50):

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

#### Yury G. Kudryashov (Apr 08 2020 at 07:51):

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

#### Yury G. Kudryashov (Apr 08 2020 at 07:52):

Yes, `frontends/lean/pp.cpp`

has `is_constant(get_app_fn(e), get_singleton_name()) && get_app_num_args(e) == 5`

#### Mario Carneiro (Apr 08 2020 at 07:53):

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 (Apr 08 2020 at 07:55):

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

#### Yury G. Kudryashov (Apr 08 2020 at 07:55):

BTW, why our notation for `sUnion`

doesn't conflict with the one from stdlib?

#### Yury G. Kudryashov (Apr 08 2020 at 07:56):

Ignore.

#### Mario Carneiro (Apr 08 2020 at 08:00):

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 (Apr 08 2020 at 08:01):

Isn't it easier to change a `5`

into a `4`

?

#### Mario Carneiro (Apr 08 2020 at 08:01):

not from lean

#### Johan Commelin (Apr 08 2020 at 08:01):

Sure... but we are changing core Lean anyway

#### Mario Carneiro (Apr 08 2020 at 08:01):

I wonder if it is worth making `unit`

a class for implicit dummy args like this

#### Mario Carneiro (Apr 08 2020 at 08:06):

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 (Apr 08 2020 at 08:06):

also amusing that lean already knows that `unit`

is printed as `()`

#### Kenny Lau (Apr 08 2020 at 08:10):

so the printer has access to definitions of stuffs?

#### Mario Carneiro (Apr 08 2020 at 08:12):

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 (Apr 08 2020 at 08:13):

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

#### Johan Commelin (Apr 08 2020 at 08:13):

@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 (Apr 08 2020 at 08:14):

did you think we had that property before?

#### Yury G. Kudryashov (Apr 08 2020 at 08:14):

Why not?

#### Johan Commelin (Apr 08 2020 at 08:15):

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 (Apr 08 2020 at 08:15):

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 (Apr 08 2020 at 08:15):

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

#### Johan Commelin (Apr 08 2020 at 08:16):

Hmmm, that's probably right

#### Mario Carneiro (Apr 08 2020 at 08:18):

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 (Apr 08 2020 at 08:19):

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

#### Mario Carneiro (Apr 08 2020 at 08:19):

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

#### Johan Commelin (Apr 08 2020 at 08:19):

Of course

#### Mario Carneiro (Apr 08 2020 at 08:20):

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

#### Mario Carneiro (Apr 08 2020 at 08:20):

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

#### Yury G. Kudryashov (Apr 08 2020 at 08:20):

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

#### Mario Carneiro (Apr 08 2020 at 08:21):

no, why?

#### Mario Carneiro (Apr 08 2020 at 08:21):

I have a pretty good idea what will happen

#### Yury G. Kudryashov (Apr 08 2020 at 08:22):

I wonder how `#check ({0, 1} : set nat)`

will work.

#### Mario Carneiro (Apr 08 2020 at 08:22):

it will produce the term `insert 0 (singleton 1)`

#### Yury G. Kudryashov (Apr 08 2020 at 08:22):

And how will it be pretty-printed?

#### Yury G. Kudryashov (Apr 08 2020 at 08:23):

`{0, 1}`

or `{1, 0}`

?

#### Mario Carneiro (Apr 08 2020 at 08:23):

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

Last updated: May 13 2021 at 18:26 UTC