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

-- NOTE: Many of these lemmas still need to be proved
-- I believe some will require postulating properties over continuous time
-- For example, if P(x) has always held, and x is unchanging currently, then P(x) holds now.
-- Identifying precisely the properties of continuous time that we need is the important next step

module Lemmas where

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

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

postulate lemS-HEqR⇒U⇒EqR : {A : Set} → (s₁ s₂ : SigVec (S A)) → Always (H (EqSample {S A} s₁ s₂) ⇒ Unchanging {S A} s₁ ⇒ Unchanging {S A} s₂ ⇒ EqSample {S A} s₁ s₂)

lemE-U⇒EqR : {A : Set} → (s₁ s₂ : SigVec (E A)) → Always (Unchanging {E A} s₁ ⇒ Unchanging {E A} s₂ ⇒ EqSample {E A} s₁ s₂)
lemE-U⇒EqR (nothing , _) (nothing , _) O      un₁ un₂ = refl
lemE-U⇒EqR _             (just y' , _) O      un₁ un₂ = magic un₂
lemE-U⇒EqR (just _ , _)  _             O      un₁ un₂ = magic un₁
lemE-U⇒EqR (_ , fdas₁)   (_ , fdas₂)   (t >0) un₁ un₂ = lem-isNothingEq un₁ un₂

lemC-HEqR⇒U⇒EqR : {A : Set} → (s₁ s₂ : SigVec (C A)) → Always (H (EqSample {C A} s₁ s₂) ⇒ Unchanging {C A} s₁ ⇒ Unchanging {C A} s₂ ⇒ EqSample {C A} s₁ s₂)
lemC-HEqR⇒U⇒EqR s₁ s₂ t Heq (t₁ , lt₁ , eq₁ , p₁) (t₂ , lt₂ , eq₂ , p₂) with compareℜ₀ t₁ t₂ | Heq t₁ lt₁ | Heq t₂ lt₂
lemC-HEqR⇒U⇒EqR s₁ s₂ t Heq (.t₂ , lt₁ , eq₁ , p₁) (t₂ , lt₂ , eq₂ , p₂) | refl   | eq₁₂ | _     = trans2 (sym eq₁) eq₁₂ eq₂
lemC-HEqR⇒U⇒EqR s₁ s₂ t Heq (_  , _   , eq₁ , p₁)  (t₂ , lt₂ , eq₂ , p₂) | less q | _    | eq₂₁  = trans2 (sym (p₁ t₂ q lt₂)) eq₂₁ eq₂
lemC-HEqR⇒U⇒EqR s₁ s₂ t Heq (t₁ , lt₁ , eq₁ , p₁) (_  , _   , eq₂ , p₂)  | more q | eq₁₂ | _     = trans2 (sym eq₁) eq₁₂ (p₂ t₁ q lt₁)

lem-HEqR⇒U⇒EqR : {as : SVDesc} → Containment → (s₁ s₂ : SigVec as) → Always (H (EqSample {as} s₁ s₂) ⇒ Unchanging {as} s₁ ⇒ Unchanging {as} s₂ ⇒ EqSample {as} s₁ s₂)
lem-HEqR⇒U⇒EqR {C _} con s₁ s₂ t Heq un₁ un₂ = lemC-HEqR⇒U⇒EqR s₁ s₂ t Heq un₁ un₂
lem-HEqR⇒U⇒EqR {S _} con s₁ s₂ t Heq un₁ un₂ = lemS-HEqR⇒U⇒EqR s₁ s₂ t Heq un₁ un₂
lem-HEqR⇒U⇒EqR {E _} con s₁ s₂ t Heq un₁ un₂ = lemE-U⇒EqR s₁ s₂ t un₁ un₂
lem-HEqR⇒U⇒EqR {as , bs} con (sa₁ , sb₁) (sa₂ , sb₂) t Heq (una₁ , unb₁) (una₂ , unb₂) with ×-split2' (result2' ×-inj Heq)
... | Heqa , Heqb = ×-cong (lem-HEqR⇒U⇒EqR {as} con sa₁ sa₂ t Heqa una₁ una₂) (lem-HEqR⇒U⇒EqR {bs} con sb₁ sb₂ t Heqb unb₁ unb₂)

lem-HEqR⇒Cʳ⇒EqR : {as : SVDesc} → Containment → (s₁ s₂ : SigVec as) → Always (H (EqSample {as} s₁ s₂) ⇒ Changelessʳ {as} s₁ ⇒ Changelessʳ {as} s₂ ⇒ EqSample {as} s₁ s₂)
lem-HEqR⇒Cʳ⇒EqR {as} con s₁ s₂ t Heq (un₁ , Gun₁) (un₂ , Gun₂) = lem-HEqR⇒U⇒EqR {as} con s₁ s₂ t Heq un₁ un₂


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

lemS-GU⇒GUcp : {A : Set} → {a : A} → (cp : ChangePrefix A) → Always (G (UnchangingS (a , cp)) ⇒ G (UnchangingCP cp))
lemS-GU⇒GUcp cp t Gun O ()
lemS-GU⇒GUcp cp t Gun (t' >0) lt = Gun (t' >0) lt

