(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                               fonctions.v                                *)
(****************************************************************************)
(*              Formal Language Theory                                      *)
(*                                                                          *)
(*              Judicael Courant - Jean-Christophe Filliatre                *)
(*                                                                          *)
(*              Developped in V5.8  June-July 1993                          *)
(*              Ported     to V5.10 October 1994                            *)
(****************************************************************************)

Require Import Ensf.
Require Import Words.
Require Import more_words.
Require Import need.
Hint Resolve dans_map_inv.
Hint Resolve dans_map.
Hint Resolve dans_add1.

Definition comp (f g : Elt -> Elt) (x : Elt) := f (g x).

Lemma map_map_eg_map_comp :
 forall (f g : Elt -> Elt) (E : Ensf),
 map f (map g E) = map (comp f g) E :>Ensf.
(* Goal: forall f g : forall _ : Elt, Elt, eg_f_W_W (Word_ext (comp f g)) (comp_word (Word_ext f) (Word_ext g)) *)
intros f g.
(* Goal: forall E : Ensf, @eq Ensf (map f (map g E)) (map (comp f g) E) *)
simple induction E; simpl in |- *; auto.
Qed.


Definition comp_word (f g : Word -> Word) (x : Word) := f (g x).

Definition eg_f_W_W (f g : Word -> Word) := forall x : Word, f x = g x :>Word.


Lemma comp_Word_ext :
 forall f g : Elt -> Elt,
 eg_f_W_W (Word_ext (comp f g)) (comp_word (Word_ext f) (Word_ext g)).
(* Goal: forall f g : forall _ : Elt, Elt, eg_f_W_W (Word_ext (comp f g)) (comp_word (Word_ext f) (Word_ext g)) *)
intros f g.
(* Goal: eg_f_W_W (Word_ext (comp f g)) (comp_word (Word_ext f) (Word_ext g)) *)
unfold eg_f_W_W, Word_ext, comp, comp_word in |- *.
(* Goal: forall x : Word, @eq Word ((fix Word_ext (f : forall _ : Elt, Elt) (w : Word) {struct w} : Word := match w with | nil => nil | cons a w' => cons (f a) (Word_ext f w') end) (fun x0 : Elt => f (g x0)) x) ((fix Word_ext (f : forall _ : Elt, Elt) (w : Word) {struct w} : Word := match w with | nil => nil | cons a w' => cons (f a) (Word_ext f w') end) f ((fix Word_ext (f : forall _ : Elt, Elt) (w : Word) {struct w} : Word := match w with | nil => nil | cons a w' => cons (f a) (Word_ext f w') end) g x)) *)
simple induction x; simpl in |- *; auto.
Qed.
Hint Resolve comp_Word_ext.

Definition Id (E : Ensf) (f : Elt -> Elt) :=
  forall x : Elt, dans x E -> f x = x :>Elt.

Lemma Id_inv :
 forall (E : Ensf) (f : Elt -> Elt) (x : Elt),
 dans x E -> Id E f -> f x = x :>Elt.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.
Qed.

Hint Unfold Id.

Lemma Id_inclus :
 forall (E F : Ensf) (f : Elt -> Elt), inclus F E -> Id E f -> Id F f.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.
Qed.

Lemma map_Id :
 forall (E : Ensf) (f : Elt -> Elt), Id E f -> map f E = E :>Ensf.
(* Goal: forall (E : Ensf) (f : forall _ : Elt, Elt) (_ : Id E f), @eq Ensf (map f E) E *)
intros E f.
(* Goal: forall _ : Id E f, @eq Ensf (map f E) E *)
 elim E; unfold map in |- *.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
 auto.

(* Goal: forall (e : Elt) (e0 : Ensf) (_ : forall _ : Id e0 f, @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e1 : Ensf) {struct e1} : Ensf := match e1 with | empty => empty | add y e2 => add (f y) (map f e2) end) f e0) e0) (_ : Id (add e e0) f), @eq Ensf (add (f e) ((fix map (f : forall _ : Elt, Elt) (e1 : Ensf) {struct e1} : Ensf := match e1 with | empty => empty | add y e2 => add (f y) (map f e2) end) f e0)) (add e e0) *)
 intros a b Hyp_rec Id_a_b_f.
