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

module OWL2.Examples.Portable.Regularity where

open import OWL2.Prelude
import OWL2.Check.Result as CheckResult
import OWL2.Data.String as String
import OWL2.Portable.Check.Regularity as RegCheck
import OWL2.Portable.Regularity as Reg
import OWL2.Portable.RegularityProof as RegProof
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P
import OWL2.Syntax.Regularity as SynReg

name : String → P.Name
name text =
  P.named (P.iri text)

className : String → P.ClassName
className =
  name

objectPropertyName : String → P.ObjectPropertyName
objectPropertyName =
  name

axiom : P.Axiom → P.Annotated P.Axiom
axiom body =
  P.annotated [] body

document : List (P.Annotated P.Axiom) → P.OntologyDocument
document axioms =
  P.ontologyDocument [] (P.ontology P.anonymousOntology [] [] axioms)

person : P.ClassName
person =
  className "https://example.org/portable-regularity#Person"

hasParent hasGrandparent hasAncestor hasSibling : P.ObjectPropertyName
hasParent =
  objectPropertyName "https://example.org/portable-regularity#hasParent"
hasGrandparent =
  objectPropertyName "https://example.org/portable-regularity#hasGrandparent"
hasAncestor =
  objectPropertyName "https://example.org/portable-regularity#hasAncestor"
hasSibling =
  objectPropertyName "https://example.org/portable-regularity#hasSibling"

PersonC : P.ClassExpression
PersonC =
  P.namedClass person

HasParent HasGrandparent HasAncestor HasSibling : P.ObjectPropertyExpression
HasParent =
  P.objectProperty hasParent
HasGrandparent =
  P.objectProperty hasGrandparent
HasAncestor =
  P.objectProperty hasAncestor
HasSibling =
  P.objectProperty hasSibling

CleanRestriction : P.ClassExpression
CleanRestriction =
  P.objectMinCardinality  HasParent absent

cleanDocument : P.OntologyDocument
cleanDocument =
  document
    ( axiom (P.declaration (P.classEntity person))
    ∷ axiom (P.declaration (P.objectPropertyEntity hasParent))
    ∷ axiom
        (P.subClassOf
          PersonC
          CleanRestriction)
    ∷ [] )

cleanReport : Reg.RegularityReport
cleanReport =
  Reg.reportRegularity cleanDocument

cleanSimplePropertyUseCount :
  Reg.regularityReportSimplePropertyUseCount cleanReport ≡ 
cleanSimplePropertyUseCount =
  refl

cleanSimplePropertyViolationCount :
  Reg.regularityReportSimplePropertyViolationCount cleanReport ≡ 
cleanSimplePropertyViolationCount =
  refl

cleanAccepted :
  Reg.PortableRegularityRestrictions cleanDocument
cleanAccepted =
  tt*

cleanCheckResult : RegCheck.RegularityCheckResult
cleanCheckResult =
  RegCheck.checkRegularity cleanDocument

cleanCheckDiagnostics :
  CheckResult.diagnostics cleanCheckResult ≡ []
cleanCheckDiagnostics =
  refl

cleanCheckClean :
  CheckResult.clean? cleanCheckResult ≡ true
cleanCheckClean =
  refl

emptyRegularityContext :
  SynReg.RegularityContext Sem.PortableSignature
emptyRegularityContext =
  record
    { Composite = λ property → ⊥
    ; HierarchyStep = λ sub super → ⊥
    }

emptyNoCompositePredecessor :
  (property : P.ObjectPropertyExpression) →
  ∀ q →
  SynReg.PropertyHierarchyPath
    emptyRegularityContext
    q
    (Sem.translateObjectPropertyExpression property) →
  ¬ SynReg.Composite emptyRegularityContext q
emptyNoCompositePredecessor property q path composite =
  composite

cleanUse : Reg.SimplePropertyUse
cleanUse =
  Reg.simplePropertyUse
    (axiom
      (P.subClassOf
        PersonC
        (P.objectMinCardinality  HasParent absent)))
    (Reg.objectMinCardinalityUse )
    HasParent
    (Reg.objectPropertyBaseKey HasParent)

