enumerate nonempty lists

Stream: Is there code for X?

[Rob Lewis]

Is there a function like def flatten {ι : Type*} (f : ℕ → {l : list ι // l ≠ []}) : ℕ → ι or similar? Given a sequence of nonempty lists, it should enumerate the elements of the lists in order.

[Yakov Pechersky]

Where n is the n-th element of the lists, when they've all be concatenated and sorted?

[Rob Lewis]

Sorry, "in order" is ambiguous there. I mean "in the order they appear." So if f 0 = [a, b], f 1 = [c], f 2 = [a, d, c], ..., I want the outpu to be a, b, c, a, d, c, ...

[Rob Lewis]

No sorting needed.

[Rob Lewis]

The nth element of the infinite concatenation

[Yaël Dillies]

I feel like you shoudn't require the lists to be nonempty. Then what you're asking for is roughly docs#list.join composed with docs#list.nth, but there's still a gap.

[Patrick Johnson]

docs#list.join is for (finite) lists of lists, but the question is about nat -> list, which is infinite. Also, if lists are allowed to be empty, then for some number the result may be undefined.

I wrote this definition (untested):

import tactic
open nat
open list

def f₁ {α : Type*} (f : ℕ → {l : list α // l ≠ []}) (i : ℕ) : {l : list α // l ≠ []} :=
dite ((f 0).1.length = 1) (λ h, f i.succ)
(λ h, ite (i = 0) ⟨tail (f 0).1, begin
  have h₁ := (f 0).2,
  cases (f 0).val with x xs,
  { exact (h₁ rfl).elim },
  { dsimp at h, rw [add_left_eq_self, length_eq_zero] at h, exact h },
end⟩ (f i))

def f₂ {α : Type*} (xs : {l : list α // l ≠ []}) : inhabited α :=
by { cases xs with xs h, cases xs with x xs, exact (h rfl).elim, use x }

def flatten {α : Type*} : (ℕ → {l : list α // l ≠ []}) → ℕ → α
| f 0 := @head α (f₂ (f 0)) (f 0).1
| f (succ n) := flatten (f₁ f) n

[Rob Lewis]

If the lists aren't nonempty, such a function may not exist: I can define f : ℕ → list empty but not f : ℕ → empty.

[Rob Lewis]

Thanks, Patrick, that's clever -- gotta process that one a bit.

[Yaël Dillies]

Patrick Johnson said:

docs#list.join is for (finite) lists of lists, but the question is about nat -> list, which is infinite. Also, if lists are allowed to be empty, then for some number the result may be undefined.

I am aware of that :smile:

[Rob Lewis]

Bedtime for me, but a challenge if you're in the mood to test your definition :smile:

import tactic
open nat
open list

def f₁ {α : Type*} (f : ℕ → {l : list α // l ≠ []}) (i : ℕ) : {l : list α // l ≠ []} :=
dite ((f 0).1.length = 1) (λ h, f i.succ)
(λ h, ite (i = 0) ⟨tail (f 0).1, begin
  have h₁ := (f 0).2,
  cases (f 0).val with x xs,
  { exact (h₁ rfl).elim },
  { dsimp at h, rw [add_left_eq_self, length_eq_zero] at h, exact h },
end⟩ (f i))

def f₂ {α : Type*} (xs : {l : list α // l ≠ []}) : inhabited α :=
by { cases xs with xs h, cases xs with x xs, exact (h rfl).elim, use x }

def flatten' {α : Type*} : (ℕ → {l : list α // l ≠ []}) → ℕ → α
| f 0 := @head α (f₂ (f 0)) (f 0).1
| f (succ n) := flatten' (f₁ f) n

def flatten {α : Type*} (f : ℕ → list α) (hf : ∀ n, f n ≠ []) : ℕ → α :=
flatten' (λ k, ⟨f k, hf k⟩)

-- `f` collects elements of `α` that have the same value under the map `v`,
-- and collects them ordered by this value
variables {α β : Type*} [linear_order β] {v : α → β}
  (f : ℕ → list α)
  (hf : ∀ n, f n ≠ [])
  (hv1 : ∀ n, ∀ i j ∈ f n, v i = v j)
  (hv2 : ∀ n, ∀ i ∈ f n, ∀ j ∈ f (n+1), v i < v j)
include hv1 hv2

lemma flatten_le (n : ℕ) : v (flatten f hf n) ≤ v (flatten f hf (n+1)) :=
sorry

[Yaël Dillies]

Note that you could also define the analogous thing for $\Z$, so maybe this should have a $\N$-specific name.

[Patrick Johnson]

@Rob Lewis Thank you for the nice challenge! Here you go:

lemma flatten_le (n : ℕ) : v (flatten f hf n) ≤ v (flatten f hf (n+1)) :=
begin
  revert f, induction n with n hn; rintro f hf hv1 hv2,
  { rw [flatten, flatten', flatten', flatten', f₁], dsimp, split_ifs,
    { dsimp, apply le_of_lt, apply hv2;
      { apply head_mem_self, apply hf }},
    { apply le_of_eq, dsimp, apply hv1,
      { apply head_mem_self, apply hf },
      { apply mem_of_mem_tail, apply head_mem_self,
        have h₁ := hf 0, cases f 0 with x xs,
        { apply (h₁ rfl).elim },
        { rw tail, simp at h, rw length_eq_zero at h, exact h }}}},
  { generalize hf' : (λ n, (f₁ (λ n, ⟨f n, hf n⟩) n).1) = f',
    have hf' : ∀ n, f' n ≠ [],
    { intro k, subst f', dsimp, rw f₁,
      split_ifs with h h₁; dsimp at h ⊢;
      try { apply hf },
      { have h₂ := hf 0, cases f 0 with x xs,
        { exact (h₂ rfl).elim },
        { dsimp at *, simp at h, rw length_eq_zero at h, exact h }}},
    have hn₁ : v (flatten f' hf' n) ≤ v (flatten f' hf' (n + 1)),
    { apply hn; clear hn n,
      { rintro n i j hi hj, subst f', dsimp at hi hj, rw f₁ at hi hj,
        split_ifs at hi hj with h h₁; dsimp at hi hj;
        try { apply hv1 _ _ _ hi hj },
        { apply hv1 0 _ _; apply mem_of_mem_tail; assumption }},
      { rintro n i hi j hj, subst f', dsimp at hi hj, dunfold f₁ at hi hj,
        split_ifs at hi hj with h₁ h₂; dsimp at *,
        { apply hv2; assumption },
        { apply hv2,
          { apply mem_of_mem_tail, assumption },
          { cases h₂ }},
        { cases h₂ },
        { replace hi := mem_of_mem_tail hi, apply hv2,
          { assumption },
          { rw h at hj, assumption }},
        { apply hv2; assumption }}},
    have h₁ : ∀ n, flatten f hf (n + 1) = flatten f' hf' n,
    { intro k, rw [flatten, flatten, flatten'], congr, funext i, subst f',
      dsimp, simp_rw f₁, split_ifs with h₁ h₂; refl },
    rw [h₁, h₁], exact hn₁ },
end

[David Wärn]

You can also implement flatten using streams:

import data.stream.init

def head_of_ne_nil {α} : Π {ls : list α}, ls ≠ [] → α
| [] h        := (h rfl).elim
| (a :: ls) _ := a

/-- `flatten_aux (ls, s₀ :: s₁ :: ...) = ls ++ₛ s₀ ++ₛ s₁ ++ ...` -/
def flatten_aux {α} : list α × stream { ls : list α // ls ≠ []} → stream α :=
stream.corec' $ λ p, match p with
  | (a :: ls, s) := (a, ls, s)
  | ([], s)      := (head_of_ne_nil s.head.2, s.head.val.tail, s.tail)
  end

def flatten {α} (s : stream { ls : list α // ls ≠ [] }) : stream α := flatten_aux ([], s)

[Rob Lewis]

Fantastic, thanks @David Wärn !

[Rob Lewis]

And thanks again @Patrick Johnson :smile: