From 4b8bf6b6e89d863c9693936203fa6193024cd2ae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hans-J=C3=B6rg?= <commits@schurr.at>
Date: Wed, 4 Dec 2024 22:50:20 +0000
Subject: [PATCH] Add shuffle rule

---
 spec/changelog.tex |  2 ++
 spec/rule_list.tex | 27 ++++++++++++++++++++++++---
 2 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/spec/changelog.tex b/spec/changelog.tex
index aa8b02b..03fd55b 100644
--- a/spec/changelog.tex
+++ b/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
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 386f60d..d31df1a 100644
--- a/spec/rule_list.tex
+++ b/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$) \\
-- 
GitLab