From 5cf6023f3aff8afa634c9289b4409b448ca2da8e Mon Sep 17 00:00:00 2001
From: Mysaa <mysaa@bernard.com.de>
Date: Tue, 21 Sep 2021 20:47:42 +0200
Subject: [PATCH] Premier commit ! Un peu de code sur les automates.

---
 README.md   | 18 ++++++++++
 automates.v | 97 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 115 insertions(+)
 create mode 100644 README.md
 create mode 100644 automates.v

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..69cdc2d
--- /dev/null
+++ b/README.md
@@ -0,0 +1,18 @@
+Coq en stock
+=
+
+Just des bouts de coq. Rien de plus.
+
+
+
+
+
+
+
+
+
+
+
+
+
+Vraiment.
diff --git a/automates.v b/automates.v
new file mode 100644
index 0000000..d38a577
--- /dev/null
+++ b/automates.v
@@ -0,0 +1,97 @@
+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.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+