ltState.v

Require Import state.
Require Import Arith.
Require Import stateDec.
Require Import Inverse_Image.
Require Import Compare.
Require Import Relation_Definitions.
Section lt.
Variable L:(list rNat).

Definition oneState :=
   [S:State] [a, b:rZ]
      Cases (eqStateRzDec S a b) of
          (left _) => O
         | (right _) => (1)
      end.

Theorem oneStateLe:
  (a, b:rZ) (S1, S2:State) (inclState S1 S2) ->
  (le (oneState S2 a b) (oneState S1 a b)).
Intros a b S1 S2 H'; Unfold oneState.
Case (eqStateRzDec S1 a b); Case (eqStateRzDec S2 a b); Auto.
Intros H'0 H'1; Case H'0; Auto.
Qed.
Hints Resolve oneStateLe.

Theorem oneStateLt:
  (a, b:rZ)
  (S1, S2:State)
  (inclState S1 S2) -> (eqStateRz S2 a b) -> ~ (eqStateRz S1 a b) ->
  (lt (oneState S2 a b) (oneState S1 a b)).
Intros a b S1 S2 H'; Unfold oneState.
Case (eqStateRzDec S1 a b); Case (eqStateRzDec S2 a b); Auto.
Intros H'0 H'1 H'2 H'3; Case H'3; Auto.
Intros H'0 H'1 H'2 H'3; Case H'0; Auto.
Intros H'0 H'1 H'2 H'3; Case H'0; Auto.
Qed.
Hints Resolve oneStateLt.

Definition oneStateAll :=
   [S:State] [a, b:rNat]
   (plus
      (plus
         (oneState S (rZPlus a) (rZPlus b)) (oneState S (rZPlus a) (rZMinus b)))
      (plus
         (oneState S (rZMinus a) (rZPlus b))
         (oneState S (rZMinus a) (rZMinus b)))).

Theorem lePlusComp:
  (a, b, c, d:nat) (le a b) -> (le c d) ->(le (plus a c) (plus b d)).
Intros a b c d H' H'0.
Apply le_trans with m := (plus a d); Auto.
Apply le_reg_l; Auto.
Apply le_reg_r; Auto.
Qed.
Hints Resolve lePlusComp.

Theorem oneStateAllLe:
  (a, b:rNat) (S1, S2:State) (inclState S1 S2) ->
  (le (oneStateAll S2 a b) (oneStateAll S1 a b)).
Intros a b S1 S2 H'; Unfold oneStateAll; Generalize oneStateLe; Intros H'; Auto.
Qed.
Hints Resolve oneStateAllLe.

Theorem ltlePlusCompL:
  (a, b, c, d:nat) (lt a b) -> (le c d) ->(lt (plus a c) (plus b d)).
Intros a b c d H' H'0; Apply lt_le_trans with m := (plus b c); Auto.
Apply lt_reg_r; Auto.
Qed.
Hints Resolve ltlePlusCompL.

Theorem ltlePlusCompR:
  (a, b, c, d:nat) (le a b) -> (lt c d) ->(lt (plus a c) (plus b d)).
Intros a b c d H' H'0; Apply le_lt_trans with m := (plus b c); Auto.
Apply lt_reg_l; Auto.
Qed.
Hints Resolve ltlePlusCompR.

Theorem oneStateAllLt:
  (a, b:rZ)
  (S1, S2:State)
  (inclState S1 S2) -> (eqStateRz S2 a b) -> ~ (eqStateRz S1 a b) ->
  (lt (oneStateAll S2 (valRz a) (valRz b)) (oneStateAll S1 (valRz a) (valRz b))).
Intros a b S1 S2 H'; Unfold oneStateAll.
Case a; Case b; Simpl; Auto.
Qed.
Hints Resolve oneStateAllLt.

Fixpoint Nrel[S1:State; a:rNat; L1:(list rNat)]: nat :=
   Cases L1 of
       nil => O
      | (cons b L2) => (plus (oneStateAll S1 a b) (Nrel S1 a L2))
   end.

Theorem NrelLe:
  (L1:(list rNat)) (a:rNat) (S1, S2:State) (inclState S1 S2) ->
  (le (Nrel S2 a L1) (Nrel S1 a L1)).
Intros L1 a S1 S2 H'; Elim L1; Simpl; Auto.
Qed.
Hints Resolve NrelLe.

Theorem NrelLt:
  (L1:(list rNat))
  (a:rNat)
  (b:rZ)
  (S1, S2:State)
  (inclState S1 S2) ->
  (eqStateRz S2 (rZPlus a) b) ->
  ~ (eqStateRz S1 (rZPlus a) b) -> (In (valRz b) L1) ->
  (lt (Nrel S2 a L1) (Nrel S1 a L1)).
