-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Basic Kripke-style semantics with abstract worlds, for soundness only.
-- Ewald-style conditions.

module A201607.BasicIS4.Semantics.BasicKripkeEwald where

open import A201607.BasicIS4.Syntax.Common public


-- Intuitionistic modal Kripke models, with frame conditions given by Ewald, Servi, and Plotkin-Stirling.

record Model : Set₁ where
  infix 3 _⊩ᵅ_
  field
    World : Set

    -- Intuitionistic accessibility; preorder.
    _≤_    : World  World  Set
    refl≤  :  {w}  w  w
    trans≤ :  {w w′ w″}  w  w′  w′  w″  w  w″

    -- Modal accessibility; preorder.
    _R_    : World  World  Set
    reflR  :  {w}  w R w
    transR :  {w w′ w″}  w R w′  w′ R w″  w R w″

    -- Forcing for atomic propositions; monotonic.
    _⊩ᵅ_   : World  Atom  Set
    mono⊩ᵅ :  {P w w′}  w  w′  w ⊩ᵅ P  w′ ⊩ᵅ P


  -- Composition of accessibility.

  _≤⨾R_ : World  World  Set
  _≤⨾R_ = _≤_  _R_

  _R⨾≤_ : World  World  Set
  _R⨾≤_ = _R_  _≤_

  _≤⊓R_ : World  World  Set
  _≤⊓R_ = _≤_  _R_

  _≤⊔R_ : World  World  Set
  _≤⊔R_ = _≤_  _R_


  -- Infimum-to-supremum condition.
  --
  --   w′          →   w′      v′
  --   ●           →   ●───R───◌
  --   │           →           │
  --   ≤  ξ,ζ      →           ≤
  --   │           →           │
  --   ◌───R───●   →           ●
  --   w       v   →           v

  field
    ≤⊓R→≤⊔R :  {v w′}  w′ ≤⊓R v  v ≤⊔R w′


  -- Minor brilliance condition.
  --
  --           v′  →   w′      v′
  --           ●   →   ◌───R───●
  --           │   →   │
  --      ζ,ξ  ≤   →   ≤
  --           │   →   │
  --   ●───R───◌   →   ●
  --   w       v   →   w
  --
  --           v′      w″  →   v″              w″
  --           ◌───R───●   →   ◌───────R───────●
  --           │           →   │
  --           ≤  ξ′,ζ′    →   │
  --   v       │           →   │
  --   ◌───R───●           →   ≤
  --   │       w′          →   │
  --   ≤  ξ,ζ              →   │
  --   │                   →   │
  --   ●                   →   ●
  --   w                   →   w

  field
    R⨾≤→≤⨾R :  {w v′}  w R⨾≤ v′  w ≤⨾R v′

  refl≤⨾R :  {w}  w ≤⨾R w
  refl≤⨾R {w} = w , (refl≤ , reflR)

  trans≤⨾R :  {w′ w w″}  w ≤⨾R w′  w′ ≤⨾R w″  w ≤⨾R w″
  trans≤⨾R {w′} (v , (ξ , ζ)) (v′ , (ξ′ , ζ′)) = let v″ , (ξ″ , ζ″) = R⨾≤→≤⨾R (w′ , (ζ , ξ′))
                                                 in  v″ , (trans≤ ξ ξ″ , transR ζ″ ζ′)

open Model {{…}} public


-- Forcing in a particular world of a particular model.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : World  Ty  Set
  w  α P   = w ⊩ᵅ P
  w  A  B =  {w′ : World}  w  w′  w′  A  w′  B
  w   A   =  {w′ : World}  w  w′   {v′}  w′ R v′  v′  A
  w  A  B = w  A × w  B
  w      = 𝟙

  infix 3 _⊩⋆_
  _⊩⋆_ : World  Cx Ty  Set
  w ⊩⋆      = 𝟙
  w ⊩⋆ Ξ , A = w ⊩⋆ Ξ × w  A


-- Monotonicity with respect to intuitionistic accessibility.

