InfiniteList

A note in the beginning: We mimic Mathlib's Stream' 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 an InfiniteList as a function from the naturals into the desired type. We abstract away from this using many convenience functions. For example, we offer head and tail to give the list a more coinductive flavor. Also, there is mem_rec as a recursor over list elements to allow showing properties of list members via induction. Furthermore, we offer a generate function that can build an infinite list from a function that builds a new element from a previous one.

def InfiniteList (α : Type u) : Type u

An InfiniteList is defined as a function from the naturals into the desired type.

Equations

• InfiniteList α = (Nat → α)

Basics

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

def InfiniteList.get {α : Type u_1} (l : InfiniteList α) (n : Nat) : α

Obtains the nth element from the list.

Equations

• l.get n = l n

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

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

Equations

• l.drop n i = l.get (n + i)

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

Returns the first element.

Equations

• l.head = l.get 0

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

Drops the first element.

Equations

• l.tail n = l.get n.succ

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

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

Equations

• InfiniteList.cons hd tl Nat.zero = hd
• InfiniteList.cons hd tl n.succ = tl n

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

Equations

• InfiniteList.instMembership = { mem := fun (l : InfiniteList α) (a : α) => ∃ (n : Nat), l.get n = a }

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

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

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

theorem InfiniteList.get_mem {α : Type u_1} {l : InfiniteList α} {n : Nat} : l.get n ∈ l

Each element we can get is in the list.

theorem InfiniteList.get_drop {α : Type u_1} {l : InfiniteList α} {n i : Nat} : (l.drop n).get i = l.get (n + i)

Get after drop can be rewritten into get.

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

Dropping zero elements changes nothing.

theorem InfiniteList.head_mem {α : Type u_1} {l : InfiniteList α} : l.head ∈ l

The head is in the list.

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

Getting the head after dropping n equals getting n.

theorem InfiniteList.tail_eq {α : Type u_1} {l : InfiniteList α} : l.tail = fun (n : Nat) => l.get n.succ

Helper theorem stating the definition of tail.

theorem InfiniteList.get_tail {α : Type u_1} {l : InfiniteList α} (n : Nat) : l.tail.get n = l.get n.succ

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

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

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

theorem InfiniteList.get_cons_zero {α : Type u_1} {hd : α} {tl : InfiniteList α} : (cons hd tl).get 0 = hd

Getting the first element on cons is the new head.

theorem InfiniteList.get_cons_succ {α : Type u_1} {hd : α} {tl : InfiniteList α} (n : Nat) : (cons hd tl).get n.succ = tl.get n

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

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

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

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

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

theorem InfiniteList.cons_head_tail {α : Type u_1} (l : InfiniteList α) : l = cons l.head l.tail

Any InfiniteList can be written using the cons constructor.

Suffixes

Here, we define a suffix relation on InfiniteList 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 InfiniteList.IsSuffix {α : Type u_1} (l1 l2 : InfiniteList α) : Prop

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

Equations

• (l1 <:+ l2) = ∃ (n : Nat), l2.drop n = l1

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

Equations

• InfiniteList.«term_<:+_» = Lean.ParserDescr.trailingNode `InfiniteList.«term_<:+_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <:+ ") (Lean.ParserDescr.cat `term 51))

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

The suffix relation is reflexive.

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

The suffix relation is transitive.

theorem InfiniteList.suffix_or_suffix_of_suffix {α : Type u_1} {l1 l2 l3 : InfiniteList α} : 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 InfiniteList.mem_of_mem_suffix {α : Type u_1} {l1 l2 : InfiniteList α} (suffix : l1 <:+ l2) (e : α) : e ∈ l1 → e ∈ l2

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

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

Dropping elements yields a suffix.

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

The tail is a suffix.

Recursor for Members

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

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

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

Equations

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

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

A recursor for proving properties about list members (Elements) via induction.

Map

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

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

Applies a function to each list element.

Equations

• l.map f n = f (l.get n)

theorem InfiniteList.get_map {α : Type u_1} {β : Type u_2} {l : InfiniteList α} {f : α → β} {n : Nat} : (l.map f).get n = f (l.get n)

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

