Zulip Chat Archive

Stream: general

Topic: out_param


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

view this post on Zulip Patrick Massot (Mar 17 2019 at 11:05):

I asked the same question last week...

view this post on Zulip Sebastien Gouezel (Mar 17 2019 at 11:05):

And what answer did you get?

view this post on Zulip Patrick Massot (Mar 17 2019 at 11:07):

none

view this post on Zulip Kevin Buzzard (Mar 17 2019 at 11:34):

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

view this post on Zulip Sebastien Gouezel (Mar 17 2019 at 11:40):

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

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

view this post on Zulip Mario Carneiro (May 05 2019 at 10:01):

out_param goes on instances and class definitions

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

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

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

view this post on Zulip Mario Carneiro (May 05 2019 at 10:05):

but the manifold instance already mentions E

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

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

view this post on Zulip Mario Carneiro (May 05 2019 at 10:07):

or is it manifold ?E ?X M

view this post on Zulip Mario Carneiro (May 05 2019 at 10:08):

what is that second argument?

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

view this post on Zulip Sebastien Gouezel (May 05 2019 at 10:08):

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

view this post on Zulip Mario Carneiro (May 05 2019 at 10:10):

can you make another class?

view this post on Zulip Mario Carneiro (May 05 2019 at 10:10):

like model_space M ?E or something

view this post on Zulip Mario Carneiro (May 05 2019 at 10:10):

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (May 05 2019 at 10:43):

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

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (May 05 2019 at 13:04):

that's not a vector space

view this post on Zulip Sebastien Gouezel (May 05 2019 at 13:04):

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

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (May 05 2019 at 15:07):

where is_C1_manifold is a Prop

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

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

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

view this post on Zulip Mario Carneiro (May 05 2019 at 16:20):

because the manifold instance depends on G

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

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

view this post on Zulip Mario Carneiro (May 05 2019 at 16:23):

The manifold lives in a different type

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

view this post on Zulip Mario Carneiro (May 05 2019 at 16:25):

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

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

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

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

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:06):

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:06):

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:15):

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

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

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

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

view this post on Zulip Kenny Lau (Apr 08 2020 at 07:22):

core lean doesn't mean C++ lean code

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:22):

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:23):

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

view this post on Zulip Kenny Lau (Apr 08 2020 at 07:23):

oh, interesting

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

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:30):

@Mario Carneiro @Gabriel Ebner

view this post on Zulip Mario Carneiro (Apr 08 2020 at 07:31):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 07:31):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 07:32):

the change you are talking about is entirely in lean

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:34):

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

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 07:35):

The change in the PR is only about parsing

view this post on Zulip Mario Carneiro (Apr 08 2020 at 07:35):

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:36):

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

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

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 07:36):

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

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 07:37):

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:38):

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

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:39):

Did you redefine singleton?

view this post on Zulip Mario Carneiro (Apr 08 2020 at 07:39):

no, this is stock lean

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:40):

If you redefine singleton, then it stops working.

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

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

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

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 07:50):

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

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

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

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:55):

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:55):

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 07:56):

Ignore.

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

view this post on Zulip Johan Commelin (Apr 08 2020 at 08:01):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:01):

not from lean

view this post on Zulip Johan Commelin (Apr 08 2020 at 08:01):

Sure... but we are changing core Lean anyway

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:01):

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

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:06):

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

view this post on Zulip Kenny Lau (Apr 08 2020 at 08:10):

so the printer has access to definitions of stuffs?

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

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

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:14):

did you think we had that property before?

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 08:14):

Why not?

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

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 08:15):

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

view this post on Zulip Johan Commelin (Apr 08 2020 at 08:16):

Hmmm, that's probably right

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

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:19):

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

view this post on Zulip Johan Commelin (Apr 08 2020 at 08:19):

Of course

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:20):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:20):

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 08:20):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:21):

no, why?

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:21):

I have a pretty good idea what will happen

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 08:22):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 08:22):

it will produce the term insert 0 (singleton 1)

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 08:22):

And how will it be pretty-printed?

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 08:23):

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

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