list.join.take

Stream: Is there code for X?

[Martin Dvořák]

Is there a lemma for the following example?

example {α : Type} (l : list (list α)) (n : ℕ) :
  ∃ k q : ℕ, ∃ k_lt : k < l.length,
    l.join.take n = (l.take k).join ++ (l.nth_le k k_lt).take q :=
begin
  sorry,
end

I know about list.take_sum_join but I hope for something closer to my goal.

[Eric Wieser]

(docs#list.take_sum_join for reference)

[Eric Rodriguez]

(the list has to be nontrivial)

[Eric Wieser]

I think it would be better to state it without the existential

[Martin Dvořák]

On the outside, I don't care how k and q relate to length of respective parts. How would you state my lemma instead?

[Eric Wieser]

By directly computing the k you need

[Eric Wieser]

And putting that in the lemma statement

[Martin Dvořák]

At this point, I should probably prove my lemma and see whether I can easily extract a formula for k from it.

[Eric Wieser]

Something like

/-- Produces something akin to `(quotient, remainder)`, but unlike division the entry being subtracted is not the same each time -/
def nat.sub_list : ℕ → list ℕ → ℕ × ℕ
| n [] := (0, n)
| n (x :: xs) := if n < x then (0, n) else
  let r := nat.sub_list (n - x) xs in (r.1 + 1, r.2)

[Eric Wieser]

I guess this generalizes to tsub

[Patrick Johnson]

Proof

[Martin Dvořák]

Wow! Thanks a lot!

[Martin Dvořák]

Would you like to add it to mathlib? I can PR it if you want.

[Martin Dvořák]

I would also add something similar for list.drop.

[Patrick Johnson]

Feel free to PR it.

[Martin Dvořák]

OK, I will. Thanks a lot for your big help!!

[Martin Dvořák]

I would like to make it a tiny bit stronger by adding k < (l.nth_le m hh).length to:

lemma list.take_join {l : list (list α)} {n : ℕ} (h : l ≠ []) :
  ∃ (m k : ℕ) hh, l.join.take n = (l.take m).join ++ (l.nth_le m hh).take k

[Martin Dvořák]

(if we were to take all of the mth part, we would instead increment m)

[Martin Dvořák]

(I don't have a use for k < (l.nth_le m hh).length here, but I want to add this property to the list.drop version)

[Martin Dvořák]

Patrick Johnson said:

Proof

Is import tactic.induction redundant?

[Patrick Johnson]

Is import tactic.induction redundant?

Seems so.

I would like to make it a tiny bit stronger by adding k < (l.nth_le m hh).length

In that case you would also need n < l.join.length. Besides that, keep in mind that l may also contain empty lists.

[Martin Dvořák]

Oh! I overlooked that I would then have to take 0 elements from the non-existent l.lengthth list.

[Martin Dvořák]

Patrick Johnson said:

Feel free to PR it.

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/list_take_join.20into.20mathlib

[Martin Dvořák]

I think that instead of list.take_join_of_lt_length_join and list.take_join I will make one "export" lemma:

lemma list.take_join_of_lt {α : Type*} {l : list (list α)} {n : ℕ} (notall : n < l.join.length) :
  ∃ m k : ℕ, ∃ mlt : m < l.length, k < (l.nth_le m mlt).length ∧
    l.join.take n = (l.take m).join ++ (l.nth_le m mlt).take k :=
begin
  sorry
end

And similarly:

lemma list.drop_join_of_lt {α : Type*} {l : list (list α)} {n : ℕ} (notall : n < l.join.length) :
  ∃ m k : ℕ, ∃ mlt : m < l.length, k < (l.nth_le m mlt).length ∧
    l.join.drop n = (l.nth_le m mlt).drop k ++ (l.drop m).join :=
begin
  sorry
end

[Martin Dvořák]

[fixed an off-by-one error in the last statement]

[Patrick Johnson]

Adding k < (l.nth_le m mlt).length is easy. The m and k from the proof already satisfy it.

The proof has been updated.

[Martin Dvořák]

Thanks a lot! I'll finally proceed to PR it (when I attempted it first, I got lost in imports, but I'll work harder this time to resolve it).