Memory.v

(* Definition of memory over signed real integer *)
Require Import rZ.
Require Import PolyList.
Require Import Inclusion.
Require Import Inverse_Image.
Require Import Wf_nat.
Require Export Option.
Section def.

(* Memory Definition *)
Parameter memory:rNat ->Set.
Variable n:rNat.

Local mem := (memory n).

(* mEval returns the canonical element of the equivalent class *)
Parameter mEval:(m:mem) (i:rZ) (rZLe i n) ->rZ.

Axiom mEvalRLe:(m:mem) (i:rZ) (Hi:(rZLe i n))(rZLe (mEval m i Hi) n).
Hints Resolve mEvalRLe.

Axiom mEvalIrr:
      (m:mem) (i, j:rZ) (Hi:(rZLe i n)) (Hj:(rZLe j n)) i=j ->
      (mEval m i Hi)=(mEval m j Hj).
Hints Resolve mEvalIrr.

Axiom mEvalInvol:
      (m:mem) (i:rZ) (Hi:(rZLe i n))
      (mEval m (mEval m i Hi) (mEvalRLe m i Hi))=(mEval m i Hi).

Axiom mEvalComp:
      (m:mem) (i:rZ) (Hi1:(rZLe i n)) (Hi2:(rZLe (rZComp i) n))
      (mEval m (rZComp i) Hi2)=(rZComp (mEval m i Hi1)).
Hints Resolve mEvalComp.

Axiom mEvalRzTrue:(a:mem)(mEval a rZTrue (rZLeTrue n))=rZTrue.
Hints Resolve mEvalRzTrue.

Theorem mEvalRzFalse: (a:mem)(mEval a rZFalse (rZLeFalse n))=rZFalse.
Intros a.
Rewrite (mEvalIrr
           a rZFalse (rZComp rZTrue) (rZLeFalse n)
           (rZLeComp n rZTrue (rZLeTrue n))).
Rewrite (mEvalComp a rZTrue (rZLeTrue n) (rZLeComp n rZTrue (rZLeTrue n))); Auto.
Rewrite mEvalRzTrue; Simpl; Auto.
Simpl; Auto.
Qed.
Hints Resolve mEvalRzFalse.
Parameter getBottomList:mem ->(list rNat).

Axiom getBottomListMax:
      (m:mem) (i:rNat) (In i (getBottomList m)) ->(rZLe (rZPlus i) n).

Axiom getBottomListBottom:
      (m:mem)
      (i:rNat) (Hi:(rZLe (rZPlus i) n)) (mEval m (rZPlus i) Hi)=(rZPlus i) ->
      (In i (getBottomList m)).

(* Initial memory and properties *)
Parameter Imem:mem.

Axiom Imem_def:
      (i, j:rZ)
      (Hi:(rZLe i n)) (Hj:(rZLe j n)) (mEval Imem i Hi)=(mEval Imem j Hj) ->i=j.
(*Memory result with 3 states: update contradiction and no change*)

Mutual Inductive tMemory: Set :=
     tSome: mem ->tMemory
    | tContr: tMemory
    | tNop: tMemory .

(* Adding an equation *)
Parameter addEq:mem ->(i, j:rZ) (rZLe i n) -> (rZLe j n) ->tMemory.

Axiom addEqDef1:
      (m1, m2:mem)
      (i, j:rZ)
      (Hi:(rZLe i n)) (Hj:(rZLe j n)) (addEq m1 i j Hi Hj)=(tSome m2) ->
      ~ (mEval m1 i Hi)=(mEval m1 j Hj).

Axiom addEqDef2:
      (m1, m2:mem)
      (i, j:rZ)
      (Hi:(rZLe i n)) (Hj:(rZLe j n)) (addEq m1 i j Hi Hj)=(tSome m2) ->
      ~ (mEval m1 i Hi)=(rZComp (mEval m1 j Hj)).

Axiom addEqTrans:
      (m1, m2:mem)
      (i1, j1, i2, j2:rZ)
      (Hi1:(rZLe i1 n))
      (Hj1:(rZLe j1 n))
      (Hi2:(rZLe i2 n))
      (Hj2:(rZLe j2 n))
      (addEq m1 i1 j1 Hi1 Hj1)=(tSome m2) ->
      (mEval m1 i2 Hi2)=(mEval m1 j2 Hj2) ->(mEval m2 i2 Hi2)=(mEval m2 j2 Hj2).

