refactor: deduplicate Symbol.matches / charMatchesClass in Glushkov

Problem

Symbol.matches (Construction.lean:138) reimplements the same character-class matching logic already present in charMatchesClass (Syntax.lean:74). This duplication has been noticed in a correctness proof: CompositionCorrectness.lean even contains an explicit bridging lemma:

have h_eq : Symbol.matches ... = charMatchesClass c ranges.ranges ...

Proposed fix

Rewrite Symbol.matches to delegate to charMatchesClass, eliminating the duplication:

def Symbol.matches (sym : Symbol) (c : Char) : Bool :=
  match sym with
  | Symbol.charClass ranges negated => charMatchesClass c ranges.ranges negated

The bridging have h_eq lemma in CompositionCorrectness becomes trivial (or can be removed via rfl/simp).

Impact

Low risk. Symbol.matches is called internally by the Glushkov matcher. The semantics are identical by construction — the existing bridge lemma proves this. No API change.

Scope

• Lck/Regex/Glushkov/Construction.lean
• Lck/Regex/Glushkov/CompositionCorrectness.lean (remove/simplify bridge lemma)

Beginne in Lck/Regex/Glushkov/Construction.lean bei Symbol.matches und vergleiche es mit charMatchesClass in Syntax.lean. Untersuche anschließend das verbindende have h_eq in Lck/Regex/Glushkov/CompositionCorrectness.lean; als abgeschlossen gilt die Aufgabe, wenn die Duplizierung entfernt und der Beweis vereinfacht wurde, ohne das Matching-Verhalten zu ändern.