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