feat(library/simplifier): add support for 'permutation' rewrite rules

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/simplifier/simplifier.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "library/expr_pair.h"
 #include "library/hop_match.h"
+#include "library/expr_lt.h"
 #include "library/simplifier/rewrite_rule_set.h"
 
 #ifndef LEAN_SIMPLIFIER_PROOFS
@@ -477,6 +478,14 @@ class simplifier_fn {
         return true;
     }
 
+    bool sorted_args(unsigned num, expr const * args) {
+        for (unsigned i = 1; i < num; i++) {
+            if (!is_lt(args[i-1], args[i], false))
+                return false;
+        }
+        return true;
+    }
+
     /**
        \brief Auxiliary function used by m_match_fn, it tries to match the given rule and
        the expression in the temporary field \c m_target.
@@ -491,6 +500,8 @@ class simplifier_fn {
             m_new_args.clear();
             m_new_args.resize(num+1);
             if (found_all_args(num)) {
+                if (rule.is_permutation() && sorted_args(num, m_new_args.begin()+1))
+                    return false;
                 // easy case: all arguments found
                 m_new_rhs   = instantiate(rule.get_rhs(), num, m_new_args.data() + 1);
                 if (m_proofs_enabled) {

tests/lean/simp6.lean

@@ -0,0 +1,8 @@
+variables a b : Nat
+rewrite_set simple
+add_rewrite Nat::add_comm eq_id : simple
+
+(*
+local t = parse_lean("a + b = b + a")
+print(simplify(t, 'simple'))
+*)

tests/lean/simp6.lean.expected.out

@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: b
+⊤	trans (congr2 (eq (a + b)) (Nat::add_comm b a)) (eq_id (a + b))