Require Import Pip.Model.ADT Pip.Model.Hardware Pip.Model.MAL Pip.Model.Lib.

Require Import Pip.Proof.StateLib.

Require Import Coq.Logic.ProofIrrelevance Arith Lia Bool.

Lemma levelEqBEqNatTrue :
∀ l l' : level, StateLib.Level.eqb l l' = true → l = l' .

Lemma levelEqBEqNatFalse :
∀ l ,
StateLib.Level.eqb l fstLevel = false → l > fstLevel.

Lemma levelEqBEqNatFalse0 :
∀ l ,
StateLib.Level.eqb l fstLevel = false → l > 0.

Lemma levelEqBEqNatTrue0 :
∀ l ,
StateLib.Level.eqb l fstLevel = true → l ≤ 0.

Lemma levelPredNone nbL:
StateLib.Level.eqb nbL fstLevel = false →
StateLib.Level.pred nbL ≠ None.

Lemma levelPredLt nbL l :
StateLib.Level.eqb nbL fstLevel = false →
StateLib.Level.pred nbL = Some l →
l < nbL.

Lemma CLevel0_r : ∀ l : level,l - CLevel 0 = l.

Lemma CLevelIdentity : ∀ l : level, CLevel (l - CLevel 0) = l.

Lemma CLevelIdentity1 : ∀ l : level, CLevel l = l.

Lemma CLevelIdentityLe :
∀ a , a < nbLevel → a ≤ CLevel a.

Lemma levelPredMinus1: ∀ l l' , StateLib.Level.eqb l fstLevel = false → StateLib.Level.pred l = Some l' → l' = CLevel (l - 1).

Lemma levelEqNat :
∀ a b , a < nbLevel → b < nbLevel → CLevel a = CLevel b → a = b.

Lemma level_gt :
∀ x x0, x - x0 < nbLevel → CLevel (x - x0) > 0 → x > x0.

Lemma getNbLevelLe :
∀ nbL,
Some nbL = StateLib.getNbLevel →
nbL ≤ CLevel (nbLevel - 1).

Lemma getNbLevelEq :
∀ nbL,
Some nbL = StateLib.getNbLevel →
nbL = CLevel (nbLevel - 1).

Lemma getNbLevelEqOption :
 StateLib.getNbLevel= Some (CLevel (nbLevel - 1)).

Lemma nbLevelEq :
nbLevel - 1 = CLevel (nbLevel - 1).

Lemma fstLevelLe :
∀ l: level ,
fstLevel ≤ l.

Lemma getNbLevelLt nbL:
StateLib.getNbLevel = Some nbL → nbL < nbLevel.

Lemma notFstLevel (level1 : level) :
 0 < level1 →
StateLib.Level.eqb level1 fstLevel = false.

Lemma ClevelMinus0Eq (nbL: level) stop :
stop ≤ nbL →
nbL = CLevel (nbL - stop) →
stop = 0.

Lemma ClevelMinus0Le (nbL: level) stop :
stop ≤ nbL →
nbL ≤ CLevel (nbL - stop) →
stop = 0.

Lemma isDefaultPageFalse : ∀ p, (defaultPage =? pa p) = false → pa p ≠ defaultPage .

Lemma isDefaultPageTrue : ∀ p, (defaultPage =? pa p) = true → pa p = defaultPage .

Lemma pageDecOrNot :
∀ p1 p2 : page, p1 = p2 ∨ p1≠p2.

Lemma listPageDecOrNot :
∀ x (l: list page), List.In x l ∨
              ¬List.In x l.

Lemma indexEqFalse :
∀ a b : nat , a < tableSize → b < tableSize → a ≠ b → CIndex a ≠ CIndex b.

Lemma indexltbTrue :
∀ i1 i2 : index ,
StateLib.Index.ltb i1 i2 = true → i1 < i2.

Lemma indexltbFalse :
∀ i1 i2 : index ,
StateLib.Index.ltb i1 i2 = false → i1 ≥ i2.

Lemma indexBoundEq :
∀ i : index , i≥ CIndex (tableSize - 1) → i = CIndex (tableSize - 1).

Lemma indexDiffLtb :
∀ i1 i2 : index, i2 < i1 ∨ i1 < i2 ↔ i2 ≠ i1.

Lemma indexEqId :
∀ i : index, CIndex i = i.

Lemma indexMaxEqFalseLt :
∀ idx : index, idx ≠ CIndex (tableSize - 1) → idx < tableSize - 1.

Lemma SuccOddEven :
∀ oneI twoI : index,
oneI < tableSize -1 →
StateLib.Index.succ oneI = Some twoI →
Nat.Odd oneI →
Nat.Even twoI.

