feat: in conv tactic, use try with_reducibe rfl (#3763)

The `conv` tactic tries to close “trivial” goals after itself. As of
now, it uses
`try rfl`, which means it can close goals that are only trivial after
reducing with
default transparency. This is suboptimal

* this can require a fair amount of unfolding, and possibly slow down
the proof
   a lot. And the user cannot even prevent it.
* it does not match what `rw` does, and a user might expect the two to
behave the
   same.

So this PR changes it to `with_reducible rfl`, matching `rw`’s behavior.

I considered `with_reducible eq_refl` to only solve trivial goals that
involve equality,
but not other relations (e.g. `Perm xs xs`), but a discussion on mathlib
pointed out
that it’s expected and desirable to solve more general reflexive goals:


https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Closing.20after.20.60rw.60.2C.20.60conv.60.3A.20.60eq_refl.60.20instead.20of.20.60rfl.60/near/429851605

src/Init/Omega/Int.lean

@@ -137,11 +137,13 @@ theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by
     lhs
     rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
       Int.add_le_add_iff_right]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem le_add_iff_sub_le (a b c : Int) : a ≤ b + c ↔ a - c ≤ b := by
   conv =>
     lhs
     rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem add_le_zero_iff_le_neg (a b : Int) : a + b ≤ 0 ↔ a ≤ - b := by
   rw [add_le_iff_le_sub, Int.zero_sub]

src/Lean/Elab/Tactic/Conv/Basic.lean

@@ -115,7 +115,7 @@ def evalSepByIndentConv (stx : Syntax) : TacticM Unit := do
     -- save state before/after entering focus on `{`
     withInfoContext (pure ()) initInfo
     evalSepByIndentConv stx[1]
-    evalTactic (← `(tactic| all_goals (try rfl)))
+    evalTactic (← `(tactic| all_goals (try with_reducible rfl)))
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.nestedConv] def evalNestedConv : Tactic := fun stx => do
   evalConvSeqBracketed stx[0]
@@ -163,7 +163,7 @@ private def convTarget (conv : Syntax) : TacticM Unit := withMainContext do
    let target ← getMainTarget
    let (targetNew, proof) ← convert target (withTacticInfoContext (← getRef) (evalTactic conv))
    liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
-   evalTactic (← `(tactic| try rfl))
+   evalTactic (← `(tactic| try with_reducible rfl))
 
 private def convLocalDecl (conv : Syntax) (hUserName : Name) : TacticM Unit := withMainContext do
    let localDecl ← getLocalDeclFromUserName hUserName

tests/lean/948.lean

@@ -17,3 +17,4 @@ def add_one_to_one (x : Int) (h : x = 1) : add_one (x : Int) = (2 : Int) := by
     pattern add_one _
     trace_state
     rw [h]
+  rfl

tests/lean/conv1.lean

@@ -37,6 +37,7 @@ example : foo (0 + a) (b + 0) = a + b := by
     case' y => skip
     case y => skip
     done
+  rfl
 
 example : foo (0 + a) (b + 0) = a + b := by
   conv =>
@@ -59,6 +60,7 @@ example : foo (0 + a) (b + 0) = a + b := by
     fail_if_success lhs
     try lhs
     trace_state
+  rfl
 
 example (x y : Nat) : p (x + y) (y + x + 0) := by
   conv =>
@@ -99,6 +101,7 @@ example (x y : Nat) : f x (x + y + 0) y = y + x := by
     change x + y
     trace_state
     rw [Nat.add_comm]
+  rfl
 
 example : id (fun x y => 0 + x + y) = Nat.add := by
   conv =>
@@ -108,6 +111,7 @@ example : id (fun x y => 0 + x + y) = Nat.add := by
     trace_state
     rw [Nat.zero_add]
     trace_state
+  rfl
 
 example : id (fun x y => 0 + x + y) = Nat.add := by
   conv =>
@@ -115,12 +119,14 @@ example : id (fun x y => 0 + x + y) = Nat.add := by
     arg 1
     intro a b
     rw [Nat.zero_add]
+  rfl
 
 example : id (fun x y => 0 + x + y) = Nat.add := by
   conv =>
     enter [1, 1, a, b]
     trace_state
     rw [Nat.zero_add]
+  rfl
 
 example (p : Nat → Prop) (h : ∀ a, p a) : ∀ a, p (id (0 + a)) := by
   conv =>
@@ -152,6 +158,7 @@ example : (fun x => 0 + x) = id := by
     tactic => funext x
     trace_state
     rw [Nat.zero_add]
+  rfl
 
 example (p : Prop) (x : Nat) : (x = x → p) → p := by
   conv =>

tests/lean/conv1.lean.expected.out

@@ -125,11 +125,11 @@ x y : Nat
 h1 : y = 0
 h2 : p x
 | y
-conv1.lean:214:10-214:13: error: invalid 'lhs' conv tactic, application has only 1 (nondependent) argument(s)
-conv1.lean:217:10-217:15: error: invalid 'arg' conv tactic, application has only 1 (nondependent) argument(s)
-conv1.lean:220:10-220:13: error: invalid 'congr' conv tactic, application or implication expected
+conv1.lean:221:10-221:13: error: invalid 'lhs' conv tactic, application has only 1 (nondependent) argument(s)
+conv1.lean:224:10-224:15: error: invalid 'arg' conv tactic, application has only 1 (nondependent) argument(s)
+conv1.lean:227:10-227:13: error: invalid 'congr' conv tactic, application or implication expected
   p
