Tactics¶
Tactics specify how to transform the proof state of an incomplete proof to eventually generate a complete proof.
Proofs can be developed in two basic ways: In forward reasoning,
the proof begins by proving simple statements that are then combined to prove the
theorem statement as the last step of the proof. With forward reasoning,
for example,
the proof of A /\ B
would begin with proofs of A
and B
, which are
then used to prove A /\ B
. Forward reasoning is probably the most common
approach in human-generated proofs.
In backward reasoning, the proof begins with the theorem statement
as the goal, which is then gradually transformed until every subgoal generated
along the way has been proven. In this case, the proof of A /\ B
begins
with that formula as the goal. This can be transformed into two subgoals,
A
and B
, followed by the proofs of A
and B
. Rocq and its tactics
primarily use backward reasoning.
A tactic may fully prove a goal, in which case the goal is removed from the proof state. More commonly, a tactic replaces a goal with one or more subgoals. (We say that a tactic reduces a goal to its subgoals.)
Most tactics require specific elements or preconditions to reduce a goal;
they display error messages if they can't be applied to the goal.
A few tactics, such as auto
, don't fail even if the proof state
is unchanged.
Goals are identified by number. The current goal is number
1. Tactics are applied to the current goal by default. (The
default can be changed with the Default Goal Selector
option.) They can
be applied to another goal or to multiple goals with a
goal selector such as 2: tactic
.
This chapter describes many of the most common built-in tactics. Built-in tactics can be combined to form tactic expressions, which are described in the Ltac chapter. Since tactic expressions can be used anywhere that a built-in tactic can be used, "tactic" may refer to both built-in tactics and tactic expressions.
Common elements of tactics¶
Reserved keywords¶
The tactics described in this chapter reserve the following keywords:
by using
Thus, these keywords cannot be used as identifiers. It also declares the following character sequences as tokens:
** [= |-
Invocation of tactics¶
Tactics may be preceded by a goal selector (see Section Goal selectors). If no selector is specified, the default selector is used.
- Option Default Goal Selector "toplevel_selector"¶
This option controls the default selector, used when no selector is specified when applying a tactic. The initial value is 1, hence the tactics are, by default, applied to the first goal.
Using value
all
will make it so that tactics are, by default, applied to every goal simultaneously. Then, to apply a tactic tac to the first goal only, you can write1:tac
.Using value
!
enforces that all tactics are used either on a single focused goal or with a local selector (’’strict focusing mode’’).Although other selectors are available, only
all
,!
or a single natural number are valid default goal selectors.
Bindings¶
Tactics that take a term as an argument may also accept bindings
to
specify the values to assign unbound variables in a term.
Bindings can be given by position or name. Generally these appear in the form
one_term_with_bindings
or with bindings
, depending on the tactic.
one_term with bindings?
— bindings for variables inone_term
are typically determined by unifyingone_term
with a tactic-dependent part of the context, with any remaining unbound variables provided by thebindings
.one_term+
— binds free variables in the left-to-right order of their first appearance in the relevant term.For some tactics, bindings for all free variables must be provided, such as for
induction
,destruct
,elim
andcase
. Other tactics automatically generate some or all of the bindings from the conclusion or a hypothesis, such asapply
andconstructor
and its variants. In this case, only instances for the dependent premises that are not bound in the conclusion of the relevant term are required (and permitted).( identnatural := term )+
— binds variables by name (ifident
is given), or by unifying with then
-th premise of the relevant term (ifnatural
is given).
Intro patterns¶
Intro patterns let you specify the name to assign to variables and hypotheses
introduced by tactics. They also let you split an introduced hypothesis into
multiple hypotheses or subgoals. Common tactics that accept intro patterns
include assert
, intros
and destruct
.
::=
*
|
**
|
simple_intropattern
simple_intropattern::=
simple_intropattern_closed % term0*
simple_intropattern_closed::=
naming_intropattern
|
_
|
or_and_intropattern
|
equality_intropattern
naming_intropattern::=
ident
|
?
|
?ident
or_and_intropattern::=
[ intropattern**| ]
|
( simple_intropattern*, )
|
( simple_intropattern*& )
equality_intropattern::=
->
|
<-
|
[= intropattern* ]
Note that the intro pattern syntax varies between tactics.
Most tactics use simple_intropattern
in the grammar.
destruct
, edestruct
, induction
,
einduction
, case
, ecase
and the various
inversion
tactics use or_and_intropattern
, while
intros
and eintros
use intropattern*
.
The eqn:
construct in various tactics uses naming_intropattern
.
Naming patterns
Use these elementary patterns to specify a name:
ident
— use the specified name?
— let Rocq generate a fresh name_
— discard the matched part (unless it is required for another hypothesis)if a disjunction pattern omits a name, such as
[|H2]
, Rocq will choose a name
Splitting patterns
The most common splitting patterns are:
split a hypothesis in the form
A /\ B
into two hypothesesH1: A
andH2: B
using the pattern(H1 & H2)
or(H1, H2)
or[H1 H2]
. Example. This also works onA <-> B
, which is just a notation representing(A -> B) /\ (B -> A)
.split a hypothesis in the form
A \/ B
into two subgoals using the pattern[H1|H2]
. The first subgoal will have the hypothesisH1: A
and the second subgoal will have the hypothesisH2: B
. Examplesplit a hypothesis in either of the forms
A /\ B
orA \/ B
using the pattern[]
.
Patterns can be nested: [[Ha|Hb] H]
can be used to split (A \/ B) /\ C
.
Note that there is no equivalent to intro patterns for goals. For a goal A /\ B
,
use the split
tactic to replace the current goal with subgoals A
and B
.
For a goal A \/ B
, use left
to replace the current goal with A
, or
right
to replace the current goal with B
.
( simple_intropattern+,
) — matches a product over an inductive type with a single constructor. If the number of patterns equals the number of constructor arguments, then it applies the patterns only to the arguments, and( simple_intropattern+, )
is equivalent to[simple_intropattern+]
. If the number of patterns equals the number of constructor arguments plus the number oflet-ins
, the patterns are applied to the arguments andlet-in
variables.( simple_intropattern+& )
— matches a right-hand nested term that consists of one or more nested binary inductive types such asa1 OP1 a2 OP2 …
(where theOPn
are right-associative). (If theOPn
are left-associative, additional parentheses will be needed to make the term right-hand nested, such asa1 OP1 (a2 OP2 …)
.) The splitting pattern can have more than 2 names, for example(H1 & H2 & H3)
matchesA /\ B /\ C
. The inductive types must have a single constructor with two parameters. Example[ intropattern*+| ]
— splits an inductive type that has multiple constructors such asA \/ B
into multiple subgoals. The number ofintropattern
s must be the same as the number of constructors for the matched part.[ intropattern+ ]
— splits an inductive type that has a single constructor with multiple parameters such asA /\ B
into multiple hypotheses. Use[H1 [H2 H3]]
to matchA /\ B /\ C
.[]
— splits an inductive type: If the inductive type has multiple constructors, such asA \/ B
, create one subgoal for each constructor. If the inductive type has a single constructor with multiple parameters, such asA /\ B
, split it into multiple hypotheses.
Equality patterns
These patterns can be used when the hypothesis is an equality:
->
— replaces the right-hand side of the hypothesis with the left-hand side of the hypothesis in the conclusion of the goal; the hypothesis is cleared; if the left-hand side of the hypothesis is a variable, it is substituted everywhere in the context and the variable is removed. Example<-
— similar to->
, but replaces the left-hand side of the hypothesis with the right-hand side of the hypothesis.[= intropattern*, ]
— If the product is over an equality type, applies eitherinjection
ordiscriminate
. Ifinjection
is applicable, the intropattern is used on the hypotheses generated byinjection
. If the number of patterns is smaller than the number of hypotheses generated, the pattern?
is used to complete the list. Example
Other patterns
*
— introduces one or more dependent premises from the result until there are no more. Example**
— introduces one or more dependent or non-dependent premises from the result until there are no more premises.intros **
is equivalent tointros
. Examplesimple_intropattern_closed % term*
— first applies each of the terms with theapply
tactic on the hypothesis to be introduced, then it usessimple_intropattern_closed
. Example
Note
A \/ B
and A /\ B
use infix notation to refer to the inductive
types or
and and
.
or
has multiple constructors (or_introl
and or_intror
),
while and
has a single constructor (conj
) with multiple parameters
(A
and B
).
These are defined in theories/Init/Logic.v
. The "where" clauses define the
infix notation for "or" and "and".
Note
intros
p+
is not always equivalent to intros p; … ; intros p
if some of the p
are _
. In the first form, all erasures are done
at once, while they're done sequentially for each tactic in the second form.
If the second matched term depends on the first matched term and the pattern
for both is _
(i.e., both will be erased), the first intros
in the second
form will fail because the second matched term still has the dependency on the first.
Examples:
Example: intro pattern for /\
- Goal forall (A: Prop) (B: Prop), (A /\ B) -> True.
- 1 goal ============================ forall A B : Prop, A /\ B -> True
- intros.
- 1 goal A, B : Prop H : A /\ B ============================ True
- destruct H as (HA & HB).
- 1 goal A, B : Prop HA : A HB : B ============================ True
Example: intro pattern for \/
- Goal forall (A: Prop) (B: Prop), (A \/ B) -> True.
- 1 goal ============================ forall A B : Prop, A \/ B -> True
- intros.
- 1 goal A, B : Prop H : A \/ B ============================ True
- destruct H as [HA|HB]. all: swap 1 2.
- 2 goals A, B : Prop HA : A ============================ True goal 2 is: True 2 goals A, B : Prop HB : B ============================ True goal 2 is: True
Example: -> intro pattern
- Goal forall (x:nat) (y:nat) (z:nat), (x = y) -> (y = z) -> (x = z).
- 1 goal ============================ forall x y z : nat, x = y -> y = z -> x = z
- intros * H.
- 1 goal x, y, z : nat H : x = y ============================ y = z -> x = z
- intros ->.
- 1 goal x, z : nat H : x = z ============================ x = z
Example: [=] intro pattern
The first
intros
[=]
usesinjection
to strip(S …)
from both sides of the matched equality. The second usesdiscriminate
on the contradiction1 = 2
(internally represented as(S O) = (S (S O))
) to complete the goal.
- Goal forall (n m:nat), (S n) = (S m) -> (S O)=(S (S O)) -> False.
- 1 goal ============================ forall n m : nat, S n = S m -> 1 = 2 -> False
- intros *.
- 1 goal n, m : nat ============================ S n = S m -> 1 = 2 -> False
- intros [= H].
- 1 goal n, m : nat H : n = m ============================ 1 = 2 -> False
- intros [=].
- No more goals.
Example: (A & B & …) intro pattern
- Parameters (A : Prop) (B: nat -> Prop) (C: Prop).
- A is declared B is declared C is declared
- Goal A /\ (exists x:nat, B x /\ C) -> True.
- 1 goal ============================ A /\ (exists x : nat, B x /\ C) -> True
- intros (a & x & b & c).
- 1 goal a : A x : nat b : B x c : C ============================ True
Example: * intro pattern
- Goal forall (A: Prop) (B: Prop), A -> B.
- 1 goal ============================ forall A B : Prop, A -> B
- intros *.
- 1 goal A, B : Prop ============================ A -> B
Example: ** pattern ("intros **" is equivalent to "intros")
- Goal forall (A: Prop) (B: Prop), A -> B.
- 1 goal ============================ forall A B : Prop, A -> B
- intros **.
- 1 goal A, B : Prop H : A ============================ B
Example: compound intro pattern
- Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
- 1 goal ============================ forall A B C : Prop, A \/ B /\ C -> (A -> C) -> C
- intros * [a | (_,c)] f.
- 2 goals A, B, C : Prop a : A f : A -> C ============================ C goal 2 is: C
- all: swap 1 2.
- 2 goals A, B, C : Prop c : C f : A -> C ============================ C goal 2 is: C
Example: combined intro pattern using [=] -> and %
- Require Import Stdlib.Lists.List.
- Section IntroPatterns.
- Variables (A : Type) (xs ys : list A).
- A is declared xs is declared ys is declared
- Example ThreeIntroPatternsCombined : S (length ys) = 1 -> xs ++ ys = xs.
- 1 goal A : Type xs, ys : list A ============================ S (length ys) = 1 -> xs ++ ys = xs
- intros [=->%length_zero_iff_nil].
- 1 goal A : Type xs : list A ============================ xs ++ nil = xs
intros
would addH : S (length ys) = 1
intros [=]
would additionally applyinjection
toH
to yieldH0 : length ys = 0
intros [=->%length_zero_iff_nil]
applies the theorem, making H the equalityl=nil
, which is then applied as for->
.Theorem length_zero_iff_nil (l : list A): length l = 0 <-> l=nil.The example is based on Tej Chajed's coq-tricks
Occurrence clauses¶
An occurrence is a subterm of a goal or hypothesis that matches a pattern provided by a tactic. Occurrence clauses select a subset of the ocurrences in a goal and/or in one or more of its hypotheses.
occurrences::=
at occs_nums|
in goal_occurrencessimple_occurrences
::=
occurrencesoccs_nums
::=
-? nat_or_var+nat_or_var
::=
naturalidentgoal_occurrences
::=
hyp_occs+, |- concl_occs??|
* |- concl_occs?|
|- concl_occs?|
concl_occs?hyp_occs
::=
hypident at occs_nums?hypident
::=
ident|
( type of ident )|
( value of ident )concl_occs
::=
* at occs_nums?
occurrences
The first form of
occurrences
selects occurrences in the conclusion of the goal. The second form can select occurrences in the goal conclusion and in one or more hypotheses.simple_occurrences
A semantically restricted form of
occurrences
that doesn't allow theat
clause anywhere within it.-? nat_or_var+
Selects the specified occurrences within a single goal or hypothesis. Occurrences are numbered starting with 1 following a depth-first traversal of the term's expression, including occurrences in implicit arguments and coercions that are not displayed by default. (Set the
Printing All
flag to show those in the printed term.)For example, when matching the pattern
_ + _
in the term(a + b) + c
, occurrence 1 is(…) + c
and occurrence 2 is(a + b)
. When matching that pattern with terma + (b + c)
, occurrence 1 isa + (…)
and occurrence 2 isb + c
.Specifying
-
includes all occurrences except the ones listed.hyp_occs*, |- concl_occs??
Selects occurrences in the specified hypotheses and the specified occurrences in the conclusion.
* |- concl_occs?
Selects all occurrences in all hypotheses and the specified occurrences in the conclusion.
|- concl_occs?
Selects the specified occurrences in the conclusion.
goal_occurrences ::= concl_occs?
Selects all occurrences in all hypotheses and in the specified occurrences in the conclusion.
hypident at occs_nums?
Omiting
occs_nums
selects all occurrences within the hypothesis.hypident ::= ident
Selects the hypothesis named
ident
.( type of ident )
Selects the type part of the named hypothesis (e.g.
: nat
).( value of ident )
Selects the value part of the named hypothesis (e.g.
:= 1
).concl_occs ::= * at occs_nums?
Selects occurrences in the conclusion. '*' by itself selects all occurrences.
occs_nums
selects the specified occurrences.Use
in *
to select all occurrences in all hypotheses and the conclusion, which is equivalent toin * |- *
. Use* |-
to select all occurrences in all hypotheses.When rewriting in multiple hypotheses, they must not appear in the term to rewrite. For instance
rewrite H in H,H'
is an error. If an hypothesis appears only through a hole, it will be removed from that hole's context.With
rewrite term in *
, hypotheses on which the dependency cannot be avoided are skipped, for instancerewrite H in *
skips rewriting inH
. This is the case even if only one hypothesis ends up rewritten.If multiple occurrences are given, such as in
rewrite
H at 1 2 3
, the tactic must match at least one occurrence in order to succeed. The tactic will fail if no occurrences match. Occurrence numbers that are out of range (e.g.at 1 3
when there are only 2 occurrences in the hypothesis or conclusion) are ignored.Tactics that use occurrence clauses include
set
,remember
,induction
anddestruct
.
Applying theorems¶
- Tactic exact one_term¶
Directly gives the exact proof term for the goal.
exact p
succeeds if and only ifone_term
and the type ofp
are unifiable (see Conversion rules).- Error Not an exact proof.¶
- Tactic assumption¶
This tactic looks in the local context for a hypothesis whose type is convertible to the goal. If it is the case, the subgoal is proved. Otherwise, it fails.
- Error No such assumption.¶
- Tactic eassumption¶
Behaves like
assumption
but is able to process goals and hypotheses with existential variables. It can also resolve existential variables, whichassumption
will not.
- Tactic simple? notypeclasses? refine one_term¶
Behaves like
exact
but allows holes (denoted by_
or(_ : type)
) inone_term
.refine
generates as many subgoals as there are remaining holes in the elaborated term. Any subgoal that occurs in other subgoals is automatically shelved, as if callingshelve_unifiable
.simple
If specified, don't shelve any subgoals or perform beta reduction.
notypeclasses
If specified, do checking without resolving typeclasses. The generated subgoals (shelved or not) are not candidates for typeclass resolution, even if they have a typeclass type as their conclusion.
Example
- Inductive Option : Set := | Fail : Option | Ok : bool -> Option.
- Option is defined Option_rect is defined Option_ind is defined Option_rec is defined Option_sind is defined
- Definition get : forall x:Option, x <> Fail -> bool.
- 1 goal ============================ forall x : Option, x <> Fail -> bool
- refine (fun x:Option => match x return x <> Fail -> bool with | Fail => _ | Ok b => fun _ => b end).
- 1 goal x : Option ============================ Fail <> Fail -> bool
- intros; absurd (Fail = Fail); trivial.
- No more goals.
- Defined.
- Error Cannot infer a term for this placeholder.¶
There is a hole in the term you gave whose type cannot be inferred. Put a cast around it.
Setting
Debug
"unification"
enables printing traces of unification steps used during elaboration/typechecking and therefine
tactic."ho-unification"
prints information about higher order heuristics.
- Tactic apply one_term_with_bindings+, in_hyp_as?¶
- in_hyp_as
::=
in ident as_ipat?+,as_ipat
::=
as simple_intropatternUses unification to match the type of each
one_term
(inone_term_with_bindings
) with the goal (to do backward reasoning) or with a hypothesis (to do forward reasoning). Specifying multipleone_term_with_bindings
is equivalent to giving each one serially, left to right, as separateapply
tactics.The type of
one_term
contains zero or more premises followed by a conclusion, i.e. it typically has the formforall open_binders ,? termpremise ->* termconclusion
. (Theforall
s may also be interleaved with the premises, but common usage is to equivalently gather them at the beginning of theone_term
.) Backward reasoning with aone_term
whose type is, for example,A -> B
replaces an as-yet unproven goalB
withA
. Forward reasoning with the sameone_term
changes a hypothesis with typeA
toB
. (Hypotheses are considered proven propositions within the context that contains them.)Unification creates a map from the variables in the type of
one_term
to matching subterms of the goal or hypothesis. The matching subterms are then substituted into the type ofone_term
when generating the updated goal or hypothesis. Unmatched premises become new subgoals with similar substitutions. If no match is found, the tactic fails.Setting
Debug
"tactic-unification"
enables printing traces of unification steps in tactic unification. Tactic unification is used in tactics such asapply
andrewrite
.The goal and hypothesis cases are described separately for clarity.
one_term
(insideone_term_with_bindings
)If
one_term
is anident
, it is the name of a theorem, lemma or hypothesis whose type is given in the theorem statement or shown in the context. Otherwise it is a proof term whose type can be displayed withCheck
one_term
.- Without
in_hyp_as
(the goal case)If the goal matches all of the type of
one_term
(both premises and the conclusion), the tactic proves the goal. Otherwise, the tactic matches the goal against the conclusion ofone_term
and, if possible, one or more premises (from right to left). If the match succeeds, the tactic replaces the current goal with a subgoal for each unmatched premise of the type ofone_term
. This example matches only the conclusion, while this one also matches a premise.If the conclusion of the type of
one_term
does not match the goal and the conclusion is an inductive type with a single constructor, then each premise in the constructor is recursively matched to the goal in right-to-left order and the first match is used. In this case, the tactic will not match premises that would result in applying a lemma of the formforall A, … -> A
. See example here.
The goal case uses first-order unification with dependent types unless the conclusion of the type of
term
is of the formP t1 … tn
withP
to be instantiated. In the latter case, the behavior depends on the form of the target. If the target is of the formQ u1 … un
and theti
andui
unify, thenP
is instantiated intoQ
. Otherwise,apply
tries to defineP
by abstracting overt1 … tn
in the target. You can usepattern
to transform the target so that it gets the form(fun x1 … xn => Q) u1 … un
. See the example here.
in_hyp_as
(the hypothesis case)Proceeding from right to left, find the first premise of the type of
one_term
that matches the specified hypothesis. If a match is found, the hypothesis is replaced with the conclusion of the type ofone_term
(substituting for the unified variables) and the tactic creates a new subgoal for each unmatched premise. See the example here.If specified,
as simple_intropattern
is applied to the conclusion of the type ofone_term
. In this case, the selected hypothesis is left unchanged if its name is not reused.If the type of
one_term
is an inductive type with a single constructor, then each premise in the constructor is recursively matched to the conclusion of the hypothesis in right-to-left order and the first match is used. See example here.For the hypothesis case, matching is done only with first-order unification.
with bindings
(inone_term_with_bindings
)Gives explicit instantiations for variables used in the type of
one_term
. There are 3 cases:
Bindings for variables can be provided in a list of
one_term
s in the left-to-right order of their first appearance in the type ofone_term
. For the goal case (example), the list should give bindings only for variables that aren't bound by unification. However, in the hypothesis case (example), the list must include bindings for all variables.Bindings for unbound variables can be given by name with the
(ident := term)
form.The form
(natural := term)
binds additional variables by unifying the Nth premise of the type ofone_term
withterm
. (Use1
for the first premise.)
- Error Unable to unify one_term with one_term.¶
The
apply
tactic failed to match the conclusion ofone_term
. You can helpapply
by transforming your goal with thechange
orpattern
tactics.
- Error Unable to apply lemma of type "..." on hypothesis of type "...".¶
This happens if the conclusion of
ident
does not match any of the premises of the type ofone_term
.
- Error Unable to find an instance for the variables ident+.¶
This occurs when some instantiations of the premises of
one_term
are not deducible from the unification. This is the case, for instance, when you want to apply a transitivity property. To fix this, add bindings for theident
s using towith bindings
or useeapply
.Example: Backward reasoning in the goal with
apply
- Goal forall A B C: Prop, (A -> B -> C) -> C.
- 1 goal ============================ forall A B C : Prop, (A -> B -> C) -> C
- intros A B C H.
- 1 goal A, B, C : Prop H : A -> B -> C ============================ C
- apply H. (* replace goal with new goals for unmatched premises of H *)
- 2 goals A, B, C : Prop H : A -> B -> C ============================ A goal 2 is: B
Example: Backward reasoning in the goal with
apply
including a premise
- Goal forall A B C: Prop, (A -> B -> C) -> (B -> C).
- 1 goal ============================ forall A B C : Prop, (A -> B -> C) -> B -> C
- intros A B C H.
- 1 goal A, B, C : Prop H : A -> B -> C ============================ B -> C
- apply H. (* match on "B -> C", replace goal with "A" *)
- 1 goal A, B, C : Prop H : A -> B -> C ============================ A
Example: Forward reasoning in hypotheses with
apply
- Goal forall A B C: Prop, B -> (A -> B -> C) -> True.
- 1 goal ============================ forall A B C : Prop, B -> (A -> B -> C) -> True
- intros A B C H0 H1.
- 1 goal A, B, C : Prop H0 : B H1 : A -> B -> C ============================ True
- apply H1 in H0. (* change H0, create new goals for unmatched premises of H1 *)
- 2 goals A, B, C : Prop H0 : C H1 : A -> B -> C ============================ True goal 2 is: A
Example: Apply a theorem with a binding in a goal
apply
unifies the conclusionn <= p
of the theoremle_trans : forall n m p, n <= m -> m <= p -> n <= p
with the goal, assigningx * x
andy * y
in the goal to, repectively,n
andp
in theorem (backward reasoning). Thewith
clause provides the binding form
:
- Require Import PeanoNat.
- Goal forall (x y : nat), x <= y -> x * x <= y * y.
- 1 goal ============================ forall x y : nat, x <= y -> x * x <= y * y
- intros x y H0.
- 1 goal x, y : nat H0 : x <= y ============================ x * x <= y * y
- apply Nat.le_trans with (y * x).
- 2 goals x, y : nat H0 : x <= y ============================ x * x <= y * x goal 2 is: y * x <= y * y
Example: Apply a theorem with a binding in a hypothesis
When applying a theorem in a hypothesis,
apply
unifies the hypothesis with one of the premises of the theoremle_trans : forall n m p, n <= m -> m <= p -> n <= p
. In this case, it unifies with the first premise (n <= m
) and assignsx * x
andy * y
to, respectively,n
andm
in the theorem (forward reasoning). Thewith
clause provides the binding forp
.In addition,
apply
in a hypothesis isn't as flexible asapply
in the goal: for hypotheses, the unbound variable can be bound by name (as shown) or values for all the variables can be given positionally, i.e.apply Nat.le_trans with (x * x) (y * y) (y * x) in H.
- Require Import PeanoNat.
- Goal forall (x y : nat), x * x <= y * y -> x <= y.
- 1 goal ============================ forall x y : nat, x * x <= y * y -> x <= y
- intros x y H.
- 1 goal x, y : nat H : x * x <= y * y ============================ x <= y
- apply Nat.le_trans with (p := y * x) in H.
- 2 goals x, y : nat H : x * x <= y * x ============================ x <= y goal 2 is: y * y <= y * x
Example: Applying theorems with
<->
A <-> B
is defined as(A -> B) /\ (B -> A)
./\
represents an inductive type with a single constructor:Inductive and (C D:Prop) : Prop := conj : C -> D -> D /\ C
. The premises ofconj
areC
andD
. The tactic uses the first matching constructor premise in right-to-left order.Theorems that use
<->
to state a logical equivalence behave consistently when applied to goals and hypotheses.
- Goal forall (A B: Prop) (H1: A <-> B) (H: A), A.
- 1 goal ============================ forall A B : Prop, A <-> B -> A -> A
- intros A B H1 H.
- 1 goal A, B : Prop H1 : A <-> B H : A ============================ A
- apply H1.
- 1 goal A, B : Prop H1 : A <-> B H : A ============================ B
- apply H1 in H.
- 1 goal A, B : Prop H1 : A <-> B H : B ============================ B
Example: Special case of second-order unification in apply
Shows the use of the special case second-order unification described here (after "unless").
Note that we usually use
induction
rather than applyingnat_ind
directly.
- Goal forall x y, x + y = y + x.
- 1 goal ============================ forall x y : nat, x + y = y + x
- intros.
- 1 goal x, y : nat ============================ x + y = y + x
- Check nat_ind.
- nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
- apply nat_ind. (* Notice the goals are unprovable. *)
- 2 goals x, y : nat ============================ x + y = 0 goal 2 is: forall n : nat, x + y = n -> x + y = S n
- Show Proof. (* apply has instantiated P with (eq (x + y)) because the goal was (eq (x + y) (y + x)) and n could be unified with (y + x) *)
- (fun x y : nat => nat_ind (eq (x + y)) ?Goal ?Goal0 (y + x))
- (* However, we can use the pattern tactic to get the instantiation we want: *)
- Undo.
- 1 goal x, y : nat ============================ x + y = y + x
- pattern x.
- 1 goal x, y : nat ============================ (fun n : nat => n + y = y + n) x
- apply nat_ind.
- 2 goals x, y : nat ============================ 0 + y = y + 0 goal 2 is: forall n : nat, n + y = y + n -> S n + y = y + S n
- Show Proof. (* apply has instantiated P with (fun n : nat => n + y = y + n) and the goal can be proven *)
- (fun x y : nat => nat_ind (fun n : nat => n + y = y + n) ?Goal ?Goal0 x : x + y = y + x)
- Tactic eapply one_term_with_bindings+, in_hyp_as?¶
Behaves like
apply
, but creates existential variables when Rocq is unable to deduce instantiations for variables, rather than failing.
- Tactic rapply one_term¶
Behaves like
eapply
but uses the proof engine ofrefine
to handle existential variables, holes and conversion problems. This may result in slightly different behavior regarding which conversion problems are solvable. However,rapply
fails if any holes remain inone_term
itself after typechecking and typeclass resolution but before unification with the goal. Note thatrapply
tries to instantiate as many hypotheses ofone_term
as possible. As a result, if it is possible to applyone_term
to arbitrarily many arguments without getting a type error,rapply
will loop.
- Tactic simple apply one_term_with_bindings+, in_hyp_as?¶
Behaves like
apply
but it reasons modulo conversion only on subterms that contain no variables to instantiate and does not traverse tuples. For instance, the following example fails because it would require convertingid ?foo
andO
.Example
- Definition id (x : nat) := x.
- id is defined
- Parameter H : forall x y, id x = y.
- H is declared
- Goal O = O.
- 1 goal ============================ 0 = 0
- Fail simple apply H.
- The command has indeed failed with message: Unable to unify "id ?M150 = ?M151" with "0 = 0".
Because it reasons modulo a limited amount of conversion,
simple apply
fails faster thanapply
and it is thus well-suited for use in user-defined tactics that backtrack often.
- Tactic simple eapply one_term_with_bindings+, in_hyp_as?¶
Example
Assume we have a transitive relation R
on nat
:
- Parameter R : nat -> nat -> Prop.
- R is declared
- Axiom Rtrans : forall x y z:nat, R x y -> R y z -> R x z.
- Rtrans is declared
- Parameters n m p : nat.
- n is declared m is declared p is declared
- Axiom Rnm : R n m.
- Rnm is declared
- Axiom Rmp : R m p.
- Rmp is declared
Consider the goal (R n p)
provable using the transitivity of R
:
- Goal R n p.
- 1 goal ============================ R n p
The direct application of Rtrans
with apply
fails because no value
for y
in Rtrans
is found by apply
:
- apply Rtrans.
- Toplevel input, characters 6-12: > apply Rtrans. > ^^^^^^ Error: Unable to find an instance for the variable y.
A solution is to apply (Rtrans n m p)
or (Rtrans n m)
.
- apply (Rtrans n m p).
- 2 goals ============================ R n m goal 2 is: R m p
Note that n
can be inferred from the goal, so the following would work
too.
- apply (Rtrans _ m).
- 2 goals ============================ R n m goal 2 is: R m p
More elegantly, apply Rtrans with (y:=m)
allows only mentioning the
unknown m:
- apply Rtrans with (y := m).
- 2 goals ============================ R n m goal 2 is: R m p
Another solution is to mention the proof of (R x y)
in Rtrans
- apply Rtrans with (1 := Rnm).
- 1 goal ============================ R m p
… or the proof of (R y z)
.
- apply Rtrans with (2 := Rmp).
- 1 goal ============================ R n m
On the opposite, one can use eapply
which postpones the problem of
finding m
. Then one can apply the hypotheses Rnm
and Rmp
. This
instantiates the existential variable and completes the proof.
- eapply Rtrans.
- 2 focused goals (shelved: 1) ============================ R n ?y goal 2 is: R ?y p
- apply Rnm.
- 1 goal ============================ R m p
- apply Rmp.
- No more goals.
Managing the local context¶
- Tactic intro ident? where?¶
Applies the
hnf
tactic until it finds an item that can be introduced in the context by removing certain constructs in the goal. If no item is found, the tactic fails. The name used isident
(if specified) or from the construct, except that if the name from the construct already exists in the local context, Rocq uses a fresh name instead. The constructs have these forms: (See examples here.)forall x : T, term
x : T
is a dependent premise. Removesforall x : T,
from the goal and addsx : T
to the context.A -> …
A
is a non-dependent premise. RemovesA ->
from the goal and addsH : A
to the context.let x := c, term
Removes
let x := c,
from the goal and addsx := c : T
to the context.
We recommend always specifying
ident
so that the names of hypotheses don't change as the proof is updated, making your proof easier to maintain. For example, if H exists in the context, Rocq will consider usingH0
,H1
, ... until it finds an unused name. Modifications to a proof can change automatically assigned names that subsequent tactics likely refer to, making the proofs harder to maintain. TheMangle Names
flag gives some control over how fresh names are generated (see Proof maintenance).Note that
intros
lets you introduce multiple items into the context with a single tactic.
ident
The name to give to the introduced item. If not given, Rocq uses the variable name from the
forall
orH
for premises. If a name such asH
is already in use, Rocq will consider usingH0
,H1
, ... until it finds a fresh name.Note
If a hypothesis name hides the base name of a global constant then the latter can still be referred to by a qualified name (see Qualified names).
where
Indicates where to place the introduced hypothesis: at the top or bottom of the context or before or after another specified hypothesis. The default is
at bottom
.
- Error ident is already used.¶
The provided
ident
is already used in the local context.
- Error No product even after head-reduction.¶
There is nothing to introduce even after
hnf
has been completely applied.Example:
intro
andintros
- Goal forall m n, m < n -> (let x := 0 in True).
- 1 goal ============================ forall m n : nat, m < n -> let x := 0 in True
- intro m.
- 1 goal m : nat ============================ forall n : nat, m < n -> let x := 0 in True
- intro n.
- 1 goal m, n : nat ============================ m < n -> let x := 0 in True
- intro H.
- 1 goal m, n : nat H : m < n ============================ let x := 0 in True
- intro x.
- 1 goal m, n : nat H : m < n x := 0 : nat ============================ True
This single
intros
tactic is equivalent to the 4 precedingintro
tactics:
- Goal forall m n, m < n -> (let x := 0 in True).
- 1 goal ============================ forall m n : nat, m < n -> let x := 0 in True
- intros m n H x.
- 1 goal m, n : nat H : m < n x := 0 : nat ============================ True
- Tactic intros intropattern*¶
- Tactic intros until identnatural¶
The first form introduces zero or more items into the context from the constructs listed in
intro
. Ifintropattern
is not specified, the tactic introduces items until it reaches the head constant; it never fails and may leave the context unchanged.If
intropattern
is specified, thehnf
tactic is applied until it finds an item that can be introduced into the context. Theintropattern
is often just a list ofident
s, but other forms can also be specified in order to, for example, introduce all dependent premises (*
); introduce all dependent and non-dependent premises (**
); split terms such asA /\ B
([]
) and pick a fresh name with a given prefix (?X
). See Intro patterns.The second form repeats
intro
until it has introduced a dependent premise with the nameident
or has introducednatural
premises (likeA
inA -> B
).We recommend explicitly naming items with
intros
instead of usingintros until natural
. See the explanation here.Example: intros until
- Goal forall x y : nat, x = y -> y = x.
- 1 goal ============================ forall x y : nat, x = y -> y = x
- intros until y.
- 1 goal x, y : nat ============================ x = y -> y = x
Or:
- Goal forall x y : nat, x = y -> y = x.
- 1 goal ============================ forall x y : nat, x = y -> y = x
- intros until 1.
- 1 goal x, y : nat H : x = y ============================ y = x
- Error No quantified hypothesis named ident in current goal even after head-reduction.¶
The
ident
in theuntil
clause doesn't appear as a dependent premise.
- Tactic eintros intropattern*¶
Works just like
intros
except that it creates existential variables for any unresolved variables rather than failing. Typically this happens when using a%
intropattern (seesimple_intropattern
).
- Tactic clear -? ident+?¶
Erases unneeded hypotheses from the context of the current goal. "Unneeded" means that the unselected hypotheses and the goal don't depend directly or indirectly on the erased hypotheses. That means the hypotheses will no longer appear in the context and therefore can't be used in subsequent proof steps. Note that erasing an uneeded hypothesis may turn a goal that was provable into an unprovable goal.
clear
All unneeded hypotheses are erased. This may leave the context unchanged; this form never fails.
clear ident+
Erases the named hypotheses if they are unneeded and fails otherwise.
clear - ident+
Selects all hypotheses that are not named by the
ident
s, then erases those that are unneeded. This may leave the context unchanged; this form never fails as long as theident
s name hypotheses in the context.
- Tactic clearbody ident+¶
This tactic expects
ident+
to be local definitions and clears their respective bodies. In other words, it turns the given definitions into assumptions.
- Tactic revert ident+¶
Moves the specified hypotheses and local definitions to the goal, if this respects dependencies. This is the inverse of
intro
.- Tactic revert dependent ident¶
Deprecated since version 8.18.
An alias for
generalize dependent
.
- Tactic move identfrom where¶
- where
::=
at top|
at bottom|
before ident|
after identMoves a hypothesis
identfrom
and hypotheses that directly or indirectly refer toidentfrom
that appear betweenidentfrom
andident
.at top
andat bottom
are equivalent to giving the name of the first or last hypotheses in the context. The dependent hypotheses will appear afteridentfrom
, appearing in dependency order. This lets users show and group hypotheses in the order they prefer. It doesn't change the goal or the proof term.Note
Perhaps confusingly, "before" and "after" are interpeted with respect to the direction in which the hypotheses are moved rather than in the order of the resulting list of hypotheses. If
identfrom
is beforeident
in the context, these notions are the same: for hypothesesA B C
,move A after B
givesB A C
, whereas ifidentfrom
is afterident
in the context, they are the opposite:move C after A
givesC A B
because the direction of movement is reversed.Example: move
- Goal forall x :nat, x = 0 -> forall y z:nat, y=y-> 0=x.
- 1 goal ============================ forall x : nat, x = 0 -> forall y : nat, nat -> y = y -> 0 = x
- intros x Hx y z Hy.
- 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
- (* x Hx y z Hy *)
- move y after z. (* x Hx z y Hy (z was left of y, intuitive case) *)
- 1 goal x : nat Hx : x = 0 z, y : nat Hy : y = y ============================ 0 = x
- Undo.
- 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
- move z after y. (* x Hx z y Hy (z was right of y, see Note above) *)
- 1 goal x : nat Hx : x = 0 z, y : nat Hy : y = y ============================ 0 = x
- Undo.
- 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
- move x after Hy. (* y z Hy x Hx (Hx depends on x, so moved) *)
- 1 goal y, z : nat Hy : y = y x : nat Hx : x = 0 ============================ 0 = x
- Undo.
- 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
- move x before Hy. (* y z x Hx Hy *)
- 1 goal y, z, x : nat Hx : x = 0 Hy : y = y ============================ 0 = x
- Undo.
- 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
- move Hy after Hx. (* x y Hy Hx z *)
- 1 goal x, y : nat Hy : y = y Hx : x = 0 z : nat ============================ 0 = x
- Undo.
- 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
- move Hy before Hx. (* x Hx y Hy z *)
- 1 goal x : nat Hx : x = 0 y : nat Hy : y = y z : nat ============================ 0 = x
- Tactic rename ident1 into ident2+,¶
Renames hypothesis
ident1
intoident2
for each pair ofident
s. Renaming is done simultaneously, which permits swapping the names of 2 hypotheses. (Note that the renaming is applied in the context and the existential variables, but the proof term doesn't change.)
- Tactic set alias_definition occurrences?¶
- Tactic set one_term as_name? occurrences?¶
- alias_definition
::=
( ident simple_binder* := term )simple_binder
::=
name|
( name+ : term )as_name
::=
as identThe first form adds a new local definition
ident := …
. Ifsimple_binder
is not specified, the definition body isterm
and otherwisefun simple_binder* => term
. Then the tactic replaces the body expression with the new variableident
in the goal or as specified byoccurrences
. The tactic may succeed and add the local definition even if no replacements are made.The second form is equivalent to
set (ident := one_term) occurrences?
usingident
, if present, or an auto-generated name if not provided.If
term
orone_term
has holes (i.e. subexpressions with the form “_
”), the tactic first checks that all subterms matching the pattern are compatible before doing the replacement using the leftmost subterm matching the pattern.Example: set with a
simple_binder
set
does a simple syntactic replacement in the goal:- Goal forall n, n = 0.
- 1 goal ============================ forall n : nat, n = 0
- intros.
- 1 goal n : nat ============================ n = 0
- pattern n. (* without this, "set" won't replace anything in the goal *)
- 1 goal n : nat ============================ (fun n0 : nat => n0 = 0) n
- set (f x := x = 0).
- 1 goal n : nat f := fun x : nat => x = 0 : nat -> Prop ============================ f n
- Tactic eset alias_definition occurrences?¶
- Tactic eset one_term as_name? occurrences?¶
Similar to
set
, but instead of failing because of uninstantiated variables, generates existential variables for them. In practice, this is relevant only wheneset
is used as a synonym ofepose
, i.e. when theterm
does not occur in the goal.
- Tactic remember one_term as_name? eqn : naming_intropattern? in goal_occurrences?¶
Similar to
set (ident := one_term) in *
but creates a hypothesis using Leibniz equality to remember the relation between the introduced variable and the term rather than creating a local definition. Ifas_name
is not specified a fresh name is used. Usenaming_intropattern
to name the new equation.- Tactic eremember one_term as_name? eqn : naming_intropattern? in goal_occurrences?¶
Similar to
remember
, but instead of failing because of uninstantiated variables, generates existential variables for them.
- Tactic pose alias_definition¶
- Tactic pose one_term as_name?¶
Similar to
set
. Adds a local definition to the context but without doing any replacement.
Controlling the proof flow¶
- Tactic assert ( ident : type ) by ltac_expr3?¶
- Tactic assert ( ident := term )¶
- Tactic assert one_type as_ipat? by ltac_expr3?
Adds a new hypothesis to the current subgoal and a new subgoal before it to prove the hypothesis. Then, if
ltac_expr3
is specified, it applies that tactic to fully prove the new subgoal (and otherwise fails).The first form adds a new hypothesis named
ident
of typetype
. (This corresponds to the cut rule of sequent calculus.)The second form is equivalent to
assert (ident : type) by exact (term)
wheretype
is the type ofterm
. It is also equivalent to usingpose proof
. If the head ofterm
isident
, the tactic is equivalent tospecialize
.In the third form, if
as_ipat
isn't specified, the tactic adds the hypothesisone_type
with a fresh name. Otherwise, it transforms the hypothesis as specified byas_ipat
and adds the resulting new hypotheses and goals. See Intro patterns.- Error The term "type" has type "type1" which should be Set, Prop or Type.¶
Occurs when the argument
type
(in the first form) orone_type
(in the third form) is not of typeProp
,Set
norType
.
- Error Proof is not complete.¶
ltac_expr3
was not able to prove the new hypothesis.
- Tactic eassert ( ident : type ) by ltac_expr3?¶
- Tactic eassert ( ident := term )¶
- Tactic eassert one_type as_ipat? by ltac_expr3?
Unlike
assert
, thetype
,term
orone_type
ineassert
may contain holes, denoted by_
, for which the tactic will create existential variables. This lets you avoid specifying the asserted statement completely before starting to prove it.
- Tactic enough ( ident : type ) by ltac_expr3?¶
- Tactic enough one_type as_ipat? by ltac_expr3?¶
Adds a new hypothesis to the current subgoal and a new subgoal after it to prove the hypothesis.
The first form adds a new hypothesis
ident : type
andtype
as the new subgoal. Then, ifltac_expr3
is specified, it applies that tactic to prove the current subgoal with the added hypothesis (and otherwise fails).In the second form, if
as_ipat
isn't specified, the tactic adds a new hypothesisone_type
with a name chosen by Rocq. Otherwise, it transformsone_type
as specified byas_ipat
and adds the resulting new hypotheses. Theas_ipat
may also expand the current subgoal into multiple subgoals. Then, ifltac_expr3
is specified, it is applied to and must succeed on all of them.- Tactic eenough ( ident : type ) by ltac_expr3?¶
- Tactic eenough one_type as_ipat? by ltac_expr3?¶
Unlike
enough
, thetype
andone_type
ineenough
may contain holes, denoted by_
, for which the tactic will create existential variables. This lets you avoid specifying the asserted statement completely until you start to use the hypothesis or later start to prove the statement.
- Tactic cut one_type¶
Implements the non-dependent case of the App typing rule, the Modus Ponens inference rule. It is equivalent to
enough (ident: one_type). revert ident.
This tactic is generally considered obsolete but it is still widely used in old scripts.
- Tactic pose proof term as_ipat?¶
- Tactic pose proof ( ident := term )¶
The first form behaves like
assert one_type as_ipat? by exact term
whereone_type
is the type ofterm
.The second form is equivalent to
assert (ident := term)
.- Tactic epose proof term as_ipat?¶
- Tactic epose proof ( ident := term )¶
While
pose proof
expects that no existential variables are generated by the tactic,epose proof
removes this constraint.
- Tactic specialize one_term_with_bindings as_ipat?¶
Specializes a term (typically a hypothesis or a lemma) by applying arguments to it.
First, the tactic generates a modified term: If the head constant of
one_term
(inone_term_with_bindings
) has the typeforall ...
, the tactic replaces one or more of the quantified variables in the type with arguments provided byone_term_with_bindings
, either in the form of a function application (which may be partial), such as(H 1)
, or with named or numbered binders, such asH with (n:=1)
.If the head constant has a non-dependent product type such as
A -> B -> C
, the tactic eliminates one or more of the premises (doing forward reasoning).Uninstantiated arguments are inferred by unification, if possible, or otherwise left quantified in the resulting term.
Then, If the head constant is a hypothesis
H
, the resulting term replaces that hypothesis. Specifyingas_ipat
will leave the original hypothesis unchanged and will introduce new hypotheses as specified by thesimple_intropattern
. IfH
appears in the conclusion or another hypothesis, you must useas_ipat
to give a fresh hypothesis name.If the head constant is a lemma or theorem, the resulting term is added as a new premise of the goal so that the behavior is similar to that of
generalize
. In this case, you can useas_ipat
to immediately introduce the modified term as one or more hypotheses.Example: partial application in
specialize
- Goal (forall n m: nat, n + m = m + n) -> True.
- 1 goal ============================ (forall n m : nat, n + m = m + n) -> True
- intros.
- 1 goal H : forall n m : nat, n + m = m + n ============================ True
- specialize (H 1). (* equivalent to: specialize H with (n := 1) *)
- 1 goal H : forall m : nat, 1 + m = m + 1 ============================ True
Example:
specialize
with a non-dependent productCompare this to a similar example that uses
apply
.specialize
won't introduce new goals asapply
can.- Goal forall A B C: Prop, B -> (A -> B -> C) -> True.
- 1 goal ============================ forall A B C : Prop, B -> (A -> B -> C) -> True
- Proof.
- intros A B C H0 H1.
- 1 goal A, B, C : Prop H0 : B H1 : A -> B -> C ============================ True
- specialize H1 with (2:=H0).
- 1 goal A, B, C : Prop H0 : B H1 : A -> C ============================ True
- Tactic generalize one_term+¶
- Tactic generalize pattern_occs as_name?+,¶
For each
one_term
(which may be in thepattern_occs
), replaces the goalG
withforall (x:T), G'
, whereone_term
is a subterm ofG
of typeT
andG'
is obtained by replacing all occurrences ofone_term
withx
withinG
.x
is a fresh variable chosen based onT
. Specifying multipleone_term
s is equivalent togeneralize one_termn; … ; generalize one_term1
. (Note they are processed right to left.)as_name
The name to use for
x
instead of a fresh name.
Example
- Goal forall x y:nat, 0 <= x + y + y.
- 1 goal ============================ forall x y : nat, 0 <= x + y + y
- Proof. intros *.
- 1 goal x, y : nat ============================ 0 <= x + y + y
- Show.
- 1 goal x, y : nat ============================ 0 <= x + y + y
- generalize (x + y + y). (* get a simpler goal that can be proven by induction *)
- 1 goal x, y : nat ============================ forall n : nat, 0 <= n
- Tactic evar ( ident : type )¶
- Tactic evar one_type¶
The
evar
tactic creates a new local definition namedident
with typetype
orone_type
in the context. The body of this binding is a fresh existential variable. If the second form is used, Rocq chooses the name.
- Tactic instantiate ( ident := term )¶
- Tactic instantiate ( natural := term ) hloc?¶
- hloc
::=
in |- *|
in ident|
in ( type of ident )|
in ( value of ident )The first form refines (see
refine
) an existential variableident
with the termterm
. It is equivalent toonly [ident]: refine term
.Note
To be able to refer to an existential variable by name, the user must have given the name explicitly (see Existential variables).
Note
When you are referring to hypotheses which you did not name explicitly, be aware that Rocq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors.
The second form refines an existential variable selected by its position. The
natural
argument is the position of the existential variable from right to left in the goal. (Use thehloc
clause to select an existential variable in a hypothesis.) Counting starts at 1 and multiple occurrences of the same existential variable are counted multiple times. Using this form is discouraged because slight changes to the goal may change the needed index, causing a maintenance issue.Advanced users may want to define and use an Ltac tactic to get more consistent behavior, such as:
Ltac instantiate_ltac_variable ev term := let H := fresh in pose ev as H; instantiate (1 := term) in (value of H); clear H.in ident
Selects the hypothesis
ident
.in |- *
Selects the goal. This is the default behavior.
in ( type of ident )
Selects existential variables in the type of the local definition
ident
. (The body is not included.)in ( value of ident )
Selects existential variables in the body of the local definition
ident
. (The type is not included.)
- Tactic absurd one_type¶
one_type
is any propositionP
of typeProp
. This tactic applies False elimination, that is it deduces the current goal from False, and generates as subgoals∼P
andP
. It is very useful in proofs by cases, where some cases are impossible. In most cases,P
or∼P
is one of the hypotheses of the local context.
- Tactic contradiction one_term_with_bindings?¶
Tries to prove the current goal by finding a contradiction.
If
one_term_with_bindings
is not provided (the most common use case), the tactic first does anintros
. The tactic then proves the goal ifthe updated context has a pair of hypotheses where one is the negation of the other (e.g.
P
and not~P
), orthere is a hypothesis with an empty inductive type (e.g.
False
), orthere is a hypothesis
~P
whereP
is a singleton inductive type (e.g.True
orx=x
) provable byGoal P. constructor.
If
one_term_with_bindings
is provided, its type must be a negation, such as~P
, or an empty inductive type, such asFalse
. If the type is a negation andP
is a hypothesis in the context, the goal is proven. If the type is a negation andP
is not in the context, the goal is replaced withP
. If the type isFalse
or another empty inductive type, the goal is proven. Otherwise the tactic fails. (If there is a hypothesisP
and you want to replace the goal with~P
, use thecontradict
tactic. If there are hypothesesH1 : P
andH2 : ~P
, usecontradiction
without arguments orcontradiction H2
sincecontradiction H1
won't work.)Use the
discriminate
tactic to prove the current goal when there is a hypothesis with an impossible structural equality such as0 = 1
.
Example: contradiction
tactic
Simple examples. To see more detail, add intros
after each Goal
.
- Inductive F :=. (* Another empty inductive type *)
- F is defined F_rect is defined F_ind is defined F_rec is defined F_sind is defined
- Goal F -> False.
- 1 goal ============================ F -> False
- contradiction.
- No more goals.
- Qed.
- Goal forall (A : Prop), A -> ~A -> False.
- 1 goal ============================ forall A : Prop, A -> ~ A -> False
- contradiction.
- No more goals.
- Qed.
- Goal forall (A : Type) (x : A), ~(x = x) -> False.
- 1 goal ============================ forall (A : Type) (x : A), x <> x -> False
- contradiction.
- No more goals.
- Qed.
Apply a fact from the standard library:
- Require Import Arith.
- [Loading ML file ring_plugin.cmxs (using legacy method) ... done]
- Goal forall (A : Prop), 0 < 0 -> A.
- 1 goal ============================ forall A : Prop, 0 < 0 -> A
- intros.
- 1 goal A : Prop H : 0 < 0 ============================ A
- contradiction (Nat.lt_irrefl 0).
- No more goals.
- Qed.
- Tactic contradict ident¶
Transforms the specified hypothesis
ident
and the goal in order to prove that the hypothesis is false. Forcontradict H
, the current goal and context are transformed as shown. (For brevity,⊢
is used to separate hypotheses from the goal; it is equivalent to the dividing line shown in a context.):H: ~A ⊢ B
becomes⊢ A
H: ~A ⊢ ~B
becomesH: B ⊢ A
H: A ⊢ B
becomes⊢ ~A
H: A ⊢ ~B
becomesH: B ⊢ ~A
- Tactic exfalso¶
Implements the “ex falso quodlibet” logical principle: an elimination of False is performed on the current goal, and the user is then required to prove that False is indeed provable in the current context.
Classical tactics¶
In order to ease the proving process, when the Classical
module is
loaded, a few more tactics are available. Make sure to load the module
using the Require Import
command.
- Tactic classical_left¶
- Tactic classical_right¶
These tactics are the analog of
left
andright
but using classical logic. They can only be used for disjunctions. Useclassical_left
to prove the left part of the disjunction with the assumption that the negation of right part holds. Useclassical_right
to prove the right part of the disjunction with the assumption that the negation of left part holds.
Performance-oriented tactic variants¶
- Tactic exact_no_check one_term¶
For advanced usage. Similar to
exact
term
, but as an optimization, it skips checking thatterm
has the goal's type, relying on the kernel check instead. Seechange_no_check
for more explanation.Example
- Goal False.
- 1 goal ============================ False
- exact_no_check I.
- No more goals.
- Fail Qed.
- The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False".
- Tactic vm_cast_no_check one_term¶
For advanced usage. Similar to
exact_no_check
term
, but additionally instructs the kernel to usevm_compute
to compare the goal's type with theterm
's type.Example
- Goal False.
- 1 goal ============================ False
- vm_cast_no_check I.
- No more goals.
- Fail Qed.
- The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False".
- Tactic native_cast_no_check one_term¶
for advanced usage. similar to
exact_no_check
term
, but additionally instructs the kernel to usenative_compute
to compare the goal's type with theterm
's type.Example
- Goal False.
- 1 goal ============================ False
- native_cast_no_check I.
- No more goals.
- Fail Qed.
- The command has indeed failed with message: Native compiler is disabled, falling back to VM conversion test. [native-compiler-disabled,native-compiler,default]