Data.List.Basic

Stream: mathlib4

[Scott Morrison]

This thread can serve to coordinate work on Data.List.Basic. Please write here if you would like to claim a section of it to work on (and then "unclaim" when you finish work).

[Johan Commelin]

I just pushed the mathlib 3 source header

[Siddhartha Gadgil]

Trying reverseRecOn

[Johan Commelin]

Fixed line 1036

[Johan Commelin]

I'll claim 1037 -- 1105

[Siddhartha Gadgil]

Siddhartha Gadgil said:

Trying reverseRecOn

done and pushed

[Johan Commelin]

I'm working on bidirectionalRec

[Johan Commelin]

done

[Johan Commelin]

From std:

/- @[refl] -/ @[simp] theorem Sublist.refl : ∀ l : List α, l <+ l
  | [] => .slnil
  | a :: l => (Sublist.refl l).cons₂ a

@Mario Carneiro I guess this commented-out @[refl] is intentional? It breaks a proof in Data.List.Basic.

[Mario Carneiro]

It wasn't legal at the time, in fact it probably still isn't because the refl attribute is in mathlib

[Mario Carneiro]

You can add the refl attribute in the corresponding mathlib file

[Johan Commelin]

I guess that file is Data.List.Basic?

[Johan Commelin]

I had to manually replace sublist.cons2 with Sublist.cons₂. Is that something that mathport ought to do?
(This was in the instance decidableSublist.)

[Johan Commelin]

I did a global replace index_of -> indexOf.

[Johan Commelin]

Oops! That messed up #align statements. Will fix.

[Johan Commelin]

Pushed a better replace

[Scott Morrison]

I think we need to add an #align for sublist.cons2. (Because it is defined in Std.)

[Siddhartha Gadgil]

Done map_take. In general I am working from the end and trying termination errors.

[Siddhartha Gadgil]

globally replacing erasep with eraseP

[Siddhartha Gadgil]

Sorry that was a mistake which I undid. The first terms of align should ha erasep

[Siddhartha Gadgil]

That said a lot of fixes are this replacement and finding that stuff is already in Std

[Mario Carneiro]

I recall doing at least one pass over data.list.basic and porting everything I could to std, so I would expect there to be a lot of #align-only code here

[Siddhartha Gadgil]

Yes, most of the work is correcting cases, finding stuff is then in Std and keeping only the align.
I am also adding attributes where things are marked [simp]. Is that correct? Some seemed not to be simp in Std

[Johan Commelin]

theorem indexOf_cons (a b : α) (l : List α) :
    indexOf a (b :: l) = if a = b then 0 else succ (indexOf a l) :=

this used to be rfl but it no longer is.
Is that a problem?

[Mario Carneiro]

let's assume not until proven otherwise

[Kevin Buzzard]

In the Data.Fin.Basic thread we see that 0 % b = 0 used to be rfl and no longer is, and all that happens is that a bunch of proofs break and have to be fixed manually. Does that count as a problem?

[Mario Carneiro]

