98 lines
2.5 KiB
Coq
98 lines
2.5 KiB
Coq
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|