feat(library/simplifier): add support for metavariables in conditional rewrite rules

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

src/library/simplifier/ceq.cpp

@@ -22,8 +22,9 @@ bool is_ceq(ro_environment const & env, expr e);
    \brief Auxiliary functional object for creating "conditional equations"
 */
 class to_ceqs_fn {
-    ro_environment const & m_env;
+    ro_environment const &           m_env;
-    unsigned               m_idx;
+    optional<ro_metavar_env> const & m_menv;
+    unsigned                         m_idx;
 
     static list<expr_pair> mk_singleton(expr const & e, expr const & H) {
         return list<expr_pair>(mk_pair(e, H));
@@ -33,6 +34,10 @@ class to_ceqs_fn {
         return m_env->imported("if_then_else");
     }
 
+    expr lift_free_vars(expr const & e, unsigned d) {
+        return ::lean::lift_free_vars(e, d, m_menv);
+    }
+
     name mk_aux_name() {
         if (m_idx == 0) {
             m_idx = 1;
@@ -114,15 +119,15 @@ class to_ceqs_fn {
         }
     }
 public:
-    to_ceqs_fn(ro_environment const & env):m_env(env), m_idx(0) {}
+    to_ceqs_fn(ro_environment const & env, optional<ro_metavar_env> const & menv):m_env(env), m_menv(menv), m_idx(0) {}
 
     list<expr_pair> operator()(expr const & e, expr const & H) {
         return filter(apply(e, H), [&](expr_pair const & p) { return is_ceq(m_env, p.first); });
     }
 };
 
-list<expr_pair> to_ceqs(ro_environment const & env, expr const & e, expr const & H) {
+list<expr_pair> to_ceqs(ro_environment const & env, optional<ro_metavar_env> const & menv, expr const & e, expr const & H) {
-    return to_ceqs_fn(env)(e, H);
+    return to_ceqs_fn(env, menv)(e, H);
 }
 
 bool is_ceq(ro_environment const & env, expr e) {
@@ -230,7 +235,10 @@ bool is_permutation_ceq(expr e) {
 
 static int to_ceqs(lua_State * L) {
     ro_shared_environment env(L, 1);
-    auto r = to_ceqs(env, to_expr(L, 2), to_expr(L, 3));
+    optional<ro_metavar_env> menv;
+    if (!lua_isnil(L, 2))
+        menv = to_metavar_env(L, 2);
+    auto r = to_ceqs(env, menv, to_expr(L, 3), to_expr(L, 4));
     lua_newtable(L);
     int i = 1;
     for (auto p : r) {

src/library/simplifier/ceq.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/lua.h"
 #include "kernel/environment.h"
+#include "kernel/metavar.h"
 #include "library/expr_pair.h"
 namespace lean {
 /**
@@ -26,7 +27,7 @@ namespace lean {
    \remark if the left-hand-side of an equation does not contain all variables, then it is
    discarded. That is, all elements in the resultant list satisfy the predicate \c is_ceq.
 */
-list<expr_pair> to_ceqs(ro_environment const & env, expr const & e, expr const & H);
+list<expr_pair> to_ceqs(ro_environment const & env, optional<ro_metavar_env> const & menv, expr const & e, expr const & H);
 /**
    \brief Return true iff \c e is a conditional equation.
 

src/library/simplifier/rewrite_rule_set.cpp

@@ -25,9 +25,9 @@ rewrite_rule_set::rewrite_rule_set(rewrite_rule_set const & other):
     m_env(other.m_env), m_rule_set(other.m_rule_set), m_disabled_rules(other.m_disabled_rules), m_congr_thms(other.m_congr_thms) {}
 rewrite_rule_set::~rewrite_rule_set() {}
 
-void rewrite_rule_set::insert(name const & id, expr const & th, expr const & proof) {
+void rewrite_rule_set::insert(name const & id, expr const & th, expr const & proof, optional<ro_metavar_env> const & menv) {
     ro_environment env(m_env);
-    for (auto const & p : to_ceqs(env, th, proof)) {
+    for (auto const & p : to_ceqs(env, menv, th, proof)) {
         expr const & ceq   = p.first;
         expr const & proof = p.second;
         bool is_perm       = is_permutation_ceq(ceq);
@@ -48,7 +48,7 @@ void rewrite_rule_set::insert(name const & th_name) {
     ro_environment env(m_env);
     auto obj = env->find_object(th_name);
     if (obj && (obj->is_theorem() || obj->is_axiom())) {
-        insert(th_name, obj->get_type(), mk_constant(th_name));
+        insert(th_name, obj->get_type(), mk_constant(th_name), none_ro_menv());
     } else {
         throw exception(sstream() << "'" << th_name << "' is not a theorem nor an axiom");
     }

src/library/simplifier/rewrite_rule_set.h

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/splay_tree.h"
 #include "util/name.h"
 #include "kernel/environment.h"
+#include "kernel/metavar.h"
 #include "kernel/formatter.h"
 #include "library/io_state_stream.h"
 #include "library/simplifier/congr.h"
@@ -59,7 +60,7 @@ public:
        \brief Convert the theorem \c th with proof \c proof into conditional rewrite rules, and
        insert the rules into this rule set. The new rules are tagged with the given \c id.
     */
-    void insert(name const & id, expr const & th, expr const & proof);
+    void insert(name const & id, expr const & th, expr const & proof, optional<ro_metavar_env> const & menv);
 
     /**
        \brief Convert the theorem/axiom named \c th_name in the environment into conditional rewrite rules,

src/library/simplifier/simplifier.cpp

@@ -184,7 +184,7 @@ class simplifier_cell::imp {
         updt_rule_set(imp & fn, expr const & H):
             m_fn(fn), m_old(m_fn.m_rule_sets[0]), m_reset_cache(m_fn.m_cache) {
             lean_assert(const_type(H));
-            m_fn.m_rule_sets[0].insert(g_local, *const_type(H), H);
+            m_fn.m_rule_sets[0].insert(g_local, *const_type(H), H, m_fn.m_menv.to_some_menv());
         }
         ~updt_rule_set() {
             m_fn.m_rule_sets[0] = m_old;

src/library/tactic/simplify_tactic.cpp

@@ -43,7 +43,7 @@ static optional<proof_state> simplify_tactic(ro_environment const & env, io_stat
         for (auto const & p : g.get_hypotheses()) {
             if (tc.is_proposition(p.second, context(), menv)) {
                 expr H = mk_constant(p.first, p.second);
-                rs.insert(g_assumption, p.second, H);
+                rs.insert(g_assumption, p.second, H, some_ro_menv(menv));
             }
         }
     }

tests/lua/ceq1.lua

@@ -11,7 +11,7 @@ end
 
 function test_ceq(name, expected, is_perm)
    local obj = env:find_object(name)
-   local r   = to_ceqs(env, obj:get_type(), Const(name))
+   local r   = to_ceqs(env, nil, obj:get_type(), Const(name))
    show_ceqs(r)
    assert(#r == expected)
    if is_perm ~= nil then