stateDec.v

Require Import PolyList.
Require Export state.

Mutual Inductive eqConstrState: State -> rZ -> rZ ->Prop :=
     eqConstrStateNil: (a:rZ)(eqConstrState (nil ?) a a)
    | eqConstrStateTail:
        (a, b:rZ) (p:rZ * rZ) (S:State) (eqConstrState S a b) ->
        (eqConstrState (cons p S) a b)
    | eqConstrStateComp1:
        (a, b, c, d:rZ)
        (S:State) (eqConstrState S a b) -> (eqConstrState S c d) ->
        (eqConstrState (cons (b, c) S) a d)
    | eqConstrStateComp2:
        (a, b, c, d:rZ)
        (S:State) (eqConstrState S a c) -> (eqConstrState S b d) ->
        (eqConstrState (cons (b, c) S) a d)
    | eqConstrStateComp3:
        (a, b, c, d:rZ)
        (S:State)
        (eqConstrState S a (rZComp b)) -> (eqConstrState S (rZComp c) d) ->
        (eqConstrState (cons (b, c) S) a d)
    | eqConstrStateComp4:
        (a, b, c, d:rZ)
        (S:State)
        (eqConstrState S a (rZComp c)) -> (eqConstrState S (rZComp b) d) ->
        (eqConstrState (cons (b, c) S) a d)
    | eqConstrStateContr:
        (a, b, c, d:rZ) (S:State) (eqConstrState S a (rZComp b)) ->
        (eqConstrState (cons (a, b) S) c d) .
Hints Resolve
eqConstrStateNil eqConstrStateTail eqConstrStateComp1 eqConstrStateComp2
eqConstrStateComp3 eqConstrStateComp4 eqConstrStateContr.

Theorem eqConstrStateRef: (a:rZ) (S:State)(eqConstrState S a a).
Intros a L; Elim L; Auto.
Qed.
Hints Resolve eqConstrStateRef.

Theorem eqConstrStateIn:
  (a, b:rZ) (S:State) (In (a, b) S) ->(eqConstrState S a b).
