Migrate tests from hand-rolled IO to LSpec framework

Summary

The current test suite uses hand-rolled IO Unit functions with manual IO.println "✓" / throw "✗" for pass/fail reporting. This reimplements scaffolding that existing Lean 4 testing frameworks already provide.

Current state

• 67 tests across ParserTest.lean, NfaTest.lean, MatcherTest.lean
• Each test is a def testFoo : IO Unit that manually prints results
• test/Main.lean calls each test function sequentially
• No structured output, no test counts, no failure summaries

Recommended approach: LSpec

LSpec is the standard Lean 4 testing framework. Tests become declarative assertions:

import LSpec
import Lck.Regex.Parser

def parserSuite := [
    test "single char" (parse "a" = Except.ok (Regex.char 'a')),
    test "reversed range fails" (parse "[z-a]" matches Except.error _),
    test "empty pattern" (parse "" = Except.error RegexError.emptyPattern)
  ]

def main := lspecIO $ .ofList [
    ("parser", parserSuite),
    ("matcher", matcherSuite)
  ]

Benefits:

• Eliminates ~200 lines of boilerplate (manual IO.println/throw per test)
• Structured pass/fail output with counts and summaries
• Standard lake test integration via testDriver
• Consistent with Lean ecosystem conventions

Other approaches worth considering

• #guard: Built-in compile-time assertions (#guard parse "a" = Except.ok (Regex.char 'a')). Zero boilerplate, failures are compilation errors. Good for simple invariants alongside LSpec.
• SlimCheck/Plausible: Property-based testing for discovering edge cases automatically. Could complement LSpec for properties like "any regex that parses successfully can be compiled to an NFA".

Migration plan

1. Add LSpec dependency to lakefile.toml
2. Convert each testFoo : IO Unit to an LSpec test "name" (assertion)
3. Group tests into suites by module
4. Wire up main := lspecIO $ .ofList [...]
5. Configure testDriver in lakefile
6. Remove manual IO scaffolding

まず test/ParserTest.lean、test/NfaTest.lean、test/MatcherTest.lean、test/Main.lean を読んで、既存の67個のテストと現在のエントリポイントを理解します。次に lakefile.toml と LSpec の統合要件を確認します。テストがグループ化された LSpec スイートを使用し、lake test が構造化された結果を提供し、手動の IO スキャフォールディングが削除されていれば完了です。