Language.v 7.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265
  1. (* Copyright © 2019 Ariadne Devos
  2. SPDX-License-Identifier: GPL-2.0 or GPL-3.0 *)
  3. Require Import Trace.
  4. Require Import Coq.Setoids.Setoid.
  5. Require Import Coq.Sets.Ensembles.
  6. Require Import Coq.Classes.Morphisms.
  7. Require Import Coq.Arith.PeanoNat.
  8. Require Import Lattice.
  9. (* A composable definition of regular expression
  10. applied to possibly infinite strings.
  11. Leibniz equality of symbols is assumed *)
  12. Section Language.
  13. (* equality: leibniz *)
  14. Variable A : Type.
  15. Definition word := trace A.
  16. (* Equivalency of languages.
  17. A language is a set of allowed words. *)
  18. Definition language := Ensemble word.
  19. (* The level is a wild guess, correct in case of
  20. strange parsings. *)
  21. Local Notation "a 'l∈' l" := ((l : language) (a : word)) (at level 50).
  22. (* Languages are equivalent if they accept the same words *)
  23. Definition lang_eqv (a : language) (b : language) :=
  24. forall k : word, k l∈ a <-> k l∈ b.
  25. Local Notation "a '≣' b" := (lang_eqv (a : language) (b : language)) (at level 30).
  26. Lemma lang_eqv_refl a : a ≣ a.
  27. Proof. unfold lang_eqv. tauto. Qed.
  28. Lemma lang_eqv_sym a b : a ≣ b -> b ≣ a.
  29. Proof. unfold lang_eqv. firstorder. Qed.
  30. Lemma lang_eqv_trans a b c : a ≣ b -> b ≣ c -> a ≣ c.
  31. Proof. unfold lang_eqv. firstorder. Qed.
  32. Add Parametric Relation: (language) lang_eqv
  33. reflexivity proved by (lang_eqv_refl)
  34. symmetry proved by (lang_eqv_sym)
  35. transitivity proved by (lang_eqv_trans)
  36. as lang_equiv.
  37. (* epsilon, constant symbols and concatenation *)
  38. Section Little.
  39. (* only a single word *)
  40. Definition fixed_string : word -> language := Singleton word.
  41. (* empty word *)
  42. Definition epsilon : language := fixed_string (Done A).
  43. Theorem fixed_string_empty_eqv_epsilon : fixed_string (Done A) ≣ epsilon.
  44. Proof. unfold epsilon. reflexivity. Qed.
  45. Theorem fixed_string_self (w : word) : w l∈ fixed_string w.
  46. Proof. unfold fixed_string. constructor. Qed.
  47. Inductive concat : language -> language -> language :=
  48. | ConcatMatch (a : language) (b : language) (t : word) (u : word) (match_at : t l∈ a) (match_bu : u l∈ b)
  49. : concat a b (seq A t u).
  50. Add Parametric Morphism : concat with
  51. signature (lang_eqv ==> lang_eqv ==> lang_eqv) as concat_morphism.
  52. Proof. (* Somewhat brute-force, but quite effective *)
  53. unfold lang_eqv.
  54. firstorder.
  55. all : (inversion H1; subst k; constructor).
  56. all : firstorder.
  57. Qed.
  58. Theorem fixed_string_match_equal (v : word) (u : word) : u l∈ fixed_string v -> u = v.
  59. Proof. simpl. intro K; inversion K; reflexivity. Qed.
  60. (* bring constants together *)
  61. Theorem concat_single (v : word) (w : word) : concat (fixed_string v) (fixed_string w) ≣ (fixed_string (seq A v w)).
  62. Proof.
  63. split. all : intro H.
  64. + inversion H; clear H H2 H1 H0.
  65. inversion match_at; clear match_at H.
  66. rewrite (fixed_string_match_equal w u match_bu).
  67. reflexivity.
  68. + inversion H; clear H H0.
  69. constructor.
  70. all : reflexivity.
  71. Qed.
  72. (* concat, epsilon is a monoid *)
  73. (* epsilon is neutral *)
  74. Theorem concat_epsilon_l (a : language) : concat epsilon a ≣ a.
  75. Proof.
  76. split. all : intro K.
  77. + inversion K.
  78. inversion match_at.
  79. rewrite seq_nil_l.
  80. assumption.
  81. + rewrite <- seq_nil_l.
  82. constructor.
  83. - constructor.
  84. - assumption.
  85. Qed.
  86. Theorem concat_epsilon_r (a : language) : concat a epsilon ≣ a.
  87. Proof.
  88. split. all : intro K.
  89. + inversion K.
  90. inversion match_bu.
  91. rewrite seq_nil_r.
  92. assumption.
  93. + rewrite <- seq_nil_r.
  94. constructor.
  95. - assumption.
  96. - constructor.
  97. Qed.
  98. (* concat is associative *)
  99. Lemma concat_assoc a b c : concat (concat a b) c ≣ concat a (concat b c).
  100. Proof.
  101. split. all : intro H.
  102. + inversion H; clear H H2 H1 H0.
  103. inversion match_at; clear match_at H1 H0 H.
  104. rewrite seq_assoc.
  105. constructor.
  106. assumption.
  107. constructor.
  108. all : assumption.
  109. + inversion H; clear H H2 H1 H0.
  110. inversion match_bu; clear match_bu H1 u H0 H.
  111. rewrite <- seq_assoc.
  112. constructor.
  113. constructor.
  114. all : assumption.
  115. Qed.
  116. End Little.
  117. Section Choice.
  118. (* recognise everything *)
  119. Definition anything : language := fun _ => True.
  120. (* recognise nothing *)
  121. Definition nothing : language := fun _ => False.
  122. (* a choice between two languages *)
  123. Definition or these those : language := fun (w : word) => these w \/ those w.
  124. (* both languages at the same time *)
  125. Definition and these those : language := fun (w : word) => these w /\ those w.
  126. Add Parametric Morphism : or with
  127. signature (lang_eqv ==> lang_eqv ==> lang_eqv) as or_morphism.
  128. Proof. firstorder. Qed.
  129. Add Parametric Morphism : and with
  130. signature (lang_eqv ==> lang_eqv ==> lang_eqv) as and_morphism.
  131. Proof. firstorder. Qed.
  132. (* or, and have a minimum and a maximum *)
  133. Lemma or_and_lattice_bottom_top : bounded_lattice_theory language lang_eqv or and nothing anything.
  134. Proof. firstorder. Qed.
  135. (* or, and are joins and meets *)
  136. Lemma or_and_lattice : lattice_theory language lang_eqv or and.
  137. Proof. exact (lattice _ _ _ _ _ _ or_and_lattice_bottom_top). Qed.
  138. (* or, and distribute over each other *)
  139. Lemma or_and_distr : distributive_theory language lang_eqv or and.
  140. Proof. firstorder. Qed.
  141. End Choice.
  142. Section Repetition.
  143. (* repeatedly concat a language, a finite number of times *)
  144. Inductive repeatN : nat -> language -> language :=
  145. | Repeat0 r : (Done _) l∈ repeatN 0 r
  146. | RepeatS r n u v : u l∈ r -> v l∈ repeatN n r -> seq _ u v l∈ repeatN (S n) r.
  147. Theorem repeat0 r : repeatN 0 r ≣ epsilon.
  148. Proof.
  149. split.
  150. all : (intro P; inversion P; constructor).
  151. Qed.
  152. Theorem combine_repeatNM r : forall n m t u, repeatN n r t -> repeatN m r u -> repeatN (n + m) r (seq _ t u).
  153. Proof.
  154. intro n.
  155. induction n.
  156. all : intros.
  157. + rewrite Nat.add_0_l.
  158. inversion H.
  159. rewrite seq_nil_l.
  160. assumption.
  161. + inversion H; clear H.
  162. clear H4 r0.
  163. rewrite Nat.add_succ_l.
  164. rewrite seq_assoc.
  165. constructor.
  166. - assumption.
  167. - apply IHn.
  168. all : assumption.
  169. Qed.
  170. (* An unbounded but finite number of repetitions.
  171. (TODO: how is the Kleene closure defined?
  172. From a quick look at his paper and some reminiscences
  173. of articles, he might even have conceived regular languages
  174. for checking infinite traces of events to match a safe
  175. pattern) *)
  176. Definition finiteStar r : language := fun w => exists k, w l∈ repeatN k r.
  177. Theorem finiteStar_epsilon_ok r w : w l∈ epsilon -> w l∈ finiteStar r.
  178. Proof.
  179. intro P; destruct P.
  180. cbv.
  181. refine (ex_intro _ 0 _).
  182. constructor.
  183. Qed.
  184. Theorem finiteStar_epsilon : finiteStar epsilon ≣ epsilon.
  185. Proof.
  186. split. all : intro P.
  187. 2 : apply (finiteStar_epsilon_ok _ _ P).
  188. destruct P.
  189. induction x.
  190. - inversion H. constructor.
  191. - inversion H.
  192. destruct H1.
  193. rewrite seq_nil_l in H4.
  194. subst v.
  195. rewrite seq_nil_l.
  196. apply IHx.
  197. assumption.
  198. Qed.
  199. Theorem finiteStar_seq r : concat (finiteStar r) (finiteStar r) ≣ finiteStar r.
  200. Proof.
  201. split. all : intro P.
  202. + unfold finiteStar.
  203. unfold finiteStar in P.
  204. inversion P; clear P.
  205. destruct match_at, match_bu.
  206. refine (ex_intro _ (x + x0) _).
  207. apply combine_repeatNM.
  208. all : assumption.
  209. + inversion P.
  210. rewrite <- seq_nil_r.
  211. constructor.
  212. - exact (ex_intro _ x H).
  213. - eapply finiteStar_epsilon_ok.
  214. constructor.
  215. Qed.
  216. (* And, in principle, r** = r*, although I don't believe
  217. the former occurs in practice *)
  218. (* TODO: infinite repeating, without vacuousity
  219. (RFCs don't specify those, for it is rather
  220. incomputable), closure operator (which one, exactly?)
  221. (* not really a priority *) *)
  222. End Repetition.
  223. End Language.