feat(library/blast/simplifier): rewrite with tmp locals

src/library/blast/simplifier.cpp

@@ -98,6 +98,7 @@ class simplifier {
     name                                         m_rel;
 
     list<expr>                                   m_local_ctx;
+    simp_rule_sets                               m_ctx_srss;
 
     /* Logging */
     unsigned                                     m_num_steps{0};
@@ -129,6 +130,17 @@ class simplifier {
         return has_free_vars(binding_body(f_type));
     }
 
+    simp_rule_sets add_to_srss(simp_rule_sets const & _srss, buffer<expr> & ls) {
+        simp_rule_sets srss = _srss;
+        for (unsigned i = 0; i < ls.size(); i++) {
+            // TODO assert no metas?
+            expr & l = ls[i];
+            tmp_type_context tctx(env(),ios());
+            srss = add(tctx,srss,mlocal_name(l),tctx.infer(l),l);
+        }
+        return srss;
+    }
+
     /* Results */
     result lift_from_eq(expr const & x, result const & r);
     result join(result const & r1, result const & r2);        
@@ -143,9 +155,9 @@ class simplifier {
     result simplify_fun(expr const & e);
     
     /* Rewriting */
-    result rewrite(expr const & e);    
+    result rewrite(expr const & e);
+    result rewrite(expr const & e, simp_rule_sets const & srss);        
     result rewrite(expr const & e, simp_rule const & sr);
-    void init_tmp_tctx_for(simp_rule_core const & sr);
 
     /* Congruence */
     result congr(result const & r_f, result const & r_arg);        
@@ -168,6 +180,7 @@ simplifier::simplifier(branch const & b, name const & rel):
     m_app_builder(*m_tmp_tctx), m_branch(b), m_rel(rel) { }
 
 /* Cache */
+
 optional<result> simplifier::cache_lookup(expr const & e) {
     simplify_cache & cache = m_simplify_caches[m_rel];
     auto it = cache.find(e);
@@ -179,7 +192,6 @@ void simplifier::cache_save(expr const & e, result const & r) {
     cache.insert(mk_pair(e,r));
 }
 
-
 /* Results */
 
 result simplifier::lift_from_eq(expr const & x, result const & r) {
@@ -375,29 +387,29 @@ result simplifier::simplify_fun(expr const & e) {
 
 result simplifier::rewrite(expr const & e) {
     result r(e);
+    while (true) {
+        result r_ctx = rewrite(r.get_new(),m_ctx_srss);
+        result r_new = rewrite(r_ctx.get_new(),get_simp_rule_sets(env()));
+        if (r_ctx.is_none() && r_new.is_none()) break;
+        r = join(join(r,r_ctx),r_new);
+    }
+    return r;
+}
 
-    /* First, we rewrite with local hypotheses */
-    //TODO
-
-    /* Next, we rewrite with the [simp_rule_set] */
-    simp_rule_set const * sr = get_simp_rule_sets(env()).find(m_rel);
+result simplifier::rewrite(expr const & e, simp_rule_sets const & srss) {
+    result r(e);
+    
+    simp_rule_set const * sr = srss.find(m_rel);
     if (!sr) return r;
 
     list<simp_rule> const * srs = sr->find_simp(e);
     if (!srs) return r;
 
-    bool modified = true;
-    while (modified) {
-        modified = false;
-        for_each(*srs,[&](simp_rule const & sr) {
-                result r_rew = rewrite(r.get_new(),sr);
-                if (r_rew.is_none()) return;
-                r = join(r,r_rew);
-                modified = true;
-            }
-            );
-    }
-    
+    for_each(*srs,[&](simp_rule const & sr) {
+            result r_new = rewrite(r.get_new(),sr);
+            if (r_new.is_none()) return;
+            r = join(r,r_new);
+        });
     return r;
 }
 
@@ -407,9 +419,11 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
     if (!tmp_tctx->is_def_eq(e,sr.get_lhs())) return result(e);
 
     if (m_trace) {
-        ios().get_diagnostic_channel() << "[" << sr.get_id() << "]\n";
+        expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
+        expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
+        ios().get_diagnostic_channel() << "[" << sr.get_lhs() << " =?= " << sr.get_rhs() << "] ==> ";        
+        ios().get_diagnostic_channel() << "[" << new_lhs << " =?= " << new_rhs << "]\n";
     }
-    
 
     /* Traverse metavariables backwards */
     for (int i = sr.get_num_emeta() - 1; i >= 0; --i) {
@@ -428,11 +442,18 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
 
         if (tmp_tctx->is_mvar_assigned(i)) continue;
 
+        // TODO REMOVE DEBUG
+        expr m_assigned = tmp_tctx->instantiate_uvars_mvars(m);
+
         if (tmp_tctx->is_prop(tmp_tctx->infer(m))) {
             // TODO try to prove
             return result(e);
         }
 
+        if (m_trace) {
+            ios().get_diagnostic_channel() << "failed to assign: " << m << "\n";
+        }
+
         /* We fail if there is a meta variable that we still cannot assign */
         return result(e);
     }
@@ -516,7 +537,8 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
     if (!tmp_tctx->is_def_eq(e,cr.get_lhs())) return result(e);
 
     if (m_trace) {
-        ios().get_diagnostic_channel() << "<" << cr.get_id() << ">\n";
+        ios().get_diagnostic_channel() << "<" << cr.get_id() << "> " 
+                                       << e << " === " << cr.get_lhs() << "\n";
     }
     
     /* First, iterate over the congruence hypotheses */
@@ -531,7 +553,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
         while (is_pi(m_type)) {
             expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data());
             expr l = tmp_tctx->mk_tmp_local(d,binding_info(e));
-            ls.push_back(tmp_tctx->instantiate_uvars_mvars(l));
+            ls.push_back(l);
             m_type = instantiate(binding_body(m_type),l);
         }
 
@@ -539,10 +561,14 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
         bool valid = is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel);
         lean_assert(valid);
         {
+            simplify_caches fresh_caches;            
+            flet<simplify_caches> set_simplify_caches(m_simplify_caches,fresh_caches);            
             flet<name> set_name(m_rel,const_name(h_rel));
-            flet<list<expr> > set_local_ctx(m_local_ctx,append(m_local_ctx,to_list(ls)));
-            simplify_caches fresh_caches;
-            flet<simplify_caches> set_simplify_caches(m_simplify_caches,fresh_caches);
+            
+            buffer<expr> ls_instantiated;
+            for (unsigned i = 0; i < ls.size(); i++) ls_instantiated.push_back(tmp_tctx->instantiate_uvars_mvars(ls[i]));
+            
+            flet<simp_rule_sets> set_ctx_srss(m_ctx_srss,add_to_srss(m_ctx_srss,ls_instantiated));
             
             h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
             result r_congr_hyp = simplify(h_lhs);
@@ -554,11 +580,14 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
                 hyp = r_congr_hyp.get_proof();
                 simplified = true;
             }
-            hyp = Fun(ls,hyp);
+
+            hyp = Fun(ls_instantiated,hyp);
             if (!tmp_tctx->is_def_eq(m,hyp)) failed = true;
         }
         });
