Dynamic table

StructureDynamic table#✓fully proved

A dynamic table with items of type \(\alpha\) consists of an array of slots \(s_0, \dots, s_{m-1}\), each either empty or holding an item of type \(\alpha\), together with an item count \(n\) satisfying \(n \le m\). The number \(m\) of slots is the capacity of the table.

public structure Table (α : Type u) where
  slots : Array (Option α)
  num : Nat
  num_le : num ≤ slots.size

Used by 31

Used byContents of a dynamic table · Formula for the contents of a dynamic table · Empty dynamic table · The empty dynamic table has no slots and no items · Lookup in a dynamic table · Lookup at the vacated position after deletion · Deletion preserves lookups below the last position · Lookup beyond the item count returns nothing · Lookup succeeds exactly below the item count · Deletion from a dynamic table · Deletion removes the last item from the contents · Item count after deletion · Capacity after deletion · Slots after deletion · Deletion preserves well-formedness · TABLE-INSERT · Amortized cost of dynamic-table insertion · Insertion appends to the contents · Inserting an array of items into a dynamic table · Inserting an array appends it to the contents · Capacity after inserting into the empty table · Total cost of insertions into the empty table · Strict cost bound for nonempty insertion sequences · Repeated insertion preserves well-formedness of a dynamic table · Insertion increases the item count by one · Capacity after an insertion · Slots after an insertion · Cost of an insertion · Insertion preserves well-formedness · Well-formed dynamic table · Characterization of well-formed dynamic tables

DefinitionWell-formed dynamic table#✓fully proved

A dynamic table with slots \(s_0, \dots, s_{m-1}\) and item count \(n\) is well formed when, for every \(i < m\), slot \(s_i\) is occupied if and only if \(i < n\); that is, the occupied slots are exactly the first \(n\).

The items held in the occupied slots are not constrained.

public def WellFormed {α : Type u} (T : Table α) : Prop :=
  ∀ (i : Nat) (h : i < T.slots.size), (T.slots[i]).isSome ↔ i < T.num

Uses 1 · Used by 11

Statement usesDynamic table

Used byDeletion preserves lookups below the last position · Lookup succeeds exactly below the item count · Deletion removes the last item from the contents · Slots after deletion · Deletion preserves well-formedness · Insertion appends to the contents · Inserting an array appends it to the contents · Repeated insertion preserves well-formedness of a dynamic table · Slots after an insertion · Insertion preserves well-formedness · Characterization of well-formed dynamic tables

TheoremCharacterization of well-formed dynamic tables#✓fully proved

A dynamic table with slots \(s_0, \dots, s_{m-1}\) and item count \(n\) is well formed if and only if, for every \(i < m\), slot \(s_i\) is occupied exactly when \(i < n\).

public theorem wellFormed_iff {α : Type u} (T : Table α) :
    WellFormed T ↔
      ∀ (i : Nat) (h : i < T.slots.size), (T.slots[i]).isSome ↔ i < T.num

Uses 2 · Used by 4

Statement usesDynamic table · Well-formed dynamic table

Used byLookup succeeds exactly below the item count · Deletion removes the last item from the contents · Slots after deletion · Deletion preserves well-formedness

DefinitionContents of a dynamic table#✓fully proved

Let \(T\) be a dynamic table with slots \(s_0, \dots, s_{m-1}\), each empty or holding an item, and item count \(n \le m\). The contents of \(T\) is the array of the items held by the occupied slots among \(s_0, \dots, s_{n-1}\), in order; empty slots in this prefix are skipped.

The insertion procedure never consults the contents.

public def contents {α : Type u} (T : Table α) : Array α :=
  (T.slots.extract 0 T.num).filterMap id

Uses 1 · Used by 4

Statement usesDynamic table

Used byFormula for the contents of a dynamic table · Deletion removes the last item from the contents · Insertion appends to the contents · Inserting an array appends it to the contents

TheoremFormula for the contents of a dynamic table#✓fully proved

Let \(T\) be a dynamic table with slots \(s_0, \dots, s_{m-1}\), each empty or holding an item, and item count \(n \le m\). The contents of \(T\) is the array obtained from the prefix \(s_0, \dots, s_{n-1}\) by skipping the empty slots and keeping the items of the occupied ones, in order.

public theorem contents_eq {α : Type u} (T : Table α) :
    contents T = (T.slots.extract 0 T.num).filterMap id

