Join list (catenable heap)

InductiveCatenable heap#✓fully proved

A catenable heap over a type \(\alpha\) is a persistent unsorted heap, represented as a join list (catenation tree): it is either the empty heap, an element of \(\alpha\) added in front of a catenable heap, or the join of two catenable heaps.

inductive CatenableHeap (α : Type u) : Type u where
  /-- The empty heap. -/
  | empty : CatenableHeap α
  /-- The heap with `head` added in front of `tail`. -/
  | cons (head : α) (tail : CatenableHeap α) : CatenableHeap α
  /-- The join of two heaps, with the elements of `left` before those of `right`. -/
  | join (left right : CatenableHeap α) : CatenableHeap α

Used by 38

Used byInsertion into a catenable heap · Cost and result of insertion into a catenable heap · Creating an empty catenable heap · Cost and result of creating a catenable heap · Result of insertion into a catenable heap · Result of creating a catenable heap · Result of the union of catenable heaps · Size of a catenable heap · Size of a heap with an element added in front · The empty catenable heap has size zero · Size of a catenable heap as a multiset cardinality · Insertion into a catenable heap increases its size by one · Size of a catenable heap join · A newly made catenable heap has size zero · Size of a catenable heap union · Insertion into a catenable heap costs one · Creating an empty catenable heap costs nothing · Union of catenable heaps costs one · Flattening of a catenable heap · Accumulating flattening of a catenable heap · Accumulator flattening of a catenable heap · Flattening a front node of a catenable heap · Flattening the empty catenable heap · Flattening of a catenable heap equals its naive flattening · Flattening after insertion into a catenable heap · Flattening a join of catenable heaps · A newly created catenable heap flattens to the empty list · Naive flattening of a catenable heap · Flattening a union of catenable heaps · Multiset of elements of a catenable heap · Multiset of a front node · The empty catenable heap has no elements · Insertion adds one copy of the element · Multiset of a join node · A newly made catenable heap has no elements · Union adds the multisets of elements · Union of catenable heaps · Union allocates one join node

39 fully proved

Flattening and observers

DefinitionNaive flattening of a catenable heap#✓fully proved

The naive flattening of a catenable heap is defined by recursion: the empty heap flattens to the empty list, the heap with an element \(x\) added in front of a heap \(t\) flattens to \(x\) followed by the naive flattening of \(t\), and the join of heaps \(l\) and \(r\) flattens to the naive flattening of \(l\) followed by that of \(r\).

It is the reference against which the accumulating flattening is checked.

def toListNaive : CatenableHeap α → List α
  | empty => []
  | cons head tail => head :: toListNaive tail
  | join left right => toListNaive left ++ toListNaive right

Uses 1 · Used by 4

Statement usesCatenable heap

Used byAccumulator flattening of a catenable heap · Flattening a front node of a catenable heap · Flattening of a catenable heap equals its naive flattening · Flattening a join of catenable heaps

DefinitionAccumulating flattening of a catenable heap#✓fully proved

Given a catenable heap \(h\) and a list \(s\), the accumulating flattening of \(h\) onto \(s\) is defined by recursion on \(h\): for the empty heap it is \(s\); for the heap with an element \(x\) added in front of a heap \(t\) it is \(x\) followed by the accumulating flattening of \(t\) onto \(s\); for the join of heaps \(l\) and \(r\) it is the accumulating flattening of \(l\) onto the accumulating flattening of \(r\) onto \(s\).

Each node of \(h\) is visited once.

def toListAux : CatenableHeap α → List α → List α
  | empty, acc => acc
  | cons head tail, acc => head :: toListAux tail acc
  | join left right, acc => toListAux left (toListAux right acc)

Uses 1 · Used by 3

Statement usesCatenable heap

Used byFlattening of a catenable heap · Accumulator flattening of a catenable heap · Flattening of a catenable heap equals its naive flattening

DefinitionFlattening of a catenable heap#✓fully proved

The flattening of a catenable heap \(h\) is the list of its elements from left to right, computed as the accumulating flattening of \(h\) onto the empty list.

def toList (h : CatenableHeap α) : List α :=
  toListAux h []

Uses 2 · Used by 14

Statement usesCatenable heap · Accumulating flattening of a catenable heap