-conv1.lean:223:10-223:15: error: cannot select argument
+conv1.lean:230:10-230:15: error: cannot select argument
 a✝ : Nat := 0
 b✝ : Nat := a✝
 | 0 = 0
@@ -160,10 +160,10 @@ x y z : Nat
 
 x y z : Nat
 | y + z
-conv1.lean:241:58-241:83: error: 'pattern' conv tactic failed, pattern was found only 4 times but 5 expected
-conv1.lean:242:58-242:85: error: 'pattern' conv tactic failed, pattern was found only 4 times but 5 expected
-conv1.lean:243:58-243:85: error: 'pattern' conv tactic failed, pattern was found only 3 times but 5 expected
-conv1.lean:244:58-244:87: error: 'pattern' conv tactic failed, pattern was found only 2 times but 5 expected
+conv1.lean:248:58-248:83: error: 'pattern' conv tactic failed, pattern was found only 4 times but 5 expected
+conv1.lean:249:58-249:85: error: 'pattern' conv tactic failed, pattern was found only 4 times but 5 expected
+conv1.lean:250:58-250:85: error: 'pattern' conv tactic failed, pattern was found only 3 times but 5 expected
+conv1.lean:251:58-251:87: error: 'pattern' conv tactic failed, pattern was found only 2 times but 5 expected
 P Q : Nat → Nat → Nat → Prop
 h : P = Q
 h2 : Q 1 2 3
@@ -180,7 +180,7 @@ P Q : Nat → Nat → Nat → Prop
 h : P = Q
 h2 : Q 1 2 3
 | P
-conv1.lean:268:10-268:13: error: invalid 'fun' conv tactic, application expected
+conv1.lean:275:10-275:13: error: invalid 'fun' conv tactic, application expected
   p
 P Q : Nat → Nat → Nat → Prop
 h : P = Q
@@ -190,5 +190,5 @@ P Q : Nat → Nat → Nat → Prop
 h : P = Q
 h2 : Q 1 2 3
 | P
-conv1.lean:280:10-280:15: error: invalid 'arg 0' conv tactic, application expected
+conv1.lean:287:10-287:15: error: invalid 'arg 0' conv tactic, application expected
   p

tests/lean/convInConv.lean

@@ -9,6 +9,7 @@ def foo1 : (λ x : Nat => id (twice (id x))) = twice := by
       simp
       trace_state
     trace_state  -- `id (twice x)`
+  rfl
 
 
 theorem foo2 (y : Nat) : (fun x => x + y = 0) = (fun x => False) := by

tests/lean/convInConv.lean.expected.out

@@ -6,7 +6,7 @@ x : Nat
 | x
 x : Nat
 | id (twice x)
-convInConv.lean:14:8-14:12: warning: declaration uses 'sorry'
+convInConv.lean:15:8-15:12: warning: declaration uses 'sorry'
 y : Nat
 | (fun x => x + y = 0) = fun x => False
 y : Nat

tests/lean/convPatternAtLetIssue.lean

@@ -10,3 +10,4 @@ def test : (λ x => f x)
     trace_state
     simp
     trace_state
+  rfl

tests/lean/convPatternMatchIssue.lean

@@ -7,3 +7,4 @@ def test : (λ x => x)
     pattern (id _)
     trace_state
     skip
+  rfl

tests/lean/matchPatternPartialApp.lean

@@ -3,3 +3,4 @@ def test2 : (Function.comp id id) = λ x : Nat => x := by
     trace_state
     simp (config := { unfoldPartialApp := true }) [Function.comp, id]
     trace_state
+  rfl

tests/lean/run/1558.lean

@@ -3,3 +3,4 @@ example : (λ (u : Nat) => u + 0) = id :=by
     lhs
     intro u
     change u
+  rfl

tests/lean/run/conv1.lean

@@ -68,6 +68,7 @@ example : id (fun x => 0 + x) = id := by
     arg 1
     ext y
     rw [Nat.zero_add]
+  rfl
 
 def f (x : Nat) :=
   if x > 0 then

tests/lean/run/repeatConv.lean

@@ -3,3 +3,4 @@ example : (fun x y => (0 + x) + (0 + y)) = Nat.add := by
     lhs
     intro x y
     repeat rw [Nat.zero_add]
+  rfl

tests/lean/run/splitIssue.lean

@@ -28,6 +28,7 @@ theorem len_1 (a : α) : len [a] = 1 := by
 
 theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
+  rfl
 
 -- The `unfold` tactic above generated the following theorem
 #check @len.eq_def

tests/lean/run/splitList.lean

@@ -47,6 +47,7 @@ theorem len_1 (a : α) : len [a] = 1 := by
 
 theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
+  rfl
 
 -- The `unfold` tactic above generated the following theorem
 #check @len.eq_def
@@ -97,6 +98,7 @@ theorem len_1 (a : α) : len [a] = 1 := by
 
 theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
+  rfl
 
 -- The `unfold` tactic above generated the following theorem
 #check @len.eq_def