Prove equivalence between AST-level and Expr-level regex semantics (`captures_iff_captures`)

(This issue is AI-generated an may contain an error. Please comment on the issue to discuss what we'll prove)

Difficulty: Intermediate

Background

Two levels of regex semantics are defined in the ast-semantics branch:

1. AST-level (Ast.Captures in correctness/RegexCorrectness/Syntax/Semantics.lean): closer to the surface pattern syntax, directly handles repeat with min/max bounds.
2. Expr-level (Expr.Captures in correctness/RegexCorrectness/Data/Expr/Semantics/Captures.lean): a lowered representation using star, more suitable as an NFA compilation source.

The conversion from AST to Expr is done by Ast.toRegexAux in regex/Regex/Syntax/Ast.lean, which uses applyRepetitions to translate (un)bounded repetitions.

Goal

Prove the equivalence statement

theorem captures_iff_captures {currentGroup it it' groups e} :
  Ast.Captures currentGroup it it' groups e ↔ Expr.Captures it it' groups (e.toRegexAux currentGroup).2

so that the AST-level semantics of a pattern agrees with the Expr-level semantics.

Key Challenges

1. Repetition translation

• applyRepetitions converts repeat min max greedy e into various Expr combinations:
  • star for unbounded repetitions (max = .none)
  • nested concat/alternate via repeatConcat for bounded cases
• One needs to show semantic equivalence between the AST-level repeat rules and these Expr-level encodings, case by case.

2. Group numbering consistency

• The AST semantics threads an explicit currentGroup : Nat parameter that is incremented as groups are traversed, while the Expr syntax embeds group tags directly.
• It must be shown that toRegexAux produces a consistent tagging scheme, and that Ast.Captures/Expr.Captures agree on which groups are captured where.

3. CaptureGroups structure

• The inductive CaptureGroups type must line up between the two semantics:
  • .group should agree on tag, start, and end positions.
  • .concat should agree on how left/right capture groups are combined.
• Alternatively, we can prove a weaker theorem that the groups are equivalent under the "last-write-win" interpretation.

Proof Strategy

Induction on the semantics is expected to be a key proof technique. In particular, it may be necessary to identify and maintain suitable invariants (e.g. about currentGroup ranges) to carry the proof through the group, alternate, concat, and repeat cases.

Notes

• The exact definitions may need adjustment during proof development (especially around repeat and group indexing).
• In particular, the currentGroup threading and the CaptureGroups constructors might need small tweaks if the current formulation makes invariants hard to state or prove.
• The example around lines 43–54 in Semantics.lean serves as a sanity check that min > max is impossible for the AST-level repeat semantics.

Tasks

• Prove the forward direction (Ast.Captures → Expr.Captures).
• Prove the backward direction (Expr.Captures → Ast.Captures).
• Adjust or refine the definitions as needed to make the proofs go through cleanly (while preserving the intended semantics).