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

module Proofs where

open import NeilPrelude
open import RealTime
open import Logic
open import SigVecs
open import Properties
open import NaryFRP
open import Lemmas

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

-- Stateless sf → Causal sf

Stateless→Causal : {as bs : SVDesc} → (sf : SF as bs) → Stateless {as} {bs} sf → Causal {as} {bs} sf
Stateless→Causal sf p s₁ s₂ t (q , f) = p s₁ s₂ t q

-- Decoupled sf → Causal sf

Decoupled→Causal : {as bs : SVDesc} → (sf : SF as bs) → Decoupled {as} {bs} sf → Causal {as} {bs} sf
Decoupled→Causal sf p s₁ s₂ t (q , f) = p s₁ s₂ t f

-- Changelessʳ sf ⇒ Changeless sf

ChangelessSFʳ⇒ChangelessSF : {as bs : SVDesc} → (sf : SF as bs) → Always (ChangelessSFʳ {as} {bs} sf ⇒ ChangelessSF {as} {bs} sf)
ChangelessSFʳ⇒ChangelessSF sf t p s = snd (p s) 

-- Changelessʳ sf ⇒ ChangePrp sf

ChangelessSFʳ⇒ChangePrp : {as bs : SVDesc} → (sf : SF as bs) → Always (ChangelessSFʳ {as} {bs} sf ⇒ ChangePrp {as} {bs} sf)
ChangelessSFʳ⇒ChangePrp sf t p s = (λ _ → fst (p s)) , λ t' t-refl _ → snd (p s) t' t-refl

-- ChangePrp sf ⇒ ChangeDep sf

ChangePrp⇒ChangeDep : {as bs : SVDesc} → (sf : SF as bs) → EM → Always (ChangePrp {as} {bs} sf ⇒ ChangeDep {as} {bs} sf)
ChangePrp⇒ChangeDep {as} {bs} sf em t f s = lem-Wʳ {Unchanging {as} s} {Unchanging {bs} (sf s)} em t (f s)

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

-- Changeless sf ⇒ Source sf

ChangelessSFʳ⇒Source : {as bs : SVDesc} → Containment → Stability → (sf : SF as bs) → Causal {as} {bs} sf → Always (ChangelessSFʳ {as} {bs} sf ⇒ Source {as} {bs} sf)
ChangelessSFʳ⇒Source {as} {bs} con stab sf cau t p s₁ s₂ Heq = lem-HEqR⇒Cʳ⇒GʳEqR {bs} con stab (sf s₁) (sf s₂) t (lem-HEqR⇒HEqRsf {as} {bs} cau s₁ s₂ t Heq) (p s₁) (p s₂)


-- ChangeDep sf ∧ Source sf ⇒ Changeless sf
-- If the output cannot change until the input changes, and the output does not depend upon the input, then the output can never change

postulate ChangeDep∧Source⇒ChangelessSFʳ : {as bs : SVDesc} → (sf : SF as bs) → Always (ChangeDep {as} {bs} sf ⇒ Source {as} {bs} sf ⇒ ChangelessSFʳ {as} {bs} sf)
-- ChangeDep∧Source⇒ChangelessSFʳ sf t p q s = {!!}

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

-- Changeless sf₁ ∧ ChangePrp sf₂ ⇒ Changeless (sf₁ >>> sf₂)

