|
Require Import TestSuite.admit.
(* 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.
Arguments lpSat : default implicits.
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.
Arguments LPTransfo : default implicits.
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 _ (projT1 p) (tr (projT1 p) (projT2 p)).
Arguments trProd : default implicits.
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 (projT1 p))) st (tr (projT1 p) (projT2 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 (projT1 p)) ext st (H (projT1 p)) (projT2 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 (projT1 p)) ext st (H (projT1 p)) (projT2 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 (projT1 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.
End TRANSFO.
End TTS_TASM.
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
