Doubly linked list

StructureDoubly linked list node#✓fully proved

A doubly linked list node with payloads in \(\alpha\) and identities in \(\iota\) consists of a payload in \(\alpha\) (the key together with any satellite data), a next pointer and a previous pointer, each of which is either an identity in \(\iota\) or NIL.

public structure Node (α : Type u) (ι : Type v) where
  /-- The full payload, including any key and satellite data. -/
  payload : α
  /-- Next node identity, or NIL at the tail. -/
  next : Option ι
  /-- Previous node identity, or NIL at the head. -/
  prev : Option ι
deriving DecidableEq, Repr

Used by 61

Used byCircular doubly linked list with a sentinel · Empty circular list with a sentinel · Deletion from a doubly linked list · Deletion from a doubly linked list allocates and frees nothing · The deleted node keeps its record · Deletion preserves lists avoiding the deleted node's neighbors · Deletion changes only the cells of the neighbors · Cellwise result of doubly linked list deletion · Header after doubly linked list deletion · Deletion preserves payloads · Correctness of doubly linked list deletion · Result of doubly linked list deletion · Running time of doubly linked list deletion · Doubly linked list deletion costs at most four events · Doubly-linked-list insertion (LIST-INSERT) · Doubly-linked-list insertion neither allocates nor frees cells · Doubly-linked-list insertion preserves disjoint lists · Frame property of doubly-linked-list insertion · Cells after doubly-linked-list insertion · Doubly-linked-list insertion preserves payloads · Insertion into a represented doubly-linked list · Result of doubly-linked-list insertion · Cost of doubly-linked-list insertion · Prepending a node to a doubly linked list · Doubly-linked list prepend preserves allocation · Doubly-linked list prepend preserves disjoint lists · Doubly-linked list prepend leaves other cells unchanged · Cells after doubly-linked list prepend · Prepending makes the supplied node the head · Pointers of the node prepended to a doubly-linked list · Old head after doubly-linked list prepend · Doubly-linked list prepend preserves payloads · Correctness of doubly-linked list prepend · Result of doubly-linked list prepend · Exact cost of doubly linked list prepend · Uniform cost bound for doubly linked list prepend · Search in a circular list with a sentinel · Sentinel search preserves the circular list · Sentinel search changes only the sentinel's key · Sentinel search returns the first matching node · Cost of sentinel search · Store representing a doubly linked list · Deletion from a circular list with a sentinel · Sentinel deletion preserves allocation · Sentinel deletion removes a node from its circular list · Sentinel deletion keeps the deleted node · Sentinel deletion preserves disjoint circular lists · Sentinel deletion changes only the two neighbours · Cells after sentinel deletion · Sentinel deletion preserves payloads · The store returned by sentinel deletion · Sentinel deletion takes two pointer assignments · Sentinel list insertion (LIST-INSERT′) · Sentinel insertion preserves allocation · Sentinel insertion preserves the circular list · Sentinel insertion preserves a disjoint circular list · Sentinel insertion leaves other cells unchanged · Sentinel insertion, cell by cell · Sentinel insertion preserves payloads · The store after sentinel insertion · Sentinel insertion takes four steps

DefinitionStore representing a doubly linked list#✓fully proved

Let a store assign to each identity below \(n\) either nothing or a doubly linked list node whose pointers are identities below \(n\) or NIL, and let the head be an identity below \(n\) or NIL. The store and head represent the list of identities \(i_0, \dots, i_{k-1}\) when these identities are pairwise distinct, the head is \(i_0\) (and NIL when \(k = 0\)), and for each \(j < k\) the store entry at \(i_j\) is a node whose previous pointer is NIL if \(j = 0\) and \(i_{j-1}\) otherwise, and whose next pointer is \(i_{j+1}\) if \(j + 1 < k\) and NIL otherwise.

public def Represents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (ids : List (Fin capacity)) : Prop :=
  ids.Nodup ∧ head = ids.head? ∧
    ∀ (i : Nat) (hi : i < ids.length), ∃ node,
      store.get ids[i] = some node ∧
      node.prev = (if i = 0 then none else ids[i - 1]?) ∧
      node.next = ids[i + 1]?

Uses 1 · Used by 6

Statement usesDoubly linked list node

Used byDeletion preserves lists avoiding the deleted node's neighbors · Correctness of doubly linked list deletion · Doubly-linked-list insertion preserves disjoint lists · Insertion into a represented doubly-linked list · Doubly-linked list prepend preserves disjoint lists · Correctness of doubly-linked list prepend

DefinitionPrepending a node to a doubly linked list#✓fully proved

Let a store assign to each identity below \(n\) either nothing or a doubly linked list node whose pointers are identities below \(n\) or NIL, let the head be an identity below \(n\) or NIL, and let \(x\) be an identity whose store entry is a node, where the store entry of the head is also a node when the head is not NIL. The procedure sets the next pointer of \(x\) to the head, then sets the previous pointer of \(x\) to NIL, then tests whether the head is NIL; if it is not, it sets the previous pointer of the node at the head (read after the two writes at \(x\)) to \(x\). Finally it makes \(x\) the new head and returns the updated store together with the head \(x\). One time unit is charged for each pointer assignment and for the NIL test, so the cost is \(4\) when the head is NIL and \(5\) otherwise.

Cslib.Algorithms.Lean.DoublyLinkedList.listPrepend · 34 lines

public def listPrepend {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) :
    TimeM Nat (Vector (Option (Node α (Fin capacity))) capacity × Option (Fin capacity)) := do
  let originalX := (store.get x).get hx
  TimeM.tick 1
  let nextX := { originalX with next := head }
  let store1 := store.set x.val (some nextX) x.isLt
  TimeM.tick 1
  let prevX := { nextX with prev := none }
  let store2 := store1.set x.val (some prevX) x.isLt
  TimeM.tick 1
  match he : head with
  | none =>
    TimeM.tick 1
    pure (store2, some x)
  | some h =>
    have hAllocated : (store2.get h).isSome := by
      change (store1.set x.val (some prevX) x.isLt)[h.val].isSome = true
      rw [Vector.getElem_set]
      split
      · rfl
      · change store1[h.val].isSome = true
        rw [Vector.getElem_set]
        split
        · rfl
        · exact hh h he
    let currentH := (store2.get h).get hAllocated
    TimeM.tick 1
    let store3 := store2.set h.val (some { currentH with prev := some x }) h.isLt
    TimeM.tick 1
    pure (store3, some x)

Uses 1 · Used by 12

Statement usesDoubly linked list node

Used byDoubly-linked list prepend preserves allocation · Doubly-linked list prepend preserves disjoint lists · Doubly-linked list prepend leaves other cells unchanged · Cells after doubly-linked list prepend · Prepending makes the supplied node the head · Pointers of the node prepended to a doubly-linked list · Old head after doubly-linked list prepend · Doubly-linked list prepend preserves payloads · Correctness of doubly-linked list prepend · Result of doubly-linked list prepend · Exact cost of doubly linked list prepend · Uniform cost bound for doubly linked list prepend

TheoremPrepending makes the supplied node the head#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Then the head returned by List Prepend on \(s\), \(\mathrm{head}\) and \(x\) is \(x\).

public theorem listPrepend_head {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) :
    (listPrepend store head x hx hh).ret.2 = some x

Uses 2 · Used by 1

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Used byCorrectness of doubly-linked list prepend

TheoremExact cost of doubly linked list prepend#✓fully proved

Let a store assign to each identity below \(n\) either nothing or a doubly linked list node, let the head be an identity below \(n\) or NIL, and let \(x\) be an identity whose store entry is a node, where the store entry of the head is also a node when the head is not NIL. Then prepending \(x\) costs exactly \(5\) time units if the head is not NIL and exactly \(4\) if it is NIL, counting one unit per pointer assignment and per NIL test of the old head.

public theorem listPrepend_time {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) :
    (listPrepend store head x hx hh).time = if head.isSome then 5 else 4

Uses 2 · Used by 1

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Used byUniform cost bound for doubly linked list prepend

TheoremResult of doubly-linked list prepend#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Let \(u\) be \(s\) with the cell at \(x\) replaced by the node \(s(x)\) with next pointer \(\mathrm{head}\) and previous pointer NIL. Then List Prepend on \(s\), \(\mathrm{head}\) and \(x\) returns the head \(x\) together with the store \(u\) when \(\mathrm{head}\) is NIL, and, when \(\mathrm{head}\) is an identity \(h\), together with the store obtained from \(u\) by replacing its cell at \(h\) with the node \(u(h)\) with previous pointer \(x\) (leaving the cell empty if \(u(h)\) is nothing).

This holds also when \(h = x\).

public theorem listPrepend_ret {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) :
    let updated := store.set x.val
      (some { (store.get x).get hx with next := head, prev := none }) x.isLt
    (listPrepend store head x hx hh).ret =
      (match head with
       | none => updated
       | some h => updated.set h.val
           ((updated.get h).map fun node => { node with prev := some x }) h.isLt,
       some x)

Uses 2 · Used by 1

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Used byCells after doubly-linked list prepend

TheoremCells after doubly-linked list prepend#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Let \(s'\) be the store returned by List Prepend on \(s\), \(\mathrm{head}\) and \(x\). For every identity \(z\), let \(c\) be the node \(s(x)\) with next pointer \(\mathrm{head}\) and previous pointer NIL if \(z = x\), and \(c = s(z)\) otherwise. Then \(s'(z)\) is \(c\) with previous pointer \(x\) (nothing, if \(c\) is nothing) when \(\mathrm{head} = z\), and \(s'(z) = c\) otherwise.