Used bySize of a catenable heap · Size of a heap with an element added in front · Size of a catenable heap as a multiset cardinality · Size of a catenable heap join · Flattening a front node of a catenable heap · Flattening the empty catenable heap · Flattening of a catenable heap equals its naive flattening · Flattening after insertion into a catenable heap · Flattening a join of catenable heaps · A newly created catenable heap flattens to the empty list · Flattening a union of catenable heaps · Multiset of elements of a catenable heap · Multiset of a front node · Multiset of a join node

DefinitionMultiset of elements of a catenable heap#✓fully proved

The multiset of elements of a catenable heap \(h\) is the multiset of the entries of the left-to-right list of elements of \(h\).

def toMultiset (h : CatenableHeap α) : Multiset α :=
  (toList h : Multiset α)

Uses 2 · Used by 7

Statement usesCatenable heap · Flattening of a catenable heap

Used bySize of a catenable heap as a multiset cardinality · Multiset of a front node · The empty catenable heap has no elements · Insertion adds one copy of the element · Multiset of a join node · A newly made catenable heap has no elements · Union adds the multisets of elements

DefinitionSize of a catenable heap#✓fully proved

The size of a catenable heap is the length of its left-to-right list of elements, that is, the number of its elements counted with multiplicity.

def size (h : CatenableHeap α) : ℕ :=
  (toList h).length

Uses 2 · Used by 7

Statement usesCatenable heap · Flattening of a catenable heap

Used bySize of a heap with an element added in front · The empty catenable heap has size zero · Size of a catenable heap as a multiset cardinality · Insertion into a catenable heap increases its size by one · Size of a catenable heap join · A newly made catenable heap has size zero · Size of a catenable heap union

TheoremAccumulator flattening of a catenable heap#✓fully proved

For every catenable heap \(h\) and list \(a\), flattening \(h\) from left to right in front of the accumulator \(a\) gives the naive left-to-right flattening of \(h\) followed by \(a\).

theorem toListAux_eq (h : CatenableHeap α) (acc : List α) :
    toListAux h acc = toListNaive h ++ acc

Uses 3 · Used by 1

Statement usesCatenable heap · Accumulating flattening of a catenable heap · Naive flattening of a catenable heap

Used byFlattening of a catenable heap equals its naive flattening

TheoremFlattening of a catenable heap equals its naive flattening#✓fully proved

For every catenable heap \(h\), the flattening of \(h\) equals the naive flattening of \(h\).

theorem toList_eq_toListNaive (h : CatenableHeap α) : toList h = toListNaive h

Uses 5 · Used by 2

Statement usesCatenable heap · Flattening of a catenable heap · Naive flattening of a catenable heap

Proof usesAccumulating flattening of a catenable heap · Accumulator flattening of a catenable heap

Used byFlattening a front node of a catenable heap · Flattening a join of catenable heaps

TheoremFlattening the empty catenable heap#✓fully proved

The flattening of the empty catenable heap is the empty list.

@[simp] theorem toList_empty : toList (empty : CatenableHeap α) = []

Uses 2

Statement usesCatenable heap · Flattening of a catenable heap

TheoremFlattening a front node of a catenable heap#✓fully proved

For an element \(x\) and a catenable heap \(t\), the flattening of the heap with \(x\) added in front of \(t\) is \(x\) followed by the flattening of \(t\).

@[simp] theorem toList_cons (head : α) (tail : CatenableHeap α) :
    toList (cons head tail) = head :: toList tail

Uses 4 · Used by 3

Statement usesCatenable heap · Flattening of a catenable heap

Proof usesNaive flattening of a catenable heap · Flattening of a catenable heap equals its naive flattening

Used bySize of a heap with an element added in front · Flattening after insertion into a catenable heap · Multiset of a front node

TheoremFlattening a join of catenable heaps#✓fully proved

For catenable heaps \(l\) and \(r\), the flattening of the join of \(l\) and \(r\) is the flattening of \(l\) followed by the flattening of \(r\).

@[simp] theorem toList_join (left right : CatenableHeap α) :
    toList (join left right) = toList left ++ toList right

Uses 4 · Used by 3

Statement usesCatenable heap · Flattening of a catenable heap

Proof usesNaive flattening of a catenable heap · Flattening of a catenable heap equals its naive flattening

Used bySize of a catenable heap join · Flattening a union of catenable heaps · Multiset of a join node

