feat(by_contra,contrapose): warn if the push_neg step does nothing

Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean

@@ -172,7 +172,7 @@ theorem ofPowerSeries_pow (q : ℕ) {k : ℕ} (hk : k ≠ 0) (f : PowerSeries R)
         exact hn
     · rwa [ofPowerSeries_apply hq, ofPowerSeries_apply (one_lt_pow' hq hk),
         Function.extend_apply', Function.extend_apply']
-      contrapose! hn
+      contrapose hn
       obtain ⟨i, rfl⟩ := hn
       exact ⟨k * i, pow_mul q k i⟩
   · simp [ofPowerSeries, hq, hk]
@@ -198,14 +198,14 @@ theorem isMultiplicative_ofPowerSeries_of_isPrimePow
     · simp_rw [ofPowerSeries_apply hp.one_lt]
       rw [Function.extend_apply', Function.extend_apply' _ _ _ hn,
         Pi.zero_apply, Pi.zero_apply, mul_zero]
-      contrapose! hn
+      contrapose hn
       obtain ⟨j, hj⟩ := hn
       obtain ⟨v, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp (Dvd.intro_left _ hj.symm)
       exact ⟨v, rfl⟩
   · simp_rw [ofPowerSeries_apply hp.one_lt]
     rw [Function.extend_apply', Function.extend_apply' _ _ _ hm,
       Pi.zero_apply, Pi.zero_apply, zero_mul]
-    contrapose! hm
+    contrapose hm
     obtain ⟨i, hi⟩ := hm
     obtain ⟨j, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp ⟨n, hi⟩
     exact ⟨j, rfl⟩

Mathlib/Tactic/ByContra.lean

@@ -54,7 +54,7 @@ local elab "try_push_neg_at" cfg:optConfig h:ident : tactic => do
 
 local elab "try_push_neg" cfg:optConfig : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[] true)
-    (ifUnchanged := .silent)
+    (ifUnchanged := .warning)
 
 macro_rules
 | `(tactic| by_contra! $cfg $[$pat?]? $[: $ty?]?) => do

Mathlib/Tactic/Contrapose.lean

@@ -127,7 +127,7 @@ syntax (name := contrapose!)
 
 local elab "try_push_neg" cfg:optConfig : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[] true)
-    (ifUnchanged := .silent)
+    (ifUnchanged := .warning)
 
 macro_rules
   | `(tactic| contrapose! $cfg) => `(tactic| (contrapose; try_push_neg $cfg))

MathlibTest/Contrapose.lean

@@ -38,20 +38,43 @@ example (p q : Prop) (h : ¬q → p) : ¬p → q := by
   exact h
 
 example (p q : Prop) (h : q → p) : ¬p → ¬q := by
-  contrapose!
+  contrapose
   guard_target = q → p
   exact h
 
+example (p q : Prop) (h : ¬p) (hpq : q → p) : ¬q := by
+  contrapose h
+  guard_target = p
+  exact hpq h
+
+example (p q : Prop) (h : ¬p) (hpq : q → p) : ¬q := by
+  contrapose h with h'
+  guard_target = p
+  exact hpq h'
+
+example (p q : Prop) (h : q → p) : ¬p → ¬q := by
+  contrapose
+  guard_target = q → p
+  exact h
+
+section -- Using contrapose in a superfluous way warns.
+
+/-- warning: `push` made no progress on the goal -/
+#guard_msgs in
 example (p q : Prop) (h : ¬p) (hpq : q → p) : ¬q := by
   contrapose! h
   guard_target = p
   exact hpq h
 
+/-- warning: `push` made no progress on the goal -/
+#guard_msgs in
 example (p q : Prop) (h : ¬p) (hpq : q → p) : ¬q := by
   contrapose! h with h'
   guard_target = p
   exact hpq h'
 
+end
+
 example (p q r : Prop) (h : ¬ q ∧ ¬ r → ¬ p) : p → q ∨ r := by
   fail_if_success (contrapose; exact h)
   contrapose!; exact h

MathlibTest/byContra.lean

@@ -85,6 +85,12 @@ example (x : α) (f : False) : x ≤ 1 := by
 
 end order
 
+example (n : ℕ) (h : n ≠ 0) : n ≠ 0 := by
+  by_contra rfl
+  simp only [Ne, not_true_eq_false] at h
+
+/-- warning: `push` made no progress at h._@.MathlibTest.byContra.2021293407._hygCtx._hyg.18 -/
+#guard_msgs in
 example (n : ℕ) (h : n ≠ 0) : n ≠ 0 := by
   by_contra! rfl
   simp only [Ne, not_true_eq_false] at h
@@ -93,6 +99,13 @@ example (p q : Prop) (hnp : ¬ p) : ¬ p ∨ ¬ q := by
   by_contra! ⟨hp, _⟩
   exact hnp hp
 
+example (p q : Prop) (hnp : ¬ p) (hnq : ¬ q) : ¬ (p ∨ q) := by
+  by_contra hp | hq
+  · exact hnp hp
+  · exact hnq hq
+
+/-- warning: `push` made no progress at h._@.MathlibTest.byContra.2021293410._hygCtx._hyg.25 -/
+#guard_msgs in
 example (p q : Prop) (hnp : ¬ p) (hnq : ¬ q) : ¬ (p ∨ q) := by
   by_contra! hp | hq
   · exact hnp hp