Zulip Chat Archive

Stream: general

Topic: universes


view this post on Zulip Phiroc (Apr 06 2020 at 11:08):

Hello,
in Theorem Proving in Lean, the authors provide the following examples:

#check list -- Type u_1 -> Type u_1
#check prod -- Type u_1 -> Type u_2 -> Type (max u_1 u_2)

Why is the universe the same in the first case, and different in the second?

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

there is one input in the first case and two in the second

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

in general, we want the output type to be determined by the inputs, and the output type will usually be the max of the universes of all the inputs

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:30):

Are there foundational problems with allowing mild(?) quantification over universe variables?

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:30):

yes, it increases the axiomatic strength

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:31):

That's the only problem?

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:31):

Sounds like a good thing to me :grinning:

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:32):

I mean it doesn't really solve any problems, you just get more universes that you aren't allowed to quantify over

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:32):

Well, it might solve my problems

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:32):

if you add the ability to quantify over all universes, including the ones you are adding, then you get a second impredicative universe and then it's hello paradox

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:33):

I think I only care about rings/modules/schemes that live in Type n for n : nat

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:33):

I think I would prefer the solution Kevin often talks about, where you have less universes, preferably none

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:34):

And since most mathematicians still pretend they only work in Type 0, I think it will take some time before we get a profound mathematical construction that genuinely takes a limit construction over Type n (n : nat) to produce something that lives in Type \omega

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:35):

Mario Carneiro said:

I think I would prefer the solution Kevin often talks about, where you have less universes, preferably none

But then, why all this trouble of being universe polymorphic?

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:35):

The thing is, once you are doing limit constructions you don't just get to Type \omega, you get to Type (aleph omega) or an even higher cardinal

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:36):

We have to be universe polymorphic because someone had the poor sense to put universes in the type theory

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:36):

Right, but my point is that I don't see such constructions happening.

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:36):

Whereas I do hope that we might be able to have etale cohomology soonish. The ingredients are slowly dripping into mathlib.

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:36):

so if you want to be generic over things you can construct in lean then you have to be universe polymorphic

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:37):

But without universes, you'll have a major pain when you try to define sheaf cohomology

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:38):

I don't think universes actually solve that pain, they just put it somewhere else

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:38):

Why?

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:39):

because you can't iterate any universe bumping construction, so inevitably you still have to figure out how to do whatever you are doing without any universe bumps

view this post on Zulip Johan Commelin (Oct 20 2020 at 06:40):

Right, but my point is that I don't know of any construction in maths that (even informally) is iterating universe bumps.

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:40):

and at the end of it you realize it all fit in ZFC to begin with

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:41):

I've said it before: what category theorists actually want is Type in Type, not this universe nonsense

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:41):

and if and when you make all the reasoning consistent you find it's just plain old ZFC

view this post on Zulip Mario Carneiro (Oct 20 2020 at 06:42):

universes make everything more complicated and don't solve the problem they set out to solve

view this post on Zulip Reid Barton (Oct 20 2020 at 13:50):

I totally disagree with the above 3 lines, with the caveat that math universes are not the same as type theory universes

view this post on Zulip Reid Barton (Oct 20 2020 at 13:51):

It all fits in ZFC+U--if we're redefining ZFC to mean that then great

view this post on Zulip Reid Barton (Oct 20 2020 at 14:01):

It's also probably the case in a given application (in algebraic geometry say) that you can remove the "U" axiom, in the reverse mathematics sense--but this doesn't mean the category theory itself lives in ZFC, any more than the modularity theorem lives in PA

view this post on Zulip Mario Carneiro (Oct 20 2020 at 15:39):

I think most real category theory still fits in higher order ZFC, with no actual universes

view this post on Zulip Mario Carneiro (Oct 20 2020 at 15:41):

and higher order ZFC fits in ZFC for most concrete arguments if you play enough logical tricks

view this post on Zulip Kevin Buzzard (Oct 20 2020 at 16:58):

There are certainly some instances where mathematicians do stuff with universes and then force everything back into ZFC. However it is getting to the point where there are things which some mathematicians (e.g. Scholze) do which cannot be forced back into ZFC, or, at least, nobody is trying to force it back into ZFC right now. We're quite a way away from this in mathlib so whether this will matter to us in practice is unclear to me -- but perhaps Reid knows other areas of maths which are also falling out of ZFC.

I am not looking forward to all this "force everything back into ZFC" issue when we run into etale cohomology. We want to take a limit over a universe and then there's a theorem saying that it's "equal to" a limit over a type. Nowadays I am quite conflicted about to how important this descent is.

view this post on Zulip Reid Barton (Oct 20 2020 at 17:48):

Mike Shulman has a paper https://arxiv.org/pdf/0810.1279.pdf discussing size issues in category theory and the possible ways to resolve them (including universes).

view this post on Zulip Reid Barton (Oct 20 2020 at 17:51):

Here's a simple example where ZFC is inadequate. Suppose I already have a theory of monoidal categories and monoid objects in them and their modules. Now a friendly Haskell programmer informs me that a monad on a category CC is "just a monoid in the category of endofunctors [C,C][C, C]". Great, now I can apply my existing theory to get a theory of monads and their modules (usually known as algebras).

view this post on Zulip Reid Barton (Oct 20 2020 at 17:52):

However, if I try to apply this to a large category (like C=SetC = \mathrm{Set} or C=ModRC = \mathrm{Mod}_R) this breaks down, because the "endofunctor category" [C,C][C, C] is "too large" to fit in ZFC even as a proper class (basically because its objects are already class-sized).

view this post on Zulip Reid Barton (Oct 20 2020 at 17:53):

So, I'm forced to develop a parallel but separate theory of monads on large categories.

view this post on Zulip Reid Barton (Oct 20 2020 at 17:58):

For a much fancier example, in algebraic geometry, there's no difficulty in ZFC in defining a stack of small categories on a small site. But, putting aside the issue of the size of the site, it's also very useful to consider stacks of large categories. For example, there is a stack which assigns to SpecR\mathrm{Spec}\,R the category ModR\mathrm{Mod}_R of RR-modules. On a scheme XX, the "global sections" of this stack is the category of quasicoherent modules on XX.

view this post on Zulip Kevin Buzzard (Oct 20 2020 at 17:59):

