Require Import Ensf.

Parameter alph : Ensf.
Parameter epsilon : Elt.
  Axiom not_dans_epsilon_alph : ~ dans epsilon alph.


Inductive inmonoid (X : Ensf) : Word -> Prop :=
  | inmonoid_nil : inmonoid X nil
  | inmonoid_cons :
      forall (w : Word) (e : Elt),
      inmonoid X w -> dans e X -> inmonoid X (cons e w).
Hint Resolve inmonoid_nil: v62.
Hint Resolve inmonoid_cons: v62.

Fixpoint Inmonoid (X : Ensf) (w : Word) {struct w} : Prop :=
  match w with
  | nil => True
  | cons a w' => dans a X /\ Inmonoid X w'
  end.

Lemma i_I : forall (X : Ensf) (w : Word), inmonoid X w -> Inmonoid X w.
intros X w H.
elim H.
red in |- *; simpl in |- *; exact I.
intros.
change (dans e X /\ Inmonoid X w0) in |- *.
auto with v62.
Qed.
Hint Resolve i_I: v62.

Lemma I_i : forall (X : Ensf) (w : Word), Inmonoid X w -> inmonoid X w.
intros X.
simple induction w.
auto with v62.
intros x w0 H H0.
cut (dans x X /\ Inmonoid X w0); auto with v62.
intro H1; elim H1; clear H1.
auto with v62.
Qed.
Hint Resolve I_i: v62.

Lemma inmonoid_cons_inv :
 forall (X : Ensf) (w : Word) (a : Elt),
 inmonoid X (cons a w) -> inmonoid X w.
intros.
cut (Inmonoid X w); auto with v62.
cut (Inmonoid X (cons a w)); auto with v62.
intro H0.
cut (dans a X /\ Inmonoid X w); auto with v62.
intro H1; elim H1; clear H1.
auto with v62.
Qed.

Lemma inmonoid_cons_inv2 :
 forall (X : Ensf) (a : Elt) (w : Word), inmonoid X (cons a w) -> dans a X.
intros.
cut (Inmonoid X (cons a w)); auto with v62.
intro.
cut (dans a X /\ Inmonoid X w); auto with v62.
intro H1; elim H1; clear H1.
auto with v62.
Qed.

Lemma inmonoid_inclus :
 forall (E F : Ensf) (x : Word), inclus E F -> inmonoid E x -> inmonoid F x.
intros E F x inclus_E_F inmonoid_E_x.
elim inmonoid_E_x.
        trivial with v62.

        intros w e inmonoid_E_w inmonoid_F_w dans_e_E.
        apply inmonoid_cons; [ assumption | apply inclus_E_F; assumption ].
Qed.


Fixpoint Append (w1 : Word) : Word -> Word :=
  fun w2 : Word =>
  match w1 with
  | nil => w2
  | cons a w3 => cons a (Append w3 w2)
  end.

Lemma Append_w_nil : forall w : Word, Append w nil = w :>Word.
simple induction w.
auto with v62.
intros x w0 H.
replace (Append (cons x w0) nil) with (cons x (Append w0 nil)); auto with v62.
rewrite H; auto with v62.
Qed.

Inductive append : Word -> Word -> Word -> Prop :=
  | append_nil : forall w : Word, append nil w w
  | append_cons :
      forall (w1 w2 w3 : Word) (a : Elt),
      append w1 w2 w3 -> append (cons a w1) w2 (cons a w3).


Lemma Append_inmonoid_g :
 forall (X : Ensf) (w1 w2 : Word), inmonoid X (Append w1 w2) -> inmonoid X w1.
intros X.
simple induction w1.
auto with v62.
intros x w H w2.
replace (Append (cons x w) w2) with (cons x (Append w w2)); auto with v62.
intro.
apply inmonoid_cons.
apply (H w2).
apply inmonoid_cons_inv with x; auto with v62.
apply inmonoid_cons_inv2 with (Append w w2); auto with v62.
Qed.

Lemma Append_inmonoid_d :
 forall (X : Ensf) (w1 w2 : Word), inmonoid X (Append w1 w2) -> inmonoid X w2.
intros X.
simple induction w1.
auto with v62.
intros x w H w2.
replace (Append (cons x w) w2) with (cons x (Append w w2)); auto with v62.
intro.
apply (H w2).
apply inmonoid_cons_inv with x; auto with v62.
Qed.