public theorem listPrepend_get {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) (z : Fin capacity) :
    (listPrepend store head x hx hh).ret.1.get z =
      let cell := if x = z then
        some { (store.get x).get hx with next := head, prev := none } else store.get z
      if head = some z then cell.map fun node => { node with prev := some x } else cell

Uses 3 · Used by 5

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Proof usesResult of doubly-linked list prepend

Used byDoubly-linked list prepend preserves allocation · Doubly-linked list prepend leaves other cells unchanged · Pointers of the node prepended to a doubly-linked list · Old head after doubly-linked list prepend · Doubly-linked list prepend preserves payloads

TheoremDoubly-linked list prepend leaves other cells unchanged#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Let \(s'\) be the store returned by List Prepend on \(s\), \(\mathrm{head}\) and \(x\). Then \(s'(z) = s(z)\) for every identity \(z\) with \(z \ne x\) and \(\mathrm{head} \ne z\).

public theorem listPrepend_frame {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) (z : Fin capacity)
    (xz : x ≠ z) (hz : head ≠ some z) :
    (listPrepend store head x hx hh).ret.1.get z = store.get z

Uses 3 · Used by 2

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Proof usesCells after doubly-linked list prepend

Used byDoubly-linked list prepend preserves disjoint lists · Correctness of doubly-linked list prepend

TheoremDoubly-linked list prepend preserves allocation#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Let \(s'\) be the store returned by List Prepend on \(s\), \(\mathrm{head}\) and \(x\). Then for every identity \(z\), \(s'(z)\) is a node if and only if \(s(z)\) is a node.

public theorem listPrepend_allocated {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) (z : Fin capacity) :
    ((listPrepend store head x hx hh).ret.1.get z).isSome = (store.get z).isSome

Uses 3

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Proof usesCells after doubly-linked list prepend

TheoremDoubly-linked list prepend preserves payloads#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Let \(s'\) be the store returned by List Prepend on \(s\), \(\mathrm{head}\) and \(x\). Then for every identity \(z\), either \(s(z)\) and \(s'(z)\) are both nothing, or both are nodes with the same payload.

public theorem listPrepend_payload {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) (z : Fin capacity) :
    ((listPrepend store head x hx hh).ret.1.get z).map Node.payload =
      (store.get z).map Node.payload

Uses 3

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Proof usesCells after doubly-linked list prepend

TheoremPointers of the node prepended to a doubly-linked list#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Suppose moreover that \(\mathrm{head}\) is not \(x\) (it may be NIL). Let \(s'\) be the store returned by List Prepend on \(s\), \(\mathrm{head}\) and \(x\). Then \(s'(x)\) is the node \(s(x)\) with next pointer \(\mathrm{head}\) and previous pointer NIL.

public theorem listPrepend_node {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) (fresh : head ≠ some x) :
    (listPrepend store head x hx hh).ret.1.get x =
      some { (store.get x).get hx with next := head, prev := none }

Uses 3 · Used by 1

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Proof usesCells after doubly-linked list prepend

Used byCorrectness of doubly-linked list prepend

TheoremOld head after doubly-linked list prepend#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Suppose moreover that \(\mathrm{head}\) is an identity \(h\) with \(h \ne x\). Let \(s'\) be the store returned by List Prepend on \(s\), \(\mathrm{head}\) and \(x\). Then \(s'(h)\) is the node \(s(h)\) with previous pointer \(x\).

public theorem listPrepend_oldHead {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) (h : Fin capacity)
    (he : head = some h) (xh : x ≠ h) :
    (listPrepend store head x hx hh).ret.1.get h =
      some { (store.get h).get (hh h he) with prev := some x }

Uses 3 · Used by 1

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Proof usesCells after doubly-linked list prepend

Used byCorrectness of doubly-linked list prepend

TheoremCorrectness of doubly-linked list prepend#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Suppose moreover that \(s\) with head \(\mathrm{head}\) represents a list \(L = (\ell_1, \dots, \ell_k)\) of identities, that is, the \(\ell_i\) are distinct, \(\mathrm{head}\) is \(\ell_1\) (NIL if \(k = 0\)), and each \(s(\ell_i)\) is a node with previous pointer \(\ell_{i-1}\) and next pointer \(\ell_{i+1}\) (NIL past the ends of \(L\)), and that \(x\) is not in \(L\). Let \(s'\) and \(h'\) be the store and head returned by List Prepend on \(s\), \(\mathrm{head}\) and \(x\). Then \(s'\) with head \(h'\) represents the list \((x, \ell_1, \dots, \ell_k)\).

public theorem listPrepend_represents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome)
    (ids : List (Fin capacity)) (rep : Represents store head ids) (fresh : x ∉ ids) :
    Represents (listPrepend store head x hx hh).ret.1
      (listPrepend store head x hx hh).ret.2 (x :: ids)

Uses 7

Statement usesDoubly linked list node · Store representing a doubly linked list · Prepending a node to a doubly linked list

Proof usesDoubly-linked list prepend leaves other cells unchanged · Prepending makes the supplied node the head · Pointers of the node prepended to a doubly-linked list · Old head after doubly-linked list prepend

TheoremDoubly-linked list prepend preserves disjoint lists#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity \(i < n\) either a node or nothing, let \(\mathrm{head}\) be NIL or an identity, and let \(x\) be an identity such that \(s(x)\) is a node and, when \(\mathrm{head}\) is an identity, \(s(\mathrm{head})\) is a node. Suppose moreover that \(s\) with some head \(o\) represents a list \(L = (\ell_1, \dots, \ell_k)\) of identities, that is, the \(\ell_i\) are distinct, \(o\) is \(\ell_1\) (NIL if \(k = 0\)), and each \(s(\ell_i)\) is a node with previous pointer \(\ell_{i-1}\) and next pointer \(\ell_{i+1}\) (NIL past the ends of \(L\)), that \(x\) is not in \(L\), and that \(\mathrm{head}\) is NIL or an identity not in \(L\). Let \(s'\) be the store returned by List Prepend on \(s\), \(\mathrm{head}\) and \(x\). Then \(s'\) with head \(o\) also represents \(L\).

public theorem listPrepend_disjoint_represents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome)
    (otherHead : Option (Fin capacity)) (otherIds : List (Fin capacity))
    (rep : Represents store otherHead otherIds) (fresh : x ∉ otherIds)
    (disjoint : ∀ h, head = some h → h ∉ otherIds) :
    Represents (listPrepend store head x hx hh).ret.1 otherHead otherIds

Uses 4

Statement usesDoubly linked list node · Store representing a doubly linked list · Prepending a node to a doubly linked list

Proof usesDoubly-linked list prepend leaves other cells unchanged

TheoremUniform cost bound for doubly linked list prepend#✓fully proved

Let a store assign to each identity below \(n\) either nothing or a doubly linked list node, let the head be an identity below \(n\) or NIL, and let \(x\) be an identity whose store entry is a node, where the store entry of the head is also a node when the head is not NIL. Then prepending \(x\) costs at most \(5\) time units, counting one unit per pointer assignment and per NIL test of the old head.

public theorem listPrepend_time_le {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hh : ∀ h, head = some h → (store.get h).isSome) :
    (listPrepend store head x hx hh).time ≤ 5

Uses 3

Statement usesDoubly linked list node · Prepending a node to a doubly linked list

Proof usesExact cost of doubly linked list prepend

DefinitionDeletion from a doubly linked list#✓fully proved

Let the store be an array of cells, each either empty or holding a node with a payload and optional next and previous pointers to cells, let \(h\) be the optional head pointer, and let \(x\) be a cell holding a node such that each cell named by its previous or next pointer also holds a node. Following CLRS LIST-DELETE, deleting \(x\) returns a new store and head as follows. If the node at \(x\) has a previous pointer \(p\), the next pointer of the node at \(p\) is set to the next pointer of \(x\) and the head stays \(h\); otherwise the head becomes the next pointer of \(x\). Then, if the node at \(x\) has a next pointer \(s\), the previous pointer of the node at \(s\) in the store from the first step is set to the previous pointer of \(x\). The computation is charged one unit for each of the two NIL tests and one unit for each executed pointer or head assignment, so three or four units in total.

The record stored at \(x\) is kept and no cell is freed; list consistency is needed only for correctness, not to run the procedure.

Cslib.Algorithms.Lean.DoublyLinkedList.listDelete · 28 lines

public def listDelete {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome) :
    TimeM Nat (Vector (Option (Node α (Fin capacity))) capacity × Option (Fin capacity)) := do
  let originalX := (store.get x).get hx
  TimeM.tick 1
  match he : originalX.prev with
  | none =>
    TimeM.tick 1
    finishDelete store originalX.next x hx hn
  | some p =>
    let originalP := (store.get p).get (hp p he)
    TimeM.tick 1
    let store1 := store.set p.val (some { originalP with next := originalX.next }) p.isLt
    have hxeq : store1.get x = store.get x := first_write_preserves_x store x p hx (hp p he)
    have hx1 : (store1.get x).isSome := by rw [hxeq]; exact hx
    have hn1 : ∀ n, ((store1.get x).get hx1).next = some n → (store1.get n).isSome := by
      intro n hnext
      have hn0 : (store.get n).isSome := hn n (by simpa only [hxeq] using hnext)
      change (store.set p.val (some { originalP with next := originalX.next }) p.isLt)[n.val].isSome
      rw [Vector.getElem_set]
      split
      · rfl
      · exact hn0
    finishDelete store1 head x hx1 hn1

Uses 1 · Used by 16

Statement usesDoubly linked list node

