feat(frontends/lean): display '[congr]' attribute when printing theorems

src/frontends/lean/builtin_cmds.cpp

@@ -192,6 +192,8 @@ void print_attributes(parser & p, name const & n) {
         out << " [instance]";
     if (is_simp_rule(env, n))
         out << " [simp]";
+    if (is_congr_rule(env, n))
+        out << " [congr]";
     switch (get_reducible_status(env, n)) {
     case reducible_status::Reducible:      out << " [reducible]"; break;
     case reducible_status::Irreducible:    out << " [irreducible]"; break;

src/library/simplifier/simp_rule_set.cpp

@@ -382,16 +382,18 @@ void add_congr_core(environment const & env, simp_rule_sets & s, name const & n)
 
 struct rrs_state {
     simp_rule_sets           m_sets;
-    name_set                 m_snames;
+    name_set                 m_simp_names;
+    name_set                 m_congr_names;
 
     void add_simp(environment const & env, name const & cname) {
         type_checker tc(env);
         m_sets = add_core(tc, m_sets, cname);
-        m_snames.insert(cname);
+        m_simp_names.insert(cname);
     }
 
     void add_congr(environment const & env, name const & n) {
         add_congr_core(env, m_sets, n);
+        m_congr_names.insert(n);
     }
 };
 
@@ -433,7 +435,11 @@ environment add_congr_rule(environment const & env, name const & n, bool persist
 }
 
 bool is_simp_rule(environment const & env, name const & n) {
-    return rrs_ext::get_state(env).m_snames.contains(n);
+    return rrs_ext::get_state(env).m_simp_names.contains(n);
+}
+
+bool is_congr_rule(environment const & env, name const & n) {
+    return rrs_ext::get_state(env).m_congr_names.contains(n);
 }
 
 simp_rule_sets get_simp_rule_sets(environment const & env) {

src/library/simplifier/simp_rule_set.h

@@ -106,6 +106,8 @@ environment add_congr_rule(environment const & env, name const & n, bool persist
 
 /** \brief Return true if \c n is an active simplification rule in \c env */
 bool is_simp_rule(environment const & env, name const & n);
+/** \brief Return true if \c n is an active congruence rule in \c env */
+bool is_congr_rule(environment const & env, name const & n);
 /** \brief Get current simplification rule sets */
 simp_rule_sets get_simp_rule_sets(environment const & env);
 /** \brief Get simplification rule sets in the given namespace. */

tests/lean/congr_print.lean

@@ -0,0 +1,5 @@
+import data.list
+open list perm
+
+set_option pp.max_depth 10
+print perm_erase_dup_of_perm

tests/lean/congr_print.lean.expected.out

@@ -0,0 +1,20 @@
+theorem perm.perm_erase_dup_of_perm [congr] : ∀ {A : Type} [H : decidable_eq A] {l₁ l₂ : list A}, l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ :=
+λ (A : Type) (H : decidable_eq A) (l₁ l₂ : list A) (p : l₁ ~ l₂),
+  perm_induction_on p nil
+    (λ (x : A) (t₁ t₂ : list A) (p : t₁ ~ t₂) (r : erase_dup t₁ ~ erase_dup t₂),
+       decidable.by_cases
+         (λ (xint₁ : x ∈ t₁), assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup …, … …)
+         (λ (nxint₁ : x ∉ t₁),
+            assert nxint₂ : x ∉ t₂, from λ (xint₂ : x ∈ t₂), … nxint₁,
+            eq.rec … (eq.symm …)))
+    (λ (y x : A) (t₁ t₂ : list A) (p : t₁ ~ t₂) (r : erase_dup t₁ ~ erase_dup t₂),
+       decidable.by_cases
+         (λ (xinyt₁ : x ∈ y :: t₁),
+            decidable.by_cases (λ (yint₁ : …), …)
+              (λ (nyint₁ : y ∉ t₁), assert nyint₂ : …, from …, …))
+         (λ (nxinyt₁ : x ∉ y :: t₁),
+            have xney : x ≠ y, from ne_of_not_mem_cons nxinyt₁,
+            have nxint₁ : x ∉ t₁, from not_mem_of_not_mem_cons nxinyt₁,
+            assert nxint₂ : x ∉ t₂, from λ (xint₂ : …), …,
+            … …))
+    (λ (t₁ t₂ t₃ : list A) (p₁ : t₁ ~ t₂) (p₂ : t₂ ~ t₃), trans)