List operations

TheoremList positions agree with values of an increasing map#✓fully proved

In a list along which f increases, position order agrees with value order.

theorem idxOf_lt_iff {α : Type*} [BEq α] [LawfulBEq α] {f : α → ℕ} {l : List α}
    (hl : l.Pairwise fun x y => f x < f y) {x y : α} (hx : x ∈ l) (hy : y ∈ l) :
    l.idxOf x < l.idxOf y ↔ f x < f y

TheoremPairwise relations on list products in lexicographic order#✓fully proved

The Cartesian product of two pairwise-related lists is pairwise-related in lexicographic order.

theorem Pairwise.product_lex {α β : Type*} {r₁ : α → α → Prop} {r₂ : β → β → Prop}
    {l₁ : List α} {l₂ : List β} (h₁ : l₁.Pairwise r₁) (h₂ : l₂.Pairwise r₂) :
    (l₁ ×ˢ l₂).Pairwise (Prod.Lex r₁ r₂)

TheoremStart position of a chunk in a split list#✓fully proved

A valid indexed chunk begins after the total length of the preceding chunks.

theorem getD_splitLengths {α : Type*} (xs : List α) (lengths : List ℕ) (fallback : List α)
    {i : ℕ} (hi : i < lengths.length) :
    (lengths.splitLengths xs).getD i fallback =
      (xs.drop (lengths.take i).sum).take lengths[i]

Used by 2

Used byNamed chunk lookup uses the first occurrence · Splitting a list at a repeated width

TheoremNamed chunk lookup uses the first occurrence#✓fully proved

Looking up a named chunk uses the first occurrence of its name.

theorem getD_splitLengths_map {ι α : Type*} [BEq ι] [LawfulBEq ι]
    (length : ι → ℕ) (names : List ι) (xs fallback : List α) {i : ι} (hi : i ∈ names) :
    ((names.map length).splitLengths xs).getD (names.idxOf i) fallback =
      (xs.drop ((names.map length).take (names.idxOf i)).sum).take (length i)

Uses 1

Proof usesStart position of a chunk in a split list

TheoremSplitting a list at a repeated width#✓fully proved

Splitting at a repeated width recovers the corresponding uniform chunk.

theorem getD_splitLengths_replicate {α : Type*} (width count i : ℕ)
    (xs fallback : List α) (hi : i < count) :
    ((List.replicate count width).splitLengths xs).getD i fallback =
      (xs.drop (i * width)).take width

Uses 1

Proof usesStart position of a chunk in a split list

TheoremEquality of uniformly split lists from equal block extracts#✓fully proved

Lists of the same uniform-block length are equal when every block extract agrees.

theorem eq_of_extract_mul_eq {α : Type*} (width count : ℕ) (xs ys : List α)
    (hxs : xs.length = count * width) (hys : ys.length = count * width)
    (h : ∀ i < count,
      xs.extract (i * width) (i * width + width) =
        ys.extract (i * width) (i * width + width)) :
    xs = ys

TheoremLength of a concatenation of equal-length lists#✓fully proved

Concatenating count lists of length width has length count * width.

theorem length_flatMap_range {α : Type*} (count width : ℕ) (blocks : ℕ → List α)
    (hblocks : ∀ i < count, (blocks i).length = width) :
    ((List.range count).flatMap blocks).length = count * width

Used by 1

Used byEvery equal-length list family is realized by its concatenation

TheoremExtracting a member from a uniform-width concatenation#✓fully proved

A uniform-width extract of a concatenated family recovers that family member.

theorem extract_flatMap_range {α : Type*} (count width : ℕ) (blocks : ℕ → List α)
    (hblocks : ∀ i < count, (blocks i).length = width) {i : ℕ} (hi : i < count) :
    ((List.range count).flatMap blocks).extract (i * width) (i * width + width) =
      blocks i

Used by 1

Used byEvery equal-length list family is realized by its concatenation

TheoremEvery equal-length list family is realized by its concatenation#✓fully proved

Every finite family of equal-length lists is realized by their concatenation.

