tactics.md

Tactics

Syntax	Description
istart	Start the proof mode.
istop	Stop the proof mode.
irename nameFrom into nameTo	Rename the hypothesis nameFrom to nameTo.
iclear hyp	Discard the hypothesis hyp.
iexists x	Instantiate an existential quantifier in the goal with x.
iexact hyp	Solve the goal with the hypothesis hyp.
iassumption	Solve the goal with a hypothesis from any context (pure, intuitionistic or spatial).
iex_falso	Change the goal to False.
ipure hyp	Move the hypothesis hyp to the pure context.
iintuitionistic hyp	Move the hypothesis hyp to the intuitionistic context. Equivalent to icases hyp with #hyp.
ispatial hyp	Move the hypothesis hyp to the spatial context.
iemp_intro	Solve the goal if it is emp and discard all hypotheses.
ipure_intro	Turn a goal of the form ⌜φ⌝ into a Lean goal φ.
ispecialize pmTerm	Specialize an hypothesis according to the proof mode term pmTerm.
isplit	Split a conjunction (e.g. ∧) into two goals, using the entire spatial context for both of them.
isplit{l|r}	Split a separating conjunction (e.g. ∗) into two goals, using the entire spatial context for the left (l) or right (r) side.
isplit{l|r} [hyps]	Split a separating conjunction (e.g. ∗) into two goals, using the hypotheses hyps as the spatial context for the left (l) or right (r) side. The remaining hypotheses in the spatial context are used for the opposite side.
ileft iright	Choose to prove the left (ileft) or right (iright) side of a disjunction in the goal.
icases pmTerm with cases-pat	Destruct pmTerm using the cases pattern cases-pat.
imod pmTerm with cases-pat	Eliminate the modality at the top of pmTerm and destruct the result using cases-pat.
iintro intro-pats	Introduce up to multiple hypotheses using the intro patterns intro-pats.
imodintro	Introduce the modality at the top of goal.
inext	Introduce a later modality at the top of goal.
iapply pmTerm	Match the conclusion of the current goal against the conclusion of the pmTerm and generates goals for each of its premises, moving all unused spatial hypotheses to the last premise.
ihave cases-pat := pmTerm	Move pmTerm into the Iris context using cases-pat. (In contrast to icases, ihave does not remove the hypothesis from the Iris context.)
ihave cases-pat : term $$ spec-pat	Assert term as cases-pat and prove it using spec-pat.
irevert hyp	Revert the hypothesis hyp.

Cases Patterns

Pattern	Description
name	Rename the hypothesis to name.
-	Drop the hypothesis.
⟨pat_1 [, pat_2]...⟩	Destruct a (separating) conjunction and recursively destruct its arguments using the patterns pat_i.
(pat_1 [| pat_2]...)	Destruct a disjunction and recursively destruct its arguments in separate goals using the patterns pat_i. The parentheses can be omitted if this pattern is not on the top level.
%name	Move the hypothesis to the pure context and rename it to name.
#pat	Move the hypothesis to the intuitionistic context and further destruct it using the pattern pat.
∗pat	Move the hypothesis to the spatial context and further destruct it using the pattern pat.
>pat	Eliminate the modality at the top of the hypothesis and further destruct the result using the pattern pat.

Example:

-- the hypothesis:
P1 ∗ (□ P2 ∨ P2) ∗ (P3 ∧ P3')
-- can be destructed using the pattern:
⟨HP1, #HP2 | HP2, ⟨HP3, -⟩⟩
-- (there are of course other valid patterns for destructing the shown hypothesis)

Intro Patterns

Pattern	Description
cases-pat	Introduce an hypothesis and destruct it following cases-pat.
!>	Introduce the modality at the top of the goal.

Specialization Patterns

Pattern	Description
H	Use the hypothesis H, which should match the premise exactly.
[H1 ... HN]	Generate a goal with the hypotheses [H1, ..., HN]
[H1 ... HN] as str	Generate a goal named str with the hypotheses [H1, ..., HN].
%t	Use the pure term t to instantiate the hypothesis.

In general, the hypotheses passed to a subgoal are not available for proving the main goal. However, if one uses the icases tactic with a persistent cases pattern or the ihave tactic with a persistent cases pattern, the hypotheses are available both for the subgoal and the main goal.

Proof Mode Terms

Proof mode terms (pmTerm) are of the form

(H $$ specPat1 ... specPatN)

where H is a hypothesis or Lean term whose conclusion is an entailment, and specPat1 ... specPatN are specialization patterns.