Uses 2 · Used by 1

Statement usesDynamic table · Contents of a dynamic table

Used byDeletion removes the last item from the contents

DefinitionEmpty dynamic table#✓fully proved

The empty dynamic table is the table with no slots (capacity \(0\)) and item count \(0\). It models a table before its first allocation.

public def empty {α : Type u} : Table α := ⟨#[], 0, by simp⟩

Uses 1 · Used by 4

Statement usesDynamic table

Used byThe empty dynamic table has no slots and no items · Capacity after inserting into the empty table · Total cost of insertions into the empty table · Strict cost bound for nonempty insertion sequences

TheoremThe empty dynamic table has no slots and no items#✓fully proved

The empty dynamic table has an empty slot array, so capacity \(0\), and item count \(0\).

public theorem empty_eq {α : Type u} :
    (empty : Table α) = ⟨#[], 0, by simp⟩

Uses 2

Statement usesDynamic table · Empty dynamic table

DefinitionTABLE-INSERT#✓fully proved

Let \(T\) be a dynamic table with slots \(s_0, \dots, s_{m-1}\) and item count \(n \le m\), and let \(x\) be an item. Inserting \(x\) into \(T\) proceeds as follows. If \(m = 0\), first replace the slots by a single empty slot. Then, if the table is full, that is, \(n\) equals the current capacity \(c\), allocate \(2c\) empty slots and copy the \(c\) old slots into the first \(c\) of them, at cost \(1\) per copied slot. Finally write \(x\) into slot \(n\), at cost \(1\), and set the item count to \(n + 1\). The result is the new table together with the total cost.

Cslib.Algorithms.Lean.DynamicTable.tableInsert · 22 lines

public def tableInsert {α : Type u} (T : Table α) (x : α) : TimeM Nat (Table α) := do
  let initial := initialTable T
  if hf : initial.num = initial.slots.size then
    let copied ← copyItems initial.slots.toList
      (Array.replicate (2 * initial.slots.size) none) 0 (by simp; omega)
    have hw : initial.num < copied.val.size := by
      rw [copied.property]
      simp only [Array.size_replicate]
      have hp : 0 < initial.slots.size := initialTable_pos T
      omega
    TimeM.tick 1
    pure ⟨copied.val.set initial.num (some x) hw, initial.num + 1, by
      simp only [Array.size_set]
      omega⟩
  else
    have hw : initial.num < initial.slots.size := by
      have hn := initial.num_le
      omega
    TimeM.tick 1
    pure ⟨initial.slots.set initial.num (some x) hw, initial.num + 1, by
      simp only [Array.size_set]
      omega⟩

Uses 1 · Used by 13

Statement usesDynamic table

Used byAmortized cost of dynamic-table insertion · Insertion appends to the contents · Inserting an array of items into a dynamic table · Inserting an array appends it to the contents · Capacity after inserting into the empty table · Total cost of insertions into the empty table · Strict cost bound for nonempty insertion sequences · Repeated insertion preserves well-formedness of a dynamic table · Insertion increases the item count by one · Capacity after an insertion · Slots after an insertion · Cost of an insertion · Insertion preserves well-formedness

DefinitionInserting an array of items into a dynamic table#✓fully proved

Given a dynamic table \(T\) and an array \(x_0, \dots, x_{k-1}\) of items, the result of inserting the array into \(T\) is obtained by starting from \(T\) and inserting \(x_0, x_1, \dots, x_{k-1}\) one at a time with TABLE-INSERT, in array order. Its cost is the sum of the costs of the \(k\) insertions; for an empty array the result is \(T\) at cost \(0\).

public def tableInsertMany {α : Type u} (T : Table α) (xs : Array α) :
    TimeM Nat (Table α) :=
  xs.foldlM (fun t x => tableInsert t x) T

Uses 2 · Used by 5

Statement usesDynamic table · TABLE-INSERT

Used byInserting an array appends it to the contents · Capacity after inserting into the empty table · Total cost of insertions into the empty table · Strict cost bound for nonempty insertion sequences · Repeated insertion preserves well-formedness of a dynamic table

TheoremInsertion increases the item count by one#✓fully proved

For every dynamic table \(T\) with item count \(n\) and every item \(x\), the table returned by inserting \(x\) into \(T\) with TABLE-INSERT has item count \(n + 1\).

public theorem tableInsert_num {α : Type u} (T : Table α) (x : α) :
    (tableInsert T x).ret.num = T.num + 1

