memoryImplement.v

Require Import rZ.
Require Import OrderedListEq.
Require Import Relation_Definitions.
Require Import LetP.
Require Import PolyListAux.
Require Import PolyList.
Require Import array.
Require Import triplet.
Require Import state.
Require Import restrictState.
Require Import ltState.
Require Import Option.
Section mem.
Variable LL:(list triplet).

Definition OlistRz := (Olist rZ rZlt).

Definition DisjointRz := (Disjoint rZ eqRz).

Definition InRz := (InEq rZ eqRz).

Theorem InEqInv:
  (a:rZ) (L:(list rZ)) (InRz a L) ->(In a L) \/ (In (rZComp a) L).
Intros a L H'; Elim H'; Clear H' a L; Auto.
Intros a b L; Case a; Case b; Unfold eqRz; Simpl; Intros a' b' Eqt; Rewrite Eqt;
Auto.
Intros a b L H' H'0; Elim H'0; Auto with datatypes.
Qed.

Theorem InRzDec: (a:rZ) (L:(list rZ)){(InRz a L)}+{~ (InRz a L)}.
Intros a L; Elim L; Auto.
Right; Red; Intros H'; Inversion H'.
Intros a0 l H'; Case H'.
Intros H'0; Left; Auto.
Red; Apply InEqSkip; Auto.
Intros H'0; Case (rNatDec (valRz a) (valRz a0)); Intros H'1.
Left; Auto.
Red; Apply InEqHead; Auto.
Right; Red; Intros H'2; Inversion_clear H'2.
Case H'1; Auto.
Case H'0; Auto.
Qed.

Definition appendRz := (appendf rZ rZlt eqRz rZltEDec).

Definition fappendRz :=
   [pol:rZ ->rZ] [Hpol:(d:rZ)(eqRz (pol d) d)]
   (fappendf
      rZ rZlt eqRz eqrZRefl eqrZSym eqrZTrans rZltEDec pol Hpol rZltEqComp).

Inductive vM: Set :=
     ref: rZ ->vM
    | class: (list rZ) ->vM .

Inductive pointerDecrease[n:rNat]: (Array n vM) ->Prop :=
     pointerDecreaseDef:
       (Ar:(Array n vM))
       ((r:rNat) (s:rZ) (Hr:(rlt r n)) (getAval n vM Ar r Hr)=(ref s) ->
        (rVlt s r)) ->(pointerDecrease n Ar) .

Inductive pointToClassRef[n:rNat]: (Array n vM) ->Prop :=
     pointToClassRefDef:
       (Ar:(Array n vM))
       ((r:rNat)
        (s, t:rZ)
        (Hr:(rlt r n)) (Hs:(rVlt s n)) (getAval n vM Ar r Hr)=(ref s) ->
        ~ (getAval n vM Ar (valRz s) Hs)=(ref t)) ->(pointToClassRef n Ar) .

Inductive pointToClassClass[n:rNat]: (Array n vM) ->Prop :=
     pointToClassClassRef:
       (Ar:(Array n vM))
       ((r:rNat)
        (s:rZ)
        (Hr:(rlt r n))
        (Hs:(rVlt s n))
        (Lr:(list rZ)) (getAval n vM Ar r Hr)=(class Lr) -> (In s Lr) ->
        (getAval n vM Ar (valRz s) Hs)=(ref (samePol s r))) ->
       ((r:rNat)
        (s:rZ)
        (Hr:(rlt r n))
        (Hs:(rVlt s n))
        (Ls:(list rZ))
        (getAval n vM Ar r Hr)=(ref s) ->
        (getAval n vM Ar (valRz s) Hs)=(class Ls) ->(In (samePol s r) Ls)) ->
       (pointToClassClass n Ar) .

Inductive classInArrray[n:rNat]: (Array n vM) ->Prop :=
     classInArrrayDef:
       (Ar:(Array n vM))
       ((r:rNat)
        (s:rZ)
        (Hr:(rlt r n))
        (Lr:(list rZ)) (getAval n vM Ar r Hr)=(class Lr) -> (In s Lr) ->
        (rVlt s n)) ->(classInArrray n Ar) .

Inductive OlistArray[n:rNat]: (Array n vM) ->Prop :=
     OlistArrayDef:
       (Ar:(Array n vM))
       ((r:rNat)
        (Hr:(rlt r n)) (Lr:(list rZ)) (getAval n vM Ar r Hr)=(class Lr) ->
        (OlistRz Lr)) ->(OlistArray n Ar) .

Inductive wellFormedArray[n:rNat]: (Array n vM) ->Prop :=
     wellFormedArrayDef:
       (Ar:(Array n vM))
       (pointerDecrease n Ar) ->
       (pointToClassRef n Ar) ->
       (pointToClassClass n Ar) -> (classInArrray n Ar) -> (OlistArray n Ar) ->
       (wellFormedArray n Ar) .

Theorem wfPd:
  (n:rNat)
  (Ar:(Array n vM))
  (r:rNat)
  (s:rZ)
  (Hr:(rlt r n)) (wellFormedArray n Ar) -> (getAval n vM Ar r Hr)=(ref s) ->
  (rVlt s r).
Intros n Ar r s Hr H' H'1; Inversion H'; Auto.
Inversion H; Auto.
Apply H5 with Hr := Hr; Auto.
Qed.

Theorem wfPcr:
  (n:rNat)
  (Ar:(Array n vM))
  (r:rNat)
  (s, t:rZ)
  (Hr:(rlt r n))
  (Hs:(rVlt s n)) (wellFormedArray n Ar) -> (getAval n vM Ar r Hr)=(ref s) ->
  ~ (getAval n vM Ar (valRz s) Hs)=(ref t).
Intros n Ar r s t Hr Hs H' H'0; Inversion H'; Auto.
Inversion H0.
Apply H5 with r := r Hr := Hr; Auto.
Qed.

Theorem wfPcc1:
  (n:rNat)
  (Ar:(Array n vM))
  (r:rNat)
  (s:rZ)
  (Hr:(rlt r n))
  (Hs:(rVlt s n))
  (Lr:(list rZ))
  (wellFormedArray n Ar) -> (getAval n vM Ar r Hr)=(class Lr) -> (In s Lr) ->
  (getAval n vM Ar (valRz s) Hs)=(ref (samePol s r)).
Intros n Ar r s Hr Hs Lr H' H'0 H'1; Inversion H'.
Inversion H1.
Apply H5 with Hr := Hr Lr := Lr; Auto.
Qed.

Theorem wfPcc2:
  (n:rNat)
  (Ar:(Array n vM))
  (r:rNat)
  (s:rZ)
  (Hr:(rlt r n))
  (Hs:(rVlt s n))
  (Ls:(list rZ))
  (wellFormedArray n Ar) ->
  (getAval n vM Ar r Hr)=(ref s) -> (getAval n vM Ar (valRz s) Hs)=(class Ls) ->
  (In (samePol s r) Ls).
Intros n Ar r s Hr Hs Ls H' H'0 H'1; Inversion H'; Auto.
Inversion H1.
Apply H6 with Hr := Hr Hs := Hs; Auto.
Qed.

Theorem wfCa:
  (n:rNat)
  (Ar:(Array n vM))
  (r:rNat)
  (s:rZ)
  (Hr:(rlt r n))
  (Lr:(list rZ))
  (wellFormedArray n Ar) -> (getAval n vM Ar r Hr)=(class Lr) -> (In s Lr) ->
  (rVlt s n).
Intros n Ar r s Hr Lr H' H'0 H'1; Inversion H'.
Inversion H2; Auto.
Apply H5 with r := r Hr := Hr Lr := Lr; Auto.
Qed.

Theorem wfOl:
  (n:rNat)
  (Ar:(Array n vM))
  (r:rNat)
  (Hr:(rlt r n))
  (Lr:(list rZ)) (wellFormedArray n Ar) -> (getAval n vM Ar r Hr)=(class Lr) ->
  (OlistRz Lr).
Intros n Ar r Hr Lr H' H'0; Inversion H'.
Inversion H3; Auto.
Apply H5 with r := r Hr := Hr; Auto.
Qed.

Theorem wfDisjoint:
  (n:rNat)
  (Ar:(Array n vM))
  (r, s:rNat)
  (Hr:(rlt r n))
  (Hs:(rlt s n))
  (Lr:(list rZ))
  (Ls:(list rZ))
  (wellFormedArray n Ar) ->
  ~ s=r ->
  (getAval n vM Ar r Hr)=(class Lr) -> (getAval n vM Ar s Hs)=(class Ls) ->
  (DisjointRz Lr Ls).
