interState.v

(* Definition of the intersection of two states *)
Require Import PolyList.
Require Export stateDec.

Definition interStateP: State -> State -> State ->Prop :=
   [S1, S2, S3:State]
   (inclState S3 S1) /\
   ((inclState S3 S2) /\
    ((S4:State) (inclState S4 S1) -> (inclState S4 S2) ->(inclState S4 S3))).

Theorem interStatePRef: (S1:State)(interStateP S1 S1 S1).
Intros S1; Red; Auto.
Qed.

Theorem interStatePSym:
  (S1, S2, S3:State) (interStateP S1 S2 S3) ->(interStateP S2 S1 S3).
Intuition.
Qed.

Theorem interStatePIncl:
  (S1, S2, S3, S4:State)
  (interStateP S1 S2 S3) -> (inclState S4 S1) -> (inclState S4 S2) ->
  (inclState S4 S3).
Intuition.
Qed.

Theorem interStatePInclSelf:
  (S1, S2:State) (inclState S1 S2) ->(interStateP S1 S2 S1).
Intuition.
Qed.

Theorem interStatePEq:
  (S1, S2, S'1, S'2, S3, S'3:State)
  (interStateP S1 S2 S3) ->
  (interStateP S'1 S'2 S'3) -> (eqState S1 S'1) -> (eqState S2 S'2) ->
  (eqState S3 S'3).
Intuition.
Apply H7; Auto.
Apply inclStateTrans with S2 := S1; Auto.
Apply inclStateTrans with S2 := S2; Auto.
Apply H9; Auto.
Apply inclStateTrans with S2 := S'1; Auto.
Apply inclStateTrans with S2 := S'2; Auto.
Qed.

Fixpoint stripRz[S:State]: (list rZ) :=
   Cases S of
       nil => (nil ?)
      | (cons (pair a b) S') =>
          (cons a (cons (rZComp a) (cons b (cons (rZComp b) (stripRz S')))))
   end.

Theorem eqConstrStateInL:
  (S:State)
  (a, b:rZ) (eqConstrState S a b) -> ~ a=b -> ~ ((a, b:rZ)(eqStateRz S a b)) ->
  (In a (stripRz S)).
Intros S a b H'; Elim H'; Clear H' S a b; Auto; Simpl.
Intros a0 H'0; Case H'0; Auto.
Intros a b p; Case p; Intros a b; Simpl; Auto.
Intros S H' H'0 H'1 H'2; Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2 H'3 H'4.
Case (rZDec a b); Intros Eq1; Auto.
Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2 H'3 H'4.
Case (rZDec a c); Intros Eq1; Auto.
Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2 H'3 H'4.
Case (rZDec a (rZComp b)); Intros Eq1; Auto.
Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2 H'3 H'4.
Case (rZDec a (rZComp c)); Intros Eq1; Auto.
Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2.
Case H'2; Intros a0 b0.
Apply eqStateRzContr with a := b; Auto.
Apply eqStateRzTrans with b := a; Auto.
Qed.

Theorem eqConstrStateInR:
  (S:State)
  (a, b:rZ) (eqConstrState S a b) -> ~ a=b -> ~ ((a, b:rZ)(eqStateRz S a b)) ->
  (In b (stripRz S)).
Intros S a b H'; Elim H'; Clear H' S a b; Auto; Simpl.
Intros a0 H'0; Case H'0; Auto.
Intros a b p; Case p; Intros a b; Simpl; Auto.
Intros S H' H'0 H'1 H'2; Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2 H'3 H'4.
Case (rZDec c d); Intros Eq1; Auto.
Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2 H'3 H'4.
Case (rZDec b d); Intros Eq1; Auto.
Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2 H'3 H'4.
Case (rZDec (rZComp c) d); Intros Eq1; Auto.
Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2 H'3 H'4.
Case (rZDec (rZComp b) d); Intros Eq1; Auto.
Right; Right; Right; Right; Auto.
Intros a b c d S H' H'0 H'1 H'2.
Case H'2; Intros a0 b0.
Apply eqStateRzContr with a := b; Auto.
Apply eqStateRzTrans with b := a; Auto.
Qed.

Fixpoint prodRz[L1:(list rZ)]: (list rZ) ->State :=
   [L2:(list rZ)]
      Cases L1 of
          nil => (nil ?)
         | (cons a L'1) => (app (map [b:rZ](a, b) L2) (prodRz L'1 L2))
      end.

Theorem prodRzProp:
  (a, b:rZ) (S1, S2:(list rZ)) (In a S1) -> (In b S2) ->
  (In (a, b) (prodRz S1 S2)).
Intros a b S1; Elim S1; Simpl; Auto.
Intros a0 l H' S2 H'0; Elim H'0; Clear H'0; Intros H'1; [Rewrite H'1 | Idtac];
Auto.
Intros H'0; Apply in_or_app; Auto.
Left.
Change (In ([b0:rZ](a, b0) b) (map [b0:rZ](a, b0) S2)).
Apply in_map; Auto.
Intros H'0; Apply in_or_app; Auto.
Qed.

Theorem eqConstrStateInDouble:
  (S:State)
  (a, b:rZ) (eqConstrState S a b) -> ~ a=b -> ~ ((a, b:rZ)(eqStateRz S a b)) ->
  (In (a, b) (prodRz (stripRz S) (stripRz S))).
Intros S a b H' H'0 H'1.
Apply prodRzProp; Auto.
Apply eqConstrStateInL with b := b; Auto.
Apply eqConstrStateInR with a := a; Auto.
Qed.

Fixpoint stripRzDec[S1, S2:State]: State :=
   Cases S2 of
       nil => (nil ?)
      | (cons (pair a b) S'2) => Cases (eqConstrStateDec S1 a b) of
                                     (left _) => (cons (a, b) (stripRzDec S1 S'2))
                                    | (right _) => (stripRzDec S1 S'2)
                                 end
   end.

Theorem stripRzDecProp1:
  (S1, S2:State) (a, b:rZ) (In (a, b) (stripRzDec S1 S2)) ->(In (a, b) S2).
Intros S1 S2; Elim S2; Simpl; Auto.
Intros p; Case p; Auto.
Intros c d l H' a b; Case (eqConstrStateDec S1 c d); Simpl; Auto.
Intros H'0 H'1; Elim H'1; Intros H'2; Clear H'1;
[Generalize H'0; Inversion H'2 | Idtac]; Auto.
Qed.

Theorem stripRzDecProp2:
  (S1, S2:State) (a, b:rZ) (In (a, b) (stripRzDec S1 S2)) ->
  (eqConstrState S1 a b).
Intros S1 S2; Elim S2; Simpl; Auto.
Intros a b H'; Elim H'; Clear H' a b.
Intros p; Case p; Auto.
Intros c d l H' a b; Case (eqConstrStateDec S1 c d); Simpl; Auto.
Intros H'0 H'1; Elim H'1; Intros H'2; Clear H'1;
[Generalize H'0; Inversion H'2 | Idtac]; Auto.
Qed.

Theorem stripRzDecProp3:
  (S1, S2:State) (a, b:rZ) (In (a, b) S2) -> (eqStateRz S1 a b) ->
  (In (a, b) (stripRzDec S1 S2)).
Intros S1 S2; Elim S2; Simpl; Auto.
Intros p; Case p; Auto.
Intros c d l H' a b; Case (eqConstrStateDec S1 c d); Simpl; Auto.
Intros H'0 H'1; Elim H'1; Intros H'2; Clear H'1;
[Generalize H'0; Inversion H'2 | Idtac]; Auto.
Intros H'0 H'1; Elim H'1; Intros H'2; Clear H'1;
[Generalize H'0; Inversion H'2 | Idtac]; Auto.
Intros H'1 H'3; Case H'0; Auto.
Rewrite H0; Rewrite H1; Auto.
Qed.

Definition interState: State -> State ->State :=
   [S1, S2:State]
      Cases (eqStateRzContrDec S1) of
          (left _) => S2
         | (right _) =>
             (stripRzDec S2 (stripRzDec S1 (prodRz (stripRz S1) (stripRz S1))))
      end.

Theorem interMemInL: (S1, S2:State)(inclState (interState S1 S2) S1).
Intros S1 S2; Unfold interState.
Case (eqStateRzContrDec S1); Auto.
Intros H'; Apply inclStateIn; Auto.
Intros H'; Apply inclStateIn; Auto.
Intros a b H'.
Apply eqConstrStateImpeqStateRz.
Apply stripRzDecProp2 with S2 := (prodRz (stripRz S1) (stripRz S1)); Auto.
Apply stripRzDecProp1 with S1 := S2; Auto.
Qed.
Hints Resolve interMemInL.

Theorem interMemInR: (S1, S2:State)(inclState (interState S1 S2) S2).
Intros S1 S2; Unfold interState.
Case (eqStateRzContrDec S1); Auto.
Intros H'; Apply inclStateIn; Auto.
Intros a b H'.
Apply eqConstrStateImpeqStateRz.
Apply stripRzDecProp2
     with S2 := (stripRzDec S1 (prodRz (stripRz S1) (stripRz S1))); Auto.
Qed.
Hints Resolve interMemInR.

Theorem interMemEqStateRz:
  (S1, S2:State) (a, b:rZ) (eqStateRz S1 a b) -> (eqStateRz S2 a b) ->
  (eqStateRz (interState S1 S2) a b).
Intros S1 S2; Unfold interState.
Case (eqStateRzContrDec S1); Auto.
Intros H' a b H'0 H'1; Case (rZDec a b); Intros Eqab; Auto.
Rewrite <- Eqab; Auto.
Apply eqStateRzIn; Auto.
Repeat Apply stripRzDecProp3; Auto.
Apply eqConstrStateInDouble; Auto.
Qed.

Theorem interMemProp: (S1, S2:State)(interStateP S1 S2 (interState S1 S2)).
Intros S1 S2.
Red; Intuition.
Red; Auto.
Intros i j H'.
Apply interMemEqStateRz; Auto.
Qed.

Theorem interMemMin:
  (S1, S2, S3:State) (inclState S3 S1) -> (inclState S3 S2) ->
  (inclState S3 (interState S1 S2)).
Intros S1 S2 S3 H' H'0.
Specialize 2 interMemProp with S1 := S1 S2 := S2; Intros H'2; Intuition; Auto.
Qed.
Hints Resolve interMemMin.

Theorem interStateEq:
  (S1, S2, S3, S4:State) (eqState S1 S3) -> (eqState S2 S4) ->
  (eqState (interState S1 S2) (interState S3 S4)).
Intros S1 S2 S3 S4 H' H'0; Red; Split; Apply interMemMin; Auto.
Apply inclStateEqStateComp with S1 := (interState S1 S2) S3 := S1; Auto.
Apply inclStateEqStateComp with S1 := (interState S1 S2) S3 := S2; Auto.
Apply inclStateEqStateComp with S1 := (interState S3 S4) S3 := S3; Auto.
Apply inclStateEqStateComp with S1 := (interState S3 S4) S3 := S4; Auto.
Qed.
Hints Resolve interStateEq.

Theorem interStateSym:
  (S1, S2:State)(eqState (interState S1 S2) (interState S2 S1)).
Red; Split; Auto.
Qed.
Hints Immediate interStateSym.

Theorem interAssoc:
  (S1, S2, S3:State)
  (eqState
     (interState S1 (interState S2 S3)) (interState (interState S1 S2) S3)).
Intros S1 S2 S3; Red; Split; Auto.
Apply interMemMin; Auto.
Apply interMemMin; Auto; Apply inclStateTrans with S2 := (interState S2 S3);
Auto.
Apply inclStateTrans with S2 := (interState S2 S3); Auto.
Apply interMemMin; Auto.
Apply inclStateTrans with S2 := (interState S1 S2); Auto.
Apply interMemMin; Auto.
Apply inclStateTrans with S2 := (interState S1 S2); Auto.
Qed.
Hints Resolve interAssoc.

Theorem ContrInterL:
  (S:State)
  (eqState S (interState S (cons ((rZPlus zero), (rZMinus zero)) (nil ?)))).
Red; Split; Auto.
Qed.
Hints Resolve ContrInterL.

Theorem ContrInterR:
  (S:State)
  (eqState S (interState (cons ((rZPlus zero), (rZMinus zero)) (nil ?)) S)).
Red; Split; Auto.
Qed.
Hints Resolve ContrInterR.

29/06/100, 12:53