Cartesian tree

DefinitionMin-heap ordered binary tree#✓fully proved

Let \(\alpha\) be a type with a relation \(\le\). A binary tree with keys in \(\alpha\) is min-heap ordered when, at every node, the key \(k\) of that node satisfies \(k \le y\) for every key \(y\) in its left subtree and every key \(y\) in its right subtree. The empty tree is min-heap ordered.

public def HeapOrdered [LE α] : BinaryTree α → Prop
  | .nil => True
  | .node key left right =>
      HeapOrdered left ∧ HeapOrdered right ∧
        BinarySearchTree.All (key ≤ ·) left ∧
        BinarySearchTree.All (key ≤ ·) right

Uses 1 · Used by 2

Statement usesA predicate holding at every key of a binary tree

Used byCartesian trees are heap-ordered · The root of a heap-ordered tree is below every key

DefinitionOptional root key of a binary tree#✓fully proved

For a binary tree \(T\) with keys in \(\alpha\), the root key of \(T\) is an optional element of \(\alpha\): it is absent (none) when \(T\) is empty, and it is \(k\) when the top node of \(T\) holds the key \(k\).

public def root : BinaryTree α → Option α
  | .nil => none
  | .node key _ _ => some key

Used by 4

Used byThe root of a binary tree is one of its keys · The Cartesian tree of a nonempty list has a root · The root of a Cartesian tree is a minimum of the list · The root of a heap-ordered tree is below every key

TheoremA predicate holds on every key iff it holds along the inorder traversal#✓fully proved

For every predicate \(p\) on \(\alpha\) and every binary tree \(T\) with keys in \(\alpha\), every key of \(T\) satisfies \(p\) if and only if every element of the inorder traversal of \(T\) satisfies \(p\).

public theorem all_iff_forall_inorder {p : α → Prop} {tree : BinaryTree α} :
    BinarySearchTree.All p tree ↔
      ∀ x ∈ BinarySearchTree.inorder tree, p x

Uses 5 · Used by 1

Statement usesA predicate holding at every key of a binary tree · Inorder traversal of a binary tree

Proof usesMembership in a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members · Membership in the inorder traversal of a binary tree

Used byCartesian trees are heap-ordered

TheoremThe root of a binary tree is one of its keys#✓fully proved

For every binary tree \(T\) and every key \(k\), if \(T\) is nonempty with root key \(k\), then \(k\) is a key of \(T\).

public theorem mem_of_root_eq_some {tree : BinaryTree α} {key : α}
    (hRoot : root tree = some key) : key ∈ tree

Uses 2 · Used by 1

Statement usesMembership in a binary tree · Optional root key of a binary tree

Used byThe root of a Cartesian tree is a minimum of the list

TheoremThe root of a heap-ordered tree is below every key#✓fully proved

Let \(T\) be a binary tree over a preordered type that is heap-ordered (in min-heap order). If \(T\) has root key \(k\), then \(k \le x\) for every key \(x\) occurring in \(T\).

public theorem root_le_of_heapOrdered [Preorder α] {tree : BinaryTree α}
    {key : α}
    (hHeap : HeapOrdered tree) (hRoot : root tree = some key) :
    ∀ x ∈ tree, key ≤ x

Uses 5 · Used by 1

Statement usesMembership in a binary tree · Min-heap ordered binary tree · Optional root key of a binary tree

Proof usesA predicate holding at every key of a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members

Used byThe root of a Cartesian tree is a minimum of the list

16 fully proved

Split At First

DefinitionSplitting a list at the first occurrence of a value#✓fully proved

For a value \(m\) of a type with decidable equality and a list \(xs\), the split of \(xs\) at \(m\) is the pair of the part of \(xs\) before the first occurrence of \(m\) and the part after it; that occurrence itself is dropped. If \(m\) does not occur in \(xs\), the split is the pair of \(xs\) and the empty list.

Only equality on the element type is needed, not the linear order required to build Cartesian trees.

