PossiblyInfiniteList

A note in the beginning: We mimic Mathlib's Stream'.Seq a lot here. Still I keep this separate to have full control about all the details. In the end, what we need should be simple enough.

This file defines a PossiblyInfiniteList which is an InfiniteList over an Option of the desired type. The offered functions are very similar to the ones of InfiniteList.

def InfiniteList.no_holes {α : Type u_1} (l : InfiniteList (Option α)) : Prop

An InfiniteList over Option has no_holes if an element being none implies its successors also being none. This is a property that we want for possibly infinite lists but we need to be able to express it on the underlying infinite list first.

Equations

• l.no_holes = ∀ (n : Nat), l.get n = none → l.get n.succ = none

structure PossiblyInfiniteList (α : Type u) : Type u

A PossiblyInfiniteList is an InfiniteList over Option that has no_holes.

• infinite_list : InfiniteList (Option α)
• no_holes : self.infinite_list.no_holes

Basics

The essential functions on infinite lists, mainly get, drop, head, and tail.

def PossiblyInfiniteList.get? {α : Type u_1} (l : PossiblyInfiniteList α) (n : Nat) : Option α

Obtains the n-th element from the list.

Equations

• l.get? n = l.infinite_list.get n

def PossiblyInfiniteList.drop {α : Type u_1} (l : PossiblyInfiniteList α) (n : Nat) : PossiblyInfiniteList α

Obtain another possibly infinite list by dropping the first n elements from the current one.

Equations

• l.drop n = { infinite_list := l.infinite_list.drop n, no_holes := ⋯ }

def PossiblyInfiniteList.head {α : Type u_1} (l : PossiblyInfiniteList α) : Option α

Returns the first element.

Equations

• l.head = l.infinite_list.head

def PossiblyInfiniteList.tail {α : Type u_1} (l : PossiblyInfiniteList α) : PossiblyInfiniteList α

Drops the first element.

Equations

• l.tail = { infinite_list := l.infinite_list.tail, no_holes := ⋯ }

def PossiblyInfiniteList.cons {α : Type u_1} (hd : α) (tl : PossiblyInfiniteList α) : PossiblyInfiniteList α

Constructs a possibly infinite list from a possibly infinite list and a new head element.

Equations

• PossiblyInfiniteList.cons hd tl = { infinite_list := InfiniteList.cons (some hd) tl.infinite_list, no_holes := ⋯ }

@[implicit_reducible]

instance PossiblyInfiniteList.instMembership {α : Type u_1} : Membership α (PossiblyInfiniteList α)

Equations

• PossiblyInfiniteList.instMembership = { mem := fun (l : PossiblyInfiniteList α) (a : α) => some a ∈ l.infinite_list }

theorem PossiblyInfiniteList.mem_iff {α : Type u_1} {l : PossiblyInfiniteList α} {e : α} : e ∈ l ↔ ∃ (n : Nat), l.get? n = some e

An element is a member of the list iff it occurs at some index.

theorem PossiblyInfiniteList.ext {α : Type u_1} {l1 l2 : PossiblyInfiniteList α} : (∀ (n : Nat), l1.get? n = l2.get? n) → l1 = l2

Two possibly infinite lists are the same of they are the same on all indices.

theorem PossiblyInfiniteList.ext_iff {α : Type u_1} {l1 l2 : PossiblyInfiniteList α} : l1 = l2 ↔ ∀ (n : Nat), l1.get? n = l2.get? n

theorem PossiblyInfiniteList.no_holes' {α : Type u_1} {l : PossiblyInfiniteList α} (n : Nat) : l.get? n = none → l.get? n.succ = none

InfiniteList.no_holes restated for the PossiblyInfiniteList.

theorem PossiblyInfiniteList.get?_eq_none_of_le_of_eq_none {α : Type u_1} {l : PossiblyInfiniteList α} {n : Nat} : l.get? n = none → ∀ (m : Nat), n ≤ m → l.get? m = none

A closed version of the no_holes property. That is, if an element is none, then not only its immediate successor but all successors are none.

@[simp]

theorem PossiblyInfiniteList.get?_drop {α : Type u_1} {l : PossiblyInfiniteList α} {n i : Nat} : (l.drop n).get? i = l.get? (n + i)

Get after drop can be rewritten into get.

@[simp]

theorem PossiblyInfiniteList.drop_zero {α : Type u_1} {l : PossiblyInfiniteList α} : l.drop 0 = l

Dropping zero elements changes nothing.

theorem PossiblyInfiniteList.head_eq {α : Type u_1} {l : PossiblyInfiniteList α} : l.head = l.get? 0

The head is the same as getting the element at index zero.

theorem PossiblyInfiniteList.head_mem {α : Type u_1} {l : PossiblyInfiniteList α} (h : α) : h ∈ l.head → h ∈ l

