state.v

(* Definition of states as the list of equations, i.e pairs of rZ *)
Require Import PolyList.
Require Export triplet.

Definition State := (list rZ * rZ).

Mutual Inductive eqStateRz: State -> rZ -> rZ ->Prop :=
     eqStateRzRef: (a:rZ) (S:State)(eqStateRz S a a)
    | eqStateRzIn: (a, b:rZ) (S:State) (In (a, b) S) ->(eqStateRz S a b)
    | eqStateRzInv:
        (a, b:rZ) (S:State) (eqStateRz S a b) ->
        (eqStateRz S (rZComp a) (rZComp b))
    | eqStateRzSym: (a, b:rZ) (S:State) (eqStateRz S a b) ->(eqStateRz S b a)
    | eqStateRzTrans:
        (a, b, c:rZ) (S:State) (eqStateRz S a b) -> (eqStateRz S b c) ->
        (eqStateRz S a c)
    | eqStateRzContr:
        (a, b, c:rZ) (S:State) (eqStateRz S a (rZComp a)) ->(eqStateRz S b c) .
Hints Resolve eqStateRzRef eqStateRzIn eqStateRzInv.

Theorem eqStateInvInv:
  (S:State) (p, q:rZ) (eqStateRz S (rZComp p) (rZComp q)) ->(eqStateRz S p q).
Intros S p0 q0 H'; Rewrite <- (rZCompInv p0); Rewrite <- (rZCompInv q0); Auto.
Qed.

Lemma eqStateContr:
  (S:State) (p, q, r, s:rZ) (eqStateRz S p q) -> (eqStateRz S p (rZComp q)) ->
  (eqStateRz S r s).
Intros S p q r s H' H'0.
Apply eqStateRzContr with a := q; Auto.
Apply eqStateRzTrans with b := p; Auto.
Apply eqStateRzSym; Auto.
Qed.

Lemma eqStateContrSimpl1:
  (S:State) (p, q:rZ) (eqStateRz S p (rZComp q)) ->(eqStateRz S (rZComp p) q).
Intros S p q H'.
Apply eqStateInvInv; Rewrite rZCompInv; Auto.
Qed.
Hints Resolve eqStateContrSimpl1.
Hints Immediate eqStateRzSym eqStateInvInv.

Definition addEq: rZ * rZ -> State ->State := [p:rZ * rZ] [S:State](cons p S).
Hints Unfold addEq.

Lemma eqStateaddEq1: (S:State) (p, q:rZ)(eqStateRz (addEq (p, q) S) p q).
Intros S p q.
Apply eqStateRzIn; Simpl; Auto.
Qed.

Lemma eqStateaddEq2:
  (S:State) (a, b, p, q:rZ) (eqStateRz S p q) ->(eqStateRz (addEq (a, b) S) p q).
Intros S a b p q H'; Generalize a b; Elim H'; Clear H' a b p q S; Auto.
Intros a b S H' a0 b0; Apply eqStateRzIn; Simpl; Auto.
Intros a b c S H' H'0 H'1 H'2 a0 b0.
Apply eqStateRzTrans with b := b; Auto.
Intros a b c S H' H'0 a0 b0.
Apply eqStateRzContr with a := a; Auto.
Qed.
Hints Resolve eqStateaddEq1 eqStateaddEq2.

(* We define the fact of being included *)

Definition inclState: State -> State ->Prop :=
   [S1, S2:State] (i, j:rZ) (eqStateRz S1 i j) ->(eqStateRz S2 i j).

Theorem inclStateRef: (S:State)(inclState S S).
Red; Auto.
Qed.
Hints Resolve inclStateRef.
(*Simpler version *)

Theorem inclStateIn:
  (S1, S2:State) ((a, b:rZ) (In (a, b) S1) ->(eqStateRz S2 a b)) ->
  (inclState S1 S2).
Intros S1 S2 H'; Red.
Intros i j H'0; Generalize H'; Elim H'0; Auto.
Intros a b L0 H'1 H'2 H'3; Apply eqStateRzSym; Auto.
Intros a b c0 L0 H'1 H'2 H'3 H'4 H'5; Apply eqStateRzTrans with b := b; Auto.
Intros a b c0 L0 H'1 H'2 H'3; Apply eqStateRzContr with a := a; Auto.
Qed.

(* We define the fact of being equal *)

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

Theorem eqStateRef: (S:State)(eqState S S).
Intros; Red; Split; Auto.
Qed.
Hints Resolve eqStateRef.

Theorem eqStateSym: (S1, S2:State) (eqState S1 S2) ->(eqState S2 S1).
Intros S1 S2 H'; Elim H'; Red; Auto.
Qed.
Hints Immediate eqStateSym.

Theorem eqStateInv:
  (S1, S2:State) (a, b:rZ) (eqState S1 S2) ->
  (iff (eqStateRz S1 a b) (eqStateRz S2 a b)).
Intros S1 S2 a b H'; Inversion H'; Red; Auto.
Qed.

