Quelle bug_2378.v Sprache: Coq

Require Import TestSuite.admit.
(* test with Coq 8.3rc1 *)

From Corelib.Program Require Import Basics Tactics.

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 TestSuite.funext.
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.

quality99%

¤ Dauer der Verarbeitung: 0.10 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.