feat(library/tactic/congruence_tactic): add congruence lemma generator

The generated congruence theorems ignore arguments that are subsingleton types.

src/library/class_instance_synth.cpp

@@ -464,7 +464,8 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
             lean_assert(p);
             substitution s = p->first.first;
             expr r        = s.instantiate_all(meta);
-            if (!has_expr_metavar_relaxed(r))
+            expr new_type = s.instantiate_all(type);
+            if (!has_expr_metavar_relaxed(r) && new_type == type)
                 return some_expr(r);
             seq = p->second;
         }
@@ -481,9 +482,18 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
 }
 
 optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
-    expr trunc_index = mk_app(mk_constant(get_is_trunc_trunc_index_of_nat_name()), mk_constant(get_nat_zero_name()));
     level lvl        = sort_level(tc.ensure_type(type).first);
-    expr is_hset     = mk_app(mk_constant(get_is_trunc_name(), {lvl}), trunc_index, type);
+    expr is_hset     = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hset_name(), {lvl}), type)).first;
     return mk_class_instance(tc.env(), ios, ctx, tc.mk_fresh_name(), is_hset);
 }
+
+optional<expr> mk_subsingleton_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
+    level lvl        = sort_level(tc.ensure_type(type).first);
+    expr subsingleton;
+    if (is_standard(tc.env()))
+        subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type);
+    else
+        subsingleton = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hprop_name(), {lvl}), type)).first;
+    return mk_class_instance(tc.env(), ios, ctx, tc.mk_fresh_name(), subsingleton);
+}
 }

src/library/class_instance_synth.h

@@ -44,6 +44,10 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
 /** \breif Try to synthesize an inhabitant for (is_hset type) using class instance resolution */
 optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);
 
+/** \breif Try to synthesize an inhabitant for (subsingleton type in the standard library, and hprop in the HoTT library)
+    using class instance resolution */
+optional<expr> mk_subsingleton_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);
+
 void initialize_class_instance_elaborator();
 void finalize_class_instance_elaborator();
 }

src/library/constants.cpp

@@ -26,6 +26,7 @@ name const * g_eq_rec_eq = nullptr;
 name const * g_eq_refl = nullptr;
 name const * g_eq_symm = nullptr;
 name const * g_eq_trans = nullptr;
+name const * g_eq_subst = nullptr;
 name const * g_exists_elim = nullptr;
 name const * g_false = nullptr;
 name const * g_false_rec = nullptr;
@@ -39,6 +40,7 @@ name const * g_iff_true_intro = nullptr;
 name const * g_implies = nullptr;
 name const * g_implies_of_if_pos = nullptr;
 name const * g_implies_of_if_neg = nullptr;
+name const * g_is_trunc_is_hprop_elim = nullptr;
 name const * g_ite = nullptr;
 name const * g_lift = nullptr;
 name const * g_lift_down = nullptr;
@@ -72,6 +74,8 @@ name const * g_sigma_mk = nullptr;
 name const * g_string = nullptr;
 name const * g_string_empty = nullptr;
 name const * g_string_str = nullptr;
+name const * g_subsingleton = nullptr;
+name const * g_subsingleton_elim = nullptr;
 name const * g_tactic = nullptr;
 name const * g_tactic_all_goals = nullptr;
 name const * g_tactic_apply = nullptr;
@@ -134,8 +138,8 @@ name const * g_trans_rel_left = nullptr;
 name const * g_trans_rel_right = nullptr;
 name const * g_true = nullptr;
 name const * g_true_intro = nullptr;
-name const * g_is_trunc = nullptr;
+name const * g_is_trunc_is_hset = nullptr;
-name const * g_is_trunc_trunc_index_of_nat = nullptr;
+name const * g_is_trunc_is_hprop = nullptr;
 name const * g_unit = nullptr;
 name const * g_unit_star = nullptr;
 name const * g_well_founded = nullptr;
