From a239cd3e7ac2c7cde36c913808f9d40c411344f6 Mon Sep 17 00:00:00 2001 From: Siddhartha Prasad Date: Wed, 25 Jan 2023 14:10:24 +0000 Subject: [PATCH] feat(algebra/order/kleene) : Kleene algebras (#17965) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Define idempotent semirings and Kleene algebras, which are used extensively in the theory of computation. Co-authored-by: Siddhartha Prasad Co-authored-by: Siddhartha Prasad Co-authored-by: Siddhartha Prasad Co-authored-by: Yaël Dillies --- docs/references.bib | 16 ++ src/algebra/order/kleene.lean | 291 +++++++++++++++++++++ src/computability/DFA.lean | 9 +- src/computability/NFA.lean | 3 +- src/computability/epsilon_NFA.lean | 4 +- src/computability/language.lean | 92 +++---- src/computability/regular_expressions.lean | 9 +- 7 files changed, 369 insertions(+), 55 deletions(-) create mode 100644 src/algebra/order/kleene.lean diff --git a/docs/references.bib b/docs/references.bib index 32680882acc87..3d2220c570725 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -1405,6 +1405,22 @@ @Article{ KoukoulopoulosMaynard2020 url = {https://doi.org/10.4007/annals.2020.192.1.5}, } +@Article{ kozen1994, + title = {A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events}, + journal = {Information and Computation}, + volume = {110}, + number = {2}, + pages = {366-390}, + year = {1994}, + issn = {0890-5401}, + doi = {https://doi.org/10.1006/inco.1994.1037}, + url = {https://www.sciencedirect.com/science/article/pii/S0890540184710376}, + author = {D. Kozen}, + abstract = {We give a finitary axiomatization of the algebra of regular events involving only + equations and equational implications. Unlike Salomaa′s axiomatizations, the + axiomatization given here is sound for all interpretations over Kleene algebras.} +} + @Article{ lazarus1973, author = {Michel Lazarus}, title = {Les familles libres maximales d'un module ont-elles le diff --git a/src/algebra/order/kleene.lean b/src/algebra/order/kleene.lean new file mode 100644 index 0000000000000..0a2487a126cdf --- /dev/null +++ b/src/algebra/order/kleene.lean @@ -0,0 +1,291 @@ +/- +Copyright (c) 2022 Siddhartha Prasad, Yaël Dillies. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Prasad, Yaël Dillies +-/ +import algebra.order.ring.canonical +import algebra.ring.pi +import algebra.ring.prod +import order.hom.complete_lattice + +/-! +# Kleene Algebras + +This file defines idempotent semirings and Kleene algebras, which are used extensively in the theory +of computation. + +An idempotent semiring is a semiring whose addition is idempotent. An idempotent semiring is +naturally a semilattice by setting `a ≤ b` if `a + b = b`. + +A Kleene algebra is an idempotent semiring equipped with an additional unary operator `∗`, the +Kleene star. + +## Main declarations + +* `idem_semiring`: Idempotent semiring +* `idem_comm_semiring`: Idempotent commutative semiring +* `kleene_algebra`: Kleene algebra + +## Notation + +`a∗` is notation for `kstar a` in locale `computability`. + +## References + +* [D. Kozen, *A completeness theorem for Kleene algebras and the algebra of regular events*] + [kozen1994] +* https://planetmath.org/idempotentsemiring +* https://encyclopediaofmath.org/wiki/Idempotent_semi-ring +* https://planetmath.org/kleene_algebra + +## TODO + +Instances for `add_opposite`, `mul_opposite`, `ulift`, `subsemiring`, `subring`, `subalgebra`. + +## Tags + +kleene algebra, idempotent semiring +-/ + +set_option old_structure_cmd true + +open function + +universe u +variables {α β ι : Type*} {π : ι → Type*} + +/-- An idempotent semiring is a semiring with the additional property that addition is idempotent. +-/ +@[protect_proj] +class idem_semiring (α : Type u) extends semiring α, semilattice_sup α := +(sup := (+)) +(add_eq_sup : ∀ a b : α, a + b = a ⊔ b . try_refl_tac) +(bot : α := 0) +(bot_le : ∀ a, bot ≤ a) + +/-- An idempotent commutative semiring is a commutative semiring with the additional property that +addition is idempotent. -/ +@[protect_proj] +class idem_comm_semiring (α : Type u) extends comm_semiring α, idem_semiring α + +/-- Notation typeclass for the Kleene star `∗`. -/ +@[protect_proj] +class has_kstar (α : Type*) := +(kstar : α → α) + +localized "postfix `∗`:1025 := has_kstar.kstar" in computability + +/-- A Kleene Algebra is an idempotent semiring with an additional unary operator `kstar` (for Kleene +star) that satisfies the following properties: +* `1 + a * a∗ ≤ a∗` +* `1 + a∗ * a ≤ a∗` +* If `a * c + b ≤ c`, then `a∗ * b ≤ c` +* If `c * a + b ≤ c`, then `b * a∗ ≤ c` +-/ +@[protect_proj] +class kleene_algebra (α : Type*) extends idem_semiring α, has_kstar α := +(one_le_kstar : ∀ a : α, 1 ≤ a∗) +(mul_kstar_le_kstar : ∀ a : α, a * a∗ ≤ a∗) +(kstar_mul_le_kstar : ∀ a : α, a∗ * a ≤ a∗) +(mul_kstar_le_self : ∀ a b : α, b * a ≤ b → b * a∗ ≤ b) +(kstar_mul_le_self : ∀ a b : α, a * b ≤ b → a∗ * b ≤ b) + +@[priority 100] -- See note [lower instance priority] +instance idem_semiring.to_order_bot [idem_semiring α] : order_bot α := { ..‹idem_semiring α› } + +/-- Construct an idempotent semiring from an idempotent addition. -/ +@[reducible] -- See note [reducible non-instances] +def idem_semiring.of_semiring [semiring α] (h : ∀ a : α, a + a = a) : idem_semiring α := +{ le := λ a b, a + b = b, + le_refl := h, + le_trans := λ a b c (hab : _ = _) (hbc : _ = _), by { change _ = _, rw [←hbc, ←add_assoc, hab] }, + le_antisymm := λ a b (hab : _ = _) (hba : _ = _), by rwa [←hba, add_comm], + sup := (+), + le_sup_left := λ a b, by { change _ = _, rw [←add_assoc, h] }, + le_sup_right := λ a b, by { change _ = _, rw [add_comm, add_assoc, h] }, + sup_le := λ a b c hab (hbc : _ = _), by { change _ = _, rwa [add_assoc, hbc] }, + bot := 0, + bot_le := zero_add, + ..‹semiring α› } + +section idem_semiring +variables [idem_semiring α] {a b c : α} + +@[simp] lemma add_eq_sup (a b : α) : a + b = a ⊔ b := idem_semiring.add_eq_sup _ _ +lemma add_idem (a : α) : a + a = a := by simp + +lemma nsmul_eq_self : ∀ {n : ℕ} (hn : n ≠ 0) (a : α), n • a = a +| 0 h := (h rfl).elim +| 1 h := one_nsmul +| (n + 2) h := λ a, by rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem] + +lemma add_eq_left_iff_le : a + b = a ↔ b ≤ a := by simp +lemma add_eq_right_iff_le : a + b = b ↔ a ≤ b := by simp + +alias add_eq_left_iff_le ↔ _ has_le.le.add_eq_left +alias add_eq_right_iff_le ↔ _ has_le.le.add_eq_right + +lemma add_le_iff : a + b ≤ c ↔ a ≤ c ∧ b ≤ c := by simp +lemma add_le (ha : a ≤ c) (hb : b ≤ c) : a + b ≤ c := add_le_iff.2 ⟨ha, hb⟩ + +@[priority 100] -- See note [lower instance priority] +instance idem_semiring.to_canonically_ordered_add_monoid : canonically_ordered_add_monoid α := +{ add_le_add_left := λ a b hbc c, by { simp_rw add_eq_sup, exact sup_le_sup_left hbc _ }, + exists_add_of_le := λ a b h, ⟨b, h.add_eq_right.symm⟩, + le_self_add := λ a b, add_eq_right_iff_le.1 $ by rw [←add_assoc, add_idem], + ..‹idem_semiring α› } + +@[priority 100] -- See note [lower instance priority] +instance idem_semiring.to_covariant_class_mul_le : covariant_class α α (*) (≤) := +⟨λ a b c hbc, add_eq_left_iff_le.1 $ by rw [←mul_add, hbc.add_eq_left]⟩ + +@[priority 100] -- See note [lower instance priority] +instance idem_semiring.to_covariant_class_swap_mul_le : covariant_class α α (swap (*)) (≤) := +⟨λ a b c hbc, add_eq_left_iff_le.1 $ by rw [←add_mul, hbc.add_eq_left]⟩ + +end idem_semiring + +section kleene_algebra +variables [kleene_algebra α] {a b c : α} + +@[simp] lemma one_le_kstar : 1 ≤ a∗ := kleene_algebra.one_le_kstar _ +lemma mul_kstar_le_kstar : a * a∗ ≤ a∗ := kleene_algebra.mul_kstar_le_kstar _ +lemma kstar_mul_le_kstar : a∗ * a ≤ a∗ := kleene_algebra.kstar_mul_le_kstar _ +lemma mul_kstar_le_self : b * a ≤ b → b * a∗ ≤ b := kleene_algebra.mul_kstar_le_self _ _ +lemma kstar_mul_le_self : a * b ≤ b → a∗ * b ≤ b := kleene_algebra.kstar_mul_le_self _ _ + +lemma mul_kstar_le (hb : b ≤ c) (ha : c * a ≤ c) : b * a∗ ≤ c := +(mul_le_mul_right' hb _).trans $ mul_kstar_le_self ha + +lemma kstar_mul_le (hb : b ≤ c) (ha : a * c ≤ c) : a∗ * b ≤ c := +(mul_le_mul_left' hb _).trans $ kstar_mul_le_self ha + +lemma kstar_le_of_mul_le_left (hb : 1 ≤ b) : b * a ≤ b → a∗ ≤ b := by simpa using mul_kstar_le hb +lemma kstar_le_of_mul_le_right (hb : 1 ≤ b) : a * b ≤ b → a∗ ≤ b := by simpa using kstar_mul_le hb + +@[simp] lemma le_kstar : a ≤ a∗ := le_trans (le_mul_of_one_le_left' one_le_kstar) kstar_mul_le_kstar + +@[mono] lemma kstar_mono : monotone (has_kstar.kstar : α → α) := +λ a b h, kstar_le_of_mul_le_left one_le_kstar $ kstar_mul_le (h.trans le_kstar) $ + mul_kstar_le_kstar + +@[simp] lemma kstar_eq_one : a∗ = 1 ↔ a ≤ 1 := +⟨le_kstar.trans_eq, λ h, one_le_kstar.antisymm' $ kstar_le_of_mul_le_left le_rfl $ by rwa one_mul⟩ + +@[simp] lemma kstar_zero : (0 : α)∗ = 1 := kstar_eq_one.2 zero_le_one +@[simp] lemma kstar_one : (1 : α)∗ = 1 := kstar_eq_one.2 le_rfl + +@[simp] lemma kstar_mul_kstar (a : α) : a∗ * a∗ = a∗ := +(mul_kstar_le le_rfl $ kstar_mul_le_kstar).antisymm $ le_mul_of_one_le_left' one_le_kstar + +@[simp] lemma kstar_eq_self : a∗ = a ↔ a * a = a ∧ 1 ≤ a := +⟨λ h, ⟨by rw [←h, kstar_mul_kstar], one_le_kstar.trans_eq h⟩, λ h, + (kstar_le_of_mul_le_left h.2 h.1.le).antisymm le_kstar⟩ + +@[simp] lemma kstar_idem (a : α) : a∗∗ = a∗ := kstar_eq_self.2 ⟨kstar_mul_kstar _, one_le_kstar⟩ + +@[simp] lemma pow_le_kstar : ∀ {n : ℕ}, a ^ n ≤ a∗ +| 0 := (pow_zero _).trans_le one_le_kstar +| (n + 1) := by {rw pow_succ, exact (mul_le_mul_left' pow_le_kstar _).trans mul_kstar_le_kstar } + +end kleene_algebra + +namespace prod + +instance [idem_semiring α] [idem_semiring β] : idem_semiring (α × β) := +{ add_eq_sup := λ a b, ext (add_eq_sup _ _) (add_eq_sup _ _), + ..prod.semiring, ..prod.semilattice_sup _ _, ..prod.order_bot _ _ } + +instance [idem_comm_semiring α] [idem_comm_semiring β] : idem_comm_semiring (α × β) := +{ ..prod.comm_semiring, ..prod.idem_semiring } + +variables [kleene_algebra α] [kleene_algebra β] + +instance : kleene_algebra (α × β) := +{ kstar := λ a, (a.1∗, a.2∗), + one_le_kstar := λ a, ⟨one_le_kstar, one_le_kstar⟩, + mul_kstar_le_kstar := λ a, ⟨mul_kstar_le_kstar, mul_kstar_le_kstar⟩, + kstar_mul_le_kstar := λ a, ⟨kstar_mul_le_kstar, kstar_mul_le_kstar⟩, + mul_kstar_le_self := λ a b, and.imp mul_kstar_le_self mul_kstar_le_self, + kstar_mul_le_self := λ a b, and.imp kstar_mul_le_self kstar_mul_le_self, + ..prod.idem_semiring } + +lemma kstar_def (a : α × β) : a∗ = (a.1∗, a.2∗) := rfl +@[simp] lemma fst_kstar (a : α × β) : a∗.1 = a.1∗ := rfl +@[simp] lemma snd_kstar (a : α × β) : a∗.2 = a.2∗ := rfl + +end prod + +namespace pi + +instance [Π i, idem_semiring (π i)] : idem_semiring (Π i, π i) := +{ add_eq_sup := λ a b, funext $ λ i, add_eq_sup _ _, + ..pi.semiring, ..pi.semilattice_sup, ..pi.order_bot } + +instance [Π i, idem_comm_semiring (π i)] : idem_comm_semiring (Π i, π i) := +{ ..pi.comm_semiring, ..pi.idem_semiring } + +variables [Π i, kleene_algebra (π i)] + +instance : kleene_algebra (Π i, π i) := +{ kstar := λ a i, (a i)∗, + one_le_kstar := λ a i, one_le_kstar, + mul_kstar_le_kstar := λ a i, mul_kstar_le_kstar, + kstar_mul_le_kstar := λ a i, kstar_mul_le_kstar, + mul_kstar_le_self := λ a b h i, mul_kstar_le_self $ h _, + kstar_mul_le_self := λ a b h i, kstar_mul_le_self $ h _, + ..pi.idem_semiring } + +lemma kstar_def (a : Π i, π i) : a∗ = λ i, (a i)∗ := rfl +@[simp] lemma kstar_apply (a : Π i, π i) (i : ι) : a∗ i = (a i)∗ := rfl + +end pi + +namespace function.injective + +/-- Pullback an `idem_semiring` instance along an injective function. -/ +@[reducible] -- See note [reducible non-instances] +protected def idem_semiring [idem_semiring α] [has_zero β] [has_one β] [has_add β] [has_mul β] + [has_pow β ℕ] [has_smul ℕ β] [has_nat_cast β] [has_sup β] [has_bot β] + (f : β → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1) + (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) + (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) + (nat_cast : ∀ n : ℕ, f n = n) (sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) : + idem_semiring β := +{ add_eq_sup := λ a b, hf $ by erw [sup, add, add_eq_sup], + bot := ⊥, + bot_le := λ a, bot.trans_le $ @bot_le _ _ _ $ f a, + ..hf.semiring f zero one add mul nsmul npow nat_cast, ..hf.semilattice_sup _ sup, ..‹has_bot β› } + +/-- Pullback an `idem_comm_semiring` instance along an injective function. -/ +@[reducible] -- See note [reducible non-instances] +protected def idem_comm_semiring [idem_comm_semiring α] [has_zero β] [has_one β] [has_add β] + [has_mul β] [has_pow β ℕ] [has_smul ℕ β] [has_nat_cast β] [has_sup β] [has_bot β] + (f : β → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1) + (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) + (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) + (nat_cast : ∀ n : ℕ, f n = n) (sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) : + idem_comm_semiring β := +{ ..hf.comm_semiring f zero one add mul nsmul npow nat_cast, + ..hf.idem_semiring f zero one add mul nsmul npow nat_cast sup bot } + +/-- Pullback an `idem_comm_semiring` instance along an injective function. -/ +@[reducible] -- See note [reducible non-instances] +protected def kleene_algebra [kleene_algebra α] [has_zero β] [has_one β] [has_add β] + [has_mul β] [has_pow β ℕ] [has_smul ℕ β] [has_nat_cast β] [has_sup β] [has_bot β] [has_kstar β] + (f : β → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1) + (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) + (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) + (nat_cast : ∀ n : ℕ, f n = n) (sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) + (kstar : ∀ a, f a∗ = (f a)∗) : + kleene_algebra β := +{ one_le_kstar := λ a, one.trans_le $ by { erw kstar, exact one_le_kstar }, + mul_kstar_le_kstar := λ a, by { change f _ ≤ _, erw [mul, kstar], exact mul_kstar_le_kstar }, + kstar_mul_le_kstar := λ a, by { change f _ ≤ _, erw [mul, kstar], exact kstar_mul_le_kstar }, + mul_kstar_le_self := λ a b (h : f _ ≤ _), + by { change f _ ≤ _, erw [mul, kstar], erw mul at h, exact mul_kstar_le_self h }, + kstar_mul_le_self := λ a b (h : f _ ≤ _), + by { change f _ ≤ _, erw [mul, kstar], erw mul at h, exact kstar_mul_le_self h }, + ..hf.idem_semiring f zero one add mul nsmul npow nat_cast sup bot, ..‹has_kstar β› } + +end function.injective diff --git a/src/computability/DFA.lean b/src/computability/DFA.lean index 57ab5cfe17b0e..0c815938b9a00 100644 --- a/src/computability/DFA.lean +++ b/src/computability/DFA.lean @@ -10,6 +10,7 @@ import tactic.norm_num /-! # Deterministic Finite Automata + This file contains the definition of a Deterministic Finite Automaton (DFA), a state machine which determines whether a string (implemented as a list over an arbitrary alphabet) is in a regular set in linear time. @@ -17,6 +18,8 @@ Note that this definition allows for Automaton with infinite states, a `fintype` supplied for true DFA's. -/ +open_locale computability + universes u v /-- A DFA is a set of states (`σ`), a transition function from state to state labelled by the @@ -109,9 +112,9 @@ begin 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 := + (hy : y ∈ ({x} : language α)∗) : M.eval_from s y = s := begin - rw language.mem_star at hy, + rw language.mem_kstar at hy, rcases hy with ⟨ S, rfl, hS ⟩, induction S with a S ih, { refl }, @@ -126,7 +129,7 @@ end lemma pumping_lemma [fintype σ] {x : list α} (hx : x ∈ M.accepts) (hlen : fintype.card σ ≤ list.length x) : ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ fintype.card σ ∧ b ≠ [] ∧ - {a} * language.star {b} * {c} ≤ M.accepts := + {a} * {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], diff --git a/src/computability/NFA.lean b/src/computability/NFA.lean index ab90f0f21d938..b1fce95851172 100644 --- a/src/computability/NFA.lean +++ b/src/computability/NFA.lean @@ -18,6 +18,7 @@ supplied for true NFA's. -/ open set +open_locale computability universes u v @@ -89,7 +90,7 @@ end lemma pumping_lemma [fintype σ] {x : list α} (hx : x ∈ M.accepts) (hlen : fintype.card (set σ) ≤ list.length x) : ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ fintype.card (set σ) ∧ b ≠ [] ∧ - {a} * language.star {b} * {c} ≤ M.accepts := + {a} * {b}∗ * {c} ≤ M.accepts := begin rw ←to_DFA_correct at hx ⊢, exact M.to_DFA.pumping_lemma hx hlen diff --git a/src/computability/epsilon_NFA.lean b/src/computability/epsilon_NFA.lean index 1b81ac03f9390..6faa55eafe884 100644 --- a/src/computability/epsilon_NFA.lean +++ b/src/computability/epsilon_NFA.lean @@ -8,6 +8,7 @@ import computability.NFA /-! # Epsilon Nondeterministic Finite Automata + This file contains the definition of an epsilon Nondeterministic Finite Automaton (`ε_NFA`), a state machine which determines whether a string (implemented as a list over an arbitrary alphabet) is in a regular set by evaluating the string over every possible path, also having access to ε-transitons, @@ -17,6 +18,7 @@ supplied for true `ε_NFA`'s. -/ open set +open_locale computability universes u v @@ -116,7 +118,7 @@ end lemma pumping_lemma [fintype σ] {x : list α} (hx : x ∈ M.accepts) (hlen : fintype.card (set σ) ≤ list.length x) : ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ fintype.card (set σ) ∧ b ≠ [] ∧ - {a} * language.star {b} * {c} ≤ M.accepts := + {a} * {b}∗ * {c} ≤ M.accepts := begin rw ←to_NFA_correct at hx ⊢, exact M.to_NFA.pumping_lemma hx hlen diff --git a/src/computability/language.lean b/src/computability/language.lean index 2a2f1e673acfd..ae2ef1a0e5ef4 100644 --- a/src/computability/language.lean +++ b/src/computability/language.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fox Thomson -/ import algebra.hom.ring +import algebra.order.kleene import data.list.join import data.set.lattice @@ -17,6 +18,7 @@ over the languages. -/ open list set +open_locale computability universes v @@ -51,23 +53,23 @@ lemma one_def : (1 : language α) = {[]} := rfl lemma add_def (l m : language α) : l + m = l ∪ m := rfl lemma mul_def (l m : language α) : l * m = image2 (++) l m := rfl -/-- The star of a language `L` is the set of all strings which can be written by concatenating - strings from `L`. -/ -def star (l : language α) : language α := -{ x | ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l} +/-- The Kleene star of a language `L` is the set of all strings which can be written by +concatenating strings from `L`. -/ +instance : has_kstar (language α) := ⟨λ l, {x | ∃ L : list (list α), x = L.join ∧ ∀ y ∈ L, y ∈ l}⟩ + +lemma kstar_def (l : language α) : l∗ = {x | ∃ L : list (list α), x = L.join ∧ ∀ y ∈ L, y ∈ l} := +rfl -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 @[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_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⟩ +lemma mem_kstar : x ∈ l∗ ↔ ∃ L : list (list α), x = L.join ∧ ∀ y ∈ L, y ∈ l := iff.rfl +lemma join_mem_kstar {L : list (list α)} (h : ∀ y ∈ L, y ∈ l) : L.join ∈ l∗ := ⟨L, rfl, h⟩ +lemma nil_mem_kstar (l : language α) : [] ∈ l∗ := ⟨[], rfl, λ _, false.elim⟩ instance : semiring (language α) := { add := (+), @@ -103,8 +105,8 @@ def map (f : α → β) : language α →+* language β := @[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 ≠ []} := +lemma kstar_def_nonempty (l : language α) : + l∗ = {x | ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []} := begin ext x, split, @@ -162,56 +164,54 @@ begin exact ⟨a, _, hS.1, ⟨S, rfl, rfl, hS.2⟩, rfl⟩ } } end -lemma star_eq_supr_pow (l : language α) : l.star = ⨆ i : ℕ, l ^ i := +lemma kstar_eq_supr_pow (l : language α) : l∗ = ⨆ i : ℕ, l ^ i := begin ext x, - simp only [mem_star, mem_supr, mem_pow], + simp only [mem_kstar, mem_supr, mem_pow], split, { rintro ⟨S, rfl, hS⟩, exact ⟨_, S, rfl, rfl, hS⟩ }, { 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) := +@[simp] lemma map_kstar (f : α → β) (l : language α) : map f l∗ = (map f l)∗ := begin - rw [star_eq_supr_pow, star_eq_supr_pow], + rw [kstar_eq_supr_pow, kstar_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'] +lemma mul_self_kstar_comm (l : language α) : l∗ * l = l * l∗ := +by simp only [kstar_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 := +@[simp] lemma one_add_self_mul_kstar_eq_kstar (l : language α) : 1 + l * l∗ = l∗ := begin - simp only [star_eq_supr_pow, mul_supr, ← pow_succ, ← pow_zero l], + simp only [kstar_eq_supr_pow, mul_supr, ← pow_succ, ← pow_zero l], exact sup_supr_nat_succ _ 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_rfl 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_rfl) ih -end +@[simp] lemma one_add_kstar_mul_self_eq_kstar (l : language α) : 1 + l∗ * l = l∗ := +by rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar] + +instance : kleene_algebra (language α) := +{ one_le_kstar := λ a l hl, ⟨[], hl, by simp⟩, + mul_kstar_le_kstar := λ a, (one_add_self_mul_kstar_eq_kstar a).le.trans' le_sup_right, + kstar_mul_le_kstar := λ a, (one_add_kstar_mul_self_eq_kstar a).le.trans' le_sup_right, + kstar_mul_le_self := λ l m h, begin + rw [kstar_eq_supr_pow, supr_mul], + refine supr_le (λ n, _), + induction n with n ih, + { simp }, + rw [pow_succ', mul_assoc (l^n) l m], + exact le_trans (le_mul_congr le_rfl h) ih, + end, + mul_kstar_le_self := λ l m h, begin + rw [kstar_eq_supr_pow, mul_supr], + refine supr_le (λ n, _), + induction n with n ih, + { simp }, + rw [pow_succ, ←mul_assoc m l (l^n)], + exact le_trans (le_mul_congr h le_rfl) ih, + end, + ..language.semiring, ..set.complete_boolean_algebra, ..language.has_kstar } end language diff --git a/src/computability/regular_expressions.lean b/src/computability/regular_expressions.lean index bcd047edbcfd6..d1f36e987068e 100644 --- a/src/computability/regular_expressions.lean +++ b/src/computability/regular_expressions.lean @@ -20,6 +20,7 @@ computer science such as the POSIX standard. -/ open list set +open_locale computability universe u @@ -69,7 +70,7 @@ attribute [pattern] has_mul.mul | (char a) := {[a]} | (P + Q) := P.matches + Q.matches | (P * Q) := P.matches * Q.matches -| (star P) := P.matches.star +| (star P) := P.matches∗ @[simp] lemma matches_zero : (0 : regular_expression α).matches = 0 := rfl @[simp] lemma matches_epsilon : (1 : regular_expression α).matches = 1 := rfl @@ -82,7 +83,7 @@ attribute [pattern] has_mul.mul ∀ n : ℕ, (P ^ n).matches = P.matches ^ n | 0 := matches_epsilon | (n + 1) := (matches_mul _ _).trans $ eq.trans (congr_arg _ (matches_pow n)) (pow_succ _ _).symm -@[simp] lemma matches_star (P : regular_expression α) : P.star.matches = P.matches.star := rfl +@[simp] lemma matches_star (P : regular_expression α) : P.star.matches = P.matches∗ := rfl /-- `match_epsilon P` is true if and only if `P` matches the empty string -/ def match_epsilon : regular_expression α → bool @@ -299,7 +300,7 @@ begin rw ←ih₂ at hmatch₂, exact ⟨ x, y, hsum.symm, hmatch₁, hmatch₂ ⟩ } }, case star : _ ih - { rw [star_rmatch_iff, language.star_def_nonempty], + { rw [star_rmatch_iff, language.kstar_def_nonempty], split, all_goals { rintro ⟨ S, hx, hS ⟩, @@ -363,7 +364,7 @@ omit dec | (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], + rw [language.kstar_eq_supr_pow, language.kstar_eq_supr_pow], simp_rw ←map_pow, exact image_Union.symm, end