lambdaclass / lambdaclass/lambda_compiler_kit
proof: add bridge theorem connecting search-mode Matches dr.toRegex to MatchesSubstring ast
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 2
- Forks
- 1
- PR merge metrics
- No merged PRs in 30d
Description
Problem
regex_search_correct in Lck/Regex/RegexSpec.lean states correctness in terms of Matches dr.toRegex input (the desugared form) rather than MatchesSubstring ast input (the original AST).
The full-match variant has desugar_fullMatch_semantics for this bridge, but search mode does not.
Goal
Prove a theorem of the form:
theorem regex_search_ast_correct (pattern input : String) :
Regex.search pattern input = .ok true ↔
(∃ ast, parse pattern = .ok ast ∧ MatchesSubstring ast input)
This requires connecting the .*-wrapped desugared form back to MatchesSubstring.
References
Raised in AI code review.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start in Lck/Regex/RegexSpec.lean by reading regex_search_correct and the existing desugar_fullMatch_semantics bridge. Trace how the .* wrapping relates Matches dr.toRegex to MatchesSubstring ast, then prove the stated regex_search_ast_correct equivalence. Done means the theorem compiles and connects search-mode results to the original AST semantics.
Written by the indexing model from the issue text.
Assessment
- Domain
- compilers
- Issue type
- Feature
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 45/100