Theorem addEqInclState: (S:State) (a, b:rZ)(inclState S (addEq (a, b) S)).
Intros S a b; Red; Auto.
Qed.
Hints Resolve addEqInclState.

Theorem inclStateTrans:
  (S1, S2, S3:State) (inclState S1 S2) -> (inclState S2 S3) ->(inclState S1 S3).
Intros S1 S2 S3 H' H'0; Red; Auto.
Qed.

Theorem eqStateIncl:
  (S1, S2:State) (p, q:rZ) (inclState S1 S2) -> (eqStateRz S1 p q) ->
  (eqStateRz S2 p q).
Intros S1 S2 p q H' H'0; Auto.
Qed.

Theorem eqStateEq:
  (S1, S2:State) (p, q:rZ) (eqState S1 S2) -> (eqStateRz S1 p q) ->
  (eqStateRz S2 p q).
Intros S1 S2 p q H' H'0.
Apply eqStateIncl with S1 := S1; Auto.
Inversion H'; Auto.
Qed.

Theorem addEqInclState2:
  (S:State) (a, b, c, d:rZ)(inclState S (addEq (a, b) (addEq (c, d) S))).
Intros S a b c d.
Apply inclStateTrans with S2 := (addEq (c, d) S); Auto.
Qed.
Hints Resolve addEqInclState2.

Theorem inclStateAddEqInv:
  (p, q:rZ) (S1, S2:State) (inclState S1 S2) -> (eqStateRz S2 p q) ->
  (inclState (addEq (p, q) S1) S2).
Intros p0 q0 S1 S2 H' H'0; Red; Auto.
Intros i j H'1; Generalize H'0 H'; Auto.
Cut (Ex [S3:State] S3=(addEq (p0, q0) S1)); Auto.
Intros H'2; Elim H'2; Intros S3 E; Rewrite <- E in H'1; Clear H'2; Auto.
Generalize E; Elim H'1; Auto.
Intros a b L H'2 H'3; Rewrite H'3 in H'2; Simpl in H'2; Case H'2; Auto.
Intros H'4; Inversion H'4; Auto.
Intros a b S H'2 H'3 H'4 H'5 H'6; Auto.
Apply eqStateRzSym; Auto.
Intros a b c S H'2 H'3 H'4 H'5 H'6 H'7 H'8.
Apply eqStateRzTrans with b := b; Auto.
Intros a b c S H'2 H'3 H'4 H'5 H'6.
Apply eqStateRzContr with a := a; Auto.
Exists (addEq (p0, q0) S1); Auto.
Qed.
Hints Resolve inclStateAddEqInv.

Theorem inclStateAddEq:
  (S1, S2:State) (a, b:rZ) (inclState S1 S2) ->
  (inclState (addEq (a, b) S1) (addEq (a, b) S2)).
Intros S1 S2 a b H'.
Apply inclStateAddEqInv; Simpl.
Apply inclStateTrans with S2 := S2; Auto.
Apply eqStateRzIn; Auto.
Simpl.
Auto.
Qed.
Hints Resolve inclStateAddEq.

Theorem eqStateAddEq:
  (S1, S2:State) (a, b:rZ) (eqState S1 S2) ->
  (eqState (addEq (a, b) S1) (addEq (a, b) S2)).
Intros S1 S2 a b H'; Inversion H'; Red; Auto.
Qed.
Hints Resolve eqStateAddEq.

Theorem inclStateEqStateComp:
  (S1, S2, S3, S4:State)
  (eqState S1 S2) -> (eqState S3 S4) -> (inclState S1 S3) ->(inclState S2 S4).
Intros S1 S2 S3 S4 H' H'0 H'1; Inversion H'; Inversion H'0.
Apply inclStateTrans with S2 := S3; Auto.
Apply inclStateTrans with S2 := S1; Auto.
Qed.

Theorem eqStateTrans:
  (S1, S2, S3:State) (eqState S1 S2) -> (eqState S2 S3) ->(eqState S1 S3).
Intros S1 S2 S3 H' H'0; Inversion H'; Inversion H'0.
Red; Split; Apply inclStateTrans with S2 := S2; Auto.
Qed.

Theorem addEqComp:
  (a, b, a', b':rZ) (S:State) (eqStateRz S a a') -> (eqStateRz S b b') ->
  (eqState (addEq (a, b) S) (addEq (a', b') S)).