Axiom addEqSome:
      (m1, m2:mem)
      (i, j:rZ)
      (Hi:(rZLe i n)) (Hj:(rZLe j n)) (addEq m1 i j Hi Hj)=(tSome m2) ->
      (mEval m2 i Hi)=(mEval m2 j Hj).

Axiom addEqContr:
      (m:mem)
      (i, j:rZ) (Hi:(rZLe i n)) (Hj:(rZLe j n)) (addEq m i j Hi Hj)=tContr ->
      (mEval m i Hi)=(rZComp (mEval m j Hj)).
Hints Resolve addEqContr.

Axiom contrAddEq:
      (m:mem)
      (i, j:rZ)
      (Hi:(rZLe i n)) (Hj:(rZLe j n)) (mEval m i Hi)=(rZComp (mEval m j Hj)) ->
      (addEq m i j Hi Hj)=tContr.

Axiom addEqNop:
      (m:mem)
      (i, j:rZ) (Hi:(rZLe i n)) (Hj:(rZLe j n)) (addEq m i j Hi Hj)=tNop ->
      (mEval m i Hi)=(mEval m j Hj).
Hints Resolve addEqNop.

Axiom nopAddEq:
      (m:mem)
      (i, j:rZ) (Hi:(rZLe i n)) (Hj:(rZLe j n)) (mEval m i Hi)=(mEval m j Hj) ->
      (addEq m i j Hi Hj)=tNop.

Axiom addEqSomeDef1:
      (m1, m2:mem)
      (i1, j1, i2, j2:rZ)
      (Hi1:(rZLe i1 n))
      (Hj1:(rZLe j1 n))
      (Hi2:(rZLe i2 n))
      (Hj2:(rZLe j2 n))
      (addEq m1 i1 j1 Hi1 Hj1)=(tSome m2) ->
      (mEval m1 i2 Hi2)=(mEval m1 j2 Hj2) ->(mEval m2 i2 Hi2)=(mEval m2 j2 Hj2).

Axiom addEqInv:
      (m1, m2:mem)
      (i1, j1, i2, j2:rZ)
      (Hi1:(rZLe i1 n))
      (Hj1:(rZLe j1 n))
      (Hi2:(rZLe i2 n))
      (Hj2:(rZLe j2 n))
      (addEq m1 i1 j1 Hi1 Hj1)=(tSome m2) ->
      (mEval m2 i2 Hi2)=(mEval m2 j2 Hj2) ->
      (mEval m1 i2 Hi2)=(mEval m1 j2 Hj2) \/
      ((mEval m1 i1 Hi1)=(mEval m1 i2 Hi2) /\
       (mEval m1 j1 Hj1)=(mEval m1 j2 Hj2) \/
       ((mEval m1 i1 Hi1)=(rZComp (mEval m1 i2 Hi2)) /\
        (mEval m1 j1 Hj1)=(rZComp (mEval m1 j2 Hj2)) \/
        ((mEval m1 i1 Hi1)=(mEval m1 j2 Hj2) /\
         (mEval m1 j1 Hj1)=(mEval m1 i2 Hi2) \/
         (mEval m1 i1 Hi1)=(rZComp (mEval m1 j2 Hj2)) /\
         (mEval m1 j1 Hj1)=(rZComp (mEval m1 i2 Hi2))))).

Theorem someAddEq:
  (m1:mem)
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  ~ (mEval m1 i Hi)=(mEval m1 j Hj) ->
  ~ (mEval m1 i Hi)=(rZComp (mEval m1 j Hj)) ->
  (Ex [m2:mem] (addEq m1 i j Hi Hj)=(tSome m2)).
Intros m1 i j Hi Hj H' H'0.
Generalize (refl_equal ? (addEq m1 i j Hi Hj)); Pattern 2 (addEq m1 i j Hi Hj);
Case (addEq m1 i j Hi Hj); Auto.
Intros m H'1; Exists m; Auto.
Intros H'1; Elim H'0; Auto.
Intros H'1; Elim H'; Auto.
Qed.

(* A memory is than another if it has less equivalent classes *)
Parameter mLess:mem -> mem ->Prop.

Axiom mLessTrans:(transitive mem mLess).

Axiom mLessWf:(well_founded mem mLess).

Axiom addEqMless:
      (m1, m2:mem)
      (i, j:rZ)
      (Hi:(rZLe i n)) (Hj:(rZLe j n)) (addEq m1 i j Hi Hj)=(tSome m2) ->
      (mLess m2 m1).
End def.
(* Realization of memory *)