It would not surprise me if some mathematicians thought that we were in some kind of second foundational crisis -- ZFC worked fine for 100 years but now people really want to do stuff which pushes it to the limits and possibly beyond. However there are many areas of mathematics for which ZFC is completely adequate; I was talking to Hairer about this and he seemed absolutely convinced that he didn't even need full AC, and that ZF + countable dependent choice could get him a Fields Medal in the kind of analysis he did.

view this post on Zulip Kevin Buzzard (Oct 20 2020 at 18:01):

I've never thought about precisely how much AC I need, but I have this uncomfortable feeling that the ZFC crisis I had in my 20s, when I carefully checked that a bunch of stuff I wanted/needed could be done in ZFC, is now going to be repeated if I ever want to dive into condensed mathematics, and this time I'm not entirely sure what the answer will be.

view this post on Zulip Reid Barton (Oct 20 2020 at 18:15):

With my category theorist hat on, I want to make two points:

  1. It really is important to make some size distinctions, at least to the extent of "small" and "large" , because you can't do very much category theory without talking about Set and other large categories, and here we already find for example that Set has (co)limits indexed by small categories but not large ones. The beginning of Shulman's paper gives more examples of this kind.
  2. It's useful at least for conceptual reasons to talk about "very large" categories like [Set,Set][\mathrm{Set}, \mathrm{Set}] or the 2-category of all stacks of locally presentable categories on a scheme (or whatever). These objects are too big to exist in ZFC(at least if we interpret Set\mathrm{Set} as referring to the category of all sets, and similarly for locally presentable categories).

view this post on Zulip Reid Barton (Oct 20 2020 at 18:24):

Now,

  • In the end, one might be interested in a specific theorem about monads or quasicoherent modules or whatever, and then one could ask whether or not this theorem is provable in ZFC. In my view, this is basically a question of reverse mathematics, and those who aren't interested in such questions shouldn't feel obliged to care about them.
  • A lot of category theory can be presented in a way which is agnostic to the specific foundations, while still making the basic small/large distinction. In this case, the reader can choose whether to interpret "small/large" as "set/class" or "element of U\mathcal{U}/non-element of U\mathcal{U}" or in some other way.

Personally, I find the interpretation using Grothendieck universes convenient because it allows me to make sense of all category theory using ordinary sets, and doesn't need classes or fancy logic. However, it does have the disadvantages that the interpretation is relative to a fixed inaccessible cardinal and that, for example, a group constructed to have a certain universal property a priori only has this universal property with respect to other groups that are small with respect to the reference cardinal, and not with respect to all groups.

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:30):

Reid, since you are in this foundational mood, and I don't know anything about all this, do you have a definitive answer to the question: if I have a set S, can I define free groups over SS as groups FF equipped with a map from i:SFi : S \to F such that, for all groups GG and f:SGf : S \to G there is a unique morphism φ:FG\varphi : F \to G such that φi=f\varphi \circ i = f? Or is it forbidden because there is no set of groups? If it's forbidden, what can be done?

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:31):

I have the vague impression this is forbidden as a definition but somewhat allowed as a theorem about a given FF, but this doesn't seem to make any sense.

view this post on Zulip Johan Commelin (Oct 20 2020 at 18:34):

At least in Lean the answer seems to be that you cannot make it the definition, but you can make it a theorem.

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:34):

Yes, this is my impression, but it's weird and I'd like to understand this one day (or at least have the feeling to understand a bit and get a reference I can read from times to times)

view this post on Zulip Kevin Buzzard (Oct 20 2020 at 18:36):

Yes that's no definition. You can only quantify over all G in some universe, so really you end up with infinitely many universal properties in some sense.

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:36):

But still it can be a property, right?

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:37):

Because if I define FF using reduced words etc. then certainly it satisfies the universal property for all groups, right?

view this post on Zulip Reid Barton (Oct 20 2020 at 18:39):

In ZFC the predicate "f:SFf : S \to F exhibits FF as the free group on SS" defined in this way (for all groups GG and maps SGS \to G there exists ...) is totally fine. For example, it could be a hypothesis to a theorem. (Of course you need to do something else to prove that there actually exists such an FF and ff, but I don't think that's what you were asking about.)

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:40):

Then where is the problem? Is it that we want more than ZFC for other purposes and this breaks this definition?

view this post on Zulip Reid Barton (Oct 20 2020 at 18:41):

The problem with doing category theory in ZFC?

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:41):

The problem with defining stuff using universal properties

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:43):

If I have several universes, I can still prove that my favorite free groups satisfies the universal property for all groups in any universe but this cannot be an assumption in a theorem, right?

view this post on Zulip Eric Wieser (Oct 20 2020 at 18:45):

... which means you can end up writing essentially the same proof over and over again for each of your favorite free groups, right?

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:45):

And if I have a low-tech definition of free groups (something like i(S)i(S) generates FF and there is no relation between elements of i(S)i(S), which can be defined properly), I cannot state something like "(F,i)(F, i) is a free group on SS iff it satisfies the universal property for every group in every universe" right?

view this post on Zulip Johan Commelin (Oct 20 2020 at 18:46):

What do you mean with "any"?

view this post on Zulip Johan Commelin (Oct 20 2020 at 18:46):

If it means "all", then you indeed cannot,
if it means "there exists a universe", then you can

view this post on Zulip Reid Barton (Oct 20 2020 at 18:46):

If you're doing category theory in ZFC+U with the "all categories implicitly relativized to a universe U\mathcal{U}" convention, then it is still meaningful to talk about whether a morphism f:SUFf : S \to UF (U:SetGrpU : \mathrm{Set} \to \mathrm{Grp} the forgetful functor) has the universal property of making FF a free group with respect to all groups. It just isn't the condition that falls out from the category theory, because Grp\mathrm{Grp} now means "all U\mathcal{U}-small groups" (and likewise for Set\mathrm{Set}).

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:47):

English is a really awful language, but hopefully I disambiguated.

view this post on Zulip Reid Barton (Oct 20 2020 at 18:48):

At least not by definition--of course in this case the two conditions really are equivalent, but the easiest way to see that might be to note that you can construct the free group in a way that does not depend upon the reference universe U\mathcal{U}.

view this post on Zulip Reid Barton (Oct 20 2020 at 18:49):

