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

module OWL2.Examples.Countermodels where

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

data CounterIRI : Type₀ where
  counterDocument : CounterIRI

data CounterClass : Type₀ where
  Person Student Graduate : CounterClass

data CounterObjectProperty : Type₀ where
  knows : CounterObjectProperty

data CounterDataProperty : Type₀ where
  noDataProperty : CounterDataProperty

data CounterDatatype : Type₀ where
  noDatatype : CounterDatatype

data CounterIndividual : Type₀ where
  Alice Bob : CounterIndividual

data CounterLiteral : Type₀ where
  noLiteral : CounterLiteral

data CounterFacet : Type₀ where
  noFacet : CounterFacet

data CounterAnnotationProperty : Type₀ where
  label : CounterAnnotationProperty

CounterSignature : Signature ℓ-zero
CounterSignature .IRI =
  CounterIRI
CounterSignature .ClassName =
  CounterClass
CounterSignature .ObjectPropertyName =
  CounterObjectProperty
CounterSignature .DataPropertyName =
  CounterDataProperty
CounterSignature .DatatypeName =
  CounterDatatype
CounterSignature .IndividualName =
  CounterIndividual
CounterSignature .Literal =
  CounterLiteral
CounterSignature .FacetName =
  CounterFacet
CounterSignature .AnnotationPropertyName =
  CounterAnnotationProperty

PersonC StudentC GraduateC NotPersonC NotStudentC :
  ClassExpression CounterSignature
PersonC =
  namedClass Person
StudentC =
  namedClass Student
GraduateC =
  namedClass Graduate
NotPersonC =
  objectComplementOf PersonC
NotStudentC =
  objectComplementOf StudentC

Knows : ObjectPropertyExpression CounterSignature
Knows =
  objectProperty knows

openWorldOntology : Ontology CounterSignature
openWorldOntology =
  ontology
    (counterDocument ∷ [])
    []
    ( declaration (classEntity Person)
    ∷ declaration (objectPropertyEntity knows)
    ∷ negativeObjectPropertyAssertion Knows Alice Bob
    ∷ [] )

alicePersonOntology aliceNotPersonOntology : Ontology CounterSignature
alicePersonOntology =
  ontology [] [] (classAssertion PersonC Alice ∷ [])
aliceNotPersonOntology =
  ontology [] [] (classAssertion NotPersonC Alice ∷ [])

complementContradictionOntology : Ontology CounterSignature
complementContradictionOntology =
  ontology
    (counterDocument ∷ [])
    []
    ( declaration (classEntity Student)
    ∷ classAssertion StudentC Alice
    ∷ classAssertion NotStudentC Alice
    ∷ [] )

irreflexiveContradictionOntology : Ontology CounterSignature
irreflexiveContradictionOntology =
  ontology
    (counterDocument ∷ [])
    []
    ( declaration (objectPropertyEntity knows)
    ∷ irreflexiveObjectProperty Knows
    ∷ objectPropertyAssertion Knows Alice Alice
    ∷ [] )

disjointContradictionOntology : Ontology CounterSignature
disjointContradictionOntology =
  ontology
    (counterDocument ∷ [])
    []
    ( declaration (classEntity Student)
    ∷ declaration (classEntity Graduate)
    ∷ disjointClasses (StudentC ∷ GraduateC ∷ [])
    ∷ classAssertion StudentC Alice
    ∷ classAssertion GraduateC Alice
    ∷ [] )

data CounterObject : Type₀ where
  aliceObject bobObject : CounterObject

data CounterData : Type₀ where
  noDataValue : CounterData

CounterIndividualDenotation : CounterIndividual → CounterObject
CounterIndividualDenotation Alice =
  aliceObject
CounterIndividualDenotation Bob =
  bobObject

CounterLiteralDenotation : CounterLiteral → CounterData
CounterLiteralDenotation noLiteral =
  noDataValue

EmptyClass : CounterObject → Type₀
EmptyClass x =
  ⊥*

SparseClassDenotation : CounterClass → CounterObject → Type₀
SparseClassDenotation Person =
  EmptyClass
SparseClassDenotation Student =
  EmptyClass
SparseClassDenotation Graduate =
  EmptyClass

SparseObjectPropertyDenotation :
  CounterObjectProperty → CounterObject → CounterObject → Type₀
SparseObjectPropertyDenotation knows x y =
  ⊥*

CounterDataPropertyDenotation :
  CounterDataProperty → CounterObject → CounterData → Type₀
CounterDataPropertyDenotation noDataProperty x y =
  ⊥*

CounterDatatypeDenotation : CounterDatatype → CounterData → Type₀
CounterDatatypeDenotation noDatatype noDataValue =
  Unit*

CounterFacetDenotation :
  CounterDatatype → CounterFacet → CounterLiteral → CounterData → Type₀
CounterFacetDenotation noDatatype noFacet noLiteral noDataValue =
  Unit*

sparseInterpretation : Interpretation CounterSignature ℓ-zero ℓ-zero ℓ-zero
sparseInterpretation .ObjectDomain =
  CounterObject
sparseInterpretation .DataDomain =
  CounterData
sparseInterpretation .classDenotation =
  SparseClassDenotation
sparseInterpretation .objectPropertyDenotation =
  SparseObjectPropertyDenotation
sparseInterpretation .dataPropertyDenotation =
  CounterDataPropertyDenotation
sparseInterpretation .datatypeDenotation =
  CounterDatatypeDenotation
sparseInterpretation .facetDenotation =
  CounterFacetDenotation
sparseInterpretation .individualDenotation =
  CounterIndividualDenotation
sparseInterpretation .literalDenotation =
  CounterLiteralDenotation

