fix: require ByCases statements to be defined

src/estimates/propositional_tactics.py

@@ -275,6 +275,10 @@ def __init__(self, statement: Boolean, name: str = "this") -> None:
     def activate(self, state: ProofState) -> list[ProofState]:
         if not isinstance(self.statement, Boolean):
             raise ValueError(f"{self.statement!s} is not a proposition.")
+        if not is_defined(self.statement, state.get_all_vars()):
+            raise ValueError(
+                f"{self.statement!s} is not defined in the current proof state."
+            )
         name = state.new(self.name)
         new_states = []
         new_state = state.copy()

tests/test_all.py

@@ -110,3 +110,16 @@ def test_subst_all_solution_reversed(self, capsys):
     def test_sympy_simplify_solution(self, capsys):
         sympy_simplify_solution()
         self.proof_complete(capsys)
+
+    def test_bycases_requires_defined(self):
+        """ByCases must reject free symbols not declared in the proof state."""
+        from sympy import Symbol
+        p = ProofAssistant()
+        x = p.var("pos_real", "x")
+        p.begin_proof(x > 0)
+        w = Symbol("w", real=True)
+        try:
+            p.use(ByCases(w > 1, "h"))
+            assert False, "expected ValueError"
+        except ValueError as e:
+            assert "not defined" in str(e)