Lemma SuccEvenOdd :
∀ oneI twoI : index,
oneI < tableSize -1 →
StateLib.Index.succ oneI = Some twoI →
Nat.Even oneI →
Nat.Odd twoI.

Lemma indexMaxEqFalseLt1 :
∀ idx : index, idx ≠ CIndex (tableSize - 1) → idx < CIndex (tableSize - 1).

Lemma noteqIndex a b:
a < tableSizeLowerBound → b < tableSizeLowerBound → a≠b →
CIndex a ≠ CIndex b.

Lemma CIndex0lt :
CIndex 0 < tableSize - 1.

Lemma CIndex1lt oneI:
StateLib.Index.succ (CIndex 0) = Some oneI→
oneI < tableSize - 1.

Lemma indexEqbTrue :
∀ idx1 idx2 : index, true = StateLib.Index.eqb idx1 idx2 →
idx1 = idx2.

Lemma indexLtZero :
∀ idx : index, idx < CIndex 0 → False.

Lemma indexSEqbZeroOdd :
∀ curidx idxsucc,
true = StateLib.Index.eqb curidx (CIndex 0) →
StateLib.Index.succ curidx = Some idxsucc →
Nat.Odd idxsucc.

Lemma indexSuccNot0:
∀ FFI nextFFI,
StateLib.Index.succ FFI = Some nextFFI →
(CIndex 0) ≠ nextFFI .

Lemma indexZeroNotOdd :
∀ idx idxsucc : index,
idx < idxsucc →
StateLib.Index.succ (CIndex 0) = Some idxsucc →
¬ Nat.Odd idx.

 Lemma indexSEqbZeroLt :
∀ idxsucc idx : index,
StateLib.Index.succ (CIndex 0) = Some idxsucc →
idx < idxsucc →
idx = CIndex 0.

Lemma indexSuccGt :
∀ idx curidx iIndex : index,
StateLib.Index.succ curidx = Some iIndex →
idx < curidx →
idx ≠ iIndex.
Lemma Succ0is1 oneI:
StateLib.Index.succ (CIndex 0) = Some oneI →
oneI = CIndex 1.

Lemma indexSuccEqFalse:
∀ curidx iIndex : index,
StateLib.Index.succ curidx = Some iIndex →
 curidx ≠ iIndex.

Lemma indexSuccSuccOddOr (curidx iIndex nextidx idx : index):
StateLib.Index.succ curidx = Some iIndex →
StateLib.Index.succ iIndex = Some nextidx →
Nat.Odd curidx →
Nat.Odd idx →
idx < nextidx →
idx = curidx ∨ idx < curidx.

Lemma indexSuccSuccEvenOr (curidx iIndex nextidx idx : index):
StateLib.Index.succ curidx = Some iIndex →
StateLib.Index.succ iIndex = Some nextidx →
Nat.Even curidx →
Nat.Even idx →
idx < nextidx →
idx = curidx ∨ idx < curidx.

Lemma indexSuccSuccEvenOddLt (curidx iIndex nextidx idx : index):
StateLib.Index.succ curidx = Some iIndex →
StateLib.Index.succ iIndex = Some nextidx →
Nat.Even idx →
Nat.Odd curidx →
idx < nextidx →
idx < iIndex →
idx < curidx.
Lemma indexSuccSuccOddEvenLt (curidx iIndex nextidx idx : index):
StateLib.Index.succ curidx = Some iIndex →
StateLib.Index.succ iIndex = Some nextidx →
Nat.Odd idx →
Nat.Even curidx →
idx < nextidx →
idx < iIndex →
idx < curidx.

Lemma succLet (Scuridx SScuridx idx:index):

StateLib.Index.succ Scuridx = Some SScuridx →
idx < SScuridx →
idx = Scuridx ∨ idx < Scuridx.



Lemma indexNotEqSuccNotEq (idx1 idx2 : index):
idx1 < tableSize -1 →
idx2 < tableSize -1 →
idx1 ≠ idx2 →
StateLib.Index.succ idx2 ≠ StateLib.Index.succ idx1.

Lemma tableSizeMinus0:
∀ idx: index, idx = CIndex (tableSize - 1) → idx>0.

Lemma tableSizeMinus2:
CIndex (tableSize - 1) - 1 = tableSize - 2.

Lemma TableSizeMinus2:
∀ idx, idx < CIndex (tableSize - 2) → idx < CIndex (tableSize - 1).

Lemma predMaxIndex :
∀ i, StateLib.Index.pred (CIndex (tableSize - 1)) = Some i →
i = CIndex (tableSize - 2).

Lemma lengthVAddrNotZero (va : vaddr) : fstLevel < (length va -1).

