release 202507

作業内容

簡約の各種性質の証明

• 2.2 Proposition3.a(reduced form): https://github.com/proof-ninja/coq-scurve/blob/202507/theories/Reduction.v#L316
• 2.4 Proposition4(合流性): https://github.com/proof-ninja/coq-scurve/blob/202507/theories/Reduction.v#L537

Admissibleでない例示

• 補題 all_e_swcc

Admissibleの簡約形の列挙

• 必要な補題と全体の設計
• 定理の言明と証明: https://github.com/proof-ninja/coq-scurve/blob/202507/theories/Admissible.v#L76

作業内容の詳細

• 3.a reduced form by @y-tak6 in #54
• fix some issues about 3.a by @y-tak6 in #55
• repeat_last_P by @yoshihiro503 in #56
• resolve prefix_brothers_is_prefix by @y-tak6 in #57
• address import warnings by @hiroshi-cl in #58
• fix example2 and issues by @y-tak6 in #59
• fix reduced_form, #60 by @y-tak6 in #61
• reduced_admissibles_form by @y-tak6 in #64

New Contributors

• @hiroshi-cl made their first contribution in #58

Full Changelog: 202506...202507

release 202506

作業内容

1. 特定の scurve が許容可能でないことの証明

• セグメント4個の場合の許容可の出ない例の証明: https://github.com/proof-ninja/coq-scurve/blob/202506/theories/Main.v#L463
• セグメント5個の場合の許容可の出ない例の証明: https://github.com/proof-ninja/coq-scurve/blob/202506/theories/Example3.v#L43
• 1.1 セグメント数5個の場合の証明と4個の場合の証明の併合 (' のついている補題等）: https://github.com/proof-ninja/coq-scurve/blob/202506/theories/Example3.v
• 1.2 IUKM2025の Fig.6 でNGとされたセグメント数7個の例が許容可能でないことの証明: https://github.com/proof-ninja/coq-scurve/blob/202506/theories/Example2.v#L185
• Axiom等の調整や必要な補題の証明

2. 簡約の各種性質の証明 (Git 内 Issues で open になっているもの)

• 2.1 Proposition1(停止性): https://github.com/proof-ninja/coq-scurve/blob/59a1de3c1cf15b0ff5fcf7c4ddbea3f0ed770dde/theories/Reduction.v#L183
• Proposition 2 rotation difference preservation : https://github.com/proof-ninja/coq-scurve/blob/59a1de3c1cf15b0ff5fcf7c4ddbea3f0ed770dde/theories/Reduction.v#L198
• 2.2 Proposition3.a(reduced form)
• 2.3 Proposition3.b(両端のシンボル): https://github.com/proof-ninja/coq-scurve/blob/59a1de3c1cf15b0ff5fcf7c4ddbea3f0ed770dde/theories/Reduction.v#L135
• 2.4 Proposition4(合流性): https://github.com/proof-ninja/coq-scurve/blob/59a1de3c1cf15b0ff5fcf7c4ddbea3f0ed770dde/theories/Reduction.v#L382

変更の詳細

• 📝 Introduce README.md by @yoshihiro503 in #1
• CI: 👷 Automatically Build and Deploy html doc using Rocqnavi by @yoshihiro503 in #2
• configure.sh を追加した by @cedretaber in #4
• .gitignore を追加した by @cedretaber in #5
• CI: Automatically build the project by @yoshihiro503 in #6
• ✨ Prove consisit_init_term by @yoshihiro503 in #7
• CI: 👷 🧑‍💻 Delete generate_docs.yml by @yoshihiro503 in #9
• PrimitiveSegment を別ファイルに分離 by @cedretaber in #8
• chore: 🔧 👷 Introduce The Opam File by @yoshihiro503 in #11
• 向きの簡約処理を追加 by @cedretaber in #3
• 向きの回転差保持 by @cedretaber in #18
• ✨ introduce Sample3 by @yoshihiro503 in #17
• feat: 🎨 Improved to make is_scurve proofs easier. by @yoshihiro503 in #19
• feat: Prop. 4. the local confluence by @yoshihiro503 in #35
• Lemma ReduceDirStep_length を追加 by @cedretaber in #37
• Definition all_sublists を追加 by @cedretaber in #38
• Fix all_prefix. by @cedretaber in #41
• ✨ 👔 strong normalization of ReduceDirStep by @yoshihiro503 in #43
• コードの整理 by @y-tak6 in #36
• ✨ Now, we can (xs =? ys) for Direction lists xs ys. by @yoshihiro503 in #44
• ✨ List all overlap reduction patterns. by @yoshihiro503 in #45
• Yoshihiro503@reduce dir local confluence aux by @yoshihiro503 in #46
• About prefix and sublists #42, #26(#39, #40), #27 by @y-tak6 in #47
• Proposition 3. b. 両端のシンボル +- は ReduceDirで変わらない by @cedretaber in #48
• 停止性のマイルストーンの残りを証明 by @y-tak6 in #50

New Contributors

• @yoshihiro503 made their first contribution in #1
• @cedretaber made their first contribution in #4
• @y-tak6 made their first contribution in #36

Full Changelog: https://github.com/proof-ninja/coq-scurve/commits/202506