(* 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                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 gram3.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.
Require Import fonctions.
Require Import Relations.
Require Import gram.
Require Import gram2.


Section resultats_iso_image.

Variable X V R : Ensf.
Variable S : Elt.
Variable f : Elt -> Elt.

Let Gim := imageGram f X V R S.
Let Xim := fst Gim.
Let Gim2 := snd Gim.
Let Vim := fst Gim2.
Let Gim3 := snd Gim2.
Let Rim := fst Gim3.
Let Sim := snd Gim3.

Let invf := inv (union X V) (union Xim Vim) f.

Let Gim' := imageGram invf Xim Vim Rim Sim.
Let Xim' := fst Gim'.
Let Gim2' := snd Gim'.
Let Vim' := fst Gim2'.
Let Gim3' := snd Gim2'.
Let Rim' := fst Gim3'.
Let Sim' := snd Gim3'.

Hypothesis Gram : isGram X V R S.

Lemma Regles_X_V_R : Regles X V R.
Proof isGram4 X V R S Gram.


Hypothesis Mono : is_mono (union X V) f.

Lemma inter_Xim_Vim_empty : inter Xim Vim empty.

(* Goal: inter Xim Vim empty *)
unfold Xim, Vim in |- *; simpl in |- *.
(* Goal: inter (map f X) (map f V) empty *)
red in |- *.
(* Goal: and (inclus empty (map f X)) (and (inclus empty (map f V)) (forall (x : Elt) (_ : dans x (map f X)) (_ : dans x (map f V)), dans x empty)) *)
(*Intuition.*) split; [ idtac | split ].

(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
auto.

(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
auto.

(* Goal: forall (x : Elt) (_ : dans x (map f X)) (_ : dans x (map f V)), dans x empty *)
intros x dans_x_map_f_X dans_x_map_f_V.
(* Goal: dans x empty *)
elimtype (exists y : Elt, dans y X /\ x = f y :>Elt).
(* Goal: forall (x0 : Elt) (_ : and (dans x0 X) (@eq Elt x (f x0))), dans x empty *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
elimtype (exists y : Elt, dans y V /\ x = f y :>Elt).
(* Goal: forall (x0 : Elt) (_ : and (dans x0 V) (@eq Elt x (f x0))) (x1 : Elt) (_ : and (dans x1 X) (@eq Elt x (f x1))), dans x empty *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
intros v temp; elim temp; clear temp.
(* Goal: forall (_ : dans v V) (_ : @eq Elt x (f v)) (x0 : Elt) (_ : and (dans x0 X) (@eq Elt x (f x0))), dans x empty *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
intros dans_v_V x_egal_f_v x_ant temp; elim temp; clear temp.
(* Goal: forall (_ : dans x_ant X) (_ : @eq Elt x (f x_ant)), dans x empty *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
intros dans_x_ant_X x_egal_f_x_ant.
(* Goal: dans x empty *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
elimtype (inter X V empty).
(* Goal: forall (_ : inclus empty X) (_ : and (inclus empty V) (forall (x : Elt) (_ : dans x X) (_ : dans x V), dans x empty)), dans x empty *)
(* Goal: and (inclus empty X) (and (inclus empty V) (forall (x : Elt) (_ : dans x X) (_ : dans x V), dans x empty)) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
intros incl_empty_X temp; elim temp; clear temp. intros incl_empty_V imp.
(* Goal: dans x empty *)
(* Goal: and (inclus empty X) (and (inclus empty V) (forall (x : Elt) (_ : dans x X) (_ : dans x V), dans x empty)) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
apply dans_empty_imp_P with v.
(* Goal: dans v empty *)
(* Goal: and (inclus empty X) (and (inclus empty V) (forall (x : Elt) (_ : dans x X) (_ : dans x V), dans x empty)) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
apply imp.
(* Goal: dans v X *)
(* Goal: dans v V *)
(* Goal: and (inclus empty X) (and (inclus empty V) (forall (x : Elt) (_ : dans x X) (_ : dans x V), dans x empty)) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
replace v with x_ant.
(* Goal: LG Xim Vim Rim Sim w *)
(* Goal: @eq Word w (wef w) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	assumption.
(* Goal: @eq Elt x_ant v *)
(* Goal: dans v V *)
(* Goal: and (inclus empty X) (and (inclus empty V) (forall (x : Elt) (_ : dans x X) (_ : dans x V), dans x empty)) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
	apply Mono.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		auto.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		auto.
(* Goal: LG Xim Vim Rim Sim w *)
(* Goal: @eq Word w (wef w) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		rewrite <- x_egal_f_x_ant; assumption.
(* Goal: LG Xim Vim Rim Sim w *)
(* Goal: @eq Word w (wef w) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
assumption.
(* Goal: and (inclus empty X) (and (inclus empty V) (forall (x : Elt) (_ : dans x X) (_ : dans x V), dans x empty)) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V) (@eq Elt x (f y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y X) (@eq Elt x (f y))) *)
exact (isGram2 X V R S Gram).
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
auto.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
auto.
Qed.


Lemma union_Xim_Vim_map_f_union_X_V :
 union Xim Vim = map f (union X V) :>Ensf.
(* Goal: @eq Ensf (union Xim Vim) (map f (union X V)) *)
unfold Xim, Vim, Gim2, Gim, imageGram in |- *; simpl in |- *.
(* Goal: @eq Ensf (union (map f X) (map f V)) (map f (union X V)) *)
apply map_union.
Qed.

Lemma Iso : is_iso (union X V) (union Xim Vim) f.
(* Goal: is_iso (union X V) (union Xim Vim) f *)
rewrite union_Xim_Vim_map_f_union_X_V.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
auto.
Qed.

Hint Resolve Iso.

Let wef := Word_ext f.
Let weinvf := Word_ext invf.

Lemma invf_f : Id (union X V) (comp invf f).
(* Goal: Id (union X V) (comp invf f) *)
(* Goal: isGram X V R S *)
unfold invf in |- *.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
auto.
Qed.

Lemma weinvf_wef : Id_words (union X V) (comp_word weinvf wef).
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
unfold Id_words in |- *.
(* Goal: forall (x : Word) (_ : inmonoid (union X V) x), @eq Word (comp_word weinvf wef x) x *)
unfold weinvf, wef in |- *.
(* Goal: forall (x : Word) (_ : inmonoid (union X V) x), @eq Word (comp_word (Word_ext invf) (Word_ext f) x) x *)
intro x.
(* Goal: forall _ : inmonoid (union X V) x, @eq Word (comp_word (Word_ext invf) (Word_ext f) x) x *)
rewrite <- (comp_Word_ext invf f x).
(* Goal: forall _ : inmonoid (union X V) x, @eq Word (Word_ext (comp invf f) x) x *)
generalize x.
(* Goal: forall (x : Word) (_ : inmonoid (union X V) x), @eq Word (Word_ext (comp invf f) x) x *)
apply (extension_Id (union X V) (comp invf f)).
(* Goal: Id (union X V) (comp invf f) *)
exact invf_f.
Qed.

Let Rf (g : Elt -> Elt) (P : Elt) :=
  couple (g (first P)) (word (Word_ext g (word_inv (second P)))).

Lemma comp_Rf :
 forall (g f : Elt -> Elt) (x : Elt),
 dans x R -> comp (Rf g) (Rf f) x = Rf (comp g f) x :>Elt.
(* Goal: forall (g f : forall _ : Elt, Elt) (x : Elt) (_ : dans x R), @eq Elt (comp (Rf g) (Rf f) x) (Rf (comp g f) x) *)
clear Mono.
(* Goal: forall (g f : forall _ : Elt, Elt) (x : Elt) (_ : dans x R), @eq Elt (comp (Rf g) (Rf f) x) (Rf (comp g f) x) *)
intros f' g x dans_x_R.
(* Goal: @eq Elt (comp (Rf f') (Rf g) x) (Rf (comp f' g) x) *)
elim (Regles_X_V_R x dans_x_R).
(* Goal: forall (x0 : Elt) (_ : dans x0 V) (_ : @ex2 Word (fun B : Word => @eq Elt x (couple x0 (word B))) (fun B : Word => inmonoid (union X V) B)), @eq Elt (comp (Rf f') (Rf g) x) (Rf (comp f' g) x) *)
intros A dans_A_V temp.
(* Goal: @eq Elt (comp (Rf f') (Rf g) x) (Rf (comp f' g) x) *)
elim temp; clear temp; intros B egal_x inmonoid_B.
(* Goal: @eq Elt (comp (Rf f') (Rf g) x) (Rf (comp f' g) x) *)
rewrite egal_x.
(* Goal: @eq Elt (comp (Rf f') (Rf g) (couple A (word B))) (Rf (comp f' g) (couple A (word B))) *)
unfold Rf in |- *.
(* Goal: @eq Elt (comp (fun P : Elt => couple (f' (first P)) (word (Word_ext f' (word_inv (second P))))) (fun P : Elt => couple (g (first P)) (word (Word_ext g (word_inv (second P))))) (couple A (word B))) (couple (comp f' g (first (couple A (word B)))) (word (Word_ext (comp f' g) (word_inv (second (couple A (word B))))))) *)
unfold comp at 1 in |- *. 
 
(* Goal: @eq Elt (couple (f' (first (couple (g (first (couple A (word B)))) (word (Word_ext g (word_inv (second (couple A (word B))))))))) (word (Word_ext f' (word_inv (second (couple (g (first (couple A (word B)))) (word (Word_ext g (word_inv (second (couple A (word B)))))))))))) (couple (comp f' g (first (couple A (word B)))) (word (Word_ext (comp f' g) (word_inv (second (couple A (word B))))))) *)
apply couple_couple.
(* Goal: @eq Word (weinvf (wef w)) (comp_word weinvf wef w) *)
(* Goal: @eq Word (comp_word weinvf wef w) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
 apply refl_equal.
(* Goal: @eq Word (weinvf (wef w)) (comp_word weinvf wef w) *)
(* Goal: @eq Word (comp_word weinvf wef w) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
 simpl in |- *. rewrite (comp_Word_ext f' g B). apply refl_equal.
Qed.


Lemma egalGim'_image_comp :
 Gim' = imageGram (comp invf f) X V R S :>Ensf * (Ensf * (Ensf * Elt)).
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) Gim' (imageGram (comp invf f) X V R S) *)
unfold Gim' in |- *.
(* Goal: @eq Elt (word (Word_ext f' (word_inv (second (couple (g (first (couple A (word B)))) (word (Word_ext g (word_inv (second (couple A (word B))))))))))) (word (Word_ext (comp f' g) (word_inv (second (couple A (word B)))))) *)
unfold Sim, Rim, Gim3, Vim, Gim2, Xim, Gim, imageGram in |- *; simpl in |- *.

(* Goal: @eq (prod Ensf Elt) (@pair Ensf Elt (map (fun P : Elt => couple (invf (first P)) (word (Word_ext invf (word_inv (second P))))) (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (invf (f S))) (@pair Ensf Elt (map (fun P : Elt => couple (comp invf f (first P)) (word (Word_ext (comp invf f) (word_inv (second P))))) R) (comp invf f S)) *)
apply pair_equal.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
rewrite (map_map_eg_map_comp invf f X); auto.

(* Goal: @eq (prod Ensf Elt) (@pair Ensf Elt (map (fun P : Elt => couple (invf (first P)) (word (Word_ext invf (word_inv (second P))))) (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (invf (f S))) (@pair Ensf Elt (map (fun P : Elt => couple (comp invf f (first P)) (word (Word_ext (comp invf f) (word_inv (second P))))) R) (comp invf f S)) *)
apply pair_equal.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
rewrite (map_map_eg_map_comp invf f V); auto.

(* Goal: @eq (prod Ensf Elt) (@pair Ensf Elt (map (fun P : Elt => couple (invf (first P)) (word (Word_ext invf (word_inv (second P))))) (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (invf (f S))) (@pair Ensf Elt (map (fun P : Elt => couple (comp invf f (first P)) (word (Word_ext (comp invf f) (word_inv (second P))))) R) (comp invf f S)) *)
apply pair_equal.

change (map (Rf invf) (map (Rf f) R) = map (Rf (comp invf f)) R :>Ensf)
 in |- *.
(* Goal: @eq Ensf (map (Rf invf) (map (Rf f) R)) (map (Rf (comp invf f)) R) *)
(* Goal: @eq Elt (invf (f S)) (comp invf f S) *)
replace (map (Rf (comp invf f)) R) with (map (comp (Rf invf) (Rf f)) R).

(* Goal: @eq Ensf (map (Rf invf) (map (Rf f) R)) (map (comp (Rf invf) (Rf f)) R) *)
(* Goal: @eq Ensf (map (comp (Rf invf) (Rf f)) R) (map (Rf (comp invf f)) R) *)
(* Goal: @eq Elt (invf (f S)) (comp invf f S) *)
apply map_map_eg_map_comp. 
(* Goal: @eq Ensf (map (comp (Rf invf) (Rf f)) R) (map (Rf (comp invf f)) R) *)
(* Goal: @eq Elt (invf (f S)) (comp invf f S) *)
apply map_egal.
(* Goal: forall (x : Elt) (_ : dans x R), @eq Elt (comp (Rf invf) (Rf f) x) (Rf (comp invf f) x) *)
(* Goal: @eq Elt (invf (f S)) (comp invf f S) *)
exact (comp_Rf invf f).

(* Goal: @eq Word (weinvf (wef w)) (comp_word weinvf wef w) *)
(* Goal: @eq Word (comp_word weinvf wef w) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
apply refl_equal.
Qed.


Lemma egalG : Gim' = (X, (V, (R, S))).
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) Gim' (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V (@pair Ensf Elt R S))) *)
rewrite egalGim'_image_comp.
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) (imageGram (comp invf f) X V R S) (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V (@pair Ensf Elt R S))) *)
apply Id_image_G.
(* Goal: Id (union X V) (comp invf f) *)
(* Goal: isGram X V R S *)
unfold invf in |- *.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
auto.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
auto.
Qed.


Lemma egalS : Sim' = S :>Elt.
(* Goal: @eq Elt Sim' S *)
unfold Sim', Rim', Gim3', Vim', Gim2', Xim' in |- *.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) Gim')) V *)
rewrite egalG.
(* Goal: @eq Word (weinvf (wef w)) (comp_word weinvf wef w) *)
(* Goal: @eq Word (comp_word weinvf wef w) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
apply refl_equal.
Qed.

Lemma egalR : Rim' = R :>Ensf.
(* Goal: @eq Ensf Rim' R *)
unfold Rim', Gim3', Vim', Gim2', Xim' in |- *.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) Gim')) V *)
rewrite egalG.
(* Goal: @eq Word (weinvf (wef w)) (comp_word weinvf wef w) *)
(* Goal: @eq Word (comp_word weinvf wef w) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
apply refl_equal.
Qed.

Lemma egalX : Xim' = X :>Ensf.
(* Goal: @eq Ensf Vim' V *)
unfold Vim', Gim2', Xim' in |- *.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) Gim')) V *)
rewrite egalG.
(* Goal: @eq Word (weinvf (wef w)) (comp_word weinvf wef w) *)
(* Goal: @eq Word (comp_word weinvf wef w) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
apply refl_equal.
Qed.

Lemma egalV : Vim' = V :>Ensf.
(* Goal: @eq Ensf Vim' V *)
unfold Vim', Gim2', Xim' in |- *.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) Gim')) V *)
rewrite egalG.
(* Goal: @eq Word (weinvf (wef w)) (comp_word weinvf wef w) *)
(* Goal: @eq Word (comp_word weinvf wef w) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
apply refl_equal.
Qed.

Lemma Reconnait_imageGram_iso :
 forall w : Word, inmonoid X w -> LG Xim Vim Rim Sim (wef w) -> LG X V R S w.
(* Goal: forall (w : Word) (_ : inmonoid X w) (_ : LG Xim Vim Rim Sim (wef w)), LG X V R S w *)
intros w inmonoid_X_w LG_wef_w.
(* Goal: LG X V R S w *)
rewrite <- egalR.
(* Goal: LG X V Rim' S w *)
rewrite <- egalS.
(* Goal: LG X V Rim' Sim' w *)
rewrite <- egalV.
(* Goal: LG X Vim' Rim' Sim' w *)
rewrite <- egalX.

(* Goal: LG Xim' Vim' Rim' Sim' w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
replace w with (weinvf (wef w)).
(* Goal: LG Xim' Vim' Rim' Sim' (weinvf (wef w)) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	unfold Sim', Rim', Gim3', Vim', Gim2', Xim', Gim', weinvf in |- *.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	auto.
(* Goal: @eq Word (weinvf (wef w)) w *)
	change (comp_word weinvf wef w = w :>Word) in |- *.
(* Goal: @eq Word (comp_word weinvf wef w) w *)
	apply Id_words_inv with X.
(* Goal: LG Xim Vim Rim Sim w *)
(* Goal: @eq Word w (wef w) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		assumption.
(* Goal: Id_words X (comp_word weinvf wef) *)
		apply Id_words_inclus with (union X V).
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
			auto.
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
			exact weinvf_wef.
Qed.



Lemma egal_Xim : Id X f -> Xim = X :>Ensf.
(* Goal: @eq Elt (word (Word_ext f' (word_inv (second (couple (g (first (couple A (word B)))) (word (Word_ext g (word_inv (second (couple A (word B))))))))))) (word (Word_ext (comp f' g) (word_inv (second (couple A (word B)))))) *)
unfold Xim, Gim, imageGram in |- *; simpl in |- *.
(* Goal: forall _ : Id X f, @eq Ensf (map f X) X *)
intros.
(* Goal: LG Xim Vim Rim Sim w *)
(* Goal: @eq Word w (wef w) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
apply map_Id; assumption.
Qed.


Lemma egal_LG : Id X f -> l_egal (LG X V R S) (LG Xim Vim Rim Sim).
(* Goal: forall _ : Id X f, l_egal (LG X V R S) (LG Xim Vim Rim Sim) *)
unfold l_egal in |- *.
(* Goal: forall _ : Id X f, and (l_inclus (LG X V R S) (LG Xim Vim Rim Sim)) (l_inclus (LG Xim Vim Rim Sim) (LG X V R S)) *)
intro Id_X.
(* Goal: and (l_inclus (LG X V R S) (LG Xim Vim Rim Sim)) (l_inclus (LG Xim Vim Rim Sim) (LG X V R S)) *)
unfold l_inclus in |- *.

(* Goal: and (forall (w : Word) (_ : LG X V R S w), LG Xim Vim Rim Sim w) (forall (w : Word) (_ : LG Xim Vim Rim Sim w), LG X V R S w) *)
split.
(* Goal: forall (w : Word) (_ : LG X V R S w), LG Xim Vim Rim Sim w *)
(* Goal: forall (w : Word) (_ : LG Xim Vim Rim Sim w), LG X V R S w *)
	intros w LG_X_w.
(* Goal: LG Xim Vim Rim Sim w *)
(* Goal: forall (w : Word) (_ : LG Xim Vim Rim Sim w), LG X V R S w *)
	replace w with (wef w).
(* Goal: LG Xim Vim Rim Sim (wef w) *)
(* Goal: @eq Word (wef w) w *)
(* Goal: forall (w : Word) (_ : LG Xim Vim Rim Sim w), LG X V R S w *)
		unfold Sim, Rim, Gim3, Vim, Gim2, Xim, Gim, wef in |- *.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		auto.

(* Goal: @eq Word (wef w) w *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		apply (Id_words_inv X).
(* Goal: inmonoid Xim w *)
(* Goal: @eq Ensf Xim X *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
			prolog [ LG_inv ] 2.
			(*Apply LG_inv with V R S;Assumption.*)
(* Goal: Id_words X wef *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
			exact (extension_Id X f Id_X).

(* Goal: forall (w : Word) (_ : LG Xim Vim Rim Sim w), LG X V R S w *)
	intros w LG_Xim_w.
(* Goal: LG X V R S w *)
	replace X with Xim'.
(* Goal: LG Xim' V R S w *)
(* Goal: @eq Ensf Xim' X *)
	replace V with Vim'.
(* Goal: LG Xim' Vim' R S w *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	replace S with Sim'.
(* Goal: LG Xim' Vim' R Sim' w *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	replace R with Rim'.
(* Goal: LG Xim' Vim' Rim' Sim' w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	replace w with (weinvf (wef w)).
(* Goal: LG Xim' Vim' Rim' Sim' (weinvf (wef w)) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		unfold Sim', Rim', Gim3', Vim', Gim2', Xim', Gim', weinvf in |- *.
(* Goal: LG (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram invf Xim Vim Rim Sim)) (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram invf Xim Vim Rim Sim))) (@fst Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram invf Xim Vim Rim Sim)))) (@snd Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram invf Xim Vim Rim Sim)))) (Word_ext invf (wef w)) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		apply Reconnait_imageGram.
(* Goal: LG Xim Vim Rim Sim (wef w) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		replace (wef w) with w.
(* Goal: LG Xim Vim Rim Sim w *)
(* Goal: @eq Word w (wef w) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
			assumption.
(* Goal: @eq Word w (wef w) *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
			apply sym_equal.
(* Goal: @eq Word (wef w) w *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
			apply (Id_words_inv X).
(* Goal: inmonoid X w *)
(* Goal: Id_words X wef *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
				rewrite <- (egal_Xim Id_X).
(* Goal: inmonoid Xim w *)
(* Goal: @eq Ensf Xim X *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
				prolog [ LG_inv ] 2.
				(*Apply LG_inv with Vim Rim Sim;Assumption.*)
(* Goal: Id_words X wef *)
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
				exact (extension_Id X f Id_X).
(* Goal: @eq Word (weinvf (wef w)) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	pattern w at 2 in |- *; replace w with (comp_word weinvf wef w).
(* Goal: @eq Word (weinvf (wef w)) (comp_word weinvf wef w) *)
(* Goal: @eq Word (comp_word weinvf wef w) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		apply refl_equal.

(* Goal: @eq Word (comp_word weinvf wef w) w *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
		apply Id_words_inv with (union X V).
(* Goal: inmonoid (union X V) w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
			apply inmonoid_inclus with X.
(* Goal: inclus X (union X V) *)
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
				auto.
(* Goal: inmonoid X w *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
				replace X with Xim.
(* Goal: inmonoid Xim w *)
(* Goal: @eq Ensf Xim X *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
				prolog [ LG_inv ] 2.
				(*Apply LG_inv with Vim Rim Sim;Assumption.*)

(* Goal: @eq Ensf Xim X *)
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
				exact (egal_Xim Id_X).
(* Goal: Id_words (union X V) (comp_word weinvf wef) *)
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
			exact weinvf_wef.
(* Goal: @eq Ensf Rim' R *)
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	exact egalR.
(* Goal: @eq Elt Sim' S *)
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	exact egalS.
(* Goal: @eq Ensf Vim' V *)
(* Goal: @eq Ensf Xim' X *)
	exact egalV.
(* Goal: @eq Ensf Xim' X *)
	exact egalX.
Qed.
		
End resultats_iso_image.