cleanUseCertificate :
  RegProof.PortableSimplePropertyUseCertificate
    emptyRegularityContext
    cleanUse
cleanUseCertificate =
  RegProof.portableSimplePropertyUseCertificate
    refl
    (emptyNoCompositePredecessor HasParent)

cleanUseNoViolations :
  Reg.NoSimplePropertyViolations
    (Reg.simplePropertyViolationsForUse [] [] cleanUse)
cleanUseNoViolations =
  tt*

cleanUseCertificateFromNoViolations :
  RegProof.PortableSimplePropertyUseCertificate
    emptyRegularityContext
    cleanUse
cleanUseCertificateFromNoViolations =
  RegProof.portableSimplePropertyUseCertificateFromNoViolations
    emptyRegularityContext
    []
    []
    cleanUse
    cleanUseNoViolations
    (emptyNoCompositePredecessor HasParent)

cleanUseMember :
  SynReg.Member
    cleanUse
    (Reg.regularityReportSimplePropertyUses cleanReport)
cleanUseMember =
  SynReg.here

cleanUseNoViolationsFromGeneratedReport :
  Reg.NoSimplePropertyViolations
    (Reg.simplePropertyViolationsForUse
      (Reg.regularityReportCompositeObjectPropertyFacts cleanReport)
      (Reg.regularityReportPropertyHierarchyFacts cleanReport)
      cleanUse)
cleanUseNoViolationsFromGeneratedReport =
  RegProof.simplePropertyUseNoViolationsFromGeneratedReport
    cleanDocument
    cleanAccepted
    cleanUse
    cleanUseMember

cleanUseCertificateFromGeneratedReport :
  RegProof.PortableSimplePropertyUseCertificate
    emptyRegularityContext
    cleanUse
cleanUseCertificateFromGeneratedReport =
  RegProof.portableSimplePropertyUseCertificateFromNoViolations
    emptyRegularityContext
    (Reg.regularityReportCompositeObjectPropertyFacts cleanReport)
    (Reg.regularityReportPropertyHierarchyFacts cleanReport)
    cleanUse
    cleanUseNoViolationsFromGeneratedReport
    (emptyNoCompositePredecessor HasParent)

cleanUseTranslatedSimple :
  SynReg.SimpleObjectPropertyExpression
    emptyRegularityContext
    (Sem.translateObjectPropertyExpression HasParent)
cleanUseTranslatedSimple =
  RegProof.portableSimplePropertyUseCertificateToSyntax
    cleanUseCertificate

cleanRestrictionCertificate :
  RegProof.PortableClassExpressionUsesOnlySimpleObjectPropertiesCertificate
    emptyRegularityContext
    CleanRestriction
cleanRestrictionCertificate =
  RegProof.portableSimpleObjectPropertyExpressionCertificate
    refl
    (emptyNoCompositePredecessor HasParent)
  ,
  tt*

cleanRestrictionTranslatedSimple :
  RegProof.TranslatedClassExpressionUsesOnlySimpleObjectProperties
    emptyRegularityContext
    (Sem.translateClassExpression CleanRestriction)
cleanRestrictionTranslatedSimple =
  RegProof.portableClassExpressionUsesOnlySimpleObjectPropertiesCertificateToSyntax
    {context = emptyRegularityContext}
    {class = CleanRestriction}
    cleanRestrictionCertificate

parentSiblingSimplePropertiesCertificate :
  RegProof.PortableObjectPropertyExpressionsSimpleCertificate
    emptyRegularityContext
    (HasParent ∷ HasSibling ∷ [])
parentSiblingSimplePropertiesCertificate =
  RegProof.portableSimpleObjectPropertyExpressionCertificate
    refl
    (emptyNoCompositePredecessor HasParent)
  ,
  RegProof.portableSimpleObjectPropertyExpressionCertificate
    refl
    (emptyNoCompositePredecessor HasSibling)
  ,
  tt*

