--#include "alfa/Memories.alfa"

--#include "FunFMProofs.alfa"

--#include "NatProofs.alfa"

package MemoriesProofs where
  open Logic  use  trans,  sym,  substSym,  subst,  cong2
  open Utils
   use  BoolAndIntro,  BoolAndElim1,  BoolAndElim2,  excludedMiddle
  open Booleans  use  ifD
  open Module_Prelude  use  (+),  PredTrue
  open Module_Nat
   use  Nat,  plus,  len,  index,  ltNat,  inst__Nat_12_1,  leNat
  open Module_Memories
   use  Addr,  Word,  Data,  Memory,  LookupUpdateM,  UpdateSameM,
        UpdateOtherM,  InRange,  EqRange,  StoreEqRange,  lookupM,
        updateM,  storeList,  StoreProp,  StoreList,  Range,
        LoadEqRange,  loadRange,  LookupInRange,  loadList
  open NatProofs
   use  proofNotLtZero,  addSucc,  proofAddZero,  proofPeano4b,
        natLeRefl,  natLtSucc,  natLeSucc,  natLtPlus,  natPlusLt
  open FunFMProofs
   use  proofLookupUpdateFM,  proofUpdateSameFM,  proofUpdateOtherFM
  proofLookupUpdateM :: LookupUpdateM
    = \(k::Addr) ->
      \(k'::Addr) ->
      \(v::Word) ->
      \(fm1::Memory) ->
      \(fm2::Memory) ->
      case fm1 of {
        (M x1 x2) ->
          case fm2 of { (M x1' x2') -> proofLookupUpdateFM Word k k' v x2 x2';};}
  proofUpdateSameM :: UpdateSameM
    = \(k::Addr) ->
      \(v::Word) ->
      \(mem::Memory) ->
      case mem of { (M free fm) -> proofUpdateSameFM Word k v fm;}
  proofUpdateOtherM :: UpdateOtherM
    = \(k1::Addr) ->
      \(k2::Addr) ->
      \(v::Word) ->
      \(fm::Memory) ->
      case fm of { (M x1 x2) -> proofUpdateOtherFM Word k1 k2 v x2;}
  lemmaStoreList (ws::Data)
                 (mem::Memory)
                 (a::Addr)
                 (i::Nat)
                 (p::PredTrue (ltNat i (len Word ws)))
    :: (===)
         Word
         (lookupM (storeList a ws mem) ((+) Nat inst__Nat_12_1 i a))
         (index Word ws i)
    = case ws of {
        (Nil) ->
          AbsurdityElim
            ((===)
               Word
               (lookupM (storeList a Nil@_ mem) ((+) Nat inst__Nat_12_1 i a))
               (index Word Nil@_ i))
            (excludedMiddle (ltNat i (len Word Nil@_)) p (proofNotLtZero i));
        (Cons x xs) ->
          case i of {
            (O) ->
              proofUpdateSameM
                ((+) Nat inst__Nat_12_1 O@_ a)
                (index Word (Cons@_ x xs) O@_)
                (storeList (S@_ a) xs mem);
            (S x1) ->
              trans
                Word
                (lookupM
                   (storeList a (Cons@_ x xs) mem)
                   ((+) Nat inst__Nat_12_1 (S@_ x1) a))
                (lookupM
                   (storeList (S@_ a) xs mem)
                   ((+) Nat inst__Nat_12_1 (S@_ x1) a))
                (index Word (Cons@_ x xs) (S@_ x1))
                (ImpliesElim
                   (Not ((===) Nat ((+) Nat inst__Nat_12_1 (S@_ x1) a) a))
                   ((===)
                      Word
                      (lookupM
                         (storeList a (Cons@_ x xs) mem)
                         ((+) Nat inst__Nat_12_1 (S@_ x1) a))
                      (lookupM
                         (storeList (S@_ a) xs mem)
                         ((+) Nat inst__Nat_12_1 (S@_ x1) a)))
                   (proofUpdateOtherM
                      ((+) Nat inst__Nat_12_1 (S@_ x1) a)
                      a
                      x
                      (storeList (S@_ a) xs mem))
                   (proofPeano4b x1 a))
                (substSym
                   Nat
                   ((+) Nat inst__Nat_12_1 (S@_ x1) a)
                   (plus x1 (S@_ a))
                   (\(h::Nat) ->
                    (===)
                      Word
                      (lookupM (storeList (S@_ a) xs mem) h)
                      (index Word xs x1))
                   (addSucc x1 a)
                   (lemmaStoreList xs mem (S@_ a) x1 p));};}
  proofStoreList :: StoreList
    = \(ws::Data) ->
      \(mem::Memory) ->
      \(a::Addr) ->
      \(i::Nat) ->
      ImpliesIntro
        (PredTrue (ltNat i (len Word ws)))
        ((===)
           Word
           (lookupM (storeList a ws mem) ((+) Nat inst__Nat_12_1 i a))
           (index Word ws i))
        (\(hyp::PredTrue (ltNat i (len Word ws))) ->
         lemmaStoreList ws mem a i hyp)
  leProp (a::Nat)
         (b::Nat)
         (P::Pred Nat)
         (r::PredTrue (leNat a b))
         (p::(i::Nat) -> P (plus i a))
    :: P b
    = case a of {
        (O) -> substSym Nat b (plus b O@_) P (proofAddZero b) (p b);
        (S x1) ->
          case b of {
            (O) -> case r of { };
            (S x1') ->
              leProp
                x1
                x1'
                (\(h::Nat) -> P (S@_ h))
                r
                (\(i::Nat) ->
                 substSym
                   Nat
                   (S@_ (plus i x1))
                   (Module_Nat.plus i (S@_ x1))
                   P
                   (addSucc i x1)
                   (p i));};}
  lemmaInRange (a::Addr)
               (n::Nat)
               (a'::Addr)
               (P::Pred Addr)
               (r::InRange (Range@_ a n) a')
               (p::(i::Nat) -> (q::PredTrue (ltNat i n)) -> P (plus i a))
    :: P a'
    = let lemma :: PredTrue (ltNat a' (plus n a)) -> P a'
            = leProp
                a
                a'
                (\(h::Nat) -> PredTrue (ltNat h (plus n a)) -> P h)
                (BoolAndElim1
                   (leNat a a')
                   (Module_Nat.ltNat
                      a'
                      (Module_Prelude.(+)
                         Module_Nat.Nat
                         Module_Nat.inst__Nat_12_1
                         n
                         a))
                   r)
                (\(i::Nat) ->
                 \(h::PredTrue (ltNat (plus i a) (plus n a))) ->
                 p i (natPlusLt i n a h))
      in  lemma (BoolAndElim2 (leNat a a') (ltNat a' (plus n a)) r)
  lemmaStoreEqRange (ws::Data)
                    (a::Addr)
                    (a'::Addr)
                    (r::Range)
                    (mem1::Memory)
                    (mem2::Memory)
                    (p::InRange (Range@_ a (len Module_Prelude.Int ws)) a')
    :: (===)
         Word
         (lookupM (storeList a ws mem1) a')
         (lookupM (storeList a ws mem2) a')
    = lemmaInRange
        a
        (len Module_Prelude.Int ws)
        a'
        (\(a''::Addr) ->
         (===)
           Word
           (lookupM (storeList a ws mem1) a'')
           (lookupM (storeList a ws mem2) a''))
        p
        (\(i::Nat) ->
         \(q::PredTrue (ltNat i (len Module_Prelude.Int ws))) ->
         trans
           Word
           (lookupM (storeList a ws mem1) (plus i a))
           (index Word ws i)
           (lookupM (storeList a ws mem2) (plus i a))
           (lemmaStoreList ws mem1 a i q)
           (sym
              Word
              (lookupM (storeList a ws mem2) (plus i a))
              (index Word ws i)
              (lemmaStoreList ws mem2 a i q)))
  proofStoreEqRange :: StoreEqRange
    = \(ws::Module_Prelude.List Module_Prelude.Int) ->
      \(a::Module_Nat.Nat) ->
      \(mem1::Memory) ->
      \(mem2::Memory) ->
      \(a'::Module_Nat.Nat) ->
      ImpliesIntro
        (Module_Prelude.PredTrue
           (Module_Prelude.(&&)
              (Module_Nat.leNat a a')
              (Module_Nat.ltNat
                 a'
                 (Module_Prelude.(+)
                    Module_Nat.Nat
                    Module_Nat.inst__Nat_12_1
                    (Module_Nat.len Module_Prelude.Int ws)
                    a))))
        ((===)
           Module_Prelude.Int
           (lookupM (storeList a ws mem1) a')
           (lookupM (storeList a ws mem2) a'))
        (lemmaStoreEqRange
           ws
           a
           a'
           (Range@_ a (len Module_Prelude.Int ws))
           mem1
           mem2)
  lemmaLookupInRange (a::Addr)
                     (r::Range)
                     (mem1::Memory)
                     (mem2::Memory)
                     (inr::InRange r a)
                     (eqr::EqRange r mem1 mem2)
    :: (===) Word (lookupM mem1 a) (lookupM mem2 a)
    = ImpliesElim
        (InRange r a)
        ((===) Word (lookupM mem1 a) (lookupM mem2 a))
        (eqr a)
        inr
  baseInRange (b::Addr)(s::Nat) :: InRange (Range@_ b (S@_ s)) b
    = BoolAndIntro
        (leNat b b)
        (ltNat b (plus (S@_ s) b))
        (natLeRefl b)
        (natLtSucc b s)
  eqSuccRange (b::Addr)
              (s::Nat)
              (mem1::Memory)
              (mem2::Memory)
              (eqr::EqRange (Range@_ b (S@_ s)) mem1 mem2)
    :: EqRange (Range@_ (S@_ b) s) mem1 mem2
    = \(a::Module_Nat.Nat) ->
      ImpliesIntro
        (Module_Prelude.PredTrue
           (Module_Prelude.(&&)
              (Module_Nat.leNat (S@_ b) a)
              (Module_Nat.ltNat
                 a
                 (Module_Prelude.(+)
                    Module_Nat.Nat
                    Module_Nat.inst__Nat_12_1
                    s
                    (S@_ b)))))
        ((===) Module_Prelude.Int (lookupM mem1 a) (lookupM mem2 a))
        (\(hyp::Module_Prelude.PredTrue
                  (Module_Prelude.(&&)
                     (Module_Nat.leNat (S@_ b) a)
                     (Module_Nat.ltNat
                        a
                        (Module_Prelude.(+)
                           Module_Nat.Nat
                           Module_Nat.inst__Nat_12_1
                           s
                           (S@_ b))))) ->
         lemmaInRange
           (S@_ b)
           s
           a
           (\(h::Addr) -> (===) Word (lookupM mem1 h) (lookupM mem2 h))
           hyp
           (\(i::Nat) ->
            \(q::PredTrue (ltNat i s)) ->
            subst
              Nat
              (S@_ (Module_Nat.plus i b))
              (plus i (S@_ b))
              (\(h::Module_Nat.Nat) ->
               (===) Word (lookupM mem1 h) (lookupM mem2 h))
              (addSucc i b)
              (lemmaLookupInRange
                 (S@_ (Module_Nat.plus i b))
                 (Range@_ b (S@_ s))
                 mem1
                 mem2
                 (BoolAndIntro
                    (leNat b (S@_ (plus i b)))
                    (ltNat (S@_ (plus i b)) (plus (S@_ s) b))
                    (natLeSucc b i)
                    (natLtPlus i s b q))
                 eqr)))
  lemmaLoadList (b::Addr)
                (s::Nat)
                (mem1::Memory)
                (mem2::Memory)
                (eqr::EqRange (Range@_ b s) mem1 mem2)
    :: (===) Data (loadList b s mem1) (loadList b s mem2)
    = case s of {
        (O) -> Ref@_;
        (S x1) ->
          cong2
            Module_Prelude.Int
            (Module_Prelude.List Module_Prelude.Int)
            Data
            (lookupM mem1 b)
            (loadList (S@_ b) x1 mem1)
            (lookupM mem2 b)
            (loadList (S@_ b) x1 mem2)
            (\(h::Module_Prelude.Int) ->
             \(h'::Module_Prelude.List Module_Prelude.Int) ->
             Cons@_ h h')
            (lemmaLookupInRange b (Range@_ b s) mem1 mem2 (baseInRange b x1) eqr)
            (lemmaLoadList (S@_ b) x1 mem1 mem2 (eqSuccRange b x1 mem1 mem2 eqr));}
  lemmaLoadEqRange (r::Range)
                   (mem1::Memory)
                   (mem2::Memory)
                   (eqr::EqRange r mem1 mem2)
    :: (===) Data (loadRange r mem1) (loadRange r mem2)
    = case r of { (Range x1 x2) -> lemmaLoadList x1 x2 mem1 mem2 eqr;}
  proofLookupInRange :: LookupInRange
    = \(a::Module_Nat.Nat) ->
      \(r::Range) ->
      \(mem1::Memory) ->
      \(mem2::Memory) ->
      ImpliesIntro
        (InRange r a)
        (Implies
           (EqRange r mem1 mem2)
           ((===) Word (lookupM mem1 a) (lookupM mem2 a)))
        (\(hyp::InRange r a) ->
         ImpliesIntro
           (EqRange r mem1 mem2)
           ((===) Word (lookupM mem1 a) (lookupM mem2 a))
           (\(hyp'::EqRange r mem1 mem2) ->
            lemmaLookupInRange a r mem1 mem2 hyp hyp'))
  proofLoadEqRange :: LoadEqRange
    = \(r::Range) ->
      \(mem1::Memory) ->
      \(mem2::Memory) ->
      ImpliesIntro
        (EqRange r mem1 mem2)
        ((===) Data (loadRange r mem1) (loadRange r mem2))
        (lemmaLoadEqRange r mem1 mem2)
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding off
var "emptyRange" hide 2
var "lemmaInRange" hide 3
var "BoolAndElim2" hide 2
var "BoolAndIntro" hide 2
 #-}