feat(Convert): less aggressive congruence (#38071)

This PR tries to make `convert` behave more predictably, disabling some of the aggressive congruence steps that `congr!` does. In particular, when the two sides have a different head constants, then we should not use congruence on these applications.

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Author: JovanGerb

Mathlib/Analysis/Complex/Exponential.lean

@@ -95,7 +95,7 @@ variable (x y : ℂ)
 theorem exp_zero : exp 0 = 1 := by
   rw [exp]
   refine lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => ?_⟩
-  convert! (config := .unfoldSameFun) ε0 -- ε0 : ε > 0 but goal is _ < ε
+  convert ε0.lt
   rcases j with - | j
   · exact absurd hj (not_le_of_gt zero_lt_one)
   · dsimp [exp']

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -400,9 +400,8 @@ theorem append_castAdd_natAdd {f : Fin (m + n) → α} :
 
 /-- Splitting a dependent finite sequence v into an initial part and a final part,
 and then concatenating these components, produces an identical sequence. -/
-theorem addCases_castAdd_natAdd {γ : Fin (m + n) → Sort*} (v : ∀ i, γ i) :
-    addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) = v := by
-  ext i
+theorem addCases_castAdd_natAdd {γ : Fin (m + n) → Sort*} (v : ∀ i, γ i) (i : Fin (m + n)) :
+    addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) i = v i := by
   cases i using addCases <;> simp
 
 theorem append_comp_sumElim {xs : Fin m → α} {ys : Fin n → α} :
