-- Basic intuitionistic propositional calculus, without ∨ or ⊥.
-- Kripke-style semantics with abstract worlds.
-- McKinsey-Tarski embedding.

module A201607.BasicIPC.Semantics.KripkeMcKinseyTarski where

open import A201607.BasicIPC.Syntax.Common public


-- Intuitionistic Kripke models.

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″

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

open Model {{…}} public


-- Forcing in a particular world of a particular model, based on the McKinsey-Tarski embedding of IPC in S4.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : World  Ty  Set
  w  α P   = w ⊩ᵅ P
  w  A  B =  {w′}  w  w′  w′  A  w′  B
  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  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

  _⟪,⟫′_ :  {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  Γ ⇒⋆ Ξ


-- 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 γ

  ⟦λ⟧ :  {A B Γ} {w : World}  (∀ {w′ : World}  w′  Γ , A  B)  w  Γ  A  B
  ⟦λ⟧ s γ = λ ξ a  s (mono⊩⋆ ξ γ , a)

  _⟦$⟧_ :  {A B Γ} {w : World}  w  Γ  A  B  w  Γ  A  w  Γ  B
  _⟦$⟧_ {A} {B} s₁ s₂ γ = _⟪$⟫_ {A} {B} (s₁ γ) (s₂ γ)

  ⟦K⟧ :  {A B Γ} {w : World}  w  Γ  A  w  Γ  B  A
  ⟦K⟧ {A} {B} a γ = ⟪K⟫ {A} {B} (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 γ = ⟪S⟫ {A} {B} {C} (s₁ γ) (s₂ γ) (a γ)

  _⟦,⟧_ :  {A B Γ} {w : World}  w  Γ  A  w  Γ  B  w  Γ  A  B
  _⟦,⟧_ {A} {B} a b γ = _,_ (a γ) (b γ)

  ⟦π₁⟧ :  {A B Γ} {w : World}  w  Γ  A  B  w  Γ  A
  ⟦π₁⟧ s γ = π₁ (s γ)

  ⟦π₂⟧ :  {A B Γ} {w : World}  w  Γ  A  B  w  Γ  B
  ⟦π₂⟧ s γ = π₂ (s γ)