Documentation

Init.Data.List.Basic

theorem List.length_add_eq_lengthTRAux {α : Type u} (as : List α) (n : Nat) :

List.length as + n = List.lengthTRAux as n

theorem List.length_eq_lengthTR :

@List.length = @List.lengthTR

@[simp]

theorem List.length_nil {α : Type u} :

List.length [] = 0

def List.reverseAux {α : Type u} :

List α → List α → List α

Equations

List.reverseAux [] x = x
List.reverseAux (a :: l) x = List.reverseAux l (a :: x)

def List.reverse {α : Type u} (as : List α) :

Equations

List.reverse as = List.reverseAux as []

theorem List.reverseAux_reverseAux_nil {α : Type u} (as : List α) (bs : List α) :

List.reverseAux (List.reverseAux as bs) [] = List.reverseAux bs as

theorem List.reverseAux_reverseAux {α : Type u} (as : List α) (bs : List α) (cs : List α) :

List.reverseAux (List.reverseAux as bs) cs = List.reverseAux bs (List.reverseAux (List.reverseAux as []) cs)

@[simp]

theorem List.reverse_reverse {α : Type u} (as : List α) :

List.reverse (List.reverse as) = as

def List.append {α : Type u} :

List α → List α → List α

Equations

List.append [] x = x
List.append (a :: l) x = a :: List.append l x

def List.appendTR {α : Type u} (as : List α) (bs : List α) :

Equations

List.appendTR as bs = List.reverseAux (List.reverse as) bs

theorem List.append_eq_appendTR :

@List.append = @List.appendTR

instance List.instAppendList {α : Type u} :

Append (List α)

Equations

List.instAppendList = { append := List.append }

@[simp]

theorem List.nil_append {α : Type u} (as : List α) :

[] ++ as = as

@[simp]

theorem List.append_nil {α : Type u} (as : List α) :

as ++ [] = as

@[simp]

theorem List.cons_append {α : Type u} (a : α) (as : List α) (bs : List α) :

a :: as ++ bs = a :: (as ++ bs)

theorem List.append_assoc {α : Type u} (as : List α) (bs : List α) (cs : List α) :

as ++ bs ++ cs = as ++ (bs ++ cs)

instance List.instEmptyCollectionList {α : Type u} :

EmptyCollection (List α)

Equations

List.instEmptyCollectionList = { emptyCollection := [] }

def List.erase {α : Type u_1} [inst : BEq α] :

List α → α → List α

Equations

List.erase [] x = []
List.erase (a :: as) x = match a == x with | true => as | false => a :: List.erase as x

def List.eraseIdx {α : Type u} :

List α → Nat → List α

Equations

List.eraseIdx [] x = []
List.eraseIdx (a :: as) 0 = as
List.eraseIdx (a :: as) (Nat.succ n) = a :: List.eraseIdx as n

def List.isEmpty {α : Type u} :

List α → Bool

Equations

List.isEmpty x = match x with | [] => true | x :: x_1 => false

@[specialize]

def List.map {α : Type u} {β : Type v} (f : α → β) :

List α → List β

Equations

List.map f [] = []
List.map f (x_1 :: x_2) = f x_1 :: List.map f x_2

@[specialize]

def List.mapTRAux {α : Type u} {β : Type v} (f : α → β) :

List α → List β → List β

Equations

List.mapTRAux f [] x = List.reverse x
List.mapTRAux f (a :: as) x = List.mapTRAux f as (f a :: x)

@[inline]

def List.mapTR {α : Type u} {β : Type v} (f : α → β) (as : List α) :

Equations

List.mapTR f as = List.mapTRAux f as []

theorem List.reverseAux_eq_append {α : Type u} (as : List α) (bs : List α) :

List.reverseAux as bs = List.reverseAux as [] ++ bs

@[simp]

theorem List.reverse_nil {α : Type u} :

List.reverse [] = []

@[simp]

