feat(Tactic): convert discharges side goals reducibly

This PR implements the main behaviour change from #39039: `convert` now discharges side goals at reducible transparency. `convert!`, which we previously switched all calls inside Mathlib to, keeps the old behaviour of working at default transparency. (Everything discussed in this PR holds analogously for the other tactics in the family: `convert_to` and `ac_change`).

The main trick in this PR is in allowing `convert!` to have different configuration options than `convert`, but still allow the user to override those options too. So `convert! (postTransparency := .instances)` will have transparency set to `.instances`, not `.default`. We achieve this by having two new structures that copy `Congr!.Config` but set different default values, and choosing between the corresponding elaborators for those configs based on the presence of an `!`. I got this trick from Jovan's #38071 which also changes settings in `Convert.Config`.

This PR should be mostly compatible with #38071 and I'd like to get both this one and #38071 in before wrapping up #39039 by replacing unnecessary calls to `convert!` with `convert`.

Author: Vierkantor

Mathlib/Tactic/CongrExclamation.lean

@@ -63,7 +63,8 @@ to right-hand sides of goals. Here is an exhaustive list of things it can try:
 
 - It can try to close goals using a few strategies, including checking
   definitional equality, trying to apply `Subsingleton.elim` or `proof_irrel_heq`, and using the
-  `assumption` tactic.
+  `assumption` tactic. Discharging is done at default transparency (unless specified otherwise),
+  but this will become reducible transparency in the future.
 
 The optional parameter is the depth of the recursive applications.
 This is useful when `congr!` is too aggressive in breaking down the goal.
@@ -106,7 +107,8 @@ structure Congr!.Config where
   closePre : Bool := true
   /-- If `closePost := true`, then try to close goals that remain after no more congruence
   lemmas can be applied, using the same tactics as `closePre`. These tactics are applied
-  with current tactic transparency level. -/
+  with the transparency level specified by `postTransparency`, which is currently default
+  transparency but in the future will become `.reducible` by default. -/
   closePost : Bool := true
   /-- The transparency level to use when applying a congruence theorem.
   By default this is `.reducible`, which prevents unfolding of most definitions. -/
@@ -115,6 +117,12 @@ structure Congr!.Config where
   This includes trying to prove the goal by `rfl` and using the `assumption` tactic.
   By default this is `.reducible`, which prevents unfolding of most definitions. -/
   preTransparency : TransparencyMode := TransparencyMode.reducible
+  /-- The transparency level to use when trying to close goals after no more congruence lemmas can
+  be applied. This includes trying to prove the goal by `rfl` and using the `assumption` tactic.
+  For backwards compatibility this is set to `.default`, which will be changed in the future to
+  `.reducible`.
+  -/
+  postTransparency : TransparencyMode := TransparencyMode.default
   /-- For passes that synthesize a congruence lemma using one side of the equality,
   we run the pass both for the left-hand side and the right-hand side. If `preferLHS` is `true`
   then we start with the left-hand side.
@@ -190,6 +198,7 @@ def Congr!.Config.unfoldSameFun : Congr!.Config where
   sameFun := true
   transparency := .default
   preTransparency := .default
+  postTransparency := .default
 
 /-- Whether the given number of arguments is allowed to be considered. -/
 def Congr!.Config.numArgsOk (config : Config) (numArgs : Nat) : Bool :=
@@ -676,7 +685,8 @@ def Lean.MVarId.congrCore! (config : Congr!.Config) (mvarId : MVarId) :
   return none
 
 /-- A pass to clean up after `Lean.MVarId.preCongr!` and `Lean.MVarId.congrCore!`. -/
-def Lean.MVarId.postCongr! (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option MVarId) := do
+def Lean.MVarId.postCongr! (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option MVarId) :=
+  withTransparency config.postTransparency do
   let some mvarId ← mvarId.preCongr! config.closePost | return none
   -- Convert `p = q` to `p ↔ q`, which is likely the more useful form:
   let mvarId ← mvarId.propext

Mathlib/Tactic/Convert.lean

@@ -77,6 +77,75 @@ public meta section
 
 open Lean Meta Elab Tactic
 
