feat(library/blast/simplifier): use generated congruence lemmas

src/library/blast/simplifier.cpp

@@ -24,7 +24,7 @@ Author: Daniel Selsam
 #include <map>
 
 #ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
-#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 100
+#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000
 #endif
 #ifndef LEAN_DEFAULT_SIMPLIFY_TOP_DOWN
 #define LEAN_DEFAULT_SIMPLIFY_TOP_DOWN false
@@ -339,7 +339,38 @@ result simplifier::simplify_app(expr const & e) {
 
     /* (2) Synthesize congruence lemma */
     if (using_eq()) {
-        // TODO(dhs): synthesize congruence lemma
+        buffer<expr> args;
+        expr fn = get_app_args(e, args);
+        if (auto congr_lemma = mk_congr_lemma_for_simp(fn, args.size())) {
+            expr proof = congr_lemma->get_proof();
+            expr type = congr_lemma->get_type();
+            unsigned i = 0;
+            bool simplified = false;
+            buffer<expr> locals;
+            for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
+                    proof = mk_app(proof, args[i]);
+                    type = instantiate(binding_body(type), args[i]);
+
+                    if (ckind == congr_arg_kind::Eq) {
+                        result r_arg = simplify(args[i]);
+                        if (!r_arg.is_none()) simplified = true;
+                        r_arg = finalize(r_arg);
+                        proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof());
+                        type = instantiate(binding_body(type), r_arg.get_new());
+                        type = instantiate(binding_body(type), r_arg.get_proof());
+                    }
+                    i++;
+                });
+            if (simplified) {
+                lean_assert(is_eq(type));
+                buffer<expr> type_args;
+                get_app_args(type, type_args);
+                expr & new_e = type_args[2];
+                return join(result(new_e, proof), simplify_fun(new_e));
+            } else {
+                return simplify_fun(e);
+            }
+        }
     }
 
     /* (3) Fall back on generic binary congruence */

src/library/congr_lemma_manager.cpp

@@ -18,7 +18,7 @@ class congr_lemma_manager::imp {
     type_context &     m_ctx;
     bool               m_ignore_inst_implicit;
     struct key {
-        expr const & m_fn;
+        expr         m_fn;
         unsigned     m_nargs;
         unsigned     m_hash;
         key(expr const & fn, unsigned nargs):

tests/lean/simplifier13.lean

@@ -0,0 +1,10 @@
+universe l
+constants (T : Type.{l}) (f : T →  T → T) (g : T → T) 
+constants (P : T → Prop) (Q : Prop) (Hfg : ∀ (x : T), f x x = g x)
+constants (c : Π (x y z : T), P x → P y → P z → Q) 
+constants (x y z : T) (px : P (f x x)) (py : P (f y y)) (pz : P (g z))
+
+attribute Hfg [simp]
+
+#simplify eq 0 c (f x x) (f y y) (g z) px py pz
+

tests/lean/simplifier13.lean.expected.out

@@ -0,0 +1 @@
+c (g x) (g y) (g z) (eq.rec px (Hfg x)) (eq.rec py (Hfg y)) (eq.rec pz (eq.refl (g z)))

tests/lean/simplifier3.lean

@@ -13,7 +13,7 @@ attribute Hgyhz [simp]
 attribute Hab [simp]
 attribute Hbc [simp]
 
-#simplify eq 2 (f x a) -- h z c
+#simplify eq 2 (f x a)
 
 end test_congr
 

tests/lean/simplifier3.lean.expected.out

@@ -1,2 +1,2 @@
-f x a = h z c
+f x a = f x c
 f x = g x

tests/lean/simplifier7.lean

@@ -11,5 +11,6 @@ attribute H3 [simp]
 attribute Hf [simp]
 attribute Hg [simp]
 
+
 #simplify iff 2 (and P1 (and P2 P3))
 #simplify iff 2 (and P1 (iff P2 P3))