Documentation

Init.Tactics

Equations

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

Equations

Introduce 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.
  • introxy 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
    | ...
    
Equations

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

Equations

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

Equations

revertx... is the inverse of introx...: it moves the given hypotheses into the main goal's target type.

Equations

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

Equations

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

Equations

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

Equations

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

Equations

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
Equations

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

Equations

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

Equations

refinee behaves like exacte, 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.

Equations

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

Equations

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

Equations

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

Equations

case' is similar to the casetag=>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.

Equations

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

Equations

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

Equations

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

Equations

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

Equations

done succeeds iff there are no remaining goals.

Equations

trace_state displays the current state in the info view.

Equations

tracemsg displays msg in the info view.

Equations

fail_if_successt fails if the tactic t succeeds.

Equations

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

Equations

trytac runs tac and succeeds even if tac failed.

Equations

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

Equations

eq_refl is equivalent to exactrfl, but has a few optimizations.

Equations

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.

Equations

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

Equations

admit is a shorthand for exactsorry.

Equations

The sorry tactic is a shorthand for exactsorry.

Equations

infer_instance is an abbreviation for exactinferInstance

Equations

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]atl 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.
Equations
Equations

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 (ct₁) and (ct₂) 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 injectionh adds two new hypothesis with types a=c and b=d to the main goal. The tactic injectionhwithh₁h₂ uses the names h₁ and h₂ to name the new hypotheses.

Equations

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.
  • simponly[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ᵢ.
  • simpath₁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.
  • simpat* simplifies all the hypotheses and the target.
  • simp[*]at* simplifies target and all (propositional) hypotheses using the other hypotheses.
Equations

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.

Equations

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

Equations

unfoldid,+ unfolds definition id. For non-recursive definitions, this tactic is identical to delta. For recursive definitions, it hides the encoding tricks used by the Lean frontend to convince the kernel that the definition terminates.

Equations

haveh: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 havepattern:=e is equivalent to matchewith|pattern=>_, and it is convenient for types that have only applicable constructor. Example: given h:pqr, have⟨h₁,h₂,h₃⟩:=h produces the hypotheses h₁:p, h₂:q, and h₃:r.

Equations

Given a main goal ctx|-t, sufficesh:t'frome replaces the main goal with ctx|-t', e must have type t in the context ctx,h:t'.

The variant sufficesh:t'bytac is a shorthand for sufficesh:t'frombytac. If h: is omitted, the name this is used.

Equations

leth: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 letpattern:=e is equivalent to matchewith|pattern=>_, and it is convenient for types that have only applicable constructor. Example: given h:pqr, let⟨h₁,h₂,h₃⟩:=h produces the hypotheses h₁:p, h₂:q, and h₃:r.

Equations

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

Equations

Assuming x is a variable in the local context with an inductive type, inductionx 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:Pn and target Qn, inductionn produces one goal with hypothesis h:P0 and target Q0, and one goal with hypotheses h:P(Nat.succa) and ih₁:Pa→Qa and target Q(Nat.succa). 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.

  • inductione, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable.
  • inductioneusingr 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 Ct, where C is a bound variable and t is a (possibly empty) sequence of bound variables
  • inductionegeneralizingz₁...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, inductionxwith|zero=>tac₁|succx'ih=>tac₂ uses tactic tac₁ for the zero case, and tac₂ for the succ case.
Equations

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.

Equations

Assuming x is a variable in the local context with an inductive type, casesx 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:Pn and target Qn, casesn produces one goal with hypothesis h:P0 and target Q0, and one goal with hypothesis h:P(Nat.succa) and target Q(Nat.succa). Here the name a is chosen automatically and are not accessible. You can use with to provide the variables names for each constructor.

  • casese, where e is an expression instead of a variable, generalizes e in the goal, and then cases on the resulting variable.
  • Given as:Listα, casesaswith|nil=>tac₁|consaas'=>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.
  • casesh: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.
Equations

rename_ix_1...x_n renames the last n inaccessible names using the given names.

Equations

repeattac applies tac to main goal. If the application succeeds, the tactic is applied recursively to the generated subgoals until it eventually fails.

Equations

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)
Equations

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

Equations

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

Equations

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

Equations

failmsg is a tactic that always fail and produces an error using the given message.

Equations

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

Equations

existse₁,e₂,... is shorthand for refine⟨e₁,e₂,...⟩;trytrivial. It is useful for existential goals.

Equations

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