TheoremThe empty catenable heap has no elements#✓fully proved

The multiset of elements of the empty catenable heap is the empty multiset.

@[simp] theorem toMultiset_empty : toMultiset (empty : CatenableHeap α) = 0

Uses 2

Statement usesCatenable heap · Multiset of elements of a catenable heap

TheoremMultiset of a front node#✓fully proved

For every element \(a\) and every catenable heap \(t\), the multiset of elements of the heap obtained by adding \(a\) in front of \(t\) is the multiset of elements of \(t\) with one more copy of \(a\).

@[simp] theorem toMultiset_cons (head : α) (tail : CatenableHeap α) :
    toMultiset (cons head tail) = head ::ₘ toMultiset tail

Uses 4 · Used by 1

Statement usesCatenable heap · Multiset of elements of a catenable heap

Proof usesFlattening of a catenable heap · Flattening a front node of a catenable heap

Used byInsertion adds one copy of the element

TheoremMultiset of a join node#✓fully proved

For all catenable heaps \(L\) and \(R\), the multiset of elements of the join node with left child \(L\) and right child \(R\) is the multiset sum of the multisets of elements of \(L\) and \(R\) (multiplicities add).

@[simp] theorem toMultiset_join (left right : CatenableHeap α) :
    toMultiset (join left right) = toMultiset left + toMultiset right

Uses 4 · Used by 1

Statement usesCatenable heap · Multiset of elements of a catenable heap

Proof usesFlattening of a catenable heap · Flattening a join of catenable heaps

Used byUnion adds the multisets of elements

TheoremThe empty catenable heap has size zero#✓fully proved

The empty catenable heap has size \(0\).

@[simp] theorem size_empty : size (empty : CatenableHeap α) = 0

Uses 2

Statement usesCatenable heap · Size of a catenable heap

TheoremSize of a heap with an element added in front#✓fully proved

For every element \(a\) and catenable heap \(t\), the size of the heap obtained by adding \(a\) in front of \(t\) is the size of \(t\) plus one.

@[simp] theorem size_cons (head : α) (tail : CatenableHeap α) :
    size (cons head tail) = size tail + 1

Uses 4 · Used by 1

Statement usesCatenable heap · Size of a catenable heap

Proof usesFlattening of a catenable heap · Flattening a front node of a catenable heap

Used byInsertion into a catenable heap increases its size by one

TheoremSize of a catenable heap join#✓fully proved

For catenable heaps \(\ell\) and \(r\), the size of the join node with left child \(\ell\) and right child \(r\) is the size of \(\ell\) plus the size of \(r\).

@[simp] theorem size_join (left right : CatenableHeap α) :
    size (join left right) = size left + size right

Uses 4 · Used by 1

Statement usesCatenable heap · Size of a catenable heap

Proof usesFlattening of a catenable heap · Flattening a join of catenable heaps

Used bySize of a catenable heap union

TheoremSize of a catenable heap as a multiset cardinality#✓fully proved

For every catenable heap \(h\), the size of \(h\) equals the cardinality of the multiset of its elements.

theorem size_eq_card_toMultiset (h : CatenableHeap α) : size h = (toMultiset h).card

Uses 4

Statement usesCatenable heap · Size of a catenable heap · Multiset of elements of a catenable heap

Proof usesFlattening of a catenable heap

Timed operations

DefinitionCreating an empty catenable heap#✓fully proved

The operation that creates a catenable heap returns the empty heap and charges cost \(0\), since it allocates no node.

def make : TimeM ℕ (CatenableHeap α) :=
  pure empty

Uses 1 · Used by 6

Statement usesCatenable heap

Used byCost and result of creating a catenable heap · Result of creating a catenable heap · A newly made catenable heap has size zero · Creating an empty catenable heap costs nothing · A newly created catenable heap flattens to the empty list · A newly made catenable heap has no elements

DefinitionInsertion into a catenable heap#✓fully proved

For an element \(x\) and a catenable heap \(h\), inserting \(x\) into \(h\) returns the heap with \(x\) added in front of \(h\) and charges cost \(1\), for the one front node it allocates.

def insert (x : α) (h : CatenableHeap α) : TimeM ℕ (CatenableHeap α) := do
  TimeM.tick 1
  pure (cons x h)

Uses 1 · Used by 6

Statement usesCatenable heap

