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

Mathlib/Tactic/Abel.lean

@@ -506,7 +506,7 @@ elab (name := abelNF) "abel_nf" tk:"!"? cfg:optConfig loc:(location)? : tactic =
   let loc := (loc.map expandLocation).getD (.targets #[] true)
   let s ← IO.mkRef {}
   let m := AtomM.recurse s cfg.toConfig (wellBehavedDischarge := true) evalExpr (cleanup cfg)
-  transformAtLocation (m ·) "abel_nf" loc (failIfUnchanged := true) false
+  transformAtLocation (m ·) "abel_nf" loc (ifUnchanged := .error) false
 
 @[tactic_alt abel]
 macro "abel_nf!" cfg:optConfig loc:(location)? : tactic =>

Mathlib/Tactic/ByCases.lean

@@ -32,7 +32,7 @@ syntax (name := byCases!) "by_cases! " optConfig (atomic(ident " : "))? term : t
 
 local elab "try_push_neg_at" cfg:optConfig h:ident : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[h] false)
-    (failIfUnchanged := false)
+    (ifUnchanged := .warning)
 
 macro_rules
   | `(tactic| by_cases! $cfg:optConfig $e) => `(tactic| by_cases! $cfg h : $e)

Mathlib/Tactic/ByContra.lean

@@ -50,11 +50,11 @@ syntax (name := byContra!)
 
 local elab "try_push_neg_at" cfg:optConfig h:ident : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[h] false)
-    (failIfUnchanged := false)
+    (ifUnchanged := .silent)
 
 local elab "try_push_neg" cfg:optConfig : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[] true)
-    (failIfUnchanged := false)
+    (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)
-    (failIfUnchanged := false)
+    (ifUnchanged := .warning)
 
 macro_rules
   | `(tactic| contrapose! $cfg) => `(tactic| (contrapose; try_push_neg $cfg))

Mathlib/Tactic/Field.lean

@@ -69,7 +69,7 @@ elab (name := field) "field" d:(ppSpace discharger)? args:(ppSpace simpArgs)? :
   let s0 ← saveState
   -- run `field_simp` (only at the top level, not recursively)
   liftMetaTactic1 (transformAtTarget ((AtomM.run .reducible ∘ reduceProp disch) ·) "field"
-    (failIfUnchanged := False) · default)
+    (ifUnchanged := .silent) · default)
   let s1 ← saveState
   try
     -- run `ring1`

Mathlib/Tactic/FieldSimp.lean

@@ -711,7 +711,7 @@ elab (name := fieldSimp) "field_simp" d:(discharger)? args:(simpArgs)? loc:(loca
   let m := AtomM.recurse s { contextual := true } (wellBehavedDischarge := false)
     (fun e ↦ reduceProp disch e <|> reduceExpr disch e) cleanup
   let loc := (loc.map expandLocation).getD (.targets #[] true)
-  transformAtLocation (m ·) "field_simp" (failIfUnchanged := true) (mayCloseGoalFromHyp := true) loc
+  transformAtLocation (m ·) "field_simp" (ifUnchanged := .error) (mayCloseGoalFromHyp := true) loc
 
 /--
 `field_simp` normalizes an expression in a (semi-)field by rewriting it to a common denominator,

Mathlib/Tactic/Group.lean

@@ -69,7 +69,7 @@ syntax (name := aux_group₂) "aux_group₂" (location)? : tactic
 
 macro_rules
 | `(tactic| aux_group₂ $[at $location]?) =>
-  `(tactic| ring_nf -failIfUnchanged $[at $location]?)
+  `(tactic| ring_nf (ifUnchanged := .silent) $[at $location]?)
 
 /-- `group` normalizes expressions in multiplicative groups that occur in the goal. `group` does not
 assume commutativity, instead using only the group axioms without any information about which group

Mathlib/Tactic/NormNum/Core.lean

@@ -261,7 +261,7 @@ def elabNormNum (cfg args loc : Syntax) (simpOnly := false) (useSimp := true) :
   let ctx ← getSimpContext cfg args (!useSimp || simpOnly)
   let loc := expandOptLocation loc
   transformAtNondepPropLocation (fun e ctx ↦ deriveSimp ctx useSimp e) "norm_num" loc
-    (failIfUnchanged := false) (mayCloseGoalFromHyp := true) ctx
+    (ifUnchanged := .silent) (mayCloseGoalFromHyp := true) ctx
 
 end Meta.NormNum
 

Mathlib/Tactic/Push.lean

@@ -209,9 +209,9 @@ def elabDischarger (stx : TSyntax ``discharger) : TacticM Simp.Discharge :=
 
 /-- Run the `push` tactic. -/
 def push (cfg : Config) (disch? : Option Simp.Discharge) (head : Head) (loc : Location)
-    (failIfUnchanged : Bool := true) : TacticM Unit := do
+    (ifUnchanged : BehaviorIfUnchanged := .error) : TacticM Unit := do
   let cfg := { distrib := cfg.distrib || (← getBoolOption `push_neg.use_distrib) }