(* Goal: @eq Ensf (add (f a) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) f b)) (add a b) *)
 apply add_add.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
	auto.

(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) f b) b *)
 	apply Hyp_rec.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
	apply Id_inclus with (add a b); auto.
Qed.


Definition Id_words (E : Ensf) (f : Word -> Word) :=
  forall x : Word, inmonoid E x -> f x = x :>Word.

Lemma Id_words_inv :
 forall (E : Ensf) (f : Word -> Word) (x : Word),
 inmonoid E x -> Id_words E f -> f x = x :>Word.

(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.
Qed.


Lemma Id_words_inclus :
 forall (E F : Ensf) (f : Word -> Word),
 inclus F E -> Id_words E f -> Id_words F f.
(* Goal: forall (E F : Ensf) (f : forall _ : Word, Word) (_ : inclus F E) (_ : Id_words E f), Id_words F f *)
intros E F f inclus_F_E Id_E_f.
(* Goal: Id_words E weinvf_wef *)
red in |- *.
(* Goal: forall (x : Word) (_ : inmonoid F x), @eq Word (f x) x *)
intros x inmonoid_F_x.
(* Goal: @eq Word (f x) x *)
apply Id_E_f.
(* Goal: inmonoid E x *)
apply inmonoid_inclus with F; assumption.
Qed.


Lemma extension_Id :
 forall (E : Ensf) (f : Elt -> Elt), Id E f -> Id_words E (Word_ext f).
(* Goal: forall (E : Ensf) (f : forall _ : Elt, Elt) (_ : Id E f), Id_words E (Word_ext f) *)
intros E f Id_E_f.
(* Goal: Id_words E weinvf_wef *)
red in |- *.
(* Goal: forall (x : Word) (_ : inmonoid F x), @ex2 Word (fun y : Word => @eq Word x (wef y)) (fun y : Word => inmonoid E y) *)
simple induction x; clear x.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
	auto.

(* Goal: forall (e : Elt) (w : Word) (_ : forall _ : inmonoid E w, @eq Word (Word_ext f w) w) (_ : inmonoid E (cons e w)), @eq Word (Word_ext f (cons e w)) (cons e w) *)
        unfold Word_ext in |- *.
	(* plus simple :
	Prolog [ cons_cons inmonoid_cons_inv2 inmonoid_cons_inv ] 8.*)
(* Goal: forall (e : Elt) (w : Word) (_ : forall _ : inmonoid E w, @eq Word ((fix Word_ext (f : forall _ : Elt, Elt) (w0 : Word) {struct w0} : Word := match w0 with | nil => nil | cons a w' => cons (f a) (Word_ext f w') end) f w) w) (_ : inmonoid E (cons e w)), @eq Word (cons (f e) ((fix Word_ext (f : forall _ : Elt, Elt) (w0 : Word) {struct w0} : Word := match w0 with | nil => nil | cons a w' => cons (f a) (Word_ext f w') end) f w)) (cons e w) *)
	intros x w Hyp inmonoid_E_cons_x_w.
(* Goal: @eq Word (cons (f x) ((fix Word_ext (f : forall _ : Elt, Elt) (w : Word) {struct w} : Word := match w with | nil => nil | cons a w' => cons (f a) (Word_ext f w') end) f w)) (cons x w) *)
        simpl in |- *.
	
(* Goal: @eq Word (cons x0 w0) (cons e r) *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	apply cons_cons.
(* Goal: @eq Elt (f x) x *)
(* Goal: @eq Word ((fix Word_ext (f : forall _ : Elt, Elt) (w : Word) {struct w} : Word := match w with | nil => nil | cons a w' => cons (f a) (Word_ext f w') end) f w) w *)
		apply Id_E_f; apply inmonoid_cons_inv2 with w; assumption.

