shttpd/coq/Language.v

(* Copyright © 2019 Ariadne Devos
   SPDX-License-Identifier: GPL-2.0 or GPL-3.0 *)

Require Import Trace.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Arith.PeanoNat.
Require Import Lattice.

(* A composable definition of regular expression
   applied to possibly infinite strings.
   Leibniz equality of symbols is assumed *)
Section Language.

(* equality: leibniz *)
Variable A : Type.

Definition word := trace A.

(* Equivalency of languages.
   A language is a set of allowed words. *)
Definition language := Ensemble word.

(* The level is a wild guess, correct in case of
   strange parsings. *)
Local Notation "a 'l∈' l" := ((l : language) (a : word)) (at level 50).

(* Languages are equivalent if they accept the same words *)
Definition lang_eqv (a : language) (b : language) :=
  forall k : word, k l∈ a <-> k l∈ b.

Local Notation "a '≣' b" := (lang_eqv (a : language) (b : language)) (at level 30).

Lemma lang_eqv_refl a : a ≣ a.
Proof. unfold lang_eqv. tauto. Qed.
Lemma lang_eqv_sym a b : a ≣ b -> b ≣ a.
Proof. unfold lang_eqv. firstorder. Qed.
Lemma lang_eqv_trans a b c : a ≣ b -> b ≣ c -> a ≣ c.
Proof. unfold lang_eqv. firstorder. Qed.

Add Parametric Relation: (language) lang_eqv
    reflexivity proved by (lang_eqv_refl)
    symmetry proved by (lang_eqv_sym)
    transitivity proved by (lang_eqv_trans)
      as lang_equiv.

(* epsilon, constant symbols and concatenation *)
Section Little.

(* only a single word *)
Definition fixed_string : word -> language := Singleton word.
(* empty word *)
Definition epsilon : language := fixed_string (Done A).

Theorem fixed_string_empty_eqv_epsilon : fixed_string (Done A) ≣ epsilon.
Proof. unfold epsilon. reflexivity. Qed.

Theorem fixed_string_self (w : word) : w l∈ fixed_string w.
Proof. unfold fixed_string. constructor. Qed.

Inductive concat : language -> language -> language :=
| ConcatMatch (a : language) (b : language) (t : word) (u : word) (match_at : t l∈ a) (match_bu : u l∈ b)
  : concat a b (seq A t u).

Add Parametric Morphism : concat with
  signature (lang_eqv ==> lang_eqv ==> lang_eqv) as concat_morphism.
Proof. (* Somewhat brute-force, but quite effective *)
  unfold lang_eqv.
  firstorder.
  all : (inversion H1; subst k; constructor).
  all : firstorder.
Qed.

Theorem fixed_string_match_equal (v : word) (u : word) : u l∈ fixed_string v -> u = v.
Proof. simpl. intro K; inversion K; reflexivity. Qed.

(* bring constants together *)
Theorem concat_single (v : word) (w : word) : concat (fixed_string v) (fixed_string w) ≣ (fixed_string (seq A v w)).
Proof.
  split. all : intro H.
  + inversion H; clear H H2 H1 H0.
    inversion match_at; clear match_at H.
    rewrite (fixed_string_match_equal w u match_bu).
    reflexivity.
  + inversion H; clear H H0.
    constructor.
    all : reflexivity.
Qed.

(* concat, epsilon is a monoid *)

(* epsilon is neutral *)
Theorem concat_epsilon_l (a : language) : concat epsilon a ≣ a.
Proof.
  split. all : intro K.
  + inversion K.
    inversion match_at.
    rewrite seq_nil_l.
    assumption.
  + rewrite <- seq_nil_l.
    constructor.
    - constructor.
    - assumption.
Qed.

Theorem concat_epsilon_r (a : language) : concat a epsilon ≣ a.
Proof.
  split. all : intro K.
  + inversion K.
    inversion match_bu.
    rewrite seq_nil_r.
    assumption.
  + rewrite <- seq_nil_r.
    constructor.
    - assumption.
    - constructor.
Qed.

(* concat is associative *)
Lemma concat_assoc a b c : concat (concat a b) c ≣ concat a (concat b c).
Proof.
  split. all : intro H.
  + inversion H; clear H H2 H1 H0.
    inversion match_at; clear match_at H1 H0 H.
    rewrite seq_assoc.
    constructor.
    assumption.
    constructor.
    all : assumption.
  + inversion H; clear H H2 H1 H0.
    inversion match_bu; clear match_bu H1 u H0 H.
    rewrite <- seq_assoc.
    constructor.
    constructor.
    all : assumption.
