Hopcroft's algorithm

DefinitionPreimage of a set under a letter#✓fully proved

For a DFA \(M\) with transition function \(\delta\), a set \(C\) of states and a letter \(a\), the preimage of \(C\) under \(a\) is the set of states \(q\) with \(\delta(q, a) \in C\).

def preimage (C : Finset σ) (a : α) : Finset σ :=
  Finset.univ.filter fun q => M.step q a ∈ C

Used by 14

Used byPredecessor cost of a Hopcroft splitter trace · Hopcroft predecessor-work as splitter counts plus pops · Termination of Hopcroft's loop · Hopcroft loop with recorded predecessor-work · Recorded Hopcroft cost equals the work of the popped trace · Number of blocks after one round · Growth of the waiting list in one round · Effect of one splitter on the common-block relation · One round preserves the invariants · One refinement round of the partition · One update of the waiting list · Potential inequality for one Hopcroft refinement round · Splitter count update after one Hopcroft round · Refined Hopcroft blocks lie inside their old blocks

DefinitionA set of states split by another#✓fully proved

A set \(D\) of states is split by a set \(P\) of states when \(D\) contains both a state in \(P\) and a state not in \(P\), that is, when \(D \cap P\) and \(D \setminus P\) are both nonempty.

def Splits (pre D : Finset σ) : Prop :=
  (D.filter (· ∈ pre)).Nonempty ∧ (D.filter (· ∉ pre)).Nonempty

Used by 11

Used byTermination of Hopcroft's loop · Number of blocks after one round · Growth of the waiting list in one round · Effect of one splitter on the common-block relation · One round preserves the invariants · One update of the waiting list · Pieces of a split block lie on one side · Splitting a block by a set · Potential inequality for one Hopcroft refinement round · Splitter count update after one Hopcroft round · Refined Hopcroft blocks lie inside their old blocks

DefinitionSplitting a block by a set#✓fully proved

For sets \(P\) and \(D\) of states, splitting \(D\) by \(P\) gives the two-element list \([D \cap P,\ D \setminus P]\) if both of these sets are nonempty, and the one-element list \([D]\) otherwise.

def splitBlock (pre D : Finset σ) : List (Finset σ) :=
  if Splits pre D then [D.filter (· ∈ pre), D.filter (· ∉ pre)] else [D]

Uses 1 · Used by 7

Statement usesA set of states split by another

Used byNumber of blocks after one round · Effect of one splitter on the common-block relation · One round preserves the invariants · One refinement round of the partition · Pieces of a split block lie on one side · Potential inequality for one Hopcroft refinement round · Refined Hopcroft blocks lie inside their old blocks

DefinitionSmaller of two finite sets of states#✓fully proved

For finite sets \(A\) and \(B\) of states, the smaller one is \(A\) if \(|A| \le |B|\) and \(B\) otherwise; on a tie in cardinality it is \(A\).

def smaller (A B : Finset σ) : Finset σ := if A.card ≤ B.card then A else B

Used by 18

Used byHopcroft's waiting list is exhausted · Hopcroft's initial waiting list · No initial Hopcroft splitters with at most one state · The invariants hold initially · Hopcroft's final partition is a partition · Growth of the waiting list in one round · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm · New splitters are halves of the split block · New splitters for a split block · One round preserves the invariants · Initial splitter count is at most one · Splitter count of newly added splitters · Potential inequality for one Hopcroft refinement round · Splitter count update after one Hopcroft round · Smaller-half splitters have at most half the block size · The smaller of two sets has at most half their total size · The smaller part of a split has at most half the size

DefinitionNew splitters for a split block#✓fully proved

Given a waiting list \(W\) of pairs of a set of states and a letter and sets \(S\) and \(D\) of states, write \(D_1 = D \cap S\) and \(D_2 = D \setminus S\). The new waiting entries for \(D\) consist, for each letter \(b\) in the enumeration order of the alphabet, of both \((D_1, b)\) and \((D_2, b)\) if \((D, b)\) is in \(W\), and otherwise of the single entry \((E, b)\), where \(E\) is the smaller of \(D_1\) and \(D_2\) by cardinality (\(D_1\) on a tie).

def newSplitters (W : List (Finset σ × α)) (pre D : Finset σ) : List (Finset σ × α) :=
  (FinEnum.toList α).flatMap fun b =>
    if (D, b) ∈ W then [(D.filter (· ∈ pre), b), (D.filter (· ∉ pre), b)]
    else [(smaller (D.filter (· ∈ pre)) (D.filter (· ∉ pre)), b)]

Uses 1 · Used by 7

Statement usesSmaller of two finite sets of states

Used byGrowth of the waiting list in one round · New splitters are halves of the split block · One round preserves the invariants · One update of the waiting list · Splitter count of newly added splitters · Splitter count update after one Hopcroft round · Smaller-half splitters have at most half the block size

DefinitionOne refinement round of the partition#✓fully proved

For a DFA \(M\) with transition function \(\delta\), a list \(P\) of blocks of states, a set \(C\) of states and a letter \(a\), let \(S = \{q : \delta(q, a) \in C\}\) be the preimage of \(C\) under \(a\). The partition after the splitter \((C, a)\) replaces each block \(D\) of \(P\), in order, by the two blocks \(D \cap S\) and \(D \setminus S\) when both are nonempty, and keeps \(D\) otherwise.

def roundP (P : List (Finset σ)) (C : Finset σ) (a : α) : List (Finset σ) :=
  P.flatMap (splitBlock (preimage M C a))

Uses 2 · Used by 15

Statement usesPreimage of a set under a letter · Splitting a block by a set

Used byHopcroft's refinement loop · Hopcroft splitter trace length equals loop fuel · Termination of Hopcroft's loop · Hopcroft loop with recorded predecessor-work · Instrumented Hopcroft loop returns the original result · Recorded Hopcroft cost equals the work of the popped trace · Trace of splitters popped by Hopcroft's algorithm · The splitter trace records exactly the splitters the loop pops · Number of blocks after one round · Popped Hopcroft splitters are nonempty · Effect of one splitter on the common-block relation · One round preserves the invariants · Splitter count bound along a Hopcroft execution · Potential inequality for one Hopcroft refinement round · Refined Hopcroft blocks lie inside their old blocks

DefinitionOne update of the waiting list#✓fully proved

For a DFA \(M\) with transition function \(\delta\), a list \(P\) of blocks of states, a list \(W\) of pairs of a set of states and a letter, a set \(C\) of states and a letter \(a\), let \(S = \{q : \delta(q, a) \in C\}\) be the preimage of \(C\) under \(a\), and say that \(S\) splits a set \(D\) when \(D\) meets both \(S\) and its complement. The waiting list after the splitter \((C, a)\), from the rest \(W\) of the waiting list, consists of the entries of \(W\) whose set is not split by \(S\), followed, for each block \(D\) of \(P\) split by \(S\) in order, by the new splitters for \(D\): for each letter \(b\) in the enumeration order of the alphabet, both \((D \cap S, b)\) and \((D \setminus S, b)\) if \((D, b)\) is in \(W\), and otherwise the single entry \((E, b)\), where \(E\) is the smaller of \(D \cap S\) and \(D \setminus S\) by cardinality (\(D \cap S\) on a tie).

def roundW (P : List (Finset σ)) (W : List (Finset σ × α)) (C : Finset σ) (a : α) :
    List (Finset σ × α) :=
  W.filter (fun cb => !decide (Splits (preimage M C a) cb.1)) ++
    (P.filter fun D => decide (Splits (preimage M C a) D)).flatMap
      (newSplitters W (preimage M C a))

