OWL2.DirectSemantics.Entailment

{-# OPTIONS --safe --cubical #-}

module OWL2.DirectSemantics.Entailment where

open import OWL2.Prelude
import Cubical.Data.Prod.Base as Prod
open import OWL2.Syntax
open import OWL2.DirectSemantics

infix 4 _∈_

data _∈_ {ℓA : Level} {A : Type ℓA} (x : A) : List A → Type ℓA where
  here :
    ∀ {xs} →
    x ∈ (x ∷ xs)
  there :
    ∀ {y xs} →
    x ∈ xs → x ∈ (y ∷ xs)

allListLookup :
  ∀ {ℓA ℓP} {A : Type ℓA}
    {P : A → Type ℓP}
    {x : A} {xs : List A} →
  x ∈ xs → AllList xs P → P x
allListLookup here pxs =
  Prod.proj₁ pxs
allListLookup {P = P} {x = x} (there {xs = xs} x∈xs) pxs =
  allListLookup {P = P} {x = x} {xs = xs} x∈xs (Prod.proj₂ pxs)

allListHead :
  ∀ {ℓA ℓP} {A : Type ℓA}
    {P : A → Type ℓP}
    {x : A} {xs : List A} →
  AllList (x ∷ xs) P → P x
allListHead =
  Prod.proj₁

allListTail :
  ∀ {ℓA ℓP} {A : Type ℓA}
    {P : A → Type ℓP}
    {x : A} {xs : List A} →
  AllList (x ∷ xs) P → AllList xs P
allListTail =
  Prod.proj₂

allListMap :
  ∀ {ℓA ℓP ℓQ} {A : Type ℓA}
    {P : A → Type ℓP}
    {Q : A → Type ℓQ}
    {xs : List A} →
  (∀ x → P x → Q x) →
  AllList xs P → AllList xs Q
allListMap {ℓA = ℓA} {ℓQ = ℓQ} {xs = []} P⊆Q _ =
  lift {ℓ' = ℓ-max ℓA ℓQ} tt
allListMap {P = P} {Q = Q} {xs = x ∷ xs} P⊆Q pxs =
  Prod._,_
    (P⊆Q x (Prod.proj₁ pxs))
    (allListMap {P = P} {Q = Q} {xs = xs} P⊆Q (Prod.proj₂ pxs))

allListAppendIntro :
  ∀ {ℓA ℓP} {A : Type ℓA}
    {P : A → Type ℓP}
    {xs ys : List A} →
  AllList xs P →
  AllList ys P →
  AllList (xs ++ ys) P
allListAppendIntro {xs = []} _ pys =
  pys
allListAppendIntro {P = P} {xs = x ∷ xs} {ys = ys} pxs pys =
  Prod._,_
    (Prod.proj₁ pxs)
    (allListAppendIntro {P = P} {xs = xs} {ys = ys} (Prod.proj₂ pxs) pys)

allListAppendLeft :
  ∀ {ℓA ℓP} {A : Type ℓA}
    {P : A → Type ℓP}
    {xs ys : List A} →
  AllList (xs ++ ys) P →
  AllList xs P
allListAppendLeft {ℓA = ℓA} {ℓP = ℓP} {xs = []} _ =
  lift {ℓ' = ℓ-max ℓA ℓP} tt
allListAppendLeft {P = P} {xs = x ∷ xs} {ys = ys} pxs++ys =
  Prod._,_
    (Prod.proj₁ pxs++ys)
    (allListAppendLeft {P = P} {xs = xs} {ys = ys} (Prod.proj₂ pxs++ys))

allListAppendRight :
  ∀ {ℓA ℓP} {A : Type ℓA}
    {P : A → Type ℓP}
    {xs ys : List A} →
  AllList (xs ++ ys) P →
  AllList ys P
allListAppendRight {xs = []} pxs++ys =
  pxs++ys
allListAppendRight {P = P} {xs = x ∷ xs} {ys = ys} pxs++ys =
  allListAppendRight {P = P} {xs = xs} {ys = ys} (Prod.proj₂ pxs++ys)

allListAppendSplit :
  ∀ {ℓA ℓP} {A : Type ℓA}
    {P : A → Type ℓP}
    {xs ys : List A} →
  AllList (xs ++ ys) P →
  AllList xs P × AllList ys P
allListAppendSplit {P = P} {xs = xs} {ys = ys} pxs++ys =
  allListAppendLeft {P = P} {xs = xs} {ys = ys} pxs++ys ,
  allListAppendRight {P = P} {xs = xs} {ys = ys} pxs++ys

appendOntology :
  ∀ {ℓSig} {Sig : Signature ℓSig} →
  Ontology Sig → Ontology Sig → Ontology Sig
appendOntology O₁ O₂ =
  ontology
    (ontologyIRI O₁ ++ ontologyIRI O₂)
    (imports O₁ ++ imports O₂)
    (axioms O₁ ++ axioms O₂)

axiomOntology :
  ∀ {ℓSig} {Sig : Signature ℓSig} →
  Axiom Sig → Ontology Sig
axiomOntology ax =
  ontology [] [] (ax ∷ [])

satisfiesOntologyAxioms :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {O : Ontology Sig} →
  SatisfiesOntology I O →
  AllList (axioms O) (SatisfiesAxiom I)
satisfiesOntologyAxioms model =
  model

satisfiesOntologyFromAxioms :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {O : Ontology Sig} →
  AllList (axioms O) (SatisfiesAxiom I) →
  SatisfiesOntology I O
satisfiesOntologyFromAxioms axiomsSatisfied =
  axiomsSatisfied

satisfiesOntologyAxiom :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {O : Ontology Sig}
    {ax : Axiom Sig} →
  ax ∈ axioms O →
  SatisfiesOntology I O →
  SatisfiesAxiom I ax
satisfiesOntologyAxiom {O = O} {ax = ax} ax∈O model =
  allListLookup {x = ax} {xs = axioms O} ax∈O model

satisfiesOntologyHead :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {iri imports : List (IRI Sig)}
    {ax : Axiom Sig}
    {axs : List (Axiom Sig)} →
  SatisfiesOntology I (ontology iri imports (ax ∷ axs)) →
  SatisfiesAxiom I ax
satisfiesOntologyHead {I = I} {ax = ax} {axs = axs} =
  allListHead {P = SatisfiesAxiom I} {x = ax} {xs = axs}

satisfiesOntologyTail :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {iri imports : List (IRI Sig)}
    {ax : Axiom Sig}
    {axs : List (Axiom Sig)} →
  SatisfiesOntology I (ontology iri imports (ax ∷ axs)) →
  AllList axs (SatisfiesAxiom I)
satisfiesOntologyTail {I = I} {ax = ax} {axs = axs} =
  allListTail {P = SatisfiesAxiom I} {x = ax} {xs = axs}

satisfiesOntologyMapAxioms :
  ∀ {ℓSig ℓObj ℓData ℓSem ℓP}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {O : Ontology Sig}
    {P : Axiom Sig → Type ℓP} →
  (∀ ax → SatisfiesAxiom I ax → P ax) →
  SatisfiesOntology I O →
  AllList (axioms O) P
satisfiesOntologyMapAxioms {I = I} {O = O} {P = P} f model =
  allListMap {P = SatisfiesAxiom I} {Q = P} {xs = axioms O} f model

satisfiesOntologyAppendIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {O₁ O₂ : Ontology Sig} →
  SatisfiesOntology I O₁ →
  SatisfiesOntology I O₂ →
  SatisfiesOntology I (appendOntology O₁ O₂)
satisfiesOntologyAppendIntro {I = I} {O₁ = O₁} {O₂ = O₂} model₁ model₂ =
  allListAppendIntro
    {P = SatisfiesAxiom I}
    {xs = axioms O₁}
    {ys = axioms O₂}
    model₁
    model₂

satisfiesOntologyAppendLeft :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {O₁ O₂ : Ontology Sig} →
  SatisfiesOntology I (appendOntology O₁ O₂) →
  SatisfiesOntology I O₁
satisfiesOntologyAppendLeft {I = I} {O₁ = O₁} {O₂ = O₂} model =
  allListAppendLeft
    {P = SatisfiesAxiom I}
    {xs = axioms O₁}
    {ys = axioms O₂}
    model

satisfiesOntologyAppendRight :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {O₁ O₂ : Ontology Sig} →
  SatisfiesOntology I (appendOntology O₁ O₂) →
  SatisfiesOntology I O₂
satisfiesOntologyAppendRight {I = I} {O₁ = O₁} {O₂ = O₂} model =
  allListAppendRight
    {P = SatisfiesAxiom I}
    {xs = axioms O₁}
    {ys = axioms O₂}
    model

satisfiesOntologyAppendSplit :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {O₁ O₂ : Ontology Sig} →
  SatisfiesOntology I (appendOntology O₁ O₂) →
  SatisfiesOntology I O₁ × SatisfiesOntology I O₂
satisfiesOntologyAppendSplit {I = I} {O₁ = O₁} {O₂ = O₂} model =
  satisfiesOntologyAppendLeft {I = I} {O₁ = O₁} {O₂ = O₂} model ,
  satisfiesOntologyAppendRight {I = I} {O₁ = O₁} {O₂ = O₂} model

entailsRefl :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O : Ontology Sig} →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O O
entailsRefl I model =
  model

entailsTrans :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O₁ O₂ O₃ : Ontology Sig} →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O₁ O₂ →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O₂ O₃ →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O₁ O₃
entailsTrans O₁⊨O₂ O₂⊨O₃ I model =
  O₂⊨O₃ I (O₁⊨O₂ I model)

entailsAppendLeft :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O₁ O₂ : Ontology Sig} →
  Entails
    {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem}
    (appendOntology O₁ O₂)
    O₁
