feat(computability/language): le on languages (#5704)

src/computability/language.lean

@@ -13,12 +13,12 @@ The operations in this file define a [Kleene algebra](https://en.wikipedia.org/w
 over the languages.
 -/
 
-universe u
+universes u v
 
 variables {α : Type u} [dec : decidable_eq α]
 
 /-- A language is a set of strings over an alphabet. -/
-@[derive [has_mem (list α), has_singleton (list α), has_insert (list α)]]
+@[derive [has_mem (list α), has_singleton (list α), has_insert (list α), complete_lattice]]
 def language (α) := set (list α)
 
 namespace language
@@ -47,16 +47,25 @@ def star (l : language α) : language α :=
 lemma star_def (l : language α) :
   l.star = { x | ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l} := rfl
 
-private lemma mul_assoc (l m n : language α) : (l * m) * n = l * (m * n) :=
+@[simp] lemma mem_one (x : list α) : x ∈ (1 : language α) ↔ x = [] := by refl
+@[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 :=
+by refl
+
+private lemma mul_assoc_lang (l m n : language α) : (l * m) * n = l * (m * n) :=
 by { ext x, simp [mul_def], tauto {closer := `[subst_vars, simp *] } }
 
-private lemma one_mul (l : language α) : 1 * l = l :=
+private lemma one_mul_lang (l : language α) : 1 * l = l :=
 by { ext x, simp [mul_def, one_def], tauto {closer := `[subst_vars, simp [*]] } }
 
-private lemma mul_one (l : language α) : l * 1 = l :=
+private lemma mul_one_lang (l : language α) : l * 1 = l :=
 by { ext x, simp [mul_def, one_def], tauto {closer := `[subst_vars, simp *] } }
 
-private lemma left_distrib (l m n : language α) : l * (m + n) = (l * m) + (l * n) :=
+private lemma left_distrib_lang (l m n : language α) : l * (m + n) = (l * m) + (l * n) :=
 begin
   ext x,
   simp only [mul_def, add_def, exists_and_distrib_left, set.mem_image2, set.image_prod,
@@ -75,7 +84,7 @@ begin
       exact ⟨ hy, hz ⟩ } }
 end
 
-private lemma right_distrib (l m n : language α) : (l + m) * n = (l * n) + (m * n) :=
+private lemma right_distrib_lang (l m n : language α) : (l + m) * n = (l * n) + (m * n) :=
 begin
   ext x,
   simp only [mul_def, set.mem_image, add_def, set.mem_prod, exists_and_distrib_left, set.mem_image2,
@@ -102,16 +111,16 @@ instance : semiring (language α) :=
   add_zero := by simp [zero_def, add_def],
   add_comm := by simp [add_def, set.union_comm],
   mul := (*),
-  mul_assoc := mul_assoc,
+  mul_assoc := mul_assoc_lang,
   zero_mul := by simp [zero_def, mul_def],
   mul_zero := by simp [zero_def, mul_def],
   one := 1,
-  one_mul := one_mul,
-  mul_one := mul_one,
-  left_distrib := left_distrib,
-  right_distrib := right_distrib }
+  one_mul := one_mul_lang,
+  mul_one := mul_one_lang,
+  left_distrib := left_distrib_lang,
+  right_distrib := right_distrib_lang }
 
-@[simp] lemma add_self (l : language α) : l + l = l := by finish [add_def]
+@[simp] lemma add_self (l : language α) : l + l = l := sup_idem
 
 lemma star_def_nonempty (l : language α) :
   l.star = { x | ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []} :=
@@ -151,4 +160,116 @@ begin
     finish }
 end
 
+lemma le_iff (l m : language α) : l ≤ m ↔ l + m = m := sup_eq_right.symm
+
+lemma le_mul_congr {l₁ l₂ m₁ m₂ : language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂ :=
+begin
+  intros h₁ h₂ x hx,
+  simp only [mul_def, exists_and_distrib_left, set.mem_image2, set.image_prod] at hx ⊢,
+  tauto
+end
+
+lemma le_add_congr {l₁ l₂ m₁ m₂ : language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ + l₂ ≤ m₁ + m₂ := sup_le_sup
+
+lemma supr_mul {ι : Sort v} (l : ι → language α) (m : language α) :
+  (⨆ i, l i) * m = ⨆ i, l i * m :=
+begin
+  ext x,
+  simp only [mem_mul, set.mem_Union, exists_and_distrib_left],
+  tauto
+end
+
+lemma mul_supr {ι : Sort v} (l : ι → language α) (m : language α) :
+  m * (⨆ i, l i) = ⨆ i, m * l i :=
+begin
+  ext x,
+  simp only [mem_mul, set.mem_Union, exists_and_distrib_left],
+  tauto
+end
+
+lemma supr_add {ι : Sort v} [nonempty ι] (l : ι → language α) (m : language α) :
+  (⨆ i, l i) + m = ⨆ i, l i + m := supr_sup
+
+lemma add_supr {ι : Sort v} [nonempty ι] (l : ι → language α) (m : language α) :
+  m + (⨆ i, l i) = ⨆ i, m + l i := sup_supr
+
+lemma star_eq_supr_pow (l : language α) : l.star = ⨆ i : ℕ, l ^ i :=
+begin
+  ext x,
+  simp only [star_def, set.mem_Union, set.mem_set_of_eq],
+  split,
+  { revert x,
+    rintros _ ⟨ S, rfl, hS ⟩,
+    induction S with x S ih,
+    { use 0,
+      tauto },
+    { specialize ih _,
+      { cases ih with i ih,
+        use i.succ,
+        rw [pow_succ, mem_mul],
+        exact ⟨ x, S.join, hS x (list.mem_cons_self _ _), ih, rfl ⟩ },
+      { exact λ y hy, hS _ (list.mem_cons_of_mem _ hy) } } },
+  { rintro ⟨ i, hx ⟩,
+    induction i with i ih generalizing x,
+    { rw [pow_zero, mem_one] at hx,
+      subst hx,
+      use [[]],
+      tauto },
+    { rw [pow_succ, mem_mul] at hx,
+      rcases hx with ⟨ a, b, ha, hb, hx ⟩,
+      rcases ih b hb with ⟨ S, hb, hS ⟩,
+      use a :: S,
+      rw list.join,
+      refine ⟨hb ▸ hx.symm, λ y, or.rec (λ hy, _) (hS _)⟩,
+      exact hy.symm ▸ ha } }
+end
+
+lemma mul_self_star_comm (l : language α) : l.star * l = l * l.star :=
+by simp [star_eq_supr_pow, mul_supr, supr_mul, ← pow_succ, ← pow_succ']
+
+@[simp] lemma one_add_self_mul_star_eq_star (l : language α) : 1 + l * l.star = l.star :=
+begin
+  rw [star_eq_supr_pow, mul_supr, add_def, supr_split_single (λ i, l ^ i) 0],
+  have h : (⨆ (i : ℕ), l * l ^ i) = ⨆ (i : ℕ) (h : i ≠ 0), (λ (i : ℕ), l ^ i) i,
+  { ext x,
+    simp only [exists_prop, set.mem_Union, ne.def],
+    split,
+    { rintro ⟨ i, hi ⟩,
+      use [i.succ, nat.succ_ne_zero i],
+      rwa pow_succ },
+    { rintro ⟨ (_ | i), h0, hi ⟩,
+      { contradiction },
+      use i,
+      rwa ←pow_succ } },
+  rw h,
+  refl
+end
+
+@[simp] lemma one_add_star_mul_self_eq_star (l : language α) : 1 + l.star * l = l.star :=
+by rw [mul_self_star_comm, one_add_self_mul_star_eq_star]
+
+lemma star_mul_le_right_of_mul_le_right (l m : language α) : l * m ≤ m → l.star * m ≤ m :=
+begin
+  intro h,
+  rw [star_eq_supr_pow, supr_mul],
+  refine supr_le _,
+  intro n,
+  induction n with n ih,
+  { simp },
+  rw [pow_succ', mul_assoc (l^n) l m],
+  exact le_trans (le_mul_congr (le_refl _) h) ih,
+end
+
+lemma star_mul_le_left_of_mul_le_left (l m : language α) : m * l ≤ m → m * l.star ≤ m :=
+begin
+  intro h,
+  rw [star_eq_supr_pow, mul_supr],
+  refine supr_le _,
+  intro n,
+  induction n with n ih,
+  { simp },
+  rw [pow_succ, ←mul_assoc m l (l^n)],
+  exact le_trans (le_mul_congr h (le_refl _)) ih
+end
+
 end language

src/order/complete_lattice.lean

@@ -654,6 +654,12 @@ by simpa only [inf_comm] using binfi_inf h
 theorem supr_sup_eq {f g : β → α} : (⨆ x, f x ⊔ g x) = (⨆ x, f x) ⊔ (⨆ x, g x) :=
 @infi_inf_eq (order_dual α) β _ _ _
 
+lemma supr_sup [h : nonempty ι] {f : ι → α} {a : α} : (⨆ x, f x) ⊔ a = (⨆ x, f x ⊔ a) :=
+@infi_inf (order_dual α) _ _ _ _ _
+
+lemma sup_supr [nonempty ι] {f : ι → α} {a : α} : a ⊔ (⨆ x, f x) = (⨆ x, a ⊔ f x) :=
+@inf_infi (order_dual α) _ _ _ _ _
+
 /- supr and infi under Prop -/
 
 @[simp] theorem infi_false {s : false → α} : infi s = ⊤ :=