Undo most changes, just add exclamations to all converts

Author: Vierkantor

Mathlib/Tactic/CongrExclamation.lean

@@ -63,8 +63,7 @@ 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. Discharging is done at default transparency (but this will be changed
-  to reducible transparency in the future).
+  `assumption` tactic.
 
 The optional parameter is the depth of the recursive applications.
 This is useful when `congr!` is too aggressive in breaking down the goal.
@@ -107,8 +106,7 @@ 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 the transparency level specified by `postTransparency`, which is currently set to
-  `.default` but will soon become `.reducible`. -/
+  with current tactic transparency level. -/
   closePost : Bool := true
   /-- The transparency level to use when applying a congruence theorem.
   By default this is `.reducible`, which prevents unfolding of most definitions. -/
@@ -117,11 +115,6 @@ 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.
@@ -197,7 +190,6 @@ 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 :=
@@ -684,8 +676,7 @@ 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) :=
-  withTransparency config.postTransparency do
+def Lean.MVarId.postCongr! (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option MVarId) := 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,25 +77,6 @@ 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.
@@ -151,7 +132,8 @@ 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 when solving side goals. This is currently the same
+  behaviour as `convert`, but `convert` will use reducible transparency in the future.
 * `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
@@ -174,7 +156,6 @@ 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
@@ -221,7 +202,7 @@ def elabTermForConvert (term : Syntax) (expectedType? : Option Expr) :
 elab_rules : tactic
 | `(tactic| convert%$tk $[!%$semireducible]? $cfg $[←%$sym]? $term $[using $n]? $[with $ps?*]?) =>
   withMainContext do
-    let config := { ← Convert.elabConfig cfg with }
+    let config ← Congr!.elabConfig (mkOptionalNode cfg)
     let patterns := (ps?.getD #[]).toList
     let expectedType ← mkFreshExprMVar (mkSort (← getLevel (← getMainTarget)))
     let (e, gs) ← elabTermForConvert term expectedType
@@ -243,7 +224,8 @@ 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, rather than reducible, when solving side goals.
+* `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 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
@@ -259,7 +241,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" ("!")? 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]
@@ -268,20 +250,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 $[!%$semireducible]? $cfg $[←%$sym]? $newType $[using $n]?
+| `(tactic| convert_to $cfg $[←%$sym]? $newType $[using $n]?
     $[with $ps?*]? $[$loc?:location]?) => do
   let n : ℕ := n |>.map (·.getNat) |>.getD 1
-    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 config ← Congr!.elabConfig cfg
   let patterns := (ps?.getD #[]).toList
   withLocation (expandOptLocation (mkOptionalNode loc?))
     (atLocal := fun fvarId ↦ do
@@ -307,7 +282,8 @@ 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, rather than reducible, when solving side goals.
+* `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 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
@@ -332,4 +308,5 @@ 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,41 +128,4 @@ 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