Lemma CLevelMinusEq0 :
∀ (a : level) b , CLevel (a - b) = CLevel 0 → a = CLevel b ∨ a < b.

Lemma beqPairsTrue :
∀ table1 idx1 table2 idx2 , table1 = table2 ∧ idx1 = idx2 ↔
beqPairs (table1, idx1) (table2, idx2) beqPage beqIndex = true.

Lemma beqPairsFalse :
∀ table1 idx1 table2 idx2 ,
table1 ≠ table2 ∨ idx1 ≠ idx2 ↔
beqPairs (table1, idx1) (table2, idx2) beqPage beqIndex = false.
Require Import List Classical_Prop.
Lemma listIndexDecOrNot :
∀ p1 p2 : list index, p1 = p2 ∨ p1≠p2.

Lemma vaddrDecOrNot :
∀ p1 p2 : vaddr, p1 = p2 ∨ p1≠p2.

Lemma idxPRsucNotEqidxPPR : PRidx < tableSize - 1 →
∃ succidx1 : index, Index.succ PRidx = Some succidx1 ∧ (succidx1 = PPRidx → False).
     Lemma idxPPRsuccNotEqidxPR : PPRidx < tableSize - 1 →
    ∃ succidx2 : index, Index.succ PPRidx = Some succidx2 ∧ (succidx2 = PRidx → False).
Lemma idxPRidxPPRNotEq : PRidx ≠ PPRidx.

    Lemma idxPPRsuccNotEqidxPD : PPRidx < tableSize - 1 →
    ∃ succidx2 : index, StateLib.Index.succ PPRidx = Some succidx2 ∧ (succidx2 = PDidx → False).

Lemma idxPPRidxPDNotEq : PPRidx ≠ PDidx.
    Lemma idxPDsucNotEqidxPPR : PDidx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ PDidx = Some succidx1 ∧ (succidx1 = PPRidx → False).

 Lemma idxPDidxPPRNotEq : PDidx ≠ PPRidx.

 Lemma idxPPRidxSh1NotEq : PPRidx ≠ sh1idx.

    Lemma idxPPRsuccNotEqidxSh1 : PPRidx < tableSize - 1 →
    ∃ succidx2 : index, StateLib.Index.succ PPRidx = Some succidx2 ∧ (succidx2 = sh1idx → False).

    Lemma idxSh1succNotEqidxPPR : sh1idx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ sh1idx = Some succidx1 ∧ (succidx1 = PPRidx → False).

Lemma idxSh1idxPPRnotEq : sh1idx ≠ PPRidx.

    Lemma idxPPRsuccNotEqidxSh2 : PPRidx < tableSize - 1 →
    ∃ succidx2 : index, StateLib.Index.succ PPRidx = Some succidx2 ∧ (succidx2 = sh2idx → False).

Lemma idxPPRidxSh2NotEq : PPRidx ≠ sh2idx.
    Lemma idxSh2succNotEqidxPPR : sh2idx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ sh2idx = Some succidx1 ∧ (succidx1 = PPRidx → False).

Lemma idxSh2idxPPRnotEq : sh2idx ≠ PPRidx.

    Lemma idxPPRsuccNotEqidxSh3 : PPRidx < tableSize - 1 →
    ∃ succidx2 : index, StateLib.Index.succ PPRidx = Some succidx2 ∧ (succidx2 = sh3idx → False).

    Lemma idxSh3succNotEqPPRidx : sh3idx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ sh3idx = Some succidx1 ∧ (succidx1 = PPRidx → False).

 Lemma idxPPRidxSh3NotEq : PPRidx ≠ sh3idx.

    Lemma idxSh3succNotEqPRidx : sh3idx < tableSize - 1 →
    ∃ succidx2 : index, StateLib.Index.succ sh3idx = Some succidx2 ∧ (succidx2 = PRidx → False).

    Lemma idxPRsuccNotEqidxSh3 : PRidx < tableSize - 1 → ∃ succidx1 : index, StateLib.Index.succ PRidx = Some succidx1 ∧ (succidx1 = sh3idx → False).

    Lemma idxPRidxSh3NotEq : PRidx ≠ sh3idx.

    Lemma idxSh3succNotEqidxPDidx : sh3idx < tableSize - 1 →
    ∃ succidx2 : index, StateLib.Index.succ sh3idx = Some succidx2 ∧ (succidx2 = PDidx → False).

    Lemma idxPDsucNotEqidxSh3 : PDidx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ PDidx = Some succidx1 ∧ (succidx1 = sh3idx → False).

    Lemma idxPDidxSh3notEq : PDidx ≠ sh3idx.

    Lemma idxSh3succNotEqidxSh1 :
    sh3idx < tableSize - 1 →
     ∃ succidx2 : index, StateLib.Index.succ sh3idx = Some succidx2 ∧ (succidx2 = sh1idx → False).
    Lemma sh1idxSh3idxNotEq : sh1idx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ sh1idx = Some succidx1 ∧ (succidx1 = sh3idx → False).
    Lemma idxSh1idxSh3notEq : sh1idx ≠ sh3idx.

    Lemma idxSh3succNotEqidxSh2 : sh3idx < tableSize - 1 →
    ∃ succidx2 : index, StateLib.Index.succ sh3idx = Some succidx2 ∧ (succidx2 = sh2idx → False).

    Lemma idxSh2succNotEqidxSh3 : sh2idx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ sh2idx = Some succidx1 ∧ (succidx1 = sh3idx → False).

    Lemma idxSh2idxSh3notEq : sh2idx ≠ sh3idx .

   Lemma idxSh2succNotEqidxPR : sh2idx < tableSize - 1 →
   ∃ succidx2 : index, StateLib.Index.succ sh2idx = Some succidx2 ∧ (succidx2 = PRidx → False).

        Lemma idxPRsuccNotEqidxSh2 : PRidx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ PRidx = Some succidx1 ∧ (succidx1 = sh2idx → False).
        Lemma idxPRidxSh2NotEq : PRidx ≠ sh2idx.

          Lemma idxSh2succNotEqidxPD : sh2idx < tableSize - 1 →
     ∃ succidx2 : index, StateLib.Index.succ sh2idx = Some succidx2 ∧ (succidx2 = PDidx → False).

        Lemma idxPDsucNotEqidxSh2 :
    PDidx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ PDidx = Some succidx1 ∧ (succidx1 = sh2idx → False).


    Lemma idxPDidxSh2notEq : PDidx ≠ sh2idx .

          Lemma idxSh2succNotEqidxSh1 :
    sh2idx < tableSize - 1 →
    ∃ succidx2 : index, StateLib.Index.succ sh2idx = Some succidx2 ∧ (succidx2 = sh1idx → False).


      Lemma idxSh1succNotEqidxSh2 :
    sh1idx < tableSize - 1 →
    ∃ succidx1 : index, StateLib.Index.succ sh1idx = Some succidx1 ∧ (succidx1 = sh2idx → False).


    Lemma idxSh1succNotEqidxPR :
    sh1idx < tableSize - 1 →
    ∃ succidx2 : index, StateLib.Index.succ sh1idx = Some succidx2 ∧ (succidx2 = PRidx → False).
        Lemma idxPRsuccNotEqidxSh1 :
    PRidx + 1 < tableSize →

    ∃ succidx1 : index, StateLib.Index.succ PRidx = Some succidx1 ∧ (succidx1 = sh1idx → False).
Lemma idxPRidxSh1NotEq : PRidx ≠ sh1idx.

          Lemma idxSh1succNotEqidxPD :
    sh1idx + 1 < tableSize →
    ∃ succidx2 : index, StateLib.Index.succ sh1idx = Some succidx2 ∧ (succidx2 = PDidx → False).

        Lemma idxPDsucNotEqidxSh1 :
    PDidx + 1 < tableSize →
    ∃ succidx1 : index, StateLib.Index.succ PDidx = Some succidx1 ∧ (succidx1 = sh1idx → False).


          Lemma idxPDsucNotEqidxPR :
    PDidx + 1 < tableSize →
     ∃ succidx2 : index, StateLib.Index.succ PDidx = Some succidx2 ∧ (succidx2 = PRidx → False).

        Lemma idxPRsucNotEqidxPD :
    PRidx + 1 < tableSize →
    ∃ succidx1 : index, Index.succ PRidx = Some succidx1 ∧ (succidx1 = PDidx → False).

        Lemma idxPRidxPDNotEq : PRidx ≠ PDidx.

Lemma pageEqNatEqEquiv : ∀ (a b : page), eq (p a) (p b) ↔ (eq a b).

Lemma pageNeqNatNeqEquiv : ∀ (a b : page), (p a) ≠ (p b) ↔ a ≠ b.

Lemma index0Ltfalse (idx:index):
idx < CIndex 0 → False.

Lemma indexDecOrNot :
∀ p1 p2 : index, p1 = p2 ∨ p1≠p2.
Lemma getNbLevelEqNat :
∀ nbL,
Some nbL = StateLib.getNbLevel →
nbLevel - 1 = nbL.

Lemma level_eq_l:
∀ x1 x2: level, l x1 = l x2 → x1 = x2.

Lemma page_eq_p:
∀ x1 x2: page, p x1 =p x2 → x1 = x2.