List.subperm_append_left should have longer name

Stream: batteries

[Malvin Gattinger]

I just stumbled upon this. Shouldn't docs#List.subperm_append_left in batteries rather be called List.append_subperm_append_left, analogous to docs#List.append_sublist_append_left in Init? And then the following could be added, the analogue of docs#List.sublist_append_left :thinking:

import Batteries.Data.List.Perm

theorem List.subperm_append_left' (l₁ l₂ : List α) : l₁.Subperm (l₁ ++ l₂) := by
  induction l₁
  · simp
  case cons head tail IH =>
    exact (subperm_cons head).mpr IH

(And the same for ..._right.)

[Ruben Van de Velde]

Yes, that seems sensible. I'd try to get the rename in before the next version bump middle of the month, and then add the new ones after

[Malvin Gattinger]

Cool, thank you!

[Malvin Gattinger]

A maybe related question: I noticed that aesop often does not find simple proofs like exact List.Subperm.trans h1 h2, even though exact? found these in most cases. Are there some annotations missing to let aesop use lemmas like this?

And similarly, why is docs#List.Subperm.refl marked with @[refl] but not with @[simp], in contrast to docs#List.Sublist.refl :thinking:

[Robin Arnez]

or have this new one be called List.subperm_left_append (and maybe also List.sublist_left_append)?
Edit: or List.left_subperm_append / List.left_sublist_append?

[Ruben Van de Velde]

In lean 3, simp would try theorems tagged with @[refl] in more places, if I understand correctly. Adding @[simp] as well is sort of a workaround for that change, but one that I'd support

[Ruben Van de Velde]

(To clarify, I'm not a decision maker for anything related to Batteries)