theorem exists_length_eq_and_extract_eq {α : Type*} (width count : ℕ)
    (blocks : ℕ → List α) (hblocks : ∀ i < count, (blocks i).length = width) :
    ∃ xs : List α,
      xs.length = count * width ∧
        ∀ i < count, xs.extract (i * width) (i * width + width) = blocks i

Uses 2

Proof usesExtracting a member from a uniform-width concatenation · Length of a concatenation of equal-length lists

DefinitionInclusive first-hit prefix of a list#✓fully proved

The prefix through the first element satisfying p, including that element. If no element satisfies p, this is the whole list.

def takeThrough {α : Type*} (p : α → Bool) (xs : List α) : List α :=
  xs.take (xs.findIdx p + 1)

Used by 15

Used byInclusive first-hit prefix has a hit iff the list does · Inclusive first-hit prefix commutes with filter-map · First-witness fold over the inclusive first-hit prefix · Members of an inclusive first-hit prefix lie in the list · Accumulator-stopped prefix as a first-hit prefix of a scan · First-witness accumulator gives the inclusive first-hit prefix · Disjunction accumulator gives the inclusive first-hit prefix · Inclusive first-hit prefix of an append with no hit on the left · Inclusive first-hit prefix of an append with a hit on the left · Inclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix when the head is a hit · Inclusive first-hit prefix of a list with no hit · Inclusive first-hit prefix of the empty list · Inclusive first-hit prefix of a range of naturals · Inclusive first-hit prefix of a singleton

TheoremInclusive first-hit prefix of the empty list#✓fully proved

The inclusive first-hit prefix of an empty list is empty.

@[simp] theorem takeThrough_nil {α : Type*} (p : α → Bool) : takeThrough p [] = []

Uses 1 · Used by 5

Statement usesInclusive first-hit prefix of a list

Used byInclusive first-hit prefix has a hit iff the list does · Inclusive first-hit prefix commutes with filter-map · Accumulator-stopped prefix as a first-hit prefix of a scan · Inclusive first-hit prefix of a list with no hit · Inclusive first-hit prefix of a singleton

TheoremInclusive first-hit prefix when the head is a hit#✓fully proved

If the head satisfies the predicate, it is the whole inclusive first-hit prefix.

@[simp] theorem takeThrough_cons_of_pos {α : Type*} {p : α → Bool} {x : α}
    (h : p x = true) (xs : List α) : takeThrough p (x :: xs) = [x]

Uses 1 · Used by 8

Statement usesInclusive first-hit prefix of a list

Used byInclusive first-hit prefix has a hit iff the list does · Inclusive first-hit prefix commutes with filter-map · First-witness fold over the inclusive first-hit prefix · Accumulator-stopped prefix as a first-hit prefix of a scan · First-witness accumulator gives the inclusive first-hit prefix · Disjunction accumulator gives the inclusive first-hit prefix · Inclusive first-hit prefix of an append with a hit on the left · Inclusive first-hit prefix of a singleton

TheoremInclusive first-hit prefix when the head is not a hit#✓fully proved

If the head does not satisfy the predicate, the search continues through the tail.

@[simp] theorem takeThrough_cons_of_neg {α : Type*} {p : α → Bool} {x : α}
    (h : p x = false) (xs : List α) :
    takeThrough p (x :: xs) = x :: takeThrough p xs

Uses 1 · Used by 10

Statement usesInclusive first-hit prefix of a list

Used byInclusive first-hit prefix has a hit iff the list does · Inclusive first-hit prefix commutes with filter-map · First-witness fold over the inclusive first-hit prefix · Accumulator-stopped prefix as a first-hit prefix of a scan · First-witness accumulator gives the inclusive first-hit prefix · Disjunction accumulator gives the inclusive first-hit prefix · Inclusive first-hit prefix of an append with no hit on the left · Inclusive first-hit prefix of an append with a hit on the left · Inclusive first-hit prefix of a list with no hit · Inclusive first-hit prefix of a singleton

TheoremInclusive first-hit prefix of a singleton#✓fully proved

A singleton is its own inclusive first-hit prefix.

@[simp] theorem takeThrough_singleton {α : Type*} (p : α → Bool) (x : α) :
    takeThrough p [x] = [x]

Uses 4

Statement usesInclusive first-hit prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix when the head is a hit · Inclusive first-hit prefix of the empty list