Intros L1; Elim L1; Simpl; Auto.
Intros a b S1 S2 H' H'0 H'1 H'2; Elim H'2; Auto.
Intros a l H' a0 b S1 S2 H'0 H'1 H'2 H'3; Elim H'3; Clear H'3; Intros H'4; Auto.
Rewrite H'4; Auto.
Apply ltlePlusCompL; Auto.
Change (lt
          (oneStateAll S2 (valRz (rZPlus a0)) (valRz b))
          (oneStateAll S1 (valRz (rZPlus a0)) (valRz b))); Auto.
Apply ltlePlusCompR; Auto.
Apply H' with b := b; Auto.
Qed.
Hints Resolve NrelLt.

Fixpoint Ncount[S1:State; L2:(list rNat); L1:(list rNat)]: nat :=
   Cases L1 of
       nil => O
      | (cons a L3) => (plus (Nrel S1 a L2) (Ncount S1 L2 L3))
   end.

Theorem NcountLe:
  (L1, L2:(list rNat)) (S1, S2:State) (inclState S2 S1) ->
  (le (Ncount S1 L2 L1) (Ncount S2 L2 L1)).
Intros L1; Elim L1; Simpl; Auto.
Qed.
Hints Resolve NcountLe.

Theorem NcountLt:
  (L1, L2:(list rNat)) (a:rNat) (b:rZ) (In a L1) -> (In (valRz b) L2) ->
  (S1, S2:State)
  (inclState S1 S2) ->
  (eqStateRz S2 (rZPlus a) b) -> ~ (eqStateRz S1 (rZPlus a) b) ->
  (lt (Ncount S2 L2 L1) (Ncount S1 L2 L1)).
Intros L1; Elim L1; Simpl; Auto.
Intros L2 a b H'; Elim H'; Auto.
Intros a l H' L2 a0 b H'0; Elim H'0; Clear H'0; Intros H'1;
[Rewrite <- H'1 | Idtac]; Auto.
Intros H'0 S1 S2 H'2 H'3 H'4.
Apply ltlePlusCompL; Auto.
Apply NrelLt with b := b; Auto.
Intros H'0 S1 S2 H'2 H'3 H'4.
Apply ltlePlusCompR; Auto.
Apply H' with a := a0 b := b; Auto.
Qed.

Definition valState := [S:State](Ncount S L L).

Theorem vallStateLe:
  (S1, S2:State) (inclState S1 S2) ->(le (valState S2) (valState S1)).
Unfold valState; Auto.
Qed.
Hints Resolve vallStateLe.

Theorem vallStateLt:
  (a, b:rZ) (In (valRz a) L) -> (In (valRz b) L) ->
  (S1, S2:State)
  (inclState S1 S2) -> (eqStateRz S2 a b) -> ~ (eqStateRz S1 a b) ->
  (lt (valState S2) (valState S1)).
Intros a; Case a; Auto.
Intros a' b H' H'0 S1 S2 H'1 H'2 H'3; Unfold valState.
Apply NcountLt with a := a' b := b; Auto.
Intros a' b H' H'0 S1 S2 H'1 H'2 H'3; Unfold valState.
Apply NcountLt with a := a' b := (rZComp b); Auto.
Generalize H'0; Case b; Auto.
Apply eqStateRzSym; Auto.
Qed.

Definition ltState := [S1, S2:State](lt (valState S1) (valState S2)).

Theorem ltStateTrans: (transitive State ltState).
Red; Unfold ltState; Auto.
Intros S1 S2 S3 H' H'0.
Apply lt_trans with m := (valState S2); Auto.
Qed.

Theorem ltStateEqComp:
  (S1, S2, S3, S4:State)
  (eqState S1 S3) -> (eqState S2 S4) -> (ltState S1 S2) ->(ltState S3 S4).
Unfold eqState ltState.
Intros S1 S2 S3 S4 H' H'0 H'1.
Elim H'0; Intros H'2 H'3; Clear H'0.
Elim H'; Intros H'0 H'4; Clear H'.
Apply lt_le_trans with m := (valState S2); Auto.
Apply le_lt_trans with m := (valState S1); Auto.
Qed.

Theorem ltStateLt:
  (a, b:rZ) (In (valRz a) L) -> (In (valRz b) L) ->
  (S1, S2:State)
  (inclState S1 S2) -> (eqStateRz S2 a b) -> ~ (eqStateRz S1 a b) ->
  (ltState S2 S1).
Intros a b H' H'0 S1 S2 H'1 H'2 H'3; Red.
Apply vallStateLt with a := a b := b; Auto.
Qed.

Theorem ltStateWf: (well_founded ? ltState).
Unfold ltState; Apply wf_inverse_image with B := nat; Auto.
Try Exact lt_wf.
Qed.
End lt.

29/06/100, 12:53