theorem List.reverse_cons {α : Type u} (a : α) (as : List α) :

List.reverse (a :: as) = List.reverse as ++ [a]

@[simp]

theorem List.reverse_append {α : Type u} (as : List α) (bs : List α) :

List.reverse (as ++ bs) = List.reverse bs ++ List.reverse as

theorem List.mapTRAux_eq {α : Type u} {β : Type v} (f : α → β) (as : List α) (bs : List β) :

List.mapTRAux f as bs = List.reverse bs ++ List.map f as

theorem List.map_eq_mapTR :

@List.map = @List.mapTR

@[specialize]

def List.map₂ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) :

List α → List β → List γ

Equations

List.map₂ f [] x = []
List.map₂ f x [] = []
List.map₂ f (a :: as) (b :: bs) = f a b :: List.map₂ f as bs

def List.join {α : Type u} :

List (List α) → List α

Equations

List.join [] = []
List.join (a :: as) = a ++ List.join as

@[specialize]

def List.filterMap {α : Type u} {β : Type v} (f : α → Option β) :

List α → List β

Equations

List.filterMap f [] = []
List.filterMap f (x_1 :: x_2) = match f x_1 with | none => List.filterMap f x_2 | some b => b :: List.filterMap f x_2

@[specialize]

def List.filterAux {α : Type u} (p : α → Bool) :

List α → List α → List α

Equations

List.filterAux p [] x = List.reverse x
List.filterAux p (a :: l) x = match p a with | true => List.filterAux p l (a :: x) | false => List.filterAux p l x

@[inline]

def List.filter {α : Type u} (p : α → Bool) (as : List α) :

Equations

List.filter p as = List.filterAux p as []

@[specialize]

def List.partitionAux {α : Type u} (p : α → Bool) :

List α → List α × List α → List α × List α

Equations

List.partitionAux p [] (bs, cs) = (List.reverse bs, List.reverse cs)
List.partitionAux p (a :: as) (bs, cs) = match p a with | true => List.partitionAux p as (a :: bs, cs) | false => List.partitionAux p as (bs, a :: cs)

@[inline]

def List.partition {α : Type u} (p : α → Bool) (as : List α) :

List α × List α

Equations

List.partition p as = List.partitionAux p as ([], [])

def List.dropWhile {α : Type u} (p : α → Bool) :

List α → List α

Equations

List.dropWhile p [] = []
List.dropWhile p (x_1 :: x_2) = match p x_1 with | true => List.dropWhile p x_2 | false => x_1 :: x_2

def List.find? {α : Type u} (p : α → Bool) :

List α → Option α

Equations

List.find? p [] = none
List.find? p (x_1 :: x_2) = match p x_1 with | true => some x_1 | false => List.find? p x_2

def List.findSome? {α : Type u} {β : Type v} (f : α → Option β) :

List α → Option β

Equations

List.findSome? f [] = none
List.findSome? f (x_1 :: x_2) = match f x_1 with | some b => some b | none => List.findSome? f x_2

def List.replace {α : Type u} [inst : BEq α] :

List α → α → α → List α

Equations

List.replace [] x x = []
List.replace (a :: as) x x = match a == x with | true => x :: as | false => a :: List.replace as x x

def List.elem {α : Type u} [inst : BEq α] (a : α) :

List α → Bool

Equations

List.elem a [] = false
List.elem a (x_1 :: x_2) = match a == x_1 with | true => true | false => List.elem a x_2

def List.notElem {α : Type u} [inst : BEq α] (a : α) (as : List α) :

Equations

List.notElem a as = !List.elem a as

@[inline]

abbrev List.contains {α : Type u} [inst : BEq α] (as : List α) (a : α) :

Equations

List.contains as a = List.elem a as

def List.eraseDupsAux {α : Type u_1} [inst : BEq α] :

List α → List α → List α

Equations