public def splitAtFirst (m : α) : List α → List α × List α
  | [] => ([], [])
  | a :: as =>
      if a = m then ([], as)
      else
        let rest := splitAtFirst m as
        (a :: rest.1, rest.2)

Used by 5

Used byFuel-bounded Cartesian tree construction · Cartesian trees are heap-ordered · Inorder traversal of a Cartesian tree · The Cartesian tree of a nonempty list has a root · Splitting at the first occurrence leaves the value out of the left part

TheoremSplitting at the first occurrence leaves the value out of the left part#✓fully proved

Let \(m\) be an element of a type with decidable equality and let \(xs\) be a list in which \(m\) occurs. When \(xs\) is split at the first occurrence of \(m\), the left part does not contain \(m\).

Together with the reconstruction property (the left part, then \(m\), then the right part give back \(xs\)), this characterizes the split point, including how duplicates of \(m\) are handled when building Cartesian trees; reconstruction alone would hold for a split at any occurrence.

public theorem splitAtFirst_not_mem_fst (m : α) :
    ∀ (xs : List α), m ∈ xs → m ∉ (splitAtFirst m xs).1

Uses 1

Statement usesSplitting a list at the first occurrence of a value

Build

DefinitionMinimum of a nonempty list#✓fully proved

For an element \(a\) and a list \(as\) over a linear order, the left-fold minimum of \(a\) and \(as\) is the minimum of the list with head \(a\) and tail \(as\). It is computed from the head: it equals \(a\) when \(as\) is empty, and when \(as\) has head \(b\) and tail \(bs\) it equals the left-fold minimum of \(\min(a, b)\) and \(bs\).

public def listMin (a : α) : List α → α
  | [] => a
  | b :: bs => listMin (min a b) bs

Used by 4

Used byFuel-bounded Cartesian tree construction · Cartesian trees are heap-ordered · Inorder traversal of a Cartesian tree · The Cartesian tree of a nonempty list has a root

DefinitionFuel-bounded Cartesian tree construction#✓fully proved

Let \(\alpha\) be a linear order. For a natural number \(n\) (the fuel) and a list \(xs\) over \(\alpha\), the tree built from \(xs\) with fuel \(n\) is the empty tree if \(n = 0\) or \(xs\) is empty. Otherwise \(n = k + 1\) and \(xs\) is nonempty; let \(m\) be the minimum of \(xs\), and let \(L\) and \(R\) be the parts of \(xs\) before and after the first occurrence of \(m\). Then the tree has root \(m\), its left subtree is built from \(L\) with fuel \(k\), and its right subtree is built from \(R\) with fuel \(k\).

Each split produces strictly shorter lists, so a fuel of at least the length of \(xs\) never runs out.

public def buildFuel : Nat → List α → BinaryTree α
  | 0, _ => .nil
  | _ + 1, [] => .nil
  | n + 1, (a :: as) =>
      let m := listMin a as
      let parts := splitAtFirst m (a :: as)
      .node m (buildFuel n parts.1) (buildFuel n parts.2)

Uses 2 · Used by 4

Statement usesMinimum of a nonempty list · Splitting a list at the first occurrence of a value

Used byCartesian tree of a list · Cartesian trees are heap-ordered · Inorder traversal of a Cartesian tree · The Cartesian tree of a nonempty list has a root

DefinitionCartesian tree of a list#✓fully proved

For a list \(xs\) over a linear order, the Cartesian tree of \(xs\) is the result of the fuel-bounded Cartesian tree construction on \(xs\) with fuel equal to the length of \(xs\). So the empty list gives the empty tree, and otherwise the root is the minimum \(m\) of \(xs\), the left subtree is built in the same way from the elements before the first occurrence of \(m\), and the right subtree from the elements after that occurrence.

Its inorder traversal is \(xs\) and it is min-heap ordered.

public def build (xs : List α) : BinaryTree α :=
  buildFuel xs.length xs

Uses 1 · Used by 6