Used byDeletion from a doubly linked list allocates and frees nothing · The deleted node keeps its record · Deletion preserves lists avoiding the deleted node's neighbors · Deletion changes only the cells of the neighbors · Cellwise result of doubly linked list deletion · Header after doubly linked list deletion · Deletion preserves payloads · Correctness of doubly linked list deletion · Result of doubly linked list deletion · Running time of doubly linked list deletion · Doubly linked list deletion costs at most four events · Sentinel deletion preserves allocation · Sentinel deletion keeps the deleted node · Sentinel deletion changes only the two neighbours · Cells after sentinel deletion · Sentinel deletion preserves payloads

TheoremRunning time of doubly linked list deletion#✓fully proved

Let the store be an array of cells, each either empty or holding a node with optional next and previous pointers, let \(h\) be the optional head pointer, and let \(x\) be a cell holding a node such that each cell named by its previous or next pointer also holds a node. Counting one unit per NIL test and per executed pointer or head assignment, deleting \(x\) from the list with head \(h\) costs exactly \(4\) units if the node at \(x\) has a next pointer, and exactly \(3\) units otherwise.

public theorem listDelete_time {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome) :
    (listDelete store head x hx hp hn).time =
      if ((store.get x).get hx).next.isSome then 4 else 3

Uses 2 · Used by 1

Statement usesDoubly linked list node · Deletion from a doubly linked list

Used byDoubly linked list deletion costs at most four events

TheoremHeader after doubly linked list deletion#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Let \(h'\) be the header returned by List Delete on \(S\), \(h\) and \(x\). Then \(h' = h\) if \(X.\mathrm{prev}\) is not NIL, and \(h' = X.\mathrm{next}\) if \(X.\mathrm{prev}\) is NIL.

public theorem listDelete_head {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome) :
    (listDelete store head x hx hp hn).ret.2 =
      if ((store.get x).get hx).prev.isSome then head else ((store.get x).get hx).next

Uses 2 · Used by 1

Statement usesDoubly linked list node · Deletion from a doubly linked list

Used byCorrectness of doubly linked list deletion

TheoremResult of doubly linked list deletion#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Let \(T\) be \(S\) if \(X.\mathrm{prev}\) is NIL, and otherwise \(S\) with the next pointer of the node in cell \(X.\mathrm{prev}\) set to \(X.\mathrm{next}\). Then List Delete on \(S\), \(h\) and \(x\) returns the store equal to \(T\) if \(X.\mathrm{next}\) is NIL, and otherwise to \(T\) with the previous pointer of the node in cell \(X.\mathrm{next}\) of \(T\) set to \(X.\mathrm{prev}\), together with the header \(h\) if \(X.\mathrm{prev}\) is not NIL and \(X.\mathrm{next}\) if it is NIL. The successor's node is read from \(T\), so when \(X.\mathrm{prev}\) and \(X.\mathrm{next}\) are the same index (not NIL), both pointer updates apply to its node.

public theorem listDelete_ret {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome) :
    let originalX := (store.get x).get hx
    let carried := match originalX.prev with

Uses 2 · Used by 6

Statement usesDoubly linked list node · Deletion from a doubly linked list

Used byCellwise result of doubly linked list deletion · Sentinel deletion preserves allocation · Sentinel deletion keeps the deleted node · Sentinel deletion changes only the two neighbours · Cells after sentinel deletion · Sentinel deletion preserves payloads

TheoremCellwise result of doubly linked list deletion#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Let \(S'\) be the store returned by List Delete on \(S\), \(h\) and \(x\). For an index \(z\), let \(C\) be the cell \(S(z)\) with the next pointer of its node set to \(X.\mathrm{next}\) if \(X.\mathrm{prev} = z\), and \(C = S(z)\) otherwise. Then \(S'(z)\) is \(C\) with the previous pointer of its node set to \(X.\mathrm{prev}\) if \(X.\mathrm{next} = z\), and \(S'(z) = C\) otherwise; an empty cell stays empty. So the write at the predecessor is applied before the write at the successor.

public theorem listDelete_get {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome)
    (z : Fin capacity) :
    (listDelete store head x hx hp hn).ret.1.get z =
      let originalX := (store.get x).get hx
      let carried := if originalX.prev = some z then
        (store.get z).map fun node => { node with next := originalX.next } else store.get z
      if originalX.next = some z then
        carried.map fun node => { node with prev := originalX.prev } else carried

Uses 3 · Used by 6

Statement usesDoubly linked list node · Deletion from a doubly linked list

Proof usesResult of doubly linked list deletion

Used byDeletion from a doubly linked list allocates and frees nothing · The deleted node keeps its record · Deletion changes only the cells of the neighbors · Deletion preserves payloads · Correctness of doubly linked list deletion · Cells after sentinel deletion

TheoremDeletion changes only the cells of the neighbors#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Let \(S'\) be the store returned by List Delete on \(S\), \(h\) and \(x\). Then \(S'(z) = S(z)\) for every index \(z\) with \(X.\mathrm{prev} \ne z\) and \(X.\mathrm{next} \ne z\).

public theorem listDelete_frame {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome)
    (z : Fin capacity)
    (hzp : ((store.get x).get hx).prev ≠ some z)
    (hzn : ((store.get x).get hx).next ≠ some z) :
    (listDelete store head x hx hp hn).ret.1.get z = store.get z

Uses 3 · Used by 2

Statement usesDoubly linked list node · Deletion from a doubly linked list

Proof usesCellwise result of doubly linked list deletion

Used byDeletion preserves lists avoiding the deleted node's neighbors · Sentinel deletion changes only the two neighbours

TheoremDeletion from a doubly linked list allocates and frees nothing#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Let \(S'\) be the store returned by List Delete on \(S\), \(h\) and \(x\). Then for every index \(z\), the cell \(S'(z)\) holds a node if and only if \(S(z)\) does.

public theorem listDelete_allocated {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome)
    (z : Fin capacity) :
    ((listDelete store head x hx hp hn).ret.1.get z).isSome = (store.get z).isSome

Uses 3 · Used by 1

Statement usesDoubly linked list node · Deletion from a doubly linked list

Proof usesCellwise result of doubly linked list deletion

Used bySentinel deletion preserves allocation

TheoremDeletion preserves payloads#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Let \(S'\) be the store returned by List Delete on \(S\), \(h\) and \(x\). Then for every index \(z\), either \(S'(z)\) and \(S(z)\) are both empty, or both hold nodes and these two nodes have the same payload.

public theorem listDelete_payload {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome)
    (z : Fin capacity) :
    ((listDelete store head x hx hp hn).ret.1.get z).map Node.payload =
      (store.get z).map Node.payload

Uses 3 · Used by 1

Statement usesDoubly linked list node · Deletion from a doubly linked list

Proof usesCellwise result of doubly linked list deletion

Used bySentinel deletion preserves payloads

TheoremThe deleted node keeps its record#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Let \(S'\) be the store returned by List Delete on \(S\), \(h\) and \(x\). Then \(S'(x) = S(x)\): the deleted node stays allocated with its payload and both of its pointers unchanged.

public theorem listDelete_deleted_record {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome) :
    (listDelete store head x hx hp hn).ret.1.get x = store.get x

Uses 3 · Used by 1

Statement usesDoubly linked list node · Deletion from a doubly linked list

Proof usesCellwise result of doubly linked list deletion

Used bySentinel deletion keeps the deleted node

TheoremDeletion preserves lists avoiding the deleted node's neighbors#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Let \(S'\) be the store returned by List Delete on \(S\), \(h\) and \(x\). Let \(h_0\) be a header and \(L\) a list of indices such that \(S\) with header \(h_0\) represents \(L\): the entries of \(L\) are distinct, \(h_0\) is the first entry of \(L\) (NIL if \(L\) is empty), and the cell of each entry of \(L\) holds a node whose previous and next pointers are the adjacent entries of \(L\), NIL at the ends. If neither \(X.\mathrm{prev}\) nor \(X.\mathrm{next}\) is an entry of \(L\), then \(S'\) with header \(h_0\) also represents \(L\).

public theorem listDelete_disjoint_represents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome)
    (otherHead : Option (Fin capacity)) (otherIds : List (Fin capacity))
    (rep : Represents store otherHead otherIds)
    (disjointP : ∀ p, ((store.get x).get hx).prev = some p → p ∉ otherIds)
    (disjointN : ∀ n, ((store.get x).get hx).next = some n → n ∉ otherIds) :
    Represents (listDelete store head x hx hp hn).ret.1 otherHead otherIds

Uses 4

Statement usesDoubly linked list node · Store representing a doubly linked list · Deletion from a doubly linked list

Proof usesDeletion changes only the cells of the neighbors

TheoremDoubly linked list deletion costs at most four events#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Then List Delete on \(S\), \(h\) and \(x\) costs at most \(4\), counting NIL tests and executed pointer and header assignments.

public theorem listDelete_time_le {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome) :
    (listDelete store head x hx hp hn).time ≤ 4

Uses 3

Statement usesDoubly linked list node · Deletion from a doubly linked list

Proof usesRunning time of doubly linked list deletion