Johan's answer is right for Lean, but not for ZFC+U, I think.

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:49):

But why is there this assymetry that I can state this as a property of a given concrete (F,i)(F, i) but not as an assumption of a theorem?

view this post on Zulip Reid Barton (Oct 20 2020 at 18:49):

You can state that, and even prove it.

view this post on Zulip Reid Barton (Oct 20 2020 at 18:50):

In Lean, it works differently because you can only quantify over types in a specific universe, and quantifiers over universes can only occur at the outside of a top-level definition.

view this post on Zulip Reid Barton (Oct 20 2020 at 18:52):

In ZFC I think that statements which use bounded quantification, i.e., only have quantifiers like X,XS\forall X, X \in S \to \ldots is a notion which is useful, but you're not restricted to only making such statements.

view this post on Zulip Reid Barton (Oct 20 2020 at 18:53):

(Sorry, that was a poorly-constructed sentence but I hope it makes sense.)

view this post on Zulip Patrick Massot (Oct 20 2020 at 18:56):

So what is impossible with ZFC + universes then?

view this post on Zulip Reid Barton (Oct 20 2020 at 19:02):

The drawback of this approach isn't that anything is impossible, but rather that if you really care about (let's say) "Universal" properties that quantify over all groups, or whatever, you will have to do some extra work to know that you have one.

view this post on Zulip Reid Barton (Oct 20 2020 at 19:03):

Whereas if you really did category theory with the category of all groups in the first place, then universal properties in category theory would be true Universal properties.

view this post on Zulip Reid Barton (Oct 20 2020 at 19:05):

(Plus of course you might be concerned about accepting the universe axiom, which does prove additional arithmetic statements like Con(ZFC).)

view this post on Zulip Patrick Massot (Oct 20 2020 at 19:05):

What is Con(ZFC)?

view this post on Zulip Patrick Massot (Oct 20 2020 at 19:05):

consistency?

view this post on Zulip Reid Barton (Oct 20 2020 at 19:06):

Yes, or more precisely, some encoding of it in terms of natural numbers.

view this post on Zulip Reid Barton (Oct 20 2020 at 19:07):

Some particular, rather large polynomial in a few variables has no integer solution.

view this post on Zulip Reid Barton (Oct 20 2020 at 19:10):

The later parts of Shulman's paper go into ways to systematically turn universe-relative universal properties into true Universal properties, and ways you might be able to talk about "very large" categories without increasing the consistency strength of the background theory.

view this post on Zulip Patrick Massot (Oct 20 2020 at 19:12):

Ok, thanks for all you explanations! I'll try to think about all that.

view this post on Zulip Adam Topaz (Oct 20 2020 at 20:26):

I have a question related to this issue about defining things in terms of their universal properties. I know of one example in mathlib which does (more-or-less) exactly this: src#stone_cech_setoid
Does this mean that mathlib only has the universal property of the Stone-Cech compactification for topological spaces which live in the same universe? Is there any way around this (without changing the definition of stone_cech)?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:11):

@Adam Topaz It is a curious consequence of "internal definitions" (for example, a free group is a certain quotient of lists) that they imply and are implied by the "external definition" (a free group is one that maps in an appropriate way to all groups) at every universe. This fact means that even a definition using an external definition at Type u is equivalent to the external definition at all types, so stone_cech's universal property applies even to larger universes even though you can't apply it directly

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:21):

Patrick Massot said:

But why is there this assymetry that I can state this as a property of a given concrete (F,i)(F, i) but not as an assumption of a theorem?

The key to this ability for us to prove external properties that we didn't quantify over to start with at the foundational level is the extra universe argument in T.rec:

inductive nat'
| zero : nat'
| succ : nat'  nat'
#print nat'.rec
-- protected eliminator nat'.rec : Π {C : nat' → Sort l},
--  C nat'.zero → (Π (a : nat'), C a → C a.succ) → Π (n : nat'), C n

Note that nat' has no universe parameters but it has a recursor that quantifies over a universe parameter l. If recursors didn't do this, for example if nat'.rec only quantified over C : nat' -> Type, then we wouldn't need the inductive axioms at all; we could use church encodings to do everything. But this universe lifting property is truly magical, as it allows you to prove that a universal property at one type implies a universal property for one specifically crafted inductive type, which then implies the universal property at a higher universe using that inductive type's recursor.

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:29):

@Mario Carneiro As a concrete example, is it possible to make the second example in the following code work?

import topology.stone_cech

noncomputable theory

universes u v
variables {α : Type u} {β : Type v} [topological_space α] [topological_space β]
  [compact_space β] [t2_space β]
variables {γ : Type u} [topological_space γ] [compact_space γ] [t2_space γ]

example (f : α  γ) (cont : continuous f) : stone_cech α  γ := stone_cech_extend cont -- works

example (f : α  β) (cont : continuous f) : stone_cech α  β := stone_cech_extend cont -- doesn't work

I understand that it's possible to prove that the stone cech compactification of a topological space in Type u, which is defined so that it satisfies the universal property with respect to every topological space of Type u, also satisfies the universal property for every topological space of Type v. But it seems to me that doing this is essentially equivalent to redefining the stone cech compactification, or more specifically in this case, the equivalence relation stone_cech_setoid, so that it doesn't quantify over types in the first place.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:32):

that's right

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:33):

you can't apply stone_cech_extend directly

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:33):

Okay, so life isn't as easy as I would have hoped.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:33):

but you can hide this construction inside a proof, for example, if you wanted to keep the definition "clean"

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:34):

Mario Carneiro said:

but you can hide this construction inside a proof, for example, if you wanted to keep the definition "clean"

What do you mean by this?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:35):

you can construct an inductive type with the requisite properties in order to prove that the universal property at u implies the universal property at v

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:35):

and then that is the theorem you would be applying instead of stone_cech_extend

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:37):

Oh, I'm not sure what such an inductive type would like like. You mean something similar to ulift?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:38):

no, it depends on the universal property

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:38):

for free groups it's lists on the basic elements

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:38):

in a lot of categorical proofs this is where we show that the presheaf is representable

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:38):

Ah okay. So this would just redefine the object altogether then.

view this post on Zulip Reid Barton (Oct 21 2020 at 13:39):