Uses 3 · Used by 14

Statement usesA set of states split by another · New splitters for a split block · Preimage of a set under a letter

Used byHopcroft's refinement loop · Hopcroft splitter trace length equals loop fuel · Termination of Hopcroft's loop · Hopcroft loop with recorded predecessor-work · Instrumented Hopcroft loop returns the original result · Recorded Hopcroft cost equals the work of the popped trace · Trace of splitters popped by Hopcroft's algorithm · The splitter trace records exactly the splitters the loop pops · Growth of the waiting list in one round · Popped Hopcroft splitters are nonempty · One round preserves the invariants · Splitter count bound along a Hopcroft execution · Potential inequality for one Hopcroft refinement round · Splitter count update after one Hopcroft round

DefinitionBlock of accepting states#✓fully proved

For a DFA \(M\) with finite state set \(Q\), this is the set \(F \subseteq Q\) of accepting states of \(M\), as a finite set.

def accBlock : Finset σ := Finset.univ.filter (· ∈ M.accept)

Used by 9

Used byHopcroft's waiting list is exhausted · Hopcroft's initial partition · Hopcroft's initial waiting list · No initial Hopcroft splitters with at most one state · The invariants hold initially · Hopcroft's final partition is a partition · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm · Initial splitter count is at most one

DefinitionRejecting states#✓fully proved

For a DFA \(M\) with state set \(Q\) and set of accepting states \(F\), the rejecting block is the set \(Q \setminus F\) of states of \(M\) that are not accepting.

def rejBlock : Finset σ := Finset.univ.filter (· ∉ M.accept)

Used by 9

Used byHopcroft's waiting list is exhausted · Hopcroft's initial partition · Hopcroft's initial waiting list · No initial Hopcroft splitters with at most one state · The invariants hold initially · Hopcroft's final partition is a partition · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm · Initial splitter count is at most one

DefinitionHopcroft's initial partition#✓fully proved

For a DFA \(M\) with finite state set \(Q\) and set of accepting states \(F\), the initial partition is the list of blocks \(F\), \(Q \setminus F\), in this order, with any empty block removed.

def initP : List (Finset σ) := [accBlock M, rejBlock M].filter (·.Nonempty)

Uses 2 · Used by 14

Statement usesBlock of accepting states · Rejecting states

Used byPredecessor-work bound for the complete Hopcroft run · Zero Hopcroft predecessor-work over an empty alphabet · Zero Hopcroft predecessor-work with at most one state · Total predecessor-work bound · \(O(|\Sigma| n \log n)\) bound on Hopcroft predecessor-work · Hopcroft's waiting list is exhausted · Instrumented complete Hopcroft run returns the minimization partition · Recorded Hopcroft cost obeys the predecessor-work bound · Hopcroft's partition · The invariants hold initially · Hopcroft's final partition is a partition · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm · Hopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter

DefinitionHopcroft's initial waiting list#✓fully proved

Let \(M\) be a DFA with finite state set \(Q\), set of accepting states \(F\) and finite alphabet \(\Sigma\). If \(F\) and \(Q \setminus F\) are both nonempty, the initial waiting list consists of the splitters \((S, b)\) for every letter \(b \in \Sigma\), where \(S = F\) if \(|F| \le |Q \setminus F|\) and \(S = Q \setminus F\) otherwise; if one of \(F\) and \(Q \setminus F\) is empty, the initial waiting list is empty.

def initW : List (Finset σ × α) :=
  if (accBlock M).Nonempty ∧ (rejBlock M).Nonempty then
    (FinEnum.toList α).map fun b => (smaller (accBlock M) (rejBlock M), b)
  else []

Uses 3 · Used by 16

Statement usesBlock of accepting states · Rejecting states · Smaller of two finite sets of states

Used byPredecessor-work bound for the complete Hopcroft run · Zero Hopcroft predecessor-work over an empty alphabet · Zero Hopcroft predecessor-work with at most one state · Total predecessor-work bound · \(O(|\Sigma| n \log n)\) bound on Hopcroft predecessor-work · Hopcroft's waiting list is exhausted · Instrumented complete Hopcroft run returns the minimization partition · Recorded Hopcroft cost obeys the predecessor-work bound · Hopcroft's partition · No initial Hopcroft splitters with at most one state · The invariants hold initially · Hopcroft's final partition is a partition · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm · Hopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter · Initial splitter count is at most one

DefinitionHopcroft's refinement loop#✓fully proved

Let \(M\) be a DFA. Given a round budget \(k\), a partition \(P\) of the states of \(M\) (a list of blocks) and a waiting list \(W\) of splitters \((C, a)\), each a block \(C\) with a letter \(a\), the loop returns the pair \((P, W)\) unchanged if \(k = 0\) or \(W\) is empty. Otherwise it removes the first splitter \((C, a)\) from \(W\), replaces \(P\) by the partition after the splitter \((C, a)\) and the remaining waiting list by the waiting list after the splitter \((C, a)\), and continues with budget \(k - 1\).

def hopcroftLoop : ℕ → List (Finset σ) → List (Finset σ × α) →
    List (Finset σ) × List (Finset σ × α)
  | 0, P, W => (P, W)
  | _ + 1, P, [] => (P, [])
  | k + 1, P, (C, a) :: W => hopcroftLoop k (roundP M P C a) (roundW M P W C a)

Uses 2 · Used by 9

Statement usesOne refinement round of the partition · One update of the waiting list

Used byHopcroft splitter trace length equals loop fuel · Termination of Hopcroft's loop · Hopcroft's waiting list is exhausted · Instrumented complete Hopcroft run returns the minimization partition · Instrumented Hopcroft loop returns the original result · Hopcroft's partition · Hopcroft's final partition is a partition · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm

DefinitionHopcroft's partition#✓fully proved

Let \(M\) be a DFA with finite state set \(Q\) over a finite alphabet \(\Sigma\). Hopcroft's partition of \(M\) is the partition returned by Hopcroft's loop run from the initial partition and the initial waiting list with a budget of \(|\Sigma| \cdot (|Q| + 1)\) rounds.

def hopcroftPartition : List (Finset σ) :=
  (M.hopcroftLoop (Fintype.card α * (Fintype.card σ + 1)) (initP M) (initW M)).1

Uses 3 · Used by 5

Statement usesHopcroft's initial partition · Hopcroft's initial waiting list · Hopcroft's refinement loop

Used byInstrumented complete Hopcroft run returns the minimization partition · Hopcroft's relation · Hopcroft's final partition is a partition · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm

DefinitionHopcroft's relation#✓fully proved

For a DFA \(M\) with finitely many states, Hopcroft's relation is the set of pairs \((p, q)\) of states of \(M\) such that \(p\) and \(q\) lie in a common block of Hopcroft's partition.

def hopcroftRel : Finset (σ × σ) :=
  Finset.univ.filter fun pq => ∃ D ∈ M.hopcroftPartition, pq.1 ∈ D ∧ pq.2 ∈ D

Uses 1 · Used by 3

Statement usesHopcroft's partition

Used byHopcroft's partition is Moore's relation · Correctness of Hopcroft's algorithm · Moore classes are Hopcroft blocks

StructurePartitions of the states#✓fully proved

A list \(P\) of sets of states is a partition into nonempty blocks when entries of \(P\) at different positions are disjoint, every entry of \(P\) is nonempty, and every state lies in some entry of \(P\).

