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

open import NeilPrelude
open import Logic

module TemporalLogic

  (Time : Set)
  (_<'_  : Rel Time)
  (irreflex : Irreflexive _<'_)
  (transit : Transitive _<'_)

where

import StrictPreOrder
open StrictPreOrder _<'_ irreflex transit public

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

infixr   _⇒_
infixr   _∨_
infixr   _∧_

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

TPred = Time → Set
TimePred = TPred

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

-- Lifted Logical Operators

_∨_ : TPred → TPred → TPred
(φ ∨ ψ) t = φ t ⊎ ψ t

_∧_ : TPred → TPred → TPred
(φ ∧ ψ) t = φ t × ψ t

_⇒_ : TPred → TPred → TPred
(φ ⇒ ψ) t = φ t → ψ t

⊥ : TPred
⊥ t = False

⊤ : TPred
⊤ t = True

¬_ : TPred → TPred
¬ φ = φ ⇒ ⊥

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

-- Global

G : TPred → TPred
G φ t = (t' : Time) → t' > t → φ t'

-- History

H : TPred → TPred
H φ t = (t' : Time) → t' < t → φ t'

-- Future

F : TPred → TPred
F φ t = Σ Time (λ t' → t' > t × φ t')

-- Past

P : TPred → TPred
P φ t = Σ Time (λ t' → t' < t × φ t')

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

-- Between, After and Before are utility Type Synonyms

Between : Time → Time → TPred → Set
Between t₀ t₁ φ = (t : Time) → t > t₀ → t < t₁ → φ t

Between* : Time → Time → TPred → Set
Between* t₀ t₁ φ = (t : Time) → t ≥ t₀ → t ≤ t₁ → φ t

After : Time → TPred → TPred
After t₀ φ t₁ = Between t₀ t₁ φ

After* : Time → TPred → TPred
After* t₀ φ t₁ = Between* t₀ t₁ φ

Before : Time → TPred → TPred
Before t₁ φ t₀ = Between t₀ t₁ φ

Before* : Time → TPred → TPred
Before* t₁ φ t₀ = Between* t₀ t₁ φ


-- Until

_U_ : TPred → TPred → TPred
(φ U ψ) t = F (ψ ∧ After t φ) t


-- Since

private _S_ : TPred → TPred → TPred
        (φ S ψ) t = P (ψ ∧ Before t φ) t

-- I introduce a synonym as S gets used elseware a lot

_Since_ = _S_

_S*_ : TPred → TPred → TPred
(φ S* ψ) t = P (ψ ∧ Before* t φ) t

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

-- Reflexive variants (including current time)

Gʳ : TPred → TPred
Gʳ φ = φ ∧ G φ

Hʳ : TPred → TPred
Hʳ φ = φ ∧ H φ

Fʳ : TPred → TPred
Fʳ φ = φ ∨ F φ

Pʳ : TPred → TPred
Pʳ φ = φ ∨ P φ

_Uʳ_ : TPred → TPred → TPred
φ Uʳ ψ = ψ ∨ (φ ∧ (φ U ψ))

_Sʳ_ : TPred → TPred → TPred
φ Sʳ ψ = ψ ∨ (φ ∧ (φ S ψ))

-- Note we don't use the standard definition of "Weak-Until" for ease of proving properties involving it

-- _W_ : TPred → TPred → TPred
-- φ W ψ = (φ U ψ) ∨ G φ

-- _Wʳ'_ : TPred → TPred → TPred
-- φ Wʳ' ψ = (φ Uʳ ψ) ∨ Gʳ φ

-- waits-for (Weak Until)

_W_ : TPred → TPred → TPred
(φ W ψ) t = G (After t (¬ ψ) ⇒ After t φ) t

_Wʳ_ : TPred → TPred → TPred
φ Wʳ ψ = ψ ∨ (φ ∧ (φ W ψ))

-- back-to (Weak Since)

private _B_ : TPred → TPred → TPred
        φ B ψ = (φ S ψ) ∨ H φ

_Back-To_ = _B_

_Bʳ_ : TPred → TPred → TPred
φ Bʳ ψ = ψ ∨ (φ ∧ (φ B ψ))


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

-- A utility

Always : TPred → Set
Always = Π Time

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

-- Some Properties

FirstPoint : Set
FirstPoint = Always (Pʳ (H ⊥))

EndPoint : Set
EndPoint = Always (Fʳ (G ⊥))

Density : Set
Density = ∀ {φ} → Always (F φ ⇒ F (F φ))

NonBranching : Set
NonBranching = ∀ {φ} →  Always ( (P (F φ) ⇒ (P φ ∨ φ ∨ F φ))
                               ∧ (F (P φ) ⇒ (F φ ∨ φ ∨ P φ)))

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

lem-G : {φ ψ : TPred} → Always (G (φ ⇒ ψ) ⇒ G φ ⇒ G ψ)
lem-G t = S-comb₂

lemGn : {φ ψ : TPred} → Always (G (φ ⇒ ψ) ⇒ ¬ G ψ ⇒ ¬ G φ)
lemGn t φ⇒ψ = argument (lem-G t φ⇒ψ)

lem-GF : {φ ψ : TPred} → Always (G (φ ⇒ ψ) ⇒ F φ ⇒ F ψ)
lem-GF t φ⇒ψ (t' , lt , φ') = t' , lt , φ⇒ψ t' lt φ'

lem-NF⇒GN : {φ : TPred} → Always (¬ F φ ⇒ G (¬ φ))
lem-NF⇒GN t = curry2

lem-NG⇒FN : {φ : TPred} → EM → Always (¬ G φ ⇒ F (¬ φ))
lem-NG⇒FN em t = must-exist-not2 em

lem-NP⇒HN : {φ : TPred} → Always (¬ P φ ⇒ H (¬ φ))
lem-NP⇒HN t = curry2

lem-F⇒NGN : {φ : TPred} → Always (F φ ⇒ ¬ G (¬ φ))
lem-F⇒NGN t = flip uncurry2

lem-G⇒NFN : {φ : TPred} → Always (G φ ⇒ ¬ F (¬ φ))
lem-G⇒NFN t Gφ (t' , gt , nφt) = nφt (Gφ t' gt)

lem-NFN⇒G : {φ : TPred} → EM → Always (¬ F (¬ φ) ⇒ G φ)
lem-NFN⇒G em t = result2' (contradiction em) ∘ curry2

lem-NGN⇒F : {φ : TPred} → EM → Always (¬ G (¬ φ) ⇒ F φ)
lem-NGN⇒F em t = contradiction em ∘ argument curry2


-- tl-contpos : {φ ψ : TPred} → Always ((φ ⇒ ψ) ⇒ (¬ ψ ⇒ ¬ φ))
-- tl-contpos t = _⋙_

-- tl-contpos-em : {φ ψ : TPred} → EM → Always ((¬ φ ⇒ ¬ ψ) ⇒ (ψ ⇒ φ))
-- tl-contpos-em {φ} em t p ψt with em {φ t}
-- ... | inl  φt  = φt
-- ... | inr nφt = absurd (p nφt ψt)

-- tl-contr : {φ ψ : TPred} → Always (¬ (φ ∧ ¬ ψ ∧ (φ ⇒ ψ)))
-- tl-contr t (φt , nψt , p) = nψt (p φt)

-- tl-nn-antecdent : {φ ψ : TPred} → Always ((¬ ¬ φ ⇒ ψ) ⇒ (φ ⇒ ψ))
-- tl-nn-antecdent t = nn-antecedent

-- tl-nn-consequent : {φ ψ : TPred} → EM → Always ((φ ⇒ ¬ ¬ ψ) ⇒ (φ ⇒ ψ))
-- tl-nn-consequent {φ} {ψ} em t p φt with em {ψ t}
-- ... | inl ψt   = ψt
-- ... | inr nψt = absurd (p φt nψt)

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

lem-Gr : {φ : TPred} → EM → Always (¬ Gʳ φ ⇒ ¬ φ ∨ ¬ G φ)
lem-Gr {φ} em t nGrφ with em {φ t}
... | inr nφt = inl nφt
... | inl φt  = left (flip (curry nGrφ)) em

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

-- lem-GF1 : {φ : TPred} → Always (Gʳ φ ⇒ ¬ Fʳ (¬ φ))
-- lem-GF1 t (φt , Gφ) = case (applyTo φt) (lem-GF1+ t Gφ)

-- lem-GF2 : {φ : TPred} → Always (¬ ¬ Fʳ (¬ φ) ⇒ ¬ Gʳ φ)
-- lem-GF2 t = contpos (lem-GF1 t)

-- lem-GF3 : {φ : TPred} → Always (Fʳ (¬ φ) ⇒ ¬ Gʳ φ)
-- lem-GF3 t = nn-antecedent (lem-GF2 t)

lem-NGr⇒FrN : {φ : TPred} → EM → Always (¬ Gʳ φ ⇒ Fʳ (¬ φ))
lem-NGr⇒FrN em t nGrφ = right (lem-NG⇒FN em t) (lem-Gr em t nGrφ)


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

lem-Wʳ : {φ ψ : TPred} → EM → Always (Gʳ (φ ⇒ ψ) ⇒ (ψ Wʳ ¬ φ))
lem-Wʳ {φ} em t (φt⇒ψt , Gφ⇒ψ) with em {φ t}
... | inr nφt = inl nφt
... | inl φt with φt⇒ψt φt
...    | ψt = inr (ψt , λ t' gt f u gt1 gt2 → Gφ⇒ψ u gt1 (contradiction em (f u gt1 gt2)))

lem-Wʳn' : {φ ψ : TPred} → EM → Always (Gʳ (¬ φ ⇒ ¬ ψ) ⇒ (¬ ψ Wʳ ¬ ¬ φ))
lem-Wʳn' = lem-Wʳ

lem-Wʳn : {φ ψ : TPred} → EM → Always (Gʳ (¬ φ ⇒ ¬ ψ) ⇒ (¬ ψ Wʳ φ))
lem-Wʳn {φ} {ψ} em t = result (map-⊎ (contradiction em) (second (result2' (argument (result3' NotNot))))) (lem-Wʳn' {φ} {ψ} em t)


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

-- lem-Wʳ' : {φ ψ : TPred} → EM → Always (Gʳ (φ ⇒ ψ) ⇒ (ψ Wʳ' ¬ φ))
-- lem-Wʳ' {φ} {ψ} em t (φ⇒ψ , Gφ⇒ψ) with em {φ t}
-- ... | inr nφt  = inl (inl nφt)
-- ... | inl φt with em {Gʳ ψ t}
-- ...    | inl Gʳψ = inr Gʳψ
-- ...    | inr nGʳψ with φ⇒ψ φt | notBoth (inl em) nGʳψ
-- ...       | ψt | inl nψt = absurd (nψt ψt)
-- ...       | ψt | inr nGψ = {!!} -- with lem-NG⇒FN em t nGψ
-- -- ...                | (t' , gt , nψt') = inl (inr (ψt , {!!}))

{-
lem-Wʳ' {φ} em t (φt⇒ψt , Gφ⇒ψ) with em {φ t}
... | inr nφt = inl nφt
... | inl φt with φt⇒ψt φt
...    | ψt = inr (ψt , λ t' gt f u gt1 gt2 → Gφ⇒ψ u gt1 (contradiction em (f u gt1 gt2)))
-}

-- The below was the (flawed) proof using the old "Weak-Until" operator.  It relied on a property of time that isn't true
-- when time is dense

-- postulate lem-1stpoint : {φ : TPred} → (t : Time) → (φ ∧ F (¬ φ) ⇒ F (¬ φ ∧ Since t φ)) t

-- lem-Wʳ : {φ ψ : TPred} → EM → Always (Gʳ (φ ⇒ ψ) ⇒ (ψ Wʳ ¬ φ))
-- lem-Wʳ {φ} {ψ} em t (φt⇒ψt , Gφ⇒ψ) with em {φ t}
-- ... | inr nφt = inl (inl nφt)
-- ... | inl φt with φt⇒ψt φt
-- ...    | ψt with em {F (¬ φ) t}
-- ...       | inl Fnφ  = inl (inr (ψt , fourth (λ g u lt1 → Gφ⇒ψ u lt1 ∘ g u lt1) (lem-1stpoint t (φt , Fnφ)))) 
-- ...       | inr nFnφ = inr (ψt , (lem-G t Gφ⇒ψ (lem-NFN⇒G em t nFnφ)))

-- lem-Wʳn' : {φ ψ : TPred} → EM → Always (Gʳ (¬ φ ⇒ ¬ ψ) ⇒ (¬ ψ Wʳ ¬ ¬ φ))
-- lem-Wʳn' = lem-Wʳ

-- lem-Wʳn : {φ ψ : TPred} → EM → Always (Gʳ (¬ φ ⇒ ¬ ψ) ⇒ (¬ ψ Wʳ φ))
-- lem-Wʳn {φ} {ψ} em t = result (left (map-⊎ (contradiction em) (fourth (first (contradiction em))))) (lem-Wʳn' {φ} {ψ} em t)

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