def Lean.Parser.Tactic.anchor : ParserDescr

def Lean.Parser.Tactic.grindLemma : ParserDescr

def Lean.Parser.Tactic.grindLemmaMin : ParserDescr

The ! modifier instructs grind to consider only minimal indexable subexpressions when selecting patterns.

def Lean.Parser.Tactic.grindErase : ParserDescr

def Lean.Parser.Tactic.grindParam : ParserDescr

The ! modifier instructs grind to consider only minimal indexable subexpressions when selecting patterns.

def Lean.Parser.Category.grind_filter : Category

def Lean.Parser.Tactic.Grind.grind_filter.quot : ParserDescr

def Lean.Parser.Tactic.Grind.grind_filter_ : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen<_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen=_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen!=_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen≤_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen<=_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen>_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen≥_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen>=_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filter(_)» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filter_&&_» : TrailingParserDescr

def Lean.Parser.Tactic.Grind.«grind_filter_||_» : TrailingParserDescr

def Lean.Parser.Tactic.Grind.grind_filter!_ : ParserDescr

def Lean.Parser.Tactic.Grind.grindFilter : ParserDescr

def Lean.Parser.Tactic.Grind.grind.quot : ParserDescr

def Lean.Parser.Category.grind : Category

grind is the syntax category for a "grind interactive tactic". A grind tactic is a program which receives a grind goal.

def Lean.Parser.Tactic.Grind.grindStep : ParserDescr

def Lean.Parser.Tactic.Grind.grindSeq1Indented : ParserDescr

def Lean.Parser.Tactic.Grind.grindSeqBracketed : ParserDescr

def Lean.Parser.Tactic.Grind.grindSeq : ParserDescr

def Lean.Parser.Tactic.Grind.paren : ParserDescr

(grindSeq) runs the grindSeq in sequence on the current list of targets. This is pure grouping with no added effects.

def Lean.Parser.Tactic.Grind.skip : ParserDescr

skip does nothing.

def Lean.Parser.Tactic.Grind.lia : ParserDescr

lia linear integer arithmetic.

def Lean.Parser.Tactic.Grind.ring : ParserDescr

ring (commutative) rings and fields.

def Lean.Parser.Tactic.Grind.ac : ParserDescr

ac associativity and commutativity procedure.

def Lean.Parser.Tactic.Grind.linarith : ParserDescr

linarith linear arithmetic.

def Lean.Parser.Tactic.Grind.sorry : ParserDescr

The sorry tactic is a temporary placeholder for an incomplete tactic proof.

def Lean.Parser.Tactic.Grind.thmNs : ParserDescr

def Lean.Parser.Tactic.Grind.thm : ParserDescr

def Lean.Parser.Tactic.Grind.instantiate : ParserDescr

Instantiates theorems using E-matching. The approx modifier is just a marker for users to easily identify automatically generated instantiate tactics that may have redundant arguments.

def Lean.Parser.Tactic.Grind.use : ParserDescr

Shorthand for instantiate only

def Lean.Parser.Tactic.Grind.showAsserted : ParserDescr

Shows asserted facts.

def Lean.Parser.Tactic.Grind.showTrue : ParserDescr

Shows propositions known to be True.

def Lean.Parser.Tactic.Grind.showFalse : ParserDescr

Shows propositions known to be False.

def Lean.Parser.Tactic.Grind.showEqcs : ParserDescr

Shows equivalence classes of terms.

def Lean.Parser.Tactic.Grind.showCases : ParserDescr

Show case-split candidates.

def Lean.Parser.Tactic.Grind.showState : ParserDescr

Show grind state.

def Lean.Parser.Tactic.Grind.showLocalThms : ParserDescr

Show active local theorems and their anchors for heuristic instantiation.

def Lean.Parser.Tactic.Grind.showTerm : ParserDescr

show_term tac runs tac, then displays the generated proof in the InfoView.