Used byCost and result of insertion into a catenable heap · Result of insertion into a catenable heap · Insertion into a catenable heap increases its size by one · Insertion into a catenable heap costs one · Flattening after insertion into a catenable heap · Insertion adds one copy of the element

DefinitionUnion of catenable heaps#✓fully proved

The union of catenable heaps \(h_1\) and \(h_2\) allocates one join node, at cost \(1\), and returns that join node, whose left child is \(h_1\) and whose right child is \(h_2\); neither operand is traversed or changed.

def union (h₁ h₂ : CatenableHeap α) : TimeM ℕ (CatenableHeap α) := do
  TimeM.tick 1
  pure (join h₁ h₂)

Uses 1 · Used by 6

Statement usesCatenable heap

Used byResult of the union of catenable heaps · Size of a catenable heap union · Union of catenable heaps costs one · Flattening a union of catenable heaps · Union adds the multisets of elements · Union allocates one join node

TheoremCost and result of creating a catenable heap#✓fully proved

Creating a catenable heap returns the empty heap, at cost \(0\).

theorem make_eq : (make : TimeM ℕ (CatenableHeap α)) = ⟨empty, 0⟩

Uses 2

Statement usesCatenable heap · Creating an empty catenable heap

TheoremCost and result of insertion into a catenable heap#✓fully proved

For every element \(x\) and catenable heap \(h\), inserting \(x\) into \(h\) returns the heap with \(x\) added in front of \(h\), at cost exactly \(1\).

theorem insert_eq (x : α) (h : CatenableHeap α) : insert x h = ⟨cons x h, 1⟩

Uses 2

Statement usesCatenable heap · Insertion into a catenable heap

TheoremUnion allocates one join node#✓fully proved

For all catenable heaps \(h_1\) and \(h_2\), the union of \(h_1\) and \(h_2\) returns the join node whose left child is \(h_1\) and whose right child is \(h_2\), at cost \(1\).

theorem union_eq (h₁ h₂ : CatenableHeap α) : union h₁ h₂ = ⟨join h₁ h₂, 1⟩

Uses 2

Statement usesCatenable heap · Union of catenable heaps

TheoremResult of creating a catenable heap#✓fully proved

The heap returned by the operation that creates a catenable heap is the empty heap.

@[simp] theorem ret_make : (make : TimeM ℕ (CatenableHeap α)).ret = empty

Uses 2

Statement usesCatenable heap · Creating an empty catenable heap

TheoremCreating an empty catenable heap costs nothing#✓fully proved

The operation that creates an empty catenable heap has time cost \(0\).

@[simp] theorem time_make : (make : TimeM ℕ (CatenableHeap α)).time = 0

Uses 2

Statement usesCatenable heap · Creating an empty catenable heap

TheoremResult of insertion into a catenable heap#✓fully proved

For every element \(x\) and catenable heap \(h\), the heap returned by inserting \(x\) into \(h\) is the heap with \(x\) added in front of \(h\).

@[simp] theorem ret_insert (x : α) (h : CatenableHeap α) : (insert x h).ret = cons x h

Uses 2

Statement usesCatenable heap · Insertion into a catenable heap

TheoremInsertion into a catenable heap costs one#✓fully proved

For every element \(x\) and catenable heap \(h\), inserting \(x\) into \(h\) has time cost exactly \(1\).

@[simp] theorem time_insert (x : α) (h : CatenableHeap α) : (insert x h).time = 1

Uses 2

Statement usesCatenable heap · Insertion into a catenable heap

TheoremResult of the union of catenable heaps#✓fully proved

For all catenable heaps \(h_1\) and \(h_2\), the heap returned by their union is the join of \(h_1\) and \(h_2\), with \(h_1\) as left child and \(h_2\) as right child, both unchanged.

@[simp] theorem ret_union (h₁ h₂ : CatenableHeap α) : (union h₁ h₂).ret = join h₁ h₂

Uses 2

Statement usesCatenable heap · Union of catenable heaps

TheoremUnion of catenable heaps costs one#✓fully proved

For all catenable heaps \(h_1\) and \(h_2\), the union of \(h_1\) and \(h_2\) has time cost exactly \(1\), independently of \(h_1\) and \(h_2\).

@[simp] theorem time_union (h₁ h₂ : CatenableHeap α) : (union h₁ h₂).time = 1