Statement usesFuel-bounded Cartesian tree construction

Used byCartesian trees are heap-ordered · Inorder traversal of a Cartesian tree · Keys of a Cartesian tree · The keys of a Cartesian tree permute its input · The Cartesian tree of a nonempty list has a root · The root of a Cartesian tree is a minimum of the list

TheoremInorder traversal of a Cartesian tree#✓fully proved

For every list \(xs\) over a linear order, the inorder traversal of the Cartesian tree of \(xs\) is \(xs\).

public theorem inorder_build (xs : List α) :
    BinarySearchTree.inorder (build xs) = xs

Uses 6 · Used by 2

Statement usesInorder traversal of a binary tree · Cartesian tree of a list

Proof usesInorder traversal of a binary tree with an accumulator · Fuel-bounded Cartesian tree construction · Minimum of a nonempty list · Splitting a list at the first occurrence of a value

Used byKeys of a Cartesian tree · The keys of a Cartesian tree permute its input

TheoremThe keys of a Cartesian tree permute its input#✓fully proved

For every list \(xs\) over a linear order, the inorder traversal of the Cartesian tree of \(xs\) is a permutation of \(xs\).

public theorem perm_build (xs : List α) :
    (BinarySearchTree.inorder (build xs)).Perm xs

Uses 3

Statement usesInorder traversal of a binary tree · Cartesian tree of a list

Proof usesInorder traversal of a Cartesian tree

TheoremKeys of a Cartesian tree#✓fully proved

For every list \(xs\) over a linear order and every element \(x\), \(x\) is a key of the Cartesian tree of \(xs\) if and only if \(x\) occurs in \(xs\).

public theorem mem_build {x : α} {xs : List α} : x ∈ build xs ↔ x ∈ xs

Uses 5 · Used by 1

Statement usesMembership in a binary tree · Cartesian tree of a list

Proof usesInorder traversal of a binary tree · Membership in the inorder traversal of a binary tree · Inorder traversal of a Cartesian tree

Used byThe root of a Cartesian tree is a minimum of the list

TheoremCartesian trees are heap-ordered#✓fully proved

For every list \(xs\) over a linear order, the Cartesian tree of \(xs\) is min-heap ordered.

public theorem heapOrdered_build (xs : List α) : HeapOrdered (build xs)

Uses 9 · Used by 1

Statement usesMin-heap ordered binary tree · Cartesian tree of a list

Proof usesA predicate holding at every key of a binary tree · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · A predicate holds on every key iff it holds along the inorder traversal · Fuel-bounded Cartesian tree construction · Minimum of a nonempty list · Splitting a list at the first occurrence of a value

Used byThe root of a Cartesian tree is a minimum of the list

TheoremThe Cartesian tree of a nonempty list has a root#✓fully proved

For every nonempty list \(xs\) over a linearly ordered type, the Cartesian tree of \(xs\) has a root key \(m\).

public theorem root_build_cons_isSome (a : α) (as : List α) :
    ∃ m, root (build (a :: as)) = some m

Uses 5

Statement usesCartesian tree of a list · Optional root key of a binary tree

Proof usesFuel-bounded Cartesian tree construction · Minimum of a nonempty list · Splitting a list at the first occurrence of a value

TheoremThe root of a Cartesian tree is a minimum of the list#✓fully proved

Let \(xs\) be a list over a linearly ordered type. If the Cartesian tree of \(xs\) has root key \(m\), then \(m\) occurs in \(xs\) and \(m \le y\) for every element \(y\) of \(xs\).

public theorem root_build_min {xs : List α} {m : α}
    (hRoot : root (build xs) = some m) :
    m ∈ xs ∧ ∀ y ∈ xs, m ≤ y

Uses 7

Statement usesCartesian tree of a list · Optional root key of a binary tree

Proof usesMembership in a binary tree · Cartesian trees are heap-ordered · Keys of a Cartesian tree · The root of a binary tree is one of its keys · The root of a heap-ordered tree is below every key

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.