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?

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

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 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 (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?

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?

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 ()

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?

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

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?

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