When I wrote the stone_cech stuff I think I just followed some notes I found online--if there's a way to describe the required topology directly, without quantifying over Type u, then that's probably a better definition.

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:39):

I think there is a way to do it, using the monadic properties of ultrafilters, but of course it's more complicated.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:41):

I think the internal definition of stone cech uses the set of ultrafilters

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:41):

Actually, maybe it's not too bad with what's in this file:
https://github.com/leanprover-community/mathlib/blob/master/src/topology/category/Compactum.lean

view this post on Zulip Reid Barton (Oct 21 2020 at 13:41):

For example maybe it's enough to consider all quotients of ultrafilter α itself

view this post on Zulip Reid Barton (Oct 21 2020 at 13:42):

or maybe you don't even need to allow a quotient

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:44):

Isn't the stone cech compactification the largest quotient of ultrafilter \a which is an algebra for the ultrafilter monad, and for which the canonical map from \a is continuous?

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:44):

This would be a description that says nothing about any type other than \a itself.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:45):

@_Wikipedia said:

There are several ways to modify this idea to make it work; for example, one can restrict the compact Hausdorff spaces K to have underlying set P(P(X)) (the power set of the power set of X), which is sufficiently large that it has cardinality at least equal to that of every compact Hausdorff set to which X can be mapped with dense image.

view this post on Zulip Adam Topaz (Oct 21 2020 at 13:47):

The constructions in terms of maps to the unit interval (from wiki) would also work, I guess.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:47):

This reminds me that hausdorff sets have an interesting cardinality bound: they are at most the double powerset of any dense subset A because you can uniquely pick out every element of X by a filter in A

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:48):

I think this proof would be easiest (I've done it in metamath before, it follows from the axioms pretty easily)

view this post on Zulip Mario Carneiro (Oct 21 2020 at 13:48):

the unit interval requires partitions of unity, which I think are more complicated

view this post on Zulip Reid Barton (Oct 22 2020 at 17:09):

By the way, what was the original point of this thread? :upside_down:

view this post on Zulip Reid Barton (Oct 22 2020 at 17:09):

What was quantifying over universe levels intended to be used for?

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:10):

I think specifying universal properties?

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:10):

Johan Commelin said:

Are there foundational problems with allowing mild(?) quantification over universe variables?

Why can't I write a bundled_hom class that is universe polymorphic...

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:10):

That's what my motivation was

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:10):

Because I want bundled_hom.funext and bundled_hom.congr_arg and bundled_hom.congr_fun, etc...

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:11):

what is a bundled hom in this context?

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:11):

Instead of having to reprove them for mul_hom, zero_hom, monoid_hom, one_hom, ring_hom, alg_hom, the list goes on...

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:11):

E.g. a group homomorphism from a group of Type u to a group of Type v.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:11):

equiv is a universe polymorphic bundled hom

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:11):

Mario Carneiro said:

what is a bundled hom in this context?

It is bundled_hom in the sense of docs#bundled_hom

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:12):

Snap!

view this post on Zulip Reid Barton (Oct 22 2020 at 17:12):

It's not clear to me why this needs more universe quantification than Lean provides

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:13):

I think it's because of bundled as in docs#category_theory.bundled

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:14):

docs#category_theory.bundled_hom is a predicate on homs from Type u to Type u. It could be a predicate on homs from Type u to Type v but then you couldn't compose them

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:14):

variables {c : Type u  Type u} (hom : Π α β : Type u ( : c α) ( : c β), Type u)

/-- Class for bundled homs. Note that the arguments order follows that of lemmas for `monoid_hom`.
This way we can use `⟨@monoid_hom.to_fun, @monoid_hom.id ...⟩` in an instance. -/
structure bundled_hom :=
(to_fun : Π {α β : Type u} ( : c α) ( : c β), hom    α  β)
(id : Π {α : Type u} (I : c α), hom I I)
(comp : Π {α β γ : Type u} ( : c α) ( : c β) ( : c γ),
  hom    hom    hom  )
(hom_ext :  {α β : Type u} ( : c α) ( : c β), function.injective (to_fun  ) . obviously)
(id_to_fun :  {α : Type u} (I : c α), to_fun I I (id I) = _root_.id . obviously)
(comp_to_fun :  {α β γ : Type u} ( : c α) ( : c β) ( : c γ)
  (f : hom  ) (g : hom  ),
  to_fun   (comp    g f) = (to_fun   g)  (to_fun   f) . obviously)

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:14):

You can't even define them with two universe variables

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:14):

Because you need id

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:14):

Actually I think c could be Type u -> Type v

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:14):

It would be cool to define the "category" of groups as having underlying object type \Sigma {u : universe} (G : Type u) (is_group : group G)

view this post on Zulip Reid Barton (Oct 22 2020 at 17:15):

oh bundled_hom isn't a bundled hom

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:15):

But nevertheless ring_hom.id is a thing

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:15):

Adam Topaz said:

It would be cool to define the "category" of groups as having underlying object type \Sigma {u : universe} (G : Type u) (is_group : group G)

Is that an example of a \HUGE category?

view this post on Zulip Reid Barton (Oct 22 2020 at 17:15):

I'm trying to understand what the end goal is though

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:15):

type in type

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:16):

So that the universal property of the free group is actually the left adjoint to the forgetful functor for example.

view this post on Zulip Reid Barton (Oct 22 2020 at 17:16):

But bundled_hom.funext and so on sounds a lot simpler than talking about universal properties

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:18):

also don't forget the "metatheorem" approach: write a tactic to generate all instantiations of a schematic theorem

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:18):

you can quite often write higher order theorems than the logic actually supports this way

view this post on Zulip Reid Barton (Oct 22 2020 at 17:19):

This was on my mind too but I wanted to understand what those theorems are first.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:20):

I think a tactic that writes the theory of foo_homs would be more useful than literal category theory

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:21):

and as long as everything is in meta-land the high consistency strength requirements of general category theory is no problem

view this post on Zulip Reid Barton (Oct 22 2020 at 17:22):

Well, I think Johan's intention was also not to literally do category theory but just be able to abstract over what it means to be a "foo hom" when multiple universes are involved

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:22):

sure, but I assume this is going to be used for something

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:23):

like perhaps proving theorems generic over different kinds of bundled homs

view this post on Zulip Reid Barton (Oct 22 2020 at 17:23):

