addEqImplement2.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.
Require Export addEqImplement.
Section update.
Require Import triplet.
Variable LL':(list triplet).
Variable maxN:rNat.
Hypothesis HmaxN:maxN=(rnext (maxVarTriplets LL')).
Definition
mkMem:
(Ar:(Array maxN vM)) (War:(wellFormedArray maxN Ar))(Mem maxN).
Intros Ar H'; Exists Ar; Auto.
Defined.
Definition
getClass:
(Ar:(Array maxN vM)) (War:(wellFormedArray maxN Ar)) (a:rZ) (Ha:(rVlt a maxN))
(list rZ).
Intros Ar War a Ha.
Case (getAval maxN vM Ar (valRz a) Ha).
Intros u; Exact (nil ?).
Intros L; Exact L.
Defined.
Theorem
getClassProp:
(Ar:(Array maxN vM))
(War:(wellFormedArray maxN Ar))
(a:rZ)
(Ha:(rVlt a maxN))
(i:rZ) (Hi:(rVlt i maxN)) (Equ:i=(evalMZ maxN (mkMem Ar War) a Ha))
(getAval maxN vM Ar (valRz i) Hi)=(class (getClass Ar War i Hi)).
Intros Ar War a; Case a; Simpl; Unfold getClass; Auto.
Intros r Ha i Hi.
Generalize [t:rZ](wfPcr maxN Ar r i t Ha Hi War).
Generalize (refl_equal ? (getAval maxN vM Ar r Ha));
Pattern -2 (getAval maxN vM Ar r Ha); Case (getAval maxN vM Ar r Ha); Auto.
Intros r0 H'; Case (getAval maxN vM Ar (valRz i) Hi); Auto.
Intros r1 H'0 H'1; LApply (H'0 r1); [Intros H'2; Case H'2 | Idtac]; Auto.
Rewrite <- H'1; Auto.
Intros l H' H'0 H'1.
Rewrite getAvalIrr with m2 := r Hm2 := Ha; Auto.
Rewrite <- H'; Auto.
Rewrite H'1; Auto.
Intros r Ha i Hi.
Generalize [t:rZ](wfPcr maxN Ar r (rZComp i) t Ha (rVltrZComp ? ? Hi) War).
Rewrite getAvalIrr with m1 := (valRz (rZComp i)) m2 := (valRz i) Hm2 := Hi; Auto.
Generalize (refl_equal ? (getAval maxN vM Ar r Ha));
Pattern -2 (getAval maxN vM Ar r Ha); Case (getAval maxN vM Ar r Ha); Auto.
Intros r0 H'; Case (getAval maxN vM Ar (valRz i) Hi); Auto.
Intros r1 H'0 H'1; LApply (H'0 r1); [Intros H'2; Case H'2 | Idtac]; Auto.
Rewrite H'1; Case r0; Auto.
Intros l H' H'0 H'1.
Rewrite getAvalIrr with m2 := r Hm2 := Ha; Auto.
Rewrite <- H'; Auto.
Rewrite H'1; Auto.
Case i; Auto.
Qed.
Definition
sameSign :=
[a, b:rZ]
Cases a b of
(rZPlus _) (rZPlus _) => true
| (rZPlus _) (rZMinus _) => false
| (rZMinus _) (rZPlus _) => false
| (rZMinus _) (rZMinus _) => true
end.
Definition
mkdList:
(a, b:rZ)
(Ha:(rlt (valRz a) maxN))
(Hb:(rlt (valRz b) maxN))
(ltab:(rlt (valRz a) (valRz b)))
(Lb:(list rZ))
(Ar:(Array maxN vM))
(War:(wellFormedArray maxN Ar))
(getb:(getAval maxN vM Ar (valRz b) Hb)=(class Lb))(dList maxN).
Intros a b Ha Hb ltab Lb Ar War getb; Exists (cons a (cons b Lb)); Split; Auto.
Red.
Apply OlistCons; Auto.
Generalize getb; Case Lb; Auto.
Intros H'.
Apply OlistOne; Auto.
Intros r l H'.
Apply OlistCons; Auto.
Apply wfOl with n := maxN Ar := Ar r := (valRz b) Hr := Hb; Auto.
Cut (rVlt (samePol r (valRz b)) (valRz r)).
Case r; Auto.
Cut (rVlt r maxN); [Intros Hr | Idtac].
Apply wfPd with n := maxN Ar := Ar Hr := Hr; Auto.
Apply wfPcc1 with Hr := Hb Lr := (cons r l); Auto with datatypes.
Apply wfCa with Ar := Ar r := (valRz b) Hr := Hb Lr := (cons r l);
Auto with datatypes.
Simpl; Auto.
Intros a0 H'; Elim H'; Clear H'; Intros H';
[Rewrite <- H' | Elim H'; Clear H'; Intros H'; [Rewrite <- H' | Idtac]]; Auto.
Apply wfCa with Ar := Ar r := (valRz b) Hr := Hb Lr := Lb; Auto with datatypes.
Defined.
Definition
updateMemorySameSign :=
[n, a, b:rNat]
[ltab:(rlt a b)] [Ha:(rlt a n)] [Hb:(rlt b n)] [La, Lb:(list rZ)]
(updateMemory
n a b ltab Ha Hb La Lb [x:?]x eqrZRefl [a0:rZ](refl_equal rZ (rZComp a0))
[c:rZ] [d:rNat](refl_equal rZ (samePol c d)) (refl_equal rZ)
[c, d:rZ](refl_equal rZ (samePolRz c d))).
Definition
updateMemoryOpSign :=
[n, a, b:rNat]
[ltab:(rlt a b)] [Ha:(rlt a n)] [Hb:(rlt b n)] [La, Lb:(list rZ)]
(updateMemory
n a b ltab Ha Hb La Lb [x:?](rZComp x)
[d:rZ](eqrZSym d (rZComp d) (eqRzComp d))
[a:rZ](refl_equal rZ (rZComp (rZComp a))) [c:rZ]
<[r:rZ] (d:rNat)
<rZ>
(samePol (rZComp r) d)=
(rZComp (samePol r d))>
Cases c of
(rZPlus r) =>
[d:rNat]
(refl_equal
rZ
(rZComp
(samePol
(rZPlus r) d)))
| (rZMinus r) =>
[d:rNat]
(refl_equal
rZ
(rZComp
(samePol
(rZMinus r) d)))
end
[c:rZ](sym_eq rZ c (rZComp (rZComp c)) (rZCompInvol c)) [c:rZ]
<[r:rZ] (d:rZ)
<rZ>
(samePolRz
(rZComp
r) d)=
(rZComp
(samePolRz
r d))>
Cases c of
(rZPlus r)
=>
[d:rZ]
(refl_equal
rZ
(rZComp
(samePolRz
(rZPlus
r)
d)))
| (rZMinus
_) =>
[d:rZ]
(rZCompInvol
d)
end).
Inductive
Triple[A, B, C:Set]: Set :=
triple: A -> B -> C ->(Triple A B C) .
Definition
mbD := (Triple (Mem maxN) bool (dList maxN)).
Definition
mbDOp := (triple (Mem maxN) bool (dList maxN)).
Definition
addEqMem:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))mbD.
Intros M a b Ha Hb.
Apply LetP with h := (evalMZ maxN M a Ha); Intros a' Eqa'.
Apply LetP with h := (evalMZ maxN M b Hb); Intros b' Eqb'.
Cut (rVlt a' maxN); [Intros Ha' | Rewrite Eqa'; Apply evalMZlt]; Auto.
Cut (rVlt b' maxN); [Intros Hb' | Rewrite Eqb'; Apply evalMZlt]; Auto.
Case (rZltEDec a' b'); Intros rLt; [Case rLt; Clear rLt; Intros rLt | Idtac].
Generalize Eqa' Eqb'; Case M; Simpl; Clear Eqa' Eqb'; Intros Ar War Eqa' Eqb'.
Apply LetP with h := (getClass Ar War a' Ha'); Intros Ca' EqCa'.
Apply LetP with h := (getClass Ar War b' Hb'); Intros Cb' EqCb'.
Cut <vM> (getAval maxN vM Ar (valRz a') Ha')=(class Ca');
[Intros HCa' | Rewrite EqCa'; Apply getClassProp with a := a Ha := Ha; Auto].
Cut <vM> (getAval maxN vM Ar (valRz b') Hb')=(class Cb');
[Intros HCb' | Rewrite EqCb'; Apply getClassProp with a := b Ha := Hb; Auto].
Case (sameSign a' b').
Apply LetP
with h :=
(updateMemorySameSign
maxN (valRz a') (valRz b') rLt Ha' Hb' Ca' Cb' Ar War HCa' HCb').
Intros mem' Mem'.
Exact (mbDOp mem' false (mkdList a' b' Ha' Hb' rLt Cb' Ar War HCb')).
Apply LetP
with h :=
(updateMemoryOpSign
maxN (valRz a') (valRz b') rLt Ha' Hb' Ca' Cb' Ar War HCa' HCb').
Intros mem' Mem'.
Exact (mbDOp mem' false (mkdList a' b' Ha' Hb' rLt Cb' Ar War HCb')).
Generalize Eqa' Eqb'; Case M; Simpl; Clear Eqa' Eqb'; Intros Ar War Eqa' Eqb'.
Apply LetP with h := (getClass Ar War a' Ha'); Intros Ca' EqCa'.
Apply LetP with h := (getClass Ar War b' Hb'); Intros Cb' EqCb'.
Cut <vM> (getAval maxN vM Ar (valRz a') Ha')=(class Ca');
[Intros HCa' | Rewrite EqCa'; Apply getClassProp with a := a Ha := Ha; Auto].
Cut <vM> (getAval maxN vM Ar (valRz b') Hb')=(class Cb');
[Intros HCb' | Rewrite EqCb'; Apply getClassProp with a := b Ha := Hb; Auto].
Case (sameSign a' b').
Apply LetP
with h :=
(updateMemorySameSign
maxN (valRz b') (valRz a') rLt Hb' Ha' Cb' Ca' Ar War HCb' HCa').
Intros mem' Mem'.
Exact (mbDOp mem' false (mkdList b' a' Hb' Ha' rLt Ca' Ar War HCa')).
Apply LetP
with h :=
(updateMemoryOpSign
maxN (valRz b') (valRz a') rLt Hb' Ha' Cb' Ca' Ar War HCb' HCa').
Intros mem' Mem'.
Exact (mbDOp mem' false (mkdList b' a' Hb' Ha' rLt Ca' Ar War HCa')).
Case (rZDec a' b'); Intros eqa'b'.
Exact (mbDOp M false (dNil maxN)).
Exact (mbDOp M true (dNil maxN)).
Defined.
Theorem
evalMnatArr1:
(a, b:rNat)
(Ha:(rlt a maxN))
(Hb:(rlt b maxN))
(La:(list rZ))
(Ar:(Array maxN vM))
(War:(wellFormedArray maxN Ar))
(geta:(getAval maxN vM Ar a Ha)=(class La))
(evalMnat maxN (mkMem Ar War) b Hb)=(rZPlus a) ->(In (rZPlus b) La) \/ b=a.
Intros a b Ha Hb La Ar War H'; Unfold evalMnat; Simpl.
Generalize [s:rZ] [Hs:(rVlt s maxN)](wfPcc2 maxN Ar b s Hb Hs La War).
Generalize (refl_equal ? (getAval maxN vM Ar b Hb));
Pattern -1 (getAval maxN vM Ar b Hb); Case (getAval maxN vM Ar b Hb); Auto.
Intros r H'0 H'1 H'2; Left.
Cut (In (samePol r b) La).
Rewrite H'2; Auto.
Cut (rlt (valRz r) maxN); [Intros Hr | Rewrite H'2]; Auto.
Apply H'1 with Hs := Hr; Auto.
Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto.
Rewrite H'2; Auto.
Intros l H'0 H'1 H'2; Inversion H'2; Auto.
Qed.
Theorem
evalMnatArr2:
(a, b:rNat)
(Ha:(rlt a maxN))
(Hb:(rlt b maxN))
(La:(list rZ))
(Ar:(Array maxN vM))
(War:(wellFormedArray maxN Ar))
(geta:(getAval maxN vM Ar a Ha)=(class La))
(evalMnat maxN (mkMem Ar War) b Hb)=(rZMinus a) ->(In (rZMinus b) La) \/ b=a.
Intros a b Ha Hb La Ar War H'; Unfold evalMnat; Simpl.
Generalize [s:rZ] [Hs:(rVlt s maxN)](wfPcc2 maxN Ar b s Hb Hs La War).
Generalize (refl_equal ? (getAval maxN vM Ar b Hb));
Pattern -1 (getAval maxN vM Ar b Hb); Case (getAval maxN vM Ar b Hb); Auto.
Intros r H'0 H'1 H'2; Left.
Cut (In (samePol r b) La).
Rewrite H'2; Auto.
Cut (rlt (valRz r) maxN); [Intros Hr | Rewrite H'2]; Auto.
Apply H'1 with Hs := Hr; Auto.
Rewrite getAvalIrr with m2 := a Hm2 := Ha; Auto.
Rewrite H'2; Auto.
Intros l H'0 H'1 H'2; Inversion H'2; Auto.
Qed.
Theorem
updateArrayEvb1:
(a, b, c:rNat)
(ltab:(rlt a b))
(Ha:(rlt a maxN))
(Hb:(rlt b maxN))
(Hc:(rlt c maxN))
(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 maxN vM))
(War:(wellFormedArray maxN Ar))
(geta:(getAval maxN vM Ar a Ha)=(class La))
(getb:(getAval maxN vM Ar b Hb)=(class Lb))
(evalMnat maxN (mkMem Ar War) c Hc)=(rZPlus b) ->
(evalMnat
maxN
(updateMemory
maxN a b ltab Ha Hb La Lb pol Hpol HpolInv HpolAx HpolHpol HpolAxRz Ar
War geta getb) c Hc)=(pol (rZPlus a)).
Intros a b c ltab Ha Hb Hc La Lb pol Hpol HpolInv HpolAx HpolHpol HpolAxRz Ar
War geta getb H'.
Unfold evalMnat updateMemory; Simpl.
Case evalMnatArr1 with 1 := getb 2 := H'; Intros Eq0.
Generalize (updateArrayInb
maxN a b ltab Ha Hb La Lb pol Hpol Ar War geta getb (rZPlus c) Eq0
Hc); Simpl; Auto.
Intros H'0; Rewrite H'0; Auto.
Rewrite (getAvalIrr
maxN vM
(updateArray maxN a b ltab Ha Hb La Lb pol Hpol Ar War geta getb) c b
Hc Hb); Auto.
Rewrite (updateArrayb maxN a b ltab Ha Hb La Lb pol Hpol Ar War geta getb); Auto.
Qed.
Theorem
updateArrayEvb2:
(a, b, c:rNat)
(ltab:(rlt a b))
(Ha:(rlt a maxN))
(Hb:(rlt b maxN))
(Hc:(rlt c maxN))
(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 maxN vM))
(War:(wellFormedArray maxN Ar))
(geta:(getAval maxN vM Ar a Ha)=(class La))
(getb:(getAval maxN vM Ar b Hb)=(class Lb))
(evalMnat maxN (mkMem Ar War) c Hc)=(rZMinus b) ->
(evalMnat
maxN
(updateMemory
maxN a b ltab Ha Hb La Lb pol Hpol HpolInv HpolAx HpolHpol HpolAxRz Ar
War geta getb) c Hc)=(pol (rZMinus a)).
Intros a b c ltab Ha Hb Hc La Lb pol Hpol HpolInv HpolAx HpolHpol HpolAxRz Ar
War geta getb H'.
Unfold evalMnat updateMemory; Simpl.
Case evalMnatArr2 with 1 := getb 2 := H'; Intros Eq0.
Generalize (updateArrayInb
maxN a b ltab Ha Hb La Lb pol Hpol Ar War geta getb (rZMinus c)
Eq0 Hc); Simpl; Auto.
Rewrite <- HpolInv; Intros H'0; Rewrite H'0; Auto.
Absurd False; Auto.
Generalize H'.
Rewrite <- Eq0; Auto.
Unfold evalMnat; Simpl; Auto.
Generalize [s:rZ](wfPd maxN Ar c s Hc War).
Case (getAval maxN vM Ar c Hc); Auto.
Intros r H'0 H'1; Absurd (rVlt (rZMinus c) c); Auto.
Unfold rVlt; Auto.
Rewrite <- H'1; Auto.
Intros l H'0 H'1; Inversion H'1.
Qed.
Theorem
updateArrayEvnb:
(a, b, c:rNat)
(ltab:(rlt a b))
(Ha:(rlt a maxN))
(Hb:(rlt b maxN))
(Hc:(rlt c maxN))
(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 maxN vM))
(War:(wellFormedArray maxN Ar))
(geta:(getAval maxN vM Ar a Ha)=(class La))
(getb:(getAval maxN vM Ar b Hb)=(class Lb))
~ (valRz (evalMnat maxN (mkMem Ar War) c Hc))=b ->
(evalMnat
maxN
(updateMemory
maxN a b ltab Ha Hb La Lb pol Hpol HpolInv HpolAx HpolHpol HpolAxRz Ar
War geta getb) c Hc)=(evalMnat maxN (mkMem Ar War) c Hc).
Intros a b c ltab Ha Hb Hc La Lb pol Hpol HpolInv HpolAx HpolHpol HpolAxRz Ar
War geta getb H'; Unfold evalMnat; Simpl; Auto.
Case (rNatDec a c); Intros Eq0.
Rewrite (getAvalIrr
maxN vM
(updateArray maxN a b ltab Ha Hb La Lb pol Hpol Ar War geta getb) c a
Hc Ha); Auto.
Rewrite (getAvalIrr maxN vM Ar c a Hc Ha); Auto.
Rewrite geta; Auto.
Rewrite (updateArraya maxN a b ltab Ha Hb La Lb pol Hpol Ar War geta getb); Auto.
Rewrite (updateArrayOtherwise
maxN a b ltab Ha Hb La Lb pol Hpol Ar War geta getb c) with Hc := Hc;
Auto.
Red; Intros H'1.
Case (InEqInv ? ? H'1); Intros H'2.
Case H'; Unfold evalMnat; Simpl; Auto.
Rewrite (getAvalIrr maxN vM Ar c (valRz (rZPlus c)) Hc Hc); Auto.
Rewrite (wfPcc1 maxN Ar b (rZPlus c) Hb Hc Lb); Auto.
Case H'; Unfold evalMnat; Simpl; Auto.
Rewrite (getAvalIrr maxN vM Ar c (valRz (rZMinus c)) Hc Hc); Auto.
Rewrite (wfPcc1 maxN Ar b (rZMinus c) Hb Hc Lb); Auto.
Red; Intros H'1; Case H'; Unfold evalMnat; Simpl.
Rewrite (getAvalIrr maxN vM Ar c b Hc Hb); Auto.
Rewrite getb; Auto.
Qed.
Theorem
addEqMemProp1:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN)) (evalMZ maxN M a Ha)=(evalMZ maxN M b Hb) ->
Cases (addEqMem M a b Ha Hb) of
(triple M false L) => L=(dNil maxN)
| _ => False
end.
Intros M a b Ha Hb Eqab; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Intros r; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Rewrite Eqab; Auto.
Intros r; Absurd (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)); Auto.
Rewrite Eqab; Auto.
Case (rZDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Simpl; Auto.
Qed.
Theorem
addEqMemProp2:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))
Cases (addEqMem M a b Ha Hb) of
(triple M' true L) => M=M' /\ L=(dNil maxN)
| _ => True
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Simpl; Auto.
Intros s; Case s; Simpl; Auto.
Case M; Simpl; Auto.
Intros Ar War.
Case (sameSign
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
a Ha)
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
b Hb)); Simpl; Auto.
Case M; Simpl; Auto.
Intros Ar War.
Case (sameSign
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
a Ha)
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
b Hb)); Simpl; Auto.
Case (rZDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Simpl; Auto.
Qed.
Theorem
addEqMemProp3:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
(sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb))=true ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZPlus (valRz (evalMZ maxN M b Hb))) ->
(evalMnat maxN M' c Hc)=(rZPlus (valRz (evalMZ maxN M a Ha)))
| _ => False
end.
Intros M a b Ha Hb Lt0 S0; Unfold addEqMem; Unfold LetP mbDOp.
Rewrite S0; Unfold mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Auto.
Case M; Auto.
Intros Ar War H' c Hc H'1.
Unfold updateMemorySameSign.
Apply updateArrayEvb1 with pol := [x:rZ]x; Simpl; Auto.
Intros H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Simpl; Auto.
Intros H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Simpl; Auto.
Red in H'; Unfold rZlt; Rewrite <- H'; Simpl; Auto.
Qed.
Theorem
addEqMemProp4:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
(sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb))=false ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZPlus (valRz (evalMZ maxN M b Hb))) ->
(evalMnat maxN M' c Hc)=(rZMinus (valRz (evalMZ maxN M a Ha)))
| _ => False
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr0 Eqr1 H'.
Rewrite H'; Auto.
Intros c Hc H'.
Unfold updateMemoryOpSign.
Replace (rZMinus
(valRz
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q)
Ar War) a Ha)))
with ([x:rZ](rZComp x)
(rZPlus
(valRz
(evalMZ
maxN
(exist
(Array maxN vM)
[q:(Array maxN vM)](wellFormedArray maxN q) Ar War) a
Ha)))).
Apply updateArrayEvb1 with pol := [x:rZ](rZComp x); Auto.
Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Red in r; Unfold rZlt; Rewrite <- r; Auto.
Qed.
Theorem
addEqMemProp5:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
(sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb))=true ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZMinus (valRz (evalMZ maxN M b Hb))) ->
(evalMnat maxN M' c Hc)=(rZMinus (valRz (evalMZ maxN M a Ha)))
| _ => False
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr0 Eqr1 H'.
Rewrite H'; Auto.
Intros c Hc H'.
Unfold updateMemorySameSign.
Apply updateArrayEvb2 with pol := [x:rZ]x; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Red in r; Unfold rZlt; Rewrite <- r; Auto.
Qed.
Theorem
addEqMemProp6:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
(sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb))=false ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZMinus (valRz (evalMZ maxN M b Hb))) ->
(evalMnat maxN M' c Hc)=(rZPlus (valRz (evalMZ maxN M a Ha)))
| _ => False
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr0 Eqr1 H'.
Rewrite H'; Auto.
Intros c Hc H'.
Unfold updateMemoryOpSign.
Replace (rZPlus
(valRz
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q)
Ar War) a Ha)))
with ([x:rZ](rZComp x)
(rZMinus
(valRz
(evalMZ
maxN
(exist
(Array maxN vM)
[q:(Array maxN vM)](wellFormedArray maxN q) Ar War) a
Ha)))).
Apply updateArrayEvb2 with pol := [x:rZ](rZComp x); Auto.
Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Red in r; Unfold rZlt; Rewrite <- r; Auto.
Qed.
Theorem
addEqMemProp7:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN)) (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN)) (evalMnat maxN M c Hc)=(evalMZ maxN M b Hb) ->
(evalMnat maxN M' c Hc)=(evalMZ maxN M a Ha)
| _ => False
end.
Intros M a b Ha Hb H'.
Generalize (addEqMemProp3 M a b Ha Hb H');
Generalize (addEqMemProp4 M a b Ha Hb H');
Generalize (addEqMemProp5 M a b Ha Hb H');
Generalize (addEqMemProp6 M a b Ha Hb H'); Auto.
Case (addEqMem M a b Ha Hb); Simpl; Auto.
Intros m b0; Case b0; Auto.
Case (sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case (evalMZ maxN M a Ha); Case (evalMZ maxN M b Hb); Auto.
Qed.
Theorem
addEqMemProp8:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN)) (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZComp (evalMZ maxN M b Hb)) ->
(evalMnat maxN M' c Hc)=(rZComp (evalMZ maxN M a Ha))
| _ => False
end.
Intros M a b Ha Hb H'.
Generalize (addEqMemProp3 M a b Ha Hb H');
Generalize (addEqMemProp4 M a b Ha Hb H');
Generalize (addEqMemProp5 M a b Ha Hb H');
Generalize (addEqMemProp6 M a b Ha Hb H'); Auto.
Case (addEqMem M a b Ha Hb); Simpl; Auto.
Intros m b0; Case b0; Auto.
Case (sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case (evalMZ maxN M a Ha); Case (evalMZ maxN M b Hb); Auto.
Qed.
Theorem
addEqMemProp9:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN)) (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
~ (valRz (evalMnat maxN M c Hc))=(valRz (evalMZ maxN M b Hb)) ->
(evalMnat maxN M' c Hc)=(evalMnat maxN M c Hc)
| _ => False
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Case M; Auto.
Intros Ar War Eqr0 Eqr1.
Case (sameSign
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
a Ha)
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
b Hb)).
Intros c Hc H'.
Unfold updateMemorySameSign.
Replace (evalMnat
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
c Hc) with (evalMnat maxN (mkMem Ar War) c Hc).
Apply updateArrayEvnb; Auto.
Simpl; Auto.
Intros c Hc H'.
Unfold updateMemoryOpSign.
Replace (evalMnat
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
c Hc) with (evalMnat maxN (mkMem Ar War) c Hc).
Apply updateArrayEvnb; Auto.
Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Red in r; Unfold rZlt; Rewrite <- r; Auto.
Qed.
Theorem
addEqMemProp11:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)) ->
(sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb))=true ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZPlus (valRz (evalMZ maxN M a Ha))) ->
(evalMnat maxN M' c Hc)=(rZPlus (valRz (evalMZ maxN M b Hb)))
| _ => False
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr0 Eqr1 H'.
Rewrite H'; Auto.
Intros c Hc H'.
Unfold updateMemorySameSign.
Apply updateArrayEvb1 with pol := [x:rZ]x; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)); Auto.
Red in r; Unfold rZlt; Rewrite <- r; Auto.
Qed.
Theorem
addEqMemProp12:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)) ->
(sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb))=false ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZPlus (valRz (evalMZ maxN M a Ha))) ->
(evalMnat maxN M' c Hc)=(rZMinus (valRz (evalMZ maxN M b Hb)))
| _ => False
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr0 Eqr1 H'.
Rewrite H'; Auto.
Intros c Hc H'.
Unfold updateMemoryOpSign.
Replace (rZMinus
(valRz
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q)
Ar War) b Hb)))
with ([x:rZ](rZComp x)
(rZPlus
(valRz
(evalMZ
maxN
(exist
(Array maxN vM)
[q:(Array maxN vM)](wellFormedArray maxN q) Ar War) b
Hb)))).
Apply updateArrayEvb1 with pol := [x:rZ](rZComp x); Auto.
Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)); Auto.
Red in r; Unfold rZlt; Rewrite <- r; Auto.
Qed.
Theorem
addEqMemProp13:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)) ->
(sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb))=true ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZMinus (valRz (evalMZ maxN M a Ha))) ->
(evalMnat maxN M' c Hc)=(rZMinus (valRz (evalMZ maxN M b Hb)))
| _ => False
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr0 Eqr1 H'.
Rewrite H'; Auto.
Intros c Hc H'.
Unfold updateMemorySameSign.
Apply updateArrayEvb2 with pol := [x:rZ]x; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)); Auto.
Red in r; Unfold rZlt; Rewrite <- r; Auto.
Qed.
Theorem
addEqMemProp14:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)) ->
(sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb))=false ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZMinus (valRz (evalMZ maxN M a Ha))) ->
(evalMnat maxN M' c Hc)=(rZPlus (valRz (evalMZ maxN M b Hb)))
| _ => False
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr0 Eqr1 H'.
Rewrite H'; Auto.
Intros c Hc H'.
Unfold updateMemoryOpSign.
Replace (rZPlus
(valRz
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q)
Ar War) b Hb)))
with ([x:rZ](rZComp x)
(rZMinus
(valRz
(evalMZ
maxN
(exist
(Array maxN vM)
[q:(Array maxN vM)](wellFormedArray maxN q) Ar War) b
Hb)))).
Apply updateArrayEvb2 with pol := [x:rZ](rZComp x); Auto.
Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)); Auto.
Red in r; Unfold rZlt; Rewrite <- r; Auto.
Qed.
Theorem
addEqMemProp15:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN)) (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)) ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN)) (evalMnat maxN M c Hc)=(evalMZ maxN M a Ha) ->
(evalMnat maxN M' c Hc)=(evalMZ maxN M b Hb)
| _ => False
end.
Intros M a b Ha Hb H'.
Generalize (addEqMemProp11 M a b Ha Hb H');
Generalize (addEqMemProp12 M a b Ha Hb H');
Generalize (addEqMemProp13 M a b Ha Hb H');
Generalize (addEqMemProp14 M a b Ha Hb H'); Auto.
Case (addEqMem M a b Ha Hb); Simpl; Auto.
Intros m b0; Case b0; Auto.
Case (sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case (evalMZ maxN M a Ha); Case (evalMZ maxN M b Hb); Auto.
Qed.
Theorem
addEqMemProp16:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN)) (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)) ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
(evalMnat maxN M c Hc)=(rZComp (evalMZ maxN M a Ha)) ->
(evalMnat maxN M' c Hc)=(rZComp (evalMZ maxN M b Hb))
| _ => False
end.
Intros M a b Ha Hb H'.
Generalize (addEqMemProp11 M a b Ha Hb H');
Generalize (addEqMemProp12 M a b Ha Hb H');
Generalize (addEqMemProp13 M a b Ha Hb H');
Generalize (addEqMemProp14 M a b Ha Hb H'); Auto.
Case (addEqMem M a b Ha Hb); Simpl; Auto.
Intros m b0; Case b0; Auto.
Case (sameSign (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case (evalMZ maxN M a Ha); Case (evalMZ maxN M b Hb); Auto.
Qed.
Theorem
addEqMemProp17:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN)) (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)) ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(c:rNat)
(Hc:(rlt c maxN))
~ (valRz (evalMnat maxN M c Hc))=(valRz (evalMZ maxN M a Ha)) ->
(evalMnat maxN M' c Hc)=(evalMnat maxN M c Hc)
| _ => False
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case M; Auto.
Intros Ar War Eqr0 Eqr1.
Case (sameSign
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
a Ha)
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
b Hb)).
Intros c Hc H'.
Unfold updateMemorySameSign.
Replace (evalMnat
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
c Hc) with (evalMnat maxN (mkMem Ar War) c Hc).
Apply updateArrayEvnb; Auto.
Simpl; Auto.
Intros c Hc H'.
Unfold updateMemoryOpSign.
Replace (evalMnat
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
c Hc) with (evalMnat maxN (mkMem Ar War) c Hc).
Apply updateArrayEvnb; Auto.
Simpl; Auto.
Intros r H'; Absurd (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)); Auto.
Red in r; Unfold rZlt; Rewrite <- r; Auto.
Qed.
Theorem
addEqMemProp18:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))
Cases (addEqMem M a b Ha Hb) of
(triple M' b L) => (eqExceptOn maxN M' M L)
| _ => True
end.
Intros M a b Ha Hb; Unfold addEqMem.
Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Clear s; Simpl; Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr.
Case (sameSign
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
a Ha)
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
b Hb)).
Unfold eqExceptOn; Simpl.
Intros a0 Maxa H'.
Apply updateArrayOtherwise; Auto.
Red; Intros H'0; Case H'; Red; Simpl; Repeat (Apply InEqSkip; Auto).
Red; Intros H'0; Case H'; Rewrite H'0; Red; Simpl.
Apply InEqHead; Auto.
Red; Intros H'0; Case H'; Rewrite H'0; Red; Simpl.
Apply InEqSkip; Apply InEqHead; Auto.
Unfold eqExceptOn; Simpl.
Intros a0 Maxa H'.
Apply updateArrayOtherwise; Auto.
Red; Intros H'0; Case H'; Red; Simpl; Repeat (Apply InEqSkip; Auto).
Red; Intros H'0; Case H'; Rewrite H'0; Red; Simpl.
Apply InEqHead; Auto.
Red; Intros H'0; Case H'; Rewrite H'0; Red; Simpl.
Apply InEqSkip; Apply InEqHead; Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr.
Case (sameSign
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
a Ha)
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
b Hb)).
Unfold eqExceptOn; Simpl.
Intros a0 Maxa H'.
Apply updateArrayOtherwise; Auto.
Red; Intros H'0; Case H'; Red; Simpl; Repeat (Apply InEqSkip; Auto).
Red; Intros H'0; Case H'; Rewrite H'0; Red; Simpl.
Apply InEqHead; Auto.
Red; Intros H'0; Case H'; Rewrite H'0; Red; Simpl.
Apply InEqSkip; Apply InEqHead; Auto.
Unfold eqExceptOn; Simpl.
Intros a0 Maxa H'.
Apply updateArrayOtherwise; Auto.
Red; Intros H'0; Case H'; Red; Simpl; Repeat (Apply InEqSkip; Auto).
Red; Intros H'0; Case H'; Rewrite H'0; Red; Simpl.
Apply InEqHead; Auto.
Red; Intros H'0; Case H'; Rewrite H'0; Red; Simpl.
Apply InEqSkip; Apply InEqHead; Auto.
Case (rZDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros H' H'0; Red; Auto.
Intros H' H'0; Red; Auto.
Qed.
Theorem
addEqMemProp19:
(M:(Mem maxN))
(a, b, c:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(Hc:(rVlt c maxN))
(rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
(evalMZ maxN M c Hc)=(evalMZ maxN M b Hb) ->Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(evalMZ maxN M' c Hc)=
(evalMZ maxN M a Ha)
| _ => False
end.
Intros M a b c; Case c; Auto.
Intros r Ha Hb Hc H'.
Generalize (addEqMemProp7 M a b Ha Hb H').
Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Case b0; Simpl; Auto.
Intros r Ha Hb Hc H'.
Generalize (addEqMemProp8 M a b Ha Hb H').
Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Case b0; Simpl; Auto.
Intros H'0 H'1 H'2; Rewrite (H'1 r Hc); Auto.
Rewrite <- H'2; Auto.
Qed.
Theorem
addEqMemProp20:
(M:(Mem maxN))
(a, b, c:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(Hc:(rVlt c maxN))
(rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)) ->
(evalMZ maxN M c Hc)=(evalMZ maxN M a Ha) ->Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(evalMZ maxN M' c Hc)=
(evalMZ maxN M b Hb)
| _ => False
end.
Intros M a b c; Case c; Auto.
Intros r Ha Hb Hc H'.
Generalize (addEqMemProp15 M a b Ha Hb H').
Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Case b0; Simpl; Auto.
Intros r Ha Hb Hc H'.
Generalize (addEqMemProp16 M a b Ha Hb H').
Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Case b0; Simpl; Auto.
Intros H'0 H'1 H'2; Rewrite (H'1 r Hc); Auto.
Rewrite <- H'2; Auto.
Qed.
Theorem
addEqMemProp21:
(M:(Mem maxN))
(a, b, c:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(Hc:(rVlt c maxN))
(rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
~ (valRz (evalMZ maxN M c Hc))=(valRz (evalMZ maxN M b Hb)) ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) => (evalMZ maxN M' c Hc)=(evalMZ maxN M c Hc)
| _ => False
end.
Intros M a b c; Case c; Auto.
Intros r Ha Hb Hc H'.
Generalize (addEqMemProp9 M a b Ha Hb H').
Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Case b0; Simpl; Auto.
Intros r Ha Hb Hc H'.
Generalize (addEqMemProp9 M a b Ha Hb H').
Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Case b0; Simpl; Auto.
Intros H'0 H'1 H'2.
Rewrite H'1; Auto.
Generalize H'2; Case (evalMnat maxN M r Hc); Case (evalMZ maxN M b Hb); Auto.
Qed.
Theorem
addEqMemProp22:
(M:(Mem maxN))
(a, b, c:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(Hc:(rVlt c maxN))
(rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)) ->
~ (valRz (evalMZ maxN M c Hc))=(valRz (evalMZ maxN M a Ha)) ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) => (evalMZ maxN M' c Hc)=(evalMZ maxN M c Hc)
| _ => False
end.
Intros M a b c; Case c; Auto.
Intros r Ha Hb Hc H'.
Generalize (addEqMemProp17 M a b Ha Hb H').
Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Case b0; Simpl; Auto.
Intros r Ha Hb Hc H'.
Generalize (addEqMemProp17 M a b Ha Hb H').
Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Case b0; Simpl; Auto.
Intros H'0 H'1 H'2.
Rewrite H'1; Auto.
Generalize H'2; Case (evalMnat maxN M r Hc); Case (evalMZ maxN M b Hb); Auto.
Qed.
Theorem
addEqMemProp23:
(M:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN)) (eqRz (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)) ->
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) => M=M' /\ (evalMZ maxN M a Ha)=(evalMZ maxN M b Hb)
| _ => True
end.
Intros M a b Ha Hb H'; Unfold addEqMem; Unfold LetP mbDOp; Auto.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Clear s.
Intros r; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto;
Unfold rZlt; Red in H'; Rewrite H'; Auto.
Intros r; Absurd (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)); Auto;
Unfold rZlt; Red in H'; Rewrite H'; Auto.
Case (rZDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Qed.
Theorem
NotrZEq: (a, b:rZ) ~ a=b -> ~ a=(rZComp b) ->~ (valRz a)=(valRz b).
Intros a b; Case a; Case b; Simpl; Auto; Intros r r0 H' H'1; Red; Intros H'4;
(Case H'; Rewrite H'4; Auto; Fail) Orelse (Case H'1; Rewrite H'4; Auto; Fail).
Qed.
Hints Resolve NotrZEq.
Theorem
addEqMemProp24:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(inclState (addEq (a, b) (memF maxN M)) (memF maxN M'))
| _ => True
end.
Intros M a b Ha Hb; Generalize [c:rZ](addEqMemProp19 M a b c Ha Hb);
Generalize [c:rZ](addEqMemProp20 M a b c Ha Hb);
Generalize [c:rZ](addEqMemProp21 M a b c Ha Hb);
Generalize [c:rZ](addEqMemProp22 M a b c Ha Hb);
Generalize (addEqMemProp23 M a b Ha Hb); Auto.
Case (addEqMem M a b Ha Hb); Auto.
Intros M' b0; Case b0; Simpl; Auto.
Intros L; Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)).
Intros s; Case s; Clear s.
Intros Eq0 Prop23 Prop22 Prop21 Prop20 Prop19.
Cut (eqStateRz (memF maxN M') a b); [Intros Eqab | Idtac].
Apply inclStateAddEqInv; Auto.
Red; Auto.
Intros i j H'0.
Case (rZDec i j); Intros Eqij.
Rewrite <- Eqij; Auto.
Elim (evalCorrectAux maxN i j M); Auto.
Intros Hi H'2; Elim H'2; Clear H'2; Intros Hj H'2;
Specialize 2 H'2 with Maxa := Hi Maxb := Hj; Intros H'3.
Apply evalInv with Maxa := Hi Maxb := Hj; Auto.
Case (rZDec (evalMZ maxN M i Hi) (evalMZ maxN M b Hb)); Intros Eq1.
Rewrite Prop19; Auto.
Apply sym_equal; Auto.
Apply Prop19; Auto.
Rewrite <- Eq1; Auto.
Case (rZDec (evalMZ maxN M i Hi) (rZComp (evalMZ maxN M b Hb))); Intros Eq2.
Cut (evalMZ maxN M' (rZComp i) (rVltrZComp ? ? Hi))=
(evalMZ maxN M' (rZComp j) (rVltrZComp ? ? Hj)).
Generalize Hi Hj; Case i; Case j; Simpl; Auto; Intros r r0 Hi0 Hj0;
Rewrite evalMnatIrr with n1 := r0 n2 := r0 Ltn2 := Hi0; Auto;
Rewrite evalMnatIrr with n1 := r n2 := r Ltn2 := Hj0; Auto; Intros tmo;
Apply rZCompEq; Auto; Repeat Rewrite <- rZCompInvol; Auto.
Rewrite Prop19; Auto.
Apply sym_equal; Auto.
Apply Prop19; Auto.
Apply rZCompEq; Auto.
Rewrite <- Eq2; Auto.
Rewrite (evalMZComp maxN M j Hj); Auto; Rewrite <- rZCompInvol; Auto.
Rewrite (evalMZComp maxN M i Hi); Auto; Rewrite Eq2; Rewrite <- rZCompInvol;
Auto.
Repeat Rewrite Prop21; Auto.
Rewrite <- H'3; Auto.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Rewrite (Prop19 b); Auto.
Apply Prop21; Auto.
Red; Intros H'; Absurd (rZlt (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto;
Unfold rZlt; Rewrite H'; Auto.
Intros Eq0 Prop23 Prop22 Prop21 Prop20 Prop19.
Cut (eqStateRz (memF maxN M') a b); [Intros Eqab | Idtac].
Apply inclStateAddEqInv; Auto.
Red; Auto.
Intros i j H'0.
Case (rZDec i j); Intros Eqij.
Rewrite <- Eqij; Auto.
Elim (evalCorrectAux maxN i j M); Auto.
Intros Hi H'2; Elim H'2; Clear H'2; Intros Hj H'2;
Specialize 2 H'2 with Maxa := Hi Maxb := Hj; Intros H'3.
Apply evalInv with Maxa := Hi Maxb := Hj; Auto.
Case (rZDec (evalMZ maxN M i Hi) (evalMZ maxN M a Ha)); Intros Eq1.
Rewrite Prop20; Auto.
Apply sym_equal; Auto.
Apply Prop20; Auto.
Rewrite <- Eq1; Auto.
Case (rZDec (evalMZ maxN M i Hi) (rZComp (evalMZ maxN M a Ha))); Intros Eq2.
Cut (evalMZ maxN M' (rZComp i) (rVltrZComp ? ? Hi))=
(evalMZ maxN M' (rZComp j) (rVltrZComp ? ? Hj)).
Generalize Hi Hj; Case i; Case j; Simpl; Auto; Intros r r0 Hi0 Hj0;
Rewrite evalMnatIrr with n1 := r0 n2 := r0 Ltn2 := Hi0; Auto;
Rewrite evalMnatIrr with n1 := r n2 := r Ltn2 := Hj0; Auto; Intros tmo;
Apply rZCompEq; Auto; Repeat Rewrite <- rZCompInvol; Auto.
Rewrite Prop20; Auto.
Apply sym_equal; Auto.
Apply Prop20; Auto.
Apply rZCompEq; Auto.
Rewrite <- Eq2; Auto.
Rewrite (evalMZComp maxN M j Hj); Auto; Rewrite <- rZCompInvol; Auto.
Rewrite (evalMZComp maxN M i Hi); Auto; Rewrite Eq2; Rewrite <- rZCompInvol;
Auto.
Repeat Rewrite Prop22; Auto.
Rewrite <- H'3; Auto.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Rewrite (Prop20 a); Auto.
Apply sym_equal; Apply Prop22; Auto.
Red; Intros H'; Absurd (rZlt (evalMZ maxN M b Hb) (evalMZ maxN M a Ha)); Auto;
Unfold rZlt; Rewrite H'; Auto.
Intros H' H'0 H'1 H'2 H'3 H'4; Elim H'0; Auto.
Intros H'5 H'6; Apply inclStateAddEqInv; Auto.
Rewrite <- H'5; Auto.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Rewrite <- H'5; Auto.
Qed.
Theorem
addEqMemProp25:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(inclState (memF maxN M') (addEq (a, b) (memF maxN M)))
| _ => True
end.
Intros M a b Ha Hb; Generalize [c:rZ](addEqMemProp19 M a b c Ha Hb);
Generalize [c:rZ](addEqMemProp20 M a b c Ha Hb);
Generalize [c:rZ](addEqMemProp21 M a b c Ha Hb);
Generalize [c:rZ](addEqMemProp22 M a b c Ha Hb);
Generalize (addEqMemProp23 M a b Ha Hb);
Generalize (addEqMemProp24 M a b Ha Hb).
Case (addEqMem M a b Ha Hb); Auto.
Intros M' b0; Case b0; Simpl; Auto.
Intros L; Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)).
Intros s; Case s; Clear s.
Intros Eq0 Prop24 Prop23 Prop22 Prop21 Prop20 Prop19.
Red; Auto.
Intros i j Hij.
Case (rZDec i j); Intros Eqij.
Rewrite <- Eqij; Auto.
Elim (evalCorrectAux maxN i j M'); Auto.
Intros Hi H'2; Elim H'2; Clear H'2; Intros Hj H'2;
Specialize 2 H'2 with Maxa := Hi Maxb := Hj; Intros H'3.
Case (rZDec (evalMZ maxN M i Hi) (evalMZ maxN M b Hb)); Intros Eq1.
Case (rZDec (evalMZ maxN M j Hj) (evalMZ maxN M b Hb)); Intros Eq2.
Apply eqStateRzTrans with b := b; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := Hb; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hb Maxb := Hj; Auto.
Case (rZDec (evalMZ maxN M j Hj) (rZComp (evalMZ maxN M b Hb))); Intros Eq3.
Absurd (contradictory (memF maxN M)); Auto.
Apply memFNotContradictory; Auto.
Red; Auto.
Exists a.
Apply evalInv with Maxa := Ha Maxb := (rVltrZComp ? ? Ha); Auto.
Rewrite <- (Prop19 i Hi); Auto.
Rewrite H'3; Auto.
Rewrite (evalMZComp maxN M a Ha (rVltrZComp ? ? Ha)); Auto.
Rewrite <- (Prop19 (rZComp j) (rVltrZComp ? ? Hj)); Auto.
Rewrite (evalMZComp maxN M' j Hj (rVltrZComp ? ? Hj)); Auto.
Rewrite (evalMZComp maxN M j Hj (rVltrZComp ? ? Hj)); Auto.
Rewrite Eq3; Auto.
Apply eqStateRzTrans with b := b; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := Hb; Auto.
Apply eqStateRzTrans with b := a; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Ha Maxb := Hj; Auto.
Rewrite <- (Prop19 i Hi); Auto.
Rewrite H'3; Auto.
Case (rZDec (evalMZ maxN M i Hi) (rZComp (evalMZ maxN M b Hb))); Intros Eq2.
Case (rZDec (evalMZ maxN M j Hj) (evalMZ maxN M b Hb)); Intros Eq3.
Absurd (contradictory (memF maxN M)); Auto.
Apply memFNotContradictory; Auto.
Red; Auto.
Exists a.
Apply evalInv with Maxa := Ha Maxb := (rVltrZComp ? ? Ha); Auto.
Rewrite <- (Prop19 j Hj); Auto.
Rewrite <- H'3; Auto.
Rewrite (evalMZComp maxN M a Ha); Auto.
Rewrite <- (Prop19 (rZComp i) (rVltrZComp ? ? Hi)); Auto.
Rewrite (evalMZComp maxN M' i Hi); Auto.
Rewrite (evalMZComp maxN M i Hi); Auto.
Rewrite Eq2; Auto.
Case (rZDec (evalMZ maxN M j Hj) (rZComp (evalMZ maxN M b Hb))); Intros Eq4.
Apply eqStateRzTrans with b := (rZComp b); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := (rVltrZComp ? ? Hb); Auto.
Rewrite (evalMZComp maxN M b Hb); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxb := Hj Maxa := (rVltrZComp ? ? Hb); Auto.
Rewrite (evalMZComp maxN M b Hb); Auto.
Apply eqStateRzTrans with b := (rZComp b); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := (rVltrZComp ? ? Hb); Auto.
Rewrite (evalMZComp maxN M b Hb); Auto.
Apply eqStateRzTrans with b := (rZComp a); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxb := Hj Maxa := (rVltrZComp ? ? Ha); Auto.
Rewrite <- (Prop21 j); Auto.
Rewrite <- H'3; Auto.
Rewrite (evalMZComp maxN M a Ha); Auto.
Rewrite <- (Prop19 (rZComp i) (rVltrZComp ? ? Hi)); Auto.
Rewrite (evalMZComp maxN M' i Hi); Auto.
Rewrite (evalMZComp maxN M i Hi); Auto.
Rewrite Eq2; Auto.
Case (rZDec (evalMZ maxN M j Hj) (evalMZ maxN M b Hb)); Intros Eq3.
Apply eqStateRzTrans with b := a; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := Ha; Auto.
Rewrite <- (Prop21 i); Auto.
Rewrite H'3; Auto.
Apply eqStateRzTrans with b := b; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxb := Hj Maxa := Hb; Auto.
Case (rZDec (evalMZ maxN M j Hj) (rZComp (evalMZ maxN M b Hb))); Intros Eq4.
Apply eqStateRzTrans with b := (rZComp a); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := (rVltrZComp ? ? Ha); Auto.
Rewrite (evalMZComp maxN M a Ha); Auto.
Rewrite <- (Prop19 (rZComp j) (rVltrZComp ? ? Hj)); Auto.
Rewrite (evalMZComp maxN M' j Hj); Auto.
Rewrite <- H'3; Auto.
Rewrite <- Prop21; Auto.
Rewrite (evalMZComp maxN M j Hj); Auto.
Rewrite Eq4; Auto.
Apply eqStateRzTrans with b := (rZComp b); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxb := Hj Maxa := (rVltrZComp ? ? Hb); Auto.
Rewrite (evalMZComp maxN M b Hb); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := Hj; Auto.
Rewrite <- (Prop21 i); Auto.
Rewrite <- (Prop21 j); Auto.
Intros Eq0 Prop24 Prop23 Prop22 Prop21 Prop20 Prop19.
Red; Auto.
Intros i j Hij.
Case (rZDec i j); Intros Eqij.
Rewrite <- Eqij; Auto.
Elim (evalCorrectAux maxN i j M'); Auto.
Intros Hi H'2; Elim H'2; Clear H'2; Intros Hj H'2;
Specialize 2 H'2 with Maxa := Hi Maxb := Hj; Intros H'3.
Case (rZDec (evalMZ maxN M i Hi) (evalMZ maxN M a Ha)); Intros Eq1.
Case (rZDec (evalMZ maxN M j Hj) (evalMZ maxN M a Ha)); Intros Eq2.
Apply eqStateRzTrans with b := a; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := Ha; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Ha Maxb := Hj; Auto.
Case (rZDec (evalMZ maxN M j Hj) (rZComp (evalMZ maxN M a Ha))); Intros Eq3.
Absurd (contradictory (memF maxN M)); Auto.
Apply memFNotContradictory; Auto.
Red; Auto.
Exists b.
Apply evalInv with Maxa := Hb Maxb := (rVltrZComp ? ? Hb); Auto.
Rewrite <- (Prop20 i Hi); Auto.
Rewrite H'3; Auto.
Rewrite (evalMZComp maxN M b Hb); Auto.
Rewrite <- (Prop20 (rZComp j) (rVltrZComp ? ? Hj)); Auto.
Rewrite (evalMZComp maxN M' j Hj); Auto.
Rewrite (evalMZComp maxN M j Hj); Auto.
Rewrite Eq3; Auto.
Apply eqStateRzTrans with b := a; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := Ha; Auto.
Apply eqStateRzTrans with b := b; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hb Maxb := Hj; Auto.
Rewrite <- (Prop20 i Hi); Auto.
Rewrite H'3; Auto.
Case (rZDec (evalMZ maxN M i Hi) (rZComp (evalMZ maxN M a Ha))); Intros Eq2.
Case (rZDec (evalMZ maxN M j Hj) (evalMZ maxN M a Ha)); Intros Eq3.
Absurd (contradictory (memF maxN M)); Auto.
Apply memFNotContradictory; Auto.
Red; Auto.
Exists b.
Apply evalInv with Maxa := Hb Maxb := (rVltrZComp ? ? Hb); Auto.
Rewrite <- (Prop20 j Hj); Auto.
Rewrite <- H'3; Auto.
Rewrite (evalMZComp maxN M b Hb); Auto.
Rewrite <- (Prop20 (rZComp i) (rVltrZComp ? ? Hi)); Auto.
Rewrite (evalMZComp maxN M' i Hi); Auto.
Rewrite (evalMZComp maxN M i Hi); Auto.
Rewrite Eq2; Auto.
Case (rZDec (evalMZ maxN M j Hj) (rZComp (evalMZ maxN M a Ha))); Intros Eq4.
Apply eqStateRzTrans with b := (rZComp a); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := (rVltrZComp ? ? Ha); Auto.
Rewrite (evalMZComp maxN M a Ha); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxb := Hj Maxa := (rVltrZComp ? ? Ha); Auto.
Rewrite (evalMZComp maxN M a Ha); Auto.
Apply eqStateRzTrans with b := (rZComp a); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := (rVltrZComp ? ? Ha); Auto.
Rewrite (evalMZComp maxN M a Ha); Auto.
Apply eqStateRzTrans with b := (rZComp b); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxb := Hj Maxa := (rVltrZComp ? ? Hb); Auto.
Rewrite <- (Prop22 j); Auto.
Rewrite <- H'3; Auto.
Rewrite (evalMZComp maxN M b Hb); Auto.
Rewrite <- (Prop20 (rZComp i) (rVltrZComp ? ? Hi)); Auto.
Rewrite (evalMZComp maxN M' i Hi); Auto.
Rewrite (evalMZComp maxN M i Hi); Auto.
Rewrite Eq2; Auto.
Case (rZDec (evalMZ maxN M j Hj) (evalMZ maxN M a Ha)); Intros Eq3.
Apply eqStateRzTrans with b := b; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := Hb; Auto.
Rewrite <- (Prop22 i); Auto.
Rewrite H'3; Auto.
Apply eqStateRzTrans with b := a; Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxb := Hj Maxa := Ha; Auto.
Case (rZDec (evalMZ maxN M j Hj) (rZComp (evalMZ maxN M a Ha))); Intros Eq4.
Apply eqStateRzTrans with b := (rZComp b); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := (rVltrZComp ? ? Hb); Auto.
Rewrite (evalMZComp maxN M b Hb); Auto.
Rewrite <- (Prop20 (rZComp j) (rVltrZComp ? ? Hj)); Auto.
Rewrite (evalMZComp maxN M' j Hj); Auto.
Rewrite <- H'3; Auto.
Rewrite <- Prop22; Auto.
Rewrite (evalMZComp maxN M j Hj); Auto.
Rewrite Eq4; Auto.
Apply eqStateRzTrans with b := (rZComp a); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxb := Hj Maxa := (rVltrZComp ? ? Ha); Auto.
Rewrite (evalMZComp maxN M a Ha); Auto.
Apply eqStateaddEq2; Auto.
Apply evalInv with Maxa := Hi Maxb := Hj; Auto.
Rewrite <- (Prop22 i); Auto.
Rewrite <- (Prop22 j); Auto.
Intros H' H'0 H'1 H'2 H'3 H'4 H'5.
Elim H'1; [Intros H'7 H'8; Rewrite <- H'7; Clear H'1 | Clear H'1]; Auto.
Qed.
Theorem
addEqMemProp26:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))
Cases (addEqMem M a b Ha Hb) of
(triple M' false L) =>
(eqState (addEq (a, b) (memF maxN M)) (memF maxN M'))
| _ => True
end.
Intros M a b Ha Hb; Generalize (addEqMemProp24 M a b Ha Hb);
Generalize (addEqMemProp25 M a b Ha Hb); Case (addEqMem M a b Ha Hb).
Intros m b0 H'; Case b0; Auto.
Intros H'0 H'1; Red; Auto.
Qed.
Theorem
addEqMemProp27:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))
Cases (addEqMem M a b Ha Hb) of
(triple M' b L) =>
~ L=(dNil maxN) ->~ (eqState (memF maxN M) (memF maxN M'))
end.
Intros M a b Ha Hb; Unfold addEq; Generalize (addEqMemProp1 M a b Ha Hb);
Generalize (addEqMemProp2 M a b Ha Hb);
Generalize (addEqMemProp26 M a b Ha Hb); Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Case b0; Auto.
Intros d H' H'0; Elim H'0; Auto.
Intros d H' H'0 H'1 H'2; Red; Intros H'3; Try Exact H'3.
Apply H'2; Auto.
Apply H'1; Auto.
Case (rZDec a b); Intros Eq0; Auto.
Apply evalMZIrr; Auto.
Elim (evalCorrectAux maxN a b M);
[Intros H'8 H'9; Elim H'9; Intros H'10 H'11;
Specialize 2 H'11 with Maxa := Ha Maxb := Hb; Intros H'13; Clear H'9 |
Idtac | Idtac]; Auto.
Apply eqStateEq with S1 := (addEq (a, b) (memF maxN M)); Auto.
Apply eqStateTrans with S2 := (memF maxN m); Auto.
Qed.
Theorem
addEqMemProp28:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))
Cases (addEqMem M a b Ha Hb) of
(triple M' true L) => (evalMZ maxN M a Ha)=(rZComp (evalMZ maxN M b Hb))
| _ => True
end.
Intros M a b Ha Hb; Unfold addEqMem; Unfold LetP mbDOp.
Case (rZltEDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Intros s; Case s; Simpl; Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr0.
Case (sameSign
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
a Ha)
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
b Hb)); Auto.
Case M; Simpl; Auto.
Intros Ar War Eqr0.
Case (sameSign
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
a Ha)
(evalMZ
maxN
(exist
(Array maxN vM) [q:(Array maxN vM)](wellFormedArray maxN q) Ar War)
b Hb)); Auto.
Case (rZDec (evalMZ maxN M a Ha) (evalMZ maxN M b Hb)); Auto.
Case (evalMZ maxN M a Ha); Case (evalMZ maxN M b Hb); Unfold eqRz; Simpl; Auto;
Intros r r0 H' H'0; Try Rewrite H'0; Auto; Case H'; Rewrite H'0; Auto.
Qed.
Definition
getMem :=
[T:mbD]
Cases T of
(triple m b l) => m
end.
Definition
getBool :=
[T:mbD]
Cases T of
(triple m b l) => b
end.
Definition
getList :=
[T:mbD]
Cases T of
(triple m b l) => l
end.
Theorem
addEqMemNEq:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))
(nEq maxN M (getMem (addEqMem M a b Ha Hb)) (getList (addEqMem M a b Ha Hb))).
Intros M a b Ha Hb; Unfold nEq; Generalize (addEqMemProp27 M a b Ha Hb).
Case (addEqMem M a b Ha Hb); Auto.
Intros m b0; Simpl; Auto.
Intros d H' H'0; Red; Intros H'1.
LApply H'; Clear H'; [Intros H'2; Case H'2 | Idtac].
Apply eqMemEqState; Auto.
Red; Intros H'; Absurd (notDnil maxN d); Auto; Rewrite H'; Auto.
Qed.
End update.
05/07/100, 11:37