Refactor proof type mapping to use PROOF_TYPES

Replaces the hardcoded DEFAULT_REALTYP_TO_COUNTERTYP dictionary with a dynamic construction based on PROOF_TYPES from proof_type.py. This improves maintainability by centralizing proof type definitions.

Author: douden

sphinx_proof/directive.py

@@ -16,27 +16,13 @@
 from sphinx.util.docutils import SphinxDirective
 from .nodes import unenumerable_node, NODE_TYPES
 from .nodes import proof_node
+from .proof_type import PROOF_TYPES
 
 logger = logging.getLogger(__name__)
 
-
-DEFAULT_REALTYP_TO_COUNTERTYP = {
-    "axiom": "axiom",
-    "theorem": "theorem",
-    "lemma": "lemma",
-    "algorithm": "algorithm",
-    "definition": "definition",
-    "remark": "remark",
-    "conjecture": "conjecture",
-    "corollary": "corollary",
-    "criterion": "criterion",
-    "example": "example",
-    "property": "property",
-    "observation": "observation",
-    "proposition": "proposition",
-    "assumption": "assumption",
-    "notation": "notation",
-}
+DEFAULT_REALTYP_TO_COUNTERTYP = {}
+for typ in PROOF_TYPES:
+    DEFAULT_REALTYP_TO_COUNTERTYP[typ] = typ
 
 
 class ElementDirective(SphinxDirective):