Non-Empty Lists

Here, we define non-empty lists based on regular lists.

inductive CustomBasicDatastructures.NonEmptyList (α : Type u) : Type u

Basically a NonEmptyList is a List without the nil constructor.

• cons {α : Type u} (hd : α) (tl : List α) : NonEmptyList α

def CustomBasicDatastructures.NonEmptyList.toList {α : Type u} : NonEmptyList α → List α

We can convert a NonEmptyList to a regular List in the obvious way.

Equations

• (CustomBasicDatastructures.NonEmptyList.cons hd tl).toList = hd :: tl

theorem CustomBasicDatastructures.NonEmptyList.toList_ne_nil {α : Type u} {l : NonEmptyList α} : l.toList ≠ []

A List obtained from a NonEmptyList is not empty as expected.

def CustomBasicDatastructures.NonEmptyList.from_ne_nil {α : Type u} (l : List α) (ne_nil : l ≠ []) : NonEmptyList α

We can build a NonEmptyList from a regular List as long as we know that the list is not empty.

Equations

• CustomBasicDatastructures.NonEmptyList.from_ne_nil [] ne_nil_2 = ⋯.elim
• CustomBasicDatastructures.NonEmptyList.from_ne_nil (a :: as) ne_nil_2 = CustomBasicDatastructures.NonEmptyList.cons a as

@[match_pattern]

def CustomBasicDatastructures.NonEmptyList.singleton {α : Type u} (a : α) : NonEmptyList α

Construct a NonEmptyList from a single element.

Equations

• CustomBasicDatastructures.NonEmptyList.singleton a = CustomBasicDatastructures.NonEmptyList.cons a []

@[simp]

theorem CustomBasicDatastructures.NonEmptyList.toList_singleton {α : Type u} {a : α} : (singleton a).toList = [a]

Transforming a singleton into a list yields a singleton list.

def CustomBasicDatastructures.NonEmptyList.cons' {α : Type u} (a : α) (as : NonEmptyList α) : NonEmptyList α

Construct a NonEmptyList from a single element and a NonEmptyList.

Equations

• CustomBasicDatastructures.NonEmptyList.cons' a as = CustomBasicDatastructures.NonEmptyList.cons a as.toList

@[simp]

theorem CustomBasicDatastructures.NonEmptyList.toList_cons' {α : Type u} {a : α} {as : NonEmptyList α} : (cons' a as).toList = a :: as.toList

Transforming a cons' into a list yields the expected list.

def CustomBasicDatastructures.NonEmptyList.cases {α : Type u} {motive : NonEmptyList α → Sort v} (l : NonEmptyList α) (singleton : (a : α) → motive (singleton a)) (cons' : (a : α) → (as : NonEmptyList α) → motive (cons' a as)) : motive l

Alternative cases eliminator.

Equations

• CustomBasicDatastructures.NonEmptyList.cases (CustomBasicDatastructures.NonEmptyList.cons a []) singleton cons' = singleton a
• CustomBasicDatastructures.NonEmptyList.cases (CustomBasicDatastructures.NonEmptyList.cons a (a' :: as)) singleton cons' = cons' a (CustomBasicDatastructures.NonEmptyList.cons a' as)

@[irreducible]

def CustomBasicDatastructures.NonEmptyList.rec' {α : Type u} {motive : NonEmptyList α → Sort v} (l : NonEmptyList α) (singleton : (a : α) → motive (singleton a)) (cons' : (a : α) → (as : NonEmptyList α) → motive as → motive (cons' a as)) : motive l

Alternative induction principle.

Equations

• One or more equations did not get rendered due to their size.
• CustomBasicDatastructures.NonEmptyList.rec' (CustomBasicDatastructures.NonEmptyList.cons a []) singleton cons' = singleton a

def CustomBasicDatastructures.NonEmptyList.head {α : Type u} : NonEmptyList α → α

Extract first element from NonEmptyList.

Equations

• (CustomBasicDatastructures.NonEmptyList.cons hd tl).head = hd

theorem CustomBasicDatastructures.NonEmptyList.head_eq {α : Type u} {l : NonEmptyList α} : l.head = l.toList.head ⋯

We can express head in terms of the regular list obtained through toList.

@[simp]

theorem CustomBasicDatastructures.NonEmptyList.head_singleton {α : Type u} {a : α} : (singleton a).head = a

The head of a singleton is the single value.

@[simp]

theorem CustomBasicDatastructures.NonEmptyList.head_cons' {α : Type u} {a : α} {as : NonEmptyList α} : (cons' a as).head = a

The head of a cons' is the first value.

def CustomBasicDatastructures.NonEmptyList.tail {α : Type u} : NonEmptyList α → List α

Extract all but the first element from NonEmptyList. This returns a plain List.

Equations

• (CustomBasicDatastructures.NonEmptyList.cons hd tl).tail = tl

theorem CustomBasicDatastructures.NonEmptyList.tail_eq {α : Type u} {l : NonEmptyList α} : l.tail = l.toList.tail

We can express tail in terms of the regular list obtained through toList.

@[simp]

theorem CustomBasicDatastructures.NonEmptyList.tail_singleton {α : Type u} {a : α} : (singleton a).tail = []

The tail of a singleton is empty.

@[simp]

theorem CustomBasicDatastructures.NonEmptyList.tail_cons' {α : Type u} {a : α} {as : NonEmptyList α} : (cons' a as).tail = as.toList

The tail of a cons' is everything but the first value.