From 698fcdc5568209fe73c924a609e64d37be7c412d Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 18:26:08 +0000 Subject: [PATCH 1/4] docs: add RESUME.md (pick-up notes for continuing on another machine) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Authoritative snapshot for resuming the grammar-proofs work elsewhere (e.g. the desktop app): current state, the full proof inventory with last verification status, exact Lean 4.30.0 / Coq 8.18.0 reinstall steps, the next increment (§7.3 ∩/¬ non-closure via cfl_pumping), CI notes, and the teleport pointer. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL --- RESUME.md | 115 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 RESUME.md diff --git a/RESUME.md b/RESUME.md new file mode 100644 index 0000000..4dd84bc --- /dev/null +++ b/RESUME.md @@ -0,0 +1,115 @@ + + + +# RESUME — grammar formal-proofs work + +Pick-up notes for continuing the `claude/v2-grammar-proofs-audit-1yqgxh` work on +another machine (e.g. the Claude Code desktop app). Everything here is committed +to that branch, so it travels with the code. + +## Where the work stands + +Goal: machine-check every necessary/sufficient proof for the grammar that exists +in this repo (`grammar/wokelang.ebnf`), install the provers, and report only +proofs that actually run. The grammar was reconciled to one source of truth, and +the proof obligations were mechanized in Lean 4 (mirrored to Coq where sensible). + +**Open PR:** #106 — *CFL pumping lemma, machine-checked from scratch in Lean* +(branch `claude/v2-grammar-proofs-audit-1yqgxh`). + +**Merged on the way here:** #102 (parser metatheory + grammar reconciliation), +#103 (no-left-recursion + lexer + classification, Lean+Coq), #104 (Coq parser +port + §7.1 not-regular), #105 (§7.3 CFL positive closure). + +## Proof inventory — all verified green (last full run in the cloud container) + +Single-file, Mathlib-free. `lean ` / `coqc ` must exit 0 with no errors. + +| File | What it proves | Status | +|---|---|---| +| `docs/proofs/verification/WokeLang.lean` / `.v` | core language metatheory (sorry-audit resolved) | ✅ | +| `docs/proofs/verification/WokeGrammar.lean` | Pratt-parser metatheory: prefix/completeness/determinism/injectivity | ✅ | +| `docs/proofs/verification/WokeGrammarStructure.lean` / `.v` | no-left-recursion (+ found a real spec bug in `pattern`), lexer maximal-munch + keyword priority, CFG/¬LL(1)/LL(2) classification | ✅ | +| `docs/proofs/verification/WokeGrammarParser.v` | Coq port of the parser metatheory | ✅ | +| `docs/proofs/verification/WokeGrammarRegular.lean` | §7.1 not-regular: bespoke pigeonhole + `Fin k` DFA + fooling set on `aⁿbⁿ` | ✅ | +| `docs/proofs/verification/WokeGrammarCFL.lean` | §7.3 CFL **positive** closure under ∪, ·, * | ✅ | +| `docs/proofs/verification/WokeGrammarPumping.lean` | **CFL pumping lemma** `cfl_pumping` (the Mathlib-gap result) | ✅ | + +Trust base for the proofs: the standard classical kernel constants only +(`propext`, `Classical.choice`, `Quot.sound`) — no holes, no project-specific +assumptions. Confirm with Lean's kernel-dependency printout per file. + +The claim-by-claim map lives in +`docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md`. + +## How to re-run the provers locally + +The provers are NOT in the repo — they were installed in the (ephemeral) cloud +container. Reinstall the pinned versions locally. + +### Lean 4.30.0 (pinned by `docs/proofs/verification/lean-toolchain`) + +The exact, Mathlib-free steps are in `.github/workflows/lean-proofs.yml`: + +```sh +ver=4.30.0 +curl -sSL -o /tmp/lean.tar.zst \ + "https://github.com/leanprover/lean4/releases/download/v${ver}/lean-${ver}-linux.tar.zst" +sudo mkdir -p /opt/lean +sudo tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst -C /opt/lean +export PATH="/opt/lean/lean-${ver}-linux/bin:$PATH" # use the macOS/win tarball on those OSes +``` + +Then, from the repo root: + +```sh +for f in WokeLang WokeGrammar WokeGrammarStructure WokeGrammarRegular WokeGrammarCFL WokeGrammarPumping; do + lean docs/proofs/verification/$f.lean && echo "OK $f" +done +``` + +### Coq 8.18.0 + +```sh +# install coq 8.18.0 (opam: `opam pin add coq 8.18.0`, or your platform package) +cd docs/proofs/verification +for f in WokeLang WokeGrammarStructure WokeGrammarParser; do coqc $f.v && echo "OK $f"; done +rm -f *.vo *.vok *.vos *.glob .*.aux # clean build artifacts +``` + +## Next increment (not yet started) + +The only remaining item in the original §7 scope is the **§7.3 ∩ / ¬ +non-closure corollary**, now unblocked by `cfl_pumping`: + +1. A **finiteness-aware `IsCFL`** predicate. (The relation-based `IsCFL` used for + the *positive* closure is too permissive for non-closure — an infinite + nonterminal type could "generate" `aⁿbⁿcⁿ`. Non-closure needs a grammar with + finitely many nonterminals, matching `cfl_pumping`'s `enum`/`card` interface.) +2. **`aⁿbⁿcⁿ ∉ CFL`** via `cfl_pumping`: any decomposition `uvwxy` with + `|vwx| ≤ p` touches at most two of the three letter-blocks, so pumping + unbalances the counts. +3. **Non-closure under ∩** (and hence ¬) by De Morgan against the already-proven + ∪ closure: `L₁ = {aⁿbⁿcᵐ}` and `L₂ = {aᵐbⁿcⁿ}` are CFLs but `L₁ ∩ L₂ = + {aⁿbⁿcⁿ}` is not. + +Plan: land it as its own follow-up PR (incremental, same as the pumping lemma). + +## CI notes + +On PR #106, the genuinely-relevant checks are green (Trusted-base reduction +policy; the Lean/Coq compile gates). Three checks are red but are **pre-existing +infrastructure failures unrelated to these proofs**, and every prior merged PR +(#102–#105) carried them too: + +- **Licence consistency** — root `LICENSE` SPDX mismatch. +- **Workflow security linter** — a `trufflehog@main` unpinned-action finding. +- **Hypatia Neurosymbolic Analysis** — scanner infrastructure. + +## Moving this session to desktop + +Per the Claude Code docs, use **teleport** to carry the conversation context + +branch + uncommitted changes from web into the local CLI / desktop app: +`claude --teleport ` (one-way: web → local). See +. Even without it, the +branch and PR #106 hold all the work. From 84dd029ab25030c6d2e551424a34f740e597024a Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 18:29:52 +0000 Subject: [PATCH 2/4] polish(proofs): record verified axiom profiles; clear unused-variable warning - GRAMMAR-PROOF-INVENTORY.md: add an "Axiom audit" table with the in-toolchain `#print axioms` results for the pumping-lemma headline theorems (only the standard classical kernel constants; no sorryAx, no project-specific constants). - WokeGrammarPumping.lean: make `yield_nonempty`'s tree a direct parameter instead of intro-then-induction, clearing the benign unused-variable linter warning. Still compiles clean (exit 0). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL --- .../verification/GRAMMAR-PROOF-INVENTORY.md | 19 +++++++++++++++++++ .../verification/WokeGrammarPumping.lean | 5 ++--- 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md b/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md index eeea362..4c8ac68 100644 --- a/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md +++ b/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md @@ -192,6 +192,25 @@ identical" per `AUDIT.md`.) could "generate" `aⁿbⁿcⁿ`), then `aⁿbⁿcⁿ ∉ CFL` via `cfl_pumping`, then `L₁ ∩ L₂` non-closure by De Morgan against the proven positive ∪ closure. +## Axiom audit (`#print axioms`, verified in-toolchain) + +Kernel-dependency printout for the headline results in `WokeGrammarPumping.lean` +(Lean 4.30.0). Only the standard classical constants appear — no `sorryAx`, no +project-specific constants: + +| Theorem | Kernel dependencies | +|---|---| +| `yield_bound` | `propext`, `Quot.sound` | +| `ht_descend` | `propext`, `Quot.sound` | +| `nodeNT_add` | `propext`, `Classical.choice`, `Quot.sound` | +| `descend_sibling_nonempty` | `propext`, `Quot.sound` | +| `cfl_pumping` | `propext`, `Classical.choice`, `Quot.sound` | + +`Classical.choice` enters only through the finite `pigeon`hole's case split; the +rest are the kernel constants Mathlib itself rests on. The other files' headline +results sit on the same or a smaller base (`WokeGrammarCFL.lean` is `propext`-only; +`WokeGrammarStructure`'s `no_left_recursion` is fully constant-free). + ## Status P1 (merged, #102) + P2/P3/P4 + the structural Coq mirror are machine-checked and diff --git a/docs/proofs/verification/WokeGrammarPumping.lean b/docs/proofs/verification/WokeGrammarPumping.lean index 048b39c..03ee298 100644 --- a/docs/proofs/verification/WokeGrammarPumping.lean +++ b/docs/proofs/verification/WokeGrammarPumping.lean @@ -264,9 +264,8 @@ theorem nodeNT_add {R : N → BProd N T → Prop} : /-- In an ε-free grammar (no `A → ε` productions), every parse tree yields a non-empty string. This is what makes the pumped portion `vx` non-empty. -/ -theorem yield_nonempty {R : N → BProd N T → Prop} (hRε : ∀ A, ¬ R A BProd.eps) : - ∀ {A w} (t : PT R A w), w ≠ [] := by - intro A w t +theorem yield_nonempty {R : N → BProd N T → Prop} (hRε : ∀ A, ¬ R A BProd.eps) + {A : N} {w : List T} (t : PT R A w) : w ≠ [] := by induction t with | @bin A B C w1 w2 _ t1 t2 ih1 ih2 => intro h; rcases List.append_eq_nil_iff.mp h with ⟨h1, _⟩; exact ih1 h1 From 1fa5c643cb12989738c820593cb9ade01cbc6d48 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 18:32:42 +0000 Subject: [PATCH 3/4] ci(governance): fix Licence-consistency + Workflow-security-linter checks MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - LICENSE: prepend `SPDX-License-Identifier: MPL-2.0` so the governance Licence-consistency check (and REUSE/cargo-license scanners) can identify the licence. Matches the Cargo.toml manifest declaration (MPL-2.0); canonical MPL text is unchanged below the header. - secret-scanner.yml: SHA-pin `trufflesecurity/trufflehog` to 30d5bb91af1a771378349dbbb0c82129392acf70 (v3.95.6) instead of the moving `@main` ref, satisfying the Workflow-security-linter and the repo's SHA-pinned-dependencies policy. SHA verified against the tag ref (lightweight tag → commit). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL --- .github/workflows/secret-scanner.yml | 2 +- LICENSE | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 3ad39fb..03266c0 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -21,6 +21,6 @@ jobs: with: fetch-depth: 0 - name: TruffleHog Secret Scan - uses: trufflesecurity/trufflehog@main + uses: trufflesecurity/trufflehog@30d5bb91af1a771378349dbbb0c82129392acf70 # v3.95.6 with: extra_args: --only-verified --fail diff --git a/LICENSE b/LICENSE index 14e2f77..2a8b960 100644 --- a/LICENSE +++ b/LICENSE @@ -1,3 +1,5 @@ +SPDX-License-Identifier: MPL-2.0 + Mozilla Public License Version 2.0 ================================== From d7a64d5f839e3a680a54b791960a9ea1f82e8b92 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 18:49:31 +0000 Subject: [PATCH 4/4] =?UTF-8?q?feat(proofs):=20a=E2=81=BFb=E2=81=BFc?= =?UTF-8?q?=E2=81=BF=20=E2=88=89=20CFL=20=E2=80=94=20the=20canonical=20non?= =?UTF-8?q?-closure=20witness=20(anbncn=5Fnot=5Fcfl)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The headline application of `cfl_pumping`: machine-checks that `aⁿbⁿcⁿ` is not context-free — the standard witness that the context-free languages are not closed under intersection / complement. Built from scratch in core Lean. New in WokeGrammarPumping.lean: • `IsCFL` — finiteness-aware: a language is CF iff some ε-free binary-normal-form grammar with an `enum`/`card` nonterminal bound generates exactly it (the relation-based `IsCFL` is too permissive — an infinite nonterminal type could "generate" aⁿbⁿcⁿ). • `prefix_pure` — positional core (induction on the prefix, no indexing): in `replicate n1 k1 ++ replicate n2 k2 ++ replicate n3 k3`, a middle segment containing a `k1` forces the prefix to be `k1`-only. • `abc_window` — a pumping window containing both an `a` and a `c` contains the whole `b`-block, so it is longer than `p`. • `anbncn_not_cfl` — apply `cfl_pumping` to `aᵖbᵖcᵖ`; pumping to `i=0` forces `count_a = count_b = count_c` in the deleted part (so it spans `a`…`c`), contradicting `|vwx| ≤ p`. Axioms (verified): `anbncn_not_cfl` → propext, Classical.choice, Quot.sound; `prefix_pure` → propext only. No holes, no project-specific assumptions. Docs (grammar-proofs.md §7.3, GRAMMAR-PROOF-INVENTORY.md incl. axiom audit, RESUME.md) updated. Remaining §7.3 step: the two witness-grammar constructions ({aⁿbⁿcᵐ}, {aᵐbⁿcⁿ}) whose intersection is aⁿbⁿcⁿ. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL --- RESUME.md | 34 ++-- .../proofs/formal-semantics/grammar-proofs.md | 8 +- .../verification/GRAMMAR-PROOF-INVENTORY.md | 25 ++- .../verification/WokeGrammarPumping.lean | 156 +++++++++++++++++- 4 files changed, 197 insertions(+), 26 deletions(-) diff --git a/RESUME.md b/RESUME.md index 4dd84bc..6486769 100644 --- a/RESUME.md +++ b/RESUME.md @@ -77,21 +77,25 @@ for f in WokeLang WokeGrammarStructure WokeGrammarParser; do coqc $f.v && echo " rm -f *.vo *.vok *.vos *.glob .*.aux # clean build artifacts ``` -## Next increment (not yet started) - -The only remaining item in the original §7 scope is the **§7.3 ∩ / ¬ -non-closure corollary**, now unblocked by `cfl_pumping`: - -1. A **finiteness-aware `IsCFL`** predicate. (The relation-based `IsCFL` used for - the *positive* closure is too permissive for non-closure — an infinite - nonterminal type could "generate" `aⁿbⁿcⁿ`. Non-closure needs a grammar with - finitely many nonterminals, matching `cfl_pumping`'s `enum`/`card` interface.) -2. **`aⁿbⁿcⁿ ∉ CFL`** via `cfl_pumping`: any decomposition `uvwxy` with - `|vwx| ≤ p` touches at most two of the three letter-blocks, so pumping - unbalances the counts. -3. **Non-closure under ∩** (and hence ¬) by De Morgan against the already-proven - ∪ closure: `L₁ = {aⁿbⁿcᵐ}` and `L₂ = {aᵐbⁿcⁿ}` are CFLs but `L₁ ∩ L₂ = - {aⁿbⁿcⁿ}` is not. +## §7.3 non-closure — status + +Done (in `WokeGrammarPumping.lean`): + +1. **Finiteness-aware `IsCFL`** — a language is CF iff some ε-free BNF grammar with + an `enum`/`card` nonterminal bound generates exactly it (matches `cfl_pumping`). +2. **`aⁿbⁿcⁿ ∉ CFL`** (`anbncn_not_cfl`) — via `cfl_pumping`: pumping down to + `i = 0` forces `count_a = count_b = count_c` in the deleted part, so the window + spans an `a` and a `c`; the positional core (`prefix_pure`, `abc_window`) then + gives `|vwx| > p`, contradicting `|vwx| ≤ p`. This is the canonical non-CFL and + the crux of the ∩/¬ non-closure result. + +Remaining (next increment): + +3. **The explicit ∩ / ¬ non-closure statement** — exhibit the two witness CFLs + `L₁ = {aⁿbⁿcᵐ}` and `L₂ = {aᵐbⁿcⁿ}` (each: a BNF grammar + an exact-generation + proof, i.e. soundness + completeness), with `L₁ ∩ L₂ = {aⁿbⁿcⁿ}` discharged by + `anbncn_not_cfl`. This is mechanical grammar-construction plumbing on top of the + verified crux. Plan: land it as its own follow-up PR (incremental, same as the pumping lemma). diff --git a/docs/proofs/formal-semantics/grammar-proofs.md b/docs/proofs/formal-semantics/grammar-proofs.md index 2f0e5ae..948807f 100644 --- a/docs/proofs/formal-semantics/grammar-proofs.md +++ b/docs/proofs/formal-semantics/grammar-proofs.md @@ -332,8 +332,12 @@ The binding power comparison ensures this: > — which even Mathlib lacks — is now machine-checked from scratch in core Lean in > [`../verification/WokeGrammarPumping.lean`](../verification/WokeGrammarPumping.lean) > (`cfl_pumping`: parse-tree spine navigation + finite pigeonhole ⇒ the `uvwxy` -> decomposition with `1 ≤ |vx|` and `|vwx| ≤ 2^(card+1)`). Only the §7.3 *non*-closure -> under ∩ / ¬ remains, and the pumping lemma it needed is now available; status in +> decomposition with `1 ≤ |vx|` and `|vwx| ≤ 2^(card+1)`). As its canonical +> application, the same file machine-checks **`aⁿbⁿcⁿ ∉ CFL`** (`anbncn_not_cfl`) — +> the standard witness that the CFLs are not closed under ∩ / ¬ (pump down to +> `i = 0` ⇒ equal letter-counts ⇒ the window spans `a`…`c` ⇒ `|vwx| > p`). The +> remaining §7.3 *non*-closure step is purely the two witness-grammar constructions +> `{aⁿbⁿcᵐ}`, `{aᵐbⁿcⁿ}`; status in > `../verification/GRAMMAR-PROOF-INVENTORY.md`. ### 7.1 Chomsky Hierarchy Position diff --git a/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md b/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md index 4c8ac68..0ce0402 100644 --- a/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md +++ b/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md @@ -72,7 +72,8 @@ reach here, with reason). | T7.3a | §7.3 CFL closed under ∪, ·, * | ✅ done from scratch | **P5→done** | `WokeGrammarCFL.lean`: CFG derivation relation + reusable embedding lemma + union/concat/star grammar constructions, `propext`-only | MACHINE-CHECKED | | T7.1 | §7.1 Not regular (pumping lemma) | ✅ done from scratch | **P6→done** | `WokeGrammarRegular.lean`: bespoke finite pigeonhole + `Fin k` DFA + fooling-set on `aⁿbⁿ` (≅ `(ⁿ)ⁿ`), Mathlib-free | MACHINE-CHECKED | | T7.0 | CFL pumping lemma (Mathlib-gap) | ✅ done from scratch | **Ext** | `WokeGrammarPumping.lean`: `cfl_pumping` — `descend`/`ht_descend`/`nodeNT_add` spine navigation + `Ctx.comp` + pigeonhole ⇒ `z = uvwxy`, `1≤|vx|`, `|vwx|≤2^(card+1)`, `uvⁱwxⁱy ∈ L`; classical kernel constants only | MACHINE-CHECKED | -| T7.3b | §7.3 CFL **not** closed under ∩, ¬ | ⚠️ remaining (pumping lemma now available) | **P6** | The blocker (CFL pumping lemma) is now proved as T7.0; remaining: finite `IsCFL` + `aⁿbⁿcⁿ ∉ CFL` + De Morgan | IN PROGRESS | +| T7.0b | `aⁿbⁿcⁿ ∉ CFL` (canonical non-CFL) | ✅ done from scratch | **Ext** | `WokeGrammarPumping.lean`: `anbncn_not_cfl` via `cfl_pumping` (pump `i=0` ⇒ equal counts ⇒ window spans `a`…`c` ⇒ `|vwx|>p`); positional core `prefix_pure`/`abc_window`; classical kernel constants only | MACHINE-CHECKED | +| T7.3b | §7.3 CFL **not** closed under ∩, ¬ | ⚠️ canonical witness done; wrapper remaining | **P6** | `aⁿbⁿcⁿ ∉ CFL` (T7.0b) is the crux and is proved; remaining: the two witness CFLs `{aⁿbⁿcᵐ}`,`{aᵐbⁿcⁿ}` (BNF grammars + exact generation) whose intersection is `aⁿbⁿcⁿ` | IN PROGRESS | ## Priority order (execution) @@ -186,11 +187,20 @@ identical" per `AUDIT.md`.) repeated-nonterminal extraction. Trust base: the three classical kernel constants (`propext`, `Classical.choice`, `Quot.sound`) — no holes, no project-specific assumptions. -- **§7.3 *non-closure* under ∩ / ¬** is the remaining increment. With the pumping - lemma in hand it follows by the standard route: a finiteness-aware `IsCFL` (the - relation-based `IsCFL` is too permissive here — an infinite nonterminal type - could "generate" `aⁿbⁿcⁿ`), then `aⁿbⁿcⁿ ∉ CFL` via `cfl_pumping`, then - `L₁ ∩ L₂` non-closure by De Morgan against the proven positive ∪ closure. +- **`aⁿbⁿcⁿ ∉ CFL` — DONE** (`WokeGrammarPumping.lean`, `anbncn_not_cfl`): the + canonical non-context-free language, the crux of any ∩/¬ non-closure argument. + `IsCFL` is defined finiteness-aware (an ε-free BNF grammar with an `enum`/`card` + nonterminal bound, matching `cfl_pumping`; the relation-based `IsCFL` used for + *positive* closure is too permissive here — an infinite nonterminal type could + "generate" `aⁿbⁿcⁿ`). Proof: apply `cfl_pumping` to `aᵖbᵖcᵖ`; pumping down to + `i = 0` forces `count_a = count_b = count_c` in the deleted part, so the pumped + window contains an `a` and a `c`; the positional core (`prefix_pure` by induction + on the prefix, `abc_window`) then gives `|vwx| > p`, contradicting `|vwx| ≤ p`. +- **§7.3 *non-closure* under ∩ / ¬** — the remaining wrapper. With `aⁿbⁿcⁿ ∉ CFL` + proved, the explicit statement follows from the two witness CFLs `{aⁿbⁿcᵐ}` and + `{aᵐbⁿcⁿ}` (whose intersection is `aⁿbⁿcⁿ`); each needs a BNF grammar plus an + exact-generation (soundness + completeness) proof — mechanical grammar-construction + plumbing on top of the verified crux. ## Axiom audit (`#print axioms`, verified in-toolchain) @@ -205,6 +215,9 @@ project-specific constants: | `nodeNT_add` | `propext`, `Classical.choice`, `Quot.sound` | | `descend_sibling_nonempty` | `propext`, `Quot.sound` | | `cfl_pumping` | `propext`, `Classical.choice`, `Quot.sound` | +| `prefix_pure` | `propext` | +| `abc_window` | `propext`, `Quot.sound` | +| `anbncn_not_cfl` | `propext`, `Classical.choice`, `Quot.sound` | `Classical.choice` enters only through the finite `pigeon`hole's case split; the rest are the kernel constants Mathlib itself rests on. The other files' headline diff --git a/docs/proofs/verification/WokeGrammarPumping.lean b/docs/proofs/verification/WokeGrammarPumping.lean index 03ee298..854ba7a 100644 --- a/docs/proofs/verification/WokeGrammarPumping.lean +++ b/docs/proofs/verification/WokeGrammarPumping.lean @@ -20,15 +20,22 @@ What is proved here (complete proofs — no holes, no escape hatches): • `cfl_pumping` : THE pumping lemma — for an ε-free binary-normal-form grammar with `card` nonterminals, any word `z ∈ L(S)` of length `≥ 2^(card+1)` splits as `z = u v w x y` with `1 ≤ |v x|`, `|v w x| ≤ 2^(card+1)`, and - `u vⁱ w xⁱ y ∈ L(S)` for every `i`. + `u vⁱ w xⁱ y ∈ L(S)` for every `i`; + • `IsCFL` + `anbncn_not_cfl` : the canonical application — `aⁿbⁿcⁿ` is NOT + context-free. Apply `cfl_pumping` to `aᵖbᵖcᵖ`; pumping down to `i = 0` forces + equal letter-counts in the pumped part, so it spans an `a` and a `c`, which + (positional core `prefix_pure`/`abc_window`) makes `|v w x| > p` — contradicting + `|v w x| ≤ p`. This is the standard witness that the CFLs are not closed under + intersection / complement. Trust base: only the three standard classical kernel constants `propext`, `Classical.choice`, and `Quot.sound` — the same foundations Mathlib relies on (`Classical.choice` enters through the `pigeon` case split). There are no holes and no project-specific assumptions; every step is checked by Lean's kernel. -NEXT: the finite-grammar `IsCFL`, `aⁿbⁿcⁿ ∉ CFL` via `cfl_pumping`, and the -∩ / ¬ non-closure corollary. +NEXT: wrap `anbncn_not_cfl` into the explicit ∩ / ¬ non-closure statement by +exhibiting the two witness CFLs `{aⁿbⁿcᵐ}`, `{aᵐbⁿcⁿ}` (BNF grammars + exact +generation) whose intersection is `aⁿbⁿcⁿ`. -/ -- A grammar in binary normal form: every production is A → B C, A → t, or A → ε. @@ -385,4 +392,147 @@ theorem cfl_pumping {R : N → BProd N T → Prop} {S : N} have h := fill outer (pumpIter pump i DP.m base) simpa [List.append_assoc] using h⟩ +/-! ### Application: `aⁿbⁿcⁿ` is not context-free -/ + +/-- The terminal alphabet `{a, b, c}`. -/ +inductive Letter | a | b | c + deriving DecidableEq + +open Letter List + +/-- A language over `{a,b,c}` is **context-free** iff some ε-free binary-normal-form +grammar with finitely many nonterminals generates exactly it. (Every ε-free CFL has +such a grammar — ε-free Chomsky normal form — so this is the standard CFL class for +ε-free languages, taken here as the definition.) -/ +def IsCFL (L : List Letter → Prop) : Prop := + ∃ (M : Type) (R : M → BProd M Letter → Prop) (S : M) (enum : M → Nat) (card : Nat), + (∀ A, enum A < card) ∧ (∀ A B, enum A = enum B → A = B) ∧ + (∀ A, ¬ R A BProd.eps) ∧ (∀ z, L z ↔ Nonempty (PT R S z)) + +/-- `aⁿbⁿcⁿ`. -/ +def abc (n : Nat) : List Letter := + replicate n a ++ replicate n b ++ replicate n c + +theorem count_repl_ne {x y : Letter} (n : Nat) (h : x ≠ y) : + count x (replicate n y) = 0 := by + rw [count_eq_zero]; intro hm; exact h (eq_of_mem_replicate hm) + +theorem count_abc (ℓ : Letter) (n : Nat) : count ℓ (abc n) = n := by + unfold abc + rw [count_append, count_append] + cases ℓ <;> + rw [count_replicate_self] <;> + rw [count_repl_ne _ (by decide), count_repl_ne _ (by decide)] <;> + omega + +theorem length_abc (n : Nat) : (abc n).length = 3 * n := by + unfold abc; rw [length_append, length_append, length_replicate, + length_replicate, length_replicate]; omega + +/-- Every element of a `{a,b,c}`-list is `a`, `b`, or `c`, so its length is the sum +of the three letter-counts. -/ +theorem length_eq_counts (l : List Letter) : + l.length = count a l + count b l + count c l := by + induction l with + | nil => simp + | cons hd t ih => cases hd <;> simp [length_cons] <;> omega + +/-- **Positional core.** In `replicate n1 k1 ++ replicate n2 k2 ++ replicate n3 k3`, +if the middle segment `m` of a split `u ++ m ++ y` contains a `k1` (and `k1` differs +from `k2`, `k3`), then the prefix `u` contains no `k2` — it lies wholly in the first +block. Proved by induction on the prefix; no indexing needed. -/ +theorem prefix_pure {k1 k2 k3 : Letter} (h12 : k1 ≠ k2) (h13 : k1 ≠ k3) : + ∀ (n1 n2 n3 : Nat) (u m y : List Letter), + u ++ m ++ y = replicate n1 k1 ++ replicate n2 k2 ++ replicate n3 k3 → + k1 ∈ m → count k2 u = 0 := by + intro n1 n2 n3 u + induction u generalizing n1 with + | nil => intro m y _ _; simp + | cons hd u' ih => + intro m y heq hmem + cases n1 with + | zero => + exfalso + have hin : k1 ∈ (hd :: u') ++ m ++ y := + mem_append.mpr (Or.inl (mem_append.mpr (Or.inr hmem))) + rw [heq] at hin + simp only [replicate, nil_append, mem_append, mem_replicate] at hin + rcases hin with ⟨_, h⟩ | ⟨_, h⟩ + · exact h12 h + · exact h13 h + | succ n1' => + rw [replicate_succ] at heq + simp only [cons_append] at heq + obtain ⟨rfl, heq'⟩ := List.cons.inj heq + rw [count_cons_of_ne h12] + exact ih n1' m y heq' hmem + +/-- **The pumping window spans `a`…`c`.** If a split `abc p = u ++ m ++ y` has `m` +containing both an `a` and a `c`, then `m` already contains the whole `b`-block, so +`p < |m|`. -/ +theorem abc_window {p : Nat} {u m y : List Letter} + (heq : abc p = u ++ m ++ y) (ha : a ∈ m) (hc : c ∈ m) : p < m.length := by + have hbu : count b u = 0 := + prefix_pure (by decide) (by decide) p p p u m y heq.symm ha + have hby : count b y = 0 := by + have hrev : (replicate p c ++ replicate p b ++ replicate p a : List Letter) + = y.reverse ++ m.reverse ++ u.reverse := by + have hr := congrArg List.reverse heq + simpa [abc, reverse_append, reverse_replicate, List.append_assoc] using hr + have hcm : c ∈ m.reverse := mem_reverse.mpr hc + have := prefix_pure (k1 := c) (k2 := b) (k3 := a) (by decide) (by decide) + p p p y.reverse m.reverse u.reverse hrev.symm hcm + rwa [count_reverse] at this + have hbz : count b (abc p) = p := count_abc b p + rw [heq, count_append, count_append, hbu, hby] at hbz + have hcm1 : 1 ≤ count c m := one_le_count_iff.mpr hc + have hlen := length_eq_counts m + omega + +/-- **`aⁿbⁿcⁿ` is not context-free.** The canonical witness that the context-free +languages are not closed under intersection / complement: apply `cfl_pumping` to +`aᵖbᵖcᵖ` (`p = 2^(card+1)`); pumping down to `i = 0` forces equal counts in the +pumped part, so it spans an `a` and a `c`, contradicting `|v w x| ≤ p`. -/ +theorem anbncn_not_cfl : ¬ IsCFL (fun z => ∃ n, 1 ≤ n ∧ z = abc n) := by + rintro ⟨M, R, S, enum, card, hcard, henj, hRε, hgen⟩ + have hp1 : 1 ≤ 2 ^ (card + 1) := Nat.one_le_two_pow + obtain ⟨t⟩ : Nonempty (PT R S (abc (2 ^ (card + 1)))) := + (hgen _).mp ⟨2 ^ (card + 1), hp1, rfl⟩ + have hlenz : 2 ^ (card + 1) ≤ (abc (2 ^ (card + 1))).length := by + rw [length_abc]; omega + obtain ⟨u, v, w, x, y, hz, hvx, hvwx, hpump⟩ := + cfl_pumping enum card hcard henj hRε t hlenz + -- Pump down to i = 0: u w y ∈ L. + obtain ⟨t0⟩ := hpump 0 + simp only [cat_zero, List.append_nil] at t0 + obtain ⟨m0, _, h0⟩ := (hgen _).mpr ⟨t0⟩ + -- For every letter, the counts removed by deleting `v` and `x` agree. + have key : ∀ ℓ : Letter, count ℓ v + count ℓ x = 2 ^ (card + 1) - m0 := by + intro ℓ + have ep : count ℓ (abc (2 ^ (card + 1))) = 2 ^ (card + 1) := count_abc ℓ _ + have em : count ℓ (abc m0) = m0 := count_abc ℓ _ + rw [hz] at ep + rw [← h0] at em + simp only [count_append] at ep em + omega + -- `|v x| = 3·(p - m0) ≥ 1`, so `p - m0 ≥ 1`: the pumped part has an `a` and a `c`. + have hvxlen : (v ++ x).length = 3 * (2 ^ (card + 1) - m0) := by + have hsum := length_eq_counts (v ++ x) + simp only [count_append] at hsum + rw [hsum, key a, key b, key c]; omega + have hk1 : 1 ≤ 2 ^ (card + 1) - m0 := by + rw [hvxlen] at hvx; omega + -- Hence `a` and `c` both occur in `v ++ w ++ x`. + have hca : 1 ≤ count a (v ++ w ++ x) := by + have := key a; simp only [count_append]; omega + have hcc : 1 ≤ count c (v ++ w ++ x) := by + have := key c; simp only [count_append]; omega + have hain : a ∈ v ++ w ++ x := one_le_count_iff.mp hca + have hcin : c ∈ v ++ w ++ x := one_le_count_iff.mp hcc + -- `v w x` is the window of `abc p`, so it spans `a`…`c` and is longer than `p`. + have hwin : abc (2 ^ (card + 1)) = u ++ (v ++ w ++ x) ++ y := by + rw [hz]; simp [List.append_assoc] + have hgt := abc_window hwin hain hcin + omega + end Pump