theorem InfiniteList.mem_map {α : Type u_1} {β : Type u_2} {l : InfiniteList α} {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.

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

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

Generating an InfiniteList

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

def InfiniteList.iterate {α : Type u_1} (start : α) (generator : α → α) : InfiniteList α

Construct an infinite list by repeating a generator function. This is essentially Stream'.iterate from Mathlib.

Equations

• InfiniteList.iterate start generator Nat.zero = start
• InfiniteList.iterate start generator n.succ = generator (InfiniteList.iterate start generator n)

theorem InfiniteList.get_succ_iterate {α : Type u_1} {start : α} {generator : α → α} (n : Nat) : (iterate start generator).get n.succ = generator ((iterate start generator).get n)

When getting the successor of a number n from an interated list, we can instead get the nth element and apply the generator once mode.

theorem InfiniteList.get_succ_iterate' {α : Type u_1} {start : α} {generator : α → α} (n : Nat) : (iterate start generator).get n.succ = (iterate (generator start) generator).get n

When getting the successor of a number n from an interated list, we can instead apply the generator once initially, then iterate and then get the nth element.

theorem InfiniteList.get_add_iterate {α : Type u_1} {start : α} {generator : α → α} (n m : Nat) : (iterate start generator).get (n + m) = (iterate ((iterate start generator).get n) generator).get m

When getting the sum of two numbers n+m from an interated list, we can instead generate the nth value, and use that as the starting value for another m iterations.

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

Instead of only iterating, we may want to create a kind of "carrier" list and then map this to the actually desired list. This is useful when the generator function requires more information that what actually ends up being in the desired list. Note that this is essentially the same as Stream'.corec from Mathlib.

Equations

• InfiniteList.generate start generator mapper = (InfiniteList.iterate start generator).map mapper

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

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

theorem InfiniteList.get_generate {α : Type u_1} {β : Type u_2} {start : α} {generator : α → α} {mapper : α → β} (n : Nat) : (generate start generator mapper).get n = mapper ((iterate start generator).get n)

The nth element of a generated list is the mapped version of the nth element of the iterated "carrier" list.

theorem InfiniteList.get_succ_generate {α : Type u_1} {β : Type u_2} {start : α} {generator : α → α} {mapper : α → β} (n : Nat) : (generate start generator mapper).get n.succ = mapper (generator ((iterate start generator).get n))

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

theorem InfiniteList.get_succ_generate' {α : Type u_1} {β : Type u_2} {start : α} {generator : α → α} {mapper : α → β} (n : Nat) : (generate start generator mapper).get n.succ = (generate (generator start) generator mapper).get n

The successor of the nth element of a generated list can be seen as taking the nth element after initializing the generation process with the generator function already applied once in the beginning.

theorem InfiniteList.tail_generate {α : Type u_1} {β : Type u_2} {start : α} {generator : α → α} {mapper : α → β} : (generate start generator mapper).tail = generate (generator start) 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.

Take

The take function puts the first n elements of an InfiniteList into a regular List.

def InfiniteList.take {α : Type u_1} (l : InfiniteList α) : Nat → List α

Obtain a finite list from an infinite list by taking the first n elements.

Equations

• l.take Nat.zero = []
• l.take n.succ = l.head :: l.tail.take n

theorem InfiniteList.length_take {α : Type u_1} {l : InfiniteList α} {n : Nat} : (l.take n).length = n

The length of a taken list has exactly the desired number of elements.

theorem InfiniteList.take_zero {α : Type u_1} {l : InfiniteList α} : l.take 0 = []

When taking zero, you get nil.

theorem InfiniteList.take_succ {α : Type u_1} {l : InfiniteList α} (n : Nat) : l.take n.succ = l.head :: l.tail.take n

When taking the successor of a number n, you get the head following by taking n from the tail.

theorem InfiniteList.take_succ' {α : Type u_1} {l : InfiniteList α} (n : Nat) : l.take n.succ = l.take n ++ [l.get n]

When taking the successor of a number n, you can take n and then also take the nth element.

theorem InfiniteList.take_add {α : Type u_1} {l : InfiniteList α} (n m : Nat) : l.take (n + m) = l.take n ++ (l.drop n).take m

When taking the sum of two numbers, you take the first and then take the second after dropping the first.