stateExtra.v

Require Export stateDec.

Definition fnAux :=
   [S:State] [f:rNat ->bool] [i:rZ] [n:rNat]
      Cases (eqStateRzDec S (rZPlus n) i) of
          (left _)=> (negb (f n))
         | (right _) => Cases (eqStateRzDec S (rZMinus n) i) of
                        (left _) => (negb (f n))
                       | (right _) => (f n)
                    end
      end.

Lemma RealizableAux1:
  (S:State) (f:rNat ->bool) (i, j:rZ) (eqStateRz S j i) ->
  (rZEval (fnAux S f i) j)=(negb (rZEval f j)).
Destruct j; Intros n Eq; Unfold fnAux; Simpl.
Case (eqStateRzDec S (rZPlus n) i); Auto.
Intros Abs; Absurd (eqStateRz S (rZPlus n) i); Auto.
Case (eqStateRzDec S (rZPlus n) i); Auto.
Case (eqStateRzDec S (rZMinus n) i); Auto.
Intros Abs; Absurd (eqStateRz S (rZMinus n) i); Auto.
Qed.

Lemma RealizableAux2:
  (S:State)
  (f:rNat ->bool)
  (i, j:rZ) ~ (eqStateRz S j i) -> ~ (eqStateRz S (rZComp j) i) ->
  (rZEval (fnAux S f i) j)=(rZEval f j).
Destruct j; Intros n Eq2 Eq2; Unfold fnAux; Simpl;
Case (eqStateRzDec S (rZPlus n) i); Case (eqStateRzDec S (rZMinus n) i); Auto;
Intros;
(Absurd (eqStateRz S (rZPlus n) i); Auto; Fail)
  Orelse Absurd (eqStateRz S (rZMinus n) i); Auto.
Qed.

Lemma negbElim: (b, b':bool) (negb b)=(negb b') ->b=b'.
Destruct b; Destruct b'; Simpl; Auto.
Qed.
Hints Immediate negbElim.

Lemma RealizableAux3:
  (S:State) (f:rNat ->bool) (i:rZ) (realizeState f S) ->
  (realizeState (fnAux S f i) S).
Unfold realizeState; Intros S f i H j k H1.
Case (eqStateRzDec S k i); Intros H2.
Rewrite (RealizableAux1 S f i k); Auto; Rewrite (RealizableAux1 S f i j);
[Rewrite (H j k H1) | Apply eqStateRzTrans with b := k]; Auto.
Case (eqStateRzDec S (rZComp k) i); Intros H3.
Apply negbElim; Rewrite <- (rZEvalCompInv j (fnAux S f i));
Rewrite <- (rZEvalCompInv k (fnAux S f i)).
Rewrite (RealizableAux1 S f i (rZComp k)); Auto;
Rewrite (RealizableAux1 S f i (rZComp j)); Auto;
[Rewrite (rZEvalCompInv j f); Rewrite (rZEvalCompInv k f); Rewrite (H j k H1) |
   Apply eqStateRzTrans with b := (rZComp k)]; Auto.
Rewrite (RealizableAux2 S f i k); Auto; Rewrite (RealizableAux2 S f i j); Auto.
Red; Intro; Absurd (eqStateRz S k i); Auto; Apply eqStateRzTrans with b := j;
Auto; Apply eqStateRzSym; Auto.
Red; Intro; Absurd (eqStateRz S (rZComp k) i); Auto;
Apply eqStateRzTrans with b := (rZComp j); Auto; Apply eqStateRzSym; Auto.
Qed.

