Require Import Ensf.
Require Import Words.
Require Import more_words.
Require Import need.
Require Import fonctions.
Require Import Relations.

Definition Mots (X : Ensf) :=
  forall a : Elt, dans a X -> exists w : Word, word w = a.

Definition Regles (X V R : Ensf) :=
  forall x : Elt,
  dans x R ->
  ex2 (fun A : Elt => dans A V)
    (fun A : Elt =>
     ex2 (fun B : Word => x = couple A (word B))
       (fun B : Word => inmonoid (union X V) B)).

Lemma Regles_inv1 :
 forall (X V R : Ensf) (x y : Elt),
 Regles X V R -> dans (couple x y) R -> dans x V.
intros X V R x y Regles_R dans_couple_R.
cut
 (ex2 (fun A : Elt => dans A V)
    (fun A : Elt =>
     ex2 (fun B : Word => couple x y = couple A (word B))
       (fun B : Word => inmonoid (union X V) B))).
intro temp; elim temp; clear temp.
intros x0 dans_x0_V temp; elim temp; clear temp.
intros u eg_couple inmonoid_u.
replace x with x0; prolog [ sym_equal couple_couple_inv1 ] 3.

auto with v62.
Qed.

Lemma Regles_inv2 :
 forall (X V R : Ensf) (x : Elt) (u : Word),
 Regles X V R -> dans (couple x (word u)) R -> inmonoid (union X V) u.
intros X V R x u Regles_R dans_couple_R.
cut
      (ex2 (fun A : Elt => dans A V)
         (fun A : Elt =>
          ex2 (fun B : Word => couple x (word u) = couple A (word B))
            (fun B : Word => inmonoid (union X V) B))).
intro temp; elim temp; clear temp.
intros x0 dans_x0_V temp; elim temp; clear temp.
intros u0 eg_couple inmonoid_u0.
replace u with u0; prolog [ sym_equal couple_couple_inv2 word_word_inv ] 4.
auto with v62.
Qed.


Definition isGram (X V R : Ensf) (S : Elt) : Prop :=
  Mots X /\ inter X V empty /\ dans S V /\ Regles X V R.

Section Easy_lemma_isGram.

Variable X V R : Ensf.
Variable S : Elt.
Let H := isGram X V R S.

Lemma isGram1 : H -> Mots X.
intro H1.
elim H1.
trivial with v62.
Qed.

Lemma isGram2 : H -> inter X V empty.
intro H1.
elim H1.
intuition.
Qed.

Lemma isGram3 : H -> dans S V.
intro H1.
elim H1.
intuition.
Qed.

Lemma isGram4 : H -> Regles X V R.
intro H1.
elim H1.
intuition.
Qed.

Lemma isGram5 : Mots X -> inter X V empty -> dans S V -> Regles X V R -> H.
intros.
red in |- *; red in |- *.
auto with v62.
Qed.

End Easy_lemma_isGram.

Lemma Regles_R :
 forall X V R R' : Ensf, inclus R' R -> Regles X V R -> Regles X V R'.
unfold Regles in |- *.
auto with v62.
Qed.

Lemma Regles_V :
 forall X V R V' : Ensf, inclus V V' -> Regles X V R -> Regles X V' R.
unfold Regles in |- *.
intros X V R V' inclus_V_V' Regles_X_V_R x dans_x_R.
elim (Regles_X_V_R x dans_x_R).
intros A dans_A_V temp; elim temp; clear temp.
intros B egal_B inmonoid_B.
exists A.
auto with v62.
exists B.
assumption.
apply inmonoid_inclus with (union X V); auto with v62.
Qed.

Lemma Regles_add :
 forall (X V R : Ensf) (a : Elt) (u : Word),
 Regles X V R ->
 dans a V -> inmonoid (union X V) u -> Regles X V (add (couple a (word u)) R).
intros X V R a u R_R dans_a_V inmonoid_u_X_V_u.
red in |- *.
intros x dans_x_R'.
cut (couple a (word u) = x :>Elt \/ dans x R). intuition.
        exists a.
                assumption.
                exists u; auto with v62.
apply dans_add; assumption.
Qed.

Lemma Regles_add2 :
 forall (X V R : Ensf) (a : Elt), Regles X V R -> Regles X (add a V) R.
intros.
apply Regles_V with V; auto with v62.
Qed.

Lemma Regles_union :
 forall X V R R' : Ensf,
 Regles X V R -> Regles X V R' -> Regles X V (union R R').

