# 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 `MathlibTest/Use.lean`.

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

Equations

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

Instances For

source
partial def Mathlib.Tactic.useLoop (eager : Bool) (gs : List Lean.MVarId) (args : List Lean.Term) (acc 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`.

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

Equations

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

Instances For

source
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`.

Equations

- Mathlib.Tactic.tacticUse_discharger = Lean.ParserDescr.node `Mathlib.Tactic.tacticUse_discharger 1024 (Lean.ParserDescr.nonReservedSymbol "use_discharger" false)

Instances For

source
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`.

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For