Machine-checked grammar proofs (Lean) + grammar reconciliation#102
Merged
Conversation
…onciliation Reconcile the grammar to a single source of truth and add the first machine-checked proofs ABOUT the grammar (the prose in grammar-proofs.md was never run by any prover). Grammar reconciliation: - grammar/wokelang.ebnf is canonical, verified against the live src/lexer + src/parser (identifier rule [a-zA-Z][a-zA-Z0-9_]*, while/break/continue, lambdas, record literals, field access, function types). Added its missing SPDX header. - spec/grammar.ebnf was a stale subset falsely claiming to supersede it; it is now a generated synchronized copy. Drift is guarded by scripts/check-grammar-sync.sh (wired into tests/e2e.sh) so the two can never silently diverge again. Lean 4.30.0 proofs (docs/proofs/verification/WokeGrammar.lean), CI-gated via lean-proofs.yml, sorry/admit/native_decide-free; #print axioms shows only propext + Quot.sound (no Classical.choice, no compiler trust): - a faithful precedence-climbing parser mirroring parse_precedence/parse_infix/ parse_prefix (levels None=0..Call=8, strict < => left associativity); - T3.3 termination (total function), T6.1 precedence + T6.3 associativity (kernel-decide battery), T3.2 completeness (completeness_rp: every expression's concrete syntax parses back, universal, via prefix_rt), T2.2 unambiguity (parse_deterministic + rp_injective), and a rejection battery witnessing T3.1 no-over-acceptance. GRAMMAR-PROOF-INVENTORY.md records the full claim-by-claim map (what is proven, what is concretely witnessed, what is honestly flagged as out of reach). 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:13
hyperpolymath
added a commit
that referenced
this pull request
Jun 26, 2026
…classification (Lean + Coq) (#103) Follow-up to #102 (merged). Continues mechanizing the grammar claims from `grammar-proofs.md` in priority order, with **Lean↔Coq parity** on the structural results. All new files are CI-gated and `sorry`/`admit`-free; the headline theorems are **axiom-free**. ## What's proved **`WokeGrammarStructure.lean`** (Lean 4.30.0): | Claim | Result | |---|---| | **T2.1 no left recursion** (whole grammar) | begins-with-first-nonterminal graph as data + strictly-decreasing rank ⇒ `no_left_recursion : ∀ a, ¬ Reach a a` — **depends on no axioms** | | **Discrepancy found** | the grammar *as written* HAS a left-recursive production: the guard pattern `pattern = … \| 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), so `no_left_recursion` holds for the implemented grammar. | | **T4.1 maximal munch / T4.2 keyword priority** | general `munch_maximal` (longest-match) + `kw_priority`, plus kernel-`decide`d concretes (`remember`↦keyword, `remembering`↦*one* identifier, `remember(`↦keyword then stop) | | **T1.2 LL(1)=✗ / T2.3 LL(2)=✓** | `not_LL1` (the `x` vs `x(…)` FIRST/FIRST conflict) + `LL2_separates` (two tokens decide — mirrors the parser's `peek=='('` branch) | **`WokeGrammarStructure.v`** (Coq 8.18.0): Coq mirror of no-left-recursion (+ the guard discrepancy) and the LL classification. `Print Assumptions` → **axiom-free** ("Closed under the global context"). ## Honestly flagged (not faked) — §7 formal-language-theory `T7.1` not-regular (pumping) and §7.3 CFL closure/non-closure are general facts about 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.md` rather than stubbed; the combinatorial kernel (unbounded balanced nesting) is exercised concretely in `WokeGrammar.lean`. ## CI `lean-proofs.yml` and `coq-proofs.yml` gain steps for the new files (the existing Lean/Coq proofs continue to be gated). Local: both compile exit-0; `#print axioms`/`Print Assumptions` confirm the axiom footprints above. Draft for review. 🤖 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>
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.
What & why
The task was to check the proofs for the grammar and make sure the necessary
and sufficient ones exist, installing the provers and only reporting proofs
actually run. The honest starting picture:
(
docs/proofs/formal-semantics/grammar-proofs.md) were informal prose. Themachine-checked
WokeLang.{lean,v}cover the type system, not the grammar.grammar/wokelang.ebnfandspec/grammar.ebnf) each declared themselves canonical and disagreed.Provers were installed and the existing proofs were run as a baseline first:
Coq 8.18.0 and Lean 4.30.0 both compile clean (the Lean toolchain is fetched
directly from the GitHub release because the
lean-lang.orgresolver hosts areblocked by egress policy — same source
lean-proofs.ymlalready uses).Grammar reconciliation
grammar/wokelang.ebnfis canonical — verified against the livesrc/lexer+src/parser(identifier rule[a-zA-Z][a-zA-Z0-9_]*,while/break/continue, lambdas, record literals, field access, function types — all presentin the parser and in this file, all absent from the stale
spec/grammar.ebnfsnapshot).
spec/grammar.ebnfis now a generated synchronized copy; drift isguarded by
scripts/check-grammar-sync.sh(wired intotests/e2e.sh). Added thecanonical grammar's missing SPDX header.
Machine-checked proofs —
docs/proofs/verification/WokeGrammar.leanLean 4.30.0, CI-gated (
lean-proofs.yml),sorry/admit/native_decide-free;#print axiomsshows onlypropext+Quot.sound(noClassical.choice, nocompiler trust). A faithful precedence-climbing parser mirroring the real
parse_precedence/parse_infix/parse_prefix(levelsNone=0..Call=8, strict<⇒ left-associativity), with:decidebattery (1+2*3↦1+(2*3),1-2-3↦(1-2)-3, full ladder, grouping, unary)completeness_rp : ∀ e, parseAll (rp e) = some e(universal, viaprefix_rt)parse_deterministic+rp_injectiveGRAMMAR-PROOF-INVENTORY.mdis the claim-by-claim map of what is proven, what isconcretely witnessed, and what is honestly flagged.
Still in progress on this branch
P2 whole-grammar no-left-recursion (a real discrepancy is already visible — the
pattern "when" expressionguard production is left-recursive, contradicting theprose's blanket §2.1 claim), P3 lexer maximal-munch/keyword-priority, P4
classification, P5/P6 CFL/regularity, and the Coq mirror. Draft until those land.
🤖 Generated with Claude Code
https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL
Generated by Claude Code