1 files changed, 608 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v
new file mode 100644
index 00000000..7deec64d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2378.v
@@ -0,0 +1,608 @@
+(* test with Coq 8.3rc1 *)
+
+Require Import Program.
+
+Inductive Unit: Set := unit: Unit.
+
+Definition eq_dec T := forall x y:T, {x=y}+{x<>y}.
+
+Section TTS_TASM.
+
+Variable Time: Set.
+Variable Zero: Time.
+Variable tle: Time -> Time -> Prop.
+Variable tlt: Time -> Time -> Prop.
+Variable tadd: Time -> Time -> Time.
+Variable tsub: Time -> Time -> Time.
+Variable tmin: Time -> Time -> Time.
+Notation "t1 @<= t2" := (tle t1 t2) (at level 70, no associativity).
+Notation "t1 @< t2" := (tlt t1 t2) (at level 70, no associativity).
+Notation "t1 @+ t2" := (tadd t1 t2) (at level 50, left associativity).
+Notation "t1 @- t2" := (tsub t1 t2) (at level 50, left associativity).
+Notation "t1 @<= t2 @<= t3" := ((tle t1 t2) /\ (tle t2 t3)) (at level 70, t2 at next level).
+Notation "t1 @<= t2 @< t3" := ((tle t1 t2) /\ (tlt t2 t3)) (at level 70, t2 at next level).
+
+Variable tzerop: forall n, (n = Zero) + {Zero @< n}.
+Variable tlt_eq_gt_dec: forall x y, {x @< y} + {x=y} + {y @< x}.
+Variable tle_plus_l: forall n m, n @<= n @+ m.
+Variable tle_lt_eq_dec: forall n m, n @<= m -> {n @< m} + {n = m}.
+
+Variable tzerop_zero: tzerop Zero = inleft (Zero @< Zero) (@eq_refl _ Zero).
+Variable tplus_n_O: forall n, n @+ Zero = n.
+Variable tlt_le_weak: forall n m, n @< m -> n @<= m.
+Variable tlt_irrefl: forall n, ~ n @< n.
+Variable tplus_nlt: forall n m, ~n @+ m @< n.
+Variable tle_n: forall n, n @<= n.
+Variable tplus_lt_compat_l: forall n m p, n @< m -> p @+ n @< p @+ m.
+Variable tlt_trans: forall n m p, n @< m -> m @< p -> n @< p.
+Variable tle_lt_trans: forall n m p, n @<= m -> m @< p -> n @< p.
+Variable tlt_le_trans: forall n m p, n @< m -> m @<= p -> n @< p.
+Variable tle_refl: forall n, n @<= n.
+Variable tplus_le_0: forall n m, n @+ m @<= n -> m = Zero.
+Variable Time_eq_dec: eq_dec Time.
+
+(*************************************************************)
+
+Section PropLogic.
+Variable Predicate: Type.
+
+Inductive LP: Type :=
+  LPPred: Predicate -> LP
+| LPAnd: LP -> LP -> LP
+| LPNot: LP -> LP.
+
+Variable State: Type.
+Variable Sat: State -> Predicate -> Prop.
+
+Fixpoint lpSat st f: Prop :=
+  match f with
+    LPPred p => Sat st p
+  | LPAnd f1 f2 => lpSat st f1 /\ lpSat st f2
+  | LPNot f1 => ~lpSat st f1
+  end.
+End PropLogic.
+
+Implicit Arguments lpSat.
+
+Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
+  match f with
+    LPPred p => p2lp p
+  | LPAnd f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
+  | LPNot f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
+  end.
+Implicit Arguments LPTransfo.
+
+Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := 
+  LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f.
+
+Section TTS.
+
+Variable State: Type.
+
+Record TTS: Type := mkTTS {
+  Init: State -> Prop;
+  Delay: State -> Time -> State -> Prop;
+  Next: State -> State -> Prop;
+  Predicate: Type;
+  Satisfy: State -> Predicate -> Prop
+}.
+
+Definition TTSIndexedProduct Ind (tts: Ind -> TTS): TTS := mkTTS
+  (fun st => forall i, Init (tts i) st)
+  (fun st d st' => forall i, Delay (tts i) st d st')
+  (fun st st' => forall i, Next (tts i) st st')
+  { i: Ind & Predicate (tts i) }
+  (fun st p => Satisfy (tts (projT1 p)) st (projT2 p)).
+
+End TTS.
+
+Section SIMU_F.
+
+Variables StateA StateC: Type.
+
+Record mapping: Type := mkMapping {
+  mState: Type;
+  mInit: StateC -> mState;
+  mNext: mState -> StateC -> mState;
+  mDelay: mState -> StateC -> Time -> mState;
+  mabs: mState -> StateC -> StateA
+}.
+
+Variable m: mapping.
+
+Record simu (Pred: Type) (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuPrf {
+  inv: (mState m) -> StateC -> Prop;
+  invInit: forall st, Init _ c st -> inv (mInit m st) st;
+  invDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 -> inv (mDelay m ex1 st1 d) st2;
+  invNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 -> inv (mNext m ex1 st1) st2;
+  simuInit: forall st, Init _ c st -> Init _ a (mabs m (mInit m st) st);
+  simuDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 ->
+    Delay _ a (mabs m ex1 st1) d (mabs m (mDelay m ex1 st1 d) st2);
+  simuNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 ->
+    Next _ a (mabs m ex1 st1) (mabs m (mNext m ex1 st1) st2);
+  simuPred: forall ext st, inv ext st -> 
+    (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p)) 
+}.
+
+Theorem satProd: forall State Ind Pred (Sat: forall i, State -> Pred i -> Prop) (st:State) i (f: LP (Pred i)),
+  lpSat (Sat i) st f
+  <->
+  lpSat
+    (fun (st : State) (p : {i : Ind &  Pred i}) => Sat (projT1 p) st (projT2 p)) st
+     (addIndex Ind _ i f).
+Proof.
+  induction f; simpl; intros; split; intros; intuition.
+Qed.
+
+Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))):
+  {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) :=
+  fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)).
+
+Implicit Arguments trProd.
+Require Import Setoid.
+
+Theorem satTrProd:
+  forall State Ind Pred (tts: Ind -> TTS State) 
+    (tr: forall i, (Pred  i) -> LP (Predicate _ (tts i))) (st:State) (p: {i:Ind & (Pred i)}),
+  lpSat (Satisfy _ (tts (projS1 p))) st (tr (projS1 p) (projS2 p))
+  <->
+  lpSat (Satisfy _ (TTSIndexedProduct _ _ tts)) st (trProd _ tts tr p).
+Proof.
+  unfold trProd, TTSIndexedProduct; simpl; intros.
+  rewrite (satProd State Ind (fun i => Predicate State (tts i))
+                      (fun i => Satisfy _ (tts i))); tauto.
+Qed.
+
+Theorem simuProd: 
+  forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+    (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
+    (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
+     (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) -> 
+       simu _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
+                  (trProd Pred tta tra) (trProd Pred ttc trc).
+Proof.
+  intros.
+  apply simuPrf with (fun ex st => forall i, inv _ _ (ttc i) (tra i) (trc i) (X i) ex st); simpl; intros; auto.
+  eapply invInit; eauto.
+  eapply invDelay; eauto.
+  eapply invNext; eauto.
+  eapply simuInit; eauto.
+  eapply simuDelay; eauto.
+  eapply simuNext; eauto.
+  split; simpl; intros.
+  generalize (proj1 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  rewrite <- (satTrProd StateA Ind Pred tta tra); apply H1.
+  rewrite (satTrProd StateC Ind Pred ttc trc); apply H0.
+
+  generalize (proj2 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  rewrite <- (satTrProd StateC Ind Pred ttc trc); apply H1.
+  rewrite (satTrProd StateA Ind Pred tta tra); apply H0.
+Qed.
+
+End SIMU_F.
+
+Section TRANSFO.
+
+Record simu_equiv StateA StateC m1 m2 Pred (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuEquivPrf {
+  simuLR: simu StateA StateC m1 Pred a c tra trc;
+  simuRL: simu StateC StateA m2 Pred c a trc tra
+}.
+
+Theorem simu_equivProd: 
+  forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+    (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
+    (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
+     (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) -> 
+       simu_equiv StateA StateC m1 m2 _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
+                  (trProd _ _ Pred tta tra) (trProd _ _ Pred ttc trc).
+Proof.
+  intros; split; intros.
+  apply simuProd; intro.
+  elim (X i); auto.
+  apply simuProd; intro.
+  elim (X i); auto.
+Qed.
+
+Record RTLanguage: Type := mkRTLanguage {
+   Syntax: Type;
+   DynamicState: Syntax -> Type;
+   Semantic: forall (mdl:Syntax), TTS (DynamicState mdl);
+   MdlPredicate: Syntax -> Type;
+   MdlPredicateDefinition: forall mdl, MdlPredicate mdl -> LP (Predicate _ (Semantic mdl))
+}.
+
+Record Transformation (l1 l2: RTLanguage): Type := mkTransformation {
+  Tmodel: Syntax l1 -> Syntax l2;
+  Tl1l2: forall mdl, mapping (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl));
+  Tl2l1: forall mdl, mapping (DynamicState l2 (Tmodel mdl)) (DynamicState l1 mdl);
+  Tpred: forall mdl, MdlPredicate l1 mdl -> LP (MdlPredicate l2 (Tmodel mdl));
+  Tsim: forall mdl, simu_equiv (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl)) (Tl1l2 mdl) (Tl2l1 mdl)
+    (MdlPredicate l1 mdl) (Semantic l1 mdl) (Semantic l2 (Tmodel mdl))
+    (MdlPredicateDefinition l1 mdl)
+    (fun p => LPTransfo (MdlPredicateDefinition l2 (Tmodel mdl)) (Tpred mdl p))
+}.
+
+Section Product.
+
+Record PSyntax (L: RTLanguage): Type := mkPSyntax {
+  pIndex: Type;
+  pIsEmpty: pIndex + {pIndex -> False};
+  pState: Type;
+  pComponents: pIndex -> Syntax L;
+  pIsShared: forall i, DynamicState L (pComponents i) = pState
+}.
+
+Definition pPredicate (L: RTLanguage) (sys: PSyntax L) := { i : pIndex L sys & MdlPredicate L (pComponents L sys i)}.
+
+(* product with shared state *)
+
+Definition PLanguage (L: RTLanguage): RTLanguage := 
+  mkRTLanguage
+    (PSyntax L)
+    (pState L)
+    (fun mdl => TTSIndexedProduct (pState L mdl) (pIndex L mdl)
+      (fun i => match pIsShared L mdl i in (_ = y) return TTS y with
+        eq_refl => Semantic L (pComponents L mdl i)
+       end))
+    (pPredicate L)
+    (fun mdl => trProd _ _ _ _ 
+      (fun i pi => match pIsShared L mdl i as e in (_ = y) return
+                     (LP (Predicate y
+                               match e in (_ = y0) return (TTS y0) with
+                               | eq_refl => Semantic L (pComponents L mdl i)
+                               end))
+     with
+     | eq_refl => MdlPredicateDefinition L (pComponents L mdl i) pi
+     end)).
+
+Inductive Empty: Type :=.
+
+Record isSharedTransfo l1 l2 tr: Prop := isSharedTransfoPrf {
+sameState:  forall mdl i j, 
+  DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
+  DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j));
+sameMState: forall mdl i j, 
+  mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl i)) =
+  mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl j));
+sameM12: forall mdl i j, 
+  Tl1l2 _ _ tr (pComponents l1 mdl i) =
+  match sym_eq (sameState mdl i j) in _=y return mapping _ y with
+    eq_refl => match sym_eq (pIsShared l1 mdl i) in _=x return mapping x _ with
+      eq_refl => match pIsShared l1 mdl j in _=x return mapping x _ with
+        eq_refl => Tl1l2 _ _ tr (pComponents l1 mdl j)
+      end
+    end         
+  end;
+sameM21: forall mdl i j, 
+  Tl2l1 l1 l2 tr (pComponents l1 mdl i) =
+  match
+    sym_eq (sameState mdl i j) in (_ = y)
+    return (mapping y (DynamicState l1 (pComponents l1 mdl i)))
+  with eq_refl =>
+    match
+      sym_eq (pIsShared l1 mdl i) in (_ = y)
+      return
+        (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y)
+    with
+    | eq_refl =>
+        match
+          pIsShared l1 mdl j in (_ = y)
+          return
+            (mapping
+               (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y)
+        with
+        | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl j)
+        end
+    end
+end
+}.
+
+Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl :=
+  mkPSyntax l2 (pIndex l1 mdl)
+    (pIsEmpty l1 mdl)
+    (match pIsEmpty l1 mdl return Type with 
+         inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+        |inright h => pState l1 mdl
+       end)
+    (fun i => Tmodel l1 l2 tr (pComponents l1 mdl i))
+    (fun i => match pIsEmpty l1 mdl as y return
+        (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
+         match y with
+         | inleft i0 =>
+             DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i0))
+         | inright _ => pState l1 mdl
+         end)
+      with
+         inleft j => sameState l1 l2 tr h mdl i j 
+      | inright h => match h i with end
+        end).
+
+Definition compSemantic l mdl i :=
+    match pIsShared l mdl i in (_=y) return TTS y with
+        eq_refl => Semantic l (pComponents l mdl i)
+    end.
+
+Definition compSemanticEq l mdl i s (e: DynamicState l (pComponents l mdl i) = s) :=
+    match e in (_=y) return TTS y with
+        eq_refl => Semantic l (pComponents l mdl i)
+    end.
+
+Definition Pmap12 l1 l2 tr (h: isSharedTransfo l1 l2 tr) (mdl : PSyntax l1) :=
+match
+  pIsEmpty l1 mdl as s
+  return
+    (mapping (pState l1 mdl)
+       match s with
+       | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+       | inright _ => pState l1 mdl
+       end)
+with
+| inleft p =>
+    match
+      pIsShared l1 mdl p in (_ = y)
+      return
+        (mapping y (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))))
+    with
+    | eq_refl => Tl1l2 l1 l2 tr (pComponents l1 mdl p)
+    end
+| inright _ =>
+    mkMapping (pState l1 mdl) (pState l1 mdl) Unit
+      (fun _ : pState l1 mdl => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit)
+      (fun (_ : Unit) (X : pState l1 mdl) => X)
+end.
+
+Definition Pmap21 l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl :=
+match
+  pIsEmpty l1 mdl as s
+  return
+    (mapping
+       match s with
+       | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+       | inright _ => pState l1 mdl
+       end (pState l1 mdl))
+with
+| inleft p =>
+    match
+      pIsShared l1 mdl p in (_ = y)
+      return
+        (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))) y)
+    with
+    | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl p)
+    end
+| inright _ =>
+    mkMapping (pState l1 mdl) (pState l1 mdl) Unit
+      (fun _ : pState l1 mdl => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit)
+      (fun (_ : Unit) (X : pState l1 mdl) => X)
+end.
+
+Definition PTpred l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl (pp : pPredicate l1 mdl):
+  LP (MdlPredicate (PLanguage l2) (PTransfoSyntax l1 l2 tr h mdl)) :=
+match pIsEmpty l1 mdl with
+| inleft _ =>
+      let (x, p) := pp in
+      addIndex (pIndex l1 mdl) (fun i => MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) x
+        (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl x))
+          (LPPred (MdlPredicate l1 (pComponents l1 mdl x)) p))
+| inright f => match f (projS1 pp) with end
+end.
+
+Lemma simu_eqA: 
+  forall A1 A2 C m P sa sc tta ttc (h: A2=A1),
+  simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end) 
+  P (match h in (_=y) return TTS y with eq_refl => sa end)
+  sc (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => tta p end)
+  ttc ->
+  simu A2 C m P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqC: 
+  forall A C1 C2 m P sa sc tta ttc (h: C2=C1),
+  simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end) 
+  P sa (match h in (_=y) return TTS y with eq_refl => sc end)
+  tta (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => ttc p end)
+   ->
+  simu A C2 m P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqA1: 
+  forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
+  simu A1 C m 
+  P 
+  (match (sym_eq h) in (_=y) return TTS y with eq_refl => sa end) sc
+  (fun p => match (sym_eq h) as e in (_=y) return LP (Predicate y (match e in (_=z) return TTS z with eq_refl => sa end)) with eq_refl => tta p end) ttc
+   ->
+  simu A2 C (match h in (_=y) return mapping _ C with eq_refl => m end) P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqA2: 
+  forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
+  simu A1 C (match (sym_eq h) in (_=y) return mapping _ C with eq_refl => m end)
+  P 
+  sa sc tta ttc
+   ->
+  simu A2 C m P
+  (match h in (_=y) return TTS y with eq_refl => sa end) sc 
+  (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sa end) with eq_refl => tta p end)
+ ttc.
+admit.
+Qed.
+
+Lemma simu_eqC2: 
+  forall A C1 C2 m P sa sc tta ttc (h: C1=C2),
+  simu A C1 (match (sym_eq h) in (_=y) return mapping A _ with eq_refl => m end)
+  P 
+  sa sc tta ttc
+   ->
+  simu A C2 m P
+  sa (match h in (_=y) return TTS y with eq_refl => sc end) 
+  tta (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sc end) with eq_refl => ttc p end).
+admit.
+Qed.
+
+Lemma simu_eqM: 
+  forall A C m1 m2 P sa sc tta ttc (h: m1=m2),
+  simu A C m1 P sa sc tta ttc
+   ->
+  simu A C m2 P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma LPTransfo_trans:
+  forall Pred1 Pred2 Pred3 (tr1: Pred1 -> LP Pred2) (tr2: Pred2 -> LP Pred3) f,
+    LPTransfo tr2 (LPTransfo tr1 f) = LPTransfo (fun x => LPTransfo tr2 (tr1 x)) f.
+Proof.
+  admit.
+Qed.
+
+Lemma LPTransfo_addIndex:
+  forall Ind Pred tr1 x (tr2: forall i, Pred i -> LP (tr1 i)) (p: LP (Pred x)),
+    addIndex Ind tr1 x (LPTransfo (tr2 x) p) =
+    LPTransfo
+      (fun p0 : {i : Ind & Pred i} =>
+        addIndex Ind tr1 (projT1 p0) (tr2 (projT1 p0) (projT2 p0)))
+      (addIndex Ind Pred x p).
+Proof.
+  unfold addIndex; intros. 
+  rewrite LPTransfo_trans.
+  rewrite LPTransfo_trans.
+  simpl.
+  auto.
+Qed.
+
+Record tr_compat I0 I1 tr := compatPrf {
+  and_compat: forall p1 p2, tr (LPAnd I0 p1 p2) = LPAnd I1 (tr p1) (tr p2);
+  not_compat: forall p, tr (LPNot I0 p) = LPNot I1 (tr p)
+}.
+
+Lemma LPTransfo_addIndex_tr:
+  forall Ind Pred tr0 tr1 x (tr2: forall i, Pred i -> LP (tr0 i))  (tr3: forall i, LP (tr0 i) -> LP (tr1 i)) (p: LP (Pred x)),
+    (forall x, tr_compat (tr0 x) (tr1 x) (tr3 x)) ->
+    addIndex Ind tr1 x (tr3 x (LPTransfo (tr2 x) p)) =
+    LPTransfo
+      (fun p0 : {i : Ind & Pred i} =>
+        addIndex Ind tr1 (projT1 p0) (tr3 (projT1 p0) (tr2 (projT1 p0) (projT2 p0))))
+      (addIndex Ind Pred x p).
+Proof.
+  unfold addIndex; simpl; intros. 
+  rewrite LPTransfo_trans; simpl.
+  rewrite <- LPTransfo_trans.
+  f_equal.
+  induction p; simpl; intros; auto.
+  rewrite (and_compat _ _ _ (H x)).
+  rewrite <- IHp1, <- IHp2; auto.
+  rewrite <- IHp.
+  rewrite (not_compat _ _ _ (H x)); auto.
+Qed.
+
+Require Export Coq.Logic.FunctionalExtensionality.
+Print PLanguage.
+Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): 
+Transformation (PLanguage l1) (PLanguage l2) :=
+  mkTransformation (PLanguage l1) (PLanguage l2)
+    (PTransfoSyntax l1 l2 tr h)
+    (Pmap12 l1 l2 tr h)
+    (Pmap21 l1 l2 tr h)
+    (PTpred l1 l2 tr h)
+    (fun mdl => simu_equivProd 
+      (pState l1 mdl) 
+      (pState l2 (PTransfoSyntax l1 l2 tr h mdl)) 
+      (Pmap12 l1 l2 tr h mdl)
+      (Pmap21 l1 l2 tr h mdl)
+      (pIndex l1 mdl) 
+      (fun i => MdlPredicate l1 (pComponents l1 mdl i))
+      (compSemantic l1 mdl)
+      (compSemantic l2 (PTransfoSyntax l1 l2 tr h mdl))
+      _
+      _
+      _
+        ).
+
+Next Obligation.
+  unfold compSemantic, PTransfoSyntax; simpl.
+  case (pIsEmpty l1 mdl); simpl; intros.
+  unfold pPredicate; simpl.
+  unfold pPredicate in X; simpl in X.
+  case (sameState l1 l2 tr h mdl i p).
+  apply (LPTransfo (MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))).
+  apply (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl i))).
+  apply (LPPred _ X).
+
+  apply False_rect; apply (f i).
+Defined.
+
+Next Obligation.
+  split; intros.
+  unfold Pmap12; simpl.
+  unfold PTransfo_obligation_1; simpl.
+  unfold compSemantic; simpl.
+  unfold eq_ind, eq_rect, f_equal; simpl.
+  case (pIsEmpty l1 mdl); intros.
+  apply simu_eqA2.
+  apply simu_eqC2.
+  apply simu_eqM with (Tl1l2 l1 l2 tr (pComponents l1 mdl i)).
+  apply sameM12.
+  apply (simuLR _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro.
+
+  apply False_rect; apply (f i).
+
+  unfold Pmap21; simpl.
+  unfold PTransfo_obligation_1; simpl.
+  unfold compSemantic; simpl.
+  unfold eq_ind, eq_rect, f_equal; simpl.
+  case (pIsEmpty l1 mdl); intros.
+  apply simu_eqC2.
+  apply simu_eqA2.
+  apply simu_eqM with (Tl2l1 l1 l2 tr (pComponents l1 mdl i)).
+  apply sameM21.
+  apply (simuRL _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro.
+
+  apply False_rect; apply (f i).
+Qed.
+
+Next Obligation.
+  unfold trProd; simpl.
+  unfold PTransfo_obligation_1; simpl.
+  unfold compSemantic; simpl.
+  unfold eq_ind, eq_rect, f_equal; simpl.
+  apply functional_extensionality; intro.
+  case x; clear x; intros.
+  unfold PTpred; simpl.
+  case (pIsEmpty l1 mdl); simpl; intros.
+  set (tr0 i :=
+   Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))
+     (Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))).
+  set (tr1 i :=
+   Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p)))
+     match sameState l1 l2 tr h mdl i p in (_ = y) return (TTS y) with
+     | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+     end).
+  set (tr2 x := MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))).
+  set (Pred x := MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))).
+  set (tr3 x f := match
+    sameState l1 l2 tr h mdl x p as e in (_ = y)
+    return
+      (LP
+         (Predicate y
+            match e in (_ = y0) return (TTS y0) with
+            | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))
+            end))
+  with
+  | eq_refl => f
+  end).
+  apply (LPTransfo_addIndex_tr _ Pred tr0 tr1 x tr2 tr3
+    (Tpred l1 l2 tr (pComponents l1 mdl x) m)).
+  unfold tr0, tr1, tr3; intros; split; simpl; intros; auto.
+  case (sameState l1 l2 tr h mdl x0 p); auto.
+  case (sameState l1 l2 tr h mdl x0 p); auto.
+
+  apply False_rect; apply (f x).
+Qed.
+
+End Product.