move Mathlib.Data.Prod.Basic to batteries

Stream: batteries

[Bulhwi Cha]

I want to prove the following theorem, List.commonPrefixWithRest_comm, but the function Prod.swap is in Mathlib.Data.Prod.Basic. Do you think it's worth moving the function and its lemmas to Lean's core library or Batteries?

namespace List

/-- Extract the longest common prefix of two lists, and the remainder of each list. -/
def commonPrefixWithRest [DecidableEq α] : (l₁ l₂ : List α) → List α × List α × List α
  | [], l₂ => ([], [], l₂)
  | l₁, [] => ([], l₁, [])
  | a₁::l₁, a₂::l₂ =>
    if a₁ = a₂ then
      Prod.map (a₁ :: ·) id (commonPrefixWithRest l₁ l₂)
    else
      ([], a₁ :: l₁, a₂ :: l₂)

theorem commonPrefixWithRest_comm [DecidableEq α] (l₁ l₂ : List α) :
    commonPrefixWithRest l₁ l₂ = Prod.map id Prod.swap (commonPrefixWithRest l₂ l₁) := by
  sorry

end List

[François G. Dorais]

That's an unexpected omission! Probably belongs in Lean core.

[Kim Morrison]

lean#5739

[Kim Morrison]

(commonPrefixWithRest should be made tail-recursive)

[Eric Wieser]

Kim Morrison said:

lean#5739

Is it appropriate to upstream these to batteries anyway in the meantime, rather than waiting 2-3 weeks until the next Lean release?

[Kim Morrison]

Yes, no problem. I'd be happy to hit merge on PRs doing that, but won't do it myself.

[Eric Wieser]

Perhaps there should be a Lean.Upstreamed folder in batteries for things that are already in lean, and have been backported? That would make your bumps just a matter of deleting everything in the directory

[Kim Morrison]

I don't think that's necessary for batteries. lake build quickly tells me what to delete.

[Bulhwi Cha]

Kim Morrison said:

(commonPrefixWithRest should be made tail-recursive)

François G. Dorais has already made its tail-recursive version. :big_smile:

https://github.com/leanprover-community/batteries/pull/994#discussion_r1802832306