Integrate Glushkov NFA engine into lck-grep CLI utility

Summary

The cli/Lck.Grep.lean CLI utility currently has a hardcoded Thompson NFA implementation for proof-of-concept. We now have a verified Glushkov NFA engine with formal correctness proofs.

Goal

Replace the Thompson PoC with the verified Glushkov engine:

• Use Glushkov.build to compile regexes to NFAs
• Verify that the Glushkov engine produces equivalent results
• Validate against existing test cases in cli/

Implementation steps

1. Expose Glushkov.build in Lck/Regex.lean
2. Replace Thompson NFA calls with Glushkov.build
3. Run existing grep tests to confirm behavior equivalence
4. Document which properties are now formally verified

Related

• Glushkov NFA file: Lck/Regex/Glushkov/
• CLI entry point: cli/Lck.Grep.lean
• Test suite: (existing example usage in test/)

Beginne mit cli/Lck.Grep.lean, Lck/Regex.lean und der Glushkov-Engine unter Lck/Regex/Glushkov/. Mache Glushkov.build verfügbar, ersetze die Aufrufe der Thompson NFA und führe die vorhandenen Beispiele oder Tests in test/ aus, um das grep-Verhalten zu vergleichen. Die Aufgabe ist erledigt, wenn die CLI die verifizierte Engine verwendet und die formal verifizierten Eigenschaften dokumentiert sind.