feat(frontends/lean): add new command for testing new congruence lemmas

Remark: #congr_simp is the old command, and #congr is the new one.

src/frontends/lean/builtin_cmds.cpp

@@ -1284,7 +1284,7 @@ static environment replace_cmd(parser & p) {
     return env;
 }
 
-static environment congr_lemma_cmd(parser & p) {
+static environment congr_cmd_core(parser & p, bool simp) {
     environment const & env = p.env();
     auto pos = p.pos();
     expr e; level_param_names ls;
@@ -1293,7 +1293,7 @@ static environment congr_lemma_cmd(parser & p) {
     app_builder         b(ctx);
     fun_info_manager    infom(ctx);
     congr_lemma_manager cm(b, infom);
-    auto r = cm.mk_congr_simp(e);
+    auto r = simp ? cm.mk_congr_simp(e) : cm.mk_congr(e);
     if (!r)
         throw parser_error("failed to generated congruence lemma", pos);
     auto out = p.regular_stream();
@@ -1316,6 +1316,14 @@ static environment congr_lemma_cmd(parser & p) {
     return env;
 }
 
+static environment congr_simp_cmd(parser & p) {
+    return congr_cmd_core(p, true);
+}
+
+static environment congr_cmd(parser & p) {
+    return congr_cmd_core(p, false);
+}
+
 static environment simplify_cmd(parser & p) {
     name rel = p.check_constant_next("invalid #simplify command, constant expected");
     unsigned o = p.parse_small_nat();
@@ -1376,7 +1384,8 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#symm",             "(for debugging purposes)", symm_cmd));
     add_cmd(r, cmd_info("#compile",          "(for debugging purposes)", compile_cmd));
     add_cmd(r, cmd_info("#replace",          "(for debugging purposes)", replace_cmd));
-    add_cmd(r, cmd_info("#congr",            "(for debugging purposes)", congr_lemma_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("#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));
     add_cmd(r, cmd_info("#relevant_thms",    "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd));

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", nullptr};
+         "#trans", "#replace", "#congr", "#congr_simp", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

tests/lean/congr1.lean

@@ -1,15 +1,16 @@
 import data.list
 
-#congr @add
-#congr @ite
-#congr @perm
+#congr_simp @add
+#congr_simp @ite
+#congr_simp @perm
+
 
 section
 variables p : nat → Prop
 variables q : nat → nat → Prop
 variables f : Π (x y : nat), p x → q x y → nat
 
-#congr f
+#congr_simp f
 end
 
 constant p : Π {A : Type}, A → Prop
@@ -19,4 +20,4 @@ constant h : Π (A : Type) (n m : A)
                (H₁ : p n) (H₂ : p m) (H₃ : q n n H₁ H₁) (H₄ : q n m H₁ H₂)
                (H₅ : r n m H₁ H₂ H₄) (H₆ : r n n H₁ H₁ H₃), A
 
-#congr h
+#congr_simp h

tests/lean/congr2.lean

@@ -0,0 +1,23 @@
+import data.list
+
+#congr @add
+#congr @perm
+
+section
+variables p : nat → Prop
+variables q : nat → nat → Prop
+variables f : Π (x y : nat), p x → q x y → nat
+
+#congr f
+end
+
+constant p : Π {A : Type}, A → Prop
+constant q : Π {A : Type} (n m : A), p n → p m → Prop
+constant r : Π {A : Type} (n m : A) (H₁ : p n) (H₂ : p m), q n m H₁ H₂ → Prop
+constant h : Π (A : Type) (n m : A)
+               (H₁ : p n) (H₂ : p m) (H₃ : q n n H₁ H₁) (H₄ : q n m H₁ H₂)
+               (H₅ : r n m H₁ H₂ H₄) (H₆ : r n n H₁ H₁ H₃), A
+
+#congr h
+
+#congr @ite

tests/lean/congr2.lean.expected.out

@@ -0,0 +1,50 @@
+[fixed, fixed, eq, eq]
+λ (A : Type) (c : has_add A) (a a_1 : A) (e_3 : a = a_1) (a_2 a_3 : A) (e_4 : a_2 = a_3), congr (congr_arg add e_3) e_4
+:
+∀ (A : Type) (c : has_add A) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → a + a_2 = a_1 + a_3)
+[fixed, eq, eq]
+λ (A : Type) (a a_1 : list A) (e_2 : a = a_1) (a_2 a_3 : list A) (e_3 : a_2 = a_3), congr (congr_arg perm e_2) e_3
+:
+∀ (A : Type) (a a_1 : list A), a = a_1 → (∀ (a_2 a_3 : list A), a_2 = a_3 → perm a a_2 = perm a_1 a_3)
+[eq, eq, cast, cast]
+λ (x x_1 : ℕ) (e_1 : x = x_1) (y y_1 : ℕ) (e_2 : y = y_1) (a : p x) (a_1 : p x_1) (a_1 : q x y) (a_2 : q x_1 y_1),
+  eq.drec (eq.drec (eq.refl (f x y (eq.rec a (eq.refl x)) (eq.rec (eq.rec a_1 (eq.refl y)) (eq.refl x)))) e_2) e_1
+:
+∀ (x x_1 : ℕ),
+  x = x_1 →
+  (∀ (y y_1 : ℕ),
+     y = y_1 → (∀ (a : p x) (a_1 : p x_1) (a_2 : q x y) (a_3 : q x_1 y_1), f x y a a_2 = f x_1 y_1 a_1 a_3))
+[fixed, eq, eq, cast, cast, cast, cast, cast, cast]
+λ (A : Type) (n n_1 : A) (e_2 : n = n_1) (m m_1 : A) (e_3 : m = m_1) (H₁ : p n) (H₁_1 : p n_1) (H₂ : p m)
+(H₂_1 : p m_1) (H₃ : q n n H₁ H₁) (H₃_1 : q n_1 n_1 H₁_1 H₁_1) (H₄ : q n m H₁ H₂)
+(H₄_1 : q n_1 m_1 H₁_1 H₂_1) (H₅ : r n m H₁ H₂ H₄) (H₅_1 : r n_1 m_1 H₁_1 H₂_1 H₄_1)
+(H₆ : r n n H₁ H₁ H₃) (H₆_1 : r n_1 n_1 H₁_1 H₁_1 H₃_1),
+  eq.drec
+    (eq.drec
+       (eq.refl
+          (h A n m (eq.rec H₁ (eq.refl n)) (eq.rec H₂ (eq.refl m)) (eq.drec H₃ (eq.refl n))
+             (eq.drec (eq.drec H₄ (eq.refl m)) (eq.refl n))
+             (eq.drec (eq.drec H₅ (eq.refl m)) (eq.refl n))
+             (eq.drec H₆ (eq.refl n))))
+       e_3)
+    e_2
+:
+∀ (A : Type) (n n_1 : A),
+  n = n_1 →
+  (∀ (m m_1 : A),
+     m = m_1 →
+     (∀ (H₁ : p n) (H₁_1 : p n_1) (H₂ : p m) (H₂_1 : p m_1) (H₃ : q n n H₁ H₁)
+      (H₃_1 : q n_1 n_1 H₁_1 H₁_1) (H₄ : q n m H₁ H₂) (H₄_1 : q n_1 m_1 H₁_1 H₂_1)
+      (H₅ : r n m H₁ H₂ H₄) (H₅_1 : r n_1 m_1 H₁_1 H₂_1 H₄_1) (H₆ : r n n H₁ H₁ H₃)
+      (H₆_1 : r n_1 n_1 H₁_1 H₁_1 H₃_1),
+        h A n m H₁ H₂ H₃ H₄ H₅ H₆ = h A n_1 m_1 H₁_1 H₂_1 H₃_1 H₄_1 H₅_1 H₆_1))
+[eq, cast, fixed, eq, eq]
+λ (c c_1 : Prop) (e_1 : c = c_1) (H : decidable c) (H_1 : decidable c_1) (A : Type) (t t_1 : A) (e_4 : t = t_1)
+(e e_2 : A) (e_5 : e = e_2),
+  eq.trans (eq.drec (eq.drec (eq.drec (eq.refl (ite c t e)) e_5) e_4) e_1)
+    (congr_fun (congr_fun (congr_fun (congr (eq.refl (ite c_1)) (subsingleton.elim (eq.rec H e_1) H_1)) A) t_1) e_2)
+:
+∀ (c c_1 : Prop),
+  c = c_1 →
+  (∀ (H : decidable c) (H_1 : decidable c_1) (A : Type) (t t_1 : A),
+     t = t_1 → (∀ (e e_1 : A), e = e_1 → ite c t e = ite c_1 t_1 e_1))