addEqImplement.v

Require Import rZ.
Require Import PolyList.
Require Import PolyListAux.
Require Import OrderedListEq.
Require Import LetP.
Require Import array.
Require Import Relation_Definitions.
Require Import state.
Require Import restrictState.
Require Import ltState.
Require Import memoryImplement.

Definition updateArray:
  (n:rNat) (a, b:rNat) (rlt a b) ->
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (Ar:(Array n vM))
  (wellFormedArray n Ar) ->
  (getAval n vM Ar a Ha)=(class La) -> (getAval n vM Ar b Hb)=(class Lb) ->
  (Array n vM).
Intros n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb.
Exact (setAval
         n vM
         (setAvalList
            n (appendRz (cons (rZPlus b) (nil ?)) Lb)
            (InLc n b Hb Lb Ar War getb) Ar (pol (rZPlus a))) a Ha
         (class (fappendRz pol Hpol La (appendRz (cons (rZPlus b) (nil ?)) Lb)))).
Defined.

Theorem updateArraya:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (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))
  (getAval
     n vM (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb) a Ha)=
  (class (fappendRz pol Hpol La (appendRz (cons (rZPlus b) (nil ?)) Lb))).
Intros n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb; Unfold updateArray;
Unfold LetP; Simpl.
Rewrite setAvalDef1; Auto.
Qed.

Theorem updateArrayb:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (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))
  (getAval
     n vM (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb) b Hb)=
  (ref (pol (rZPlus a))).
Intros n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb; Unfold updateArray;
Unfold LetP; Simpl.
Cut ~ a=b; [Intros Neqab | Apply rltDef2; Auto].
Rewrite setAvalDef2; Auto.
Rewrite getAvalIrr with m2 := (valRz (rZPlus b)) Hm2 := Hb; Auto.
Rewrite setAvalListInv2; Auto.
Red; Unfold appendRz; Apply appendfOlist; Auto.
Exact rZltEqComp.
Apply OlistOne; Auto.
Apply wfOl with 2 := getb; Auto.
Generalize appendfIncl1; Unfold incl; Auto with datatypes.
Intros H'; Unfold appendRz; Apply H'; Auto with datatypes.
Apply DisjbLb with n := n Hb := Hb Ar := Ar; Auto.
Qed.

Theorem updateArrayInb:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (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)) (c:rZ) (In c Lb) ->
  (Hc:(rVlt c n))
  (getAval
     n vM (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb)
     (valRz c) Hc)=(ref (samePolRz c (pol (rZPlus a)))).
Intros n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb c InLb Hc;
Unfold updateArray; Unfold LetP; Simpl.
Rewrite setAvalDef2; Auto.
Rewrite setAvalListInv2; Auto.
Red; Unfold appendRz; Apply appendfOlist; Auto.
Exact rZltEqComp.
Apply OlistOne; Auto.
Apply wfOl with 2 := getb; Auto.
Generalize appendfIncl2; Unfold incl; Auto with datatypes.
Unfold appendRz; Intros H'; Apply H'; Auto.
Apply DisjbLb with n := n Hb := Hb Ar := Ar; Auto.
Red; Intros H'; Absurd (InRz (rZPlus a) Lb); Auto.
Apply wellFormedArrayInImpNotEq with 2 := geta 3 := getb; Auto.
Rewrite H'; Auto.
Red.
Apply InEqComp with a := c; Auto.
Apply inImpInEq; Auto.
Qed.

Theorem updateArrayOtherwise:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (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))
  (c:rNat) ~ (InRz (rZPlus c) Lb) -> ~ c=a -> ~ c=b ->
  (Hc:(rlt c n))
  (getAval
     n vM (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb) c Hc)=
  (getAval n vM Ar c Hc).
Intros n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb c NotPInb NotEqca
       NotEqcb Hc.