TheoremCorrectness of doubly linked list deletion#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node (a payload with next and previous pointers, each an index or NIL), let \(h\) be a header (an index in \(\{0, \dots, n-1\}\) or NIL), and let \(x\) be an index whose cell holds a node \(X\) such that the cells at the predecessor \(X.\mathrm{prev}\) and the successor \(X.\mathrm{next}\) hold nodes whenever these pointers are not NIL. Let \(S'\) and \(h'\) be the store and header returned by List Delete on \(S\), \(h\) and \(x\). Let \(L\) be a list of indices such that \(S\) with header \(h\) represents \(L\): the entries of \(L\) are distinct, \(h\) is the first entry of \(L\) (NIL if \(L\) is empty), and the cell of each entry of \(L\) holds a node whose previous and next pointers are the adjacent entries of \(L\), NIL at the ends. If \(x\) is an entry of \(L\), then \(S'\) with header \(h'\) represents the list obtained from \(L\) by removing \(x\).

public theorem listDelete_represents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hn : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome)
    (ids : List (Fin capacity)) (rep : Represents store head ids) (member : x ∈ ids) :
    Represents (listDelete store head x hx hp hn).ret.1
      (listDelete store head x hx hp hn).ret.2 (ids.erase x)

Uses 5

Statement usesDoubly linked list node · Store representing a doubly linked list · Deletion from a doubly linked list

Proof usesCellwise result of doubly linked list deletion · Header after doubly linked list deletion

DefinitionDoubly-linked-list insertion (LIST-INSERT)#✓fully proved

A store is an array of \(n\) cells, each either empty or holding a node with a payload and optional next and previous pointers to cells. Given allocated cells \(x\) and \(y\) such that the successor of \(y\), if any, is allocated, inserting \(x\) after \(y\) performs the five lines of LIST-INSERT in order, each reading the store as updated so far: set the next pointer of \(x\) to the next pointer of \(y\); set the previous pointer of \(x\) to \(y\); test whether the next pointer of \(y\) is NIL; if it is some cell \(z\), set the previous pointer of \(z\) to \(x\); set the next pointer of \(y\) to \(x\). The result is the updated store, with cost one unit per pointer assignment and per NIL test.

Cslib.Algorithms.Lean.DoublyLinkedList.listInsert · 36 lines

public def listInsert {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hs : ∀ z, ((store.get y).get hy).next = some z → (store.get z).isSome) :
    TimeM Nat (Vector (Option (Node α (Fin n))) n) := do
  let oldY := (store.get y).get hy
  TimeM.tick 1
  let nextX := { (store.get x).get hx with next := oldY.next }
  let store1 := store.set x.val (some nextX) x.isLt
  have hx1 := (allocated_set store x hx nextX x).trans hx
  have hy1 := (allocated_set store x hx nextX y).trans hy
  TimeM.tick 1
  let prevX := { (store1.get x).get hx1 with prev := some y }
  let store2 := store1.set x.val (some prevX) x.isLt
  have hy2 := (allocated_set store1 x hx1 prevX y).trans hy1
  let currentY2 := (store2.get y).get hy2
  have nextPreserved : currentY2.next = oldY.next :=
    (y_next_after_prev store1 x y hx1 hy1).trans
      (y_next_after_set store x y hx hy)
  TimeM.tick 1
  match he : currentY2.next with
  | none =>
    TimeM.tick 1
    pure (store2.set y.val (some { currentY2 with next := some x }) y.isLt)
  | some z =>
    have hz := hs z (nextPreserved.symm.trans he)
    have hz1 := (allocated_set store x hx nextX z).trans hz
    have hz2 := (allocated_set store1 x hx1 prevX z).trans hz1
    let currentZ := (store2.get z).get hz2
    TimeM.tick 1
    let newZ := { currentZ with prev := some x }
    let store3 := store2.set z.val (some newZ) z.isLt
    have hy3 := (allocated_set store2 z hz2 newZ y).trans hy2
    let currentY3 := (store3.get y).get hy3
    TimeM.tick 1
    pure (store3.set y.val (some { currentY3 with next := some x }) y.isLt)

Uses 1 · Used by 12

Statement usesDoubly linked list node

Used byDoubly-linked-list insertion neither allocates nor frees cells · Doubly-linked-list insertion preserves disjoint lists · Frame property of doubly-linked-list insertion · Cells after doubly-linked-list insertion · Doubly-linked-list insertion preserves payloads · Insertion into a represented doubly-linked list · Result of doubly-linked-list insertion · Cost of doubly-linked-list insertion · Sentinel insertion preserves allocation · Sentinel insertion leaves other cells unchanged · Sentinel insertion, cell by cell · Sentinel insertion preserves payloads

TheoremCost of doubly-linked-list insertion#✓fully proved

For a store \(S\) and allocated cells \(x\) and \(y\) such that the successor of \(y\) in \(S\), if any, is allocated, the cost of inserting \(x\) after \(y\), counting one unit per pointer assignment and per NIL test, is \(5\) if \(y\) has a successor in \(S\) and \(4\) if the next pointer of \(y\) in \(S\) is NIL.

No distinctness of \(x\) and \(y\) is assumed.

public theorem listInsert_time {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hs : ∀ z, ((store.get y).get hy).next = some z → (store.get z).isSome) :
    (listInsert store x y hx hy hs).time =
      if ((store.get y).get hy).next.isSome then 5 else 4

Uses 2

Statement usesDoubly linked list node · Doubly-linked-list insertion (LIST-INSERT)

TheoremResult of doubly-linked-list insertion#✓fully proved

For a store \(S\) and allocated cells \(x\) and \(y\) such that the successor of \(y\) in \(S\), if any, is allocated, let \(s\) be the next pointer of \(y\) in \(S\). Let \(S_1\) be \(S\) with cell \(x\) replaced by the node of \(x\) with next pointer \(s\) and previous pointer \(y\). Let \(S_2 = S_1\) if \(s\) is NIL; if \(s\) is a cell \(z\), let \(S_2\) be \(S_1\) with the previous pointer of the node in cell \(z\) of \(S_1\) replaced by \(x\). Then the store returned by inserting \(x\) after \(y\) is \(S_2\) with the next pointer of the node in cell \(y\) of \(S_2\) replaced by \(x\).

No distinctness or representation hypothesis is assumed.

public theorem listInsert_ret {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hs : ∀ z, ((store.get y).get hy).next = some z → (store.get z).isSome) :
    let updated := store.set x.val (some { (store.get x).get hx with
      next := ((store.get y).get hy).next, prev := some y }) x.isLt
    let backlinked := match ((store.get y).get hy).next with

Uses 2 · Used by 5

Statement usesDoubly linked list node · Doubly-linked-list insertion (LIST-INSERT)

Used byCells after doubly-linked-list insertion · Sentinel insertion preserves allocation · Sentinel insertion leaves other cells unchanged · Sentinel insertion, cell by cell · Sentinel insertion preserves payloads

TheoremCells after doubly-linked-list insertion#✓fully proved

For a store \(S\), allocated cells \(x\) and \(y\) such that the successor of \(y\) in \(S\), if any, is allocated, and any cell \(z\), let \(s\) be the next pointer of \(y\) in \(S\). Let \(c_1\) be the node of \(x\) in \(S\) with next pointer replaced by \(s\) and previous pointer replaced by \(y\) if \(z = x\), and the content of cell \(z\) in \(S\) otherwise. Let \(c_2\) be \(c_1\) with previous pointer replaced by \(x\) if \(s = z\), and \(c_1\) otherwise. Then cell \(z\) of the store returned by inserting \(x\) after \(y\) is \(c_2\) with next pointer replaced by \(x\) if \(z = y\), and \(c_2\) otherwise (an empty cell stays empty).

No distinctness of \(x\), \(y\) and \(s\) is assumed.

public theorem listInsert_get {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y z : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hs : ∀ w, ((store.get y).get hy).next = some w → (store.get w).isSome) :
    let first := if x = z then some { (store.get x).get hx with
      next := ((store.get y).get hy).next, prev := some y } else store.get z
    let second := if ((store.get y).get hy).next = some z then
      first.map (fun (node : Node α (Fin n)) => { node with prev := some x }) else first
    (listInsert store x y hx hy hs).ret.get z =
      if y = z then second.map (fun (node : Node α (Fin n)) =>
        { node with next := some x }) else second

Uses 3 · Used by 5

Statement usesDoubly linked list node · Doubly-linked-list insertion (LIST-INSERT)

Proof usesResult of doubly-linked-list insertion

Used byDoubly-linked-list insertion neither allocates nor frees cells · Frame property of doubly-linked-list insertion · Doubly-linked-list insertion preserves payloads · Insertion into a represented doubly-linked list · Sentinel insertion, cell by cell

TheoremFrame property of doubly-linked-list insertion#✓fully proved

For a store \(S\) and allocated cells \(x\) and \(y\) such that the successor of \(y\) in \(S\), if any, is allocated, let \(z\) be a cell with \(z \ne x\), \(z \ne y\), and \(z\) not the successor of \(y\) in \(S\). Then cell \(z\) of the store returned by inserting \(x\) after \(y\) equals cell \(z\) of \(S\).

public theorem listInsert_frame {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y z : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hs : ∀ w, ((store.get y).get hy).next = some w → (store.get w).isSome)
    (hxz : x ≠ z) (hyz : y ≠ z) (hsz : ((store.get y).get hy).next ≠ some z) :
    (listInsert store x y hx hy hs).ret.get z = store.get z

Uses 3 · Used by 2

Statement usesDoubly linked list node · Doubly-linked-list insertion (LIST-INSERT)

Proof usesCells after doubly-linked-list insertion

Used byDoubly-linked-list insertion preserves disjoint lists · Sentinel insertion leaves other cells unchanged

TheoremDoubly-linked-list insertion neither allocates nor frees cells#✓fully proved

For a store \(S\) and allocated cells \(x\) and \(y\) such that the successor of \(y\) in \(S\), if any, is allocated, every cell \(z\) of the store returned by inserting \(x\) after \(y\) is allocated if and only if cell \(z\) of \(S\) is allocated. No distinctness of \(x\), \(y\) and the successor of \(y\) is assumed.

