The convert tactic.

The exact e and refine e tactics require a term e whose type is definitionally equal to the goal. convert e is similar to refine e, but the type of e is not required to exactly match the goal. Instead, new goals are created for differences between the type of e and the goal using the same strategies as the congr! tactic. For example, in the proof state

n : ℕ,
e : Prime (2 * n + 1)
⊢ Prime (n + n + 1)

the tactic convert e using 2 will change the goal to

⊢ 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:

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 in this case.

The syntax convert ← e will reverse the direction of the new goals (producing ⊢ 2 * n = n + n in this example).

Internally, convert e works by creating a new goal asserting that the goal equals the type of e, then simplifying it using congr!. The syntax convert e using n can be used to control the depth of matching (like congr! n). In the example, convert e using 1 would produce a new goal ⊢ n + n + 1 = 2 * n + 1.

Refer to the congr! tactic to understand the congruence operations. One of its many features is that if x y : t and an instance Subsingleton t is in scope, then any goals of the form x = y are solved automatically.

Like congr!, convert takes an optional with clause of rintro patterns, for example convert e using n with x y z.

The convert tactic also takes a configuration option, for example

convert (config := {transparency := .default}) h

These are passed to congr!. See Congr!.Config for options.

structure Convert.CheapConfigextends Congr!.Config : Type

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.

• closePre : Bool
• closePost : Bool
• transparency : Lean.Meta.TransparencyMode
• preTransparency : Lean.Meta.TransparencyMode
• postTransparency : Lean.Meta.TransparencyMode
• preferLHS : Bool
• partialApp : Bool
• sameFun : Bool
• maxArgs : Option ℕ
• typeEqs : Bool
• etaExpand : Bool
• useCongrSimp : Bool
• beqEq : Bool

def Convert.elabCheapConfig (cfg : Lean.Syntax) (init : CheapConfig := { }) (logExceptions : Bool := true) : Lean.Elab.Tactic.TacticM CheapConfig

Internal elaborator for Convert.CheapConfig: use Convert.elabConfig instead.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Convert.CheapConfig.unfoldSameFun : 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.

Equations

• Convert.CheapConfig.unfoldSameFun = { toConfig := Congr!.Config.unfoldSameFun }

structure Convert.ExpensiveConfigextends Convert.CheapConfig : Type

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)

• closePre : Bool
• closePost : Bool
• transparency : Lean.Meta.TransparencyMode
• preTransparency : Lean.Meta.TransparencyMode
• postTransparency : Lean.Meta.TransparencyMode
• preferLHS : Bool
• partialApp : Bool
• sameFun : Bool
• maxArgs : Option ℕ
• typeEqs : Bool
• etaExpand : Bool
• useCongrSimp : Bool
• beqEq : Bool

def Convert.elabExpensiveConfig (cfg : Lean.Syntax) (init : ExpensiveConfig := { }) (logExceptions : Bool := true) : Lean.Elab.Tactic.TacticM ExpensiveConfig

Internal elaborator for Convert.ExpensiveConfig: use Convert.elabConfig instead.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Convert.ExpensiveConfig.unfoldSameFun : 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.

Equations

• Convert.ExpensiveConfig.unfoldSameFun = { toConfig := Congr!.Config.unfoldSameFun }

def Convert.elabConfig (expensive : Bool) (stx : Lean.Syntax) : Lean.Elab.Tactic.TacticM Congr!.Config

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).)

Equations

• One or more equations did not get rendered due to their size.

def Lean.MVarId.convert (e : Expr) (symm : Bool) (depth : Option ℕ := none) (config : Congr!.Config := { }) (patterns : List (TSyntax `rintroPat) := []) (g : MVarId) : MetaM (List MVarId)

Close the goal g using Eq.mp v e, where v is a metavariable asserting that the type of g and e are equal. Then call MVarId.congrN! (also using local hypotheses and reflexivity) on v, and return the resulting goals.

With symm = true, reverses the equality in v, and uses Eq.mpr v e instead. With depth = some n, calls MVarId.congrN! n instead, with n as the max recursion depth.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MVarId.convertLocalDecl (g : MVarId) (fvarId : FVarId) (typeNew : Expr) (symm : Bool) (depth : Option ℕ := none) (config : Congr!.Config := { }) (patterns : List (TSyntax `rintroPat) := []) : MetaM (MVarId × List MVarId)

Replaces the type of the local declaration fvarId with typeNew, using Lean.MVarId.congrN! to prove that the old type of fvarId is equal to typeNew. Uses Lean.MVarId.replaceLocalDecl to replace the type. Returns the new goal along with the side goals generated by congrN!.

With symm = true, reverses the equality, changing the goal to prove typeNew is equal to typeOld. With depth = some n, calls MVarId.congrN! n instead, with n as the max recursion depth.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.convert : Lean.ParserDescr

convert e, where the term e is inferred to have type t, replaces the main goal ⊢ t' with new goals for proving the equality t' = t using congruence. The goals are created like congr! would. Like refine e, any holes (?_ or ?x) in e that are not solved by unification are converted into new goals, using the hole's name, if any, as the goal case name. Like congr!, convert introduces variables while applying congruence rules. These can be 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 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 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. By default, the depth is unlimited.
• convert e with x ⟨y₁, y₂⟩ (z₁ | z₂) names or pattern-matches the variables introduced by congruence rules, like rintro x ⟨y₁, y₂⟩ (z₁ | z₂) would.
• convert (config := cfg) e uses the configuration options in cfg to control the congruence rules (see Congr!.Config).

Examples:

