doTriplets.v

(* Propagation as transitive closure of the one step propagation *)
Require Export doTriplet.
Require Import PolyListAux.

Mutual Inductive doTripletsP: State -> (list triplet) -> State ->Prop :=
     doTripletsRef:
       (S1, S2:State) (L:(list triplet)) (eqState S1 S2) ->(doTripletsP S1 L S2)
    | doTripletsTrans:
        (S1, S2, S3:State)
        (L:(list triplet))
        (t:triplet) (In t L) -> (doTripletP S1 t S2) -> (doTripletsP S2 L S3) ->
        (doTripletsP S1 L S3) .
Hints Resolve doTripletsRef.

Theorem doTripletsComp:
  (S1, S2, S3, S4:State)
  (L:(list triplet))
  (doTripletsP S1 L S2) -> (eqState S3 S1) -> (eqState S4 S2) ->
  (doTripletsP S3 L S4).
Intros S1 S2 S3 S4 L H'; Generalize S3 S4; Elim H'; Clear H' L S1 S2 S3 S4; Auto.
Intros S1 S2 L H' S3 S4 H'0 H'1.
Apply doTripletsRef; Auto.
Apply eqStateTrans with S2 := S1; Auto.
Apply eqStateTrans with S2 := S2; Auto.
Intros S1 S2 S3 L t H' H'0 H'1 H'2 S0 S4 H'3 H'4.
Elim (doTripletEqCompEx S1 S2 S0 t);
[Intros S6 E; Elim E; Intros H'11 H'12; Clear E | Idtac | Idtac]; Auto.
Apply doTripletsTrans with S2 := S6 t := t; Auto.
Qed.

Theorem doTripletsRTrans:
  (S1, S2, S3:State)
  (L:(list triplet)) (doTripletsP S1 L S2) -> (doTripletsP S2 L S3) ->
  (doTripletsP S1 L S3).
Intros S1 S2 S3 L H'; Elim H'; Auto.
Intros S4 S5 L0 H'0 H'1.
Apply doTripletsComp with S1 := S5 S2 := S3; Auto.
Intros S4 S5 S0 L0 t H'0 H'1 H'2 H'3 H'4.
Apply doTripletsTrans with S2 := S5 t := t; Auto.
Qed.

Theorem doTripletsUnionEx:
  (S1, S2:State) (L:(list triplet)) (doTripletsP S1 L S2) ->
  (Ex [S3:State] (eqState S2 (unionState S3 S1))).
Intros S1 S2 L H'; Elim H'; Auto.
Intros S3 S4 H'0 H'1; Exists S3; Auto.
Apply eqStateTrans with S2 := S3; Auto.
Red; Split; Auto.
Intros S3 S4 S5 L0 t H'0 H'1 H'2 H'3.
Elim (doTripletUnionEx S3 S4 t); [Intros S6 E | Idtac]; Auto.
Elim H'3; Intros S7 E0.
Exists (unionState S7 S6).
Apply eqStateTrans with S2 := (unionState S7 S4); Auto.
Rewrite E; Auto.
Apply unionStateAssoc; Auto.
Qed.

Theorem doTripletsIncl:
  (S1, S2:State) (L:(list triplet)) (doTripletsP S1 L S2) ->(inclState S1 S2).
Intros S1 S2 L H'.
Elim (doTripletsUnionEx S1 S2 L); [Intros S3 E | Idtac]; Auto.
Apply inclStateEqStateComp with S1 := S1 S3 := (unionState S3 S1); Auto.
Qed.

Theorem doTripletCongruent:
  (S1, S2, S3:State) (L:(list triplet)) (doTripletsP S1 L S2) ->
  (doTripletsP (unionState S3 S1) L (unionState S3 S2)).
Intros S1 S2 S3 L H'; Elim H'; Clear H' S1 S2 L; Auto.
Intros S1 S2 S0 L t H' H'0 H'1 H'2.
Apply doTripletsRTrans with S2 := (unionState S3 S2); Auto.
Elim (doTripletCongruentEx S1 S2 S3 t);
[Intros S4 E; Elim E; Intros H'8 H'9; Clear E | Idtac]; Auto.
Apply doTripletsRTrans with S2 := S4; Auto.
Apply doTripletsTrans with S2 := S4 t := t; Auto.
Qed.

Theorem doTripletsMonotoneEx:
  (S1, S2, S3:State)
  (L:(list triplet)) (doTripletsP S1 L S3) -> (inclState S1 S2) ->
  (Ex [S4:State] (doTripletsP S2 L S4) /\ (inclState S3 S4)).