structure IsPartition (P : List (Finset σ)) : Prop where
  disjoint : P.Pairwise Disjoint
  nonempty : ∀ D ∈ P, D.Nonempty
  cover : ∀ q, ∃ D ∈ P, q ∈ D

Used by 13

Used byTermination of Hopcroft's loop · Invariants of Hopcroft's loop · The invariants hold initially · Hopcroft's final partition is a partition · A partition has at most as many blocks as there are states · A block contains both or neither of two related states · Popped Hopcroft splitters are nonempty · One round preserves the invariants · Splitter count bound along a Hopcroft execution · Hopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter · Potential inequality for one Hopcroft refinement round · Splitter count update after one Hopcroft round · Refined Hopcroft blocks lie inside their old blocks

DefinitionLying in a common block#✓fully proved

For a list \(P\) of sets of states, two states \(p\) and \(q\) are related by \(P\) when some block \(D\) of \(P\) contains both \(p\) and \(q\).

def Rel (P : List (Finset σ)) (p q : σ) : Prop := ∃ D ∈ P, p ∈ D ∧ q ∈ D

Used by 9

Used byInvariants of Hopcroft's loop · The invariants hold initially · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm · A block contains both or neither of two related states · With an empty waiting list, blocks are the classes of equal continuation languages · Effect of one splitter on the common-block relation · One round preserves the invariants · Potential inequality for one Hopcroft refinement round

TheoremA block contains both or neither of two related states#✓fully proved

Let \(P\) be a list of sets of states that is a partition into nonempty blocks, let \(C\) be an entry of \(P\), and let \(p\) and \(q\) be states lying in a common entry of \(P\). Then \(p \in C\) if and only if \(q \in C\).

theorem IsPartition.mem_iff_of_rel {P : List (Finset σ)} (hP : IsPartition P) {C : Finset σ}
    (hC : C ∈ P) {p q : σ} (h : Rel P p q) : p ∈ C ↔ q ∈ C

Uses 2 · Used by 2

Statement usesPartitions of the states · Lying in a common block

Used byBlocks of Hopcroft's partition are language classes · One round preserves the invariants

TheoremA partition has at most as many blocks as there are states#✓fully proved

If a list \(P\) of sets of states is a partition into nonempty blocks, then the length of \(P\) is at most the number \(|Q|\) of states.

theorem IsPartition.length_le {P : List (Finset σ)} (hP : IsPartition P) :
    P.length ≤ Fintype.card σ

Uses 1 · Used by 1

Statement usesPartitions of the states

Used byTermination of Hopcroft's loop

TheoremPieces of a split block lie on one side#✓fully proved

Let \(S\) and \(D\) be sets of states. Every piece of \(D\) split by \(S\) (the two sets \(D \cap S\) and \(D \setminus S\) if \(D\) meets both \(S\) and its complement, and \(D\) itself otherwise) is contained in \(S\) or disjoint from \(S\): any two states \(x\) and \(y\) of the piece satisfy \(x \in S \iff y \in S\).

theorem side_of_mem_splitBlock {pre D D' : Finset σ} (h : D' ∈ splitBlock pre D) {x y : σ}
    (hx : x ∈ D') (hy : y ∈ D') : x ∈ pre ↔ y ∈ pre

Uses 2 · Used by 1

Statement usesSplitting a block by a set

Proof usesA set of states split by another

Used byEffect of one splitter on the common-block relation

TheoremEffect of one splitter on the common-block relation#✓fully proved

Let \(M\) be a DFA with transition function \(\delta\), \(P\) a list of blocks of states, \(C\) a set of states and \(a\) a letter. Two states \(p\) and \(q\) lie in a common block after the splitter \((C, a)\) is applied to \(P\) if and only if they lie in a common block of \(P\) and \(\delta(p, a) \in C \iff \delta(q, a) \in C\).

theorem rel_roundP_iff {P : List (Finset σ)} {C : Finset σ} {a : α} {p q : σ} :
    Rel (roundP M P C a) p q ↔ Rel P p q ∧ (p ∈ preimage M C a ↔ q ∈ preimage M C a)

Uses 6 · Used by 2

Statement usesLying in a common block · Preimage of a set under a letter · One refinement round of the partition

Proof usesA set of states split by another · Pieces of a split block lie on one side · Splitting a block by a set

Used byOne round preserves the invariants · Potential inequality for one Hopcroft refinement round

TheoremNumber of blocks after one round#✓fully proved

Let \(M\) be a DFA with transition function \(\delta\), let \(P\) be a list of sets of states, \(C\) a set of states and \(a\) a letter, and let \(\mathrm{pre} = \{q : \delta(q, a) \in C\}\). The partition after the splitter \((C, a)\), which replaces each entry \(D\) of \(P\) meeting both \(\mathrm{pre}\) and its complement by \(D \cap \mathrm{pre}\) and \(D \setminus \mathrm{pre}\), has length equal to the length of \(P\) plus the number of entries of \(P\) (counted with repetition) that meet both \(\mathrm{pre}\) and its complement.

theorem length_roundP {P : List (Finset σ)} {C : Finset σ} {a : α} :
    (roundP M P C a).length =
      P.length + (P.filter fun D => decide (Splits (preimage M C a) D)).length

Uses 4 · Used by 1

Statement usesA set of states split by another · Preimage of a set under a letter · One refinement round of the partition

Proof usesSplitting a block by a set

Used byTermination of Hopcroft's loop

TheoremGrowth of the waiting list in one round#✓fully proved

Let \(M\) be a DFA with transition function \(\delta\) over a finite alphabet \(\Sigma\), let \(P\) be a list of sets of states with no repeated entries, let \(W\) be a list of pairs of a set of states and a letter, let \(C\) be a set of states and \(a\) a letter, and let \(S = \{q : \delta(q, a) \in C\}\) be the preimage of \(C\) under \(a\). Then the waiting list after the splitter \((C, a)\), computed from the blocks \(P\) and the rest \(W\) of the waiting list, has length at most \(|W| + |\Sigma| \cdot k\), where \(k\) is the number of entries of \(P\) split by \(S\), that is, meeting both \(S\) and its complement.

theorem length_roundW_le {P : List (Finset σ)} (hnd : P.Nodup) {W : List (Finset σ × α)}
    {C : Finset σ} {a : α} :
    (roundW M P W C a).length ≤
      W.length +
        Fintype.card α * (P.filter fun D => decide (Splits (preimage M C a) D)).length

Uses 5 · Used by 1

Statement usesA set of states split by another · Preimage of a set under a letter · One update of the waiting list

Proof usesNew splitters for a split block · Smaller of two finite sets of states

Used byTermination of Hopcroft's loop

StructureInvariants of Hopcroft's loop#✓fully proved

Let \(M\) be a DFA with transition function \(\delta\). A list \(P\) of sets of states and a waiting list \(W\) of pairs \((C, b)\) of a set of states \(C\) and a letter \(b\) satisfy the invariants when: (i) \(P\) is a partition of the states into nonempty blocks; (ii) for every \((C, b)\) in \(W\), \(C\) is an entry of \(P\); (iii) for every letter \(b\) and all states \(p\), \(q\) lying in a common entry of \(P\), if for every \(C\) with \((C, b)\) in \(W\) the states \(\delta(p, b)\) and \(\delta(q, b)\) are both in \(C\) or both outside \(C\), then \(\delta(p, b)\) and \(\delta(q, b)\) lie in a common entry of \(P\); (iv) any two states lying in a common entry of \(P\) are both accepting or both rejecting; and (v) any two states from which \(M\) accepts the same language lie in a common entry of \(P\).

