unionState.v

(* Definition of the union of two states *)

Require Import PolyList.
Require Export state.

Mutual Inductive unionStateP: State -> State -> State ->Prop :=
     unionStatePDef:
       (S1, S2, S3:State)
       (inclState S1 S3) ->
       (inclState S2 S3) ->
       ((S4:State) (inclState S1 S4) -> (inclState S2 S4) ->(inclState S3 S4)) ->
       (unionStateP S1 S2 S3) .
Hints Resolve unionStatePDef.

Theorem unionStatePRef: (S1:State)(unionStateP S1 S1 S1).
Auto.
Qed.

Theorem unionStatePSym:
  (S1, S2, S3:State) (unionStateP S1 S2 S3) ->(unionStateP S2 S1 S3).
Intros S1 S2 S3 H'; Inversion H'; Auto.
Qed.

Theorem unionStatePIncl:
  (S1, S2, S3, S4:State)
  (unionStateP S1 S2 S3) -> (inclState S1 S4) -> (inclState S2 S4) ->
  (inclState S3 S4).
Intros S1 S2 S3 S4 H' H'0 H'1; Inversion H'; Auto.
Qed.

Theorem unionStatePInclSelf:
  (S1, S2:State) (inclState S2 S1) ->(unionStateP S1 S2 S1).
Auto.
Qed.