def Lean.Parser.Tactic.Grind.showGoals : ParserDescr

Shows the pending goals.

def Lean.Parser.Category.grind_ref : Category

def Lean.Parser.Tactic.Grind.grind_ref.quot : ParserDescr

def Lean.Parser.Tactic.Grind.grind_ref_ : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_ref__/__» : ParserDescr

Anchor with an ordinal disambiguator. Distinct case-split candidates may have the same anchor. For example, two candidates that differ only in inaccessible variables have identical anchors. #a56e/2 refers to the second candidate (in the case-split candidate list) matching the anchor #a56e.

def Lean.Parser.Tactic.Grind.grind_ref__1 : ParserDescr

def Lean.Parser.Tactic.Grind.cases : ParserDescr

Performs a case-split on a logical connective, match-expression, if-then-else-expression, or inductive predicate. The argument is an anchor referencing one of the case-split candidates in the grind state. You can use cases? to select a specific candidate using a code action. If multiple candidates match the anchor (e.g., they differ only in inaccessible variables), an ordinal reference such as #a56e/2 selects the second matching candidate.

def Lean.Parser.Tactic.Grind.casesTrace : ParserDescr

A variant of cases that provides a code-action for selecting one of the candidate case-splits available in the grind state.

def Lean.Parser.Tactic.Grind.casesNext : ParserDescr

Performs the next case-split. The case-split is selected using the same heuristic used by finish.

def Lean.Parser.Tactic.Grind.done : ParserDescr

done succeeds iff there are no remaining goals.

def Lean.Parser.Tactic.Grind.finish : ParserDescr

finish tries to close the current goal using grind's default strategy

def Lean.Parser.Tactic.Grind.finishTrace : ParserDescr

finish? tries to close the current goal using grind's default strategy and suggests a tactic script.

def Lean.Parser.Tactic.Grind.have : ParserDescr

The have tactic is for adding opaque definitions and hypotheses to the local context of the main goal. The definitions forget their associated value and cannot be unfolded.

• have h : t := e adds the hypothesis h : t if e is a term of type t.
• have h := e uses the type of e for t.
• have : t := e and have := e use this for the name of the hypothesis.

def Lean.Parser.Tactic.Grind.nestedTacticCore : ParserDescr

Executes the given tactic block to close the current goal.

def Lean.Parser.Tactic.Grind.allGoals : ParserDescr

all_goals tac runs tac on each goal, concatenating the resulting goals. If the tactic fails on any goal, the entire all_goals tactic fails.

def Lean.Parser.Tactic.Grind.focus : ParserDescr

focus tac focuses on the main goal, suppressing all other goals, and runs tac on it. Usually · tac, which enforces that the goal is closed by tac, should be preferred.

def Lean.Parser.Tactic.Grind.next : ParserDescr

next => tac focuses on the next goal and solves it using tac, or else fails. next x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.

def Lean.Parser.Tactic.Grind.«grind·_» : ParserDescr

· grindSeq focuses on the main grind goal and tries to solve it using the given sequence of grind tactics.

def Lean.Parser.Tactic.Grind.case : ParserDescr

• case tag => tac focuses on the goal with case name tag and solves it using tac, or else fails.
• case tag x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.
• case tag₁ | tag₂ => tac is equivalent to (case tag₁ => tac); (case tag₂ => tac).

def Lean.Parser.Tactic.Grind.anyGoals : ParserDescr

any_goals tac applies the tactic tac to every goal, concatenating the resulting goals for successful tactic applications. If the tactic fails on all of the goals, the entire any_goals tactic fails.

This tactic is like all_goals try tac except that it fails if none of the applications of tac succeeds.

def Lean.Parser.Tactic.Grind.withAnnotateState : ParserDescr

with_annotate_state stx t annotates the lexical range of stx : Syntax with the initial and final state of running tactic t.

def Lean.Parser.Tactic.Grind.«grind_<;>_» : TrailingParserDescr

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

