def Lean.Parser.Tactic.withAnnotateState : Lean.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.intro : Lean.ParserDescr

Introduces one or more hypotheses, optionally naming and/or pattern-matching them. For each hypothesis to be introduced, the remaining main goal's target type must be a let or function type.

• intro by itself introduces one anonymous hypothesis, which can be accessed by e.g. assumption.
• intro x y introduces two hypotheses and names them. Individual hypotheses can be anonymized via _, or matched against a pattern:

  -- ... ⊢ α × β → ...
  intro (a, b)
  -- ..., a : α, b : β ⊢ ...
  

• Alternatively, intro can be combined with pattern matching much like fun:

  intro
  | n + 1, 0 => tac
  | ...
  

def Lean.Parser.Tactic.intros : Lean.ParserDescr

intros x... behaves like intro x..., but then keeps introducing (anonymous) hypotheses until goal is not of a function type.

def Lean.Parser.Tactic.rename : Lean.ParserDescr

rename t => x renames the most recent hypothesis whose type matches t (which may contain placeholders) to x, or fails if no such hypothesis could be found.

def Lean.Parser.Tactic.revert : Lean.ParserDescr

revert x... is the inverse of intro x...: it moves the given hypotheses into the main goal's target type.

def Lean.Parser.Tactic.clear : Lean.ParserDescr

clear x... removes the given hypotheses, or fails if there are remaining references to a hypothesis.

def Lean.Parser.Tactic.subst : Lean.ParserDescr

subst x... substitutes each x with e in the goal if there is a hypothesis of type x = e or e = x. If x is itself a hypothesis of type y = e or e = y, y is substituted instead.

def Lean.Parser.Tactic.substVars : Lean.ParserDescr

Applies subst to all hypotheses of the form h : x = t or h : t = x.

def Lean.Parser.Tactic.assumption : Lean.ParserDescr

assumption tries to solve the main goal using a hypothesis of compatible type, or else fails. Note also the ‹t› term notation, which is a shorthand for show t by assumption.

def Lean.Parser.Tactic.contradiction : Lean.ParserDescr

contradiction closes the main goal if its hypotheses are "trivially contradictory".

• Inductive type/family with no applicable constructors

example (h : False) : p := by contradiction

• Injectivity of constructors

example (h : none = some true) : p := by contradiction  --

• Decidable false proposition

example (h : 2 + 2 = 3) : p := by contradiction

• Contradictory hypotheses