Theorem unionStatePEq:
  (S1, S2, S'1, S'2, S3, S'3:State)
  (unionStateP S1 S2 S3) ->
  (unionStateP S'1 S'2 S'3) -> (eqState S1 S'1) -> (eqState S2 S'2) ->
  (eqState S3 S'3).
Intros S1 S2 S'1 S'2 S3 S'3 H' H'0; Inversion H'; Inversion H'0; Auto.
Intros H'1 H'2; Red; Split; Auto.
Apply H1; Auto.
Apply inclStateEqStateComp with S1 := S'1 S3 := S'3; Auto.
Apply inclStateEqStateComp with S1 := S'2 S3 := S'3; Auto.
Apply H7; Auto.
Apply inclStateEqStateComp with S1 := S1 S3 := S3; Auto.
Apply inclStateEqStateComp with S1 := S2 S3 := S3; Auto.
Qed.

Theorem unionStatePEqComp:
  (S1, S2, S3, S'1, S'2, S'3:State)
  (unionStateP S1 S2 S3) ->
  (eqState S1 S'1) -> (eqState S2 S'2) -> (eqState S3 S'3) ->
  (unionStateP S'1 S'2 S'3).
Intros S1 S2 S3 S'1 S'2 S'3 H' H'0 H'1 H'2.
Apply unionStatePDef; Auto.
Apply inclStateEqStateComp with S1 := S1 S3 := S3; Auto.
Inversion H'; Auto.
Apply inclStateEqStateComp with S1 := S2 S3 := S3; Auto.
Inversion H'; Auto.
Intros S4 H'3 H'4.
Apply inclStateEqStateComp with S1 := S3 S3 := S4; Auto.
Inversion H'; Auto.
Apply H1; Auto.
Apply inclStateEqStateComp with S1 := S'1 S3 := S4; Auto.
Apply inclStateEqStateComp with S1 := S'2 S3 := S4; Auto.
Qed.

Theorem unionStateAssoc1:
  (S1, S2, S3, S'1, S'2, S'3:State)
  (unionStateP S1 S2 S'1) ->
  (unionStateP S'1 S3 S'2) -> (unionStateP S2 S3 S'3) ->(unionStateP S1 S'3 S'2).
Intros S1 S2 S3 S'1 S'2 S'3 H' H'0 H'1.
Apply unionStatePDef; Auto.
Apply inclStateTrans with S2 := S'1; Auto.
Inversion H'; Auto.
Inversion H'0; Auto.
Apply unionStatePIncl with 1 := H'1; Auto.
Apply inclStateTrans with S2 := S'1; Auto.
Inversion H'; Auto.
Inversion H'0; Auto.
Inversion H'0; Auto.
Intros S4 H'2 H'3.
Apply unionStatePIncl with 1 := H'0; Auto.
Apply unionStatePIncl with 1 := H'; Auto.
Apply inclStateTrans with S2 := S'3; Auto.
Inversion H'1; Auto.
Apply inclStateTrans with S2 := S'3; Auto.
Inversion H'1; Auto.
Qed.

Theorem unionStatePAssoc2:
  (S1, S2, S3, S'1, S'2, S'3:State)
  (unionStateP S2 S3 S'1) ->
  (unionStateP S1 S'1 S'2) -> (unionStateP S1 S2 S'3) ->(unionStateP S'3 S3 S'2).
Intros S1 S2 S3 S'1 S'2 S'3 H' H'0 H'1.
Apply unionStatePDef; Auto.
Apply unionStatePIncl with 1 := H'1; Auto.
Inversion H'0; Auto.
Apply inclStateTrans with S2 := S'1; Auto.
Inversion H'; Auto.
Inversion H'0; Auto.
Apply inclStateTrans with S2 := S'1; Auto.
Inversion H'; Auto.
Inversion H'0; Auto.
Intros S4 H'2 H'3.
Apply unionStatePIncl with 1 := H'0; Auto.
Apply inclStateTrans with S2 := S'3; Auto.
Inversion H'1; Auto.
Apply unionStatePIncl with 1 := H'; Auto.
Apply inclStateTrans with S2 := S'3; Auto.
Inversion H'1; Auto.
Qed.

Theorem addEqUnion:
  (S:State) (p, q:rZ)(unionStateP (cons (p, q) (nil ?)) S (addEq (p, q) S)).
Intros S p q.
Apply unionStatePDef; Auto.
Apply inclStateIn; Simpl; Auto.
Intros a b H'; Elim H'; Intros H'0; Inversion H'0; Auto.
Intros S4 H' H'0.
Apply inclStateAddEqInv; Auto.
Apply eqStateIncl with S1 := (cons (p, q) (nil rZ * rZ)); Auto with datatypes.
Qed.

Definition unionState := [S1, S2:State](app S1 S2).

Theorem unionStatePunionState:
  (S1, S2:State)(unionStateP S1 S2 (unionState S1 S2)).
Intros S1; Elim S1; Simpl; Auto.
Intros S2.
Apply unionStatePSym; Auto.
Apply unionStatePInclSelf; Auto.
Apply inclStateIn; Simpl; Auto.
Intros a b H'; Elim H'; Auto.
Intros p l H' S2; Case p; Intros a b.
Apply unionStatePAssoc2
     with S1 := (cons (a, b) (nil ?)) S2 := l S'1 := (unionState l S2); Auto.
Generalize addEqUnion; Unfold addEq; Auto.
Generalize addEqUnion; Unfold addEq; Auto.
Qed.

Theorem unionStateInclL: (S1, S2:State)(inclState S1 (unionState S1 S2)).
Intros S1 S2.
Specialize 2 unionStatePunionState with S1 := S1 S2 := S2; Intros H'0;
Inversion H'0; Auto.
Qed.
Hints Resolve unionStateInclL.

Theorem unionStateInclR: (S1, S2:State)(inclState S2 (unionState S1 S2)).
Intros S1 S2.
Specialize 2 unionStatePunionState with S1 := S1 S2 := S2; Intros H'0;
Inversion H'0; Auto.
Qed.
Hints Resolve unionStateInclR.

Theorem unionStateMin:
  (S1, S2, S3:State) (inclState S1 S3) -> (inclState S2 S3) ->
  (inclState (unionState S1 S2) S3).
Intros S1 S2 S3 H' H'0.
Specialize 2 unionStatePunionState with S1 := S1 S2 := S2; Intros H'1;
Inversion H'1; Auto.
Qed.
Hints Resolve unionStateMin.

Theorem unionStateSym:
  (S1, S2:State)(eqState (unionState S1 S2) (unionState S2 S1)).
Intros S1 S2; Red; Split; Auto.
Qed.
Hints Immediate unionStateSym.

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

Theorem unionStateAssoc:
  (S1, S2, S3:State)
  (eqState
     (unionState S1 (unionState S2 S3)) (unionState (unionState S1 S2) S3)).
Intros S1 S2 S3; Red; Split.
Apply unionStateMin; Auto.
Apply inclStateTrans with S2 := (unionState S1 S2); Auto.
Apply unionStateMin; Auto.
Apply inclStateTrans with S2 := (unionState S1 S2); Auto.
Apply unionStateMin; Auto.
Apply unionStateMin; Auto.
Apply inclStateTrans with S2 := (unionState S2 S3); Auto.
Apply inclStateTrans with S2 := (unionState S2 S3); Auto.
Qed.
Hints Resolve unionStateMin.

29/06/100, 12:53