From 34b910489c1826f455e58847528a38f329713337 Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 18 Jul 2026 20:05:16 +0300 Subject: [PATCH] fix: require ByCases statements to be defined Match Claim: reject free symbols that are not in the proof state. --- src/estimates/propositional_tactics.py | 4 ++++ tests/test_all.py | 13 +++++++++++++ 2 files changed, 17 insertions(+) diff --git a/src/estimates/propositional_tactics.py b/src/estimates/propositional_tactics.py index 5f921bc..00ba8b8 100644 --- a/src/estimates/propositional_tactics.py +++ b/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() diff --git a/tests/test_all.py b/tests/test_all.py index 862b3ed..81f16bf 100644 --- a/tests/test_all.py +++ b/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)