Stack with multipop

DefinitionStack push#✓fully proved

Stacks over a type \(\alpha\) are lists of elements of \(\alpha\), with the first element as the top. Pushing \(v \in \alpha\) onto a stack \(s\) returns the stack with top \(v\) followed by the elements of \(s\), at cost \(1\) (one successful push event).

def push {α : Type u} (stack : List α) (value : α) : TimeM Nat (List α) := do
  TimeM.tick 1
  pure (value :: stack)

Used by 2

Used byRunning a PUSH agrees with the standalone PUSH · Result and cost of the stack operations

DefinitionStack pop#✓fully proved

Stacks over a type \(\alpha\) are lists of elements of \(\alpha\), with the first element as the top. Popping the empty stack returns underflow (no value) at cost \(0\). Popping a stack with top \(v\) and remaining stack \(t\) returns the pair \((v, t)\) at cost \(1\) (one successful pop event).

def pop {α : Type u} : List α → TimeM Nat (Option (α × List α))
  | [] => pure none
  | value :: tail => do
    TimeM.tick 1
    pure (some (value, tail))

Used by 3

Used byRunning a POP agrees with the standalone POP · Result and cost of the stack operations · Result and cost of stack pop

DefinitionStack top#✓fully proved

Stacks over a type \(\alpha\) are lists of elements of \(\alpha\), with the first element as the top. Reading the top of the empty stack returns underflow (no value) at cost \(0\). Reading the top of a stack with top \(v\) returns \(v\) at cost \(1\) (one successful top event); the stack itself is not returned or changed.

def top {α : Type u} : List α → TimeM Nat (Option α)
  | [] => pure none
  | value :: _ => do
    TimeM.tick 1
    pure (some value)

Used by 2

Used byResult and cost of the stack operations · Result and cost of reading the stack top

TheoremResult and cost of stack pop#✓fully proved

Let \(s\) be a stack over a type \(\alpha\) (a list of elements of \(\alpha\) whose first element is the top). If \(s\) is empty, popping \(s\) returns underflow (no value) at cost \(0\). If \(s\) has top \(h\) and remaining stack \(t\), popping \(s\) returns the pair \((h, t)\) at cost \(1\).

This holds for every type \(\alpha\); no element of \(\alpha\) is assumed to exist.

theorem pop_eq {α : Type u} (stack : List α) :
    pop stack = (match stack with
      | [] => ⟨none, 0⟩
      | head :: tail => ⟨some (head, tail), 1⟩)

Uses 1

Statement usesStack pop

TheoremResult and cost of reading the stack top#✓fully proved

Let \(s\) be a stack over a type \(\alpha\) (a list of elements of \(\alpha\) whose first element is the top). If \(s\) is empty, reading the top of \(s\) returns underflow (no value) at cost \(0\). If \(s\) has top \(h\), reading the top of \(s\) returns \(h\) at cost \(1\).

This holds for every type \(\alpha\); no element of \(\alpha\) is assumed to exist.

theorem top_eq {α : Type u} (stack : List α) :
    top stack = (match stack with
      | [] => ⟨none, 0⟩
      | head :: _ => ⟨some head, 1⟩)

Uses 1

Statement usesStack top

TheoremResult and cost of the stack operations#✓fully proved

Let \(\alpha\) be a type, let \(s\) be a stack over \(\alpha\) (a list of elements of \(\alpha\) whose first element is the top) and let \(v \in \alpha\). Pushing \(v\) onto \(s\) returns the stack with top \(v\) followed by the elements of \(s\), at cost \(1\). Popping \(s\) returns underflow (no value) at cost \(0\) if \(s\) is empty, and returns the pair \((h, t)\) at cost \(1\) if \(s\) has top \(h\) and remaining stack \(t\). Reading the top of \(s\) returns underflow (no value) at cost \(0\) if \(s\) is empty, and returns \(h\) at cost \(1\) if \(s\) has top \(h\).

theorem operations_spec {α : Type u} (stack : List α) (value : α) :
    push stack value = ⟨value :: stack, 1⟩ ∧
    pop stack = (match stack with
      | [] => ⟨none, 0⟩
      | head :: tail => ⟨some (head, tail), 1⟩) ∧
    top stack = (match stack with
      | [] => ⟨none, 0⟩
      | head :: _ => ⟨some head, 1⟩)