parentSiblingTranslatedSimpleProperties :
  SynReg.ObjectPropertyExpressionsSimple
    emptyRegularityContext
    (Sem.translateObjectPropertyExpressionList (HasParent ∷ HasSibling ∷ []))
parentSiblingTranslatedSimpleProperties =
  RegProof.portableObjectPropertyExpressionsSimpleCertificateToSyntax
    parentSiblingSimplePropertiesCertificate

cleanAnnotatedAxiomsUseOnlySimple :
  RegProof.AnnotatedAxiomsUseOnlySimpleObjectProperties
    emptyRegularityContext
    (P.axioms (P.documentOntology cleanDocument))
cleanAnnotatedAxiomsUseOnlySimple =
  (tt* , tt*) ,
  (tt* , tt*) ,
  ((tt* , cleanRestrictionTranslatedSimple) , tt*) ,
  tt*

cleanTranslatedAnnotatedAxiomsUseOnlySimple :
  SynReg.AxiomsUseOnlySimpleObjectProperties
    emptyRegularityContext
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology cleanDocument))))
cleanTranslatedAnnotatedAxiomsUseOnlySimple =
  RegProof.translatedAnnotatedAxiomsUseOnlySimpleObjectProperties
    emptyRegularityContext
    (P.axioms (P.documentOntology cleanDocument))
    cleanAnnotatedAxiomsUseOnlySimple

cleanAnnotatedAxiomsUseOnlySimpleCertificate :
  RegProof.AnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate
    emptyRegularityContext
    (P.axioms (P.documentOntology cleanDocument))
cleanAnnotatedAxiomsUseOnlySimpleCertificate =
  tt* ,
  tt* ,
  (tt* , cleanRestrictionCertificate) ,
  tt*

cleanTranslatedAnnotatedAxiomsUseOnlySimpleFromCertificate :
  SynReg.AxiomsUseOnlySimpleObjectProperties
    emptyRegularityContext
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology cleanDocument))))
cleanTranslatedAnnotatedAxiomsUseOnlySimpleFromCertificate =
  RegProof.translatedAnnotatedAxiomsUseOnlySimpleObjectPropertiesCertificate
    emptyRegularityContext
    (P.axioms (P.documentOntology cleanDocument))
    cleanAnnotatedAxiomsUseOnlySimpleCertificate

cleanDocumentUseOnlySimpleCertificate :
  RegProof.OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate
    emptyRegularityContext
    cleanDocument
cleanDocumentUseOnlySimpleCertificate =
  cleanAnnotatedAxiomsUseOnlySimpleCertificate

cleanDocumentTranslatedUseOnlySimpleFromCertificate :
  SynReg.AxiomsUseOnlySimpleObjectProperties
    emptyRegularityContext
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology cleanDocument))))
cleanDocumentTranslatedUseOnlySimpleFromCertificate =
  RegProof.ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateToTranslatedAxioms
    emptyRegularityContext
    cleanDocument
    cleanDocumentUseOnlySimpleCertificate

cleanUseResolver :
  RegProof.SimplePropertyUseCertificateResolver
    emptyRegularityContext
    (Reg.ontologyDocumentSimplePropertyUses cleanDocument)
cleanUseResolver use SynReg.here =
  cleanUseCertificate
cleanUseResolver use (SynReg.there ())

cleanDocumentUseOnlySimpleCertificateFromResolver :
  RegProof.OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate
    emptyRegularityContext
    cleanDocument
cleanDocumentUseOnlySimpleCertificateFromResolver =
  RegProof.ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromUseResolver
    emptyRegularityContext
    cleanDocument
    cleanUseResolver

cleanDocumentTranslatedUseOnlySimpleFromResolver :
  SynReg.AxiomsUseOnlySimpleObjectProperties
    emptyRegularityContext
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology cleanDocument))))
cleanDocumentTranslatedUseOnlySimpleFromResolver =
  RegProof.ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateToTranslatedAxioms
    emptyRegularityContext
    cleanDocument
    cleanDocumentUseOnlySimpleCertificateFromResolver

emptyUseDocument : P.OntologyDocument
emptyUseDocument =
  document []