Intros S1 S2 S3 L H' H'0.
LApply (doTripletCongruent S1 S3 S2 L); [Intros H'5 | Idtac]; Auto.
Exists (unionState S2 S3); Split; Auto.
Apply doTripletsComp with S1 := (unionState S2 S1) S2 := (unionState S2 S3);
Auto.
Red; Split; Auto.
Qed.

Theorem doTripletsConftEx:
  (L:(list triplet))
  (S1, S2, S3:State) (doTripletsP S1 L S2) -> (doTripletsP S1 L S3) ->
  (Ex [S4:State] (doTripletsP S2 L S4) /\ (doTripletsP S3 L S4)).
Intros L S1 S2 S3 H' H'0.
Elim (doTripletsUnionEx S1 S2 L); [Intros S4 E | Idtac]; Auto.
Elim (doTripletsUnionEx S1 S3 L); [Intros S5 E0 | Idtac]; Auto.
Exists (unionState S5 S2); Split; Auto.
Apply doTripletsComp with S1 := (unionState S4 S1) S2 := (unionState S4 S3);
Auto.
Apply doTripletCongruent; Auto.
Apply eqStateTrans with S2 := (unionState S5 (unionState S4 S1)); Auto.
Apply eqStateTrans with S2 := (unionState (unionState S5 S4) S1); Auto.
Apply unionStateAssoc; Auto.
Apply eqStateTrans with S2 := (unionState (unionState S4 S5) S1); Auto.
Apply eqStateTrans with S2 := (unionState S4 (unionState S5 S1)); Auto.
Apply eqStateTrans with S2 := (unionState (unionState S4 S5) S1); Auto.
Apply eqStateSym; Auto.
Apply unionStateAssoc; Auto.
Apply doTripletsComp with S1 := (unionState S5 S1) S2 := (unionState S5 S2);
Auto.
Apply doTripletCongruent; Auto.
Qed.
(* We don't loose realizability of memories if the triplets are realized *)

Theorem doTripletsRealizeStateEval:
  (f:rNat ->bool)
  (S1, S2:State)
  (L:(list triplet))
  (realizeState f S1) ->
  (doTripletsP S1 L S2) -> (realizeTriplets f L) -> (f zero)=true ->
  (realizeState f S2).
Intros f S1 S2 L H' H'0; Generalize H'; Elim H'0; Auto.
Intros S3 S4 L0 H'1 H'2 H'3 H'4.
Apply realizeStateIncl with S1 := S3; Auto; Inversion H'1; Auto.
Intros S3 S4 S5 L0 t H'1 H'2 H'3 H'4 H'5 H'6 H'7.
Apply H'4; Auto.
Apply realizeStateEval with 2 := H'2; Auto.
Qed.

Theorem doTripletsTermExAux:
  (L:(list triplet)) (S1, S2:State) (doTripletsP S1 L S2) ->
  (t:triplet) (In t L) ->
  (doTripletsP S1 (rem ? tripletDec t L) S2) \/
  (Ex [S3:State]
  (Ex [S4:State]
  (doTripletsP S1 (rem ? tripletDec t L) S3) /\
  ((doTripletP S3 t S4) /\ (doTripletsP S4 (rem ? tripletDec t L) S2)))).
Intros L S1 S2 H'; Elim H'; Clear H' L S1 S2; Auto.
Intros S1 S2 S3 L t H' H'0 H'1 H'2 t0 H'3.
Case (tripletDec t t0); Intros H.
Elim (H'2 t);
[Intros H'6 |
   Intros H'6; Elim H'6; Intros S0 E; Elim E; Intros S4 E0; Elim E0;
    Intros H'7 H'8; Elim H'8; Intros H'9 H'10; Clear H'8 E0 E H'6 | Idtac]; Auto.
Right; Exists S1; Exists S2; Split; Auto; Split; Auto.
Rewrite <- H; Auto.
Rewrite <- H; Auto.
Right; Exists S1; Exists S2; Split; Auto; Split; Auto.
Rewrite <- H; Auto.
Apply doTripletsRTrans with S2 := S0; Auto.
Rewrite <- H; Auto.
Apply doTripletsComp with S1 := S4 S2 := S3; Auto.
Rewrite <- H; Auto.
Apply doTripletInvol with t := t S1 := S1 S2 := S2; Auto.
Apply doTripletsIncl with L := (rem triplet tripletDec t L); Auto.
Elim (H'2 t0);
[Intros H'6 |
   Intros H'6; Elim H'6; Intros S0 E; Elim E; Intros S4 E0; Elim E0;
    Intros H'7 H'8; Elim H'8; Intros H'9 H'10; Clear H'8 E0 E H'6 | Idtac]; Auto.
Left.
Apply doTripletsTrans with S2 := S2 t := t; Auto.
Right; Exists S0; Exists S4; Split; [Idtac | Split]; Auto.
Apply doTripletsTrans with S2 := S2 t := t; Auto.
Qed.

Theorem doTripletsTermEx:
  (L:(list triplet)) (S1, S2:State) (doTripletsP S1 L S2) ->
  (eqState S1 S2) \/
  (Ex [t:triplet]
  (Ex [S3:State]
  (In t L) /\
  ((doTripletP S1 t S3) /\ (doTripletsP S3 (rem ? tripletDec t L) S2)))).
Intros L S1 S2 H'; Inversion H'; Auto.
Right; Exists t; Exists S3; Split; Try Split; Auto.
LApply (doTripletsTermExAux L S3 S2);
[Intros H'3; Elim (H'3 t);
   [Intros H'6 |
     Intros H'6; Elim H'6; Intros S5 E; Elim E; Intros S6 E0; Elim E0;
      Intros H'7 H'8; Elim H'8; Intros H'9 H'10; Clear H'8 E0 E H'6 | Idtac] |
   Idtac]; Auto.
Apply doTripletsRTrans with S2 := S5; Auto.
Apply doTripletsComp with S1 := S6 S2 := S2; Auto.
Apply doTripletInvol with t := t S1 := S1 S2 := S3; Auto.
Apply doTripletsIncl with L := (rem triplet tripletDec t L); Auto.
Qed.

Theorem doTripletsInclList:
  (L1, L2:(list triplet))
  (S1, S2:State) (incl L1 L2) -> (doTripletsP S1 L1 S2) ->(doTripletsP S1 L2 S2).
Intros L1 L2 S1 S2 H' H'0; Generalize L2 H'; Elim H'0; Clear H'0 H' L2; Auto.
Intros S3 S4 S5 L0 t H' H'0 H'1 H'2 L2 H'3.
Apply doTripletsTrans with S2 := S4 t := t; Auto with datatypes.
Qed.

29/06/100, 12:53