unfold Regles in |- *.
intros X V R R' R_R R_R' x dans_x_union.
cut (dans x R \/ dans x R'); auto with v62.
intros [HR| HR']; auto.
Qed.

Lemma isGram_inclus2 :
 forall (X V R R' : Ensf) (S : Elt),
 inclus R' R -> isGram X V R S -> isGram X V R' S.
prolog [ isGram4 Regles_R isGram3 isGram2 isGram1 isGram5 ] 11.

Qed.

Lemma isGram_inclus3 :
 forall (X V R : Ensf) (S a : Elt), isGram X V (add a R) S -> isGram X V R S.
intros X V R S a isGram_X_V_a_R_S.
apply isGram_inclus2 with (add a R); auto with v62.
Qed.


Inductive Derive (R : Ensf) : Word -> Word -> Prop :=
 
 
  | Derive1 :
      forall (u v : Word) (A : Elt),
      dans (couple A (word u)) R ->
      Derive R (cons A v) (Append u v)
      
      
  | Derive2 :
      forall (u v : Word) (x : Elt),
      Derive R u v -> Derive R (cons x u) (cons x v).

Hint Resolve Derive1: v62.
Hint Resolve Derive2: v62.

Lemma Derive_inclus :
 forall (R1 R2 : Ensf) (u v : Word),
 inclus R1 R2 -> Derive R1 u v -> Derive R2 u v.
intros R1 R2 u v inclus_R1_R2 Der_R1.
elim Der_R1; auto with v62.
Qed.

Definition Derive_inv (R : Ensf) (x y : Word) :=
  match x return Prop with
  | nil =>
       False
      
  | cons A w =>
      ex2 (fun u : Word => dans (couple A (word u)) R)
        (fun u : Word =>
         ex2 (fun v : Word => cons A v = x :>Word)
           (fun v : Word => Append u v = y :>Word)) \/
      ex2 (fun v : Word => Derive R w v)
        (fun v : Word => cons A v = y :>Word)
  end.

Lemma Derive_inv1 :
 forall (R : Ensf) (u v : Word), Derive R u v -> Derive_inv R u v.
intros R x y Der_x_y.
unfold Derive_inv in |- *.
elim Der_x_y; prolog [ ex_intro2 refl_equal or_intror or_introl ] 8.
Qed.

Hint Resolve Derive_inv1: v62.

Lemma Derive_inv2 :
 forall (R : Ensf) (x y : Word),
 Derive_inv R x y ->
 exists A : Elt,
   (exists2 w : Word,
      cons A w = x &
      (exists2 u : Word,
         dans (couple A (word u)) R &
         (exists2 v : Word, cons A v = x & Append u v = y)) \/
      (exists2 v : Word, Derive R w v & cons A v = y)).
intros R x y.
elim x.
unfold Derive_inv in |- *.

intuition.

intros x0 w Hyp_rec.
unfold Derive_inv in |- *.
exists x0.
exists w; trivial with v62.
Qed.

Lemma Derive_inv3 :
 forall (R : Ensf) (x y : Word),
 Derive R x y ->
 exists A : _,
   (exists2 w : _,
      cons A w = x &
      (exists2 u : _,
         dans (couple A (word u)) R &
         (exists2 v : _, cons A v = x & Append u v = y)) \/
      (exists2 v : _, Derive R w v & cons A v = y)).

prolog [ Derive_inv1 Derive Derive_inv2 ] 7.
Qed.

Lemma in_mon_X_Der_imp_inmon_X :
 forall (X V R : Ensf) (u v : Word),
 Regles X V R ->
 Derive R u v -> inmonoid (union X V) u -> inmonoid (union X V) v.

intros X V1 R1 u v Regles_R1 Der_R1.
elim Der_R1;
 prolog
  [ Regles_inv2 inmonoid_cons_inv inmonoid_cons_inv2 inmonoid_cons
   inmonoid_Append ] 10.

Qed.


Definition Derivestar (R : Ensf) := Rstar Word (Derive R).

Hint Unfold Derivestar: v62.

Lemma Derivestar_refl : forall (R : Ensf) (u : Word), Derivestar R u u.
auto with v62.
Qed.

Hint Resolve Derivestar_refl: v62.

Lemma Derivestar_R :
 forall (R : Ensf) (u v w : Word),
 Derive R u v -> Derivestar R v w -> Derivestar R u w.
unfold Derivestar in |- *.
prolog [ Rstar_R ] 8.
Qed.

Lemma Derivestar_inv :
 forall (R : Ensf) (u v : Word),
 Derivestar R u v ->
 u = v \/ (exists2 w : Word, Derive R u w & Derivestar R w v).
unfold Derivestar in |- *.
prolog [ Rstar_inv ] 6.
Qed.

Hint Resolve Derivestar_inv: v62.

Lemma Derivestar_inclus :
 forall (R1 R2 : Ensf) (u v : Word),
 inclus R1 R2 -> Derivestar R1 u v -> Derivestar R2 u v.
intros R1 R2 u v inclus_R1_R2 Der_R1.
unfold Derivestar, Rstar in Der_R1.
pattern u, v in |- *.
apply Der_R1.
        auto with v62.
        intros; prolog [ Derive_inclus Derivestar_R ] 3.
Qed.


Definition LG (X V R : Ensf) (S : Elt) : wordset :=
  fun w : Word => Derivestar R (cons S nil) w /\ inmonoid X w.

Lemma LG_inv :
 forall (X V R : Ensf) (S : Elt) (w : Word), LG X V R S w -> inmonoid X w.
unfold LG in |- *.
intros.
elim H; auto with v62.
Qed.


Lemma LG_langage :
 forall (X V R : Ensf) (S : Elt), isGram X V R S -> islanguage X (LG X V R S).
intros; red in |- *; intros; elim H0; auto with v62.
Qed.


Definition Gunion (V1 R1 V2 R2 : Ensf) := (union V1 V2, union R1 R2).

Section injprod.

Let injproduc (f : Elt -> Elt) (V : Ensf) := extension V f.

Definition injproducg : Ensf -> Elt -> Elt := injproduc injgauche.

Definition injproducd : Ensf -> Elt -> Elt := injproduc injdroite.


End injprod.

Definition Gunion_disj_p (V1 R1 : Ensf) (S1 : Elt)
  (V2 R2 : Ensf) (S2 S : Elt) :=
  (add S (fst (Gunion V1 R1 V2 R2)),
  (add (couple S (word (cons S1 nil)))
     (add (couple S (word (cons S2 nil))) (snd (Gunion V1 R1 V2 R2))), S)).


Definition imageGram (f : Elt -> Elt) (X V R : Ensf)
  (S : Elt) :=
  (map f X,
  (map f V,
  (map
     (fun P : Elt =>
      couple (f (first P))
        ((fun w : Elt => word (Word_ext f (word_inv w))) (second P))) R,
  f S))).