|
| 1 | +/- |
| 2 | +SPDX-License-Identifier: MPL-2.0 |
| 3 | +Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 4 | +
|
| 5 | +WokeGrammarCFL.lean — machine-checks grammar-proofs.md §7.3 (positive direction): |
| 6 | +the class of context-free languages is closed under union, concatenation and |
| 7 | +Kleene star. Self-contained: Lean core prelude only (no Mathlib). |
| 8 | +
|
| 9 | +A CFG is a production relation `P : N → List (N ⊕ T) → Prop`; `Gen P A w` is the |
| 10 | +derivation relation (a nonterminal generates a terminal string). `IsCFL L` means |
| 11 | +some grammar generates exactly `L`. The proofs go through one reusable lemma — |
| 12 | +`embGen_iff`, that embedding a grammar's nonterminals into a larger disjoint |
| 13 | +grammar preserves the generated language — then build the union/concat/star |
| 14 | +grammars (`none → S1 | S2`, `none → S1 S2`, `none → ε | S1 S`) and prove the |
| 15 | +language equalities. |
| 16 | +
|
| 17 | +Connection to WokeLang: the surface grammar IS context-free (every production of |
| 18 | +`grammar/wokelang.ebnf` has the form `A → α`), so it inhabits this class and these |
| 19 | +closure operations apply to it. |
| 20 | +
|
| 21 | +Scope note: the §7.3 *negative* results (CFL NOT closed under intersection / |
| 22 | +complement) need the pumping lemma FOR CFLs (to show e.g. `aⁿbⁿcⁿ` is not |
| 23 | +context-free) — a separate, larger development, left scoped. |
| 24 | +-/ |
| 25 | +namespace CFL |
| 26 | + |
| 27 | +variable {T : Type} |
| 28 | + |
| 29 | +abbrev GSym (N T : Type) := N ⊕ T |
| 30 | + |
| 31 | +mutual |
| 32 | + inductive Gen {N : Type} (P : N → List (GSym N T) → Prop) : N → List T → Prop |
| 33 | + | mk {A rhs w} : P A rhs → GenL P rhs w → Gen P A w |
| 34 | + inductive GenL {N : Type} (P : N → List (GSym N T) → Prop) : List (GSym N T) → List T → Prop |
| 35 | + | nil : GenL P [] [] |
| 36 | + | consT {t rest w} : GenL P rest w → GenL P (Sum.inr t :: rest) (t :: w) |
| 37 | + | consN {A rest w1 w2} : Gen P A w1 → GenL P rest w2 → GenL P (Sum.inl A :: rest) (w1 ++ w2) |
| 38 | +end |
| 39 | + |
| 40 | +def IsCFL (L : List T → Prop) : Prop := |
| 41 | + ∃ (N : Type) (P : N → List (GSym N T) → Prop) (s : N), ∀ w, L w ↔ Gen P s w |
| 42 | + |
| 43 | +abbrev emap {N1 Nu : Type} (emb : N1 → Nu) : GSym N1 T → GSym Nu T := Sum.map emb id |
| 44 | + |
| 45 | +/-! ### Generic grammar embedding (reused for union / concat / star) -/ |
| 46 | + |
| 47 | +mutual |
| 48 | + theorem embLiftGen {N1 Nu} {P1 : N1 → List (GSym N1 T) → Prop} {Pu : Nu → List (GSym Nu T) → Prop} |
| 49 | + {emb : N1 → Nu} (hC : ∀ A rhs, Pu (emb A) rhs ↔ ∃ rhs1, P1 A rhs1 ∧ rhs = rhs1.map (emap emb)) |
| 50 | + {A w} (h : Gen P1 A w) : Gen Pu (emb A) w := |
| 51 | + match h with |
| 52 | + | .mk hP hL => .mk ((hC A _).mpr ⟨_, hP, rfl⟩) (embLiftGenL hC hL) |
| 53 | + theorem embLiftGenL {N1 Nu} {P1 : N1 → List (GSym N1 T) → Prop} {Pu : Nu → List (GSym Nu T) → Prop} |
| 54 | + {emb : N1 → Nu} (hC : ∀ A rhs, Pu (emb A) rhs ↔ ∃ rhs1, P1 A rhs1 ∧ rhs = rhs1.map (emap emb)) |
| 55 | + {rhs w} (h : GenL P1 rhs w) : GenL Pu (rhs.map (emap emb)) w := |
| 56 | + match h with |
| 57 | + | .nil => .nil |
| 58 | + | .consT hL => .consT (embLiftGenL hC hL) |
| 59 | + | .consN hG hL => .consN (embLiftGen hC hG) (embLiftGenL hC hL) |
| 60 | +end |
| 61 | + |
| 62 | +mutual |
| 63 | + theorem embReflGen {N1 Nu} {P1 : N1 → List (GSym N1 T) → Prop} {Pu : Nu → List (GSym Nu T) → Prop} |
| 64 | + {emb : N1 → Nu} (hC : ∀ A rhs, Pu (emb A) rhs ↔ ∃ rhs1, P1 A rhs1 ∧ rhs = rhs1.map (emap emb)) |
| 65 | + {X w} (h : Gen Pu X w) : ∀ A, X = emb A → Gen P1 A w := |
| 66 | + match h with |
| 67 | + | .mk hP hL => fun A hX => by |
| 68 | + rw [hX] at hP |
| 69 | + obtain ⟨rhs1, hP1, hrel⟩ := (hC A _).mp hP |
| 70 | + exact Gen.mk hP1 (embReflGenL hC hL rhs1 hrel) |
| 71 | + theorem embReflGenL {N1 Nu} {P1 : N1 → List (GSym N1 T) → Prop} {Pu : Nu → List (GSym Nu T) → Prop} |
| 72 | + {emb : N1 → Nu} (hC : ∀ A rhs, Pu (emb A) rhs ↔ ∃ rhs1, P1 A rhs1 ∧ rhs = rhs1.map (emap emb)) |
| 73 | + {s w} (h : GenL Pu s w) : ∀ rhs1, s = rhs1.map (emap emb) → GenL P1 rhs1 w := |
| 74 | + match h with |
| 75 | + | .nil => fun rhs1 hs => by |
| 76 | + cases rhs1 with |
| 77 | + | nil => exact GenL.nil |
| 78 | + | cons x r => simp [emap] at hs |
| 79 | + | .consT hL' => fun rhs1 hs => by |
| 80 | + cases rhs1 with |
| 81 | + | nil => simp [emap] at hs |
| 82 | + | cons x r => |
| 83 | + cases x with |
| 84 | + | inl A => simp [emap] at hs |
| 85 | + | inr t => |
| 86 | + simp only [List.map_cons, emap, Sum.map_inr, id_eq, List.cons.injEq, Sum.inr.injEq] at hs |
| 87 | + obtain ⟨ht, hrest⟩ := hs; subst ht |
| 88 | + exact GenL.consT (embReflGenL hC hL' r hrest) |
| 89 | + | .consN hG hL' => fun rhs1 hs => by |
| 90 | + cases rhs1 with |
| 91 | + | nil => simp [emap] at hs |
| 92 | + | cons x r => |
| 93 | + cases x with |
| 94 | + | inr t => simp [emap] at hs |
| 95 | + | inl A' => |
| 96 | + simp only [List.map_cons, emap, Sum.map_inl, List.cons.injEq, Sum.inl.injEq] at hs |
| 97 | + obtain ⟨hA, hrest⟩ := hs |
| 98 | + exact GenL.consN (embReflGen hC hG A' hA) (embReflGenL hC hL' r hrest) |
| 99 | +end |
| 100 | + |
| 101 | +theorem embGen_iff {N1 Nu} {P1 : N1 → List (GSym N1 T) → Prop} {Pu : Nu → List (GSym Nu T) → Prop} |
| 102 | + {emb : N1 → Nu} (hC : ∀ A rhs, Pu (emb A) rhs ↔ ∃ rhs1, P1 A rhs1 ∧ rhs = rhs1.map (emap emb)) |
| 103 | + {A w} : Gen Pu (emb A) w ↔ Gen P1 A w := |
| 104 | + ⟨fun h => embReflGen hC h A rfl, embLiftGen hC⟩ |
| 105 | + |
| 106 | +/-- A single-nonterminal sentential form generates the same strings as the |
| 107 | +nonterminal itself. -/ |
| 108 | +theorem genL_single {N} {P : N → List (GSym N T) → Prop} {X w} : |
| 109 | + GenL P [Sum.inl X] w ↔ Gen P X w := by |
| 110 | + constructor |
| 111 | + · intro h |
| 112 | + cases h with | consN hG hL => cases hL with | nil => simpa using hG |
| 113 | + · intro h; simpa using GenL.consN h GenL.nil |
| 114 | + |
| 115 | +/-! ### Closure under union -/ |
| 116 | + |
| 117 | +section Union |
| 118 | +variable {N1 N2 : Type} |
| 119 | + |
| 120 | +def emb1 : N1 → Option (N1 ⊕ N2) := fun A => some (Sum.inl A) |
| 121 | +def emb2 : N2 → Option (N1 ⊕ N2) := fun B => some (Sum.inr B) |
| 122 | + |
| 123 | +/-- Union grammar: fresh start `none`, with `none → S1 | S2`, and each side's |
| 124 | +productions relabelled into the disjoint copy. -/ |
| 125 | +def unionP (P1 : N1 → List (GSym N1 T) → Prop) (P2 : N2 → List (GSym N2 T) → Prop) |
| 126 | + (s1 : N1) (s2 : N2) : Option (N1 ⊕ N2) → List (GSym (Option (N1 ⊕ N2)) T) → Prop := |
| 127 | + fun X rhs => match X with |
| 128 | + | none => rhs = [Sum.inl (emb1 s1)] ∨ rhs = [Sum.inl (emb2 s2)] |
| 129 | + | some (Sum.inl A) => ∃ r1, P1 A r1 ∧ rhs = r1.map (emap (emb1 (N2 := N2))) |
| 130 | + | some (Sum.inr B) => ∃ r2, P2 B r2 ∧ rhs = r2.map (emap (emb2 (N1 := N1))) |
| 131 | + |
| 132 | +variable (P1 : N1 → List (GSym N1 T) → Prop) (P2 : N2 → List (GSym N2 T) → Prop) (s1 : N1) (s2 : N2) |
| 133 | + |
| 134 | +theorem union_left {A w} : Gen (unionP P1 P2 s1 s2) (emb1 A) w ↔ Gen P1 A w := |
| 135 | + embGen_iff (emb := emb1) (fun _ _ => Iff.rfl) |
| 136 | + |
| 137 | +theorem union_right {B w} : Gen (unionP P1 P2 s1 s2) (emb2 B) w ↔ Gen P2 B w := |
| 138 | + embGen_iff (emb := emb2) (fun _ _ => Iff.rfl) |
| 139 | + |
| 140 | +theorem cfl_union_gen {w} : |
| 141 | + Gen (unionP P1 P2 s1 s2) none w ↔ (Gen P1 s1 w ∨ Gen P2 s2 w) := by |
| 142 | + constructor |
| 143 | + · intro h |
| 144 | + cases h with |
| 145 | + | mk hP hL => |
| 146 | + rcases hP with hP | hP <;> rw [hP] at hL <;> rw [genL_single] at hL |
| 147 | + · exact Or.inl ((union_left P1 P2 s1 s2).mp hL) |
| 148 | + · exact Or.inr ((union_right P1 P2 s1 s2).mp hL) |
| 149 | + · intro h |
| 150 | + rcases h with h | h |
| 151 | + · exact Gen.mk (Or.inl rfl) (genL_single.mpr ((union_left P1 P2 s1 s2).mpr h)) |
| 152 | + · exact Gen.mk (Or.inr rfl) (genL_single.mpr ((union_right P1 P2 s1 s2).mpr h)) |
| 153 | + |
| 154 | +end Union |
| 155 | + |
| 156 | +/-- **§7.3 — CFL closed under union.** -/ |
| 157 | +theorem cfl_union {L1 L2 : List T → Prop} (h1 : IsCFL L1) (h2 : IsCFL L2) : |
| 158 | + IsCFL (fun w => L1 w ∨ L2 w) := by |
| 159 | + obtain ⟨N1, P1, s1, hL1⟩ := h1 |
| 160 | + obtain ⟨N2, P2, s2, hL2⟩ := h2 |
| 161 | + refine ⟨Option (N1 ⊕ N2), unionP P1 P2 s1 s2, none, fun w => ?_⟩ |
| 162 | + simp only [hL1, hL2]; exact (cfl_union_gen P1 P2 s1 s2).symm |
| 163 | + |
| 164 | +/-! ### Closure under concatenation -/ |
| 165 | + |
| 166 | +/-- A two-nonterminal sentential form splits the string between them. -/ |
| 167 | +theorem genL_pair {N} {P : N → List (GSym N T) → Prop} {X Y w} : |
| 168 | + GenL P [Sum.inl X, Sum.inl Y] w ↔ ∃ w1 w2, w = w1 ++ w2 ∧ Gen P X w1 ∧ Gen P Y w2 := by |
| 169 | + constructor |
| 170 | + · intro h |
| 171 | + cases h with |
| 172 | + | consN hG1 hL2 => cases hL2 with |
| 173 | + | consN hG2 hL3 => cases hL3 with | nil => exact ⟨_, _, by simp, hG1, hG2⟩ |
| 174 | + · rintro ⟨w1, w2, rfl, hX, hY⟩ |
| 175 | + simpa using GenL.consN hX (GenL.consN hY GenL.nil) |
| 176 | + |
| 177 | +section Concat |
| 178 | +variable {N1 N2 : Type} |
| 179 | + |
| 180 | +/-- Concatenation grammar: `none → S1 S2`, plus each side relabelled. -/ |
| 181 | +def concatP (P1 : N1 → List (GSym N1 T) → Prop) (P2 : N2 → List (GSym N2 T) → Prop) |
| 182 | + (s1 : N1) (s2 : N2) : Option (N1 ⊕ N2) → List (GSym (Option (N1 ⊕ N2)) T) → Prop := |
| 183 | + fun X rhs => match X with |
| 184 | + | none => rhs = [Sum.inl (emb1 s1), Sum.inl (emb2 s2)] |
| 185 | + | some (Sum.inl A) => ∃ r1, P1 A r1 ∧ rhs = r1.map (emap (emb1 (N2 := N2))) |
| 186 | + | some (Sum.inr B) => ∃ r2, P2 B r2 ∧ rhs = r2.map (emap (emb2 (N1 := N1))) |
| 187 | + |
| 188 | +variable (P1 : N1 → List (GSym N1 T) → Prop) (P2 : N2 → List (GSym N2 T) → Prop) (s1 : N1) (s2 : N2) |
| 189 | + |
| 190 | +theorem concat_left {A w} : Gen (concatP P1 P2 s1 s2) (emb1 A) w ↔ Gen P1 A w := |
| 191 | + embGen_iff (emb := emb1) (fun _ _ => Iff.rfl) |
| 192 | +theorem concat_right {B w} : Gen (concatP P1 P2 s1 s2) (emb2 B) w ↔ Gen P2 B w := |
| 193 | + embGen_iff (emb := emb2) (fun _ _ => Iff.rfl) |
| 194 | + |
| 195 | +theorem cfl_concat_gen {w} : |
| 196 | + Gen (concatP P1 P2 s1 s2) none w ↔ ∃ w1 w2, w = w1 ++ w2 ∧ Gen P1 s1 w1 ∧ Gen P2 s2 w2 := by |
| 197 | + constructor |
| 198 | + · intro h |
| 199 | + cases h with |
| 200 | + | mk hP hL => |
| 201 | + rw [hP, genL_pair] at hL |
| 202 | + obtain ⟨w1, w2, hw, hG1, hG2⟩ := hL |
| 203 | + exact ⟨w1, w2, hw, (concat_left P1 P2 s1 s2).mp hG1, (concat_right P1 P2 s1 s2).mp hG2⟩ |
| 204 | + · rintro ⟨w1, w2, hw, hG1, hG2⟩ |
| 205 | + refine Gen.mk rfl (genL_pair.mpr ⟨w1, w2, hw, ?_, ?_⟩) |
| 206 | + · exact (concat_left P1 P2 s1 s2).mpr hG1 |
| 207 | + · exact (concat_right P1 P2 s1 s2).mpr hG2 |
| 208 | + |
| 209 | +end Concat |
| 210 | + |
| 211 | +/-- **§7.3 — CFL closed under concatenation.** -/ |
| 212 | +theorem cfl_concat {L1 L2 : List T → Prop} (h1 : IsCFL L1) (h2 : IsCFL L2) : |
| 213 | + IsCFL (fun w => ∃ w1 w2, w = w1 ++ w2 ∧ L1 w1 ∧ L2 w2) := by |
| 214 | + obtain ⟨N1, P1, s1, hL1⟩ := h1 |
| 215 | + obtain ⟨N2, P2, s2, hL2⟩ := h2 |
| 216 | + refine ⟨Option (N1 ⊕ N2), concatP P1 P2 s1 s2, none, fun w => ?_⟩ |
| 217 | + rw [cfl_concat_gen P1 P2 s1 s2] |
| 218 | + constructor |
| 219 | + · rintro ⟨w1, w2, hw, h1', h2'⟩; exact ⟨w1, w2, hw, (hL1 w1).mp h1', (hL2 w2).mp h2'⟩ |
| 220 | + · rintro ⟨w1, w2, hw, h1', h2'⟩; exact ⟨w1, w2, hw, (hL1 w1).mpr h1', (hL2 w2).mpr h2'⟩ |
| 221 | + |
| 222 | +/-! ### Closure under Kleene star -/ |
| 223 | + |
| 224 | +/-- Right-recursive Kleene star of a language. -/ |
| 225 | +inductive Star (L : List T → Prop) : List T → Prop |
| 226 | + | nil : Star L [] |
| 227 | + | step {w1 w2} : L w1 → Star L w2 → Star L (w1 ++ w2) |
| 228 | + |
| 229 | +section StarS |
| 230 | +variable {N1 : Type} |
| 231 | + |
| 232 | +def embS : N1 → Option N1 := some |
| 233 | + |
| 234 | +/-- Star grammar over `Option N1`: `none → ε | S1 S` (right-recursive), and the |
| 235 | +original productions relabelled under `some`. -/ |
| 236 | +def starP (P1 : N1 → List (GSym N1 T) → Prop) (s1 : N1) : |
| 237 | + Option N1 → List (GSym (Option N1) T) → Prop := |
| 238 | + fun X rhs => match X with |
| 239 | + | none => rhs = [] ∨ rhs = [Sum.inl (embS s1), Sum.inl none] |
| 240 | + | some A => ∃ r1, P1 A r1 ∧ rhs = r1.map (emap embS) |
| 241 | + |
| 242 | +variable (P1 : N1 → List (GSym N1 T) → Prop) (s1 : N1) |
| 243 | + |
| 244 | +theorem star_some {A w} : Gen (starP P1 s1) (embS A) w ↔ Gen P1 A w := |
| 245 | + embGen_iff (emb := embS) (fun _ _ => Iff.rfl) |
| 246 | + |
| 247 | +mutual |
| 248 | + theorem star_fwd_g {X w} (h : Gen (starP P1 s1) X w) : X = none → Star (Gen P1 s1) w := |
| 249 | + match h with |
| 250 | + | .mk hP hL => fun hX => by rw [hX] at hP; exact star_fwd_l hL hP |
| 251 | + theorem star_fwd_l {rhs w} (h : GenL (starP P1 s1) rhs w) : |
| 252 | + starP P1 s1 none rhs → Star (Gen P1 s1) w := |
| 253 | + match h with |
| 254 | + | .nil => fun _ => Star.nil |
| 255 | + | .consT _ => fun hP => by simp [starP] at hP |
| 256 | + | .consN hG1 hL2 => |
| 257 | + match hL2 with |
| 258 | + | .nil => fun hP => by simp [starP, embS] at hP |
| 259 | + | .consT _ => fun hP => by simp [starP, embS] at hP |
| 260 | + | .consN hG2 hL3 => |
| 261 | + match hL3 with |
| 262 | + | .consT _ => fun hP => by simp [starP, embS] at hP |
| 263 | + | .consN _ _ => fun hP => by simp [starP, embS] at hP |
| 264 | + | .nil => fun hP => by |
| 265 | + simp only [starP, embS, List.cons.injEq, Sum.inl.injEq, and_true, |
| 266 | + reduceCtorEq, false_or] at hP |
| 267 | + obtain ⟨hX', hY'⟩ := hP |
| 268 | + have h2 := star_fwd_g hG2 hY' |
| 269 | + have h1 := (star_some P1 s1).mp (hX' ▸ hG1) |
| 270 | + simpa using Star.step h1 h2 |
| 271 | +end |
| 272 | + |
| 273 | +theorem star_bwd {w} (h : Star (Gen P1 s1) w) : Gen (starP P1 s1) none w := by |
| 274 | + induction h with |
| 275 | + | nil => exact Gen.mk (Or.inl rfl) GenL.nil |
| 276 | + | @step w1 w2 hw1 _ ih => |
| 277 | + refine Gen.mk (Or.inr rfl) ?_ |
| 278 | + have h1 : Gen (starP P1 s1) (embS s1) w1 := (star_some P1 s1).mpr hw1 |
| 279 | + simpa using GenL.consN h1 (GenL.consN ih GenL.nil) |
| 280 | + |
| 281 | +theorem cfl_star_gen {w} : Gen (starP P1 s1) none w ↔ Star (Gen P1 s1) w := |
| 282 | + ⟨fun h => star_fwd_g P1 s1 h rfl, star_bwd P1 s1⟩ |
| 283 | + |
| 284 | +end StarS |
| 285 | + |
| 286 | +/-- **§7.3 — CFL closed under Kleene star.** -/ |
| 287 | +theorem cfl_star {L : List T → Prop} (h : IsCFL L) : IsCFL (Star L) := by |
| 288 | + obtain ⟨N1, P1, s1, hL⟩ := h |
| 289 | + refine ⟨Option N1, starP P1 s1, none, fun w => ?_⟩ |
| 290 | + rw [cfl_star_gen P1 s1] |
| 291 | + constructor |
| 292 | + · intro hs; induction hs with |
| 293 | + | nil => exact Star.nil |
| 294 | + | step hw1 _ ih => exact Star.step ((hL _).mp hw1) ih |
| 295 | + · intro hs; induction hs with |
| 296 | + | nil => exact Star.nil |
| 297 | + | step hw1 _ ih => exact Star.step ((hL _).mpr hw1) ih |
| 298 | + |
| 299 | +/-- Sanity: the singleton language `{[t]}` is context-free — so `IsCFL` is |
| 300 | +non-vacuous and the closure theorems above are not about an empty class. -/ |
| 301 | +theorem cfl_single (t : T) : IsCFL (fun w => w = [t]) := by |
| 302 | + refine ⟨Unit, fun _ rhs => rhs = [Sum.inr t], (), fun w => ?_⟩ |
| 303 | + constructor |
| 304 | + · intro hw; subst hw; exact Gen.mk rfl (GenL.consT GenL.nil) |
| 305 | + · intro h |
| 306 | + cases h with | mk hP hL => subst hP; cases hL with | consT hL' => cases hL' with | nil => rfl |
| 307 | + |
| 308 | +end CFL |
0 commit comments