Uses 2

Statement usesCatenable heap · Union of catenable heaps

TheoremA newly created catenable heap flattens to the empty list#✓fully proved

The flattening of the heap returned by the operation that creates a catenable heap is the empty list.

theorem toList_make : toList (make : TimeM ℕ (CatenableHeap α)).ret = []

Uses 3

Statement usesCatenable heap · Creating an empty catenable heap · Flattening of a catenable heap

TheoremFlattening after insertion into a catenable heap#✓fully proved

For an element \(x\) and a catenable heap \(h\), the flattening of the heap returned by inserting \(x\) into \(h\) is \(x\) followed by the flattening of \(h\).

theorem toList_insert (x : α) (h : CatenableHeap α) :
    toList (insert x h).ret = x :: toList h

Uses 4

Statement usesCatenable heap · Insertion into a catenable heap · Flattening of a catenable heap

Proof usesFlattening a front node of a catenable heap

TheoremFlattening a union of catenable heaps#✓fully proved

For catenable heaps \(h_1\) and \(h_2\), the flattening of the heap returned by the union of \(h_1\) and \(h_2\) is the flattening of \(h_1\) followed by the flattening of \(h_2\).

theorem toList_union (h₁ h₂ : CatenableHeap α) :
    toList (union h₁ h₂).ret = toList h₁ ++ toList h₂

Uses 4

Statement usesCatenable heap · Flattening of a catenable heap · Union of catenable heaps

Proof usesFlattening a join of catenable heaps

TheoremA newly made catenable heap has no elements#✓fully proved

The multiset of elements of the heap returned by the make operation is the empty multiset.

theorem toMultiset_make : toMultiset (make : TimeM ℕ (CatenableHeap α)).ret = 0

Uses 3

Statement usesCatenable heap · Creating an empty catenable heap · Multiset of elements of a catenable heap

TheoremInsertion adds one copy of the element#✓fully proved

For every element \(x\) and every catenable heap \(h\), the multiset of elements of the heap returned by inserting \(x\) into \(h\) is the multiset of elements of \(h\) with one more copy of \(x\).

theorem toMultiset_insert (x : α) (h : CatenableHeap α) :
    toMultiset (insert x h).ret = x ::ₘ toMultiset h

Uses 4

Statement usesCatenable heap · Insertion into a catenable heap · Multiset of elements of a catenable heap

Proof usesMultiset of a front node

TheoremUnion adds the multisets of elements#✓fully proved

For all catenable heaps \(h_1\) and \(h_2\), the multiset of elements of the heap returned by the union of \(h_1\) and \(h_2\) is the multiset sum of the multisets of elements of \(h_1\) and \(h_2\) (multiplicities add).

theorem toMultiset_union (h₁ h₂ : CatenableHeap α) :
    toMultiset (union h₁ h₂).ret = toMultiset h₁ + toMultiset h₂

Uses 4

Statement usesCatenable heap · Multiset of elements of a catenable heap · Union of catenable heaps

Proof usesMultiset of a join node

TheoremA newly made catenable heap has size zero#✓fully proved

The heap returned by the operation that creates an empty catenable heap has size \(0\).

theorem size_make : size (make : TimeM ℕ (CatenableHeap α)).ret = 0

Uses 3

Statement usesCatenable heap · Creating an empty catenable heap · Size of a catenable heap

TheoremInsertion into a catenable heap increases its size by one#✓fully proved

For every element \(x\) and catenable heap \(h\), the heap returned by inserting \(x\) into \(h\) has size one more than the size of \(h\).

theorem size_insert (x : α) (h : CatenableHeap α) : size (insert x h).ret = size h + 1

Uses 4

Statement usesCatenable heap · Insertion into a catenable heap · Size of a catenable heap

Proof usesSize of a heap with an element added in front

TheoremSize of a catenable heap union#✓fully proved

For catenable heaps \(h_1\) and \(h_2\), the heap returned by the union of \(h_1\) and \(h_2\) has size equal to the size of \(h_1\) plus the size of \(h_2\).

theorem size_union (h₁ h₂ : CatenableHeap α) :
    size (union h₁ h₂).ret = size h₁ + size h₂

Uses 4

Statement usesCatenable heap · Size of a catenable heap · Union of catenable heaps

Proof usesSize of a catenable heap join

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.