proof: add bridge theorem connecting search-mode Matches dr.toRegex to MatchesSubstring ast
まだ誰も着手していません。
評価
- 難易度
- 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 にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- 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
-
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
-
internal.h中，漏掉了1个定义。 オープン
難易度 1/5 1時間未満 初心者へのやさしさ 95/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 88/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 88/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 88/100
oxc-project/oxc#26944 ·