emptyUseGeneratedResolver :
  RegProof.SimplePropertyUseCertificateResolver
    (RegProof.generatedRegularityContext emptyUseDocument)
    (Reg.regularityReportSimplePropertyUses (Reg.reportRegularity emptyUseDocument))
emptyUseGeneratedResolver use ()

emptyUseNoCompositeResolver :
  RegProof.SimplePropertyUseNoCompositePredecessorResolver
    (RegProof.generatedRegularityContext emptyUseDocument)
    (Reg.regularityReportSimplePropertyUses (Reg.reportRegularity emptyUseDocument))
emptyUseNoCompositeResolver use ()

emptyUseDocumentGeneratedCertificateFromResolver :
  RegProof.OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate
    (RegProof.generatedRegularityContext emptyUseDocument)
    emptyUseDocument
emptyUseDocumentGeneratedCertificateFromResolver =
  RegProof.ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromGeneratedUseResolver
    emptyUseDocument
    emptyUseGeneratedResolver

emptyUseDocumentTranslatedUseOnlySimpleFromGeneratedResolver :
  SynReg.AxiomsUseOnlySimpleObjectProperties
    (RegProof.generatedRegularityContext emptyUseDocument)
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology emptyUseDocument))))
emptyUseDocumentTranslatedUseOnlySimpleFromGeneratedResolver =
  RegProof.ontologyDocumentUsesOnlySimpleObjectPropertiesFromGeneratedUseResolver
    emptyUseDocument
    emptyUseGeneratedResolver

emptyUseDocumentGeneratedCertificateFromCleanReport :
  RegProof.OntologyDocumentUsesOnlySimpleObjectPropertiesCertificate
    (RegProof.generatedRegularityContext emptyUseDocument)
    emptyUseDocument
emptyUseDocumentGeneratedCertificateFromCleanReport =
  RegProof.ontologyDocumentUsesOnlySimpleObjectPropertiesCertificateFromGeneratedCleanReportAndNoCompositeResolver
    emptyUseDocument
    tt*
    emptyUseNoCompositeResolver

emptyUseDocumentTranslatedUseOnlySimpleFromCleanReport :
  SynReg.AxiomsUseOnlySimpleObjectProperties
    (RegProof.generatedRegularityContext emptyUseDocument)
    (Sem.semanticAxioms
      (Sem.translateAnnotatedAxioms
        (P.axioms (P.documentOntology emptyUseDocument))))
emptyUseDocumentTranslatedUseOnlySimpleFromCleanReport =
  RegProof.ontologyDocumentUsesOnlySimpleObjectPropertiesFromGeneratedCleanReportAndNoCompositeResolver
    emptyUseDocument
    tt*
    emptyUseNoCompositeResolver

parentParentChain : P.ObjectPropertyChain
parentParentChain =
  P.objectPropertyChain (P.twoOrMore HasParent HasParent [])

chainDocument : P.OntologyDocument
chainDocument =
  document
    ( axiom
        (P.subObjectPropertyOf
          (P.subObjectPropertyChain parentParentChain)
          HasGrandparent)
    ∷ axiom
        (P.subClassOf
          PersonC
          (P.objectMinCardinality  HasGrandparent absent))
    ∷ [] )

chainReport : Reg.RegularityReport
chainReport =
  Reg.reportRegularity chainDocument

chainCompositeObjectPropertyCount :
  Reg.regularityReportCompositeObjectPropertyCount chainReport ≡ 
chainCompositeObjectPropertyCount =
  refl

chainSimplePropertyViolationCount :
  Reg.regularityReportSimplePropertyViolationCount chainReport ≡ 
chainSimplePropertyViolationCount =
  refl

chainRejected :
  ¬ Reg.PortableRegularityRestrictions chainDocument
chainRejected impossible =
  impossible

chainUse : Reg.SimplePropertyUse
chainUse =
  Reg.simplePropertyUse
    (axiom
      (P.subClassOf
        PersonC
        (P.objectMinCardinality  HasGrandparent absent)))
    (Reg.objectMinCardinalityUse )
    HasGrandparent
    (Reg.objectPropertyBaseKey HasGrandparent)