TheoremMembers of an inclusive first-hit prefix lie in the list#✓fully proved

Every member of an inclusive first-hit prefix belongs to the source list.

theorem mem_of_mem_takeThrough {α : Type*} {p : α → Bool} {xs : List α} {x : α}
    (h : x ∈ takeThrough p xs) : x ∈ xs

Uses 1

Statement usesInclusive first-hit prefix of a list

TheoremInclusive first-hit prefix of a list with no hit#✓fully proved

If no element satisfies the predicate, the inclusive first-hit prefix is the whole list.

theorem takeThrough_eq_self_of_any_eq_false {α : Type*} {p : α → Bool} {xs : List α}
    (h : xs.any p = false) : takeThrough p xs = xs

Uses 3

Statement usesInclusive first-hit prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix of the empty list

TheoremInclusive first-hit prefix of an append with a hit on the left#✓fully proved

Once the left list has a hit, appending another list does not change the prefix.

theorem takeThrough_append_of_any_eq_true {α : Type*} {p : α → Bool} {xs : List α}
    (h : xs.any p = true) (ys : List α) : takeThrough p (xs ++ ys) = takeThrough p xs

Uses 3

Statement usesInclusive first-hit prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix when the head is a hit

TheoremInclusive first-hit prefix of an append with no hit on the left#✓fully proved

If the left list has no hit, the prefix contains all of it and continues into the right list.

theorem takeThrough_append_of_any_eq_false {α : Type*} {p : α → Bool} {xs : List α}
    (h : xs.any p = false) (ys : List α) :
    takeThrough p (xs ++ ys) = xs ++ takeThrough p ys

Uses 2

Statement usesInclusive first-hit prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit

TheoremInclusive first-hit prefix has a hit iff the list does#✓fully proved

The inclusive first-hit prefix has a hit exactly when the source list has one.

theorem any_takeThrough {α : Type*} (p : α → Bool) (xs : List α) :
    (takeThrough p xs).any p = xs.any p

Uses 4

Statement usesInclusive first-hit prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix when the head is a hit · Inclusive first-hit prefix of the empty list

TheoremInclusive first-hit prefix of a range of naturals#✓fully proved

On range n, the prefix ends one past the first hit, or at n if there is no hit.

theorem takeThrough_range (q : Nat → Bool) (n : Nat) :
    takeThrough q (range n) =
      range (match (range n).find? q with | some i => i + 1 | none => n)

Uses 1

Statement usesInclusive first-hit prefix of a list

TheoremInclusive first-hit prefix commutes with filter-map#✓fully proved

Filtering selected elements from an inclusive prefix commutes with taking the corresponding inclusive prefix of the selected elements.

theorem filterMap_takeThrough {α β : Type*} (sel : α → Option β) (p : β → Bool)
    (xs : List α) :
    (takeThrough (fun x => (sel x).any p) xs).filterMap sel =
      takeThrough p (xs.filterMap sel)

Uses 4

Statement usesInclusive first-hit prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix when the head is a hit · Inclusive first-hit prefix of the empty list

DefinitionAccumulator-stopped inclusive prefix of a list#✓fully proved

The prefix through the first element after whose update the accumulator satisfies stop, including that element. The initial accumulator is not tested. If no updated accumulator satisfies stop, this is the whole list.

def takeThroughAcc {α γ : Type*} (f : γ → α → γ) (stop : γ → Bool) :
    γ → List α → List α
  | _, [] => []
  | c, x :: xs =>
    let c' := f c x
    if stop c' then [x] else x :: takeThroughAcc f stop c' xs

Used by 8

Used byMembers of an accumulator-stopped prefix lie in the list · Accumulator-stopped prefix when the head update continues · Accumulator-stopped prefix when the head update stops · Accumulator-stopped prefix as a first-hit prefix of a scan · First-witness accumulator gives the inclusive first-hit prefix · Accumulator-stopped prefix of the empty list · Disjunction accumulator gives the inclusive first-hit prefix · Accumulator-stopped list is a prefix of its source

TheoremAccumulator-stopped prefix of the empty list#✓fully proved

An empty list has an empty accumulator-stopped prefix.

