Double-ended queue

19 fully proved

Deque

StructureTwo-list deque#✓fully proved

A deque with elements in a type \(\alpha\) consists of two lists of elements of \(\alpha\), the front list and the back list. The front list holds the front part of the sequence in order and the back list holds the back part in reverse order.

structure Deque (α : Type u) where
  front : List α
  back : List α

Used by 18

Used byRepresented sequence of a deque · Popping the back of a deque · Popping the front of a deque · Pushing at the back of a deque · Pushing at the front of a deque · The empty deque · Emptiness test for a deque · Correctness of the deque emptiness test · Peek at the back of a deque · Peeking at the back of a deque · Peek at the front of a deque · Peeking at the front gives the first element · Pop the back of a deque · Popping the back fails exactly on empty deques · Pop the front of a deque · Popping the front fails exactly on empty deques · Push at the back of a deque · Push at the front of a deque

DefinitionRepresented sequence of a deque#✓fully proved

The sequence represented by a deque with front list \(f\) and back list \(b\) is \(f\) followed by the reverse of \(b\); it lists the elements from front to back.

def contents (d : Deque α) : List α :=
  d.front ++ d.back.reverse

Uses 1 · Used by 9

Statement usesTwo-list deque

Used byPopping the back of a deque · Popping the front of a deque · Pushing at the back of a deque · Pushing at the front of a deque · Correctness of the deque emptiness test · Peeking at the back of a deque · Peeking at the front gives the first element · Popping the back fails exactly on empty deques · Popping the front fails exactly on empty deques

DefinitionThe empty deque#✓fully proved

The empty deque is the deque whose front list and back list are both empty.

def empty : Deque α :=
  ⟨[], []⟩

Uses 1

Statement usesTwo-list deque

DefinitionEmptiness test for a deque#✓fully proved

The emptiness test of a deque returns true exactly when both its front list and its back list are empty.

def isEmpty (d : Deque α) : Bool :=
  d.front.isEmpty && d.back.isEmpty

Uses 1 · Used by 1

Statement usesTwo-list deque

Used byCorrectness of the deque emptiness test

TheoremCorrectness of the deque emptiness test#✓fully proved

For every deque \(d\), the emptiness test of \(d\) returns true if and only if the sequence represented by \(d\) is empty.

@[simp]
theorem isEmpty_eq_true_iff (d : Deque α) :
    d.isEmpty = true ↔ contents d = []

Uses 3

Statement usesTwo-list deque · Represented sequence of a deque · Emptiness test for a deque

DefinitionPush at the front of a deque#✓fully proved

Let \(d\) be a deque with front list \(f\) and back list \(b\), where \(b\) is stored in reverse order. Pushing an element \(x\) at the front of \(d\) gives the deque with front list consisting of \(x\) followed by the entries of \(f\), and back list \(b\).

def pushFront (d : Deque α) (value : α) : Deque α :=
  ⟨value :: d.front, d.back⟩

Uses 1 · Used by 1

Statement usesTwo-list deque

Used byPushing at the front of a deque

TheoremPushing at the front of a deque#✓fully proved

For every deque \(d\) and element \(x\), the sequence represented by the deque obtained by pushing \(x\) at the front of \(d\) is \(x\) followed by the sequence represented by \(d\).

@[simp]
theorem contents_pushFront (d : Deque α) (value : α) :
    contents (d.pushFront value) = value :: contents d

Uses 3

Statement usesTwo-list deque · Represented sequence of a deque · Push at the front of a deque

DefinitionPush at the back of a deque#✓fully proved

Let \(d\) be a deque with front list \(f\) and back list \(b\), where \(b\) is stored in reverse order. Pushing an element \(x\) at the back of \(d\) gives the deque with front list \(f\) and back list consisting of \(x\) followed by the entries of \(b\).

def pushBack (d : Deque α) (value : α) : Deque α :=
  ⟨d.front, value :: d.back⟩

Uses 1 · Used by 1

Statement usesTwo-list deque

Used byPushing at the back of a deque

TheoremPushing at the back of a deque#✓fully proved

For every deque \(d\) and element \(x\), the sequence represented by the deque obtained by pushing \(x\) at the back of \(d\) is the sequence represented by \(d\) followed by \(x\).

@[simp]
theorem contents_pushBack (d : Deque α) (value : α) :
    contents (d.pushBack value) = contents d ++ [value]

Uses 3

Statement usesTwo-list deque · Represented sequence of a deque · Push at the back of a deque

DefinitionPeek at the front of a deque#✓fully proved

Let \(d\) be a deque with front list \(f\) and back list \(b\), where \(b\) is stored in reverse order. Peeking at the front of \(d\) returns, without removing it, the first element of \(f\) when \(f\) is nonempty, and otherwise the last element of \(b\); when both lists are empty it returns no element.

def peekFront : Deque α → Option α
  | ⟨value :: _, _⟩ => some value
  | ⟨[], back⟩ => back.getLast?

Uses 1 · Used by 1

Statement usesTwo-list deque

Used byPeeking at the front gives the first element

TheoremPeeking at the front gives the first element#✓fully proved

