feat(library/tactic): add 'congruence' tactic

It is the f_equal described at issue #500.

hott/init/tactic.hlean

@@ -43,7 +43,8 @@ opaque definition beta        : tactic := builtin
 opaque definition info        : tactic := builtin
 opaque definition whnf        : tactic := builtin
 opaque definition contradiction : tactic := builtin
-opaque definition exfalso : tactic := builtin
+opaque definition exfalso     : tactic := builtin
+opaque definition congruence  : tactic := builtin
 opaque definition rotate_left (k : num) := builtin
 opaque definition rotate_right (k : num) := builtin
 definition rotate (k : num) := rotate_left k

library/init/tactic.lean

@@ -44,6 +44,7 @@ opaque definition info        : tactic := builtin
 opaque definition whnf        : tactic := builtin
 opaque definition contradiction : tactic := builtin
 opaque definition exfalso     : tactic := builtin
+opaque definition congruence  : tactic := builtin
 opaque definition rotate_left (k : num) := builtin
 opaque definition rotate_right (k : num) := builtin
 definition rotate (k : num) := rotate_left k

src/emacs/lean-syntax.el

@@ -136,7 +136,7 @@
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
                 "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp"
                 "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "left" "right"
-                "injection"))
+                "injection" "congruence"))
            word-end)
       (1 'font-lock-constant-face))
      ;; Types

src/library/constants.cpp

@@ -13,6 +13,7 @@ name const * g_bool_ff = nullptr;
 name const * g_bool_tt = nullptr;
 name const * g_char = nullptr;
 name const * g_char_mk = nullptr;
+name const * g_congr = nullptr;
 name const * g_dite = nullptr;
 name const * g_empty = nullptr;
 name const * g_empty_rec = nullptr;
@@ -139,6 +140,7 @@ void initialize_constants() {
     g_bool_tt = new name{"bool", "tt"};
     g_char = new name{"char"};
     g_char_mk = new name{"char", "mk"};
+    g_congr = new name{"congr"};
     g_dite = new name{"dite"};
     g_empty = new name{"empty"};
     g_empty_rec = new name{"empty", "rec"};
@@ -266,6 +268,7 @@ void finalize_constants() {
     delete g_bool_tt;
     delete g_char;
     delete g_char_mk;
+    delete g_congr;
     delete g_dite;
     delete g_empty;
     delete g_empty_rec;
@@ -392,6 +395,7 @@ name const & get_bool_ff_name() { return *g_bool_ff; }
 name const & get_bool_tt_name() { return *g_bool_tt; }
 name const & get_char_name() { return *g_char; }
 name const & get_char_mk_name() { return *g_char_mk; }
+name const & get_congr_name() { return *g_congr; }
 name const & get_dite_name() { return *g_dite; }
 name const & get_empty_name() { return *g_empty; }
 name const & get_empty_rec_name() { return *g_empty_rec; }

src/library/constants.h

@@ -15,6 +15,7 @@ name const & get_bool_ff_name();
 name const & get_bool_tt_name();
 name const & get_char_name();
 name const & get_char_mk_name();
+name const & get_congr_name();
 name const & get_dite_name();
 name const & get_empty_name();
 name const & get_empty_rec_name();

src/library/constants.txt

@@ -8,6 +8,7 @@ bool.ff
 bool.tt
 char
 char.mk
+congr
 dite
 empty
 empty.rec

src/library/tactic/CMakeLists.txt

@@ -5,6 +5,7 @@ inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp
 assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp
 rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp
 change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp
-exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp)
+exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp
+congruence_tactic.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/congruence_tactic.cpp

@@ -0,0 +1,123 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/util.h"
+#include "library/constants.h"
+#include "library/reducible.h"
+#include "library/tactic/util.h"
+#include "library/tactic/intros_tactic.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+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();
+        if (empty(gs)) {
+            throw_no_goal_if_enabled(s);
+            return none_proof_state();
+        }
+        goal const & g      = head(gs);
+        expr t              = g.get_type();
+        substitution subst  = s.get_subst();
+        name_generator ngen = s.get_ngen();
+        auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+        constraint_seq cs;
+        t = tc->whnf(t, cs);
+        expr lhs, rhs;
+        if (!is_eq(t, lhs, rhs)) {
+            throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, goal is not an equality");
+            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");
+                    return none_expr();
+                }
+                return mk_eq_goal(lhs, rhs);
+            }
+            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 mk_eq_goal(lhs, rhs);
+            }
+            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);
+            }
+
+            if (!closed(binding_body(fn_type))) {
+                if (first) {
+                    throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, cannot be applied to dependent functions");
+                    return none_expr();
+                }
+                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);
+            }
+
+            optional<expr> opt_fn_pr = process(lhs_fn, rhs_fn, false);
+            if (!opt_fn_pr)
+                return none_expr();
+            expr fn_pr = *opt_fn_pr;
+
+            expr A   = binding_domain(fn_type);
+            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);
+}
+void initialize_congruence_tactic() { register_simple_tac(name{"tactic", "congruence"}, congruence_tactic); }
+void finalize_congruence_tactic() {}
+}

src/library/tactic/congruence_tactic.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_congruence_tactic();
+void finalize_congruence_tactic();
+}

src/library/tactic/init_module.cpp

@@ -27,6 +27,7 @@ Author: Leonardo de Moura
 #include "library/tactic/exfalso_tactic.h"
 #include "library/tactic/constructor_tactic.h"
 #include "library/tactic/injection_tactic.h"
+#include "library/tactic/congruence_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -53,9 +54,11 @@ void initialize_tactic_module() {
     initialize_exfalso_tactic();
     initialize_constructor_tactic();
     initialize_injection_tactic();
+    initialize_congruence_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_congruence_tactic();
     finalize_injection_tactic();
     finalize_constructor_tactic();
     finalize_exfalso_tactic();

tests/lean/hott/congr_tac.hlean

@@ -0,0 +1,46 @@
+example (f : nat → nat → nat) (a b c : nat) : b = c → f a b = f a c :=
+begin
+  intro bc,
+  congruence,
+  assumption
+end
+
+example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c :=
+begin
+  intro fg bc,
+  congruence,
+  exact fg,
+  exact bc
+end
+
+example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c :=
+by intros; congruence; assumption
+
+inductive list (A : Type) :=
+| nil {} : list A
+| cons   : A → list A → list A
+
+namespace list
+notation `[` a `]` := list.cons a list.nil
+notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
+notation h :: t  := cons h t
+variable {T : Type}
+definition append : list T → list T → list T
+| []       l := l
+| (h :: s) t := h :: (append s t)
+notation l₁ ++ l₂ := append l₁ l₂
+end list
+open list
+
+example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] :=
+begin
+  intro ab,
+  congruence,
+  {congruence,
+   exact ab},
+  {congruence,
+   exact (eq.symm ab)}
+end
+
+example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] :=
+by intros; repeat (congruence | assumption | apply eq.symm)

tests/lean/run/congr_tac.lean

@@ -0,0 +1,34 @@
+import data.list
+
+example (f : nat → nat → nat) (a b c : nat) : b = c → f a b = f a c :=
+begin
+  intro bc,
+  congruence,
+  assumption
+end
+
+example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c :=
+begin
+  intro fg bc,
+  congruence,
+  exact fg,
+  exact bc
+end
+
+example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c :=
+by intros; congruence; assumption
+
+open list
+
+example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] :=
+begin
+  intro ab,
+  congruence,
+  {congruence,
+   exact ab},
+  {congruence,
+   exact (eq.symm ab)}
+end
+
+example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] :=
+by intros; repeat (congruence | assumption | apply eq.symm)