Qed.
End Little.

Section Choice.

(* recognise everything *)
Definition anything : language := fun _ => True.
(* recognise nothing *)
Definition nothing : language := fun _ => False.

(* a choice between two languages *)
Definition or these those : language := fun (w : word) => these w \/ those w.
(* both languages at the same time *)
Definition and these those : language := fun (w : word) => these w /\ those w.

Add Parametric Morphism : or with
  signature (lang_eqv ==> lang_eqv ==> lang_eqv) as or_morphism.
Proof. firstorder. Qed.
Add Parametric Morphism : and with
  signature (lang_eqv ==> lang_eqv ==> lang_eqv) as and_morphism.
Proof. firstorder. Qed.

(* or, and have a minimum and a maximum *)
Lemma or_and_lattice_bottom_top : bounded_lattice_theory language lang_eqv or and nothing anything.
Proof. firstorder. Qed.

(* or, and are joins and meets *)
Lemma or_and_lattice : lattice_theory language lang_eqv or and.
Proof. exact (lattice _ _ _ _ _ _ or_and_lattice_bottom_top). Qed.

(* or, and distribute over each other *)
Lemma or_and_distr : distributive_theory language lang_eqv or and.
Proof. firstorder. Qed.

End Choice.

Section Repetition.

(* repeatedly concat a language, a finite number of times *)
Inductive repeatN : nat -> language -> language :=
| Repeat0 r : (Done _) l∈ repeatN 0 r
| RepeatS r n u v : u l∈ r -> v l∈ repeatN n r -> seq _ u v l∈ repeatN (S n) r.

Theorem repeat0 r : repeatN 0 r ≣ epsilon.
Proof.
  split.
  all : (intro P; inversion P; constructor).
Qed.

Theorem combine_repeatNM r : forall n m t u, repeatN n r t -> repeatN m r u -> repeatN (n + m) r (seq _ t u).
Proof.
  intro n.
  induction n.
  all : intros.
  + rewrite Nat.add_0_l.
    inversion H.
    rewrite seq_nil_l.
    assumption.
  + inversion H; clear H.
    clear H4 r0.
    rewrite Nat.add_succ_l.
    rewrite seq_assoc.
    constructor.
    - assumption.
    - apply IHn.
      all : assumption.
Qed.

(* An unbounded but finite number of repetitions.
   (TODO: how is the Kleene closure defined?
   From a quick look at his paper and some reminiscences
   of articles, he might even have conceived regular languages
   for checking infinite traces of events to match a safe
   pattern) *)
Definition finiteStar r : language := fun w => exists k, w l∈ repeatN k r.

Theorem finiteStar_epsilon_ok r w : w l∈ epsilon -> w l∈ finiteStar r.
Proof.
  intro P; destruct P.
  cbv.
  refine (ex_intro _ 0 _).
  constructor.
Qed.

Theorem finiteStar_epsilon : finiteStar epsilon ≣ epsilon.
Proof.
  split. all : intro P.
  2 : apply (finiteStar_epsilon_ok _ _ P).
  destruct P.
  induction x.
  - inversion H. constructor.
  - inversion H.
    destruct H1.
    rewrite seq_nil_l in H4.
    subst v.
    rewrite seq_nil_l.
    apply IHx.
    assumption.
Qed.

Theorem finiteStar_seq r : concat (finiteStar r) (finiteStar r) ≣ finiteStar r.
Proof.
  split. all : intro P.
  + unfold finiteStar.
    unfold finiteStar in P.
    inversion P; clear P.
    destruct match_at, match_bu.
    refine (ex_intro _ (x + x0) _).
    apply combine_repeatNM.
    all : assumption.
  + inversion P.
    rewrite <- seq_nil_r.
    constructor.
    - exact (ex_intro _ x H).
    - eapply finiteStar_epsilon_ok.
      constructor.
Qed.

(* And, in principle, r** = r*, although I don't believe
   the former occurs in practice *)

(* TODO: infinite repeating, without vacuousity
   (RFCs don't specify those, for it is rather
   incomputable), closure operator (which one, exactly?)
   (* not really a priority *) *)

End Repetition.
End Language.