From f36397585603bc261dc5a53747a3c4c85ca83115 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Nov 2015 15:43:10 -0800
Subject: [PATCH] feat(frontends/lean): add command #congr_rel for testing new
 congruence lemma for equivalence relations

---
 src/frontends/lean/builtin_cmds.cpp | 20 ++++++++++++++++----
 src/frontends/lean/token_table.cpp  |  2 +-
 tests/lean/congr_rel.lean           |  6 ++++++
 3 files changed, 23 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/congr_rel.lean

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index f2ea0d3db..9f2289a90 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -1287,7 +1287,9 @@ static environment replace_cmd(parser & p) {
     return env;
 }
 
-static environment congr_cmd_core(parser & p, bool simp) {
+enum class congr_kind { Simp, Default, Rel };
+
+static environment congr_cmd_core(parser & p, congr_kind kind) {
     environment const & env = p.env();
     auto pos = p.pos();
     expr e; level_param_names ls;
@@ -1296,7 +1298,12 @@ static environment congr_cmd_core(parser & p, bool simp) {
     app_builder         b(ctx);
     fun_info_manager    infom(ctx);
     congr_lemma_manager cm(b, infom);
-    auto r = simp ? cm.mk_congr_simp(e) : cm.mk_congr(e);
+    optional<congr_lemma> r;
+    switch (kind) {
+    case congr_kind::Simp:    r = cm.mk_congr_simp(e); break;
+    case congr_kind::Default: r = cm.mk_congr(e); break;
+    case congr_kind::Rel:     r = cm.mk_rel_iff_congr(e); break;
+    }
     if (!r)
         throw parser_error("failed to generated congruence lemma", pos);
     auto out = p.regular_stream();
@@ -1320,11 +1327,15 @@ static environment congr_cmd_core(parser & p, bool simp) {
 }
 
 static environment congr_simp_cmd(parser & p) {
-    return congr_cmd_core(p, true);
+    return congr_cmd_core(p, congr_kind::Simp);
 }
 
 static environment congr_cmd(parser & p) {
-    return congr_cmd_core(p, false);
+    return congr_cmd_core(p, congr_kind::Default);
+}
+
+static environment congr_rel_cmd(parser & p) {
+    return congr_cmd_core(p, congr_kind::Rel);
 }
 
 static environment simplify_cmd(parser & p) {
@@ -1435,6 +1446,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#replace",          "(for debugging purposes)", replace_cmd));
     add_cmd(r, cmd_info("#congr",            "(for debugging purposes)", congr_cmd));
     add_cmd(r, cmd_info("#congr_simp",       "(for debugging purposes)", congr_simp_cmd));
+    add_cmd(r, cmd_info("#congr_rel",        "(for debugging purposes)", congr_rel_cmd));
     add_cmd(r, cmd_info("#normalizer",       "(for debugging purposes)", normalizer_cmd));
     add_cmd(r, cmd_info("#accessible",       "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
     add_cmd(r, cmd_info("#decl_stats",       "(for debugging purposes) display declaration statistics", decl_stats_cmd));
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index e0a11662b..421fa67a0 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -121,7 +121,7 @@ void init_token_table(token_table & t) {
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
          "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm",
-         "#trans", "#replace", "#congr", "#congr_simp", "#normalizer", "#abstract_expr", nullptr};
+         "#trans", "#replace", "#congr", "#congr_simp", "#congr_rel", "#normalizer", "#abstract_expr", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
diff --git a/tests/lean/congr_rel.lean b/tests/lean/congr_rel.lean
new file mode 100644
index 000000000..57ce18cc3
--- /dev/null
+++ b/tests/lean/congr_rel.lean
@@ -0,0 +1,6 @@
+import data.list
+open perm
+
+#congr_rel @eq
+#congr_rel @iff
+#congr_rel @perm