Uses 2 · Used by 6

Statement usesDynamic table · TABLE-INSERT

Used byAmortized cost of dynamic-table insertion · Insertion appends to the contents · Capacity after inserting into the empty table · Total cost of insertions into the empty table · Strict cost bound for nonempty insertion sequences · Insertion preserves well-formedness

TheoremCapacity after an insertion#✓fully proved

Let \(T\) be a dynamic table with item count \(n\) and capacity (number of slots) \(m\), and let \(x\) be an item. The table returned by inserting \(x\) into \(T\) with TABLE-INSERT has capacity \(1\) if \(m = 0\), capacity \(2m\) if \(m > 0\) and \(n = m\), and capacity \(m\) otherwise.

public theorem tableInsert_size {α : Type u} (T : Table α) (x : α) :
    (tableInsert T x).ret.slots.size =
      if T.slots.size = 0 then 1
      else if T.num = T.slots.size then 2 * T.slots.size else T.slots.size

Uses 2 · Used by 5

Statement usesDynamic table · TABLE-INSERT

Used byAmortized cost of dynamic-table insertion · Capacity after inserting into the empty table · Total cost of insertions into the empty table · Strict cost bound for nonempty insertion sequences · Slots after an insertion

TheoremCost of an insertion#✓fully proved

Let \(T\) be a dynamic table with item count \(n\) and capacity \(m\), and let \(x\) be an item. Inserting \(x\) into \(T\) with TABLE-INSERT costs \(1 + n\) if \(m > 0\) and \(n = m\), and costs \(1\) otherwise.

public theorem tableInsert_time {α : Type u} (T : Table α) (x : α) :
    (tableInsert T x).time =
      1 + if T.slots.size > 0 ∧ T.num = T.slots.size then T.num else 0

Uses 2 · Used by 3

Statement usesDynamic table · TABLE-INSERT

Used byAmortized cost of dynamic-table insertion · Total cost of insertions into the empty table · Strict cost bound for nonempty insertion sequences

TheoremAmortized cost of dynamic-table insertion#✓fully proved

For a dynamic table \(T\) with item count \(n\) and capacity (number of slots) \(m\), let \(\Phi(T) = 2n - m\), an integer that may be negative. If inserting an item \(x\) into \(T\) has cost \(c\) and returns the table \(T'\), then \(c + \Phi(T') - \Phi(T) \le 3\). Here the cost of an insertion is one unit for writing \(x\) plus one unit for each old slot copied when a full table is doubled.

public theorem tableInsert_amortized {α : Type u} (T : Table α) (x : α) :
    ((tableInsert T x).time : Int) +
      (2 * ((tableInsert T x).ret.num : Int) - ((tableInsert T x).ret.slots.size : Int)) -
      (2 * (T.num : Int) - (T.slots.size : Int)) ≤ 3

Uses 5

Statement usesDynamic table · TABLE-INSERT

Proof usesInsertion increases the item count by one · Capacity after an insertion · Cost of an insertion

TheoremSlots after an insertion#✓fully proved

Let \(T\) be a well-formed dynamic table with slots \(s_0, \dots, s_{m-1}\) and item count \(n\), let \(x\) be an item, and let \(T'\) be the table returned by inserting \(x\) into \(T\) with TABLE-INSERT, with capacity \(m'\). Then the slots of \(T'\) are \(s_0, \dots, s_{n-1}\), followed by a slot holding \(x\), followed by \(m' - (n + 1)\) empty slots.

public theorem tableInsert_slots {α : Type u} (T : Table α) (x : α) :
    WellFormed T → (tableInsert T x).ret.slots =
      T.slots.extract 0 T.num ++ #[some x] ++
        Array.replicate ((tableInsert T x).ret.slots.size - (T.num + 1)) none

Uses 4 · Used by 2

Statement usesDynamic table · Well-formed dynamic table · TABLE-INSERT

Proof usesCapacity after an insertion

Used byInsertion appends to the contents · Insertion preserves well-formedness

TheoremInsertion preserves well-formedness#✓fully proved

If \(T\) is a well-formed dynamic table and \(x\) is an item, then the table returned by inserting \(x\) into \(T\) with TABLE-INSERT is well formed.

public theorem tableInsert_wellFormed {α : Type u} (T : Table α) (x : α) :
    WellFormed T → WellFormed (tableInsert T x).ret