Uses 3

Statement usesStack pop · Stack push · Stack top

DefinitionMULTIPOP#✓fully proved

For a stack \(S\), stored as a list with its top first, and a natural number \(k\), MULTIPOP of \(S\) with count \(k\) repeatedly removes the top element while the stack is nonempty and fewer than \(k\) elements have been removed, and returns the remaining stack. Each removed element costs one unit, and nothing else is charged.

This is MULTIPOP from CLRS, fourth edition, Section 16.1.

public def multipop {α : Type u} : List α → Nat → TimeM Nat (List α)
  | stack, 0 => pure stack
  | [], _ + 1 => pure []
  | _ :: tail, k + 1 => do
    TimeM.tick 1
    multipop tail k

Used by 5

Used byCost balance for stack operation sequences · Result of MULTIPOP · MULTIPOP with an integer count · MULTIPOP with a nonpositive count does nothing · Cost of MULTIPOP

TheoremResult of MULTIPOP#✓fully proved

For every stack \(S\), stored as a list with its top first, and every natural number \(k\), the stack returned by MULTIPOP of \(S\) with count \(k\) is \(S\) with its top \(k\) elements removed, or the empty stack if \(S\) has fewer than \(k\) elements.

public theorem multipop_ret {α : Type u} (stack : List α) (k : Nat) :
    (multipop stack k).ret = stack.drop k

Uses 1 · Used by 1

Statement usesMULTIPOP

Used byCost balance for stack operation sequences

TheoremCost of MULTIPOP#✓fully proved

For every stack \(S\) and every natural number \(k\), the cost of MULTIPOP of \(S\) with count \(k\) is \(\min(|S|, k)\), where \(|S|\) is the number of elements of \(S\).

public theorem multipop_time {α : Type u} (stack : List α) (k : Nat) :
    (multipop stack k).time = min stack.length k

Uses 1 · Used by 1

Statement usesMULTIPOP

Used byCost balance for stack operation sequences

DefinitionMULTIPOP with an integer count#✓fully proved

For a stack \(S\) and an integer \(k\), MULTIPOP with integer count \(k\) is MULTIPOP of \(S\) with the natural count \(\max(k, 0)\), with the same result and cost. In particular, a count \(k \le 0\) removes nothing.

public def multipopSigned {α : Type u} (stack : List α) (k : Int) : TimeM Nat (List α) :=
  multipop stack k.toNat

Uses 1 · Used by 3

Statement usesMULTIPOP

Used byRunning a sequence of stack operations · Cost balance for stack operation sequences · MULTIPOP with a nonpositive count does nothing

TheoremMULTIPOP with a nonpositive count does nothing#✓fully proved

For every stack \(S\) and every integer \(k \le 0\), MULTIPOP with integer count \(k\) applied to \(S\) returns \(S\) at cost \(0\).

public theorem multipopSigned_of_nonpos {α : Type u} (stack : List α) (k : Int) (hk : k ≤ 0) :
    multipopSigned stack k = pure stack

Uses 2

Statement usesMULTIPOP with an integer count

Proof usesMULTIPOP

InductiveStack operations for the MULTIPOP aggregate analysis#✓fully proved

For a type \(\alpha\) of stack entries, a stack operation is one of the following: \(\mathrm{PUSH}(x)\) for an element \(x \in \alpha\), \(\mathrm{POP}\), or \(\mathrm{MULTIPOP}(k)\) for an integer count \(k\).

These are the operations whose sequences CLRS analyse in Section 16.1.

public inductive Operation (α : Type u) where
  | push (value : α)
  | pop
  | multipop (count : Int)
deriving Repr

Used by 5

Used byRunning a sequence of stack operations · Cost balance for stack operation sequences · Running a POP agrees with the standalone POP · Running a PUSH agrees with the standalone PUSH · Aggregate cost of stack operation sequences

DefinitionRunning a sequence of stack operations#✓fully proved

Given a stack \(S\) and a finite sequence of operations, each a PUSH of a value, a POP or a MULTIPOP with an integer count, the operations are applied to \(S\) in order. PUSH of \(x\) puts \(x\) on top at cost \(1\); POP removes the top element at cost \(1\); MULTIPOP with count \(k\) is MULTIPOP with an integer count, costing one unit per element removed. If a POP meets an empty stack, the run stops and reports an error, that POP is not charged, and the cost is that of the operations before it. Otherwise the run returns the final stack, and its cost is the sum of the costs of all operations.

