{-# OPTIONS --type-in-type
   #-}

module ChangePrefixLemmas where

open import NeilPrelude
open import RealTime
open import Logic
open import List
open import SigVecs
open import TimeDeltaList
open import TimeDeltaListProps
open import Properties
open import Utilities
open import StrictTotalOrder hiding (_<_ ; _≤_)

------------------------------------------------------------------

lemCP-O-empty : {A : Set} → (cp : ChangePrefix A) → Contained cp → cp O ≡ []
lemCP-O-empty cp con with con {O}
... | con' with cp O
lemCP-O-empty cp con | con' | [] = refl
lemCP-O-empty cp con | inl () | _ ∷ _
lemCP-O-empty cp con | inr () | _ ∷ _

lemCP-O-equal : {A : Set} → (cp₁ cp₂ : ChangePrefix A) → Contained cp₁ → Contained cp₂ → cp₁ O ≡ cp₂ O
lemCP-O-equal cp₁ cp₂ con₁ con₂ = trans (lemCP-O-empty cp₁ con₁) (sym (lemCP-O-empty cp₂ con₂))

------------------------------------------------------------------

lemCP-lookupStable : {A : Set} → (t₁ t₂ : Time) → (cp : ChangePrefix A) → Stable cp → t₁ ≤ℜ₀ t₂ → lookupTDL (cp t₂) t₁ ≡ lookupTDL (cp t₁) t₁
lemCP-lookupStable t₁ t₂ cp stab lt with stab lt
lemCP-lookupStable t₁ t₂ cp stab lt | eq with cp t₁
lemCP-lookupStable t₁ t₂ cp stab lt | refl | ._ = sym (lemTDL-lookupTaken t₁ t₁ ≤ℜ₀-refl (cp t₂))

lemCP-lookupAt : {A : Set} → (t₁ t₂ : Time) → (cp : ChangePrefix A) → Stable cp → t₁ ≤ℜ₀ t₂ → IsJust (lookupTDL (cp t₂) t₁) → IsJust (lookupTDL (cp t₁) t₁)
lemCP-lookupAt t₁ t₂ cp stab lt = subst (cong IsJust (lemCP-lookupStable t₁ t₂ cp stab lt))

lemCP-lookupBeyond : {A : Set} → (t₁ t₂ : Time) → (cp : ChangePrefix A) → Contained cp → t₁ <ℜ₀ t₂ → IsNothing (lookupTDL (cp t₁) t₂)
lemCP-lookupBeyond t₁ t₂ cp con lt = lemTDL-lookupBeyond t₂ (cp t₁) (≤<ℜ₀-trans con lt)

lemCP-lookup : {A : Set} → (t₁ t₂ : Time) → (cp : ChangePrefix A) → Stable cp → Contained cp → IsJust (lookupTDL (cp t₂) t₁) → IsJust (lookupTDL (cp t₁) t₁)
lemCP-lookup t₁ t₂ cp stab con p with compareLeqℜ₀ t₁ t₂
lemCP-lookup t₁ t₂ cp stab con p | leq q  = lemCP-lookupAt t₁ t₂ cp stab q p
lemCP-lookup t₁ t₂ cp stab con p | more q = absurd (lemCP-lookupBeyond t₂ t₁ cp con q p)

------------------------------------------------------------------

lemCP-drop-empty : {A : Set} → (t₁ t₂ : Time) → t₁ ≤ℜ₀ t₂ → (cp : ChangePrefix A) → Contained cp → dropIncl t₂ (cp t₁) ≡ []
lemCP-drop-empty t₁ t₂ p cp con = lemTDL-dropInclSum→Empty t₂ (cp t₁) (≤ℜ₀-trans con p) 

lemCP-drop-now-empty : {A : Set} → (t : Time) → (cp : ChangePrefix A) → Contained cp → dropIncl t (cp t) ≡ []
lemCP-drop-now-empty t = lemCP-drop-empty t t ≤ℜ₀-refl

------------------------------------------------------------------