module _ {{_ : Model}} where
  mono⊩ :  {A} {w w′ : World}  w  w′  w  A  w′  A
  mono⊩ {α P}   ξ s = mono⊩ᵅ ξ s
  mono⊩ {A  B} ξ s = λ ξ′ a  s (trans≤ ξ ξ′) a
  mono⊩ { A}   ξ s = λ ξ′ ζ  s (trans≤ ξ ξ′) ζ
  mono⊩ {A  B} ξ s = mono⊩ {A} ξ (π₁ s) , mono⊩ {B} ξ (π₂ s)
  mono⊩ {}    ξ s = 

  mono⊩⋆ :  {Γ} {w w′ : World}  w  w′  w ⊩⋆ Γ  w′ ⊩⋆ Γ
  mono⊩⋆ {}     ξ        = 
  mono⊩⋆ {Γ , A} ξ (γ , a) = mono⊩⋆ {Γ} ξ γ , mono⊩ {A} ξ a


-- Additional useful equipment.

module _ {{_ : Model}} where
  _⟪$⟫_ :  {A B} {w : World}  w  A  B  w  A  w  B
  s ⟪$⟫ a = s refl≤ a

  ⟪K⟫ :  {A B} {w : World}  w  A  w  B  A
  ⟪K⟫ {A} a ξ = K (mono⊩ {A} ξ a)

  ⟪S⟫ :  {A B C} {w : World}  w  A  B  C  w  A  B  w  A  w  C
  ⟪S⟫ {A} {B} {C} s₁ s₂ a = _⟪$⟫_ {B} {C} (_⟪$⟫_ {A} {B  C} s₁ a) (_⟪$⟫_ {A} {B} s₂ a)

  ⟪S⟫′ :  {A B C} {w : World}  w  A  B  C  w  (A  B)  A  C
  ⟪S⟫′ {A} {B} {C} s₁ ξ s₂ ξ′ a = let s₁′ = mono⊩ {A  B  C} (trans≤ ξ ξ′) s₁
                                      s₂′ = mono⊩ {A  B} ξ′ s₂
                                  in  ⟪S⟫ {A} {B} {C} s₁′ s₂′ a

  _⟪D⟫_ :  {A B} {w : World}  w   (A  B)  w   A  w   B
  _⟪D⟫_ {A} {B} s₁ s₂ ξ ζ = let s₁′ = s₁ ξ ζ
                                s₂′ = s₂ ξ ζ
                            in  _⟪$⟫_ {A} {B} s₁′ s₂′

  _⟪D⟫′_ :  {A B} {w : World}  w   (A  B)  w   A   B
  _⟪D⟫′_ {A} {B} s₁ ξ = _⟪D⟫_ {A} {B} (mono⊩ { (A  B)} ξ s₁)

  ⟪↑⟫ :  {A} {w : World}  w   A  w    A
  ⟪↑⟫ s ξ ζ ξ′ ζ′ = let _ , (ξ″ , ζ″) = trans≤⨾R (_ , (ξ , ζ)) (_ , (ξ′ , ζ′))
                    in  s ξ″ ζ″

  ⟪↓⟫ :  {A} {w : World}  w   A  w  A
  ⟪↓⟫ s = s refl≤ reflR

  _⟪,⟫′_ :  {A B} {w : World}  w  A  w  B  A  B
  _⟪,⟫′_ {A} {B} a ξ = _,_ (mono⊩ {A} ξ a)


-- Forcing in a particular world of a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 _⊩_⇒_
  _⊩_⇒_ : World  Cx Ty  Ty  Set
  w  Γ  A = w ⊩⋆ Γ  w  A

  infix 3 _⊩_⇒⋆_
  _⊩_⇒⋆_ : World  Cx Ty  Cx Ty  Set
  w  Γ ⇒⋆ Ξ = w ⊩⋆ Γ  w ⊩⋆ Ξ


-- Entailment, or forcing in all worlds of all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx Ty  Ty  Set₁
Γ  A =  {{_ : Model}} {w : World}  w  Γ  A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty  Cx Ty  Set₁
Γ ⊨⋆ Ξ =  {{_ : Model}} {w : World}  w  Γ ⇒⋆ Ξ

infix 3 _⁏_⊨_
_⁏_⊨_ : Cx Ty  Cx Ty  Ty  Set₁
Γ  Δ  A =  {{_ : Model}} {w : World}
              w ⊩⋆ Γ  (∀ {w′ : World}  w  w′   {v′ : World}  w′ R v′  v′ ⊩⋆ Δ)  w  A


-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup :  {A Γ} {w : World}  A  Γ  w  Γ  A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