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.
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.
iintro cases-pats	Introduce up to multiple hypotheses and destruct them using the cases patterns cases-pats.
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 name := pmTerm	Move pmTerm into the Iris context with the name name.
ihave name : term $$ spec-pat	Assert term as name and prove it using spec-pat.

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.

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)

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.

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.