-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Basic Kripke-style semantics with abstract worlds, for soundness only.
-- Božić-Došen-style conditions.

module A201607.BasicIS4.Semantics.BasicKripkeBozicDosen where

open import A201607.BasicIS4.Syntax.Common public


-- Intuitionistic modal Kripke models, with frame conditions given by Božić-Došen.

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_  _≤_


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

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

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

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

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′}  w  w′  w′  A  w′  B
  w   A   =  {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 = λ ζ  let v , (ζ′ , ξ′) = ≤⨾R→R⨾≤ (_ , (ξ , ζ))
                              in  mono⊩ {A} ξ′ (s ζ′)
  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 ζ ζ′ = s (transR ζ ζ′)

  ⟪↓⟫ :  {A} {w : World}  w   A  w  A
  ⟪↓⟫ s = s 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 ⊩⋆ Γ  (∀ {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 γ