example (h : p) (h' : ¬ p) : q := by contradiction

• Other simple contradictions such as

example (x : Nat) (h : x ≠ x) : p := by contradiction

def Lean.Parser.Tactic.apply : Lean.ParserDescr

apply e tries to match the current goal against the conclusion of e's type. If it succeeds, then the tactic returns as many subgoals as the number of premises that have not been fixed by type inference or type class resolution. Non-dependent premises are added before dependent ones.

The apply tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.

def Lean.Parser.Tactic.exact : Lean.ParserDescr

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

def Lean.Parser.Tactic.refine : Lean.ParserDescr

refine e behaves like exact e, except that named (?x) or unnamed (?_) holes in e that are not solved by unification with the main goal's target type are converted into new goals, using the hole's name, if any, as the goal case name.

def Lean.Parser.Tactic.refine' : Lean.ParserDescr

refine' e behaves like refine e, except that unsolved placeholders (_) and implicit parameters are also converted into new goals.

def Lean.Parser.Tactic.constructor : Lean.ParserDescr

If the main goal's target type is an inductive type, constructor solves it with the first matching constructor, or else fails.

def Lean.Parser.Tactic.case : Lean.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.case' : Lean.ParserDescr

case' is similar to the case tag => tac tactic, but does not ensure the goal has been solved after applying tac, nor admits the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

def Lean.Parser.Tactic.«tacticNext_=>_» : Lean.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.allGoals : Lean.ParserDescr

all_goals tac runs tac on each goal, concatenating the resulting goals, if any.

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

any_goals tac applies the tactic tac to every goal, and succeeds if at least one application succeeds.

def Lean.Parser.Tactic.focus : Lean.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.skip : Lean.ParserDescr

skip does nothing.

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

done succeeds iff there are no remaining goals.

def Lean.Parser.Tactic.traceState : Lean.ParserDescr

trace_state displays the current state in the info view.

def Lean.Parser.Tactic.traceMessage : Lean.ParserDescr

trace msg displays msg in the info view.

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

fail_if_success t fails if the tactic t succeeds.

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

(tacs) executes a list of tactics in sequence, without requiring that the goal be closed at the end like · tacs. Like by itself, the tactics can be either separated by newlines or ;.

def Lean.Parser.Tactic.withReducible : Lean.ParserDescr

with_reducible tacs excutes tacs using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

def Lean.Parser.Tactic.withReducibleAndInstances : Lean.ParserDescr

with_reducible_and_instances tacs excutes tacs using the .instances transparency setting. In this setting only definitions tagged as [reducible] or type class instances are unfolded.

def Lean.Parser.Tactic.withUnfoldingAll : Lean.ParserDescr

with_unfolding_all tacs excutes tacs using the .all transparency setting. In this setting all definitions that are not opaque are unfolded.

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

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

def Lean.Parser.Tactic.rotateLeft : Lean.ParserDescr

rotate_left n rotates goals to the left by n. That is, rotate_left 1 takes the main goal and puts it to the back of the subgoal list. If n is omitted, it defaults to 1.

def Lean.Parser.Tactic.rotateRight : Lean.ParserDescr

Rotate the goals to the right by n. That is, take the goal at the back and push it to the front n times. If n is omitted, it defaults to 1.

def Lean.Parser.Tactic.tacticTry_ : Lean.ParserDescr

try tac runs tac and succeeds even if tac failed.

def Lean.Parser.Tactic.«tactic_<;>_» : Lean.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.refl : Lean.ParserDescr

eq_refl is equivalent to exact rfl, but has a few optimizations.

def Lean.Parser.Tactic.tacticRfl : Lean.ParserDescr

rfl tries to close the current goal using reflexivity. This is supposed to be an extensible tactic and users can add their own support for new reflexive relations.

def Lean.Parser.Tactic.tacticRfl' : Lean.ParserDescr

rfl' is similar to rfl, but disables smart unfolding and unfolds all kinds of definitions, theorems included (relevant for declarations defined by well-founded recursion).

def Lean.Parser.Tactic.acRfl : Lean.ParserDescr

ac_rfl proves equalities up to application of an associative and commutative operator.

instance : IsAssociative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : IsCommutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩

example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl

def Lean.Parser.Tactic.tacticSorry : Lean.ParserDescr

The sorry tactic closes the goal using sorryAx. This is intended for stubbing out incomplete parts of a proof while still having a syntactically correct proof skeleton. Lean will give a warning whenever a proof uses sorry, so you aren't likely to miss it, but you can double check if a theorem depends on sorry by using #print axioms my_thm and looking for sorryAx in the axiom list.

def Lean.Parser.Tactic.tacticAdmit : Lean.ParserDescr

admit is a shorthand for exact sorry.

def Lean.Parser.Tactic.tacticInfer_instance : Lean.ParserDescr

infer_instance is an abbreviation for exact inferInstance. It synthesizes a value of any target type by typeclass inference.

def Lean.Parser.Tactic.config : Lean.ParserDescr

Optional configuration option for tactics

def Lean.Parser.Tactic.locationWildcard : Lean.ParserDescr

The * location refers to all hypotheses and the goal.

def Lean.Parser.Tactic.locationHyp : Lean.ParserDescr

A hypothesis location specification consists of 1 or more hypothesis references and optionally ⊢ denoting the goal.

def Lean.Parser.Tactic.location : Lean.ParserDescr

Location specifications are used by many tactics that can operate on either the hypotheses or the goal. It can have one of the forms:

• 'empty' is not actually present in this syntax, but most tactics use (location)? matchers. It means to target the goal only.
• at h₁ ... hₙ: target the hypotheses h₁, ..., hₙ
• at h₁ h₂ ⊢: target the hypotheses h₁ and h₂, and the goal
• at *: target all hypotheses and the goal

def Lean.Parser.Tactic.change : Lean.ParserDescr

• change tgt' will change the goal from tgt to tgt', assuming these are definitionally equal.
• change t' at h will change hypothesis h : t to have type t', assuming assuming t and t' are definitionally equal.

def Lean.Parser.Tactic.changeWith : Lean.ParserDescr

• change a with b will change occurrences of a to b in the goal, assuming a and b are are definitionally equal.
• change a with b at h similarly changes a to b in the type of hypothesis h.

def Lean.Parser.Tactic.rwRule : Lean.ParserDescr

If thm is a theorem a = b, then as a rewrite rule,

• thm means to replace a with b, and
• ← thm means to replace b with a.

def Lean.Parser.Tactic.rwRuleSeq : Lean.ParserDescr

A rwRuleSeq is a list of rwRule in brackets.

def Lean.Parser.Tactic.rewriteSeq : Lean.ParserDescr

rewrite [e] applies identity e as a rewrite rule to the target of the main goal. If e is preceded by left arrow (← or <-), the rewrite is applied in the reverse direction. If e is a defined constant, then the equational theorems associated with e are used. This provides a convenient way to unfold e.

• rewrite [e₁, ..., eₙ] applies the given rules sequentially.
• rewrite [e] at l rewrites e at location(s) l, where l is either * or a list of hypotheses in the local context. In the latter case, a turnstile ⊢ or |- can also be used, to signify the target of the goal.

def Lean.Parser.Tactic.rwSeq : Lean.ParserDescr

rw is like rewrite, but also tries to close the goal by "cheap" (reducible) rfl afterwards.

def Lean.Parser.Tactic.injection : Lean.ParserDescr

The injection tactic is based on the fact that constructors of inductive data types are injections. That means that if c is a constructor of an inductive datatype, and if (c t₁) and (c t₂) are two terms that are equal then t₁ and t₂ are equal too. If q is a proof of a statement of conclusion t₁ = t₂, then injection applies injectivity to derive the equality of all arguments of t₁ and t₂ placed in the same positions. For example, from (a::b) = (c::d) we derive a=c and b=d. To use this tactic t₁ and t₂ should be constructor applications of the same constructor. Given h : a::b = c::d, the tactic injection h adds two new hypothesis with types a = c and b = d to the main goal. The tactic injection h with h₁ h₂ uses the names h₁ and h₂ to name the new hypotheses.

def Lean.Parser.Tactic.injections : Lean.ParserDescr

injections applies injection to all hypotheses recursively (since injection can produce new hypotheses). Useful for destructing nested constructor equalities like (a::b::c) = (d::e::f).

def Lean.Parser.Tactic.discharger : Lean.ParserDescr

The discharger clause of simp and related tactics. This is a tactic used to discharge the side conditions on conditional rewrite rules.

def Lean.Parser.Tactic.simpPre : Lean.ParserDescr

Use this rewrite rule before entering the subterms

def Lean.Parser.Tactic.simpPost : Lean.ParserDescr

Use this rewrite rule after entering the subterms

def Lean.Parser.Tactic.simpLemma : Lean.ParserDescr

A simp lemma specification is:

• optional ↑ or ↓ to specify use before or after entering the subterm
• optional ← to use the lemma backward
• thm for the theorem to rewrite with

def Lean.Parser.Tactic.simpErase : Lean.ParserDescr

An erasure specification -thm says to remove thm from the simp set

def Lean.Parser.Tactic.simpStar : Lean.ParserDescr

The simp lemma specification * means to rewrite with all hypotheses

def Lean.Parser.Tactic.simp : Lean.ParserDescr

The simp tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses. It has many variants:

• simp simplifies the main goal target using lemmas tagged with the attribute [simp].
• simp [h₁, h₂, ..., hₙ] simplifies the main goal target using the lemmas tagged with the attribute [simp] and the given hᵢ's, where the hᵢ's are expressions. If an hᵢ is a defined constant f, then the equational lemmas associated with f are used. This provides a convenient way to unfold f.
• simp [*] simplifies the main goal target using the lemmas tagged with the attribute [simp] and all hypotheses.
• simp only [h₁, h₂, ..., hₙ] is like simp [h₁, h₂, ..., hₙ] but does not use [simp] lemmas.
• simp [-id₁, ..., -idₙ] simplifies the main goal target using the lemmas tagged with the attribute [simp], but removes the ones named idᵢ.
• simp at h₁ h₂ ... hₙ simplifies the hypotheses h₁ : T₁ ... hₙ : Tₙ. If the target or another hypothesis depends on hᵢ, a new simplified hypothesis hᵢ is introduced, but the old one remains in the local context.
• simp at * simplifies all the hypotheses and the target.
• simp [*] at * simplifies target and all (propositional) hypotheses using the other hypotheses.

def Lean.Parser.Tactic.simpAll : Lean.ParserDescr

simp_all is a stronger version of simp [*] at * where the hypotheses and target are simplified multiple times until no simplication is applicable. Only non-dependent propositional hypotheses are considered.

def Lean.Parser.Tactic.dsimp : Lean.ParserDescr

The dsimp tactic is the definitional simplifier. It is similar to simp but only applies theorems that hold by reflexivity. Thus, the result is guaranteed to be definitionally equal to the input.

def Lean.Parser.Tactic.delta : Lean.ParserDescr

delta id1 id2 ... delta-expands the definitions id1, id2, .... This is a low-level tactic, it will expose how recursive definitions have been compiled by Lean.

def Lean.Parser.Tactic.unfold : Lean.ParserDescr

• unfold id unfolds definition id.
• unfold id1 id2 ... is equivalent to unfold id1; unfold id2; ....

For non-recursive definitions, this tactic is identical to delta. For definitions by pattern matching, it uses "equation lemmas" which are autogenerated for each match arm.

def Lean.Parser.Tactic.tacticRefine_lift_ : Lean.ParserDescr

Auxiliary macro for lifting have/suffices/let/... It makes sure the "continuation" ?_ is the main goal after refining.

def Lean.Parser.Tactic.tacticHave_ : Lean.ParserDescr

have h : t := e adds the hypothesis h : t to the current goal if e a term of type t.

• If t is omitted, it will be inferred.
• If h is omitted, the name this is used.
• The variant have pattern := e is equivalent to match e with | pattern => _, and it is convenient for types that have only one applicable constructor. For example, given h : p ∧ q ∧ r, have ⟨h₁, h₂, h₃⟩ := h produces the hypotheses h₁ : p, h₂ : q, and h₃ : r.

def Lean.Parser.Tactic.tacticSuffices_ : Lean.ParserDescr

Given a main goal ctx ⊢ t, suffices h : t' from e replaces the main goal with ctx ⊢ t', e must have type t in the context ctx, h : t'.

The variant suffices h : t' by tac is a shorthand for suffices h : t' from by tac. If h : is omitted, the name this is used.

def Lean.Parser.Tactic.tacticLet_ : Lean.ParserDescr

let h : t := e adds the hypothesis h : t := e to the current goal if e a term of type t. If t is omitted, it will be inferred. The variant let pattern := e is equivalent to match e with | pattern => _, and it is convenient for types that have only applicable constructor. Example: given h : p ∧ q ∧ r, let ⟨h₁, h₂, h₃⟩ := h produces the hypotheses h₁ : p, h₂ : q, and h₃ : r.

def Lean.Parser.Tactic.tacticShow_ : Lean.ParserDescr

show t finds the first goal whose target unifies with t. It makes that the main goal, performs the unification, and replaces the target with the unified version of t.

def Lean.Parser.Tactic.letrec : Lean.ParserDescr

let rec f : t := e adds a recursive definition f to the current goal. The syntax is the same as term-mode let rec.

def Lean.Parser.Tactic.tacticRefine_lift'_ : Lean.ParserDescr

Similar to refine_lift, but using refine'

def Lean.Parser.Tactic.tacticHave'_ : Lean.ParserDescr

Similar to have, but using refine'

def Lean.Parser.Tactic.«tacticHave'_:=_» : Lean.ParserDescr

Similar to have, but using refine'

def Lean.Parser.Tactic.tacticLet'_ : Lean.ParserDescr

Similar to let, but using refine'

def Lean.Parser.Tactic.inductionAltLHS : Lean.ParserDescr

The left hand side of an induction arm, | foo a b c or | @foo a b c where foo is a constructor of the inductive type and a b c are the arguments to the contstructor.

def Lean.Parser.Tactic.inductionAlt : Lean.ParserDescr

In induction alternative, which can have 1 or more cases on the left and _, ?_, or a tactic sequence after the =>.

def Lean.Parser.Tactic.inductionAlts : Lean.ParserDescr

After with, there is an optional tactic that runs on all branches, and then a list of alternatives.

def Lean.Parser.Tactic.induction : Lean.ParserDescr

Assuming x is a variable in the local context with an inductive type, induction x applies induction on x to the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor and an inductive hypothesis is added for each recursive argument to the constructor. If the type of an element in the local context depends on x, that element is reverted and reintroduced afterward, so that the inductive hypothesis incorporates that hypothesis as well.

For example, given n : Nat and a goal with a hypothesis h : P n and target Q n, induction n produces one goal with hypothesis h : P 0 and target Q 0, and one goal with hypotheses h : P (Nat.succ a) and ih₁ : P a → Q a and target Q (Nat.succ a). Here the names a and ih₁ are chosen automatically and are not accessible. You can use with to provide the variables names for each constructor.

• induction e, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable.
• induction e using r allows the user to specify the principle of induction that should be used. Here r should be a theorem whose result type must be of the form C t, where C is a bound variable and t is a (possibly empty) sequence of bound variables
• induction e generalizing z₁ ... zₙ, where z₁ ... zₙ are variables in the local context, generalizes over z₁ ... zₙ before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized.
• Given x : Nat, induction x with | zero => tac₁ | succ x' ih => tac₂ uses tactic tac₁ for the zero case, and tac₂ for the succ case.

def Lean.Parser.Tactic.generalizeArg : Lean.ParserDescr

A generalize argument, of the form term = x or h : term = x.

def Lean.Parser.Tactic.generalize : Lean.ParserDescr

• generalize ([h :] e = x),+ replaces all occurrences es in the main goal with a fresh hypothesis xs. If h is given, h : e = x is introduced as well.
• generalize e = x at h₁ ... hₙ also generalizes occurrences of e inside h₁, ..., hₙ.
• generalize e = x at * will generalize occurrences of e everywhere.

def Lean.Parser.Tactic.casesTarget : Lean.ParserDescr

A cases argument, of the form e or h : e (where h asserts that e = cᵢ a b for each constructor cᵢ of the inductive).

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

Assuming x is a variable in the local context with an inductive type, cases x splits the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor. If the type of an element in the local context depends on x, that element is reverted and reintroduced afterward, so that the case split affects that hypothesis as well. cases detects unreachable cases and closes them automatically.

For example, given n : Nat and a goal with a hypothesis h : P n and target Q n, cases n produces one goal with hypothesis h : P 0 and target Q 0, and one goal with hypothesis h : P (Nat.succ a) and target Q (Nat.succ a). Here the name a is chosen automatically and is not accessible. You can use with to provide the variables names for each constructor.

• cases e, where e is an expression instead of a variable, generalizes e in the goal, and then cases on the resulting variable.
• Given as : List α, cases as with | nil => tac₁ | cons a as' => tac₂, uses tactic tac₁ for the nil case, and tac₂ for the cons case, and a and as' are used as names for the new variables introduced.
• cases h : e, where e is a variable or an expression, performs cases on e as above, but also adds a hypothesis h : e = ... to each hypothesis, where ... is the constructor instance for that particular case.

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

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

def Lean.Parser.Tactic.tacticRepeat_ : Lean.ParserDescr

repeat tac repeatedly applies tac to the main goal until it fails. That is, if tac produces multiple subgoals, only subgoals up to the first failure will be visited. The Std library provides repeat' which repeats separately in each subgoal.

def Lean.Parser.Tactic.tacticTrivial : Lean.ParserDescr

trivial tries different simple tactics (e.g., rfl, contradiction, ...) to close the current goal. You can use the command macro_rules to extend the set of tactics used. Example:

macro_rules | `(tactic| trivial) => `(tactic| simp)

def Lean.Parser.Tactic.split : Lean.ParserDescr

The split tactic is useful for breaking nested if-then-else and match expressions into separate cases. For a match expression with n cases, the split tactic generates at most n subgoals.

For example, given n : Nat, and a target if n = 0 then Q else R, split will generate one goal with hypothesis n = 0 and target Q, and a second goal with hypothesis ¬n = 0 and target R. Note that the introduced hypothesis is unnamed, and is commonly renamed used the case or next tactics.

• split will split the goal (target).
• split at h will split the hypothesis h.

def Lean.Parser.Tactic.dbgTrace : Lean.ParserDescr

dbg_trace "foo" prints foo when elaborated. Useful for debugging tactic control flow:

example : False ∨ True := by
  first
  | apply Or.inl; trivial; dbg_trace "left"
  | apply Or.inr; trivial; dbg_trace "right"

def Lean.Parser.Tactic.tacticStop_ : Lean.ParserDescr

stop is a helper tactic for "discarding" the rest of a proof: it is defined as repeat sorry. It is useful when working on the middle of a complex proofs, and less messy than commenting the remainder of the proof.

def Lean.Parser.Tactic.specialize : Lean.ParserDescr

The tactic specialize h a₁ ... aₙ works on local hypothesis h. The premises of this hypothesis, either universal quantifications or non-dependent implications, are instantiated by concrete terms coming from arguments a₁ ... aₙ. The tactic adds a new hypothesis with the same name h := h a₁ ... aₙ and tries to clear the previous one.

def Lean.Parser.Tactic.tacticUnhygienic_ : Lean.ParserDescr

unhygienic tacs runs tacs with name hygiene disabled. This means that tactics that would normally create inaccessible names will instead make regular variables. Warning: Tactics may change their variable naming strategies at any time, so code that depends on autogenerated names is brittle. Users should try not to use unhygienic if possible.

example : ∀ x : Nat, x = x := by unhygienic
  intro            -- x would normally be intro'd as inaccessible
  exact Eq.refl x  -- refer to x

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

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

def Lean.Parser.Tactic.checkpoint : Lean.ParserDescr

checkpoint tac acts the same as tac, but it caches the input and output of tac, and if the file is re-elaborated and the input matches, the tactic is not re-run and its effects are reapplied to the state. This is useful for improving responsiveness when working on a long tactic proof, by wrapping expensive tactics with checkpoint.

See the save tactic, which may be more convenient to use.

(TODO: do this automatically and transparently so that users don't have to use this combinator explicitly.)

def Lean.Parser.Tactic.save : Lean.ParserDescr

save is defined to be the same as skip, but the elaborator has special handling for occurrences of save in tactic scripts and will transform by tac1; save; tac2 to by (checkpoint tac1); tac2, meaning that the effect of tac1 will be cached and replayed. This is useful for improving responsiveness when working on a long tactic proof, by using save after expensive tactics.

(TODO: do this automatically and transparently so that users don't have to use this combinator explicitly.)

def Lean.Parser.Tactic.sleep : Lean.ParserDescr

The tactic sleep ms sleeps for ms milliseconds and does nothing. It is used for debugging purposes only.

def Lean.Parser.Tactic.«tacticExists_,,» : Lean.ParserDescr

exists e₁, e₂, ... is shorthand for refine ⟨e₁, e₂, ...⟩; try trivial. It is useful for existential goals.

def Lean.Parser.Tactic.congr : Lean.ParserDescr

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ HEq (f as) (f bs). The optional parameter is the depth of the recursive applications. This is useful when congr is too aggressive in breaking down the goal. For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr produces the goals ⊢ x = y and ⊢ y = x, while congr 2 produces the intended ⊢ x + y = y + x.

def Lean.Parser.Attr.simp : Lean.ParserDescr

Theorems tagged with the simp attribute are by the simplifier (i.e., the simp tactic, and its variants) to simplify expressions occurring in your goals. We call theorems tagged with the simp attribute "simp theorems" or "simp lemmas". Lean maintains a database/index containing all active simp theorems. Here is an example of a simp theorem.

@[simp] theorem ne_eq (a b : α) : (a ≠ b) = Not (a = b) := rfl

This simp theorem instructs the simplifier to replace instances of the term a ≠ b (e.g. x + 0 ≠ y) with Not (a = b) (e.g., Not (x + 0 = y)). The simplifier applies simp theorems in one direction only: if A = B is a simp theorem, then simp replaces As with Bs, but it doesn't replace Bs with As. Hence a simp theorem should have the property that its right-hand side is "simpler" than its left-hand side. In particular, = and ↔ should not be viewed as symmetric operators in this situation. The following would be a terrible simp theorem (if it were even allowed):

@[simp] lemma mul_right_inv_bad (a : G) : 1 = a * a⁻¹ := ...

Replacing 1 with a * a⁻¹ is not a sensible default direction to travel. Even worse would be a theorem that causes expressions to grow without bound, causing simp to loop forever.

By default the simplifier applies simp theorems to an expression e after its sub-expressions have been simplified. We say it performs a bottom-up simplification. You can instruct the simplifier to apply a theorem before its sub-expressions have been simplified by using the modifier ↓. Here is an example

@[simp↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ∨ ¬q) :=

When multiple simp theorems are applicable, the simplifier uses the one with highest priority. If there are several with the same priority, it is uses the "most recent one". Example:

@[simp high] theorem cond_true (a b : α) : cond true a b = a := rfl
@[simp low+1] theorem or_true (p : Prop) : (p ∨ True) = True :=
  propext <| Iff.intro (fun _ => trivial) (fun _ => Or.inr trivial)
@[simp 100] theorem ite_self {d : Decidable c} (a : α) : ite c a a = a := by
  cases d <;> rfl

def «term‹_›» : Lean.ParserDescr

‹t› resolves to an (arbitrary) hypothesis of type t. It is useful for referring to hypotheses without accessible names. t may contain holes that are solved by unification with the expected type; in particular, ‹_› is a shortcut for by assumption.

def tacticGet_elem_tactic_trivial : Lean.ParserDescr

get_elem_tactic_trivial is an extensible tactic automatically called by the notation arr[i] to prove any side conditions that arise when constructing the term (e.g. the index is in bounds of the array). The default behavior is to just try trivial (which handles the case where i < arr.size is in the context) and simp_arith (for doing linear arithmetic in the index).

def tacticGet_elem_tactic : Lean.ParserDescr

get_elem_tactic is the tactic automatically called by the notation arr[i] to prove any side conditions that arise when constructing the term (e.g. the index is in bounds of the array). It just delegates to get_elem_tactic_trivial and gives a diagnostic error message otherwise; users are encouraged to extend get_elem_tactic_trivial instead of this tactic.

def «term__[_]» : Lean.TrailingParserDescr

The syntax arr[i] gets the i'th element of the collection arr. If there are proof side conditions to the application, they will be automatically inferred by the get_elem_tactic tactic.

The actual behavior of this class is type-dependent, but here are some important implementations:

• arr[i] : α where arr : Array α and i : Nat or i : USize: does array indexing with no bounds check and a proof side goal i < arr.size.
• l[i] : α where l : List α and i : Nat: index into a list, with proof side goal i < l.length.
• stx[i] : Syntax where stx : Syntax and i : Nat: get a syntax argument, no side goal (returns .missing out of range)

There are other variations on this syntax:

• arr[i]: proves the proof side goal by get_elem_tactic
• arr[i]!: panics if the side goal is false
• arr[i]?: returns none if the side goal is false
• arr[i]'h: uses h to prove the side goal

def «term__[_]'_» : Lean.TrailingParserDescr

The syntax arr[i] gets the i'th element of the collection arr. If there are proof side conditions to the application, they will be automatically inferred by the get_elem_tactic tactic.

The actual behavior of this class is type-dependent, but here are some important implementations:

• arr[i] : α where arr : Array α and i : Nat or i : USize: does array indexing with no bounds check and a proof side goal i < arr.size.
• l[i] : α where l : List α and i : Nat: index into a list, with proof side goal i < l.length.
• stx[i] : Syntax where stx : Syntax and i : Nat: get a syntax argument, no side goal (returns .missing out of range)

There are other variations on this syntax:

• arr[i]: proves the proof side goal by get_elem_tactic
• arr[i]!: panics if the side goal is false
• arr[i]?: returns none if the side goal is false
• arr[i]'h: uses h to prove the side goal