Library ATBR.Model_Languages

Require Import Common.
Require Import Classes.
Require Import MxGraph.
Require Converse.
Require Import List.

Section Def.

  Context {A: Type}.

  Definition lang := list A -> Prop.
  Definition lang_equal (L L': lang): Prop := forall x, L x <-> L' x.
  Definition lang_union (L L': lang): lang := fun x => L x \/ L' x.
  Definition lang_Union I (L: I -> lang): lang := fun x => exists i, L i x.
  Definition lang_inter (L L': lang): lang := fun x => L x /\ L' x.
  Definition lang_comp (L L': lang): lang := fun x => exists2 u, L u & exists2 v, L' v & x=u++v.
  Definition lang_conv (L: lang): lang := fun x => L (rev x).
  Definition lang_id: lang := fun x => x=nil.
  Definition lang_empty: lang := fun x => False.
  Definition lang_top: lang := fun x => True.
  Fixpoint lang_iter (L: lang) n: lang :=
    match n with
      | 0 => lang_id
      | S n => lang_comp (lang_iter L n) L
    end.
  Definition lang_star (L: lang): lang := fun x => exists n, lang_iter L n x.

  Program Instance lang_Graph: Graph := {
    T := unit;
    X A B := lang;
    equal A B := lang_equal
  }.

  Instance lang_SemiLattice_Ops: SemiLattice_Ops lang_Graph := {
    plus A B := lang_union;
    zero A B := lang_empty
  }.

  Instance lang_Monoid_Ops: Monoid_Ops lang_Graph := {
    dot A B C := lang_comp;
    one A := lang_id
  }.

  Instance lang_Star_Op: Star_Op lang_Graph := {
    star A := lang_star
  }.

  Instance lang_Converse_Op: Converse_Op lang_Graph := {
    conv A B := lang_conv
  }.

  Transparent equal.

  Instance lang_SemiLattice: SemiLattice lang_Graph.

  Instance lang_ConverseSemiRing: ConverseIdemSemiRing lang_Graph.

  Definition lang_IdemSemiRing: IdemSemiRing lang_Graph := Converse.CISR_ISR.

  Notation LX := (@X lang_Graph tt tt).

  Lemma lang_leq n m: forall (a b: @X (lang_Graph) n m), a<==b <-> forall x, a x -> b x.

  Lemma lang_Union_spec I (L: I -> LX): forall L': LX, (lang_Union L: LX) <== L' <-> forall i, L i <== L'.

  Lemma leq_lang_Union I (L: I -> LX): forall i, L i <== lang_Union L.

  Instance lang_ConverseKleeneAlgebra: ConverseKleeneAlgebra lang_Graph.

  Definition lang_KleeneAlgebra: KleeneAlgebra lang_Graph := Converse.CKA_KA.

End Def.

Module Load.


  Canonical Structure lang_Graph.

  Transparent equal plus dot one zero star.

  Notation LX A := (@X (@lang_Graph A) tt tt).
  Notation LMX A n m := (@X (@mx_Graph (@lang_Graph A) tt) (n%nat) (m%nat)).

  Ltac fold_langAlg A :=
    change (@lang_equal A) with (@equal (@lang_Graph A) tt tt);
      change (@lang_id A) with (@one (@lang_Graph A) (@lang_Monoid_Ops A) tt);
        change (@lang_comp A) with (@dot (@lang_Graph A) (@lang_Monoid_Ops A) tt tt tt);
          change (@lang_union A) with (@plus (@lang_Graph A) (@lang_SemiLattice_Ops A) tt tt);
            change (@lang_empty A) with (@zero (@lang_Graph A) (@lang_SemiLattice_Ops A) tt tt);
              change (@lang_star A) with (@star (@lang_Graph A) (@lang_Star_Op A) tt).

End Load.