feat(computability/{language/regular_expressions): Map along a function (#13197)

Define `language.map` and `regular_expression.map`.

Co-authored-by: Fox Thomson

Author: YaelDillies

src/computability/language.lean

@@ -15,11 +15,11 @@ The operations in this file define a [Kleene algebra](https://en.wikipedia.org/w
 over the languages.
 -/
 
-universes u v
-
 open list set
 
-variables {α : Type u}
+universes v
+
+variables {α β γ : Type*}
 
 /-- A language is a set of strings over an alphabet. -/
 @[derive [has_mem (list α), has_singleton (list α), has_insert (list α), complete_boolean_algebra]]
@@ -87,6 +87,18 @@ instance : semiring (language α) :=
 
 @[simp] lemma add_self (l : language α) : l + l = l := sup_idem
 
+/-- Maps the alphabet of a language. -/
+def map (f : α → β) : language α →+* language β :=
+{ to_fun := image (list.map f),
+  map_zero' := image_empty _,
+  map_one' := image_singleton,
+  map_add' := image_union _,
+  map_mul' := λ _ _, image_image2_distrib $ map_append _ }
+
+@[simp] lemma map_id (l : language α) : map id l = l := by simp [map]
+@[simp] lemma map_map (g : β → γ) (f : α → β) (l : language α) : map g (map f l) = map (g ∘ f) l :=
+by simp [map, image_image]
+
 lemma star_def_nonempty (l : language α) :
   l.star = {x | ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []} :=
 begin
@@ -155,6 +167,13 @@ begin
   { rintro ⟨_, S, rfl, rfl, hS⟩, exact ⟨S, rfl, hS⟩ }
 end
 
+@[simp] lemma map_star (f : α → β) (l : language α) : map f (star l) = star (map f l) :=
+begin
+  rw [star_eq_supr_pow, star_eq_supr_pow],
+  simp_rw ←map_pow,
+  exact image_Union,
+end
+
 lemma mul_self_star_comm (l : language α) : l.star * l = l * l.star :=
 by simp only [star_eq_supr_pow, mul_supr, supr_mul, ← pow_succ, ← pow_succ']
 

src/computability/regular_expressions.lean

@@ -19,9 +19,11 @@ computer science such as the POSIX standard.
 * `attribute [pattern] has_mul.mul` has been added into this file, it could be moved.
 -/
 
+open list set
+
 universe u
 
-variables {α : Type u} [dec : decidable_eq α]
+variables {α β γ : Type*} [dec : decidable_eq α]
 
 /--
 This is the definition of regular expressions. The names used here is to mirror the definition
@@ -60,7 +62,7 @@ attribute [pattern] has_mul.mul
 @[simp] lemma comp_def (P Q : regular_expression α) : comp P Q = P * Q := rfl
 
 /-- `matches P` provides a language which contains all strings that `P` matches -/
-def matches : regular_expression α → language α
+@[simp] def matches : regular_expression α → language α
 | 0 := 0
 | 1 := 1
 | (char a) := {[a]}
@@ -313,4 +315,47 @@ begin
   exact eq.decidable _ _
 end
 
+omit dec
+
+/-- Map the alphabet of a regular expression. -/
+@[simp] def map (f : α → β) : regular_expression α → regular_expression β
+| 0 := 0
+| 1 := 1
+| (char a) := char (f a)
+| (R + S) := map R + map S
+| (R * S) := map R * map S
+| (star R) := star (map R)
+
+@[simp] lemma map_id : ∀ (P : regular_expression α), P.map id = P
+| 0 := rfl
+| 1 := rfl
+| (char a) := rfl
+| (R + S) := by simp_rw [map, map_id]
+| (R * S) := by simp_rw [map, map_id]
+| (star R) := by simp_rw [map, map_id]
+
+@[simp] lemma map_map (g : β → γ) (f : α → β) :
+  ∀ (P : regular_expression α), (P.map f).map g = P.map (g ∘ f)
+| 0 := rfl
+| 1 := rfl
+| (char a) := rfl
+| (R + S) := by simp_rw [map, map_map]
+| (R * S) := by simp_rw [map, map_map]
+| (star R) := by simp_rw [map, map_map]
+
+/-- The language of the map is the map of the language. -/
+@[simp] lemma matches_map (f : α → β) :
+  ∀ P : regular_expression α, (P.map f).matches = language.map f P.matches
+| 0 := (map_zero _).symm
+| 1 := (map_one _).symm
+| (char a) := by { rw eq_comm, exact image_singleton }
+| (R + S) := by simp only [matches_map, map, matches_add, map_add]
+| (R * S) := by simp only [matches_map, map, matches_mul, map_mul]
+| (star R) := begin
+    simp_rw [map, matches, matches_map],
+    rw [language.star_eq_supr_pow, language.star_eq_supr_pow],
+    simp_rw ←map_pow,
+    exact image_Union.symm,
+  end
+
 end regular_expression