public theorem listInsert_allocated {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y z : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hs : ∀ w, ((store.get y).get hy).next = some w → (store.get w).isSome) :
    ((listInsert store x y hx hy hs).ret.get z).isSome =
      (store.get z).isSome

Uses 3 · Used by 1

Statement usesDoubly linked list node · Doubly-linked-list insertion (LIST-INSERT)

Proof usesCells after doubly-linked-list insertion

Used bySentinel insertion preserves allocation

TheoremDoubly-linked-list insertion preserves payloads#✓fully proved

For a store \(S\) and allocated cells \(x\) and \(y\) such that the successor of \(y\) in \(S\), if any, is allocated, every cell \(z\) of the store returned by inserting \(x\) after \(y\) is empty exactly when cell \(z\) of \(S\) is empty, and otherwise holds a node with the same payload as the node in cell \(z\) of \(S\).

No hypothesis on the payloads, such as distinct keys, is needed.

public theorem listInsert_payload {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y z : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hs : ∀ w, ((store.get y).get hy).next = some w → (store.get w).isSome) :
    ((listInsert store x y hx hy hs).ret.get z).map Node.payload =
      (store.get z).map Node.payload

Uses 3 · Used by 1

Statement usesDoubly linked list node · Doubly-linked-list insertion (LIST-INSERT)

Proof usesCells after doubly-linked-list insertion

Used bySentinel insertion preserves payloads

TheoremInsertion into a represented doubly-linked list#✓fully proved

Suppose the store \(S\) with head \(h\) represents the list of distinct cells \((i_0, \dots, i_{m-1})\). Let \(k < m\), let \(x\) be an allocated cell not among \(i_0, \dots, i_{m-1}\), and assume that cell \(i_k\) and its successor in \(S\), if any, are allocated. Then the store returned by inserting \(x\) after \(i_k\), with the same head \(h\), represents the list \((i_0, \dots, i_k, x, i_{k+1}, \dots, i_{m-1})\).

The hypothesis that \(x\) is not in the list is used only in the proof; the insertion itself runs without it.

public theorem listInsert_represents {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x : Fin n)
    (head : Option (Fin n)) (ids : List (Fin n)) (rep : Represents store head ids)
    (fresh : x ∉ ids) (k : Nat) (hk : k < ids.length)
    (hx : (store.get x).isSome) (hy : (store.get ids[k]).isSome)
    (hs : ∀ z, ((store.get ids[k]).get hy).next = some z → (store.get z).isSome) :
    Represents (listInsert store x ids[k] hx hy hs).ret head
      (ids.insertIdx (k + 1) x)

Uses 4

Statement usesDoubly linked list node · Store representing a doubly linked list · Doubly-linked-list insertion (LIST-INSERT)

Proof usesCells after doubly-linked-list insertion

TheoremDoubly-linked-list insertion preserves disjoint lists#✓fully proved

