lists

Stream: maths

[Yaël Dillies]

@Mario Carneiro, I'm about to write docstrings for lists. How should I understand the choice to make lists' α contain a copy of α (using atom)? Also, is the bool in there really meaning "this is a proper list, not an atom"?

[Mario Carneiro]

You should think of lists A as a kind of naive set theory, like you find in early discussions about \in and \subseteq. It is basically finite ZFA

[Mario Carneiro]

it's computable, so that you can evaluate stuff like {2, 3} \in {2, {2, 3}, 5}

[Mario Carneiro]

Indeed the bool in the underlying implementation is there to distinguish proper lists from list-or-atom

[Mario Carneiro]

It would have been a mutual inductive but the support for that in lean 3 isn't so great

[Mario Carneiro]

It was originally intended to be used for formalizing elementary set theory problems, back when @Kevin Buzzard was looking at formalizing his problem sheets and got stuck on questions about set theory

[Yaël Dillies]

But terms of lists A are ordered, right?

[Mario Carneiro]

I never got around to the quotient part, lists is just the substrate

[Yaël Dillies]

Ah okay, that makes more sense!

[Mario Carneiro]

you can take a quotient in much the same way as pSet / Set

[Yaël Dillies]

Yeah that's what I was expecting to see.

[Yaël Dillies]

And how should I explain the difference between lists' and lists?

[Mario Carneiro]

it would be nice to finish it at some point but the demand wasn't so high and it wasn't a high priority

[Mario Carneiro]

I think lists' is an implementation detail

[Yaël Dillies]

And why using the plural? You used a cap for pSet and Set.

[Mario Carneiro]

The reason for the distinction is that we don't want cons 1 2 to be well formed

[Yaël Dillies]

Aaah yeah

[Yaël Dillies]

Actually, isn't Set the usual notation for the category of sets?

[Yaël Dillies]

Would it make more sense if they were called zfc_set, zfc_pset, zfa_list, zfa_list'?

[Mario Carneiro]

I don't see a contradiction in the naming, the caps are since it is a higher order object containing all the sets at once, much like the category

[Mario Carneiro]

in fact I imagine you could also make it the category literally

[Yaël Dillies]

Well it will nameclash when people will want to define the category. But yeah stuff can be decided then.

[Mario Carneiro]

but keep in mind that these were all written a very long time ago (category theory was not in mathlib at all)

[Yaël Dillies]

Still I don't get lists. It's not the type of several lists

[Mario Carneiro]

most category stuff is in the category_theory namespace

[Yaël Dillies]

Ah okay, then I retract

[Mario Carneiro]

It's still a type constructor, like list, since it's parameterized over a base type of atoms

[Mario Carneiro]

it's the type of list-of-list-of-list... of A

[Yaël Dillies]

So the plural refers to the fact that elements of a list are themselves lists?

[Mario Carneiro]

except not really since it also allows mixed level objects like [1, [2, 3]]

[Mario Carneiro]

yeah

[Mario Carneiro]

it's lists all the way down :)

[Yaël Dillies]

Aaaah :scream:

[Kevin Buzzard]

Mario Carneiro said:

It was originally intended to be used for formalizing elementary set theory problems, back when Kevin Buzzard was looking at formalizing his problem sheets and got stuck on questions about set theory

At that time I was making the canonical error of saying "it says it like this in the book, therefore I need to make an exact copy of this somehow in Lean" (I didn't know anything about type theory at the time).

[Yaël Dillies]

Dumb question, what is the A in ZFA standing for?

[Kevin Buzzard]

Maybe "atoms"? Is this some theory with urelements?

[Yaël Dillies]

Hmm, yeah, maybe. The central object is

inductive {u} lists' (α : Type u) : bool → Type u
| atom : α → lists' ff
| nil : lists' tt
| cons' {b} : lists' b → lists' tt → lists' tt

[Mario Carneiro]

yes, this is ZF with "atoms" that are not sets. It is the perfect setting for talking about simple sets of natural numbers like {1, {2, 3}, 4}

[Mario Carneiro]

Kevin Buzzard said:

At that time I was making the canonical error of saying "it says it like this in the book, therefore I need to make an exact copy of this somehow in Lean" (I didn't know anything about type theory at the time).

I think this is only half of an error. You shouldn't exactly replicate the book, but you also shouldn't be too eager to simply drop an area or a kind of question just because it's not easy to formalize. That's the mentality that leads to formal mathematics only ever exploring stuff like finite combinatorics, lists, and natural numbers

[Yaël Dillies]

I now reached an alternate state of mind. All docstrings in this file now look like "does something to a list to make it a list" and now my brain can't access the meaning of "list" anymore :dizzy:

[Yaël Dillies]

All I see is a chain of four characters sounding funny together. list, list, list, lissst

[Ruben Van de Velde]

I can't let the opportunity to mention "semantic satiation" go by!

[Yaël Dillies]

Eheheh :wink:

[Yaël Dillies]

Here's #8967 for the vertigo-enjoyers.

[Kyle Miller]

If I understand it correctly, lists' and lists together are "compiling" the following (invalid) recursive definition as an inductive type:

def lists (α : Type*) := α ⊕ list (lists α)

The bool index in lists' is encoding which side of the sum something is. If this is correct, maybe mentioning it might help motivate things in the documentation.

In that case, it seems the goal for ZFA sets is to compile the following recursive definition:

def finsets (α : Type*) := α ⊕ finset (finsets α)

[Yaël Dillies]

Yes, you're absolutely right.

[Kyle Miller]

Hmm, this seems to execute very slowly:

inductive lists (α : Type*)
| atom : α → lists
| list : list lists → lists

[Yakov Pechersky]

Universe issue?

[Kyle Miller]

Don't think so. It seems like nested inductive types might just be slow for Lean to work out -- it generates a whole lot of auxiliary definitions, and it seems to be coming up with something along the lines of Mario's lists definition (haven't really confirmed that, though).

Lean doesn't allow the following, since it doesn't know how to eliminate the recursion:

inductive finsets (α : Type u)
| atom : α → finsets
| fs : finset finsets → finsets

[Mario Carneiro]

Kyle Miller said:

Hmm, this seems to execute very slowly:

inductive lists (α : Type*)
| atom : α → lists
| list : list lists → lists

It might be good to put this exact definition in the comment for lists and/or lists' as motivation