feat(computability/DFA): the pumping lemma (#5925)

src/computability/DFA.lean

@@ -6,6 +6,7 @@ Authors: Fox Thomson
 
 import data.fintype.basic
 import computability.language
+import tactic.norm_num
 
 /-!
 # Deterministic Finite Automata
@@ -43,4 +44,87 @@ def eval := M.eval_from M.start
 def accepts : language α :=
 λ x, M.eval x ∈ M.accept
 
+lemma mem_accepts (x : list α) : x ∈ M.accepts ↔ M.eval_from M.start x ∈ M.accept := by refl
+
+lemma eval_from_of_append (start : σ) (x y : list α) :
+  M.eval_from start (x ++ y) = M.eval_from (M.eval_from start x) y :=
+x.foldl_append _ _ y
+
+lemma eval_from_split [fintype σ] {x : list α} {s t : σ} (hlen : fintype.card σ + 1 ≤ x.length)
+  (hx : M.eval_from s x = t) :
+  ∃ q a b c,
+  x = a ++ b ++ c ∧
+  a.length + b.length ≤ fintype.card σ + 1 ∧
+  b ≠ [] ∧
+  M.eval_from s a = q ∧
+  M.eval_from q b = q ∧
+  M.eval_from q c = t :=
+begin
+  obtain ⟨⟨n, hn⟩, ⟨m, hm⟩, hneq, heq⟩ := fintype.exists_ne_map_eq_of_card_lt
+    (λ n : fin (fintype.card σ + 1), M.eval_from s (x.take n)) (by norm_num),
+  wlog hle : n ≤ m := le_total n m using [n m, m n],
+
+  refine ⟨M.eval_from s ((x.take m).take n), (x.take m).take n, (x.take m).drop n, x.drop m,
+    _, _, _, by refl, _⟩,
+
+  { rw [list.take_append_drop, list.take_append_drop] },
+
+  { simp only [list.length_drop, list.length_take],
+    rw [min_eq_left (hm.le.trans hlen), min_eq_left hle, nat.add_sub_cancel' hle],
+    exact hm.le },
+
+  { intro h,
+    have hlen' := congr_arg list.length h,
+    simp only [list.length_drop, list.length, list.length_take] at hlen',
+    rw [min_eq_left_of_lt, nat.sub_eq_zero_iff_le] at hlen',
+    { apply hneq,
+      apply le_antisymm,
+      assumption' },
+    exact hm.trans_le hlen, },
+
+  have hq :
+    M.eval_from (M.eval_from s ((x.take m).take n)) ((x.take m).drop n) =
+      M.eval_from s ((x.take m).take n),
+  { simp only [fin.coe_mk] at heq,
+    rw [list.take_take, min_eq_left hle, ←eval_from_of_append, heq, ←min_eq_left hle,
+        ←list.take_take, min_eq_left hle, list.take_append_drop] },
+
+  use hq,
+  rwa [←hq, ←eval_from_of_append, ←eval_from_of_append, ←list.append_assoc, list.take_append_drop,
+       list.take_append_drop]
+end
+
+lemma eval_from_of_pow {x y : list α} {s : σ} (hx : M.eval_from s x = s)
+  (hy : y ∈ @language.star α {x}) : M.eval_from s y = s :=
+begin
+  rw language.mem_star at hy,
+  rcases hy with ⟨ S, rfl, hS ⟩,
+  induction S with a S ih,
+  { refl },
+  { have ha := hS a (list.mem_cons_self _ _),
+    rw set.mem_singleton_iff at ha,
+    rw [list.join, eval_from_of_append, ha, hx],
+    apply ih,
+    intros z hz,
+    exact hS z (list.mem_cons_of_mem a hz) }
+end
+
+lemma pumping_lemma [fintype σ] {x : list α} (hx : x ∈ M.accepts)
+  (hlen : fintype.card σ + 1 ≤ list.length x) :
+  ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ fintype.card σ + 1 ∧ b ≠ [] ∧
+  {a} * language.star {b} * {c} ≤ M.accepts :=
+begin
+  obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.eval_from_split hlen rfl,
+  use [a, b, c, hx, hlen, hnil],
+  intros y hy,
+  rw language.mem_mul at hy,
+  rcases hy with ⟨ ab, c', hab, hc', rfl ⟩,
+  rw language.mem_mul at hab,
+  rcases hab with ⟨ a', b', ha', hb', rfl ⟩,
+  rw set.mem_singleton_iff at ha' hc',
+  substs ha' hc',
+  have h := M.eval_from_of_pow hb hb',
+  rwa [mem_accepts, eval_from_of_append, eval_from_of_append, h, hc]
+end
+
 end DFA

src/computability/NFA.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fox Thomson
 -/
 
-import data.fintype.basic
 import computability.DFA
 
 /-!
@@ -72,6 +71,15 @@ begin
   finish
 end
 
+lemma pumping_lemma [fintype σ] {x : list α} (hx : x ∈ M.accepts)
+  (hlen : fintype.card (set σ) + 1 ≤ list.length x) :
+  ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ fintype.card (set σ) + 1 ∧ b ≠ [] ∧
+  {a} * language.star {b} * {c} ≤ M.accepts :=
+begin
+  rw ←to_DFA_correct at hx ⊢,
+  exact M.to_DFA.pumping_lemma hx hlen
+end
+
 end NFA
 
 namespace DFA