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)

Inizia in Lck/Regex/Glushkov/Construction.lean, in Symbol.matches, e confrontalo con charMatchesClass in Syntax.lean. Poi esamina il have h_eq di collegamento in Lck/Regex/Glushkov/CompositionCorrectness.lean; il lavoro è completato quando la duplicazione è stata rimossa e la dimostrazione è stata semplificata senza modificare il comportamento del matching.