Intros a b a' b' S H' H'0.
Red; Split; Apply inclStateIn; Simpl;
(Intros a0 b0 H'1; Elim H'1; Clear H'1; Intros H'2; [Inversion H'2 | Idtac]);
Auto; Rewrite <- H1; Rewrite <- H0.
Apply eqStateRzTrans with b := a'; Auto.
Apply eqStateRzTrans with b := b'; Auto.
Apply eqStateRzTrans with b := a; Auto.
Apply eqStateRzTrans with b := b; Auto.
Qed.
Hints Resolve addEqComp.

(* A valuation function realizes a state if all its basic equations are true *)

Definition realizeState: (rNat ->bool) -> State ->Prop :=
   [f:rNat ->bool] [S:State] (i, j:rZ) (In (i, j) S) ->(rZEval f i)=(rZEval f j).

Theorem realizeStateNil: (f:rNat ->bool)(realizeState f (nil ?)).
Intros f; Red; Simpl.
Intros i j H'; Elim H'.
Qed.
Hints Resolve realizeStateNil.

Theorem rZEvalCompInv:
  (a:rZ) (f:rNat ->bool)(rZEval f (rZComp a))=(negb (rZEval f a)).
Intros a f; Case a; Simpl; Auto.
Intros r; Case (f r); Auto.
Qed.
(* If a valuation function realizes a state then all its equations are true *)

Theorem realizeStateInv:
  (f:rNat ->bool) (S:State) (realizeState f S) ->
  (i, j:rZ) (eqStateRz S i j) ->(rZEval f i)=(rZEval f j).
Intros f S H' i j H'0; Generalize H'; Elim H'0; Auto.
Intros a b S0 H'1 H'2 H'3.
Rewrite rZEvalCompInv; Auto; Rewrite rZEvalCompInv; Auto.
Rewrite H'2; Auto.
Intros a b S0 H'1 H'2 H'3.
Rewrite H'2; Auto.
Intros a b c S0 H'1 H'2 H'3 H'4 H'5.
Rewrite H'2; Auto.
Intros a b c S0 H'1 H'2 H'3.
Absurd (rZEval f a)=(rZEval f (rZComp a)); Auto.
Rewrite rZEvalCompInv; Case (rZEval f a); Simpl; Red; Intros; Discriminate.
Qed.

Theorem realizeStateInvComp:
  (f:rNat ->bool) (S:State) (realizeState f S) ->
  (i, j:rZ) (eqStateRz S i (rZComp j)) ->(rZEval f i)=(negb (rZEval f j)).
Intros f S H' i j H'0.
Rewrite <- rZEvalCompInv.
Apply realizeStateInv with S := S; Auto.
Qed.

Theorem realizeStateAddEq:
  (f:rNat ->bool) (S:State) (realizeState f S) ->
  (i, j:rZ) (rZEval f i)=(rZEval f j) ->(realizeState f (addEq (i, j) S)).
Intros f S H' i j H'0; Red; Simpl; Auto.
Intros i0 j0 H'1; Elim H'1; Intros H'2; Clear H'1; [Inversion H'2 | Idtac]; Auto.
Rewrite <- H1; Auto.
Rewrite <- H0; Auto.
Qed.
Hints Resolve realizeStateAddEq.

Theorem realizeStateIncl:
  (f:rNat ->bool) (S1, S2:State) (realizeState f S1) -> (inclState S2 S1) ->
  (realizeState f S2).
Intros f S1 S2 H' H'0; Red; Auto.
Intros i j H'1.
Apply realizeStateInv with S := S1; Auto.
Qed.

Theorem realizeStateInvAddEq:
  (f:rNat ->bool) (S:State) (i, j:rZ) (realizeState f (addEq (i, j) S)) ->
  (rZEval f i)=(rZEval f j).
Intros f S i j H'.
Apply realizeStateInv with S := (addEq (i, j) S); Auto.
Qed.

Theorem realizeStateInvAddEq2:
  (f:rNat ->bool)
  (S:State) (i, j, k, l:rZ) (realizeState f (addEq (i, j) (addEq (k, l) S))) ->
  (rZEval f k)=(rZEval f l) /\ (rZEval f i)=(rZEval f j).
Intros f S i j k l H'; Split.
Apply realizeStateInvAddEq with S := S; Auto.
Apply realizeStateIncl with S1 := (addEq (i, j) (addEq (k, l) S)); Auto.
Apply realizeStateInvAddEq with S := (addEq (k, l) S); Auto.
Qed.

(* What it means for a state to be contradictory *)

Definition contradictory: State ->Prop :=
   [S:State](Ex [a:rZ] (eqStateRz S a (rZComp a))).
(* Of course if a state is contradictory it can't be realized *)

Theorem contradictoryNotRealize:
  (S:State) (contradictory S) ->(f:rNat ->bool)~ (realizeState f S).
Intros S H' f; Red; Intros H'0; Inversion H'.
Absurd (rZEval f x)=(rZEval f (rZComp x)).
Rewrite rZEvalCompInv; Case (rZEval f x); Auto; Red; Intros; Discriminate.
Apply realizeStateInv with S := S; Auto.
Qed.
Hints Resolve contradictoryNotRealize.

Theorem ContrIncl:
  (S:State)(inclState S (cons ((rZPlus zero), (rZMinus zero)) (nil ?))).
Intros S; Red; Auto.
Intros i j H'.
Apply eqStateRzContr with a := (rZPlus zero); Auto with datatypes.
Qed.
Hints Resolve ContrIncl.

29/06/100, 12:53