that one is going to be more annoying (it's not that 0 % b = 0 was rfl but rather that the definition of 0 : Fin n changed from 0 to 0 % n), but I don't see much of an option without making fin have two different OfNat instances, which is also a headache

[Thomas Murrills]

Cleaning up lines 1300 - 1500 right now (mostly good, a few spread-out errors)

[Thomas Murrills]

Moving onto 1500 - 1600

[Thomas Murrills]

Do we rename or delete ext? There's already List.ext from Std, but that one uses get? and this one uses nth

[Thomas Murrills]

The get? version seems to make the subsequent theorems throw errors

[Thomas Murrills]

I've temporarily renamed it ext_nth in keeping with ext_le below it.

[Mario Carneiro]

is get? different from nth?

[Mario Carneiro]

List.nth is identical to List.get?. It should be deleted and #aligned

[Mario Carneiro]

other definitions in Mathlib.Init.Data.List.Basic that are duplicates:

• List.map₂-> List.zipWith
• List.mapWithIndex -> List.mapIdx
• List.findIndex -> List.findIdxₓ (prop -> bool)
• List.updateNth -> List.set
• List.bor -> List.or
• List.band -> List.and
• List.repeat -> List.replicateₓ (argument order)
• List.init -> List.dropLast

[Thomas Murrills]

A lot (100+) of theorems use nth somewhere in their name; is it better to use nth as an alias for get? or to ctrl+F and change all of the theorem names to reference get? (Likewise for the other ones with significantly different names which might be referenced in theorems, I guess, but it's probably not as big a deal)

[Thomas Murrills]

Fixing errors in indexOf section (~1250 -1300)

[Mario Carneiro]

mathport is the new ctrl-F

[Thomas Murrills]

the theorems I'm talking about are all in Data.List.Basic already, not future files

[Thomas Murrills]

also I'm just asking a stylistic question, not saying it's difficult...like, do we want lots of theorem names to have _get?_ in the middle? or do we want to use nth in those names by having an alias

[Thomas Murrills]

Ok, ported the indexOf section—as mentioned, the previous proofs were very short (e.g. rfl), whereas these new ones require diving into findIdx.go. I reordered a couple so I could use them as components. I tried to keep them more elementary than fancy, e.g. "string of rewrites" instead of simp—hopefully they can be golfed nonetheless, though. But in the meantime, they work! :)

[Scott Morrison]

Ideally there are no more nths at all. We're replacing it with get?.

[Thomas Murrills]

Cleaning up nth_injective and indexOf_cons_ne

[Johan Commelin]

I pushed a tiny bit more progress

[Chris Hughes]

Scott Morrison said:

Ideally there are no more nths at all. We're replacing it with get?.

I'm not entirely sure about this decision. Maybe leave the nthLes there for now and tidy stuff up after mathlib is ported. It's easier to fix all in one go and minimize design changes while porting?

[Scott Morrison]

Sorry, ignore me, that was an completely stupid thing for me to say. Of course we're not changing nth to get?.

[Scott Morrison]

I thought this was just a rename. :shrug:

[Mario Carneiro]

but it is a rename?

[Mario Carneiro]

nth is gone, long live get?. nthLe is still around though

[Mario Carneiro]

also to address @Thomas Murrills 's naming question re: get? in the middle of theorem names: yes, it's just treated like any other name. You get names like get?_of_nthLe and so on

[Thomas Murrills]

If we switch every nth to get?, why would we not also switch nthLe to get?Le? isn’t nthLe meant to conjure up nth? And if there is no nth…

[Mario Carneiro]

there isn't an le in nthLe either, it's a bad name

[Mario Carneiro]

(I think I named it, but I don't know what I was thinking)

[Mario Carneiro]

but until we're ready to rename it it should just stay as is

[Thomas Murrills]

i'll take' on the section Take' (~ 2540 - 2570) right now

[Eric Wieser]

Isn't docs#list.nth_le ultimately obsolete in favor of docs4#List.get, but we're delaying the refactor till after the port?

[Chris Hughes]

I vote yes

[Eric Wieser]

(unless someone wants to backport it to mathlib3 first, but it doesn't seem very important)

[Mario Carneiro]

there are some advantages to having them be separate arguments for induction proofs, but it can probably be marginalized to just some specialized situations

[Thomas Murrills]

if it won't be used much but is still useful occasionally, get'? or getLT?

[Thomas Murrills]

also I'm noticing that take' doesn't actually match with takeD—the new takeD allows any element to be specified as a default, whereas take required [Inhabited α]. should we:

• correspondingly generalize the theorems by adding that explicit value as an (implicit?) argument to the theorems in take
• just use default and maintain that these theorems require [Inhabited α]

[Thomas Murrills]

std seems to have chosen the first option when it absorbed take'_nil as takeD_nil, so I'll do that as well if there aren't any objections.

[Thomas Murrills]

Hmm...in general, in cases like this, is it worth putting porting note:s in /-- ... -/ docstrings so that people who are porting can see that we've e.g. changed the arguments required on mouseover?

[Thomas Murrills]

done (without docstrings) (I'll change it back to using [Inhabited α] if I made the wrong choice)

[Mario Carneiro]

The inhabited-taking version should be named takeI

[Thomas Murrills]

Do we want to use that instead? Or have both? Currently take' is aligned with takeD. Is that a mistake?

[Thomas Murrills]

or wait. takeI doesn't exist yet—you're talking about in the future

[Mario Carneiro]

What is the type of take'?

[Thomas Murrills]

Π {α : Type u} [_inst_1 : inhabited α], ℕ → list α → list α

[Mario Carneiro]

then it should be renamed to takeI

[Mario Carneiro]

and not aligned to takeD which is a different function

[Thomas Murrills]

Alright, that align is in Data.List.Defs (and the definition of take' was there too). So...I'll make a PR on a separate branch to fix Data.List.Defs and define takeI there?

[Thomas Murrills]

Hang on. Mathlib.Data.List.Defs currently depends on Mathlib.Data.List.Basic?? Not the other way around?

[Thomas Murrills]

I suppose I'll define takeI in Data.List.Basic until I figure out what's going on.

[Mario Carneiro]

That import is definitely an error

[Mario Carneiro]

the import of Data.List.Chain seems to be the issue

[Mario Carneiro]

don't work around an ad hoc port issue by adding more ad hoc port issues

[Mario Carneiro]

when in doubt, copy the structure of mathlib3

[Thomas Murrills]

the import of Data.List.Chain seems to be the issue

and in turn Data.List.Pairwise which imports Data.List.Basic directly

[Thomas Murrills]

Ok, here's the current state of things.

[Thomas Murrills]

Data.List.Defs has a Chain section where it defines decidableChain, decidableChain'. This needs chain_cons and is the only reason Data.List.Chain is imported.

[Thomas Murrills]

However, things were different in mathlib3: chain_cons was defined in data.list.defs, not data.list.chain.

[Thomas Murrills]

As far as I can tell, data.list.defs did not depend on data.list.chain in mathlib3. This is a new dependency introduced in mathlib4.

[Thomas Murrills]

In fact, I think it was the other way around: data.list.chain depended on data.list.defs.

[Mario Carneiro]

Mario Carneiro said:

when in doubt, copy the structure of mathlib3

[Mario Carneiro]

Move everything where it is supposed to be and everything will be resolved

[Thomas Murrills]

Alright, I'll try my best—the imports are totally different for lots of things in mathlib3, it's not just that one file. (For example, seems like old data.list.basic depended on data.list.defs but doesn't anymore, so that'll be a new import in Data.List.Basic.)

[Arien Malec]

The definition of take' (through mathlib3port was

def take' : ∀ n, List α → List α
  | 0, l => []
  | n + 1, l => l.head :: take' n l.tail

The misalignment was my mistake based on an assumption that D = Default (although I got the naming convention right elsewhere)

The import of Data.List.Chain was required to port the defs for the Chain section -- as noted, moving that whole section to Data.List.Chain will remove the dependency (but will also be a divergence from mathlib3)./

[Thomas Murrills]

I did the reverse: move chain_cons to Data.List.Defs. This is how it was in mathlib3

[Thomas Murrills]

mathlib4#1118

[Thomas Murrills]

All other chain definitions previously in data.list.defs are now in std, so it was the only one that needed to be moved :)

[Thomas Murrills]

Still trying to make it build, though. Is there some reason the dependency needs to flow from Data.List.Chain -> Data.List.Defs now?

[Arien Malec]

No idea... Data.List.Chain existed before the port of Data.List.Defs

[Arien Malec]

Fortunately, the only reference to takeD is in Data.List.Defs so removing the align and adding takeI should be fine.

[Arien Malec]

I think it would be better to define takeI as:

def takeI : ∀ n, List α → List α
  List.takeD default

[Thomas Murrills]

I think we're on the same page—I defined it in the PR as

def takeI [Inhabited α] (n : Nat) (l : List α) : List α :=
  takeD n l default

[Thomas Murrills]

Ok, neat; mathlib4#1118 is good to go, and should fix things.

[Thomas Murrills]

it worked :) now fixing 2600 - 2620

[Thomas Murrills]

Did foldrRecOn etc.; had to work around the code generator not handling List.rec for now. I'll double-check the IH's I manually gave tomorrow; it's late :)

[Johan Commelin]

List.mem_cons is in Std. What is the canonical place to add #align list.mem_cons_iff List.mem_cons?

[Johan Commelin]

The first error in Data.List.Basic is on

theorem nthLe_insertNth_self (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length)
    (hn' : n < (insertNth n x l).length := by rwa [length_insertNth _ _ hn, Nat.lt_succ_iff]) :

with error message

invalid auto tactic, identifier is not allowed

on the length_insertNth

[Johan Commelin]

How should we do these auto tactics?

[Johan Commelin]

Johan Commelin said:

List.mem_cons is in Std. What is the canonical place to add #align list.mem_cons_iff List.mem_cons?

I see, it is already on L21. But it hasn't been used in the rest of the file yet.

[Mario Carneiro]

Johan Commelin said:

List.mem_cons is in Std. What is the canonical place to add #align list.mem_cons_iff List.mem_cons?

The canonical place to put an #align is in the same place and ordering as the original mathlib3 definition, regardless of whether the lean 4 definition is in mathlib4 or upstream. If the definition is in mathlib4, it should come immediately before the #align unless there is a reason it has to be moved elsewhere

[Mario Carneiro]

Johan Commelin said:

The first error in Data.List.Basic is on

theorem nthLe_insertNth_self (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length)
    (hn' : n < (insertNth n x l).length := by rwa [length_insertNth _ _ hn, Nat.lt_succ_iff]) :

with error message

invalid auto tactic, identifier is not allowed

on the length_insertNth

How did that happen? Mathport will not generate autoparams like that

[Johan Commelin]

No idea... but that's the code I found on the branch

[Johan Commelin]

Mario Carneiro said:

The canonical place to put an #align is in the same place and ordering as the original mathlib3 definition, regardless of whether the lean 4 definition is in mathlib4 or upstream. If the definition is in mathlib4, it should come immediately before the #align unless there is a reason it has to be moved elsewhere

But somehow a lot of #aligns are missing, when the definitions ended up in Std.

[Johan Commelin]

I think Data.List.Basic is quite a mess. E.g., apparently those autoparams are also garbage that shouldn't roll out of mathport.

[Johan Commelin]

And because of all the missing #aligns there are many names that need tweaking and fixing.

[Johan Commelin]

@Mario Carneiro Do you think you could take a look? And maybe use some oneshot magic trickery to get this file to behave?

[Johan Commelin]

Roughly 2900 lines are now error free. But there's another 2400 lines in that file.

[Mario Carneiro]

Was the port botched in some way? Do we need to start over from mathport output?

[Johan Commelin]

I dunno. Throwing away 3000 lines of porting effort also feels sad.

[Mario Carneiro]

well it's fine if they are good code, I'm not sure exactly what the problem is here

[Mario Carneiro]

I'll take a look, data.rat.order needs a review

[Mario Carneiro]

For anyone else who is working on this file: I'm currently doing major brain surgery on it, you might want to wait until afterwards and hopefully you already committed any changes you had

[Mario Carneiro]

Mario Carneiro said:

Johan Commelin said:

The first error in Data.List.Basic is on

theorem nthLe_insertNth_self (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length)
    (hn' : n < (insertNth n x l).length := by rwa [length_insertNth _ _ hn, Nat.lt_succ_iff]) :

with error message

invalid auto tactic, identifier is not allowed

on the length_insertNth

How did that happen? Mathport will not generate autoparams like that

I ran across this issue while going over mathport's data.list.basic output again. I see what happened now: in lean 3 the proof looked like this:

@[simp] lemma nth_le_insert_nth_self (l : list α) (x : α) (n : ℕ)
  (hn : n ≤ l.length) (hn' : n < (insert_nth n x l).length :=
    by rwa [length_insert_nth _ _ hn, nat.lt_succ_iff]) :
  (insert_nth n x l).nth_le n hn' = x :=

That is, there is an opt param whose value is given by a by block. In lean 4 this syntax (that is, (x : ty := by tac) has been reappropriated for auto params (in which := by is a composite keyword), and if you want an opt param whose value is a by block you have to write (x : ty := (by tac)) instead. Pinging @Sebastian Ullrich since this is another parenthesizer bug that isn't about precedence

[Sebastian Ullrich]

Mario Carneiro said:

another parenthesizer bug that isn't about precedence

Yes, and because of that I don't think the general parenthesizer framework should solve this, or at least I don't see any reasonable way short of some crazy grammar analysis. But this specific case (and I already forgot the other one) is easy enough to fix. https://github.com/leanprover/lean4/commit/96ccf192e8a5fe216bbc63c688a06b2032bd14f5

[Mario Carneiro]

I don't think we should have crazy grammar analysis, I think we should have special case parenthesizers which handle this stuff

[Mario Carneiro]

the other one is (try foo); bar turning into try foo; bar

[Mario Carneiro]

Okay, I'm releasing my hold on Data.List.Basic. I did the first 2900 lines, plus renaming stuff for the part that still hasn't been touched yet.

[Thomas Murrills]

fixing 2900-2970

[Thomas Murrills]

Hmm, foldrM_cons was moved to std, but now requires an instance of LawfulMonad which was not previously assumed for the Data.List.Basic version of it.

How should we proceed? Make all of the downstream theorems also depend on a LawfulMonad instance, or use a different name?

[Mario Carneiro]

yes, the downstream theorems are almost certainly assuming LawfulMonad anyway

[Mario Carneiro]

it's not true without the assumption anymore

[Thomas Murrills]

working on splitAt_eq_take_drop

[Thomas Murrills]

splitOnP now takes a Bool-valued predicate instead of a Prop-valued one—we're rewriting everything related to splitOnP to match, not keeping a separate Prop-predicate version of splitOnP, right? just checking.

[Scott Morrison]

Seems reasonable. You'll want to #align with an ₓ.

[Chris Hughes]

Having trouble proving things about the new definition of splitOnP. Can't even seem to prove the equation lemmas for splitOnP.go

[Thomas Murrills]

I'll try to work on it rn (~3000 - 3220)

[Thomas Murrills]

Can we safely get rid of theorems of the form split_on_p_aux*? It seems like they're only used to help prove facts about splitOnP, and it might be easier to prove those from scratch due to the new plumbing in splitOnP. (I can't find any occurrences for each of them anywhere else in mathlib3.)

[Chris Hughes]

I think so

[Thomas Murrills]

Ok, I think I’ve broken through the worst of the go’s—whew! haven’t committed because I’ve got a bunch of false starts lying around, and don’t want to subject anyone else to the mess :) I’ll resume in a couple hours and try to get a clean commit in for this section.

[Reid Barton]

Is the general consensus for this file that lemmas about e.g. filter should take as argument p : α → Bool and not α → Prop?

[Reid Barton]

It seems to be really hard to apply versions with Prop in situations where you have Bool, because the p in filter p is not actually the variable like it appears

[Mario Carneiro]

I think the lemmas should use A -> Bool iff the function does

[Mario Carneiro]

it doesn't make any sense for them not to match

[Reid Barton]

And if the lemma also involves an if about p x where p : A -> Bool, then should it be changed to bif?

[Reid Barton]

Seems like maybe sticking with if is better, since if is used in a lot of other places?

[Mario Carneiro]

We may or may not want two versions in those cases. I think if is handled a bit better than bif, which is really just syntax for cond and doesn't get special handling by the split/split_ifs tactics

[Thomas Murrills]

finished splitOnP! moving onto lookmap—it seems to be the same sort of go-wrangling.

[Thomas Murrills]

Oh, I wanted to ask: I proved a couple of thorny theorems about modifyLast that dive into modifyLast.go, but didn’t wind up needing them. Though, they fit pretty well in Data.List.Basic and are natural equalities to want (modifyLast f (l ++ [a]) = l ++ [f a] and modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂ given l₂ ≠ []).

Should I leave them in their own new section as they are now, or save them til after the port/discard them?

[Johan Commelin]

Lean complains on L4128 (the first error in the file)

#align list.erasep List.erasePₓ -- prop -> bool
-- list.erasep has already been aligned (to List.erasep)

[Johan Commelin]

Can we just erase it?

[Johan Commelin]

I guess so. The align is done in Data.List.Defs.

[Johan Commelin]

Pushed a minifix

[Thomas Murrills]

I think something else should be done: it's currently aligned to something that doesn't change prop to Bool

/-- `erasep p l` removes the first element of `l` satisfying the predicate `p`. -/
def erasep (p : α → Prop) [DecidablePred p] : List α → List α
  | [] => []
  | a :: l => if p a then l else a :: erasep p l
#align list.erasep List.erasep

[Thomas Murrills]

Note the name: erasep vs. eraseP, the latter of which is in Std and makes the switch from Prop to Bool

[Johan Commelin]

First error is now on L4313. Second error on L4729. Getting close!

[Thomas Murrills]

I think erasep should be deleted from Data.List.Defs

[Johan Commelin]

Aha, that sounds sensible!

[Johan Commelin]

Feel free to revert my minifix

[Thomas Murrills]

I'm not seeing your minifix on github; I'll just fix it as-is and hope it goes through :sweat_smile:

[Thomas Murrills]

What's the canonical place for #aligns between Lean 3 core and Std? (Here the relevant aligns were ball_cons to forall_mem_cons and ball_nil to forall_mem_nil, all in the namespace list/List)

[Mario Carneiro]

in the relevant mathlib4 file

[Mario Carneiro]

ball_cons is in init.data.list.lemmas, so the #align ball_cons forall_mem_cons should go in Mathlib.Init.Data.List.Lemmas (in the same order as the lean 3 declarations)

[Thomas Murrills]

I see, I didn't realize Lean core had that sort of correspondence with mathlib—makes sense now that I do :)

[Reid Barton]

I don't want to get anyone too excited but Data.List.Basic now compiles without errors.

[Reid Barton]

What now?

[Reid Barton]

I read through the whole file and it seems to be in pretty good shape actually. Some remaining questions:

• Should we align list.repeat and List.replicate?
• Are we really adding instance : Monad List?
• We don't want to keep these enormous "dubious translation" comments, do we?
• Do we need to add dozens of xs, e.g. on all the lemmas about filter? How?

[Reid Barton]

I think the answers to the first and third ones are "no".

[Ruben Van de Velde]

Repeat and replicate have the arguments in the opposite order, so I think not

[Eric Wieser]

The suggestion elsewhere was to backport the argument reorder

[Reid Barton]

Right. So presumably that doesn't require any action in mathlib4 for now

[Eric Wieser]

If we backport first then we can align and not have to merge things later

[Reid Barton]

Hmm, I'd almost rather not backport/align at all

[Mario Carneiro]

We can also not backport and #align with x. The resulting files will not compile because they will e.g. call List.replicate with arguments in the wrong order, but that might be good enough for manual porting work, since we've probably already seen most of the uses of this function in this file

[Reid Barton]

Ad Monad List, does attribute [local instance] work in Lean 4?

[Reid Barton]

Maybe we can just make a def and locally make it an instance to state its API lemmas and wherever else the instance is needed in mathlib

[Kevin Buzzard]

class foo (α : Type) where

def bar : foo Nat := { }

#synth foo Nat -- fails

attribute [local instance] bar

#synth foo Nat -- works

Looks like it's OK

[Mario Carneiro]

We could make Monad List a scoped instance

[Johan Commelin]

I fixed the non simp_nf linting errors

[Reid Barton]

Scoped to List, or to something more specific (ListMonad?)?

[Johan Commelin]

-- somewhere in Std
@[simp] theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
  cases l <;> rfl

Is this a good simp lemma? Should getLastD be the snf?

[Johan Commelin]

What should we do with lint errors like

#check @List.mem_map_swap /- Left-hand side simplifies from
  (y, x) ∈ List.map Prod.swap xs
to
  Exists fun a ↦ Exists fun b ↦ (a, b) ∈ xs ∧ b = y ∧ a = x
using
  simp only [List.mem_map', Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
Try to change the left-hand side to the simplified term!
 -/

[Johan Commelin]

Should we

1. remove the @[simp] and do nothing else
2. remove the @[simp] and create a new simp-lemma with a simplified LHS as instructed by the linter
3. just modify the statement, as instructed

[Johan Commelin]

I've fixed all the trivial linting errors. The remaining ones are variations on :up:

[Reid Barton]

I guess maybe the first question is what is the situation in mathlib 3? Does the LHS not simplify with mathlib's simp set?

[Johan Commelin]

I think Std introduces a bunch of simp lemmas that diverge from the mathlib3 simpset

[Mario Carneiro]

Both of the examples look like reasonable simp lemmas. List.map_mem_swap less so

[Mario Carneiro]

getLastD has better defeqs than getLast

[Jihoon Hyun]

Hello, I'd like to contribute to Data.List.Basic or its successor. I could find that there were intense discussions on linting Data.List.Basic, and the only work left is about linting. As I'm still kind of new here, I'd like to ask if I can start porting the successor like Data.List.TFAE, or it should start after every linting errors are corrected.

[Mario Carneiro]

You can always work on a file which is still in PR stage, you just need to make your PR dependent on that one. If it's still giving linting errors then you will most likely see those same errors in CI for your branch, so it won't be able to be merged either until the other one is fixed and your branch merges the fixes in, but otherwise it shouldn't be a blocker to preparing the PR

[Johan Commelin]

For the record, this is what's left here:

-- Found 4 errors in 25005 declarations (plus 59456 automatically generated ones) in mathlib with 13 linters

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.Data.List.Basic
#check List.get_insertNth_self.{u} /- Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
 -/
#check List.nthLe_insertNth_self.{u} /- Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
 -/
#check List.init_cons_of_ne_nil.{u_1} /- simp can prove this:
  by simp only [_private.Std.Data.List.Init.Lemmas.0.List.dropLast._eq_3]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
 -/
#check List.attach_map_coe'.{u, v} /- Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
 -/

[Johan Commelin]

These seem to be final end-bosses.

[Thomas Murrills]

Does it make sense to delete init_cons_of_ne_nil and #noalign it? It seems it can replaced in a simp call by simp only [dropLast] now. Or do we align it with the equation for dropLast, if that's possible?

[Mario Carneiro]

if the theorem is still true I don't see any reason to remove it

[Thomas Murrills]

ok! so just remove @[simp] from it?

[Mario Carneiro]

is dropLast marked as simp?

[Thomas Murrills]

ah...no, it's not.

[Thomas Murrills]

however, example {α : Type _} {x : α} {l : List α} (_ : l ≠ []) : (x :: l).dropLast = x :: l.dropLast := by simp works and the trace shows that it uses a dropLast definition lemma (@List.dropLast._eq_3, as expected)

[Thomas Murrills]

(maybe I don't know the appropriate way to check if dropLast is marked as simp...all I know is @[simp] doesn't appear above the declaration)

[Gabriel Ebner]

There's an attribute [simp] dropLast in std4.

[Thomas Murrills]

(ah, ok, I see how it works now!)

[Johan Commelin]

Gabriel Ebner said:

There's an attribute [simp] dropLast in std4.

Wait, I thought those weren't global? Am I mistaken?

[Reid Barton]

attribute [simp] is global, but attribute [local simp] and attribute [-simp] are not

[Johan Commelin]

oooh! I see. That's not what I expected.

[Yaël Dillies]

That certainly is a bit confusing. Is there a hover or something else that will teach people this?

[Johan Commelin]

This file is now passing the linter! Thanks @Mario Carneiro

[Johan Commelin]

What do we do here?

theorem nthLe_reverse' (l : List α) (n : ℕ) (hn : n < l.reverse.length) (hn') :
    l.reverse.nthLe n hn = l.nthLe (l.length - 1 - n) hn' := by
  rw [eq_comm]
  convert nthLe_reverse l.reverse n (by simpa) hn using 1
  simp
#align list.nth_le_reverse' List.nthLe_reverse'

theorem get_reverse' (l : List α) (n) (hn') :
    l.reverse.get n = l.get ⟨l.length - 1 - n, hn'⟩ := nthLe_reverse' ..

-- FIXME: prove it the other way around
attribute [deprecated get_reverse'] nthLe_reverse'

[Johan Commelin]

Note that the types don't line up:

#check nthLe_reverse'
-- List.nthLe_reverse'.{u} {α : Type u} (l : List α) (n : ℕ) (hn : n < length (reverse l))
--   (hn' : length l - 1 - n < length l) : nthLe (reverse l) n hn = nthLe l (length l - 1 - n) hn'
#check get_reverse'
-- List.get_reverse'.{u} {α : Type u} (l : List α) (n : Fin (length (reverse l))) (hn' : length l - 1 - ↑n < length l) :
--   get (reverse l) n = get l { val := length l - 1 - ↑n, isLt := hn' }

[Johan Commelin]

So I'm questioning whether the attribute [deprecated] is even correct.

[Johan Commelin]

Ooh, I guess this is just a very general thing about nthLe vs get?

[Johan Commelin]

I'm not sure we should have deprecated nthLe in that case. Sounds like something that should better be done after the port.

[Johan Commelin]

We're doing too many refactors on the fly.

[Johan Commelin]

I fixed two of the FIXMEs in the file. What remains is very non-urgent.

[Johan Commelin]

I'm going to kick this on the queue.

[Johan Commelin]

Ooh, @Chris Hughes was faster (-;

[Henrik Böving]

done :octopus:

[Mario Carneiro]

Johan Commelin said:

We're doing too many refactors on the fly.

deprecated is explicitly not a refactor. It is a marker which is used to prepare the library for a future refactor. Importantly, the original lemmas still exist and still have the types required for downstream stuff.

[Mario Carneiro]

the nthLe refactor cannot proceed until we have at least the majority of code using nthLe available, which means it will not be removed / reassessed until after the port

[Mario Carneiro]

in general deprecated is being used when the replacement lemma is more than a little different, such that it would be too much to do the refactor on the fly

[Johan Commelin]

but the deprecated linter can be an annoying speedbump. Should we be lax about nolinting in that case?

[Mario Carneiro]

nolint doesn't work on the deprecated linter, since it's not a real linter but just a warning that is thrown up when you use a deprecated definition directly during elaboration. You have to use set_option linter.deprecated false to turn it off or else CI will complain

[Johan Commelin]

So should we be lax with that option?

[Mario Carneiro]

yes

[Mario Carneiro]

I mean it's a requirement in any case

[Johan Commelin]

Or you rewrite the proof... which can be tedious.

[Mario Carneiro]

for a theorem which mentions nthLe rewriting the proof isn't an option

[Johan Commelin]

sure, but I've seen examples where only the proof used deprecated decls.

[Johan Commelin]

I vote for allowing those during the port.

[Mario Carneiro]

for theorems which use nthLe internally but not in the statement, I will leave it up to the porter whether they want to try removing it or not

[Mario Carneiro]

leaving it alone is totally fine