Grammar proofs, extensions: Coq parser port + §7.1 not-regular (from scratch)#104
Merged
Merged
Conversation
…arity)
WokeGrammarParser.v mirrors WokeGrammar.lean's expression-grammar proofs in
Coq 8.18.0: a faithful fuel-based precedence-climbing parser + the concrete
precedence/associativity/rejection battery + 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. CI-gated via coq-proofs.yml.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL
…igeonhole) WokeGrammarRegular.lean proves grammar-proofs.md §7.1 (the WokeLang expression language is not regular) without Mathlib: - a bespoke finite pigeonhole proved from scratch in core Lean; - a Fin k DFA model (runFrom, runFrom_append); - the fooling-set / pigeonhole argument on a^n b^n (the combinatorial heart of the pumping lemma): among k+1 prefixes a^0..a^k two reach the same state, so a^j b^i reaches the same final state as the accepted a^i b^i, forcing the DFA to accept a^j b^i (j != i) which is not in the language — contradiction. a^n b^n is isomorphic to the grammar's balanced nesting (^n x )^n, so the expression language is non-regular. sorry-free (classical-logic axioms only); CI-gated via lean-proofs.yml. The prose §7 note and GRAMMAR-PROOF-INVENTORY.md are updated (T7.1 now machine-checked; §7.3 CFL closure remains scoped). 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 22:13
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 and #103, delivering the two scoped extensions. Both new files
are CI-gated and axiom-free (
Print Assumptions/#print axiomschecked).Extension A — Coq port of the universal parser proof (
WokeGrammarParser.v)Full Coq 8.18.0 mirror of
WokeGrammar.lean: a faithful fuel-basedprecedence-climbing parser, the concrete precedence/associativity/rejection
battery, and the universal round-trip —
prefix_rt(the parser inverts the fully-parenthesised rendererrp),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") — evencleaner 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:
Fin kDFA model (runFrom,runFrom_append);aⁿbⁿ(the combinatorial heart ofthe pumping lemma): among
a⁰..aᵏtwo prefixes reach the same state, soaʲbⁱreaches the same final state as the accepted
aⁱbⁱ, forcing the DFA to acceptaʲbⁱ ∉ L— contradiction.aⁿbⁿ ≅ (ⁿ x )ⁿ, the grammar's balanced-nesting sublanguage, so the WokeLangexpression language is non-regular.
sorry-free (classical-logic axioms only).The prose §7 note and
GRAMMAR-PROOF-INVENTORY.mdare 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
Derivesrelation + relabelingreflection 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.ymlgain steps for the two new files. Local: allfive grammar-proof files (3 Lean + 2 Coq) compile exit-0; axiom footprints verified.
🤖 Generated with Claude Code
https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL
Generated by Claude Code