Library fl.int.Base2

Require Import List.

(* Add LoadPath "~/Git/YC_in_Coq/". *)
Require Import fl.cfg.Definitions.

Module Base.

  Import Definitions.

  Section Definitions.

    Context {Tt Vt: Type}.

    Definition word := list (@ter Tt).

    Definition language := word → Prop.

    Definition language_union (l1 l2 : language) := fun w ⇒ (l1 w) ∨ (l2 w).

    Definition language_intersection (l1 l2 : language) := fun w ⇒ (l1 w) ∧ (l2 w).

    Definition language_eq (l1 l2 : language) := ∀ w : word, l1 w ↔ l2 w.

    Notation "l1 [\/] l2" := (language_union l1 l2) (at level 85).
    Notation "l1 [/\] l2" := (language_intersection l1 l2) (at level 80).
    Notation "l1 [==] l2" := (language_eq l1 l2) (at level 90).

  End Definitions.

  Section Kek.

    Fixpoint to_phrase {T V: Type} (w: word): @phrase T V :=
      match w with
        | s::sx ⇒ Ts s :: to_phrase sx
        | _ ⇒ [::]
      end.

  End Kek.


  Section Lemmas.

     Context {Tt Vt: Type}.
    (* TODO: del *)
    Notation "l1 [\/] l2" := (language_union l1 l2) (at level 85).
    Notation "l1 [/\] l2" := (language_intersection l1 l2) (at level 80).
    Notation "l1 [==] l2" := (language_eq l1 l2) (at level 90).

    Lemma mk_laguage_eq :
      ∀ (l1 l2 : @language Tt),
        (∀ w, l1 w → l2 w) →
        (∀ w, l2 w → l1 w) → l1 [==] l2.

    Theorem lang_distr : ∀ l1 l2 l3 : (@language Tt),
                           l1 [/\] (l2 [\/] l3) [==] (l1 [/\] l2) [\/] (l1 [/\] l3).

    Fixpoint language_list_union (l : list (@language Tt)) := fun w ⇒
                                                          match l with
                                                            | nil ⇒ False
                                                            | h :: t ⇒ (h w) ∨ language_list_union t w
                                                          end.

    Theorem lang_distr_2 : ∀ (l2 : language) (ls : list language),
                             (l2 [/\] (language_list_union ls)) [==]
                                                               (language_list_union (map (fun l ⇒ l2 [/\] l) ls)).

  End Lemmas.

End Base.