feat(library/blast/simplifier): conditional rewriting

src/frontends/lean/builtin_cmds.cpp

@@ -1335,6 +1335,7 @@ static environment simplify_cmd(parser & p) {
     }
     else {
         auto tc = mk_type_checker(p.env(), p.mk_ngen());
+        
         expr pf_type = tc->check(r.get_proof(), ls).first;
 
         if (o == 0) p.regular_stream() << r.get_new() << endl;

src/library/blast/simplifier.cpp

@@ -97,7 +97,6 @@ class simplifier {
     branch                                       m_branch;
     name                                         m_rel;
 
-    list<expr>                                   m_local_ctx;
     simp_rule_sets                               m_ctx_srss;
 
     /* Logging */
@@ -250,7 +249,7 @@ result simplifier::simplify(expr const & e) {
     flet<unsigned> inc_depth(m_depth, m_depth+1);
 
     if (m_trace) {
-        ios().get_diagnostic_channel() << m_depth << "." << m_rel << "." << m_local_ctx << " " << e << "\n";
+        ios().get_diagnostic_channel() << m_depth << "." << m_rel << ": " << e << "\n";
     }
 
     if (m_num_steps > m_max_steps)
@@ -335,7 +334,6 @@ result simplifier::simplify_pi(expr const & e) {
 
 result simplifier::simplify_app(expr const & e) {
     lean_assert(is_app(e));
-    // TODO simplify operator as well, in cases (1) and (2)
     
     /* (1) Try user-defined congruences */
     result r = try_congrs(e);
@@ -419,8 +417,9 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
     if (m_trace) {
         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";
+        ios().get_diagnostic_channel()
+            << "REW(" << sr.get_id() << ") "
+            << "[" << new_lhs << " =?= " << new_rhs << "]\n";
     }
 
     /* Traverse metavariables backwards */
@@ -429,27 +428,39 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
         bool is_instance = sr.is_instance(i);
 
         if (is_instance) {
-            expr type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
-            if (auto v = tmp_tctx->mk_class_instance(type)) {
-                if (!tmp_tctx->force_assign(m, *v))
+            expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
+            if (auto v = tmp_tctx->mk_class_instance(m_type)) {
+                if (!tmp_tctx->force_assign(m, *v)) {
+                    if (m_trace) {
+                        ios().get_diagnostic_channel() << "unable to assign instance for: " << m_type << "\n";
+                    }
                     return result(e);
+                }
             } else {
+                if (m_trace) {
+                    ios().get_diagnostic_channel() << "unable to synthesize instance for: " << m_type << "\n";
+                }
                 return result(e);
             }
         }
 
         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);
+        expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
+        if (tmp_tctx->is_prop(m_type)) {
+            flet<name> set_name(m_rel,get_iff_name());
+            result r_cond = simplify(m_type);
+            if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) {
+                auto pf = m_app_builder.mk_app(name("iff","elim_right"),finalize(r_cond).get_proof(),mk_constant(get_true_intro_name()));
+                lean_assert(pf);
+                bool success = tmp_tctx->is_def_eq(m,*pf);
+                lean_assert(success);
+                continue;
+            }
         }
 
         if (m_trace) {
-            ios().get_diagnostic_channel() << "failed to assign: " << m << "\n";
+            ios().get_diagnostic_channel() << "failed to assign: " << m << " : " << m_type << "\n";
         }
 
         /* We fail if there is a meta variable that we still cannot assign */
@@ -460,16 +471,22 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
         if (!tmp_tctx->is_uvar_assigned(i)) return result(e);
     }
 
-    expr e_s = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
+    expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
+    expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
+
+    if (sr.is_perm()) {
+        if (!is_lt(new_rhs,new_lhs,false))
+            return result(e);
+    }
 
-    if (sr.is_perm() && !is_lt(e_s,e,false)) return result(e);
     expr pf = tmp_tctx->instantiate_uvars_mvars(sr.get_proof());
-    return result(result(e_s,pf));
+    return result(result(new_rhs,pf));
 }
 
 
 
 /* Congruence */
+
 result simplifier::congr(result const & r_f, result const & r_arg) {
     lean_assert(!r_f.is_none() && !r_arg.is_none());
     // theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂
@@ -546,11 +563,11 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
     for_each(congr_hyps,[&](expr const & m) {
         if (failed) return;
         buffer<expr> ls;
-        expr m_type = tmp_tctx->infer(m);
+        expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
 
         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));
+            expr l = tmp_tctx->mk_tmp_local(d,binding_info(m_type));
             ls.push_back(l);
             m_type = instantiate(binding_body(m_type),l);
         }
@@ -563,10 +580,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
             flet<simplify_caches> set_simplify_caches(m_simplify_caches,fresh_caches);            
             flet<name> set_name(m_rel,const_name(h_rel));
             
-            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));
+            flet<simp_rule_sets> set_ctx_srss(m_ctx_srss,add_to_srss(m_ctx_srss,ls));
             
             h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
             result r_congr_hyp = simplify(h_lhs);
@@ -579,8 +593,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
                 simplified = true;
             }
 
-            hyp = Fun(ls_instantiated,hyp);
-            if (!tmp_tctx->is_def_eq(m,hyp)) failed = true;
+            if (!tmp_tctx->is_def_eq(m,Fun(ls,hyp))) failed = true;
         }
         });
     

src/library/simplifier/ceqv.cpp