Uses 5 · Used by 2

Statement usesDynamic table · Well-formed dynamic table · TABLE-INSERT

Proof usesInsertion increases the item count by one · Slots after an insertion

Used byInserting an array appends it to the contents · Repeated insertion preserves well-formedness of a dynamic table

TheoremInsertion appends to the contents#✓fully proved

If \(T\) is a well-formed dynamic table and \(x\) is an item, then the contents of the table obtained by inserting \(x\) into \(T\) are the contents of \(T\) followed by \(x\).

public theorem tableInsert_contents {α : Type u} (T : Table α) (x : α) :
    WellFormed T → contents (tableInsert T x).ret = (contents T).push x

Uses 6 · Used by 1

Statement usesDynamic table · Well-formed dynamic table · Contents of a dynamic table · TABLE-INSERT

Proof usesInsertion increases the item count by one · Slots after an insertion

Used byInserting an array appends it to the contents

TheoremRepeated insertion preserves well-formedness of a dynamic table#✓fully proved

Call a dynamic table with item count \(n\) well formed when, for every slot index \(i\), slot \(i\) is occupied exactly when \(i < n\). If a dynamic table \(T\) is well formed, then for every array \(xs\), the table obtained from \(T\) by inserting the entries of \(xs\) one at a time with TABLE-INSERT, in array order, is again well formed.

public theorem tableInsertMany_wellFormed {α : Type u} (T : Table α) (xs : Array α) :
    WellFormed T → WellFormed (tableInsertMany T xs).ret

Uses 5

Statement usesDynamic table · Well-formed dynamic table · Inserting an array of items into a dynamic table

Proof usesTABLE-INSERT · Insertion preserves well-formedness

TheoremInserting an array appends it to the contents#✓fully proved

If \(T\) is a well-formed dynamic table and \(x_1, \dots, x_k\) is an array of items, then inserting \(x_1, \dots, x_k\) into \(T\) one at a time, in this order, gives a table whose contents are the contents of \(T\) followed by \(x_1, \dots, x_k\).

public theorem tableInsertMany_contents {α : Type u} (T : Table α) (xs : Array α) :
    WellFormed T → contents (tableInsertMany T xs).ret = contents T ++ xs

Uses 7

Statement usesDynamic table · Well-formed dynamic table · Contents of a dynamic table · Inserting an array of items into a dynamic table

Proof usesTABLE-INSERT · Insertion appends to the contents · Insertion preserves well-formedness

TheoremCapacity after inserting into the empty table#✓fully proved

Starting from the empty dynamic table and inserting the items of an array of length \(k\) one at a time, the resulting table has capacity (number of slots) at most \(2k\).

public theorem tableInsertMany_size_le {α : Type u} (xs : Array α) :
    (tableInsertMany empty xs).ret.slots.size ≤ 2 * xs.size

Uses 6

Statement usesDynamic table · Empty dynamic table · Inserting an array of items into a dynamic table

Proof usesTABLE-INSERT · Insertion increases the item count by one · Capacity after an insertion

TheoremTotal cost of insertions into the empty table#✓fully proved

Starting from the empty dynamic table and inserting the items of an array of length \(k\) one at a time, the total cost is at most \(3k\), where each insertion costs one unit for writing the new item plus one unit for each old slot copied when a full table is doubled.

public theorem tableInsertMany_time_le {α : Type u} (xs : Array α) :
    (tableInsertMany empty xs).time ≤ 3 * xs.size

Uses 7

Statement usesDynamic table · Empty dynamic table · Inserting an array of items into a dynamic table

Proof usesTABLE-INSERT · Insertion increases the item count by one · Capacity after an insertion · Cost of an insertion

TheoremStrict cost bound for nonempty insertion sequences#✓fully proved

Starting from the empty dynamic table and inserting the items of a nonempty array of length \(k\) one at a time, the total cost is less than \(3k\).

The bound is strict because the first insertion, which allocates the first slot, has amortized cost \(2\) rather than \(3\).

public theorem tableInsertMany_time_lt {α : Type u} (xs : Array α) :
    xs.size > 0 → (tableInsertMany empty xs).time < 3 * xs.size

Uses 7

Statement usesDynamic table · Empty dynamic table · Inserting an array of items into a dynamic table

Proof usesTABLE-INSERT · Insertion increases the item count by one · Capacity after an insertion · Cost of an insertion

