# Library LangAlg.language

Basics of languages.

Set Implicit Arguments.

Require Export tools.
Delimit Scope lang_scope with lang.

A language over the alphabet Σ is a predicate over lists of Σ.
Definition language := fun (Σ : Set) ⇒ list Σ Prop.

Notation " x ⋵ L " := ((L : language _) x) (at level 60).

Section defs.
Hypothesis Σ : Set.

We define the equality and containment of language as follows:
Global Instance lang_eq : SemEquiv (language Σ) :=
fun l m w, w l w m.

Global Instance lang_incl : SemSmaller (language Σ) :=
fun l m w, w l w m.

Equality is an equivalence relation, and containment is a partial order.
Global Instance lang_eq_Equivalence : Equivalence sequiv.

Global Instance lang_incl_PreOrder : PreOrder ssmaller.

Global Instance lang_incl_PartialOrder :
PartialOrder sequiv ssmaller.

We now define the elementary operations on languages.
Definition prod (l m : language Σ) : language Σ:=
fun w u v, u l v m w = u++v.

Definition union (l m : language Σ) : language Σ:=
fun ww l w m.

Definition intersection (l m : language Σ) : language Σ:=
fun ww l w m.

Definition mirror (l : language Σ) : language Σ:=
fun w(rev w) l.

Definition unit : language Σ := fun ww = [].

Definition empty : language Σ := fun _False.

These operations are monotone.
Global Instance prod_lang_incl :
Proper (ssmaller ==> ssmaller ==> ssmaller) prod.

Global Instance union_lang_incl :
Proper (ssmaller ==> ssmaller ==> ssmaller) union.

Global Instance intersection_lang_incl :
Proper (ssmaller ==> ssmaller ==> ssmaller) intersection.

Global Instance mirror_lang_incl :
Proper (ssmaller ==> ssmaller) mirror.

Global Instance union_lang_eq :
Proper (sequiv ==> sequiv ==> sequiv) union.

Global Instance prod_lang_eq :
Proper (sequiv ==> sequiv ==> sequiv) prod.

Global Instance intersection_lang_eq :
Proper (sequiv ==> sequiv ==> sequiv) intersection.

Global Instance mirror_lang_eq :
Proper (sequiv ==> sequiv) mirror.

End defs.

The empty words belongs to a language exactly when it belongs to its mirror image.
Lemma mirror_nil {Σ : Set} (L : language Σ) : mirror L [] L [].

An assignment of type XΣ is a map from variables in X to languages over Σ.
Definition assignment (X Σ : Set) := X language Σ.

Notation " 𝕬[ X → Σ ] " := (assignment X Σ).
σ is test-compatible with A, written A σ, if for every variable a in A the empty list belongs to σ(a).
Definition test_compatible {Σ X} (σ : 𝕬[XΣ]) (A : list X) :=
a : X, a A [] σ a.

Notation " A ⊢ σ " := (test_compatible σ A) (at level 70).

Being test-compatible with a concatenation of two lists means being compatible with both lists.
Lemma test_compatible_app {Σ X} A B (σ : 𝕬[XΣ]): A++B σ A σ B σ.