@@ -100,7 +100,7 @@ class to_ceqvs_fn {
             }
             if (is_standard(m_env) && is_prop(e)) {
                 expr new_e = mk_iff(e, mk_true());
-                expr new_H = mk_app(mk_constant(get_iff_true_intro_name()), arg1, H);
+                expr new_H = mk_app(mk_constant(get_iff_true_intro_name()), e, H);
                 return mk_singleton(new_e, new_H);
             } else {
                 return list<expr_pair>();

tests/lean/simplifier10.lean

@@ -0,0 +1,19 @@
+import logic.connectives logic.quantifiers
+
+universe l
+constants (T : Type.{l}) (x y z : T) (P : T → Prop) (Q : T → T → T → Prop) (R W V : T → T → Prop) 
+constants (px : P x) (wxz : W x z) (vzy : V z y)
+constants (H : ∀ (x y z : T), P x → W x z → V z y → (Q z y x ↔ R x y))
+attribute px [simp]
+attribute wxz [simp]
+attribute vzy [simp]
+attribute H [simp]
+
+#simplify iff 0 P x
+#simplify iff 0 W x z
+#simplify iff 0 V z y
+#simplify iff 0 Q z y x
+#simplify iff 0 V z y ↔ Q z y x
+
+
+

tests/lean/simplifier10.lean.expected.out

@@ -0,0 +1,5 @@
+true
+true
+true
+R x y
+R x y

tests/lean/simplifier11.lean

@@ -0,0 +1,74 @@
+-- Conditional congruence
+import logic.connectives logic.quantifiers
+
+namespace if_congr
+constants {A : Type} {b c : Prop} (dec_b : decidable b) (dec_c : decidable c)
+          {x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v)
+
+local attribute dec_b [instance]
+local attribute dec_c [instance]
+local attribute h_c [simp]
+local attribute h_t [simp]
+local attribute h_e [simp]
+
+attribute if_congr [congr]
+
+#simplify eq 0 (ite b x y)
+end if_congr
+
+namespace if_ctx_simp_congr
+constants {A : Type} {b c : Prop} (dec_b : decidable b)
+          {x y u v : A} (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v)
+
+local attribute dec_b [instance]
+local attribute h_c [simp]
+local attribute h_t [simp]
+local attribute h_e [simp]
+
+attribute if_ctx_simp_congr [congr]
+
+#simplify eq 0 (ite b x y)
+
+end if_ctx_simp_congr
+
+namespace if_congr_prop
+constants {b c x y u v : Prop} (dec_b : decidable b) (dec_c : decidable c)
+          (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v))
+
+local attribute dec_b [instance]
+local attribute dec_c [instance]
+local attribute h_c [simp]
+local attribute h_t [simp]
+local attribute h_e [simp]
+
+attribute if_congr_prop [congr]
+
+#simplify iff 0 (ite b x y)
+end if_congr_prop
+
+namespace if_ctx_simp_congr_prop
+constants (b c x y u v : Prop) (dec_b : decidable b)
+          (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬ c → (y ↔ v))
+
+local attribute dec_b [instance]
+local attribute h_c [simp]
+local attribute h_t [simp]
+local attribute h_e [simp]
+
+attribute if_ctx_simp_congr_prop [congr]
+#simplify iff 0 (ite b x y)
+
+end if_ctx_simp_congr_prop
+
+namespace if_simp_congr_prop
+constants (b c x y u v : Prop) (dec_b : decidable b)
+          (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v)
+
+local attribute dec_b [instance]
+local attribute h_c [simp]
+local attribute h_t [simp]
+local attribute h_e [simp]
+
+attribute if_simp_congr_prop [congr]
+#simplify iff 0 (ite b x y)
+end if_simp_congr_prop

tests/lean/simplifier11.lean.expected.out

@@ -0,0 +1,5 @@
+ite c u v
+ite c u v
+ite c u v
+ite c u v
+ite c u v

tests/lean/simplifier12.lean

@@ -0,0 +1,23 @@
+import algebra.ring
+open algebra
+
+set_option simplify.max_steps 1000
+universe l
+constants (T : Type.{l}) (s : algebra.comm_ring T)
+constants (x1 x2 x3 x4 : T) (f g : T → T)
+attribute s [instance]
+
+attribute add.comm [simp]
+attribute add.assoc [simp]
+attribute left_distrib [simp]
+attribute right_distrib [simp]
+
+attribute mul.comm [simp]
+attribute mul.assoc [simp]
+
+theorem add.o2 [simp] {A : Type} [s : add_comm_semigroup A] (a b c : A) :
+  a + (b + c) = b + (a + c) := sorry
+
+#simplify eq 0 x2 + (g x1 + (f x3 * 3 * (x2 + g x1 * 7) * x2)) + 5 * (x4 + f x1)
+
+

tests/lean/simplifier12.lean.expected.out

@@ -0,0 +1 @@
+x2 + (g x1 + (x4 * 5 + (f x1 * 5 + (x2 * (f x3 * (x2 * 3)) + x2 * (f x3 * (3 * (g x1 * 7)))))))

tests/lean/simplifier9.lean.expected.out

@@ -0,0 +1,13 @@
+x = y → y = y
+T → x = y → y = y
+∀ (x_1 : T), x = x_1 → x_1 = y
+∀ (x_1 : T), x_1 = x → x = x
+T → T → x = y → y = y
+T → T → x = y → P y
+(∀ (x : T), P x ↔ Q x) → Q x
+Prop → (∀ (x : T), P x ↔ Q x) → Prop → Q x
+∀ (x_1 : Prop), (∀ (x : T), P x ↔ Q x) → x_1 ∨ Q x
+(∀ (x : T), P x ↔ Q x) → Q x
+(∀ (x : T), P x ↔ Q x) → Q x
+∀ (x : T), T → (∀ (x : T), P x ↔ Q x) → Q x
+∀ (x x_1 : T), x = x_1 → (∀ (w : T), P w ↔ Q w) → Q x_1