Parameter Sigma : Set. (* L'alphabet utilisé *)

Inductive automate_deterministe (Q:Set): Type := 
  | autod : (Q -> Sigma -> Q) -> Q -> (Q -> Prop) -> automate_deterministe Q.

Inductive automate_nondeterministe (Q:Set): Type := 
  | autond : (Q -> Sigma -> (Q -> Prop)) -> Q -> (Q -> Prop) -> automate_nondeterministe Q.

Inductive expression_rationelle : Type :=
  | epsilon : expression_rationelle
  | vide : expression_rationelle
  | lettre : Sigma -> expression_rationelle
  | union : expression_rationelle -> expression_rationelle -> expression_rationelle
  | concat : expression_rationelle -> expression_rationelle -> expression_rationelle
  | etoile : expression_rationelle -> expression_rationelle.


Inductive automate_rationnel (Q: Set): Set :=
  | autorat : (Q -> Q -> expression_rationelle) -> Q -> Q -> automate_rationnel Q.

Check automate_rationnel.

Definition autorat_gen (Q : Set) (aa : automate_rationnel Q) : Prop := match aa with
  | autorat _ delta qi qf => forall a : Q, ((delta a qi) = vide)/\((delta qf a) = vide)
end.

Record automate_generalise (Q: Set): Set := mkAG
{
  autogen: automate_rationnel Q;
  autogen_cond: (autorat_gen Q) autogen
}.

Definition mot := list Sigma.
Definition langage := mot -> Prop.

Fixpoint executeMot (Q :Set) (ad: automate_deterministe Q) (m: mot) : Q := 
    match m with
    | nil =>
      match ad with
        | autod _ _ q0 _ => q0
      end
    | cons l s => 
      match ad with
        | autod _ delta q0 _ => delta (executeMot Q ad s) l
      end
    end.

Definition reconnait_ad (Q :Set) (ad: automate_deterministe Q) (m: mot) :Prop := match ad with
  | autod _ _ _ ff => ff (executeMot Q ad m)
end.

Definition reconnait_ad_lang (Q: Set) (ad: automate_deterministe Q) (l :langage) :=
  forall m:mot, l m -> reconnait_ad Q ad m.

Fixpoint pow_list (E: Type) (l: list E) (k: nat) : list E :=
  match k with
  | 0 => nil
  | S kk => l ++ (pow_list E l kk)
end.

Definition concatenate (E: Type) (ll lr: list E) : list E := ll ++ lr. 

Fixpoint exprat_lang (ex :expression_rationelle): langage := fun m =>
match ex with
  | epsilon => m=nil
  | vide => False
  | lettre l => m=(cons l nil)
  | union ex1 ex2 => (exprat_lang ex1 m) \/ (exprat_lang ex2 m)
  | concat exl exr => exists (ml mr:mot), ((concatenate Sigma ml mr) = m) /\ (exprat_lang exl m) /\ (exprat_lang exr m)
  | etoile exx => exists (k:nat) (mm: mot), (pow_list Sigma mm k)=m /\ (exprat_lang exx mm)
end.

Definition langage_rationnel (ll :langage) :=
  exists (Q: Set) (ad: automate_deterministe Q), reconnait_ad_lang Q ad ll.