Lists of blocks indexed by a natural-number range

Facts about (List.range n).flatMap f and (List.range n).reverse.flatMap f: the list of blocks f 0, …, f (n - 1), in increasing or decreasing order.

Main results

• List.isChain_flatMap_range, List.isChain_flatMap_reverse_range: nonempty chained blocks, each linked to the next one, form a chain.
• List.head?_flatMap_range, List.getLast?_flatMap_range, List.head?_flatMap_reverse_range, List.getLast?_flatMap_reverse_range: the first and last entries come from the first and last nonempty end blocks.

theorem List.isChain_flatMap_range {α : Type u_1} {R : α → α → Prop} {f : ℕ → List α} {n : ℕ} (hne : ∀ (a : ℕ), a < n → f a ≠ []) (hblock : ∀ (a : ℕ), a < n → IsChain R (f a)) (hlink : ∀ (a : ℕ), a + 1 < n → ∀ (x : α), x ∈ (f a).getLast? → ∀ (y : α), y ∈ (f (a + 1)).head? → R x y) : IsChain R (flatMap f (range n))

Nonempty chains indexed by 0, …, n - 1, each linked to the next, form a chain.

theorem List.isChain_flatMap_reverse_range {α : Type u_1} {R : α → α → Prop} {f : ℕ → List α} {n : ℕ} (hne : ∀ (a : ℕ), a < n → f a ≠ []) (hblock : ∀ (a : ℕ), a < n → IsChain R (f a)) (hlink : ∀ (a : ℕ), a + 1 < n → ∀ (x : α), x ∈ (f (a + 1)).getLast? → ∀ (y : α), y ∈ (f a).head? → R x y) : IsChain R (flatMap f (range n).reverse)

Nonempty chains indexed by n - 1, …, 0, each linked to the previous, form a chain.

theorem List.head?_flatMap_range {α : Type u_1} {f : ℕ → List α} {n : ℕ} (hn : 0 < n) (h : f 0 ≠ []) : (flatMap f (range n)).head? = (f 0).head?

With a nonempty first block, the blocks in increasing order start with its head.

theorem List.getLast?_flatMap_range {α : Type u_1} {f : ℕ → List α} {n : ℕ} (hn : 0 < n) (h : f (n - 1) ≠ []) : (flatMap f (range n)).getLast? = (f (n - 1)).getLast?

With a nonempty last block, the blocks in increasing order end with its last entry.

theorem List.head?_flatMap_reverse_range {α : Type u_1} {f : ℕ → List α} {n : ℕ} (hn : 0 < n) (h : f (n - 1) ≠ []) : (flatMap f (range n).reverse).head? = (f (n - 1)).head?

With a nonempty block n - 1, the blocks in decreasing order start with its head.

theorem List.getLast?_flatMap_reverse_range {α : Type u_1} {f : ℕ → List α} {n : ℕ} (hn : 0 < n) (h : f 0 ≠ []) : (flatMap f (range n).reverse).getLast? = (f 0).getLast?

With a nonempty block 0, the blocks in decreasing order end with its last entry.