Over eager simplification of Array.drop

Stream: general

[cmlsharp]

simp will simplify (Array.drop xs n).toListto List.take (as.size - n) (List.drop n xs.toList). This seems wrong to me. The List.take there is totally superfluous, and this has made some proofs involving Array.extract/Array.drop a bit more annoying than they need to be for me. I think perhaps Array.drop_eq_extract and Array.take_eq_extract should not be simp lemmas (the analogous lemmas for lists are not), and Array.toList_take and Array.toList_drop (which do not currently exist) should be added and made simp lemmas. MWE:

example : (Array.drop as n).toList = List.take (as.size - n) (List.drop n as.toList) := by
  simp

[cmlsharp]

GitHub issue: https://github.com/leanprover/lean4/issues/12299

[Kim Morrison]

Hmm... the intention here had been to eliminate Array.drop and Array.take from all simp normal forms, by directly simplifying them to extract, so we can just write the API for that instead.

This does have some bad consequences, as you point out.

Would it work if we made drop_eq_extract and take_eq_extract lower priority simp lemmas, and also provide some basics like toList_take and toList_drop?

[Eric Wieser]

Adding

@[simp]
theorem List.take_eq_self_of_le (l : List α) (n : ℕ) (hn : l.length ≤ n) : l.take n = l := by simpa

-- or
-- @[simp] alias ⟨_, take_eq_self_of_le⟩ := List.take_eq_self_iff

to make things confluent also helps

[Eric Wieser]

(which is to say; I would support both lowing the priority, adding toList_take, and adding that lemma for confluence)

[Robin Arnez]

Well, with the current state of things, removing drop_eq_extract and take_eq_extract doesn't actually do anything because both drop and take are also abbrevs. So we'd at least need to convert it into a @[inline] def.

[cmlsharp]

Hmm... the intention here had been to eliminate Array.drop and Array.take from all simp normal forms, by directly simplifying them to extract, so we can just write the API for that instead

Can I ask why this is desirable for Array when it is (presumably) not for List? E.g. why doesn't List.take/drop also simplify to List.extract?

[Wrenna Robson]

Kim Morrison said:

Hmm... the intention here had been to eliminate Array.drop and Array.take from all simp normal forms, by directly simplifying them to extract, so we can just write the API for that instead.

This does have some bad consequences, as you point out.

Would it work if we made drop_eq_extract and take_eq_extract lower priority simp lemmas, and also provide some basics like toList_take and toList_drop?

To be quite honest I don't understand why this is particularly desirable. At least conceptually I don't think of drop and take as the same kind of operation - indeed to an extent they are kind of "paired" operations, right? Like for List we have List.splitAt - conceptually I do kind of think of drop and take as the two components that output from that. I don't think we have Array.splitAt... but we could. The point is, to calculate Array.drop xs n and Array.take xs n only takes one costly operation if you are doing it efficiently.

[Wrenna Robson]

We don't really provide much API for splitAt, mind - it is easier to just have the API for take and drop. Why you would want to involve extract I have never quite understood.

[Wrenna Robson]

Of course it's weird for Array I suppose - my understanding is that because of how arrays are stored, in some ways dropping from the end is more natural, but then you have to reverse it... I guess this is why you just use extract.

[cmlsharp]

I agree that 'drop' and 'take' are, at least in my mental model, atomic operations (on both list and array). I really don't want 'simp' converting them to some more general operation