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/)

Inizia da cli/Lck.Grep.lean, Lck/Regex.lean e dal motore Glushkov in Lck/Regex/Glushkov/. Esponi Glushkov.build, sostituisci le chiamate a Thompson NFA ed esegui gli esempi o test esistenti in test/ per confrontare il comportamento di grep. Il lavoro è completato quando la CLI utilizza il motore verificato e le proprietà verificate formalmente sono documentate.