Grouping consecutive list elements into pairs

This file provides the elementary list operation that groups consecutive elements into disjoint ordered pairs, dropping a possible final unpaired element.

Main results

• List.pairAdjacent groups consecutive elements into pairs.
• List.prod_map_pairAdjacent recovers a mapped product from the pairs of an even-length list.
• List.length_pairAdjacent computes the number of pairs.

def List.pairAdjacent {α : Type u} : List α → List (α × α)

Group consecutive elements into disjoint ordered pairs, dropping a final unpaired element.

Equations

• (a :: b :: l).pairAdjacent = (a, b) :: l.pairAdjacent
• x✝.pairAdjacent = []

theorem List.prod_map_pairAdjacent {α : Type u} {β : Type v} [Monoid β] (f : α → β) (l : List α) : Even l.length → (map (fun (p : α × α) => f p.fst * f p.snd) l.pairAdjacent).prod = (map f l).prod

Multiplying the mapped entries of each consecutive pair recovers the mapped product of an even-length list.

@[simp]

theorem List.length_pairAdjacent {α : Type u} (l : List α) : l.pairAdjacent.length = l.length / 2

The number of consecutive pairs in a list is half its length, rounded down.