feat: context-free languages closure reversal

Mathlib.lean

@@ -1312,7 +1312,7 @@ import Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
 import Mathlib.Combinatorics.Young.SemistandardTableau
 import Mathlib.Combinatorics.Young.YoungDiagram
 import Mathlib.Computability.Ackermann
-import Mathlib.Computability.ContextFreeGrammar
+import Mathlib.Computability.ContextFree
 import Mathlib.Computability.DFA
 import Mathlib.Computability.Encoding
 import Mathlib.Computability.EpsilonNFA

Mathlib/Computability/ContextFreeGrammar.lean → Mathlib/Computability/ContextFree.lean

@@ -6,14 +6,18 @@ Authors: Martin Dvorak
 import Mathlib.Computability.Language
 
 /-!
-# Context-Free Grammar
+# Context-Free
 
 This file contains the definition of a context-free grammar, which is a grammar that has a single
 nonterminal symbol on the left-hand side of each rule.
+Then we prove basic properties of context-free languages.
 
 ## Main definitions
 * `ContextFreeGrammar`: A context-free grammar.
-* `ContextFreeGrammar.language`: A language generated by a given context-free grammar.
+* `Language.IsContextFree`: A language generated by a context-free grammar.
+
+## Main theorems
+* `Language.IsContextFree.reverse`: The class of context-free languages is closed under reversal.
 -/
 
 universe uT uN in
@@ -51,7 +55,7 @@ inductive Rewrites (r : ContextFreeRule T N) : List (Symbol T N) → List (Symbo
 
 lemma Rewrites.exists_parts {r : ContextFreeRule T N} {u v : List (Symbol T N)}
     (hyp : r.Rewrites u v) :
-    ∃ p : List (Symbol T N), ∃ q : List (Symbol T N),
+    ∃ p q : List (Symbol T N),
       u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q := by
   induction hyp with
   | head xs =>
@@ -143,3 +147,73 @@ lemma Derives.eq_or_tail {u w : List (Symbol T g.NT)} (huw : g.Derives u w) :
   (Relation.ReflTransGen.cases_tail huw).casesOn (Or.inl ∘ Eq.symm) Or.inr
 
 end ContextFreeGrammar
+
+/-- Context-free languages are defined by context-free grammars. -/
+def Language.IsContextFree (L : Language T) : Prop :=
+  ∃ g : ContextFreeGrammar.{uT} T, g.language = L
+
+private def reverseRule {N : Type uN} (r : ContextFreeRule T N) : ContextFreeRule T N :=
+  ⟨r.input, r.output.reverse⟩
+
+private def reverseGrammar (g : ContextFreeGrammar T) : ContextFreeGrammar T :=
+  ⟨g.NT, g.initial, g.rules.map reverseRule⟩
+
+private lemma reverseRule_reverseRule {N : Type uN} (r : ContextFreeRule T N) :
+    reverseRule (reverseRule r) = r := by
+  simp [reverseRule]
+
+private lemma dual_reverseRule {N : Type uN} : reverseRule ∘ @reverseRule T N = id := by
+  ext
+  apply reverseRule_reverseRule
+
+private lemma reverseGrammar_reverseGrammar (g : ContextFreeGrammar T) :
+    reverseGrammar (reverseGrammar g) = g := by
+  cases g with
+  | mk => simp [reverseGrammar, dual_reverseRule, List.map_map, List.map_id]
+
+private lemma derives_reverse {g : ContextFreeGrammar T} {s : List (Symbol T g.NT)}
+    (hgs : (reverseGrammar g).Derives [Symbol.nonterminal (reverseGrammar g).initial] s) :
+    g.Derives [Symbol.nonterminal g.initial] s.reverse := by
+  induction hgs with
+  | refl =>
+    rw [List.reverse_singleton]
+    apply ContextFreeGrammar.Derives.refl
+  | @tail u v _ orig ih =>
+    apply ContextFreeGrammar.Derives.trans_produces ih
+    rcases orig with ⟨r, rin, rewr⟩
+    simp only [reverseGrammar, List.mem_map] at rin
+    rcases rin with ⟨r₀, rin₀, r_of_r₀⟩
+    use r₀
+    constructor
+    · exact rin₀
+    rw [ContextFreeRule.rewrites_iff] at rewr ⊢
+    rcases rewr with ⟨p, q, rfl, rfl⟩
+    use q.reverse, p.reverse
+    rw [← r_of_r₀]
+    simp [reverseRule]
+
+private lemma reversed_word_in_original_language {g : ContextFreeGrammar T} {w : List T}
+    (hgw : w ∈ (reverseGrammar g).language) :
+    w.reverse ∈ g.language := by
+  convert derives_reverse hgw
+  simp [List.map_reverse]
+
+/-- The class of context-free languages is closed under reversal. -/
+theorem Language.IsContextFree.reverse {L : Language T} (CFL : L.IsContextFree) :
+    L.reverse.IsContextFree := by
+  cases CFL with
+  | intro g hgL =>
+    rw [← hgL]
+    use reverseGrammar g
+    apply Set.eq_of_subset_of_subset
+    · apply reversed_word_in_original_language
+    · intro w hwg
+      have pre_reversal : ∃ g₀, g = reverseGrammar g₀
+      · use reverseGrammar g
+        rw [reverseGrammar_reverseGrammar]
+      cases' pre_reversal with g₀ pre_rev
+      rw [pre_rev] at hwg ⊢
+      have finished_modulo_reverses := reversed_word_in_original_language hwg
+      rw [reverseGrammar_reverseGrammar]
+      rw [List.reverse_reverse] at finished_modulo_reverses
+      exact finished_modulo_reverses

Mathlib/Computability/Language.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Fox Thomson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fox Thomson
+Authors: Fox Thomson, Martin Dvorak
 -/
 import Mathlib.Algebra.Hom.Ring.Defs
 import Mathlib.Algebra.Order.Kleene
@@ -297,6 +297,65 @@ instance : KleeneAlgebra (Language α) :=
       rw [pow_succ, ←mul_assoc m l (l^n)]
       exact le_trans (le_mul_congr h le_rfl) ih }
 
