feat(library/tactic): expose congr_lemmas

This commit also adds several helper code, and fixes bugs in congr_lemma.cpp

library/init/meta/congr_lemma.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.tactic init.meta.format init.function
+
+inductive congr_arg_kind :=
+/- It is a parameter for the congruence lemma, the parameter occurs in the left and right hand sides. -/
+| fixed
+/- 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. -/
+| fixed_no_param
+/- 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. -/
+| eq
+/- 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. -/
+| cast
+/- 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 heterogeneous equality. -/
+| heq
+
+structure congr_lemma :=
+(type : expr) (proof : expr) (arg_kids : list congr_arg_kind)
+
+namespace tactic
+meta_constant mk_congr_simp   : expr → tactic congr_lemma
+meta_constant mk_congr_simp_n : expr → nat → tactic congr_lemma
+/- Create a specialized theorem using (a prefix of) the arguments of the given application. -/
+meta_constant mk_specialized_congr_simp : expr → tactic congr_lemma
+
+meta_constant mk_congr   : expr → tactic congr_lemma
+meta_constant mk_congr_n : expr → nat → tactic congr_lemma
+/- Create a specialized theorem using (a prefix of) the arguments of the given application. -/
+meta_constant mk_specialized_congr : expr → tactic congr_lemma
+
+meta_constant mk_hcongr   : expr → tactic congr_lemma
+meta_constant mk_hcongr_n : expr → nat → tactic congr_lemma
+
+/- If R is an equivalence relation, construct the congruence lemma
+   R a1 a2 -> R b1 b2 -> (R a1 b1) <-> (R a2 b2) -/
+meta_constant mk_rel_iff_congr : expr → tactic congr_lemma
+
+/- Similar to mk_rel_iff_congr
+   It fails if propext is not available.
+
+   R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) -/
+meta_constant mk_rel_eq_congr : expr → tactic congr_lemma
+end tactic

library/init/meta/default.lean

@@ -8,3 +8,4 @@ import init.meta.name init.meta.options init.meta.format init.meta.rb_map
 import init.meta.level init.meta.expr init.meta.base_tactic init.meta.environment
 import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tactic
 import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info
+import init.meta.congr_lemma

src/library/congr_lemma.cpp

@@ -72,7 +72,7 @@ struct congr_lemma_manager {
             return cast(e, type, tail(deps), eqs);
         } else {
             expr lhs, rhs;
-            lean_verify(is_eq(mlocal_type(*major), lhs, rhs));
+            lean_verify(is_eq(m_ctx.infer(*major), lhs, rhs));
             lean_assert(is_local(lhs));
             lean_assert(is_local(rhs));
             // We compute the new type by replacing rhs with lhs, and major with (refl lhs).
@@ -147,7 +147,7 @@ struct congr_lemma_manager {
         } else {
             expr major = *eqs[i];
             expr x_1, x_2;
-            lean_verify(is_eq(mlocal_type(major), x_1, x_2));
+            lean_verify(is_eq(m_ctx.infer(major), x_1, x_2));
             lean_assert(is_local(x_1));
             lean_assert(is_local(x_2));
             expr motive_eq = mk_eq(m_ctx, lhs, rhs);
@@ -491,9 +491,9 @@ struct congr_lemma_manager {
             lean_assert(closed(type) && closed(motive));
             expr minor  = mk_hcongr_proof(type);
             expr major  = eq_pr;
-            if (is_heq(mlocal_type(eq_pr)))
+            if (is_heq(m_ctx.infer(eq_pr)))
                 major  = mk_eq_of_heq(m_ctx, eq_pr);
-            motive      = Fun(b, motive);
+            motive      = m_ctx.mk_lambda({b}, motive);
             return m_ctx.mk_lambda({a, b, eq_pr}, mk_eq_rec(m_ctx, motive, minor, major));
         }
     }

src/library/congr_lemma.h

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 enum class congr_arg_kind {
-    /* It is a parameter for the congruence lemma, the parit occurs in the left and right hand sides. */
+    /* It is a parameter for the congruence lemma, the parameter occurs in the left and right hand sides. */
     Fixed,
     /* 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. */

src/library/tactic/CMakeLists.txt

@@ -2,4 +2,5 @@ add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp
   revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp
   app_builder_tactics.cpp subst_tactic.cpp exact_tactic.cpp
   change_tactic.cpp assert_tactic.cpp apply_tactic.cpp
-  fun_info_tactics.cpp elaborate.cpp init_module.cpp)
+  fun_info_tactics.cpp congr_lemma_tactics.cpp
+  elaborate.cpp init_module.cpp)

src/library/tactic/congr_lemma_tactics.cpp