Mutual Inductive realizeMemory[n:rNat; f:rNat ->bool; b:(memory n)]: Prop :=
     realizeMemoryDef:
       ((i, j:rZ)
        (Hi:(rZLe i n)) (Hj:(rZLe j n)) (mEval n b i Hi)=(mEval n b j Hj) ->
        (fEval f i)=(fEval f j)) ->(realizeMemory n f b) .

Theorem fEvalComp:
  (f:rNat ->bool) (i:rZ)(fEval f (rZComp i))=(negb (fEval f i)).
Intros f i; Case i; Simpl; Auto; Intros r0; Case (f r0); Auto.
Qed.
Hints Resolve mEvalComp.
(*Some properties of Memory *)

Theorem mEvalEval:
  (n:rNat) (f:rNat ->bool) (a:(memory n)) (realizeMemory n f a) ->
  (i:rZ) (Hi:(rZLe i n))(fEval f i)=(fEval f (mEval n a i Hi)).
Intros n f a rMa i Hi; Inversion rMa; Auto.
Apply H with Hi := Hi Hj := (mEvalRLe n a i Hi); Auto.
Apply sym_equal; Apply mEvalInvol; Auto.
Qed.

Theorem realizeMemoryinv1:
  (n:rNat)
  (f:rNat ->bool)
  (a:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n)) (realizeMemory n f a) -> (mEval n a i Hi)=(mEval n a j Hj) ->
  (fEval f i)=(fEval f j).
Intros n f a i j Hi Hj rMa; Inversion rMa; Auto.
Intros H'; Auto.
Apply H with Hi := Hi Hj := Hj; Auto.
Qed.

Theorem realizeMemoryinv2:
  (n:rNat)
  (f:rNat ->bool)
  (a:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (realizeMemory n f a) -> (mEval n a i Hi)=(rZComp (mEval n a j Hj)) ->
  (fEval f i)=(negb (fEval f j)).
Intros n f a i j Hi Hj rMa; Inversion rMa; Auto.
Intros H'; Auto.
Rewrite <- (fEvalComp f j); Auto.
Apply realizeMemoryinv1 with n := n a := a Hi := Hi Hj := (rZLeComp n j Hj);
Auto.
Rewrite H'; Auto.
Qed.

Theorem realizeMemoryinvTrue:
  (n:rNat)
  (f:rNat ->bool)
  (a:(memory n))
  (i:rZ) (Hi:(rZLe i n)) (realizeMemory n f a) -> (mEval n a i Hi)=rZTrue ->
  (fEval f i)=true.
Intros n f a i Hi H' H'0; Change (fEval f i)=(fEval f rZTrue); Auto.
Apply realizeMemoryinv1 with n := n a := a Hi := Hi Hj := (rZLeTrue n); Auto.
Apply sym_equal; Rewrite H'0; Auto.
Apply mEvalRzTrue; Auto.
Qed.

Theorem realizeMemoryinvFalse:
  (n:rNat)
  (f:rNat ->bool)
  (a:(memory n))
  (i:rZ) (Hi:(rZLe i n)) (realizeMemory n f a) -> (mEval n a i Hi)=rZFalse ->
  (fEval f i)=false.
Intros n f a i Hi H' H'0; Change (fEval f i)=(fEval f rZFalse); Auto.
Apply realizeMemoryinv1 with n := n a := a Hi := Hi Hj := (rZLeFalse n); Auto.
Apply sym_equal; Rewrite H'0; Auto.
Apply mEvalRzFalse; Auto.
Qed.
Section incl.
Variable n:rNat.
(*Inclusion and equality of memory*)

Mutual Inductive inclMem[a, b:(memory n)]: Prop :=
     inclMemDef:
       ((i, j:rZ)
        (Hi:(rZLe i n)) (Hj:(rZLe j n)) (mEval n a i Hi)=(mEval n a j Hj) ->
        (mEval n b i Hi)=(mEval n b j Hj)) ->(inclMem a b) .
Hints Resolve inclMemDef.

Axiom inclMemLessComp:
      (a, b, c, d:(memory n)) (inclMem a b) -> (mLess n b c) -> (inclMem c d) ->
      (mLess n a d).

Theorem inclMemRef: (a:(memory n))(inclMem a a).
Intros a; Auto.
Qed.
Hints Resolve inclMemRef.

Theorem inclMemTrans: (transitive (memory n) inclMem).
Red.
Intros x y z H' H'0.
Apply inclMemDef; Auto.
Intros i j Hi Hj H'1.
Inversion H'0; Inversion H'; Auto.
Qed.

Theorem addEqSomeIncl:
  (m1, m2:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n)) (Hj:(rZLe j n)) (addEq n m1 i j Hi Hj)=(tSome n m2) ->
  (inclMem m1 m2).
