The witness encoding respects concatenation to Length of an encoded PATH instance

TheoremThe witness encoding respects concatenation#✓fully proved

For lists \(p\) and \(p'\) of natural numbers, the witness encoding of the concatenation of \(p\) and \(p'\) is the witness encoding of \(p\) followed by the witness encoding of \(p'\).

theorem encW_append (p p' : List ℕ) : encW (p ++ p') = encW p ++ encW p'

Uses 1 · Used by 1

Statement usesWitness encoding

Used byThe repeat scan of the Hamiltonian path verifier

TheoremDecoding the empty witness#✓fully proved

The witness decoder succeeds on the empty list of bits and returns the empty list of vertices.

theorem decodeW_nil : decodeW [] = some []

Uses 3 · Used by 3

Statement usesWitness decoder

Proof usesReading a unary number shortens the input · Reading a unary length prefix

Used byDecoding inverts the witness encoding · The witness decoder succeeds only on encodings · The witness check of the Hamiltonian-path verifier

TheoremWitness decoding fails on a cut-off first number#✓fully proved

If a list \(w\) of bits is nonempty and reading a unary number (a run of true ended by false) from the front of \(w\) fails, that is, every bit of \(w\) is true, then the witness decoder fails on \(w\).

theorem decodeW_of_none {w : List Bool} (hw : w ≠ []) (h : readUnaryLength w = none) :
    decodeW w = none

Uses 3 · Used by 2

Statement usesWitness decoder · Reading a unary length prefix

Proof usesReading a unary number shortens the input

Used byThe witness decoder succeeds only on encodings · The witness check of the Hamiltonian-path verifier

TheoremDecoding peels off the first number#✓fully proved

If reading a unary number from the front of a list \(w\) of bits returns \(v\) with remaining bits \(r\), that is, \(w\) is \(v\) copies of true, then false, then \(r\), then the witness decoder succeeds on \(w\) exactly when it succeeds on \(r\), and its result on \(w\) is \(v\) followed by its result on \(r\).

theorem decodeW_of_some {w r : List Bool} {v : ℕ} (h : readUnaryLength w = some (v, r)) :
    decodeW w = (decodeW r).map (v :: ·)

Uses 3 · Used by 3

Statement usesWitness decoder · Reading a unary length prefix

Proof usesReading a unary number shortens the input

Used byDecoding inverts the witness encoding · The witness decoder succeeds only on encodings · The witness check of the Hamiltonian-path verifier

TheoremDecoding inverts the witness encoding#✓fully proved

For every list \(p\) of natural numbers, the witness decoder applied to the witness encoding of \(p\) (each entry \(v\) written as \(v\) copies of true followed by false) succeeds and returns \(p\).

theorem decodeW_encW : ∀ p, decodeW (encW p) = some p

Uses 6 · Used by 3

Statement usesWitness decoder · Witness encoding

Proof usesDecoding the empty witness · Decoding peels off the first number · Witness encoding of a nonempty list · Reading a unary length prefix

Used byThe witness codec · The verifier on an encoded instance and witness · What the HAMPATH verifier accepts

TheoremThe witness decoder succeeds only on encodings#✓fully proved

For every bit string \(w\) and every list \(p\) of natural numbers, if the witness decoder returns \(p\) on \(w\), then \(w\) is the witness encoding of \(p\).

theorem encW_of_decodeW : ∀ {p : List ℕ} {w : List Bool}, decodeW w = some p → encW p = w

Uses 7 · Used by 2

Statement usesWitness decoder · Witness encoding

Proof usesDecoding the empty witness · Witness decoding fails on a cut-off first number · Decoding peels off the first number · Witness encoding of a nonempty list · Reading a unary length prefix

Used byThe witness codec · Correctness and running time of the Hamiltonian path verifier

TheoremThe witness codec#✓fully proved

For every list \(w\) of bits and every list \(p\) of natural numbers, the witness decoder returns \(p\) on \(w\) if and only if \(w\) is the witness encoding of \(p\), which writes each entry \(v\) of \(p\) as \(v\) copies of true followed by false.

theorem decodeW_eq_some {w : List Bool} {p : List ℕ} : decodeW w = some p ↔ encW p = w

Uses 4 · Used by 1

Statement usesWitness decoder · Witness encoding

Proof usesDecoding inverts the witness encoding · The witness decoder succeeds only on encodings

Used byWhat the HAMPATH verifier accepts

TheoremWitness length#✓fully proved

For every list \(p = (v_1, \dots, v_k)\) of natural numbers, the witness encoding of \(p\) has length \(\sum_{i=1}^{k} (v_i + 1)\).

theorem length_encW (p : List ℕ) : (encW p).length = (p.map (· + 1)).sum

Uses 2 · Used by 1

Statement usesWitness encoding

Proof usesWitness encoding of a nonempty list

Used byA witness is at least as long as its vertex list

TheoremWitness length bound#✓fully proved

For every natural number \(n\) and every list \(p\) of natural numbers all below \(n\), the witness encoding of \(p\) has length at most \(|p| \cdot n\).

theorem length_encW_le {n : ℕ} : ∀ {p : List ℕ}, (∀ v ∈ p, v < n) →
    (encW p).length ≤ p.length * n

Uses 2 · Used by 1

Statement usesWitness encoding

Proof usesWitness encoding of a nonempty list

Used byHAMPATH is verified with quadratic-size witnesses

TheoremA witness is at least as long as its vertex list#✓fully proved

For every list \(p\) of natural numbers, the witness encoding of \(p\) has length at least \(|p|\).

theorem length_le_length_encW (p : List ℕ) : p.length ≤ (encW p).length

Uses 2 · Used by 1

Statement usesWitness encoding

Proof usesWitness length

Used byCorrectness and running time of the Hamiltonian path verifier

DefinitionArc check of a vertex list#✓fully proved

Given \(n \in \mathbb{N}\) and a list \(E\) of pairs of natural numbers, the arc check of a list \(p\) of natural numbers returns true when every two consecutive entries \(u, v\) of \(p\) satisfy \((u, v) \in E\), \(u < n\) and \(v < n\), and false otherwise; in particular every list with fewer than two entries passes.

def chainOk (n : ℕ) (es : List (ℕ × ℕ)) : List ℕ → Bool
  | u :: v :: p => decide ((u, v) ∈ es ∧ u < n ∧ v < n) && chainOk n es (v :: p)
  | _ => true

Used by 4

Used byChecking a vertex list against the arcs · The Hamiltonian path check · The Hamiltonian path check is correct · The machine's walk is the check

TheoremChecking a vertex list against the arcs#✓fully proved

For every \(n \in \mathbb{N}\), every list \(E\) of pairs of natural numbers and every list \(p\) of natural numbers, the arc check of \(p\) against \(n\) and \(E\) returns true if and only if every two consecutive entries \(u, v\) of \(p\) form an arc of the digraph on \(0, \dots, n - 1\) listed by \(E\), that is, \((u, v) \in E\), \(u < n\) and \(v < n\).

theorem chainOk_iff (n : ℕ) (es : List (ℕ × ℕ)) :
    ∀ p, chainOk n es p = true ↔ p.IsChain (Path.arc n es)

Uses 2 · Used by 1

Statement usesArc check of a vertex list · Arcs of the PATH digraph

Used byThe Hamiltonian path check is correct

DefinitionThe Hamiltonian path check#✓fully proved

Given a natural number \(n\), an edge list \(E\), vertices \(s\) and \(t\) and a list \(p\) of natural numbers, the Boolean test that \(p\) has no repeated entries, has length \(n\), has all entries below \(n\), has first entry \(s\) and last entry \(t\), and that every two consecutive entries \(u, v\) of \(p\) satisfy \((u, v) \in E\), \(u < n\) and \(v < n\).

def hamOk (n : ℕ) (es : List (ℕ × ℕ)) (s t : ℕ) (p : List ℕ) : Bool :=
  decide p.Nodup && p.length == n && p.all (· < n) && p.head? == some s &&
    p.getLast? == some t && chainOk n es p

Uses 1 · Used by 8

Statement usesArc check of a vertex list

Used byThe HAMPATH verifier · The verifier on an encoded instance and witness · What the HAMPATH verifier accepts · Instances that do not decode are rejected · Witnesses that do not decode are rejected · The Hamiltonian path check is correct · The machine's walk is the check · Correctness and running time of the Hamiltonian path verifier

TheoremThe Hamiltonian path check is correct#✓fully proved

For all natural numbers \(n\), \(s\), \(t\), every edge list \(E\) and every list \(p\) of natural numbers, the Hamiltonian path check on \((n, E, s, t, p)\) returns true if and only if \(p\) is a Hamiltonian path from \(s\) to \(t\) in the digraph on \(\{0, \dots, n-1\}\) with edge list \(E\).

theorem hamOk_iff {n : ℕ} {es : List (ℕ × ℕ)} {s t : ℕ} {p : List ℕ} :
    hamOk n es s t p = true ↔ IsHamPath n es s t p

Uses 5 · Used by 2

Statement usesThe Hamiltonian path check · Hamiltonian paths

Proof usesArc check of a vertex list · Checking a vertex list against the arcs · Arcs of the PATH digraph

Used byWhat the HAMPATH verifier accepts · The machine's walk is the check

DefinitionThe HAMPATH verifier#✓fully proved

Given bit strings \(x\) and \(w\), the verifier decodes \(x\) as a PATH instance, consisting of a start vertex \(s\), a target vertex \(t\), a vertex count \(n\) and an edge list \(E\), and decodes \(w\) as a witness, a list \(p\) of natural numbers each written in unary. If both decodings succeed, it accepts exactly when the Hamiltonian path check passes, that is, when \(p\) is a Hamiltonian path from \(s\) to \(t\) in the digraph on \(\{0, \dots, n-1\}\) with edge list \(E\). If either decoding fails, it rejects.

def hamCheck (x w : List Bool) : Bool :=
  match Path.decodeP x, decodeW w with
  | some (s, t, n, es), some p => hamOk n es s t p
  | _, _ => false

Uses 3 · Used by 7

Statement usesWitness decoder · The Hamiltonian path check · Decoding a PATH instance

Used byThe verifier on an encoded instance and witness · What the HAMPATH verifier accepts · Instances that do not decode are rejected · Witnesses that do not decode are rejected · HAMPATH is verified with quadratic-size witnesses · HAMPATH is in NP · Correctness and running time of the Hamiltonian path verifier

TheoremWhat the HAMPATH verifier accepts#✓fully proved

For bit strings \(x\) and \(w\), the HAMPATH verifier accepts \((x, w)\) if and only if there are natural numbers \(s\), \(t\), \(n\), a list \(es\) of pairs of natural numbers and a list \(p\) of natural numbers such that \(x\) is the PATH encoding of \((s, t, n, es)\), \(w\) is the witness encoding of \(p\), and \(p\) is a Hamiltonian path from \(s\) to \(t\) in the digraph on \(0, \dots, n - 1\) with edge list \(es\).

theorem hamCheck_iff (x w : List Bool) : hamCheck x w = true ↔
    ∃ s t n es p, Path.encodeP s t n es = x ∧ encW p = w ∧ IsHamPath n es s t p

Uses 12 · Used by 1

Statement usesWitness encoding · The HAMPATH verifier · Hamiltonian paths · Encoding of a PATH instance

Proof usesWitness decoder · Decoding inverts the witness encoding · The witness codec · The Hamiltonian path check · The Hamiltonian path check is correct · Decoding a PATH instance · Decoding inverts the PATH instance encoding · The PATH instance parser succeeds exactly on encodings

Used byHAMPATH is verified with quadratic-size witnesses

TheoremThe verifier on an encoded instance and witness#✓fully proved

For natural numbers \(s\), \(t\), \(n\), a list \(es\) of pairs of natural numbers and a list \(p\) of natural numbers, the HAMPATH verifier applied to the PATH encoding of \((s, t, n, es)\) and the witness encoding of \(p\) returns the same boolean as the Hamiltonian path check on \(n\), \(es\), \(s\), \(t\) and \(p\).

theorem hamCheck_encode (s t n : ℕ) (es : List (ℕ × ℕ)) (p : List ℕ) :
    hamCheck (Path.encodeP s t n es) (encW p) = hamOk n es s t p

Uses 8 · Used by 1

Statement usesWitness encoding · The HAMPATH verifier · The Hamiltonian path check · Encoding of a PATH instance

Proof usesWitness decoder · Decoding inverts the witness encoding · Decoding a PATH instance · Decoding inverts the PATH instance encoding

Used byCorrectness and running time of the Hamiltonian path verifier

TheoremInstances that do not decode are rejected#✓fully proved

If the PATH instance decoder fails on a bit string \(x\), then for every bit string \(w\) the HAMPATH verifier rejects \((x, w)\), that is, returns false.

theorem hamCheck_of_decodeP {x : List Bool} (h : Path.decodeP x = none) (w : List Bool) :
    hamCheck x w = false

Uses 4 · Used by 1

Statement usesThe HAMPATH verifier · Decoding a PATH instance

Proof usesWitness decoder · The Hamiltonian path check

Used byCorrectness and running time of the Hamiltonian path verifier

TheoremWitnesses that do not decode are rejected#✓fully proved

If the witness decoder fails on a bit string \(w\), then for every bit string \(x\) the HAMPATH verifier rejects \((x, w)\), that is, returns false.

theorem hamCheck_of_decodeW (x : List Bool) {w : List Bool} (h : decodeW w = none) :
    hamCheck x w = false

Uses 4 · Used by 1

Statement usesWitness decoder · The HAMPATH verifier

Proof usesThe Hamiltonian path check · Decoding a PATH instance

Used byCorrectness and running time of the Hamiltonian path verifier

TheoremLength of an encoded PATH instance#✓fully proved

For all natural numbers \(s\), \(t\), \(n\) and every edge list \(E\), the encoding of the PATH instance \((s, t, n, E)\) has length \(s + t + n + 3 + \ell\), where \(\ell\) is the length of the bit encoding of the edge list \(E\).

theorem length_encodeP (s t n : ℕ) (es : List (ℕ × ℕ)) :
    (Path.encodeP s t n es).length = s + t + n + 3 + (Karp.edgeBits es).length

Uses 2 · Used by 1

Statement usesBit encoding of an edge list · Encoding of a PATH instance

Used byHAMPATH is verified with quadratic-size witnesses

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.