structure Inv (P : List (Finset σ)) (W : List (Finset σ × α)) : Prop where
  /-- `P` is a partition into nonempty blocks. -/
  part : IsPartition P
  /-- Every waiting set is a block. -/
  mem : ∀ cb ∈ W, cb.1 ∈ P
  /-- Two states in one block whose `b`-successors agree on every set waiting with `b` have
  `b`-successors in one block. -/
  stable : ∀ b p q, Rel P p q → (∀ C, (C, b) ∈ W → (M.step p b ∈ C ↔ M.step q b ∈ C)) →
    Rel P (M.step p b) (M.step q b)
  /-- Blocks agree on acceptance. -/
  accept : ∀ p q, Rel P p q → (p ∈ M.accept ↔ q ∈ M.accept)
  /-- States with one continuation language share a block. -/
  coarse : ∀ p q, M.acceptsFrom p = M.acceptsFrom q → Rel P p q

Uses 2 · Used by 11

Statement usesPartitions of the states · Lying in a common block

Used byTermination of Hopcroft's loop · Hopcroft's waiting list is exhausted · The invariants hold initially · Hopcroft's final partition is a partition · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm · Popped Hopcroft splitters are nonempty · With an empty waiting list, blocks are the classes of equal continuation languages · One round preserves the invariants · Splitter count bound along a Hopcroft execution · Hopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter

TheoremOne round preserves the invariants#✓fully proved

Let \(M\) be a DFA, \(P\) a list of blocks of states, \(W\) a list of pairs of a set of states and a letter, \(C\) a set of states and \(a\) a letter. If \(P\) and the waiting list obtained by putting \((C, a)\) in front of \(W\) satisfy the invariants of Hopcroft's loop, then so do the partition after the splitter \((C, a)\) and the waiting list after the splitter \((C, a)\) from the rest \(W\).

theorem Inv.round {P : List (Finset σ)} {C : Finset σ} {a : α} {W : List (Finset σ × α)}
    (h : Inv M P ((C, a) :: W)) : Inv M (roundP M P C a) (roundW M P W C a)

Uses 12 · Used by 3

Statement usesInvariants of Hopcroft's loop · One refinement round of the partition · One update of the waiting list

Proof usesPartitions of the states · A block contains both or neither of two related states · Lying in a common block · A set of states split by another · New splitters for a split block · Preimage of a set under a letter · Effect of one splitter on the common-block relation · Smaller of two finite sets of states · Splitting a block by a set

Used byTermination of Hopcroft's loop · Popped Hopcroft splitters are nonempty · Splitter count bound along a Hopcroft execution

TheoremWith an empty waiting list, blocks are the classes of equal continuation languages#✓fully proved

Let \(M\) be a DFA and \(P\) a list of blocks of states such that \(P\) with the empty waiting list satisfies the invariants of Hopcroft's loop. Then two states \(p\) and \(q\) lie in a common block of \(P\) if and only if they accept the same continuation languages, that is, \(M\) accepts a word from \(p\) exactly when it accepts it from \(q\).

With an empty waiting list the invariants say that \(P\) is a right congruence refining acceptance.

theorem Inv.rel_iff {P : List (Finset σ)} (h : Inv M P []) {p q : σ} :
    Rel P p q ↔ M.acceptsFrom p = M.acceptsFrom q

Uses 2 · Used by 2

Statement usesInvariants of Hopcroft's loop · Lying in a common block

Used byBlocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm

TheoremThe invariants hold initially#✓fully proved

For every DFA \(M\) with finitely many states over a finite alphabet, Hopcroft's initial partition and initial waiting list satisfy the invariants of Hopcroft's loop.

theorem inv_init : Inv M (initP M) (initW M)

Uses 8 · Used by 6

Statement usesInvariants of Hopcroft's loop · Hopcroft's initial partition · Hopcroft's initial waiting list

Proof usesPartitions of the states · Lying in a common block · Block of accepting states · Rejecting states · Smaller of two finite sets of states

Used byTotal predecessor-work bound · Hopcroft's waiting list is exhausted · Hopcroft's final partition is a partition · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm · Hopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter

TheoremTermination of Hopcroft's loop#✓fully proved

Let \(M\) be a DFA with finite state set \(Q\) over a finite alphabet \(\Sigma\), let \(P\) be a partition of the states given as a list of blocks, let \(W\) be a waiting list of splitters, and let \(k\) be a natural number. If \(P\) and \(W\) satisfy the invariants of Hopcroft's loop and \(|W| + |\Sigma| \cdot (|Q| - |P|) \le k\), where \(|P|\) and \(|W|\) are the lengths of the lists, then Hopcroft's loop run from \((P, W)\) with a budget of \(k\) rounds ends with an empty waiting list, and the partition and waiting list it returns again satisfy the invariants.

The invariants make \(P\) a partition into nonempty blocks, so \(|P| \le |Q|\) and the difference \(|Q| - |P|\) is not truncated.

theorem hopcroftLoop_spec : ∀ (k : ℕ) (P : List (Finset σ)) (W : List (Finset σ × α)),
    Inv M P W → W.length + Fintype.card α * (Fintype.card σ - P.length) ≤ k →
    (M.hopcroftLoop k P W).2 = [] ∧ Inv M (M.hopcroftLoop k P W).1 (M.hopcroftLoop k P W).2

Uses 11 · Used by 4

Statement usesInvariants of Hopcroft's loop · Hopcroft's refinement loop

Proof usesOne round preserves the invariants · Partitions of the states · A partition has at most as many blocks as there are states · A set of states split by another · Number of blocks after one round · Growth of the waiting list in one round · Preimage of a set under a letter · One refinement round of the partition · One update of the waiting list

Used byHopcroft's waiting list is exhausted · Hopcroft's final partition is a partition · Blocks of Hopcroft's partition are language classes · Correctness of Hopcroft's algorithm

TheoremHopcroft's waiting list is exhausted#✓fully proved

Let \(M\) be a DFA with finite state set \(Q\) over a finite alphabet \(\Sigma\). Hopcroft's loop, run from the initial partition and the initial waiting list with a budget of \(|\Sigma| \cdot (|Q| + 1)\) rounds, ends with an empty waiting list.

theorem hopcroftLoop_waiting_eq_nil :
    (M.hopcroftLoop (Fintype.card α * (Fintype.card σ + 1)) (initP M) (initW M)).2 = []

Uses 9 · Used by 1

Statement usesHopcroft's initial partition · Hopcroft's initial waiting list · Hopcroft's refinement loop

Proof usesInvariants of Hopcroft's loop · Block of accepting states · The invariants hold initially · Rejecting states · Smaller of two finite sets of states · Termination of Hopcroft's loop

Used byInstrumented complete Hopcroft run returns the minimization partition

TheoremHopcroft's final partition is a partition#✓fully proved

For a DFA \(M\), Hopcroft's final partition of \(M\) is a partition of the states of \(M\) into nonempty blocks.

theorem isPartition_hopcroftPartition : IsPartition M.hopcroftPartition

Uses 11 · Used by 1

Statement usesPartitions of the states · Hopcroft's partition

Proof usesInvariants of Hopcroft's loop · Block of accepting states · Hopcroft's initial partition · Hopcroft's initial waiting list · The invariants hold initially · Rejecting states · Smaller of two finite sets of states · Hopcroft's refinement loop · Termination of Hopcroft's loop

Used byBlocks of Hopcroft's partition are language classes