Intros m1 m2 i j Hi Hj H'.
Apply inclMemDef; Auto.
Intros i0 j0 Hi0 Hj0 H'0.
Apply addEqSomeDef1 with m1 := m1 i1 := i j1 := j Hi1 := Hi Hj1 := Hj; Auto.
Qed.

Theorem addEqNopIncl:
  (m1, m2:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n)) (addEq n m1 i j Hi Hj)=(tNop n) -> (inclMem m1 m2) ->
  (addEq n m2 i j Hi Hj)=(tNop n).
Intros m1 m2 i j Hi Hj H' H'0.
Apply nopAddEq; Auto.
Inversion H'0.
Apply H; Auto.
Apply addEqNop; Auto.
Qed.

Theorem addEqContrIncl:
  (m1, m2:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n)) (addEq n m1 i j Hi Hj)=(tContr n) -> (inclMem m1 m2) ->
  (addEq n m2 i j Hi Hj)=(tContr n).
Intros m1 m2 i j Hi Hj H' H'0.
Apply contrAddEq; Auto.
Rewrite <- (mEvalComp n m2 j Hj (rZLeComp n j Hj)).
Inversion H'0.
Apply H; Auto.
Rewrite (mEvalComp n m1 j Hj (rZLeComp n j Hj)).
Apply addEqContr; Auto.
Qed.

Lemma RealizeInclMemComp:
  (a, b:(memory n)) (f:rNat ->bool) (realizeMemory n f b) -> (inclMem a b) ->
  (realizeMemory n f a).
Intros a b f rMa Incl; Inversion rMa.
Apply realizeMemoryDef; Auto.
Intros i j Hi Hj H'.
Apply H with Hi := Hi Hj := Hj; Auto.
Inversion Incl; Auto.
Qed.

(*Intersection *)
Parameter Minter:
          (a, b, c:(memory n)) (inclMem a b) -> (inclMem a c) ->
          {q:(Option (memory n)) | Cases q of
                                       None => True
                                      | (Some r) =>
                                          (inclMem r b) /\
                                          ((inclMem r c) /\
                                           ((inclMem a r) /\ (mLess n r a)))
                                   end}.

Mutual Inductive eqMem[a, b:(memory n)]: Prop :=
     eqMemDef: (inclMem a b) -> (inclMem b a) ->(eqMem a b) .
Hints Resolve eqMemDef.

Theorem eqMemRef: (a:(memory n))(eqMem a a).
Auto.
Qed.
Hints Resolve eqMemRef.

Theorem eqMemSym: (symmetric (memory n) eqMem).
Red.
Intros x y H'; Inversion H'; Apply eqMemDef; Auto.
Qed.

Theorem eqMemTrans: (transitive (memory n) eqMem).
Red.
Intros x y z H' H'0.
Apply eqMemDef; Auto.
Inversion H'0; Inversion H'; Auto.
Apply inclMemTrans with y := y; Auto.
Inversion H'0; Inversion H'; Auto.
Apply inclMemTrans with y := y; Auto.
Qed.

Theorem eqMeminv1:
  (m1, m2:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n)) (eqMem m1 m2) -> (mEval n m1 i Hi)=(mEval n m1 j Hj) ->
  (mEval n m2 i Hi)=(mEval n m2 j Hj).
Intros m1 m2 i j Hi Hj H' H'0; Inversion H'; Auto.
Inversion H; Auto.
Qed.

Theorem eqMeminvTrue:
  (m1, m2:(memory n))
  (i:rZ) (Hi:(rZLe i n)) (eqMem m1 m2) -> (mEval n m1 i Hi)=rZTrue ->
  (mEval n m2 i Hi)=rZTrue.
Intros m1 m2 i Hi H'0 H'1.
Rewrite <- (mEvalRzTrue n m2).
Apply eqMeminv1 with m1 := m1; Auto.
Rewrite (mEvalRzTrue n m1); Auto.
Qed.

Theorem eqMeminvFalse:
  (m1, m2:(memory n))
  (i:rZ) (Hi:(rZLe i n)) (eqMem m1 m2) -> (mEval n m1 i Hi)=rZFalse ->
  (mEval n m2 i Hi)=rZFalse.
