instance List.instGetElemListNatLtInstLTNatLength {α : Type u} : GetElem (List α) Nat α fun as i => i < List.length as

Equations

• List.instGetElemListNatLtInstLTNatLength = { getElem := fun as i h => List.get as { val := i, isLt := h } }

@[simp]

theorem List.cons_getElem_zero {α : Type u} (a : α) (as : List α) (h : 0 < List.length (a :: as)) : (a :: as)[0] = a

@[simp]

theorem List.cons_getElem_succ {α : Type u} (a : α) (as : List α) (i : Nat) (h : i + 1 < List.length (a :: as)) : (a :: as)[i + 1] = as[i]

theorem List.length_add_eq_lengthTRAux {α : Type u} (as : List α) (n : Nat) : List.length as + n = List.lengthTRAux as n

@[csimp]

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 [] _fun_discr = _fun_discr
• List.reverseAux (a :: l) _fun_discr = List.reverseAux l (a :: _fun_discr)

def List.reverse {α : Type u} (as : List α) : 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 [] _fun_discr = _fun_discr
• List.append (a :: l) _fun_discr = a :: List.append l _fun_discr

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

Equations

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

@[csimp]

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)

@[simp]

theorem List.List.append_eq {α : Type u} (as : List α) (bs : List α) : List.append as bs = as ++ bs

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