Rewrite getAvalIrr with m2 := (valRz (rZPlus c)) Hm2 := Hc; Auto.
Rewrite getAvalIrr with Ar := Ar m2 := (valRz (rZPlus c)) Hm2 := Hc; Auto.
Unfold updateArray; Unfold LetP.
Rewrite setAvalDef2; Auto.
Rewrite setAvalListInv1; Simpl; Auto.
Red; Intros H'.
Unfold appendRz in H'.
Case appendfInvEq with 1 := H'; Auto; Intros H'0; Inversion_clear H'0;
Inversion H; Auto.
Qed.

Definition updateArrayPointerDecrease:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (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))
  (pointerDecrease
     n (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb)).
Intros n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb.
Apply pointerDecreaseDef; Auto.
Intros r s Hr H'.
Case (rNatDec r a); Intros eqra.
Generalize H'; Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto;
Rewrite updateArraya; Auto; Clear H'; Intros H'; Discriminate.
Case (rNatDec r b); Intros eqrb.
Generalize H'; Rewrite getAvalIrr with m2 := b Hm2 := Hb; Auto;
Rewrite updateArrayb; Auto; Clear H'; Intros H'; Inversion H'.
Unfold rZlt; Simpl; Red.
Rewrite eqrb; Unfold eqRz in Hpol; Rewrite Hpol; Simpl; Auto.
Case (InRzDec (rZPlus r) Lb); Intros inPb.
Case (InEqInv (rZPlus r) Lb); Auto; Intros inPb'.
Generalize H'; Rewrite getAvalIrr with m2 := (valRz (rZPlus r)) Hm2 := Hr; Auto;
Rewrite updateArrayInb; Auto; Clear H'; Intros H'; Inversion H'.
Red; Apply rltTrans with y := b; Auto.
Simpl; Unfold eqRz in Hpol; Rewrite Hpol; Auto.
Change (rlt b (valRz (rZPlus r))).
Apply wellFormedArrayInImpLt with Ar := Ar Ha := Hb La := Lb; Auto.
Generalize H'; Rewrite getAvalIrr with m2 := (valRz (rZMinus r)) Hm2 := Hr;
Auto; Rewrite updateArrayInb; Auto; Clear H'; Intros H'; Inversion H'.
Simpl; Apply rVltrZComp; Auto.
Red; Unfold eqRz in Hpol; Rewrite Hpol; Simpl; Auto.
Apply rltTrans with y := b; Auto.
Change (rlt b (valRz (rZMinus r))).
Apply wellFormedArrayInImpLt with Ar := Ar Ha := Hb La := Lb; Auto.
Apply wfPd with n := n Ar := Ar Hr := Hr; Auto.
Rewrite <- H'.
Apply sym_equal.
Apply updateArrayOtherwise; Auto.
Qed.

Theorem updateGetIsClass:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (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))
  (r:rNat)
  (Hr:(rlt r n))
  (Lr:(list rZ))
  <vM>
    (getAval
       n vM (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb) r Hr)=
    (class Lr) -> ~ r=a ->(getAval n vM Ar r Hr)=(class Lr).
Intros n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb r Hr Lr H' H'0.
Case (rNatDec r b); Intros Eqb; Auto.
Generalize H'; Rewrite getAvalIrr with m2 := b Hm2 := Hb; Auto;
Rewrite updateArrayb; Clear H'; Intros H'; Discriminate.
Case (InRzDec (rZPlus r) Lb); Intros InRLb; Auto.
Case (InEqInv (rZPlus r) Lb); Auto; Intros InRLb'.
Generalize H'; Rewrite getAvalIrr with m2 := (valRz (rZPlus r)) Hm2 := Hr; Auto;
Rewrite updateArrayInb; Auto; Clear H'; Intros H'; Discriminate.
Generalize H'; Rewrite getAvalIrr with m2 := (valRz (rZMinus r)) Hm2 := Hr;
Auto; Rewrite updateArrayInb; Auto; Clear H'; Intros H'; Discriminate.
Rewrite <- H'; Apply sym_equal.
Apply updateArrayOtherwise; Auto.
Qed.

Definition updateArrayOlist:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (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))
  (OlistArray n (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb)).
