Grammar structural proofs: no-left-recursion (+ discrepancy), lexer, classification (Lean + Coq)#103
Merged
Conversation
…screpancy), lexer, classification (Lean + Coq) Follow-up to #102. Mechanizes the remaining grammar claims from grammar-proofs.md in priority order, with Lean↔Coq parity on the structural results. New, CI-gated (lean-proofs.yml / coq-proofs.yml), sorry/admit-free. docs/proofs/verification/WokeGrammarStructure.lean (Lean 4.30.0): - T2.1 no left recursion, WHOLE grammar: the begins-with-first-nonterminal graph as data + a strictly-decreasing rank ⇒ no nonterminal reaches itself. no_left_recursion depends on NO axioms. - Discrepancy found and machine-checked: the grammar as literally written DOES have one left-recursive production — the guard pattern `pattern = … | pattern "when" expression` — which the parser does not implement (the grammar's own NOTE). The prose §2.1 blanket "no left recursion" is corrected in-place. - T4.1 maximal munch + T4.2 keyword priority: a word scanner with general longest-match and keyword-on-exact-match lemmas + kernel-decided concretes (remember↦keyword, remembering↦one identifier, remember(↦keyword then stop). - T1.2 LL(1)=NO / T2.3 LL(2)=YES: the x vs x(…) FIRST/FIRST conflict and its two-token resolution (mirrors the parser's peek=='(' branch). docs/proofs/verification/WokeGrammarStructure.v (Coq 8.18.0): - Coq mirror of no-left-recursion (+ guard discrepancy) and the LL classification. Print Assumptions: axiom-free ("Closed under the global context"). Docs: GRAMMAR-PROOF-INVENTORY.md records P2/P3/P4 + the Coq mirror, and honestly FLAGS the §7 formal-language-theory claims (T7.1 not-regular, §7.3 CFL closure) as general REG/CFL facts needing an automata library (Mathlib) unavailable in the offline single-file setup — recorded rather than stubbed. grammar-proofs.md gets the in-place §2.1 correction and a §7 mechanization-status note. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL
hyperpolymath
marked this pull request as ready for review
June 26, 2026 21:49
hyperpolymath
added a commit
that referenced
this pull request
Jun 26, 2026
…scratch) (#104) Follow-up to #102 and #103, delivering the two scoped extensions. Both new files are CI-gated and **axiom-free** (`Print Assumptions` / `#print axioms` checked). ## Extension A — Coq port of the universal parser proof (`WokeGrammarParser.v`) Full Coq 8.18.0 mirror of `WokeGrammar.lean`: a faithful fuel-based precedence-climbing parser, the concrete precedence/associativity/rejection battery, and the universal round-trip — - `prefix_rt` (the parser inverts the fully-parenthesised renderer `rp`), - `parse_closed`, `completeness_rp` (`∀ e, parseAll (rp e) = Some e`), - `parse_deterministic` (unambiguity), `rp_injective`. `Print Assumptions`: all **axiom-free** ("Closed under the global context") — even cleaner than the Lean development. Lean and Coq now carry the parser metatheory at full parity. ## Extension B — §7.1 not regular, from scratch (`WokeGrammarRegular.lean`) Mathlib has the automata library but it's unavailable offline (egress-blocked), so this is built from scratch in core Lean: - a **bespoke finite pigeonhole** (proved by induction, collapsing the codomain); - a `Fin k` **DFA** model (`runFrom`, `runFrom_append`); - the **fooling-set / pigeonhole argument** on `aⁿbⁿ` (the combinatorial heart of the pumping lemma): among `a⁰..aᵏ` two prefixes reach the same state, so `aʲbⁱ` reaches the same final state as the accepted `aⁱbⁱ`, forcing the DFA to accept `aʲbⁱ ∉ L` — contradiction. `aⁿbⁿ ≅ (ⁿ x )ⁿ`, the grammar's balanced-nesting sublanguage, so the WokeLang expression language is non-regular. `sorry`-free (classical-logic axioms only). The prose §7 note and `GRAMMAR-PROOF-INVENTORY.md` are updated accordingly. ## Honestly scoped **§7.3 CFL closure / non-closure** remains the one un-mechanized item: it is a general fact about the *class* CFL (not this grammar) requiring a full grammar-derivation module (a 3-way mutual `Derives` relation + relabeling reflection lemmas for each construction; the negative direction additionally needs the CFL pumping lemma). Recorded in the inventory rather than stubbed. Happy to do it as a dedicated follow-up. ## CI `lean-proofs.yml` / `coq-proofs.yml` gain steps for the two new files. Local: all five grammar-proof files (3 Lean + 2 Coq) compile exit-0; axiom footprints verified. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL --- _Generated by [Claude Code](https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Follow-up to #102 (merged). Continues mechanizing the grammar claims from
grammar-proofs.mdin priority order, with Lean↔Coq parity on the structuralresults. All new files are CI-gated and
sorry/admit-free; the headlinetheorems are axiom-free.
What's proved
WokeGrammarStructure.lean(Lean 4.30.0):no_left_recursion : ∀ a, ¬ Reach a a— depends on no axiomspattern = … | pattern "when" expression(guard_pattern_is_left_recursive). The prose §2.1 blanket "no left recursion" is false as written — corrected in place. The parser doesn't implement the guard alt (the grammar's own NOTE), sono_left_recursionholds for the implemented grammar.munch_maximal(longest-match) +kw_priority, plus kernel-decided concretes (remember↦keyword,remembering↦one identifier,remember(↦keyword then stop)not_LL1(thexvsx(…)FIRST/FIRST conflict) +LL2_separates(two tokens decide — mirrors the parser'speek=='('branch)WokeGrammarStructure.v(Coq 8.18.0): Coq mirror of no-left-recursion (+ theguard discrepancy) and the LL classification.
Print Assumptions→ axiom-free("Closed under the global context").
Honestly flagged (not faked) — §7 formal-language-theory
T7.1not-regular (pumping) and §7.3 CFL closure/non-closure are general factsabout the classes REG/CFL, not this grammar, and need an automata library
(Mathlib
Computability.*) that the repo's deliberately Mathlib-free, offline,single-file prover setup doesn't provide. Recorded in
GRAMMAR-PROOF-INVENTORY.mdrather than stubbed; the combinatorial kernel(unbounded balanced nesting) is exercised concretely in
WokeGrammar.lean.CI
lean-proofs.ymlandcoq-proofs.ymlgain steps for the new files (the existingLean/Coq proofs continue to be gated). Local: both compile exit-0;
#print axioms/Print Assumptionsconfirm the axiom footprints above.Draft for review.
🤖 Generated with Claude Code
https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL
Generated by Claude Code