Intros a b L; Elim L; Simpl; Auto.
Intros H'; Elim H'; Auto.
Intros a0 l H' H'0; Elim H'0;
[Intros H'1; Rewrite H'1; Clear H'0 | Intros H'1; Clear H'0]; Auto.
Qed.
Hints Resolve eqConstrStateIn.

Theorem eqConstrStateInv:
  (a, b:rZ) (S:State) (eqConstrState S a b) ->
  (eqConstrState S (rZComp a) (rZComp b)).
Intros a b S H'; Elim H'; Auto.
Intros a0 b0 S0; Repeat Rewrite rZCompInv; Auto.
Intros a0 b0 S0; Repeat Rewrite rZCompInv; Auto.
Qed.
Hints Resolve eqConstrStateInv.

Theorem eqConstrStateSym:
  (a, b:rZ) (S:State) (eqConstrState S a b) ->(eqConstrState S b a).
Intros a b S H'; Elim H'; Auto.
Qed.
Hints Immediate eqConstrStateSym.

Theorem eqConstrStateSimpl:
  (a, b:rZ) (S:State) (eqConstrState S (rZComp a) b) ->
  (eqConstrState S a (rZComp b)).
Intros a b S H'; Auto.
Rewrite <- (rZCompInv a); Auto.
Qed.
Hints Resolve eqConstrStateSimpl.

Theorem eqConstrStateTransConstr:
  (S:State)
  ((a, b, c:rZ) (eqConstrState S a (rZComp a)) ->(eqConstrState S b c)) /\
  ((a, b, c:rZ) (eqConstrState S a b) -> (eqConstrState S b c) ->
   (eqConstrState S a c)).
Intros L; Elim L; Auto.
Split; Intros a b c H'; Inversion H'; Auto.
Generalize H1; Case a; Intros; Discriminate.
Intros p; Case p.
Intros e f l H'; Elim H'; Intros H'0 H'1; Clear H'.
Split;
[Intros a b c H'; Inversion H'; Generalize (H'0 a);
   Generalize [b, c:rZ](H'1 b a c); Generalize [b, c:rZ](H'1 b (rZComp a) c);
   Intros Hc0 Hc1 Hc2; Auto 4 | Idtac].
Apply eqConstrStateContr; Auto.
Apply Hc1; Auto.
Rewrite <- (rZCompInv e); Rewrite <- (rZCompInv a); Apply eqConstrStateInv; Auto.
Intros a b c H'; Inversion H'; Intros H'2; Inversion H'2; Generalize (H'0 f);
Generalize [a, c:rZ](H'1 a b c); Intros Hc0 Hc1; Auto 4.
Apply eqConstrStateTail.
Apply H'1 with b := e; Auto.
Apply eqConstrStateTail.
Apply H'1 with b := f; Auto.
Apply eqConstrStateTail; Auto.
Apply H'0 with a := e; Auto.
Apply eqConstrStateTail; Auto.
Apply H'1 with b := (rZComp e); Auto.
Apply eqConstrStateTail; Auto.
Apply H'0 with a := e; Auto.
Apply eqConstrStateTail; Auto.
Apply H'1 with b := (rZComp f); Auto.
Qed.

Theorem eqConstrStateTrans:
  (S:State) (a, b, c:rZ) (eqConstrState S a b) -> (eqConstrState S b c) ->
  (eqConstrState S a c).
Intros S a b c H' H'0.
Elim (eqConstrStateTransConstr S); Intros H'2 H'3; LApply (H'3 a b c);
[Intros H'7; LApply H'7; [Intros H'8; Apply H'8; Clear H'7 | Clear H'7] | Idtac];
Auto.
Qed.

Theorem eqConstrStateContrGen:
  (S:State) (a, b, c:rZ) (eqConstrState S a (rZComp a)) ->(eqConstrState S b c).
Intros S a b c H'.
Elim (eqConstrStateTransConstr S); Intros H'1 H'2; LApply (H'1 a b c);
[Intros H'6; Apply H'6 | Idtac]; Auto.
Qed.

Theorem eqStateRzPImpeqConstrState:
  (S:State) (a, b:rZ) (eqStateRz S a b) ->(eqConstrState S a b).
Intros S a b H'; Elim H'; Auto.
Intros a0 b0 c S0 H'0 H'1 H'2 H'3.
Apply eqConstrStateTrans with b := b0; Auto.
Intros a0 b0 c S0 H'0 H'1.
Apply eqConstrStateContrGen with a := a0; Auto.
Qed.

Theorem eqStateRzTail:
  (a, b:rZ) (S:State) (p:rZ * rZ) (eqStateRz S a b) ->(eqStateRz (cons p S) a b).
Intros a b S p H'; Elim H'; Auto.
Intros a0 b0 S0 H'0.
Apply eqStateRzIn; Simpl; Auto.
Intros a0 b0 c S0 H'0 H'1 H'2 H'3.
Apply eqStateRzTrans with b := b0; Auto.
Intros a0 b0 c S0 H'0 H'1.
Apply eqStateRzContr with a := a0; Auto.
Qed.
Hints Resolve eqStateRzTail.

Theorem eqConstrStateCons: (S:State) (a, b:rZ)(eqStateRz (cons (a, b) S) a b).
Auto with datatypes.
Qed.
Hints Resolve eqConstrStateCons.

Theorem eqConstrStateImpeqStateRz:
  (S:State) (a, b:rZ) (eqConstrState S a b) ->(eqStateRz S a b).
Intros S a b H'; Elim H'; Auto.
Intros a0 b0 c d S0 H'0 H'1 H'2 H'3.
Apply eqStateRzTrans with b := b0; Auto.
Apply eqStateRzTrans with b := c; Auto.
Intros a0 b0 c d S0 H'0 H'1 H'2 H'3.
Apply eqStateRzTrans with b := c; Auto.
Apply eqStateRzTrans with b := b0; Auto.
Intros a0 b0 c d S0 H'0 H'1 H'2 H'3.
Apply eqStateRzTrans with b := (rZComp b0); Auto.
Apply eqStateRzTrans with b := (rZComp c); Auto.
Intros a0 b0 c d S0 H'0 H'1 H'2 H'3.
Apply eqStateRzTrans with b := (rZComp c); Auto.
Apply eqStateRzTrans with b := (rZComp b0); Auto.
Intros a0 b0 c d S0 H'0 H'1.
Apply eqStateRzContr with a := b0; Auto.
Apply eqStateRzTrans with b := a0; Auto.
Qed.
Hints Immediate eqStateRzPImpeqConstrState eqConstrStateImpeqStateRz.

Definition eqConstrStateDec:
  (S:State) (a, b:rZ){(eqConstrState S a b)}+{~ (eqConstrState S a b)}.
Intros L; Elim L; Simpl; Auto.
Intros a b; Case (rZDec a b); Intros Eqab.
Rewrite <- Eqab; Auto.
Right; Red; Intros H'.
Apply Eqab; Inversion H'; Auto.
Intros p l H' a b.
Case (H' a b); Intros EqabL; Auto.
Case p.
Intros c d.
Case (H' a (rZComp a)); Intros Eqama; Auto.
Left; Apply eqConstrStateContrGen with a := a; Auto.
Case (H' c (rZComp d)); Intros Eqcmd; Auto.
Case (H' c d); Intros Eqcd; Auto.
Case (H' a b); Intros Eqab; Auto.
Right; Red; Intros H'0; Apply Eqab; Auto.
Apply eqStateRzPImpeqConstrState.
Apply eqStateIncl with S1 := (addEq (c, d) l); Auto.
Case (H' a c); Intros Eqac; Auto.
Case (H' d b); Intros EqdbL; Auto.
Right; Red; Intros H'0; Inversion H'0; Auto.
Case Eqcd; Apply eqConstrStateTrans with b := a; Auto.
Case Eqama; Apply eqConstrStateTrans with b := c; Auto.
Case Eqcmd; Apply eqConstrStateTrans with b := a; Auto.
Case (H' a d); Intros Eqad; Auto.
Case (H' c b); Intros Eqcb; Auto.
Right; Red; Intros H'0; Inversion H'0; Auto.
Case Eqcmd; Apply eqConstrStateTrans with b := (rZComp a); Auto.
Case Eqama; Apply eqConstrStateTrans with b := (rZComp d); Auto.
Case (H' a (rZComp c)); Intros Eqamc; Auto.
Case (H' (rZComp d) b); Intros Eqmdb; Auto.
Right; Red; Intros H'0; Inversion H'0; Auto.
Case Eqcd; Apply eqConstrStateTrans with b := (rZComp a); Auto.
Apply eqConstrStateSym; Auto.
Case (H' a (rZComp d)); Intros Eqamd; Auto.
Case (H' (rZComp c) b); Intros Eqmcb; Auto.
Right; Red; Intros H'0; Inversion H'0; Auto.
Right; Red; Intros H'0; Inversion H'0; Auto.
Defined.

Definition eqStateRzDec:
  (S:State) (a, b:rZ){(eqStateRz S a b)}+{~ (eqStateRz S a b)}.
Intros S a b; Case (eqConstrStateDec S a b); Auto.
Defined.

Definition eqStateRzContrDec:
  (S:State){(a, b:rZ)(eqStateRz S a b)}+{~ ((a, b:rZ)(eqStateRz S a b))}.
Intros S; Case S; Auto.
Right; Red; Intros H'; Auto.
Cut (eqConstrState (nil ?) (rZPlus zero) (rZMinus zero)); Auto.
Intros H'0; Inversion H'0; Auto.
Intros p S'; Case p; Intros a b.
Case (eqStateRzDec (cons (a, b) S') a (rZComp a)); Auto.
Intros H'; Left; Intros a0 b0.
Apply eqStateRzContr with a := a; Auto.
Qed.

Theorem inclStateDec: (S1, S2:State){(inclState S1 S2)}+{~ (inclState S1 S2)}.
Intros S1; Elim S1; Auto.
Intros S2; Left; Red; Auto with datatypes; Intros i j H'1; Elim S2; Auto.
Intros a; Case a; Auto.
Intros a' b' l H' S2.
Elim (H' S2); Intros H'1; Auto.
Case (eqStateRzDec S2 a' b'); Intros EqS2; Auto.
Left; Change (inclState (addEq (a', b') l) S2); Auto.
Right; Red; Intros H'0; Case H'1; Auto.
Apply inclStateTrans with S2 := (addEq (a', b') l); Auto.
Qed.

Theorem eqStateDec: (S1, S2:State){(eqState S1 S2)}+{~ (eqState S1 S2)}.
Intros S1 S2.
Case (inclStateDec S1 S2); Intros inclS1S2; Auto.
Case (inclStateDec S2 S1); Intros inclS2S1; Auto.
Left; Red; Auto.
Right; Red; Intros H'; Red in H'; Case inclS2S1; Auto.
Elim H'; Intros H'0 H'1; Auto.
Right; Red; Intros H'; Case inclS1S2; Auto.
Red in H'; Elim H'; Auto.
Qed.

Theorem inclStateDecBis:
  (S1, S2:State)
  {(inclState S1 S2)}+
  {(Ex [a:rZ] (Ex [b:rZ] (eqStateRz S1 a b) /\ ~ (eqStateRz S2 a b)))}.
Intros S1; Elim S1; Auto.
Intros S2; Left; Auto.
Red; Intros i j H'1; Elim S2; Auto.
Intros a; Case a; Auto.
Intros a' b' l H' S2.
Elim (H' S2); Intros H'1; Auto.
Case (eqStateRzDec S2 a' b'); Intros EqS2; Auto.
Left; Change (inclState (addEq (a', b') l) S2); Auto.
Right; Exists a'; Exists b'; Split; Auto.
Right.
Elim H'1; Intros a0 E; Elim E; Intros b E0; Elim E0; Intros H'0 H'2;
Try Exact H'0; Clear E0 E H'1.
Exists a0; Exists b; Split; Auto.
Qed.

29/06/100, 12:53