Suppose the store \(S\) with head \(h\) represents the list of cells \((i_0, \dots, i_{m-1})\) and with head \(h'\) represents a list \(L'\) of cells, and that the two lists have no cell in common. Let \(k < m\), let \(x\) be an allocated cell not in \(L'\), and assume that cell \(i_k\) and its successor in \(S\), if any, are allocated. Then the store returned by inserting \(x\) after \(i_k\), with head \(h'\), still represents \(L'\).

public theorem listInsert_disjoint_represents {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x : Fin n)
    (head otherHead : Option (Fin n)) (ids otherIds : List (Fin n))
    (rep : Represents store head ids) (otherRep : Represents store otherHead otherIds)
    (disjoint : List.Disjoint ids otherIds) (freshOther : x ∉ otherIds)
    (k : Nat) (hk : k < ids.length) (hx : (store.get x).isSome)
    (hy : (store.get ids[k]).isSome)
    (hs : ∀ z, ((store.get ids[k]).get hy).next = some z → (store.get z).isSome) :
    Represents (listInsert store x ids[k] hx hy hs).ret otherHead otherIds

Uses 4

Statement usesDoubly linked list node · Store representing a doubly linked list · Doubly-linked-list insertion (LIST-INSERT)

Proof usesFrame property of doubly-linked-list insertion

DefinitionCircular doubly linked list with a sentinel#✓fully proved

Let \(S\) be a store of \(n\) slots indexed by \(\{0, \dots, n-1\}\), each either empty or holding a node with a payload and optional next and previous indices. The store \(S\) represents a circular list with sentinel \(s\) and data nodes \(x_1, \dots, x_k\) (a list of indices) when the \(x_i\) are pairwise distinct and all differ from \(s\); slot \(s\) holds a node whose next index is \(x_1\) and whose previous index is \(x_k\) (both are \(s\) when \(k = 0\)); and for every \(i\) with \(1 \le i \le k\), slot \(x_i\) holds a node whose previous index is \(x_{i-1}\) and whose next index is \(x_{i+1}\), where \(x_0 = x_{k+1} = s\).

def CircularRepresents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (s : Fin capacity) (ids : List (Fin capacity)) : Prop :=
  ids.Nodup ∧ s ∉ ids ∧
    (∃ sentinel, store.get s = some sentinel ∧
      sentinel.next = some (ids.headD s) ∧ sentinel.prev = some (ids.getLastD s)) ∧
    ∀ (before : List (Fin capacity)) (a : Fin capacity) (after : List (Fin capacity)),
      ids = before ++ a :: after → ∃ node, store.get a = some node ∧
        node.prev = some (before.getLastD s) ∧ node.next = some (after.headD s)

Uses 1 · Used by 10

Statement usesDoubly linked list node

Used byEmpty circular list with a sentinel · Search in a circular list with a sentinel · Sentinel search preserves the circular list · Sentinel search changes only the sentinel's key · Sentinel search returns the first matching node · Cost of sentinel search · Sentinel deletion removes a node from its circular list · Sentinel deletion preserves disjoint circular lists · Sentinel insertion preserves the circular list · Sentinel insertion preserves a disjoint circular list

TheoremEmpty circular list with a sentinel#✓fully proved

Let \(S\) be a store of \(n\) slots indexed by \(\{0, \dots, n-1\}\), each either empty or holding a node with a payload and optional next and previous indices, and let \(s\) be an index. Then \(S\) represents the empty circular list with sentinel \(s\) if and only if slot \(s\) holds a node whose next index and previous index are both \(s\).

public theorem CircularRepresents_nil {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity) (s : Fin capacity) :
    CircularRepresents store s [] ↔
      ∃ sentinel, store.get s = some sentinel ∧
        sentinel.next = some s ∧ sentinel.prev = some s

Uses 2

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node

DefinitionDeletion from a circular list with a sentinel#✓fully proved

Let \(S\) be a node store with \(c\) cells, each either empty or holding a node (a payload, an optional next address and an optional previous address in \(\{0, \dots, c-1\}\)). Let \(x\) be an address whose cell holds a node \(\nu\) with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. Sentinel deletion of \(x\) from \(S\) is the timed computation that first sets the next address of the node at \(p\) to \(n\), at cost \(1\), then sets the previous address of the node at \(n\) in the resulting store to \(p\), at cost \(1\), and returns the store obtained.

These dereferences are its only preconditions: it does not check that \(x\) is not the sentinel or that \(x\) lies on a represented list.

Cslib.Algorithms.Lean.DoublyLinkedList.sentinelDelete · 40 lines

public def sentinelDelete {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ((store.get x).get hx).prev.isSome)
    (hn : ((store.get x).get hx).next.isSome)
    (hprev : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hnext : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome) :
    TimeM Nat (Vector (Option (Node α (Fin capacity))) capacity) := do
  let nx := (store.get x).get hx
  let p := nx.prev.get hp
  have hpAllocated := hprev p (Option.some_get hp).symm
  let currentP := (store.get p).get hpAllocated
  TimeM.tick 1
  let updatedP := { currentP with next := nx.next }
  let store1 := store.set p.val (some updatedP) p.isLt
  have hStable : store1.get x = some nx :=
    first_write_keeps_x store x p nx currentP
      (Option.some_get hx).symm (Option.some_get hpAllocated).symm
  have hx1 : (store1.get x).isSome := by
    rw [hStable]
    rfl
  let currentX := (store1.get x).get hx1
  have currentX_eq : currentX = nx :=
    Option.some.inj ((Option.some_get hx1).trans hStable)
  have hn1 : currentX.next.isSome := by
    rw [currentX_eq]
    exact hn
  let n := currentX.next.get hn1
  have hNext : nx.next = some n := by
    rw [← currentX_eq]
    exact (Option.some_get hn1).symm
  have hnAllocated : (store1.get n).isSome := by
    dsimp only [store1]
    rw [get_set]
    split
    · rfl
    · exact hnext n hNext
  let currentN := (store1.get n).get hnAllocated
  TimeM.tick 1
  pure (store1.set n.val (some { currentN with prev := currentX.prev }) n.isLt)

Uses 1 · Used by 9

Statement usesDoubly linked list node

Used bySentinel deletion preserves allocation · Sentinel deletion removes a node from its circular list · Sentinel deletion keeps the deleted node · Sentinel deletion preserves disjoint circular lists · Sentinel deletion changes only the two neighbours · Cells after sentinel deletion · Sentinel deletion preserves payloads · The store returned by sentinel deletion · Sentinel deletion takes two pointer assignments

TheoremSentinel deletion takes two pointer assignments#✓fully proved

Let \(S\) be a node store and \(x\) an address whose cell holds a node with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. Then sentinel deletion of \(x\) from \(S\) has cost exactly \(2\), one for each pointer assignment.

This includes the alias cases in which \(p\), \(n\) and \(x\) are not pairwise distinct.

public theorem sentinelDelete_time {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ((store.get x).get hx).prev.isSome)
    (hn : ((store.get x).get hx).next.isSome)
    (hprev : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hnext : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome) :
    (sentinelDelete store x hx hp hn hprev hnext).time = 2

Uses 2

Statement usesDoubly linked list node · Deletion from a circular list with a sentinel

TheoremThe store returned by sentinel deletion#✓fully proved

Let \(S\) be a node store and \(x\) an address whose cell holds a node with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. Let \(S_1\) be \(S\) with the node at \(p\) replaced by a copy whose next address is \(n\). Then sentinel deletion of \(x\) from \(S\) returns \(S_1\) with the node of \(S_1\) at \(n\) replaced by a copy whose previous address is \(p\).

public theorem sentinelDelete_ret {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ((store.get x).get hx).prev.isSome)
    (hn : ((store.get x).get hx).next.isSome)
    (hprev : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hnext : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome) :
    let nx := (store.get x).get hx
    let p := nx.prev.get hp
    let n := nx.next.get hn
    let carried := store.set p.val
      ((store.get p).map fun node => { node with next := nx.next }) p.isLt
    (sentinelDelete store x hx hp hn hprev hnext).ret =
      carried.set n.val ((carried.get n).map fun node => { node with prev := nx.prev }) n.isLt

Uses 2 · Used by 5

Statement usesDoubly linked list node · Deletion from a circular list with a sentinel

Used bySentinel deletion preserves allocation · Sentinel deletion keeps the deleted node · Sentinel deletion changes only the two neighbours · Cells after sentinel deletion · Sentinel deletion preserves payloads

TheoremCells after sentinel deletion#✓fully proved

Let \(S\) be a node store and \(x\) an address whose cell holds a node with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. For every address \(z\), let \(C\) be the cell of \(S\) at \(z\) if \(z \ne p\), and that cell with its next address set to \(n\) if \(z = p\). Then after sentinel deletion of \(x\) from \(S\) the cell at \(z\) is \(C\) if \(z \ne n\), and \(C\) with its previous address set to \(p\) if \(z = n\).

public theorem sentinelDelete_get (z : Fin capacity) :
    (sentinelDelete store x hx hp hn hprev hnext).ret.get z =
      let nx := (store.get x).get hx
      let carried := if nx.prev = some z then
        (store.get z).map fun node => { node with next := nx.next } else store.get z
      if nx.next = some z then
        carried.map fun node => { node with prev := nx.prev } else carried

Uses 6 · Used by 1

Statement usesDoubly linked list node · Deletion from a circular list with a sentinel

Proof usesDeletion from a doubly linked list · Cellwise result of doubly linked list deletion · Result of doubly linked list deletion · The store returned by sentinel deletion

Used bySentinel deletion removes a node from its circular list

TheoremSentinel deletion changes only the two neighbours#✓fully proved

Let \(S\) be a node store and \(x\) an address whose cell holds a node with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. For every address \(z\) with \(z \ne p\) and \(z \ne n\), the cell at \(z\) after sentinel deletion of \(x\) from \(S\) equals the cell of \(S\) at \(z\).

public theorem sentinelDelete_frame (z : Fin capacity)
    (hzp : ((store.get x).get hx).prev ≠ some z)
    (hzn : ((store.get x).get hx).next ≠ some z) :
    (sentinelDelete store x hx hp hn hprev hnext).ret.get z = store.get z

Uses 6 · Used by 1

Statement usesDoubly linked list node · Deletion from a circular list with a sentinel

Proof usesDeletion from a doubly linked list · Deletion changes only the cells of the neighbors · Result of doubly linked list deletion · The store returned by sentinel deletion

Used bySentinel deletion preserves disjoint circular lists

TheoremSentinel deletion preserves allocation#✓fully proved

Let \(S\) be a node store and \(x\) an address whose cell holds a node with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. For every address \(z\), the cell at \(z\) after sentinel deletion of \(x\) from \(S\) is nonempty if and only if the cell of \(S\) at \(z\) is nonempty.

public theorem sentinelDelete_allocated (z : Fin capacity) :
    ((sentinelDelete store x hx hp hn hprev hnext).ret.get z).isSome =
      (store.get z).isSome

Uses 6

Statement usesDoubly linked list node · Deletion from a circular list with a sentinel

Proof usesDeletion from a doubly linked list · Deletion from a doubly linked list allocates and frees nothing · Result of doubly linked list deletion · The store returned by sentinel deletion

TheoremSentinel deletion preserves payloads#✓fully proved

Let \(S\) be a node store and \(x\) an address whose cell holds a node with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. For every address \(z\), the cell at \(z\) after sentinel deletion of \(x\) from \(S\) and the cell of \(S\) at \(z\) are either both empty or both hold nodes with the same payload.

The payload includes any key and satellite data.

public theorem sentinelDelete_payload (z : Fin capacity) :
    ((sentinelDelete store x hx hp hn hprev hnext).ret.get z).map Node.payload =
      (store.get z).map Node.payload

Uses 6

Statement usesDoubly linked list node · Deletion from a circular list with a sentinel

Proof usesDeletion from a doubly linked list · Deletion preserves payloads · Result of doubly linked list deletion · The store returned by sentinel deletion

TheoremSentinel deletion keeps the deleted node#✓fully proved

Let \(S\) be a node store and \(x\) an address whose cell holds a node with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. The cell at \(x\) after sentinel deletion of \(x\) from \(S\) equals the cell of \(S\) at \(x\), so the deleted node stays allocated and unchanged.

public theorem sentinelDelete_deleted_record :
    (sentinelDelete store x hx hp hn hprev hnext).ret.get x = store.get x

Uses 6

Statement usesDoubly linked list node · Deletion from a circular list with a sentinel

Proof usesDeletion from a doubly linked list · The deleted node keeps its record · Result of doubly linked list deletion · The store returned by sentinel deletion

TheoremSentinel deletion removes a node from its circular list#✓fully proved

Let \(S\) be a node store and \(x\) an address whose cell holds a node with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. If \(S\) represents a circular doubly linked list with sentinel \(s\) and data addresses \(\ell\), and \(x\) occurs in \(\ell\), then the store returned by sentinel deletion of \(x\) from \(S\) represents a circular doubly linked list with sentinel \(s\) and the list of data addresses obtained from \(\ell\) by removing the first occurrence of \(x\).

public theorem sentinelDelete_circular {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ((store.get x).get hx).prev.isSome)
    (hn : ((store.get x).get hx).next.isSome)
    (hprev : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hnext : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome)
    (s : Fin capacity) (ids : List (Fin capacity))
    (rep : CircularRepresents store s ids) (member : x ∈ ids) :
    CircularRepresents (sentinelDelete store x hx hp hn hprev hnext).ret
      s (ids.erase x)

Uses 4

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node · Deletion from a circular list with a sentinel

Proof usesCells after sentinel deletion

TheoremSentinel deletion preserves disjoint circular lists#✓fully proved

Let \(S\) be a node store and \(x\) an address whose cell holds a node with previous address \(p\) and next address \(n\), where the cells at \(p\) and \(n\) are nonempty. Suppose \(S\) represents a circular doubly linked list with sentinel \(s\) and data addresses \(\ell\), with \(x\) in \(\ell\), and also one with sentinel \(t\) and data addresses \(m\), such that no address occurs both among \(s\) and \(\ell\) and among \(t\) and \(m\). Then the store returned by sentinel deletion of \(x\) from \(S\) still represents the circular doubly linked list with sentinel \(t\) and data addresses \(m\).

public theorem sentinelDelete_disjoint_circular {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (hp : ((store.get x).get hx).prev.isSome)
    (hn : ((store.get x).get hx).next.isSome)
    (hprev : ∀ p, ((store.get x).get hx).prev = some p → (store.get p).isSome)
    (hnext : ∀ n, ((store.get x).get hx).next = some n → (store.get n).isSome)
    (s t : Fin capacity) (ids otherIds : List (Fin capacity))
    (rep : CircularRepresents store s ids) (member : x ∈ ids)
    (otherRep : CircularRepresents store t otherIds)
    (disjoint : (s :: ids).Disjoint (t :: otherIds)) :
    CircularRepresents (sentinelDelete store x hx hp hn hprev hnext).ret
      t otherIds

Uses 4

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node · Deletion from a circular list with a sentinel

Proof usesSentinel deletion changes only the two neighbours

DefinitionSentinel list insertion (LIST-INSERT′)#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node, in which the cells \(x\) and \(y\) are allocated, the next pointer of \(y\) is not NIL, and the cell \(w\) it points to is allocated. Sentinel insertion of \(x\) after \(y\) performs four pointer assignments in order, each costing one time unit, and returns the resulting store: set the next pointer of \(x\) to the next pointer of \(y\); set the previous pointer of \(x\) to \(y\); set the previous pointer of the successor \(w\) of \(y\) to \(x\); set the next pointer of \(y\) to \(x\).

Each assignment reads the store left by the previous ones, so aliased cells see earlier writes. Unlike LIST-INSERT, there is no NIL test.

Cslib.Algorithms.Lean.DoublyLinkedList.sentinelInsert · 34 lines

public def sentinelInsert {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hn : ((store.get y).get hy).next.isSome)
    (hs : ∀ z, ((store.get y).get hy).next = some z → (store.get z).isSome) :
    TimeM Nat (Vector (Option (Node α (Fin n))) n) := do
  let oldY := (store.get y).get hy
  TimeM.tick 1
  let nextX := { (store.get x).get hx with next := oldY.next }
  let store1 := store.set x.val (some nextX) x.isLt
  have hx1 := (allocated_set store x hx nextX x).trans hx
  have hy1 := (allocated_set store x hx nextX y).trans hy
  TimeM.tick 1
  let prevX := { (store1.get x).get hx1 with prev := some y }
  let store2 := store1.set x.val (some prevX) x.isLt
  have hy2 := (allocated_set store1 x hx1 prevX y).trans hy1
  let currentY2 := (store2.get y).get hy2
  have nextPreserved : currentY2.next = oldY.next :=
    (y_next_after_prev store1 x y hx1 hy1).trans
      (y_next_after_set store x y hx hy)
  have hn2 : currentY2.next.isSome := by rw [nextPreserved]; exact hn
  let z := currentY2.next.get hn2
  have he : oldY.next = some z :=
    nextPreserved.symm.trans (Option.some_get hn2).symm
  have hz := hs z he
  have hz1 := (allocated_set store x hx nextX z).trans hz
  have hz2 := (allocated_set store1 x hx1 prevX z).trans hz1
  TimeM.tick 1
  let newZ := { (store2.get z).get hz2 with prev := some x }
  let store3 := store2.set z.val (some newZ) z.isLt
  have hy3 := (allocated_set store2 z hz2 newZ y).trans hy2
  TimeM.tick 1
  pure (store3.set y.val
    (some { (store3.get y).get hy3 with next := some x }) y.isLt)

Uses 1 · Used by 8

Statement usesDoubly linked list node

Used bySentinel insertion preserves allocation · Sentinel insertion preserves the circular list · Sentinel insertion preserves a disjoint circular list · Sentinel insertion leaves other cells unchanged · Sentinel insertion, cell by cell · Sentinel insertion preserves payloads · The store after sentinel insertion · Sentinel insertion takes four steps

TheoremSentinel insertion takes four steps#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node, in which the cells \(x\) and \(y\) are allocated, the next pointer of \(y\) is not NIL, and the cell it points to is allocated. Then sentinel insertion of \(x\) after \(y\) in \(S\) costs exactly \(4\) time units, one per pointer assignment.

This counts logical pointer assignments, not full RAM cost.

public theorem sentinelInsert_time {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hn : ((store.get y).get hy).next.isSome)
    (hs : ∀ z, ((store.get y).get hy).next = some z → (store.get z).isSome) :
    (sentinelInsert store x y hx hy hn hs).time = 4

Uses 2

Statement usesDoubly linked list node · Sentinel list insertion (LIST-INSERT′)

TheoremThe store after sentinel insertion#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node, in which the cells \(x\) and \(y\) are allocated, the next pointer of \(y\) is not NIL, and the cell \(w\) it points to is allocated; write \(S[c]\) for the node at an allocated cell \(c\). Then the store returned by sentinel insertion of \(x\) after \(y\) is obtained from \(S\) by three updates, each applied to the result of the previous one: replace the content of \(x\) by the node \(S[x]\) with next pointer equal to the next pointer of \(S[y]\) and previous pointer \(y\); set the previous pointer of the node at \(w\) to \(x\); set the next pointer of the node at \(y\) to \(x\).

No freshness or distinctness of \(x\), \(y\) and \(w\) is assumed.

public theorem sentinelInsert_ret {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hn : ((store.get y).get hy).next.isSome)
    (hs : ∀ z, ((store.get y).get hy).next = some z → (store.get z).isSome) :
    let updated := store.set x.val (some { (store.get x).get hx with
      next := ((store.get y).get hy).next, prev := some y }) x.isLt
    let z := ((store.get y).get hy).next.get hn
    let backlinked := updated.set z.val
      ((updated.get z).map fun (node : Node α (Fin n)) =>
        { node with prev := some x }) z.isLt
    (sentinelInsert store x y hx hy hn hs).ret = backlinked.set y.val
      ((backlinked.get y).map fun (node : Node α (Fin n)) =>
        { node with next := some x }) y.isLt

Uses 2 · Used by 4

Statement usesDoubly linked list node · Sentinel list insertion (LIST-INSERT′)

Used bySentinel insertion preserves allocation · Sentinel insertion leaves other cells unchanged · Sentinel insertion, cell by cell · Sentinel insertion preserves payloads

TheoremSentinel insertion, cell by cell#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node, in which the cells \(x\) and \(y\) are allocated, the next pointer of \(y\) is not NIL, and the cell it points to is allocated; write \(S[c]\) for the node at an allocated cell \(c\). Let \(S'\) be the store returned by sentinel insertion of \(x\) after \(y\). Then for every cell \(z\), the content of \(z\) in \(S'\) is obtained from its content in \(S\) by three steps in order: if \(z = x\), replace the content by the node \(S[x]\) with next pointer equal to the next pointer of \(S[y]\) and previous pointer \(y\); if the next pointer of \(S[y]\) is \(z\), set the previous pointer to \(x\); if \(z = y\), set the next pointer to \(x\). The last two steps leave an empty cell empty.

No distinctness of \(x\), \(y\), \(z\) and the successor of \(y\) is assumed.

public theorem sentinelInsert_get {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y z : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hn : ((store.get y).get hy).next.isSome)
    (hs : ∀ w, ((store.get y).get hy).next = some w → (store.get w).isSome) :
    let first := if x = z then some { (store.get x).get hx with
      next := ((store.get y).get hy).next, prev := some y } else store.get z
    let second := if ((store.get y).get hy).next = some z then
      first.map (fun (node : Node α (Fin n)) => { node with prev := some x }) else first
    (sentinelInsert store x y hx hy hn hs).ret.get z =
      if y = z then second.map (fun (node : Node α (Fin n)) =>
        { node with next := some x }) else second

Uses 6 · Used by 1

Statement usesDoubly linked list node · Sentinel list insertion (LIST-INSERT′)

Proof usesDoubly-linked-list insertion (LIST-INSERT) · Cells after doubly-linked-list insertion · Result of doubly-linked-list insertion · The store after sentinel insertion

Used bySentinel insertion preserves the circular list

TheoremSentinel insertion leaves other cells unchanged#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node, in which the cells \(x\) and \(y\) are allocated, the next pointer of \(y\) is not NIL, and the cell it points to is allocated. Let \(S'\) be the store returned by sentinel insertion of \(x\) after \(y\). If a cell \(z\) differs from \(x\) and from \(y\), and the next pointer of \(y\) in \(S\) is not \(z\), then \(z\) has the same content in \(S'\) as in \(S\).

public theorem sentinelInsert_frame {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y z : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hn : ((store.get y).get hy).next.isSome)
    (hs : ∀ w, ((store.get y).get hy).next = some w → (store.get w).isSome)
    (hxz : x ≠ z) (hyz : y ≠ z) (hsz : ((store.get y).get hy).next ≠ some z) :
    (sentinelInsert store x y hx hy hn hs).ret.get z = store.get z

Uses 6 · Used by 1

Statement usesDoubly linked list node · Sentinel list insertion (LIST-INSERT′)

Proof usesDoubly-linked-list insertion (LIST-INSERT) · Frame property of doubly-linked-list insertion · Result of doubly-linked-list insertion · The store after sentinel insertion

Used bySentinel insertion preserves a disjoint circular list

TheoremSentinel insertion preserves allocation#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node, in which the cells \(x\) and \(y\) are allocated, the next pointer of \(y\) is not NIL, and the cell it points to is allocated. Let \(S'\) be the store returned by sentinel insertion of \(x\) after \(y\). Then every cell \(z\) is allocated in \(S'\) if and only if it is allocated in \(S\).

No distinctness of \(x\), \(y\), \(z\) and the successor of \(y\) is assumed.

public theorem sentinelInsert_allocated {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y z : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hn : ((store.get y).get hy).next.isSome)
    (hs : ∀ w, ((store.get y).get hy).next = some w → (store.get w).isSome) :
    ((sentinelInsert store x y hx hy hn hs).ret.get z).isSome =
      (store.get z).isSome

Uses 6

Statement usesDoubly linked list node · Sentinel list insertion (LIST-INSERT′)

Proof usesDoubly-linked-list insertion (LIST-INSERT) · Doubly-linked-list insertion neither allocates nor frees cells · Result of doubly-linked-list insertion · The store after sentinel insertion

TheoremSentinel insertion preserves payloads#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node, in which the cells \(x\) and \(y\) are allocated, the next pointer of \(y\) is not NIL, and the cell it points to is allocated. Let \(S'\) be the store returned by sentinel insertion of \(x\) after \(y\). Then for every cell \(z\), either \(z\) is empty in both \(S\) and \(S'\), or it holds a node in both and the two nodes have the same payload, including keys and satellite data.

public theorem sentinelInsert_payload {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y z : Fin n)
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hn : ((store.get y).get hy).next.isSome)
    (hs : ∀ w, ((store.get y).get hy).next = some w → (store.get w).isSome) :
    ((sentinelInsert store x y hx hy hn hs).ret.get z).map Node.payload =
      (store.get z).map Node.payload

Uses 6

Statement usesDoubly linked list node · Sentinel list insertion (LIST-INSERT′)

Proof usesDoubly-linked-list insertion (LIST-INSERT) · Doubly-linked-list insertion preserves payloads · Result of doubly-linked-list insertion · The store after sentinel insertion

TheoremSentinel insertion preserves the circular list#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node, in which the cells \(x\) and \(y\) are allocated, the next pointer of \(y\) is not NIL, and the cell it points to is allocated. Suppose \(S\) circularly represents the list \(L\) of cells with sentinel \(s\), that \(L\) is the concatenation of lists \(B\) and \(A\), and that \(y\) is the last element of \(B\), or \(y = s\) if \(B\) is empty. If \(x \ne s\) and \(x\) does not occur in \(L\), then the store returned by sentinel insertion of \(x\) after \(y\) circularly represents, with sentinel \(s\), the list consisting of the elements of \(B\), then \(x\), then the elements of \(A\).

public theorem sentinelInsert_circular {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y s : Fin n)
    (ids before after : List (Fin n))
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hn : ((store.get y).get hy).next.isSome)
    (hs : ∀ z, ((store.get y).get hy).next = some z → (store.get z).isSome)
    (hc : CircularRepresents store s ids)
    (hSplit : ids = before ++ after) (hPosition : y = before.getLastD s)
    (hFreshSentinel : x ≠ s) (hFreshData : x ∉ ids) :
    CircularRepresents (sentinelInsert store x y hx hy hn hs).ret s
      (before ++ x :: after)

