Documentation

Mathlib.Tactic.Use

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

      use_discharger is used by use to discharge side goals.

      This is an extensible tactic using macro_rules. By default it can:

      • rewrite a goal ∃ _ : p, q into p ∧ q if p is in Prop;
      • solve the goal p ∧ q by creating subgoals p and q;
      • apply rfl;
      • solve a goal by applying an assumption;
      • solve the goal True.
      Equations
      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₂, ⋯ instantiates all existential quantifiers in the main goal by using e₁, e₂, ... as witnesses, creates goals for all the remaining witnesses, and tries to discharge these goals automatically.

          use is similar to exists or existsi, 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).

          • use! e₁, e₂, ⋯ 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.
          • use (discharger := tac) e₁, e₂, ... calls tac as a discharger, on all remaining Prop-valued goals. If this option is omitted, use calls try with_reducible use_discharger as default discharger. To turn off the discharger and keep all goals, use (discharger := skip). To allow "heavy refls", use (discharger := try use_discharger). If tac fails on the new goal, use (discharger := tac) fails (hint: you might want to use (discharger := try tac) instead).

          Examples:

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

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

example : Nonempty Nat := by use 5

example : Nonempty (PNat ≃ Nat) := by
  use PNat.natPred, Nat.succPNat
  · exact PNat.succPNat_natPred
  · intro; rfl

-- With `use!` one can feed in each `42` one at a time:
example : ∃ n : {n : Nat // n % 2 = 0}, n.val > 10 := by use! 20; simp

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.
-/
          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₂, ⋯ instantiates all existential quantifiers in the main goal by using e₁, e₂, ... as witnesses, creates goals for all the remaining witnesses, and tries to discharge these goals automatically.

            use is similar to exists or existsi, 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).

            • use! e₁, e₂, ⋯ 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.
            • use (discharger := tac) e₁, e₂, ... calls tac as a discharger, on all remaining Prop-valued goals. If this option is omitted, use calls try with_reducible use_discharger as default discharger. To turn off the discharger and keep all goals, use (discharger := skip). To allow "heavy refls", use (discharger := try use_discharger). If tac fails on the new goal, use (discharger := tac) fails (hint: you might want to use (discharger := try tac) instead).

            Examples:

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

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

example : Nonempty Nat := by use 5

example : Nonempty (PNat ≃ Nat) := by
  use PNat.natPred, Nat.succPNat
  · exact PNat.succPNat_natPred
  · intro; rfl

-- With `use!` one can feed in each `42` one at a time:
example : ∃ n : {n : Nat // n % 2 = 0}, n.val > 10 := by use! 20; simp

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.
-/
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For