@@ -163,6 +167,7 @@ void initialize_constants() {
     g_eq_refl = new name{"eq", "refl"};
     g_eq_symm = new name{"eq", "symm"};
     g_eq_trans = new name{"eq", "trans"};
+    g_eq_subst = new name{"eq", "subst"};
     g_exists_elim = new name{"exists", "elim"};
     g_false = new name{"false"};
     g_false_rec = new name{"false", "rec"};
@@ -176,6 +181,7 @@ void initialize_constants() {
     g_implies = new name{"implies"};
     g_implies_of_if_pos = new name{"implies_of_if_pos"};
     g_implies_of_if_neg = new name{"implies_of_if_neg"};
+    g_is_trunc_is_hprop_elim = new name{"is_trunc", "is_hprop", "elim"};
     g_ite = new name{"ite"};
     g_lift = new name{"lift"};
     g_lift_down = new name{"lift", "down"};
@@ -209,6 +215,8 @@ void initialize_constants() {
     g_string = new name{"string"};
     g_string_empty = new name{"string", "empty"};
     g_string_str = new name{"string", "str"};
+    g_subsingleton = new name{"subsingleton"};
+    g_subsingleton_elim = new name{"subsingleton", "elim"};
     g_tactic = new name{"tactic"};
     g_tactic_all_goals = new name{"tactic", "all_goals"};
     g_tactic_apply = new name{"tactic", "apply"};
@@ -271,8 +279,8 @@ void initialize_constants() {
     g_trans_rel_right = new name{"trans_rel_right"};
     g_true = new name{"true"};
     g_true_intro = new name{"true", "intro"};
-    g_is_trunc = new name{"is_trunc"};
+    g_is_trunc_is_hset = new name{"is_trunc", "is_hset"};
-    g_is_trunc_trunc_index_of_nat = new name{"is_trunc", "trunc_index", "of_nat"};
+    g_is_trunc_is_hprop = new name{"is_trunc", "is_hprop"};
     g_unit = new name{"unit"};
     g_unit_star = new name{"unit", "star"};
     g_well_founded = new name{"well_founded"};
@@ -301,6 +309,7 @@ void finalize_constants() {
     delete g_eq_refl;
     delete g_eq_symm;
     delete g_eq_trans;
+    delete g_eq_subst;
     delete g_exists_elim;
     delete g_false;
     delete g_false_rec;
@@ -314,6 +323,7 @@ void finalize_constants() {
     delete g_implies;
     delete g_implies_of_if_pos;
     delete g_implies_of_if_neg;
+    delete g_is_trunc_is_hprop_elim;
     delete g_ite;
     delete g_lift;
     delete g_lift_down;
@@ -347,6 +357,8 @@ void finalize_constants() {
     delete g_string;
     delete g_string_empty;
     delete g_string_str;
+    delete g_subsingleton;
+    delete g_subsingleton_elim;
     delete g_tactic;
     delete g_tactic_all_goals;
     delete g_tactic_apply;
@@ -409,8 +421,8 @@ void finalize_constants() {
     delete g_trans_rel_right;
     delete g_true;
     delete g_true_intro;
-    delete g_is_trunc;
+    delete g_is_trunc_is_hset;
-    delete g_is_trunc_trunc_index_of_nat;
+    delete g_is_trunc_is_hprop;
     delete g_unit;
     delete g_unit_star;
     delete g_well_founded;
@@ -438,6 +450,7 @@ name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; }
 name const & get_eq_refl_name() { return *g_eq_refl; }
 name const & get_eq_symm_name() { return *g_eq_symm; }
 name const & get_eq_trans_name() { return *g_eq_trans; }
+name const & get_eq_subst_name() { return *g_eq_subst; }
 name const & get_exists_elim_name() { return *g_exists_elim; }
 name const & get_false_name() { return *g_false; }
 name const & get_false_rec_name() { return *g_false_rec; }
@@ -451,6 +464,7 @@ name const & get_iff_true_intro_name() { return *g_iff_true_intro; }
 name const & get_implies_name() { return *g_implies; }
 name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; }
 name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; }
+name const & get_is_trunc_is_hprop_elim_name() { return *g_is_trunc_is_hprop_elim; }
 name const & get_ite_name() { return *g_ite; }
 name const & get_lift_name() { return *g_lift; }
 name const & get_lift_down_name() { return *g_lift_down; }
@@ -484,6 +498,8 @@ name const & get_sigma_mk_name() { return *g_sigma_mk; }
 name const & get_string_name() { return *g_string; }
 name const & get_string_empty_name() { return *g_string_empty; }
 name const & get_string_str_name() { return *g_string_str; }
+name const & get_subsingleton_name() { return *g_subsingleton; }
+name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; }
 name const & get_tactic_name() { return *g_tactic; }
 name const & get_tactic_all_goals_name() { return *g_tactic_all_goals; }
 name const & get_tactic_apply_name() { return *g_tactic_apply; }
@@ -546,8 +562,8 @@ name const & get_trans_rel_left_name() { return *g_trans_rel_left; }
 name const & get_trans_rel_right_name() { return *g_trans_rel_right; }
 name const & get_true_name() { return *g_true; }
 name const & get_true_intro_name() { return *g_true_intro; }
-name const & get_is_trunc_name() { return *g_is_trunc; }
+name const & get_is_trunc_is_hset_name() { return *g_is_trunc_is_hset; }
-name const & get_is_trunc_trunc_index_of_nat_name() { return *g_is_trunc_trunc_index_of_nat; }
+name const & get_is_trunc_is_hprop_name() { return *g_is_trunc_is_hprop; }
 name const & get_unit_name() { return *g_unit; }
 name const & get_unit_star_name() { return *g_unit_star; }
 name const & get_well_founded_name() { return *g_well_founded; }

src/library/constants.h

@@ -28,6 +28,7 @@ name const & get_eq_rec_eq_name();
 name const & get_eq_refl_name();
 name const & get_eq_symm_name();
 name const & get_eq_trans_name();
+name const & get_eq_subst_name();
 name const & get_exists_elim_name();
 name const & get_false_name();
 name const & get_false_rec_name();
@@ -41,6 +42,7 @@ name const & get_iff_true_intro_name();
 name const & get_implies_name();
 name const & get_implies_of_if_pos_name();
 name const & get_implies_of_if_neg_name();
+name const & get_is_trunc_is_hprop_elim_name();
 name const & get_ite_name();
 name const & get_lift_name();
 name const & get_lift_down_name();
@@ -74,6 +76,8 @@ name const & get_sigma_mk_name();
 name const & get_string_name();
 name const & get_string_empty_name();
 name const & get_string_str_name();
+name const & get_subsingleton_name();
+name const & get_subsingleton_elim_name();
 name const & get_tactic_name();
 name const & get_tactic_all_goals_name();
 name const & get_tactic_apply_name();
@@ -136,8 +140,8 @@ name const & get_trans_rel_left_name();
 name const & get_trans_rel_right_name();
 name const & get_true_name();
 name const & get_true_intro_name();
-name const & get_is_trunc_name();
+name const & get_is_trunc_is_hset_name();
-name const & get_is_trunc_trunc_index_of_nat_name();
+name const & get_is_trunc_is_hprop_name();
 name const & get_unit_name();
 name const & get_unit_star_name();
 name const & get_well_founded_name();

src/library/constants.txt

@@ -21,6 +21,7 @@ eq_rec_eq
 eq.refl
 eq.symm
 eq.trans
+eq.subst
 exists.elim
 false
 false.rec
@@ -34,6 +35,7 @@ iff_true_intro
 implies
 implies_of_if_pos
 implies_of_if_neg
+is_trunc.is_hprop.elim
 ite
 lift
 lift.down
@@ -67,6 +69,8 @@ sigma.mk
 string
 string.empty
 string.str
+subsingleton
+subsingleton.elim
 tactic
 tactic.all_goals
 tactic.apply
@@ -129,8 +133,8 @@ trans_rel_left
 trans_rel_right
 true
 true.intro
-is_trunc
+is_trunc.is_hset
-is_trunc.trunc_index.of_nat
+is_trunc.is_hprop
 unit
 unit.star
 well_founded

src/library/locals.cpp

@@ -1,10 +1,12 @@
 /*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
 #include "util/name_set.h"
+#include "kernel/abstract.h"
+#include "kernel/instantiate.h"
 #include "kernel/expr.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/find_fn.h"
@@ -59,17 +61,43 @@ void collected_locals::insert(expr const & l) {
 void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
     if (!has_local(e))
         return;
-    for_each(e, [&](expr const & e, unsigned) {
+    expr_set visited;
+    std::function<void(expr const & e)> visit = [&](expr const & e) {
         if (!has_local(e))
-                return false;
+            return;
-            if (is_local(e)) {
+        if (restricted && is_meta(e))
+            return;
+        if (visited.find(e) != visited.end())
+            return;
+        visited.insert(e);
+        switch (e.kind()) {
+        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort:
+            break; // do nothing
+        case expr_kind::Local:
+            if (!restricted)
+                visit(mlocal_type(e));
             ls.insert(e);
-                return !restricted; // search type if not restricted
+            break;
+        case expr_kind::Meta:
+            lean_assert(!restricted);
+            visit(mlocal_type(e));
+            break;
+        case expr_kind::Macro:
+            for (unsigned i = 0; i < macro_num_args(e); i++)
+                visit(macro_arg(e, i));
+            break;
+        case expr_kind::App:
+            visit(app_fn(e));
+            visit(app_arg(e));
+            break;
+        case expr_kind::Lambda:
+        case expr_kind::Pi:
+            visit(binding_domain(e));
+            visit(binding_body(e));
+            break;
         }
-            if (is_meta(e))
+    };
-                return !restricted; // search type if not restricted
+    visit(e);
-            return true;
-        });
 }
 
 bool contains_local(expr const & e, name const & n) {
@@ -99,4 +127,14 @@ optional<expr> depends_on(unsigned sz, expr const * es, expr const & h) {
 bool depends_on_any(expr const & e, unsigned hs_sz, expr const * hs) {
     return std::any_of(hs, hs+hs_sz, [&](expr const & h) { return depends_on(e, h); });
 }
+
+expr replace_locals(expr const & e, unsigned sz, expr const * locals, expr const * terms) {
+    return instantiate_rev(abstract_locals(e, sz, locals), sz, terms);
+}
+
+expr replace_locals(expr const & e, buffer<expr> const & locals, buffer<expr> const & terms) {
+    lean_assert(locals.size() == terms.size());
+    lean_assert(std::all_of(locals.begin(), locals.end(), is_local));
+    return replace_locals(e, locals.size(), locals.data(), terms.data());
+}
 }

src/library/locals.h

@@ -1,5 +1,5 @@
 /*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
@@ -56,4 +56,8 @@ bool depends_on_any(expr const & e, unsigned hs_sz, expr const * hs);
 inline bool depends_on_any(expr const & e, buffer<expr> const & hs) {
     return depends_on_any(e, hs.size(), hs.data());
 }
+
+/** \brief Replace the given local constants occurring in \c e with the given terms */
+expr replace_locals(expr const & e, unsigned sz, expr const * locals, expr const * terms);
+expr replace_locals(expr const & e, buffer<expr> const & locals, buffer<expr> const & terms);
 }

src/library/tactic/congruence_tactic.cpp

@@ -4,14 +4,186 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <algorithm>
+#include "kernel/abstract.h"
+#include "kernel/instantiate.h"
 #include "library/util.h"
+#include "library/locals.h"
 #include "library/constants.h"
 #include "library/reducible.h"
+#include "library/class_instance_synth.h"
 #include "library/tactic/util.h"
 #include "library/tactic/intros_tactic.h"
+#include "library/tactic/subst_tactic.h"
 #include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
+enum class congr_arg_kind { Fixed, Singleton, Eq };
+
+optional<expr> mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios, expr const & fn, optional<unsigned> const & expected_num_args,
+                                         buffer<congr_arg_kind> & arg_kinds, constraint_seq & cs) {
+    expr fn_type = tc.infer(fn, cs);
+    buffer<expr> hyps;
+    collected_locals ctx_buffer;
+    collect_locals(fn_type, ctx_buffer);
+    collect_locals(fn, ctx_buffer);
+    hyps.append(ctx_buffer.get_collected());
+    list<expr> ctx = to_list(hyps);
+
+    buffer<expr> domain;
+    expr codomain = to_telescope(tc, fn_type, domain, optional<binder_info>(), cs);
+    if (expected_num_args && *expected_num_args != domain.size()) {
+        if (*expected_num_args > domain.size())
+            return none_expr();
+        lean_assert(*expected_num_args < domain.size());
+        while (domain.size() > *expected_num_args) {
+            codomain = Pi(domain.back(), codomain);
+            domain.pop_back();
+        }
+    }
+
+    buffer<bool> prop;   // pp[i] iff i-th arg is a proposition
+    buffer<bool> ss;     // ss[i] is not none iff i-th arg is a subsingleton
+    buffer<bool> codomain_deps_on; // codomain_deps_on[i] iff codomain depends on i-th argument
+    for (expr const & d : domain) {
+        prop.push_back(tc.is_prop(mlocal_type(d), cs) && tc.env().prop_proof_irrel());
+        if (prop.back()) {
+            ss.push_back(true);
+        } else {
+            ss.push_back(static_cast<bool>(mk_subsingleton_instance(tc, ios, ctx, mlocal_type(d))));
+        }
+        codomain_deps_on.push_back(depends_on(codomain, d));
+        ctx = cons(d, ctx);
+    }
+
+    buffer<expr> new_domain;
+    buffer<expr> conclusion_lhs;
+    for (unsigned i = 0; i < domain.size(); i++) {
+        lean_assert(i == new_domain.size());
+        expr const & d_i = domain[i];
+        expr new_type    = replace_locals(mlocal_type(d_i), i, domain.data(), new_domain.data());
+        expr new_d_i     = mk_local(get_unused_name(local_pp_name(d_i), hyps), new_type);
+        hyps.push_back(new_d_i);
+        conclusion_lhs.push_back(new_d_i);
+        new_domain.push_back(new_d_i);
+    }
+
+    buffer<expr> lhss, rhss;
+    buffer<optional<expr>> eqs;
+    buffer<bool> ss_elim; // true if equality proof should be synthesized using singletion elimination
+    buffer<expr> conclusion_rhs;
+    name h("he");
+    unsigned eqidx = 1;
+    for (unsigned i = 0; i < new_domain.size(); i++) {
+        expr const & d_i = new_domain[i];
+        if (ss[i]) {
+            arg_kinds.push_back(congr_arg_kind::Singleton);
+            expr new_type = replace_locals(mlocal_type(d_i), rhss, lhss);
+            expr new_d_i  = mk_local(get_unused_name(name(local_pp_name(d_i), "new"), hyps), new_type);
+            hyps.push_back(new_d_i);
+            rhss.push_back(d_i);
+            lhss.push_back(new_d_i);
+            conclusion_rhs.push_back(new_d_i);
+            ss_elim.push_back(!prop[i]);
+            eqs.push_back(none_expr());
+        } else {
+            unsigned j = i+1;
+            for (; j < new_domain.size(); j++) {
+                expr t_j = mlocal_type(new_domain[j]);
+                if (depends_on(t_j, d_i) && !ss[j])
+                    break;
+            }
+            if (j < new_domain.size() || codomain_deps_on[i]) {
+                arg_kinds.push_back(congr_arg_kind::Fixed);
+                conclusion_rhs.push_back(d_i);
+            } else {
+                arg_kinds.push_back(congr_arg_kind::Eq);
+                expr new_type   = replace_locals(mlocal_type(d_i), rhss, lhss);
+                expr new_d_i    = mk_local(get_unused_name(name(local_pp_name(d_i), "new"), hyps), new_type);
+                name new_h_name = get_unused_name(name(h, eqidx), hyps);
+                eqidx++;
+                expr new_eq     = mk_local(new_h_name, mk_eq(tc, new_d_i, d_i));
+                hyps.push_back(new_d_i);
+                rhss.push_back(d_i);
+                lhss.push_back(new_d_i);
+                conclusion_rhs.push_back(new_d_i);
+                ss_elim.push_back(false);
+                eqs.push_back(some_expr(new_eq));
+            }
+        }
+    }
+    for (optional<expr> const & eq : eqs) {
+        if (eq)
+            hyps.push_back(*eq);
+    }
+    expr conclusion = mk_eq(tc, mk_app(fn, conclusion_lhs), mk_app(fn, conclusion_rhs));
+    expr mvar_type  = Pi(hyps, conclusion);
+    expr mvar       = mk_metavar(tc.mk_fresh_name(), mvar_type);
+    expr meta       = mk_app(mvar, hyps);
+    proof_state ps  = to_proof_state(meta, conclusion, tc.mk_ngen()).update_report_failure(false);
+    for (unsigned i = 0; i < eqs.size(); i++) {
+        goal const & g = head(ps.get_goals());
+        optional<expr> const & eq = eqs[i];
+        if (eq) {
+            auto new_eq = g.find_hyp(local_pp_name(*eq));
+            if (auto new_ps = subst(tc.env(), mlocal_name(new_eq->first), false, ps)) {
+                ps = *new_ps;
+            } else {
+                return none_expr();
+            }
+        } else if (ss_elim[i]) {
+            expr lhs       = lhss[i];
+            expr rhs       = rhss[i];
+            expr new_lhs, new_rhs;
+            if (auto it = g.find_hyp(local_pp_name(lhs)))
+                new_lhs = it->first;
+            else
+                return none_expr();
+            if (auto it = g.find_hyp(local_pp_name(rhs)))
+                new_rhs = it->first;
+            else
+                return none_expr();
+            buffer<expr> hyps;
+            g.get_hyps(hyps);
+            auto spr = mk_subsingleton_instance(tc, ios, to_list(hyps), mlocal_type(new_lhs));
+            if (!spr)
+                return none_expr();
+            expr new_eq    = mk_local(get_unused_name(name(h, eqidx), hyps), mk_eq(tc, new_rhs, new_lhs));
+            eqidx++;
+            expr new_eq_pr      = mk_subsingleton_elim(tc, *spr, new_rhs, new_lhs);
+            expr aux_mvar       = mk_metavar(tc.mk_fresh_name(), Pi(hyps, g.get_type()));
+            expr aux_meta_core  = mk_app(aux_mvar, hyps);
+            goal aux_g(mk_app(aux_meta_core, new_eq), g.get_type());
+            substitution new_subst = ps.get_subst();
+            assign(new_subst, g, mk_app(aux_meta_core, new_eq_pr));
+            proof_state aux_ps  = proof_state(ps, goals(aux_g), new_subst);
+            if (auto new_ps = subst(tc.env(), mlocal_name(new_eq), false, aux_ps)) {
+                ps = *new_ps;
+            } else {
+                return none_expr();
+            }
+        } else {
+            // do nothing, it is a proposition
+        }
+    }
+
+    substitution subst = ps.get_subst();
+    goal const & g = head(ps.get_goals());
+    assign(subst, g, mk_refl(tc, app_arg(g.get_type())));
+    expr result    = subst.instantiate_all(mvar);
+    try {
+        check_term(tc, result);
+    } catch (exception &) {
+        return none_expr();
+    }
+    for (expr const & ctx_local : ctx_buffer.get_collected()) {
+        result    = mk_app(result, ctx_local);
+        mvar_type = instantiate(binding_body(mvar_type), ctx_local);
+    }
+    result = head_beta_reduce(result);
+    return some_expr(result);
+}
+
 tactic congruence_tactic() {
     auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) -> optional<proof_state> {
         goals const & gs = s.get_goals();
@@ -32,88 +204,79 @@ tactic congruence_tactic() {
             return none_proof_state();
         }
 
-        buffer<goal> new_goals;
-
-        auto mk_eq_goal = [&](expr const & lhs, expr const & rhs) {
-            expr new_type = mk_eq(*tc, lhs, rhs);
-            expr new_meta = g.mk_meta(ngen.next(), new_type);
-            new_goals.push_back(goal(new_meta, new_type));
-            return some_expr(new_meta);
-        };
-
-        std::function<optional<expr>(expr const &, expr const &, bool)> process =
-        [&](expr const & lhs, expr const & rhs, bool first) {
-            if (tc->is_def_eq(lhs, rhs, justification(), cs)) {
-                return some_expr(mk_refl(*tc, lhs));
-            }
         if (!is_app(lhs) || !is_app(rhs)) {
-                if (first) {
+            throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, left and right hand side of equation must be a function application");
-                    throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, left (and right) hand side of equation must be a function application");
+            return none_proof_state();
-                    return none_expr();
         }
-                return mk_eq_goal(lhs, rhs);
+
+        buffer<expr> lhs_args, rhs_args;
+        expr lhs_fn = get_app_args(lhs, lhs_args);
+        expr rhs_fn = get_app_args(rhs, rhs_args);
+
+        if (lhs_args.size() != rhs_args.size()) {
+            throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, left and right hand side of equation must have the same number of arguments");
+            return none_proof_state();
         }
-            expr lhs_fn = app_fn(lhs);
+
-            expr rhs_fn = app_fn(rhs);
         expr lhs_fn_type = tc->whnf(tc->infer(lhs_fn, cs), cs);
         expr rhs_fn_type = tc->whnf(tc->infer(rhs_fn, cs), cs);
         if (!tc->is_def_eq(lhs_fn_type, rhs_fn_type, justification(), cs)) {
-                if (first) {
             throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, functions do not have the same type");
-                    return none_expr();
+            return none_proof_state();
         }
-                return mk_eq_goal(lhs, rhs);
+
+        buffer<goal> new_goals;
+        optional<expr> fn_pr;
+        if (!tc->is_def_eq(lhs_fn, rhs_fn, justification(), cs)) {
+            expr new_type = mk_eq(*tc, lhs_fn, rhs_fn);
+            expr new_meta = g.mk_meta(ngen.next(), new_type);
+            new_goals.push_back(goal(new_meta, new_type));
+            fn_pr = new_meta;
+        }
+
+        buffer<congr_arg_kind> arg_kinds;
+        auto cg_proof = mk_congr_subsingleton_thm(*tc, ios, lhs_fn, some(lhs_args.size()), arg_kinds, cs);
+        if (!cg_proof) {
+            throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, tactic does not support this kind of dependent function");
+            return none_proof_state();
+        }
+
+        expr pr = mk_app(*cg_proof, lhs_args);
+        for (unsigned i = 0; i < arg_kinds.size(); i++) {
+            if (arg_kinds[i] == congr_arg_kind::Fixed) {
+                if (!tc->is_def_eq(lhs_args[i], rhs_args[i], justification(), cs)) {
+                    throw_tactic_exception_if_enabled(s, sstream() << "invalid 'congruence' tactic, argument #" << (i+1)
+                                                      << " must be the same in the left and right hand sides");
+                    return none_proof_state();
                 }
-            expr fn_type;
-            if (is_pi(lhs_fn_type)) {
-                fn_type = lhs_fn_type;
-            } else if (is_pi(rhs_fn_type)) {
-                fn_type = rhs_fn_type;
-            } else if (first) {
-                throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, failed to compute function type");
-                return none_expr();
             } else {
-                return mk_eq_goal(lhs, rhs);
+                pr = mk_app(pr, rhs_args[i]);
+            }
         }
 
-            if (!closed(binding_body(fn_type))) {
+        for (unsigned i = 0; i < arg_kinds.size(); i++) {
-                if (first) {
+            if (arg_kinds[i] == congr_arg_kind::Eq) {
-                    throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, cannot be applied to dependent functions");
+                if (tc->is_def_eq(lhs_args[i], rhs_args[i], justification(), cs)) {
-                    return none_expr();
+                    pr = mk_app(pr, mk_refl(*tc, lhs_args[i]));
-                }
-                return mk_eq_goal(lhs, rhs);
-            }
-
-            expr lhs_arg = app_arg(lhs);
-            expr rhs_arg = app_arg(rhs);
-            expr arg_pr;
-            if (tc->is_def_eq(lhs_arg, rhs_arg, justification(), cs)) {
-                arg_pr = mk_refl(*tc, lhs_arg);
                 } else {
-                arg_pr = *mk_eq_goal(lhs_arg, rhs_arg);
+                    expr new_type = mk_eq(*tc, lhs_args[i], rhs_args[i]);
+                    expr new_meta = g.mk_meta(ngen.next(), new_type);
+                    new_goals.push_back(goal(new_meta, new_type));
+                    pr = mk_app(pr, mk_symm(*tc, new_meta));
+                }
+            }
         }
 
-            optional<expr> opt_fn_pr = process(lhs_fn, rhs_fn, false);
+        if (fn_pr) {
-            if (!opt_fn_pr)
+            expr motive_rhs = mk_app(mk_var(0), rhs_args);
-                return none_expr();
+            expr motive     = mk_lambda("f", lhs_fn_type, mk_app(app_fn(app_fn(g.get_type())), lhs, motive_rhs));
-            expr fn_pr = *opt_fn_pr;
+            pr = mk_subst(*tc, motive, lhs_fn, rhs_fn, *fn_pr, pr);
+        }
 
-            expr A   = binding_domain(fn_type);
+        assign(subst, g, pr);
-            expr B   = binding_body(fn_type);
-            level l1 = sort_level(tc->ensure_type(A, cs));
-            level l2 = sort_level(tc->ensure_type(B, cs));
-
-            return some_expr(mk_app({mk_constant(get_congr_name(), {l1, l2}),
-                            A, B, lhs_fn, rhs_fn, lhs_arg, rhs_arg, fn_pr, arg_pr}));
-        };
-
-        if (optional<expr> pr = process(lhs, rhs, true)) {
-            std::reverse(new_goals.begin(), new_goals.end());
-            assign(subst, g, *pr);
         proof_state new_ps(s, to_list(new_goals.begin(), new_goals.end(), tail(gs)), subst, ngen);
         if (solve_constraints(env, ios, new_ps, cs))
             return some_proof_state(new_ps);
-        }
         return none_proof_state();
     };
     return tactic01(fn);

src/library/tactic/congruence_tactic.h

@@ -5,7 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "kernel/type_checker.h"
 namespace lean {
+enum class congr_arg_kind { Fixed, Singleton, Eq };
+optional<expr> mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios,
+                                         expr const & fn, optional<unsigned> const & expected_num_args,
+                                         buffer<congr_arg_kind> & arg_kinds, constraint_seq & cs);
 void initialize_congruence_tactic();
 void finalize_congruence_tactic();
 }

src/library/util.cpp

@@ -505,6 +505,48 @@ expr mk_symm(type_checker & tc, expr const & H) {
     return mk_app(mk_constant(get_eq_symm_name(), {lvl}), A, lhs, rhs, H);
 }
 
+expr mk_trans(type_checker & tc, expr const & H1, expr const & H2) {
+    expr p1    = tc.whnf(tc.infer(H1).first).first;
+    expr p2    = tc.whnf(tc.infer(H2).first).first;
+    lean_assert(is_eq(p1) && is_eq(p2));
+    expr lhs1  = app_arg(app_fn(p1));
+    expr rhs1  = app_arg(p1);
+    expr rhs2  = app_arg(p2);
+    expr A     = tc.infer(lhs1).first;
+    level lvl  = sort_level(tc.ensure_type(A).first);
+    return mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, lhs1, rhs1, rhs2, H1, H2});
+}
+
+expr mk_subst(type_checker & tc, expr const & motive, expr const & x, expr const & y, expr const & xeqy, expr const & h) {
+    expr A    = tc.infer(x).first;
+    level l1  = sort_level(tc.ensure_type(A).first);
+    expr r;
+    if (is_standard(tc.env())) {
+        r = mk_constant(get_eq_subst_name(), {l1});
+    } else {
+        level l2 = sort_level(tc.ensure_type(tc.infer(h).first).first);
+        r = mk_constant(get_eq_subst_name(), {l1, l2});
+    }
+    return mk_app({r, A, x, y, motive, xeqy, h});
+}
+
+expr mk_subst(type_checker & tc, expr const & motive, expr const & xeqy, expr const & h) {
+    expr xeqy_type = tc.whnf(tc.infer(xeqy).first).first;
+    return mk_subst(tc, motive, app_arg(app_fn(xeqy_type)), app_arg(xeqy_type), xeqy, h);
+}
+
+expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, expr const & y) {
+    expr A  = tc.infer(x).first;
+    level l = sort_level(tc.ensure_type(A).first);
+    expr r;
+    if (is_standard(tc.env())) {
+        r = mk_constant(get_subsingleton_elim_name(), {l});
+    } else {
+        r = mk_constant(get_is_trunc_is_hprop_elim_name(), {l});
+    }
+    return mk_app({r, A, h, x, y});
+}
+
 expr mk_heq(type_checker & tc, expr const & lhs, expr const & rhs) {
     expr A    = tc.whnf(tc.infer(lhs).first).first;
     expr B    = tc.whnf(tc.infer(rhs).first).first;

src/library/util.h

@@ -154,6 +154,11 @@ expr mk_absurd(type_checker & tc, expr const & t, expr const & e, expr const & n
 expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs);
 expr mk_refl(type_checker & tc, expr const & a);
 expr mk_symm(type_checker & tc, expr const & H);
+expr mk_trans(type_checker & tc, expr const & H1, expr const & H2);
+expr mk_subst(type_checker & tc, expr const & motive, expr const & x, expr const & y, expr const & xeqy, expr const & h);
+expr mk_subst(type_checker & tc, expr const & motive, expr const & xeqy, expr const & h);
+/** \brief Create an proof for x = y using subsingleton.elim (in standard mode) and is_trunc.is_hprop.elim (in HoTT mode) */
+expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, expr const & y);
 bool is_eq_rec(expr const & e);
 bool is_eq(expr const & e);
 bool is_eq(expr const & e, expr & lhs, expr & rhs);

tests/lean/hott/congr_tac2.hlean

@@ -0,0 +1,8 @@
+open nat is_trunc
+
+example (f : Π (a b : nat), a = b → nat) (a₁ a₂ b₁ b₂ : nat) (h₁ : a₁ = b₁) (h₂ : a₂ = b₂) : a₁ = a₂ → b₁ = b₂ → f a₁ b₁ h₁ = f a₂ b₂ h₂ :=
+begin
+  intros,
+  congruence,
+  repeat assumption
+end

tests/lean/run/congr_tac2.lean

@@ -0,0 +1,49 @@
+import data.finset
+open finset list
+
+example (A : Type) (f : nat → nat → nat → nat) (a b : nat) : a = b → f a = f b :=
+begin
+  intros,
+  congruence,
+  assumption
+end
+
+structure finite_set [class] {T : Type} (xs : set T) :=
+(to_finset : finset T) (is_equiv : to_set to_finset = xs)
+
+definition finset_set.is_subsingleton [instance] (T : Type) (xs : set T) : subsingleton (finite_set xs) :=
+begin
+  constructor, intro a b,
+  induction a with f₁ h₁,
+  induction b with f₂ h₂,
+  subst xs,
+  let e := to_set.inj h₂,
+  subst e
+end
+
+open finite_set
+
+definition card {T : Type} (xs : set T) [fxs : finite_set xs] :=
+finset.card (to_finset xs)
+
+example (A : Type) (s₁ s₂ : set A) [fxs₁ : finite_set s₁] [fxs₂ : finite_set s₂] : s₁ = s₂ → card s₁ = card s₂ :=
+begin
+  intros,
+  congruence,
+  assumption
+end
+
+example {A : Type} (l₁ l₂ : list A) (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) : l₁ = l₂ → last l₁ h₁ = last l₂ h₂ :=
+begin
+  intros,
+  congruence,
+  assumption
+end
+
+example (A : Type) (last₁ last₂ : Π l : list A, l ≠ [] → A) (l₁ l₂ : list A) (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) :
+        last₁ = last₂ → l₁ = l₂ → last₁ l₁ h₁ = last₂ l₂ h₂ :=
+begin
+  intro e₁ e₂,
+  congruence,
+  repeat assumption
+end