TheoremCorrectness of Hopcroft's algorithm#✓fully proved

For a DFA \(M\), two states \(p\) and \(q\) share a block of Hopcroft's final partition of \(M\) exactly when the language accepted by \(M\) from \(p\) equals the language accepted by \(M\) from \(q\).

theorem mem_hopcroftRel_iff {p q : σ} :
    (p, q) ∈ M.hopcroftRel ↔ M.acceptsFrom p = M.acceptsFrom q

Uses 13 · Used by 2

Statement usesHopcroft's relation

Proof usesInvariants of Hopcroft's loop · With an empty waiting list, blocks are the classes of equal continuation languages · Lying in a common block · Block of accepting states · Hopcroft's initial partition · Hopcroft's initial waiting list · The invariants hold initially · Rejecting states · Smaller of two finite sets of states · Hopcroft's refinement loop · Termination of Hopcroft's loop · Hopcroft's partition

Used byHopcroft's partition is Moore's relation · Moore classes are Hopcroft blocks

TheoremHopcroft's partition is Moore's relation#✓fully proved

For every DFA \(M\) with finitely many states over a finite alphabet, Hopcroft's relation of \(M\), the set of pairs of states lying in a common block of Hopcroft's partition, equals Moore's state equivalence of \(M\) as a set of pairs of states.

theorem hopcroftRel_eq_mooreRel : M.hopcroftRel = M.mooreRel

Uses 4

Statement usesHopcroft's relation · Moore's relation

Proof usesCorrectness of Hopcroft's algorithm · Correctness of Moore's refinement

TheoremMoore classes are Hopcroft blocks#✓fully proved

For a DFA \(M\) and reachable states \(p\) and \(q\) of \(M\), the classes of \(p\) and \(q\) under Moore's equivalence on reachable states (the states of Moore's minimal automaton) are equal if and only if \(p\) and \(q\) share a block of Hopcroft's final partition of \(M\).

