summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/2378.v
blob: 35c69db2fe9374497df61a6891e5e8969af46fe7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
(* 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.

Unset Standard Proposition Elimination Names.

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.