+/-- Configuration for the `convert` family of tactics.
+This is `Congr!.Config` with different, less aggressive, defaults.
+
+To elaborate config options for `convert`, use `Convert.elabConfig` which chooses
+between `Convert.CheapConfig` and `Convert.ExpensiveConfig` based on other flags.
+-/
+structure Convert.CheapConfig extends Congr!.Config where
+  postTransparency := .reducible
+
+/-- 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.
+
+To elaborate config options for `convert`, use `Convert.elabConfig` which chooses
+between `Convert.CheapConfig` and `Convert.ExpensiveConfig` based on other flags.
+
+We separate out the two structures to allow the user to explicitly set options in the call, so for
+example the following call runs at `.instances` transparency.
+```
+convert! (postTransparency := .instances)
+```
+-/
+structure Convert.ExpensiveConfig extends Convert.CheapConfig where
+  -- TODO: also enable this in the future? (For backwards compatibility we won't do so right now.)
+  -- 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
+transparency (unless explicitly overridden by the user saying e.g. `(transparency := .instances)`.)
+-/
+def Convert.elabConfig (expensive : Bool) (stx : Syntax) : TacticM Congr!.Config := do
+  -- Implement overridable fields by choosing to elaborate one of two structures,
+  -- which have different defaults (that can later be overridden by the user).
+  if expensive then
+    pure { ← Convert.elabExpensiveConfig stx with }
+  else
+    pure { ← Convert.elabCheapConfig stx with }
+
 /--
 Close the goal `g` using `Eq.mp v e`,
 where `v` is a metavariable asserting that the type of `g` and `e` are equal.
@@ -132,8 +201,7 @@ 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 when solving side goals. This is currently the same
-  behaviour as `convert`, but `convert` will use reducible transparency in the future.
+* `convert! e` uses default transparency, rather than reducible, when solving side goals.
 * `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
   applied. For example, if the main goal is `⊢ Prime (n + n + 1)` and `e : Prime (2 * n + 1)`, then
@@ -156,6 +224,7 @@ example {n : ℕ} (e : Prime (2 * n + 1)) :
   ring
 
 -- `convert` can fail where `exact` succeeds.
+def p (n : ℕ) := True
 example (h : p 0) : p 1 := by
   fail_if_success
     convert h -- fails, left-over goal 1 = 0
@@ -200,9 +269,9 @@ def elabTermForConvert (term : Syntax) (expectedType? : Option Expr) :
       return t
 
 elab_rules : tactic
-| `(tactic| convert $[!]? $cfg $[←%$sym]? $term $[using $n]? $[with $ps?*]?) =>
+| `(tactic| convert $[!%$expensive]? $cfg $[←%$sym]? $term $[using $n]? $[with $ps?*]?) =>
   withMainContext do
-    let config ← Congr!.elabConfig (mkOptionalNode cfg)
+    let config ← Convert.elabConfig expensive.isSome cfg
     let patterns := (ps?.getD #[]).toList
     let expectedType ← mkFreshExprMVar (mkSort (← getLevel (← getMainTarget)))
     let (e, gs) ← elabTermForConvert term expectedType
@@ -221,8 +290,7 @@ pattern-matched, like `rintro` would, using the `with` keyword.
 `convert e`, where `e` is a term of type `t`, uses `e` to close the new main goal. In other words,
 `convert e` works like `convert_to t; refine e`. Both tactics use the same options.
 
-* `convert_to! t` uses default transparency when solving side goals. This is currently the same
-  behaviour as `convert_to`, but `convert_to` will use reducible transparency in the future.
+* `convert_to! t` uses default transparency, rather than reducible, when solving side goals.
 * `convert_to ty at h` changes the type of the local hypothesis `h` to `ty`. If later local
   hypotheses or the goal depend on `h`, then `convert_to t at h` may leave a copy of `h`.
 * `convert_to ← t` creates equality goals in the opposite direction (with the original goal type on
@@ -238,7 +306,7 @@ pattern-matched, like `rintro` would, using the `with` keyword.
 * `convert_to (config := cfg) t` uses the configuration options in `cfg` to control the congruence
   rules (see `Congr!.Config`).
 -/
-syntax (name := convertTo) "convert_to" Lean.Parser.Tactic.optConfig " ←"? ppSpace term
+syntax (name := convertTo) "convert_to" ("!")? Lean.Parser.Tactic.optConfig " ←"? ppSpace term
   (" using " num)? (" with" (ppSpace colGt rintroPat)*)? (Parser.Tactic.location)? : tactic
 
 @[tactic_alt convertTo]
@@ -247,13 +315,13 @@ syntax (name := convert_to!) "convert_to!" Lean.Parser.Tactic.optConfig " ←"?
 
 macro_rules
 | `(tactic| convert_to! $cfg $[←%$l]? $t $[using $n]? $[with $w]? $[$loc]?) =>
-    `(tactic| convert_to $cfg $[←%$l]? $t:term $[using $n]? $[with $w]? $[$loc]?)
+    `(tactic| convert_to ! $cfg $[←%$l]? $t:term $[using $n]? $[with $w]? $[$loc]?)
 
 elab_rules : tactic
-| `(tactic| convert_to $cfg $[←%$sym]? $newType $[using $n]?
+| `(tactic| convert_to $[!%$expensive]? $cfg $[←%$sym]? $newType $[using $n]?
     $[with $ps?*]? $[$loc?:location]?) => do
   let n : ℕ := n |>.map (·.getNat) |>.getD 1
-  let config ← Congr!.elabConfig cfg
+  let config ← Convert.elabConfig expensive.isSome cfg
   let patterns := (ps?.getD #[]).toList
   withLocation (expandOptLocation (mkOptionalNode loc?))
     (atLocal := fun fvarId ↦ do
@@ -279,8 +347,7 @@ into new goals, using the hole's name, if any, as the goal case name.
 Like `congr!`, `convert_to` introduces variables while applying congruence rules. These can be
 pattern-matched, like `rintro` would, using the `with` keyword.
 
-* `ac_change! t` uses default transparency when solving side goals. This is currently the same
-  behaviour as `ac_change`, but `ac_change` will use reducible transparency in the future.
+* `ac_change! t` uses default transparency, rather than reducible, when solving side goals.
 * `ac_change t using n`, where `n` is a positive numeral, controls the depth with which congruence
   is applied. For example, if the main goal is `⊢ Prime ((a * b + 1) + c)`,
   then `ac_change Prime ((1 + a * b) + c) using 2` solves the side goals, and
@@ -305,5 +372,4 @@ macro_rules
 | `(tactic| ac_change! $t $[using $n]?) =>
     `(tactic| convert_to! $t:term $[using $n]? <;> try ac_rfl)
 
-
 end Mathlib.Tactic

MathlibTest/Tactic/Convert/Basic.lean

@@ -73,6 +73,14 @@ example (prime : Nat → Prop) (n : Nat) (h : prime (2 * n + 1)) :
   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
+  guard_target = n + n = 2 * n
+  exact test_sorry
+
 example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
     ∀ ε > 0, q ε := by
   convert h using 2 with ε hε
@@ -128,4 +136,37 @@ example (x y z : Nat) (h : x + y = z) : y + x = z := by
   · rw [Nat.add_comm]
   exact h
 
+/-! Check that we don't unfold at semireducible transparency: although `congr!` (which
+`convert` relies on) applies lemmas at reducible transparency, it used to call
+`assumption`/`rfl` at default transparency and solve too much.
+`convert!` uses default transparency throughout, and solves the goals all at once.
+-/
+
+/-- An identity function at default transparency, to test that we don't unfold too much. -/
+def semireducibleId {α : Type*} (a : α) := a
+
+example (P : ℕ → Prop) {a b : ℕ} (h : P a) : P (semireducibleId a) := by
+  convert h
+  guard_target =ₛ semireducibleId a = a
+  rfl
+
+example (P : ℕ → Prop) {a b : ℕ} (h : P a) : P (semireducibleId a) := by
+  convert! h
+
+example (P : ℕ → Prop) {a b : ℕ} (hab : b = a) (h : P a) : P (semireducibleId b) := by
+  convert h
+  guard_target =ₛ semireducibleId b = a
+  exact hab
+
+example (P : ℕ → Prop) {a b : ℕ} (hab : b = a) (h : P (semireducibleId a)) : P b := by
+  convert! h
+
+example (P : ℕ → Prop) {a b : ℕ} (hab : b = a) (h : P a) : P (semireducibleId b) := by
+  convert h
+  guard_target =ₛ semireducibleId b = a
+  exact hab
+
+example (P : ℕ → Prop) {a b : ℕ} (hab : b = a) (h : P (semireducibleId a)) : P b := by
+  convert! h
+
 end Tests