public def execute {α : Type u} : List α → List (Operation α) → TimeM Nat (Option (List α))
  | stack, [] => pure (some stack)
  | stack, .push value :: ops => do
    TimeM.tick 1
    execute (value :: stack) ops
  | [], .pop :: _ => pure none
  | _ :: tail, .pop :: ops => do
    TimeM.tick 1
    execute tail ops
  | stack, .multipop count :: ops => do
    let next ← multipopSigned stack count
    execute next ops

Uses 2 · Used by 4

Statement usesStack operations for the MULTIPOP aggregate analysis · MULTIPOP with an integer count

Used byCost balance for stack operation sequences · Running a POP agrees with the standalone POP · Running a PUSH agrees with the standalone PUSH · Aggregate cost of stack operation sequences

TheoremRunning a PUSH agrees with the standalone PUSH#✓fully proved

For every stack \(S\), every value \(x\) and every finite sequence \(\sigma\) of stack operations, running PUSH \(x\) followed by \(\sigma\) on \(S\) has the same result and cost as first performing the standalone PUSH of \(x\) on \(S\) and then running \(\sigma\) on the resulting stack, the two costs being added.

public theorem execute_push_eq_bind_push {α : Type u} (stack : List α) (value : α)
    (ops : List (Operation α)) :
    execute stack (.push value :: ops) = (do
      let next ← push stack value
      execute next ops)

Uses 3

Statement usesStack operations for the MULTIPOP aggregate analysis · Running a sequence of stack operations · Stack push

TheoremRunning a POP agrees with the standalone POP#✓fully proved

For every stack \(S\) and every finite sequence \(\sigma\) of stack operations, running POP followed by \(\sigma\) on \(S\) has the same result and cost as first performing the standalone POP on \(S\) and then, if it reports underflow, stopping with an error at no further cost, or, if it removes the top element and leaves the stack \(S'\), running \(\sigma\) on \(S'\), the two costs being added.

public theorem execute_pop_eq_bind_pop {α : Type u} (stack : List α)
    (ops : List (Operation α)) :
    execute stack (.pop :: ops) = (do
      let removed ← pop stack
      match removed with
      | none => pure none
      | some (_, next) => execute next ops)

Uses 3

Statement usesStack operations for the MULTIPOP aggregate analysis · Running a sequence of stack operations · Stack pop

TheoremCost balance for stack operation sequences#✓fully proved

For every stack \(S\) and every finite sequence \(\sigma\) of stack operations, if running \(\sigma\) on \(S\) succeeds with final stack \(F\), then the cost of the run plus the number of elements of \(F\) equals the number of elements of \(S\) plus twice the number of PUSH operations in \(\sigma\).

public theorem execute_balance {α : Type u} (stack : List α) (ops : List (Operation α))
    (final : List α) (h : (execute stack ops).ret = some final) :
    (execute stack ops).time + final.length = stack.length +
      2 * ops.countP (fun op => match op with | .push _ => true | _ => false)

Uses 6 · Used by 1

Statement usesStack operations for the MULTIPOP aggregate analysis · Running a sequence of stack operations

Proof usesMULTIPOP · MULTIPOP with an integer count · Result of MULTIPOP · Cost of MULTIPOP

Used byAggregate cost of stack operation sequences

TheoremAggregate cost of stack operation sequences#✓fully proved

For every stack \(S\) and every sequence of \(n\) stack operations (PUSH, POP and MULTIPOP), if running the sequence on \(S\) succeeds, that is, no POP meets an empty stack, then its cost is at most \(|S| + 2n\), where \(|S|\) is the number of elements of \(S\).

public theorem execute_time_le {α : Type u} (stack : List α) (ops : List (Operation α))
    (final : List α) (h : (execute stack ops).ret = some final) :
    (execute stack ops).time ≤ stack.length + 2 * ops.length

Uses 3

Statement usesStack operations for the MULTIPOP aggregate analysis · Running a sequence of stack operations

Proof usesCost balance for stack operation sequences

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.