Zulip Chat Archive

Stream: mathlib4

Topic: Data.List.Sublists mathlib4#1494

Johan Commelin (Jan 13 2023 at 08:07):

What's the deal with sublistsAux_1 being moved and such?

Johan Commelin (Jan 13 2023 at 08:08):

Can someone explain this commit https://github.com/leanprover-community/mathlib4/pull/1494/commits/82bf12a2727213acf872bae48d4d6cec7656a1d3 to me?

Jihoon Hyun (Jan 13 2023 at 08:13):

There was a TODO at Data.List.Defs which says to move sublistsAux1 when ported.
So I just moved sublistsAux1 to Data.List.Sublists.
Also I couldn't find any occurances of sublists'Aux or sublists'_aux, so removed all theorems which uses it in the statement.

Mario Carneiro (Jan 13 2023 at 08:14):

FYI, this function will eventually be moved to std and redefined in terms of arrays, but I think it is best to wait until the work on Data.List dies down before doing that, so that mathlib isn't affected

Johan Commelin (Jan 13 2023 at 08:17):

@Mario Carneiro So you suggest to revert the move for now?

Johan Commelin (Jan 13 2023 at 08:17):

Also, was sublists'_aux something from core that hasn't been ported yet?

Mario Carneiro (Jan 13 2023 at 08:18):

I think it doesn't really matter, do whatever gets stuff working acceptably

Ruben Van de Velde (Jan 13 2023 at 08:19):

I think sublists'_aux existed in mathlib3, but sublists'Aux isn't particularly related

Mario Carneiro (Jan 13 2023 at 08:19):

My guess is that mathlib only needs the "naive" definition of sublists (I think this is list.sublists) and can skip all the aux stuff and sublists' which is about performance optimization of the function which is no longer applicable (lean 4 performance optimization looks completely different)

Johan Commelin (Jan 13 2023 at 08:20):

Ok, so all the stuff that @Jihoon Hyun commented out can remain commented out.

Mario Carneiro (Jan 13 2023 at 08:21):

actually we might still need sublists and sublists', since they are actually different functions, they use a different convention for how to collate the results as little vs big endian

Johan Commelin (Jan 13 2023 at 08:25):

But sublists' still exists.

Johan Commelin (Jan 13 2023 at 08:25):

So that's fine

Chris Hughes (Jan 13 2023 at 08:33):

Both sublists and sublists' are already defined in terms of arrays

Chris Hughes (Jan 13 2023 at 08:34):

sublistsAux was just to help me prove theorems

Mario Carneiro (Jan 13 2023 at 08:37):

one of the sublists definitions has a neat recursive definition which you want to use for reasoning, that one should be the main definition so it's a defeq and the fancy definition should be a csimp lemma

Last updated: Dec 20 2023 at 11:08 UTC