chainCompositeFact : Reg.CompositeObjectPropertyFact
chainCompositeFact =
  Reg.compositeObjectPropertyFact
    (Reg.objectPropertyBaseKey HasGrandparent)
    HasGrandparent
    Reg.propertyChainSuperPropertyComposite
    (present
      (axiom
        (P.subObjectPropertyOf
          (P.subObjectPropertyChain parentParentChain)
          HasGrandparent)))

chainCheckResult : RegCheck.RegularityCheckResult
chainCheckResult =
  RegCheck.checkRegularity chainDocument

chainCheckDiagnostics :
  CheckResult.diagnostics chainCheckResult ≡
  RegCheck.simplePropertyViolationDiagnostic
    (Reg.simplePropertyViolation
      chainUse
      (Reg.compositeSimplePropertyUse chainCompositeFact))
  ∷ []
chainCheckDiagnostics =
  refl

chainCheckUnclean :
  CheckResult.clean? chainCheckResult ≡ false
chainCheckUnclean =
  refl

chainCheckEvidenceUnavailable :
  CheckResult.evidence? chainCheckResult ≡ absent
chainCheckEvidenceUnavailable =
  refl

chainCompositeFactKeyCoherent :
  RegProof.CompositeObjectPropertyFactKeyCoherent chainCompositeFact
chainCompositeFactKeyCoherent =
  RegProof.ontologyDocumentCompositeObjectPropertyFactsKeyCoherent
    chainDocument
    chainCompositeFact
    (SynReg.there (SynReg.there SynReg.here))

chainCleanContradictsDirectCompositeKey :
  Reg.PortableRegularityRestrictions chainDocument →
  ⊥
chainCleanContradictsDirectCompositeKey clean =
  RegProof.generatedReportRejectsDirectCompositeKey
    chainDocument
    clean
    chainUse
    SynReg.here
    chainCompositeFact
    (SynReg.there (SynReg.there SynReg.here))
    (String.stringEqualityTrueFromEqual
      (Reg.simplePropertyUseKey chainUse)
      (Reg.compositeObjectPropertyKey chainCompositeFact)
      refl)

chainHierarchyDocument : P.OntologyDocument
chainHierarchyDocument =
  document
    ( axiom
        (P.subObjectPropertyOf
          (P.subObjectPropertyChain parentParentChain)
          HasGrandparent)
    ∷ axiom
        (P.subObjectPropertyOf
          (P.subObjectProperty HasGrandparent)
          HasAncestor)
    ∷ axiom
        (P.subClassOf
          PersonC
          (P.objectMinCardinality  HasAncestor absent))
    ∷ [] )

chainHierarchyReport : Reg.RegularityReport
chainHierarchyReport =
  Reg.reportRegularity chainHierarchyDocument

chainHierarchyCompositeObjectPropertyCount :
  Reg.regularityReportCompositeObjectPropertyCount
    chainHierarchyReport
    ≡ 
chainHierarchyCompositeObjectPropertyCount =
  refl

chainHierarchyPropertyHierarchyCount :
  Reg.regularityReportPropertyHierarchyCount chainHierarchyReport ≡ 
chainHierarchyPropertyHierarchyCount =
  refl

chainHierarchySimplePropertyUseCount :
  Reg.regularityReportSimplePropertyUseCount chainHierarchyReport ≡ 
chainHierarchySimplePropertyUseCount =
  refl

chainHierarchySimplePropertyViolationCount :
  Reg.regularityReportSimplePropertyViolationCount
    chainHierarchyReport
    ≡ 
chainHierarchySimplePropertyViolationCount =
  refl

chainHierarchyPathExtracted :
  Reg.propertyKeyReachable
    (Reg.ontologyDocumentPropertyHierarchyFacts chainHierarchyDocument)
    (Reg.objectPropertyBaseKey HasGrandparent)
    (Reg.objectPropertyBaseKey HasAncestor)
    ≡ true