lemE-GU⇒GUcp : {A : Set} → {ma : Maybe A} → (cp : ChangePrefix A) → Always (G (UnchangingE (ma , cp)) ⇒ G (UnchangingCP cp))
lemE-GU⇒GUcp cp t Gun O ()
lemE-GU⇒GUcp cp t Gun (t' >0) lt = Gun (t' >0) lt

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

postulate lemS-EqR⇒C⇒GEqR : {A : Set} → Containment → Stability → (s₁ s₂ : SigVec (S A)) → Always ((EqSample {S A} s₁ s₂) ⇒ Changeless {S A} s₁ ⇒ Changeless {S A} s₂ ⇒ G (EqSample {S A} s₁ s₂))

lemE-EqR⇒C⇒GEqR : {A : Set} → (s₁ s₂ : SigVec (E A)) → Always (Changeless {E A} s₁ ⇒ Changeless {E A} s₂ ⇒ G (EqSample {E A} s₁ s₂))
lemE-EqR⇒C⇒GEqR s₁ s₂ t un₁ un₂ t' lt = lemE-U⇒EqR s₁ s₂ t' (un₁ t' lt) (un₂ t' lt)

postulate lemC-EqR⇒C⇒GEqR : {A : Set} → (s₁ s₂ : SigVec (C A)) → Always ((EqSample {C A} s₁ s₂) ⇒ Changeless {C A} s₁ ⇒ Changeless {C A} s₂ ⇒ G (EqSample {C A} s₁ s₂))

lem-EqR⇒C⇒GEqR : {as : SVDesc} → Containment → Stability → (s₁ s₂ : SigVec as) → Always ((EqSample {as} s₁ s₂) ⇒ Changeless {as} s₁ ⇒ Changeless {as} s₂ ⇒ G (EqSample {as} s₁ s₂))
lem-EqR⇒C⇒GEqR {C A} con stab s₁ s₂ t eq un₁ un₂  = lemC-EqR⇒C⇒GEqR s₁ s₂ t eq un₁ un₂
lem-EqR⇒C⇒GEqR {E A} con stab s₁ s₂ t eq un₁ un₂  = lemE-EqR⇒C⇒GEqR s₁ s₂ t un₁ un₂
lem-EqR⇒C⇒GEqR {S A} con stab s₁ s₂ t eq un₁ un₂  = lemS-EqR⇒C⇒GEqR con stab s₁ s₂ t eq un₁ un₂
lem-EqR⇒C⇒GEqR {as , bs} con stab (sa₁ , sb₁) (sa₂ , sb₂) t eq un₁ un₂  with ×-inj eq
... | eqa , eqb  = λ t' lt → ×-cong (lem-EqR⇒C⇒GEqR {as} con stab sa₁ sa₂ t eqa (result2' fst un₁) (result2' fst un₂) t' lt) (lem-EqR⇒C⇒GEqR {bs} con stab sb₁ sb₂ t eqb (result2' snd un₁) (result2' snd un₂) t' lt)

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

lem-EqR⇒Cʳ⇒GʳEq : {as : SVDesc} → Containment → Stability → (s₁ s₂ : SigVec as) → Always ((EqSample {as} s₁ s₂) ⇒ Changelessʳ {as} s₁ ⇒ Changelessʳ {as} s₂ ⇒ Gʳ (EqSample {as} s₁ s₂))
lem-EqR⇒Cʳ⇒GʳEq {as} con stab s₁ s₂ t eq (_ , Gun₁) (_ , Gun₂) = eq , lem-EqR⇒C⇒GEqR {as} con stab s₁ s₂ t eq Gun₁ Gun₂

lem-HEqR⇒Cʳ⇒GʳEqR : {as : SVDesc} → Containment → Stability → (s₁ s₂ : SigVec as) → Always (H (EqSample {as} s₁ s₂) ⇒ Changelessʳ {as} s₁ ⇒ Changelessʳ {as} s₂ ⇒ Gʳ (EqSample {as} s₁ s₂))
lem-HEqR⇒Cʳ⇒GʳEqR {as} con stab s₁ s₂ t Heq un₁ un₂ = lem-EqR⇒Cʳ⇒GʳEq {as} con stab s₁ s₂ t (lem-HEqR⇒Cʳ⇒EqR {as} con s₁ s₂ t Heq un₁ un₂) un₁ un₂

lem-HEqR⇒HEqRsf : {as bs : SVDesc} → {sf : SF as bs} → Causal {as} {bs} sf → (s₁ s₂ : SigVec as) → Always (H (EqSample {as} s₁ s₂) ⇒ H (EqSample {bs} (sf s₁) (sf s₂)))
lem-HEqR⇒HEqRsf cau s₁ s₂ t Heq t' lt = cau s₁ s₂ t' (STOℜ₀.reduce-range-<-incl lt Heq)

lem-HEqR⇒HʳEqRsf : {as bs : SVDesc} → {sf : SF as bs} → Decoupled {as} {bs} sf → (s₁ s₂ : SigVec as) → Always (H (EqSample {as} s₁ s₂) ⇒ Hʳ (EqSample {bs} (sf s₁) (sf s₂)))
lem-HEqR⇒HʳEqRsf dec s₁ s₂ t Heq  = dec s₁ s₂ t Heq , λ t' lt → dec s₁ s₂ t' (STOℜ₀.reduce-range-< lt Heq)

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