Add shuffle rule
This adds a shuffle rule to Alethe that can be used to change the order of arguments of commutative operators. Two remarks:
- Reconstruction might be easier if steps using this rules come with a permutation in the arguments. So for example:
(step s1 (= (cl (+ a b c) (+ b a c)) :rule shuffle :args (2 1 3))However, I am not certain of hard it is to generate this. I suggest we think about adding this after Hanna used this rule.
- We should consider renaming
reorderingtoshuffle_clause. In the proofs meeting yesterday we said that "reorder" is not a good name, because it implies a specific order.
Merge request reports
Activity
mentioned in commit c9505bb8
865 866 literals in the premise. 866 867 \end{RuleDescription} 867 868 869 \begin{RuleDescription}{shuffle} 870 871 \begin{AletheXS} 872 $i$. & \ctxsep & $\Gamma$ & 873 $\circ\ t_1 \dots t_n ≈ \circ\ u_1 \dots u_n $ & \currule \\ 874 \end{AletheXS} 875 876 where $\circ$ is a commutative operator, and 877 the multisets $\{t_1, \cdots, t_n\}$ and $\{u_1, \cdots, u_n\}$ 878 are the same. 879 880 In the logics currently supported 881 by Alethe $\circ \in\{+, *, \land, \lor\}$. mentioned in commit 31d52ce0
Oehm I accidentally merged this, let me know (especially @hbarbosa) if you want me to reverse this.
It's pretty easy to generate the permutation. Once upon a time when we were printing Lean proofs out of cvc5 the rule corresponding to
reorderwas giving the permutation, with the permutation being generating during the translation of the proof node. The same could be done in the Alethe translator.As for the name, it sounds fine to me. As for the current
reorderrule, we could afterwards remove that rule by makingshufflealso work for clauses? I think that'd be fine.Edited by Haniel Barbosa
Would those permutations help the reconstruction?
Regarding the
reorderingrule: we can't really unify those since the conclusion ofshuffleis an equality which we can't have between clauses. Alsoreorderingtakes a the clause as a premise and returns the shuffled clause as its conclusion.Oh, I missed that detail. Best keep them separate indeed.
As for helping reconstruction, I think it depends on how one is representing the clause. At the time when this was relevant to how we were doing reconstruction in Lean, it did help. I do not quite remember if it'd help with the way it is done now there.