Intros n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb.
Apply OlistArrayDef; Auto.
Intros r Hr Lr H'.
Case (rNatDec r a); Intros Eqt.
Generalize H'; Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto;
Rewrite updateArraya; Auto; Clear H'; Intros H'; Inversion H'.
Red; Unfold fappendRz; Apply fappendfOlist; Auto.
Apply wfOl with 2 := geta; Auto.
Unfold appendRz; Apply appendfOlist; Auto.
Exact rZltEqComp.
Apply OlistOne; Auto.
Apply wfOl with 2 := getb; Auto.
Apply wfOl with n := n Ar := Ar r := r Hr := Hr; Auto.
Apply updateGetIsClass with 1 := H'; Auto.
Qed.

Definition updateArrayClassInArray:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (Hpol':(d:rZ)(pol (pol d))=d)
  (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))
  (classInArrray
     n (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb)).
Intros n a b ltab Ha Hb La Lb pol Hpol Hpol' Ar War geta getb.
Apply classInArrrayDef.
Intros r s Hr Lr H'.
Case (rNatDec r a); Intros Eqt.
Generalize H'; Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto;
Rewrite updateArraya; Auto; Clear H'; Intros H'; Inversion H'.
Unfold fappendRz; Intros Infa; Case (fappendfInv rZ) with 1 := Infa; Auto;
Intros H'1.
Apply wfCa with 2 := geta; Auto.
Cut (In (pol s) (appendRz (cons (rZPlus b) (nil rZ)) Lb));
[Unfold appendRz; Intros Hspol | Idtac]; Auto.
Case appendfInv with ltADec := rZltEDec 1 := Hspol; Auto; Intros H'0.
Elim H'0; [Intros H'2; Unfold rVlt; Clear H'0 | Intros H'2; Elim H'2; Clear H'0].
Unfold eqRz in Hpol; Rewrite <- (Hpol s); Rewrite <- H'2; Simpl; Auto.
Unfold rVlt; Unfold eqRz in Hpol; Rewrite <- (Hpol s).
Change (rVlt (pol s) n).
Apply wfCa with 2 := getb; Auto.
LApply (map_id rZ pol);
[Intros H'3; Rewrite <- (H'3 (appendRz (cons (rZPlus b) (nil rZ)) Lb)) | Idtac];
Auto.
Apply in_map with A := rZ B := rZ; Auto.
Intros H'0; Apply wfCa with Ar := Ar r := r Hr := Hr Lr := Lr; Auto.
Apply updateGetIsClass with 1 := H'; Auto.
Qed.

Theorem updateArrayPointToRef:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (HpolInv:(a:rZ)(pol (rZComp a))=(rZComp (pol a)))
  (HpolAx:(c:rZ) (d:rNat)(samePol (pol c) d)=(pol (samePol c d)))
  (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))
  (pointToClassRef
     n (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb)).