-  transformAtLocation (pushCore head cfg disch? ·) s!"push {head}" loc failIfUnchanged
+  transformAtLocation (pushCore head cfg disch? ·) s!"push {head}" loc ifUnchanged
 
 /--
 `push c` rewrites the goal by pushing the constant `c` deeper into an expression.
@@ -318,7 +318,7 @@ elab (name := pull) "pull" disch?:(discharger)? head:(ppSpace colGt term) loc:(l
   let disch? ← disch?.mapM elabDischarger
   let head ← elabHead head
   let loc := (loc.map expandLocation).getD (.targets #[] true)
-  transformAtLocation (pullCore head · disch?) "pull" loc (failIfUnchanged := true) false
+  transformAtLocation (pullCore head · disch?) "pull" loc (ifUnchanged := .error) false
 
 /-- A simproc variant of `push fun _ ↦ _`, to be used as `simp [↓pushFun]`. -/
 simproc_decl _root_.pushFun (fun _ ↦ ?_) := pushStep .lambda {}

Mathlib/Tactic/ReduceModChar.lean

@@ -296,11 +296,11 @@ elab_rules : tactic
 | `(tactic| reduce_mod_char $[$loc]?) => unsafe do
   let loc := expandOptLocation (Lean.mkOptionalNode loc)
   transformAtNondepPropLocation (derive (expensive := false) ·) "reduce_mod_char" loc
-    (failIfUnchanged := false)
+    (ifUnchanged := .silent)
 | `(tactic| reduce_mod_char! $[$loc]?) => unsafe do
   let loc := expandOptLocation (Lean.mkOptionalNode loc)
   transformAtNondepPropLocation (derive (expensive := true) ·) "reduce_mod_char"
-    loc (failIfUnchanged := false)
+    loc (ifUnchanged := .silent)
 
 end ReduceModChar
 

Mathlib/Tactic/Ring/RingNF.lean

@@ -38,8 +38,8 @@ inductive RingMode where
 
 /-- Configuration for `ring_nf`. -/
 structure Config extends AtomM.Recurse.Config where
-  /-- if true, then fail if no progress is made -/
-  failIfUnchanged := true
+  /-- how to behave if no progress is made: warn, error or keep silent -/
+  ifUnchanged := BehaviorIfUnchanged.error
   /-- The normalization style. -/
   mode := RingMode.SOP
   deriving Inhabited, BEq, Repr
@@ -138,7 +138,7 @@ elab (name := ringNF) "ring_nf" tk:"!"? cfg:optConfig loc:(location)? : tactic =
   let loc := (loc.map expandLocation).getD (.targets #[] true)
   let s ← IO.mkRef {}
   let m := AtomM.recurse s cfg.toConfig (wellBehavedDischarge := true) evalExpr (cleanup cfg)
-  transformAtLocation (m ·) "ring_nf" loc cfg.failIfUnchanged false
+  transformAtLocation (m ·) "ring_nf" loc cfg.ifUnchanged false
 
 @[tactic_alt ringNF] macro "ring_nf!" cfg:optConfig loc:(location)? : tactic =>
   `(tactic| ring_nf ! $cfg:optConfig $(loc)?)

Mathlib/Tactic/WLOG.lean

@@ -133,7 +133,7 @@ def wlogCore (h : TSyntax ``binderIdent) (P : Term) (xs : Option (TSyntaxArray `
     reductionGoal.withContext do
       let negHygName := mkIdent <| ← reductionFVarIds.2.getUserName
       Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[(negHygName)] false)
-          (failIfUnchanged := false)
+        (ifUnchanged := .error)
 
 /-- `wlog h : P` adds an assumption `h : P` to the main goal, and adds a side goal that
 requires showing that the case `h : ¬ P` can be reduced to the case where `P` holds

Mathlib/Util/AtLocation.lean

@@ -47,18 +47,35 @@ def Lean.Elab.Tactic.withNondepPropLocation (loc : Location) (atLocal : FVarId 
 namespace Mathlib.Tactic
 open Lean Meta Elab.Tactic
 
+
+/-- Different settings of communicating about a tactic which made no progress:
+do nothing (keep silent), print a warning or throw an error. -/
+inductive BehaviorIfUnchanged where
+  /-- Don't log anything -/
+  | silent
+  /-- Log a warning -/
+  | warning
+  /-- Throw an error -/
+  | error
+deriving BEq, Inhabited, Repr
+
+
 /-- Use the procedure `m` to rewrite the provided goal.
 
 Assumes `proc` is not surrounded by backticks. -/
 def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
-    (failIfUnchanged : Bool) (goal : MVarId) :
+    (ifUnchanged : BehaviorIfUnchanged) (goal : MVarId) :
     ReaderT Simp.Context MetaM (Option MVarId) := do
   let tgt ← instantiateMVars (← goal.getType)
   let r ← m tgt
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToTarget`
   let unchanged := tgt.cleanupAnnotations == r.expr.cleanupAnnotations
-  if failIfUnchanged && unchanged then throwError "`{proc}` made no progress on the goal"
+  if unchanged then
+    match ifUnchanged with
+    | .warning => logWarning m!"`{proc}` made no progress on the goal"
+    | .error => throwError "`{proc}` made no progress on the goal"
+    | .silent => pure ()
   if r.expr.isTrue then
     goal.assign (← mkOfEqTrue (← r.getProof))
     pure none
@@ -76,7 +93,7 @@ this ensures that if the procedure `m` involves rewriting by this `SimpTheoremsA
 
 Assumes `proc` is not surrounded by backticks. -/
 def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
-    (failIfUnchanged : Bool) (mayCloseGoal : Bool) (fvarId : FVarId) (goal : MVarId) :
+    (ifUnchanged : BehaviorIfUnchanged) (mayCloseGoal : Bool) (fvarId : FVarId) (goal : MVarId) :
     ReaderT Simp.Context MetaM (Option MVarId) := do
   let ldecl ← fvarId.getDecl
   if ldecl.isImplementationDetail then
@@ -87,22 +104,26 @@ def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (
   let r ← withReader eraseFVarId <| m tgt
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToLocalDeclCore`
-  if failIfUnchanged && tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
-    throwError "`{proc}` made no progress at `{Expr.fvar fvarId}`"
+  if tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
+    match ifUnchanged with
+    | .warning => logWarning m!"`{proc}` made no progress at {Expr.fvar fvarId}"
+    | .error => throwError "`{proc}` made no progress at `{Expr.fvar fvarId}`"
+    | .silent => pure ()
   return (← applySimpResultToLocalDecl goal fvarId r mayCloseGoal).map Prod.snd
 
 /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).
 
 Assumes `proc` is not surrounded by backticks. -/
 def transformAtLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
-    (loc : Location) (failIfUnchanged : Bool := true) (mayCloseGoalFromHyp : Bool := false)
+    (loc : Location) (ifUnchanged : BehaviorIfUnchanged := .error)
+    (mayCloseGoalFromHyp : Bool := false)
     -- streamline the most common use case, in which the procedure `m`'s implementation is not
     -- simp-based and its `Simp.Context` is ignored
     (ctx : Simp.Context := default) :
     TacticM Unit :=
   withLocation loc
-    (liftMetaTactic1 ∘ (transformAtLocalDecl m proc failIfUnchanged mayCloseGoalFromHyp · · ctx))
-    (liftMetaTactic1 (transformAtTarget m proc failIfUnchanged · ctx))
+    (liftMetaTactic1 ∘ (transformAtLocalDecl m proc ifUnchanged mayCloseGoalFromHyp · · ctx))
+    (liftMetaTactic1 (transformAtTarget m proc ifUnchanged · ctx))
     fun _ ↦ throwError "`{proc}` made no progress anywhere"
 
 /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).
@@ -111,15 +132,15 @@ In the wildcard case (`*`), filter out all dependent and/or non-`Prop` hypothese
 
 Assumes `proc` is not surrounded by backticks. -/
 def transformAtNondepPropLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result)
-    (proc : String) (loc : Location) (failIfUnchanged : Bool := true)
+    (proc : String) (loc : Location) (ifUnchanged : BehaviorIfUnchanged := .error)
     (mayCloseGoalFromHyp : Bool := false)
     -- streamline the most common use case, in which the procedure `m`'s implementation is not
     -- simp-based and its `Simp.Context` is ignored
     (ctx : Simp.Context := default) :
     TacticM Unit :=
   withNondepPropLocation loc
-    (liftMetaTactic1 ∘ (transformAtLocalDecl m proc failIfUnchanged mayCloseGoalFromHyp · · ctx))
-    (liftMetaTactic1 (transformAtTarget m proc failIfUnchanged · ctx))
+    (liftMetaTactic1 ∘ (transformAtLocalDecl m proc ifUnchanged mayCloseGoalFromHyp · · ctx))
+    (liftMetaTactic1 (transformAtTarget m proc ifUnchanged · ctx))
     fun _ ↦ throwError "`{proc}` made no progress anywhere"
 
 end Mathlib.Tactic

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

MathlibTest/ring.lean

@@ -258,16 +258,16 @@ example (x : ℝ) (f : ℝ → ℝ) : True := by
   to use `fail_if_success` since the instances could change without warning.
   -/
   have : x = y := by
-    ring_nf -failIfUnchanged
+    ring_nf (ifUnchanged := .silent)
     ring_nf!
   have : x - y = 0 := by
-    ring_nf -failIfUnchanged
+    ring_nf (ifUnchanged := .silent)
     ring_nf!
   have : f x = f y := by
-    ring_nf -failIfUnchanged
+    ring_nf (ifUnchanged := .silent)
     ring_nf!
   have : f x - f y = 0 := by
-    ring_nf -failIfUnchanged
+    ring_nf (ifUnchanged := .silent)
     ring_nf!
   trivial