From 0d978d44293c4bb575dc8fb3feb0d704bd48b4a9 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 27 Mar 2022 19:09:13 -0700 Subject: [PATCH] feat(simp_lemmas): allow user congr lemma to have fixed parameters --- src/library/tactic/simp_lemmas.cpp | 5 ++++- tests/lean/congr_user_fixed.lean | 21 +++++++++++++++++++ tests/lean/congr_user_fixed.lean.expected.out | 2 ++ 3 files changed, 27 insertions(+), 1 deletion(-) create mode 100644 tests/lean/congr_user_fixed.lean create mode 100644 tests/lean/congr_user_fixed.lean.expected.out diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index 0e7b3807e8..e39539f478 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/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 (" diff --git a/tests/lean/congr_user_fixed.lean b/tests/lean/congr_user_fixed.lean new file mode 100644 index 0000000000..46eaa8d6dd --- /dev/null +++ b/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 diff --git a/tests/lean/congr_user_fixed.lean.expected.out b/tests/lean/congr_user_fixed.lean.expected.out new file mode 100644 index 0000000000..98d6779013 --- /dev/null +++ b/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