@@ -0,0 +1,127 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/congr_lemma.h"
+#include "library/vm/vm_list.h"
+#include "library/vm/vm_expr.h"
+#include "library/vm/vm_nat.h"
+#include "library/tactic/tactic_state.h"
+
+namespace lean {
+vm_obj to_obj(congr_arg_kind k) {
+    return mk_vm_simple(static_cast<unsigned>(k));
+}
+
+vm_obj to_obj(list<congr_arg_kind> const & ls) {
+    return to_vm_list(ls, [&](congr_arg_kind const & k) { return to_obj(k); });
+}
+
+/*
+ structure congr_lemma :=
+ (type : expr) (proof : expr) (arg_kids : list congr_arg_kind)
+*/
+vm_obj to_obj(congr_lemma const & c) {
+    return mk_vm_constructor(0, to_obj(c.get_type()), to_obj(c.get_proof()), to_obj(c.get_arg_kinds()));
+}
+
+static vm_obj mk_result(optional<congr_lemma> const & l, vm_obj const & s) {
+    if (l)
+        return mk_tactic_success(to_obj(*l), to_tactic_state(s));
+    else
+        return mk_tactic_exception("failed to generate congruence lemma, "
+                                   "use 'set_option trace.congr_lemma true' to obtain additional information",
+                                   to_tactic_state(s));
+}
+
+#define TRY   LEAN_TACTIC_TRY
+#define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s))
+
+vm_obj tactic_mk_congr_simp(vm_obj const & fn, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_congr_simp(ctx, to_expr(fn)), s);
+    CATCH;
+}
+
+vm_obj tactic_mk_congr_simp_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_congr_simp(ctx, to_expr(fn), force_to_unsigned(n, 0)), s);
+    CATCH;
+}
+
+vm_obj tactic_mk_specialized_congr_simp(vm_obj const & a, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_specialized_congr_simp(ctx, to_expr(a)), s);
+    CATCH;
+}
+
+vm_obj tactic_mk_congr(vm_obj const & fn, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_congr(ctx, to_expr(fn)), s);
+    CATCH;
+}
+
+vm_obj tactic_mk_congr_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_congr(ctx, to_expr(fn), force_to_unsigned(n, 0)), s);
+    CATCH;
+}
+
+vm_obj tactic_mk_specialized_congr(vm_obj const & a, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_specialized_congr(ctx, to_expr(a)), s);
+    CATCH;
+}
+
+vm_obj tactic_mk_hcongr(vm_obj const & fn, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_hcongr(ctx, to_expr(fn)), s);
+    CATCH;
+}
+
+vm_obj tactic_mk_hcongr_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_hcongr(ctx, to_expr(fn), force_to_unsigned(n, 0)), s);
+    CATCH;
+}
+
+vm_obj tactic_mk_rel_iff_congr(vm_obj const & r, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_rel_iff_congr(ctx, to_expr(r)), s);
+    CATCH;
+}
+
+vm_obj tactic_mk_rel_eq_congr(vm_obj const & r, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(mk_rel_eq_congr(ctx, to_expr(r)), s);
+    CATCH;
+}
+
+void initialize_congr_lemma_tactics() {
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_simp"}),             tactic_mk_congr_simp);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_simp_n"}),           tactic_mk_congr_simp_n);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr_simp"}), tactic_mk_specialized_congr_simp);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_congr"}),                  tactic_mk_congr);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_n"}),                tactic_mk_congr_n);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr"}),      tactic_mk_specialized_congr);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_hcongr"}),                 tactic_mk_hcongr);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_hcongr_n"}),               tactic_mk_hcongr_n);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_iff_congr"}),          tactic_mk_rel_iff_congr);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_eq_congr"}),           tactic_mk_rel_eq_congr);
+}
+
+void finalize_congr_lemma_tactics() {
+}
+}

src/library/tactic/congr_lemma_tactics.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2016 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_congr_lemma_tactics();
+void finalize_congr_lemma_tactics();
+}

src/library/tactic/fun_info_tactics.cpp

@@ -65,32 +65,40 @@ fun_info get_fun_info(type_context & ctx, expr const & fn, unsigned nargs);
 fun_info get_specialized_fun_info(type_context & ctx, expr const & app);
 unsigned get_specialization_prefix_size(type_context & ctx, expr const & fn, unsigned nargs);
 
