feat(library/congr_lemma_manager): add new kind of congr_arg

src/library/blast/congruence_closure.cpp

@@ -192,6 +192,7 @@ static optional<ext_congr_lemma> to_ext_congr_lemma(name const & R, expr const &
     Rcs.resize(lhs_args.size(), optional<name>());
     r_hyps.resize(lhs_args.size(), none_expr());
     // Set Fixed args
+    // TODO(Leo): handle FixedNoParam case?
     for (unsigned i = 0; i < lhs_args.size(); i++) {
         if (lhs_args[i] == rhs_args[i])
             kinds[i] = congr_arg_kind::Fixed;
@@ -241,6 +242,9 @@ static optional<ext_congr_lemma> to_ext_congr_lemma(name const & R, expr const &
             return optional<ext_congr_lemma>();
         }
         switch (kinds[i]) {
+        case congr_arg_kind::FixedNoParam:
+            // TODO(Leo): revise this code
+            break;
         case congr_arg_kind::Fixed:
             break;
         case congr_arg_kind::Eq: {
@@ -431,6 +435,7 @@ int congruence_closure::congr_key_cmp::operator()(congr_key const & k1, congr_ke
                     if (r != 0) return r;
                     break;
                 case congr_arg_kind::Fixed:
+                case congr_arg_kind::FixedNoParam:
                     r = expr_quick_cmp()(args1[i], args2[i]);
                     if (r != 0) return r;
                     break;
@@ -491,6 +496,7 @@ auto congruence_closure::mk_congr_key(ext_congr_lemma const & lemma, expr const
                     h = hash(h, get_root(*head(*it1), args[i]).hash());
                     break;
                 case congr_arg_kind::Fixed:
+                case congr_arg_kind::FixedNoParam:
                     h = hash(h, args[i].hash());
                     break;
                 case congr_arg_kind::Cast:
@@ -967,6 +973,8 @@ expr congruence_closure::mk_congr_proof_core(name const & R, expr const & lhs, e
             case congr_arg_kind::Fixed:
                 lemma_args.push_back(lhs_args[i]);
                 break;
+            case congr_arg_kind::FixedNoParam:
+                break;
             case congr_arg_kind::Cast:
                 lemma_args.push_back(lhs_args[i]);
                 lemma_args.push_back(rhs_args[i]);

src/library/blast/simplifier/simplifier.cpp

@@ -277,22 +277,26 @@ optional<result> simplifier::cache_lookup(expr const & e) {
 
     unsigned i = 0;
     for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
-            if (ckind != congr_arg_kind::Cast) {
+            lean_assert(ckind == congr_arg_kind::Cast || new_args[i] == old_args[i]);
-                lean_assert(new_args[i] == old_args[i]);
-            }
-            proof = mk_app(proof, new_args[i]);
-            type = instantiate(binding_body(type), new_args[i]);
             expr rfl;
             switch (ckind) {
             case congr_arg_kind::Fixed:
+                proof = mk_app(proof, new_args[i]);
+                type = instantiate(binding_body(type), new_args[i]);
+                break;
+            case congr_arg_kind::FixedNoParam:
                 break;
             case congr_arg_kind::Eq:
+                proof = mk_app(proof, new_args[i]);
+                type = instantiate(binding_body(type), new_args[i]);
                 rfl = get_app_builder().mk_eq_refl(old_args[i]);
                 proof = mk_app(proof, old_args[i], rfl);
                 type = instantiate(binding_body(type), old_args[i]);
                 type = instantiate(binding_body(type), rfl);
                 break;
             case congr_arg_kind::Cast:
+                proof = mk_app(proof, new_args[i]);
+                type = instantiate(binding_body(type), new_args[i]);
                 proof = mk_app(proof, old_args[i]);
                 type = instantiate(binding_body(type), old_args[i]);
                 break;
@@ -807,17 +811,30 @@ optional<result> simplifier::synth_congr(expr const & e, F && simp) {
     bool has_cast = false;
     buffer<expr> locals;
     for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
+            switch (ckind) {
+            case congr_arg_kind::Fixed:
                 proof = mk_app(proof, args[i]);
                 type = instantiate(binding_body(type), args[i]);
-            if (ckind == congr_arg_kind::Eq) {
+                break;
+            case congr_arg_kind::FixedNoParam:
+                break;
+            case congr_arg_kind::Eq:
+                proof = mk_app(proof, args[i]);
+                type = instantiate(binding_body(type), args[i]);
+                {
                     result r_arg = simp(args[i]);
                     if (r_arg.has_proof()) has_proof = 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());
-            } else if (ckind == congr_arg_kind::Cast) {
+                }
+                break;
+            case congr_arg_kind::Cast:
+                proof = mk_app(proof, args[i]);
+                type = instantiate(binding_body(type), args[i]);
                 has_cast = true;
+                break;
             }
             i++;
         });

src/library/congr_lemma_manager.cpp

@@ -199,6 +199,9 @@ struct congr_lemma_manager::imp {
                     rhss.push_back(lhs);
                     eqs.push_back(none_expr());
                     break;
+                case congr_arg_kind::FixedNoParam:
+                    lean_unreachable(); // TODO(Leo): not implemented yet
+                    break;
                 case congr_arg_kind::Cast: {
                     expr rhs_type = mlocal_type(lhs);
                     rhs_type = instantiate_rev(abstract_locals(rhs_type, lhss.size()-1, lhss.data()), rhss.size(), rhss.data());
@@ -274,6 +277,9 @@ struct congr_lemma_manager::imp {
                     rhss.push_back(rhs);
                     eqs.push_back(none_expr());
                     break;
+                case congr_arg_kind::FixedNoParam:
+                    lean_unreachable(); // TODO(Leo): not implemented yet
+                    break;
                 case congr_arg_kind::Cast: {
                     rhs     = m_ctx.mk_tmp_local(binding_name(fn_type2), binding_domain(fn_type2));
                     rhss.push_back(rhs);

src/library/congr_lemma_manager.h

@@ -10,7 +10,15 @@ Author: Leonardo de Moura
 #include "library/fun_info_manager.h"
 
 namespace lean {
-enum class congr_arg_kind { Fixed, Eq, Cast };
+enum class congr_arg_kind {
+    Fixed,        /* It is a parameter for the congruence lemma, the parit occurs in the left and right hand sides. */
+    FixedNoParam, /* It is not a parameter for the congruence lemma, the lemma was specialized for this parameter.
+                     This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. */
+    Eq, /* The lemma contains three parameters for this kind of argument a_i, b_i and (eq_i : a_i = b_i).
+           a_i and b_i represent the left and right hand sides, and eq_i is a proof for their equality. */
+    Cast /* congr-simp lemma contains only one parameter for this kind of argument, and congr-lemmas contains two.
+            They correspond to arguments that are subsingletons/propositions. */
+};
 
 class congr_lemma {
     expr                 m_type;