Skip to content

Fix: take assumptions into account for subproof statements

Sankalp Gambhir requested to merge github/fork/sankalpgambhir/subproof-bot-fix into main

Assumptions are currently not taken into account when checking that a subproof has succeeded in proving its goal at the top-level.

Example:

assume(C)
val ab = have(A |- B)

have(A |- B) subproof {
  have(thesis) by Restate.from(ab)
}

Will raise an error saying the subproof proved C; A |- B, instead of the expected sequent A |- B. So, C is being propagated into the subproof as expected, but the top-level correctness check fails to take this assumption into account.

This has been fixed by adding assumptions into the sequent the subproof uses for checking.

Merge request reports