-- `convert using` controls the depth of congruence.
example {n : ℕ} (e : Prime (2 * n + 1)) :
    Prime (n + n + 1) := by
  convert e using 2
  -- One goal: ⊢ n + n = 2 * n
  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
    done
  exact h -- succeeds

-- `convert with` names introduced variables.
example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
    ∀ ε > 0, q ε := by
  convert h using 2 with ε hε
  -- Goal now looks like:
  -- hε : ε > 0
  -- ⊢ q ε ↔ p ε
  sorry

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.convert! : Lean.ParserDescr

convert e, where the term e is inferred to have type t, replaces the main goal ⊢ t' with new goals for proving the equality t' = t using congruence. The goals are created like congr! would. Like refine e, any holes (?_ or ?x) in e that are not solved by unification are converted into new goals, using the hole's name, if any, as the goal case name. Like congr!, convert introduces variables while applying congruence rules. These can be 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 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 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. By default, the depth is unlimited.
• convert e with x ⟨y₁, y₂⟩ (z₁ | z₂) names or pattern-matches the variables introduced by congruence rules, like rintro x ⟨y₁, y₂⟩ (z₁ | z₂) would.
• convert (config := cfg) e uses the configuration options in cfg to control the congruence rules (see Congr!.Config).

Examples:

-- `convert using` controls the depth of congruence.
example {n : ℕ} (e : Prime (2 * n + 1)) :
    Prime (n + n + 1) := by
  convert e using 2
  -- One goal: ⊢ n + n = 2 * n
  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
    done
  exact h -- succeeds

-- `convert with` names introduced variables.
example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
    ∀ ε > 0, q ε := by
  convert h using 2 with ε hε
  -- Goal now looks like:
  -- hε : ε > 0
  -- ⊢ q ε ↔ p ε
  sorry

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.elabTermForConvert (term : Lean.Syntax) (expectedType? : Option Lean.Expr) : Lean.Elab.Tactic.TacticM (Lean.Expr × List Lean.MVarId)

Elaborates term ensuring the expected type, allowing stuck metavariables. Returns stuck metavariables as additional goals.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.convertTo : Lean.ParserDescr

convert_to t on a goal ⊢ t' changes the goal to ⊢ t and adds new goals for proving the equality t' = t using congruence. The goals are created like congr! would. Any remaining congruence goals come before the main goal. Like refine e, any holes (?_ or ?x) in t that are not solved by unification are converted 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.

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 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 the right).
• convert_to 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 (n + n + 1), then convert_to Prime (2 * n + 1) using 2 results in one goal, ⊢ n + n = 2 * n, and convert_to Prime (2 * n + 1) using 3 (or more) results in two (impossible) goals ⊢ HAdd.hAdd = HMul.hMul and ⊢ n = 2. The default value for n is 1.
• convert_to t with x ⟨y₁, y₂⟩ (z₁ | z₂) names or pattern-matches the variables introduced by congruence rules, like rintro x ⟨y₁, y₂⟩ (z₁ | z₂) would.
• convert_to (config := cfg) t uses the configuration options in cfg to control the congruence rules (see Congr!.Config).

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.convert_to! : Lean.ParserDescr

convert_to t on a goal ⊢ t' changes the goal to ⊢ t and adds new goals for proving the equality t' = t using congruence. The goals are created like congr! would. Any remaining congruence goals come before the main goal. Like refine e, any holes (?_ or ?x) in t that are not solved by unification are converted 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.

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 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 the right).
• convert_to 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 (n + n + 1), then convert_to Prime (2 * n + 1) using 2 results in one goal, ⊢ n + n = 2 * n, and convert_to Prime (2 * n + 1) using 3 (or more) results in two (impossible) goals ⊢ HAdd.hAdd = HMul.hMul and ⊢ n = 2. The default value for n is 1.
• convert_to t with x ⟨y₁, y₂⟩ (z₁ | z₂) names or pattern-matches the variables introduced by congruence rules, like rintro x ⟨y₁, y₂⟩ (z₁ | z₂) would.
• convert_to (config := cfg) t uses the configuration options in cfg to control the congruence rules (see Congr!.Config).

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.acChange : Lean.ParserDescr

ac_change t on a goal ⊢ t' changes the goal to ⊢ t and adds new goals for proving the equality t' = t using congruence, then tries proving these goals by associativity and commutativity. The goals are created like congr! would. In other words, ac_change t is like convert_to t followed by ac_refl.

Like refine e, any holes (?_ or ?x) in t that are not solved by unification are converted 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 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 ac_change Prime ((1 + a * b) + c) using 3 (or more) results in two (impossible) goals ⊢ 1 = a * b and ⊢ a * b = 1. The default value for n is 1.

Example:

example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
  ac_change a + d + e + f + c + g + b ≤ _
  -- ⊢ a + d + e + f + c + g + b ≤ N

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.acChange! : Lean.ParserDescr

ac_change t on a goal ⊢ t' changes the goal to ⊢ t and adds new goals for proving the equality t' = t using congruence, then tries proving these goals by associativity and commutativity. The goals are created like congr! would. In other words, ac_change t is like convert_to t followed by ac_refl.

Like refine e, any holes (?_ or ?x) in t that are not solved by unification are converted 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 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 ac_change Prime ((1 + a * b) + c) using 3 (or more) results in two (impossible) goals ⊢ 1 = a * b and ⊢ a * b = 1. The default value for n is 1.

Example:

example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
  ac_change a + d + e + f + c + g + b ≤ _
  -- ⊢ a + d + e + f + c + g + b ≤ N

Equations

• One or more equations did not get rendered due to their size.