ChangelessSF1∧ChangePrp2⇒ChangelessSF :  {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Always (ChangelessSF {as} {bs} sf₁ ⇒ ChangePrp {bs} {cs} sf₂ ⇒ ChangelessSF {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂))
ChangelessSF1∧ChangePrp2⇒ChangelessSF sf₁ sf₂ t unch chp s = S-comb₂ (snd (chp (sf₁ s))) (unch s)

-- Changelessʳ sf₁ ∧ ChangePrp sf₂ ⇒ Changelessʳ (sf₁ >>> sf₂)

ChangelessSFʳ1∧ChangePrp2⇒ChangelessSFʳ :  {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Always (ChangelessSFʳ {as} {bs} sf₁ ⇒ ChangePrp {bs} {cs} sf₂ ⇒ ChangelessSFʳ {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂))
ChangelessSFʳ1∧ChangePrp2⇒ChangelessSFʳ sf₁ sf₂ t ch chp s with ch s | chp (sf₁ s)
... | unch , Gunch | cp , Gcp = cp unch , S-comb₂ Gcp Gunch

-- Changelessʳ sf₁ ∧ ChangeDep sf₂ ⇒ Changelessʳ (sf₁ >>> sf₂)

ChangelessSFʳ1∧ChangeDep2⇒ChangelessSFʳ :  {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Always (ChangelessSFʳ {as} {bs} sf₁ ⇒ ChangeDep {bs} {cs} sf₂ ⇒ ChangelessSFʳ {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂))
ChangelessSFʳ1∧ChangeDep2⇒ChangelessSFʳ sf₁ sf₂ t unch₁ chd₂ s with unch₁ s | chd₂ (sf₁ s)
... | unch , Gunch₂ | inl ch₁              = absurd (ch₁ unch)
... | unch , Gunch₁ | inr (unch₂ , Gunch₂) = unch₂ , λ t₁ gt → Gunch₂ (t₁ ₀+₀ ı₀) (<ℜ₀-trans gt lem-ℜ₀-+ı-increasing)
                                                    (λ t' p _ → NotNot (Gunch₁ t' p)) t₁ gt lem-ℜ₀-+ı-increasing


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

-- Preservation of Properties by (>>>)

-- Causal sf₁ × Causal sf₂ → Causal (sf₁ >>> sf₂)

Causal1Causal2→CausalSeq : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Causal {as} {bs} sf₁ → Causal {bs} {cs} sf₂ → Causal {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂)
Causal1Causal2→CausalSeq {as} {bs} sf₁ sf₂ cau₁ cau₂ s₁ s₂ t (eq , Heq) = cau₂ (sf₁ s₁) (sf₁ s₂) t (cau₁ s₁ s₂ t (eq , Heq) , lem-HEqR⇒HEqRsf {as} {bs} cau₁ s₁ s₂ t Heq)


-- Stateless sf₁ × Stateless sf₂ → Stateless (sf₁ >>> sf₂)

Stateless1Stateless2→StatelessSeq : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Stateless {as} {bs} sf₁ → Stateless {bs} {cs} sf₂ → Stateless {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂)
Stateless1Stateless2→StatelessSeq sf₁ sf₂ p q s₁ s₂ t eq = q (sf₁ s₁) (sf₁ s₂) t (p s₁ s₂ t eq)


-- Decoupled sf₁ ⊎ Decoupled sf₂ → Decoupled (sf₁ >>> sf₂)

Decoupled1Decoupled2→DecoupledSeq : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Causal {as} {bs} sf₁ → Causal {bs} {cs} sf₂
                                     → Decoupled {as} {bs} sf₁ ⊎ Decoupled {bs} {cs} sf₂ → Decoupled {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂)
Decoupled1Decoupled2→DecoupledSeq {as} {bs} sf₁ sf₂ cau₁ cau₂ (inl dec₁) s₁ s₂ t Heq = cau₂ (sf₁ s₁) (sf₁ s₂) t (lem-HEqR⇒HʳEqRsf {as} {bs} dec₁ s₁ s₂ t Heq)
Decoupled1Decoupled2→DecoupledSeq {as} {bs} sf₁ sf₂ cau₁ cau₂ (inr dec₂) s₁ s₂ t Heq = dec₂ (sf₁ s₁) (sf₁ s₂) t (lem-HEqR⇒HEqRsf {as} {bs} cau₁ s₁ s₂ t Heq)


-- Source sf₁ ∨ Source sf₂ ⇒ Source (sf₁ >>> sf₂)

Source1Source2⇒SourceSeq : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Causal {as} {bs} sf₁ → Causal {bs} {cs} sf₂ → Always (Source {as} {bs} sf₁ ∨ Source {bs} {cs} sf₂ ⇒ Source {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂))
Source1Source2⇒SourceSeq {as} {bs} sf₁ sf₂ cau₁ cau₂ t src s₁ s₂ Heq with lem-HEqR⇒HEqRsf {as} {bs} cau₁ s₁ s₂ t Heq
Source1Source2⇒SourceSeq           sf₁ sf₂ cau₁ cau₂ t (inr src₂) s₁ s₂ Heq | HeqB = src₂ (sf₁ s₁) (sf₁ s₂) HeqB
Source1Source2⇒SourceSeq           sf₁ sf₂ cau₁ cau₂ t (inl src₁) s₁ s₂ Heq | HeqB with src₁ s₁ s₂ Heq
... | eqB , GeqB = cau₂ (sf₁ s₁) (sf₁ s₂) t (eqB , HeqB) , λ t' lt → cau₂ (sf₁ s₁) (sf₁ s₂) t' (GeqB t' lt , λ t₁ _ → STOℜ₀.lem-LeqEqGeq HeqB eqB GeqB t₁)


-- Changeless sf₂ ⇒ Changeless (sf₁ >>> sf₂)

Changeless2⇒ChangelessSeq : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Always (ChangelessSF {bs} {cs} sf₂ ⇒ ChangelessSF {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂))
Changeless2⇒ChangelessSeq sf₁ sf₂ t p s = p (sf₁ s)


-- Changelessʳ sf₂ ⇒ Changelessʳ (sf₁ >>> sf₂)

Changelessʳ2⇒ChangelessʳSeq : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Always (ChangelessSFʳ {bs} {cs} sf₂ ⇒ ChangelessSFʳ {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂))
Changelessʳ2⇒ChangelessʳSeq sf₁ sf₂ t p s = p (sf₁ s) 


-- ChangePrp sf₁ ∧ ChangePrp sf₂ ⇒ ChangePrp (sf₁ >>> sf₂)

ChangePrp1ChangePrp2⇒ChangePrpSeq : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Always (ChangePrp {as} {bs} sf₁ ⇒ ChangePrp {bs} {cs} sf₂ ⇒ ChangePrp {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂))
ChangePrp1ChangePrp2⇒ChangePrpSeq sf₁ sf₂ t chp₁ chp₂ s with chp₁ s | chp₂ (sf₁ s)
... | unch₁ , Hunch₁ | unch₂ , Hunch₂ = unch₂ ∘ unch₁ , λ t' lt un → Hunch₂ t' lt (Hunch₁ t' lt un)


-- ChangeDep sf₁ ∧ ChangeDep sf₂ ⇒ ChangeDep (sf₁ >>> sf₂)

ChangeDep1ChangeDep2⇒ChangeDepSeq : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF bs cs) → Always (ChangeDep {as} {bs} sf₁ ⇒ ChangeDep {bs} {cs} sf₂ ⇒ ChangeDep {as} {cs} (_>>>_ {as} {bs} {cs} sf₁ sf₂))
ChangeDep1ChangeDep2⇒ChangeDepSeq sf₁ sf₂ t chd₁ chd₂ s with chd₁ s | chd₂ (sf₁ s)
... | inl ch₁           | _                 = inl ch₁ 
... | inr (un₁ , unch₁) | inl ch₁           = absurd (ch₁ un₁)
... | inr (un₁ , unch₁) | inr (un₂ , unch₂) = inr (un₂ , λ t' lt unch → unch₂ t' lt (λ t'' p q → NotNot (unch₁ t' lt unch t'' p q)))


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

-- Preservation of Properties by (&&&)

-- Causal sf₁ × Causal sf₂ → Causal (sf₁ &&& sf₂)

Causal1Causal2→CausalFan : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF as cs) → Causal {as} {bs} sf₁ → Causal {as} {cs} sf₂ → Causal {as} {bs , cs} (_&&&_ {as} {bs} {cs} sf₁ sf₂)
Causal1Causal2→CausalFan {as} {bs} sf₁ sf₂ cau₁ cau₂ s₁ s₂ t Heq = ×-cong (cau₁ s₁ s₂ t Heq) (cau₂ s₁ s₂ t Heq)


-- Stateless sf₁ × Stateless sf₂ → Stateless (sf₁ &&& sf₂)

Stateless1Stateless2→StatelessFan : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF as cs) → Stateless {as} {bs} sf₁ → Stateless {as} {cs} sf₂ → Stateless {as} {bs , cs} (_&&&_ {as} {bs} {cs} sf₁ sf₂)
Stateless1Stateless2→StatelessFan {as} {bs} sf₁ sf₂ sl₁ sl₂ s₁ s₂ t eq = ×-cong (sl₁ s₁ s₂ t eq) (sl₂ s₁ s₂ t eq)


-- Decoupled sf₁ × Decoupled sf₂ → Decoupled (sf₁ &&& sf₂)

Decoupled1Decoupled2→DecoupledFan : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF as cs) → Decoupled {as} {bs} sf₁ → Decoupled {as} {cs} sf₂ → Decoupled {as} {bs , cs} (_&&&_ {as} {bs} {cs} sf₁ sf₂)
Decoupled1Decoupled2→DecoupledFan {as} {bs} sf₁ sf₂ dec₁ dec₂ s₁ s₂ t Heq = ×-cong (dec₁ s₁ s₂ t Heq) (dec₂ s₁ s₂ t Heq)


-- Source sf₁ ∧ Source sf₂ ⇒ Source (sf₁ &&& sf₂)

Source1Source2⇒SourceFan : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF as cs) → Causal {as} {bs} sf₁ → Causal {as} {cs} sf₂ → Always (Source {as} {bs} sf₁ ⇒ Source {as} {cs} sf₂ ⇒ Source {as} {bs , cs} (_&&&_ {as} {bs} {cs} sf₁ sf₂))
Source1Source2⇒SourceFan {as} {bs} sf₁ sf₂ cau₁ cau₂ t src₁ src₂ s₁ s₂ Heq with src₁ s₁ s₂ Heq | src₂ s₁ s₂ Heq
... | eqB , HeqB | eqC , HeqC = ×-cong eqB eqC , result2' (uncurry ×-cong) (HeqB &₂ HeqC)


-- Changeless sf₁ ∧ Changeless sf₂ ⇒ Changeless (sf₁ &&& sf₂)

Changeless1Changeless2⇒ChangelessFan : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF as cs) → Causal {as} {bs} sf₁ → Causal {as} {cs} sf₂ → Always (ChangelessSF {as} {bs} sf₁ ⇒ ChangelessSF {as} {cs} sf₂ ⇒ ChangelessSF {as} {bs , cs} (_&&&_ {as} {bs} {cs} sf₁ sf₂))
Changeless1Changeless2⇒ChangelessFan {as} {bs} sf₁ sf₂ cau₁ cau₂ t ch₁ ch₂ = ch₁ &₃ ch₂


-- Changelessʳ sf₁ ∧ Changelessʳ sf₂ ⇒ Changelessʳ (sf₁ &&& sf₂)

Changelessʳ1Changelessʳ2⇒ChangelessʳFan : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF as cs) → Causal {as} {bs} sf₁ → Causal {as} {cs} sf₂ → Always (ChangelessSFʳ {as} {bs} sf₁ ⇒ ChangelessSFʳ {as} {cs} sf₂ ⇒ ChangelessSFʳ {as} {bs , cs} (_&&&_ {as} {bs} {cs} sf₁ sf₂))
Changelessʳ1Changelessʳ2⇒ChangelessʳFan {as} {bs} sf₁ sf₂ cau₁ cau₂ t ch₁ ch₂ s with ch₁ s | ch₂ s
... | un₁ , Gun₁ | un₂ , Gun₂ = (un₁ , un₂) , Gun₁ &₂ Gun₂