Lemma inmonoid_Append :
 forall (X : Ensf) (w1 w2 : Word),
 inmonoid X w1 -> inmonoid X w2 -> inmonoid X (Append w1 w2).
intros X.
simple induction w1.
auto with v62.
intros x w H w2 H0 H1.
replace (Append (cons x w) w2) with (cons x (Append w w2)); auto with v62.
apply inmonoid_cons.
apply (H w2); auto with v62.
apply inmonoid_cons_inv with x; auto with v62.
apply inmonoid_cons_inv2 with w; auto with v62.
Qed.


Definition wordset := Word -> Prop.

Definition eqwordset (l1 l2 : wordset) : Prop :=
  forall w : Word, (l1 w -> l2 w) /\ (l2 w -> l1 w).

Lemma eqwordset_refl : forall L : wordset, eqwordset L L.
red in |- *.
auto with v62.
Qed.

Lemma eqwordset_sym :
 forall l1 l2 : wordset, eqwordset l1 l2 -> eqwordset l2 l1.
unfold eqwordset in |- *.
intros.
elim (H w); clear H; intros; auto with v62.
Qed.

Lemma eqwordset_trans :
 forall l1 l2 l3 : wordset,
 eqwordset l1 l2 -> eqwordset l2 l3 -> eqwordset l1 l3.
unfold eqwordset in |- *.
intros.
elim (H0 w); clear H0; intros.
elim (H w); clear H; intros.
auto with v62.
Qed.


Definition islanguage (X : Ensf) (L : wordset) : Prop :=
  forall w : Word, L w -> inmonoid X w.


Fixpoint Word_ext (f : Elt -> Elt) (w : Word) {struct w} : Word :=
  match w with
  | nil => nil
  | cons a w' => cons (f a) (Word_ext f w')
  end.

Lemma inmonoid_map :
 forall (f : Elt -> Elt) (a : Ensf) (w : Word),
 inmonoid a w -> inmonoid (map f a) (Word_ext f w).
intros.
elim H; [ unfold Word_ext in |- *; auto with v62 | idtac ].
intros; unfold Word_ext in |- *; simpl in |- *.
apply inmonoid_cons; try apply dans_map_inv; auto with v62.
Qed.
Hint Resolve inmonoid_map: v62.


Lemma cons_cons :
 forall (x1 x2 : Elt) (w1 w2 : Word),
 x1 = x2 :>Elt -> w1 = w2 :>Word -> cons x1 w1 = cons x2 w2 :>Word.
intros.
rewrite H0.
rewrite H.
auto with v62.
Qed.
Hint Resolve cons_cons: v62.

Definition fun_consaw_a (w : Word) : Elt :=
  match w return Elt with
  | nil =>
       zero
      
  | cons a w' => a
  end.

Definition fun_consaw_w (w : Word) : Word :=
  match w return Word with
  | nil =>
       nil
      
  | cons a w' => w'
  end.

Lemma cons_cons_inv :
 forall (x1 x2 : Elt) (w1 w2 : Word),
 cons x1 w1 = cons x2 w2 -> x1 = x2 /\ w1 = w2.
intros.
split.
replace x1 with (fun_consaw_a (cons x1 w1)); auto with v62.
replace x2 with (fun_consaw_a (cons x2 w2)); auto with v62.
apply (f_equal (A:=Word) (B:=Elt)); auto with v62.
replace w1 with (fun_consaw_w (cons x1 w1)); auto with v62.
replace w2 with (fun_consaw_w (cons x2 w2)); auto with v62.
apply (f_equal (A:=Word) (B:=Word)); auto with v62.
Qed.

Hint Resolve cons_cons_inv: v62.

Lemma cons_cons_inv1 :
 forall (x1 x2 : Elt) (w1 w2 : Word),
 cons x1 w1 = cons x2 w2 :>Word -> x1 = x2 :>Elt.
intros.
cut (x1 = x2 :>Elt /\ w1 = w2 :>Word); [ intuition | auto with v62 ].
Qed.

Lemma cons_cons_inv2 :
 forall (x1 x2 : Elt) (w1 w2 : Word), cons x1 w1 = cons x2 w2 -> w1 = w2.
intros.
cut (x1 = x2 /\ w1 = w2); [ intuition | auto with v62 ].
Qed.


Lemma nil_or_cons :
 forall w : Word,
 w = nil \/ (exists x : Elt, (exists w0 : Word, w = cons x w0)).
simple induction w.

left; auto with v62.

intros x w0 H.
right.
exists x.
exists w0.
auto with v62.
Qed.