restrictState.v

Require Import stalmarck.
Require Import ltState.

Theorem contradictoryAddEq:
  (S:State) (a, b:rZ) (contradictory (addEq (a, b) S)) ->
  (eqStateRz S a (rZComp b)).
Intros S a b H'; Cut (eqConstrState (addEq (a, b) S) a (rZComp a)).
Unfold addEq; Intros H'1; Inversion H'1; Auto;
Try (Apply eqStateRzContr with a := a; Auto; Fail).
Apply eqStateRzSym; Auto.
Red in H'.
Elim H'; Intros a0 E; Clear H'.
Apply eqStateRzPImpeqConstrState.
Apply eqStateRzContr with a := a0; Auto.
Qed.
Hints Resolve contradictoryAddEq.

Theorem prodRzInL:
  (a, b:rZ) (L1, L2:(list rZ)) (In (a, b) (prodRz L1 L2)) ->(In a L1).
Intros a b L1; Elim L1; Simpl; Auto.
Intros a0 l H' L2 H'0.
Case (in_app_or H'0); Auto.
Elim L2; Simpl; Auto.
Intros H'1; Elim H'1; Auto.
Intros a1 l0 H'1 H'2; Elim H'2;
[Intros H'3; Inversion H'3; Clear H'2 | Intros H'3; Clear H'2]; Auto.
Intros H'1; Right; Auto.
Apply H' with L2 := L2; Auto.
Qed.

Theorem prodRzInR:
  (a, b:rZ) (L1, L2:(list rZ)) (In (a, b) (prodRz L1 L2)) ->(In b L2).
Intros a b L1; Elim L1; Simpl; Auto.
Intros L2 H'; Elim H'; Auto.
Intros a0 l H' L2 H'0.
Case (in_app_or H'0); Auto.
Elim L2; Simpl; Auto.
Intros a1 l0 H'1 H'2; Elim H'2;
[Intros H'3; Inversion H'3; Clear H'2 | Intros H'3; Clear H'2]; Auto.
Qed.

Fixpoint stripInRz[L:(list rNat); L1:(list rZ)]: (list rZ) :=
   Cases L1 of
       nil => (nil ?)
      | (cons a L1') => Cases (In_dec rNatDec (valRz a) L) of
                            (left _) => (cons a (stripInRz L L1'))
                           | (right _) => (stripInRz L L1')
                        end
   end.

Theorem stripInRzIn1:
  (L:(list rNat)) (L1:(list rZ)) (a:rZ) (In a (stripInRz L L1)) ->
  (In (valRz a) L).
Intros L L1; Elim L1; Simpl; Auto.
Intros a H'; Elim H'; Auto.
Intros a l H' a0.
Case (In_dec rNatDec (valRz a) L); Simpl; Auto.
Intros H'0 H'1; Elim H'1;
[Intros H'2; Rewrite <- H'2; Clear H'1 | Intros H'2; Clear H'1]; Auto.
Qed.

Theorem stripInRzIn:
  (L:(list rNat)) (L1:(list rZ)) (a:rZ) (In a L1) -> (In (valRz a) L) ->
  (In a (stripInRz L L1)).
Intros L L1; Elim L1; Simpl; Auto.
Intros a l H' a0 H'0; Elim H'0;
[Intros H'1; Rewrite <- H'1; Clear H'0 | Intros H'1; Clear H'0]; Auto.
Case (In_dec rNatDec (valRz a) L); Simpl; Auto.
Intros H'0 H'2; Case H'0; Auto.
Case (In_dec rNatDec (valRz a) L); Simpl; Auto.
Qed.

Definition restrictState: State -> (list rNat) ->State :=
   [S:State] [L:(list rNat)]
      Cases (eqStateRzContrDec S) of
          (left _) => (cons (rZTrue, rZFalse) (nil ?))
         | (right _) =>
             (stripRzDec
                S (prodRz (stripInRz L (stripRz S)) (stripInRz L (stripRz S))))
      end.

Theorem restrictStateIncl:
  (S:State) (L:(list rNat))(inclState (restrictState S L) S).
Intros S L; Unfold restrictState.
Case (eqStateRzContrDec S); Auto.
Intros H'; Red; Auto.
Intros H'; Apply inclStateIn; Auto.
Intros a b H'0; Apply eqConstrStateImpeqStateRz.
Apply stripRzDecProp2
     with S2 := (prodRz (stripInRz L (stripRz S)) (stripInRz L (stripRz S)));
Auto.
Qed.

Lemma andSym: (A, B:Prop) A /\ B ->B /\ A.
Intuition.
Qed.

Theorem InState:
  (S:State)
  (L:(list rNat))
  ((a, b:rZ) (In (a, b) S) ->(In (valRz a) L) /\ (In (valRz b) L)) ->
  (a, b:rZ) (eqStateRz S a b) -> ~ a=b -> ~ (contradictory S) ->
  (In (valRz a) L) /\ (In (valRz b) L).
Intros S L H' a b H'0; Generalize H'; Elim H'0; Clear H' H'0 S a b; Auto.
Intros a S H' H'0; Case H'0; Auto.
Intros a b S H' H'0 H'1 H'2 H'3.
Repeat Rewrite valRzComp; Auto.
Apply H'0; Auto.
Red; Intros H'4; Case H'2; Auto.
Rewrite H'4; Auto.
Intros a b S H' H'0 H'1 H'2 H'3.
Apply andSym; Auto.
Intros a b c S H' H'0 H'1 H'2 H'3 H'4 H'5; Split.
Case (rZDec a b); Intros Eqab.
Rewrite Eqab; Auto.
Elim H'2;
[Intros H'9 H'10; Apply H'9; Clear H'2 | Clear H'2 | Clear H'2 | Clear H'2];
Auto.
Rewrite <- Eqab; Auto.
Elim H'0;
[Intros H'9 H'10; Apply H'9; Clear H'0 | Clear H'0 | Clear H'0 | Clear H'0];
Auto.
Case (rZDec b c); Intros Eqbc.
Rewrite <- Eqbc; Auto.
Elim H'0;
[Intros H'9 H'10; Apply H'10; Clear H'0 | Clear H'0 | Clear H'0 | Clear H'0];
Auto.
Rewrite Eqbc; Auto.
Elim H'2;
[Intros H'9 H'10; Apply H'10; Clear H'2 | Clear H'2 | Clear H'2 | Clear H'2];
Auto.
Intros a b c S H' H'0 H'1 H'2 H'3; Case H'3; Auto.
Red.
Exists a; Auto.
Qed.

Theorem restrictContradiction:
  (S:State) (L:(list rNat))
  (iff (contradictory S) (contradictory (restrictState S L))).
Intros S L; Red; Split; Auto.
Unfold restrictState; Case (eqStateRzContrDec S); Auto.
Intros H' H'0; Red; Exists rZTrue; Auto; Auto.
Intros H' H'0; Case H'; Red in H'0.
Elim H'0; Intros a E; Clear H'0.
Intros a0 b; Apply eqStateRzContr with a := a; Auto.
Intros H'; Red in H'.
Elim H'; Intros a E; Clear H'.
Red; Exists a; Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateIncl; Auto.
Qed.

Theorem InRestrictState:
  (S:State)
  (L:(list rNat))
  (a, b:rZ)
  (eqStateRz (restrictState S L) a b) -> ~ a=b -> ~ (contradictory S) ->
  (In (valRz a) L) /\ (In (valRz b) L).
Intros S L a b H' H'0 H'1.
Apply InState with S := (restrictState S L); Auto.
2:Specialize 2 restrictContradiction with S := S L := L; Intros H'3; Red in H'3;
   Auto.
2:Red; Intros H'2; Apply H'1; Auto.
2:Elim H'3; Intros H'4 H'5; LApply H'5;
   [Intros H'6; Apply H'6; Clear H'5 H'3 | Clear H'5 H'3]; Auto.
Intros a0 b0; Unfold restrictState.
Case (eqStateRzContrDec S); Auto.
Intros H'2; Case H'1; Auto.
Red; Exists rZTrue; Auto.
Intros H'2 H'3; Split.
Apply stripInRzIn1 with L1 := (stripRz S); Auto.
Apply prodRzInL with b := b0 L2 := (stripInRz L (stripRz S)); Auto.
Apply stripRzDecProp1 with S1 := S; Auto.
Apply stripInRzIn1 with L1 := (stripRz S); Auto.
Apply prodRzInR with a := a0 L1 := (stripInRz L (stripRz S)); Auto.
Apply stripRzDecProp1 with S1 := S; Auto.
Qed.

Theorem vallStateLtNEq:
  (L:(list rNat))
  (S1, S2:State)
  (inclState S1 S2) ->
  (eqState (restrictState S2 L) S2) ->
  ~ (contradictory S2) -> ~ (eqState S1 S2) ->
  (lt (valState L S2) (valState L S1)).
Intros L S1 S2 H' H'0 Contr0 H'1.
Elim (inclStateDecBis S2 S1); Intros H'4; Auto.
Case H'1; Red; Auto.
Elim H'4; Intros a E; Elim E; Intros b E0; Elim E0; Intros H'2 H'3;
Clear E0 E H'4.
Elim (InRestrictState S2 L a b); [Intros H'10 H'11 | Idtac | Idtac | Idtac];
Auto.
Generalize H'2 H'3 H'10; Clear H'2 H'3 H'10; Case a; Intros a' H'2 H'3 H'4.
Apply vallStateLt with a := (rZPlus a') b := b; Auto.
Apply vallStateLt with a := (rZMinus a') b := b; Auto.
Apply eqStateRzSym; Auto.
Apply eqStateEq with S1 := S2; Auto.
Red; Intros H'4; Case H'3; Rewrite H'4; Auto.
Qed.

Theorem restrictStateComp:
  (S:State)
  (L:(list rNat))
  (a, b:rZ) (In (valRz a) L) -> (In (valRz b) L) -> (eqStateRz S a b) ->
  (eqStateRz (restrictState S L) a b).
Intros S L a b H' H'0 H'1.
Unfold restrictState.
Case (eqStateRzContrDec S).
Intros H'2.
Apply eqStateRzContr with a := rZTrue; Auto.
Intros H'2.
Case (rZDec a b).
Intros H'3; Rewrite H'3; Auto.
Intros H'3.
Apply eqStateRzIn; Auto.
Apply stripRzDecProp3; Auto.
Apply prodRzProp; Auto.
Apply stripInRzIn; Auto.
Apply eqConstrStateInL with b := b; Auto.
Apply stripInRzIn; Auto.
Apply eqConstrStateInR with a := a; Auto.
Qed.

Definition ResTriplet: triplet ->(list rNat) :=
   [t:triplet]
      Cases t of
          (Triplet _ v1 v2 v3) =>
            (cons
               (valRz v1)
               (cons (valRz v2) (cons (valRz v3) (cons zero (nil rNat)))))
      end.

Theorem RestrictAddEq1:
  (S:State)
  (L:(list rNat))
  (a, b:rZ) (In (valRz a) L) -> (In (valRz b) L) -> (In zero L) ->
  (inclState
     (addEq (a, b) (restrictState S L)) (restrictState (addEq (a, b) S) L)).
Intros S L a b H' H'0 H'1.
Apply inclStateIn; Auto.
Simpl; Auto.
Intros a0 b0 H'2; Elim H'2; Clear H'2; Intros H'2; Auto.
Inversion H'2; Auto.
Rewrite <- H0; Auto.
Rewrite <- H1; Auto.
Apply restrictStateComp; Auto.
Apply restrictStateComp; Auto.
Generalize H'2; Unfold restrictState.
Case (eqStateRzContrDec S); Simpl; Auto.
Intros H'3 H'4; Elim H'4; Clear H'4; Intros H'4; Auto; Inversion H'4; Auto.
Intros H'3 H'4.
Apply stripInRzIn1 with L1 := (stripRz S); Auto.
Apply prodRzInL with b := b0 L2 := (stripInRz L (stripRz S)); Auto.
Apply stripRzDecProp1 with S1 := S; Auto.
Generalize H'2; Unfold restrictState.
Case (eqStateRzContrDec S); Simpl; Auto.
Intros H'3 H'4; Elim H'4; Clear H'4; Intros H'4; Auto; Inversion H'4; Auto.
Intros H'3 H'4.
Apply stripInRzIn1 with L1 := (stripRz S); Auto.
Apply prodRzInR with a := a0 L1 := (stripInRz L (stripRz S)); Auto.
Apply stripRzDecProp1 with S1 := S; Auto.
Apply eqStateIncl with S1 := S; Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateIncl.
Qed.

Theorem restrictStateInZeroL:
  (S:State)
  (L:(list rNat)) (a, b:rZ) (In zero L) -> (In (a, b) (restrictState S L)) ->
  (In (valRz a) L).
Intros S L a b H'; Unfold restrictState.
Case (eqStateRzContrDec S); Simpl; Auto.
Intros H'0 H'1; Elim H'1; Clear H'1; Intros H'1; Inversion H'1; Auto.
Intros H'0 H'1.
Apply stripInRzIn1 with L1 := (stripRz S); Auto.
Apply prodRzInL with b := b L2 := (stripInRz L (stripRz S)); Auto.
Apply stripRzDecProp1 with S1 := S; Auto.
Qed.

Theorem restrictStateInZeroR:
  (S:State)
  (L:(list rNat)) (a, b:rZ) (In zero L) -> (In (a, b) (restrictState S L)) ->
  (In (valRz b) L).
Intros S L a b H'; Unfold restrictState.
Case (eqStateRzContrDec S); Simpl; Auto.
Intros H'0 H'1; Elim H'1; Clear H'1; Intros H'1; Inversion H'1; Auto.
Intros H'0 H'1.
Apply stripInRzIn1 with L1 := (stripRz S); Auto.
Apply prodRzInR with a := a L1 := (stripInRz L (stripRz S)); Auto.
Apply stripRzDecProp1 with S1 := S; Auto.
Qed.

Theorem RestrictAddEq2:
  (S:State)
  (L:(list rNat))
  (a, b:rZ) (In (valRz a) L) -> (In (valRz b) L) -> (In zero L) ->
  (inclState
     (restrictState (addEq (a, b) S) L) (addEq (a, b) (restrictState S L))).
Intros S L a b H' H'0 Eqz; Apply inclStateIn; Auto.
Intros a0 b0 H'1.
Cut (eqConstrState (addEq (a, b) S) a0 b0).
Cut (In (valRz a0) L);
[Intros Ina0L | Apply restrictStateInZeroL with S := (addEq (a, b) S) b := b0];
Auto.
Cut (In (valRz b0) L);
[Intros Inb0L | Apply restrictStateInZeroR with S := (addEq (a, b) S) a := a0];
Auto.
Intros H'2; Unfold addEq in H'2; Inversion H'2.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto.
Apply eqStateRzTrans with b := a; Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto.
Apply eqStateRzTrans with b := b; Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto.
Apply eqStateRzTrans with b := b; Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto.
Apply eqStateRzTrans with b := a; Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto.
Apply eqStateRzTrans with b := (rZComp a); Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto; Rewrite valRzComp; Auto.
Apply eqStateRzTrans with b := (rZComp b); Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto; Rewrite valRzComp; Auto.
Apply eqStateRzTrans with b := (rZComp b); Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto; Rewrite valRzComp; Auto.
Apply eqStateRzTrans with b := (rZComp a); Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto; Rewrite valRzComp; Auto.
Apply eqStateContr with p := a q := b; Auto.
Apply eqStateIncl with S1 := (restrictState S L); Auto.
Apply restrictStateComp; Auto; Rewrite valRzComp; Auto.
Apply eqStateRzPImpeqConstrState; Auto.
Apply eqStateIncl with S1 := (restrictState (addEq (a, b) S) L); Auto.
Apply restrictStateIncl; Auto.
Qed.

Theorem RestrictAddEq:
  (S:State)
  (L:(list rNat))
  (a, b:rZ) (In (valRz a) L) -> (In (valRz b) L) -> (In zero L) ->
  (eqState
     (restrictState (addEq (a, b) S) L) (addEq (a, b) (restrictState S L))).
Intros S L a b H' H'0 H'1; Red; Split.
Apply RestrictAddEq2; Auto.
Apply RestrictAddEq1; Auto.
Qed.

Theorem doTripletRestrictAux1:
  (S:State)
  (t:triplet)
  (L:(list rNat))
  (p1, q1, p, q, r, s:rZ)
  (eqStateRz S p1 q1) ->
  (eqStateRz (restrictState S L) p1 q1) ->
  (In (valRz p) L) ->
  (In (valRz q) L) ->
  (In (valRz r) L) ->
  (In (valRz s) L) ->
  (In zero L) ->
  ((eqStateRz (restrictState S L) p1 q1) ->
   (doTripletP
      (restrictState S L) t (addEq (p, q) (addEq (r, s) (restrictState S L))))) ->
  (ex
     State
     [S':State]
     (doTripletP (restrictState S L) t S') /\
     (eqState (restrictState (addEq (p, q) (addEq (r, s) S)) L) S')).
Intros S t L p1 q1 p q r s H' H'0 H'1 H'2 H'3 H'4 H'5 H'6;
Exists (addEq (p, q) (addEq (r, s) (restrictState S L))); Split; Auto.
Apply eqStateTrans with S2 := (addEq (p, q) (restrictState (addEq (r, s) S) L));
Auto.
Apply RestrictAddEq; Auto.
Apply eqStateAddEq; Auto.
Apply RestrictAddEq; Auto.
Qed.

Theorem doTripletRestrictAux2:
  (S:State)
  (t:triplet)
  (L:(list rNat))
  (p1, q1, p, q:rZ)
  (eqStateRz S p1 q1) ->
  (eqStateRz (restrictState S L) p1 q1) ->
  (In (valRz p) L) ->
  (In (valRz q) L) ->
  (In zero L) ->
  ((eqStateRz (restrictState S L) p1 q1) ->
   (doTripletP (restrictState S L) t (addEq (p, q) (restrictState S L)))) ->
  (ex
     State
     [S':State]
     (doTripletP (restrictState S L) t S') /\
     (eqState (restrictState (addEq (p, q) S) L) S')).
Intros S t L p1 q1 p q H' H'0 H'1 H'2 H'3 H'4;
Exists (addEq (p, q) (restrictState S L)); Split; Auto.
Apply RestrictAddEq; Auto.
Qed.

Theorem doTripletRestrict:
  (S1, S2:State)
  (t:triplet) (L:(list rNat)) (doTripletP S1 t S2) -> (incl (ResTriplet t) L) ->
  (Ex [S3:State]
  (doTripletP (restrictState S1 L) t S3) /\ (eqState (restrictState S2 L) S3)).
Intros S1 S2 t L H' H'0; Inversion H';
Apply doTripletRestrictAux1 with 1 := H
  Orelse Apply doTripletRestrictAux2 with 1 := H; Rewrite <- H0 in H'0;
Simpl in H'0; Simpl; Repeat Rewrite valRzComp; Auto with datatypes;
Apply restrictStateComp; Repeat Rewrite valRzComp; Auto with datatypes.
Qed.

Theorem restrictStateInvol:
  (S:State) (L:(list rNat)) (In zero L) ->
  (eqState (restrictState S L) (restrictState (restrictState S L) L)).
Intros S L H; Red; Split; Auto.
2:Apply restrictStateIncl; Auto.
Apply inclStateIn; Auto.
Intros a b H'.
Apply restrictStateComp; Auto.
Apply restrictStateInZeroL with S := S b := b; Auto.
Apply restrictStateInZeroR with S := S a := a; Auto.
Qed.

Theorem restricMonotone:
  (S1, S2:State) (L1, L2:(list rNat)) (inclState S1 S2) -> (incl L1 L2) ->
  (inclState (restrictState S1 L1) (restrictState S2 L2)).
Intros S1 S2 L1 L2 H' H'0.
Apply inclStateIn; Auto.
Intros a b H'1.
Unfold restrictState in H'1; Generalize H'1; Clear H'1.
Case (eqStateRzContrDec S1); Auto.
Intros H'1 H'2; Unfold restrictState.
Case (eqStateRzContrDec S2); Auto.
Intros H'3; Case H'3; Auto.
Intros H'1 H'2.
Apply restrictStateComp; Auto.
Red in H'0.
Apply H'0.
Apply stripInRzIn1 with L1 := (stripRz S1); Auto.
Apply prodRzInL with b := b L2 := (stripInRz L1 (stripRz S1)); Auto.
Apply stripRzDecProp1 with S1 := S1; Auto.
Red in H'0.
Apply H'0.
Apply stripInRzIn1 with L1 := (stripRz S1); Auto.
Apply prodRzInR with a := a L1 := (stripInRz L1 (stripRz S1)); Auto.
Apply stripRzDecProp1 with S1 := S1; Auto.
Apply eqStateIncl with S1 := S1; Auto.
Apply eqStateIncl with S1 := (restrictState S1 L1); Auto.
Apply restrictStateIncl; Auto.
Unfold restrictState; Case (eqStateRzContrDec S1); Auto.
Intros H'3; Case H'1; Auto.
Qed.

Theorem restrictEqComp:
  (S1, S2:State) (L:(list rNat)) (eqState S1 S2) ->
  (eqState (restrictState S1 L) (restrictState S2 L)).
Intros S1 S2 L H'; Red; Split; Apply restricMonotone; Auto with datatypes;
Red in H'; Elim H'; Auto.
Qed.

Theorem restrictDoTripletCompAux1:
  (S1:State)
  (L:(list rNat))
  (p, q, r, s:rZ)
  (In (valRz p) L) ->
  (In (valRz q) L) -> (In (valRz r) L) -> (In (valRz s) L) -> (In zero L) ->
  (eqState
     (addEq (p, q) (addEq (r, s) (restrictState S1 L)))
     (restrictState (addEq (p, q) (addEq (r, s) (restrictState S1 L))) L)).
Intros S1 L p q r s H' H'0 H'1 H'2 H'3.
Apply eqStateTrans with S2 := (restrictState (addEq (p, q) (addEq (r, s) S1)) L);
Auto.
Apply eqStateTrans with S2 := (addEq (p, q) (restrictState (addEq (r, s) S1) L));
Auto.
Apply eqStateAddEq; Auto.
Apply eqStateSym.
Apply RestrictAddEq; Auto with datatypes.
Apply eqStateSym.
Apply RestrictAddEq; Auto with datatypes.
Apply eqStateTrans
     with S2 :=
          (restrictState (restrictState (addEq (p, q) (addEq (r, s) S1)) L) L);
Auto.
Apply restrictStateInvol; Auto with datatypes.
Apply restrictEqComp; Auto.
Apply eqStateTrans with S2 := (addEq (p, q) (restrictState (addEq (r, s) S1) L));
Auto.
Apply RestrictAddEq; Auto with datatypes.
Apply eqStateAddEq; Auto.
Apply RestrictAddEq; Auto with datatypes.
Qed.

Theorem restrictDoTripletCompAux2:
  (S1:State)
  (L:(list rNat))
  (p, q:rZ) (In (valRz p) L) -> (In (valRz q) L) -> (In zero L) ->
  (eqState
     (addEq (p, q) (restrictState S1 L))
     (restrictState (addEq (p, q) (restrictState S1 L)) L)).
Intros S1 L p q H' H'0 H'1.
Apply eqStateTrans with S2 := (restrictState (addEq (p, q) S1) L); Auto.
Apply eqStateTrans with S2 := (addEq (p, q) (restrictState S1 L)); Auto.
Apply eqStateSym.
Apply RestrictAddEq; Auto with datatypes.
Apply eqStateTrans
     with S2 := (restrictState (restrictState (addEq (p, q) S1) L) L); Auto.
Apply restrictStateInvol; Auto with datatypes.
Apply restrictEqComp; Auto.
Apply RestrictAddEq; Auto with datatypes.
Qed.

Theorem restrictDoTripletComp:
  (S1, S2:State)
  (t:triplet)
  (L:(list rNat))
  (incl (ResTriplet t) L) -> (doTripletP (restrictState S1 L) t S2) ->
  (eqState S2 (restrictState S2 L)).
Intros S1 S2 t L H' H'0; Inversion H'0; Auto; Rewrite <- H0 in H'; Simpl in H';
Apply restrictDoTripletCompAux1 Orelse Apply restrictDoTripletCompAux2;
Auto with datatypes; Repeat Rewrite valRzComp; Auto with datatypes.
Qed.

Theorem doTripletRestrictInv:
  (S1, S2:State)
  (t:triplet)
  (L:(list rNat))
  (incl (ResTriplet t) L) -> (doTripletP (restrictState S1 L) t S2) ->
  (Ex [S3:State]
  (doTripletP S1 t S3) /\ (eqState S3 (unionState (restrictState S2 L) S1))).
Intros S1 S2 t L H' H'0.
Elim (doTripletCongruentEx (restrictState S1 L) S2 S1 t);
[Intros S4 E; Elim E; Intros H'4 H'5; Clear E | Idtac]; Auto.
Elim (doTripletEqCompEx (unionState S1 (restrictState S1 L)) S4 S1 t);
[Intros S5 E; Elim E; Intros H'8 H'9; Clear E | Idtac | Idtac]; Auto.
Exists S5; Split; Auto.
Apply eqStateTrans with S2 := S4; Auto.
Apply eqStateTrans with S2 := (unionState S1 S2); Auto.
Apply eqStateTrans with S2 := (unionState S1 (restrictState S2 L)); Auto.
Apply unionStateEq; Auto.
Apply restrictDoTripletComp with S1 := S1 t := t; Auto.
Red; Split; Auto.
Apply unionStateMin; Auto.
Apply restrictStateIncl; Auto.
Qed.

Fixpoint ResTriplets[L:(list triplet)]: (list rNat) :=
   Cases L of
       nil => (cons zero (nil ?))
      | (cons t L') => (app (ResTriplet t) (ResTriplets L'))
   end.

Theorem zeroInL: (L:(list triplet))(In zero (ResTriplets L)).
Intros L; Elim L; Simpl; Auto with datatypes.
Qed.
Hints Resolve zeroInL.

Theorem ResTripletInResTriplets:
  (t:triplet) (L:(list triplet)) (In t L) ->
  (incl (ResTriplet t) (ResTriplets L)).
Intros t L; Elim L; Simpl; Auto.
Intros H'; Elim H'; Auto.
Intros a l H' H'0; Elim H'0;
[Intros H'1; Rewrite <- H'1; Clear H'0 | Intros H'1; Clear H'0];
Auto with datatypes.
Qed.

Theorem doTripletsRestrict:
  (S1, S2:State) (L:(list triplet)) (doTripletsP S1 L S2) ->
  (doTripletsP
     (restrictState S1 (ResTriplets L)) L (restrictState S2 (ResTriplets L))).
Intros S1 S2 L H'; Elim H'; Clear H' L S1 S2; Auto.
Intros S1 S2 L H'; Apply doTripletsRef; Auto.
Apply restrictEqComp; Auto.
Intros S1 S2 S3 L t H' H'0 H'1 H'2.
Apply doTripletsRTrans with S2 := (restrictState S2 (ResTriplets L)); Auto.
Elim (doTripletRestrict S1 S2 t (ResTriplets L));
[Intros S4 E; Elim E; Intros H'10 H'11; Clear E | Idtac | Idtac]; Auto.
Apply doTripletsRTrans with S2 := (restrictState S2 (ResTriplets L)); Auto.
Apply doTripletsTrans with S2 := S4 t := t; Auto.
Apply ResTripletInResTriplets; Auto.
Qed.

Theorem restrictDoTripletsCompAux1:
  (S1, S2:State) (L:(list triplet)) (doTripletsP S1 L S2) ->
  (S3:State) (eqState S1 (restrictState S3 (ResTriplets L))) ->
  (eqState S2 (restrictState S2 (ResTriplets L))).
Intros S1 S2 L H'; Elim H'; Clear H' L S1 S2; Auto.
Intros S1 S2 L H' S3 H'0.
Apply eqStateTrans with S2 := S1; Auto.
Apply eqStateTrans with S2 := (restrictState S3 (ResTriplets L)); Auto.
Apply eqStateTrans
     with S2 :=
          (restrictState (restrictState S3 (ResTriplets L)) (ResTriplets L));
Auto.
Apply restrictStateInvol; Auto.
Apply restrictEqComp; Auto.
Apply eqStateTrans with S2 := S1; Auto.
Intros S1 S2 S3 L t H' H'0 H'1 H'2 S0 H'3.
Elim (doTripletEqCompEx S1 S2 (restrictState S0 (ResTriplets L)) t);
[Intros S4 E; Elim E; Intros H'10 H'11; Clear E | Idtac | Idtac]; Auto.
Apply H'2 with S0 := S2; Auto.
Apply eqStateTrans with S2 := S4; Auto.
Apply eqStateTrans with S2 := (restrictState S4 (ResTriplets L)); Auto.
Apply restrictDoTripletComp with S1 := S0 t := t; Auto.
Apply ResTripletInResTriplets; Auto.
Apply restrictEqComp; Auto.
Qed.

Theorem restrictDoTripletsComp:
  (S1, S2:State)
  (L:(list triplet)) (doTripletsP (restrictState S1 (ResTriplets L)) L S2) ->
  (eqState S2 (restrictState S2 (ResTriplets L))).
Intros S1 S2 L H'.
Apply restrictDoTripletsCompAux1
     with S1 := (restrictState S1 (ResTriplets L)) S3 := S1; Auto.
Qed.

Theorem doTripletsRestrictInv:
  (S1, S2:State)
  (L:(list triplet)) (doTripletsP (restrictState S1 (ResTriplets L)) L S2) ->
  (doTripletsP S1 L (unionState (restrictState S2 (ResTriplets L)) S1)).
Intros S1 S2 L H'.
LApply (restrictDoTripletsComp S1 S2 L); [Intros H'3 | Idtac]; Auto.
Apply doTripletsComp
     with S1 := (unionState S1 (restrictState S1 (ResTriplets L)))
          S2 := (unionState S1 S2); Auto.
Apply doTripletCongruent; Auto.
Red; Split; Auto.
Apply unionStateMin; Auto.
Apply restrictStateIncl; Auto.
Apply eqStateTrans with S2 := (unionState S2 S1); Auto.
Qed.

Theorem doTripletsRestrictBis:
  (S1, S2:State)
  (L:(list triplet))
  (doTripletsP S1 L S2) -> (eqState S1 (restrictState S1 (ResTriplets L))) ->
  (eqState S2 (restrictState S2 (ResTriplets L))).
Intros S1 S2 L H' H'0.
Apply restrictDoTripletsComp with S1 := S1; Auto.
Apply doTripletsComp with S1 := S1 S2 := S2; Auto.
Qed.

29/06/100, 12:53