@@ -802,8 +801,8 @@ theorem forall_fin_add_pi {γ : Fin (m + n) → Sort*} {P : (∀ i, γ i) → Pr
       (∀ (vₘ : ∀ i, γ (castAdd n i)) (vₙ : ∀ j, γ (natAdd m j)), P (addCases vₘ vₙ)) where
   mp hv vm vn := hv (addCases vm vn)
   mpr h v := by
-    convert! h (fun i => v (castAdd n i)) (fun j => v (natAdd m j))
-    exact (addCases_castAdd_natAdd v).symm
+    convert h (fun i => v (castAdd n i)) (fun j => v (natAdd m j))
+    exact (addCases_castAdd_natAdd v _).symm
 
 lemma exists_iff_castSucc {P : Fin (n + 1) → Prop} :
     (∃ i, P i) ↔ P (last n) ∨ ∃ i : Fin n, P i.castSucc where

Mathlib/Data/List/Perm/Basic.lean

@@ -164,7 +164,8 @@ end Rel
 lemma count_eq_count_filter_add [DecidableEq α] (P : α → Prop) [DecidablePred P]
     (l : List α) (a : α) :
     count a l = count a (l.filter P) + count a (l.filter (¬ P ·)) := by
-  convert! countP_eq_countP_filter_add l _ P
+  unfold count
+  convert countP_eq_countP_filter_add l _ P
   simp only [decide_not]
 
 theorem Perm.foldl_eq {f : β → α → β} {l₁ l₂ : List α} [rcomm : RightCommutative f] (p : l₁ ~ l₂) :

Mathlib/Tactic/Convert.lean

@@ -24,30 +24,22 @@ e : Prime (2 * n + 1)
 ⊢ Prime (n + n + 1)
 ```
 
-the tactic `convert e using 2` will change the goal to
+the tactic `convert e` will change the goal to
 
 ```lean
 ⊢ n + n = 2 * n
 ```
 
 In this example, the new goal can be solved using `ring`.
 
-The `using 2` indicates it should iterate the congruence algorithm up to two times,
-where `convert e` would use an unrestricted number of iterations and lead to two
-impossible goals: `⊢ HAdd.hAdd = HMul.hMul` and `⊢ n = 2`.
-
-A variant configuration is `convert (config := .unfoldSameFun) e`, which only equates function
-applications for the same function (while doing so at the higher `default` transparency).
-This gives the same goal of `⊢ n + n = 2 * n` without needing `using 2`.
-
 The `convert` tactic applies congruence lemmas eagerly before reducing,
 therefore it can fail in cases where `exact` succeeds:
 ```lean
 def p (n : ℕ) := True
 example (h : p 0) : p 1 := by exact h -- succeeds
 example (h : p 0) : p 1 := by convert h -- fails, with leftover goal `1 = 0`
 ```
-Limiting the depth of recursion can help with this. For example, `convert h using 1` will work
+Limiting the depth of recursion can help with this. For example, `convert h using 0` will work
 in this case.
 
 The syntax `convert ← e` will reverse the direction of the new goals
@@ -85,21 +77,12 @@ between `Convert.CheapConfig` and `Convert.ExpensiveConfig` based on other flags
 -/
 structure Convert.CheapConfig extends Congr!.Config where
   postTransparency := .reducible
+  partialApp := false
+  sameFun := true
 
 /-- Internal elaborator for `Convert.CheapConfig`: use `Convert.elabConfig` instead. -/
 declare_config_elab Convert.elabCheapConfig Convert.CheapConfig
 
-/-- A configuration option that makes `convert` do the sorts of aggressive unfoldings that `congr`
-does while also similarly preventing `convert` from considering partial applications or congruences
-between different functions being applied.
-
-Note that `convert (config := .unfoldSameFun)` and `convert! (config := .unfoldSameFun)`
-currently do the same thing since `.unfoldSameFun` runs at default transparency always.
-This may change in the future, if `convert!` affects other options too.
--/
-abbrev Convert.CheapConfig.unfoldSameFun : Convert.CheapConfig :=
-  { Congr!.Config.unfoldSameFun with }
-
 /-- Configuration for the `convert!` family of tactics.
 This is `Convert.CheapConfig` (used by `convert` without exclamation mark) with different,
 more aggressive, defaults.
@@ -113,26 +96,14 @@ example the following call runs at `.instances` transparency.
 convert! (postTransparency := .instances)
 ```
 -/
-structure Convert.ExpensiveConfig extends Convert.CheapConfig where
+structure Convert.ExpensiveConfig extends Congr!.Config where
   -- TODO: also enable this in the future?
   -- preTransparency := .default
   -- transparency := .default
-  postTransparency := .default
 
 /-- Internal elaborator for `Convert.ExpensiveConfig`: use `Convert.elabConfig` instead. -/
 declare_config_elab Convert.elabExpensiveConfig Convert.ExpensiveConfig
 
-/-- A configuration option that makes `convert!` do the sorts of aggressive unfoldings that `congr`
-does while also similarly preventing `convert!` from considering partial applications or congruences
-between different functions being applied.
-
-Note that `convert (config := .unfoldSameFun)` and `convert! (config := .unfoldSameFun)`
-currently do the same thing since `.unfoldSameFun` runs at default transparency always.
-This may change in the future, if `convert!` affects other options too.
--/
-abbrev Convert.ExpensiveConfig.unfoldSameFun : Convert.ExpensiveConfig :=
-  { Congr!.Config.unfoldSameFun with }
-
 /-- Configuration elaborator for the `convert`/`convert!` family of tactics.
 
 If `expensive` is true, we're elaborating for `convert!`, and will configure to run at default
@@ -201,9 +172,10 @@ pattern-matched, like `rintro` would, using the `with` keyword.
 See also `convert_to t`, where `t` specifies the expected type, instead of a proof term of type `t`.
 In other words, `convert_to t` works like `convert (?_ : t)`. Both tactics use the same options.
 
-* `convert! e` uses default transparency, rather than reducible, when solving side goals.
+* `convert! e` uses default transparency, rather than reducible, when solving side goals, and
+  it tries to apply congruence even if the two expressions do not have the same head constant.
 * `convert ← e` creates equality goals in the opposite direction (with the goal type on the right).
-* `convert e using n`, where `n` is a positive numeral, controls the depth with which congruence is
+* `convert e using n`, where `n` is a numeral, controls the depth with which congruence is
   applied. For example, if the main goal is `⊢ Prime (n + n + 1)` and `e : Prime (2 * n + 1)`, then
   `convert e using 2` results in one goal, `⊢ n + n = 2 * n`, and `convert e using 3` (or more)
   results in two (impossible) goals `⊢ HAdd.hAdd = HMul.hMul` and `⊢ n = 2`.
@@ -216,10 +188,9 @@ In other words, `convert_to t` works like `convert (?_ : t)`. Both tactics use t
 Examples:
 
 ```lean
--- `convert using` controls the depth of congruence.
 example {n : ℕ} (e : Prime (2 * n + 1)) :
     Prime (n + n + 1) := by
-  convert e using 2
+  convert e
   -- One goal: ⊢ n + n = 2 * n
   ring
 
@@ -234,7 +205,7 @@ example (h : p 0) : p 1 := by
 -- `convert with` names introduced variables.
 example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
     ∀ ε > 0, q ε := by
-  convert h using 2 with ε hε
+  convert h with ε hε
   -- Goal now looks like:
   -- hε : ε > 0
   -- ⊢ q ε ↔ p ε

MathlibTest/Tactic/Convert/Basic.lean

@@ -61,23 +61,15 @@ end convert_to
 
 example (prime : Nat → Prop) (n : Nat) (h : prime (2 * n + 1)) :
     prime (n + n + 1) := by
-  convert h
+  convert! h
   · guard_target = (HAdd.hAdd : Nat → Nat → Nat) = HMul.hMul
     exact test_sorry
   · guard_target = n = 2
     exact test_sorry
 
 example (prime : Nat → Prop) (n : Nat) (h : prime (2 * n + 1)) :
     prime (n + n + 1) := by
-  convert (config := .unfoldSameFun) h
-  guard_target = n + n = 2 * n
-  exact test_sorry
-
--- `convert! (config := .unfoldSameFun)` does the same thing as `convert (config := .unfoldSameFun)`
--- (at least for now)
-example (prime : Nat → Prop) (n : Nat) (h : prime (2 * n + 1)) :
-    prime (n + n + 1) := by
-  convert! (config := .unfoldSameFun) h
+  convert h
   guard_target = n + n = 2 * n
   exact test_sorry