DefinitionLookup in a dynamic table#✓fully proved

Let \(T\) be a dynamic table with slots \(s_0, \dots, s_{m-1}\), each empty or holding an item, and item count \(n \le m\). The lookup at logical position \(i\) returns the item held by \(s_i\) when \(i < n\) and \(s_i\) is occupied; it returns no value when \(i < n\) and \(s_i\) is empty, and when \(i \ge n\).

public def get? {α : Type u} (T : Table α) (i : Nat) : Option α :=
  if i < T.num then (T.slots[i]?).bind id else none

Uses 1 · Used by 4

Statement usesDynamic table

Used byLookup at the vacated position after deletion · Deletion preserves lookups below the last position · Lookup beyond the item count returns nothing · Lookup succeeds exactly below the item count

TheoremLookup beyond the item count returns nothing#✓fully proved

Let \(T\) be a dynamic table with item count \(n\). For every natural number \(i \ge n\), the lookup at logical position \(i\) in \(T\) returns no value.

public theorem get?_eq_none_of_le {α : Type u} (T : Table α) {i : Nat}
    (h : T.num ≤ i) : get? T i = none

Uses 2 · Used by 2

Statement usesDynamic table · Lookup in a dynamic table

Used byLookup at the vacated position after deletion · Lookup succeeds exactly below the item count

TheoremLookup succeeds exactly below the item count#✓fully proved

Let \(T\) be a well-formed dynamic table holding \(n\) items. For every natural number \(i\), the lookup at logical position \(i\) in \(T\) returns a value if and only if \(i < n\).

public theorem get?_isSome_iff {α : Type u} (T : Table α) (hT : WellFormed T)
    (i : Nat) : (get? T i).isSome ↔ i < T.num

Uses 5

Statement usesDynamic table · Well-formed dynamic table · Lookup in a dynamic table

Proof usesLookup beyond the item count returns nothing · Characterization of well-formed dynamic tables

DefinitionDeletion from a dynamic table#✓fully proved

Let \(T\) be a dynamic table with slots \(s_0, \dots, s_{m-1}\), each empty or holding an item, and item count \(n \le m\). Deleting the last item of \(T\) gives the following table. If \(n = 0\), the result is \(T\) itself. Otherwise, if \(4(n-1) < m\), that is, the load factor after deletion is strictly below \(1/4\), the table contracts: the result has slots \(s_0, \dots, s_{n-2}\) followed by \(\lfloor m/2 \rfloor - (n-1)\) empty slots, so capacity \(\lfloor m/2 \rfloor\), and item count \(n-1\). Otherwise the result has the slots of \(T\) with \(s_{n-1}\) made empty, and item count \(n-1\).

Cslib.Algorithms.Lean.DynamicTable.tableDelete · 15 lines

public def tableDelete {α : Type u} (T : Table α) : Table α :=
  if hnum : T.num = 0 then T
  else if hcon : 4 * (T.num - 1) < T.slots.size then
    ⟨T.slots.extract 0 (T.num - 1) ++
        Array.replicate (T.slots.size / 2 - (T.num - 1)) none, T.num - 1, by
      have hkle : T.num - 1 ≤ T.slots.size := by have h := T.num_le; omega
      have he : (T.slots.extract 0 (T.num - 1)).size = T.num - 1 :=
        extract_size_of_le T.slots hkle
      simp only [Array.size_append, he, Array.size_replicate]
      omega⟩
  else
    ⟨T.slots.set (T.num - 1) none (by have h := T.num_le; omega), T.num - 1, by
      simp only [Array.size_set]
      have h := T.num_le
      omega⟩

Uses 1 · Used by 7

Statement usesDynamic table

Used byLookup at the vacated position after deletion · Deletion preserves lookups below the last position · Deletion removes the last item from the contents · Item count after deletion · Capacity after deletion · Slots after deletion · Deletion preserves well-formedness

TheoremItem count after deletion#✓fully proved

Applying deletion to a dynamic table with item count \(n\) gives a table with item count \(n - 1\) when \(n \ge 1\), and item count \(0\) when \(n = 0\).

public theorem tableDelete_num {α : Type u} (T : Table α) :
    (tableDelete T).num = T.num - 1

Uses 2 · Used by 4

Statement usesDynamic table · Deletion from a dynamic table

Used byLookup at the vacated position after deletion · Deletion preserves lookups below the last position · Deletion removes the last item from the contents · Deletion preserves well-formedness

