From 54748b6bcea1ed7552a02824edea653512a797cd Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Mon, 12 Aug 2024 12:11:49 -0500
Subject: [PATCH] Make the description of the comp_simplify rule clearer
By changing the variable names we clarify that those are rules
that can match.
Furthermore, we also change all occurrences of the very awkward
"as long as possible" to "until a fixed point is reached".
---
spec/rule_list.tex | 123 +++++++++++++++++++++++----------------------
1 file changed, 63 insertions(+), 60 deletions(-)
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 26b3b84..d6b6be1 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -110,7 +110,7 @@ to quickly find the definition of rules.
Rule & Description \\
\hline
\ruleref{la_generic} & Tautologous disjunction of linear inequalities. \\
-\ruleref{lia_generic} & Tautologous disjunction of linear integer inequalities. \\
+\ruleref{KIA_generic} & Tautologous disjunction of linear integer inequalities. \\
\ruleref{la_disequality} & $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \\
\ruleref{la_totality} & $t_1 \leq t_2 \lor t_2 \leq t_1$ \\
\ruleref{la_tautology} & A trivial linear tautology. \\
@@ -573,20 +573,20 @@ as for the rule \proofRule{la_generic}.
Either of the form:
- \begin{AletheX}
- $i$. & \ctxsep &
- $(t_1 > 0 \wedge t_2 \bowtie t_3) \to t_1 * t_2 \bowtie t_1 * t_3$
- & (\currule) \\
- \end{AletheX}
+ \begin{AletheX}
+ $i$. & \ctxsep &
+ $(t_1 > 0 \wedge t_2 \bowtie t_3) \to t_1 * t_2 \bowtie t_1 * t_3$
+ & (\currule) \\
+ \end{AletheX}
with $\bowtie \in \{<,>, \le,\ge, ≈\}$.\\
\noindent Or of the form:
\begin{AletheX}
- $i$. & \ctxsep &
- $(t_1 > 0 \land \neg (t_2 ≈ t_3)) \rightarrow \neg (t_1 * t_2 ≈ t_1 * t_3)$
- & (\currule) \\
+ $i$. & \ctxsep &
+ $(t_1 > 0 \land \neg (t_2 ≈ t_3)) \rightarrow \neg (t_1 * t_2 ≈ t_1 * t_3)$
+ & (\currule) \\
\end{AletheX}
\end{RuleDescription}
@@ -595,35 +595,35 @@ with $\bowtie \in \{<,>, \le,\ge, ≈\}$.\\
Either of the form:
- \begin{AletheX}
- $i$. & \ctxsep &
- $(t_1 < 0 \land t_2 \bowtie t_3) \rightarrow t_1 * t_2 \bowtie_{inv} t_1 * t_3$
- & (\currule) \\
- \end{AletheX}
-
- with $\bowtie \in \{<,>, \le,\ge, ≈\}$ and $\bowtie_{inv}$ being defined according to the following table.
-
- \begin{center}
- \begin{tabular}{|c | c|}
- \hline
- $\bowtie$ & $\bowtie_{inv}$ is defined as: \\
- \hline
- $ < $ & $ > $ \\
- $ \le $ & $ \ge $ \\
- $ ≈ $ & $ ≈ $ \\
- $ > $ & $ < $ \\
- $ \ge $ & $ \le $ \\
- \hline
- \end{tabular}
- \end{center}
+ \begin{AletheX}
+ $i$. & \ctxsep &
+ $(t_1 < 0 \land t_2 \bowtie t_3) \rightarrow t_1 * t_2 \bowtie_{inv} t_1 * t_3$
+ & (\currule) \\
+ \end{AletheX}
+
+ with $\bowtie \in \{<,>, \le,\ge, ≈\}$ and $\bowtie_{inv}$ being defined according to the following table.
+
+ \begin{center}
+ \begin{tabular}{|c | c|}
+ \hline
+ $\bowtie$ & $\bowtie_{inv}$ is defined as: \\
+ \hline
+ $ < $ & $ > $ \\
+ $ \le $ & $ \ge $ \\
+ $ ≈ $ & $ ≈ $ \\
+ $ > $ & $ < $ \\
+ $ \ge $ & $ \le $ \\
+ \hline
+ \end{tabular}
+ \end{center}
\noindent Or of the form:
- \begin{AletheX}
- $i$. & \ctxsep &
- $(t_1 < 0 \land \neg (t_2 ≈ t_3)) \rightarrow \neg (t_1 * t_2 ≈ t_1 * t_3)$
- & (\currule) \\
- \end{AletheX}
+ \begin{AletheX}
+ $i$. & \ctxsep &
+ $(t_1 < 0 \land \neg (t_2 ≈ t_3)) \rightarrow \neg (t_1 * t_2 ≈ t_1 * t_3)$
+ & (\currule) \\
+ \end{AletheX}
\end{RuleDescription}
\begin{RuleDescription}{bind}
@@ -1115,7 +1115,7 @@ $i$. & \ctxsep & $\Gamma$ &
\begin{RuleDescription}{and_simplify}
This rule simplifies an $\land$ term by applying equivalence-preserving
-transformations as long as possible. Hence, the general form is
+transformations until a fixed point is reached. Hence, the general form is
\begin{AletheXS}
$i$. & \ctxsep & $\Gamma$ & $\varphi_1\land \cdots\land\varphi_n ≈ \psi$ & \currule \\
@@ -1144,7 +1144,7 @@ The possible transformations are:
\begin{RuleDescription}{or_simplify}
This rule simplifies an $\lor$ term by applying equivalence-preserving
-transformations as long as possible. Hence, the general form is
+transformations until a fixed point is reached. Hence, the general form is
\begin{AletheXS}
$i$. & \ctxsep & $\Gamma$ & $(\varphi_1\lor \cdots\lor\varphi_n) ≈ \psi$ & \currule \\
@@ -1173,7 +1173,7 @@ The possible transformations are:
\begin{RuleDescription}{not_simplify}
This rule simplifies an $\neg$ term by applying equivalence-preserving
-transformations as long as possible. Hence, the general form is
+transformations until a fixed point is reached. Hence, the general form is
\begin{AletheXS}
$i$. & \ctxsep & $\Gamma$ & $\neg\varphi ≈ \psi$ & \currule \\
@@ -1190,7 +1190,7 @@ The possible transformations are:
\begin{RuleDescription}{implies_simplify}
This rule simplifies an $\rightarrow$ term by applying equivalence-preserving
-transformations as long as possible. Hence, the general form is
+transformations until a fixed point is reached. Hence, the general form is
\begin{AletheXS}
$i$. & \ctxsep & $\Gamma$ & $\varphi_1\rightarrow \varphi_2 ≈ \psi$ & \currule \\
@@ -1213,7 +1213,7 @@ The possible transformations are:
\begin{RuleDescription}{equiv_simplify}
This rule simplifies a formula with the head symbol $≈\,: \lsymb{Bool}\,\lsymb{Bool}\,\lsymb{Bool}$
by applying equivalence-preserving
-transformations as long as possible. Hence, the general form is
+transformations until a fixed point is reached. Hence, the general form is
\begin{AletheXS}
$i$. & \ctxsep & $\Gamma$ & $(\varphi_1≈ \varphi_2) ≈ \psi$ & \currule \\
@@ -1235,7 +1235,7 @@ The possible transformations are:
\begin{RuleDescription}{bool_simplify}
This rule simplifies a boolean term by applying equivalence-preserving
-transformations as long as possible. Hence, the general form is
+transformations until a fixed point is reached. Hence, the general form is
\begin{AletheXS}
$i$. & \ctxsep & $\Gamma$ & $\varphi≈ \psi$ & \currule \\
@@ -1379,7 +1379,7 @@ $i$. & \ctxsep & $\Gamma$ & $Q x_1, \dots, x_n.\,\varphi ≈ Q x_{k_1}, \dots, x
\begin{RuleDescription}{eq_simplify}
This rule simplifies an $≈$ term by applying equivalence-preserving
- transformations as long as possible. Hence, the general form is
+ transformations until a fixed point is reached. Hence, the general form is
\begin{AletheXS}
$i$. & \ctxsep & $\Gamma$ & $(t_1≈ t_2) ≈ \varphi$ & \currule \\
@@ -1413,7 +1413,7 @@ The possible transformations are:
\begin{RuleDescription}{prod_simplify}
This rule simplifies a product by applying equivalence-preserving
-transformations as long as possible. The general form is
+transformations until a fixed point is reached. The general form is
\begin{AletheXS}
$i$. & \ctxsep & $\Gamma$ & $t_1\times\cdots\times t_n ≈ u$ & \currule \\
@@ -1470,7 +1470,7 @@ The possible transformations are:
\begin{RuleDescription}{sum_simplify}
This rule simplifies a sum by applying equivalence-preserving
-transformations as long as possible. The general form is
+transformations until a fixed point is reached. The general form is
\begin{AletheXS}
$i$. & \ctxsep & $\Gamma$ & $t_1+\cdots+t_n ≈ u$ & \currule \\
@@ -1494,27 +1494,30 @@ The possible transformations are:
\begin{RuleDescription}{comp_simplify}
This rule simplifies a comparison by applying equivalence-preserving
-transformations as long as possible. The general form is
+transformations until a fixed point is reached. The general form is
\begin{AletheXS}
-$i$. & \ctxsep & $\Gamma$ & $t_1 \bowtie t_n ≈ \psi$ & \currule \\
+$i$. & \ctxsep & $\Gamma$ & $t_1 \bowtie t_2 ≈ \psi$ & \currule \\
\end{AletheXS}
-where $\bowtie$ is as for the proof rule \proofRule{la_generic}, but never
-$≈$.
+where $\bowtie \in \{<, >, \leq, \geq\}$.
-The possible transformations are:
+The following transformation rules are used to simplify $t_1 \bowtie t_2$:
\begin{itemize}
- \item $t_1 < t_2 ⇒ \varphi$ where $t_1$ and
- $t_2$ are numerical constants and $\varphi$ is $\top$ if $t_1$ is
- strictly greater than $t_2$ and $\bot$ otherwise.
- \item $t < t ⇒ \bot$
- \item $t_1 \leq t_2 ⇒ \varphi$ where $t_1$ and
- $t_2$ are numerical constants and $\varphi$ is $\top$ if $t_1$ is
- greater than $t_2$ or equal and $\bot$ otherwise.
- \item $t \leq t ⇒ \top$
- \item $t_1 \geq t_2 ⇒ t_2 \leq t_1$
- \item $t_1 < t_2 ⇒ \neg (t_2 \leq t_1)$
- \item $t_1 > t_2 ⇒ \neg (t_1 \leq t_2)$
+ \item $s_1 < s_2 ⇒ \top$ if $s_1, s_2$ are numerical constants and
+ $s_1$ is strictly less than $s_2$
+ \item $s_1 < s_2 ⇒ \bot$ if $s_1, s_2$ are numerical constants and
+ $s_1$ is greater or equal than $s_2$
+
+ \item $s_1 \leq s_2 ⇒ \top$ if $s_1, s_2$ are numerical constants and
+ $s_1$ is less or equal than $s_2$
+ \item $s_1 \leq s_2 ⇒ \bot$ if $s_1, s_2$ are numerical constants and
+ $s_1$ is strictly greater than $s_2$
+
+ \item $s < s ⇒ \bot$
+ \item $s \leq s ⇒ \top$
+ \item $s_1 \geq s_2 ⇒ s_2 \leq s_1$
+ \item $s_1 < s_2 ⇒ \neg (s_2 \leq s_1)$
+ \item $s_1 > s_2 ⇒ \neg (s_1 \leq s_2)$
\end{itemize}
\end{RuleDescription}
--
GitLab