feat(Tactic): automatically replace convert with convert!

This PR sets up an option for `congr!` to close generated goals with configurable transparency, but does not enable this by default. Then it adds a check to `convert` where it will run the `congr!` algorithm at both reducible and default transparency. In the case the default transparency generates different goals, it pops up a "Try this:" suggestion to use `convert!`. Applying all the "Try this:" suggestions to Mathlib means we can then change the semantics of `convert` to close the goals reducibly.

Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards.

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 (but this will be changed
+  to 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 set to
+  `.default` but will soon become `.reducible`. -/
   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,11 @@ 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 soon 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 +197,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 :=
@@ -636,7 +644,8 @@ where
 /-- Convert a goal into an `Eq` goal if possible (since we have a better shot at those).
 Also, if `tryClose := true`, then try to close the goal using an assumption, `Subsingleton.Elim`,
 or definitional equality. -/
-def Lean.MVarId.preCongr! (mvarId : MVarId) (tryClose : Bool) : MetaM (Option MVarId) := do
+def Lean.MVarId.preCongr! (mvarId : MVarId) (tryClose : Bool) :
+    MetaM (Option MVarId) := do
   -- Next, turn `HEq` and `Iff` into `Eq`
   let mvarId ← mvarId.heqOfEq
   if tryClose then
@@ -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,25 @@ public meta section
 
 open Lean Meta Elab Tactic
 
+/-- Configuration for the `convert` family of tactics.
+This is `Congr!.Config` with different, less aggressive, defaults.
+-/
+structure Convert.Config extends Congr!.Config where
+  postTransparency := .default -- Will be set to .reducible in a follow-up PR
+
+/-- Elaborator for `Convert.Config` (which is equivalent to `Congr!.Config`
+but with different, less aggressive, defaults). -/
+declare_config_elab Convert.elabConfig Convert.Config
+
+/--
+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.
+-/
+abbrev Convert.Config.unfoldSameFun : Convert.Config :=
+  { Congr!.Config.unfoldSameFun with
+    postTransparency := .default } -- Will be set to .reducible in a follow-up PR
+
 /--
 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 +151,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 +174,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
@@ -172,16 +191,16 @@ example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
   sorry
 ```
 -/
-syntax (name := convert) "convert" Lean.Parser.Tactic.optConfig " ←"? ppSpace term (" using " num)?
-  (" with" (ppSpace colGt rintroPat)*)? : tactic
+syntax (name := convert) "convert" "!"? Lean.Parser.Tactic.optConfig " ←"? ppSpace term
+  (" using " num)? (" with" (ppSpace colGt rintroPat)*)? : tactic
 
 @[tactic_alt convert]
 syntax (name := convert!) "convert!" Lean.Parser.Tactic.optConfig " ←"? ppSpace term
   (" using " num)? (" with" (ppSpace colGt rintroPat)*)? : tactic
 
 macro_rules
 | `(tactic| convert! $cfg $[←%$l]? $t $[using $n]? $[with $[$w]*]?) =>
-    `(tactic| convert $cfg $[←%$l]? $t:term $[using $n]? $[with $[$w]*]?)
+    `(tactic| convert ! $cfg $[←%$l]? $t:term $[using $n]? $[with $[$w]*]?)
 
 /--
 Elaborates `term` ensuring the expected type, allowing stuck metavariables.
@@ -200,14 +219,39 @@ def elabTermForConvert (term : Syntax) (expectedType? : Option Expr) :
       return t
 
 elab_rules : tactic
-| `(tactic| convert $cfg $[←%$sym]? $term $[using $n]? $[with $ps?*]?) =>
+| `(tactic| convert%$tk $[!%$semireducible]? $cfg $[←%$sym]? $term $[using $n]? $[with $ps?*]?) =>
   withMainContext do
-    let config ← Congr!.elabConfig (mkOptionalNode cfg)
+    let config := { ← Convert.elabConfig cfg with }
     let patterns := (ps?.getD #[]).toList
     let expectedType ← mkFreshExprMVar (mkSort (← getLevel (← getMainTarget)))
     let (e, gs) ← elabTermForConvert term expectedType
-    liftMetaTactic fun g ↦
-      return (← g.convert e sym.isSome (n.map (·.getNat)) config patterns) ++ gs
+    if semireducible.isNone then
+      liftMetaTactic fun g ↦ do
+        -- Suggest `convert!` instead of `convert` if we rely on default transparency.
+        let redGoals ← g.convert e sym.isSome (n.map (·.getNat))
+          { config with postTransparency := .reducible }
+          patterns
+        let defaultGoals ← g.convert e sym.isSome (n.map (·.getNat))
+          { config with postTransparency := .default }
+          patterns
+        if redGoals.length == defaultGoals.length then
+          let sameGoals ← try
+            (redGoals.zip defaultGoals).allM fun (g₁, g₂) => do
+              -- Check that they agree on the set of free variables, otherwise we get errors.
+              -- We assume the context in the `convert` case is a subset of the `convert!` case
+              -- since `convert!` can more agressively unfold and introduce more variables.
+              if !(← g₁.getDecl).lctx.isSubPrefixOf (← g₂.getDecl).lctx then return false
+              g₂.withContext <| withReducible <| isDefEq (← g₁.getType) (← g₂.getType)
+            catch _ => pure false
+          -- If the goals are not the same then we should preserve the original behaviour
+          -- and use `convert!`.
+          if !sameGoals then
+            let tac ← `(tactic| convert!%$tk $cfg $[←%$sym]? $term $[using $n]? $[with $ps?*]?)
+            TryThis.addSuggestion tk { suggestion := tac } (origSpan? := ← getRef)
+        return defaultGoals ++ gs
+    else
+      liftMetaTactic fun g ↦
+        return (← g.convert e sym.isSome (n.map (·.getNat)) config patterns) ++ gs
 
 /--
 `convert_to t` on a goal `⊢ t'` changes the goal to `⊢ t` and adds new goals for proving the
@@ -221,8 +265,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 +281,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" ("!")? Parser.Tactic.optConfig " ←"? ppSpace term
   (" using " num)? (" with" (ppSpace colGt rintroPat)*)? (Parser.Tactic.location)? : tactic
 
 @[tactic_alt convertTo]
@@ -247,13 +290,20 @@ 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 $[!%$semireducible]? $cfg $[←%$sym]? $newType $[using $n]?
     $[with $ps?*]? $[$loc?:location]?) => do
   let n : ℕ := n |>.map (·.getNat) |>.getD 1
-  let config ← Congr!.elabConfig cfg
+    let mut config := { ← Convert.elabConfig cfg with }
+    if semireducible.isSome then
+      config := { config with
+        -- TODO: also enable this in the future? (Not right now, for backwards compatibility).
+        -- transparency := default,
+        -- preTransparency := default,
+        -- postTransparency := default -- Disabled while the port to `convert!` happens.
+        }
   let patterns := (ps?.getD #[]).toList
   withLocation (expandOptLocation (mkOptionalNode loc?))
     (atLocal := fun fvarId ↦ do
@@ -279,8 +329,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 +354,4 @@ macro_rules
 | `(tactic| ac_change! $t $[using $n]?) =>
     `(tactic| convert_to! $t:term $[using $n]? <;> try ac_rfl)
 
-
 end Mathlib.Tactic

MathlibTest/convert.lean

@@ -75,7 +75,7 @@ example (prime : Nat → Prop) (n : Nat) (h : prime (2 * n + 1)) :
 
 example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
     ∀ ε > 0, q ε := by
-  convert h using 2 with ε hε
+  convert! h using 2 with ε hε
   guard_hyp hε : ε > 0
   guard_target = q ε ↔ p ε
   exact test_sorry
@@ -128,4 +128,41 @@ 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
+
+/-
+-- These examples can be uncommented when `convert` is reducible by default.
+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