RIS.closed_languages: languages closed by α-equivalence.

Set Implicit Arguments.

Require Import tools algebra language regexp alpha_regexp.

Section s.
  Context {atom : Set}{𝐀 : Atom atom}.
  Context {X : Set} {𝐗 : Alphabet 𝐀 X}.
  Definition α_closed : (@language letter) → Prop := fun L ⇒ ∀ u v, u ≡ v → L u ↔ L v.

  Definition cl_α : language → language := fun L w ⇒ ∃ u, L u ∧ u ≡ w.

  Lemma cl_α_closed L : α_closed (cl_α L).

  Lemma cl_α_idem l : cl_α (cl_α l) ≃ cl_α l.

  Lemma cl_α_incr l : l ≲ cl_α l.

  Lemma cl_α_closed_idem L : α_closed L → cl_α L ≃ L.

  Global Instance inf_lang_cl_α : Proper (ssmaller ==> ssmaller) cl_α.

  Lemma minimal_cl_α L M : L ≲ M → α_closed M → cl_α L ≲ M.

  Lemma cl_α_inf L M : cl_α L ≲ cl_α M ↔ L ≲ cl_α M.

  Lemma cl_α_join L M : cl_α (L∪M) ≃ cl_α L ∪ cl_α M.

  Lemma cl_α_nil L : L [] ↔ cl_α L [].

  Global Instance cl_α_eq_lang : Proper (sequiv ==> sequiv) cl_α.

  Global Instance cl_α_inf_lang : Proper (ssmaller ==> ssmaller) cl_α.

  Global Instance cl_α_αeq l : Proper (equiv ==> iff) (cl_α l).

  Lemma cl_α_prod l m: cl_α (l · m) ≃ cl_α (cl_α l · cl_α m).

  Lemma cl_α_star l: cl_α (l⋆) ≃ cl_α ((cl_α l)⋆).

  Definition restrict L A : (@language letter) := fun u ⇒ L u ∧ ⌊u⌋ ⊆ A.

  Infix " ⇂ " := restrict (at level 20).

  Global Instance restrict_eqLists : Proper (sequiv ==> (@equivalent _) ==> sequiv) restrict.
  Global Instance restrict_inclLists : Proper (ssmaller ==> (@incl _) ==> ssmaller) restrict.

  Proposition restrict_inf e f :
    cl_α ⟦e⟧ ≲ cl_α ⟦f⟧ ↔ ⟦e⟧ ≲ (cl_α ⟦f⟧) ⇂ (⌊e⌋++⌊f⌋) .

  Proposition restrict_inf_bis e f :
    cl_α ⟦e⟧ ≲ cl_α ⟦f⟧ ↔ (cl_α ⟦e⟧)⇂(⌊e⌋++⌊f⌋) ≲ (cl_α ⟦f⟧) ⇂ (⌊e⌋++⌊f⌋).

  Corollary restrict_eq e f :
    cl_α ⟦e⟧ ≃ cl_α ⟦f⟧ ↔ (cl_α ⟦e⟧)⇂(⌊e⌋++⌊f⌋) ≃ (cl_α ⟦f⟧) ⇂ (⌊e⌋++⌊f⌋).

End s.