Skip to content

Conversation

@dpvc
Copy link
Member

@dpvc dpvc commented Jun 30, 2024

This PR fixes problems with the computation of the left- and right-hand width adjustments that are used to get the correct bounding box for the final proof table. Currently, the left-hand adjustment can be too big, while the right-hand can be too small or too big. This is true, for example, with this proof:

$$\bbox[orange]{
\begin{prooftree}\AxiomC{}
\RightLabel{Ax}\UnaryInfC{p ⊢ p}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{¬p ⊢ ¬p}
\RightLabel{E→}\BinaryInfC{¬p, p ⊢ ⊥}
\RightLabel{I→}\UnaryInfC{¬p, p ⊢ ¬ ¬q}
\RightLabel{DNE}\UnaryInfC{¬p, p ⊢ q}
\RightLabel{I→}\UnaryInfC{¬p ⊢ p → q}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{(p → q) → p ⊢ (p → q) → p}
\RightLabel{E→}\BinaryInfC{(p → q) → p, ¬p ⊢ p}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{p ⊢ p}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{¬p ⊢ ¬p}
\RightLabel{E→}\BinaryInfC{¬p, p ⊢ ⊥}
\RightLabel{I→}\UnaryInfC{¬p ⊢ ¬p}
\RightLabel{E→}\BinaryInfC{¬p, (p → q) → p ⊢ ⊥}
\RightLabel{I→}\UnaryInfC{(p → q) → p ⊢ ¬ ¬p}
\RightLabel{DNE}\UnaryInfC{(p → q) → p ⊢ p}
\RightLabel{I→}\UnaryInfC{ ⊢ ((p → q) → p) → p}
\end{prooftree}
}$$

On the right, the maxAdjust computations are not correct, leading to the wrong size. Some things that can show this are labels that exceed past the width of the material above it, and conclusions that are shorter than the lines below it.

On the left, too much space will be added if a conclusion above a rule is shorter than the rule itself.

This PR introduces a new means of computing the maxAdjust value (that doesn't rely on saving it in a property), and takes care of the short-conclusion-over-longer-rule discrepancy as well. I don't have any knowledge of the buss proofs package myself, so relied on this example and a few others to test this, so I may have missed something, but I think it is correct.

I also fixed the label placement and bounding boxes, which were not quite right.

I didn't adjust the comments above balanceRules() as I didn't really understand them, but they no longer completely apply.

Resolves issues mathjax/MathJax#3251 and mathjax/MathJax#3240.

@dpvc dpvc requested a review from zorkow June 30, 2024 17:34
@dpvc dpvc added this to the v4.0 milestone Jun 30, 2024
Copy link
Member

@zorkow zorkow left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm.

@dpvc dpvc merged commit a56f679 into develop Jul 2, 2024
@dpvc dpvc deleted the issue3251 branch July 2, 2024 12:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants