{- THE COINDUCTIVE FORMULATION OF COMMON KNOWLEDGE -}
{-   by Colm Baston and Venanzio Capretta          -}

module Common-Knowledge (State : Set) where

open import Level hiding (_⊔_) renaming (suc to lsuc ; zero to lzero)
open import Data.Empty
open import Data.Bool    hiding   (_∨_ ;  _∧_)
open import Data.Sum     renaming (_⊎_ to _∨_)
open import Data.Product renaming (_×_ to _∧_)
open import Relation.Nullary
open import Relation.Binary
open import Function

open IsEquivalence {{...}}

postulate
  ¬¬-elim : ∀ {α} {P : Set α} → ¬ (¬ P) → P

{- Events and Event Operations -}

Event : Set₁
Event = State → Set

_⊓_ : Event → Event → Event
e₁ ⊓ e₂ = λ w → e₁ w ∧ e₂ w

_⊔_ : Event → Event → Event
e₁ ⊔ e₂ = λ w → e₁ w ∨ e₂ w

_⊏_ : Event → Event → Event
e₁ ⊏ e₂ = λ w → e₁ w → e₂ w

~_ : Event → Event
~ e = λ w → ¬ e w

infix  15 ~_
infixr 14 _⊓_
infixr 13 _⊔_
infixr 12 _⊏_

{- Logical Statements About Events and Event Families -}

_⊂_ : Event → Event → Set
e₁ ⊂ e₂ = ∀ {w} → e₁ w → e₂ w

_≡_ : Event → Event → Set
e₁ ≡ e₂ = (e₁ ⊂ e₂) ∧ (e₂ ⊂ e₁)

_⊂ᶠ_ : ∀ {α} {X : Set α} → (X → Event) → Event → Set α
E ⊂ᶠ e = ∀ {w} → (∀ x → E x w) → e w


all_ : Event → Set
all e = ∀ {w} → e w

infixr 11 _⊂_
infixr 11 _⊂ᶠ_
infixr 10 _≡_

{- Knowledge Operator Properties -}

record KOp {α} (K : Event → Event) : Set (lsuc α) where
  field
    preserves-⊂ : ∀ {X : Set α} {E : X → Event} {e : Event} → (∀ {w} → (∀ x → E x w) → e w) → (K ∘ E) ⊂ᶠ K e
    axiomT : ∀ {e} → K e ⊂ e
    axiom4 : ∀ {e} → K e ⊂ K (K e)
    axiom5 : ∀ {e} → ~ K e ⊂ K (~ K e)

open KOp {{...}}

{- Knowledge Generalisation and Axiom K Follow from Preservation of Semantic Entailment -}

𝟘-fam : ⊥ → Event
𝟘-fam ()

generalisation : ∀ {K} {{_ : KOp K}} {e : Event} → all e → all K e
generalisation ae = preserves-⊂ {E = 𝟘-fam} (λ _ → ae) (λ ())

𝟚-fam : Event → Event → Bool → Event
𝟚-fam e₁ e₂ = λ {false → e₁ ⊏ e₂ ; true → e₁}

axiomK : ∀ {K} {{_ : KOp K}} {e₁ e₂} → K (e₁ ⊏ e₂) ⊂ K e₁ ⊏ K e₂
axiomK {_} {e₁} {e₂} f x = preserves-⊂ {E = 𝟚-fam e₁ e₂} (λ g → g false (g true)) (λ {false → f ; true → x})

{- Transformations Between Knowledge Operators and Equivalence Relations -}

K[_] : ∀ {α β} → Rel State α → (State → Set β) → State → Set _
K[ _R_ ] = λ e w → ∀ {v} → w R v → e v

R[_] : ∀ {α β} → ((State → Set α) → State → Set β) → Rel State _
R[ K ] = λ w v → ∀ {e} → K e w → K e v

instance
  EqRel-KOp : ∀ {α R} → {{_ : IsEquivalence R}} → KOp {α} K[ R ]
  EqRel-KOp = record { preserves-⊂ = λ Ee Hx wRv → Ee (λ x → Hx x wRv)                         ;
                       axiomT      = λ k → k refl                                              ;
                       axiom4      = λ k wRv vRu → k (trans wRv vRu)                           ;
                       axiom5      = λ f wRv k → f ((λ vRw → k ∘ trans vRw) (sym wRv)) }

  KOp-EqRel : ∀ {α K} → {{_ : KOp {α} K}} → IsEquivalence R[ K ]
  KOp-EqRel = record { refl  = id                                                            ;
                       sym   = λ wRv Kev → ¬¬-elim (flip axiomT Kev ∘ wRv ∘ axiom5) ;
                       trans = λ wRv vRu → vRu ∘ wRv                                         }

{- These Transformations Form an Isomorphism -}

R-iso₁ : ∀ {α _R_ w v} {{_ : IsEquivalence _R_}} → w R v → R[ K[ _R_ ] ] w v
R-iso₁ {α} wRv Kew vRu = axiom4 {{EqRel-KOp {α}}} Kew (trans wRv vRu) refl

R-iso₂ : ∀ {α} {_R_ : Rel State α} {w v} {{_ : IsEquivalence _R_}} → R[ K[ _R_ ] ] w v → w R v
R-iso₂ {_} {R} {w} wRv = wRv {R w} id refl