For ext this problem is already solved by @[ext], right?

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:23):

I think the interesting problem is explicating the actual set of theorems we'd like to generate for foo homs

view this post on Zulip Reid Barton (Oct 22 2020 at 17:23):

What's an example of a theorem in mathlib which would be a special case of one of these generalized theorems?

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:25):

I am still stuck at the stage where everything category theory appears to deliver is utterly trivial results about associativity pentagons that are one line proofs in the concrete case, which is why I have a poor opinion of the subject

view this post on Zulip Reid Barton (Oct 22 2020 at 17:25):

In particular, it's not clear to me that we couldn't solve whatever the problem is by just having a class like class has_hom (foo : Type*) (bar : Type*) without it knowing that we're always going to set e.g. foo = ring.{u} and bar = ring.{v}.

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:25):

I would like to be able to write the following, for example:

class is_free_group (G : Type u) (S : Type u) [group G] :=
(incl : S  G)
(lift {v : universe} {H : Type v} [group H] (f : S  H) : G →* H)
(lift_comp_incl {v : universe} {H : Type v} [group H] {f : S  H} : (lift f)  incl = f)
(lift_unique {v : universe} {H : Type v} [group H] {f : S  H} {g : G →* H} :
  g  incl = f  g = lift f)

view this post on Zulip Reid Barton (Oct 22 2020 at 17:26):

No, this universal property example I understand and it seems hard but it sounded like the things Johan wanted might be easy.

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:27):

Oh, then I misunderstood what the goal was.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:31):

you can get reasonably close to a general theory using

class is_free_group_lift (G : Type u) (S : Type u) [group G] (incl : S  G)
  {H : Type v} [group H] (f : S  H) :=
(lift : G →* H)
(lift_comp_incl : lift  incl = f)
(lift_unique {g : G →* H} : g  incl = f  g = lift)

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:33):

Oh interesting.

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:34):

But of course this wouldn't give a specification of the free group.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:35):

no but I'm not trying to do that, I'm trying to do everything a specification of the free group would do

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:36):

anyway we know how to specify free groups, you can just restrict to universe u and that works because free groups have some presentability property

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:37):

you can always say "I wish my foundations were more expressive than they are, because they miss <use case X>", that's godel incompleteness

view this post on Zulip Reid Barton (Oct 22 2020 at 17:37):

Right, the fact that you can't directly state what I called the "Universal property" is kind of annoying, but in specific cases you can find alternative definitions (e.g., by restricting the universe to an appropriate one) and then prove an "improved" eliminator which removes the universe restriction.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:39):

My contention above is actually that you can use is_free_group_lift to work with the unreduced is_free_group predicate by referring to it obliquely

view this post on Zulip Reid Barton (Oct 22 2020 at 17:39):

For example in your original is_free_group, if we replace v by u (since we know the free group construction doesn't increase the universe level, this should be fine), then the type of is_free_group.lift is something like Pi (G : Type u) (S : Type u) [group G] [is_free_group G S] {H : Type u} [group H] (f : S -> H) : G ->* H, but we can define a better projection with the type Pi (G : Type u) (S : Type u) [group G] [is_free_group G S] {H : Type v} [group H] (f : S -> H) : G ->* H.

view this post on Zulip Reid Barton (Oct 22 2020 at 17:40):

And for the construction side, obviously it's fine to only have to pass the fields in in the special case v = u.

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:40):

I think for every foo in one, mul, monoid, ring, we have about 100 lines of quasi-consistent api for foo_hom (and linear_map and alg_hom maybe, although they depend on R), and then another 100 lines for foo_equiv.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:41):

so let's automate it

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:41):

But these APIs are currently not all homogeneous, there are gaps all over the place.

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:41):

Our only hope is that Yury will refactor them....

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:42):

We want ext, ext_iff, coe, coe_injective, funext, congr_arg, congr_fun, coe_mk, and another 10 common lemmas

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:42):

It would be nice to have a framework for writing entire theory templates that will be multiply instantiated

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:42):

id, comp, id_comp, comp_id, comp_assoc, id_apply, comp_apply

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:43):

those lemmas are all inputs to the category theory though, you get no help in proving them

view this post on Zulip Reid Barton (Oct 22 2020 at 17:44):

I don't think abstracting over the category is really viable anyways when using the style of unbundled objects and arrows that specify which structure they preserve

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:45):

Not all of them are input, and some of them the automation should be able to guess

view this post on Zulip Reid Barton (Oct 22 2020 at 17:45):

I mean, I guess it might be but it's not the way the category theory library is set up at least

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:45):

it's certainly viable for meta code to abstract over the category

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:46):

even if it's a large/universe polymorphic category

view this post on Zulip Reid Barton (Oct 22 2020 at 17:46):

Right, I meant trying to prove the theorems like comp_assoc for all the variants like ->* simultaneously (or even making them all instances of the same type class or whatever).

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:47):

it does seem like a good idea to focus on the concrete category case though, because almost all our examples are of that form

view this post on Zulip Reid Barton (Oct 22 2020 at 17:47):

By simultaneously I mean in a single Lean definition

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:47):

I feel like we're going back to all those discussions about universal algebra ;)

view this post on Zulip Reid Barton (Oct 22 2020 at 17:47):

Yay!

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:48):

didn't someone write a program that would do some of this? Subgroups and submonoids and other subthings?

view this post on Zulip Adam Topaz (Oct 22 2020 at 17:49):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Free.20stuff/near/209873309

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:52):

Clearly a framework for doing this in a more ergonomic way would be good

