Two-list queue

DefinitionPotential of a two-list queue#✓fully proved

For a queue stored as an enqueue list and a dequeue list, the potential is the length of the enqueue list: the number of elements that will be reversed when they are moved to the dequeue list.

def potential (q : Std.Queue α) : Nat :=
  q.eList.length

Used by 5

Used byAmortized cost of dequeueing · Amortized cost of enqueueing · Amortized cost of a sequence of queue operations · Linear bound on the cost of queue operations · Amortized cost of one queue operation

DefinitionModeled cost of a dequeue#✓fully proved

For a queue stored as an enqueue list and a dequeue list, the modeled cost of dequeueing is \(1\) when the dequeue list is nonempty, and \(m + 1\) when the dequeue list is empty, where \(m\) is the length of the enqueue list (the number of elements reversed when they are moved to the dequeue list).

def dequeueCost (q : Std.Queue α) : Nat :=
  if q.dList.isEmpty then q.eList.length + 1 else 1

Used by 2

Used byTimed dequeue · Amortized cost of dequeueing

DefinitionTimed enqueue#✓fully proved

Enqueueing a value \(v\) onto a two-list queue \(q\) returns the queue obtained from \(q\) by adding \(v\) at the back, that is, by prepending \(v\) to the enqueue list, together with a recorded cost of \(1\).

def enqueue (q : Std.Queue α) (value : α) : TimeM Nat (Std.Queue α) :=
  ⟨q.enqueue value, 1⟩

Used by 2

Used byAmortized cost of enqueueing · One step of a queue operation

TheoremAmortized cost of enqueueing#✓fully proved

For every two-list queue \(q\) and every value \(v\), the modeled cost of enqueueing \(v\) onto \(q\) plus the potential of the resulting queue equals the potential of \(q\) plus \(2\).

theorem enqueue_amortized (q : Std.Queue α) (value : α) :
    (enqueue q value).time + potential (enqueue q value).ret = potential q + 2

Uses 2 · Used by 1

Statement usesTimed enqueue · Potential of a two-list queue

Used byAmortized cost of one queue operation

DefinitionTimed dequeue#✓fully proved

Dequeueing from a two-list queue \(q\) returns the next element in first-in, first-out order together with the remaining queue, or returns no element together with \(q\) itself when \(q\) is empty. In both cases the recorded cost is the modeled dequeue cost of \(q\).

def dequeue (q : Std.Queue α) : TimeM Nat (Option α × Std.Queue α) :=
  ⟨match q.dequeue? with
    | none => (none, q)
    | some (value, rest) => (some value, rest),
   dequeueCost q⟩

Uses 1 · Used by 2

Statement usesModeled cost of a dequeue

Used byAmortized cost of dequeueing · One step of a queue operation

TheoremAmortized cost of dequeueing#✓fully proved

For every two-list queue \(q\), the modeled cost of dequeueing from \(q\) plus the potential of the resulting queue equals the potential of \(q\) plus \(1\). This includes the case where \(q\) is empty.

theorem dequeue_amortized (q : Std.Queue α) :
    (dequeue q).time + potential (dequeue q).ret.2 = potential q + 1

Uses 3 · Used by 1

Statement usesTimed dequeue · Potential of a two-list queue

Proof usesModeled cost of a dequeue

Used byAmortized cost of one queue operation

InductiveQueue operation#✓fully proved

A queue operation over a type \(\alpha\) is either a request to enqueue a value \(v \in \alpha\) or a request to dequeue. Sequences of such operations are used to state aggregate cost bounds.

inductive Operation (α : Type u) where
  | enqueue (value : α)
  | dequeue

Used by 7

Used byAmortized charge of a queue operation · Running a sequence of queue operations · Amortized cost of a sequence of queue operations · Linear bound on the cost of queue operations · One step of a queue operation · Amortized cost of one queue operation · Total charge of a sequence of queue operations

DefinitionAmortized charge of a queue operation#✓fully proved

The potential-method charge of a queue operation is \(2\) for an enqueue and \(1\) for a dequeue.

def Operation.charge : Operation α → Nat
  | .enqueue _ => 2
  | .dequeue => 1

Uses 1 · Used by 4

Statement usesQueue operation

