From b181fd83efafcab4a64412ea8c797a0e8d6e235d Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 29 Mar 2024 12:59:45 +0100
Subject: [PATCH] feat: in conv tactic, use `try with_reducibe rfl` (#3763)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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                 |  2 ++
 src/Lean/Elab/Tactic/Conv/Basic.lean    |  4 ++--
 tests/lean/948.lean                     |  1 +
 tests/lean/conv1.lean                   |  7 +++++++
 tests/lean/conv1.lean.expected.out      | 20 ++++++++++----------
 tests/lean/convInConv.lean              |  1 +
 tests/lean/convInConv.lean.expected.out |  2 +-
 tests/lean/convPatternAtLetIssue.lean   |  1 +
 tests/lean/convPatternMatchIssue.lean   |  1 +
 tests/lean/matchPatternPartialApp.lean  |  1 +
 tests/lean/run/1558.lean                |  1 +
 tests/lean/run/conv1.lean               |  1 +
 tests/lean/run/repeatConv.lean          |  1 +
 tests/lean/run/splitIssue.lean          |  1 +
 tests/lean/run/splitList.lean           |  2 ++
 15 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean
index 348579dbee51..9a8e9f54bb6b 100644
--- a/src/Init/Omega/Int.lean
+++ b/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]
diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index abf49010a486..8a5879e002e9 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/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
diff --git a/tests/lean/948.lean b/tests/lean/948.lean
index 8658f3b21d2b..0d60c6f8334c 100644
--- a/tests/lean/948.lean
+++ b/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
diff --git a/tests/lean/conv1.lean b/tests/lean/conv1.lean
index b1e2feae08f9..46ced9a3211d 100644
--- a/tests/lean/conv1.lean
+++ b/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 =>
diff --git a/tests/lean/conv1.lean.expected.out b/tests/lean/conv1.lean.expected.out
index 0044021de23f..21bcb4c82130 100644
--- a/tests/lean/conv1.lean.expected.out
+++ b/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
diff --git a/tests/lean/convInConv.lean b/tests/lean/convInConv.lean
index 8cc859256d1c..f24f2fe20e39 100644
--- a/tests/lean/convInConv.lean
+++ b/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
diff --git a/tests/lean/convInConv.lean.expected.out b/tests/lean/convInConv.lean.expected.out
index 60952ff17724..d27c28c38e4a 100644
--- a/tests/lean/convInConv.lean.expected.out
+++ b/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
diff --git a/tests/lean/convPatternAtLetIssue.lean b/tests/lean/convPatternAtLetIssue.lean
index 2ced3e81eaed..7a1c79cf33a9 100644
--- a/tests/lean/convPatternAtLetIssue.lean
+++ b/tests/lean/convPatternAtLetIssue.lean
@@ -10,3 +10,4 @@ def test : (λ x => f x)
     trace_state
     simp
     trace_state
+  rfl
diff --git a/tests/lean/convPatternMatchIssue.lean b/tests/lean/convPatternMatchIssue.lean
index 8da8c6251a50..7b8d7ccd3ed7 100644
--- a/tests/lean/convPatternMatchIssue.lean
+++ b/tests/lean/convPatternMatchIssue.lean
@@ -7,3 +7,4 @@ def test : (λ x => x)
     pattern (id _)
     trace_state
     skip
+  rfl
diff --git a/tests/lean/matchPatternPartialApp.lean b/tests/lean/matchPatternPartialApp.lean
index a8bcc50b2819..ca4572c86b39 100644
--- a/tests/lean/matchPatternPartialApp.lean
+++ b/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
diff --git a/tests/lean/run/1558.lean b/tests/lean/run/1558.lean
index b2b7f6aa28b7..799fffe4ff1c 100644
--- a/tests/lean/run/1558.lean
+++ b/tests/lean/run/1558.lean
@@ -3,3 +3,4 @@ example : (λ (u : Nat) => u + 0) = id :=by
     lhs
     intro u
     change u
+  rfl
diff --git a/tests/lean/run/conv1.lean b/tests/lean/run/conv1.lean
index ac0919186072..60fe133e3cb4 100644
--- a/tests/lean/run/conv1.lean
+++ b/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
diff --git a/tests/lean/run/repeatConv.lean b/tests/lean/run/repeatConv.lean
index f731817ab2f1..84b29da3fbf2 100644
--- a/tests/lean/run/repeatConv.lean
+++ b/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
diff --git a/tests/lean/run/splitIssue.lean b/tests/lean/run/splitIssue.lean
index 268c6884f4a6..b555f3541607 100644
--- a/tests/lean/run/splitIssue.lean
+++ b/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
diff --git a/tests/lean/run/splitList.lean b/tests/lean/run/splitList.lean
index d16bd8d4e2d8..26f22f3a7562 100644
--- a/tests/lean/run/splitList.lean
+++ b/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