chainHierarchyPathExtracted =
  refl

chainHierarchyRegularityContext :
  SynReg.RegularityContext Sem.PortableSignature
chainHierarchyRegularityContext =
  RegProof.generatedRegularityContext chainHierarchyDocument

chainHierarchyGrandparentComposite :
  SynReg.Composite
    chainHierarchyRegularityContext
    (Sem.translateObjectPropertyExpression HasGrandparent)
chainHierarchyGrandparentComposite =
  RegProof.portableCompositeObjectPropertyEvidenceForMember
    (SynReg.there (SynReg.there SynReg.here))

chainHierarchyGrandparentAncestorStep :
  SynReg.HierarchyStep
    chainHierarchyRegularityContext
    (Sem.translateObjectPropertyExpression HasGrandparent)
    (Sem.translateObjectPropertyExpression HasAncestor)
chainHierarchyGrandparentAncestorStep =
  RegProof.portablePropertyHierarchyStepEvidenceForMember
    SynReg.here

chainHierarchyPathExtractedFromStepEvidence :
  Reg.propertyKeyReachable
    (Reg.ontologyDocumentPropertyHierarchyFacts chainHierarchyDocument)
    (Reg.objectPropertyBaseKey HasGrandparent)
    (Reg.objectPropertyBaseKey HasAncestor)
    ≡ true
chainHierarchyPathExtractedFromStepEvidence =
  RegProof.propertyKeyReachableFromHierarchyStepEvidence
    chainHierarchyGrandparentAncestorStep

chainHierarchyKeyPathFromStepEvidence :
  RegProof.PropertyKeyPath
    (Reg.ontologyDocumentPropertyHierarchyFacts chainHierarchyDocument)
    (Reg.objectPropertyBaseKey HasGrandparent)
    (Reg.objectPropertyBaseKey HasAncestor)
chainHierarchyKeyPathFromStepEvidence =
  RegProof.propertyKeyPathFromHierarchyStepEvidence
    chainHierarchyGrandparentAncestorStep

chainHierarchyKeyPathComputedReachable :
  Reg.propertyKeyReachableWithin
    (RegProof.propertyKeyPathLength chainHierarchyKeyPathFromStepEvidence)
    (Reg.ontologyDocumentPropertyHierarchyFacts chainHierarchyDocument)
    (Reg.objectPropertyBaseKey HasGrandparent)
    (Reg.objectPropertyBaseKey HasAncestor)
    ≡ true
chainHierarchyKeyPathComputedReachable =
  RegProof.propertyKeyReachableWithinFromKeyPath
    chainHierarchyKeyPathFromStepEvidence

chainHierarchyFactKeyCoherent :
  RegProof.PropertyHierarchyFactKeyCoherentResolver
    (Reg.ontologyDocumentPropertyHierarchyFacts chainHierarchyDocument)
chainHierarchyFactKeyCoherent fact SynReg.here =
  RegProof.ontologyDocumentPropertyHierarchyFactsKeyCoherent
    chainHierarchyDocument
    fact
    SynReg.here
chainHierarchyFactKeyCoherent fact (SynReg.there member) =
  RegProof.ontologyDocumentPropertyHierarchyFactsKeyCoherent
    chainHierarchyDocument
    fact
    (SynReg.there member)

chainHierarchyGrandparentAncestorPath :
  SynReg.PropertyHierarchyPath
    chainHierarchyRegularityContext
    (Sem.translateObjectPropertyExpression HasGrandparent)
    (Sem.translateObjectPropertyExpression HasAncestor)
chainHierarchyGrandparentAncestorPath =
  RegProof.portablePropertyHierarchyPathFromStepEvidence
    chainHierarchyGrandparentAncestorStep

chainHierarchyKeyPathFromSemanticPath :
  RegProof.PropertyKeyPath
    (Reg.ontologyDocumentPropertyHierarchyFacts chainHierarchyDocument)
    (Reg.objectPropertyBaseKey HasGrandparent)
    (Reg.objectPropertyBaseKey HasAncestor)