Used byAmortized cost of a sequence of queue operations · Linear bound on the cost of queue operations · Amortized cost of one queue operation · Total charge of a sequence of queue operations

DefinitionOne step of a queue operation#✓fully proved

For a queue \(q\), an enqueue operation with value \(v\) performs the costed enqueue of \(v\) onto \(q\). A dequeue operation performs the costed dequeue of \(q\) and keeps the remaining queue and the cost, discarding the removed value; on an empty queue the remaining queue is \(q\) itself.

def step (q : Std.Queue α) : Operation α → TimeM Nat (Std.Queue α)
  | .enqueue value => enqueue q value
  | .dequeue =>
      let result := dequeue q
      ⟨result.ret.2, result.time⟩

Uses 3 · Used by 3

Statement usesQueue operation · Timed dequeue · Timed enqueue

Used byRunning a sequence of queue operations · Amortized cost of a sequence of queue operations · Amortized cost of one queue operation

TheoremAmortized cost of one queue operation#✓fully proved

For every queue \(q\) and every queue operation \(o\), the modeled cost of performing \(o\) on \(q\) plus the potential of the resulting queue equals the potential of \(q\) plus the charge of \(o\).

theorem step_amortized (q : Std.Queue α) (op : Operation α) :
    (step q op).time + potential (step q op).ret = potential q + op.charge

Uses 6 · Used by 1

Statement usesQueue operation · Amortized charge of a queue operation · Potential of a two-list queue · One step of a queue operation

Proof usesAmortized cost of dequeueing · Amortized cost of enqueueing

Used byAmortized cost of a sequence of queue operations

DefinitionRunning a sequence of queue operations#✓fully proved

Running a list of queue operations from a queue \(q\) performs the operations one step at a time from left to right, starting at \(q\). The result is the final queue, and the cost is the sum of the costs of the individual steps; running the empty list returns \(q\) at cost \(0\).

def run : List (Operation α) → Std.Queue α → TimeM Nat (Std.Queue α)
  | [], q => ⟨q, 0⟩
  | op :: ops, q =>
      let first := step q op
      let rest := run ops first.ret
      ⟨rest.ret, first.time + rest.time⟩

Uses 2 · Used by 2

Statement usesQueue operation · One step of a queue operation

Used byAmortized cost of a sequence of queue operations · Linear bound on the cost of queue operations

DefinitionTotal charge of a sequence of queue operations#✓fully proved

For a list of queue operations, the total charge is the sum of the amortized charges of its operations, where an enqueue is charged \(2\) and a dequeue is charged \(1\).

def totalCharge (ops : List (Operation α)) : Nat :=
  (ops.map Operation.charge).sum

Uses 2 · Used by 2

Statement usesQueue operation · Amortized charge of a queue operation

Used byAmortized cost of a sequence of queue operations · Linear bound on the cost of queue operations

TheoremAmortized cost of a sequence of queue operations#✓fully proved

For every list of queue operations and every two-list queue \(q\), the modeled cost of running the operations from left to right starting at \(q\), plus the potential of the final queue, equals the potential of \(q\) plus the total charge of the operations.

theorem run_amortized (ops : List (Operation α)) (q : Std.Queue α) :
    (run ops q).time + potential (run ops q).ret = potential q + totalCharge ops

Uses 7 · Used by 1

Statement usesQueue operation · Potential of a two-list queue · Running a sequence of queue operations · Total charge of a sequence of queue operations

Proof usesAmortized charge of a queue operation · One step of a queue operation · Amortized cost of one queue operation

Used byLinear bound on the cost of queue operations

TheoremLinear bound on the cost of queue operations#✓fully proved

For every list of \(n\) queue operations and every two-list queue \(q\), the modeled cost of running the operations from left to right starting at \(q\) is at most the potential of \(q\) plus \(2n\).

theorem run_time_le_potential_add_twice_length
    (ops : List (Operation α)) (q : Std.Queue α) :
    (run ops q).time ≤ potential q + 2 * ops.length

Uses 6

Statement usesQueue operation · Potential of a two-list queue · Running a sequence of queue operations

Proof usesAmortized charge of a queue operation · Amortized cost of a sequence of queue operations · Total charge of a sequence of queue operations

DefinitionContents of a two-list queue#✓fully proved