theorem mooreClass_eq_iff_mem_hopcroftRel {p q : {s // s ∈ M.reachable}} :
    M.mooreClass p = M.mooreClass q ↔ (p.1, q.1) ∈ M.hopcroftRel

Uses 7

Statement usesStates of Moore's automaton · Hopcroft's relation · Moore class of a reachable state · Reachable states of a DFA

Proof usesCorrectness of Hopcroft's algorithm · Correctness of Moore's refinement · Moore equivalence on reachable states

TheoremBlocks of Hopcroft's partition are language classes#✓fully proved

Let \(M\) be a DFA, \(D\) a block of Hopcroft's final partition of \(M\) and \(p\) a state in \(D\). Then a state \(q\) lies in \(D\) if and only if the language accepted by \(M\) from \(q\) equals the language accepted by \(M\) from \(p\).

theorem mem_block_iff {D : Finset σ} (hD : D ∈ M.hopcroftPartition) {p : σ} (hp : p ∈ D)
    {q : σ} : q ∈ D ↔ M.acceptsFrom q = M.acceptsFrom p

Uses 14

Statement usesHopcroft's partition

Proof usesInvariants of Hopcroft's loop · With an empty waiting list, blocks are the classes of equal continuation languages · A block contains both or neither of two related states · Lying in a common block · Block of accepting states · Hopcroft's initial partition · Hopcroft's initial waiting list · The invariants hold initially · Rejecting states · Smaller of two finite sets of states · Hopcroft's refinement loop · Termination of Hopcroft's loop · Hopcroft's final partition is a partition

TheoremThe smaller of two sets has at most half their total size#✓fully proved

The smaller of two sets has at most half their combined size: it is one of the two sets, so twice its size is at most the sum of the two sizes.

theorem two_mul_smaller_card_le {σ : Type*} (A B : Finset σ) :
    2 * (smaller A B).card ≤ A.card + B.card

Uses 1 · Used by 1

Statement usesSmaller of two finite sets of states

Used byThe smaller part of a split has at most half the size

TheoremThe smaller part of a split has at most half the size#✓fully proved

If two disjoint sets union to D, the smaller of them has at most half the size of D.

theorem two_mul_smaller_card_le_of_split {σ : Type*} [DecidableEq σ] {D A B : Finset σ}
    (hun : A ∪ B = D) (hdis : Disjoint A B) : 2 * (smaller A B).card ≤ D.card

Uses 2 · Used by 2

Statement usesSmaller of two finite sets of states

Proof usesThe smaller of two sets has at most half their total size

Used byPotential inequality for one Hopcroft refinement round · Smaller-half splitters have at most half the block size

TheoremHalving chains shrink blocks by a factor of at least \(2^k\)#✓fully proved

After k halving steps, the initial block is at least 2 ^ k times the final block. The halving hypothesis is stated for the cardinalities only; no subset hypothesis is needed.

theorem mul_pow_le_card_of_halving_chain {σ : Type*} {f : ℕ → Finset σ} {k : ℕ}
    (hstep : ∀ i, i < k → 2 * (f (i + 1)).card ≤ (f i).card) :
    2 ^ k * (f k).card ≤ (f 0).card

Used by 1

Used byThe smaller-half counting lemma

TheoremThe smaller-half counting lemma#✓fully proved

In a chain of blocks where each step at least halves the size, a block containing a given state can occur at most Nat.log 2 n times past the start, where n is the number of states. In Hopcroft's algorithm, the successive smaller halves containing one fixed state form such a chain: each of them is the smaller half of a split of the previous block containing that state.

theorem smaller_half_chain_le_log {σ : Type*} [Fintype σ] {f : ℕ → Finset σ} {q : σ}
    {k : ℕ} (hmem : ∀ i, i ≤ k → q ∈ f i)
    (hstep : ∀ i, i < k → 2 * (f (i + 1)).card ≤ (f i).card) :
    k ≤ Nat.log 2 (Fintype.card σ)

Sources

• J. E. Hopcroft, "An n log n algorithm for minimizing states in a finite automaton", Theory of Machines and Computations, 1971; the counting argument is presented in J. Berstel, L. Boasson, O. Carton and I. Fagnot, "Minimization of automata", 2010.

Uses 1

Proof usesHalving chains shrink blocks by a factor of at least \(2^k\)

TheoremNew splitters are halves of the split block#✓fully proved

Every entry newSplitters adds for a block D is a half of D (one of the two sides of the split by pre), or the smaller half.

theorem mem_newSplitters {W : List (Finset σ × α)} {pre D : Finset σ} {X : Finset σ}
    {b : α} (h : (X, b) ∈ newSplitters W pre D) :
    X ⊆ D ∧ (X = D.filter (· ∈ pre) ∨ X = D.filter (· ∉ pre) ∨
      X = smaller (D.filter (· ∈ pre)) (D.filter (· ∉ pre)))

Uses 2 · Used by 1

Statement usesNew splitters for a split block · Smaller of two finite sets of states

Used bySplitter count update after one Hopcroft round

TheoremSmaller-half splitters have at most half the block size#✓fully proved

A smaller-half entry added by newSplitters for a block D has at most half the size of D: the two halves are disjoint and union to D. No split hypothesis is needed: the halves of any block partition it.

theorem two_mul_card_le_of_mem_newSplitters_smaller {W : List (Finset σ × α)}
    {pre D : Finset σ} {X : Finset σ} {b : α} (h : (X, b) ∈ newSplitters W pre D)
    (hDb : (D, b) ∉ W) :
    2 * X.card ≤ D.card

Uses 3

Statement usesNew splitters for a split block

Proof usesSmaller of two finite sets of states · The smaller part of a split has at most half the size

DefinitionTrace of splitters popped by Hopcroft's algorithm#✓fully proved

The splitters popped by Hopcroft's loop, in order: the same recursion as DFA.hopcroftLoop, collecting each popped splitter. The cost of processing one popped splitter (C, a) is (preimage M C a).card + 1: one predecessor visit per state whose a-successor lies in C, plus O(1) per-splitter overhead. See hopcroftCost. hopcroftLoop_eq_hopcroftLoop_of_length proves this trace records exactly the splitters the loop pops, so the trace cannot drift from the loop.

def hopcroftSplitters : ℕ → List (Finset σ) → List (Finset σ × α) → List (Finset σ × α)
  | 0, _, _ => []
  | _ + 1, _, [] => []
  | k + 1, P, (C, a) :: W =>
      (C, a) :: hopcroftSplitters k (roundP M P C a) (roundW M P W C a)

Uses 2 · Used by 12

Statement usesOne refinement round of the partition · One update of the waiting list

Used byPredecessor-work bound for the complete Hopcroft run · Zero Hopcroft predecessor-work over an empty alphabet · Zero Hopcroft predecessor-work with at most one state · Total predecessor-work bound · \(O(|\Sigma| n \log n)\) bound on Hopcroft predecessor-work · Hopcroft splitter trace length equals loop fuel · Recorded Hopcroft cost obeys the predecessor-work bound · Recorded Hopcroft cost equals the work of the popped trace · The splitter trace records exactly the splitters the loop pops · Popped Hopcroft splitters are nonempty · Splitter count bound along a Hopcroft execution · Hopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter

DefinitionPredecessor cost of a Hopcroft splitter trace#✓fully proved

The predecessor cost of a splitter trace: for each popped splitter (C, a), one predecessor visit per state in the preimage preimage M C a, plus 1 per-splitter overhead. This is the quantity the total-work bound constrains to O(|Σ| n log n). Charging splitter size C.card instead would undercount: if all n states transition on a to one state q, processing the singleton splitter ({q}, a) costs n predecessor visits while C.card charges only 1.

def hopcroftCost (trace : List (Finset σ × α)) : ℕ :=
  (trace.map fun cb => (preimage M cb.1 cb.2).card + 1).sum

Uses 1 · Used by 8

Statement usesPreimage of a set under a letter

Used byPredecessor-work bound for the complete Hopcroft run · Hopcroft predecessor-work as splitter counts plus pops · Zero Hopcroft predecessor-work over an empty alphabet · Zero Hopcroft predecessor-work with at most one state · Total predecessor-work bound · \(O(|\Sigma| n \log n)\) bound on Hopcroft predecessor-work · Recorded Hopcroft cost obeys the predecessor-work bound · Recorded Hopcroft cost equals the work of the popped trace

TheoremThe splitter trace records exactly the splitters the loop pops#✓fully proved

The loop and the trace recurse on the same state, so they take the same number of steps. The two theorems below make the correspondence usable: the trace length is at most k, and running the loop for exactly the trace's length gives the full loop result, so the trace contains every splitter the loop pops and no others.

theorem hopcroftSplitters_length_le {α σ : Type*} [FinEnum α] [Fintype σ]
    [DecidableEq σ] (M : DFA α σ) (k : ℕ)
    (P : List (Finset σ))
    (W : List (Finset σ × α)) :
    (hopcroftSplitters M k P W).length ≤ k

Uses 3

Statement usesTrace of splitters popped by Hopcroft's algorithm

Proof usesOne refinement round of the partition · One update of the waiting list

TheoremHopcroft splitter trace length equals loop fuel#✓fully proved

The trace and the loop take the same number of steps: the trace length is the fuel the loop consumed, i.e. the loop would stop after exactly that many rounds if run with only that much fuel.

theorem hopcroftLoop_eq_hopcroftLoop_of_length {α σ : Type*} [FinEnum α]
    [Fintype σ] [DecidableEq σ] (M : DFA α σ) (k : ℕ)
    (P : List (Finset σ))
    (W : List (Finset σ × α)) :
    M.hopcroftLoop ((hopcroftSplitters M k P W).length) P W =
      M.hopcroftLoop k P W

Uses 4

Statement usesTrace of splitters popped by Hopcroft's algorithm · Hopcroft's refinement loop

Proof usesOne refinement round of the partition · One update of the waiting list

DefinitionSplitter count of a state and letter#✓fully proved

Number of splitters with letter b containing q, with multiplicity. This applies both to the waiting list and to the actual popped trace.

def splitterCount (q : σ) (b : α) (W : List (Finset σ × α)) : ℕ :=
  W.countP fun cb => decide (cb.2 = b ∧ q ∈ cb.1)

Used by 10

Used byHopcroft predecessor-work as splitter counts plus pops · Total predecessor-work bound · Number of pops bounded by the total splitter count · Splitter count bound along a Hopcroft execution · Hopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter · Initial splitter count is at most one · Splitter count of newly added splitters · Waiting entries give positive splitter count · Potential inequality for one Hopcroft refinement round · Splitter count update after one Hopcroft round

TheoremSplitter count of newly added splitters#✓fully proved

Replacement contributes one token at a state in the parent block; otherwise only membership in the smaller half contributes a token.

theorem splitterCount_newSplitters (q : σ) (b : α)
    (W : List (Finset σ × α)) (pre D : Finset σ) :
    splitterCount q b (newSplitters W pre D) =
      if (D, b) ∈ W then (if q ∈ D then 1 else 0)
      else if q ∈ smaller (D.filter (· ∈ pre))
          (D.filter (· ∉ pre)) then 1 else 0

Uses 3 · Used by 1

Statement usesNew splitters for a split block · Smaller of two finite sets of states · Splitter count of a state and letter

Used bySplitter count update after one Hopcroft round

TheoremSplitter count update after one Hopcroft round#✓fully proved

The exact token update at a state. Only its unique parent block can contribute a new token, even when other blocks split in the same round.

theorem splitterCount_roundW (M : DFA α σ) {P : List (Finset σ)}
    (hP : IsPartition P) (W : List (Finset σ × α))
    (hW : ∀ cb ∈ W, cb.1 ∈ P) (q : σ) (b : α)
    (C D : Finset σ) (a : α) (hD : D ∈ P) (hq : q ∈ D) :
    splitterCount q b (roundW M P W C a) =
      if Splits (preimage M C a) D then
        if (D, b) ∈ W then 1
        else if q ∈ smaller (D.filter (· ∈ preimage M C a))
            (D.filter (· ∉ preimage M C a)) then 1 else 0
      else splitterCount q b W

Uses 9 · Used by 1

Statement usesPartitions of the states · A set of states split by another · Preimage of a set under a letter · One update of the waiting list · Smaller of two finite sets of states · Splitter count of a state and letter

Proof usesNew splitters are halves of the split block · New splitters for a split block · Splitter count of newly added splitters

Used byPotential inequality for one Hopcroft refinement round

TheoremWaiting entries give positive splitter count#✓fully proved

A waiting entry supplies a token; duplicate entries remain counted.

theorem splitterCount_pos_of_mem (q : σ) (b : α)
    {W : List (Finset σ × α)} {D : Finset σ}
    (hW : (D, b) ∈ W) (hq : q ∈ D) : 0 < splitterCount q b W

Uses 1 · Used by 1

Statement usesSplitter count of a state and letter

Used byPotential inequality for one Hopcroft refinement round

TheoremRefined Hopcroft blocks lie inside their old blocks#✓fully proved

A refined block containing q is a subset of the old block containing q. Both partitions are the canonical Hopcroft partitions.

theorem IsPartition.subset_of_mem_roundP (M : DFA α σ)
    {P : List (Finset σ)} (hP : IsPartition P)
    {C D E : Finset σ} {a : α} {q : σ}
    (hD : D ∈ P) (hqD : q ∈ D)
    (hE : E ∈ Hopcroft.roundP M P C a) (hqE : q ∈ E) : E ⊆ D

Uses 5 · Used by 1

Statement usesPartitions of the states · One refinement round of the partition

Proof usesA set of states split by another · Preimage of a set under a letter · Splitting a block by a set

Used byPotential inequality for one Hopcroft refinement round

TheoremPotential inequality for one Hopcroft refinement round#✓fully proved

One refinement cannot increase logarithmic block-size credit plus pending-token credit. Replacing a pending splitter spends no new credit; adding a nonpending smaller half spends one logarithmic unit.

theorem splitterCount_round_potential (M : DFA α σ)
    {P : List (Finset σ)} (hP : IsPartition P)
    (W : List (Finset σ × α)) (hW : ∀ cb ∈ W, cb.1 ∈ P)
    (q : σ) (b : α) {C D E : Finset σ} {a : α}
    (hD : D ∈ P) (hqD : q ∈ D)
    (hE : E ∈ roundP M P C a) (hqE : q ∈ E) :
    splitterCount q b (roundW M P W C a) + Nat.log 2 E.card ≤
      splitterCount q b W + Nat.log 2 D.card

Uses 14 · Used by 1

Statement usesPartitions of the states · One refinement round of the partition · One update of the waiting list · Splitter count of a state and letter

Proof usesRefined Hopcroft blocks lie inside their old blocks · Lying in a common block · A set of states split by another · Preimage of a set under a letter · Effect of one splitter on the common-block relation · Smaller of two finite sets of states · Splitting a block by a set · Waiting entries give positive splitter count · Splitter count update after one Hopcroft round · The smaller part of a split has at most half the size

Used bySplitter count bound along a Hopcroft execution

TheoremSplitter count bound along a Hopcroft execution#✓fully proved

Total state/letter charging along the actual execution. The bound includes initial tokens and tokens still pending through replacements. No amortized bound is assumed in the execution invariant.

theorem splitterCount_hopcroftSplitters_le (M : DFA α σ) (k : ℕ)
    {P : List (Finset σ)} {W : List (Finset σ × α)} (hI : Inv M P W)
    (q : σ) (b : α) {D : Finset σ} (hD : D ∈ P) (hqD : q ∈ D) :
    splitterCount q b (hopcroftSplitters M k P W) ≤
      splitterCount q b W + Nat.log 2 D.card

Uses 8 · Used by 1

Statement usesInvariants of Hopcroft's loop · Trace of splitters popped by Hopcroft's algorithm · Splitter count of a state and letter

Proof usesOne round preserves the invariants · Partitions of the states · One refinement round of the partition · One update of the waiting list · Potential inequality for one Hopcroft refinement round

Used byHopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter

TheoremInitial splitter count is at most one#✓fully proved

Initially there is at most one token for each state and letter.

theorem splitterCount_initW_le (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] (q : σ) (b : α) :
    splitterCount q b (initW M) ≤ 1

Uses 5 · Used by 1

Statement usesHopcroft's initial waiting list · Splitter count of a state and letter

Proof usesBlock of accepting states · Rejecting states · Smaller of two finite sets of states

Used byHopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter

TheoremHopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter#✓fully proved

Each state is processed with a fixed letter at most log₂ n + 1 times during any prefix of the actual initialized Hopcroft execution.

theorem splitterCount_init_trace_le (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] (k : ℕ) (q : σ) (b : α) :
    splitterCount q b (hopcroftSplitters M k (initP M) (initW M)) ≤
      Nat.log 2 (Fintype.card σ) + 1

Uses 9 · Used by 1

Statement usesTrace of splitters popped by Hopcroft's algorithm · Hopcroft's initial partition · Hopcroft's initial waiting list · Splitter count of a state and letter

Proof usesInvariants of Hopcroft's loop · Partitions of the states · The invariants hold initially · Splitter count bound along a Hopcroft execution · Initial splitter count is at most one

Used byTotal predecessor-work bound

TheoremPopped Hopcroft splitters are nonempty#✓fully proved

Every popped splitter has a nonempty block, including splitters whose predecessor set is empty.

theorem nonempty_of_mem_hopcroftSplitters (M : DFA α σ) (k : ℕ)
    {P : List (Finset σ)} {W : List (Finset σ × α)} (hI : Inv M P W)
    {cb : Finset σ × α} (hcb : cb ∈ hopcroftSplitters M k P W) :
    cb.1.Nonempty

Uses 6 · Used by 1

Statement usesInvariants of Hopcroft's loop · Trace of splitters popped by Hopcroft's algorithm

Proof usesOne round preserves the invariants · Partitions of the states · One refinement round of the partition · One update of the waiting list

Used byTotal predecessor-work bound

TheoremHopcroft predecessor-work as splitter counts plus pops#✓fully proved

Double counting visits by source state and letter, retaining every incoming transition even when many sources have the same successor.

theorem hopcroftCost_eq_sum_splitterCount (M : DFA α σ)
    (trace : List (Finset σ × α)) :
    hopcroftCost M trace =
      (∑ b : α, ∑ q : σ, splitterCount (M.step q b) b trace) +
        trace.length

Uses 3 · Used by 1

Statement usesPredecessor cost of a Hopcroft splitter trace · Splitter count of a state and letter

Proof usesPreimage of a set under a letter

Used byTotal predecessor-work bound

TheoremNumber of pops bounded by the total splitter count#✓fully proved

A nonempty popped block pays for its pop, even if its preimage is empty. This bounds the +1 term independently of predecessor visits.

theorem length_le_sum_splitterCount (trace : List (Finset σ × α))
    (hne : ∀ cb ∈ trace, cb.1.Nonempty) :
    trace.length ≤ ∑ b : α, ∑ q : σ, splitterCount q b trace

Uses 1 · Used by 1

Statement usesSplitter count of a state and letter

Used byTotal predecessor-work bound

TheoremTotal predecessor-work bound#✓fully proved

Total predecessor-work bound, including one unit for every pop, for every prefix of the initialized execution. No runtime claim is made for the scanning implementation or for initialization.

theorem hopcroftCost_init_trace_le (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] (k : ℕ) :
    hopcroftCost M (hopcroftSplitters M k (initP M) (initW M)) ≤
      2 * Fintype.card α * Fintype.card σ *
        (Nat.log 2 (Fintype.card σ) + 1)

Uses 10 · Used by 4

Statement usesPredecessor cost of a Hopcroft splitter trace · Trace of splitters popped by Hopcroft's algorithm · Hopcroft's initial partition · Hopcroft's initial waiting list

Proof usesHopcroft predecessor-work as splitter counts plus pops · The invariants hold initially · Number of pops bounded by the total splitter count · Popped Hopcroft splitters are nonempty · Splitter count of a state and letter · Hopcroft visits each of \(n\) states at most \(\log_2 n + 1\) times per letter

Used byPredecessor-work bound for the complete Hopcroft run · Zero Hopcroft predecessor-work over an empty alphabet · \(O(|\Sigma| n \log n)\) bound on Hopcroft predecessor-work · Recorded Hopcroft cost obeys the predecessor-work bound

Theorem\(O(|\Sigma| n \log n)\) bound on Hopcroft predecessor-work#✓fully proved

A uniform O(|Σ| n log n) bound, with the explicit constant 4. The condition n ≥ 2 is essential when absorbing the additive unit into the logarithm. This concerns predecessor-work, not scan runtime.

theorem hopcroftCost_init_trace_le_log (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] (k : ℕ)
    (hn : 2 ≤ Fintype.card σ) :
    hopcroftCost M (hopcroftSplitters M k (initP M) (initW M)) ≤
      4 * Fintype.card α * Fintype.card σ *
        Nat.log 2 (Fintype.card σ)

Uses 5

Statement usesPredecessor cost of a Hopcroft splitter trace · Trace of splitters popped by Hopcroft's algorithm · Hopcroft's initial partition · Hopcroft's initial waiting list

Proof usesTotal predecessor-work bound

TheoremPredecessor-work bound for the complete Hopcroft run#✓fully proved

The bound for the complete terminating minimization execution. DFA.hopcroftLoop_waiting_eq_nil proves this fuel exhausts the queue; hopcroftLoop_eq_hopcroftLoop_of_length ties the trace to its result.

theorem hopcroftCost_complete_le (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] :
    hopcroftCost M (hopcroftSplitters M
      (Fintype.card α * (Fintype.card σ + 1)) (initP M) (initW M)) ≤
        2 * Fintype.card α * Fintype.card σ *
          (Nat.log 2 (Fintype.card σ) + 1)

Uses 5

Statement usesPredecessor cost of a Hopcroft splitter trace · Trace of splitters popped by Hopcroft's algorithm · Hopcroft's initial partition · Hopcroft's initial waiting list

Proof usesTotal predecessor-work bound

TheoremNo initial Hopcroft splitters with at most one state#✓fully proved

With at most one state, the accepting/rejecting split has an empty side, so the algorithm has no initial splitters.

theorem initW_eq_nil_of_card_le_one (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] (hn : Fintype.card σ ≤ 1) :
    initW M = []

Uses 4 · Used by 1

Statement usesHopcroft's initial waiting list

Proof usesBlock of accepting states · Rejecting states · Smaller of two finite sets of states

Used byZero Hopcroft predecessor-work with at most one state

TheoremZero Hopcroft predecessor-work with at most one state#✓fully proved

Zero predecessor-work for zero/one-state boundary parameters. This does not assert that constructing the initial partition costs zero.

theorem hopcroftCost_eq_zero_of_card_le_one (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] (k : ℕ) (hn : Fintype.card σ ≤ 1) :
    hopcroftCost M (hopcroftSplitters M k (initP M) (initW M)) = 0

Uses 5

Statement usesPredecessor cost of a Hopcroft splitter trace · Trace of splitters popped by Hopcroft's algorithm · Hopcroft's initial partition · Hopcroft's initial waiting list

Proof usesNo initial Hopcroft splitters with at most one state

TheoremZero Hopcroft predecessor-work over an empty alphabet#✓fully proved

An empty alphabet causes no predecessor-work, for any state count.

theorem hopcroftCost_eq_zero_of_alphabet_card_eq_zero (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] (k : ℕ) (ha : Fintype.card α = 0) :
    hopcroftCost M (hopcroftSplitters M k (initP M) (initW M)) = 0

Uses 5

Statement usesPredecessor cost of a Hopcroft splitter trace · Trace of splitters popped by Hopcroft's algorithm · Hopcroft's initial partition · Hopcroft's initial waiting list

Proof usesTotal predecessor-work bound

DefinitionHopcroft loop with recorded predecessor-work#✓fully proved

The actual loop with predecessor-visit and pop events recorded in CSLib's TimeM. Pure scans are not charged in this event model.

def hopcroftLoopWork (M : DFA α σ) : ℕ → List (Finset σ) →
    List (Finset σ × α) →
      TimeM ℕ (List (Finset σ) × List (Finset σ × α))
  | 0, P, W => pure (P, W)
  | _ + 1, P, [] => pure (P, [])
  | k + 1, P, (C, a) :: W => do
      TimeM.tick ((preimage M C a).card + 1)
      hopcroftLoopWork M k (roundP M P C a) (roundW M P W C a)

Uses 3 · Used by 4

Statement usesPreimage of a set under a letter · One refinement round of the partition · One update of the waiting list

Used byInstrumented complete Hopcroft run returns the minimization partition · Recorded Hopcroft cost obeys the predecessor-work bound · Instrumented Hopcroft loop returns the original result · Recorded Hopcroft cost equals the work of the popped trace

TheoremInstrumented Hopcroft loop returns the original result#✓fully proved

Instrumentation preserves the exact loop result.

@[simp]
theorem hopcroftLoopWork_ret (M : DFA α σ) (k : ℕ)
    (P : List (Finset σ)) (W : List (Finset σ × α)) :
    (hopcroftLoopWork M k P W).ret = M.hopcroftLoop k P W

Uses 4 · Used by 1

Statement usesHopcroft loop with recorded predecessor-work · Hopcroft's refinement loop

Proof usesOne refinement round of the partition · One update of the waiting list

Used byInstrumented complete Hopcroft run returns the minimization partition

TheoremRecorded Hopcroft cost equals the work of the popped trace#✓fully proved

The recorded cost is exactly the work of the actual popped trace.

@[simp]
theorem hopcroftLoopWork_time (M : DFA α σ) (k : ℕ)
    (P : List (Finset σ)) (W : List (Finset σ × α)) :
    (hopcroftLoopWork M k P W).time =
      hopcroftCost M (hopcroftSplitters M k P W)

Uses 6 · Used by 1

Statement usesPredecessor cost of a Hopcroft splitter trace · Hopcroft loop with recorded predecessor-work · Trace of splitters popped by Hopcroft's algorithm

Proof usesPreimage of a set under a letter · One refinement round of the partition · One update of the waiting list

Used byRecorded Hopcroft cost obeys the predecessor-work bound

TheoremRecorded Hopcroft cost obeys the predecessor-work bound#✓fully proved

The canonical cost monad records the proved total predecessor-work bound for every initialized execution prefix.

theorem hopcroftLoopWork_init_le [Fintype α] (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] (k : ℕ) :
    (hopcroftLoopWork M k (initP M) (initW M)).time ≤
      2 * Fintype.card α * Fintype.card σ *
        (Nat.log 2 (Fintype.card σ) + 1)

Uses 7

Statement usesHopcroft loop with recorded predecessor-work · Hopcroft's initial partition · Hopcroft's initial waiting list

Proof usesPredecessor cost of a Hopcroft splitter trace · Total predecessor-work bound · Recorded Hopcroft cost equals the work of the popped trace · Trace of splitters popped by Hopcroft's algorithm

TheoremInstrumented complete Hopcroft run returns the minimization partition#✓fully proved

At the proved terminating fuel, instrumentation returns the original correct minimization partition and an empty waiting list.

theorem hopcroftLoopWork_complete_ret [Fintype α] (M : DFA α σ)
    [DecidablePred (· ∈ M.accept)] :
    (hopcroftLoopWork M (Fintype.card α * (Fintype.card σ + 1))
      (initP M) (initW M)).ret = (M.hopcroftPartition, [])

Uses 7

Statement usesHopcroft loop with recorded predecessor-work · Hopcroft's initial partition · Hopcroft's initial waiting list · Hopcroft's partition

Proof usesInstrumented Hopcroft loop returns the original result · Hopcroft's refinement loop · Hopcroft's waiting list is exhausted

66 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.