chainHierarchyKeyPathFromSemanticPath =
  RegProof.propertyKeyPathFromHierarchyPath
    chainHierarchyFactKeyCoherent
    chainHierarchyGrandparentAncestorPath

chainHierarchySemanticPathComputedReachable :
  Reg.propertyKeyReachableWithin
    (RegProof.propertyKeyPathLength chainHierarchyKeyPathFromSemanticPath)
    (Reg.ontologyDocumentPropertyHierarchyFacts chainHierarchyDocument)
    (Reg.objectPropertyBaseKey HasGrandparent)
    (Reg.objectPropertyBaseKey HasAncestor)
    ≡ true
chainHierarchySemanticPathComputedReachable =
  RegProof.propertyKeyReachableWithinFromHierarchyPath
    chainHierarchyFactKeyCoherent
    chainHierarchyGrandparentAncestorPath

chainHierarchySemanticPathReachableWitness :
  Σ ℕ
    (λ fuel →
      Reg.propertyKeyReachableWithin
        fuel
        (Reg.ontologyDocumentPropertyHierarchyFacts chainHierarchyDocument)
        (Reg.objectPropertyBaseKey HasGrandparent)
        (Reg.objectPropertyBaseKey HasAncestor)
      ≡
      true)
chainHierarchySemanticPathReachableWitness =
  RegProof.propertyKeyReachableWithinWitnessFromHierarchyPath
    chainHierarchyFactKeyCoherent
    chainHierarchyGrandparentAncestorPath

chainHierarchyAncestorNonSimple :
  SynReg.NonSimpleObjectPropertyExpression
    chainHierarchyRegularityContext
    (Sem.translateObjectPropertyExpression HasAncestor)
chainHierarchyAncestorNonSimple =
  Sem.translateObjectPropertyExpression HasGrandparent ,
  chainHierarchyGrandparentAncestorPath ,
  chainHierarchyGrandparentComposite

chainHierarchyUse : Reg.SimplePropertyUse
chainHierarchyUse =
  Reg.simplePropertyUse
    (axiom
      (P.subClassOf
        PersonC
        (P.objectMinCardinality  HasAncestor absent)))
    (Reg.objectMinCardinalityUse )
    HasAncestor
    (Reg.objectPropertyBaseKey HasAncestor)

chainHierarchyCompositeFact : Reg.CompositeObjectPropertyFact
chainHierarchyCompositeFact =
  Reg.compositeObjectPropertyFact
    (Reg.objectPropertyBaseKey HasGrandparent)
    HasGrandparent
    Reg.propertyChainSuperPropertyComposite
    (present
      (axiom
        (P.subObjectPropertyOf
          (P.subObjectPropertyChain parentParentChain)
          HasGrandparent)))

chainHierarchyCheckResult : RegCheck.RegularityCheckResult
chainHierarchyCheckResult =
  RegCheck.checkRegularity chainHierarchyDocument

chainHierarchyCheckDiagnostics :
  CheckResult.diagnostics chainHierarchyCheckResult ≡
  RegCheck.simplePropertyViolationDiagnostic
    (Reg.simplePropertyViolation
      chainHierarchyUse
      (Reg.compositeHierarchySimplePropertyUse
        chainHierarchyCompositeFact))
  ∷ []
chainHierarchyCheckDiagnostics =
  refl

chainHierarchyCheckUnclean :
  CheckResult.clean? chainHierarchyCheckResult ≡ false
chainHierarchyCheckUnclean =
  refl

chainHierarchyCheckEvidenceUnavailable :
  CheckResult.evidence? chainHierarchyCheckResult ≡ absent
chainHierarchyCheckEvidenceUnavailable =
  refl

chainHierarchyCompositeFactKeyCoherent :
  RegProof.CompositeObjectPropertyFactKeyCoherent chainHierarchyCompositeFact
chainHierarchyCompositeFactKeyCoherent =
  RegProof.ontologyDocumentCompositeObjectPropertyFactsKeyCoherent
    chainHierarchyDocument
    chainHierarchyCompositeFact
    (SynReg.there (SynReg.there SynReg.here))

