memoryRealize.v

Require Import rZ.
Require Import state.
Require Import PolyList.
Require Import PolyListAux.
Require Import memoryImplement.
Section InitialMemory.
Variable L:(list rNat).
Variable f:rNat ->rZ.

Local InRnatDec := (In_dec rNatDec).
Hypothesis fLess:(a:rNat) (In a L) ->(rVlt (f a) a).
Hypothesis fOut:(a:rNat) ~ (In a L) ->(f a)=(rZPlus a).
Hypothesis fInvol:(a:rNat)~ (In (valRz (f a)) L).

Theorem fNotContr: (a:rNat)~ (f a)=(rZMinus a).
Intros a; Case (InRnatDec a L); Auto.
Intros H'; Red; Intros H'0; Generalize (fLess a H').
Rewrite H'0; Unfold rVlt; Simpl; Auto.
Intros H'1; Absurd (rlt a a); Auto.
Intros H'; Rewrite fOut; Auto.
Red; Intros H'0; Discriminate.
Qed.

Definition image := [L':(list rNat)](map [a:rNat]((rZPlus a), (f a)) L').

Theorem InImage:
  (L':(list rNat)) (a:rNat) (In a L') ->(In ((rZPlus a), (f a)) (image L')).
Intros L'; Elim L'; Simpl; Auto.
Intros a l H' a0 H'0; Elim H'0;
[Intros H'1; Rewrite H'1; Clear H'0 | Intros H'1; Clear H'0]; Auto.
Qed.
Hints Resolve InImage.

Theorem InImageInv:
  (L':(list rNat)) (a, b:rZ) (In (a, b) (image L')) ->
  (Ex [a':rNat] a=(rZPlus a') /\ (f a')=b).
Intros L'; Elim L'; Simpl; Auto.
Intros a b H'; Elim H'; Auto.
Intros a l H' a0 b H'0; Elim H'0;
[Intros H'1; Inversion H'1; Clear H'0 | Intros H'1; Clear H'0]; Auto.
Exists a; Split; Auto.
Qed.

Definition eqF := [f:rNat ->rZ] [a, b:rZ](liftRz f a)=(liftRz f b).

Theorem eqFImpEqState: (a, b:rZ) (eqF f a b) ->(eqStateRz (image L) a b).
Intros a b; Unfold eqF; Case a; Case b; Simpl; Auto; Intros a' b' H';
Case (InRnatDec a' L); Case (InRnatDec b' L); Intros H'0 H'1; Auto;
Replace (rZMinus a') with (rZComp (rZPlus a')); Auto;
Replace (rZMinus b') with (rZComp (rZPlus b')); Auto;
Try (Rewrite <- (fOut b' H'0); Auto); Try (Rewrite <- (fOut a' H'1); Auto);
Auto; Try Rewrite H'; Auto.
Apply eqStateRzTrans with b := (f b'); Auto.
Rewrite H'; Auto; Apply eqStateRzSym; Auto.
Apply eqStateRzSym; Auto.
Rewrite <- H'; Auto.
Apply eqStateRzTrans with b := (f b'); Auto.
Rewrite H'; Auto; Apply eqStateRzSym; Auto.
Apply eqStateRzSym; Auto.
Rewrite <- H'; Auto.
Apply eqStateRzTrans with b := (rZComp (f b')); Auto.
Rewrite H'; Auto; Apply eqStateRzSym; Auto.
Apply eqStateRzSym; Auto.
Apply eqStateRzTrans with b := (rZComp (f b')); Auto.
Rewrite H'; Auto.
Apply eqStateRzTrans with b := (rZComp (f b')); Auto.
Rewrite H'; Auto; Apply eqStateRzSym; Auto.
Apply eqStateRzSym; Auto.
Rewrite <- H'; Auto.
Qed.

Theorem EqfRef: (a:rZ)(eqF f a a).
Intros a; Case a; Unfold eqF; Simpl; Auto.
Qed.

Theorem liftRzComp:
  (a, b:rZ) <rZ> (liftRz f a)=(liftRz f b) ->
  <rZ> (liftRz f (rZComp a))=(liftRz f (rZComp b)).
Intros a b; Case a; Case b; Simpl; Auto; Intros a' b' H';
Try (Rewrite H' Orelse Rewrite <- H'); Auto; Apply rZCompEq; Auto.
Qed.
Hints Resolve liftRzComp.

Theorem eqStateImpEqFAux:
  (a, b:rZ) (M:State) (eqStateRz M a b) -> M=(image L) ->(eqF f a b).
Intros a b M H'; Elim H'; Clear H' a b M; Unfold eqF; Simpl; Auto.
Intros a b L0 H' H'0; Rewrite H'0 in H'.
Elim (InImageInv L a b);
[Intros a' E; Elim E; Intros H'5 H'6; Rewrite H'5; Clear E | Idtac]; Auto.
Rewrite <- H'6; Auto.
Simpl; Generalize (fInvol a'); Case (f a'); Simpl; Auto; Intros r H'2;
Apply sym_equal; Auto.
Rewrite fOut; Auto.
Intros a b L0 H' H'0 H'1; Auto.
Rewrite <- H'0; Auto.
Intros a b c L0 H' H'0 H'1 H'2 H'3; Rewrite H'0; Auto.
Intros a b c L0 H' H'0 H'1; Absurd (liftRz f a)=(liftRz f (rZComp a)); Auto.
Case a; Simpl; Auto.
Qed.

Theorem eqStateImpEqF: (a, b:rZ) (eqStateRz (image L) a b) ->(eqF f a b).
Intros a b H'.
Apply eqStateImpEqFAux with M := (image L); Auto.
Qed.

Definition eqFDec: (a, b:rZ){(eqF f a b)}+{~ (eqF f a b)}.
Intros a b; Case a; Case b; Intros b' a'.
Case (rZDec (f a') (f b')); Intros Eqt; Auto.
Case (rZDec (f a') (rZComp (f b'))); Intros Eqt; Auto.
Case (rZDec (rZComp (f a')) (f b')); Intros Eqt; Auto.
Case (rZDec (rZComp (f a')) (rZComp (f b'))); Intros Eqt; Auto.
Defined.
(* Theorem eqMemInclImage:   (L1:(list rNat)) (incl L L1) ->(eqState (image L1) (image L)). Intros L1; Elim L1; Simpl. Case L; Auto. Intros r l H'; Absurd (In r (nil ?)); Auto with datatypes. Intros a l H' H'0. Case (in_inv a l). *)
End InitialMemory.
Section NextMemory.
Variable L:(list rNat).
Variable f:rNat ->rZ.

Local InRnatDec := (In_dec rNatDec).
Hypothesis fLess:(a:rNat) (In a L) ->(rVlt (f a) a).
Hypothesis fOut:(a:rNat) ~ (In a L) ->(f a)=(rZPlus a).
Hypothesis fInvol:(a:rNat)~ (In (valRz (f a)) L).
Variables c, d:rZ.
Hypothesis NotInc:~ (In (valRz c) L).
Hypothesis NotInd:~ (In (valRz d) L).
Hypothesis Lessdc:(rZlt d c).

Definition f': rNat ->rZ.
Intros a.
Case (rZDec (f a) c); Intros Eqac.
Exact d.
Case (rZDec (f a) (rZComp c)); Intros Eqamc.
Exact (rZComp d).
Case (rZDec (rZPlus a) c); Intros Eqac'.
Exact d.
Case (rZDec (rZMinus a) c); Intros Eqamc'.
Exact (rZComp d).
Exact (f a).
Defined.

Local L' := (cons (valRz c) L).

Theorem f'Less: (a:rNat) (In a L') ->(rVlt (f' a) a).
Intros a; Unfold f'; Case (rZDec (f a) c).
Intros H' H'0; Elim H'0;
[Intros H'1; Rewrite <- H'1; Clear H'0 | Intros H'1; Clear H'0]; Auto.
Red; Apply rltTrans with y := (valRz c); Auto.
Rewrite <- H'; Auto.
Change (rVlt (f a) a); Auto.
Case (rZDec (f a) (rZComp c)).
Intros H' H'0 H'1; Elim H'1;
[Intros H'2; Rewrite <- H'2; Clear H'1 | Intros H'2; Clear H'1]; Auto.
Red; Apply rltTrans with y := (valRz c); Auto.
Change (rVlt (rZComp d) (valRz c)); Auto.
Rewrite <- valRzComp; Auto.
Rewrite <- H'.
Change (rVlt (f a) a); Auto.
Case (rZDec (rZPlus a) c).
Intros H' H'0 H'1 H'2; Change (rZlt d (rZPlus a)).
Rewrite H'; Auto.
Case (rZDec (rZMinus a) c).
Intros H' H'0 H'1 H'2 H'3; Change (rZlt (rZComp d) (rZMinus a)).
Rewrite H'; Auto.
Red; Rewrite valRzComp; Auto.
Intros H' H'0 H'1 H'2 H'3; Case H'3; Auto.
Intros H'4; Generalize H' H'0; Rewrite <- H'4; Case c; Simpl; Auto.
Intros r H'5 H'6; Case H'6; Auto.
Intros r H'5; Case H'5; Auto.
Qed.

Theorem f'Out: (a:rNat) ~ (In a L') ->(f' a)=(rZPlus a).
Intros a; Unfold f'; Intros H'.
Cut (valRz (f a))=a;
[Intros Vala | Rewrite fOut; Auto; Red; Intros H'1; Case H'; Simpl]; Auto.
Case (rZDec (f a) c); Intros H1'.
Case (rZDec (rZPlus a) d); Intros H'2; Auto.
Case H'; Simpl; Auto.
Rewrite <- H1'; Auto.
Case (rZDec (f a) (rZComp c)); Intros H'2.
Case (rZDec (rZPlus a) (rZComp d)); Intros H'3; Auto.
Case H'; Simpl; Auto.
Left; Rewrite <- (valRzComp c).
Rewrite <- H'2; Auto.
Case (rZDec (rZPlus a) c); Intros H'3; Auto.
Case (rZDec (rZPlus a) d); Intros H'4; Auto.
Case H'; Simpl; Auto.
Rewrite <- H'3; Auto.
Case (rZDec (rZMinus a) c); Intros H'4; Auto.
Case (rZDec (rZPlus a) (rZComp d)); Intros H'5; Auto.
Case H'; Simpl; Auto.
Rewrite <- H'4; Auto.
Apply fOut; Auto.
Red; Intros H'0; Case H'; Simpl; Auto.
Qed.

Theorem notEqcd: ~ (eqRz c d).
Red; Intros tmp; Absurd (eqRz d c); Auto.
Qed.
Hints Resolve notEqcd.

Theorem f'Invol: (a:rNat)~ (In (valRz (f' a)) L').
Intros a; Unfold f'; Case (rZDec (f a) c); Auto; Intros Eq1.
Red; Intros H'0; Case H'0; Auto; Intros H'1.
Case (rZDec (f a) (rZComp c)); Auto; Intros Eq2.
Rewrite valRzComp; Red; Intros H'0; Case H'0; Auto; Intros H'1.
Case (rZDec (rZPlus a) c); Auto; Intros Eq3.
Red; Intros H'0; Case H'0; Auto; Intros H'1.
Case (rZDec (rZMinus a) c); Auto; Intros Eq4.
Rewrite valRzComp; Red; Intros H'0; Case H'0; Auto; Intros H'1.
Simpl; Red; Intros H'0; Case H'0; Auto; Intros H'1.
Generalize Eq1 Eq2 H'1; Case c; Case (f a); Simpl; Auto;
Intros c' fa' H'2 H'3 H'4; Try (Case H'2; Rewrite H'4; Auto; Fail);
Try (Case H'3; Rewrite H'4; Auto; Fail).
Case (fInvol a); Auto.
Qed.

Theorem eqF'ImpEqState: (a, b:rZ) (eqF f' a b) ->(eqStateRz (image f' L') a b).
Intros a b H'.
Apply eqFImpEqState; Auto.
Try Exact f'Out.
Qed.

Theorem eqStateImpEqF': (a, b:rZ) (eqStateRz (image f' L') a b) ->(eqF f' a b).
Intros a b H'.
Apply eqStateImpEqF with L := L'; Auto.
Try Exact f'Out.
Try Exact f'Invol.
Qed.

Theorem f'cEquald: (liftRz f' c)=d.
Generalize (refl_equal ? c); Pattern -2 c; Case c; Simpl; Intros c'; Unfold f';
Intros Eqc.
Case (rZDec (f c') c); Intros Eq1; Auto.
Case (rZDec (f c') (rZComp c)); Intros Eq2; Auto.
Absurd <rZ> (f c')=(rZComp c); Auto.
Rewrite <- Eqc; Simpl; Auto.
Apply fNotContr with L := L; Auto.
Case (rZDec (rZPlus c') c); Intros Eq3; Auto.
Case Eq3; Auto.
Case (rZDec (f c') c); Intros Eq1; Auto.
Absurd <rZ> (f c')=(rZMinus c'); Auto.
Apply fNotContr with L := L; Auto.
Rewrite Eqc; Auto.
Case (rZDec (f c') (rZComp c)); Intros Eq2; Auto.
Case (rZDec (rZPlus c') c); Intros Eq3; Auto.
Rewrite <- Eqc in Eq3; Auto.
Inversion Eq3; Auto.
Case (rZDec (rZMinus c') c); Intros Eq4; Auto.
Case Eq4; Auto.
Qed.

Theorem f'dEquald: (liftRz f' d)=d.
Generalize (refl_equal ? d); Pattern -2 d; Case d; Simpl; Intros d'; Intros Eqd.
Rewrite f'Out; Auto.
Rewrite <- Eqd in NotInd; Simpl in NotInd; Auto.
Simpl; Red; Intros H'; Case NotInd.
Case H'; Intros H'1; Auto.
Absurd (eqRz c d); Auto.
Red; Rewrite H'1; Rewrite <- Eqd; Auto.
Rewrite f'Out; Auto.
Rewrite <- Eqd in NotInd; Simpl in NotInd; Auto.
Simpl; Red; Intros H'; Case NotInd.
Case H'; Intros H'1; Auto.
Absurd (eqRz c d); Auto.
Red; Rewrite H'1; Rewrite <- Eqd; Auto.
Qed.

Theorem cEquald: (eqF f' c d).
Red.
Rewrite f'dEquald; Auto.
Exact f'cEquald; Auto.
Qed.

Theorem MrEquivAux1: (a:rNat)(f' a)=(liftRz f' (f a)).
Intros a; Unfold f'; Auto.
Unfold liftRz; Generalize (refl_equal ? (f a)); Pattern -2 (f a); Case (f a);
Intros fa Eqfa.
Cut ~ (In fa L); [Intros Infa | Idtac].
2:Change ~ (In (valRz (rZPlus fa)) L); Auto.
2:Rewrite Eqfa; Auto.
Case (rZDec (rZPlus fa) c); Intros Eq1; Auto.
Case (rZDec (f fa) c); Auto.
Case (rZDec (f fa) (rZComp c)); Auto.
Intros H' H'0; Case H'0.
Change (f (valRz (rZPlus fa)))=c.
Rewrite <- Eq1; Auto.
Case (rZDec (rZPlus fa) (rZComp c)); Intros Eq2; Auto.
Case (rZDec (f fa) c); Auto.
Intros H'; Case Eq1.
Rewrite <- H'.
Apply sym_equal.
Change (f (valRz (rZPlus fa)))=(rZPlus fa).
Apply fOut; Auto.
Case (rZDec (f fa) (rZComp c)); Auto.
Intros H' H'0; Case H'.
Rewrite <- Eq2; Auto.
Case (rZDec (rZPlus a) c); Intros Eq3; Auto.
Case Eq1; Auto.
Rewrite Eqfa.
Rewrite <- Eq3.
Apply fOut; Auto.
Change ~ (In (valRz (rZPlus a)) L); Auto.
Rewrite Eq3; Auto.
Case (rZDec (rZMinus a) c); Intros Eq4; Auto.
Case Eq2; Rewrite Eqfa.
Rewrite <- Eq4; Simpl.
Apply fOut; Auto.
Change ~ (In (valRz (rZMinus a)) L); Auto.
Rewrite Eq4; Auto.
Case (rZDec (f fa) c); Intros Eq5; Auto.
Case Eq1; Rewrite Eqfa; Auto.
Rewrite <- Eq5.
Rewrite (fOut fa); Auto.
Case (rZDec (f fa) (rZComp c)); Intros Eq6; Auto.
Case Eq2; Rewrite Eqfa; Auto.
Rewrite <- Eq6.
Rewrite <- Eqfa; Apply sym_equal; Auto.
Case (rZDec (rZMinus fa) c); Intros Eq7; Auto.
Case Eq2; Rewrite Eqfa; Auto.
Rewrite <- Eq7; Auto.
Apply sym_equal; Auto.
Cut ~ (In fa L); [Intros Infa | Idtac].
2:Change ~ (In (valRz (rZMinus fa)) L); Auto.
2:Rewrite Eqfa; Auto.
Case (rZDec (rZMinus fa) c); Intros Eq1; Auto.
Case (rZDec (f fa) c); Auto.
Intros H'; Absurd (f fa)=c; Auto.
Change ~ (f (valRz (rZMinus fa)))=c.
Rewrite fOut; Auto.
Rewrite <- Eq1; Red; Intros; Discriminate.
Case (rZDec (f fa) (rZComp c)); Auto.
Intros H'; Case H'.
Rewrite <- Eq1.
Change (f (valRz (rZPlus fa)))=(rZPlus fa); Auto.
Case (rZDec (rZMinus fa) (rZComp c)); Intros Eq2; Auto.
Case (rZDec (f fa) c); Auto.
Intros H'; Case H'.
Cut (rZComp (rZMinus fa))=c; [Intros H'1; Rewrite <- H'1 | Rewrite Eq2]; Simpl;
Auto.
Case (rZDec (rZPlus a) c); Intros Eq3; Auto.
Case Eq1; Auto.
Rewrite Eqfa.
Rewrite <- Eq3.
Apply fOut; Auto.
Change ~ (In (valRz (rZPlus a)) L); Auto.
Rewrite Eq3; Auto.
Case (rZDec (rZMinus a) c); Intros Eq4; Auto.
Case Eq2; Rewrite Eqfa.
Rewrite <- Eq4; Simpl.
Apply fOut; Auto.
Change ~ (In (valRz (rZMinus a)) L); Auto.
Rewrite Eq4; Auto.
Case (rZDec (f fa) c); Intros Eq5; Auto.
Case Eq2; Rewrite <- Eq5; Auto.
Rewrite (fOut fa); Auto.
Case (rZDec (f fa) (rZComp c)); Intros Eq6; Auto.
Case Eq1; Auto.
Rewrite <- (rZCompInv c).
Rewrite <- Eq6.
Rewrite (fOut fa); Auto.
Case (rZDec (rZPlus fa) c); Intros Eq7; Auto.
Case Eq2; Rewrite <- Eq7; Auto.
Rewrite (fOut fa); Auto.
Qed.

Theorem MrEquivAux2:
  (a:rNat)(eqStateRz (addEq (c, d) (image f L)) (rZPlus a) (f' a)).
Intros a; Unfold f'; Auto.
Case (rZDec (f a) c); Intros Eq1; Auto.
Apply eqStateRzTrans with b := c; Auto with datatypes.
Case (rZDec (rZPlus a) c); Auto.
Intros H'; Rewrite H'; Auto.
Intros H'.
Apply eqStateIncl with S1 := (image f L); Auto.
Apply eqStateRzIn; Auto.
Rewrite <- Eq1.
Apply InImage; Auto.
Case (InRnatDec a L); Auto.
Intros H'0; Case H'.
Rewrite <- Eq1; Apply sym_equal; Auto.
Case (rZDec (f a) (rZComp c)); Auto; Intros Eq2.
Apply eqStateRzTrans with b := (rZComp c); Auto with datatypes.
Case (rZDec (rZPlus a) (rZComp c)); Intros Eq3.
Rewrite Eq3; Auto.
Apply eqStateIncl with S1 := (image f L); Auto.
Apply eqStateRzIn; Auto.
Rewrite <- Eq2; Auto.
Apply InImage; Auto.
Case (InRnatDec a L); Auto.
Intros Eq4; Case Eq3.
Rewrite <- Eq2; Apply sym_equal; Auto.
Case (rZDec (rZPlus a) c); Intros Eq3; Auto.
Rewrite Eq3; Auto with datatypes; Auto.
Case (rZDec (rZMinus a) c); Intros Eq4; Auto.
Apply eqStateRzTrans with b := (rZComp c); Auto.
Rewrite <- Eq4; Auto.
Case (InRnatDec a L); Auto; Intros InaL.
Apply eqStateIncl with S1 := (image f L); Auto.
Apply eqStateRzIn; Auto.
Apply InImage; Auto.
Rewrite fOut; Auto.
Qed.

Theorem MrEquiv: (eqState (cons (c, d) (image f L)) (image f' L')).
Red; Split; Auto.
Apply inclStateIn; Auto.
Simpl; Auto.
Intros a b H'; Elim H';
[Intros H'0; Inversion H'0; Clear H' | Intros H'0; Clear H']; Auto.
Rewrite <- H1; Auto.
Rewrite <- H0; Auto.
Apply eqF'ImpEqState; Auto.
Apply cEquald; Auto.
Elim (InImageInv f L a b);
[Intros a' E; Elim E; Intros H'5 H'6; Rewrite <- H'6; Rewrite H'5; Clear E |
   Idtac]; Auto.
Apply eqF'ImpEqState; Auto.
Unfold eqF; Auto.
Rewrite <- MrEquivAux1; Auto.
Apply inclStateIn; Auto.
Intros a b H'.
Elim (InImageInv f' L' a b);
[Intros a' E; Elim E; Intros H'5 H'6; Rewrite <- H'6; Rewrite H'5; Clear E |
   Idtac]; Auto.
Apply MrEquivAux2; Auto.
Qed.
End NextMemory.

17/05/100, 13:19