Imported Upstream version 8.5~beta1+dfsg

1 files changed, 0 insertions, 608 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v
deleted file mode 100644
index 7deec64d..00000000
--- a/test-suite/bugs/closed/shouldsucceed/2378.v
+++ /dev/null
@@ -1,608 +0,0 @@
-(* 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.