Lemma EqboolDec: (b, b':bool){b=b'}+{(negb b)=b'}.
Destruct b; Destruct b'; Simpl; Auto.
Qed.

Theorem Realizable:
  (S:State) ~ (contradictory S) ->(Ex [f:rNat ->bool] (realizeState f S)).
Induction S.
Intros Abs; Exists [n:rNat]true; Auto.
Intros p; Case p; Intros i j l HR Abs.
Cut ~ (contradictory l).
Intros Abs'; Elim (HR Abs'); Intros f Hf.
Case (eqStateRzDec l j i); Intros Lij.
Exists f; Apply (realizeStateIncl f l (cons <rZ, rZ> (i, j) l)); Auto;
Apply (inclStateAddEqInv i j l l); Auto.
Case (EqboolDec (rZEval f i) (rZEval f j)); Intros Fij.
Exists f; LApply (realizeStateAddEq f l Hf i j); Auto.
Exists (fnAux l f i);
LApply (realizeStateAddEq (fnAux l f i) l (RealizableAux3 l f i Hf) i j); Auto.
Rewrite (RealizableAux1 l f i i); Auto; Rewrite Fij.
Rewrite (RealizableAux2 l f i j); Auto.
Red; Intros Abs1; Absurd (contradictory (cons <rZ, rZ> (i, j) l)); Auto.
Unfold contradictory; Exists i; Auto; Apply eqStateRzTrans with b := (rZComp j);
Auto.
Red; Unfold contradictory; Intros Abs1; Elim Abs1; Intros a Pa.
Absurd (contradictory (cons <rZ, rZ> (i, j) l)); Auto; Unfold contradictory;
Exists a; Auto.
Qed.

Lemma RealizeNegb:
  (S:State) (f:rNat ->bool) (realizeState f S) ->
  (realizeState [n:rNat](negb (f n)) S).
Unfold realizeState; Intros S f Hf i j Hij; Generalize (Hf i j Hij); Case i;
Case j; Simpl; Intros n m Hnm; Rewrite Hnm; Auto.
Qed.
Hints Resolve RealizeNegb.

Theorem Realizable2:
  (S:State) ~ (contradictory S) ->
  (Ex [f:rNat ->bool] (realizeState f S) /\ (f zero)=true).
Intros S HS; Elim (Realizable S HS); Intros f Hf.
Case (EqboolDec (f zero) true); Intros H.
Exists f; Auto.
Exists [n:rNat](negb (f n)); Split; Auto with bool.
Qed.

Theorem RealizableCstr:
  (S:State) (i, j:rZ) ~ (eqStateRz S i j) ->
  (Ex [f:rNat ->bool] (realizeState f S) /\ (negb (rZEval f i))=(rZEval f j)).
Intros S i j Hij; Elim (Realizable S); [Intros f Pf | Idtac].
Case (eqStateRzDec S (rZComp j) i); Intros Hij'.
Exists f; Split; Auto; Rewrite (realizeStateInvComp f S Pf j i); Auto;
Rewrite <- (rZCompInv j); Auto.
Case (EqboolDec (rZEval f i) (rZEval f j)); Intros Fij.
Exists (fnAux S f i); Split; Auto;
[Apply RealizableAux3 |
   Rewrite (RealizableAux1 S f i i); Auto; Rewrite (RealizableAux2 S f i j)];
Auto.
Rewrite Fij; Case (rZEval f j); Simpl; Auto.
Exists f; Split; Auto.
Red; Intros Contr; Elim Contr; Intros a Pa; Absurd (eqStateRz S i j); Auto;
Apply eqStateRzContr with a := a; Auto.
Qed.

Theorem realizeStateInclInv:
  (S1, S2:State)
  ((f:rNat ->bool) (f zero)=true -> (realizeState f S2) ->(realizeState f S1)) ->
  (inclState S1 S2).
Intros S1 S2 H; Apply inclStateIn; Intros i j Pij1.
Case (eqStateRzDec S2 j i); Intros Pij2; Auto.
Elim (RealizableCstr S2 i j); Auto; Intros f Pf; Elim Pf; Intros Pf1 Pf2.
Case (EqboolDec (f zero) true); Intros P0.
Generalize (H f P0 Pf1); Unfold realizeState; Intros H1.
Rewrite (H1 i j) in Pf2; Auto.
Generalize Pf2; Case (rZEval f j); Simpl; Intros Abs; Inversion Abs.
Generalize (H [n:rNat](negb (f n)) P0 (RealizeNegb S2 f Pf1));
Unfold realizeState; Intros H1.
Generalize (H1 i j Pij1) Pf2; Case i; Case j; Simpl; Intros n m Abs1;
Rewrite Abs1; Case (f n); Simpl; Intros Abs2; Inversion Abs2.
Qed.

29/06/100, 12:53