@[simp] theorem takeThroughAcc_nil {α γ : Type*} (f : γ → α → γ) (stop : γ → Bool)
    (c : γ) : takeThroughAcc f stop c [] = []

Uses 1

Statement usesAccumulator-stopped inclusive prefix of a list

TheoremAccumulator-stopped prefix when the head update stops#✓fully proved

If the accumulator stops after the head update, the prefix contains only the head.

@[simp] theorem takeThroughAcc_cons_of_stop {α γ : Type*} {f : γ → α → γ}
    {stop : γ → Bool} {c : γ} {x : α} (h : stop (f c x) = true) (xs : List α) :
    takeThroughAcc f stop c (x :: xs) = [x]

Uses 1

Statement usesAccumulator-stopped inclusive prefix of a list

TheoremAccumulator-stopped prefix when the head update continues#✓fully proved

If the accumulator continues after the head update, the same updated accumulator processes the tail.

@[simp] theorem takeThroughAcc_cons_of_continue {α γ : Type*} {f : γ → α → γ}
    {stop : γ → Bool} {c : γ} {x : α} (h : stop (f c x) = false) (xs : List α) :
    takeThroughAcc f stop c (x :: xs) = x :: takeThroughAcc f stop (f c x) xs

Uses 1

Statement usesAccumulator-stopped inclusive prefix of a list

TheoremAccumulator-stopped list is a prefix of its source#✓fully proved

The accumulator-stopped list is a prefix of its source list.

theorem takeThroughAcc_prefix {α γ : Type*} (f : γ → α → γ) (stop : γ → Bool)
    (c : γ) (xs : List α) : takeThroughAcc f stop c xs <+: xs

Uses 1 · Used by 1

Statement usesAccumulator-stopped inclusive prefix of a list

Used byMembers of an accumulator-stopped prefix lie in the list

TheoremMembers of an accumulator-stopped prefix lie in the list#✓fully proved

Every member of an accumulator-stopped prefix belongs to the source list.

theorem mem_of_mem_takeThroughAcc {α γ : Type*} {f : γ → α → γ} {stop : γ → Bool}
    {c : γ} {xs : List α} {x : α} (h : x ∈ takeThroughAcc f stop c xs) : x ∈ xs

Uses 2

Statement usesAccumulator-stopped inclusive prefix of a list

Proof usesAccumulator-stopped list is a prefix of its source

TheoremDisjunction accumulator gives the inclusive first-hit prefix#✓fully proved

Accumulating disjunction from false gives the ordinary inclusive first-hit prefix.

theorem takeThroughAcc_or {α : Type*} (p : α → Bool) (xs : List α) :
    takeThroughAcc (fun found x => found || p x) id false xs = takeThrough p xs

Uses 4

Statement usesInclusive first-hit prefix of a list · Accumulator-stopped inclusive prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix when the head is a hit

TheoremFirst-witness accumulator gives the inclusive first-hit prefix#✓fully proved

Accumulating a projection of the first witness in an Option gives the ordinary inclusive first-hit prefix.

theorem takeThroughAcc_first {α β δ : Type*} (p : β → Bool) (v : α → β) (w : α → δ)
    (xs : List α) :
    takeThroughAcc (fun found x =>
        match found with
        | some old => some old
        | none => if p (v x) then some (w x) else none)
        Option.isSome none xs = takeThrough (fun x => p (v x)) xs

Uses 4

Statement usesInclusive first-hit prefix of a list · Accumulator-stopped inclusive prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix when the head is a hit

TheoremFirst-witness fold over the inclusive first-hit prefix#✓fully proved

Folding the first-witness update over the inclusive tested prefix returns the first witness in the whole source list.

theorem foldl_first_takeThrough {α β δ : Type*} (p : β → Bool) (v : α → β) (w : α → δ)
    (xs : List α) :
    (takeThrough (fun x => p (v x)) xs).foldl
        (fun found x =>
          match found with
          | some old => some old
          | none => if p (v x) then some (w x) else none) none =
      (xs.find? fun x => p (v x)).map w

Uses 3

Statement usesInclusive first-hit prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix when the head is a hit

TheoremAccumulator-stopped prefix as a first-hit prefix of a scan#✓fully proved

