proof: add bridge theorem connecting search-mode Matches dr.toRegex to MatchesSubstring ast
还没有人认领这个 Issue。
评估
- 难度
- 4/5
- 预计耗时
- 3-5 天
- 新手友好度
- 45/100
- Issue 类型
- 功能
- 描述清晰度
- 基本清楚
- 活跃度
- 停滞
- 领域
- compilers
调研方向
从 Lck/Regex/RegexSpec.lean 开始，阅读 regex_search_correct 和现有的 desugar_fullMatch_semantics 桥接。跟踪 .* 包装如何将 Matches dr.toRegex 与 MatchesSubstring ast 联系起来，然后证明所述的 regex_search_ast_correct 等价性。完成标准是定理能够编译，并将搜索模式的结果与原始 AST 语义连接起来。
由索引模型根据 Issue 内容生成。
描述
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.
- 主要语言
- Lean
- 星标
- 2
- 派生
- 1
- PR 合并指标
- 30 天内没有已合并 PR
贡献指南
这个仓库没有索引到贡献指南
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
lambdaclass/lambda_compiler_kit 的其他 Issue
-
难度 1/5 1 小时以内 新手友好度 72/100
-
难度 1/5 1 小时以内 新手友好度 68/100
-
难度 2/5 1-3 小时 新手友好度 68/100
-
enhancement
难度 4/5 3-5 天 新手友好度 48/100
-
难度 2/5 1-3 小时 新手友好度 50/100
查看 lambdaclass/lambda_compiler_kit 的全部 Issue
相似的 Issue
-
bug
难度 2/5 1-3 小时 新手友好度 75/100
bradcypert/plum#58 ·
-
flang:fir-hlfir
难度 2/5 1-3 小时 新手友好度 70/100
llvm/llvm-project#225935 ·
-
area:cards hand-tail ready-for-agent
难度 2/5 1-3 小时 新手友好度 65/100
fil-donadoni/tolaria#4446 ·
-
难度 2/5 1-3 小时 新手友好度 75/100
objectionary/eo#8923 ·
-
难度 2/5 1-3 小时 新手友好度 75/100