List properties

This file contains useful custom definitions and lemmas about Lists.

Equiv

def List.Equiv {α : Type u_1} (a b : List α) : Prop

Equations

• (a ≡ b) = (a ⊆ b ∧ b ⊆ a)

def List.«term_≡_» : Lean.TrailingParserDescr

Equations

• List.«term_≡_» = Lean.ParserDescr.trailingNode `List.«term_≡_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 51))

theorem List.Equiv.refl {α : Type u_1} {a : List α} : a ≡ a

theorem List.Equiv.symm {α : Type u_1} {a b : List α} : a ≡ b → b ≡ a

theorem List.Equiv.trans {α : Type u_1} {a b c : List α} : a ≡ b → b ≡ c → a ≡ c

theorem List.equiv_nil {α : Type u_1} (xs : List α) : xs ≡ [] ↔ xs = []

theorem List.cons_equiv_cons {α : Type u_1} (x : α) (xs ys : List α) : xs ≡ ys → x :: xs ≡ x :: ys

theorem List.cons_equiv_implies_equiv {α : Type u_1} (x : α) (xs ys : List α) : x :: xs ≡ x :: ys → ¬x ∈ xs → ¬x ∈ ys → xs ≡ ys

theorem List.dup_head_equiv {α : Type u_1} (x : α) (xs : List α) : x :: x :: xs ≡ x :: xs

theorem List.dup_head_equiv' {α : Type u_1} {x : α} {xs : List α} : x ∈ xs → x :: xs ≡ xs

theorem List.swap_cons_cons_equiv {α : Type u_1} (x₁ x₂ : α) (xs : List α) : x₁ :: x₂ :: xs ≡ x₂ :: x₁ :: xs

theorem List.filter_equiv {α : Type u_1} (f : α → Bool) (xs ys : List α) : xs ≡ ys → filter f xs ≡ filter f ys

theorem List.map_equiv {α : Type u_1} {β : Type u_2} (f : α → β) (xs ys : List α) : xs ≡ ys → map f xs ≡ map f ys

theorem List.filterMap_equiv {α : Type u_1} {β : Type u_2} (f : α → Option β) (xs ys : List α) : xs ≡ ys → filterMap f xs ≡ filterMap f ys

theorem List.append_swap_equiv {α : Type u_1} (xs ys : List α) : xs ++ ys ≡ ys ++ xs

theorem List.append_left_equiv {α : Type u_1} (xs ys zs : List α) : xs ≡ ys → xs ++ zs ≡ ys ++ zs

theorem List.append_right_equiv {α : Type u_1} (xs ys zs : List α) : ys ≡ zs → xs ++ ys ≡ xs ++ zs

Sorted

inductive List.SortedBy {β : Type u_1} {α : Type u_2} [LT β] (f : α → β) : List α → Prop

• nil {β : Type u_1} {α : Type u_2} [LT β] {f : α → β} : SortedBy f []
• cons_nil {β : Type u_1} {α : Type u_2} [LT β] {f : α → β} {x : α} : SortedBy f [x]
• cons_cons {β : Type u_1} {α : Type u_2} [LT β] {f : α → β} {x y : α} {ys : List α} : f x < f y → SortedBy f (y :: ys) → SortedBy f (x :: y :: ys)

@[reducible, inline]

abbrev List.Sorted {α : Type u_1} [LT α] (xs : List α) : Prop

Equations

• xs.Sorted = List.SortedBy id xs

theorem List.tail_sortedBy {β : Type u_1} {α : Type u_2} [LT β] {f : α → β} {x : α} {xs : List α} : SortedBy f (x :: xs) → SortedBy f xs

theorem List.sortedBy_implies_head_lt_tail {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] {f : α → β} {x : α} {xs : List α} : SortedBy f (x :: xs) → ∀ (y : α), y ∈ xs → f x < f y

theorem List.sortedBy_equiv_implies_head_eq {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] (f : α → β) {x y : α} {xs ys : List α} : SortedBy f (x :: xs) → SortedBy f (y :: ys) → x :: xs ≡ y :: ys → x = y

theorem List.sortedBy_equiv_implies_tail_subset {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] (f : α → β) {x : α} {xs ys : List α} : SortedBy f (x :: xs) → SortedBy f (x :: ys) → x :: xs ⊆ x :: ys → xs ⊆ ys

theorem List.sortedBy_equiv_implies_tail_equiv {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] (f : α → β) {x : α} {xs ys : List α} : SortedBy f (x :: xs) → SortedBy f (x :: ys) → x :: xs ≡ x :: ys → xs ≡ ys

theorem List.sortedBy_equiv_implies_eq {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] (f : α → β) {xs ys : List α} : SortedBy f xs → SortedBy f ys → xs ≡ ys → xs = ys

theorem List.sortedBy_cons {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] {f : α → β} {x : α} {ys : List α} : SortedBy f ys → (∀ (y : α), y ∈ ys → f x < f y) → SortedBy f (x :: ys)

theorem List.mem_of_sortedBy_unique {α : Type u_1} {β : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] [DecidableEq β] {f : α → β} {x y : α} {xs : List α} : SortedBy f xs → x ∈ xs → y ∈ xs → f x = f y → x = y

theorem List.mem_of_sortedBy_implies_find? {α : Type u_1} {β : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] [DecidableEq β] {f : α → β} {x : α} {xs : List α} : x ∈ xs → SortedBy f xs → find? (fun (y : α) => f y == f x) xs = some x

theorem List.map_eq_implies_sortedBy {β : Type u_1} {α : Type u_2} {γ : Type u_3} [LT β] [Cedar.Data.StrictLT β] {f : α → β} {g : γ → β} {xs : List α} {ys : List γ} : map f xs = map g ys → (SortedBy f xs ↔ SortedBy g ys)

theorem List.filter_sortedBy {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] {f : α → β} (p : α → Bool) {xs : List α} : SortedBy f xs → SortedBy f (filter p xs)

theorem List.filterMap_sortedBy {β : Type u_1} {α : Type u_2} {γ : Type u_3} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] {f : α → β} {g : α → Option γ} {f' : γ → β} {xs : List α} : (∀ (x : α) (y : γ), g x = some y → f x = f' y) → SortedBy f xs → SortedBy f' (filterMap g xs)

theorem List.filterMap_key_id_sortedBy_key {α β : Type} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {ks : List α} {fn : α → Option β} (hs : ks.Sorted) : SortedBy Prod.fst (filterMap (fun (k : α) => do let __do_lift ← fn k some (k, __do_lift)) ks)

theorem List.find?_filterMap_key_id {α β : Type} [BEq α] [LawfulBEq α] {ks : List α} {fn : α → Option β} {k : α} (h₂ : k ∈ ks) : Option.map Prod.snd (find? (fun (x : α × β) => match x with | (k', snd) => k' == k) (filterMap (fun (k : α) => do let __do_lift ← fn k some (k, __do_lift)) ks)) = fn k

theorem List.mapM_key_id_sortedBy_key {α β : Type} [LT α] {ks : List α} {kvs : List (α × β)} {fn : α → Option β} (hm : mapM (fun (k : α) => do let __do_lift ← fn k some (k, __do_lift)) ks = some kvs) (hs : ks.Sorted) : SortedBy Prod.fst kvs

theorem List.isSortedBy_correct {α : Type u_1} {β : Type u_2} [LT β] [DecidableLT β] {l : List α} {f : α → β} : SortedBy f l ↔ l.isSortedBy f = true

theorem List.isSorted_correct {α : Type u_1} [LT α] [DecidableLT α] {l : List α} : l.Sorted ↔ l.isSorted = true

Forallᵥ

def List.Forallᵥ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) : Prop

Equations

• List.Forallᵥ p kvs₁ kvs₂ = List.Forall₂ (fun (kv₁ : α × β) (kv₂ : α × γ) => kv₁.fst = kv₂.fst ∧ p kv₁.snd kv₂.snd) kvs₁ kvs₂

theorem List.forallᵥ_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : β → γ → Prop} {kvs₁ : List (α × β)} {kvs₂ : List (α × γ)} : Forallᵥ p kvs₁ kvs₂ = Forall₂ (fun (kv₁ : α × β) (kv₂ : α × γ) => kv₁.fst = kv₂.fst ∧ p kv₁.snd kv₂.snd) kvs₁ kvs₂