The use tactic

The use and use! tactics are for instantiating one-constructor inductive types just like the exists tactic, but they can be a little more flexible.

use is the more restrained version for mathlib4, and use! is the exuberant version that more closely matches use from mathlib3.

Note: The use! tactic is almost exactly the mathlib3 use except that it does not try applying exists_prop. See the failing test in test/Use.lean.

def Mathlib.Tactic.applyTheConstructor (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId × List Lean.MVarId × List Lean.MVarId)

When the goal mvarId is an inductive datatype with a single constructor, this applies that constructor, then returns metavariables for the non-parameter explicit arguments along with metavariables for the parameters and implicit arguments.

The first list of returned metavariables correspond to the arguments that ⟨x,y,...⟩ notation uses. The second list corresponds to everything else: the parameters and implicit arguments. The third list consists of those implicit arguments that are instance implicits, which one can try to synthesize. The third list is a sublist of the second list.

Returns metavariables for all arguments whether or not the metavariables are assigned.

partial def Mathlib.Tactic.useLoop (eager : Bool) (gs : List Lean.MVarId) (args : List Lean.Term) (acc : List Lean.MVarId) (insts : List Lean.MVarId) : Lean.Elab.TermElabM (List Lean.MVarId × List Lean.MVarId × List Lean.MVarId)

Use the args to refine the goals gs in order, but whenever there is a single goal remaining then first try applying a single constructor if it's for a single-constructor inductive type. In eager mode, instead we always first try to refine, and if that fails we always try to apply such a constructor no matter if it's the last goal.

Returns the remaining explicit goals gs, any goals acc due to refine, and a sublist of these of instance arguments that we should try synthesizing after the loop. The new set of goals should be gs ++ acc.

def Mathlib.Tactic.runUse (eager : Bool) (discharger : Lean.Elab.Tactic.TacticM Unit) (args : List Lean.Term) : Lean.Elab.Tactic.TacticM Unit

Run the useLoop on the main goal then discharge remaining explicit Prop arguments.

def Mathlib.Tactic.tacticUse_discharger : Lean.ParserDescr

Default discharger to try to use for the use and use! tactics. This is similar to the trivial tactic but doesn't do things like contradiction or decide.

def Mathlib.Tactic.mkUseDischarger (discharger? : Option (Lean.TSyntax `Lean.Parser.Tactic.discharger)) : Lean.Elab.Tactic.TacticM (Lean.Elab.Tactic.TacticM Unit)

Returns a TacticM Unit that either runs the tactic sequence from discharger? if it's non-none, or it does try with_reducible use_discharger.

def Mathlib.Tactic.useSyntax : Lean.ParserDescr

use e₁, e₂, ⋯ is similar to exists, but unlike exists it is equivalent to applying the tactic refine ⟨e₁, e₂, ⋯, ?_, ⋯, ?_⟩ with any number of placeholders (rather than just one) and then trying to close goals associated to the placeholders with a configurable discharger (rather than just try trivial).

Examples:

example : ∃ x : Nat, x = x := by use 42

example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42

example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")

use! e₁, e₂, ⋯ is similar but it applies constructors everywhere rather than just for goals that correspond to the last argument of a constructor. This gives the effect that nested constructors are being flattened out, with the supplied values being used along the leaves and nodes of the tree of constructors. With use! one can feed in each 42 one at a time:

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! 42, 42

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)

The second line makes use of the fact that use! tries refining with the argument before applying a constructor. Also note that use/use! by default uses a tactic called use_discharger to discharge goals, so use! 42 will close the goal in this example since use_discharger applies rfl, which as a consequence solves for the other Nat metavariable.

These tactics take an optional discharger to handle remaining explicit Prop constructor arguments. By default it is use (discharger := try with_reducible use_discharger) e₁, e₂, ⋯. To turn off the discharger and keep all goals, use (discharger := skip). To allow "heavy refls", use (discharger := try use_discharger).

def Mathlib.Tactic.«tacticUse!___,,» : Lean.ParserDescr

use e₁, e₂, ⋯ is similar to exists, but unlike exists it is equivalent to applying the tactic refine ⟨e₁, e₂, ⋯, ?_, ⋯, ?_⟩ with any number of placeholders (rather than just one) and then trying to close goals associated to the placeholders with a configurable discharger (rather than just try trivial).

Examples:

example : ∃ x : Nat, x = x := by use 42

example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42

example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")

use! e₁, e₂, ⋯ is similar but it applies constructors everywhere rather than just for goals that correspond to the last argument of a constructor. This gives the effect that nested constructors are being flattened out, with the supplied values being used along the leaves and nodes of the tree of constructors. With use! one can feed in each 42 one at a time:

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! 42, 42

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)

The second line makes use of the fact that use! tries refining with the argument before applying a constructor. Also note that use/use! by default uses a tactic called use_discharger to discharge goals, so use! 42 will close the goal in this example since use_discharger applies rfl, which as a consequence solves for the other Nat metavariable.

These tactics take an optional discharger to handle remaining explicit Prop constructor arguments. By default it is use (discharger := try with_reducible use_discharger) e₁, e₂, ⋯. To turn off the discharger and keep all goals, use (discharger := skip). To allow "heavy refls", use (discharger := try use_discharger).