chainHierarchyCleanContradictsReachableCompositeKey :
  Reg.PortableRegularityRestrictions chainHierarchyDocument →
  ⊥
chainHierarchyCleanContradictsReachableCompositeKey clean =
  RegProof.generatedReportRejectsReachableCompositeKey
    chainHierarchyDocument
    clean
    chainHierarchyUse
    SynReg.here
    chainHierarchyCompositeFact
    (SynReg.there (SynReg.there SynReg.here))
    chainHierarchyPathExtractedFromStepEvidence

chainHierarchyRejected :
  ¬ Reg.PortableRegularityRestrictions chainHierarchyDocument
chainHierarchyRejected impossible =
  impossible

topPropertyDocument : P.OntologyDocument
topPropertyDocument =
  document
    ( axiom
        (P.functionalObjectProperty P.topObjectProperty)
    ∷ [] )

topPropertyReport : Reg.RegularityReport
topPropertyReport =
  Reg.reportRegularity topPropertyDocument

topPropertyRejectedByBuiltInComposite :
  Reg.regularityReportSimplePropertyViolationCount topPropertyReport ≡ 
topPropertyRejectedByBuiltInComposite =
  refl

topPropertyCanonicalTranslated :
  SynReg.CanonicalObjectPropertyExpression
    (Sem.translateObjectPropertyExpression P.topObjectProperty)
topPropertyCanonicalTranslated =
  RegProof.portableCanonicalObjectPropertyExpression
    P.topObjectProperty
    refl

nestedInverseDocument : P.OntologyDocument
nestedInverseDocument =
  document
    ( axiom
        (P.irreflexiveObjectProperty
          (P.objectInverseOf (P.objectInverseOf HasSibling)))
    ∷ [] )

nestedInverseReport : Reg.RegularityReport
nestedInverseReport =
  Reg.reportRegularity nestedInverseDocument

nestedInverseRejectedAsNonCanonical :
  Reg.regularityReportSimplePropertyViolationCount nestedInverseReport ≡ 
nestedInverseRejectedAsNonCanonical =
  refl

nestedInverseUse : Reg.SimplePropertyUse
nestedInverseUse =
  Reg.simplePropertyUse
    (axiom
      (P.irreflexiveObjectProperty
        (P.objectInverseOf (P.objectInverseOf HasSibling))))
    Reg.irreflexiveObjectPropertyUse
    (P.objectInverseOf (P.objectInverseOf HasSibling))
    (Reg.objectPropertyBaseKey
      (P.objectInverseOf (P.objectInverseOf HasSibling)))

nestedInverseCheckResult : RegCheck.RegularityCheckResult
nestedInverseCheckResult =
  RegCheck.checkRegularity nestedInverseDocument

nestedInverseCheckDiagnostics :
  CheckResult.diagnostics nestedInverseCheckResult ≡
  RegCheck.simplePropertyViolationDiagnostic
    (Reg.simplePropertyViolation
      nestedInverseUse
      Reg.nonCanonicalSimplePropertyUse)
  ∷ []
nestedInverseCheckDiagnostics =
  refl

nestedInverseCheckUnclean :
  CheckResult.clean? nestedInverseCheckResult ≡ false
nestedInverseCheckUnclean =
  refl

nestedInverseCheckEvidenceUnavailable :
  CheckResult.evidence? nestedInverseCheckResult ≡ absent
nestedInverseCheckEvidenceUnavailable =
  refl

LocalBoolIsTrue : Bool → Type₀
LocalBoolIsTrue true =
  Unit*
LocalBoolIsTrue false =
  ⊥

localFalseNotTrue : false ≡ true → ⊥
localFalseNotTrue equality =
  subst LocalBoolIsTrue (sym equality) tt*

nestedInverseCanonicalRejected :
  Reg.canonicalForSimplePropertyUse
    (P.objectInverseOf (P.objectInverseOf HasSibling))
  ≡ true →
  ⊥
nestedInverseCanonicalRejected canonical =
  localFalseNotTrue canonical