feat(computability/*): Automata lemmas (#13194)

A bunch of missing API for `language`, `regular_expression`, `DFA`, `NFA`, `ε_NFA`.

Co-authored-by: Fox Thomson

src/computability/DFA.lean

@@ -37,19 +37,31 @@ instance [inhabited σ] : inhabited (DFA α σ) :=
 def eval_from (start : σ) : list α → σ :=
 list.foldl M.step start
 
+@[simp] lemma eval_from_nil (s : σ) : M.eval_from s [] = s := rfl
+@[simp] lemma eval_from_singleton (s : σ) (a : α) : M.eval_from s [a] = M.step s a := rfl
+@[simp] lemma eval_from_append_singleton (s : σ) (x : list α) (a : α) :
+  M.eval_from s (x ++ [a]) = M.step (M.eval_from s x) a :=
+by simp only [eval_from, list.foldl_append, list.foldl_cons, list.foldl_nil]
+
 /-- `M.eval x` evaluates `M` with input `x` starting from the state `M.start`. -/
-def eval := M.eval_from M.start
+def eval : list α → σ := M.eval_from M.start
+
+@[simp] lemma eval_nil : M.eval [] = M.start := rfl
+@[simp] lemma eval_singleton (a : α) : M.eval [a] = M.step M.start a := rfl
+@[simp] lemma eval_append_singleton (x : list α) (a : α) :
+  M.eval (x ++ [a]) = M.step (M.eval x) a :=
+eval_from_append_singleton _ _ _ _
+
+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
 
 /-- `M.accepts` is the language of `x` such that `M.eval x` is an accept state. -/
 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 σ ≤ x.length)
   (hx : M.eval_from s x = t) :
   ∃ q a b c,

src/computability/NFA.lean

@@ -17,6 +17,8 @@ Note that this definition allows for Automaton with infinite states, a `fintype`
 supplied for true NFA's.
 -/
 
+open set
+
 universes u v
 
 /-- An NFA is a set of states (`σ`), a transition function from state to state labelled by the
@@ -35,21 +37,34 @@ namespace NFA
 instance : inhabited (NFA α σ) := ⟨ NFA.mk (λ _ _, ∅) ∅ ∅ ⟩
 
 /-- `M.step_set S a` is the union of `M.step s a` for all `s ∈ S`. -/
-def step_set : set σ → α → set σ :=
-λ Ss a, Ss >>= (λ S, (M.step S a))
+def step_set (S : set σ) (a : α) : set σ := ⋃ s ∈ S, M.step s a
+
+lemma mem_step_set (s : σ) (S : set σ) (a : α) : s ∈ M.step_set S a ↔ ∃ t ∈ S, s ∈ M.step t a :=
+mem_Union₂
 
-lemma mem_step_set (s : σ) (S : set σ) (a : α) :
-  s ∈ M.step_set S a ↔ ∃ t ∈ S, s ∈ M.step t a :=
-by simp only [step_set, set.mem_Union, set.bind_def]
+@[simp] lemma step_set_empty (a : α) : M.step_set ∅ a = ∅ :=
+by simp_rw [step_set, Union_false, Union_empty]
 
 /-- `M.eval_from S x` computes all possible paths though `M` with input `x` starting at an element
   of `S`. -/
 def eval_from (start : set σ) : list α → set σ :=
 list.foldl M.step_set start
 
+@[simp] lemma eval_from_nil (S : set σ) : M.eval_from S [] = S := rfl
+@[simp] lemma eval_from_singleton (S : set σ) (a : α) : M.eval_from S [a] = M.step_set S a := rfl
+@[simp] lemma eval_from_append_singleton (S : set σ) (x : list α) (a : α) :
+  M.eval_from S (x ++ [a]) = M.step_set (M.eval_from S x) a :=
+by simp only [eval_from, list.foldl_append, list.foldl_cons, list.foldl_nil]
+
 /-- `M.eval x` computes all possible paths though `M` with input `x` starting at an element of
   `M.start`. -/
-def eval := M.eval_from M.start
+def eval : list α → set σ := M.eval_from M.start
+
+@[simp] lemma eval_nil : M.eval [] = M.start := rfl
+@[simp] lemma eval_singleton (a : α) : M.eval [a] = M.step_set M.start a := rfl
+@[simp] lemma eval_append_singleton (x : list α) (a : α) :
+  M.eval (x ++ [a]) = M.step_set (M.eval x) a :=
+eval_from_append_singleton _ _ _ _
 
 /-- `M.accepts` is the language of `x` such that there is an accept state in `M.eval x`. -/
 def accepts : language α :=

src/computability/epsilon_NFA.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Fox Thomson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fox Thomson
+Authors: Fox Thomson, Yaël Dillies
 -/
 
 import computability.NFA
@@ -16,6 +16,8 @@ Since this definition allows for automata with infinite states, a `fintype` inst
 supplied for true `ε_NFA`'s.
 -/
 
+open set
+
 universes u v
 
 /-- An `ε_NFA` is a set of states (`σ`), a transition function from state to state labelled by the
@@ -29,34 +31,70 @@ structure ε_NFA (α : Type u) (σ : Type v) :=
 (start : set σ)
 (accept : set σ)
 
-variables {α : Type u} {σ σ' : Type v} (M : ε_NFA α σ)
+variables {α : Type u} {σ σ' : Type v} (M : ε_NFA α σ) {S : set σ} {x : list α} {s : σ} {a : α}
 
 namespace ε_NFA
 
-instance : inhabited (ε_NFA α σ) := ⟨ ε_NFA.mk (λ _ _, ∅) ∅ ∅ ⟩
-
 /-- The `ε_closure` of a set is the set of states which can be reached by taking a finite string of
-  ε-transitions from an element of the set -/
-inductive ε_closure : set σ → set σ
-| base : ∀ S (s ∈ S), ε_closure S s
-| step : ∀ S s (t ∈ M.step s none), ε_closure S s → ε_closure S t
+ε-transitions from an element of the set. -/
+inductive ε_closure (S : set σ) : set σ
+| base : ∀ s ∈ S, ε_closure s
+| step : ∀ s (t ∈ M.step s none), ε_closure s → ε_closure t
+
+@[simp] lemma subset_ε_closure (S : set σ) : S ⊆ M.ε_closure S := ε_closure.base
+
+@[simp] lemma ε_closure_empty : M.ε_closure ∅ = ∅ :=
+eq_empty_of_forall_not_mem $ λ s hs, by induction hs with t ht _ _ _ _ ih; assumption
+
+@[simp] lemma ε_closure_univ : M.ε_closure univ = univ :=
+eq_univ_of_univ_subset $ subset_ε_closure _ _
 
 /-- `M.step_set S a` is the union of the ε-closure of `M.step s a` for all `s ∈ S`. -/
-def step_set : set σ → α → set σ :=
-λ S a, S >>= (λ s, M.ε_closure (M.step s a))
+def step_set (S : set σ) (a : α) : set σ := ⋃ s ∈ S, M.ε_closure $ M.step s a
+
+variables {M}
+
+@[simp] lemma mem_step_set_iff : s ∈ M.step_set S a ↔ ∃ t ∈ S, s ∈ M.ε_closure (M.step t a) :=
+mem_Union₂
 
-/-- `M.eval_from S x` computes all possible paths though `M` with input `x` starting at an element
-  of `S`. -/
+@[simp] lemma step_set_empty (a : α) : M.step_set ∅ a = ∅ :=
+by simp_rw [step_set, Union_false, Union_empty]
+
+variables (M)
+
+/-- `M.eval_from S x` computes all possible paths through `M` with input `x` starting at an element
+of `S`. -/
 def eval_from (start : set σ) : list α → set σ :=
 list.foldl M.step_set (M.ε_closure start)
 
-/-- `M.eval x` computes all possible paths though `M` with input `x` starting at an element of
-  `M.start`. -/
+@[simp] lemma eval_from_nil (S : set σ) : M.eval_from S [] = M.ε_closure S := rfl
+@[simp] lemma eval_from_singleton (S : set σ) (a : α) :
+  M.eval_from S [a] = M.step_set (M.ε_closure S) a := rfl
+@[simp] lemma eval_from_append_singleton (S : set σ) (x : list α) (a : α) :
+  M.eval_from S (x ++ [a]) = M.step_set (M.eval_from S x) a :=
+by simp only [eval_from, list.foldl_append, list.foldl_cons, list.foldl_nil]
+
+@[simp] lemma eval_from_empty (x : list α) : M.eval_from ∅ x = ∅ :=
+begin
+  induction x using list.reverse_rec_on with x a ih,
+  { rw [eval_from_nil, ε_closure_empty] },
+  { rw [eval_from_append_singleton, ih, step_set_empty] }
+end
+
+/-- `M.eval x` computes all possible paths through `M` with input `x` starting at an element of
+`M.start`. -/
 def eval := M.eval_from M.start
 
+@[simp] lemma eval_nil : M.eval [] = M.ε_closure M.start := rfl
+@[simp] lemma eval_singleton (a : α) : M.eval [a] = M.step_set (M.ε_closure M.start) a := rfl
+@[simp] lemma eval_append_singleton (x : list α) (a : α) :
+  M.eval (x ++ [a]) = M.step_set (M.eval x) a :=
+eval_from_append_singleton _ _ _ _
+
 /-- `M.accepts` is the language of `x` such that there is an accept state in `M.eval x`. -/
-def accepts : language α :=
-λ x, ∃ S ∈ M.accept, S ∈ M.eval x
+def accepts : language α := {x | ∃ S ∈ M.accept, S ∈ M.eval x}
+
+/-! ### Conversions between `ε_NFA` and `NFA` -/
 
 /-- `M.to_NFA` is an `NFA` constructed from an `ε_NFA` `M`. -/
 def to_NFA : NFA α σ :=
@@ -98,22 +136,19 @@ def to_ε_NFA (M : NFA α σ) : ε_NFA α σ :=
 @[simp] lemma to_ε_NFA_ε_closure (M : NFA α σ) (S : set σ) : M.to_ε_NFA.ε_closure S = S :=
 begin
   ext a,
-  split,
-  { rintro ( ⟨ _, _, h ⟩ | ⟨ _, _, _, h, _ ⟩ ),
-    exact h,
-    cases h },
-  { intro h,
-    apply ε_NFA.ε_closure.base,
-    exact h }
+  refine ⟨_, ε_NFA.ε_closure.base _⟩,
+  rintro (⟨_, h⟩ | ⟨_, _, h, _⟩),
+  { exact h },
+  { cases h }
 end
 
 @[simp] lemma to_ε_NFA_eval_from_match (M : NFA α σ) (start : set σ) :
   M.to_ε_NFA.eval_from start = M.eval_from start :=
 begin
-  rw [eval_from, ε_NFA.eval_from, step_set, ε_NFA.step_set, to_ε_NFA_ε_closure],
+  rw [eval_from, ε_NFA.eval_from, to_ε_NFA_ε_closure],
   congr,
   ext S s,
-  simp only [exists_prop, set.mem_Union, set.bind_def],
+  simp only [step_set, ε_NFA.step_set, exists_prop, set.mem_Union, set.bind_def],
   apply exists_congr,
   simp only [and.congr_right_iff],
   intros t ht,
@@ -129,3 +164,25 @@ begin
 end
 
 end NFA
+
+/-! ### Regex-like operations -/
+
+namespace ε_NFA
+
+instance : has_zero (ε_NFA α σ) := ⟨⟨λ _ _, ∅, ∅, ∅⟩⟩
+instance : has_one (ε_NFA α σ) := ⟨⟨λ _ _, ∅, univ, univ⟩⟩
+
+instance : inhabited (ε_NFA α σ) := ⟨0⟩
+
+variables (P : ε_NFA α σ) (Q : ε_NFA α σ')
+
+@[simp] lemma step_zero (s a) : (0 : ε_NFA α σ).step s a = ∅ := rfl
+@[simp] lemma step_one (s a) : (1 : ε_NFA α σ).step s a = ∅ := rfl
+
+@[simp] lemma start_zero : (0 : ε_NFA α σ).start = ∅ := rfl
+@[simp] lemma start_one : (1 : ε_NFA α σ).start = univ := rfl
+
+@[simp] lemma accept_zero : (0 : ε_NFA α σ).accept = ∅ := rfl
+@[simp] lemma accept_one : (1 : ε_NFA α σ).accept = univ := rfl
+
+end ε_NFA

src/computability/language.lean

@@ -26,6 +26,7 @@ variables {α : Type u}
 def language (α) := set (list α)
 
 namespace language
+variables {l m : language α} {a b x : list α}
 
 local attribute [reducible] language
 
@@ -58,15 +59,14 @@ lemma star_def (l : language α) :
   l.star = { x | ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l} := rfl
 
 @[simp] lemma not_mem_zero (x : list α) : x ∉ (0 : language α) := id
-lemma nil_mem_one : [] ∈ (1 : language α) := mem_singleton _
-@[simp] lemma mem_one (x : list α) : x ∈ (1 : language α) ↔ x = [] := iff.rfl
-@[simp] lemma mem_add (l m : language α) (x : list α) : x ∈ l + m ↔ x ∈ l ∨ x ∈ m :=
-by simp [add_def]
-lemma mem_mul (l m : language α) (x : list α) : x ∈ l * m ↔ ∃ a b, a ∈ l ∧ b ∈ m ∧ a ++ b = x :=
-by simp [mul_def]
-lemma mem_star (l : language α) (x : list α) :
-  x ∈ l.star ↔ ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l :=
-iff.rfl
+@[simp] lemma mem_one (x : list α) : x ∈ (1 : language α) ↔ x = [] := by refl
+lemma nil_mem_one : [] ∈ (1 : language α) := set.mem_singleton _
+@[simp] lemma mem_add (l m : language α) (x : list α) : x ∈ l + m ↔ x ∈ l ∨ x ∈ m := iff.rfl
+lemma mem_mul : x ∈ l * m ↔ ∃ a b, a ∈ l ∧ b ∈ m ∧ a ++ b = x := mem_image2
+lemma append_mem_mul : a ∈ l → b ∈ m → a ++ b ∈ l * m := mem_image2_of_mem
+lemma mem_star : x ∈ l.star ↔ ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l := iff.rfl
+lemma join_mem_star {S : list (list α)} (h : ∀ y ∈ S, y ∈ l) : S.join ∈ l.star := ⟨S, rfl, h⟩
+lemma nil_mem_star (l : language α) : [] ∈ l.star := ⟨[], rfl, λ _, false.elim⟩
 
 instance : semiring (language α) :=
 { add := (+),

src/computability/regular_expressions.lean

@@ -13,7 +13,8 @@ This file contains the formal definition for regular expressions and basic lemma
 regular expressions in terms of formal language theory. Note this is different to regex's used in
 computer science such as the POSIX standard.
 
-TODO
+## TODO
+
 * Show that this regular expressions and DFA/NFA's are equivalent.
 * `attribute [pattern] has_mul.mul` has been added into this file, it could be moved.
 -/
@@ -41,6 +42,7 @@ inductive regular_expression (α : Type u) : Type u
 | star : regular_expression → regular_expression
 
 namespace regular_expression
+variables {a b : α}
 
 instance : inhabited (regular_expression α) := ⟨zero⟩
 
@@ -66,13 +68,14 @@ def matches : regular_expression α → language α
 | (P * Q) := P.matches * Q.matches
 | (star P) := P.matches.star
 
-@[simp] lemma matches_zero_def : (0 : regular_expression α).matches = 0 := rfl
-@[simp] lemma matches_epsilon_def : (1 : regular_expression α).matches = 1 := rfl
-@[simp] lemma matches_add_def (P Q : regular_expression α) :
+@[simp] lemma matches_zero : (0 : regular_expression α).matches = 0 := rfl
+@[simp] lemma matches_epsilon : (1 : regular_expression α).matches = 1 := rfl
+@[simp] lemma matches_char (a : α) : (char a).matches = {[a]} := rfl
+@[simp] lemma matches_add (P Q : regular_expression α) :
   (P + Q).matches = P.matches + Q.matches := rfl
-@[simp] lemma matches_mul_def (P Q : regular_expression α) :
+@[simp] lemma matches_mul (P Q : regular_expression α) :
   (P * Q).matches = P.matches * Q.matches := rfl
-@[simp] lemma matches_star_def (P : regular_expression α) : P.star.matches = P.matches.star := rfl
+@[simp] lemma matches_star (P : regular_expression α) : P.star.matches = P.matches.star := rfl
 
 /-- `match_epsilon P` is true if and only if `P` matches the empty string -/
 def match_epsilon : regular_expression α → bool
@@ -99,17 +102,26 @@ def deriv : regular_expression α → α → regular_expression α
     deriv P a * Q
 | (star P) a := deriv P a * star P
 
+@[simp] lemma deriv_zero (a : α) : deriv 0 a = 0 := rfl
+@[simp] lemma deriv_one (a : α) : deriv 1 a = 0 := rfl
+@[simp] lemma deriv_char_self (a : α) : deriv (char a) a = 1 := if_pos rfl
+@[simp] lemma deriv_char_of_ne (h : a ≠ b) : deriv (char a) b = 0 := if_neg h
+@[simp] lemma deriv_add (P Q : regular_expression α) (a : α) :
+  deriv (P + Q) a = deriv P a + deriv Q a := rfl
+@[simp] lemma deriv_star (P : regular_expression α) (a : α) :
+  deriv (P.star) a = deriv P a * star P := rfl
+
 /-- `P.rmatch x` is true if and only if `P` matches `x`. This is a computable definition equivalent
   to `matches`. -/
 def rmatch : regular_expression α → list α → bool
 | P [] := match_epsilon P
 | P (a::as) := rmatch (P.deriv a) as
 
 @[simp] lemma zero_rmatch (x : list α) : rmatch 0 x = ff :=
-by induction x; simp [rmatch, match_epsilon, deriv, *]
+by induction x; simp [rmatch, match_epsilon, *]
 
 lemma one_rmatch_iff (x : list α) : rmatch 1 x ↔ x = [] :=
-by induction x; simp [rmatch, match_epsilon, deriv, *]
+by induction x; simp [rmatch, match_epsilon, *]
 
 lemma char_rmatch_iff (a : α) (x : list α) : rmatch (char a) x ↔ x = [a] :=
 begin

src/data/set/basic.lean

@@ -373,6 +373,8 @@ theorem subset_empty_iff {s : set α} : s ⊆ ∅ ↔ s = ∅ :=
 
 theorem eq_empty_iff_forall_not_mem {s : set α} : s = ∅ ↔ ∀ x, x ∉ s := subset_empty_iff.symm
 
+lemma eq_empty_of_forall_not_mem (h : ∀ x, x ∉ s) : s = ∅ := subset_empty_iff.1 h
+
 theorem eq_empty_of_subset_empty {s : set α} : s ⊆ ∅ → s = ∅ := subset_empty_iff.1
 
 theorem eq_empty_of_is_empty [is_empty α] (s : set α) : s = ∅ :=