K-iso₁ : ∀ {α K e w} {{_ : KOp {α} K}} → K e w → K[ R[ K ] ] e w
K-iso₁ Kew wRv = axiomT (wRv Kew)

K-fam : (K : Event → Event) (w : State) → Σ Event (λ e → K e w) → Event
K-fam K w (e , _) = K e

KRK-K-fam : ∀ {α K e w} {{_ : KOp {α} K}} → K[ R[ K ] ] e w → K-fam K w ⊂ᶠ e
KRK-K-fam Kew h = Kew (λ {e} Kew' → h (e , Kew'))

K-iso₂ : ∀ {K e w} {{_ : KOp {lsuc lzero} K}} → K[ R[ K ] ] e w → K e w
K-iso₂ {K} {e} {w} Kew = preserves-⊂ {E = K-fam K w} (KRK-K-fam Kew) (λ {(_ , h) → axiom4 h})

{- Relational Semantics for Epistemic Logic -}

module Relational
  (Agent : Set)
  (an-agent : Agent)
  (≃ : Agent → Rel State lzero)
  (≃-EqRel : ∀ {a} → IsEquivalence (≃ a)) where

  instance
    _ : ∀ {a} → IsEquivalence (≃ a)
    _ = ≃-EqRel

  K : Agent → Event → Event
  K a = K[ ≃ a ]

  EK : Event → Event
  EK e w = ∀ {a} → K a e w

  data _∝_ : State → State → Set where
    ∝-union : ∀ {a w v} → (≃ a) w v → w ∝ v
    ∝-trans : ∀ {w v u} → w ∝ v → v ∝ u → w ∝ u

  ∝-refl : ∀ {w} → w ∝ w
  ∝-refl = ∝-union {an-agent} refl

  ∝-sym : ∀ {w v} → w ∝ v → v ∝ w
  ∝-sym (∝-union  w≃v)    = ∝-union (sym w≃v)
  ∝-sym (∝-trans w∝v v∝u) = ∝-trans (∝-sym v∝u) (∝-sym w∝v)

  instance
    ∝-EqRel : IsEquivalence _∝_
    ∝-EqRel = record { refl  = ∝-refl  ;
                       sym   = ∝-sym   ;
                       trans = ∝-trans }

  rCK : Event → Event
  rCK = K[ _∝_ ]

  rCK-EK : ∀ {e} → rCK e ⊂ EK e
  rCK-EK r w≃v = r (∝-union w≃v)

  rCK-rCKEK : ∀ {e} → rCK e ⊂ rCK (EK e)
  rCK-rCKEK r w∝v v≃u = r (∝-trans w∝v (∝-union v≃u))

{- Coinductive Definition of Common Knowledge -}

  record cCK (e : Event) (w : State) : Set where
    coinductive
    constructor cCK-intro
    field
      cCK-EK    : EK e w
      cCK-cCKEK : cCK (EK e) w

  open cCK

  cCK-EKcCK : ∀ {e} → cCK e ⊂ EK (cCK e)
  cCK-EK    (cCK-EKcCK c w≃v) = cCK-EK    (cCK-cCKEK c) w≃v
  cCK-cCKEK (cCK-EKcCK c w≃v) = cCK-EKcCK (cCK-cCKEK c) w≃v

  cCK-transport : ∀ {α e w v} → cCK e w → w ∝ v → cCK e v
  cCK-transport {α} c (∝-union w≃v)     = axiomT {{EqRel-KOp {α}}} (axiom4 {{EqRel-KOp {α}}} (cCK-EKcCK c) w≃v)
  cCK-transport {α} c (∝-trans w∝v v∝u) = cCK-transport {α} (cCK-transport {α} c w∝v) v∝u

{- Equivalence of Relational and Coinductive Common Knowledge -}

  rCK-cCK : ∀ {e} → rCK e ⊂ cCK e
  cCK-EK    (rCK-cCK r) = rCK-EK r
  cCK-cCKEK (rCK-cCK r) = rCK-cCK (rCK-rCKEK r)

  cCK-rCK : ∀ {α e} → cCK e ⊂ rCK e
  cCK-rCK {α} c w∝v = axiomT {{EqRel-KOp {α}}} (cCK-EK (cCK-transport {α} c w∝v) {an-agent})

  rCK-cCK-equiv : ∀ {α e} → rCK e ≡ cCK e
  rCK-cCK-equiv {α} = rCK-cCK , cCK-rCK {α}

{- cCK is a Knowledge Operator -}

  cCK-KOp : ∀ {α} → KOp {α} cCK
  cCK-KOp {α} = record { preserves-⊂ = λ Ee Hx → rCK-cCK (preserves-⊂ {{EqRel-KOp}} Ee (cCK-rCK {α} ∘ Hx))                                     ;
                         axiomT      = λ c → axiomT {{EqRel-KOp {α}}} (cCK-rCK {α} c)                                                          ;
                         axiom4      = λ c → rCK-cCK (λ w∝v → rCK-cCK (λ v∝u → axiom4 {{EqRel-KOp {α}}} (cCK-rCK {α} c) (trans w∝v v∝u) refl)) ;
                         axiom5      = λ nc → rCK-cCK (λ w∝v c → nc (cCK-transport {α} c (sym w∝v)))                                           }