The head is in the list.

@[simp]

theorem PossiblyInfiniteList.head_drop {α : Type u_1} {l : PossiblyInfiniteList α} {n : Nat} : (l.drop n).head = l.get? n

Getting the head after dropping n equals getting n.

@[simp]

theorem PossiblyInfiniteList.get?_tail {α : Type u_1} {l : PossiblyInfiniteList α} (n : Nat) : l.tail.get? n = l.get? n.succ

Getting the n-th element from the tail equals getting the successor of n from the original list.

@[simp]

theorem PossiblyInfiniteList.tail_drop {α : Type u_1} {l : PossiblyInfiniteList α} {n : Nat} : (l.drop n).tail = l.drop n.succ

Getting the tail after dropping n is the same as dropping n.succ.

@[simp]

theorem PossiblyInfiniteList.get?_cons_zero {α : Type u_1} {hd : α} {tl : PossiblyInfiniteList α} : (cons hd tl).get? 0 = some hd

Getting the first element on cons is the new head.

@[simp]

theorem PossiblyInfiniteList.get?_cons_succ {α : Type u_1} {hd : α} {tl : PossiblyInfiniteList α} (n : Nat) : (cons hd tl).get? n.succ = tl.get? n

Getting any index > 0 on cons yields the respective element from the previous possibly infinite list.

@[simp]

theorem PossiblyInfiniteList.head_cons {α : Type u_1} (hd : α) (tl : PossiblyInfiniteList α) : (cons hd tl).head = some hd

The head of cons is the head used in the construction.

@[simp]

theorem PossiblyInfiniteList.tail_cons {α : Type u_1} (hd : α) (tl : PossiblyInfiniteList α) : (cons hd tl).tail = tl

The tail of cons is the list used in the construction.

theorem PossiblyInfiniteList.cons_head_tail {α : Type u_1} (l : PossiblyInfiniteList α) (hd : α) (h : l.head = some hd) : l = cons hd l.tail

Any PossiblyInfiniteList can be written using the cons constructor.

Suffixes

Here, we define a suffix relation on PossiblyInfiniteList inspired by List.IsSuffix. For l1 and l2, l1 <:+ l2 denotes that l1 is a suffix of l2.

The suffix relation is reflexive and transitive but not necesarrily antisymmetric!

def PossiblyInfiniteList.IsSuffix {α : Type u_1} (l1 l2 : PossiblyInfiniteList α) : Prop

A suffix relation on possibly infinite lists. This is inspired by List.IsSuffix. Read l1 <:+ l2 as: l1 is a suffix of l2.

Equations

• (l1 <:+ l2) = (l1.infinite_list <:+ l2.infinite_list)

def PossiblyInfiniteList.«term_<:+_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem PossiblyInfiniteList.IsSuffix_iff {α : Type u_1} {l1 l2 : PossiblyInfiniteList α} : l1 <:+ l2 ↔ ∃ (n : Nat), l2.drop n = l1

l1 is a suffix of l2 if l1 can be obtained from l2 by dropping some elements.

theorem PossiblyInfiniteList.IsSuffix_refl {α : Type u_1} {l : PossiblyInfiniteList α} : l <:+ l

The suffix relation is reflexive.

theorem PossiblyInfiniteList.IsSuffix_trans {α : Type u_1} {l1 l2 l3 : PossiblyInfiniteList α} : l1 <:+ l2 → l2 <:+ l3 → l1 <:+ l3

The suffix relation is transitive.

theorem PossiblyInfiniteList.suffix_or_suffix_of_suffix {α : Type u_1} {l1 l2 l3 : PossiblyInfiniteList α} : l1 <:+ l3 → l2 <:+ l3 → l1 <:+ l2 ∨ l2 <:+ l1

Two suffixes of the same list must be suffixes of each other in some way. This is similar to List.suffix_or_suffix_of_suffix.

theorem PossiblyInfiniteList.mem_of_mem_suffix {α : Type u_1} {l1 l2 : PossiblyInfiniteList α} (suffix : l1 <:+ l2) (e : α) : e ∈ l1 → e ∈ l2

A member of a suffix is also a member of the current list.

theorem PossiblyInfiniteList.IsSuffix_drop {α : Type u_1} {l : PossiblyInfiniteList α} (n : Nat) : l.drop n <:+ l

Dropping elements yields a suffix.

theorem PossiblyInfiniteList.IsSuffix_tail {α : Type u_1} {l : PossiblyInfiniteList α} : l.tail <:+ l

The tail is a suffix.

Recursor for Members

We define a recursion (induction) principle for members (Elements) of a PossiblyInfiniteList called mem_rec. This can be used with the induction tactic to prove a property for each Element of a PossiblyInfiniteList. Note that for using this coveniently, the goal needs to expressed (rewritten) using an Element.