entailsAppendLeft {O₁ = O₁} {O₂ = O₂} I model =
  satisfiesOntologyAppendLeft {O₁ = O₁} {O₂ = O₂} model

entailsAppendRight :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O₁ O₂ : Ontology Sig} →
  Entails
    {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem}
    (appendOntology O₁ O₂)
    O₂
entailsAppendRight {O₁ = O₁} {O₂ = O₂} I model =
  satisfiesOntologyAppendRight {O₁ = O₁} {O₂ = O₂} model

entailsAppendIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O O₁ O₂ : Ontology Sig} →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O O₁ →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O O₂ →
  Entails
    {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem}
    O
    (appendOntology O₁ O₂)
entailsAppendIntro {O₁ = O₁} {O₂ = O₂} O⊨O₁ O⊨O₂ I model =
  satisfiesOntologyAppendIntro
    {O₁ = O₁}
    {O₂ = O₂}
    (O⊨O₁ I model)
    (O⊨O₂ I model)

entailsWeakeningLeft :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O₁ O₂ O : Ontology Sig} →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O₁ O₂ →
  Entails
    {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem}
    (appendOntology O₁ O)
    O₂
entailsWeakeningLeft {O₁ = O₁} {O = O} O₁⊨O₂ I model =
  O₁⊨O₂ I (satisfiesOntologyAppendLeft {O₁ = O₁} {O₂ = O} model)

