Singly linked list

StructureSingly linked list node#✓fully proved

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

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 ι
deriving DecidableEq, Repr

Used by 35

Used byPayload list of a singly linked list store · The payload list depends only on the listed cells · The payload list has one entry per identity · Deleting the successor in a singly linked list · Contents after deleting a successor · Deleting a successor leaves other cells unchanged · Cells after deleting a successor · Deleting a successor preserves payloads · Deleting a successor removes it from the represented list · Deleting the head of a singly linked list · Deleting the head removes the first identity · Inserting a node after another in a singly linked list · Contents after singly-linked-list insertion · Frame property of singly-linked-list insertion · Cells after singly-linked-list insertion · Singly-linked-list insertion preserves payloads · Insertion into a represented singly linked list · Prepending a node to a singly linked list · Contents after prepending to a singly linked list · Frame property of prepending to a singly linked list · Store after prepending to a singly linked list · Prepending makes the node the head · The prepended node points at the old head · Prepending conses onto the represented list · Store representing a singly linked list · Represented identities hold nodes · Represented lists have no missing contents · Represented lists fit in the store · Representation of the empty singly linked list · Search in a singly-linked list · Fuel-bounded search in a singly-linked list · Fuel-bounded search finds the first matching represented identity · Search finds the first matching represented identity · Search fails exactly when no represented node has the target payload · A successful search returns a matching represented identity

DefinitionStore representing a singly linked list#✓fully proved

Fix a capacity \(n\), let a store assign to each identity below \(n\) either nothing or a singly linked list node whose next pointer is an identity 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 next pointer is \(i_{j+1}\) if \(j + 1 < k\) and NIL otherwise.

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.next = ids[i + 1]?

Uses 1 · Used by 12

Statement usesSingly linked list node

Used byDeleting a successor removes it from the represented list · Deleting the head removes the first identity · Insertion into a represented singly linked list · Prepending conses onto the represented list · Represented identities hold nodes · Represented lists have no missing contents · Represented lists fit in the store · Representation of the empty singly linked list · Fuel-bounded search finds the first matching represented identity · Search finds the first matching represented identity · Search fails exactly when no represented node has the target payload · A successful search returns a matching represented identity

TheoremRepresentation of the empty singly linked list#✓fully proved

Fix a capacity \(n\) and let \(s\) be any store assigning to each identity below \(n\) either nothing or a singly linked list node. Then \(s\) with head NIL represents the empty list of identities.

theorem represents_nil {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity) :
    Represents store none ([] : List (Fin capacity))

Uses 2 · Used by 1

Statement usesSingly linked list node · Store representing a singly linked list

Used byDeleting the head removes the first identity

TheoremRepresented identities hold nodes#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, and let \(\mathrm{head}\) be an identity below \(n\) or NIL. If \(s\) and \(\mathrm{head}\) represent the list of identities \(i_0, \dots, i_{k-1}\), then for every identity \(i\) in this list the store entry \(s(i)\) is a node.

theorem represents_allocated {α : Type u} {capacity : Nat}
    {store : Vector (Option (Node α (Fin capacity))) capacity}
    {head : Option (Fin capacity)} {ids : List (Fin capacity)}
    (rep : Represents store head ids) {i : Fin capacity} (hi : i ∈ ids) :
    (store.get i).isSome

Uses 2 · Used by 1

Statement usesSingly linked list node · Store representing a singly linked list

Used byRepresented lists have no missing contents

DefinitionPayload list of a singly linked list store#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node (a payload together with a next pointer that is an identity below \(n\) or NIL). For a list of identities \(i_0, \dots, i_{m-1}\) below \(n\), the contents of \(s\) at this list are the list \(c_0, \dots, c_{m-1}\), where \(c_j\) is the payload of \(s(i_j)\) when \(s(i_j)\) is a node and \(c_j\) is nothing (marking an unallocated cell) when \(s(i_j)\) is nothing.