-vm_obj tactic_get_fun_info(vm_obj const & fn, vm_obj const & s0) {
-    tactic_state const & s = to_tactic_state(s0);
-    metavar_context mctx_tmp   = s.mctx();
-    type_context ctx = mk_type_context_for(s, mctx_tmp);
-    return mk_tactic_success(to_obj(get_fun_info(ctx, to_expr(fn))), s);
+#define TRY   LEAN_TACTIC_TRY
+#define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s))
+
+static vm_obj mk_result(fun_info const & info, vm_obj const & s) {
+    return mk_tactic_success(to_obj(info), to_tactic_state(s));
 }
 
-vm_obj tactic_get_fun_info_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s0) {
-    tactic_state const & s = to_tactic_state(s0);
-    metavar_context mctx_tmp   = s.mctx();
-    type_context ctx = mk_type_context_for(s, mctx_tmp);
-    return mk_tactic_success(to_obj(get_fun_info(ctx, to_expr(fn), force_to_unsigned(n, 0))), s);
+vm_obj tactic_get_fun_info(vm_obj const & fn, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(get_fun_info(ctx, to_expr(fn)), s);
+    CATCH;
 }
 
-vm_obj tactic_get_spec_fun_info(vm_obj const & app, vm_obj const & s0) {
-    tactic_state const & s = to_tactic_state(s0);
-    metavar_context mctx_tmp   = s.mctx();
-    type_context ctx = mk_type_context_for(s, mctx_tmp);
-    return mk_tactic_success(to_obj(get_specialized_fun_info(ctx, to_expr(app))), s);
+vm_obj tactic_get_fun_info_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(get_fun_info(ctx, to_expr(fn), force_to_unsigned(n, 0)), s);
+    CATCH;
 }
 
-vm_obj tactic_get_spec_prefix_size(vm_obj const & fn, vm_obj const & n, vm_obj const & s0) {
-    tactic_state const & s = to_tactic_state(s0);
-    metavar_context mctx_tmp   = s.mctx();
-    type_context ctx = mk_type_context_for(s, mctx_tmp);
-    return mk_tactic_success(to_obj(get_specialization_prefix_size(ctx, to_expr(fn), force_to_unsigned(n, 0))), s);
+vm_obj tactic_get_spec_fun_info(vm_obj const & app, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_result(get_specialized_fun_info(ctx, to_expr(app)), s);
+    CATCH;
+}
+
+vm_obj tactic_get_spec_prefix_size(vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
+    TRY;
+    type_context_scope ctx(s);
+    return mk_tactic_success(mk_vm_nat(get_specialization_prefix_size(ctx, to_expr(fn), force_to_unsigned(n, 0))),
+                             to_tactic_state(s));
+    CATCH;
 }
 
 void initialize_fun_info_tactics() {

src/library/tactic/init_module.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "library/tactic/assert_tactic.h"
 #include "library/tactic/apply_tactic.h"
 #include "library/tactic/fun_info_tactics.h"
+#include "library/tactic/congr_lemma_tactics.h"
 #include "library/tactic/elaborate.h"
 #include "library/tactic/defeq_simplifier/init_module.h"
 
@@ -33,12 +34,14 @@ void initialize_tactic_module() {
     initialize_assert_tactic();
     initialize_apply_tactic();
     initialize_fun_info_tactics();
+    initialize_congr_lemma_tactics();
     initialize_elaborate();
     initialize_defeq_simplifier_module();
 }
 void finalize_tactic_module() {
     finalize_defeq_simplifier_module();
     finalize_elaborate();
+    finalize_congr_lemma_tactics();
     finalize_fun_info_tactics();
     finalize_apply_tactic();
     finalize_assert_tactic();

src/library/tactic/tactic_state.cpp

@@ -79,8 +79,7 @@ tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx
 }
 
 format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) const {
-    metavar_context mctx_tmp   = mctx();
-    type_context ctx = mk_type_context_for(*this, mctx_tmp, transparency_mode::All);
+    type_context_scope ctx(*this, transparency_mode::All);
     formatter fmt = fmtf(env(), get_options(), ctx);
     return fmt(e);
 }

src/library/tactic/tactic_state.h

@@ -123,6 +123,19 @@ inline type_context mk_type_context_for(tactic_state const & s, metavar_context
     Code                                                \
 })
 
+struct type_context_scope {
+    metavar_context m_mctx;
+    type_context    m_ctx;
+    type_context_scope(tactic_state const & s, transparency_mode m = transparency_mode::Semireducible):
+        m_mctx(s.mctx()), m_ctx(mk_type_context_for(s, m_mctx, m)) {}
+    type_context_scope(vm_obj const & s, transparency_mode m = transparency_mode::Semireducible):
+        type_context_scope(to_tactic_state(s), m) {}
+    operator type_context &() { return m_ctx; }
+};
+
+#define LEAN_TACTIC_TRY try {
+#define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return mk_tactic_exception(ex, S); }
+
 void initialize_tactic_state();
 void finalize_tactic_state();
 }

tests/lean/run/congr_lemma1.lean

@@ -0,0 +1,12 @@
+open tactic
+
+set_option pp.binder_types true
+
+example : true :=
+by do
+  ite ← mk_const "ite",
+  l   ← mk_congr_simp ite,
+  trace_expr (congr_lemma.type l),
+  l   ← mk_hcongr ite,
+  trace_expr (congr_lemma.type l),
+  constructor