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)

Start in Lck/Regex/Glushkov/Construction.lean at Symbol.matches and compare it with charMatchesClass in Syntax.lean. Then inspect the bridging have h_eq in Lck/Regex/Glushkov/CompositionCorrectness.lean; done means the duplication is removed and the proof is simplified without changing matching behavior.