-- ChangePrp sf₁ ∧ ChangePrp sf₂ ⇒ ChangePrp (sf₁ &&& sf₂)

ChangePrp1ChangePrp2⇒ChangePrpFan : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF as cs) → Causal {as} {bs} sf₁ → Causal {as} {cs} sf₂ → Always (ChangePrp {as} {bs} sf₁ ⇒ ChangePrp {as} {cs} sf₂ ⇒ ChangePrp {as} {bs , cs} (_&&&_ {as} {bs} {cs} sf₁ sf₂))
ChangePrp1ChangePrp2⇒ChangePrpFan {as} {bs} sf₁ sf₂ cau₁ cau₂ t chp₁ chp₂ s with chp₁ s | chp₂ s
... | un₁ , Gun₁ | un₂ , Gun₂ = un₁ & un₂ , Gun₁ &₃ Gun₂


-- ChangeDep sf₁ ∧ ChangeDep sf₂ ⇒ ChangeDep (sf₁ &&& sf₂)

ChangeDep1ChangeDep2⇒ChangeDepFan : {as bs cs : SVDesc} → (sf₁ : SF as bs) → (sf₂ : SF as cs) → Causal {as} {bs} sf₁ → Causal {as} {cs} sf₂ → Always (ChangeDep {as} {bs} sf₁ ⇒ ChangeDep {as} {cs} sf₂ ⇒ ChangeDep {as} {bs , cs} (_&&&_ {as} {bs} {cs} sf₁ sf₂))
ChangeDep1ChangeDep2⇒ChangeDepFan {as} {bs} sf₁ sf₂ cau₁ cau₂ t chd₁ chd₂ s with chd₁ s | chd₂ s
... | inl ch₁          | _                = inl ch₁
... | _                | inl ch₂          = inl ch₂
... | inr (un₁ , Gun₁) | inr (un₂ , Gun₂) = inr ((un₁ , un₂) , (Gun₁ &₆ Gun₂))


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

-- Preservation of Properties by (switch)

-- Causal sf × Causal (∀ {e} → f e) → Causal (switch sf f)

-- Causal1Causal2→CausalSwitch : {as bs : SVDesc} → {A : Set} → (sf : SF as (bs , E A)) → (f : A → SF as bs) → Causal {as} {bs , E A} sf → ({e : A} → Causal {as} {bs} (f e)) → Causal {as} {bs} (switch {as} {bs} sf f)
-- Causal1Causal2→CausalSwitch {as} {bs} {A} sf f cau₁ cau₂ = ?

-- Causal1Causal2→CausalSwitch' : {as bs : SVDesc} → {A : Set} → {e : A} → (sf : SF as (bs , E A)) → (f : A → SF as bs) → Causal {as} {bs , E A} sf → Causal {as} {bs} (f e) → Causal {as} {bs} (switch {as} {bs} sf f)
-- Causal1Causal2→CausalSwitch' {as} {bs} {A} {e} sf f cau₁ cau₂ = {!!}

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