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)

Comienza en Lck/Regex/Glushkov/Construction.lean, en Symbol.matches, y compáralo con charMatchesClass en Syntax.lean. Después inspecciona el have h_eq de enlace en Lck/Regex/Glushkov/CompositionCorrectness.lean; se considera terminado cuando se haya eliminado la duplicación y simplificado la demostración sin cambiar el comportamiento de matching.