Intros m1 m2 i Hi H'0 H'1.
Rewrite <- (mEvalRzFalse n m2).
Apply eqMeminv1 with m1 := m1; Auto.
Rewrite (mEvalRzFalse n m1); Auto.
Qed.

Theorem eqMeminvopp1:
  (m1, m2:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (eqMem m1 m2) -> (mEval n m1 i Hi)=(rZComp (mEval n m1 j Hj)) ->
  (mEval n m2 i Hi)=(rZComp (mEval n m2 j Hj)).
Intros m1 m2 i j Hi Hj H' H'0; Inversion H'; Auto.
Inversion H; Auto.
Rewrite <- (mEvalComp n m2 j Hj (rZLeComp n j Hj)).
Apply H1; Auto.
Rewrite (mEvalComp n m1 j Hj (rZLeComp n j Hj)); Auto.
Qed.

Theorem eqMeminv2:
  (m1, m2:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n)) (eqMem m1 m2) -> (mEval n m2 i Hi)=(mEval n m2 j Hj) ->
  (mEval n m1 i Hi)=(mEval n m1 j Hj).
Intros m1 m2 i j Hi Hj H' H'0; Inversion H'; Auto.
Inversion H0; Auto.
Qed.

Theorem eqMeminvopp2:
  (m1, m2:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (eqMem m1 m2) -> (mEval n m2 i Hi)=(rZComp (mEval n m2 j Hj)) ->
  (mEval n m1 i Hi)=(rZComp (mEval n m1 j Hj)).
Intros m1 m2 i j Hi Hj H' H'0.
Apply eqMeminvopp1 with m1 := m2; Auto.
Apply eqMemSym; Auto.
Qed.

Theorem addEqEqNopNop:
  (m1, m2:(memory n))
  (i1, i2, j1, j2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (eqMem m1 m2) ->
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (addEq n m1 i1 j1 Hi1 Hj1)=(tNop n) ->(addEq n m2 i2 j2 Hi2 Hj2)=(tNop n).
Intros m1 m2 i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H' H'0 H'1 H'2.
Apply nopAddEq; Auto.
Apply trans_equal with y := (mEval n m2 i1 Hi1); Auto.
Apply sym_equal.
Apply eqMeminv1 with m1 := m1; Auto.
Apply trans_equal with y := (mEval n m2 j1 Hj1); Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply addEqNop; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Qed.

Theorem addEqEqContr:
  (m1, m2:(memory n))
  (i1, i2, j1, j2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (eqMem m1 m2) ->
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (addEq n m1 i1 j1 Hi1 Hj1)=(tContr n) ->(addEq n m2 i2 j2 Hi2 Hj2)=(tContr n).
Intros m1 m2 i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H' H'0 H'1 H'2.
Apply contrAddEq; Auto.
Rewrite <- (mEvalComp n m2 j2 Hj2 (rZLeComp n j2 Hj2)).
Apply trans_equal with y := (mEval n m2 (rZComp j1) (rZLeComp n j1 Hj1)); Auto.
Apply trans_equal with y := (mEval n m2 i1 Hi1); Auto.
Apply sym_equal.
Apply eqMeminv1 with m1 := m1; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Rewrite (mEvalComp n m1 j1 Hj1 (rZLeComp n j1 Hj1)).
Apply addEqContr; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Rewrite (mEvalComp n m1 j1 Hj1 (rZLeComp n j1 Hj1)).
Rewrite (mEvalComp n m1 j2 Hj2 (rZLeComp n j2 Hj2)).
Apply rZCompComp; Auto.
Qed.

Theorem addEqInclSome:
  (m1, m2, m3, m4:(memory n))
  (i1, i2, j1, j2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (eqMem m1 m2) ->
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (addEq n m1 i1 j1 Hi1 Hj1)=(tSome n m3) ->
  (addEq n m2 i2 j2 Hi2 Hj2)=(tSome n m4) ->(inclMem m3 m4).
Intros m1 m2 m3 m4 i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H' H'0 H'1 H'2 H'3.
Apply inclMemDef; Auto.
Intros i j Hi Hj H'4.
Cut (mEval n m4 i1 Hi1)=(mEval n m4 i2 Hi2); [Intros Eqi1i2 | Idtac].
2:Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2;
   Auto.
2:Apply eqMeminv1 with m1 := m1; Auto.
Cut (mEval n m4 j1 Hj1)=(mEval n m4 j2 Hj2); [Intros Eqj1j2 | Idtac].
2:Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2;
   Auto.
2:Apply eqMeminv1 with m1 := m1; Auto.
Elim (addEqInv n m1 m3 i1 j1 i j Hi1 Hj1 Hi Hj); Auto; Intros Eq0;
[Idtac |
   Elim Eq0; Clear Eq0; Intros Eq0; Elim Eq0; Clear Eq0; Intros Eq0;
    [Intros Eq1 | Elim Eq0; Clear Eq0; Intros Eq0 Eq1 |
      Elim Eq0; Clear Eq0; Intros Eq0; Elim Eq0; Clear Eq0; Intros Eq0 Eq1]];
Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply trans_equal with y := (mEval n m4 i1 Hi1); Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply trans_equal with y := (mEval n m4 i2 Hi2); Auto.
Apply trans_equal with y := (mEval n m4 j2 Hj2); Auto.
Apply addEqSome with m1 := m2; Auto.
Apply trans_equal with y := (mEval n m4 j1 Hj1); Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply trans_equal with y := (mEval n m4 (rZComp i1) (rZLeComp n i1 Hi1)); Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Rewrite (mEvalComp n m1 i1 Hi1 (rZLeComp n i1 Hi1)).
Rewrite Eq0; Rewrite rZCompInv; Auto.
Apply trans_equal with y := (mEval n m4 (rZComp i2) (rZLeComp n i2 Hi2)); Auto.
Rewrite (mEvalComp n m4 i1 Hi1 (rZLeComp n i1 Hi1));
Rewrite (mEvalComp n m4 i2 Hi2 (rZLeComp n i2 Hi2)); Auto.
Apply trans_equal with y := (mEval n m4 (rZComp j2) (rZLeComp n j2 Hj2)); Auto.
Rewrite (mEvalComp n m4 i2 Hi2 (rZLeComp n i2 Hi2));
Rewrite (mEvalComp n m4 j2 Hj2 (rZLeComp n j2 Hj2)); Auto.
Apply rZCompComp; Auto.
Apply addEqSome with m1 := m2; Auto.
Apply trans_equal with y := (mEval n m4 (rZComp j1) (rZLeComp n j1 Hj1)); Auto.
Rewrite (mEvalComp n m4 j1 Hj1 (rZLeComp n j1 Hj1));
Rewrite (mEvalComp n m4 j2 Hj2 (rZLeComp n j2 Hj2)); Auto.
Apply sym_equal; Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Rewrite (mEvalComp n m1 j1 Hj1 (rZLeComp n j1 Hj1)).
Rewrite Eq1; Rewrite rZCompInv; Auto.
Apply sym_equal; Apply trans_equal with y := (mEval n m4 j1 Hj1); Auto.
Apply sym_equal; Apply trans_equal with y := (mEval n m4 i1 Hi1); Auto.
Apply trans_equal with y := (mEval n m4 j2 Hj2); Auto.
Apply trans_equal with y := (mEval n m4 i2 Hi2); Auto.
Apply sym_equal; Auto.
Apply addEqSome with m1 := m2; Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply trans_equal with y := (mEval n m4 (rZComp j1) (rZLeComp n j1 Hj1)); Auto.
Apply sym_equal; Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Rewrite (mEvalComp n m1 j1 Hj1 (rZLeComp n j1 Hj1)).
Rewrite Eq1; Rewrite rZCompInv; Auto.
Apply trans_equal with y := (mEval n m4 (rZComp j2) (rZLeComp n j2 Hj2)); Auto.
Rewrite (mEvalComp n m4 j1 Hj1 (rZLeComp n j1 Hj1));
Rewrite (mEvalComp n m4 j2 Hj2 (rZLeComp n j2 Hj2)); Auto.
Apply trans_equal with y := (mEval n m4 (rZComp i2) (rZLeComp n i2 Hi2)); Auto.
Rewrite (mEvalComp n m4 i2 Hi2 (rZLeComp n i2 Hi2));
Rewrite (mEvalComp n m4 j2 Hj2 (rZLeComp n j2 Hj2)); Auto.
Apply rZCompComp; Auto.
Apply sym_equal; Apply addEqSome with m1 := m2; Auto.
Apply trans_equal with y := (mEval n m4 (rZComp i1) (rZLeComp n i1 Hi1)); Auto.
Rewrite (mEvalComp n m4 i1 Hi1 (rZLeComp n i1 Hi1));
Rewrite (mEvalComp n m4 i2 Hi2 (rZLeComp n i2 Hi2)); Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Rewrite (mEvalComp n m1 i1 Hi1 (rZLeComp n i1 Hi1)).
Rewrite Eq0; Rewrite rZCompInv; Auto.
Qed.

Theorem addEqSomeEq:
  (m1, m2, m3, m4:(memory n))
  (i1, i2, j1, j2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (eqMem m1 m2) ->
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (addEq n m1 i1 j1 Hi1 Hj1)=(tSome n m3) ->
  (addEq n m2 i2 j2 Hi2 Hj2)=(tSome n m4) ->(eqMem m3 m4).
Intros m1 m2 m3 m4 i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H' H'0 H'1 H'2 H'3.
Apply eqMemDef; Auto.
Apply addEqInclSome
     with m1 := m1 m2 := m2 i1 := i1 i2 := i2 j1 := j1 j2 := j2 Hi1 := Hi1
          Hi2 := Hi2 Hj1 := Hj1 Hj2 := Hj2; Auto.
Apply addEqInclSome
     with m1 := m2 m2 := m1 i1 := i2 i2 := i1 j1 := j2 j2 := j1 Hi1 := Hi2
          Hi2 := Hi1 Hj1 := Hj2 Hj2 := Hj1; Auto.
Apply eqMemSym; Auto.
Apply sym_equal; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply sym_equal; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Qed.

Theorem eqMemLessComp:
  (a, b, c, d:(memory n)) (eqMem a b) -> (mLess n b c) -> (eqMem c d) ->
  (mLess n a d).
Intros a b c d H' H'0 H'1; Inversion H'; Inversion H'1.
Apply inclMemLessComp with b := b c := c; Auto.
Qed.

Mutual Inductive eqtMem: (tMemory n) -> (tMemory n) ->Prop :=
     eqtMemDefSome:
       (a, b:(memory n)) (eqMem a b) ->(eqtMem (tSome n a) (tSome n b))
    | eqtMemDefNop: (eqtMem (tNop n) (tNop n))
    | eqtMemDefContr: (eqtMem (tContr n) (tContr n)) .
Hints Resolve eqtMemDefSome eqtMemDefNop eqtMemDefContr.

Theorem eqtMemRef: (a:(tMemory n))(eqtMem a a).
Intros a; Case a; Auto.
Qed.
Hints Resolve eqtMemRef.

Theorem eqtMemTrans: (transitive (tMemory n) eqtMem).
Red.
Intros x y z H'; Inversion H'; Auto.
Intros H'0; Inversion H'0.
Apply eqtMemDefSome; Auto.
Apply eqMemTrans with y := b; Auto.
Qed.

Theorem addEqEqSomeNotNop:
  (m1, m2, m3:(memory n))
  (i1, i2, j1, j2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (addEq n m1 i1 j1 Hi1 Hj1)=(tSome n m3) -> (eqMem m1 m2) ->
  ~ (addEq n m2 i2 j2 Hi2 Hj2)=(tNop n).
Intros m1 m2 m3 i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H' H'0 H'1 H'2; Red; Intros H'3.
Absurd (mEval n m1 i1 Hi1)=(mEval n m1 j1 Hj1); Auto.
Apply addEqDef1 with m2 := m3; Auto.
Rewrite H'; Rewrite H'0; Auto.
Apply eqMeminv2 with m2 := m2; Auto.
Apply addEqNop; Auto.
Qed.

Theorem addEqEqSomeNotContr:
  (m1, m2, m3:(memory n))
  (i1, i2, j1, j2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (addEq n m1 i1 j1 Hi1 Hj1)=(tSome n m3) -> (eqMem m1 m2) ->
  ~ (addEq n m2 i2 j2 Hi2 Hj2)=(tContr n).
Intros m1 m2 m3 i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H' H'0 H'1 H'2; Red; Intros H'3.
Absurd (mEval n m1 i1 Hi1)=(rZComp (mEval n m1 j1 Hj1)); Auto.
Apply addEqDef2 with m2 := m3; Auto.
Rewrite H'0; Rewrite H'; Auto.
Rewrite <- (mEvalComp n m1 j2 Hj2 (rZLeComp n j2 Hj2)).
Apply eqMeminv2 with m2 := m2; Auto.
Rewrite (mEvalComp n m2 j2 Hj2 (rZLeComp n j2 Hj2)).
Apply addEqContr; Auto.
Qed.

Theorem addEqEqNopNotContr:
  (m1, m2:(memory n))
  (i1, i2, j1, j2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (addEq n m1 i1 j1 Hi1 Hj1)=(tNop n) -> (eqMem m1 m2) ->
  ~ (addEq n m2 i2 j2 Hi2 Hj2)=(tContr n).
Intros m1 m2 i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H'0 H'1 H'2 H'3; Red; Intros H'4.
Absurd (mEval n m2 j2 Hj2)=(rZComp (mEval n m2 j2 Hj2)); Auto.
Apply trans_equal with y := (mEval n m2 i2 Hi2); Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Rewrite <- H'1; Rewrite <- H'0; Auto.
Apply sym_equal; Apply addEqNop; Auto.
Apply addEqContr; Auto.
Qed.

Theorem addEqEqAux:
  (m1, m2:(memory n)) (eqMem m1 m2) ->
  (m3, m4:(tMemory n))
  (i1, i2, j1, j2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (addEq n m1 i1 j1 Hi1 Hj1)=m3 -> (addEq n m2 i2 j2 Hi2 Hj2)=m4 ->
  (eqtMem m3 m4).
Intros m1 m2 H'; Cut (eqMem m2 m1); [Intros EqRev | Apply eqMemSym]; Auto.
Intros m3 m4; Case m3; Case m4; Auto.
Intros m m0 i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H'0 H'1 H'2 H'3.
Apply eqtMemDefSome.
Apply addEqSomeEq
     with m1 := m1 m2 := m2 i1 := i1 i2 := i2 j1 := j1 j2 := j2 Hi1 := Hi1
          Hi2 := Hi2 Hj1 := Hj1 Hj2 := Hj2; Auto.
Intros m i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H'0 H'1 H'2 H'3;
Absurd (addEq n m2 i2 j2 Hi2 Hj2)=(tContr n); Auto.
Apply addEqEqSomeNotContr
     with m1 := m1 m3 := m i1 := i1 j1 := j1 Hi1 := Hi1 Hj1 := Hj1; Auto.
Intros m i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H'0 H'1 H'2 H'3;
Absurd (addEq n m2 i2 j2 Hi2 Hj2)=(tNop n); Auto.
Apply addEqEqSomeNotNop
     with m1 := m1 m3 := m i1 := i1 j1 := j1 Hi1 := Hi1 Hj1 := Hj1; Auto.
Intros m i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H'0 H'1 H'2 H'3;
Absurd (addEq n m1 i1 j1 Hi1 Hj1)=(tContr n); Auto.
Apply addEqEqSomeNotContr
     with m1 := m2 m3 := m i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply sym_equal; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply sym_equal; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Intros i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H'0 H'1 H'2 H'3;
Absurd (addEq n m1 i1 j1 Hi1 Hj1)=(tContr n); Auto.
Apply addEqEqNopNotContr with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2;
Auto.
Apply sym_equal; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply sym_equal; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Intros m i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H'0 H'1 H'2 H'3;
Absurd (addEq n m1 i1 j1 Hi1 Hj1)=(tNop n); Auto.
Apply addEqEqSomeNotNop
     with m1 := m2 m3 := m i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply sym_equal; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply sym_equal; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Intros i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H'0 H'1 H'2 H'3;
Absurd (addEq n m2 i2 j2 Hi2 Hj2)=(tContr n); Auto.
Apply addEqEqNopNotContr with m1 := m1 i1 := i1 j1 := j1 Hi1 := Hi1 Hj1 := Hj1;
Auto.
Qed.

Theorem addEqEq:
  (m1, m2:(memory n))
  (i1, i2, j1, j2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (eqMem m1 m2) ->
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (eqtMem (addEq n m1 i1 j1 Hi1 Hj1) (addEq n m2 i2 j2 Hi2 Hj2)).
Intros m1 m2 i1 i2 j1 j2 Hi1 Hi2 Hj1 Hj2 H' H'2 H'3.
Apply addEqEqAux
     with m1 := m1 m2 := m2 i1 := i1 i2 := i2 j1 := j1 j2 := j2 Hi1 := Hi1
          Hi2 := Hi2 Hj1 := Hj1 Hj2 := Hj2; Auto.
Qed.
End incl.
Hints Resolve
mEvalRLe mEvalIrr mEvalComp mEvalRzTrue mEvalRzFalse addEqContr addEqNop
mEvalComp inclMemDef inclMemRef eqMemDef eqMemRef eqtMemRef eqtMemDefSome
eqtMemDefNop eqtMemDefContr addEqEq.

23/02/99, 16:50