(* Goal: @eq Elt x0 e *)
(* Goal: @eq Word w0 r *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
		apply Hyp.
(* Goal: inmonoid E w *)
		apply inmonoid_cons_inv with x; assumption.

Qed.


Section fonctions.


Variable E : Ensf.
Variable F : Ensf.
Variable f : Elt -> Elt.

(*Definition d'une application*)

Definition application := forall x : Elt, dans x E -> dans (f x) F.

Hint Unfold application.

(*Definition de l'injectivite*)

Definition is_mono :=
  forall x y : Elt, dans x E -> dans y E -> f x = f y :>Elt -> x = y :>Elt.



(*Definition surjectivite*)

Definition is_epi :=
  application /\
  (forall x : Elt, dans x F -> exists2 y : Elt, x = f y & dans y E).


Definition is_iso := is_epi /\ is_mono.


Lemma mono_epi_imp_iso : is_mono -> is_epi -> is_iso.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
intros; red in |- *; auto.
Qed.


Variable fw : Word -> Word.

(*Definition d'une application pour les mots*)

Definition application_words :=
  forall x : Word, inmonoid E x -> inmonoid F (fw x).



(*Definition de l'injectivite*)


Definition is_mono_words :=
  forall x y : Word,
  inmonoid E x -> inmonoid E y -> fw x = fw y :>Word -> x = y :>Word.


(*Definition surjectivite pour les fonctions sur les monoides*)


Definition is_epi_words :=
  application_words /\
  (forall x : Word, inmonoid F x -> exists2 y : Word, x = fw y & inmonoid E y).


Definition is_iso_words := is_mono_words /\ is_epi_words.

Lemma mono_epi_imp_iso_words : is_mono_words -> is_epi_words -> is_iso_words.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
intros; red in |- *; auto.
Qed.

End fonctions.


Hint Resolve mono_epi_imp_iso.


Parameter inv : Ensf -> Ensf -> (Elt -> Elt) -> Elt -> Elt.

Axiom
  dans_inv_f :
    forall (E F : Ensf) (f : Elt -> Elt),
    is_iso E F f -> forall x : Elt, dans x F -> dans (inv E F f x) E.
Hint Resolve dans_inv_f.

Axiom
  inv1 :
    forall (E F : Ensf) (f : Elt -> Elt),
    is_iso E F f -> forall x : Elt, dans x E -> inv E F f (f x) = x :>Elt.

Hint Resolve inv1.

Axiom
  inv2 :
    forall (E F : Ensf) (f : Elt -> Elt),
    is_iso E F f -> forall x : Elt, dans x F -> f (inv E F f x) = x :>Elt.

Hint Resolve inv2.

Lemma inv1' :
 forall (E F : Ensf) (f : Elt -> Elt),
 is_iso E F f -> Id E (comp (inv E F f) f).
(* Goal: forall (E F : Ensf) (f : forall _ : Elt, Elt) (_ : is_iso E F f), Id E (comp (inv E F f) f) *)
unfold Id, comp in |- *.
(* Goal: forall (_ : @eq Elt (f e) (f x0)) (_ : @eq Word (wef r) (wef w0)), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
intros.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.
Qed.
Hint Resolve inv1'.
(* On etend la fonction f : Elt-> Elt definie sur V*)
(*en la fonction F=(extension V f)*)
(*definie sur Elt par F(x) = f(x) sur V et F(x)=x ailleurs*)

Axiom
  extension_spec :
    forall (V : Ensf) (f : Elt -> Elt) (x : Elt),
    {y : Elt | dans x V /\ y = f x :>Elt \/ ~ dans x V /\ y = x :>Elt}.
(*
Lemma extension_spec : (V:Ensf)(f:Elt->Elt)(x:Elt)
{y:Elt | ((dans x V)/\<Elt>y=(f x)) \/ (~(dans x V)/\<Elt>y=x)}.
Realizer 
	[V:Ensf][f:Elt -> Elt][x : Elt]
			(<Elt> Match (Dans_spec x V) with 
							(*true*) (f x)
							(*false*) x
			)
.
Program_all.
Save.
*)

Definition extension (V : Ensf) (f : Elt -> Elt) (x : Elt) :=
  let (y, p) return Elt := extension_spec V f x in y.


Lemma extension_in :
 forall (e : Ensf) (f : Elt -> Elt) (x : Elt),
 dans x e -> extension e f x = f x :>Elt.
(* Goal: forall (e : Ensf) (f : forall _ : Elt, Elt) (x : Elt) (_ : not (dans x e)), @eq Elt (extension e f x) x *)
unfold extension in |- *.
(* Goal: forall (e : Ensf) (f : forall _ : Elt, Elt) (x : Elt) (_ : dans x e), @eq Elt (let (y, _) := extension_spec e f x in y) (f x) *)
intros e f x dans_x_e.
(* Goal: @eq Elt (let (y, _) := extension_spec e f x in y) x *)
elim (extension_spec e f x).
(* Goal: forall (x0 : Elt) (_ : and (dans x0 E) (@eq Elt x (f x0))), @ex2 Elt (fun y : Elt => @eq Elt x (f y)) (fun y : Elt => dans y E) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y E) (@eq Elt x (f y))) *)
intro.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
tauto.
Qed.

Lemma extension_out :
 forall (e : Ensf) (f : Elt -> Elt) (x : Elt),
 ~ dans x e -> extension e f x = x :>Elt.
(* Goal: forall (e : Ensf) (f : forall _ : Elt, Elt) (x : Elt) (_ : not (dans x e)), @eq Elt (extension e f x) x *)
unfold extension in |- *.
(* Goal: forall (e : Ensf) (f : forall _ : Elt, Elt) (x : Elt) (_ : not (dans x e)), @eq Elt (let (y, _) := extension_spec e f x in y) x *)
intros e f x N_dans_x_e.
(* Goal: @eq Elt (let (y, _) := extension_spec e f x in y) x *)
elim (extension_spec e f x).
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
intro; tauto.
Qed.



Section fonctions2.


Variable E : Ensf.
Variable F : Ensf.
Variable f : Elt -> Elt.

Hint Unfold application.
Lemma is_epi_f_over_image : is_epi E (map f E) f.

(* Goal: is_epi_words E F wef *)
split.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
 auto.


(* Goal: forall (_ : @eq Elt (f e) (f x0)) (_ : @eq Word (wef r) (wef w0)), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
 intros.
(* Goal: @ex2 Elt (fun y : Elt => @eq Elt x (f y)) (fun y : Elt => dans y E) *)
 cut (exists y : Elt, dans y E /\ x = f y :>Elt).
(* Goal: forall _ : @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E), @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	intro temp; elim temp; clear temp.
(* Goal: forall (x0 : Elt) (_ : and (dans x0 E) (@eq Elt x (f x0))), @ex2 Elt (fun y : Elt => @eq Elt x (f y)) (fun y : Elt => dans y E) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y E) (@eq Elt x (f y))) *)
	intro. intuition.

(* Goal: @ex2 Elt (fun y : Elt => @eq Elt x (f y)) (fun y : Elt => dans y E) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y E) (@eq Elt x (f y))) *)
	prolog [ ex_intro2 ] 4.
	(*Intros y temp; Elim temp; Clear temp ; Intros dans_y egal_y.
	Exists y;Auto.*)

(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
 	auto.

Qed.

Hint Resolve is_epi_f_over_image.

Lemma mono_imp_iso_over_image : is_mono E f -> is_iso E (map f E) f.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.
Qed.

Let invf := inv E F f.

Hint Unfold invf.

Lemma inv_is_mono : is_iso E F f -> is_mono F invf.
(* Goal: forall (_ : @eq Elt (f e) (f x0)) (_ : @eq Word (wef r) (wef w0)), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
intros.
(* Goal: Id_words E weinvf_wef *)
red in |- *.
(* Goal: forall (x y : Elt) (_ : dans x F) (_ : dans y F) (_ : @eq Elt (invf x) (invf y)), @eq Elt x y *)
intros x y dans_x dans_y egal_inv.
(* Goal: @eq Elt x y *)
replace x with (f (inv E F f x)).
(* Goal: @eq Elt (f (inv E F f x)) y *)
(* Goal: @eq Elt (f (inv E F f x)) x *)
replace y with (f (inv E F f y)).
(* Goal: @eq Elt (f (inv E F f x)) (f (inv E F f y)) *)
(* Goal: @eq Elt (f (inv E F f y)) y *)
(* Goal: @eq Elt (f (inv E F f x)) x *)
apply (f_equal (A:=Elt) (B:=Elt)); assumption.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.
Qed.


Lemma inv_is_epi : is_iso E F f -> is_epi F E invf.
(* Goal: forall _ : is_iso E F f, is_epi F E invf *)
unfold invf in |- *.
(* Goal: forall _ : is_iso E F f, Id_words E weinvf_wef *)
intro is_iso_f.
(* Goal: is_epi_words E F wef *)
split.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
 auto. (* Hint : dans_inv_f*)

(* Hints Resolve inv1 .*)
(* Goal: forall (x : Elt) (_ : dans x E), @ex2 Elt (fun y : Elt => @eq Elt x (inv E F f y)) (fun y : Elt => dans y F) *)
 intros x dans_x.
(* Goal: @ex2 Elt (fun y : Elt => @eq Elt x (inv E F f y)) (fun y : Elt => dans y F) *)
 exists (f x); [ apply sym_equal; auto | elim is_iso_f ].
(* Goal: forall (_ : is_epi E F f) (_ : is_mono E f), dans (f x) F *)
 intros is_epi_f. elim is_epi_f.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
 auto.

Qed.

Let wef := Word_ext f.

Lemma application_imp_application_words :
 application E F f -> application_words E F wef.
(* Goal: forall (_ : forall x : Word, @eq Word (Word_ext (comp invf' f) x) (comp_word (Word_ext invf') (Word_ext f) x)) (_ : inmonoid E x), @eq Word (comp_word (Word_ext invf') (Word_ext f) x) x *)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
intro Hyp.
(* Goal: Id_words E weinvf_wef *)
red in |- *.
(* Goal: forall (x : Word) (_ : inmonoid E x), inmonoid F (wef x) *)
intros x inmon; elim inmon; clear inmon.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
	auto.

(* Goal: forall (_ : @eq Elt (f e) (f x0)) (_ : @eq Word (wef r) (wef w0)), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	intros.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
	replace (wef (cons e w)) with (cons (f e) (wef w)); auto.

Qed.

Hint Resolve application_imp_application_words.

Lemma is_mono_f_imp_is_mono_words : is_mono E f -> is_mono_words E wef.
(* Goal: forall (_ : forall x : Word, @eq Word (Word_ext (comp invf' f) x) (comp_word (Word_ext invf') (Word_ext f) x)) (_ : inmonoid E x), @eq Word (comp_word (Word_ext invf') (Word_ext f) x) x *)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
intro Hyp.
(* Goal: Id_words E weinvf_wef *)
red in |- *.
(* Goal: forall (x y : Word) (_ : inmonoid E x) (_ : inmonoid E y) (_ : @eq Word (wef x) (wef y)), @eq Word x y *)
simple induction x.
(* Goal: forall (_ : @eq Elt (f e) (f x0)) (_ : @eq Word (wef r) (wef w0)), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	intros.
(* Goal: @eq Word nil y *)
(* Goal: forall (e : Elt) (w : Word) (_ : forall (y : Word) (_ : inmonoid E w) (_ : inmonoid E y) (_ : @eq Word (wef w) (wef y)), @eq Word w y) (y : Word) (_ : inmonoid E (cons e w)) (_ : inmonoid E y) (_ : @eq Word (wef (cons e w)) (wef y)), @eq Word (cons e w) y *)
	apply sym_equal.
(* Goal: @eq Word y nil *)
(* Goal: forall (e : Elt) (w : Word) (_ : forall (y : Word) (_ : inmonoid E w) (_ : inmonoid E y) (_ : @eq Word (wef w) (wef y)), @eq Word w y) (y : Word) (_ : inmonoid E (cons e w)) (_ : inmonoid E y) (_ : @eq Word (wef (cons e w)) (wef y)), @eq Word (cons e w) y *)
	apply wef_nil with f.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
	auto.

(* Goal: forall (_ : @eq Elt (f e) (f x0)) (_ : @eq Word (wef r) (wef w0)), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	intros x0 w0. intros.
	cut
  (exists x : Elt,
     (exists2 w : Word, cons x w = y & f x = f x0 /\ wef w = wef w0)).
(* Goal: forall _ : @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E), @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	intro temp; elim temp; clear temp.
(* Goal: forall (x : Elt) (_ : @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	intro e.
(* Goal: forall _ : @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E), @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	intro temp; elim temp; clear temp.
(* Goal: forall (x : Word) (_ : @eq Word (cons e x) y) (_ : and (@eq Elt (f e) (f x0)) (@eq Word (wef x) (wef w0))), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	intro r.
(* Goal: forall (_ : @eq Word (cons e r) y) (_ : and (@eq Elt (f e) (f x0)) (@eq Word (wef r) (wef w0))), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	intros y_egal temp.
(* Goal: @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	elim temp; clear temp.
(* Goal: forall (_ : @eq Elt (f e) (f x0)) (_ : @eq Word (wef r) (wef w0)), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	intros.
(* Goal: @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	rewrite <- y_egal.
(* Goal: @eq Word (cons x0 w0) (cons e r) *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	apply cons_cons.
(* Goal: @eq Elt x0 e *)
(* Goal: @eq Word w0 r *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	apply Hyp. (*; Auto.*)
(* Goal: dans x0 E *)
(* Goal: dans e E *)
(* Goal: @eq Elt (f x0) (f e) *)
(* Goal: @eq Word w0 r *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	apply inmonoid_cons_inv2 with w0; assumption.
(* Goal: dans e E *)
(* Goal: @eq Elt (f x0) (f e) *)
(* Goal: @eq Word w0 r *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	apply inmonoid_cons_inv2 with r; rewrite y_egal; assumption.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
	auto.
(* Goal: @eq Word w0 r *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	apply H.
(* Goal: inmonoid E w0 *)
(* Goal: inmonoid E r *)
(* Goal: @eq Word (wef w0) (wef r) *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
		apply (inmonoid_cons_inv E w0 x0); assumption.
(* Goal: inmonoid E r *)
(* Goal: @eq Word (wef w0) (wef r) *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
		apply (inmonoid_cons_inv E r e); rewrite y_egal; assumption.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
		auto.

	(*Resolution du Cut*)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
	unfold wef in |- *.
(*	Apply wef_cons.*)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
	auto.
Qed.

Hint Resolve is_mono_f_imp_is_mono_words.

Lemma is_epi_f_imp_is_epi_words : is_epi E F f -> is_epi_words E F wef.
(* Goal: forall _ : @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E), @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
intro temp; elim temp; clear temp.
(* Goal: forall (_ : application E F f) (_ : forall (x : Elt) (_ : dans x F), @ex2 Elt (fun y : Elt => @eq Elt x (f y)) (fun y : Elt => dans y E)), is_epi_words E F wef *)
intro application_f.
(* Goal: forall _ : forall (x : Elt) (_ : dans x F), @ex2 Elt (fun y : Elt => @eq Elt x (f y)) (fun y : Elt => dans y E), is_epi_words E F wef *)
intro is_epi_f.
(* Goal: is_epi_words E F wef *)
split.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.

(* Goal: forall (x : Word) (_ : inmonoid F x), @ex2 Word (fun y : Word => @eq Word x (wef y)) (fun y : Word => inmonoid E y) *)
simple induction x; clear x.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
	exists nil; auto.

(* Goal: forall (e : Elt) (w : Word) (_ : forall _ : inmonoid F w, @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y)) (_ : inmonoid F (cons e w)), @ex2 Word (fun y : Word => @eq Word (cons e w) (wef y)) (fun y : Word => inmonoid E y) *)
	intros x w Hyp inmonoid_F_cons.
(* Goal: @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
	cut (exists2 y : Word, w = wef y & inmonoid E y). (*1*)
(* Goal: forall _ : @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E), @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	intro temp; elim temp; clear temp.
(* Goal: forall (x0 : Word) (_ : @eq Word w (wef x0)) (_ : inmonoid E x0), @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	intros y1 y1_egal inmonoid_y1.
(* Goal: @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	cut (exists2 x_ant : Elt, x = f x_ant & dans x_ant E). (*2*)
(* Goal: forall _ : @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E), @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	intro temp; elim temp; clear temp.
(* Goal: forall (x0 : Elt) (_ : @eq Elt x (f x0)) (_ : dans x0 E), @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	intros x_ant x_egal dans_x_ant.
(* Goal: @ex2 Word (fun y : Word => @eq Word (cons x w) (wef y)) (fun y : Word => inmonoid E y) *)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	exists (cons x_ant y1).
(* Goal: @eq Word (cons x w) (wef (cons x_ant y1)) *)
(* Goal: inmonoid E (cons x_ant y1) *)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
		unfold wef, Word_ext in |- *.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
		auto.
		
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
		auto. (* inmonoid_cons *)
	(*Cut2*)
(* Goal: @ex2 Elt (fun x_ant : Elt => @eq Elt x (f x_ant)) (fun x_ant : Elt => dans x_ant E) *)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	prolog [ inmonoid_cons_inv2 ] 3.     (*Apply is_epi_f.
		Apply inmonoid_cons_inv2 with w; Assumption.*)

	(*Cut1*)
(* Goal: @ex2 Word (fun y : Word => @eq Word w (wef y)) (fun y : Word => inmonoid E y) *)
	prolog [ inmonoid_cons_inv ] 3. (*Apply Hyp;
			Apply inmonoid_cons_inv with x; Assumption.*)

Qed.

Hint Resolve is_epi_f_imp_is_epi_words.

Lemma is_iso_f_imp_is_iso_words : is_iso E F f -> is_iso_words E F wef.
(* Goal: forall _ : is_iso E F f, Id_words E weinvf_wef *)
intro is_iso_f.
(* Goal: forall (_ : @eq Elt (f e) (f x0)) (_ : @eq Word (wef r) (wef w0)), @eq Word (cons x0 w0) y *)
(* Goal: @ex Elt (fun x : Elt => @ex2 Word (fun w : Word => @eq Word (cons x w) y) (fun w : Word => and (@eq Elt (f x) (f x0)) (@eq Word (wef w) (wef w0)))) *)
elim is_iso_f; intros.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
split; auto.
Qed.

Let invf' := inv E F f.
Let weinvf := Word_ext invf'.
Let weinvf_wef := comp_word weinvf wef.


Lemma is_iso_f_imp_Id_words_weinvf_wef :
 is_iso E F f -> Id_words E weinvf_wef.


(* Goal: forall _ : is_iso E F f, Id_words E weinvf_wef *)
intro is_iso_f.
(* Goal: Id_words E weinvf_wef *)
red in |- *.
(* Goal: forall (x : Word) (_ : inmonoid E x), @eq Word (weinvf_wef x) x *)
intro x.
(* Goal: forall _ : inmonoid E x, @eq Word (weinvf_wef x) x *)
unfold weinvf_wef, weinvf, wef in |- *. 
cut
 (eg_f_W_W (Word_ext (comp invf' f))
    (comp_word (Word_ext invf') (Word_ext f))).
(* Goal: forall (_ : eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f))) (_ : inmonoid E x), @eq Word (comp_word (Word_ext invf') (Word_ext f) x) x *)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
unfold eg_f_W_W in |- *.
(* Goal: forall (_ : forall x : Word, @eq Word (Word_ext (comp invf' f) x) (comp_word (Word_ext invf') (Word_ext f) x)) (_ : inmonoid E x), @eq Word (comp_word (Word_ext invf') (Word_ext f) x) x *)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
intro Hyp.
(* Goal: forall _ : inmonoid E x, @eq Word (comp_word (Word_ext invf') (Word_ext f) x) x *)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
rewrite <- (Hyp x).
(* Goal: forall _ : inmonoid E x, @eq Word (Word_ext (comp invf' f) x) x *)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
generalize x.
(* Goal: forall (x : Word) (_ : inmonoid E x), @eq Word (Word_ext (comp invf' f) x) x *)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
change (Id_words E (Word_ext (comp invf' f))) in |- *.
(* Goal: Id_words E (Word_ext (comp invf' f)) *)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
apply extension_Id.
(* Goal: Id E (comp invf' f) *)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
unfold invf' in |- *.
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.

(*Cut*)
(* Goal: eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f)) *)
auto.
Qed.



End fonctions2.
Hint Resolve mono_imp_iso_over_image.