+    
     if (failed || !simplified) return result(e);
+    
     /* Traverse metavariables backwards, proving or synthesizing the rest */
     for (int i = cr.get_num_emeta() - 1; i >= 0; --i) {
         expr const & m = cr.get_emeta(i);
@@ -581,6 +610,11 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
             return result(e);
         }
 
+        if (m_trace) {
+            ios().get_diagnostic_channel() << "failed to assign: " << tmp_tctx->instantiate_uvars_mvars(m) << " : "
+                                           << tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)) << "\n";
+        }
+
         /* We fail if there is a meta variable that we still cannot assign */
         return result(e);
     }

tests/lean/simplifier1.lean

@@ -4,13 +4,7 @@ constant T : Type.{l}
 constants (x y z : T) (f g h : T → T) 
 constants (Hfxgy : f x = g y) (Hgyhz : g y = h z)
 
-#simplify eq 2 (f x) -- f x
-
 attribute Hfxgy [simp]
+#simplify eq 2 (f x)
 attribute Hgyhz [simp]
-
-set_option simplify.exhaustive false
-#simplify eq 2 (f x) -- g y
-
-set_option simplify.exhaustive true
-#simplify eq 2 (f x) -- h z
+#simplify eq 2 (f x)

tests/lean/simplifier1.lean.expected.out

@@ -1,3 +1,2 @@
-<refl>
 f x = g y
 f x = h z

tests/lean/simplifier2.lean

@@ -5,11 +5,7 @@ constants (x y z : T) (f g h : T → T)
 constants (Hfxgy : f x = g y) (Hgyhz : g y = h z)
 
 attribute Hfxgy [simp]
-attribute Hgyhz [simp]
-
-set_option simplify.exhaustive false
 #simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), g y
-
-set_option simplify.exhaustive true
+attribute Hgyhz [simp]
 #simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), h z
 

tests/lean/simplifier3.lean

@@ -7,17 +7,12 @@ constant T : Type.{l}
 constants (x y z : T → T) (f g h : (T →  T) → (T →  T)) (a b c : T)
 constants (Hfxgy : f x = g y) (Hgyhz : g y = h z) (Hab : a = b) (Hbc : b = c)
 
-#simplify eq 2 (f x a) -- f x a
 
 attribute Hfxgy [simp]
 attribute Hgyhz [simp]
 attribute Hab [simp]
 attribute Hbc [simp]
 
-set_option simplify.exhaustive false
-#simplify eq 2 (f x a) -- g y b
-
-set_option simplify.exhaustive true
 #simplify eq 2 (f x a) -- h z c
 
 end test_congr

tests/lean/simplifier3.lean.expected.out

@@ -1,4 +1,2 @@
-<refl>
-f x a = g y b
 f x a = h z c
 f x = g x

tests/lean/simplifier9.lean

@@ -0,0 +1,27 @@
+-- Rewriting with (tmp)-local hypotheses
+import logic.quantifiers
+
+universe l
+constants (T : Type.{l}) (P Q : T → Prop) 
+
+set_option simplify.max_steps 50000
+constants (x y : T)
+
+#simplify iff 0 x = y →  x = y
+#simplify iff 0 T → x = y →  x = y
+#simplify iff 0 ∀ z : T, x = z → x = y
+#simplify iff 0 ∀ z : T, z = x → x = z
+#simplify iff 0 ∀ (z w : T), x = y →  x = y
+#simplify iff 0 ∀ (z w : T), x = y →  P x
+
+#simplify iff 0 ∀ (H : ∀ x, P x ↔ Q x), P x
+#simplify iff 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x) (q : Prop), P x
+
+#simplify iff 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x), p ∨ P x
+#simplify iff 0 (∀ (x : T), P x ↔ Q x) →  P x
+#simplify iff 0 (∀ (x : T), P x ↔ Q x) →  P x
+#simplify iff 0 ∀ (x y : T), (∀ (x : T), P x ↔ Q x) →  P x
+
+#simplify iff 0 ∀ (x z : T), x = z → (∀ (w : T), P w ↔ Q w) →  P x
+
+