data RichPerson : CounterObject → Type₀ where
  alicePerson : RichPerson aliceObject

RichClassDenotation : CounterClass → CounterObject → Type₀
RichClassDenotation Person =
  RichPerson
RichClassDenotation Student =
  EmptyClass
RichClassDenotation Graduate =
  EmptyClass

data RichKnows : CounterObject → CounterObject → Type₀ where
  bobKnowsAlice : RichKnows bobObject aliceObject

RichObjectPropertyDenotation :
  CounterObjectProperty → CounterObject → CounterObject → Type₀
RichObjectPropertyDenotation knows =
  RichKnows

richInterpretation : Interpretation CounterSignature ℓ-zero ℓ-zero ℓ-zero
richInterpretation .ObjectDomain =
  CounterObject
richInterpretation .DataDomain =
  CounterData
richInterpretation .classDenotation =
  RichClassDenotation
richInterpretation .objectPropertyDenotation =
  RichObjectPropertyDenotation
richInterpretation .dataPropertyDenotation =
  CounterDataPropertyDenotation
richInterpretation .datatypeDenotation =
  CounterDatatypeDenotation
richInterpretation .facetDenotation =
  CounterFacetDenotation
richInterpretation .individualDenotation =
  CounterIndividualDenotation
richInterpretation .literalDenotation =
  CounterLiteralDenotation

sparseAliceDoesNotKnowBob :
  SatisfiesAxiom sparseInterpretation
    (negativeObjectPropertyAssertion Knows Alice Bob)
sparseAliceDoesNotKnowBob ()

richAliceDoesNotKnowBob :
  SatisfiesAxiom richInterpretation
    (negativeObjectPropertyAssertion Knows Alice Bob)
richAliceDoesNotKnowBob ()

sparseOpenWorldModel : Model sparseInterpretation openWorldOntology
sparseOpenWorldModel =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ sparseAliceDoesNotKnowBob
    (lift tt)))

richOpenWorldModel : Model richInterpretation openWorldOntology
richOpenWorldModel =
  Prod._,_ (lift tt)
  (Prod._,_ (lift tt)
  (Prod._,_ richAliceDoesNotKnowBob
    (lift tt)))

openWorldHasMultipleModels :
  Model sparseInterpretation openWorldOntology ×
  Model richInterpretation openWorldOntology
openWorldHasMultipleModels =
  sparseOpenWorldModel , richOpenWorldModel

sparseAliceNeedNotBePerson :
  ¬ evalClass sparseInterpretation PersonC aliceObject
sparseAliceNeedNotBePerson ()

richAliceMayBePerson :
  evalClass richInterpretation PersonC aliceObject
richAliceMayBePerson =
  alicePerson

richBobMayKnowAlice :
  evalObjectProperty richInterpretation Knows bobObject aliceObject
richBobMayKnowAlice =
  bobKnowsAlice

openWorldDoesNotEntailAlicePerson :
  ¬ Entails {ℓObj = ℓ-zero} {ℓData = ℓ-zero} {ℓSem = ℓ-zero}
      openWorldOntology
      alicePersonOntology
openWorldDoesNotEntailAlicePerson entails =
  sparseAliceNeedNotBePerson
    (Prod.proj₁ (entails sparseInterpretation sparseOpenWorldModel))

openWorldDoesNotEntailAliceNotPerson :
  ¬ Entails {ℓObj = ℓ-zero} {ℓData = ℓ-zero} {ℓSem = ℓ-zero}
      openWorldOntology
      aliceNotPersonOntology
openWorldDoesNotEntailAliceNotPerson entails =
  Prod.proj₁ (entails richInterpretation richOpenWorldModel)
    richAliceMayBePerson

complementContradictionNoModel :
  ∀ {ℓObj ℓData ℓSem}
  (I : Interpretation CounterSignature ℓObj ℓData ℓSem) →
  ¬ Model I complementContradictionOntology
complementContradictionNoModel I model =
  aliceNotStudent aliceStudent
  where
  afterDeclaration =
    Prod.proj₂ model

  aliceStudent =
    Prod.proj₁ afterDeclaration

  aliceNotStudent =
    Prod.proj₁ (Prod.proj₂ afterDeclaration)

irreflexiveContradictionNoModel :
  ∀ {ℓObj ℓData ℓSem}
  (I : Interpretation CounterSignature ℓObj ℓData ℓSem) →
  ¬ Model I irreflexiveContradictionOntology
irreflexiveContradictionNoModel I model =
  knowsIrreflexive (individualDenotation I Alice) aliceKnowsSelf
  where
  afterDeclaration =
    Prod.proj₂ model

  knowsIrreflexive =
    Prod.proj₁ afterDeclaration

  aliceKnowsSelf =
    Prod.proj₁ (Prod.proj₂ afterDeclaration)

disjointContradictionNoModel :
  ∀ {ℓObj ℓData ℓSem}
  (I : Interpretation CounterSignature ℓObj ℓData ℓSem) →
  ¬ Model I disjointContradictionOntology
disjointContradictionNoModel I model =
  Prod.proj₁ (fst studentGraduateDisjoint)
    (individualDenotation I Alice)
    aliceStudent
    aliceGraduate
  where
  afterStudentDeclaration =
    Prod.proj₂ model

  afterGraduateDeclaration =
    Prod.proj₂ afterStudentDeclaration

  studentGraduateDisjoint =
    Prod.proj₁ afterGraduateDeclaration

  afterDisjoint =
    Prod.proj₂ afterGraduateDeclaration

  aliceStudent =
    Prod.proj₁ afterDisjoint

  aliceGraduate =
    Prod.proj₁ (Prod.proj₂ afterDisjoint)