Fixing Nonactive Hypotheses Treated as Active

Issue Description:

We need to ensure that if a step in a proof has the type $e or $f, its label corresponds to an active hypothesis. Currently, there is an issue where labels of hypotheses are erroneously active outside of their intended scope.

Example Scenario:

Consider the attached database. When this file is passed to mmverify.py, there is no output, indicating that the proof of "a1i" is correct.

Expected Behavior:

The label "min" should cause an error since it should only be active in the "ax-mp" frame.

Proposed Solution:

def treat_normal_proof(self, proof: list[str]) -> list[Stmt]:
    """Return the proof stack once the given normal proof has been
    processed.
    """
    stack: list[Stmt] = []
    active_hypotheses = {label for frame in self.fs for labels in (frame.f_labels, frame.e_labels) for label in labels.values()}
    for label in proof:
        stmt_info = self.labels.get(label)
        if stmt_info:
            label_type = stmt_info[0]
            if label_type in {'$e', '$f'}:
                if label in active_hypotheses:
                    self.treat_step(stmt_info, stack)
                else:
                    raise MMError(f"The label {label} is the label of a nonactive hypothesis.")
            else:
                self.treat_step(stmt_info, stack)
        else:
            raise MMError(f"No statement information found for label {label}")
    return stack

error.mm.txt

david-a-wheeler / mmverify.py

Fixing Nonactive Hypotheses Treated as Active #24