interImplement.v
Require Import rZ.
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.
Require Export addEqImplement2.
Require Export interState.
Section inter.
Variable LL:(list triplet).
Variable maxN:rNat.
Hypothesis HmaxN:maxN=(rnext (maxVarTriplets LL)).
Definition
getEquivAux:
(M:(Mem maxN)) (a:rNat) (Ha:(rlt a maxN)){Res:(list rZ) * bool | Cases Res of
(pair
L true)
=>
(OlistRz
L)
/\
(((c:rZ)
(In
c
L) ->
(rVlt
c
maxN))
/\
((c:rZ)
(Hc:(rVlt
c
maxN))
(iff
(In
(rZComp
c)
L)
(evalMZ
maxN
M
c
Hc)=
(evalMZ
maxN
M
(rZPlus
a)
Ha))))
| (pair
L
false)
=>
(OlistRz
L)
/\
(((c:rZ)
(In
c
L) ->
(rVlt
c
maxN))
/\
((c:rZ)
(Hc:(rVlt
c
maxN))
(iff
(In
c
L)
(evalMZ
maxN
M
c
Hc)=
(evalMZ
maxN
M
(rZPlus
a)
Ha))))
end}.
Intros M a Ha; Generalize (refl_equal ? (eMZ maxN M a Ha));
Pattern -1 (eMZ maxN M a Ha); Case (eMZ maxN M a Ha).
Intros r; Case r.
Intros r0 H'; (Cut (rlt r0 maxN); [Intros Hr0 | Idtac]).
Generalize (refl_equal ? (eMZ maxN M r0 Hr0)); Pattern -1 (eMZ maxN M r0 Hr0);
Case (eMZ maxN M r0 Hr0).
Intros r1 H'0; Absurd False; Auto.
Generalize H' H'0; Case M; Simpl; Auto.
Intros Ar War H'2;
Change ~ <vM> (getAval maxN vM Ar (valRz (rZPlus r0)) Hr0)=(ref r1).
Apply wfPcr with r := a Hr := Ha; Auto.
Intros L HL; Exists ((cons (rZPlus r0) L), false); Split; Auto.
Generalize HL; Case L; Auto.
Intros H'0; Red; Apply OlistOne; Auto.
Intros r1 l H'0.
Red; Apply OlistCons; Auto.
Apply eMZOlist with 1 := H'0; Auto.
Generalize H'0; Case M; Simpl; Auto.
Intros Ar War H'2; Red; Simpl; Auto.
Apply wellFormedArrayInImpLt with 2 := H'2; Auto with datatypes.
Simpl; Auto.
Rewrite eMZevalMnat; Rewrite H'; Auto.
Split; Auto.
Intros c H'0; Elim H'0; Clear H'0; Intros H'0; Auto.
Rewrite <- H'0; Auto.
Apply eMZlt' with 1 := HL; Auto.
Red; Apply inImpInEq; Auto.
Intros c Hc; Red; Split.
Intros H'0; Elim H'0; Clear H'0; Intros H'1.
Rewrite (evalMZIrr maxN M c (rZPlus r0) Hc Hr0); Auto.
Simpl; Rewrite eMZevalMnat; Rewrite HL; Auto.
Cut <vM> (eMZ maxN M (valRz c) Hc)=(ref (samePol c r0)).
Generalize Hc; Case c; Simpl; Auto; Intros r1 Hc0; Rewrite eMZevalMnat;
Intros H'0; Rewrite H'0; Auto.
Apply eMZref with L := L Ha := Hr0; Auto.
Generalize Hc; Case c; Simpl; Auto.
Generalize HL; Case M; Simpl; Auto.
Intros Ar War H'1 r1 Hc0.
Generalize (refl_equal ? (getAval maxN vM Ar r1 Hc0));
Pattern -1 (getAval maxN vM Ar r1 Hc0); Case (getAval maxN vM Ar r1 Hc0); Auto.
Intros r2 H'0 H'2; Rewrite H'2 in H'0; Auto.
Right.
Change (In (samePol (rZPlus r0) r1) L); Auto.
Apply wfPcc2 with 2 := H'0 3 := H'1; Auto.
Generalize HL; Case M; Simpl; Auto.
Intros Ar War H'1 r1 Hc0.
Generalize (refl_equal ? (getAval maxN vM Ar r1 Hc0));
Pattern -1 (getAval maxN vM Ar r1 Hc0); Case (getAval maxN vM Ar r1 Hc0); Auto.
Right.
Change (In (samePol (rZMinus r0) r1) L); Auto.
Cut (rVlt (rZMinus r0) maxN); [Intros Hr0' | Idtac]; Auto.
Apply wfPcc2 with n := maxN Ar := Ar Hs := Hr0' Hr := Hc0; Auto.
Replace (rZMinus r0) with (rZComp (rZPlus r0)); Auto.
Rewrite <- H0; Rewrite <- rZCompInvol; Rewrite <- H; Auto.
Rewrite <- H'1; Apply getAvalIrr; Auto.
Apply rltTrans with y := a; Auto.
Change (rVlt (rZPlus r0) a); Auto.
Apply eMZlt with 1 := H'; Auto.
Intros r0 H'; (Cut (rlt r0 maxN); [Intros Hr0 | Idtac]).
Generalize (refl_equal ? (eMZ maxN M r0 Hr0)); Pattern -1 (eMZ maxN M r0 Hr0);
Case (eMZ maxN M r0 Hr0).
Intros r1 H'0; Absurd False; Auto.
Generalize H' H'0; Case M; Simpl; Auto.
Intros Ar War H'2;
Change ~ <vM> (getAval maxN vM Ar (valRz (rZMinus r0)) Hr0)=(ref r1).
Apply wfPcr with r := a Hr := Ha; Auto.
Intros L HL; Exists ((cons (rZPlus r0) L), true); Split.
Generalize HL; Case L; Auto.
Intros H'0; Red; Apply OlistOne; Auto.
Intros r1 l H'0.
Red; Apply OlistCons; Auto.
Apply eMZOlist with 1 := H'0; Auto.
Generalize H'0; Case M; Simpl; Auto.
Intros Ar War H'2; Red; Simpl; Auto.
Apply wellFormedArrayInImpLt with 2 := H'2; Auto with datatypes.
Simpl; Auto.
Rewrite eMZevalMnat; Rewrite H'; Auto.
Split; Auto.
Intros c H'0; Elim H'0; Clear H'0; Intros H'0; Auto.
Rewrite <- H'0; Auto.
Apply eMZlt' with 1 := HL; Auto.
Red; Apply inImpInEq; Auto.
Intros c Hc; Red; Split.
Intros H'0; Elim H'0; Clear H'0; Intros H'1.
Rewrite (evalMZIrr maxN M c (rZMinus r0) Hc Hr0); Auto.
Simpl; Rewrite eMZevalMnat; Rewrite HL; Auto.
Apply rZCompEq; Simpl; Auto.
Cut (rVlt (rZComp c) maxN); [Intros Hc' | Apply rVltrZComp]; Auto.
Cut <vM> (eMZ maxN M (valRz (rZComp c)) Hc')=(ref (samePol (rZComp c) r0)).
Generalize Hc' Hc; Case c; Simpl; Intros r1 Hc'0 Hc0;
Rewrite (eMZIrr maxN M r1 r1 Hc'0 Hc0); Auto; Rewrite eMZevalMnat; Intros H'0;
Rewrite H'0; Auto.
Apply eMZref with L := L Ha := Hr0; Auto.
Generalize Hc; Case c; Simpl; Auto.
Generalize HL; Case M; Simpl; Auto.
Intros Ar War H'1 r1 Hc0.
Generalize (refl_equal ? (getAval maxN vM Ar r1 Hc0));
Pattern -1 (getAval maxN vM Ar r1 Hc0); Case (getAval maxN vM Ar r1 Hc0); Auto.
Intros r2 H'0 H'2; Rewrite H'2 in H'0; Auto.
Right.
Change (In (samePol (rZMinus r0) r1) L); Auto.
Apply wfPcc2 with 2 := H'0 3 := H'1; Auto.
Intros l H'0 H'2; Left; Apply rZCompEq; Auto.
Generalize HL; Case M; Simpl; Auto.
Intros Ar War H'1 r1 Hc0.
Generalize (refl_equal ? (getAval maxN vM Ar r1 Hc0));
Pattern -1 (getAval maxN vM Ar r1 Hc0); Case (getAval maxN vM Ar r1 Hc0); Auto.
Right.
Change (In (samePol (rZPlus r0) r1) L); Auto.
Apply (wfPcc2 ? Ar r1 (rZPlus r0) Hc0 Hr0); Auto.
Replace (rZPlus r0) with (rZComp (rZMinus r0)); Auto.
Rewrite <- H0; Rewrite <- rZCompInvol; Auto.
Simpl; Intros l H'0 H'2; Left; Apply rZCompEq; Auto.
Apply rltTrans with y := a; Auto.
Change (rVlt (rZMinus r0) a); Auto.
Apply eMZlt with 1 := H'; Auto.
Intros L H'; Exists ((cons (rZPlus a) L), false); Split.
Generalize H'; Case L.
Intros H'0; Red; Apply OlistOne; Auto.
Intros r l H'0; Red; Apply OlistCons; Auto.
Apply eMZOlist with 1 := H'0; Auto.
Generalize H'0; Case M; Simpl; Auto.
Intros Ar War H'2; Red; Simpl; Auto.
Apply wellFormedArrayInImpLt with 2 := H'2; Auto with datatypes.
Simpl; Auto.
Rewrite eMZevalMnat; Rewrite H'; Auto.
Split; Auto.
Intros c H'0; Elim H'0; Clear H'0; Intros H'0.
Rewrite <- H'0; Auto.
Apply eMZlt' with 1 := H'; Auto.
Red; Apply inImpInEq; Auto.
Intros c Hc; Red; Split.
Intros H'0; Elim H'0; Clear H'0; Intros H'1.
Rewrite (evalMZIrr maxN M c (rZPlus a) Hc Ha); Simpl; Auto.
Rewrite eMZevalMnat; Rewrite H'; Auto.
Cut <vM> (eMZ maxN M (valRz c) Hc)=(ref (samePol c a)).
Generalize Hc; Case c; Simpl; Auto; Intros r1 Hc0; Rewrite eMZevalMnat;
Intros H'0; Rewrite H'0; Auto.
Apply eMZref with L := L Ha := Ha; Auto.
Generalize Hc H'; Case c; Case M; Simpl; Auto.
Intros Ar War r Hc0 H'1.
Generalize (refl_equal ? (getAval maxN vM Ar r Hc0));
Pattern -1 (getAval maxN vM Ar r Hc0); Case (getAval maxN vM Ar r Hc0); Auto.
Intros r0 H'0 H'2; Rewrite H'2 in H'0.
Right.
Change (In (samePol (rZPlus a) r) L); Auto.
Apply wfPcc2 with 2 := H'0 3 := H'1; Auto.
Intros Ar War r Hc0 H'1.
Generalize (refl_equal ? (getAval maxN vM Ar r Hc0));
Pattern -1 (getAval maxN vM Ar r Hc0); Case (getAval maxN vM Ar r Hc0); Auto.
Intros r0 H'0 H'2; Right.
Change (In (samePol (rZMinus a) r) L); Auto.
Apply (wfPcc2 ? Ar r (rZMinus a) Hc0 Ha); Auto.
Replace (rZMinus a) with (rZComp (rZPlus a)); Auto.
Rewrite <- H'2; Auto.
Rewrite <- rZCompInvol; Auto.
Defined.
Definition
getEquiv :=
[M:(Mem maxN)] [a:rNat] [Ha:(rlt a maxN)]
Cases (getEquivAux M a Ha) of
(exist x _) => x
end.
Theorem
getEquivProp1:
(M:(Mem maxN))
(a:rNat) (Ha:(rlt a maxN)) (c:rZ) (In c (Fst (getEquiv M a Ha))) ->
(rVlt c maxN).
Intros M a Ha c; Try Unfold getEquiv; Case (getEquivAux M a Ha); Auto.
Intros x; Case x; Auto.
Intros l b; Case b; Simpl; Intuition; Auto.
Qed.
Theorem
getEquivProp2:
(M:(Mem maxN))
(a:rNat)
(Ha:(rlt a maxN)) (c:rZ) (Hc:(rVlt c maxN)) (Snd (getEquiv M a Ha))=true ->
(iff
(In (rZComp c) (Fst (getEquiv M a Ha)))
(evalMZ maxN M c Hc)=(evalMZ maxN M (rZPlus a) Ha)).
Intros M a Ha c; Try Unfold getEquiv; Case (getEquivAux M a Ha); Auto.
Intros x; Case x; Auto.
Intros l b; Case b; Simpl; Auto.
Intros H' Hc H'0.
Elim H'; Intros H'1 H'2; Elim H'2; Intros H'3 H'4; Apply H'4; Auto.
Intros H' Hc H'0; Discriminate.
Qed.
Theorem
getEquivProp3:
(M:(Mem maxN))
(a:rNat)
(Ha:(rlt a maxN)) (c:rZ) (Hc:(rVlt c maxN)) (Snd (getEquiv M a Ha))=false ->
(iff
(In c (Fst (getEquiv M a Ha)))
(evalMZ maxN M c Hc)=(evalMZ maxN M (rZPlus a) Ha)).
Intros M a Ha c; Try Unfold getEquiv; Case (getEquivAux M a Ha); Auto.
Intros x; Case x; Auto.
Intros l b; Case b; Simpl; Auto.
Intros H' Hc H'0; Discriminate.
Intros H' Hc H'0.
Elim H'; Intros H'1 H'2; Elim H'2; Intros H'3 H'4; Apply H'4; Auto.
Qed.
Theorem
getEquivProp4:
(M:(Mem maxN)) (a:rNat) (Ha:(rlt a maxN))(OlistRz (Fst (getEquiv M a Ha))).
Intros M a Ha; Try Unfold getEquiv; Case (getEquivAux M a Ha); Auto.
Intros x; Case x; Auto.
Intros l b; Case b; Simpl; Intuition; Auto.
Qed.
Definition
getEquivList: (Mem maxN) ->(a:rZ) (rVlt a maxN) ->(list rZ) :=
[M:(Mem maxN)] [a:rZ]
<[r:rZ] (rVlt r maxN) ->(list rZ)>Cases a of
(rZPlus a') => [Ha':(rVlt (rZPlus a') maxN)]
Cases (getEquiv M a' Ha') of
(pair L true) => (map rZComp L)
| (pair L false) => L
end
| (rZMinus a') => [Ha':(rVlt (rZMinus a') maxN)]
Cases (getEquiv M a' Ha') of
(pair L true) => L
| (pair L false) => (map rZComp L)
end
end.
Theorem
inMapComp:
(a:rZ) (L:(list rZ)) (In (rZComp a) (map rZComp L)) ->(In a L).
Intros a L; Elim L; Simpl; Auto.
Intros a0 l H' H'0; Elim H'0; Clear H'0; Intros H'0; Auto.
Left; Apply rZCompEq; Auto.
Qed.
Theorem
getEquivListProp1:
(M:(Mem maxN))
(a:rZ) (Ha:(rVlt a maxN)) (c:rZ) (In c (getEquivList M a Ha)) ->(rVlt c maxN).
Intros M a; Unfold getEquivList; Case a; Intros a' Ha';
Generalize (getEquivProp1 M a' Ha'); Case (getEquiv M a' Ha'); Simpl;
Intros l b; Case b; Auto; Intros H' c H'0; Rewrite (rZCompInvol c);
Apply rVltrZComp; Apply H'; Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Qed.
Theorem
getEquivListProp2:
(M:(Mem maxN)) (a:rZ) (Ha:(rVlt a maxN)) (c:rZ) (Hc:(rVlt c maxN))
(iff (In c (getEquivList M a Ha)) (evalMZ maxN M c Hc)=(evalMZ maxN M a Ha)).
Intros M a; Unfold getEquivList; Case a; Intros a' Ha';
Generalize (getEquivProp2 M a' Ha'); Generalize (getEquivProp3 M a' Ha');
Case (getEquiv M a' Ha'); Simpl; Auto; Intros l b; Case b; Auto.
Intros H' H'0 c Hc.
LApply (H'0 c Hc); [Intros H'3; Red in H'3 | Idtac]; Auto.
Elim H'3; Intros H'1 H'2; Clear H'3.
Red; Split; Intros H'3; Auto.
Apply H'1; Auto.
Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Rewrite (rZCompInvol c); Apply in_map; Auto.
Intros H' H'0 c Hc.
LApply (H'0 (rZComp c) (rVltrZComp ? ? Hc));
[Rewrite <- rZCompInvol; Intros H'3; Red in H'3 | Idtac]; Auto.
Elim H'3; Intros H'1 H'2; Clear H'3.
Red; Split; Intros H'3; Auto.
Rewrite <- H'1; Auto.
Rewrite (evalMZComp maxN M c Hc); Auto.
Apply H'2; Auto.
Rewrite (evalMZComp maxN M c Hc); Auto.
Rewrite H'3; Auto.
Intros H' H'0 c Hc.
LApply (H' (rZComp c) (rVltrZComp ? ? Hc)); [Intros H'3; Red in H'3 | Idtac];
Auto.
Elim H'3; Intros H'1 H'2; Clear H'3.
Red; Split; Intros H'3; Auto.
Rewrite <- H'1; Auto.
Rewrite (evalMZComp maxN M c Hc); Auto.
Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Rewrite (rZCompInvol c); Apply in_map; Auto.
Apply H'2; Auto.
Rewrite (evalMZComp maxN M c Hc); Auto.
Rewrite H'3; Auto.
Qed.
Theorem
getEquivListProp3:
(M:(Mem maxN)) (a:rZ) (Ha:(rVlt a maxN))(OlistRz (getEquivList M a Ha)).
Intros M a; Unfold getEquivList; Case a; Intros a' Ha';
Generalize (getEquivProp4 M a' Ha'); Case (getEquiv M a' Ha'); Simpl; Auto;
Intros l b; Case b; Auto; Intros H'; Red; Apply Olistf with eqA := eqRz; Auto;
Exact rZltEqComp.
Qed.
Theorem
getEquivListProp4:
(M:(Mem maxN)) (a:rZ) (Ha:(rVlt a maxN))(In a (getEquivList M a Ha)).
Intros M a Ha.
Specialize 5 getEquivListProp2 with M := M a := a Ha := Ha c := a Hc := Ha;
Intros H'3; Red in H'3; Auto.
Elim H'3; Auto.
Qed.
Theorem
getEquivListProp5:
(M:(Mem maxN)) (a, b:rZ) (Ha:(rVlt a maxN)) (Hb:(rVlt b maxN))
(iff
(eqStateRz (memF maxN M) a b) (getEquivList M a Ha)=(getEquivList M b Hb)).
Intros M a b Ha Hb; Red; Split; Intros H'1; Auto.
Cut (EqL ? (eq rZ) (getEquivList M a Ha) (getEquivList M b Hb)).
Intros H'; Elim H'; Simpl; Auto.
Intros a0 b0 L1 L2 H'0 H'2 H'3; Rewrite H'0; Rewrite H'3; Auto.
Apply EqLOlist with ltA := rZlt; Try (Red; Auto; Fail); Auto.
Intros a0 b0 H'; Red; Intros H'0; Absurd (rZlt a0 b0); Auto; Rewrite H'0; Auto.
Intros a0 b0 c d H' H'0 H'2; Rewrite <- H'0; Rewrite <- H'2; Auto.
Apply getEquivListProp3; Auto.
Apply getEquivListProp3; Auto.
Apply InclEqDef; Auto.
Intros a0 H'; Apply inImpInEq; Auto.
Red; Auto.
Cut (rVlt a0 maxN); [Intros Ha0 | Idtac].
Specialize 5 getEquivListProp2 with M := M a := b Ha := Hb c := a0 Hc := Ha0;
Intros H'5; Red in H'5.
Elim H'5; Intros H'0 H'2; LApply H'2;
[Intros H'3; Apply H'3; Clear H'2 H'5 | Clear H'2 H'5]; Auto.
Apply evalCorrect; Auto.
Apply eqStateRzTrans with b := a; Auto.
Apply evalInv with Maxa := Ha0 Maxb := Ha.
Specialize 5 getEquivListProp2 with M := M a := a Ha := Ha c := a0 Hc := Ha0;
Intros H'5; Red in H'5.
Elim H'5; Intros H'2 H'3; LApply H'2;
[Intros H'4; Apply H'4; Clear H'2 H'5 | Clear H'2 H'5]; Auto.
Elim H'; Auto with datatypes.
Intros a1 b0 L H'2; Rewrite H'2; Auto with datatypes.
Apply getEquivListProp1 with M := M a := a Ha := Ha; Auto.
Elim H'; Auto with datatypes.
Intros a1 b0 L H'2; Rewrite H'2; Auto with datatypes.
Apply InclEqDef; Auto.
Intros a0 H'; Apply inImpInEq; Auto.
Red; Auto.
Cut (rVlt a0 maxN); [Intros Ha0 | Idtac].
Specialize 5 getEquivListProp2 with M := M a := a Ha := Ha c := a0 Hc := Ha0;
Intros H'5; Red in H'5.
Elim H'5; Intros H'0 H'2; LApply H'2;
[Intros H'3; Apply H'3; Clear H'2 H'5 | Clear H'2 H'5]; Auto.
Apply evalCorrect; Auto.
Apply eqStateRzTrans with b := b; Auto.
Apply evalInv with Maxa := Ha0 Maxb := Hb.
Specialize 5 getEquivListProp2 with M := M a := b Ha := Hb c := a0 Hc := Ha0;
Intros H'5; Red in H'5.
Elim H'5; Intros H'2 H'3; LApply H'2;
[Intros H'4; Apply H'4; Clear H'2 H'5 | Clear H'2 H'5]; Auto.
Elim H'; Auto with datatypes.
Intros a1 b0 L H'2; Rewrite H'2; Auto with datatypes.
Apply getEquivListProp1 with M := M a := b Ha := Hb; Auto.
Elim H'; Auto with datatypes.
Intros a1 b0 L H'2; Rewrite H'2; Auto with datatypes.
Apply evalInv with Maxa := Ha Maxb := Hb; Auto.
Specialize 5 getEquivListProp2 with M := M a := a Ha := Ha c := b Hc := Hb;
Intros H'4; Red in H'4.
Elim H'4; Intros H' H'0; Rewrite H'; Auto.
Rewrite H'1; Auto.
Apply getEquivListProp4; Auto.
Qed.
Definition
getMinId :=
(getMin
? rZlt eqRz eqrZRefl eqrZSym rZltEDec rZltTrans rZltNotRefl rZltDef2
rZltEqComp (eq rZ) [a, b:rZ] [_:?](rZDec a b)
[a, b:rZ] [H':?](eq_ind_r rZ b [r:rZ](eqRz r b) (eqrZRefl b) a H')).
Theorem
getMinIdSym:
(L1, L2:(list rZ)) (OlistRz L1) -> (OlistRz L2) ->
(getMinId L1 L2)=(getMinId L2 L1).
Intros L1 L2 H' H'0; Unfold getMinId getMin.
Case (getMinAux
? rZlt eqRz eqrZRefl eqrZSym rZltEDec rZltTrans rZltNotRefl rZltDef2
rZltEqComp (eq rZ) [a, b:rZ] [_:?](rZDec a b)
[a, b:rZ] [H':a=b](eq_ind_r rZ b [r:rZ](eqRz r b) (eqrZRefl b) a H')
(L1, L2)); Simpl.
Intros x; Case x; Clear x.
Intros a H'1;
Case (getMinAux
? rZlt eqRz eqrZRefl eqrZSym rZltEDec rZltTrans rZltNotRefl rZltDef2
rZltEqComp (eq rZ) [a, b:rZ] [_:?](rZDec a b)
[a, b:rZ] [H':a=b](eq_ind_r rZ b [r:rZ](eqRz r b) (eqrZRefl b) a H')
(L2, L1)); Simpl.
Intros x; Case x; Clear x.
Intros b H'2.
Generalize (H'2 H'0 H'); Clear H'2; Intros H'2.
Generalize (H'1 H' H'0); Clear H'1; Intros H'1.
Rewrite (OlistIn ? rZlt eqRz) with a := a b := b L := L1; Auto.
Apply MinPropIn with ltA := rZlt test := (eq rZ) L2 := L2; Auto.
Inversion H'2; Auto.
Rewrite H1; Auto.
Inversion_clear H'1; Inversion_clear H'2.
Case (rZltEDec a b); Auto; Intros s; Case s; Clear s; Intros Lt0.
Case (H6 a a); Auto.
Rewrite H1; Auto.
Case (H2 b b); Auto.
Rewrite H5; Auto.
Intros H'2.
Generalize (H'1 H' H'0); Intros min1; Inversion min1.
Case (H'2 H'0 H' b a); Auto.
Intros H'1;
Case (getMinAux
? rZlt eqRz eqrZRefl eqrZSym rZltEDec rZltTrans rZltNotRefl rZltDef2
rZltEqComp (eq rZ) [a, b:rZ] [_:?](rZDec a b)
[a, b:rZ] [H':a=b](eq_ind_r rZ b [r:rZ](eqRz r b) (eqrZRefl b) a H')
(L2, L1)); Simpl.
Intros x; Case x; Clear x; Auto.
Intros b H'2.
Generalize (H'2 H'0 H'); Intros min1; Inversion min1.
Case (H'1 H' H'0 b a); Auto.
Rewrite H1; Auto.
Rewrite H5; Auto.
Qed.
Definition
getMinInv :=
(getMin
? rZlt eqRz eqrZRefl eqrZSym rZltEDec rZltTrans rZltNotRefl rZltDef2
rZltEqComp [a, b:rZ]a=(rZComp b)
[a, b:rZ] [_:(eqRz a b)](rZDec a (rZComp b))
[a, b:rZ] [H':?]
(eq_ind_r
rZ (rZComp b) [r:rZ](eqRz r b) (eqrZSym b (rZComp b) (eqRzComp b)) a H')).
Theorem
getMinInvSym:
(L1, L2:(list rZ)) (OlistRz L1) -> (OlistRz L2) ->Cases (getMinInv L1 L2) of
None =>
(getMinInv L2 L1)=
(None ?)
| (Some a) =>
(getMinInv L2 L1)=
(Some ? (rZComp a))
end.
Intros L1 L2 H' H'0; Unfold getMinInv getMin.
Case (getMinAux
? rZlt eqRz eqrZRefl eqrZSym rZltEDec rZltTrans rZltNotRefl rZltDef2
rZltEqComp [a, b:rZ]<rZ> a=(rZComp b)
[a, b:rZ] [_:?](rZDec a (rZComp b))
[a, b:rZ] [H':a=(rZComp b)]
(eq_ind_r
rZ (rZComp b) [r:rZ](eqRz r b) (eqrZSym b (rZComp b) (eqRzComp b)) a
H') (L1, L2)); Simpl.
Intros x; Case x; Clear x.
Intros a H'1;
Case (getMinAux
? rZlt eqRz eqrZRefl eqrZSym rZltEDec rZltTrans rZltNotRefl rZltDef2
rZltEqComp [a, b:rZ]<rZ> a=(rZComp b)
[a, b:rZ] [_:?](rZDec a (rZComp b))
[a, b:rZ] [H':a=(rZComp b)]
(eq_ind_r
rZ (rZComp b) [r:rZ](eqRz r b) (eqrZSym b (rZComp b) (eqRzComp b)) a
H') (L2, L1)); Simpl.
Intros x; Case x; Clear x.
Intros b H'2.
Generalize (H'2 H'0 H'); Clear H'2; Intros H'2.
Generalize (H'1 H' H'0); Clear H'1; Intros H'1.
Rewrite (OlistIn ? rZlt eqRz) with a := a b := (rZComp b) L := L1; Auto.
Apply MinPropIn with ltA := rZlt test := [a0, b:rZ]<rZ> a0=(rZComp b) L2 := L2;
Auto.
Inversion H'2; Auto.
Rewrite H1; Auto.
Rewrite <- rZCompInvol; Auto.
Inversion_clear H'1; Inversion_clear H'2.
Case (rZltEDec a (rZComp b)); Auto; Intros s; Case s; Clear s; Intros Lt0.
Case (H6 (rZComp a) a); Auto.
Rewrite H1; Rewrite <- rZCompInvol; Auto.
Generalize Lt0; Unfold rZlt; Case a; Case b; Auto.
Case (H2 (rZComp b) b); Auto.
Rewrite H5; Rewrite <- rZCompInvol; Auto.
Intros H'2.
Generalize (H'1 H' H'0); Intros min1; Inversion min1.
Case (H'2 H'0 H' b a); Auto.
Rewrite H1; Rewrite <- rZCompInvol; Auto.
Intros H'1;
Case (getMinAux
? rZlt eqRz eqrZRefl eqrZSym rZltEDec rZltTrans rZltNotRefl rZltDef2
rZltEqComp [a, b:rZ]<rZ> a=(rZComp b)
[a, b:rZ] [_:?](rZDec a (rZComp b))
[a, b:rZ] [H':a=(rZComp b)]
(eq_ind_r
rZ (rZComp b) [r:rZ](eqRz r b) (eqrZSym b (rZComp b) (eqRzComp b)) a
H') (L2, L1)); Simpl.
Intros x; Case x; Clear x; Auto.
Intros b H'2.
Generalize (H'2 H'0 H'); Clear H'2; Intros H'2.
Generalize (H'1 H' H'0); Clear H'1; Intros H'1.
Inversion H'2.
Case (H'1 (rZComp b) a); Auto.
Rewrite H1; Rewrite <- rZCompInvol; Auto.
Rewrite H5; Auto.
Rewrite H5; Auto.
Qed.
Definition
getEquivMin: (Mem maxN) -> (Mem maxN) ->(a:rNat) (rlt a maxN) ->rZ :=
[M1, M2:(Mem maxN)] [a:rNat] [Ha:(rlt a maxN)]
Cases (getEquiv M1 a Ha) of
(pair L1 true) => Cases (getEquiv M2 a Ha) of
(pair L2 true) => Cases (getMinId L1 L2) of
(Some b) => (rZComp b)
| None => (rZPlus zero)
end
| (pair L2 false) => Cases (getMinInv L1 L2) of
(Some b) => (rZComp b)
| None => (rZPlus zero)
end
end
| (pair L1 false) => Cases (getEquiv M2 a Ha) of
(pair L2 true) => Cases (getMinInv L1 L2) of
(Some b) => b
| None => (rZPlus zero)
end
| (pair L2 false) => Cases (getMinId L1 L2) of
(Some b) => b
| None => (rZPlus zero)
end
end
end.
Theorem
getEquivMinSym:
(M1, M2:(Mem maxN)) (a:rNat) (Ha:(rlt a maxN))
(getEquivMin M1 M2 a Ha)=(getEquivMin M2 M1 a Ha).
Intros M1 M2 a Ha; Unfold getEquivMin; Generalize (getEquivProp4 M1 a Ha);
Generalize (getEquivProp4 M2 a Ha); Case (getEquiv M1 a Ha);
Case (getEquiv M2 a Ha); Simpl.
Intros L1 b1 L2 b2 OL1 OL2; Case b1; Case b2; Auto;
Try Rewrite (getMinIdSym L1 L2); Auto; Generalize (getMinInvSym L1 L2); Auto;
Case (getMinInv L1 L2); Auto; Case (getMinInv L2 L1); Auto;
Intros x1 x2 Hx1 Orelse Intros x1 Hx1; Auto; Generalize (Hx1 OL1 OL2);
Intros Inv0; Inversion Inv0; Auto.
Qed.
Theorem
getEquivMinMaxn:
(M1, M2:(Mem maxN)) (a:rNat) (Ha:(rlt a maxN))
(rVlt (getEquivMin M1 M2 a Ha) maxN).
Intros M1 M2 a Ha; Unfold getEquivMin; Generalize (getEquivProp1 M1 a Ha);
Generalize (getEquivProp4 M1 a Ha); Generalize (getEquivProp1 M2 a Ha);
Generalize (getEquivProp4 M2 a Ha); Case (getEquiv M1 a Ha);
Case (getEquiv M2 a Ha); Simpl; Auto; Intros L1 b1 L2 b2 Max1 OL1 Max2 OL2;
Case b1; Case b2; Auto.
Generalize (refl_equal ? (getMinId L2 L1)); Pattern -1 (getMinId L2 L1);
Case (getMinId L2 L1); Auto.
Intros x H'; Apply rVltrZComp; Apply OL2; Auto.
Unfold getMinId in H'; Apply getMinIn with 3 := H'; Auto.
Intros H'; Red; Rewrite HmaxN; Simpl; Auto.
Generalize (refl_equal ? (getMinInv L2 L1)); Pattern -1 (getMinInv L2 L1);
Case (getMinInv L2 L1); Auto.
Intros x H'; Apply OL2; Auto.
Unfold getMinInv in H'; Apply getMinIn with 3 := H'; Auto.
Intros H'; Red; Rewrite HmaxN; Simpl; Auto.
Generalize (refl_equal ? (getMinInv L2 L1)); Pattern -1 (getMinInv L2 L1);
Case (getMinInv L2 L1); Auto.
Intros x H'; Apply rVltrZComp; Apply OL2; Auto.
Unfold getMinInv in H'; Apply getMinIn with 3 := H'; Auto.
Intros H'; Red; Rewrite HmaxN; Simpl; Auto.
Generalize (refl_equal ? (getMinId L2 L1)); Pattern -1 (getMinId L2 L1);
Case (getMinId L2 L1); Auto.
Intros x H'; Apply OL2; Auto.
Unfold getMinId in H'; Apply getMinIn with 3 := H'; Auto.
Intros H'; Red; Rewrite HmaxN; Simpl; Auto.
Qed.
Theorem
rZCompInvolList: (L:(list rZ))L=(map rZComp (map rZComp L)).
Intros L; Elim L; Simpl; Auto.
Intros a l H'; Rewrite <- H'; Auto with datatypes.
Rewrite <- rZCompInvol; Auto.
Qed.
Theorem
getEquivMinIn1:
(M1, M2:(Mem maxN)) (a:rNat) (Ha:(rlt a maxN))
(In (getEquivMin M1 M2 a Ha) (getEquivList M1 (rZPlus a) Ha)).
Intros M1 M2 a Ha; Generalize (getEquivListProp3 M1 (rZPlus a) Ha);
Generalize (getEquivListProp4 M1 (rZPlus a) Ha);
Generalize (getEquivListProp3 M2 (rZPlus a) Ha);
Generalize (getEquivListProp4 M2 (rZPlus a) Ha); Simpl; Unfold getEquivMin;
Case (getEquiv M1 a Ha); Intros l b; Case b; Case (getEquiv M2 a Ha);
Intros l0 b0; Case b0; Auto.
(Generalize (refl_equal ? (getMinId l l0)); Pattern -1 (getMinId l l0);
Case (getMinId l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3; Apply in_map; Auto.
Unfold getMinId in H'; Apply getMinIn with 3 := H'; Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinId in H';
Case getMinNone with 3 := H' a := (rZMinus a) b := (rZMinus a); Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Auto.
Apply inMapComp; Auto.
(Generalize (refl_equal ? (getMinInv l l0)); Pattern -1 (getMinInv l l0);
Case (getMinInv l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3; Apply in_map; Auto.
Unfold getMinInv in H'; Apply getMinIn with 3 := H'; Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinInv in H';
Case getMinNone with 3 := H' a := (rZMinus a) b := (rZPlus a); Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Auto.
(Generalize (refl_equal ? (getMinInv l l0)); Pattern -1 (getMinInv l l0);
Case (getMinInv l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3.
Unfold getMinInv in H'; Apply getMinIn with 3 := H'; Auto.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinInv in H';
Case getMinNone with 3 := H' a := (rZPlus a) b := (rZMinus a); Auto.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Auto.
(Generalize (refl_equal ? (getMinId l l0)); Pattern -1 (getMinId l l0);
Case (getMinId l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3.
Unfold getMinId in H'; Apply getMinIn with 3 := H'; Auto.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinId in H';
Case getMinNone with 3 := H' a := (rZPlus a) b := (rZPlus a); Auto.
Qed.
Theorem
getEquivMinIn2:
(M1, M2:(Mem maxN)) (a:rNat) (Ha:(rlt a maxN))
(In (getEquivMin M1 M2 a Ha) (getEquivList M2 (rZPlus a) Ha)).
Intros M1 M2 a Ha; Generalize (getEquivListProp3 M1 (rZPlus a) Ha);
Generalize (getEquivListProp4 M1 (rZPlus a) Ha);
Generalize (getEquivListProp3 M2 (rZPlus a) Ha);
Generalize (getEquivListProp4 M2 (rZPlus a) Ha); Simpl; Unfold getEquivMin;
Case (getEquiv M1 a Ha); Intros l b; Case b; Case (getEquiv M2 a Ha);
Intros l0 b0; Case b0; Auto.
(Generalize (refl_equal ? (getMinId l l0)); Pattern -1 (getMinId l l0);
Case (getMinId l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3; Apply in_map; Auto.
Unfold getMinId in H'; Elim getMinComp with 3 := H'; Auto.
Intros x0 H'4; Elim H'4; Intros H'5 H'6; Rewrite H'5; Clear H'4; Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinId in H';
Case getMinNone with 3 := H' a := (rZMinus a) b := (rZMinus a); Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Auto.
Apply inMapComp; Auto.
(Generalize (refl_equal ? (getMinInv l l0)); Pattern -1 (getMinInv l l0);
Case (getMinInv l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3; Apply inMapComp; Auto.
Unfold getMinInv in H'; Elim getMinComp with 3 := H'; Auto.
Intros x0 H'4; Elim H'4; Intros H'5 H'6; Rewrite H'5; Clear H'4;
Rewrite <- rZCompInvol; Apply in_map; Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinInv in H';
Case getMinNone with 3 := H' a := (rZMinus a) b := (rZPlus a); Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Auto.
(Generalize (refl_equal ? (getMinInv l l0)); Pattern -1 (getMinInv l l0);
Case (getMinInv l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3.
Unfold getMinInv in H'; Elim getMinComp with 3 := H'; Auto.
Intros x0 H'4; Elim H'4; Intros H'5 H'6; Rewrite H'5; Clear H'4; Apply in_map;
Auto.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinInv in H';
Case getMinNone with 3 := H' a := (rZPlus a) b := (rZMinus a); Auto.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Auto.
(Generalize (refl_equal ? (getMinId l l0)); Pattern -1 (getMinId l l0);
Case (getMinId l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3.
Unfold getMinId in H'; Elim getMinComp with 3 := H'; Auto.
Intros x0 H'4; Elim H'4; Intros H'5 H'6; Rewrite H'5; Clear H'4; Auto.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinId in H';
Case getMinNone with 3 := H' a := (rZPlus a) b := (rZPlus a); Auto.
Qed.
Theorem
getEquivMinMin:
(M1, M2:(Mem maxN))
(a:rNat) (Ha:(rlt a maxN)) (c:rZ) (rZlt c (getEquivMin M1 M2 a Ha)) ->
~ ((In c (getEquivList M1 (rZPlus a) Ha)) /\
(In c (getEquivList M2 (rZPlus a) Ha))).
Intros M1 M2 a Ha; Generalize (getEquivListProp3 M1 (rZPlus a) Ha);
Generalize (getEquivListProp4 M1 (rZPlus a) Ha);
Generalize (getEquivListProp3 M2 (rZPlus a) Ha);
Generalize (getEquivListProp4 M2 (rZPlus a) Ha); Simpl; Unfold getEquivMin;
Case (getEquiv M1 a Ha); Intros l b; Case b; Case (getEquiv M2 a Ha);
Intros l0 b0; Case b0; Auto.
(Generalize (refl_equal ? (getMinId l l0)); Pattern -1 (getMinId l l0);
Case (getMinId l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3 c H'4; Red; Intros H'5; Elim H'5; Intros H'6 H'7;
Clear H'5.
Absurd (rZComp c)=(rZComp c); Auto.
Unfold getMinId in H'; Apply getMinMin with 3 := H'; Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply rZltEqComp with a := c b := (rZComp x); Auto.
Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinId in H';
Case getMinNone with 3 := H' a := (rZMinus a) b := (rZMinus a); Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Auto.
Apply inMapComp; Auto.
(Generalize (refl_equal ? (getMinInv l l0)); Pattern -1 (getMinInv l l0);
Case (getMinInv l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3 c H'4; Red; Intros H'5; Elim H'5; Intros H'6 H'7;
Clear H'5; Auto.
Absurd (rZComp c)=(rZComp c); Auto.
Unfold getMinInv in H'; Apply getMinMin with 3 := H'; Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply rZltEqComp with a := c b := (rZComp x); Auto.
Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinInv in H';
Case getMinNone with 3 := H' a := (rZMinus a) b := (rZPlus a); Auto.
Rewrite (rZCompInvolList l); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Auto.
(Generalize (refl_equal ? (getMinInv l l0)); Pattern -1 (getMinInv l l0);
Case (getMinInv l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3 c H'4; Red; Intros H'5; Elim H'5; Intros H'6 H'7;
Clear H'5.
Absurd c=(rZComp (rZComp c)); Auto.
Unfold getMinInv in H'; Apply getMinMin with 3 := H'; Auto.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinInv in H';
Case getMinNone with 3 := H' a := (rZPlus a) b := (rZMinus a); Auto.
Rewrite (rZCompInvolList l0); Auto.
Apply Olistf with eqA := eqRz; Auto.
Try Exact rZltEqComp.
Apply inMapComp; Auto.
(Generalize (refl_equal ? (getMinId l l0)); Pattern -1 (getMinId l l0);
Case (getMinId l l0)); Auto.
Intros x H' H'0 H'1 H'2 H'3 c H'4; Red; Intros H'5; Elim H'5; Intros H'6 H'7;
Clear H'5.
Absurd c=c; Auto.
Unfold getMinId in H'; Apply getMinMin with 3 := H'; Auto.
Intros H' H'0 H'1 H'2 H'3.
Unfold getMinId in H';
Case getMinNone with 3 := H' a := (rZPlus a) b := (rZPlus a); Auto.
Qed.
Theorem
getEquivMinEq1:
(M1, M2:(Mem maxN)) (a:rNat) (Ha:(rlt a maxN))
(eqStateRz (memF maxN M1) (rZPlus a) (getEquivMin M1 M2 a Ha)).
Intros M1 M2 a Ha.
Cut (rVlt (getEquivMin M1 M2 a Ha) maxN); [Intros Hc | Idtac].
Cut (rVlt (rZPlus a) maxN); [Intros Ha' | Idtac]; Auto.
Apply evalInv with Maxa := Ha' Maxb := Hc.
Rewrite (evalMZIrr maxN M1 (rZPlus a) (rZPlus a) Ha' Ha); Auto.
Specialize 5 getEquivListProp2
with M := M1 a := (rZPlus a) Ha := Ha c := (getEquivMin M1 M2 a Ha)
Hc := Hc; Intros H'6; Red in H'6.
Elim H'6; Intros H' H'0; Rewrite <- H'; Auto.
Apply getEquivMinIn1.
Apply getEquivMinMaxn; Auto.
Qed.
Theorem
getEquivMinEq2:
(M1, M2:(Mem maxN)) (a:rNat) (Ha:(rlt a maxN))
(eqStateRz (memF maxN M2) (rZPlus a) (getEquivMin M1 M2 a Ha)).
Intros M1 M2 a Ha.
Cut (rVlt (getEquivMin M1 M2 a Ha) maxN); [Intros Hc | Idtac].
Cut (rVlt (rZPlus a) maxN); [Intros Ha' | Idtac]; Auto.
Apply evalInv with Maxa := Ha' Maxb := Hc.
Rewrite (evalMZIrr maxN M2 (rZPlus a) (rZPlus a) Ha' Ha); Auto.
Specialize 5 getEquivListProp2
with M := M2 a := (rZPlus a) Ha := Ha c := (getEquivMin M1 M2 a Ha)
Hc := Hc; Intros H'6; Red in H'6.
Elim H'6; Intros H' H'0; Rewrite <- H'; Auto.
Apply getEquivMinIn2.
Apply getEquivMinMaxn; Auto.
Qed.
Theorem
getEquivMinMinEq:
(M1, M2:(Mem maxN))
(a:rNat) (Ha:(rlt a maxN)) (c:rZ) (rZlt c (getEquivMin M1 M2 a Ha)) ->
~ ((eqStateRz (memF maxN M1) (rZPlus a) c) /\
(eqStateRz (memF maxN M2) (rZPlus a) c)).
Intros M1 M2 a Ha c H'; Red; Intros H'0; Elim H'0; Intros H'1 H'2; Clear H'0;
Auto.
Absurd (In c (getEquivList M1 (rZPlus a) Ha)) /\
(In c (getEquivList M2 (rZPlus a) Ha)); Auto.
Apply getEquivMinMin; Auto.
Cut (rVlt c maxN); [Intros Hc | Idtac].
Split; Auto.
Specialize 5 getEquivListProp2
with M := M1 a := (rZPlus a) Ha := Ha c := c Hc := Hc; Intros H'6;
Red in H'6.
Elim H'6; Intros H'0 H'3; LApply H'3;
[Intros H'4; Apply H'4; Clear H'3 H'6 | Clear H'3 H'6]; Auto.
Apply evalCorrect; Auto.
Specialize 5 getEquivListProp2
with M := M2 a := (rZPlus a) Ha := Ha c := c Hc := Hc; Intros H'6;
Red in H'6.
Elim H'6; Intros H'0 H'3; LApply H'3;
[Intros H'4; Apply H'4; Clear H'3 H'6 | Clear H'3 H'6]; Auto.
Apply evalCorrect; Auto.
Red; Apply rltTrans with y := (valRz (getEquivMin M1 M2 a Ha)); Auto.
Change (rVlt (getEquivMin M1 M2 a Ha) maxN); Auto.
Apply getEquivMinMaxn.
Qed.
Theorem
eqNotltRz: (a, b:rZ) (rZlt a b) ->~ a=b.
Intros a b H'; Red; Intros H'0; Absurd (rZlt a b); Auto.
Rewrite H'0; Auto.
Qed.
Hints Resolve eqNotltRz.
Theorem
evalMZMin:
(M:(Mem maxN))
(a:rZ) (Ha:(rVlt a maxN)) (c:rZ) (rZlt c (evalMZ maxN M a Ha)) ->
~ (eqStateRz (memF maxN M) a c).
Intros M a Ha c H'; Red; Intros H'0.
Cut (rVlt c maxN); [Intros Hc | Idtac].
Absurd (evalMZ maxN M c Hc)=(evalMZ maxN M a Ha); Auto.
2:Apply evalCorrect; Auto.
2:Red; Apply rltTrans with y := (valRz (evalMZ maxN M a Ha)); Auto.
2:Change (rVlt (evalMZ maxN M a Ha) maxN); Auto.
2:Apply evalMZlt; Auto.
Generalize Hc Ha H'.
Case M; Intros Ar War; Auto.
Case c; Case a; Simpl; Intros a' c' Hc' 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');
Generalize (refl_equal ? (getAval maxN vM Ar c' Hc'));
Pattern -1 (getAval maxN vM Ar c' Hc'); Case (getAval maxN vM Ar c' Hc'); Auto;
Intros r H'1 r0 H'2 H'3; Red; Intros H'4;
(Absurd (rVlt r c'); [Idtac | Apply wfPd with n := maxN Ar := Ar Hr := Hc']);
Auto; Try (Rewrite H'4; Unfold rVlt; Apply rltAntiSym; Auto);
Rewrite (rZCompInvol r); Rewrite H'4; Unfold rVlt; Apply rltAntiSym;
Generalize H'3; Case r0; Simpl; Auto.
Qed.
Theorem
getEquivIdR:
(M1, M2:(Mem maxN))
(a:rNat)
(Ha:(rlt a maxN))
(eqStateRz (memF maxN M2) (rZPlus a) (evalMZ maxN M1 (rZPlus a) Ha)) ->
(getEquivMin M1 M2 a Ha)=(evalMZ maxN M1 (rZPlus a) Ha).
Intros M1 M2 a Ha H';
Case (rZltEDec (getEquivMin M1 M2 a Ha) (evalMZ maxN M1 (rZPlus a) Ha));
Intros s; [Case s; Clear s; Intros s | Idtac].
Case evalMZMin with 1 := s; Auto.
Apply getEquivMinEq1; Auto.
Case getEquivMinMinEq with 1 := s; Split; Auto.
Apply evalEq; Auto.
Case (eqRzElim ? ? s); Auto.
Intros H'0; Absurd (contradictory (memF maxN M1)); Auto.
Apply memFNotContradictory; Auto.
Red; Auto.
Exists (rZPlus a); Auto.
Apply eqStateRzTrans with b := (evalMZ maxN M1 (rZPlus a) Ha); Auto.
Apply evalEq; Auto.
Apply eqStateInvInv; Auto.
Rewrite <- H'0; Auto.
Rewrite <- rZCompInvol; Auto.
Apply eqStateRzSym.
Apply getEquivMinEq1; Auto.
Qed.
Theorem
getEquivIdL:
(M1, M2:(Mem maxN))
(a:rNat)
(Ha:(rlt a maxN))
(eqStateRz (memF maxN M1) (rZPlus a) (evalMZ maxN M2 (rZPlus a) Ha)) ->
(getEquivMin M1 M2 a Ha)=(evalMZ maxN M2 (rZPlus a) Ha).
Intros M1 M2 a Ha H'.
Rewrite getEquivMinSym; Auto.
Apply getEquivIdR; Auto.
Qed.
Theorem
getMinInvInd:
(L1, L2:(list rZ)) (OlistRz L1) -> (OlistRz L2) ->
(getMinInv L1 (map rZComp L2))=(getMinId L1 L2).
Intros L1 L2 Ol1 Ol2; Auto.
Cut (OlistRz (map rZComp L2));
[Intros Ol2' | Red; Apply Olistf with eqA := eqRz; Auto; Exact rZltEqComp].
Generalize (refl_equal ? (getMinInv L1 (map rZComp L2)));
Pattern -1 (getMinInv L1 (map rZComp L2)); Case (getMinInv L1 (map rZComp L2));
Auto.
Generalize (refl_equal ? (getMinId L1 L2)); Pattern -1 (getMinId L1 L2);
Case (getMinId L1 L2); Auto.
Intros x H' x0 H'0.
Case (rZltEDec x0 x); Intros s; [Case s; Clear s; Intros s | Idtac].
Absurd x0=x0; Auto.
Unfold getMinId in H'; Apply getMinMin with 3 := H'; Auto.
Unfold getMinInv in H'0; Apply getMinIn with 3 := H'0; Auto.
Unfold getMinInv in H'0; Elim getMinComp with 3 := H'0; Auto.
Intros x1 H'1; Elim H'1; Intros H'2 H'3; Rewrite H'2; Clear H'1.
Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Absurd x=(rZComp (rZComp x)); Auto.
Unfold getMinInv in H'0; Apply getMinMin with 3 := H'0; Auto.
Unfold getMinId in H'; Apply getMinIn with 3 := H'; Auto.
Apply in_map; Auto.
Unfold getMinId in H'; Elim getMinComp with 3 := H'; Auto.
Intros x1 H'1; Elim H'1; Intros H'2 H'3; Rewrite H'2; Clear H'1; Auto.
Rewrite (OlistIn ? rZlt eqRz) with a := x0 b := x L := L1; Auto.
Unfold getMinInv in H'0; Apply getMinIn with 3 := H'0; Auto.
Unfold getMinId in H'; Apply getMinIn with 3 := H'; Auto.
Intros H' x H'0; Absurd x=x; Auto.
Unfold getMinId in H'; Apply getMinNone with 3 := H'; Auto.
Unfold getMinInv in H'0; Apply getMinIn with 3 := H'0; Auto.
Apply inMapComp; Auto.
Unfold getMinInv in H'0; Elim getMinComp with 3 := H'0; Auto.
Intros x0 H'1; Elim H'1; Intros H'2 H'3; Rewrite H'2; Clear H'1;
Rewrite <- rZCompInvol; Auto.
Generalize (refl_equal ? (getMinId L1 L2)); Pattern -1 (getMinId L1 L2);
Case (getMinId L1 L2); Auto.
Intros x H' H'0.
Absurd x=(rZComp (rZComp x)); Auto.
Unfold getMinInv in H'0; Apply getMinNone with 3 := H'0; Auto.
Unfold getMinId in H'; Apply getMinIn with 3 := H'; Auto.
Apply in_map; Auto.
Unfold getMinId in H'; Elim getMinComp with 3 := H'; Auto.
Intros x0 H'1; Elim H'1; Intros H'2 H'3; Rewrite H'2; Clear H'1; Auto.
Qed.
Definition
getRzMin: (Mem maxN) -> (Mem maxN) ->(a:rZ) (rVlt a maxN) ->rZ :=
[M1, M2:(Mem maxN)] [a:rZ]
<[r:rZ] (rVlt r maxN) ->rZ>Cases a of
(rZPlus a') => [Ha':(rVlt (rZPlus a') maxN)](getEquivMin M1 M2 a' Ha')
| (rZMinus a') =>
[Ha':(rVlt (rZMinus a') maxN)](rZComp (getEquivMin M1 M2 a' Ha'))
end.
Theorem
getRzMinSym:
(M1, M2:(Mem maxN)) (a:rZ) (Ha:(rVlt a maxN))
(getRzMin M1 M2 a Ha)=(getRzMin M2 M1 a Ha).
Intros M1 M2 a; Case a; Simpl; Intros a' Ha'; Rewrite getEquivMinSym; Auto.
Qed.
Theorem
getRzMinMaxn:
(M1, M2:(Mem maxN)) (a:rZ) (Ha:(rVlt a maxN))(rVlt (getRzMin M1 M2 a Ha) maxN).
Intros M1 M2 a; Case a; Simpl; Intros a' Ha'; Try Apply rVltrZComp;
Apply getEquivMinMaxn; Auto.
Qed.
Theorem
getRzMinIn1:
(M1, M2:(Mem maxN)) (a:rZ) (Ha:(rVlt a maxN))
(In (getRzMin M1 M2 a Ha) (getEquivList M1 a Ha)).
Intros M1 M2 a; Case a; Intros a' Ha'; Generalize (getEquivMinIn1 M1 M2 a' Ha');
Simpl; Auto.
Case (getEquiv M1 a' Ha'); Auto.
Intros l b; Case b; Intros H'; Auto.
Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Apply in_map; Auto.
Qed.
Theorem
getRzMinIn2:
(M1, M2:(Mem maxN)) (a:rZ) (Ha:(rVlt a maxN))
(In (getRzMin M1 M2 a Ha) (getEquivList M2 a Ha)).
Intros M1 M2 a; Case a; Intros a' Ha'; Generalize (getEquivMinIn2 M1 M2 a' Ha');
Simpl; Auto.
Case (getEquiv M2 a' Ha'); Auto.
Intros l b; Case b; Intros H'; Auto.
Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Apply in_map; Auto.
Qed.
Theorem
getRzMinMin:
(M1, M2:(Mem maxN))
(a:rZ) (Ha:(rVlt a maxN)) (c:rZ) (rZlt c (getRzMin M1 M2 a Ha)) ->
~ ((In c (getEquivList M1 a Ha)) /\ (In c (getEquivList M2 a Ha))).
Intros M1 M2 a; Case a; Intros a' Ha'; Generalize (getEquivMinMin M1 M2 a' Ha');
Simpl; Auto.
Case (getEquiv M1 a' Ha'); Case (getEquiv M2 a' Ha'); Intros l b l0 b0; Case b;
Case b0; Simpl; Intros H' c H'0; Red; Intros H'1; Elim H'1; Clear H'1;
Intros H'2 H'3;
(Case (H' (rZComp c)); [Apply rZltEqComp with 1 := H'0; Auto | Idtac]); Split;
Try Apply in_map; Auto; Apply inMapComp; Rewrite <- rZCompInvol; Auto.
Qed.
Theorem
getRzMinEq1:
(M1, M2:(Mem maxN)) (a:rZ) (Ha:(rVlt a maxN))
(eqStateRz (memF maxN M1) a (getRzMin M1 M2 a Ha)).
Intros M1 M2 a; Case a; Intros a' Ha'; Generalize (getEquivMinEq1 M1 M2 a' Ha');
Simpl; Auto.
Intros H'; Apply eqStateRzInv with 1 := H'; Auto.
Qed.
Theorem
getRzMinEq2:
(M1, M2:(Mem maxN)) (a:rZ) (Ha:(rVlt a maxN))
(eqStateRz (memF maxN M2) a (getRzMin M1 M2 a Ha)).
Intros M1 M2 a; Case a; Intros a' Ha'; Generalize (getEquivMinEq2 M1 M2 a' Ha');
Simpl; Auto.
Intros H'; Apply eqStateRzInv with 1 := H'; Auto.
Qed.
Theorem
getRzMinMinEq:
(M1, M2:(Mem maxN))
(a:rZ) (Ha:(rVlt a maxN)) (c:rZ) (rZlt c (getRzMin M1 M2 a Ha)) ->
~ ((eqStateRz (memF maxN M1) a c) /\ (eqStateRz (memF maxN M2) a c)).
Intros M1 M2 a; Case a; Intros a' Ha';
Generalize (getEquivMinMinEq M1 M2 a' Ha'); Simpl; Auto.
Intros H' c H'0; Red; Intros H'1; Elim H'1; Intros H'2 H'3; Clear H'1.
(Case (H' (rZComp c)); [Apply rZltEqComp with 1 := H'0; Auto | Idtac]); Split;
Auto; Try Apply eqStateRzInv with 1 := H'2; Apply eqStateRzInv with 1 := H'3;
Auto.
Qed.
Theorem
getRzMinUnique:
(M1, M2:(Mem maxN))
(a, b:rZ)
(Ha:(rVlt a maxN))
(Hb:(rVlt b maxN))
(eqStateRz (memF maxN M1) a b) -> (eqStateRz (memF maxN M2) a b) ->
(getRzMin M1 M2 a Ha)=(getRzMin M1 M2 b Hb).
Intros M1 M2 a b Ha Hb H' H'0.
Cut (getEquivList M1 a Ha)=(getEquivList M1 b Hb);
[Intros Eq1 |
Specialize 5 getEquivListProp5 with M := M1 a := a b := b Ha := Ha Hb := Hb;
Intros H'5; Red in H'5; Elim H'5]; Auto.
Cut (getEquivList M2 a Ha)=(getEquivList M2 b Hb);
[Intros Eq2 |
Specialize 5 getEquivListProp5 with M := M2 a := a b := b Ha := Ha Hb := Hb;
Intros H'5; Red in H'5; Elim H'5]; Auto.
Case (rZltEDec (getRzMin M1 M2 a Ha) (getRzMin M1 M2 b Hb)); Intros s;
[Case s; Clear s; Intros s | Idtac].
Case getRzMinMinEq with 1 := s; Auto; Split; Auto.
Apply eqStateRzTrans with b := a; Auto.
Apply getRzMinEq1; Auto.
Cut (rVlt (getRzMin M1 M2 a Ha) maxN); [Intros Hi | Apply getRzMinMaxn]; Auto.
Apply evalInv with Maxa := Hb Maxb := Hi.
Apply sym_equal; Auto.
Specialize 5 getEquivListProp2
with M := M2 a := b Ha := Hb c := (getRzMin M1 M2 a Ha) Hc := Hi;
Intros H'5; Red in H'5.
Elim H'5; Intros H'1 H'2; Apply H'1; Clear H'5; Auto.
Rewrite <- Eq2; Auto.
Apply getRzMinIn2; Auto.
Case getRzMinMinEq with 1 := s; Auto; Split; Auto.
Apply eqStateRzTrans with b := b; Auto.
Apply getRzMinEq1; Auto.
Cut (rVlt (getRzMin M1 M2 b Hb) maxN); [Intros Hi | Apply getRzMinMaxn]; Auto.
Apply evalInv with Maxa := Ha Maxb := Hi.
Apply sym_equal; Auto.
Specialize 5 getEquivListProp2
with M := M2 a := a Ha := Ha c := (getRzMin M1 M2 b Hb) Hc := Hi;
Intros H'5; Red in H'5.
Elim H'5; Intros H'1 H'2; Apply H'1; Clear H'5; Auto.
Rewrite Eq2; Auto.
Apply getRzMinIn2; Auto.
Apply OlistIn with ltA := rZlt eqA := eqRz L := (getEquivList M1 a Ha); Auto.
Apply getRzMinIn1; Auto.
Rewrite Eq1; Auto.
Apply getRzMinIn1; Auto.
Apply getEquivListProp3; Auto.
Qed.
Theorem
forallgetEquivgetRzMin:
(M1, M2:(Mem maxN))
(S:State)
((a:rNat) (Ha:(rlt a maxN))(eqStateRz S (rZPlus a) (getEquivMin M1 M2 a Ha))) ->
(a:rZ) (Ha:(rVlt a maxN))(eqStateRz S a (getRzMin M1 M2 a Ha)).
Intros M1 M2 S H' a; Case a; Intros a' Ha'; Simpl; Auto.
Apply eqStateRzInv with 1 := (H' a' Ha'); Auto.
Qed.
Theorem
getEquivInter:
(M1, M2:(Mem maxN))
(S:State)
((a:rNat) (Ha:(rlt a maxN))(eqStateRz S (rZPlus a) (getEquivMin M1 M2 a Ha))) ->
(inclState (interState (memF maxN M1) (memF maxN M2)) S).
Intros M1 M2 S H'.
Red; Auto.
Intros i j H'0.
Cut (eqStateRz (memF maxN M1) i j);
[Intros Em1 | Apply eqStateIncl with 2 := H'0]; Auto.
Cut (eqStateRz (memF maxN M2) i j);
[Intros Em2 | Apply eqStateIncl with 2 := H'0]; Auto.
Case (rZDec i j); Intros Eqij; Auto.
Rewrite Eqij; Auto.
Cut (rVlt i maxN); [Intros Hi | Elim (evalCorrectAux maxN i j M1)]; Auto.
Cut (rVlt j maxN);
[Intros Hj | Elim (evalCorrectAux maxN i j M1); Auto; Intros Hi Hk; Elim Hk];
Auto.
Apply eqStateRzTrans with b := (getRzMin M1 M2 i Hi).
Apply forallgetEquivgetRzMin; Auto.
Rewrite (getRzMinUnique M1 M2 i j Hi Hj); Auto.
Apply eqStateRzSym; Auto.
Apply forallgetEquivgetRzMin; Auto.
Qed.
End inter.
05/07/100, 11:37