DoTripletAnd.v
Require Export DoTripletAux.
Require Export Option.
Section sect.
Variable n:rNat.
Variable a:(memory n).
Variable f:rNat ->bool.
Variable rMa:(realizeMemory n f a).
Variables p, q, r:rZ.
Hypothesis Hp:(rZLe p n).
Hypothesis Hq:(rZLe q n).
Hypothesis Hr:(rZLe r n).
Local tContraddEqDoubleIsEqual := (tContraddEqDoubleIsEqual n a f rMa).
Local tContrAddEq := (tContrAddEq n a f rMa).
Local tSometrAddEq := (tSometrAddEq n a f rMa).
Local tSometrAddEqbis := (tSometrAddEqbis n a f).
Local someaddEqDouble := (someaddEqDouble n a f rMa).
Mutual Inductive
doTripletAndP: (tMemory n) ->Prop :=
doTripletAndPpmq:
(mEval n a p Hp)=(rZComp (mEval n a q Hq)) ->
(doTripletAndP
(addEqDouble n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)))
| doTripletAndPpmr:
(mEval n a p Hp)=(rZComp (mEval n a r Hr)) ->
(doTripletAndP
(addEqDouble n a q rZFalse r rZTrue Hq (rZLeFalse n) Hr (rZLeTrue n)))
| doTripletAndPqr:
(mEval n a q Hq)=(mEval n a r Hr) ->
(doTripletAndP (addEq n a p r Hp Hr))
| doTripletAndPqrm:
(mEval n a q Hq)=(rZComp (mEval n a r Hr)) ->
(doTripletAndP (addEq n a p rZFalse Hp (rZLeFalse n)))
| doTripletAndPpT:
(mEval n a p Hp)=rZTrue ->
(doTripletAndP
(addEqDouble n a q rZTrue r rZTrue Hq (rZLeTrue n) Hr (rZLeTrue n)))
| doTripletAndPqT:
(mEval n a q Hq)=rZTrue ->(doTripletAndP (addEq n a p r Hp Hr))
| doTripletAndPqF:
(mEval n a q Hq)=rZFalse ->
(doTripletAndP (addEq n a p rZFalse Hp (rZLeFalse n)))
| doTripletAndPrT:
(mEval n a r Hr)=rZTrue ->(doTripletAndP (addEq n a p q Hp Hq))
| doTripletAndPrF:
(mEval n a r Hr)=rZFalse ->
(doTripletAndP (addEq n a p rZFalse Hp (rZLeFalse n))) .
Hints Resolve
doTripletAndPpmq doTripletAndPpmr doTripletAndPqr doTripletAndPqrm
doTripletAndPpT doTripletAndPqT doTripletAndPqF doTripletAndPrT doTripletAndPrF
doTripletAndPrF.
Theorem
tContrRealizeMemoryAnd:
(doTripletAndP (tContr n)) ->(evalTriplet f (Triplet rAnd p q r))=false.
Intros H'; Simpl; Inversion H'.
Rewrite (realizeMemoryinv2 n f a p q Hp Hq); Auto.
Generalize (tContraddEqDoubleIsEqual
q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n) H).
Case (fEval f q); Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a p r Hp Hr); Auto.
Generalize (tContraddEqDoubleIsEqual
q rZFalse r rZTrue Hq (rZLeFalse n) Hr (rZLeTrue n) H).
Case (fEval f q); Case (fEval f r); Simpl; Auto.
Rewrite (tContrAddEq p r Hp Hr); Auto.
Rewrite (realizeMemoryinv1 n f a q r Hq Hr); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a q r Hq Hr); Auto.
Rewrite (tContrAddEq p rZFalse Hp (rZLeFalse n)); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a p Hp); Auto.
Generalize (tContraddEqDoubleIsEqual
q rZTrue r rZTrue Hq (rZLeTrue n) Hr (rZLeTrue n) H).
Case (fEval f r); Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a q Hq); Auto.
Rewrite (tContrAddEq p r Hp Hr); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvFalse n f a q Hq); Auto.
Rewrite (tContrAddEq p rZFalse Hp (rZLeFalse n)); Auto.
Rewrite (realizeMemoryinvTrue n f a r Hr); Auto.
Rewrite (tContrAddEq p q Hp Hq); Simpl; Auto.
Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinvFalse n f a r Hr); Auto.
Rewrite (tContrAddEq p rZFalse Hp (rZLeFalse n)); Auto.
Case (fEval f q); Simpl; Auto.
Qed.
Theorem
tSomeRealizeMemoryAndEval:
(b:(memory n)) (realizeMemory n f b) -> (doTripletAndP (tSome n b)) ->
(evalTriplet f (Triplet rAnd p q r))=true.
Intros b rMb doT; Inversion rMb; Inversion doT; Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a p q Hp Hq); Auto.
Rewrite (H r rZFalse Hr (rZLeFalse n)); Auto; Simpl; Auto.
Rewrite (H q rZTrue Hq (rZLeTrue n)); Auto; Simpl; Auto.
Apply addEqDoubleIsEqual1
with n := n a := a k := r l := rZFalse Hi := Hq Hj := (rZLeTrue n) Hk := Hr
Hl := (rZLeFalse n); Auto.
Apply addEqDoubleIsEqual2
with n := n a := a i := q j := rZTrue Hi := Hq Hj := (rZLeTrue n) Hk := Hr
Hl := (rZLeFalse n); Auto.
Rewrite (realizeMemoryinv2 n f a p r Hp Hr); Auto.
Rewrite (H q rZFalse Hq (rZLeFalse n)); Auto; Simpl; Auto.
Rewrite (H r rZTrue Hr (rZLeTrue n)); Auto; Simpl; Auto.
Apply addEqDoubleIsEqual2
with n := n a := a i := q j := rZFalse Hi := Hq Hj := (rZLeFalse n)
Hk := Hr Hl := (rZLeTrue n); Auto.
Apply addEqDoubleIsEqual1
with n := n a := a k := r l := rZTrue Hi := Hq Hj := (rZLeFalse n) Hk := Hr
Hl := (rZLeTrue n); Auto.
Rewrite (realizeMemoryinv1 n f a q r Hq Hr); Auto.
Rewrite (H p r Hp Hr); Auto.
Case (fEval f r); Simpl; Auto.
Apply addEqSome with m1 := a; Auto.
Rewrite (realizeMemoryinv2 n f a q r Hq Hr); Auto.
Rewrite (H p rZFalse Hp (rZLeFalse n)); Auto.
Case (fEval f r); Simpl; Auto.
Apply addEqSome with m1 := a; Auto.
Rewrite (realizeMemoryinvTrue n f a p Hp); Auto.
Rewrite (H q rZTrue Hq (rZLeTrue n)); Auto; Simpl; Auto.
Rewrite (H r rZTrue Hr (rZLeTrue n)); Auto; Simpl; Auto.
Apply addEqDoubleIsEqual2
with n := n a := a i := q j := rZTrue Hi := Hq Hj := (rZLeTrue n) Hk := Hr
Hl := (rZLeTrue n); Auto.
Apply addEqDoubleIsEqual1
with n := n a := a k := r l := rZTrue Hi := Hq Hj := (rZLeTrue n) Hk := Hr
Hl := (rZLeTrue n); Auto.
Rewrite (realizeMemoryinvTrue n f a q Hq); Auto.
Rewrite (H p r Hp Hr); Auto.
Case (fEval f r); Simpl; Auto.
Apply addEqSome with m1 := a; Auto.
Rewrite (realizeMemoryinvFalse n f a q Hq); Auto.
Rewrite (H p rZFalse Hp (rZLeFalse n)); Auto; Simpl; Auto.
Apply addEqSome with m1 := a; Auto.
Rewrite (realizeMemoryinvTrue n f a r Hr); Auto.
Rewrite (H p q Hp Hq); Auto.
Case (fEval f q); Simpl; Auto.
Apply addEqSome with m1 := a; Auto.
Rewrite (realizeMemoryinvFalse n f a r Hr); Auto.
Rewrite (H p rZFalse Hp (rZLeFalse n)); Auto.
Case (fEval f q); Simpl; Auto.
Apply addEqSome with m1 := a; Auto.
Qed.
Theorem
tNopRealizeMemoryAndEval:
(doTripletAndP (tNop n)) ->(evalTriplet f (Triplet rAnd p q r))=true.
Intros doT; Inversion rMa; Inversion doT; Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a p q Hp Hq); Auto.
Rewrite (H r rZFalse Hr (rZLeFalse n)); Auto; Simpl; Auto.
Rewrite (H q rZTrue Hq (rZLeTrue n)); Auto; Simpl; Auto.
Apply addEqDoubleNopIsEqual1
with n := n a := a k := r l := rZFalse Hi := Hq Hj := (rZLeTrue n) Hk := Hr
Hl := (rZLeFalse n); Auto.
Apply addEqDoubleNopIsEqual2
with n := n a := a i := q j := rZTrue Hi := Hq Hj := (rZLeTrue n) Hk := Hr
Hl := (rZLeFalse n); Auto.
Rewrite (realizeMemoryinv2 n f a p r Hp Hr); Auto.
Rewrite (H q rZFalse Hq (rZLeFalse n)); Auto; Simpl; Auto.
Rewrite (H r rZTrue Hr (rZLeTrue n)); Auto; Simpl; Auto.
Apply addEqDoubleNopIsEqual2
with n := n a := a i := q j := rZFalse Hi := Hq Hj := (rZLeFalse n)
Hk := Hr Hl := (rZLeTrue n); Auto.
Apply addEqDoubleNopIsEqual1
with n := n a := a k := r l := rZTrue Hi := Hq Hj := (rZLeFalse n) Hk := Hr
Hl := (rZLeTrue n); Auto.
Rewrite (realizeMemoryinv1 n f a q r Hq Hr); Auto.
Rewrite (H p r Hp Hr); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a q r Hq Hr); Auto.
Rewrite (H p rZFalse Hp (rZLeFalse n)); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a p Hp); Auto.
Rewrite (H q rZTrue Hq (rZLeTrue n)); Auto; Simpl; Auto.
Rewrite (H r rZTrue Hr (rZLeTrue n)); Auto; Simpl; Auto.
Apply addEqDoubleNopIsEqual2
with n := n a := a i := q j := rZTrue Hi := Hq Hj := (rZLeTrue n) Hk := Hr
Hl := (rZLeTrue n); Auto.
Apply addEqDoubleNopIsEqual1
with n := n a := a k := r l := rZTrue Hi := Hq Hj := (rZLeTrue n) Hk := Hr
Hl := (rZLeTrue n); Auto.
Rewrite (realizeMemoryinvTrue n f a q Hq); Auto.
Rewrite (H p r Hp Hr); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvFalse n f a q Hq); Auto.
Rewrite (H p rZFalse Hp (rZLeFalse n)); Auto; Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a r Hr); Auto.
Rewrite (H p q Hp Hq); Auto.
Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinvFalse n f a r Hr); Auto.
Rewrite (H p rZFalse Hp (rZLeFalse n)); Auto.
Case (fEval f q); Simpl; Auto.
Qed.
Theorem
tSomeRealizeMemoryAnd:
(b:(memory n))
(doTripletAndP (tSome n b)) -> (evalTriplet f (Triplet rAnd p q r))=true ->
(realizeMemory n f b).
Intros b doT Eval0; Apply realizeMemoryDef; Auto.
Intros i j Hi Hj H'.
Generalize Eval0; Clear Eval0; Inversion doT; Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a p q Hp Hq); Auto.
Generalize (someaddEqDouble
b q rZTrue r rZFalse i j Hq (rZLeTrue n) Hr (rZLeFalse n) Hi Hj H
H').
Case (fEval f r); Simpl; Case (fEval f q); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a p r Hp Hr); Auto.
Generalize (someaddEqDouble
b q rZFalse r rZTrue i j Hq (rZLeFalse n) Hr (rZLeTrue n) Hi Hj H
H').
Case (fEval f r); Simpl; Case (fEval f q); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Auto.
Rewrite (realizeMemoryinv1 n f a q r Hq Hr); Auto.
Generalize (tSometrAddEq b p r i j Hp Hr Hi Hj H H').
Case (fEval f r); Simpl; Case (fEval f p); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a q r Hq Hr); Auto.
Generalize (tSometrAddEq b p rZFalse i j Hp (rZLeFalse n) Hi Hj H H').
Case (fEval f r); Simpl; Case (fEval f p); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a p Hp); Auto.
Generalize (someaddEqDouble
b q rZTrue r rZTrue i j Hq (rZLeTrue n) Hr (rZLeTrue n) Hi Hj H H').
Case (fEval f r); Simpl; Case (fEval f q); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a q Hq); Auto.
Generalize (tSometrAddEq b p r i j Hp Hr Hi Hj H H').
Case (fEval f r); Simpl; Case (fEval f p); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Auto.
Rewrite (realizeMemoryinvFalse n f a q Hq); Auto.
Generalize (tSometrAddEq b p rZFalse i j Hp (rZLeFalse n) Hi Hj H H').
Case (fEval f r); Simpl; Case (fEval f p); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a r Hr); Auto.
Generalize (tSometrAddEq b p q i j Hp Hq Hi Hj H H').
Case (fEval f q); Simpl; Case (fEval f p); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Auto.
Rewrite (realizeMemoryinvFalse n f a r Hr); Auto.
Generalize (tSometrAddEq b p rZFalse i j Hp (rZLeFalse n) Hi Hj H H').
Case (fEval f q); Simpl; Case (fEval f p); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Auto.
Qed.
Theorem
mLessDoTripletAnd:
(b:(memory n)) (doTripletAndP (tSome n b)) ->(mLess n b a).
Intros b doT; Inversion doT.
Apply mLessAddEqDouble
with i := q j := rZTrue k := r l := rZFalse Hi := Hq Hj := (rZLeTrue n)
Hk := Hr Hl := (rZLeFalse n); Auto.
Apply mLessAddEqDouble
with i := q j := rZFalse k := r l := rZTrue Hi := Hq Hj := (rZLeFalse n)
Hk := Hr Hl := (rZLeTrue n); Auto.
Apply addEqMless with i := p j := r Hi := Hp Hj := Hr; Auto.
Apply addEqMless with i := p j := rZFalse Hi := Hp Hj := (rZLeFalse n); Auto.
Apply mLessAddEqDouble
with i := q j := rZTrue k := r l := rZTrue Hi := Hq Hj := (rZLeTrue n)
Hk := Hr Hl := (rZLeTrue n); Auto.
Apply addEqMless with i := p j := r Hi := Hp Hj := Hr; Auto.
Apply addEqMless with i := p j := rZFalse Hi := Hp Hj := (rZLeFalse n); Auto.
Apply addEqMless with i := p j := q Hi := Hp Hj := Hq; Auto.
Apply addEqMless with i := p j := rZFalse Hi := Hp Hj := (rZLeFalse n); Auto.
Qed.
Theorem
doTripletAndSomeInc:
(b:(memory n)) (doTripletAndP (tSome n b)) ->(inclMem n a b).
Intros b doT; Inversion doT; Auto.
Apply addEqDoubleSomeInc
with i := q j := rZTrue k := r l := rZFalse Hi := Hq Hj := (rZLeTrue n)
Hk := Hr Hl := (rZLeFalse n); Auto.
Apply addEqDoubleSomeInc
with i := q j := rZFalse k := r l := rZTrue Hi := Hq Hj := (rZLeFalse n)
Hk := Hr Hl := (rZLeTrue n); Auto.
Apply addEqSomeIncl with i := p j := r Hi := Hp Hj := Hr; Auto.
Apply addEqSomeIncl with i := p j := rZFalse Hi := Hp Hj := (rZLeFalse n); Auto.
Apply addEqDoubleSomeInc
with i := q j := rZTrue k := r l := rZTrue Hi := Hq Hj := (rZLeTrue n)
Hk := Hr Hl := (rZLeTrue n); Auto.
Apply addEqSomeIncl with i := p j := r Hi := Hp Hj := Hr; Auto.
Apply addEqSomeIncl with i := p j := rZFalse Hi := Hp Hj := (rZLeFalse n); Auto.
Apply addEqSomeIncl with i := p j := q Hi := Hp Hj := Hq; Auto.
Apply addEqSomeIncl with i := p j := rZFalse Hi := Hp Hj := (rZLeFalse n); Auto.
Qed.
Definition
doTripletAnd :=
Cases (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))) of
left =>
(Some
?
(addEqDouble
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)))
| right => Cases (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))) of
left =>
(Some
?
(addEqDouble
n a q rZFalse r rZTrue Hq (rZLeFalse n) Hr
(rZLeTrue n)))
| right =>
Cases (rZDec (mEval n a q Hq) (mEval n a r Hr)) of
left => (Some ? (addEq n a p r Hp Hr))
| right =>
Cases (rZDec
(mEval n a q Hq)
(rZComp (mEval n a r Hr))) of
left =>
(Some
? (addEq n a p rZFalse Hp (rZLeFalse n)))
| right =>
Cases (rZDec (mEval n a p Hp) rZTrue) of
left =>
(Some
?
(addEqDouble
n a q rZTrue r rZTrue Hq
(rZLeTrue n) Hr (rZLeTrue n)))
| right =>
Cases (rZDec
(mEval n a q Hq) rZTrue) of
left =>
(Some
? (addEq n a p r Hp Hr))
| right =>
Cases (rZDec
(mEval n a q Hq)
rZFalse) of
left =>
(Some
?
(addEq
n a p rZFalse Hp
(rZLeFalse n)))
| right =>
Cases (rZDec
(mEval
n a r Hr)
rZTrue) of
left =>
(Some
?
(addEq
n a p q
Hp Hq))
| right =>
Cases (rZDec
(mEval
n
a
r
Hr)
rZFalse) of
left =>
(Some
?
(addEq
n
a
p
rZFalse
Hp
(rZLeFalse
n)))
| right =>
(None
(tMemory
n))
end
end
end
end
end
end
end
end
end.
End sect.
Hints Resolve
doTripletAndPpmq doTripletAndPpmr doTripletAndPqr doTripletAndPqrm
doTripletAndPpT doTripletAndPqT doTripletAndPqF doTripletAndPrT doTripletAndPrF
doTripletAndPrF.
Theorem
doTripletAndisP:
(n:rNat)
(a:(memory n))
(b:(tMemory n))
(p, q, r:rZ)
(Hp:(rZLe p n))
(Hq:(rZLe q n))
(Hr:(rZLe r n)) (doTripletAnd n a p q r Hp Hq Hr)=(Some ? b) ->
(doTripletAndP n a p q r Hp Hq Hr b).
Intros n a b p q r Hp Hq Hr; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a r Hr) rZTrue); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a r Hr) rZFalse); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Intros H'; Inversion H'.
Qed.
Theorem
doTripletAndisNotP:
(n:rNat)
(a:(memory n))
(b:(tMemory n))
(p, q, r:rZ)
(Hp:(rZLe p n))
(Hq:(rZLe q n))
(Hr:(rZLe r n)) (doTripletAnd n a p q r Hp Hq Hr)=(None (tMemory n)) ->
~ (doTripletAndP n a p q r Hp Hq Hr b).
Intros n a b p q r Hp Hq Hr; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eq0;
[Intros EqS; Inversion EqS; Auto | Idtac].
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eq1;
[Intros EqS; Inversion EqS; Auto | Idtac].
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eq2;
[Intros EqS; Inversion EqS; Auto | Idtac].
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eq3;
[Intros EqS; Inversion EqS; Auto | Idtac].
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eq4;
[Intros EqS; Inversion EqS; Auto | Idtac].
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eq5;
[Intros EqS; Inversion EqS; Auto | Idtac].
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eq6;
[Intros EqS; Inversion EqS; Auto | Idtac].
Case (rZDec (mEval n a r Hr) rZTrue); Intros Eq7;
[Intros EqS; Inversion EqS; Auto | Idtac].
Case (rZDec (mEval n a r Hr) rZFalse); Intros Eq8;
[Intros EqS; Inversion EqS; Auto | Idtac].
Intros H'; Red; Intros H'0; Inversion H'0; Auto.
Qed.
Theorem
doTripletAndNopNop:
(n:rNat)
(a:(memory n))
(b:(tMemory n))
(p, q, r:rZ)
(Hp:(rZLe p n))
(Hq:(rZLe q n))
(Hr:(rZLe r n))
(doTripletAndP n a p q r Hp Hq Hr b) ->
(doTripletAnd n a p q r Hp Hq Hr)=(Some ? (tNop n)) ->b=(tNop n).
Intros n a b p q r Hp Hq Hr H'; Elim H'; Auto.
Intros H'0; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp; Auto.
Intros H'1; Inversion H'1; Auto.
Case Eqp; Auto.
Intros Eq0; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a p Hp)=(rZComp (mEval n a r Hr));
Auto.
Rewrite Eqp; Auto.
Rewrite (addEqDoubleNopIsEqual1
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)); Auto.
Rewrite (addEqDoubleNopIsEqual2
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)); Auto.
Rewrite (mEvalRzTrue n a); Rewrite (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp; Auto.
Intros H'1; Inversion H'1; Auto.
Case Eqp0; Auto.
Intros Eqq; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a q Hq)=(mEval n a r Hr); Auto.
Rewrite (addEqDoubleNopIsEqual1
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)); Auto.
Rewrite (addEqDoubleNopIsEqual2
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)); Auto.
Rewrite (mEvalRzTrue n a); Rewrite (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'; Auto.
Case Eqp; Rewrite Eqq; Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq'; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqq'; Auto.
Intros Eqq; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqp.
Rewrite (addEqDoubleNopIsEqual1
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)); Auto.
Rewrite (mEvalRzTrue n a); Rewrite (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqp'.
Rewrite (addEqDoubleNopIsEqual2
n a q rZFalse r rZTrue Hq (rZLeFalse n) Hr (rZLeTrue n)); Auto.
Rewrite (mEvalRzTrue n a); Rewrite (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq'; Auto.
Absurd (mEval n a q Hq)=(rZComp (mEval n a r Hr)); Auto.
Rewrite Eqq'; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq''; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqq''; Auto.
Intros Eqp; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a p Hp)=rZTrue; Auto.
Rewrite Eqp0.
Rewrite (addEqDoubleNopIsEqual1
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)); Auto.
Rewrite (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a p Hp)=(rZComp (mEval n a r Hr));
Auto.
Rewrite Eqp.
Rewrite (addEqDoubleNopIsEqual2
n a q rZFalse r rZTrue Hq (rZLeFalse n) Hr (rZLeTrue n)); Auto.
Rewrite (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq; Auto.
Intros H'0.
Apply addEqDoubleNopDef; Auto; Inversion H'0.
Apply sym_equal; Rewrite (mEvalRzTrue n a); Rewrite <- Eqp; Rewrite Eqq.
Apply addEqNop; Auto.
Rewrite (mEvalRzTrue n a); Auto.
Apply sym_equal; Rewrite <- Eqp.
Apply addEqNop; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq'; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a p Hp)=rZTrue; Auto.
Rewrite (addEqNop n a p rZFalse Hp (rZLeFalse n)); Auto.
Rewrite (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp''; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqp''; Auto.
Intros Eqq; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp; Auto.
Intros H'0; Apply nopAddEq; Inversion H'0.
Rewrite Eqp; Rewrite Eqq; Simpl.
Apply sym_equal.
Rewrite (addEqDoubleNopIsEqual2
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a q Hq)=rZTrue; Auto.
Rewrite (addEqDoubleNopIsEqual1
n a q rZFalse r rZTrue Hq (rZLeFalse n) Hr (rZLeTrue n)); Auto.
Rewrite (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq'; Auto.
Intros H'0; Inversion H'0; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq''; Auto.
Intros H'0; Apply nopAddEq; Inversion H'0.
Rewrite <- (rZCompInv (mEval n a r Hr)); Rewrite <- Eqq''; Rewrite Eqq; Simpl;
Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp''; Auto.
Intros H'0; Apply nopAddEq; Inversion H'0.
Rewrite Eqp'';
Rewrite (addEqDoubleNopIsEqual2
n a q rZTrue r rZTrue Hq (rZLeTrue n) Hr (rZLeTrue n)); Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Epq'''; Auto.
Intros H'0; Inversion H'0; Auto.
Case Epq'''; Auto.
Intros Eqq; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a q Hq)=rZFalse; Auto.
Rewrite (addEqDoubleNopIsEqual1
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)); Auto.
Rewrite (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqp';
Rewrite (addEqDoubleNopIsEqual2
n a q rZFalse r rZTrue Hq (rZLeFalse n) Hr (rZLeTrue n)); Auto.
Rewrite (mEvalRzTrue n a); Rewrite (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq'; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite (mEvalRzFalse n a); Rewrite <- Eqq; Rewrite Eqq'; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq''; Auto.
Intros H'0; Inversion H'0; Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp''; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a q Hq)=rZFalse; Auto.
Rewrite (addEqDoubleNopIsEqual1
n a q rZTrue r rZTrue Hq (rZLeTrue n) Hr (rZLeTrue n)); Auto;
Rewrite (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eqq'''; Auto.
Absurd (mEval n a q Hq)=rZTrue; Auto; Rewrite Eqq; Auto.
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eqq''''; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqq''''; Auto.
Intros Eqr; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a r Hr)=rZTrue; Auto.
Rewrite (addEqDoubleNopIsEqual2
n a q rZTrue r rZFalse Hq (rZLeTrue n) Hr (rZLeFalse n)); Auto;
Rewrite (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqp'; Rewrite Eqr; Simpl; Rewrite <- (mEvalRzFalse n a); Auto.
Apply sym_equal;
Apply addEqDoubleNopIsEqual1
with k := r l := rZTrue Hk := Hr Hl := (rZLeTrue n); Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqq; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq'; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqq'; Rewrite Eqr; Simpl; Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp''; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqp''; Rewrite <- (mEvalRzTrue n a).
Apply sym_equal;
Apply addEqDoubleNopIsEqual1
with k := r l := rZTrue Hk := Hr Hl := (rZLeTrue n); Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eqp'''; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqp'''; Rewrite <- Eqr; Auto.
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eqp''''; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqp''''; Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a r Hr) rZTrue); Intros Eqr'; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqr'; Auto.
Intros Eqr; Unfold doTripletAnd.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite Eqp; Rewrite (mEvalRzFalse n a);
Change (rZComp (mEval n a q Hq))=(rZComp rZTrue); Rewrite <- (mEvalRzTrue n a);
Apply rZCompComp.
Apply addEqDoubleNopIsEqual1
with k := r l := rZFalse Hk := Hr Hl := (rZLeFalse n); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a r Hr)=rZFalse; Auto.
Rewrite (addEqDoubleNopIsEqual2
n a q rZFalse r rZTrue Hq (rZLeFalse n) Hr (rZLeTrue n)); Auto;
Rewrite (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq; Auto.
Intros H'0; Apply nopAddEq; Auto; Inversion H'0.
Rewrite (mEvalRzFalse n a); Rewrite <- Eqr; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq'; Auto.
Intros H'0; Inversion H'0; Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp''; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a r Hr)=rZFalse; Auto.
Rewrite (addEqDoubleNopIsEqual2
n a q rZTrue r rZTrue Hq (rZLeTrue n) Hr (rZLeTrue n)); Auto;
Rewrite (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eqp'''; Auto.
Case Eqq'; Rewrite Eqr; Rewrite Eqp'''; Auto.
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eqp''''; Auto.
Case Eqq; Rewrite Eqr; Rewrite Eqp''''; Auto.
Case (rZDec (mEval n a r Hr) rZTrue); Intros Eqr'; Auto.
Absurd (mEval n a r Hr)=rZTrue; Auto; Rewrite Eqr; Auto.
Case (rZDec (mEval n a r Hr) rZFalse); Intros Eqr''; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqr''; Auto.
Qed.
Theorem
doTripletAndEqEq:
(n:rNat)
(m1, m2:(memory n))
(p1, p2, q1, q2, r1, r2:rZ)
(Hp1:(rZLe p1 n))
(Hp2:(rZLe p2 n))
(Hq1:(rZLe q1 n))
(Hq2:(rZLe q2 n))
(Hr1:(rZLe r1 n))
(Hr2:(rZLe r2 n))
(eqMem n m1 m2) ->
(mEval n m1 p1 Hp1)=(mEval n m1 p2 Hp2) ->
(mEval n m1 q1 Hq1)=(mEval n m1 q2 Hq2) ->
(mEval n m1 r1 Hr1)=(mEval n m1 r2 Hr2) ->
(eqOption
(tMemory n) (eqtMem n) (doTripletAnd n m1 p1 q1 r1 Hp1 Hq1 Hr1)
(doTripletAnd n m2 p2 q2 r2 Hp2 Hq2 Hr2)).
Intros n m1 m2 p1 p2 q1 q2 r1 r2 Hp1 Hp2 Hq1 Hq2 Hr1 Hr2 eqM Eqp Eqq Eqr;
Unfold doTripletAnd.
Cut (eqMem n m2 m1); [Intros Eqm2m1 | Apply (eqMemSym n)]; Auto.
Cut (mEval n m2 p1 Hp1)=(mEval n m2 p2 Hp2);
[Intros Eqp' | Apply eqMeminv1 with m1 := m1]; Auto.
Cut (mEval n m2 q1 Hq1)=(mEval n m2 q2 Hq2);
[Intros Eqq' | Apply eqMeminv1 with m1 := m1]; Auto.
Cut (mEval n m2 r1 Hr1)=(mEval n m2 r2 Hr2);
[Intros Eqr' | Apply eqMeminv1 with m1 := m1]; Auto.
Case (rZDec (mEval n m1 p1 Hp1) (rZComp (mEval n m1 q1 Hq1)));
Case (rZDec (mEval n m2 p2 Hp2) (rZComp (mEval n m2 q2 Hq2))); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvopp1 with m1 := m1; Auto;
Rewrite <- Eqq; Rewrite <- Eqp; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvopp2 with m2 := m2; Auto; Rewrite Eqq';
Rewrite Eqp'; Auto.
Intros H'0 H'1; Clear H'0 H'1;
Case (rZDec (mEval n m1 p1 Hp1) (rZComp (mEval n m1 r1 Hr1)));
Case (rZDec (mEval n m2 p2 Hp2) (rZComp (mEval n m2 r2 Hr2))); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvopp1 with m1 := m1; Auto;
Rewrite <- Eqr; Rewrite <- Eqp; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvopp2 with m2 := m2; Auto; Rewrite Eqr';
Rewrite Eqp'; Auto.
Intros H'0 H'1; Clear H'0 H'1;
Case (rZDec (mEval n m1 q1 Hq1) (mEval n m1 r1 Hr1));
Case (rZDec (mEval n m2 q2 Hq2) (mEval n m2 r2 Hr2)); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminv1 with m1 := m1; Auto; Rewrite <- Eqr;
Rewrite <- Eqq; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminv2 with m2 := m2; Auto; Rewrite Eqr';
Rewrite Eqq'; Auto.
Intros H'0 H'1; Clear H'0 H'1;
Case (rZDec (mEval n m1 q1 Hq1) (rZComp (mEval n m1 r1 Hr1)));
Case (rZDec (mEval n m2 q2 Hq2) (rZComp (mEval n m2 r2 Hr2))); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvopp1 with m1 := m1; Auto;
Rewrite <- Eqr; Rewrite <- Eqq; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvopp2 with m2 := m2; Auto; Rewrite Eqr';
Rewrite Eqq'; Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 p1 Hp1) rZTrue);
Case (rZDec (mEval n m2 p2 Hp2) rZTrue); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvTrue with m1 := m1; Auto;
Rewrite <- Eqp; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvTrue with m1 := m2; Auto; Rewrite Eqp';
Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 q1 Hq1) rZTrue);
Case (rZDec (mEval n m2 q2 Hq2) rZTrue); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvTrue with m1 := m1; Auto;
Rewrite <- Eqq; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvTrue with m1 := m2; Auto; Rewrite Eqq';
Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 q1 Hq1) rZFalse);
Case (rZDec (mEval n m2 q2 Hq2) rZFalse); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvFalse with m1 := m1; Auto;
Rewrite <- Eqq; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvFalse with m1 := m2; Auto; Rewrite Eqq';
Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 r1 Hr1) rZTrue);
Case (rZDec (mEval n m2 r2 Hr2) rZTrue); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvTrue with m1 := m1; Auto;
Rewrite <- Eqr; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvTrue with m1 := m2; Auto; Rewrite Eqr';
Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 r1 Hr1) rZFalse);
Case (rZDec (mEval n m2 r2 Hr2) rZFalse); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvFalse with m1 := m1; Auto;
Rewrite <- Eqr; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvFalse with m1 := m2; Auto; Rewrite Eqr';
Auto.
Qed.
Hints Resolve doTripletAndEqEq.
23/02/99, 17:50