proposition: Theorem TraceCorrect : forall (Ar : rArray vM) (T : Trace) (LL : list triplet), TraceInList T LL -> forall S : State, wellFormedArray Ar -> rArrayState Ar S -> match evalTraceF T Ar with | triple Ar' false L => wellFormedArray Ar' /\ (exists S' : State, stalmarckP S LL S' /\ rArrayState Ar' S') /\ OlistRz L /\ (forall e : rNat, ~ InRz (rZPlus e) L -> rArrayGet _ Ar' e = rArrayGet _ Ar e) | triple Ar' true L => exists S' : State, stalmarckP S LL S' /\ contradictory S' end.
proof: Proof. intros Ar T; generalize Ar; clear Ar; elim T; simpl in |- *. intros Ar LL H' S H'0 H'1; repeat (split; auto with stalmarck). exists S; split; auto with stalmarck. red in |- *; apply OlistNil; auto with stalmarck. intros t Ar LL H' S H'0 H'1. generalize (doTripletFCorrect Ar t S H'0 H'1). case (doTripletF Ar t). intros x; case x; auto with stalmarck. intros Ar' b' L'; case b'. intros H'3; Elimc H'3; intros S' E; Elimc E; intros H'3 H'4. exists S'; split; auto with stalmarck. apply stalmarckPref; auto with stalmarck. apply doTripletsTrans with (S2 := S') (t := t); auto with stalmarck. intros H'3; Elimc H'3; intros H'3 H'4; Elimc H'4; intros H'4 H'5; Elimc H'5; intros H'5 H'6. Elimc H'4; intros S' E; Elimc E; intros H'4 H'7. repeat (split; auto with stalmarck). exists S'; split; auto with stalmarck. apply stalmarckTrans with (S2 := S'); auto with stalmarck. apply stalmarckPref; auto with stalmarck. apply doTripletsTrans with (S2 := S') (t := t); auto with stalmarck. intros H'2; repeat (split; auto with stalmarck). exists S; split; auto with stalmarck. red in |- *; apply OlistNil; auto with stalmarck. intros t H' t0 H'0 Ar LL H'1 S H'2 H'3. elim H'1; intros H'4 H'5; clear H'1. generalize (H' Ar LL H'4 S H'2 H'3). case (evalTraceF t Ar). intros Ar'' b'' L''; case b''; simpl in |- *; auto with stalmarck. intros H'1; elim H'1; intros H'6 H'7; elim H'7; intros H'8 H'9; elim H'9; intros H'10 H'11; clear H'9 H'7 H'1. elim H'8; intros S' E; elim E; intros H'1 H'7; clear E H'8. generalize (H'0 Ar'' LL H'5 S' H'6 H'7). case (evalTraceF t0 Ar''); auto with stalmarck. intros Ar''' b''' L'''; case b'''; simpl in |- *; auto with stalmarck. intros H'8; elim H'8; intros S'0 E; elim E; intros H'9 H'12; clear E H'8. exists S'0; split; auto with stalmarck. apply stalmarckTrans with (S2 := S'); auto with stalmarck. intros H'8; elim H'8; intros H'9 H'12; elim H'12; intros H'13 H'14; elim H'14; intros H'15 H'16; clear H'14 H'12 H'8. repeat (split; auto with stalmarck). elim H'13; intros S'0 E; elim E; intros H'8 H'12; clear E H'13. exists S'0; split; auto with stalmarck. apply stalmarckTrans with (S2 := S'); auto with stalmarck. unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. try exact rZltEqComp. intros e H'14. rewrite H'16. apply H'11; auto with stalmarck. Contradict H'14; auto with stalmarck. cut (InclEq _ eqRz L'' (appendf _ rZlt eqRz rZltEDec L'' L''')). intros H'8; inversion H'8; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'14; auto with stalmarck. cut (InclEq _ eqRz L''' (appendf _ rZlt eqRz rZltEDec L'' L''')). intros H'8; inversion H'8; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. intros a b t H' t0 H'0 Ar LL H'1 S H'2 H'3. generalize (addEqMemCorrect Ar a b S H'2 H'3). case (addEqMem Ar a b). intros Ar1 b1 L1; case b1. intros H'4. generalize (addEqMemCorrect Ar a (rZComp b) S H'2 H'3); auto with stalmarck. case (addEqMem Ar a (rZComp b)); auto with stalmarck. intros Ar2 b2 L2; case b2. intros H'5; exists S; split; auto with stalmarck. red in |- *. exists a. apply eqStateRzTrans with (b := rZComp (rZComp b)); auto with stalmarck. apply eqStateRzInv; auto with stalmarck. apply eqStateRzSym; auto with stalmarck. intros H'5; Elimc H'5; intros H'5 H'6; Elimc H'6; intros H'6 H'7; Elimc H'7; intros H'7 H'8. Elimc H'1; intros H'1 H'9. generalize (H'0 Ar2 LL H'9 _ H'5 H'6). case (evalTraceF t0 Ar2); auto with stalmarck. intros Ar2' b2' L2'; case b2'; simpl in |- *; auto with stalmarck. intros H'10; Elimc H'10; intros S' E; Elimc E; intros H'10 H'11. exists S'; split; auto with stalmarck. apply stalmarckTrans with (S2 := S'); auto with stalmarck. apply stalmarckPSplit with (a := a) (b := b) (S2 := addEq (a, b) S) (S3 := S'); auto with stalmarck. red in |- *; split; auto with stalmarck. red in |- *. intros i j H'12. apply interMemEqStateRz; auto with stalmarck. case H'4. intros x H'13. apply eqStateRzContr with (a := x); auto with stalmarck. intros H'10; Elimc H'10; intros H'10 H'11; Elimc H'11; intros H'11 H'12; Elimc H'12; intros H'12 H'13. Elimc H'11; intros S' E; Elimc E; intros H'11 H'14. repeat (split; auto with stalmarck). exists S'; split; auto with stalmarck. apply stalmarckPSplit with (a := a) (b := b) (S2 := addEq (a, b) S) (S3 := S'); auto with stalmarck. red in |- *; split; auto with stalmarck. red in |- *. intros i j H'15. apply interMemEqStateRz; auto with stalmarck. case H'4. intros x H'16. apply eqStateRzContr with (a := x); auto with stalmarck. unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. try exact rZltEqComp. intros e H'15. rewrite H'13. apply H'8; auto with stalmarck. Contradict H'15; auto with stalmarck. cut (InclEq _ eqRz L2 (appendf _ rZlt eqRz rZltEDec L2 L2')). intros H'16; inversion H'16; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'15; auto with stalmarck. cut (InclEq _ eqRz L2' (appendf _ rZlt eqRz rZltEDec L2 L2')). intros H'16; inversion H'16; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. intros H'4; Elimc H'4; intros H'4 H'5; Elimc H'5; intros H'5 H'6; Elimc H'6; intros H'6 H'7. Elimc H'1; intros H'1 H'8. generalize (addEqMemCorrect Ar a (rZComp b) S H'2 H'3); auto with stalmarck. case (addEqMem Ar a (rZComp b)); auto with stalmarck. intros Ar2 b2 L2; case b2. intros H'9. generalize (H' Ar1 LL H'1 _ H'4 H'5). case (evalTraceF t Ar1). intros Ar1' b1' L1'; case b1'; simpl in |- *; auto with stalmarck. intros H'10; Elimc H'10; intros S' E; Elimc E; intros H'10 H'11. exists S'; split; auto with stalmarck. apply stalmarckPSplit with (a := a) (b := b) (S2 := S') (S3 := addEq (a, rZComp b) S); auto with stalmarck. red in |- *; split; auto with stalmarck; auto with stalmarck. red in |- *. intros i j H'12. apply interMemEqStateRz; auto with stalmarck. case H'9. intros x H'13. apply eqStateRzContr with (a := x); auto with stalmarck. intros H'10; Elimc H'10; intros H'10 H'11; Elimc H'11; intros H'11 H'12; Elimc H'12; intros H'12 H'13. repeat (split; auto with stalmarck). Elimc H'11; intros S' E; Elimc E; intros H'11 H'14. exists S'; split; auto with stalmarck. apply stalmarckPSplit with (a := a) (b := b) (S2 := S') (S3 := addEq (a, rZComp b) S); auto with stalmarck. red in |- *; split; auto with stalmarck; auto with stalmarck. red in |- *. intros i j H'15. apply interMemEqStateRz; auto with stalmarck. case H'9. intros x H'16. apply eqStateRzContr with (a := x); auto with stalmarck. unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. try exact rZltEqComp. intros e H'14. rewrite H'13. apply H'7; auto with stalmarck. Contradict H'14; auto with stalmarck. cut (InclEq _ eqRz L1 (appendf _ rZlt eqRz rZltEDec L1 L1')). intros H'15; inversion H'15; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'14; auto with stalmarck. cut (InclEq _ eqRz L1' (appendf _ rZlt eqRz rZltEDec L1 L1')). intros H'15; inversion H'15; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. intros H'9; Elimc H'9; intros H'9 H'10; Elimc H'10; intros H'10 H'11; Elimc H'11; intros H'11 H'12. generalize (H' Ar1 LL H'1 _ H'4 H'5). case (evalTraceF t Ar1). intros Ar1' b1' L1'; case b1'; simpl in |- *; auto with stalmarck. intros H'13; Elimc H'13; intros S' E; Elimc E; intros H'13 H'14. generalize (H'0 Ar2 LL H'8 _ H'9 H'10). case (evalTraceF t0 Ar2). intros Ar2' b2' L2'; case b2'; simpl in |- *; auto with stalmarck. intros H'15; Elimc H'15; intros S'0 E; Elimc E; intros H'15 H'16. exists S'; split; auto with stalmarck. apply stalmarckPSplit with (a := a) (b := b) (S2 := S') (S3 := S'0); auto with stalmarck. split; auto with stalmarck. red in |- *. intros i j H'17. apply interMemEqStateRz; auto with stalmarck. case H'16. intros x H'18. apply eqStateRzContr with (a := x); auto with stalmarck. intros H'15; Elimc H'15; intros H'15 H'16; Elimc H'16; intros H'16 H'17; Elimc H'17; intros H'17 H'18. Elimc H'16; intros S'0 E; Elimc E; intros H'16 H'19. repeat (split; auto with stalmarck). exists S'0; split; auto with stalmarck. apply stalmarckPSplit with (a := a) (b := b) (S2 := S') (S3 := S'0); auto with stalmarck. split; auto with stalmarck. red in |- *. intros i j H'20. apply interMemEqStateRz; auto with stalmarck. case H'14. intros x H'21. apply eqStateRzContr with (a := x); auto with stalmarck. unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. try exact rZltEqComp. intros e H'20. rewrite H'18. apply H'12; auto with stalmarck. Contradict H'20; auto with stalmarck. cut (InclEq _ eqRz L2 (appendf _ rZlt eqRz rZltEDec L2 L2')). intros H'21; inversion H'21; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'20; auto with stalmarck. cut (InclEq _ eqRz L2' (appendf _ rZlt eqRz rZltEDec L2 L2')). intros H'21; inversion H'21; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. intros H'13; Elimc H'13; intros H'13 H'14; Elimc H'14; intros H'14 H'15; Elimc H'15; intros H'15 H'16. cut (OlistRz (appendRz L1 L1')); [ intros O1 | idtac ]. 2: unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. 2: try exact rZltEqComp. cut (forall e : rNat, ~ InRz (rZPlus e) (appendRz L1 L1') -> rArrayGet vM Ar1' e = rArrayGet vM Ar e); [ intros E1 | idtac ]. 2: intros e H'17. 2: rewrite H'16; auto with stalmarck. 2: apply H'7; auto with stalmarck. 2: Contradict H'17; auto with stalmarck. 2: cut (InclEq _ eqRz L1 (appendf _ rZlt eqRz rZltEDec L1 L1')). 2: intros H'18; inversion H'18; red in |- *; auto with stalmarck. 2: apply appendfInclEq1; auto with stalmarck. 2: Contradict H'17; auto with stalmarck. 2: cut (InclEq _ eqRz L1' (appendf _ rZlt eqRz rZltEDec L1 L1')). 2: intros H'18; inversion H'18; red in |- *; auto with stalmarck. 2: apply appendfInclEq2; auto with stalmarck. generalize (H'0 Ar2 LL H'8 _ H'9 H'10). case (evalTraceF t0 Ar2). intros Ar2' b2' L2'; case b2'; simpl in |- *; auto with stalmarck. intros H'17; Elimc H'17; intros S' E; Elimc E; intros H'17 H'18. repeat (split; auto with stalmarck). Elimc H'14; intros S'0 E; Elimc E; intros H'14 H'19. exists S'0; split; auto with stalmarck. apply stalmarckPSplit with (a := a) (b := b) (S2 := S'0) (S3 := S'); auto with stalmarck. split; auto with stalmarck. red in |- *. intros i j H'20. apply interMemEqStateRz; auto with stalmarck. case H'18. intros x H'21. apply eqStateRzContr with (a := x); auto with stalmarck. intros H'17; Elimc H'17; intros H'17 H'18; Elimc H'18; intros H'18 H'19; Elimc H'19; intros H'19 H'20. cut (OlistRz (appendRz L2 L2')); [ intros O2 | idtac ]. 2: unfold appendRz in |- *; red in |- *; apply appendfOlist; auto with stalmarck. 2: try exact rZltEqComp. cut (forall e : rNat, ~ InRz (rZPlus e) (appendRz L2 L2') -> rArrayGet vM Ar2' e = rArrayGet vM Ar e); [ intros E2 | idtac ]. 2: intros e H'21. 2: rewrite H'20; auto with stalmarck. 2: apply H'12; auto with stalmarck. 2: Contradict H'21; auto with stalmarck. 2: cut (InclEq _ eqRz L2 (appendf _ rZlt eqRz rZltEDec L2 L2')). 2: intros H'22; inversion H'22; red in |- *; auto with stalmarck. 2: apply appendfInclEq1; auto with stalmarck. 2: Contradict H'21; auto with stalmarck. 2: cut (InclEq _ eqRz L2' (appendf _ rZlt eqRz rZltEDec L2 L2')). 2: intros H'22; inversion H'22; red in |- *; auto with stalmarck. 2: apply appendfInclEq2; auto with stalmarck. Elimc H'18; intros S'0 E; Elimc E; intros H'18 H'21. Elimc H'14; intros S' E; Elimc E; intros H'14 H'22. cut (inclState S S'); [ intros I1 | idtac ]. cut (inclState S S'0); [ intros I2 | idtac ]. generalize (interMemProp Ar1' Ar2' Ar H'13 H'17 H'2 (appendRz L1 L1') (appendRz L2 L2') O1 O2 _ _ _ H'22 H'21 H'3 I1 I2 E1 E2). case (interMem Ar1' Ar2' Ar (appendRz L1 L1') (appendRz L2 L2')). intros Ar' L' H'23; Elimc H'23; intros H'23 H'24; Elimc H'24; intros H'24 H'25; Elimc H'25; intros H'25 H'26. repeat (split; auto with stalmarck). exists (interState S' S'0); split; auto with stalmarck. apply stalmarckPSplit with (a := a) (b := b) (S2 := S') (S3 := S'0); auto with stalmarck. apply inclStateTrans with (addEq (a, rZComp b) S); auto with stalmarck. apply stalmarckIncl with (L := LL); auto with stalmarck. apply inclStateTrans with (addEq (a, b) S); auto with stalmarck. apply stalmarckIncl with (L := LL); auto with stalmarck. Qed.
imports: Stalmarck(makeTriplet)