A queue is stored as a dequeue list and an enqueue list whose most recently enqueued element comes first. Its contents are its elements in FIFO order: the dequeue list followed by the reverse of the enqueue list.

def contents (q : Std.Queue α) : List α :=
  q.dList ++ q.eList.reverse

Used by 28

Used byEnqueueing appends to the contents · A successful dequeue splits off the first element · Dequeueing fails exactly on empty queues · The queue emptiness test matches the contents · Array conversion lists the contents · The executable BFS agrees with the list model · Exact cost of BFS with parents · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS discovers vertices in nondecreasing distance · BFS lists exactly the reachable vertices · BFS discovers each vertex at most once · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · A BFS parent is one step closer to the source · BFS parents are joined by graph edges · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent · The saved-parent relation is acyclic · Breadth-first search places the source at distance zero · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · A successful topological sort lists every vertex · A successful topological sort points every edge forward · A successful topological sort has no repeated vertex

TheoremArray conversion lists the contents#✓fully proved

For every queue \(q\), the array obtained from \(q\), read as a list, equals the contents of \(q\).

@[simp]
theorem toArray_toList (q : Std.Queue α) : q.toArray.toList = contents q

Uses 1

Statement usesContents of a two-list queue

TheoremEnqueueing appends to the contents#✓fully proved

For every queue \(q\) and value \(v\), the contents of the queue obtained by enqueueing \(v\) onto \(q\) are the contents of \(q\) followed by \(v\).

@[simp]
theorem contents_enqueue (q : Std.Queue α) (value : α) :
    contents (q.enqueue value) = contents q ++ [value]

Uses 1 · Used by 23

Statement usesContents of a two-list queue

Used byThe executable BFS agrees with the list model · Exact cost of BFS with parents · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS discovers vertices in nondecreasing distance · BFS lists exactly the reachable vertices · BFS discovers each vertex at most once · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · A BFS parent is one step closer to the source · BFS parents are joined by graph edges · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent · The saved-parent relation is acyclic · Breadth-first search places the source at distance zero · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · A successful topological sort lists every vertex · A successful topological sort points every edge forward · A successful topological sort has no repeated vertex

TheoremThe queue emptiness test matches the contents#✓fully proved

For every queue \(q\), the emptiness test of \(q\) returns true if and only if the contents of \(q\) are empty.

@[simp]
theorem isEmpty_eq_true_iff (q : Std.Queue α) :
    q.isEmpty = true ↔ contents q = []

Uses 1

Statement usesContents of a two-list queue

TheoremDequeueing fails exactly on empty queues#✓fully proved

For every queue \(q\), dequeueing \(q\) returns nothing if and only if the contents of \(q\) are empty.

@[simp]
theorem dequeue?_eq_none_iff (q : Std.Queue α) :
    q.dequeue? = none ↔ contents q = []

Uses 1 · Used by 12

Statement usesContents of a two-list queue

Used byThe executable BFS agrees with the list model · Exact cost of BFS with parents · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS discovers vertices in nondecreasing distance · BFS lists exactly the reachable vertices · BFS discovers each vertex at most once · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · A successful topological sort lists every vertex · A successful topological sort points every edge forward · A successful topological sort has no repeated vertex

TheoremA successful dequeue splits off the first element#✓fully proved

If dequeueing a queue \(q\) succeeds and returns an element \(a\) and a queue \(r\), then the contents of \(q\) are \(a\) followed by the contents of \(r\).

theorem contents_eq_cons_of_dequeue?_eq_some
    {q : Std.Queue α} {head : α} {rest : Std.Queue α}
    (h : q.dequeue? = some (head, rest)) :
    contents q = head :: contents rest

Uses 1 · Used by 23

Statement usesContents of a two-list queue

Used byThe executable BFS agrees with the list model · Exact cost of BFS with parents · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS discovers vertices in nondecreasing distance · BFS lists exactly the reachable vertices · BFS discovers each vertex at most once · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · A BFS parent is one step closer to the source · BFS parents are joined by graph edges · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent · The saved-parent relation is acyclic · Breadth-first search places the source at distance zero · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · A successful topological sort lists every vertex · A successful topological sort points every edge forward · A successful topological sort has no repeated vertex

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.