theorem List.append_cons {α : Type u} (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs

instance List.instEmptyCollectionList {α : Type u} : EmptyCollection (List α)

Equations

• List.instEmptyCollectionList = { emptyCollection := [] }

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

Equations

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

def List.eraseIdx {α : Type u} : List α → Nat → List α

Equations

• List.eraseIdx [] _fun_discr = []
• List.eraseIdx (head :: 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 _fun_discr = match _fun_discr with | [] => true | head :: tail => false

@[specialize #[]]

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

Equations

• List.map f [] = []
• List.map f (head :: tail) = f head :: List.map f tail

@[specialize #[]]

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

Equations

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

@[inline]

def List.mapTR {α : Type u} {β : Type v} (f : α → β) (as : List α) : 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

@[csimp]

theorem List.map_eq_mapTR : @List.map = @List.mapTR

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 (head :: tail) = match f head with | none => List.filterMap f tail | some b => b :: List.filterMap f tail

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

Equations

• List.filter p [] = []
• List.filter p (head :: tail) = match p head with | true => head :: List.filter p tail | false => List.filter p tail

@[specialize #[]]

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

Equations

• List.filterTRAux p [] _fun_discr = List.reverse _fun_discr
• List.filterTRAux p (a :: l) _fun_discr = match p a with | true => List.filterTRAux p l (a :: _fun_discr) | false => List.filterTRAux p l _fun_discr

@[inline]

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

Equations

• List.filterTR p as = List.filterTRAux p as []

theorem List.filterTRAux_eq {α : Type u} (p : α → Bool) (as : List α) (bs : List α) : List.filterTRAux p as bs = List.reverse bs ++ List.filter p as

@[csimp]

theorem List.filter_eq_filterTR : @List.filter = @List.filterTR

@[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 (head :: tail) = match p head with | true => List.dropWhile p tail | false => head :: tail

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

Equations

• List.find? p [] = none
• List.find? p (head :: tail) = match p head with | true => some head | false => List.find? p tail

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

Equations

• List.findSome? f [] = none
• List.findSome? f (head :: tail) = match f head with | some b => some b | none => List.findSome? f tail

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

Equations

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

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

Equations

• List.elem a [] = false
• List.elem a (head :: tail) = match a == head with | true => true | false => List.elem a tail

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

Equations

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

@[inline]

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

Equations

• List.contains as a = List.elem a as

inductive List.Mem {α : Type u} : α → List α → Prop

• head: ∀ {α : Type u} (a : α) (as : List α), List.Mem a (a :: as)
• tail: ∀ {α : Type u} (a : α) {b : α} {as : List α}, List.Mem b as → List.Mem b (a :: as)

instance List.instMembershipList {α : Type u} : Membership α (List α)

Equations

• List.instMembershipList = { mem := List.Mem }

theorem List.mem_of_elem_eq_true {α : Type u} [inst : DecidableEq α] {a : α} {as : List α} : List.elem a as = true → a ∈ as

theorem List.elem_eq_true_of_mem {α : Type u} [inst : DecidableEq α] {a : α} {as : List α} (h : a ∈ as) : List.elem a as = true

instance List.instDecidableMemListInstMembershipList {α : Type u} [inst : DecidableEq α] (a : α) (as : List α) : Decidable (a ∈ as)

Equations

• List.instDecidableMemListInstMembershipList a as = decidable_of_decidable_of_iff (_ : List.elem a as = true ↔ a ∈ as)

theorem List.mem_append_of_mem_left {α : Type u} {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs

theorem List.mem_append_of_mem_right {α : Type u} {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs

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

Equations

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

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

Equations

• List.eraseDups as = List.eraseDupsAux as []

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

Equations

• One or more equations did not get rendered due to their size.
• List.eraseRepsAux _fun_discr [] _fun_discr = List.reverse (_fun_discr :: _fun_discr)

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

Erase repeated adjacent elements.

Equations

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

@[specialize #[]]

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

Equations

• List.spanAux p [] _fun_discr = (List.reverse _fun_discr, [])
• List.spanAux p (a :: l) _fun_discr = match p a with | true => List.spanAux p l (a :: _fun_discr) | false => (List.reverse _fun_discr, 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

• One or more equations did not get rendered due to their size.
• List.groupByAux eq _fun_discr _fun_discr = List.reverse _fun_discr

@[specialize #[]]

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

Equations

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

def List.lookup {α : Type u} {β : Type v} [inst : BEq α] : α → List (α × β) → Option β

Equations

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

def List.removeAll {α : Type u} [inst : BEq α] (xs : List α) (ys : List α) : 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 _fun_discr = _fun_discr
• List.drop (Nat.succ n) [] = []
• List.drop (Nat.succ n) (head :: as) = List.drop n as

@[simp]

theorem List.drop_nil {α : Type u} {i : Nat} : List.drop i [] = []

theorem List.get_drop_eq_drop {α : Type u} (as : List α) (i : Nat) (h : i < List.length as) : as[i] :: List.drop (i + 1) as = List.drop i as

def List.take {α : Type u} : Nat → List α → List α

Equations

• List.take 0 _fun_discr = []
• List.take (Nat.succ n) [] = []
• List.take (Nat.succ n) (head :: as) = head :: List.take n as

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

Equations

• List.takeWhile p [] = []
• List.takeWhile p (head :: tail) = match p head with | true => head :: List.takeWhile p tail | false => []

@[specialize #[]]

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

Equations

• List.foldr f init [] = init
• List.foldr f init (head :: tail) = f head (List.foldr f init tail)

@[inline]

def List.any {α : Type u} (l : List α) (p : α → Bool) : 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) : Bool

Equations

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

def List.or (bs : List Bool) : Bool

Equations

• List.or bs = List.any bs id

def List.and (bs : List Bool) : Bool

Equations

• List.and bs = List.all bs id

@[specialize #[]]

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

Equations

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

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) = match List.unzip t with | (al, bl) => (a :: al, b :: bl)

def List.rangeAux : Nat → List Nat → List Nat

Equations

• List.rangeAux 0 _fun_discr = _fun_discr
• List.rangeAux (Nat.succ n) _fun_discr = List.rangeAux n (n :: _fun_discr)

def List.range (n : Nat) : List 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.iotaTR (n : Nat) : List Nat

Equations

• List.iotaTR n = List.iotaTR.go n []

def List.iotaTR.go : Nat → List Nat → List Nat

Equations

• List.iotaTR.go 0 _fun_discr = List.reverse _fun_discr
• List.iotaTR.go (Nat.succ n) _fun_discr = List.iotaTR.go n (Nat.succ n :: _fun_discr)

@[csimp]

theorem List.iota_eq_iotaTR : List.iota = List.iotaTR

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

Equations

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

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

Equations

• List.enum = List.enumFrom 0

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

Equations

• List.intersperse sep [] = []
• List.intersperse sep [x] = [x]
• List.intersperse sep (x :: xs) = x :: sep :: List.intersperse sep xs

def List.intercalate {α : Type u} (sep : List α) (xs : List (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 β) : List β

Equations

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

@[inline]

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

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

• One or more equations did not get rendered due to their size.
• List.hasDecidableLt [] [] = isFalse (_ : [] < [] → False)
• List.hasDecidableLt [] (head :: tail) = isTrue (_ : List.lt [] (head :: tail))
• List.hasDecidableLt (head :: tail) [] = isFalse (_ : head :: tail < [] → False)

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 α] [inst : DecidableRel fun a a_1 => a < a_1] (l₁ : List α) (l₂ : List α) : Decidable (l₁ ≤ l₂)

Equations

• List.instForAllListDecidableLeInstLEList x x = inferInstanceAs (Decidable ¬x < x)

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

isPrefixOf l₁ l₂ returns true Iff l₁ is a prefix of l₂. That is, there exists a t such that l₂ == l₁ ++ t.

Equations

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

def List.isPrefixOf? {α : Type u} [inst : BEq α] : List α → List α → Option (List α)

isPrefixOf? l₁ l₂ returns some t when l₂ == l₁ ++ t.

Equations

• List.isPrefixOf? [] _fun_discr = some _fun_discr
• List.isPrefixOf? _fun_discr [] = none
• List.isPrefixOf? (a :: as) (b :: bs) = if (a == b) = true then List.isPrefixOf? as bs else none

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

isSuffixOf l₁ l₂ returns true Iff l₁ is a suffix of l₂. That is, there exists a t such that l₂ == t ++ l₁.

Equations

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

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

isSuffixOf? l₁ l₂ returns some t when l₂ == t ++ l₁.

Equations

• List.isSuffixOf? l₁ l₂ = Option.map List.reverse (List.isPrefixOf? (List.reverse l₁) (List.reverse l₂))

@[specialize #[]]

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

Equations

• List.isEqv [] [] _fun_discr = true
• List.isEqv (a :: as) (b :: bs) _fun_discr = (_fun_discr a b && List.isEqv as bs _fun_discr)
• List.isEqv _fun_discr _fun_discr _fun_discr = 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 _fun_discr _fun_discr = false

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

Equations

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

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

Equations

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

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

Equations

• List.replicateTR n a = List.replicateTR.loop a n []

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

Equations

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

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

@[csimp]

theorem List.replicate_eq_replicateTR : @List.replicate = @List.replicateTR

def List.dropLast {α : Type u_1} : List α → List α

Equations

• List.dropLast [] = []
• List.dropLast [x] = []
• List.dropLast (x :: xs) = x :: List.dropLast xs

@[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_cons {α : Type u} (a : α) (as : List α) : List.length (List.dropLast (a :: as)) = List.length as

@[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_map {α : Type u} {β : Type v} (as : List α) (f : α → β) : List.length (List.map f as) = List.length as

@[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? _fun_discr = match _fun_discr 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? _fun_discr = match _fun_discr with | [] => none | a :: as => some (List.foldl min a as)

instance List.instLawfulBEqListInstBEqList {α : Type u} [inst : BEq α] [inst : LawfulBEq α] : LawfulBEq (List α)

Equations

• @List.instLawfulBEqListInstBEqList = @List.instLawfulBEqListInstBEqList.proof_1

theorem List.of_concat_eq_concat {α : Type u} {as : List α} {bs : List α} {a : α} {b : α} (h : List.concat as a = List.concat bs b) : as = bs ∧ a = b

theorem List.concat_eq_append {α : Type u} (as : List α) (a : α) : List.concat as a = as ++ [a]

theorem List.drop_eq_nil_of_le {α : Type u} {as : List α} {i : Nat} (h : List.length as ≤ i) : List.drop i as = []