List.eraseDupsAux [] x = List.reverse x
List.eraseDupsAux (a :: l) x = match List.elem a x with | true => List.eraseDupsAux l x | false => List.eraseDupsAux l (a :: x)

def List.eraseDups {α : Type u_1} [inst : BEq α] (as : List α) :

Equations

List.eraseDups as = List.eraseDupsAux as []

def List.eraseRepsAux {α : Type u_1} [inst : BEq α] :

α → List α → List α → List α

Equations

List.eraseRepsAux x [] x = List.reverse (x :: x)
List.eraseRepsAux x (a' :: as) x = match x == a' with | true => List.eraseRepsAux x as x | false => List.eraseRepsAux a' as (x :: x)

def List.eraseReps {α : Type u_1} [inst : BEq α] :

List α → List α

Equations

List.eraseReps x = match x with | [] => [] | a :: as => List.eraseRepsAux a as []

@[specialize]

def List.spanAux {α : Type u} (p : α → Bool) :

List α → List α → List α × List α

Equations

List.spanAux p [] x = (List.reverse x, [])
List.spanAux p (a :: l) x = match p a with | true => List.spanAux p l (a :: x) | false => (List.reverse x, a :: l)

@[inline]

def List.span {α : Type u} (p : α → Bool) (as : List α) :

List α × List α

Equations

List.span p as = List.spanAux p as []

@[specialize]

def List.groupByAux {α : Type u} (eq : α → α → Bool) :

List α → List (List α) → List (List α)

Equations

List.groupByAux eq (a :: as) ((ag :: g) :: gs) = match eq a ag with | true => List.groupByAux eq as ((a :: ag :: g) :: gs) | false => List.groupByAux eq as ([a] :: List.reverse (ag :: g) :: gs)
List.groupByAux eq x x = List.reverse x

@[specialize]

def List.groupBy {α : Type u} (p : α → α → Bool) :

List α → List (List α)

Equations

List.groupBy p x = match x with | [] => [] | a :: as => List.groupByAux p as [[a]]

def List.lookup {α : Type u} {β : Type v} [inst : BEq α] :

α → List (α × β) → Option β

Equations

List.lookup x [] = none
List.lookup x ((k, b) :: es) = match x == k with | true => some b | false => List.lookup x es

def List.removeAll {α : Type u} [inst : BEq α] (xs : List α) (ys : List α) :

Equations

List.removeAll xs ys = List.filter (fun x => List.notElem x ys) xs

def List.drop {α : Type u} :

Nat → List α → List α

Equations

List.drop 0 x = x
List.drop (Nat.succ n) [] = []
List.drop (Nat.succ n) (a :: as) = List.drop n as

def List.take {α : Type u} :

Nat → List α → List α

Equations

List.take 0 x = []
List.take (Nat.succ n) [] = []
List.take (Nat.succ n) (a :: as) = a :: List.take n as

def List.takeWhile {α : Type u} (p : α → Bool) :

List α → List α

Equations

List.takeWhile p [] = []
List.takeWhile p (x_1 :: x_2) = match p x_1 with | true => x_1 :: List.takeWhile p x_2 | false => []

@[specialize]

def List.foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) :

List α → β

Equations

List.foldr f init [] = init
List.foldr f init (x_1 :: x_2) = f x_1 (List.foldr f init x_2)

@[inline]

def List.any {α : Type u} (l : List α) (p : α → Bool) :

Equations

List.any l p = List.foldr (fun a r => p a || r) false l

@[inline]

def List.all {α : Type u} (l : List α) (p : α → Bool) :

Equations

List.all l p = List.foldr (fun a r => p a && r) true l

def List.or (bs : List Bool) :

Equations

List.or bs = List.any bs id

def List.and (bs : List Bool) :

Equations

List.and bs = List.all bs id

def List.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) :

List α → List β → List γ

Equations

List.zipWith f (x_2 :: xs) (y :: ys) = f x_2 y :: List.zipWith f xs ys
List.zipWith f x x = []