def PossiblyInfiniteList.Element {α : Type u_1} (l : PossiblyInfiniteList α) : Type u_1

A list Element is a Subtype featuring a proof of being a list member.

Equations

• l.Element = { e : α // e ∈ l }

theorem PossiblyInfiniteList.mem_rec {α : Type u_1} {l : PossiblyInfiniteList α} {motive : l.Element → Prop} (head : ∀ (head : α) (mem : head ∈ l.head), motive ⟨head, ⋯⟩) (step : ∀ (l2 : PossiblyInfiniteList α) (suffix : l2 <:+ l), (∃ (head : α), ∃ (mem : head ∈ l2.head), motive ⟨head, ⋯⟩) → ∀ (tail_head : α) (mem_th : tail_head ∈ l2.tail.head), motive ⟨tail_head, ⋯⟩) (a : l.Element) : motive a

A recursor for proving properties about list members via induction.

Map

We allow to map over PossiblyInfiniteList just like List.map.

def PossiblyInfiniteList.map {α : Type u_1} {β : Type u_2} (l : PossiblyInfiniteList α) (f : α → β) : PossiblyInfiniteList β

Applies a function to each list element; just like List.map.

Equations

• l.map f = { infinite_list := l.infinite_list.map fun (o : Option α) => Option.map f o, no_holes := ⋯ }

@[simp]

theorem PossiblyInfiniteList.get?_map {α : Type u_1} {β : Type u_2} {l : PossiblyInfiniteList α} {f : α → β} {n : Nat} : (l.map f).get? n = Option.map f (l.get? n)

When getting after map, we can instead get and then apply the mapping function.

@[simp]

theorem PossiblyInfiniteList.mem_map {α : Type u_1} {β : Type u_2} {l : PossiblyInfiniteList α} {f : α → β} (e : β) : e ∈ l.map f ↔ ∃ (e' : α), e' ∈ l ∧ f e' = e

An element e is in the mapped list if there was an element that maps to e.

@[simp]

theorem PossiblyInfiniteList.head_map {α : Type u_1} {β : Type u_2} {l : PossiblyInfiniteList α} {f : α → β} : (l.map f).head = Option.map f l.head

The head of a mapped list is the same as applying the function to the head.

@[simp]

theorem PossiblyInfiniteList.tail_map {α : Type u_1} {β : Type u_2} {l : PossiblyInfiniteList α} {f : α → β} : (l.map f).tail = l.tail.map f

The tail of a mapped list is the same as applyign map to the tail.

Attach

We allow to attach membership proofs to list elements just like List.attach.

def PossiblyInfiniteList.attach {α : Type u_1} (l : PossiblyInfiniteList α) : PossiblyInfiniteList l.Element

Attaches a membership proof to each list element.

Equations

• One or more equations did not get rendered due to their size.

theorem PossiblyInfiniteList.val_get?_attach {α : Type u_1} {l : PossiblyInfiniteList α} {n : Nat} : Option.map (fun (e : l.Element) => e.val) (l.attach.get? n) = l.get? n

Calling get? after attach returns the correct element with its membership proof.

Generating a PossiblyInfiniteList

We provide functions for "step-by-step" generation of a PossiblyInfiniteList from a function building a next element from an existing one. This is very similar to what is done for Mathlib's Stream'.Seq.

def PossiblyInfiniteList.generate {α : Type u_1} {β : Type u_2} (start : Option α) (generator : α → Option α) (mapper : α → β) : PossiblyInfiniteList β

Making use of InfiniteList.generate, we can also generate a PossiblyInfiniteList only that the start value and the result of the generator function are now options.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PossiblyInfiniteList.head_generate {α : Type u_1} {β : Type u_2} {start : Option α} {generator : α → Option α} {mapper : α → β} : (generate start generator mapper).head = Option.map mapper start

The head of a generated list is the mapped version of the starting value.

theorem PossiblyInfiniteList.get?_generate {α : Type u_1} {β : Type u_2} {start : Option α} {generator : α → Option α} {mapper : α → β} (n : Nat) : (generate start generator mapper).get? n = Option.map mapper ((InfiniteList.iterate start fun (x : Option α) => x.bind generator).get n)

The n-th element of a generated list is the mapped version of the n-th element of the iterated "carrier" list.

theorem PossiblyInfiniteList.get?_succ_generate {α : Type u_1} {β : Type u_2} {start : Option α} {generator : α → Option α} {mapper : α → β} (n : Nat) : (generate start generator mapper).get? n.succ = Option.map mapper (((InfiniteList.iterate start fun (x : Option α) => x.bind generator).get n).bind generator)

The successor of the n-th element of a generated list can be seen as applying the mapper function after the generator function after taking the n-th element from the iterated "carrier" list.

theorem PossiblyInfiniteList.tail_generate {α : Type u_1} {β : Type u_2} {start : Option α} {generator : α → Option α} {mapper : α → β} : (generate start generator mapper).tail = generate (start.bind generator) generator mapper

The tail of a generated list is the list generated when applying the generator function once on the starting element before the actual generation.

Empty Infinite Lists

The empty PossiblyInfiniteList is simply the PossiblyInfiniteList that is none on all indices.

def PossiblyInfiniteList.empty {α : Type u_1} : PossiblyInfiniteList α

The empty PossiblyInfiniteList is none everywhere.

Equations

• PossiblyInfiniteList.empty = { infinite_list := fun (x : Nat) => none, no_holes := ⋯ }

@[simp]

theorem PossiblyInfiniteList.get?_empty {α : Type u_1} {n : Nat} : empty.get? n = none

Getting from the empty list always returns none.

@[simp]

theorem PossiblyInfiniteList.head_empty {α : Type u_1} : empty.head = none

The head of the empty list is none.

@[simp]

theorem PossiblyInfiniteList.map_empty {β : Type u_1} {α : Type u_2} {f : α → β} : empty.map f = empty

The empty list stays empty when mapped.

theorem PossiblyInfiniteList.empty_iff_head_none {α : Type u_1} {l : PossiblyInfiniteList α} : l = empty ↔ l.head = none

A PossiblyInfiniteList is empty if and only if its head is none.

Finite PossiblyInfiniteList

We define when we consider a PossiblyInfiniteList to be finite, namely when it is none on some index. We also define a function converting a finite PossiblyInfiniteList into a plain List.

def PossiblyInfiniteList.finite {α : Type u_1} (l : PossiblyInfiniteList α) : Prop

The PossiblyInfiniteList is finite if some element is none.

Equations

• l.finite = ∃ (k : Nat), l.get? k = none

def PossiblyInfiniteList.toList_of_finite {α : Type u_1} (l : PossiblyInfiniteList α) (fin : l.finite) : List α

Transforms a finite list into an inductive List.

Equations

• l.toList_of_finite fin = PossiblyInfiniteList.toList_of_finite.loop✝ l fin 0

theorem PossiblyInfiniteList.map_finite_of_finite {α : Type u_1} {β : Type u_2} {l : PossiblyInfiniteList α} {f : α → β} : l.finite → (l.map f).finite

A mapped list is finite if the original list is finite.

theorem PossiblyInfiniteList.finite_empty {α : Type u_1} : empty.finite

The empty list is finite.

@[simp]

theorem PossiblyInfiniteList.getElem?_toList_of_finite {α : Type u_1} {l : PossiblyInfiniteList α} {fin : l.finite} {n : Nat} : (l.toList_of_finite fin)[n]? = l.get? n

The n-th element in the transformed list is the n-th element from the original list.

@[simp]

theorem PossiblyInfiniteList.mem_toList_of_finite {α : Type u_1} {l : PossiblyInfiniteList α} {fin : l.finite} {e : α} : e ∈ l.toList_of_finite fin ↔ e ∈ l

An element is in the transformed finite list if and only if it is in the original list.

@[simp]

theorem PossiblyInfiniteList.map_toList_of_finite {α : Type u_1} {β : Type u_2} {l : PossiblyInfiniteList α} {fin : l.finite} {f : α → β} : List.map f (l.toList_of_finite fin) = (l.map f).toList_of_finite ⋯

Mapping over the transformed finite list is the same as mapping first and then transforming.

theorem PossiblyInfiniteList.toList_of_finite_empty_iff {α : Type u_1} {l : PossiblyInfiniteList α} {fin : l.finite} : l.toList_of_finite fin = [] ↔ l = empty

The transformed list is empty if and only if the original list is empty.

Converting a List into a PossiblyInfiniteList

We can always convert a plain List into a PossiblyInfiniteList by setting all indices beyond the length of the list to none.

def PossiblyInfiniteList.from_list {α : Type u_1} (l : List α) : PossiblyInfiniteList α

Builds a PossiblyInfiniteList from an inductive List.

Equations

• PossiblyInfiniteList.from_list l = { infinite_list := fun (n : Nat) => l[n]?, no_holes := ⋯ }

@[simp]

theorem PossiblyInfiniteList.get?_from_list {α : Type u_1} {l : List α} {n : Nat} : (from_list l).get? n = l[n]?

After building from a List, the n-th elements are the same.

theorem PossiblyInfiniteList.finite_from_list {α : Type u_1} {l : List α} : (from_list l).finite

When building from a List, the PossiblyInfiniteList is finite.

@[simp]

theorem PossiblyInfiniteList.toList_of_finite_after_from_list {α : Type u_1} {l : List α} : (from_list l).toList_of_finite ⋯ = l

Transforming a List to a PossiblyInfiniteList and back, gives the original list.