+/-- Language `l.reverse` is defined as the set of words from `l` backwards. -/
+def reverse (l : Language α) : Language α := { w : List α | w.reverse ∈ l }
+
+@[simp]
+lemma reverse_mem_reverse : a.reverse ∈ l.reverse ↔ a ∈ l := by
+  show a.reverse.reverse ∈ l ↔ a ∈ l
+  rw [List.reverse_reverse]
+
+lemma zero_reverse : (0 : Language α).reverse = 0 := by
+  rfl
+
+lemma one_reverse : (1 : Language α).reverse = 1 := by
+  simp [reverse, ←one_def]
+
+lemma reverse_reverse : l.reverse.reverse = l := by
+  ext w
+  convert_to w.reverse.reverse ∈ reverse (reverse l) ↔ w ∈ l using 5
+  · rw [List.reverse_reverse]
+  rw [reverse_mem_reverse, reverse_mem_reverse]
+
+lemma reverse_union : (l + m).reverse = l.reverse + m.reverse := by
+  ext w
+  apply mem_add
+
+lemma reverse_concatenation : (l * m).reverse = m.reverse * l.reverse := by
+  ext w
+  show
+    (∃ u v, u ∈ l ∧ v ∈ m ∧ u ++ v = w.reverse) ↔
+    (∃ u v, u.reverse ∈ m ∧ v.reverse ∈ l ∧ u ++ v = w)
+  constructor <;>
+  · rintro ⟨u, v, hul, hvm, huvw⟩
+    use v.reverse, u.reverse
+    simp_all [← List.reverse_append]
+
+lemma reverse_kstar : l∗.reverse = l.reverse∗ := by
+  ext w
+  simp only [reverse, kstar_def]
+  show
+    (∃ L, w.reverse = join L ∧ ∀ y, y ∈ L → y ∈ l) ↔
+    (∃ L, w = join L ∧ ∀ y, y ∈ L → y.reverse ∈ l)
+  constructor
+  · rintro ⟨L, hwL, hLl⟩
+    use (L.map List.reverse).reverse
+    constructor
+    · rw [List.reverse_eq_iff] at hwL
+      simp [hwL, List.join_reverse, List.map_map, reverse_involutive]
+    · intros
+      simp_all [mem_reverse, mem_map, reverse_involutive,
+        Function.Involutive.exists_mem_and_apply_eq_iff]
+  · rintro ⟨L, hwL, hLl⟩
+    use (L.map List.reverse).reverse
+    constructor
+    · simp [List.join_reverse, List.map_map, hwL, reverse_involutive]
+    · intro y hy
+      simp only [mem_reverse, mem_map, reverse_involutive,
+        Function.Involutive.exists_mem_and_apply_eq_iff] at hy
+      specialize hLl y.reverse hy
+      rwa [List.reverse_reverse] at hLl
+
 end Language
 
 /-- Symbols for use by all kinds of grammars. -/