Intros n a b ltab Ha Hb La Lb pol Hpol H' H'0 Ar War geta getb.
Apply pointToClassRefDef; Auto.
Intros r s t Hr Hs H'1.
Case (rNatDec (valRz s) a); Intros eqsa.
Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto; Rewrite updateArraya; Red;
Intros H'2; Discriminate.
Case (rNatDec r a); Intros eqra.
Generalize H'1; Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto;
Rewrite updateArraya; Auto; Clear H'1; Intros H'1; Discriminate.
Case (rNatDec r b); Intros eqrb; Auto.
Generalize H'1; Rewrite getAvalIrr with m2 := b Hm2 := Hb; Auto;
Rewrite updateArrayb; Auto; Clear H'1; Intros H'1; Case eqsa; Inversion H'1.
Change (eqRz (pol (rZPlus a)) (rZPlus a)); Auto.
Case (InRzDec (rZPlus r) Lb); Intros InRLb; Auto.
Case (InEqInv (rZPlus r) Lb); Auto; Intros InRLb'.
Generalize H'1; Rewrite getAvalIrr with m2 := (valRz (rZPlus r)) Hm2 := Hr;
Auto; Rewrite updateArrayInb; Auto; Clear H'1; Intros H'1; Case eqsa;
Inversion H'1; Simpl; Auto.
Change (eqRz (pol (rZPlus a)) (rZPlus a)); Auto.
Generalize H'1; Rewrite getAvalIrr with m2 := (valRz (rZMinus r)) Hm2 := Hr;
Auto; Rewrite updateArrayInb; Auto; Clear H'1; Intros H'1; Case eqsa;
Inversion H'1; Simpl; Auto.
Change (eqRz (rZComp (pol (rZPlus a))) (rZPlus a)); Auto.
Apply eqrZTrans with y := (pol (rZPlus a)); Auto.
Generalize H'1; Auto; Rewrite updateArrayOtherwise; Auto; Clear H'1; Intros H'1.
Case (rNatDec (valRz s) b); Intros eqsb; Auto.
Case InRLb; Red.
Apply InEqComp with a := (samePol s r); Auto.
Apply inImpInEq; Auto.
Apply wfPcc2 with n := n Ar := Ar Hr := Hr Hs := Hs; Auto.
Rewrite getAvalIrr with m2 := b Hm2 := Hb; Auto; Rewrite updateArrayb; Auto.
Case s; Simpl; Auto.
Case (InRzDec s Lb); Intros InRLb'; Auto.
Case (InEqInv s Lb); Auto; Intros InRLb''.
Absurd <vM> (getAval n vM Ar (valRz s) Hs)=(ref (samePol s b)); Auto.
Inversion War.
Inversion H0.
Apply H5 with r := r Hr := Hr; Auto.
Inversion War.
Inversion H1.
Apply H5 with Hr := Hb Lr := Lb; Auto.
Cut (rVlt (rZComp s) n); [Intros Hms | Idtac].
Absurd (getAval n vM Ar (valRz (rZComp s)) Hms)=(ref (samePol (rZComp s) b)).
Rewrite getAvalIrr with m2 := (valRz s) Hm2 := Hs; Auto.
Inversion War.
Inversion H0.
Apply H5 with r := r Hr := Hr; Auto.
Change (eqRz (rZComp s) s); Auto.
Inversion War.
Inversion H1.
Apply H5 with Hr := Hb Lr := Lb; Auto.
Apply rVltrZComp; Auto.
Rewrite updateArrayOtherwise; Auto.
Inversion War.
Inversion H0.
Apply H5 with r := r Hr := Hr; Auto.
Red; Intros H'2; Case InRLb'; Red.
Apply InEqComp with a := (rZPlus (valRz s)); Auto.
Qed.

Theorem updatePointToClassClassRef1:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (HpolInv:(a:rZ)(pol (rZComp a))=(rZComp (pol a)))
  (HpolAx:(c:rZ) (d:rNat)(samePol (pol c) d)=(pol (samePol c d)))
  (HpolHpol:(c:rZ)(pol (pol c))=c)
  (HpolAxRz:(c:rZ) (c, d:rZ)(samePolRz (pol c) d)=(pol (samePolRz c d)))
  (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))
  (r:rNat)
  (s:rZ)
  (Hr:(rlt r n))
  (Hs:(rVlt s n))
  (Lr:(list rZ))
  (getAval
     n vM (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb) r Hr)=
  (class Lr) -> (In s Lr) ->
  (getAval
     n vM (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb)
     (valRz s) Hs)=(ref (samePol s r)).
Intros n a b ltab Ha Hb La Lb pol Hpol HpolInv HpolAx HpolHpol HpolAxRz Ar War
       geta getb r s Hr Hs Lr H'.
Case (rNatDec r a); Intros eqra.
Generalize H'; Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto;
Rewrite updateArraya; Auto; Clear H'; Intros H'; Inversion H'.
Unfold fappendRz; Unfold appendRz; Intros Eqt.
Case (fappendfInv rZ) with 1 := Eqt; Intros Eqt'; Auto.
Rewrite updateArrayOtherwise; Auto.
Rewrite eqra.
Apply wfPcc1 with Hr := Ha Lr := La; Auto.
Red; Intros H'2; Absurd a=b; Auto.
Red; Intros H'3; Absurd (rlt a b); Auto.
Rewrite <- H'3; Auto.
Apply wellFormedArrayInRzBothImpEq
     with 2 := geta 3 := getb c := (rZPlus (valRz s)); Auto.