def List.zip {α : Type u} {β : Type v} :

List α → List β → List (α × β)

Equations

List.zip = List.zipWith Prod.mk

def List.unzip {α : Type u} {β : Type v} :

List (α × β) → List α × List β

Equations

List.unzip [] = ([], [])
List.unzip ((a, b) :: t) = (a :: (List.unzip t).1, b :: (List.unzip t).2)

def List.rangeAux :

Nat → List Nat → List Nat

Equations

List.rangeAux 0 x = x
List.rangeAux (Nat.succ n) x = List.rangeAux n (n :: x)

def List.range (n : Nat) :

Equations

List.range n = List.rangeAux n []

def List.iota :

Nat → List Nat

Equations

List.iota 0 = []
List.iota (Nat.succ n) = Nat.succ n :: List.iota n

def List.enumFrom {α : Type u} :

Nat → List α → List (Nat × α)

Equations

List.enumFrom x [] = []
List.enumFrom x (x_2 :: xs) = (x, x_2) :: List.enumFrom (x + 1) xs

def List.enum {α : Type u} :

List α → List (Nat × α)

Equations

List.enum = List.enumFrom 0

def List.init {α : Type u} :

List α → List α

Equations

List.init [] = []
List.init [a] = []
List.init (a :: l) = a :: List.init l

def List.intersperse {α : Type u} (sep : α) :

List α → List α

Equations

List.intersperse sep [] = []
List.intersperse sep [a] = [a]
List.intersperse sep (a :: l) = a :: sep :: List.intersperse sep l

def List.intercalate {α : Type u} (sep : List α) (xs : List (List α)) :

Equations

List.intercalate sep xs = List.join (List.intersperse sep xs)

@[inline]

def List.bind {α : Type u} {β : Type v} (a : List α) (b : α → List β) :

Equations

List.bind a b = List.join (List.map b a)

@[inline]

def List.pure {α : Type u} (a : α) :

Equations

List.pure a = [a]

inductive List.lt {α : Type u} [inst : LT α] :

List α → List α → Prop

nil: ∀ {α : Type u} [inst : LT α] (b : α) (bs : List α), List.lt [] (b :: bs)
head: ∀ {α : Type u} [inst : LT α] {a : α} (as : List α) {b : α} (bs : List α), a < b → List.lt (a :: as) (b :: bs)
tail: ∀ {α : Type u} [inst : LT α] {a : α} {as : List α} {b : α} {bs : List α}, ¬a < b → ¬b < a → List.lt as bs → List.lt (a :: as) (b :: bs)

instance List.instLTList {α : Type u} [inst : LT α] :

LT (List α)

Equations

List.instLTList = { lt := List.lt }

instance List.hasDecidableLt {α : Type u} [inst : LT α] [h : DecidableRel fun a a_1 => a < a_1] (l₁ : List α) (l₂ : List α) :

Decidable (l₁ < l₂)

Equations

List.hasDecidableLt [] [] = isFalse (_ : [] < [] → False)
List.hasDecidableLt [] (b :: bs) = isTrue (_ : List.lt [] (b :: bs))
List.hasDecidableLt (a :: as) [] = isFalse (_ : a :: as < [] → False)
List.hasDecidableLt (a :: as) (b :: bs) = match h a b with | isTrue h₁ => isTrue (_ : List.lt (a :: as) (b :: bs)) | isFalse h₁ => match h b a with | isTrue h₂ => isFalse (_ : a :: as < b :: bs → False) | isFalse h₂ => match List.hasDecidableLt as bs with | isTrue h₃ => isTrue (_ : List.lt (a :: as) (b :: bs)) | isFalse h₃ => isFalse (_ : a :: as < b :: bs → False)

noncomputable def List.le {α : Type u} [inst : LT α] (a : List α) (b : List α) :

Prop

Equations

List.le a b = ¬b < a

instance List.instLEList {α : Type u} [inst : LT α] :

