{-# OPTIONS --type-in-type #-}
open import NeilPrelude
module TemporalFunction
(Time : Set)
(_<'_ : Rel Time)
(irreflex : Irreflexive _<'_)
(transit : Transitive _<'_)
where
import TemporalLogic
open TemporalLogic Time _<'_ irreflex transit public
infix 3 _≐_
TVal : Set → Set
TVal A = Time → A
TFun : Set → Set → Set
TFun A B = TVal A → TVal B
_≐_ : {A : Set} → TVal A → TVal A → TPred
(p ≐ q) t = p t ≡ q t
EqualTo : {A : Set} → TVal A → A → TPred
EqualTo s a t = s t ≡ a
EqualAt : {A : Set} → TVal A → Time → TPred
EqualAt s t = EqualTo s (s t)
Contractive : {A B : Set} → TFun A B → Set
Contractive {A} f = (s₁ s₂ : TVal A) → Always (H (s₁ ≐ s₂) ⇒ f s₁ ≐ f s₂)
NonExpansive : {A B : Set} → TFun A B → Set
NonExpansive {A} f = (s₁ s₂ : TVal A) → Always (Hʳ (s₁ ≐ s₂) ⇒ f s₁ ≐ f s₂)
lem-cont→nonexpansive : {A B : Set} → {f : TVal A → TVal B} → Contractive f → NonExpansive f
lem-cont→nonexpansive = result3' (argument snd)
lem-ne2 : {A B C : Set} → {f : TFun (A × B) C} → NonExpansive f → (a₁ a₂ : TVal A) → (b₁ b₂ : TVal B)
→ Always (Hʳ (a₁ ≐ a₂) ⇒ Hʳ (b₁ ≐ b₂) ⇒ f (a₁ & b₁) ≐ f (a₂ & b₂))
lem-ne2 ne a₁ a₂ b₁ b₂ t (eqa , Heqa) (eqb , Heqb) = ne (a₁ & b₁) (a₂ & b₂) t (×-cong eqa eqb , ×-cong3 Heqa Heqb)
lem-H-cong : {A B : Set} → {f : TFun A B} → NonExpansive f → (s₁ s₂ : TVal A) → Always (H (s₁ ≐ s₂) ⇒ H (f s₁ ≐ f s₂))
lem-H-cong ne s₁ s₂ t Heq t' lt = ne s₁ s₂ t' (reduce-range-<-incl lt Heq)
lem-Hʳ : {A B : Set} → {f : TFun A B} → NonExpansive f → (s₁ s₂ : TVal A) → Always (Hʳ (s₁ ≐ s₂) ⇒ (f s₁ ≐ f s₂)) → Always (Hʳ (s₁ ≐ s₂) ⇒ Hʳ (f s₁ ≐ f s₂))
lem-Hʳ ne s₁ s₂ g t Heq = g t Heq , lem-H-cong ne s₁ s₂ t (snd Heq)
lem-Hʳ-cong2 : {A B C : Set} → {f : TFun (A × B) C} → NonExpansive f → (a₁ a₂ : TVal A) → (b₁ b₂ : TVal B)
→ Always (Hʳ (a₁ ≐ a₂) ⇒ Hʳ (b₁ ≐ b₂) ⇒ f (a₁ & b₁) ≐ f (a₂ & b₂))
lem-Hʳ-cong2 ne a₁ a₂ b₁ b₂ t (eqa , Heqa) (eqb , Heqb) = ne (a₁ & b₁) (a₂ & b₂) t (×-cong eqa eqb , ×-cong3 Heqa Heqb)
lem-Hʳ-cong2L : {A B C : Set} → {f : TFun (A × B) C} → NonExpansive f → (a : TVal A) → (b₁ b₂ : TVal B)
→ Always (Hʳ (b₁ ≐ b₂) ⇒ f (a & b₁) ≐ f (a & b₂))
lem-Hʳ-cong2L ne a b₁ b₂ t Heqb = lem-Hʳ-cong2 ne a a b₁ b₂ t (refl , λ _ _ → refl) Heqb
lem-Hʳ-cong2R : {A B C : Set} → {f : TFun (A × B) C} → NonExpansive f → (a₁ a₂ : TVal A) → (b : TVal B)
→ Always (Hʳ (a₁ ≐ a₂) ⇒ f (a₁ & b) ≐ f (a₂ & b))
lem-Hʳ-cong2R ne a₁ a₂ b t Heqa = lem-Hʳ-cong2 ne a₁ a₂ b b t Heqa (refl , λ _ _ → refl)