Uses 4

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node · Sentinel list insertion (LIST-INSERT′)

Proof usesSentinel insertion, cell by cell

TheoremSentinel insertion preserves a disjoint circular list#✓fully proved

Let \(S\) be a store of \(n\) cells, each empty or holding a node, in which the cells \(x\) and \(y\) are allocated, the next pointer of \(y\) is not NIL, and the cell it points to is allocated. Suppose \(S\) circularly represents the list \(L\) with sentinel \(s\), that \(L\) is the concatenation of lists \(B\) and \(A\), and that \(y\) is the last element of \(B\), or \(y = s\) if \(B\) is empty. Suppose \(S\) also circularly represents the list \(M\) with sentinel \(t\), that no cell among \(s\) and the elements of \(L\) equals \(t\) or an element of \(M\), and that \(x \ne t\) and \(x\) does not occur in \(M\). Then the store returned by sentinel insertion of \(x\) after \(y\) still circularly represents \(M\) with sentinel \(t\).

public theorem sentinelInsert_disjoint_circular {α : Type u} {n : Nat}
    (store : Vector (Option (Node α (Fin n))) n) (x y s t : Fin n)
    (ids before after other : List (Fin n))
    (hx : (store.get x).isSome) (hy : (store.get y).isSome)
    (hn : ((store.get y).get hy).next.isSome)
    (hs : ∀ z, ((store.get y).get hy).next = some z → (store.get z).isSome)
    (hc : CircularRepresents store s ids)
    (hSplit : ids = before ++ after) (hPosition : y = before.getLastD s)
    (hcOther : CircularRepresents store t other)
    (hDisjoint : List.Disjoint (s :: ids) (t :: other))
    (hFreshSentinel : x ≠ t) (hFreshData : x ∉ other) :
    CircularRepresents (sentinelInsert store x y hx hy hn hs).ret t other