meta def homomorphism_comp (struct_name : name) : tactic declaration :=
do (params, fields)  get_parameters_and_data_fields struct_name,
   let base_type := params.head,
   let struct_u : expr :=  expr.const struct_name [level.param `u],
   let struct_v : expr :=  expr.const struct_name [level.param `v],
   let struct_w : expr :=  expr.const struct_name [level.param `w],
   α  mk_local' `α binder_info.implicit (sort (level.succ (level.param `u))),
   ia  mk_local' `ia binder_info.inst_implicit (struct_u α),
   β  mk_local' `β binder_info.implicit (sort (level.succ (level.param `v))),
   ib  mk_local' `ib binder_info.inst_implicit (struct_v β),
   γ  mk_local' `γ binder_info.implicit (sort (level.succ (level.param `w))),
   ic  mk_local' `ic binder_info.inst_implicit (struct_w γ),
   f  mk_local' `f binder_info.implicit (pi `_x binder_info.default α β),
   g  mk_local' `g binder_info.implicit (pi `_x binder_info.default β γ),
   let hom_name := mk_simple_name (string.append struct_name.to_string "_homomorphism"),
   let hom_constr_name := hom_name <.> "mk",
   hom_f  mk_app hom_name [α, β, ia, ib, f],
   hom_g  mk_app hom_name [β, γ, ib, ic, g],
   hf  mk_local' `hf binder_info.default hom_f,
   hg  mk_local' `hg binder_info.default hom_g,
   compos  mk_mapp `function.comp [none, none, none, g, f],
   stmt  mk_app hom_name [α, γ, ia, ic, compos],
   let field_numbers := list.range fields.length,
   let fields_enum := list.zip fields field_numbers,
   compatibilities  fields_enum.mmap
    (λ field_enum, homomorphism_comp_part struct_name base_type α β γ ia ib ic f g hf hg
                    field_enum.fst field_enum.snd fields_enum.length),
   constr  mk_mapp hom_constr_name [some α, some γ, some ia, some ic, some compos],
   let body := expr.app_of_list constr compatibilities,
   let decl_body := expr.lambdas [α, β, γ, ia, ib, ic, f, g, hf, hg] body,
   let decl_type := expr.pis [α, β, γ, ia, ib, ic, f, g, hf, hg] stmt,
   let decl_name := mk_simple_name (string.append struct_name.to_string "_homomorphism_comp"),
   return $ declaration.thm decl_name (collect_univ_params decl_type) decl_type (task.pure decl_body)
-- for any transitive target? eq, if, iff, ...

view this post on Zulip Mario Carneiro (Oct 22 2020 at 17:55):

One possibility, similar to to_additive, would be to write a sort of "sample definition" and extract the template to instantiate from it, changing the names of constants and possibly applying a substitution but otherwise keeping things as is

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:55):

@Cyril Cohen How hard is it to tie your algebra framework into Lean?

view this post on Zulip Reid Barton (Oct 22 2020 at 18:00):

Mario Carneiro said:

One possibility, similar to to_additive, would be to write a sort of "sample definition" and extract the template to instantiate from it, changing the names of constants and possibly applying a substitution but otherwise keeping things as is

I believe you'll find that such a tool already exists and is known as "the C preprocessor" :upside_down:

view this post on Zulip Reid Barton (Oct 22 2020 at 18:02):

I guess stuff like "preserves the algebraic structure" needs to iterate over a variable number of operations (e.g. +, * or both)

view this post on Zulip Johan Commelin (Oct 22 2020 at 18:03):

But the proof of ext_iff doesn't care about algebraic structure. And neither does comp_assoc, nor does comp_id or id_apply.

view this post on Zulip Johan Commelin (Oct 22 2020 at 18:13):

lemma one_hom.to_fun_eq_coe
lemma one_hom.coe_mk
lemma one_hom.coe_inj
lemma one_hom.ext
lemma one_hom.ext_iff
lemma one_hom.id_apply
lemma one_hom.comp_apply
lemma one_hom.comp_assoc
lemma one_hom.cancel_right
lemma one_hom.cancel_left
lemma one_hom.comp_id
lemma one_hom.id_comp

this is what I extracted about one_homs

The proofs don't use any properties of one_hom, except that it behaves like a function.
It's all rfl or cases, cases, congr or some generic logic lemmas.

view this post on Zulip Johan Commelin (Oct 22 2020 at 18:14):

The list is incomplete, because things like funext and congr_arg are missing.

view this post on Zulip Reid Barton (Oct 22 2020 at 18:20):

Right, so while I think it's probably better to autogenerate these lemmas at the same time as we autogenerate the rest of the theory of has_ones and sub_has_ones and so on, I claim you don't need any fancy universe polymorphism to implement one_hom.comp_assoc, say, in terms of ingredients that say that "taking the underlying function" is injective and commutes with composition.

view this post on Zulip Reid Barton (Oct 22 2020 at 18:21):

I'm not really sure, though.

view this post on Zulip Eric Wieser (Oct 22 2020 at 18:23):

Could those particular lemmas be written in terms of a has_to_fun typeclass?

view this post on Zulip Eric Wieser (Oct 22 2020 at 18:24):

Which provides has_coe_to_fun in term of the member

view this post on Zulip Reid Barton (Oct 22 2020 at 18:25):

Right, I would just start with things like class has_comp (a b : Type) (c : out_param Type) and compatibility classes and see whether that's good enough

view this post on Zulip Adam Topaz (Oct 22 2020 at 18:28):

So I'm trying something like this:

import tactic

variables (hom : Π (α : Type*) (β : Type*), Type*)

class has_faithful_coe_to_fun :=
(coe {α β} : hom α β  α  β)
(is_faithful {α β} {f g : hom α β} : coe f = coe g  f = g)

namespace has_faithful_coe_to_fun

variable [has_faithful_coe_to_fun hom]

instance {α β} : has_coe_to_fun (hom α β) := λ f, α  β,λ f, coe f

@[ext]
lemma ext {α β} (f g : hom α β) : f = g  f = g := λ h, is_faithful h

end has_faithful_coe_to_fun

view this post on Zulip Adam Topaz (Oct 22 2020 at 18:30):

But I'm getting an error at ext saying only constants and Pi types are supported: hom α β.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 18:31):

Reid Barton said:

Mario Carneiro said:

One possibility, similar to to_additive, would be to write a sort of "sample definition" and extract the template to instantiate from it, changing the names of constants and possibly applying a substitution but otherwise keeping things as is

I believe you'll find that such a tool already exists and is known as "the C preprocessor" :upside_down:

You know, we have something that is just as flexible/hackish as the C preprocessor: emit_code_here

view this post on Zulip Mario Carneiro (Oct 22 2020 at 18:32):

that's definitely one way to make theory templates, just do string replacement in a big code block in quotes

view this post on Zulip Mario Carneiro (Oct 22 2020 at 18:34):

plus, unlike the tactic approach, it actually lets you write defs that are just as good as the real thing

view this post on Zulip Adam Topaz (Oct 22 2020 at 18:35):

How do you use it? Can I just write the following?

run_cmd emit_code_here "def foo := 1"

view this post on Zulip Johan Commelin (Oct 22 2020 at 18:38):

Can we use this: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Generate.20homomorphism.20types.20for.20algebraic.20structures/ ?

view this post on Zulip Mario Carneiro (Oct 22 2020 at 18:39):

huh, I guess we need a run_parser command to make this easier

view this post on Zulip Adam Topaz (Oct 22 2020 at 18:40):

There must be some tactic unit that takes a parser and runs it no?

view this post on Zulip Adam Topaz (Oct 22 2020 at 18:54):

I have absolutely no idea what I'm doing... Can I make this work?

@[user_command]
meta def add_thing (_ : interactive.parse $ lean.parser.tk "add_thing") : lean.parser unit :=
do s  lean.parser.ident,
  lean.parser.emit_code_here (to_string s)

view this post on Zulip Reid Barton (Oct 22 2020 at 18:57):

import tactic.core

@[user_command]
meta def add_thing (_ : interactive.parse $ lean.parser.tk "add_thing") : lean.parser unit :=
do s  lean.parser.ident,
  lean.parser.emit_code_here (to_string s)
.

add_thing «#check 5»

view this post on Zulip Adam Topaz (Oct 22 2020 at 18:57):

Oh, the . is necessary?

view this post on Zulip Reid Barton (Oct 22 2020 at 18:58):

Well add_thing isn't a user command until the declaration ends, and if add_thing is not a user command then writing it will not end the declaration.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 18:58):

import tactic.basic

open tactic lean.parser interactive interactive.types
@[user_command] meta def run_parser_cmd (_ : parse $ tk "run_parser") : lean.parser unit :=
do e  lean.parser.pexpr 0,
  e  tactic.to_expr e,
  p  eval_expr (lean.parser unit) e,
  p.

run_parser emit_code_here "def foo := 1"

#print foo

view this post on Zulip Reid Barton (Oct 22 2020 at 18:59):

You could also put any other command in between.

view this post on Zulip Adam Topaz (Oct 22 2020 at 18:59):

Like I said, I really had no idea what I was doing. That's the first piece of meta code I've even tried to write.

view this post on Zulip Reid Barton (Oct 22 2020 at 18:59):

I don't know if it's what you intended but I'm amused at the idea of writing entire Lean definitions inside «...».

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:00):

oh, you are using ident quoting? That's an interesting way to get highlighting

view this post on Zulip Adam Topaz (Oct 22 2020 at 19:00):

It's not highlighting in vscode

view this post on Zulip Reid Barton (Oct 22 2020 at 19:01):

it doesn't give the correct highlighting in emacs though, does it work well in ...

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:01):

it also doesn't work with newlines apparently

view this post on Zulip Reid Barton (Oct 22 2020 at 19:01):

ok well at least it works in Zulip! :octopus:

view this post on Zulip Reid Barton (Oct 22 2020 at 19:01):

oh, no newlines is bad

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:01):

run_parser emit_code_here «
  def foo := 1
»
-- error: illegal character in escaped identifier

view this post on Zulip Reid Barton (Oct 22 2020 at 19:03):

I don't suppose there's a parser for an entire top-level command?

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:03):

this also doesn't seem to work:

run_parser emit_code_here "
  def foo := 1
"

something funny happens when the last " is not indented

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:03):

there is

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:03):

command_like

view this post on Zulip Reid Barton (Oct 22 2020 at 19:03):

can you get the source string out?

view this post on Zulip Reid Barton (Oct 22 2020 at 19:04):

meta constant command_like : parser unit

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:04):

no, it executes on the spot

view this post on Zulip Reid Barton (Oct 22 2020 at 19:04):

doesn't seem entirely helpful

view this post on Zulip Reid Barton (Oct 22 2020 at 19:04):

ah, I see

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:04):

it's actually the way emit_code_here works

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:05):

it's just with_input command_like

view this post on Zulip Reid Barton (Oct 22 2020 at 19:05):

It would be slick if instead of doing any quoting at all like foo "def ...", you could just write foo def ...

view this post on Zulip Eric Wieser (Oct 22 2020 at 19:05):

Anyone have any idea why the faithful_has_coe_to_fun a little ways above didn't work? It seems unfortunate to have to resort to code generation to define basic stuff about morphisms, where we don't have to do so for structures

view this post on Zulip Adam Topaz (Oct 22 2020 at 19:06):

Eric Wieser said:

Anyone have any idea why the faithful_has_coe_to_fun a little ways above didn't work? It seems unfortunate to have to resort to code generation to define basic stuff about morphisms, where we don't have to do so for structures

I think it has to do with the @[ext] attribute itself.

view this post on Zulip Reid Barton (Oct 22 2020 at 19:06):

Do you mean the error about ext?

view this post on Zulip Reid Barton (Oct 22 2020 at 19:06):

ext expects the lemmas to have a certain form, kind of like simp

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:07):

hom is a variable, not a constant

view this post on Zulip Eric Wieser (Oct 22 2020 at 19:08):

Ah, so we'd need code generation at least for populating ext attributes

view this post on Zulip Reid Barton (Oct 22 2020 at 19:08):

Or we could change how ext works. But I think doing code generation is preferable anyways.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:10):

yeah, right now this string interpolation approach seems better than alternatives, even for the more complex use cases with a variable number of operations

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:10):

in fact it might not even be horrible looking if you use format!

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:10):

which I don't find enough uses for

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:12):

run_parser do
  let foo := "bar",
  emit_code_here (format!"
    def {foo} := 1
    ").to_string

#print bar

view this post on Zulip Adam Topaz (Oct 22 2020 at 19:18):

Does lean have something like python's multiline strings with """?

view this post on Zulip Adam Topaz (Oct 22 2020 at 19:19):

Or can I just write multiline strings with "?

view this post on Zulip Adam Topaz (Oct 22 2020 at 19:19):

Cool. It's strange about the indentation of ", in Mario's comment above.

view this post on Zulip Adam Topaz (Oct 22 2020 at 19:21):

Looks like it's about the final newline.
E.g. this works

def str : string :=
"
def foo := 1
def bar := 2"

run_parser emit_code_here str

view this post on Zulip Adam Topaz (Oct 22 2020 at 19:21):

But this doesn't (or at least it looks like run_parser loops forever)

def str : string :=
"
def foo := 1
def bar := 2
"

run_parser emit_code_here str

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:25):

run_parser PR'd in #4745

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:26):

run_parser emit_code_here "\n" -- loops

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:27):

run_parser do with_input command_like "\n", pure () -- no loop

view this post on Zulip Adam Topaz (Oct 22 2020 at 19:27):

I guess we could make a new function emit_code_here' which removes trailing newlines

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:28):

Oh I see:

meta def emit_code_here : string  lean.parser unit
| str := do left  emit_command_here str,
            if left.length = 0 then return ()
            else emit_code_here left

this has no termination condition

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:29):

It should check that left.length < str.length

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:38):

#4746

view this post on Zulip Patrick Massot (Oct 22 2020 at 19:38):

Already failing CI...

view this post on Zulip Mario Carneiro (Oct 22 2020 at 19:47):

I don't always test my code, but when I do, I do it in production.

-- Mario's shirt

view this post on Zulip Mario Carneiro (Oct 22 2020 at 20:28):

Hm, I wasn't really planning on using run_parser to actually parse something in the source, but it is possible:

run_parser do -- 4
  tk ".",
  e  texpr,
  (to_expr e >>= eval_expr  >>= trace)
.
2 + 2

view this post on Zulip Mario Carneiro (Oct 22 2020 at 20:30):

unfortunately parsers can't parse command keywords like def so this isn't quite what reid was looking for

view this post on Zulip Adam Topaz (Oct 22 2020 at 20:57):

This is fun!

def monoid_stuff : list (string × nat) := [("mul",2),("one",0)]

def mk_op_str_aux (s : string) : nat  string
| nat.zero := s
| (nat.succ n) := s ++ " → " ++ (mk_op_str_aux n)

def mk_op_str (nn : string) (s : string) (n : nat) : string := nn ++ " : " ++ mk_op_str_aux s n

def mk_class_str_aux (nn : string) : list (string × nat)  string
| list.nil := ""
| (list.cons hd tl) := "\n( " ++ mk_op_str hd.1 nn hd.2 ++ " )" ++ mk_class_str_aux tl

def mk_class_str (class_name : string) : list (string × nat)  string :=
λ ls, "class " ++ class_name ++ " (α : Type*) :=" ++ mk_class_str_aux "α" ls

run_parser emit_code_here (mk_class_str "raw_monoid" monoid_stuff)

#print raw_monoid

view this post on Zulip Adam Topaz (Oct 22 2020 at 21:11):

Ah, but I get a "deep recursion" error if I try to define a typeclass with a 1000010000-ary operation.

view this post on Zulip Adam Topaz (Oct 22 2020 at 21:12):

36793679-ary operations are okay though

view this post on Zulip Reid Barton (Oct 22 2020 at 21:13):

Well, hopefully Lean 4 will let us supoport 3680-ary operations

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:32):

It's a bit slow for some reason, but this works:

def monoid_stuff : list (string × nat) := [("mul",10000),("one",0)]

def arity (α : Type*) : nat  Type*
| nat.zero := α
| (nat.succ n) := α  arity n

meta def mk_class_str_aux (s : string) : list (string × nat)  string
| list.nil := ""
| (list.cons (nn, n) tl) :=
  (format!"\n({nn} : arity {s} {to_string n})").to_string ++ mk_class_str_aux tl

meta def mk_class_str (class_name : string) : list (string × nat)  string :=
λ ls, "class " ++ class_name ++ " (α : Type*) :=" ++ mk_class_str_aux "α" ls

run_parser emit_code_here (mk_class_str "raw_monoid" monoid_stuff)

#print raw_monoid

view this post on Zulip Adam Topaz (Oct 22 2020 at 21:34):

Oh interesting. So the the deep recursion is only a problem when you generate a large string, and not when you generate a long type expression

view this post on Zulip Adam Topaz (Oct 22 2020 at 21:34):

This arity type is in mathlib somewhere...

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:35):

no, the deep recursion isn't for the string, it's for the parsing of the notation A -> A -> A -> ... -> A

view this post on Zulip Adam Topaz (Oct 22 2020 at 21:35):

Oh ok

view this post on Zulip Adam Topaz (Oct 22 2020 at 21:35):

docs#arity

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:35):

although I think that you can also get into deep recursion trouble when constructing the strings too

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:36):

or at least quadratic behavior

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:37):

you should probably stick to the iterated arrows instead of arity though, since it requires unfolding at point of use

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:38):

Ooh, I had another idea...

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:48):

def monoid_stuff : list (string × nat) := [("mul",10000),("one",0)]

meta def arity (α : pexpr) (n : nat) : tactic unit :=
do α  to_expr α,
  tactic.exact $ (expr.pi `_x binder_info.default α)^[n] α

meta def mk_class_str_aux (s : string) : list (string × nat)  string
| list.nil := ""
| (list.cons (nn, n) tl) :=
  "\n(" ++ nn ++ " : by arity ```(" ++ s ++ ") " ++ to_string n ++ ")" ++ mk_class_str_aux tl

meta def mk_class_str (class_name : string) : list (string × nat)  string :=
λ ls, "class " ++ class_name ++ " (α : Type*) :=" ++ mk_class_str_aux "α" ls

run_parser emit_code_here (mk_class_str "raw_monoid" monoid_stuff)

#print raw_monoid

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:49):

it times out, unfortunately. I think it's getting stuck somewhere in the aux defs of the structure

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:52):

it's a metametametaprogram

view this post on Zulip Adam Topaz (Oct 22 2020 at 21:53):

That's cool, even just to be able to write

def foo := by arity ```() 3
#print fo

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:54):

it makes the parser's job easier here, since there are no long chains in the source text

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:55):

I think lean still has to go through them all when dealing with the exprs later in elaboration and typechecking

view this post on Zulip Adam Topaz (Oct 22 2020 at 21:57):

def foo := by arity ```() 24525

Lean is happy with that, but not with 2452624526.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 21:59):

to be fair, if you have a structure with a 24526-ary operation then perhaps you would rather generalize to n-ary

view this post on Zulip Adam Topaz (Oct 22 2020 at 23:36):

Ping @Colter MacDonald


Last updated: May 15 2021 at 23:13 UTC