TheoremCapacity after deletion#✓fully proved

Let \(T\) be a dynamic table with capacity \(m\) and item count \(n\), and apply deletion to \(T\). If \(n = 0\), the capacity stays \(m\). If \(n \ge 1\) and \(4(n-1) < m\), the new capacity is \(\lfloor m/2 \rfloor\). Otherwise the capacity stays \(m\).

public theorem tableDelete_size {α : Type u} (T : Table α) :
    (tableDelete T).slots.size =
      if T.num = 0 then T.slots.size
      else if 4 * (T.num - 1) < T.slots.size then T.slots.size / 2
      else T.slots.size

Uses 2 · Used by 1

Statement usesDynamic table · Deletion from a dynamic table

Used bySlots after deletion

TheoremSlots after deletion#✓fully proved

Let \(T\) be a well-formed dynamic table with slots \(s_0, \dots, s_{m-1}\) holding \(n \ge 1\) items, and let \(m'\) be the capacity of the table obtained by applying deletion to \(T\). The slots of that table are the first \(n - 1\) slots \(s_0, \dots, s_{n-2}\) of \(T\) followed by \(m' - (n - 1)\) empty slots.

public theorem tableDelete_slots {α : Type u} (T : Table α) (hT : WellFormed T)
    (hnum : T.num ≠ 0) :
    (tableDelete T).slots =
      T.slots.extract 0 (T.num - 1) ++
        Array.replicate ((tableDelete T).slots.size - (T.num - 1)) none

Uses 5 · Used by 3

Statement usesDynamic table · Well-formed dynamic table · Deletion from a dynamic table

Proof usesCapacity after deletion · Characterization of well-formed dynamic tables

Used byDeletion preserves lookups below the last position · Deletion removes the last item from the contents · Deletion preserves well-formedness

TheoremDeletion preserves well-formedness#✓fully proved

Let \(T\) be a well-formed dynamic table, that is, its occupied slots are exactly its first \(n\) slots, where \(n\) is its item count. Then the table obtained by applying deletion to \(T\) is again well-formed.

public theorem tableDelete_wellFormed {α : Type u} (T : Table α)
    (hT : WellFormed T) : WellFormed (tableDelete T)

Uses 6

Statement usesDynamic table · Well-formed dynamic table · Deletion from a dynamic table

Proof usesItem count after deletion · Slots after deletion · Characterization of well-formed dynamic tables

TheoremDeletion removes the last item from the contents#✓fully proved

Let \(T\) be a well-formed dynamic table. The contents of the table obtained by applying deletion to \(T\) is the contents of \(T\) with its last entry removed; when the contents of \(T\) is empty, it stays empty.

public theorem tableDelete_contents {α : Type u} (T : Table α) (hT : WellFormed T) :
    (contents (tableDelete T)).toList = (contents T).toList.dropLast

Uses 8

Statement usesDynamic table · Well-formed dynamic table · Contents of a dynamic table · Deletion from a dynamic table

Proof usesFormula for the contents of a dynamic table · Item count after deletion · Slots after deletion · Characterization of well-formed dynamic tables

TheoremDeletion preserves lookups below the last position#✓fully proved

Let \(T\) be a well-formed dynamic table holding \(n\) items, and let \(i\) be a natural number with \(i < n - 1\). After applying deletion to \(T\), the lookup at logical position \(i\) returns the same result as the lookup at position \(i\) in \(T\).

public theorem get?_delete_of_lt {α : Type u} (T : Table α) (hT : WellFormed T)
    {i : Nat} (hi : i < T.num - 1) : get? (tableDelete T) i = get? T i

Uses 6

Statement usesDynamic table · Well-formed dynamic table · Lookup in a dynamic table · Deletion from a dynamic table

Proof usesItem count after deletion · Slots after deletion

TheoremLookup at the vacated position after deletion#✓fully proved

Let \(T\) be a dynamic table with item count \(n\), where \(n - 1\) is read as \(0\) when \(n = 0\). After applying deletion to \(T\), the lookup at logical position \(n - 1\) returns no value.

public theorem get?_delete_last {α : Type u} (T : Table α) :
    get? (tableDelete T) (T.num - 1) = none

Uses 5

Statement usesDynamic table · Lookup in a dynamic table · Deletion from a dynamic table

Proof usesLookup beyond the item count returns nothing · Item count after deletion

32 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.