Commit 2025-06-07 07:26 a8c0ebf8

View on Github →

feat(Computability/NFA): add a Path API (#25321) The Path API allows for proofs that speak about a particular path through an NFA, with constructions that depend on the specific states the path passes through, rather than just the abstract existence of such a path, which is what evalFrom computes. This is the part of the API that proved uncontroversial, extracted out of #23929.

Estimated changes

Modified Mathlib/Computability/DFA.lean

Modified Mathlib/Computability/NFA.lean

added def NFA.Path.supp

added inductive NFA.Path

added theorem NFA.accepts_iff_exists_path

added theorem NFA.evalFrom_biUnion

added theorem NFA.evalFrom_cons

added theorem NFA.evalFrom_eq_biUnion_singleton

added theorem NFA.mem_evalFrom_iff_exists

added theorem NFA.mem_evalFrom_iff_nonempty_path

added theorem NFA.stepSet_singleton