Unfold InRz; Simpl; Intros; Apply InEqComp with a := s; Auto.
Apply inImpInEq; Auto.
Red; Intros H'2; Absurd (InRz (rZPlus a) La).
Apply wellFormedArrayInImpNotEqSimpl with 2 := geta; Auto.
Rewrite <- H'2.
Unfold InRz; Simpl; Intros; Apply InEqComp with a := s; Auto.
Apply inImpInEq; Auto.
Red; Intros H'2; Absurd (InRz (rZPlus b) La); Auto.
Apply wellFormedArrayInImpNotEq with 2 := getb 3 := geta; Auto.
Rewrite <- H'2.
Unfold InRz; Simpl; Intros; Apply InEqComp with a := s; Auto.
Apply inImpInEq; Auto.
Elim (appendfInv rZ rZlt eqRz rZltEDec (cons (rZPlus b) (nil rZ)) Lb (pol s));
Auto.
Simpl; Intros Int.
Elim Int; [Intros H'2; Clear Int | Intros H'2; Elim H'2; Clear Int]; Auto.
Rewrite getAvalIrr with m2 := b Hm2 := Hb; Auto.
Rewrite updateArrayb; Auto.
Rewrite eqra; Auto.
Apply trans_equal with y := (ref (pol (samePol (pol s) a))); Auto.
Rewrite <- H'2; Simpl; Auto.
Rewrite HpolAx.
Rewrite HpolHpol; Auto.
Change (eqRz s (rZPlus b)).
Rewrite H'2; Auto.
Intros Int; Cut (rVlt (pol s) n); [Intros Hpols | Idtac].
Rewrite getAvalIrr with m2 := (valRz (pol s)) Hm2 := Hpols; Auto.
Rewrite updateArrayInb; Auto.
Rewrite eqra.
Rewrite HpolAxRz; Simpl; Auto.
Case s; Simpl; Intros s'.
Rewrite HpolHpol; Simpl; Auto.
Rewrite HpolInv; Simpl; Auto.
Rewrite HpolHpol; Simpl; Auto.
Change (eqRz s (pol s)); Auto.
Red; Unfold eqRz in Hpol; Rewrite (Hpol s); Auto.
Rewrite <- (map_id
              rZ pol HpolHpol
              (appendf rZ rZlt eqRz rZltEDec (cons (rZPlus b) (nil rZ)) Lb));
Auto.
Apply in_map; Auto.
Intros Int.
Case (rNatDec r b); Intros eqrb.
Generalize H'; Rewrite getAvalIrr with m2 := b Hm2 := Hb; Auto;
Rewrite updateArrayb; Auto; Clear H'; Intros H'; Discriminate.
Case (InRzDec (rZPlus r) Lb); Intros InRLb; Auto.
Case (InEqInv (rZPlus r) Lb); Auto; Intros InRLb'.
Generalize H'; Rewrite getAvalIrr with m2 := (valRz (rZPlus r)) Hm2 := Hr; Auto;
Rewrite updateArrayInb; Auto; Clear H'; Intros H'; Discriminate.
Generalize H'; Rewrite getAvalIrr with m2 := (valRz (rZMinus r)) Hm2 := Hr;
Auto; Rewrite updateArrayInb; Auto; Clear H'; Intros H'; Discriminate.
Case (rNatDec (valRz s) a); Intros eqsa.
Absurd (InRz (rZPlus a) Lr); Auto.
Apply wellFormedArrayInImpNotEq
     with n := n Ar := Ar b := r Ha := Ha Hb := Hr La := La; Auto.
Apply updateGetIsClass with 1 := H'; Auto.
Red; Apply InEqComp with a := s; Auto.
Apply inImpInEq; Auto.
Case (rNatDec (valRz s) b); Intros eqsb.
Absurd (InRz (rZPlus b) Lr); Auto.
Apply wellFormedArrayInImpNotEq
     with n := n Ar := Ar b := r Ha := Hb Hb := Hr La := Lb; Auto.
Apply updateGetIsClass with 1 := H'; Auto.
Red; Apply InEqComp with a := s; Auto.
Apply inImpInEq; Auto.
Rewrite updateArrayOtherwise; Auto.
Apply wfPcc1 with Hr := Hr Lr := Lr; Auto.
Apply updateGetIsClass with 1 := H'; Auto.
Red; Intros H'2; Absurd r=b; Auto.
Apply wellFormedArrayInRzBothImpEq
     with n := n Ar := Ar c := s Ha := Hr Hb := Hb La := Lr Lb := Lb; Auto.
Apply updateGetIsClass with 1 := H'; Auto.
Red; Apply InEqComp with a := s; Auto.
Apply inImpInEq; Auto.
Red; Apply InEqComp with a := (rZPlus (valRz s)); Auto.
Qed.

Theorem updatePointToClassClassRef2:
  (n:rNat)
  (a, b:rNat)
  (ltab:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (HpolInv:(a:rZ)(pol (rZComp a))=(rZComp (pol a)))
  (HpolAx:(c:rZ) (d:rNat)(samePol (pol c) d)=(pol (samePol c d)))
  (HpolHpol:(c:rZ)(pol (pol c))=c)
  (HpolAxRz:(c, d:rZ)(samePolRz (pol c) d)=(pol (samePolRz c d)))
  (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))
  (r:rNat)
  (s:rZ)
  (Hr:(rlt r n))
  (Hs:(rVlt s n))
  (Ls:(list rZ))
  (getAval
     n vM (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb) r Hr)=
  (ref s) ->
  (getAval
     n vM (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb)
     (valRz s) Hs)=(class Ls) ->(In (samePol s r) Ls).
Intros n a b ltab Ha Hb La Lb pol Hpol HpolInv HpolAx HpolHpol HpolAxRz Ar War
       geta getb r s Hr Hs Ls.
Case (rNatDec r a); Intros eqra.
Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto; Rewrite updateArraya; Auto;
Intros H'; Inversion H'.
Case (rNatDec r b); Intros eqrb.
Rewrite getAvalIrr with m2 := b Hm2 := Hb; Auto; Rewrite updateArrayb; Auto;
Intros H'; Inversion H'.
Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto.
Rewrite updateArraya; Auto; Intros H'2; Inversion H'2.
Rewrite eqrb.
Unfold fappendRz; Unfold appendRz; Generalize fappendfIncl2; Unfold incl;
Intros incl2; Apply incl2; Auto; Clear incl2.
Apply DisjLaLc with 3 := geta 4 := getb; Auto.
Rewrite <- eqrb; Auto.
Rewrite <- H0.
Rewrite HpolAx.
Apply in_map with A := rZ B := rZ; Auto.
Generalize appendfIncl1; Unfold incl; Intros incl1; Apply incl1;
Auto with datatypes; Clear incl1.
Apply DisjbLb with 2 := getb; Auto.
Rewrite <- H0; Auto.
Change (eqRz (pol (rZPlus a)) (rZPlus a)); Auto.
Case (InRzDec (rZPlus r) Lb); Intros InRLb; Auto.
Case (InEqInv (rZPlus r) Lb); Auto; Intros InRLb'.
Rewrite getAvalIrr with m2 := (valRz (rZPlus r)) Hm2 := Hr; Auto.
Rewrite updateArrayInb; Auto; Intros H'2; Inversion H'2.
Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto.
Rewrite updateArraya; Auto.
Intros H'; Inversion H'.
Rewrite <- H0; Simpl; Rewrite HpolAx; Simpl; Auto.
Unfold fappendRz; Unfold appendRz; Generalize fappendfIncl2; Unfold incl;
Intros incl2; Apply incl2; Auto; Clear incl2.
Apply DisjLaLc with 3 := geta 4 := getb; Auto.
Apply rltDef2; Auto.
Apply in_map with A := rZ B := rZ; Auto.
Generalize appendfIncl2; Unfold incl; Intros incl1; Apply incl1;
Auto with datatypes; Clear incl1.
Apply DisjbLb with 2 := getb; Auto.
Rewrite <- H0; Simpl; Auto.
Change (eqRz (pol (rZPlus a)) (rZPlus a)); Auto.
Rewrite getAvalIrr with m2 := (valRz (rZMinus r)) Hm2 := Hr; Auto.
Rewrite updateArrayInb; Auto; Intros H'2; Inversion H'2.
Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto.
Rewrite updateArraya; Auto.
Intros H'; Inversion H'.
Rewrite <- H0; Simpl; Auto.
Rewrite <- HpolInv.
Rewrite HpolAx; Simpl; Auto.
Unfold fappendRz; Unfold appendRz; Generalize fappendfIncl2; Unfold incl;
Intros incl2; Apply incl2; Auto; Clear incl2.
Apply DisjLaLc with 3 := geta 4 := getb; Auto.
Apply rltDef2; Auto.
Apply in_map with A := rZ B := rZ; Auto.
Generalize appendfIncl2; Unfold incl; Intros incl1; Apply incl1;
Auto with datatypes; Clear incl1.
Apply DisjbLb with 2 := getb; Auto.
Rewrite <- H0; Simpl; Auto.
Change (eqRz (rZComp (pol (rZPlus a))) (rZPlus a)).
Apply eqrZTrans with y := (pol (rZPlus a)); Auto.
Rewrite updateArrayOtherwise; Auto; Intros Eqr.
Case (rNatDec (valRz s) a); Intros Eqt.
Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto; Rewrite updateArraya; Auto;
Intros H'; Inversion H'.
Unfold fappendRz; Unfold appendRz; Generalize fappendfIncl1; Unfold incl;
Intros incl2; Apply incl2; Auto; Clear incl2.
Apply DisjLaLc with 3 := geta 4 := getb; Auto.
Apply rltDef2; Auto.
Apply wfPcc2 with n := n Ar := Ar Hr := Hr Hs := Hs; Auto.
Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto.
Intros Eqs.
Apply wfPcc2 with n := n Ar := Ar Hr := Hr Hs := Hs; Auto.
Apply updateGetIsClass with 1 := Eqs; Auto.
Qed.

Definition updateMemory:
  (n:rNat)
  (a, b:rNat)
  (lta:(rlt a b))
  (Ha:(rlt a n))
  (Hb:(rlt b n))
  (La:(list rZ))
  (Lb:(list rZ))
  (pol:rZ ->rZ)
  (Hpol:(d:rZ)(eqRz (pol d) d))
  (HpolInv:(a:rZ)(pol (rZComp a))=(rZComp (pol a)))
  (HpolAx:(c:rZ) (d:rNat)(samePol (pol c) d)=(pol (samePol c d)))
  (HpolHpol:(c:rZ)(pol (pol c))=c)
  (HpolAxRz:(c, d:rZ)(samePolRz (pol c) d)=(pol (samePolRz c d)))
  (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))(memory n).
Intros n a b ltab Ha Hb La Lb pol Hpol HpolInv HpolAx HpolHpol HpolAxRz Ar War
       geta getb.
Exists (updateArray n a b ltab Ha Hb La Lb pol Hpol Ar War geta getb).
Apply wellFormedArrayDef; Auto.
Apply updateArrayPointerDecrease; Auto.
Apply updateArrayPointToRef; Auto.
Apply pointToClassClassRef; Auto.
Intros r s Hr Hs Lr H' H'0.
Apply updatePointToClassClassRef1 with Hr := Hr Lr := Lr; Auto.
Intros r s Hr Hs Ls H' H'0.
Apply updatePointToClassClassRef2 with 5 := H' 6 := H'0; Auto.
Apply updateArrayClassInArray; Auto.
Apply updateArrayOlist; Auto.
Defined.
Require Import triplet.

05/07/100, 11:37