def Lean.Parser.Tactic.Grind.first : ParserDescr

first (tac) ... runs each tac until one succeeds, or else fails.

def Lean.Parser.Tactic.Grind.grindTry_ : ParserDescr

try tac runs tac and succeeds even if tac failed.

def Lean.Parser.Tactic.Grind.failIfSuccess : ParserDescr

fail_if_success t fails if the tactic t succeeds.

def Lean.Parser.Tactic.Grind.grindAdmit : ParserDescr

admit is a synonym for sorry.

def Lean.Parser.Tactic.Grind.fail : ParserDescr

fail msg is a tactic that always fails, and produces an error using the given message.

def Lean.Parser.Tactic.Grind.grindRepeat_ : ParserDescr

repeat tac repeatedly applies tac so long as it succeeds. The tactic tac may be a tactic sequence, and if tac fails at any point in its execution, repeat will revert any partial changes that tac made to the tactic state. The tactic tac should eventually fail, otherwise repeat tac will run indefinitely.

def Lean.Parser.Tactic.Grind.renameI : ParserDescr

rename_i x_1 ... x_n renames the last n inaccessible names using the given names.

def Lean.Parser.Tactic.Grind.exposeNames : ParserDescr

expose_names renames all inaccessible variables with accessible names, making them available for reference in generated tactics. However, this renaming introduces machine-generated names that are not fully under user control. expose_names is primarily intended as a preamble for generated grind tactic scripts.

def Lean.Parser.Tactic.Grind.setOption : ParserDescr

set_option opt val in tacs (the tactic) acts like set_option opt val at the command level, but it sets the option only within the tactics tacs.

def Lean.Parser.Tactic.Grind.setConfig : ParserDescr

set_config configItem+ in tacs executes tacs with the updated configuration options configItem+

def Lean.Parser.Tactic.Grind.haveSilent : ParserDescr

Proves <term> using the current grind state and default search strategy.

def Lean.Parser.Tactic.Grind.mbtc : ParserDescr

Adds new case-splits using model-based theory combination.

def Lean.Parser.Tactic.Grind.symIntro : ParserDescr

intro x₁ ... xₙ introduces binders and internalizes them into the E-graph. Only available in sym => mode. intro with no arguments introduces one binder with an inaccessible name. Use intro (internalize := false) or intro~ to skip internalization.

def Lean.Parser.Tactic.Grind.symIntroLight : ParserDescr

intro~ x₁ ... xₙ is shorthand for intro (internalize := false).

def Lean.Parser.Tactic.Grind.symIntros : ParserDescr

intros introduces all remaining binders and internalizes them. Only available in sym => mode. Use intros (internalize := false) or intros~ to skip internalization.

def Lean.Parser.Tactic.Grind.symIntrosLight : ParserDescr

intros~ is shorthand for intros (internalize := false).

def Lean.Parser.Tactic.Grind.symApply : ParserDescr

apply t applies theorem t as a backward rule. Only available in sym => mode. When used with repeat, the backward rule is cached for efficiency.

def Lean.Parser.Tactic.Grind.symInternalize : ParserDescr

internalize internalizes hypotheses into the grind E-graph. Only available in sym => mode.

• internalize internalizes the next hypothesis.
• internalize <num> internalizes the next <num> hypotheses.

def Lean.Parser.Tactic.Grind.symInternalizeAll : ParserDescr

internalize_all internalizes all pending hypotheses into the grind E-graph. Only available in sym => mode.

def Lean.Parser.Tactic.Grind.symByContra : ParserDescr

by_contra applies proof by contradiction, negating the target and making it False. Only available in sym => mode.

def Lean.Parser.Tactic.Grind.symSimp : ParserDescr

simp applies the structural simplifier to the goal target. Only available in sym => mode.

• simp — uses the default (identity) variant
• simp myVariant — uses a named variant registered via register_sym_simp
• simp [thm₁, thm₂, ...] — default variant with extra rewrite theorems appended to post
• simp myVariant [thm₁, thm₂, ...] — named variant with extra theorems