Intros n Ar r s Hr Hs Lr Ls Wf H' H'0 H'1; Red.
Apply DisjointDef; Auto.
Intros a H'2; Red; Intros H'3.
Case (InEqInv ? ? H'3); Case (InEqInv ? ? H'2); Intros In1 In2; Auto;
Try ((Cut (rVlt a n); [Intros Ha | Apply wfCa with 2 := H'1; Auto; Fail])
       Orelse (Cut (rVlt (rZComp a) n);
                [Intros Ha | Apply wfCa with 2 := H'1; Auto; Fail]));
Try Try ((Cut (rVlt a n); [Intros Ha' | Apply wfCa with 2 := H'0; Auto; Fail])
           Orelse (Cut (rVlt (rZComp a) n);
                    [Intros Ha' | Apply wfCa with 2 := H'0; Auto; Fail])); Auto;
[Absurd (ref (samePol a s))=(ref (samePol a r)) |
   Absurd (ref (samePol a s))=(ref (samePol (rZComp a) r)) |
   Absurd (ref (samePol (rZComp a) s))=(ref (samePol a r)) |
   Absurd (ref (samePol (rZComp a) s))=(ref (samePol (rZComp a) r))];
Try (Case a; Simpl; Red; Intros a' H'4; Case H'; Inversion H'4; Auto; Fail);
Auto; Rewrite <- wfPcc1 with Hs := Ha 2 := H'1; Auto;
Rewrite <- wfPcc1 with Hs := Ha' 2 := H'0; Auto; Apply getAvalIrr; Auto;
Case a; Auto.
Qed.

Definition memory := [n:rNat]{q:(Array n vM) | (wellFormedArray n q)}.

Theorem getNotIdP:
  (n:rNat) (Ar:(Array n vM)) (r:rZ) (Hr:(rVlt r n)) (wellFormedArray n Ar) ->
  ~ (getAval n vM Ar (valRz r) Hr)=(ref r).
Intros n Ar r Hr H'; Red; Intros H'1.
Absurd (rVlt r (valRz r)); Auto.
Unfold rVlt; Auto.
Apply wfPd with n := n Ar := Ar Hr := Hr; Auto.
Qed.

Definition setAvalList:
  (n:rNat) (mL:(list rZ)) ((m:rZ) (In m mL) ->(rVlt m n)) ->
  (Ar:(Array n vM)) rZ ->(Array n vM).
Fix 2.
Intros n mL; Case mL.
Intros Inmml' Ar a; Exact Ar.
Intros m ml' Inm Ar a.
Cut (m:rZ) (In m ml') ->(rVlt m n); [Intros Inml' | Idtac].
Cut (rVlt m n); [Intros Hm | Idtac].
Exact (setAvalList
         n ml' Inml' (setAval n vM Ar (valRz m) Hm (ref (samePolRz m a))) a).
Apply Inm; Simpl; Auto.
Intros m0 H'; Apply Inm; Auto; (Simpl; Auto).
Defined.

Theorem setAvalListInv1:
  (n:rNat)
  (a:rZ)
  (mL:(list rZ))
  (Inml:(m:rZ) (In m mL) ->(rVlt m n))
  (Ar:(Array n vM)) (m:rZ) (mle:(rVlt m n)) ~ (InRz m mL) ->
  (getAval n vM (setAvalList n mL Inml Ar a) (valRz m) mle)=
  (getAval n vM Ar (valRz m) mle).
Intros n a mL; Elim mL; Simpl; Auto.
Intros r l Rec Inml Ar m mle H'0.
Rewrite Rec; Auto.
Rewrite setAvalDef2; Auto.
Red; Intros H'; Case H'0; Auto.
Red; Apply InEqHead; Auto; Red; Auto.
Red; Intros H'; Case H'0; Auto.
Red; Apply InEqSkip; Auto.
Qed.

Theorem setAvalListInv2:
  (n:rNat)
  (a:rZ) (mL:(list rZ)) (Inml:(m:rZ) (In m mL) ->(rVlt m n)) (OlistRz mL) ->
  (Ar:(Array n vM)) (m:rZ) (mle:(rVlt m n)) (In m mL) ->
  (getAval n vM (setAvalList n mL Inml Ar a) (valRz m) mle)=
  (ref (samePolRz m a)).
Intros n a mL; Elim mL; Simpl; Auto.
Intros H' H'0 Ar m mle H'1; Elim H'1.
Intros a0 l H' Inml H'0 Ar m mle H'1; Elim H'1;
[Intros H'2; Clear H'1 | Intros H'2; Clear H'1]; Auto.
Rewrite setAvalListInv1; Auto.
Rewrite (setAvalIrr
           n vM Ar (valRz a0) (valRz m)
           (Inml a0 (or_introl a0=a0 (In a0 l) (refl_equal rZ a0))) mle); Auto.
Rewrite setAvalDef1; Auto.
Rewrite <- H'2; Auto.
Rewrite <- H'2; Auto.
Rewrite <- H'2; Auto.
Apply OlistUniqueEq with A := rZ ltA := rZlt eqA := eqRz a := a0; Auto.
Exact rZltEqComp.
Rewrite H'; Auto.
Red; Apply OlistInv with a := a0; Auto.
Qed.

Theorem wellFormedArrayInImpLt:
  (n:rNat)
  (Ar:(Array n vM))
  (a:rNat)
  (b:rZ)
  (Ha:(rlt a n))
  (La:(list rZ))
  (wellFormedArray n Ar) -> (getAval n vM Ar a Ha)=(class La) -> (In b La) ->
  (rlt a (valRz b)).
Intros n Ar a b Ha La War geta Inb.
Cut (rVlt (samePol b a) (valRz b)).
Case b; Simpl; Auto.
Cut (rVlt b n); [Intros Hb | Idtac].
Apply wfPd with n := n Ar := Ar Hr := Hb; Auto.
Apply wfPcc1 with Hr := Ha Lr := La; Auto.
Apply wfCa with 2 := geta; Auto.
Qed.

Theorem wellFormedArrayInRzLt:
  (n:rNat)
  (Ar:(Array n vM))
  (a:rNat)
  (b:rZ)
  (Ha:(rlt a n))
  (La:(list rZ))
  (wellFormedArray n Ar) -> (getAval n vM Ar a Ha)=(class La) -> (InRz b La) ->
  (rVlt b n).
Intros n Ar a b Ha La H' H'0 H'1; Case (InEqInv b La H'1); Intros H'2; Auto.
Apply wfCa with 2 := H'0; Auto.
Cut (rVlt (rZComp b) n); [Case b; Simpl | Idtac]; Auto.
Apply wfCa with 2 := H'0; Auto.
Qed.

Theorem wellFormedArrayInImpNotEq:
  (n:rNat)
  (Ar:(Array n vM))
  (a, b:rNat)
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (wellFormedArray n Ar) ->
  (getAval n vM Ar a Ha)=(class La) -> (getAval n vM Ar b Hb)=(class Lb) ->
  ~ (InRz (rZPlus a) Lb).
Intros n Ar a b Ha Hb La Lb War geta getb; Red; Intros H'3.
Case (InEqInv (rZPlus a) Lb H'3); Intros H'4; Auto.
Absurd (getAval n vM Ar (valRz (rZPlus a)) Ha)=(class La); Auto.
Rewrite wfPcc1 with 2 := getb; Auto.
Red; Intro; Discriminate.
Absurd (getAval n vM Ar (valRz (rZMinus a)) Ha)=(class La); Auto.
Rewrite wfPcc1 with 2 := getb; Auto.
Red; Intro; Discriminate.
Qed.

Theorem wellFormedArrayInBothImpEq:
  (n:rNat)
  (Ar:(Array n vM))
  (a, b:rNat)
  (c, d:rZ)
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (wellFormedArray n Ar) ->
  (getAval n vM Ar a Ha)=(class La) ->
  (getAval n vM Ar b Hb)=(class Lb) -> (In c La) -> (In d Lb) -> (eqRz c d) ->
  a=b.
Intros n Ar a b c d Ha Hb La Lb War geta getb inc1 inc2 eqRz1.
Cut (rVlt c n); [Intros Hc | Apply wfCa with 2 := geta]; Auto.
Cut (rVlt d n); [Intros Hd | Apply wfCa with 2 := getb]; Auto.
Cut (ref (samePol c a))=(ref (samePol d b)).
Generalize eqRz1; Case c; Case d; Simpl; Intros c' d' H' H'1; Inversion H'1;
Auto.
Rewrite <- wfPcc1 with 2 := geta Hs := Hc; Auto.
Rewrite <- wfPcc1 with 2 := getb Hs := Hd; Auto.
Apply getAvalIrr; Auto.
Qed.

Theorem wellFormedArrayInRzBothImpEq:
  (n:rNat)
  (Ar:(Array n vM))
  (a, b:rNat)
  (c:rZ)
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (wellFormedArray n Ar) ->
  (getAval n vM Ar a Ha)=(class La) ->
  (getAval n vM Ar b Hb)=(class Lb) -> (InRz c La) -> (InRz c Lb) ->a=b.
Intros n Ar a b c Ha Hb La Lb H' H'0 H'1 H'2 H'3.
Case (InEqInv c La H'2); Case (InEqInv c Lb H'3); Intros H'4 H'5;
Apply wellFormedArrayInBothImpEq with 2 := H'0 3 := H'1 4 := H'5 5 := H'4;
Auto; Case c; Auto.
Qed.

Theorem wellFormedArrayInImpNotEqSimpl:
  (n:rNat)
  (Ar:(Array n vM))
  (a:rNat)
  (Ha:(rlt a n))
  (La:(list rZ)) (wellFormedArray n Ar) -> (getAval n vM Ar a Ha)=(class La) ->
  ~ (InRz (rZPlus a) La).
Intros n Ar a Ha La H' H'0.
Apply wellFormedArrayInImpNotEq with 2 := H'0 3 := H'0; Auto.
Qed.

Theorem DisjbLb:
  (n:rNat)
  (b:rNat)
  (Hb:(rlt b n))
  (Lb:(list rZ))
  (Ar:(Array n vM))
  (War:(wellFormedArray n Ar)) (getb:(getAval n vM Ar b Hb)=(class Lb))
  (DisjointRz (cons (rZPlus b) (nil ?)) Lb).
Intros n b Hb Lb Ar War getb; Red; Simpl.
Apply DisjointDef; Simpl; Auto.
Intros a H'; Inversion_clear H'.
Apply NotInEqComp with a := (rZPlus b); Auto.
Apply wellFormedArrayInImpNotEqSimpl with 2 := getb; Auto.
Inversion H.
Qed.

Theorem DisjLaLc:
  (n:rNat)
  (a, b:rNat)
  (Neqab:~ a=b)
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (Ar:(Array n vM))
  (War:(wellFormedArray n Ar))
  (geta:(getAval n vM Ar a Ha)=(class La))
  (getb:(getAval n vM Ar b Hb)=(class Lb))
  (DisjointRz La (appendRz (cons (rZPlus b) (nil ?)) Lb)).
Intros n a b ltab Ha Hb La Lb Ar War geta getb.
Cut (DisjointRz La Lb);
[Intros DLaLb | Apply wfDisjoint with 3 := geta 4 := getb; Auto].
Red; Auto.
Apply DisjointCom; Unfold appendRz; Apply appendfDisjoint; Auto.
Apply DisjbLb with n := n Hb := Hb Ar := Ar; Auto.
Apply DisjointDef; Simpl; Auto.
Intros a0 H'; Inversion_clear H'.
Apply NotInEqComp with a := (rZPlus b); Auto.
Apply wellFormedArrayInImpNotEq with 2 := getb 3 := geta; Auto.
Inversion_clear H.
Apply DisjointCom; Auto.
Qed.

Theorem InRzLc:
  (n:rNat)
  (b:rNat)
  (Hb:(rlt b n))
  (Lb:(list rZ))
  (Ar:(Array n vM))
  (War:(wellFormedArray n Ar))
  (getb:(getAval n vM Ar b Hb)=(class Lb))
  (c:rZ) (InRz c (appendRz (cons (rZPlus b) (nil ?)) Lb)) ->(rVlt c n).
Intros n b Hb Lb Ar War getb c0 H'.
Case (appendfInvEq rZ ? ? rZltEDec (cons (rZPlus b) (nil rZ)) Lb c0); Auto.
Intros H'0; Inversion_clear H'0; Auto.
Red; Unfold eqRz in H; Rewrite H; Auto.
Inversion_clear H.
Intros H'0.
Apply wellFormedArrayInRzLt with 2 := getb; Auto.
Qed.

Theorem InLc:
  (n:rNat)
  (b:rNat)
  (Hb:(rlt b n))
  (Lb:(list rZ))
  (Ar:(Array n vM))
  (War:(wellFormedArray n Ar))
  (getb:(getAval n vM Ar b Hb)=(class Lb))
  (c:rZ) (In c (appendRz (cons (rZPlus b) (nil ?)) Lb)) ->(rVlt c n).
Intros n b Hb Lb Ar War getb c0 H'.
Apply InRzLc with 1 := War 2 := getb; Auto.
Red.
Apply inImpInEq; Auto.
Qed.
Variable maxN:rNat.
Hypothesis HmaxN:maxN=(rnext (maxVarTriplets LL)).

Theorem inTripletmaxN: (v:rZ) (inTriplets v LL) ->(rVlt v maxN).
Rewrite HmaxN; Elim LL; Simpl; Auto.
Intros v H'; Elim H'; Auto.
Unfold rVlt; Unfold eqRz in H'; Rewrite H'; Auto.
Intros a; Case a; Simpl; Auto.
Intros H' r r0 r1 l H'0 v H'1; Elim H'1; Clear H'1; Intros H'1;
[Elim H'1; Clear H'1; Intros H'1; [Idtac | Elim H'1; Clear H'1; Intros H'1];
   Unfold rVlt; Unfold eqRz in H'1; Rewrite H'1;
   Apply rltTransRnext1 with m := (rmax (rmax (valRz r) (valRz r0)) (valRz r1)) |
   Idtac]; Auto.
Apply rltTransRnext1 with m := (rmax (valRz r) (valRz r0)); Auto.
Apply rltTransRnext1 with m := (rmax (valRz r) (valRz r0)); Auto.
Unfold rVlt; Apply rltTransRnext1 with m := (maxVarTriplets l); Auto.
Unfold rVlt in H'0; Auto.
Qed.

Definition Mem := (memory maxN).

Definition evalMnat :=
   [M:Mem] [n:rNat] [Ltn:(rlt n maxN)]
      Cases M of
          (exist Ar _) => Cases (getAval maxN vM Ar n Ltn) of
                              (ref p) => p
                             | (class _) => (rZPlus n)
                          end
      end.

Theorem evalMnatIrr:
  (M:Mem) (n1, n2:rNat) (Ltn1:(rlt n1 maxN)) (Ltn2:(rlt n2 maxN)) n1=n2 ->
  (evalMnat M n1 Ltn1)=(evalMnat M n2 Ltn2).
Intros M; Case M; Simpl; Auto.
Intros Ar War n1 n2 Ltn1 Ltn2 Eqn1n2.
Rewrite (getAvalIrr maxN vM Ar n1 n2 Ltn1 Ltn2); Auto.
Rewrite Eqn1n2; Auto.
Qed.
Hints Resolve evalMnatIrr.

Definition evalMZ: Mem ->(v:rZ) (rVlt v maxN) ->rZ :=
   [M:Mem] [v:rZ]
      <[r:rZ] (rVlt r maxN) ->rZ>Cases v of
          (rZPlus a) => [Maxv:(rVlt (rZPlus a) maxN)](evalMnat M a Maxv)
         | (rZMinus a) =>
             [Maxv:(rVlt (rZMinus a) maxN)](rZComp (evalMnat M a Maxv))
      end.

Theorem EqrZComp: (a, b:rZ) a=b ->(rZComp a)=(rZComp b).
Intros a b H'; Rewrite H'; Auto.
Qed.
Hints Resolve EqrZComp.

Theorem evalMZIrr:
  (M:Mem) (v1, v2:rZ) (Maxv1:(rVlt v1 maxN)) (Maxv2:(rVlt v2 maxN)) v1=v2 ->
  (evalMZ M v1 Maxv1)=(evalMZ M v2 Maxv2).
Intros M v1 v2; Case v1; Case v2; Intros a2 a1 Maxv1 Maxv2 Eqv1v2;
Inversion Eqv1v2; Unfold evalMZ; Try Apply EqrZComp; Apply evalMnatIrr; Auto.
Qed.
Hints Resolve evalMZIrr.

Definition eMZ: Mem ->(a:rNat) (Ha:(rlt a maxN))vM.
Intros M; Case M.
Intros Ar War a Ha.
Exact (getAval maxN vM Ar a Ha).
Defined.

Theorem eMZIrr:
  (M:Mem) (a, b:rNat) (Maxa:(rlt a maxN)) (Maxb:(rlt b maxN)) a=b ->
  (eMZ M a Maxa)=(eMZ M b Maxb).
Intros M; Case M; Simpl; Auto.
Intros x H' a b Maxa Maxb H'0.
Apply getAvalIrr; Auto.
Qed.

Definition eqMem :=
   [M1, M2:Mem] (a:rNat) (Maxa:(rlt a maxN))(eMZ M1 a Maxa)=(eMZ M2 a Maxa).

Theorem eqMemSym: (symmetric ? eqMem).
Red; Unfold eqMem; Auto.
Qed.
Hints Immediate eqMemSym.

Theorem eqMemRef: (M:Mem)(eqMem M M).
Red; Unfold eqMem; Auto.
Qed.
Hints Resolve eqMemRef.

Theorem eqMemTrans: (transitive Mem eqMem).
Red; Unfold eqMem; Auto.
Intros x y z H' H'0 v Inv; Rewrite H'; Auto.
Qed.

Theorem evalMnatEqM:
  (M1, M2:Mem) (n:rNat) (Ltn:(rlt n maxN)) (eqMem M1 M2) ->
  (evalMnat M1 n Ltn)=(evalMnat M2 n Ltn).
Intros M1 M2 n Ltn; Unfold eqMem; Case M1; Case M2; Simpl.
Intros Ar1 War1 Ar2 War2 H'1; Rewrite (H'1 n Ltn); Auto.
Qed.

Definition dList :=
   {L:(list rZ) | (OlistRz L) /\ ((a:rZ) (In a L) ->(rVlt a maxN))}.

Definition appd: dList -> dList ->dList.
Intros d1 d2; Case d2; Case d1.
Intros L1 OL1 L2 OL2; Exists (appendRz L1 L2); Split; Auto.
Elim OL1; Intros H' H'0; Clear OL1.
Elim OL2; Intros H'1 H'2; Clear OL2; Auto.
Red.
Unfold appendRz; Apply appendfOlist; Auto.
Intros a b c d H'3 H'4 H'5.
Apply rZltEqComp with a := a b := b; Auto.
Elim OL1; Intros H' H'0; Clear OL1.
Elim OL2; Intros H'1 H'2; Clear OL2; Auto.
Intros a H'3.
Elim (appendfInv ? rZlt eqRz rZltEDec L1 L2 a); Auto.
Defined.

Definition Ind: rZ -> dList ->Prop :=
   [a:rZ] [L:dList]
      Cases L of
          (exist x _) => (InRz a x)
      end.

Theorem IndAppdL: (L1, L2:dList) (a:rZ) (Ind a L1) ->(Ind a (appd L1 L2)).
Intros L1 L2; Case L1; Case L2; Simpl; Auto.
Intros x H' x0 H'0 a H'1.
Red; Auto.
Generalize appendfInclEq1; Unfold InclEq; Auto.
Intros H'2;
Specialize 6 H'2
      with ltA := rZlt eqA := eqRz ltADec := rZltEDec L1 := x0 L2 := x;
Intros H'8; Inversion H'8; Auto.
Qed.

Theorem IndAppdR: (L1, L2:dList) (a:rZ) (Ind a L2) ->(Ind a (appd L1 L2)).
Intros L1 L2; Case L1; Case L2; Simpl; Auto.
Intros x H' x0 H'0 a H'1.
Red; Auto.
Generalize appendfInclEq2; Unfold InclEq; Auto.
Intros H'2; LApply (H'2 ? rZlt eqRz);
[Intros H'6; LApply H'6;
   [Intros H'7; Specialize 3 H'7 with ltADec := rZltEDec L1 := x0 L2 := x;
     Intros H'10; Inversion H'10; Clear H'6 | Clear H'6] | Idtac]; Auto.
Qed.

Theorem IndAppdInv:
  (L1, L2:dList) (a:rZ) (Ind a (appd L1 L2)) ->(Ind a L1) \/ (Ind a L2).
Intros L1 L2; Case L1; Case L2; Simpl; Auto.
Unfold InRz; Auto.
Intros x H' x0 H'0 a H'1.
Apply appendfInvEq with ltA := rZlt eqA := eqRz ltADec := rZltEDec; Auto.
Qed.

Definition eqExceptOn :=
   [M1, M2:Mem] [L:dList] (a:rNat) (Maxa:(rlt a maxN)) ~ (Ind (rZPlus a) L) ->
   (eMZ M1 a Maxa)=(eMZ M2 a Maxa).

Theorem eqExceptOnRef:
  (M1, M2:Mem) (L:dList) (eqMem M1 M2) ->(eqExceptOn M1 M2 L).
Unfold eqMem; Intros M1 M2 L0 H'; Red; Auto.
Qed.
Hints Resolve eqExceptOnRef.

Theorem eqExceptOnrTrans:
  (M1, M2, M3:Mem) (L:dList) (eqExceptOn M1 M2 L) -> (eqExceptOn M2 M3 L) ->
  (eqExceptOn M1 M3 L).
Unfold eqExceptOn.
Intros M1 M2 M3 L H' H'0 v Inv H'1.
Rewrite H'; Auto.
Qed.

Definition InclRz := [L1, L2:(list rZ)] (v:rZ) (In v L1) ->(InRz v L2).

Definition InRzComp: (v:rZ) (L:(list rZ)) (InRz v L) ->(InRz (rZComp v) L).
Intros v L H'; Elim H'; Auto.
Intros a b L0 H'0; Red; Auto.
Apply InEqHead; Auto.
Generalize H'0; Case a; Simpl; Auto.
Intros a b L0 H'0 H'1; Red; Auto.
Apply InEqSkip; Auto.
Qed.
Hints Resolve InRzComp.

Definition InRzCompInv: (v:rZ) (L:(list rZ)) (InRz (rZComp v) L) ->(InRz v L).
Intros v L H'; Rewrite (rZCompInvol v); Auto.
Qed.

Theorem InclRzInRz:
  (L1, L2:(list rZ)) (v:rZ) (InclRz L1 L2) -> (InRz v L1) ->(InRz v L2).
Intros L1 L2 v H' H'0; Auto.
Case (In_dec rZDec v L1); Intros InvL1; Auto.
Case (In_dec rZDec (rZComp v) L1); Intros InvL1'; Auto.
Apply InRzCompInv; Auto.
Case (InEqInv v L1); Auto.
Intros H'1; Case InvL1'; Auto.
Qed.

Definition Incld := [L1, L2:dList] (a:rZ) (Ind a L1) ->(Ind a L2).

Theorem eqExceptOnIncl:
  (M1, M2:Mem) (L1, L2:dList) (eqExceptOn M1 M2 L1) -> (Incld L1 L2) ->
  (eqExceptOn M1 M2 L2).
Unfold eqExceptOn Incld; Auto.
Qed.

Theorem eqExceptOnSym:
  (M1, M2:Mem) (L:dList) (eqExceptOn M1 M2 L) ->(eqExceptOn M2 M1 L).
Unfold eqExceptOn; Intros M1 M2 L0 H' v Inv H'0; Auto.
Rewrite H'; Auto.
Qed.
Hints Immediate eqExceptOnSym.

Theorem eqExceptOnAppd:
  (M1, M2, M3:Mem)
  (L1, L2:dList) (eqExceptOn M1 M2 L1) -> (eqExceptOn M2 M3 L2) ->
  (eqExceptOn M1 M3 (appd L1 L2)).
Unfold eqExceptOn; Intros M1 M2 M3 L1 L2 H' H'0; Auto.
Intros a Maxa H'1.
Rewrite H'; Auto.
Apply H'0; Auto.
Red; Intros H'2; Case H'1; Auto.
Apply IndAppdR; Auto.
Red; Intros H'2; Case H'1; Auto.
Apply IndAppdL; Auto.
Qed.

Theorem notrltzero: (r:rZ)~ (rVlt r zero).
Intros r; Red; Intros H'; Absurd (rlt (valRz r) (valRz r)); Auto.
Apply rltTransRnext2 with m := zero; Auto.
Qed.
Hints Resolve notrltzero.

Theorem MaxTrue: (rVlt rZTrue maxN).
Red; Rewrite HmaxN; Auto.
Qed.

Theorem evalMZTrue: (M:Mem)(evalMZ M rZTrue MaxTrue)=rZTrue.
Intros M; Case M; Simpl; Auto.
Intros Ar War; Generalize [s:rZ](wfPd ? Ar zero s MaxTrue War).
Case (getAval maxN vM Ar zero MaxTrue); Auto.
Intros r H'; Absurd (rVlt r zero); Auto.
Qed.

Theorem MaxFalse: (rVlt rZFalse maxN).
Red; Rewrite HmaxN; Auto.
Qed.

Theorem evalMZFalse: (M:Mem)(evalMZ M rZFalse MaxFalse)=rZFalse.
Intros M; Case M; Simpl; Auto.
Intros Ar War; Generalize [s:rZ](wfPd ? Ar zero s MaxFalse War).
Case (getAval maxN vM Ar zero MaxFalse); Auto.
Intros r H'; Absurd (rVlt r zero); Auto.
Qed.

Theorem evalMZComp:
  (M:Mem) (v:rZ) (Maxv:(rVlt v maxN)) (Maxmv:(rVlt (rZComp v) maxN))
  (evalMZ M (rZComp v) Maxmv)=(rZComp (evalMZ M v Maxv)).
Intros M v; Case M; Case v; Unfold evalMZ; Simpl; Auto.
Intros a Ar War Maxv Maxmv.
Rewrite (getAvalIrr maxN vM Ar a a Maxmv Maxv); Auto.
Intros a Ar War Maxv Maxmv.
Rewrite (getAvalIrr maxN vM Ar a a Maxv Maxmv); Auto.
Qed.

Theorem evalMZltOr:
  (M:Mem) (v:rZ) (Maxv:(rVlt v maxN))
  (evalMZ M v Maxv)=v \/ (rZlt (evalMZ M v Maxv) v).
Intros M v; Case M; Case v; Simpl; Auto; Intros a Ar War Maxv;
Generalize [s:rZ](wfPd ? Ar a s Maxv War); Case (getAval maxN vM Ar a Maxv);
Auto; Intros r H'; Auto; Right; Auto.
LApply (H' r); Auto.
Apply rZltEqComp with a := r b := (rZMinus a); Auto.
LApply (H' r); Auto.
Qed.

Theorem evalMZlt:
  (M:Mem) (v:rZ) (Maxv:(rVlt v maxN))(rVlt (evalMZ M v Maxv) maxN).
Intros M v Maxv.
Case (evalMZltOr M v Maxv); Auto.
Intros H'; Rewrite H'; Auto.
Intros H'.
Red; Apply rltTrans with y := (valRz v); Auto.
Qed.
Hints Resolve evalMZlt.

Theorem evalMZInv:
  (M:Mem) (v:rZ) (Maxv:(rVlt v maxN)) (Maxvv:(rVlt (evalMZ M v Maxv) maxN))
  (evalMZ M (evalMZ M v Maxv) Maxvv)=(evalMZ M v Maxv).
Intros M v; Case M; Case v; Intros a Ar War Maxa; Simpl; Auto; Inversion War;
Inversion H0.
Generalize [s, t:rZ](H5 a s t Maxa).
Generalize (refl_equal ? (getAval maxN vM Ar a Maxa));
Pattern -1 (getAval maxN vM Ar a Maxa); Case (getAval maxN vM Ar a Maxa); Auto.
Intros r; Case r; Simpl; Auto.
Intros r0 Eqr0 H' Maxvv.
Generalize [t:rZ](H' (rZPlus r0) t Maxvv); Simpl; Auto.
Case (getAval maxN vM Ar r0 Maxvv); Auto.
Intros r1 H'0; LApply (H'0 r1); Auto.
Intros H'1; Case H'1; Auto.
Intros r0 Eqr0 H' Maxvv.
Generalize [t:rZ](H' (rZMinus r0) t Maxvv); Simpl; Auto.
Case (getAval maxN vM Ar r0 Maxvv); Auto.
Intros r1 H'0; LApply (H'0 r1); Auto.
Intros H'1; Case H'1; Auto.
Simpl; Auto.
Intros l H' H'0 Maxvv.
Rewrite (getAvalIrr maxN vM Ar a a Maxvv Maxa); Auto.
Rewrite H'; Auto.
Generalize [s, t:rZ](H5 a s t Maxa).
Generalize (refl_equal ? (getAval maxN vM Ar a Maxa));
Pattern -1 (getAval maxN vM Ar a Maxa); Case (getAval maxN vM Ar a Maxa); Auto.
Intros r; Case r; Simpl; Auto.
Intros r0 Eqr0 H' Maxvv.
Generalize [t:rZ](H' (rZPlus r0) t Maxvv); Simpl; Auto.
Case (getAval maxN vM Ar r0 Maxvv); Auto.
Intros r1 H'0; LApply (H'0 r1); Auto.
Intros H'1; Case H'1; Auto.
Intros r0 Eqr0 H' Maxvv.
Generalize [t:rZ](H' (rZMinus r0) t Maxvv); Simpl; Auto.
Case (getAval maxN vM Ar r0 Maxvv); Auto.
Intros r1 H'0; LApply (H'0 r1); Auto.
Intros H'1; Case H'1; Auto.
Simpl; Auto.
Intros l H' H'0 Maxvv.
Rewrite (getAvalIrr maxN vM Ar a a Maxvv Maxa); Auto.
Rewrite H'; Auto.
Qed.

Definition getRefList :=
   [M:Mem]
      Cases M of
          (exist Ar _) => (getSubset
                             ? ? Ar [v:vM]
                                       Cases v of
                                           (ref _) => true
                                          | (class _) => false
                                       end)
      end.

Theorem getRefListLt: (M:Mem) (a:rNat) (In a (getRefList M)) ->(rlt a maxN).
Intros M a; Case M; Simpl; Auto.
Intros Ar War H'0.
Apply getSubsetLe with 1 := H'0; Auto.
Qed.

Theorem getRefListProp1:
  (M:Mem) (a:rNat) (Ha:(rlt a maxN)) (In a (getRefList M)) ->
  (rVlt (evalMnat M a Ha) a).
Intros M a Ha; Case M; Simpl; Auto.
Intros Ar War H'0.
Generalize [s:rZ](wfPd ? Ar a s Ha War).
Generalize (getSubsetTestTrue ? ? Ar ? a Ha H'0).
Case (getAval maxN vM Ar a Ha); Auto.
Intros l H'; Discriminate.
Qed.

Theorem getRefListProp2:
  (M:Mem) (a:rNat) (Ha:(rlt a maxN)) ~ a=(valRz (evalMnat M a Ha)) ->
  (In a (getRefList M)).
Intros M a Ha; Case M; Simpl; Auto.
Intros Ar War.
Generalize (getSubsetTestTrueRev
              ? ? Ar [v:vM]
                        Cases v of
                            (ref _) => true
                           | (class _) => false
                        end a Ha).
Case (getAval maxN vM Ar a Ha); Auto.
Intros H' H'0 H'1; Case H'1; Auto.
Qed.

Fixpoint memFaux[L:(list rNat)]:
   (M:Mem) ((n:rNat) (In n L) ->(rlt n maxN)) ->State :=
   <[l:(list rNat)] Mem -> ((n:rNat) (In n l) ->(rlt n maxN)) ->State>Cases L of
       nil => [_:Mem] [_:?](nil rZ * rZ)
      | (cons a l) =>
          [M:Mem] [H'0:?]
          (addEq
             ((rZPlus a), (evalMnat M a (H'0 a (in_eq a l))))
             (memFaux l M [n:rNat] [H:(In n l)](H'0 n (in_cons a H))))
   end.

Theorem memFauxIrr:
  (L1, L2:(list rNat)) L1=L2 ->
  (M:Mem)
  (InM1:(n:rNat) (In n L1) ->(rlt n maxN))
  (InM2:(n:rNat) (In n L2) ->(rlt n maxN))
  (memFaux L1 M InM1)=(memFaux L2 M InM2).
Intros L1; Elim L1; Simpl; Auto.
Intros L2; Case L2; Auto.
Intros r l H'; Discriminate.
Intros a0 l H' L2; Case L2; Simpl; Auto.
Intros H'0; Discriminate.
Intros r l0 H'0 M InM1 InM2.
LApply (H' l0);
[Intros H'2;
   Rewrite (H'2
              M [n:rNat] [H:(In n l)](InM1 n (in_cons a0 H))
              [n:rNat] [H:(In n l0)](InM2 n (in_cons r H))) | Idtac]; Auto.
Inversion H'0; Auto.
Rewrite (evalMnatIrr M a0 r (InM1 a0 (in_eq a0 l)) (InM2 r (in_eq r l0))); Auto.
Rewrite H0; Auto.
Inversion H'0; Auto.
Qed.

Theorem memFauxProp1:
  (a, b:rZ)
  (L:(list rNat))
  (M:Mem)
  (InM:(n:rNat) (In n L) ->(rlt n maxN)) (In (a, b) (memFaux L M InM)) ->
  (rVlt a maxN) /\ ((Maxa:(rVlt a maxN))<rZ> b=(evalMZ M a Maxa)).
Intros a b L; Elim L; Simpl; Auto.
Intros H' H'0 H'1; Elim H'1; Auto.
Intros a0 l H' M InM H'0; Elim H'0; Clear H'0; Intros H'1; Auto.
Inversion H'1; Simpl; Auto.
Split; [Idtac | Intros Maxa]; Auto.
Red; Auto.
Apply H' with 1 := H'1; Auto.
Qed.

Theorem memFauxProp2:
  (a:rNat)
  (Maxa:(rlt a maxN))
  (L:(list rNat)) (M:Mem) (InM:(n:rNat) (In n L) ->(rlt n maxN)) (In a L) ->
  (In ((rZPlus a), (evalMnat M a Maxa)) (memFaux L M InM)).
Intros a Maxa L; Elim L; Simpl; Auto.
Intros a0 l H' M InM H'0; Elim H'0; Clear H'0; Intros H'1; Auto.
Left.
Apply f_equal2 with A1 := rZ A2 := rZ; Auto.
Rewrite H'1; Auto.
Qed.

Theorem memFauxProp3:
  (M1, M2:Mem)
  (L:(list rNat)) (InM:(n:rNat) (In n L) ->(rlt n maxN)) (eqMem M1 M2) ->
  (memFaux L M1 InM)=(memFaux L M2 InM).
Intros M1 M2 L; Elim L; Simpl; Auto.
Intros a l H' InM H'1.
Unfold addEq.
Rewrite (evalMnatEqM M1 M2); Auto.
Rewrite (H' [n:rNat] [H:(In n l)](InM n (in_cons a H))); Auto.
Qed.

Definition memF := [M:Mem](memFaux (getRefList M) M (getRefListLt M)).

Theorem memFProp1:
  (M:Mem) (a, b:rZ) (In (a, b) (memF M)) ->
  (rVlt a maxN) /\ ((Maxa:(rVlt a maxN))<rZ> b=(evalMZ M a Maxa)).
Intros M a b H'.
Apply memFauxProp1 with L := (getRefList M) InM := (getRefListLt M); Auto.
Qed.

Theorem memFProp2:
  (a:rZ) (Maxa:(rVlt a maxN)) (M:Mem) ~ a=(evalMZ M a Maxa) ->
  (In (a, (evalMZ M a Maxa)) (memF M)) \/
  (In ((rZComp a), (rZComp (evalMZ M a Maxa))) (memF M)).
Intros a; Case a; Simpl.
Intros r Maxa M H'; Left.
Unfold memF; Apply memFauxProp2; Auto.
Apply getRefListProp2 with Ha := Maxa; Auto.
Simpl; Red; Intros H'0; Case H'; Auto.
Absurd (rZlt (evalMZ M (rZPlus r) Maxa) (rZPlus r)); Auto.
Simpl; Unfold rZlt; Rewrite <- H'0; Auto.
Case (evalMZltOr M (rZPlus r) Maxa); Auto.
Intros H'1; Case H'; Auto.
Intros r Maxa M H'; Right.
Rewrite rZCompInv; Unfold memF; Apply memFauxProp2; Auto.
Apply getRefListProp2 with Ha := Maxa; Auto.
Simpl; Red; Intros H'0; Case H'; Auto.
Absurd (rZlt (evalMZ M (rZPlus r) Maxa) (rZMinus r)); Auto.
Simpl; Unfold rZlt; Rewrite <- H'0; Auto.
Case (evalMZltOr M (rZMinus r) Maxa); Auto.
Intros H'1; Case H'; Auto.
Simpl; Auto.
Intros H'1.
Apply rZltEqComp with 1 := H'1; Auto.
Qed.

Theorem evalCorrectAux:
  (a, b:rZ) (M:Mem) (eqStateRz (memF M) a b) -> ~ a=b ->
  (rVlt a maxN) /\
  ((rVlt b maxN) /\
   ((Maxa:(rVlt a maxN)) (Maxb:(rVlt b maxN))(evalMZ M a Maxa)=(evalMZ M b Maxb))).
Intros a b M H'; Generalize (memFProp1 M); Elim H'; Auto.
Intros a0 S H'0 H'1; Case H'1; Auto.
Intros a0 b0 S H'0 H'1 H'2.
Elim (H'1 a0 b0); [Intros H'6 H'7 | Idtac]; Auto.
Split; [Idtac | Split; [Idtac | Intros Maxa Maxb]]; Auto.
Rewrite (H'7 H'6); Auto.
Apply sym_equal.
Cut (rVlt (evalMZ M a0 Maxa) maxN); [Intros Max2 | Idtac].
Apply trans_equal with y := (evalMZ M (evalMZ M a0 Maxa) Max2).
Apply evalMZIrr; Auto.
Apply trans_equal with y := (evalMZ M a0 Maxa); Auto.
Apply evalMZInv; Auto.
Apply evalMZlt; Auto.
Intros a0 b0 S H'0 H'1 H'2 H'3.
Elim H'1;
[Intros H'6 H'7; Elim H'7; Intros H'8 H'9; Clear H'7 H'1 | Clear H'1 |
   Clear H'1]; Auto.
Split; [Idtac | Split; [Idtac | Intros Maxa Maxb]]; Auto.
Rewrite (evalMZComp M b0 H'8).
Rewrite <- (H'9 H'6 H'8).
Apply evalMZComp; Auto.
Intros a0 b0 S H'0 H'1 H'2 H'3.
Elim H'1;
[Intros H'6 H'7; Elim H'7; Intros H'8 H'9; Clear H'7 H'1 | Clear H'1 |
   Clear H'1]; Auto.
Intros a0 b0 c S H'0 H'1 H'2 H'3 H'4 H'5.
Case (rZDec b0 c); Intros Eqb0c; Auto.
Rewrite <- Eqb0c in H'5.
Elim H'1;
[Intros H'8 H'9; Elim H'9; Intros H'10 H'11; Clear H'9 H'1 | Clear H'1 |
   Clear H'1]; Auto.
Split; [Idtac | Split; [Idtac | Intros Maxa Maxb]]; Auto.
Rewrite <- Eqb0c; Auto.
Apply trans_equal with y := (evalMZ M b0 H'10); Auto.
Case (rZDec a0 b0); Intros Eqa0b0; Auto.
Rewrite Eqa0b0 in H'5.
Elim H'3;
[Intros H'8 H'9; Elim H'9; Intros H'10 H'11; Clear H'9 H'3 | Clear H'3 |
   Clear H'3]; Auto.
Split; [Idtac | Split; [Idtac | Intros Maxa Maxb]]; Auto.
Rewrite Eqa0b0; Auto.
Apply trans_equal with y := (evalMZ M b0 H'8); Auto.
Elim H'3;
[Intros H'8 H'9; Elim H'9; Intros H'10 H'11; Clear H'9 H'3 | Clear H'3 |
   Clear H'3]; Auto.
Elim H'1;
[Intros H'7 H'9; Elim H'9; Intros H'12 H'13; Clear H'9 H'1 | Clear H'1 |
   Clear H'1]; Auto.
Split; [Idtac | Split; [Idtac | Intros Maxa Maxb]]; Auto.
Apply trans_equal with y := (evalMZ M b0 H'12); Auto.
Intros a0 b0 c S H'0 H'1 H'2 H'3.
Elim H'1;
[Intros H'6 H'7; Elim H'7; Intros H'8 H'9; Clear H'7 H'1 | Clear H'1 |
   Clear H'1]; Auto.
Absurd <rZ> (evalMZ M a0 H'6)=(evalMZ M (rZComp a0) H'8); Auto.
Rewrite (evalMZComp M a0 H'6 H'8); Auto.
Qed.

Theorem memFNotContradictory: (M:Mem)~ (contradictory (memF M)).
Intros M; Red; Intros H'; Red in H'; Auto.
Elim H'; Intros a E; Clear H'.
Elim (evalCorrectAux a (rZComp a) M);
[Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Clear H'5 | Idtac | Idtac]; Auto.
Absurd (evalMZ M a H'4)=(evalMZ M (rZComp a) H'6); Auto.
Rewrite (evalMZComp M a H'4 H'6); Auto.
Qed.
Hints Immediate memFNotContradictory.

Theorem evalCorrect:
  (M:Mem)
  (a, b:rZ)
  (Maxa:(rVlt a maxN)) (Maxb:(rVlt b maxN)) (eqStateRz (memF M) a b) ->
  (evalMZ M a Maxa)=(evalMZ M b Maxb).
Intros M a b Maxa Maxb H'.
Case (rZDec a b); Intros Eqab.
Apply evalMZIrr; Auto.
Elim (evalCorrectAux a b M);
[Intros H'5 H'6; Elim H'6; Intros H'7 H'8; Apply H'8; Clear H'6 | Idtac | Idtac];
Auto.
Qed.

Theorem evalEq:
  (M:Mem) (a:rZ) (Maxa:(rVlt a maxN))(eqStateRz (memF M) a (evalMZ M a Maxa)).
Intros M a Maxa; Case (rZDec a (evalMZ M a Maxa)); Intros Eqaeva; Auto.
Rewrite <- Eqaeva; Auto.
Case (memFProp2 a Maxa M); Auto; Intros H'3.
Apply eqStateInvInv; Auto.
Qed.
Hints Immediate evalEq.

Theorem evalCorrectComp:
  (M:Mem)
  (a, b:rZ)
  (Maxa:(rVlt a maxN)) (Maxb:(rVlt b maxN)) (eqStateRz (memF M) a (rZComp b)) ->
  (evalMZ M a Maxa)=(rZComp (evalMZ M b Maxb)).
Intros M a b Maxa Maxb H'.
Rewrite <- (evalMZComp M b Maxb (rVltrZComp ? ? Maxb)); Auto.
Apply evalCorrect; Auto.
Qed.

Theorem evalInv:
  (M:Mem)
  (a, b:rZ)
  (Maxa:(rVlt a maxN))
  (Maxb:(rVlt b maxN)) (evalMZ M a Maxa)=(evalMZ M b Maxb) ->
  (eqStateRz (memF M) a b).
Intros M a b Maxa Maxb H'.
Apply eqStateRzTrans with b := (evalMZ M a Maxa); Auto.
Rewrite H'; Auto.
Apply eqStateRzSym; Auto.
Qed.
Hints Immediate evalInv.

Theorem evalInvComp:
  (M:Mem)
  (a, b:rZ)
  (Maxa:(rVlt a maxN))
  (Maxb:(rVlt b maxN)) (evalMZ M a Maxa)=(rZComp (evalMZ M b Maxb)) ->
  (eqStateRz (memF M) a (rZComp b)).
Intros M a b Maxa Maxb H'.
Apply evalInv with Maxa := Maxa Maxb := (rVltrZComp ? ? Maxb); Auto.
Rewrite H'; Auto.
Apply sym_equal.
Apply evalCorrectComp; Auto.
Qed.

Definition notDnil: dList ->Prop :=
   [D:dList]
      Cases D of
          (exist (cons _ _) _) => True
         | _ => False
      end.

Definition dNil: dList.
Exists (nil rZ); Split; Auto.
Red; Auto.
Apply OlistNil; Auto.
Intros a H'; Elim H'; Auto.
Defined.

Theorem isDnil0: ~ (notDnil dNil).
Simpl; Auto.
Qed.

Theorem isDnilAppdL: (L1, L2:dList) (notDnil L1) ->(notDnil (appd L1 L2)).
Intros L1 L2; Case L1; Case L2; Simpl; Auto.
Intros x H' x0; Case x0; Simpl; Auto.
Intros H'0 H'1; Elim H'1; Auto.
Intros r l H'0 H'1; Generalize (appendfInclEq1 ? ? ? rZltEDec (cons r l) x); Auto.
Unfold appendRz; Case (appendf rZ rZlt eqRz rZltEDec (cons r l) x); Auto.
Intros H'2; Inversion H'2; Auto.
LApply (H r); Simpl; [Intros H'3; Inversion H'3 | Apply InEqHead]; Auto.
Qed.

Theorem isDnilAppdR: (L1, L2:dList) (notDnil L2) ->(notDnil (appd L1 L2)).
Intros L1 L2; Case L1; Case L2; Simpl; Auto.
Intros x H' x0; Case x; Simpl; Auto.
Intros H'0 H'1; Elim H'1.
Intros r l H'0 H'1;
Generalize (appendfInclEq2 ? ? ? eqrZSym eqrZTrans rZltEDec x0 (cons r l)); Auto.
Unfold appendRz; Case (appendf rZ rZlt eqRz rZltEDec x0 (cons r l)); Auto.
Intros H'2; Inversion H'2; Auto.
LApply (H r); Simpl; [Intros H'3; Inversion H'3 | Apply InEqHead]; Auto.
Qed.

Theorem isDnilAppdInv:
  (L1, L2:dList) (notDnil (appd L1 L2)) ->(notDnil L1) \/ (notDnil L2).
Intros L1 L2; Case L1; Case L2; Simpl; Auto.
Intros x H' x0; Case x; Simpl; Auto; Case x0; Auto.
Generalize (appendfAppend ? ? ? rZltEDec (nil rZ) (nil rZ)).
Unfold appendRz; Intros H'0; Inversion H'0; Auto.
Qed.

Definition idDnilP: (d:dList){(notDnil d)}+{~ (notDnil d)}.
Intros d; Case d.
Intros x; Case x; Simpl; Auto.
Defined.

Definition listDec:
  (A:Set) (eqDec:(a, b:A){a=b}+{~ a=b}) (L1, L2:(list A)){L1=L2}+{~ L1=L2}.
Intros A eqDec L1; Elim L1.
Intros L2; Case L2; Auto.
Intros a l; Right; Red; Intros H'0; Discriminate.
Intros a l Rec L2; Case L2; Auto.
Right; Red; Intros H'1; Discriminate.
Intros a0 l0; Case (eqDec a a0).
Intros H'; Rewrite <- H'; Auto.
Case (Rec l0); Intros H'0.
Rewrite <- H'0; Auto.
Right; Red; Intros H'1; Inversion H'1; Auto.
Intros H'; Right; Red; Intros H'0; Case H'; Inversion H'0; Auto.
Qed.

Definition vMDec: (a, b:vM){a=b}+{~ a=b}.
Intros a b; Case a; Case b; Try (Intros; Right; Red; Intros; Discriminate; Fail).
Intros r r0; Case (rZDec r r0); Intros Eq1.
Rewrite <- Eq1; Auto.
Right; Red; Intros H'; Case Eq1; Inversion H'; Auto.
Intros l l0; Case (listDec ? rZDec l0 l); Intros Eq1.
Rewrite <- Eq1; Auto.
Right; Red; Intros H'; Case Eq1; Inversion H'; Auto.
Defined.

Definition findNeqAux:
  (M1, M2:Mem) (L:(list rNat)) ((a:rNat) (In a L) ->(rlt a maxN)) ->
  {q:(Option rNat) | Cases q of
                         (Some a) =>
                           (rlt a maxN) /\
                           ((Ha:(rlt a maxN))~ (eMZ M1 a Ha)=(eMZ M2 a Ha))
                        | _ =>
                            (a:rNat) (Ha:(rlt a maxN)) (In a L) ->
                            (eMZ M1 a Ha)=(eMZ M2 a Ha)
                     end}.
Intros M1 M2 L; Elim L; Auto.
Intros H; Exists (None rNat).
Intros a Ha H'0; Inversion H'0; Auto.
Intros a l H'0 H'1.
Cut (rlt a maxN); [Intros Ha | Auto with datatypes].
Case (vMDec (eMZ M1 a Ha) (eMZ M2 a Ha)); Intros Eq1.
Case H'0; Auto with datatypes.
Intros x; Case x; Auto.
Intros a H'; Elim H'; Clear H'; Intros H' H'1.
Exists (Some ? a0); Split; Auto.
Intros H'; Exists (None rNat); Simpl; Auto.
Intros a0 Ha0 H'2; Elim H'2; Clear H'2; Intros H'2; Auto.
Repeat Rewrite [M1:Mem](eMZIrr M1 a0 a Ha0 Ha); Auto.
Exists (Some ? a); Split; Auto.
Intros Ha0; Red; Intros H'; Case Eq1; Auto.
Repeat Rewrite [M1:Mem](eMZIrr M1 a a Ha Ha0); Auto.
Defined.

Definition findNeq: (M1, M2:Mem){q:(Option rNat) | Cases q of
                                                       (Some a) =>
                                                         (rlt a maxN) /\
                                                         ((Ha:(rlt a maxN))
                                                          ~ (eMZ M1 a Ha)=
                                                            (eMZ M2 a Ha))
                                                      | _ => (eqMem M1 M2)
                                                   end}.
Intros M1 M2; Case (findNeqAux M1 M2 (rZList maxN)).
Exact [a:rNat](InrZList a maxN).
Intros x; Case x; Auto.
Intros a H'; Elim H'; Clear H'; Intros H' H'0.
Exists (Some ? a); Split; Auto.
Intros H'; Exists (None rNat); Red; Auto.
Intros a Maxa.
Apply H'; Auto.
Apply rZListIn; Auto.
Defined.

Theorem evalMzMin:
  (M:Mem)
  (a:rNat)
  (b, c:rZ)
  (Ha:(rlt a maxN)) (Hc:(rVlt c maxN)) (evalMnat M a Ha)=b -> (rZlt c b) ->
  ~ (evalMnat M a Ha)=(evalMZ M c Hc).
Intros M; Case M; Simpl; Auto.
Intros Ar War a b c Ha.
Generalize (refl_equal ? (getAval maxN vM Ar a Ha));
Pattern -1 (getAval maxN vM Ar a Ha); Case (getAval maxN vM Ar a Ha).
Case c; Simpl; Auto.
Intros c' a' H' Hc H'0 H'1.
Generalize (refl_equal ? (getAval maxN vM Ar c' Hc));
Pattern -1 (getAval maxN vM Ar c' Hc); Case (getAval maxN vM Ar c' Hc).
Intros r H'2; Red; Intros H'3; Rewrite <- H'3 in H'2.
Absurd (rVlt a' c'); Auto.
Rewrite H'0; Auto.
Unfold rVlt; Apply rltAntiSym; Auto.
Apply wfPd with n := maxN Ar := Ar Hr := Hc; Auto.
Intros l H'2; Red; Intros H'3; Rewrite H'3 in H'.
Generalize H'1; Rewrite <- H'0; Rewrite H'3; Auto.
Change ~ (rlt c' c'); Auto.
Intros c' a' H' Hc H'0 H'1.
Generalize (refl_equal ? (getAval maxN vM Ar c' Hc));
Pattern -1 (getAval maxN vM Ar c' Hc); Case (getAval maxN vM Ar c' Hc).
Intros r H'2; Red; Intros H'3.
Absurd (rVlt (rZComp a') c'); Auto.
Rewrite H'0; Auto.
Unfold rVlt; Apply rltAntiSym; Auto.
Generalize H'1; Case b; Simpl; Auto.
Rewrite H'3; Rewrite <- rZCompInvol; Auto.
Apply wfPd with n := maxN Ar := Ar Hr := Hc; Auto.
Simpl; Auto.
Intros l H'2; Red; Intros H'3.
Generalize H'1; Rewrite <- H'3; Rewrite H'0; Auto.
Change ~ (rZlt b b); Auto.
Case c; Simpl; Auto.
Intros c' a' H' Hc H'0 H'1.
Generalize (refl_equal ? (getAval maxN vM Ar c' Hc));
Pattern -1 (getAval maxN vM Ar c' Hc); Case (getAval maxN vM Ar c' Hc).
Intros r H'2; Red; Intros H'3; Rewrite <- H'3 in H'2.
Absurd (rVlt (rZPlus a) c'); Auto.
Rewrite H'0; Auto.
Unfold rVlt; Apply rltAntiSym; Auto.
Apply wfPd with n := maxN Ar := Ar Hr := Hc; Auto.
Intros l H'2; Red; Intros H'3; Inversion H'3.
Generalize H'1; Rewrite <- H0; Rewrite <- H'0; Auto.
Change ~ (rlt a a); Auto.
Intros c' a' H' Hc H'0 H'1.
Generalize (refl_equal ? (getAval maxN vM Ar c' Hc));
Pattern -1 (getAval maxN vM Ar c' Hc); Case (getAval maxN vM Ar c' Hc).
Intros r H'2; Red; Intros H'3.
Absurd (rVlt (rZPlus a) c'); Auto.
Rewrite H'0; Auto.
Unfold rVlt; Apply rltAntiSym; Auto.
Rewrite H'3; Auto.
Apply rVltrZComp.
Apply wfPd with n := maxN Ar := Ar Hr := Hc; Auto.
Simpl; Intros l H'2; Red; Intros H'3; Try Exact H'3.
Generalize H'1; Rewrite <- H'3; Rewrite H'0; Auto.
Change ~ (rZlt b b); Auto.
Qed.

Theorem eMZevalMnat:
  (M:Mem) (a:rNat) (Ha:(rlt a maxN))(evalMnat M a Ha)=(Cases (eMZ M a Ha) of
                                                           (ref b) => b
                                                          | (class l) =>
                                                              (rZPlus a)
                                                       end).
Intros M; Case M; Simpl; Auto.
Qed.

Theorem eMZlt:
  (M:Mem) (a:rNat) (b:rZ) (Ha:(rlt a maxN)) (eMZ M a Ha)=(ref b) ->(rVlt b a).
Intros M; Case M; Simpl; Auto.
Intros Ar War a b Ha H'0.
Apply wfPd with n := maxN Ar := Ar Hr := Ha; Auto.
Qed.

Theorem eMZOlist:
  (M:Mem) (a:rNat) (L:(list rZ)) (Ha:(rlt a maxN)) (eMZ M a Ha)=(class L) ->
  (OlistRz L).
Intros M; Case M; Simpl; Auto.
Intros Ar War a b Ha H'0.
Apply wfOl with n := maxN Ar := Ar r := a Hr := Ha; Auto.
Qed.

Theorem eMZlt':
  (M:Mem)
  (a:rNat)
  (b:rZ) (L:(list rZ)) (Ha:(rlt a maxN)) (eMZ M a Ha)=(class L) -> (InRz b L) ->
  (rVlt b maxN).
Intros M; Case M; Simpl; Auto.
Intros Ar War a b L Ha H'0 H'1.
Apply wellFormedArrayInRzLt with Ar := Ar a := a Ha := Ha La := L; Auto.
Qed.

Theorem eMZref:
  (M:Mem)
  (a:rNat)
  (b:rZ)
  (L:(list rZ))
  (Ha:(rlt a maxN)) (Hb:(rVlt b maxN)) (eMZ M a Ha)=(class L) -> (In b L) ->
  (eMZ M (valRz b) Hb)=(ref (samePol b a)).
Intros M; Case M; Simpl; Auto.
Intros Ar War a b L Ha Hb H'0 H'1.
Apply wfPcc1 with Hr := Ha Lr := L; Auto.
Qed.

Theorem eMZNref:
  (M:Mem)
  (a:rNat)
  (b:rZ)
  (L:(list rZ))
  (Ha:(rlt a maxN)) (Hb:(rVlt b maxN)) (eMZ M a Ha)=(class L) -> ~ (In b L) ->
  ~ (eMZ M (valRz b) Hb)=(ref (samePol b a)).
Intros M; Case M; Simpl; Auto.
Intros Ar War a b L Ha Hb H'0 H'1; Red; Intros H'2.
Case H'1.
Cut (samePol (samePol b a) (valRz b))=b.
2:Case b; Simpl; Auto.
Intros H'3; Rewrite <- H'3; Auto.
Cut (rlt (valRz (samePol b a)) maxN); [Intros Ha' | Case b]; Auto.
Apply wfPcc2 with n := maxN Ar := Ar Hr := Hb Hs := Ha'; Auto.
Rewrite <- H'0; Auto.
Apply getAvalIrr; Auto.
Case b; Auto.
Qed.

Definition findDiff:
  (M1, M2:Mem) ~ (eqMem M1 M2) ->
  {a:rNat |
    (rlt a maxN) /\ ((Ha:(rlt a maxN))~ (evalMnat M1 a Ha)=(evalMnat M2 a Ha))}.
Intros M1 M2 H'; Case (findNeq M1 M2).
Intros x; Case x; Auto.
2:Intros H'0; Absurd True; Auto; Case H'; Auto.
Intros a H'0; Elim H'0; Clear H'0; Intros Ha H'1; Generalize (H'1 Ha); Clear H'1.
Generalize (refl_equal ? (eMZ M1 a Ha)); Pattern -1 (eMZ M1 a Ha);
Case (eMZ M1 a Ha); Generalize (refl_equal ? (eMZ M2 a Ha));
Pattern -1 (eMZ M2 a Ha); Case (eMZ M2 a Ha).
Intros a'' H'0 a' H'1 H'2; Exists a; Split; Auto.
Intros Ha0; Red.
Repeat (Rewrite [M1:Mem](evalMnatIrr M1 a a Ha0 Ha); Auto).
Repeat Rewrite eMZevalMnat; Auto.
Rewrite H'1; Rewrite H'0; Auto.
Intros H'3; Case H'2; Rewrite H'3; Auto.
Intros l H'0 r H'1 H'2; Exists a; Split; Auto.
Intros Ha0; Red.
Repeat (Rewrite [M1:Mem](evalMnatIrr M1 a a Ha0 Ha); Auto).
Repeat Rewrite eMZevalMnat; Auto.
Rewrite H'1; Rewrite H'0; Auto.
Intros H'3; Absurd (rVlt r a); Auto.
Rewrite H'3; Unfold rVlt; Auto.
Apply eMZlt with M := M1 Ha := Ha; Auto.
Intros r H'0 l H'1 H'2; Exists a; Split; Auto.
Intros Ha0; Red.
Repeat (Rewrite [M1:Mem](evalMnatIrr M1 a a Ha0 Ha); Auto).
Repeat Rewrite eMZevalMnat; Auto.
Rewrite H'1; Rewrite H'0; Auto.
Intros H'3; Absurd (rVlt r a); Auto.
Rewrite <- H'3; Unfold rVlt; Auto.
Apply eMZlt with M := M2 Ha := Ha; Auto.
Intros l H'0 l0 H'1 H'2.
Case (olistDiff ? rZlt) with eqA := (eq rZ) L1 := l L2 := l0; Auto;
Try (Red; Auto).
Intros x0 y z H'3; Rewrite H'3; Auto.
Intros a0 b H'3 H'4; Generalize H'3; Rewrite H'4; Auto.
Change ~ (rZlt b b); Auto.
Intros a0 b c d H'3 H'4 H'5; Rewrite <- H'4; Rewrite <- H'5; Auto.
Exact rZDec; Auto.
Apply eMZOlist with M := M2 a := a Ha := Ha; Auto.
Apply eMZOlist with M := M1 a := a Ha := Ha; Auto.
Intros H'3; Case H'2; Elim H'3; Auto.
Intros a0 b L1 L2 H'4 H'5 H'6; Rewrite H'4; Inversion H'6; Auto.
Intros c H'3; Exists (valRz c); Split; Auto.
Change (rVlt c maxN); Auto.
Elim H'3; Clear H'3; Intros H'3; Elim H'3; Clear H'3; Intros H'3 H'4.
Apply eMZlt' with M := M2 a := a L := l Ha := Ha; Auto.
Elim H'3; Auto.
Intros a0 b L H'5; Rewrite H'5; Auto.
Red; Apply InEqHead; Auto.
Intros a0 b L H'5 H'6; Red; Apply InEqSkip; Auto.
Apply eMZlt' with M := M1 a := a L := l0 Ha := Ha; Auto.
Elim H'4; Auto.
Intros a0 b L H'5; Rewrite H'5; Auto.
Red; Apply InEqHead; Auto.
Intros a0 b L H'5 H'6; Red; Apply InEqSkip; Auto.
Intros Ha0; Red; Intros H'4.
Elim H'3; Clear H'3; Intros H'3; Elim H'3; Clear H'3; Intros H'3 H'4.
Generalize H'4.
Rewrite (eMZevalMnat M2).
Rewrite (eMZref M2 a c l Ha Ha0); Auto.
Intros H'6.
Cut (rlt a (valRz c)); [Intros Hc | Idtac].
Absurd (eMZ M1 (valRz c) Ha0)=(ref (samePol c a)); Auto.
Apply eMZNref with L := l0 Ha := Ha; Auto.
Red; Intros H'7; Case H'5; Auto.
Apply inImpInEq; Auto.
Red; Auto; Auto.
Generalize H'6; Auto.
Rewrite eMZevalMnat; Auto.
Case (eMZ M1 (valRz c) Ha0); Auto.
Intros r H'7; Rewrite H'7; Auto.
Intros l1 H'7; Absurd (rZlt (rZPlus a) (rZPlus (valRz c))); Auto.
Rewrite H'7; Case c; Simpl; Unfold rZlt; Auto.
Cut (rVlt (samePol c a) (valRz c)); [Case c | Idtac]; Auto.
Apply eMZlt with M := M2 Ha := Ha0; Auto.
Apply eMZref with L := l Ha := Ha; Auto.
Elim H'3; Auto with datatypes.
Intros a0 b L H'8; Rewrite H'8; Auto with datatypes.
Elim H'3; Auto with datatypes.
Intros a0 b L H'8; Rewrite H'8; Auto with datatypes.
Generalize H'4.
Rewrite (eMZevalMnat M1).
Rewrite (eMZref M1 a c l0 Ha Ha0); Auto.
Intros H'6.
Cut (rlt a (valRz c)); [Intros Hc | Idtac].
Absurd (eMZ M2 (valRz c) Ha0)=(ref (samePol c a)); Auto.
Apply eMZNref with L := l Ha := Ha; Auto.
Red; Intros H'7; Case H'3; Auto.
Apply inImpInEq; Auto.
Red; Auto; Auto.
Generalize H'6; Auto.
Rewrite eMZevalMnat; Auto.
Case (eMZ M2 (valRz c) Ha0); Auto.
Intros r H'7; Rewrite H'7; Auto.
Intros l1 H'7; Absurd (rZlt (rZPlus a) (rZPlus (valRz c))); Auto.
Rewrite <- H'7; Case c; Simpl; Unfold rZlt; Auto.
Cut (rVlt (samePol c a) (valRz c)); [Case c | Idtac]; Auto.
Apply eMZlt with M := M1 Ha := Ha0; Auto.
Apply eMZref with L := l0 Ha := Ha; Auto.
Elim H'5; Auto with datatypes.
Intros a0 b L H'8; Rewrite H'8; Auto with datatypes.
Elim H'5; Auto with datatypes.
Intros a0 b L H'8; Rewrite H'8; Auto with datatypes.
Qed.

Definition findDiffF: (M1, M2:Mem) ~ (eqMem M1 M2) ->{ab:rZ * rZ | Cases ab of
                                                                       (pair
                                                                          a b)
                                                                         =>
                                                                         (rVlt
                                                                            a
                                                                            maxN)
                                                                         /\
                                                                         ((rVlt
                                                                             b
                                                                             maxN)
                                                                          /\
                                                                          ((Ha:(rVlt
                                                                                  a
                                                                                  maxN))
                                                                           (Hb:(rVlt
                                                                                  b
                                                                                  maxN))
                                                                           (evalMZ
                                                                              M1
                                                                              a
                                                                              Ha)=
                                                                           (evalMZ
                                                                              M1
                                                                              b
                                                                              Hb)
                                                                           /\
                                                                           ~ (evalMZ
                                                                                M2
                                                                                a
                                                                                Ha)=
                                                                             (evalMZ
                                                                                M2
                                                                                b
                                                                                Hb)
                                                                           \/
                                                                           ~ (evalMZ
                                                                                M1
                                                                                a
                                                                                Ha)=
                                                                             (evalMZ
                                                                                M1
                                                                                b
                                                                                Hb)
                                                                           /\
                                                                           (evalMZ
                                                                              M2
                                                                              a
                                                                              Ha)=
                                                                           (evalMZ
                                                                              M2
                                                                              b
                                                                              Hb)))
                                                                   end}.
Intros M1 M2 H'.
Case (findDiff M1 M2 H'); Auto.
Intros c H'0; Elim H'0; Intros H'1 H'2; Clear H'0.
Case (rZltEDec (evalMnat M1 c H'1) (evalMnat M2 c H'1)); Auto.
Intros s; Case s.
Intros H'0.
Exists ((rZPlus c), (evalMnat M1 c H'1)); Auto.
Repeat Split; Auto.
Replace (evalMnat M1 c H'1) with (evalMZ M1 (rZPlus c) H'1); Auto.
Intros Ha Hb; Left; Split; Auto.
Apply sym_equal.
Cut (rVlt (evalMZ M1 (rZPlus c) Ha) maxN); [Intros Hb' | Simpl]; Auto.
Rewrite <- (evalMZInv M1 (rZPlus c) Ha Hb'); Simpl; Auto.
Rewrite (evalMnatIrr M1 c c Ha H'1); Auto.
Simpl; Apply evalMzMin with b := (evalMnat M2 c H'1); Auto.
Intros H'0.
Exists ((rZPlus c), (evalMnat M2 c H'1)); Auto.
Repeat Split; Auto.
Replace (evalMnat M2 c H'1) with (evalMZ M2 (rZPlus c) H'1); Auto.
Intros Ha Hb; Right; Split; Auto.
Simpl; Apply evalMzMin with b := (evalMnat M1 c H'1); Auto.
Apply sym_equal.
Cut (rVlt (evalMZ M2 (rZPlus c) Ha) maxN); [Intros Hb' | Simpl]; Auto.
Rewrite <- (evalMZInv M2 (rZPlus c) Ha Hb'); Simpl; Auto.
Rewrite (evalMnatIrr M2 c c Ha H'1); Auto.
Intros H'0; Exists ((rZPlus c), (evalMnat M1 c H'1)).
Repeat Split; Auto.
Replace (evalMnat M1 c H'1) with (evalMZ M1 (rZPlus c) H'1); Auto.
Intros Ha Hb; Left; Split; Auto.
Apply sym_equal.
Cut (rVlt (evalMZ M1 (rZPlus c) Ha) maxN); [Intros Hb' | Simpl]; Auto.
Rewrite <- (evalMZInv M1 (rZPlus c) Ha Hb'); Simpl; Auto.
Rewrite (evalMnatIrr M1 c c Ha H'1); Auto.
Case (rZSignDec (evalMnat M1 c H'1) (evalMnat M2 c H'1)); Auto.
Intros s; Case s; Auto.
Intros H'3; Case (H'2 H'1); Auto.
Intros H'3.
Cut (rVlt (rZComp (evalMnat M2 c H'1)) maxN); [Intros Hb' | Simpl]; Auto.
Rewrite (evalMZIrr M2 (evalMnat M1 c H'1) (rZComp (evalMnat M2 c H'1)) Hb Hb');
Auto.
Cut (rVlt (evalMnat M2 c H'1) maxN); [Intros Hb'' | Simpl]; Auto.
Rewrite (evalMZComp M2 (evalMnat M2 c H'1) Hb'' Hb'); Auto.
Rewrite (evalMZIrr M2 (rZPlus c) (rZPlus c) Ha H'1); Auto.
Rewrite <- (evalMZInv M2 (rZPlus c) H'1 Hb''); Simpl; Auto.
Generalize Hb'; Case (evalMnat M2 c H'1); Auto.
Rewrite <- H'3; Auto.
Qed.

Definition ltMem := [M1, M2:Mem](ltState (rZList maxN) (memF M1) (memF M2)).

Theorem MemLtMem:
  (M1, M2:Mem) (inclState (memF M1) (memF M2)) -> ~ (eqMem M1 M2) ->
  (ltMem M2 M1).
Intros M1 M2 H' H'0; Red; Auto.
Case (findDiffF M1 M2 H'0).
Intros x; Case x.
Intros a b H'1; Elim H'1; Clear H'1; Intros Ha H'1; Elim H'1; Clear H'1;
Intros Hb H'1; Elim (H'1 Ha Hb); Clear H'1; Intros H'1; Elim H'1; Clear H'1;
Intros H'1 H'2.
Case H'2.
Apply evalCorrect; Auto.
Apply eqStateIncl with S1 := (memF M1); Auto.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Apply ltStateLt with a := a b := b; Auto.
Apply rZListIn; Auto.
Apply rZListIn; Auto.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Red; Intros H'3; Case H'1; Auto.
Apply evalCorrect; Auto.
Qed.

Theorem getRefListEq:
  (M1, M2:Mem) (eqMem M1 M2) ->(getRefList M1)=(getRefList M2).
Intros M1 M2; Case M1; Case M2; Unfold eqMem; Simpl.
Intros Ar1 War1 Ar2 War2 EqM1M2.
Apply getSubsetIrr; Auto.
Qed.

Theorem eqMemEqState:
  (M1, M2:Mem) (eqMem M1 M2) ->(eqState (memF M1) (memF M2)).
Unfold memF.
Intros M1 M2 H'.
LApply (memFauxIrr (getRefList M1) (getRefList M2));
[Intros H'2; Rewrite (H'2 M1 (getRefListLt M1) (getRefListLt M2)) | Idtac];
Auto.
Rewrite (memFauxProp3 M1 M2); Auto.
Apply getRefListEq; Auto.
Qed.

Theorem ltMemEqComp:
  (M1, M2, M3, M4:Mem) (eqMem M1 M2) -> (eqMem M3 M4) -> (ltMem M1 M3) ->
  (ltMem M2 M4).
Unfold ltMem; Intros M1 M2 M3 M4 H' H'0 H'1.
Apply ltStateEqComp with S1 := (memF M1) S2 := (memF M3); Auto.
Apply eqMemEqState; Auto.
Apply eqMemEqState; Auto.
Qed.

Theorem ltMemTrans: (transitive Mem ltMem).
Red; Unfold ltMem; Auto.
Intros x y z H' H'0; Apply (ltStateTrans (rZList maxN)) with y := (memF y); Auto.
Qed.

Definition nEq := [M1, M2:Mem] [L:dList] (notDnil L) ->~ (eqMem M1 M2).

Theorem nEqRef: (M1, M2:Mem)(nEq M1 M2 dNil).
Intros M1 M2; Red; Auto.
Qed.

Theorem nEqSym: (M1, M2:Mem) (L:dList) (nEq M1 M2 L) ->(nEq M2 M1 L).
Intros M1 M2; Red; Auto.
Intros L H' H'0; Red; Intros H'1; Case H'; Auto.
Apply eqMemSym; Auto.
Qed.

Theorem nEqWeak:
  (M1, M2:Mem) (L1, L2:dList) ((notDnil L1) ->(notDnil L2)) -> (nEq M1 M2 L2) ->
  (nEq M1 M2 L1).
Unfold nEq; Auto.
Qed.

Theorem nEqInclL:
  (L:dList)
  (M1, M2, M3:Mem)
  (inclState (memF M1) (memF M2)) ->
  (inclState (memF M2) (memF M3)) -> (nEq M1 M2 L) ->(nEq M1 M3 L).
Unfold nEq.
Intros L M1 M2 M3 H' H'0 H'1 H'2; Red; Intros H'3.
Case (findDiffF M1 M2 (H'1 H'2)).
Intros x; Case x; Auto.
Intros a b H'4; Elim H'4; Clear H'4; Intros Ha H'4; Elim H'4; Clear H'4;
Intros Hb H'4; Elim (H'4 Ha Hb); Clear H'4; Intros H'4; Elim H'4; Clear H'4;
Intros H'4 H'5.
Case H'5.
Apply evalCorrect; Auto.
Apply eqStateIncl with S1 := (memF M1); Auto.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Case H'4.
Apply evalCorrect; Auto.
Apply eqStateEq with S1 := (memF M3); Auto.
Apply eqMemEqState; Auto.
Apply eqMemSym; Auto.
Apply eqStateIncl with S1 := (memF M2); Auto.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Qed.

Theorem nEqInclR:
  (L:dList)
  (M1, M2, M3:Mem)
  (inclState (memF M1) (memF M2)) ->
  (inclState (memF M2) (memF M3)) -> (nEq M2 M3 L) ->(nEq M1 M3 L).
Unfold nEq.
Intros L M1 M2 M3 H' H'0 H'1 H'2; Red; Intros H'3.
Case (findDiffF M2 M3 (H'1 H'2)).
Intros x; Case x; Auto.
Intros a b H'4; Elim H'4; Clear H'4; Intros Ha H'4; Elim H'4; Clear H'4;
Intros Hb H'4; Elim (H'4 Ha Hb); Clear H'4; Intros H'4; Elim H'4; Clear H'4;
Intros H'4 H'5.
Case H'5.
Apply evalCorrect; Auto.
Apply eqStateIncl with S1 := (memF M2); Auto.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Case H'4.
Apply evalCorrect; Auto.
Apply eqStateIncl with S1 := (memF M1); Auto.
Apply eqStateEq with S1 := (memF M3); Auto.
Apply eqMemEqState; Auto.
Apply eqMemSym; Auto.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Qed.

Theorem nEqAppd:
  (M1, M2, M3:Mem)
  (L1, L2:dList)
  (inclState (memF M1) (memF M2)) ->
  (nEq M1 M2 L1) -> (inclState (memF M2) (memF M3)) -> (nEq M2 M3 L2) ->
  (nEq M1 M3 (appd L1 L2)).
Intros M1 M2 M3 L1 L2 H' H'0 H'1 H'2.
Case (idDnilP (appd L1 L2)); Auto.
2:Intros H'3; Red.
2:Intros H'4; Case H'3; Auto.
Intros H'3; Case (isDnilAppdInv ? ? H'3); Intros H'4.
Apply nEqWeak with L2 := L1; Auto.
Apply nEqInclL with M2 := M2; Auto.
Apply nEqWeak with L2 := L2; Auto.
Apply nEqInclR with M2 := M2; Auto.
Qed.

Theorem WarCompEq:
  (n:rNat)
  (Ar1, Ar2:(Array n vM))
  ((a:rNat) (Ha:(rlt a n))(getAval n vM Ar1 a Ha)=(getAval n vM Ar2 a Ha)) ->
  (wellFormedArray n Ar1) ->(wellFormedArray n Ar2).
Intros n Ar1 Ar2 H' War1; Inversion War1.
Apply wellFormedArrayDef; Auto.
Apply pointerDecreaseDef; Auto.
Intros r s Hr; Rewrite <- H'; Inversion H; Auto.
Intros H'0; Apply H5 with Hr := Hr; Auto.
Apply pointToClassRefDef; Auto.
Intros r s t Hr Hs; Repeat Rewrite <- H'; Auto.
Intros H'0; Inversion H0; Auto.
Apply H5 with r := r Hr := Hr; Auto.
Apply pointToClassClassRef; Auto.
Intros r s Hr Hs Lr; Repeat Rewrite <- H'; Auto.
Intros H'0 H'1; Inversion H1; Auto.
Apply H5 with Hr := Hr Lr := Lr; Auto.
Intros r s Hr Hs Ls; Repeat Rewrite <- H'; Auto.
Intros H'0 H'1; Inversion H1; Auto.
Apply H6 with Hr := Hr Hs := Hs; Auto.
Apply classInArrrayDef; Auto.
Intros r s Hr Lr; Repeat Rewrite <- H'; Auto.
Intros H'0 H'1; Inversion H2; Auto.
Apply H5 with r := r Hr := Hr Lr := Lr; Auto.
Apply OlistArrayDef; Auto.
Intros r Hr Lr; Repeat Rewrite <- H'; Auto.
Intros H'0; Inversion H3; Auto.
Apply H5 with r := r Hr := Hr; Auto.
Qed.

Definition resetAvalList:
  (n:rNat) (mL:(list rZ)) ((m:rZ) (In m mL) ->(rVlt m n)) ->
  (Ar1, Ar2:(Array n vM))(Array n vM).
Fix 2.
Intros n mL; Case mL.
Intros Inmml' Ar1 Ar2; Exact Ar1.
Intros m ml' Inm Ar1 Ar2.
Cut (m:rZ) (In m ml') ->(rVlt m n); [Intros Inml' | Idtac].
Cut (rVlt m n); [Intros Hm | Idtac].
Exact (setAval
         n vM (resetAvalList n ml' Inml' Ar1 Ar2) (valRz m) Hm
         (getAval n vM Ar2 (valRz m) Hm)).
Apply Inm; Simpl; Auto.
Intros m0 H'; Apply Inm; Auto; (Simpl; Auto).
Defined.

Theorem resetAvalListProp1:
  (n:rNat)
  (mL:(list rZ))
  (Iml:(m:rZ) (In m mL) ->(rVlt m n))
  (Ar1, Ar2:(Array n vM))
  (a:rNat) (Maxa:(rlt a n)) (In (rZPlus a) mL) \/ (In (rZMinus a) mL) ->
  (getAval n vM (resetAvalList n mL Iml Ar1 Ar2) a Maxa)=
  (getAval n vM Ar2 a Maxa).
Intros n mL; Elim mL; Simpl; Auto.
Intros H' Ar1 Ar2 a Maxa H'0; Elim H'0; Clear H'0; Intros H'0; Elim H'0.
Intros a l H' Iml Ar1 Ar2 a0 Maxa H'0.
Case (rNatDec a0 (valRz a)); Intros Eqaa0.
Rewrite (getAvalIrr
           n vM Ar2 a0 (valRz a) Maxa
           (Iml a (or_introl <rZ> a=a (In a l) (refl_equal rZ a)))); Auto.
Rewrite [A:(Array n vM)]
        (getAvalIrr
           n vM A a0 (valRz a) Maxa
           (Iml a (or_introl <rZ> a=a (In a l) (refl_equal rZ a)))); Auto.
Apply setAvalDef1; Auto.
Rewrite setAvalDef2; Auto.
Apply H'; Auto.
Elim H'0; Clear H'0; Intros H'0; Elim H'0; Clear H'0; Intros H'0; Auto.
Case Eqaa0; Rewrite H'0; Auto.
Case Eqaa0; Rewrite H'0; Auto.
Qed.

Theorem resetAvalListProp2:
  (n:rNat)
  (mL:(list rZ))
  (Iml:(m:rZ) (In m mL) ->(rVlt m n))
  (Ar1, Ar2:(Array n vM))
  (a:rNat) (Maxa:(rlt a n)) ~ (In (rZPlus a) mL) -> ~ (In (rZMinus a) mL) ->
  (getAval n vM (resetAvalList n mL Iml Ar1 Ar2) a Maxa)=
  (getAval n vM Ar1 a Maxa).
Intros n mL; Elim mL; Simpl; Auto.
Intros a l H' Iml Ar1 Ar2 a0 Maxa H'0 H'1.
Rewrite setAvalDef2; Auto.
Generalize H'1 H'0; Case a; Simpl; Auto.
Intros r H'2 H'3; Red; Intros H'4.
Case H'3; Rewrite H'4; Auto.
Intros r H'2 H'3; Red; Intros H'4.
Case H'2; Rewrite H'4; Auto.
Qed.

Theorem resetAvalListProp3:
  (n:rNat)
  (mL:(list rZ))
  (Iml:(m:rZ) (In m mL) ->(rVlt m n))
  (Ar1, Ar2:(Array n vM))
  ((a:rNat) (Maxa:(rlt a n)) ~ (In (rZPlus a) mL) -> ~ (In (rZMinus a) mL) ->
   (getAval n vM Ar1 a Maxa)=(getAval n vM Ar2 a Maxa)) ->
  (a:rNat) (Maxa:(rlt a n))
  (getAval n vM (resetAvalList n mL Iml Ar1 Ar2) a Maxa)=
  (getAval n vM Ar2 a Maxa).
Intros n mL Iml Ar1 Ar2 H' a Maxa.
Case (In_dec rZDec (rZPlus a) mL); Intros InaML.
Apply resetAvalListProp1; Auto.
Case (In_dec rZDec (rZMinus a) mL); Intros InMaML.
Apply resetAvalListProp1; Auto.
Rewrite <- H'; Auto.
Apply resetAvalListProp2; Auto.
Qed.

Definition resetMem: (M1, M2:Mem) (L:dList) (eqExceptOn M1 M2 L) ->Mem.
Intros M1 M2 L; Case M1; Case M2; Case L; Unfold eqExceptOn; Simpl.
Intros L' H' Ar2 War2 Ar1 War1 H'2.
Exists (resetAvalList
          maxN L' Cases H' of
                      (conj _ H'1) => H'1
                  end Ar1 Ar2).
Apply WarCompEq with Ar1 := Ar2; Auto.
Intros a Ha.
Apply sym_equal.
Apply resetAvalListProp3; Auto.
Intros a0 Maxa H' H'3.
Apply H'2; Auto.
Red; Intros H'4; Case (InEqInv ? ? H'4); Auto.
Defined.

Theorem resetMemIrr:
  (M1, M2:Mem) (L:dList) (Ex1, Ex2:(eqExceptOn M1 M2 L))
  (eqMem (resetMem M1 M2 L Ex1) (resetMem M1 M2 L Ex2)).
Intros M1 M2 L; Case M1; Case M2; Case L; Unfold eqExceptOn; Unfold eqMem;
Simpl; Auto.
Qed.

Theorem resetMemProp:
  (M1, M2:Mem) (L:dList) (Ex:(eqExceptOn M1 M2 L))
  (eqMem (resetMem M1 M2 L Ex) M2).
Intros M1 M2 L; Case M1; Case M2; Case L; Unfold eqExceptOn; Unfold eqMem;
Simpl; Auto.
Intros x a x0 H' x1 H'0 H'1 a0 Maxa.
Rewrite resetAvalListProp3; Auto.
Intros a1 Maxa0 H'2 H'3; Apply H'1; Auto.
Red; Intros H'4; Case (InEqInv ? ? H'4); Auto.
Qed.
End mem.

05/07/100, 11:37