Merge branch 'add/shuffle' into 'master'

Add shuffle rule

See merge request !17

spec/changelog.tex

@@ -18,6 +18,8 @@ Proof rules:
   \item Addition of the \proofRule{bind_let} rule.  This rule can be used to
         preprocess \inlineAlethe{let} expressions similar to the \proofRule{bind}
         rule used with ordinary quantifiers.
+  \item Additon of the \proofRule{shuffle} to permute the arguments of a
+        commutative operator.
 \end{itemize}
 
 \noindent

spec/rule_list.tex

@@ -256,12 +256,13 @@ simplifications.}
 \ruleref{la_mult_neg} & Multiplication with a negative factor.\\
 \ruleref{symm}     & Symmetry of equality. \\
 \ruleref{not_symm} & Symmetry of not-equal.\\
-\ruleref{reordering} & Reording of the literals in a clause.\\
+\ruleref{reordering} & Permutation of the literals in a clause.\\
+\ruleref{shuffle} & Permutation of the arguments of a commutative operator.\\
 \end{xltabular}
 
 \begin{xltabular}{\linewidth}{l X}
 \caption{Rules used by the Carcara elaborator.}
-\label{rule-tab:cvc5}\\
+\label{rule-tab:carcara}\\
   Rule & Description \\
   \hline
 \ruleref{weakening} & Weakening of a clause. \\
@@ -486,7 +487,7 @@ A simple \proofRule{la_generic} step in the logic \textsf{LRA} might look like t
     :rule la_generic :args (1.0 -1.0))
 \end{AletheVerb}
 
-To verify this we have to check the insatisfiability of $(f\,a) > (f\,b) \land
+To verify this we have to check the unsatisfiability of $(f\,a) > (f\,b) \land
 (f\,a) ≈ (f\,b)$ (step 2). After step~3 we get $(f\,a) - (f\,b) > 0 \land
 (f\,a) - (f\,b) ≈ 0$. Since we don't have an integer sort in this logic step~4 does
 not apply. Finally, after step~5 the conjunction is $(f\,a) - (f\,b) > 0 \land
@@ -865,6 +866,26 @@ are the same.  That is, the conclusion of the rule is a reordering of the
 literals in the premise.
 \end{RuleDescription}
 
+\begin{RuleDescription}{shuffle}
+
+\begin{AletheXS}
+$i$. & \ctxsep  & $\Gamma$  &
+      $\circ\ t_1 \dots t_n ≈ \circ\ u_1 \dots u_n $ & \currule \\
+\end{AletheXS}
+
+where $\circ$ is a commutative operator, and
+the multisets $\{t_1, \cdots, t_n\}$ and $\{u_1, \cdots, u_n\}$
+are the same.
+
+In the logics currently supported
+by Alethe $\circ \in\{+, *, \land, \lor\}$.
+
+\ruleparagraph{Remark.} To permute the literals in a clause the
+\proofRule{reordering} rule can be used.
+
+\end{RuleDescription}
+
+
 \begin{RuleDescription}{not_and}
 \begin{AletheX}
 $i$. & \ctxsep & $\neg (\varphi_1 \land \dots \land \varphi_n)$ & ($\dots$) \\