The recursive ETH operation is the ordinary inclusive first-hit prefix of the elements paired with their updated accumulators.

theorem takeThroughAcc_eq_map_takeThrough_scanl {α γ : Type*} (f : γ → α → γ)
    (stop : γ → Bool) (c : γ) (xs : List α) :
    takeThroughAcc f stop c xs =
      ((xs.zip (xs.scanl f c).tail).takeThrough (fun x => stop x.2)).map Prod.fst

Uses 5

Statement usesInclusive first-hit prefix of a list · Accumulator-stopped inclusive prefix of a list

Proof usesInclusive first-hit prefix when the head is not a hit · Inclusive first-hit prefix when the head is a hit · Inclusive first-hit prefix of the empty list

TheoremChunks of a list have length at most the chunk size#✓fully proved

Let \(n > 0\) and let \(L\) be a list. Split \(L\) from left to right into consecutive chunks of size \(n\): elements go into the current chunk until it holds \(n\) elements, then a new chunk is started. Every chunk produced has at most \(n\) elements.

theorem length_le_of_mem_toChunks {α : Type u} (n : Nat) (xs : List α)
    (hn : 0 < n) (chunk : List α) (hchunk : chunk ∈ toChunks n xs) :
    chunk.length ≤ n

Used by 1

Used byComparison cost of the group medians

DefinitionOrdered insertion into a list#✓fully proved

For an element \(x\) of a linearly ordered type, the ordered insertion of \(x\) into the empty list is \([x]\). For a list with head \(a\) and tail \(\ell\), it is \(x\) followed by the whole list if \(x < a\); it is \(a\) followed by the ordered insertion of \(x\) into \(\ell\) if \(a < x\); and it is the list unchanged if \(a = x\).

On a strictly increasing list a key that is already present is therefore ignored. On an unsorted list a later duplicate is not detected: inserting \(2\) into \([3, 2]\) gives \([2, 3, 2]\).

public def orderedInsert [LinearOrder α] (x : α) : List α → List α
  | [] => [x]
  | a :: as =>
      if x < a then x :: a :: as
      else if a < x then a :: orderedInsert x as
      else a :: as

Used by 13

Used byMembers after ordered insertion · Inserting a present element into a strictly increasing list · Insertion into a 2-3 tree is ordered insertion into its traversal · Insertion specification for 2-3 trees · Correctness of 2-3 tree insertion · Keys after insertion into a 2-3 tree · Insertion preserves the ordering of 2-3 trees · Building a B-tree from a strictly increasing list · B-tree insertion as sorted list insertion · Size of a B-tree after insertion · Insertion into a B-tree leaf · Insertion preserves the B-tree invariant · Membership after B-tree insertion

TheoremMembers after ordered insertion#✓fully proved

Over a linearly ordered type, for all elements \(x\), \(y\) and every list \(\ell\), the element \(y\) belongs to the ordered insertion of \(x\) into \(\ell\) if and only if \(y = x\) or \(y\) belongs to \(\ell\).

public theorem mem_orderedInsert [LinearOrder α] {x y : α} {xs : List α} :
    y ∈ orderedInsert x xs ↔ y = x ∨ y ∈ xs

Uses 1 · Used by 3

Statement usesOrdered insertion into a list

Used byKeys after insertion into a 2-3 tree · Insertion preserves the B-tree invariant · Membership after B-tree insertion

TheoremInserting a present element into a strictly increasing list#✓fully proved

Over a linearly ordered type, if every element of a list \(\ell\) is smaller than every later element of \(\ell\) and \(x\) belongs to \(\ell\), then the ordered insertion of \(x\) into \(\ell\) is \(\ell\) itself.

Without strict increase this fails: inserting \(2\) into \([3, 2]\) gives \([2, 3, 2]\).

public theorem orderedInsert_eq_of_mem [LinearOrder α] {x : α} {xs : List α}
    (hSorted : xs.Pairwise (· < ·)) (hMem : x ∈ xs) :
    orderedInsert x xs = xs

Uses 1 · Used by 3

Statement usesOrdered insertion into a list

Used byB-tree insertion as sorted list insertion · Size of a B-tree after insertion · Insertion preserves the B-tree invariant

35 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.