def Lean.Parser.Tactic.Grind.symDSimp : ParserDescr

dsimp applies the definitional simplifier to the goal target. Only available in sym => mode.

• dsimp — uses the default (identity) variant
• dsimp myVariant — uses a named variant registered via register_sym_dsimp
• dsimp [id₁, id₂, ...] — default variant with extra declarations to unfold
• dsimp myVariant [id₁, id₂, ...] — named variant with extra declarations

def Lean.Parser.Tactic.Grind.symRw : ParserDescr

rw [h₁, ..., hₙ] rewrites the goal target using the given equations or iffs, left to right. Use ← h to rewrite right to left. Only available in sym => mode, and it only rewrites the target: in sym => mode hypotheses are never modified.

Premises of a conditional rewrite rule that cannot be resolved by unification or type class resolution become new goals.

rw is not a high-performance tactic: it does not exploit the maximal sharing maintained by sym => mode, and should be used for surgical changes to the goal, not for bulk simplification. Use simp/dsimp variants for that.

def Lean.Parser.Tactic.Grind.grindExact_ : ParserDescr

exact e closes the main goal if its target type matches that of e.

def Lean.Parser.Tactic.Grind.symCbv : ParserDescr

cbv performs simplification that closely mimics call-by-value evaluation. It reduces terms by unfolding definitions using their defining equations and applying matcher equations. The unfolding is propositional, so cbv also works with functions defined via well-founded recursion or partial fixpoints.

cbv reduces the goal target using call-by-value evaluation. For equation goals (lhs = rhs), cbv automatically attempts refl after reduction to close the goal.

Unlike the standalone cbv tactic, this variant does not support the at location syntax: in sym => mode it only reduces the goal target.

cbv is not a finishing tactic in general: it may leave a new (simpler) goal.

The proofs produced by cbv only use the three standard axioms. In particular, they do not require trust in the correctness of the code generator.

This is a variant of cbv that only works in sym => mode.

def Lean.Parser.Tactic.Grind.bvNormalize : ParserDescr

Run the normalization procedure of bv_decide only. Sometimes this is enough to solve basic BitVec goals already.

Note: include import Std.Tactic.BVDecide

def Lean.Parser.Tactic.Grind.bvDecide : ParserDescr

Close fixed-width BitVec and Bool goals by obtaining a proof from an external SAT solver and verifying it inside Lean. The solvable goals are currently limited to

• the Lean equivalent of QF_BV
• automatically splitting up structures that contain information about BitVec or Bool

example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
  intros
  bv_decide

If bv_decide encounters an unknown definition it will be treated like an unconstrained BitVec variable. Sometimes this enables solving goals despite not understanding the definition because the precise properties of the definition do not matter in the specific proof.

If bv_decide fails to close a goal it provides a counter-example, containing assignments for all terms that were considered as variables.

In order to avoid calling a SAT solver every time, the proof can be cached with bv_decide?.

If solving your problem relies inherently on using associativity or commutativity, consider enabling the bv.ac_nf option.

bv_decide types [T₁, ..., Tₙ] restricts the analysis of structures and enum inductives to T₁, ..., Tₙ, treating all other ones as opaque variables.

Note: bv_decide trusts the correctness of the code generator and adds a axioms asserting its result.

Note: include import Std.Tactic.BVDecide

def Lean.Parser.Tactic.Grind.bvTrace : ParserDescr

Suggest a proof script for a bv_decide tactic call. Useful for caching LRAT proofs.

Note: include import Std.Tactic.BVDecide

def Lean.Parser.Tactic.Grind.bvCheck : ParserDescr

This tactic works just like bv_decide but skips calling a SAT solver by using a proof that is already stored on disk. It is called with the name of an LRAT file in the same directory as the current Lean file:

bv_check "proof.lrat"