feat(simp_lemmas): allow user congr lemma to have fixed parameters

src/library/tactic/simp_lemmas.cpp

@@ -993,9 +993,12 @@ static simp_lemmas add_congr_core(type_context_old & ctx, simp_lemmas const & s,
                            << "' resulting type is not of the form (" << const_name(lhs_fn) << "  ...) "
                            << "~ (" << const_name(lhs_fn) << " ...), where ~ is '" << const_name(rel) << "'");
         }
-        for (expr const & lhs_arg : lhs_args) {
+        for (unsigned i = 0; i < lhs_args.size(); i++) {
+            expr const & lhs_arg = lhs_args[i], & rhs_arg = rhs_args[i];
             if (is_sort(lhs_arg))
                 continue;
+            if (!has_metavar(lhs_arg) && lhs_arg == rhs_arg)
+                continue;
             if (!is_metavar(lhs_arg) || found_mvars.contains(mlocal_name(lhs_arg))) {
                 report_failure(sstream() << "invalid congruence lemma, '" << n
                                << "' the left-hand-side of the congruence resulting type must be of the form ("

tests/lean/congr_user_fixed.lean

@@ -0,0 +1,21 @@
+def mod5 (a b : ℕ) : Prop := a % 5 = b % 5
+
+infix ` ≡ `:50 := mod5
+
+@[refl] theorem mod5.refl (a : ℕ) : a ≡ a := @rfl _ _
+
+@[symm] theorem mod5.symm (a b : ℕ) : a ≡ b → b ≡ a := eq.symm
+
+@[trans] theorem mod5.trans (a b c : ℕ) : a ≡ b → b ≡ c → a ≡ c := eq.trans
+
+@[congr]
+theorem mod5.add (a b c d : ℕ) (h₁ : a ≡ b) (h₂ : c ≡ d) : a + c ≡ b + d := sorry
+
+@[congr]
+theorem mod5.congr (a b c d : ℕ) (h1 : a ≡ c) (h2 : b ≡ d) : (a ≡ b) = (c ≡ d) := sorry
+
+example (a b c d : ℕ) (h : a ≡ b + c) (h' : c + c ≡ 2*c) (h'' : b + c + c ≡ b + (c + c)) :
+  a + c ≡ b + 2*c :=
+begin
+  simp only [h, h', h''],
+end

tests/lean/congr_user_fixed.lean.expected.out

@@ -0,0 +1,2 @@
+congr_user_fixed.lean:12:0: warning: declaration 'mod5.add' uses sorry
+congr_user_fixed.lean:15:0: warning: declaration 'mod5.congr' uses sorry