For every deque \(d\), peeking at the front of \(d\) returns the first element of the sequence represented by \(d\), and returns no element when that sequence is empty.

@[simp]
theorem peekFront_eq_head (d : Deque α) : d.peekFront = (contents d).head?

Uses 3

Statement usesTwo-list deque · Represented sequence of a deque · Peek at the front of a deque

DefinitionPeek at the back of a deque#✓fully proved

Let \(d\) be a deque with front list \(f\) and back list \(b\), where \(b\) is stored in reverse order. Peeking at the back of \(d\) returns, without removing it, the first element of \(b\) when \(b\) is nonempty, and otherwise the last element of \(f\); when both lists are empty it returns no element.

def peekBack : Deque α → Option α
  | ⟨_, value :: _⟩ => some value
  | ⟨front, []⟩ => front.getLast?

Uses 1 · Used by 1

Statement usesTwo-list deque

Used byPeeking at the back of a deque

TheoremPeeking at the back of a deque#✓fully proved

For every deque \(d\), peeking at the back of \(d\) returns the last element of the sequence represented by \(d\) when that sequence is nonempty, and returns nothing when it is empty.

@[simp]
theorem peekBack_eq_getLast (d : Deque α) : d.peekBack = (contents d).getLast?

Uses 3

Statement usesTwo-list deque · Represented sequence of a deque · Peek at the back of a deque

DefinitionPop the front of a deque#✓fully proved

Let \(d\) be a deque with front list \(f\) and back list \(b\), where \(b\) is stored in reverse order. If \(f\) has first element \(v\) and remaining list \(f'\), popping the front of \(d\) returns \(v\) together with the deque with front list \(f'\) and back list \(b\). If \(f\) is empty and the reverse of \(b\) has first element \(v\) and remaining list \(r\), it returns \(v\) together with the deque with front list \(r\) and empty back list. If both lists are empty, it returns no result.

def popFront : Deque α → Option (α × Deque α)
  | ⟨value :: front', back⟩ => some (value, ⟨front', back⟩)
  | ⟨[], back⟩ =>
      match back.reverse with
      | [] => none
      | value :: rest => some (value, ⟨rest, []⟩)

Uses 1 · Used by 2

Statement usesTwo-list deque

Used byPopping the front of a deque · Popping the front fails exactly on empty deques

TheoremPopping the front fails exactly on empty deques#✓fully proved

For every deque \(d\), popping the front of \(d\) returns no result if and only if the sequence represented by \(d\) is empty.

@[simp]
theorem popFront_eq_none_iff (d : Deque α) :
    d.popFront = none ↔ contents d = []

Uses 3

Statement usesTwo-list deque · Represented sequence of a deque · Pop the front of a deque

TheoremPopping the front of a deque#✓fully proved

If popping the front of a deque \(d\) succeeds and returns an element \(x\) and a deque \(d'\), then the sequence represented by \(d\) is \(x\) followed by the sequence represented by \(d'\).

theorem contents_eq_cons_of_popFront_eq_some
    {d : Deque α} {head : α} {rest : Deque α}
    (h : d.popFront = some (head, rest)) :
    contents d = head :: contents rest

Uses 3

Statement usesTwo-list deque · Represented sequence of a deque · Pop the front of a deque

DefinitionPop the back of a deque#✓fully proved

Let \(d\) be a deque with front list \(f\) and back list \(b\), where \(b\) is stored in reverse order. If \(b\) has first element \(v\) and remaining list \(b'\), popping the back of \(d\) returns \(v\) together with the deque with front list \(f\) and back list \(b'\). If \(b\) is empty and the reverse of \(f\) has first element \(v\) and remaining list \(r\), it returns \(v\) together with the deque with empty front list and back list \(r\). If both lists are empty, it returns no result.

def popBack : Deque α → Option (α × Deque α)
  | ⟨front, value :: back'⟩ => some (value, ⟨front, back'⟩)
  | ⟨front, []⟩ =>
      match front.reverse with
      | [] => none
      | value :: rest => some (value, ⟨[], rest⟩)

Uses 1 · Used by 2

Statement usesTwo-list deque

Used byPopping the back of a deque · Popping the back fails exactly on empty deques

TheoremPopping the back fails exactly on empty deques#✓fully proved

For every deque \(d\), popping the back of \(d\) returns no result if and only if the sequence represented by \(d\) is empty.

@[simp]
theorem popBack_eq_none_iff (d : Deque α) :
    d.popBack = none ↔ contents d = []

Uses 3

Statement usesTwo-list deque · Represented sequence of a deque · Pop the back of a deque

TheoremPopping the back of a deque#✓fully proved

If popping the back of a deque \(d\) succeeds and returns an element \(x\) and a deque \(d'\), then the sequence represented by \(d\) is the sequence represented by \(d'\) followed by \(x\).

theorem contents_eq_append_of_popBack_eq_some
    {d : Deque α} {last : α} {rest : Deque α}
    (h : d.popBack = some (last, rest)) :
    contents d = contents rest ++ [last]

Uses 3

Statement usesTwo-list deque · Represented sequence of a deque · Pop the back of a deque

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.