Some more formula transformation algorithms

	new file:   src/notebook/math/logic/transformation/dual.py

Author: v--

notebook.tex

@@ -202,7 +202,7 @@
   \include{text/logical_consequence}
   \include{text/boolean_functions}
   \include{text/propositional_logic}
-  \include{text/propositional_normal_forms}
+  \include{text/propositional_formula_transformations}
   \include{text/propositional_axiomatic_derivations}
   \include{text/propositional_natural_deduction}
   \include{text/propositional_completeness}

packages/math_macros.sty

@@ -21,7 +21,6 @@
 \NewDocumentCommand \boxprod      {} {\mathbin \smwhtsquare}
 \NewDocumentCommand \anon        {s} {\mathbin {\IfBooleanTF {#1} - \smblkcircle}}
 \NewDocumentCommand \Anon        {s} {\mathbin {\IfBooleanTF {#1} - \mdsmblkcircle}}
-\NewDocumentCommand \relcirc     {s} {\IfBooleanTF {#1} {\thinspace \circ \thinspace} {\mathrel \circ}}
 \NewDocumentCommand \bincirc     {s} {\IfBooleanTF {#1} {\thinspace \circ \thinspace} {\mathbin \circ}}
 \NewDocumentCommand \binast      {s} {\IfBooleanTF {#1} {\thinspace \circ \ast} {\mathbin \ast}}
 \NewDocumentCommand \multto       {} {\rightrightarrows}

src/notebook/math/combinatorics/ramsey.py

@@ -26,7 +26,7 @@ def ramsey_upper_bound(s: int, t: int, *rest: int) -> int:
 def enumerate_edge_coloring_sequences(n: int, r: int) -> Iterable[Collection[int]]:
     colors = list(range(r))
     m = choose(n, 2)
-    yield from itertools.product(*([colors] * m))
+    yield from itertools.product(colors, repeat=m)
 
 
 def enumerate_complete_graph_coloring(n: int, r: int) -> Iterable[EdgeColoredGraph]:

src/notebook/math/lambda_/curry_howard/conftest.py

@@ -6,9 +6,6 @@
 
 @pytest.fixture
 def ch_logic_dummy_signature() -> FormalLogicSignature:
-    signature = PropositionalLogicSignature()
-
-    for ind in range(ord('α'), ord('ω') + 1):
-        signature.add_symbol(PropositionalVariable(chr(ind)))
-
-    return signature
+    return PropositionalLogicSignature(
+        *(PropositionalVariable(chr(i)) for i in range(ord('α'), ord('ω') + 1))
+    )

src/notebook/math/lambda_/terms/schemas.py

@@ -13,6 +13,9 @@ class VariablePlaceholder:
     def __str__(self) -> str:
         return str(self.identifier)
 
+    def __repr__(self) -> str:
+        return f"parse_term_schema('{self}')"
+
 
 @dataclass(frozen=True)
 class TermPlaceholder:
@@ -21,6 +24,9 @@ class TermPlaceholder:
     def __str__(self) -> str:
         return str(self.identifier)
 
+    def __repr__(self) -> str:
+        return f"parse_term_schema('{self}')"
+
 
 @dataclass(frozen=True)
 class TypedApplicationSchema:
@@ -30,6 +36,9 @@ class TypedApplicationSchema:
     def __str__(self) -> str:
         return f'({self.left}{self.right})'
 
+    def __repr__(self) -> str:
+        return f"parse_term_schema('{self}')"
+
 
 @dataclass(frozen=True)
 class TypedAbstractionSchema:
@@ -40,5 +49,8 @@ class TypedAbstractionSchema:
     def __str__(self) -> str:
         return f'({BinderSymbol.LAMBDA}{self.var}:{self.var_type}.{self.body})'
 
+    def __repr__(self) -> str:
+        return f"parse_term_schema('{self}')"
+
 
 TypedTermSchema = Constant | VariablePlaceholder | TermPlaceholder | TypedApplicationSchema | TypedAbstractionSchema

src/notebook/math/lambda_/terms/terms.py

@@ -12,6 +12,9 @@ class Constant:
     def __str__(self) -> str:
         return str(self.name)
 
+    def __repr__(self) -> str:
+        return f"parse_term('{self}')"
+
 
 @dataclass(frozen=True)
 class Variable:
@@ -20,6 +23,9 @@ class Variable:
     def __str__(self) -> str:
         return str(self.identifier)
 
+    def __repr__(self) -> str:
+        return f"parse_term('{self}')"
+
 
 @dataclass(frozen=True)
 class UntypedApplication:
@@ -29,6 +35,9 @@ class UntypedApplication:
     def __str__(self) -> str:
         return f'({self.left}{self.right})'
 
+    def __repr__(self) -> str:
+        return f"parse_term('{self}')"
+
 
 @dataclass(frozen=True)
 class TypedApplication:
@@ -38,6 +47,9 @@ class TypedApplication:
     def __str__(self) -> str:
         return f'({self.left}{self.right})'
 
+    def __repr__(self) -> str:
+        return f"parse_term('{self}')"
+
 
 @dataclass(frozen=True)
 class UntypedAbstraction:
@@ -47,6 +59,9 @@ class UntypedAbstraction:
     def __str__(self) -> str:
         return f'({BinderSymbol.LAMBDA}{self.var}.{self.body})'
 
+    def __repr__(self) -> str:
+        return f"parse_term('{self}')"
+
 
 @dataclass(frozen=True)
 class TypedAbstraction:
@@ -57,6 +72,9 @@ class TypedAbstraction:
     def __str__(self) -> str:
         return f'({BinderSymbol.LAMBDA}{self.var}:{self.var_type}.{self.body})'
 
+    def __repr__(self) -> str:
+        return f"parse_term('{self}')"
+
 
 UntypedTerm = Constant | Variable | UntypedApplication | UntypedAbstraction
 TypedTerm = Constant | Variable | TypedApplication | TypedAbstraction

src/notebook/math/lambda_/types/schemas.py

@@ -12,6 +12,9 @@ class TypePlaceholder:
     def __str__(self) -> str:
         return str(self.identifier)
 
+    def __repr__(self) -> str:
+        return f"parse_type_schema('{self}')"
+
 
 @dataclass(frozen=True)
 class SimpleConnectiveTypeSchema:
@@ -22,5 +25,8 @@ class SimpleConnectiveTypeSchema:
     def __str__(self) -> str:
         return f'({self.left} {self.conn} {self.right})'
 
+    def __repr__(self) -> str:
+        return f"parse_type_schema('{self}')"
+
 
 SimpleTypeSchema = BaseType | TypePlaceholder | SimpleConnectiveTypeSchema

src/notebook/math/lambda_/types/types.py

@@ -12,6 +12,9 @@ class BaseType:
     def __str__(self) -> str:
         return str(self.name)
 
+    def __repr__(self) -> str:
+        return f"parse_type('{self}')"
+
 
 @dataclass(frozen=True)
 class TypeVariable:
@@ -20,6 +23,9 @@ class TypeVariable:
     def __str__(self) -> str:
         return str(self.identifier)
 
+    def __repr__(self) -> str:
+        return f"parse_type('{self}')"
+
 
 @dataclass(frozen=True)
 class SimpleConnectiveType:
@@ -30,6 +36,9 @@ class SimpleConnectiveType:
     def __str__(self) -> str:
         return f'({self.left} {self.conn} {self.right})'
 
+    def __repr__(self) -> str:
+        return f"parse_type('{self}')"
+
 
 SimpleType = BaseType | TypeVariable | SimpleConnectiveType
 

src/notebook/math/logic/deduction/test_proof_tree.py

@@ -11,10 +11,10 @@
     parse_formula_placeholder,
     parse_formula_with_substitution,
     parse_marker,
-    parse_propositional_formula,
     parse_term_substitution_spec,
     parse_variable,
 )
+from ..propositional import parse_propositional_formula
 from ..signature import FormalLogicSignature
 from .exceptions import RuleApplicationError
 from .proof_tree import AssumptionTree, ProofTree, RuleApplicationPremise, apply, assume, premise

src/notebook/math/logic/derivation/test_axiomatic_derivation.py

@@ -2,7 +2,7 @@
 from textwrap import dedent
 
 from ....support.pytest import pytest_parametrize_kwargs, pytest_parametrize_lists
-from ..parsing import parse_propositional_formula
+from ..propositional import parse_propositional_formula
 from .axiomatic_derivation import (
     AxiomaticDerivation,
     are_derivations_equivalent,