entailsWeakeningRight :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O₁ O₂ O : Ontology Sig} →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O₁ O₂ →
  Entails
    {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem}
    (appendOntology O O₁)
    O₂
entailsWeakeningRight {O₁ = O₁} {O = O} O₁⊨O₂ I model =
  O₁⊨O₂ I (satisfiesOntologyAppendRight {O₁ = O} {O₂ = O₁} model)

entailsAppendMonotone :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O₁ O₂ O₃ O₄ : Ontology Sig} →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O₁ O₂ →
  Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O₃ O₄ →
  Entails
    {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem}
    (appendOntology O₁ O₃)
    (appendOntology O₂ O₄)
entailsAppendMonotone {O₁ = O₁} {O₂ = O₂} {O₃ = O₃} {O₄ = O₄}
  O₁⊨O₂ O₃⊨O₄ I model =
  satisfiesOntologyAppendIntro
    {I = I}
    {O₁ = O₂}
    {O₂ = O₄}
    (O₁⊨O₂ I (satisfiesOntologyAppendLeft {I = I} {O₁ = O₁} {O₂ = O₃} model))
    (O₃⊨O₄ I (satisfiesOntologyAppendRight {I = I} {O₁ = O₁} {O₂ = O₃} model))

entailsAxiom :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O : Ontology Sig}
    {ax : Axiom Sig} →
  ((I : Interpretation Sig ℓObj ℓData ℓSem) →
    Model I O → SatisfiesAxiom I ax) →
  Entails
    {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem}
    O
    (axiomOntology ax)
entailsAxiom
  {ℓSig = ℓSig} {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem}
  axSatisfied I model =
  Prod._,_
    (axSatisfied I model)
    (lift {ℓ' = ℓ-max ℓSig (SemLevel ℓSig ℓObj ℓData ℓSem)} tt)

entailsOntologyAxiom :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {O : Ontology Sig}
    {ax : Axiom Sig} →
  ax ∈ axioms O →
  Entails
    {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem}
    O
    (axiomOntology ax)
entailsOntologyAxiom {O = O} {ax = ax} ax∈O =
  entailsAxiom
    {O = O}
    {ax = ax}
    (λ I model → satisfiesOntologyAxiom {O = O} {ax = ax} ax∈O model)