Equations
- Lean.Parser.Tactic.withAnnotateState = Lean.ParserDescr.node `Lean.Parser.Tactic.withAnnotateState 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "with_annotate_state " false) (Lean.ParserDescr.cat `rawStx 0)) (Lean.ParserDescr.const `ppSpace)) (Lean.ParserDescr.cat `tactic 0))
with_annotate_statestxt
annotates the lexical range of stx:Syntax
with the initial and final state of running tactic t
.
Equations
- Lean.Parser.Tactic.intro = Lean.ParserDescr.node `Lean.Parser.Tactic.intro 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "intro " false) (Lean.ParserDescr.unary `notFollowedBy (Lean.ParserDescr.symbol "|"))) (Lean.ParserDescr.unary `many (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.cat `term 1024))))
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 likefun
:intro | n + 1, 0 => tac | ...
Equations
- Lean.Parser.Tactic.intros = Lean.ParserDescr.node `Lean.Parser.Tactic.intros 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "intros " false) (Lean.ParserDescr.unary `many (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol "_")))))
introsx...
behaves like introx...
, but then keeps introducing (anonymous) hypotheses until goal is not of a function type.
Equations
- Lean.Parser.Tactic.rename = Lean.ParserDescr.node `Lean.Parser.Tactic.rename 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rename " false) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " => ")) (Lean.ParserDescr.const `ident))
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
- Lean.Parser.Tactic.revert = Lean.ParserDescr.node `Lean.Parser.Tactic.revert 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "revert " false) (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.cat `term 1024))))
revertx...
is the inverse of introx...
: it moves the given hypotheses into the main goal's target type.
Equations
- Lean.Parser.Tactic.clear = Lean.ParserDescr.node `Lean.Parser.Tactic.clear 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "clear " false) (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.cat `term 1024))))
clearx...
removes the given hypotheses, or fails if there are remaining references to a hypothesis.
Equations
- Lean.Parser.Tactic.subst = Lean.ParserDescr.node `Lean.Parser.Tactic.subst 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "subst " false) (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.cat `term 1024))))
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
- Lean.Parser.Tactic.substVars = Lean.ParserDescr.node `Lean.Parser.Tactic.substVars 1024 (Lean.ParserDescr.nonReservedSymbol "subst_vars" false)
Equations
- Lean.Parser.Tactic.assumption = Lean.ParserDescr.node `Lean.Parser.Tactic.assumption 1024 (Lean.ParserDescr.nonReservedSymbol "assumption" false)
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
- Lean.Parser.Tactic.contradiction = Lean.ParserDescr.node `Lean.Parser.Tactic.contradiction 1024 (Lean.ParserDescr.nonReservedSymbol "contradiction" false)
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
- Lean.Parser.Tactic.apply = Lean.ParserDescr.node `Lean.Parser.Tactic.apply 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "apply " false) (Lean.ParserDescr.cat `term 0))
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
- Lean.Parser.Tactic.exact = Lean.ParserDescr.node `Lean.Parser.Tactic.exact 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "exact " false) (Lean.ParserDescr.cat `term 0))
exacte
closes the main goal if its target type matches that of e
.
Equations
- Lean.Parser.Tactic.refine = Lean.ParserDescr.node `Lean.Parser.Tactic.refine 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "refine " false) (Lean.ParserDescr.cat `term 0))
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
- Lean.Parser.Tactic.refine' = Lean.ParserDescr.node `Lean.Parser.Tactic.refine' 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "refine' " false) (Lean.ParserDescr.cat `term 0))
refine'e
behaves like refinee
, except that unsolved placeholders (_
) and implicit parameters are also converted into new goals.
Equations
- Lean.Parser.Tactic.constructor = Lean.ParserDescr.node `Lean.Parser.Tactic.constructor 1024 (Lean.ParserDescr.nonReservedSymbol "constructor" false)
If the main goal's target type is an inductive type, constructor
solves it with the first matching constructor, or else fails.
Equations
- Lean.Parser.Tactic.case = Lean.ParserDescr.node `Lean.Parser.Tactic.case 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "case " false) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol "_"))) (Lean.ParserDescr.unary `many (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol "_")))) (Lean.ParserDescr.symbol " => ")) (Lean.ParserDescr.const `tacticSeq))
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
- Lean.Parser.Tactic.case' = Lean.ParserDescr.node `Lean.Parser.Tactic.case' 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "case' " false) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol "_"))) (Lean.ParserDescr.unary `many (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol "_")))) (Lean.ParserDescr.symbol " => ")) (Lean.ParserDescr.const `tacticSeq))
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
- Lean.Parser.Tactic.«tacticNext___=>_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«tacticNext___=>_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "next " false) (Lean.ParserDescr.unary `many (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol "_")))) (Lean.ParserDescr.symbol " => ")) (Lean.ParserDescr.const `tacticSeq))
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
- Lean.Parser.Tactic.allGoals = Lean.ParserDescr.node `Lean.Parser.Tactic.allGoals 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "all_goals " false) (Lean.ParserDescr.const `tacticSeq))
all_goalstac
runs tac
on each goal, concatenating the resulting goals, if any.
Equations
- Lean.Parser.Tactic.anyGoals = Lean.ParserDescr.node `Lean.Parser.Tactic.anyGoals 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "any_goals " false) (Lean.ParserDescr.const `tacticSeq))
any_goalstac
applies the tactic tac
to every goal, and succeeds if at least one application succeeds.
Equations
- Lean.Parser.Tactic.focus = Lean.ParserDescr.node `Lean.Parser.Tactic.focus 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "focus " false) (Lean.ParserDescr.const `tacticSeq))
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
- Lean.Parser.Tactic.skip = Lean.ParserDescr.node `Lean.Parser.Tactic.skip 1024 (Lean.ParserDescr.nonReservedSymbol "skip" false)
skip
does nothing.
Equations
- Lean.Parser.Tactic.done = Lean.ParserDescr.node `Lean.Parser.Tactic.done 1024 (Lean.ParserDescr.nonReservedSymbol "done" false)
done
succeeds iff there are no remaining goals.
Equations
- Lean.Parser.Tactic.traceState = Lean.ParserDescr.node `Lean.Parser.Tactic.traceState 1024 (Lean.ParserDescr.nonReservedSymbol "trace_state" false)
trace_state
displays the current state in the info view.
Equations
- Lean.Parser.Tactic.traceMessage = Lean.ParserDescr.node `Lean.Parser.Tactic.traceMessage 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "trace " false) (Lean.ParserDescr.const `str))
tracemsg
displays msg
in the info view.
Equations
- Lean.Parser.Tactic.failIfSuccess = Lean.ParserDescr.node `Lean.Parser.Tactic.failIfSuccess 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "fail_if_success " false) (Lean.ParserDescr.const `tacticSeq))
Equations
- Lean.Parser.Tactic.paren = Lean.ParserDescr.node `Lean.Parser.Tactic.paren 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "(" false) (Lean.ParserDescr.const `tacticSeq)) (Lean.ParserDescr.symbol ")"))
Equations
- Lean.Parser.Tactic.withReducible = Lean.ParserDescr.node `Lean.Parser.Tactic.withReducible 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "with_reducible " false) (Lean.ParserDescr.const `tacticSeq))
Equations
- Lean.Parser.Tactic.withReducibleAndInstances = Lean.ParserDescr.node `Lean.Parser.Tactic.withReducibleAndInstances 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "with_reducible_and_instances " false) (Lean.ParserDescr.const `tacticSeq))
Equations
- Lean.Parser.Tactic.withUnfoldingAll = Lean.ParserDescr.node `Lean.Parser.Tactic.withUnfoldingAll 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "with_unfolding_all " false) (Lean.ParserDescr.const `tacticSeq))
Equations
- Lean.Parser.Tactic.first = Lean.ParserDescr.node `Lean.Parser.Tactic.first 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "first " false) (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGe) (Lean.ParserDescr.symbol "|")) (Lean.ParserDescr.const `tacticSeq))))))
first|tac|...
runs each tac
until one succeeds, or else fails.
Equations
- Lean.Parser.Tactic.rotateLeft = Lean.ParserDescr.node `Lean.Parser.Tactic.rotateLeft 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rotate_left" false) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.const `num)))
Equations
- Lean.Parser.Tactic.rotateRight = Lean.ParserDescr.node `Lean.Parser.Tactic.rotateRight 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rotate_right" false) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.const `num)))
Equations
- Lean.Parser.Tactic.tacticTry_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticTry_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "try " false) (Lean.ParserDescr.const `tacticSeq))
trytac
runs tac
and succeeds even if tac
failed.
Equations
- Lean.Parser.Tactic.«tactic_<;>_» = Lean.ParserDescr.trailingNode `Lean.Parser.Tactic.«tactic_<;>_» 1 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <;> ") (Lean.ParserDescr.cat `tactic 0))
tac<;>tac'
runs tac
on the main goal and tac'
on each produced goal, concatenating all goals produced by tac'
.
Equations
- Lean.Parser.Tactic.refl = Lean.ParserDescr.node `Lean.Parser.Tactic.refl 1024 (Lean.ParserDescr.nonReservedSymbol "eq_refl" false)
eq_refl
is equivalent to exactrfl
, but has a few optimizations.
Equations
- Lean.Parser.Tactic.tacticRfl = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticRfl 1024 (Lean.ParserDescr.nonReservedSymbol "rfl" false)
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
- Lean.Parser.Tactic.tacticRfl' = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticRfl' 1024 (Lean.ParserDescr.nonReservedSymbol "rfl'" false)
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
- Lean.Parser.Tactic.ac_refl = Lean.ParserDescr.node `Lean.Parser.Tactic.ac_refl 1024 (Lean.ParserDescr.nonReservedSymbol "ac_refl " false)
Equations
- Lean.Parser.Tactic.tacticAdmit = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticAdmit 1024 (Lean.ParserDescr.nonReservedSymbol "admit" false)
admit
is a shorthand for exactsorry
.
Equations
- Lean.Parser.Tactic.tacticSorry = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticSorry 1024 (Lean.ParserDescr.nonReservedSymbol "sorry" false)
The sorry
tactic is a shorthand for exactsorry
.
Equations
- Lean.Parser.Tactic.tacticInfer_instance = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticInfer_instance 1024 (Lean.ParserDescr.nonReservedSymbol "infer_instance" false)
infer_instance
is an abbreviation for exactinferInstance
Equations
- Lean.Parser.Tactic.config = Lean.ParserDescr.nodeWithAntiquot "config" `Lean.Parser.Tactic.config (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `atomic (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "(") (Lean.ParserDescr.nonReservedSymbol "config" false))) (Lean.ParserDescr.symbol " := ")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol ")"))
Optional configuration option for tactics
Equations
- Lean.Parser.Tactic.locationWildcard = Lean.ParserDescr.nodeWithAntiquot "locationWildcard" `Lean.Parser.Tactic.locationWildcard (Lean.ParserDescr.symbol "*")
Equations
- Lean.Parser.Tactic.locationHyp = Lean.ParserDescr.nodeWithAntiquot "locationHyp" `Lean.Parser.Tactic.locationHyp (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.cat `term 1024))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.symbol "⊢") (Lean.ParserDescr.symbol "|-"))))
Equations
- Lean.Parser.Tactic.location = Lean.ParserDescr.nodeWithAntiquot "location" `Lean.Parser.Tactic.location (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " at ") (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.locationWildcard Lean.Parser.Tactic.locationHyp)))
Equations
- Lean.Parser.Tactic.change = Lean.ParserDescr.node `Lean.Parser.Tactic.change 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "change " false) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))
Equations
- Lean.Parser.Tactic.changeWith = Lean.ParserDescr.node `Lean.Parser.Tactic.changeWith 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "change " false) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " with ")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))
Equations
- Lean.Parser.Tactic.rwRule = Lean.ParserDescr.nodeWithAntiquot "rwRule" `Lean.Parser.Tactic.rwRule (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.symbol "← ") (Lean.ParserDescr.symbol "<- "))) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.rwRuleSeq = Lean.ParserDescr.nodeWithAntiquot "rwRuleSeq" `Lean.Parser.Tactic.rwRuleSeq (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.sepBy Lean.Parser.Tactic.rwRule "," (Lean.ParserDescr.symbol ", ") true)) (Lean.ParserDescr.symbol "]"))
Equations
- Lean.Parser.Tactic.rewriteSeq = Lean.ParserDescr.node `Lean.Parser.Tactic.rewriteSeq 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rewrite " false) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.config)) Lean.Parser.Tactic.rwRuleSeq) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))
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
.
Equations
- Lean.Parser.Tactic.rwSeq = Lean.ParserDescr.node `Lean.Parser.Tactic.rwSeq 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rw " false) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.config)) Lean.Parser.Tactic.rwRuleSeq) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))
rw
is like rewrite
, but also tries to close the goal by "cheap" (reducible) rfl
afterwards.
Equations
- Lean.Parser.Tactic.rwWithRfl kind atom stx = let seq := Lean.Syntax.getOp stx 2; let rbrak := Lean.Syntax.getOp seq 2; let seq := Lean.Syntax.setArg seq 2 (Lean.mkAtom "]"); let tac := Lean.Syntax.setArg (Lean.Syntax.setArg (Lean.Syntax.setKind stx kind) 0 (Lean.mkAtomFrom stx atom)) 2 seq; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.seq1 #[Lean.Syntax.node Lean.SourceInfo.none `null #[tac, Lean.Syntax.atom info ";", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticTry_ #[Lean.Syntax.atom info "try", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.withReducible #[Lean.Syntax.atom info "with_reducible", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticRfl #[Lean.Syntax.atom (Option.getD (Lean.Syntax.getHeadInfo? rbrak) info) "rfl"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.atom info ")"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]]])
Equations
- Lean.Parser.Tactic.expandRwSeq = Lean.Parser.Tactic.rwWithRfl `Lean.Parser.Tactic.rewriteSeq "rewrite"
Equations
- Lean.Parser.Tactic.injection = Lean.ParserDescr.node `Lean.Parser.Tactic.injection 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "injection " false) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " with ") (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol "_")))))))
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
- Lean.Parser.Tactic.injections = Lean.ParserDescr.node `Lean.Parser.Tactic.injections 1024 (Lean.ParserDescr.nonReservedSymbol "injections" false)
Equations
- Lean.Parser.Tactic.discharger = Lean.ParserDescr.nodeWithAntiquot "discharger" `Lean.Parser.Tactic.discharger (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `atomic (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "(") (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.nonReservedSymbol "discharger" false) (Lean.ParserDescr.nonReservedSymbol "disch" false)))) (Lean.ParserDescr.symbol " := ")) (Lean.ParserDescr.const `tacticSeq)) (Lean.ParserDescr.symbol ")"))
Equations
- Lean.Parser.Tactic.simpPre = Lean.ParserDescr.nodeWithAntiquot "simpPre" `Lean.Parser.Tactic.simpPre (Lean.ParserDescr.symbol "↓")
Equations
- Lean.Parser.Tactic.simpPost = Lean.ParserDescr.nodeWithAntiquot "simpPost" `Lean.Parser.Tactic.simpPost (Lean.ParserDescr.symbol "↑")
Equations
- Lean.Parser.Tactic.simpLemma = Lean.ParserDescr.nodeWithAntiquot "simpLemma" `Lean.Parser.Tactic.simpLemma (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpPre Lean.Parser.Tactic.simpPost)) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.symbol "← ") (Lean.ParserDescr.symbol "<- ")))) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.simpErase = Lean.ParserDescr.nodeWithAntiquot "simpErase" `Lean.Parser.Tactic.simpErase (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "-") (Lean.ParserDescr.cat `term 1024))
Equations
- Lean.Parser.Tactic.simpStar = Lean.ParserDescr.nodeWithAntiquot "simpStar" `Lean.Parser.Tactic.simpStar (Lean.ParserDescr.symbol "*")
Equations
- Lean.Parser.Tactic.simp = Lean.ParserDescr.node `Lean.Parser.Tactic.simp 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "simp " false) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.config)) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.discharger)) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.nonReservedSymbol "only " false))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.sepBy (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpStar (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpErase Lean.Parser.Tactic.simpLemma)) "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.symbol "]")))) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))
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 givenhᵢ
's, where thehᵢ
's are expressions. If anhᵢ
is a defined constantf
, then the equational lemmas associated withf
are used. This provides a convenient way to unfoldf
.simp[*]
simplifies the main goal target using the lemmas tagged with the attribute[simp]
and all hypotheses.simponly[h₁,h₂,...,hₙ]
is likesimp[h₁,h₂,...,hₙ]
but does not use[simp]
lemmassimp[-id₁,...,-idₙ]
simplifies the main goal target using the lemmas tagged with the attribute[simp]
, but removes the ones namedidᵢ
.simpath₁h₂...hₙ
simplifies the hypothesesh₁:T₁
...hₙ:Tₙ
. If the target or another hypothesis depends onhᵢ
, a new simplified hypothesishᵢ
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
- Lean.Parser.Tactic.simpAll = Lean.ParserDescr.node `Lean.Parser.Tactic.simpAll 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "simp_all " false) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.config)) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.discharger)) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.nonReservedSymbol "only " false))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.sepBy (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpErase Lean.Parser.Tactic.simpLemma) "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.symbol "]"))))
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
- Lean.Parser.Tactic.dsimp = Lean.ParserDescr.node `Lean.Parser.Tactic.dsimp 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "dsimp " false) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.config)) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.discharger)) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.nonReservedSymbol "only " false))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.sepBy (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpErase Lean.Parser.Tactic.simpLemma) "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.symbol "]")))) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))
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.
Equations
- Lean.Parser.Tactic.delta = Lean.ParserDescr.node `Lean.Parser.Tactic.delta 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "delta " false) (Lean.ParserDescr.const `ident)) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))
deltaid
delta-expands the definition id
.
This is a low-level tactic, it will expose how recursive definitions have been compiled by Lean.
Equations
- Lean.Parser.Tactic.unfold = Lean.ParserDescr.node `Lean.Parser.Tactic.unfold 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "unfold " false) (Lean.ParserDescr.sepBy1 (Lean.ParserDescr.const `ident) "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))
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
- Lean.Parser.Tactic.tacticRefine_lift_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticRefine_lift_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "refine_lift " false) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.tacticHave_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticHave_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "have " false) (Lean.ParserDescr.const `haveDecl))
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:p∧q∧r
, have⟨h₁,h₂,h₃⟩:=h
produces the hypotheses h₁:p
, h₂:q
, and h₃:r
.
Equations
- Lean.Parser.Tactic.«tacticHave__:=_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«tacticHave__:=_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "have" false) (Lean.ParserDescr.const `ident)) (Lean.ParserDescr.symbol " := ")) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.tacticSuffices_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticSuffices_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "suffices " false) (Lean.ParserDescr.const `sufficesDecl))
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
- Lean.Parser.Tactic.tacticLet_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticLet_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "let " false) (Lean.ParserDescr.const `letDecl))
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:p∧q∧r
, let⟨h₁,h₂,h₃⟩:=h
produces the hypotheses h₁:p
, h₂:q
, and h₃:r
.
Equations
- Lean.Parser.Tactic.tacticShow_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticShow_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "show " false) (Lean.ParserDescr.cat `term 0))
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
- Lean.Parser.Tactic.letrec = Lean.ParserDescr.node `Lean.Parser.Tactic.letrec 1022 (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `atomic (Lean.ParserDescr.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "let ") (Lean.ParserDescr.nonReservedSymbol "rec " false)))) (Lean.ParserDescr.const `letRecDecls)))
Equations
- Lean.Parser.Tactic.tacticRefine_lift'_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticRefine_lift'_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "refine_lift' " false) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.tacticHave'_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticHave'_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "have' " false) (Lean.ParserDescr.const `haveDecl))
Equations
- Lean.Parser.Tactic.«tacticHave'__:=_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«tacticHave'__:=_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "have'" false) (Lean.ParserDescr.const `ident)) (Lean.ParserDescr.symbol " := ")) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.tacticLet'_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticLet'_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "let' " false) (Lean.ParserDescr.const `letDecl))
Equations
- Lean.Parser.Tactic.inductionAltLHS = Lean.ParserDescr.nodeWithAntiquot "inductionAltLHS" `Lean.Parser.Tactic.inductionAltLHS (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "| ") (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `optional (Lean.ParserDescr.symbol "@")) (Lean.ParserDescr.const `ident))) (Lean.ParserDescr.symbol "_"))) (Lean.ParserDescr.unary `many (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol "_"))))
Equations
- Lean.Parser.Tactic.inductionAlt = Lean.ParserDescr.nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `ppDedent (Lean.ParserDescr.const `ppLine)) (Lean.ParserDescr.unary `many1 Lean.Parser.Tactic.inductionAltLHS)) (Lean.ParserDescr.symbol " => ")) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `hole) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `syntheticHole) (Lean.ParserDescr.const `tacticSeq))))
Equations
- Lean.Parser.Tactic.inductionAlts = Lean.ParserDescr.nodeWithAntiquot "inductionAlts" `Lean.Parser.Tactic.inductionAlts (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "with ") (Lean.ParserDescr.unary `optional (Lean.ParserDescr.cat `tactic 0))) (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGe) Lean.Parser.Tactic.inductionAlt))))
Equations
- Lean.Parser.Tactic.induction = Lean.ParserDescr.node `Lean.Parser.Tactic.induction 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "induction " false) (Lean.ParserDescr.sepBy1 (Lean.ParserDescr.cat `term 0) "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " using ") (Lean.ParserDescr.const `ident)))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "generalizing ") (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.cat `term 1024)))))) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.inductionAlts))
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
, wheree
is an expression instead of a variable, generalizese
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. Herer
should be a theorem whose result type must be of the formCt
, whereC
is a bound variable andt
is a (possibly empty) sequence of bound variablesinductionegeneralizingz₁...zₙ
, wherez₁...zₙ
are variables in the local context, generalizes overz₁...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 tactictac₁
for thezero
case, andtac₂
for thesucc
case.
Equations
- Lean.Parser.Tactic.generalizeArg = Lean.ParserDescr.nodeWithAntiquot "generalizeArg" `Lean.Parser.Tactic.generalizeArg (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `optional (Lean.ParserDescr.unary `atomic (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol " : ")))) (Lean.ParserDescr.cat `term 51)) (Lean.ParserDescr.symbol " = ")) (Lean.ParserDescr.const `ident))
Equations
- Lean.Parser.Tactic.generalize = Lean.ParserDescr.node `Lean.Parser.Tactic.generalize 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "generalize " false) (Lean.ParserDescr.sepBy1 Lean.Parser.Tactic.generalizeArg "," (Lean.ParserDescr.symbol ", ")))
generalize([h:]e=x),+
replaces all occurrences e
s in the main goal with a fresh hypothesis x
s.
If h
is given, h:e=x
is introduced as well.
Equations
- Lean.Parser.Tactic.casesTarget = Lean.ParserDescr.nodeWithAntiquot "casesTarget" `Lean.Parser.Tactic.casesTarget (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `optional (Lean.ParserDescr.unary `atomic (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol " : ")))) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.cases = Lean.ParserDescr.node `Lean.Parser.Tactic.cases 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "cases " false) (Lean.ParserDescr.sepBy1 Lean.Parser.Tactic.casesTarget "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " using ") (Lean.ParserDescr.const `ident)))) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.inductionAlts))
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
, wheree
is an expression instead of a variable, generalizese
in the goal, and then cases on the resulting variable.- Given
as:Listα
,casesaswith|nil=>tac₁|consaas'=>tac₂
, uses tactictac₁
for thenil
case, andtac₂
for thecons
case, anda
andas'
are used as names for the new variables introduced. casesh:e
, wheree
is a variable or an expression, performs cases one
as above, but also adds a hypothesish:e=...
to each hypothesis, where...
is the constructor instance for that particular case.
Equations
- Lean.Parser.Tactic.renameI = Lean.ParserDescr.node `Lean.Parser.Tactic.renameI 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rename_i " false) (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol "_")))))
rename_ix_1...x_n
renames the last n
inaccessible names using the given names.
Equations
- Lean.Parser.Tactic.tacticRepeat_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticRepeat_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "repeat " false) (Lean.ParserDescr.const `tacticSeq))
repeattac
applies tac
to main goal. If the application succeeds,
the tactic is applied recursively to the generated subgoals until it eventually fails.
Equations
- Lean.Parser.Tactic.tacticTrivial = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticTrivial 1024 (Lean.ParserDescr.nonReservedSymbol "trivial" false)
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
- Lean.Parser.Tactic.split = Lean.ParserDescr.node `Lean.Parser.Tactic.split 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "split " false) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.cat `term 0)))) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))
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
- Lean.Parser.Tactic.dbgTrace = Lean.ParserDescr.node `Lean.Parser.Tactic.dbgTrace 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "dbg_trace " false) (Lean.ParserDescr.const `str))
Equations
- Lean.Parser.Tactic.tacticStop_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticStop_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "stop" false) (Lean.ParserDescr.unary `group (Lean.ParserDescr.const `tacticSeq)))
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
- Lean.Parser.Tactic.specialize = Lean.ParserDescr.node `Lean.Parser.Tactic.specialize 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "specialize " false) (Lean.ParserDescr.cat `term 0))
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
- Lean.Parser.Tactic.tacticUnhygienic_ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticUnhygienic_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "unhygienic " false) (Lean.ParserDescr.const `tacticSeq))
Equations
- Lean.Parser.Tactic.fail = Lean.ParserDescr.node `Lean.Parser.Tactic.fail 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "fail " false) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.const `str)))
failmsg
is a tactic that always fail and produces an error using the given message.
Equations
- Lean.Parser.Tactic.checkpoint = Lean.ParserDescr.node `Lean.Parser.Tactic.checkpoint 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "checkpoint " false) (Lean.ParserDescr.const `tacticSeq))
Equations
- Lean.Parser.Tactic.save = Lean.ParserDescr.node `Lean.Parser.Tactic.save 1024 (Lean.ParserDescr.nonReservedSymbol "save" false)
Equations
- Lean.Parser.Tactic.sleep = Lean.ParserDescr.node `Lean.Parser.Tactic.sleep 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "sleep" false) (Lean.ParserDescr.const `num))
The tactic sleepms
sleeps for ms
milliseconds and does nothing. It is used for debugging purposes only.
Equations
- Lean.Parser.Tactic.«tacticExists_,,» = Lean.ParserDescr.node `Lean.Parser.Tactic.«tacticExists_,,» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "exists " false) (Lean.ParserDescr.sepBy1 (Lean.ParserDescr.cat `term 0) "," (Lean.ParserDescr.symbol ", ")))
existse₁,e₂,...
is shorthand for refine⟨e₁,e₂,...⟩;trytrivial
. It is useful for existential goals.
Equations
- Lean.Parser.Attr.simp = Lean.ParserDescr.node `Lean.Parser.Attr.simp 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "simp" false) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpPre Lean.Parser.Tactic.simpPost))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.cat `prio 0)))
Equations
- «term‹_›» = Lean.ParserDescr.node `«term‹_›» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "‹") (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol "›"))
‹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
.