List.take_join

Stream: Is there code for X?

[Martin Dvořák]

Has https://github.com/user7230724/lean-projects/blob/master/src/list_take_join/main.lean been ported to Lean 4?
Or do we have something that subsumes it?

Statement in Lean 4: https://github.com/madvorak/chomsky/blob/3baa6086d94c2e717b3fa1e88af0025b39f1befa/Chomsky/Utilities/ListUtils.lean#L79

[Vlad]

import Mathlib

open List

theorem take_join_of_lt {α : Type*} {L : List (List α)} {n : ℕ}
(h₁ : n < L.flatten.length) : ∃ m k : ℕ, ∃ mlt : m < L.length,
k < (L.get ⟨m, mlt⟩).length ∧ L.flatten.take n =
(L.take m).flatten ++ (L.get ⟨m, mlt⟩).take k := by
  simp at h₁; have h₂ : ∃ m, n < (L.take m |>.map length).sum; use L.length; simpa
  generalize hm : Nat.find h₂ = m; have h₃ := Nat.find_spec h₂
  have h₅ := @Nat.find_min' (H := h₂) _ _; rw [hm] at h₃ h₅
  have h₄ := @h₅ L.length $ by simp at h₁ ⊢; exact h₁
  cases m; simp at h₃; rename_i m; rw [Nat.succ_le_iff] at h₄
  specialize @h₅ m; simp at h₅; use m; simp [h₄]
  generalize hr : (L.map length |>.take m).sum = r at h₅
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h₅; use n
  simp [take_add, ←take_sum_flatten, hr]
  have h₂ : L = L.take m ++ L.drop m; simp
  rw [h₂] at h₃; simp [-take_append_drop] at h₃; rw [take_append] at h₃; simp at h₃
  rw [take_take] at h₃; simp [hr] at h₃; rw [min_eq_left_of_lt h₄] at h₃; simp at h₃
  rw [take_one] at h₃; simp [getElem?_eq_getElem h₄] at h₃; use h₃
  rw [←drop_take_succ_flatten_eq_getElem, hr, take_sum_flatten, take_add,
    flatten_append, drop_append]; simp [hr]
  simp [show L.flatten.drop r = (L.drop m).flatten by subst hr; apply drop_sum_flatten,
    ←show L.flatten.take r = (L.take m).flatten by subst hr; apply take_sum_flatten]
  generalize hM : L.drop m = M
  have h₇ : 0 < M.length; simpa [←hM]
  have h₈ : M.take 1 = [M[0]]; simp [←hM, take_one, head?_drop]
  simp [h₈]; rw [show L[m] = M[0] by simp [←hM]] at h₃
  cases M; simp at h₈; simp at h₃; simp [le_of_lt h₃]

[Kim Morrison]

Impressive, but it's not super useful to prove theorems like this without developing API.

A better approach here is:

• Prove theorems characterising the List.scanl operation defined in Batteries, e.g. at least getElem_scanl and take_scanl.
• State and prove the missing theorems List.getElem?_flatten and getElem_flatten, which will rewrite L.flatten[i] = L[j][k], where j is something of the form I.findIdx f, where I is the list of partial sums of lengths (constructed via scanl).
• Prove L.flatten.take i = (L.take j).flatten ++ (L[j]?.getD []).take k, where j and k are values defined using let in the statement of the theorem (similarly, using findIdx). This theorem should hold for any i, without requiring an inequality. It is proved just using extensionality via the theorems above.
• An existential statement like above is then easy to extract (but maybe isn't even needed).

[Kim Morrison]

batteries#1498 contains the lemmas about scanl.

[Kim Morrison]

lean#11113 has some relevant missing lemmas about List.findIdx.

[Chris Henson]

Just double checking, batteries#1498 does have some overlap with Mathlib.Data.List.Scan, should some/all of that file move to Batteries?

[Kim Morrison]

Hmm, not the lemmas I would have written, I guess. I'll certainly delete the identical ones from Mathlib afterwards.

[Chris Henson]

Not sure how used this is, I just had a vague memory and loogled. Some are definitely subsumed by your proofs and could be written in terms of them and/or deprecated.

Maybe better organizationaly if the corresponding scanr changes are made at the same time?

[Martin Dvořák]

Vlad said:

[proof]

Thanks a lot!
https://github.com/madvorak/chomsky/commit/d2b2774f32184fb6129f79471f010077c0ff4b7f
If you want to give me your full name, I'll give you credit under your full name.

[Vlad]

https://gist.github.com/vllladd/14b5074a58cbdeeff12718925f4eb3c7

[Kim Morrison]

I did some of this in branch, but I almost forgot about it. I've put it up as a draft PR at batteries#1511. If anyone wants to adopt that would be lovely.

[Alfredo Moreira-Rosa]

Just filling the sorry with proof or there more work to do (like adding more lemmas) ?

[Kim Morrison]

I'd be happy with the sorries filled.

[Alfredo Moreira-Rosa]

Ok, i'll take some time to see if i can put this to completion.