def contents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (ids : List (Fin capacity)) : List (Option α) :=
  ids.map fun i => (store.get i).map Node.payload

Uses 1 · Used by 6

Statement usesSingly linked list node

Used byThe payload list depends only on the listed cells · The payload list has one entry per identity · Contents after deleting a successor · Contents after singly-linked-list insertion · Contents after prepending to a singly linked list · Represented lists have no missing contents

TheoremThe payload list has one entry per identity#✓fully proved

Fix a capacity \(n\) and let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node. For every list \(L\) of identities below \(n\), the contents of \(s\) at \(L\) have the same length as \(L\).

@[simp]
theorem contents_length {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (ids : List (Fin capacity)) :
    (contents store ids).length = ids.length

Uses 2

Statement usesSingly linked list node · Payload list of a singly linked list store

TheoremThe payload list depends only on the listed cells#✓fully proved

Fix a capacity \(n\) and let \(s\) and \(s'\) be stores assigning to each identity below \(n\) either nothing or a singly linked list node. If \(L\) is a list of identities below \(n\) and \(s'(i) = s(i)\) for every \(i\) in \(L\), then the contents of \(s'\) at \(L\) equal the contents of \(s\) at \(L\).

theorem contents_congr {α : Type u} {capacity : Nat}
    {store store' : Vector (Option (Node α (Fin capacity))) capacity}
    {ids : List (Fin capacity)}
    (h : ∀ i ∈ ids, store'.get i = store.get i) :
    contents store' ids = contents store ids

Uses 2 · Used by 1

Statement usesSingly linked list node · Payload list of a singly linked list store

Used byContents after prepending to a singly linked list

TheoremRepresented lists have no missing contents#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, and let \(\mathrm{head}\) be an identity below \(n\) or NIL. If \(s\) and \(\mathrm{head}\) represent the list of identities \(i_0, \dots, i_{k-1}\), then every entry of the contents of \(s\) at \(i_0, \dots, i_{k-1}\) is a payload rather than nothing.

theorem represents_contents_isSome {α : Type u} {capacity : Nat}
    {store : Vector (Option (Node α (Fin capacity))) capacity}
    {head : Option (Fin capacity)} {ids : List (Fin capacity)}
    (rep : Represents store head ids) :
    ∀ x ∈ contents store ids, x.isSome = true

Uses 4

Statement usesSingly linked list node · Store representing a singly linked list · Payload list of a singly linked list store

Proof usesRepresented identities hold nodes

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

Fix a capacity \(n\), let a store assign to each identity below \(n\) either nothing or a singly 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. Prepending \(x\) replaces the store entry at \(x\) by the same node with its next pointer set to the head, leaves every other entry unchanged, and returns the updated store together with the new head \(x\).

def prepend {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome) :
    Vector (Option (Node α (Fin capacity))) capacity × Option (Fin capacity) :=
  (store.set x.val (some { (store.get x).get hx with next := head }) x.isLt, some x)

Uses 1 · Used by 6

Statement usesSingly linked list node

Used byContents after prepending to a singly linked list · Frame property of prepending to a singly linked list · Store after prepending to a singly linked list · Prepending makes the node the head · The prepended node points at the old head · Prepending conses onto the represented list

TheoremPrepending makes the node the head#✓fully proved

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

theorem prepend_head {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome) :
    (prepend store head x hx).2 = some x

Uses 2 · Used by 1

Statement usesSingly linked list node · Prepending a node to a singly linked list

Used byPrepending conses onto the represented list

TheoremStore after prepending to a singly linked list#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(\mathrm{head}\) be an identity below \(n\) or NIL, and let \(x\) be an identity such that \(s(x)\) is a node. Then for every identity \(z\) below \(n\), the entry at \(z\) of the store returned by Prepend on \(s\), \(\mathrm{head}\) and \(x\) is the node \(s(x)\) with its next pointer replaced by \(\mathrm{head}\) when \(z = x\), and is \(s(z)\) when \(z \ne x\).

theorem prepend_get {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome) (z : Fin capacity) :
    (prepend store head x hx).1.get z =
      if x = z then some { (store.get x).get hx with next := head } else store.get z

Uses 2 · Used by 2

Statement usesSingly linked list node · Prepending a node to a singly linked list

Used byFrame property of prepending to a singly linked list · The prepended node points at the old head

TheoremFrame property of prepending to a singly linked list#✓fully proved

Let \(S\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(h\) be an identity below \(n\) or NIL, and let \(x\) be an identity whose store entry is a node. For every identity \(z \ne x\), cell \(z\) of the store obtained by prepending \(x\) to the list with head \(h\) equals cell \(z\) of \(S\).

theorem prepend_frame {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome) (z : Fin capacity) (hz : x ≠ z) :
    (prepend store head x hx).1.get z = store.get z

Uses 3 · Used by 2

Statement usesSingly linked list node · Prepending a node to a singly linked list

Proof usesStore after prepending to a singly linked list

Used byContents after prepending to a singly linked list · Prepending conses onto the represented list

TheoremThe prepended node points at the old head#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(\mathrm{head}\) be an identity below \(n\) or NIL, and let \(x\) be an identity such that \(s(x)\) is a node. Then the entry at \(x\) of the store returned by Prepend on \(s\), \(\mathrm{head}\) and \(x\) is the node \(s(x)\) with its payload kept and its next pointer replaced by \(\mathrm{head}\).

theorem prepend_node {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome) :
    (prepend store head x hx).1.get x =
      some { (store.get x).get hx with next := head }

Uses 3 · Used by 2

Statement usesSingly linked list node · Prepending a node to a singly linked list

Proof usesStore after prepending to a singly linked list

Used byContents after prepending to a singly linked list · Prepending conses onto the represented list

TheoremPrepending conses onto the represented list#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(\mathrm{head}\) be an identity below \(n\) or NIL, and let \(x\) be an identity such that \(s(x)\) is a node. If \(s\) and \(\mathrm{head}\) represent the list of identities \(i_0, \dots, i_{k-1}\) and \(x\) is none of \(i_0, \dots, i_{k-1}\), then the store and head returned by Prepend on \(s\), \(\mathrm{head}\) and \(x\) represent the list \(x, i_0, \dots, i_{k-1}\).

theorem prepend_represents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (ids : List (Fin capacity)) (rep : Represents store head ids) (fresh : x ∉ ids) :
    Represents (prepend store head x hx).1 (prepend store head x hx).2 (x :: ids)

Uses 6

Statement usesSingly linked list node · Store representing a singly linked list · Prepending a node to a singly linked list

Proof usesFrame property of prepending to a singly linked list · Prepending makes the node the head · The prepended node points at the old head

TheoremContents after prepending to a singly linked list#✓fully proved

Let \(S\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(h\) be an identity below \(n\) or NIL, let \(x\) be an identity whose store entry is a node with payload \(a\), and let \((i_0, \dots, i_{m-1})\) be a list of identities below \(n\) not containing \(x\). Then the contents, at the list \((x, i_0, \dots, i_{m-1})\), of the store obtained by prepending \(x\) to the list with head \(h\) are the present payload \(a\) followed by the contents of \(S\) at the list \((i_0, \dots, i_{m-1})\).

theorem prepend_contents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (x : Fin capacity)
    (hx : (store.get x).isSome)
    (ids : List (Fin capacity)) (fresh : x ∉ ids) :
    contents (prepend store head x hx).1 (x :: ids) =
      some ((store.get x).get hx).payload :: contents store ids

Uses 6

Statement usesSingly linked list node · Payload list of a singly linked list store · Prepending a node to a singly linked list

Proof usesThe payload list depends only on the listed cells · Frame property of prepending to a singly linked list · The prepended node points at the old head

DefinitionInserting a node after another in a singly linked list#✓fully proved

Let a store \(S\) assign to each identity below \(n\) either nothing or a singly linked list node whose next pointer is an identity below \(n\) or NIL, and let \(x\) and \(y\) be identities whose store entries are nodes. Inserting \(x\) after \(y\) first replaces cell \(x\) by the node of \(x\) with next pointer replaced by the next pointer of \(y\) in \(S\), then, in the store so obtained, replaces the next pointer of the node in cell \(y\) by \(x\), and returns the resulting store.

def insertAfter {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (y x : Fin capacity)
    (hy : (store.get y).isSome) (hx : (store.get x).isSome) :
    Vector (Option (Node α (Fin capacity))) capacity :=
  let store₁ := store.set x.val
    (some { (store.get x).get hx with next := ((store.get y).get hy).next }) x.isLt
  store₁.set y.val ((store₁.get y).map fun node => { node with next := some x }) y.isLt

Uses 1 · Used by 5

Statement usesSingly linked list node

Used byContents after singly-linked-list insertion · Frame property of singly-linked-list insertion · Cells after singly-linked-list insertion · Singly-linked-list insertion preserves payloads · Insertion into a represented singly linked list

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

Let \(S\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(x\) and \(y\) be identities whose store entries are nodes, and let \(z\) be any identity. Let \(c\) be the node of \(x\) in \(S\) with next pointer replaced by the next pointer of \(y\) in \(S\) if \(z = x\), and the content of cell \(z\) in \(S\) otherwise. Then cell \(z\) of the store obtained by inserting \(x\) after \(y\) is \(c\) with next pointer replaced by \(x\) if \(z = y\), and \(c\) otherwise.

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

theorem insertAfter_get {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (y x : Fin capacity)
    (hy : (store.get y).isSome) (hx : (store.get x).isSome) (z : Fin capacity) :
    (insertAfter store y x hy hx).get z =
      if y = z then
        (if x = z then
          some { (store.get x).get hx with next := ((store.get y).get hy).next }
        else store.get z).map (fun node => { node with next := some x })
      else if x = z then
        some { (store.get x).get hx with next := ((store.get y).get hy).next }
      else store.get z

Uses 2 · Used by 3

Statement usesSingly linked list node · Inserting a node after another in a singly linked list

Used byFrame property of singly-linked-list insertion · Singly-linked-list insertion preserves payloads · Insertion into a represented singly linked list

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

Let \(S\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, and let \(x\) and \(y\) be identities whose store entries are nodes. For every identity \(z\) with \(z \ne y\) and \(z \ne x\), cell \(z\) of the store obtained by inserting \(x\) after \(y\) equals cell \(z\) of \(S\).

theorem insertAfter_frame {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (y x : Fin capacity)
    (hy : (store.get y).isSome) (hx : (store.get x).isSome) (z : Fin capacity)
    (hyz : y ≠ z) (hxz : x ≠ z) :
    (insertAfter store y x hy hx).get z = store.get z

Uses 3

Statement usesSingly linked list node · Inserting a node after another in a singly linked list

Proof usesCells after singly-linked-list insertion

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

Let \(S\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, and let \(x\) and \(y\) be identities whose store entries are nodes. For every identity \(z\), cell \(z\) of the store obtained 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\).

theorem insertAfter_payload {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (y x : Fin capacity)
    (hy : (store.get y).isSome) (hx : (store.get x).isSome) (z : Fin capacity) :
    ((insertAfter store y x hy hx).get z).map Node.payload =
      (store.get z).map Node.payload

Uses 3 · Used by 1

Statement usesSingly linked list node · Inserting a node after another in a singly linked list

Proof usesCells after singly-linked-list insertion

Used byContents after singly-linked-list insertion

TheoremInsertion into a represented singly linked list#✓fully proved

Suppose the store \(S\) with head \(h\) represents the list of distinct identities \((i_0, \dots, i_{m-1})\). Let \(k < m\), assume that the store entry of \(i_k\) is a node, and let \(x\) be an identity whose store entry is a node and which is not among \(i_0, \dots, i_{m-1}\). Then the store obtained 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})\).

theorem insertAfter_represents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity) (x : Fin capacity)
    (head : Option (Fin capacity)) (ids : List (Fin capacity))
    (rep : Represents store head ids) (fresh : x ∉ ids)
    (k : Nat) (hk : k < ids.length)
    (hy : (store.get ids[k]).isSome) (hx : (store.get x).isSome) :
    Represents (insertAfter store ids[k] x hy hx) head (ids.insertIdx (k + 1) x)

Uses 4

Statement usesSingly linked list node · Store representing a singly linked list · Inserting a node after another in a singly linked list

Proof usesCells after singly-linked-list insertion

TheoremContents after singly-linked-list insertion#✓fully proved

Let \(S\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \((i_0, \dots, i_{m-1})\) be a list of identities below \(n\), let \(k < m\), and let \(x\) be an identity such that the store entries of \(x\) and \(i_k\) are nodes, the node of \(x\) having payload \(a\). Then the contents of the store obtained by inserting \(x\) after \(i_k\) at the list \((i_0, \dots, i_k, x, i_{k+1}, \dots, i_{m-1})\) equal the contents of \(S\) at \((i_0, \dots, i_{m-1})\) with the present payload \(a\) inserted as entry \(k + 1\) (counting from \(0\)).

No representation or distinctness hypothesis is assumed.

theorem insertAfter_contents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity) (x : Fin capacity)
    (ids : List (Fin capacity)) (k : Nat) (hk : k < ids.length)
    (hy : (store.get ids[k]).isSome) (hx : (store.get x).isSome) :
    contents (insertAfter store ids[k] x hy hx) (ids.insertIdx (k + 1) x) =
      (contents store ids).insertIdx (k + 1) (some ((store.get x).get hx).payload)

Uses 4

Statement usesSingly linked list node · Payload list of a singly linked list store · Inserting a node after another in a singly linked list

Proof usesSingly-linked-list insertion preserves payloads

DefinitionDeleting the head of a singly linked list#✓fully proved

Let a store assign to each identity below \(n\) either nothing or a singly linked list node whose next pointer is an identity below \(n\) or NIL, and let the head be an identity below \(n\) or NIL. Deleting the head returns the store unchanged together with a new head: NIL if the head is NIL or the store entry at the head is empty, and otherwise the next pointer of the node stored at the head.

def deleteHead {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) :
    Vector (Option (Node α (Fin capacity))) capacity × Option (Fin capacity) :=
  (store, head.bind fun h => (store.get h).bind fun node => node.next)

Uses 1 · Used by 1

Statement usesSingly linked list node

Used byDeleting the head removes the first identity

TheoremDeleting the head removes the first identity#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, and suppose that \(s\) with head \(h\) represents the list of identities \(L\), where \(h\) is an identity below \(n\) or NIL. Let \((s', h')\) be the store and head returned by deleting the head of \(s\) with head \(h\). Then \(s'\) with head \(h'\) represents \(L\) with its first entry removed, which is the empty list when \(L\) is empty.

theorem deleteHead_represents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (ids : List (Fin capacity))
    (rep : Represents store head ids) :
    Represents (deleteHead store head).1 (deleteHead store head).2 ids.tail

Uses 4

Statement usesSingly linked list node · Store representing a singly linked list · Deleting the head of a singly linked list

Proof usesRepresentation of the empty singly linked list

DefinitionDeleting the successor in a singly linked list#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node whose next pointer is an identity below \(n\) or NIL, and let \(y\) be an identity such that \(s(y)\) is a node. Deleting after \(y\) returns the store that agrees with \(s\) except at \(y\), where it holds the node \(s(y)\) with its next pointer replaced as follows: if the next pointer of \(s(y)\) is an identity \(m\) and \(s(m)\) is a node, the new next pointer is the next pointer of \(s(m)\); otherwise it is NIL.

The removed node stays allocated in the store; at the tail the links are unchanged.

def deleteAfter {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (y : Fin capacity) (hy : (store.get y).isSome) :
    Vector (Option (Node α (Fin capacity))) capacity :=
  store.set y.val (some { (store.get y).get hy with
    next := ((store.get y).get hy).next.bind
      fun n => (store.get n).bind fun node => node.next }) y.isLt

Uses 1 · Used by 5

Statement usesSingly linked list node

Used byContents after deleting a successor · Deleting a successor leaves other cells unchanged · Cells after deleting a successor · Deleting a successor preserves payloads · Deleting a successor removes it from the represented list

TheoremCells after deleting a successor#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(y\) be an identity such that \(s(y)\) is a node, and let \(s'\) be the store obtained from \(s\) by deleting the successor of \(y\). Let \(c\) be the node \(s(y)\) with its next pointer replaced by the next pointer of \(s(m)\) if the next pointer of \(s(y)\) is an identity \(m\) such that \(s(m)\) is a node, and by NIL otherwise. Then for every identity \(z\), \(s'(z)\) is the node \(c\) if \(z = y\), and \(s'(z) = s(z)\) if \(z \ne y\).

theorem deleteAfter_get {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (y : Fin capacity) (hy : (store.get y).isSome) (z : Fin capacity) :
    (deleteAfter store y hy).get z =
      if y = z then
        some { (store.get y).get hy with
          next := ((store.get y).get hy).next.bind
            fun n => (store.get n).bind fun node => node.next }
      else store.get z

Uses 2 · Used by 3

Statement usesSingly linked list node · Deleting the successor in a singly linked list

Used byDeleting a successor leaves other cells unchanged · Deleting a successor preserves payloads · Deleting a successor removes it from the represented list

TheoremDeleting a successor leaves other cells unchanged#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(y\) be an identity such that \(s(y)\) is a node, and let \(s'\) be the store obtained from \(s\) by deleting the successor of \(y\). Then \(s'(z) = s(z)\) for every identity \(z \ne y\).

theorem deleteAfter_frame {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (y : Fin capacity) (hy : (store.get y).isSome) (z : Fin capacity)
    (hyz : y ≠ z) :
    (deleteAfter store y hy).get z = store.get z

Uses 3 · Used by 1

Statement usesSingly linked list node · Deleting the successor in a singly linked list

Proof usesCells after deleting a successor

Used byDeleting a successor removes it from the represented list

TheoremDeleting a successor preserves payloads#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(y\) be an identity such that \(s(y)\) is a node, and let \(s'\) be the store obtained from \(s\) by deleting the successor of \(y\). Then for every identity \(z\), either \(s(z)\) and \(s'(z)\) are both nothing, or both are nodes with the same payload.

theorem deleteAfter_payload {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (y : Fin capacity) (hy : (store.get y).isSome) (z : Fin capacity) :
    ((deleteAfter store y hy).get z).map Node.payload =
      (store.get z).map Node.payload

Uses 3 · Used by 1

Statement usesSingly linked list node · Deleting the successor in a singly linked list

Proof usesCells after deleting a successor

Used byContents after deleting a successor

TheoremDeleting a successor removes it from the represented list#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, and suppose that \(s\) with head \(h\) represents the list of identities \(L = (i_0, \dots, i_{m-1})\). Let \(k < m\) be such that \(s(i_k)\) is a node, and let \(s'\) be the store obtained from \(s\) by deleting the successor of \(i_k\). Then \(s'\) with the same head \(h\) represents the list obtained from \(L\) by removing the entry at position \(k + 1\). Positions count from \(0\), and at the tail (\(k + 1 = m\)) the list is unchanged.

theorem deleteAfter_represents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (ids : List (Fin capacity))
    (rep : Represents store head ids) (k : Nat) (hk : k < ids.length)
    (hy : (store.get ids[k]).isSome) :
    Represents (deleteAfter store ids[k] hy) head (ids.eraseIdx (k + 1))

Uses 5

Statement usesSingly linked list node · Store representing a singly linked list · Deleting the successor in a singly linked list

Proof usesDeleting a successor leaves other cells unchanged · Cells after deleting a successor

TheoremContents after deleting a successor#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, let \(L = (i_0, \dots, i_{m-1})\) be a list of identities below \(n\), and let \(k < m\) be such that \(s(i_k)\) is a node. Let \(s'\) be the store obtained from \(s\) by deleting the successor of \(i_k\). Then the contents of \(s'\) at the list obtained from \(L\) by removing the entry at position \(k + 1\) equal the list obtained from the contents of \(s\) at \(L\) by removing the entry at position \(k + 1\). Positions count from \(0\), and nothing is removed when \(k + 1 = m\).

theorem deleteAfter_contents {α : Type u} {capacity : Nat}
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (ids : List (Fin capacity)) (k : Nat) (hk : k < ids.length)
    (hy : (store.get ids[k]).isSome) :
    contents (deleteAfter store ids[k] hy) (ids.eraseIdx (k + 1)) =
      (contents store ids).eraseIdx (k + 1)

Uses 4

Statement usesSingly linked list node · Payload list of a singly linked list store · Deleting the successor in a singly linked list

Proof usesDeleting a successor preserves payloads

DefinitionFuel-bounded search in a singly-linked list#✓fully proved

Given a node pool with \(n\) cells, a target payload \(t\), a fuel \(f \in \mathbb{N}\) and a start \(h\) that is either an identity in \(\{0, \dots, n-1\}\) or NIL, fuel-bounded search for \(t\) from \(h\) with fuel \(f\) returns nothing if \(f = 0\) or \(h\) is NIL. Otherwise \(h\) is an identity \(i\): the search returns nothing if cell \(i\) is unallocated, returns \(i\) if the node in cell \(i\) has payload \(t\), and otherwise continues from the next pointer of that node with fuel \(f - 1\).

def searchAux {α : Type u} {capacity : Nat} [DecidableEq α]
    (store : Vector (Option (Node α (Fin capacity))) capacity) (target : α) :
    Nat → Option (Fin capacity) → Option (Fin capacity)
  | 0, _ => none
  | _ + 1, none => none
  | fuel + 1, some i =>
    match store.get i with
    | none => none
    | some node =>
      if node.payload = target then some i
      else searchAux store target fuel node.next

Uses 1 · Used by 2

Statement usesSingly linked list node

Used bySearch in a singly-linked list · Fuel-bounded search finds the first matching represented identity

DefinitionSearch in a singly-linked list#✓fully proved

Given a node pool with \(n\) cells, a head \(h\) that is either an identity in \(\{0, \dots, n-1\}\) or NIL, and a target payload \(t\), the search for \(t\) from \(h\) is fuel-bounded search for \(t\) from \(h\) with fuel \(n\). It follows next pointers from \(h\) and returns the first visited identity whose node has payload \(t\), returning nothing if it reaches NIL or an unallocated cell first, or if \(n\) steps run out.

def search {α : Type u} {capacity : Nat} [DecidableEq α]
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (target : α) : Option (Fin capacity) :=
  searchAux store target capacity head

Uses 2 · Used by 3

Statement usesSingly linked list node · Fuel-bounded search in a singly-linked list

Used bySearch finds the first matching represented identity · Search fails exactly when no represented node has the target payload · A successful search returns a matching represented identity

TheoremFuel-bounded search finds the first matching represented identity#✓fully proved

Suppose a node pool represents, from the head \(h\), the list of distinct identities \(\ell\). Then for every target payload \(t\) and every fuel \(f\) with \(f \ge |\ell|\), fuel-bounded search for \(t\) from \(h\) with fuel \(f\) returns the first identity in \(\ell\) whose cell holds a node with payload \(t\), and returns nothing if no identity in \(\ell\) has this property.

theorem searchAux_eq_find? {α : Type u} {capacity : Nat} [DecidableEq α]
    (store : Vector (Option (Node α (Fin capacity))) capacity) (target : α)
    (fuel : Nat) (head : Option (Fin capacity)) (ids : List (Fin capacity))
    (rep : Represents store head ids) (hlen : ids.length ≤ fuel) :
    searchAux store target fuel head =
      ids.find? (fun i => decide ((store.get i).map Node.payload = some target))

Uses 3 · Used by 1

Statement usesSingly linked list node · Store representing a singly linked list · Fuel-bounded search in a singly-linked list

Used bySearch finds the first matching represented identity

TheoremRepresented lists fit in the store#✓fully proved

Fix a capacity \(n\), let \(s\) be a store assigning to each identity below \(n\) either nothing or a singly linked list node, and let \(\mathrm{head}\) be an identity below \(n\) or NIL. If \(s\) and \(\mathrm{head}\) represent the list of identities \(i_0, \dots, i_{k-1}\), then \(k \le n\).

The identities are pairwise distinct and there are only \(n\) of them.

theorem represents_length_le_capacity {α : Type u} {capacity : Nat}
    {store : Vector (Option (Node α (Fin capacity))) capacity}
    {head : Option (Fin capacity)} {ids : List (Fin capacity)}
    (rep : Represents store head ids) :
    ids.length ≤ capacity

Uses 2 · Used by 1

Statement usesSingly linked list node · Store representing a singly linked list

Used bySearch finds the first matching represented identity

TheoremSearch finds the first matching represented identity#✓fully proved

If a node pool represents, from the head \(h\), the list of distinct identities \(\ell\), then for every target payload \(t\) the search for \(t\) from \(h\) returns the first identity in \(\ell\) whose cell holds a node with payload \(t\), and returns nothing if no identity in \(\ell\) has this property.

theorem search_eq_find? {α : Type u} {capacity : Nat} [DecidableEq α]
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (target : α) (ids : List (Fin capacity))
    (rep : Represents store head ids) :
    search store head target =
      ids.find? (fun i => decide ((store.get i).map Node.payload = some target))

Uses 5 · Used by 2

Statement usesSingly linked list node · Store representing a singly linked list · Search in a singly-linked list

Proof usesRepresented lists fit in the store · Fuel-bounded search finds the first matching represented identity

Used bySearch fails exactly when no represented node has the target payload · A successful search returns a matching represented identity

TheoremA successful search returns a matching represented identity#✓fully proved

If a node pool represents, from the head \(h\), the list of distinct identities \(\ell\), and the search for a target payload \(t\) from \(h\) returns an identity \(x\), then \(x\) belongs to \(\ell\) and cell \(x\) holds a node with payload \(t\).

theorem search_eq_some {α : Type u} {capacity : Nat} [DecidableEq α]
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (target : α) (ids : List (Fin capacity))
    (rep : Represents store head ids)
    {x : Fin capacity} (h : search store head target = some x) :
    x ∈ ids ∧ (store.get x).map Node.payload = some target

Uses 4

Statement usesSingly linked list node · Store representing a singly linked list · Search in a singly-linked list

Proof usesSearch finds the first matching represented identity

TheoremSearch fails exactly when no represented node has the target payload#✓fully proved

If a node pool represents, from the head \(h\), the list of distinct identities \(\ell\), then for every target payload \(t\) the search for \(t\) from \(h\) returns nothing if and only if no identity in \(\ell\) has a cell holding a node with payload \(t\).

theorem search_eq_none_iff {α : Type u} {capacity : Nat} [DecidableEq α]
    (store : Vector (Option (Node α (Fin capacity))) capacity)
    (head : Option (Fin capacity)) (target : α) (ids : List (Fin capacity))
    (rep : Represents store head ids) :
    search store head target = none ↔
      ∀ i ∈ ids, (store.get i).map Node.payload ≠ some target

Uses 4

Statement usesSingly linked list node · Store representing a singly linked list · Search in a singly-linked list

Proof usesSearch finds the first matching represented identity

36 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.