Uses 4

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node · Sentinel list insertion (LIST-INSERT′)

Proof usesSentinel insertion leaves other cells unchanged

DefinitionSearch in a circular list with a sentinel#✓fully proved

Let a store have cells indexed by \(\{0, \dots, m-1\}\), each empty or holding a node that carries a key, satellite data and optional next and prev links, and let the cell \(s\) be the sentinel of some list of data nodes that the store circularly represents. Sentinel search for a key \(k\) first overwrites the key of the sentinel with \(k\), keeping its satellite data and links, then starts at the successor of \(s\) and follows next links until it reaches a node whose key is \(k\). It returns the modified store together with that node, or no node if the scan stopped at \(s\).

Only the sentinel key is overwritten, and its old key is not restored. The cost charges one unit for the key write, one for initializing the cursor, one for each key comparison, one for each advance past a mismatching node and one for the final test against \(s\); reads and result construction are free, and physical storage or bit operations are not counted.

Cslib.Algorithms.Lean.DoublyLinkedList.listSearchSentinel · 25 lines

public def listSearchSentinel {Key : Type u} {Satellite : Type v} {capacity : Nat} [DecidableEq Key]
    (store : Vector (Option (Node (Key × Satellite) (Fin capacity))) capacity)
    (s : Fin capacity) (key : Key) (valid : ∃ ids, CircularRepresents store s ids) :
    TimeM Nat (Vector (Option (Node (Key × Satellite) (Fin capacity))) capacity ×
      Option (Fin capacity)) :=
  let hs := onCircle_allocated store s s (valid_sentinel store s valid)
  do
    TimeM.tick 1
    let updated := keyWrite store s key hs
    have updatedValid : ∃ ids, CircularRepresents updated s ids := by
      obtain ⟨ids, rep⟩ := valid
      exact ⟨ids, keyWrite_circular store s key hs ids rep⟩
    let allocated := onCircle_allocated updated s
    let sentinel := (updated.get s).get (allocated s (valid_sentinel updated s updatedValid))
    let nextProof := valid_initial updated s updatedValid
      (allocated s (valid_sentinel updated s updatedValid))
    TimeM.tick 1
    let cursor := sentinel.next.get nextProof.choose
    let hg := nextProof.choose_spec
    let acc := onCircle_acc updated s key (keyWrite_match store s key hs) cursor hg
    let scan := reachableLoop updated key (OnCircle updated s) allocated
      (onCircle_next updated s key (keyWrite_match store s key hs)) cursor acc hg
    TimeM.tick scan.time
    TimeM.tick 1
    pure (updated, if scan.ret = s then none else some scan.ret)

Uses 2 · Used by 4

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node

Used bySentinel search preserves the circular list · Sentinel search changes only the sentinel's key · Sentinel search returns the first matching node · Cost of sentinel search

TheoremSentinel search returns the first matching node#✓fully proved

If a store circularly represents the list \(L\) of data nodes with sentinel \(s\), then sentinel search for a key \(k\) returns the first node of \(L\) (in list order, which starts at the successor of \(s\)) whose key in the input store is \(k\), and returns no node if no node of \(L\) has key \(k\). In particular, the sentinel is never returned.

public theorem listSearchSentinel_ret {Key : Type u} {Satellite : Type v} {capacity : Nat}
    [DecidableEq Key]
    (store : Vector (Option (Node (Key × Satellite) (Fin capacity))) capacity)
    (s : Fin capacity) (key : Key) (ids : List (Fin capacity))
    (rep : CircularRepresents store s ids) :
    (listSearchSentinel store s key ⟨ids, rep⟩).ret.2 =
      ids.find? (fun x => decide
        ((store.get x).map (fun node => node.payload.1) = some key))

Uses 3

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node · Search in a circular list with a sentinel

TheoremCost of sentinel search#✓fully proved

If a store circularly represents the list \(L\) of \(n\) data nodes with sentinel \(s\), then sentinel search for a key \(k\) costs exactly \(2i + 4\), where \(i\) is the position, counting from \(0\), of the first node of \(L\) whose key is \(k\), and \(i = n\) if no node of \(L\) has key \(k\).

That is, two units for each mismatching data node before the match plus four fixed units; an unsuccessful search scans all \(n\) data nodes.

public theorem listSearchSentinel_time {Key : Type u} {Satellite : Type v} {capacity : Nat}
    [DecidableEq Key]
    (store : Vector (Option (Node (Key × Satellite) (Fin capacity))) capacity)
    (s : Fin capacity) (key : Key) (ids : List (Fin capacity))
    (rep : CircularRepresents store s ids) :
    (listSearchSentinel store s key ⟨ids, rep⟩).time =
      2 * (ids.findIdx? (fun x => decide
        ((store.get x).map (fun node => node.payload.1) = some key))).getD ids.length + 4

Uses 3

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node · Search in a circular list with a sentinel

TheoremSentinel search changes only the sentinel's key#✓fully proved

Let \(s\) be the sentinel of some list of data nodes that a store circularly represents, and let \(k\) be a key. In the store returned by sentinel search for \(k\), the cell \(s\) holds the original sentinel node with its key replaced by \(k\) and its satellite data and next and prev links unchanged, and every cell \(z \ne s\) holds exactly what it held in the input store.

public theorem listSearchSentinel_get {Key : Type u} {Satellite : Type v} {capacity : Nat}
    [DecidableEq Key]
    (store : Vector (Option (Node (Key × Satellite) (Fin capacity))) capacity)
    (s : Fin capacity) (key : Key) (valid : ∃ ids, CircularRepresents store s ids)
    (z : Fin capacity) :
    (listSearchSentinel store s key valid).ret.1.get z =
      if z = s then
        (store.get z).map (fun node => { node with payload := (key, node.payload.2) })
      else store.get z

Uses 3

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node · Search in a circular list with a sentinel

TheoremSentinel search preserves the circular list#✓fully proved

If a store circularly represents the list \(L\) of data nodes with sentinel \(s\), then for every key \(k\) the store returned by sentinel search for \(k\) still circularly represents \(L\) with sentinel \(s\).

public theorem listSearchSentinel_circular {Key : Type u} {Satellite : Type v} {capacity : Nat}
    [DecidableEq Key]
    (store : Vector (Option (Node (Key × Satellite) (Fin capacity))) capacity)
    (s : Fin capacity) (key : Key) (ids : List (Fin capacity))
    (rep : CircularRepresents store s ids) :
    CircularRepresents (listSearchSentinel store s key ⟨ids, rep⟩).ret.1 s ids

Uses 3

Statement usesCircular doubly linked list with a sentinel · Doubly linked list node · Search in a circular list with a sentinel

62 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.