LE (List α)

Equations

List.instLEList = { le := List.le }

instance List.instForAllListDecidableLeInstLEList {α : Type u} [inst : LT α] [h : DecidableRel fun a a_1 => a < a_1] (l₁ : List α) (l₂ : List α) :

Decidable (l₁ ≤ l₂)

Equations

List.instForAllListDecidableLeInstLEList a b = inferInstanceAs (Decidable ¬b < a)

def List.isPrefixOf {α : Type u} [inst : BEq α] :

List α → List α → Bool

Equations

List.isPrefixOf [] x = true
List.isPrefixOf x [] = false
List.isPrefixOf (a :: as) (b :: bs) = (a == b && List.isPrefixOf as bs)

def List.isSuffixOf {α : Type u} [inst : BEq α] (l₁ : List α) (l₂ : List α) :

Equations

List.isSuffixOf l₁ l₂ = List.isPrefixOf (List.reverse l₁) (List.reverse l₂)

@[specialize]

def List.isEqv {α : Type u} :

List α → List α → (α → α → Bool) → Bool

Equations

List.isEqv [] [] x = true
List.isEqv (a :: as) (b :: bs) x = (x a b && List.isEqv as bs x)
List.isEqv x x x = false

def List.beq {α : Type u} [inst : BEq α] :

List α → List α → Bool

Equations

List.beq [] [] = true
List.beq (a :: as) (b :: bs) = (a == b && List.beq as bs)
List.beq x x = false

instance List.instBEqList {α : Type u} [inst : BEq α] :

Equations

List.instBEqList = { beq := List.beq }

def List.replicate {α : Type u} (n : Nat) (a : α) :

Equations

List.replicate 0 x = []
List.replicate (Nat.succ n) x = x :: List.replicate n x

def List.replicateTR {α : Type u} (n : Nat) (a : α) :

Equations

List.replicateTR n a = (fun loop => loop n []) (List.replicateTR.loop a)

def List.replicateTR.loop {α : Type u} (a : α) :

Nat → List α → List α

Equations

List.replicateTR.loop a 0 x = x
List.replicateTR.loop a (Nat.succ n) x = List.replicateTR.loop a n (a :: x)

theorem List.replicateTR_loop_replicate_eq {α : Type u} (a : α) (m : Nat) (n : Nat) :

List.replicateTR.loop a n (List.replicate m a) = List.replicate (n + m) a

theorem List.replicate_eq_replicateTR :

@List.replicate = @List.replicateTR

def List.dropLast {α : Type u_1} :

List α → List α

Equations

List.dropLast [] = []
List.dropLast [a] = []
List.dropLast (a :: l) = a :: List.dropLast l

@[simp]

theorem List.length_replicate {α : Type u} (n : Nat) (a : α) :

List.length (List.replicate n a) = n

@[simp]

theorem List.length_concat {α : Type u} (as : List α) (a : α) :

List.length (List.concat as a) = List.length as + 1

@[simp]

theorem List.length_set {α : Type u} (as : List α) (i : Nat) (a : α) :

List.length (List.set as i a) = List.length as

@[simp]

theorem List.length_dropLast {α : Type u} (as : List α) :

List.length (List.dropLast as) = List.length as - 1

@[simp]

theorem List.length_append {α : Type u} (as : List α) (bs : List α) :

List.length (as ++ bs) = List.length as + List.length bs

@[simp]

theorem List.length_reverse {α : Type u} (as : List α) :

List.length (List.reverse as) = List.length as

def List.maximum? {α : Type u} [inst : LT α] [inst : DecidableRel LT.lt] :

List α → Option α

Equations

List.maximum? x = match x with | [] => none | a :: as => some (List.foldl max a as)

def List.minimum? {α : Type u} [inst : LE α] [inst : DecidableRel LE.le] :

List α → Option α

Equations

List.minimum? x = match x with | [] => none | a :: as => some (List.foldl min a as)