Probably better to learn to use the few ssreflect notions rather than getting familiar with this long list of tactics.
—
List
- Tactics
- [ ]
intro - [ ]
intros - [X]
revert - [X]
clear - [X]
exfalso - [X]
shelve/Unshelve - [ ]
unshelve - [ ]
congruence - [X]
discriminate - [ ]
destruct - [ ]
constructor - [X]
induction - [X]
cut - [ ]
fold - [ ]
unfold - [X]
set - [ ]
rewrite - [ ]
simpl - [ ]
cbn - [X]
exists - [X]
reflexivity - [X]
injection - [ ]
inversion - [ ]
apply - [X]
split - [ ]
case - [X]
elim - [X]
assumption - [X]
symmetry - [X]
pose - [X]
enough - [X]
assert - [ ]
specialize - [ ]
generalize - [ ]
subst - [X]
replace - [X]
remember - [X]
exact - [ ]
refine - [X]
left/right - [X]
contradiction - [ ]
trivial - [ ]
auto - [X]
f_equal - [X]
give_up - [X]
transitivity~ - [X]
rename~ - [ ]
change
- [ ]
- Relatively advanced tactics:
- [ ]
ring - [ ]
field - [ ]
lia - [ ]
lra
- [ ]
- Same tactics with 'e-prefix' is same as their counterparts except that they can handle existential variables as well (ie, holes).
- [ ]
eauto - [ ]
epose
- [ ]
Tacticals:
repeat
DONE exact
Provide a value of the goal type.
Say that goal type matches type of provided value exactly.
Goal
nat.
Proof.
exact 1.
Qed.
DONE assert
State and prove a theorem in the middle of another proof.
Once this theorem is proved, it is added to the context as a hypothesis.
Goal
2 * 3 = 3 + 3.
Proof.
assert (forall n:nat, 2 * n = n + n).
- intros.
ring.
- exact (H 3).
Qed.
Here's another example:
Goal
forall n:nat,
n + 0 = n.
Proof.
intro n.
assert (n+0 = 0+n).
- simpl.
induction n.
+ reflexivity.
+ simpl.
rewrite IHn.
reflexivity.
- rewrite H.
reflexivity.
Qed.
DONE enough
Almost same as assert tactic, except that the assertion needs to be proved only after it is used.
Require Import Arith. (* For [ring] on nat *)
Goal
2 * 3 = 3 + 3.
Proof.
enough (forall n:nat, 2 * n = n + n).
- apply (H 3).
- intro n.
ring.
Qed.
DONE f_equal
If same constructor shows on both sides of a goal (not hypothesis. Use injection?? for that?).
Goal
forall n m:nat, n = m -> S n = S m.
Proof.
intros.
f_equal.
Qed.
DONE revert
Moves a hypothesis to goal.
Sort of like the reverse of intro.
Goal
forall n:nat, n + 0 = n.
Proof.
intro n.
revert n.
Resembles generalize, which is more powerful. ⁵
DONE reflexivity
A simple tactic.
Broadly speaking, reflexivity solves the goal if it is of the form t = u after verifying that t and u are definitively equal; otherwise fails.
Lemma bar : forall (a : nat), a = a.
Proof.
intros.
(* a = a *)
reflexivity.
(* All goals completed *)
reflexivity implicitly has the effect of simpl as well.
DONE symmetry
Change a goal of the form a = b to b = a.
Lemma bar : forall (a b : nat), a + b = b + a.
Proof.
intros.
(* a + b = b + a *)
symmetry.
(* b + a = a + b *)
DONE induction
Perform induction over a term of an inductive type. Generates two sub-goals:
- base case
- inductive case
For example, for nat,
Goal
forall n:nat,
n + 0 = n.
Proof.
intro n.
induction n.
- reflexivity.
- simpl.
rewrite IHn.
reflexivity.
Qed.
DONE discriminate
If a proof goal has an associated hypothesis which is an impossible (ie, False:Prop) structural equality of the form term1 = term2 like one among
S O = O
S (S O) = O
S O = S (S (S O))
then, discriminate can prove that goal.
If goal is in the term₁ <> term₂ form, using discriminate has the same effect as intro H. discriminate H.. Helps avoid introducing a new name in such a case.
Example:
Goal
forall n:nat,
S n <> O.
Proof.
intros a H.
(* [a<>b] is actually [a=b -> False]. That's why. *)
discriminate H.
Qed.
Goal
forall n:nat,
S n <> O.
Proof.
discriminate.
Qed.
Goal
true = false -> False.
Proof.
discriminate.
Qed.
DONE elim
Something like an older, more basic version of induction. Coq docs recommends using induction instead.
Unlike induction, elim doesn't modify the local context. We got to do it ourselves.
Goal
forall n:nat,
n + 0 = n.
Proof.
intro n.
elim n.
- reflexivity.
- intros n1 IHn.
simpl.
rewrite IHn.
reflexivity.
Qed.
DONE assumption
Roughly put, assumption can be used if the goal is same as one of the hypotheses in the current context.
Goal
forall p:Prop, p -> p.
Proof.
intros p H.
assumption.
Qed.
DONE exists
When the goal involves a ∃, provide a term of that type to solve that goal.
Goal
exists n, 0+n = 0.
Proof.
exists 0.
reflexivity.
Qed.
DONE left / right
Applicable when the goal consists two parts and only one of them needs to be proved to prove the whole thing.
left proceeds with the first one, while right is used to go with the other.
left≡constructor 1right≡constructor 2
An example with left and Prop:
Goal
forall p:Prop, (2<3) \/ (3<2).
Proof.
left.
constructor.
Qed.
Another example, with right and sumbool:
Goal
{2>3} + {2<=3}.
Proof.
right.
auto.
Qed.
DONE injection
Takes advantage of the fact that the constructors in Coq are injective.
For example, if we got an assumption saying
constr a = constr b~
where constr is a constructor of some type, then injection can figure out that
a = b
would be true as well.
Goal
forall a b:nat, S a = S b -> a = b.
Proof.
intros.
injection H.
intro IHh.
exact IHh.
Qed.
DONE clear
Remove a hypothesis from the local context.
Eg:
With
Goal
forall n:nat, n > 0 -> n >= 0.
Proof.
intros n H.
where goal would be
1 subgoal
n : nat
H : n > 0
========================= (1 / 1)
n >= 0
Use clear H. and the goal will change to:
1 subgoal
n : nat
========================= (1 / 1)
n >= 0
DONE set
Give a name to a term in the conclusion of the goal and add it to the local context.
Require Import Nat.
Goal
forall n:nat,
match (Nat.even n) with
| true => 1
| false => 0
end >= 0.
Proof.
intro n.
and the goal would be:
1 subgoal
n : nat
========================= (1 / 1)
(if even n then 1 else 0) >= 0
But do
set (ie:= Nat.even n).
then the goal would become
1 subgoal
n : nat
ie := even n : bool
========================= (1 / 1)
(if ie then 1 else 0) >= 0
Useful in cases where we need a term to do case analysis on.
In the example, we can do destruct ie which wouldn't have been possible before the set usage.
DONE cut
Provide an extra hypothesis, prove the goal and then prove that the hypothesis is indeed correct.
a la 'cut-rule'.
Probably better to make a separate theorem and use it instead of trying cut. Always good to be able to reuse proofs that have already been made. And reusage is possible only if they have names.
Example:
Require Nat.
Goal
forall a b c:nat,
b = 0 -> a + b + c = a + c.
Proof.
intros a b c.
intro Hb0.
cut (a + b + c = a + c).
- auto.
- rewrite Hb0.
rewrite <- Plus.plus_assoc.
reflexivity.
Qed.
We knew that a + b + c was a + c since b is zero. So we stated and used it to prove the original goal via cut tactic. Afterwards, we prove that this extra hypothesis that we used to prove the goal is also sound.
So, cut generates two sub-goals.
- original goal
- extra hypothesis
DONE replace
Replace a term with another term.
Generates two sub-goals and involves the following steps:
- prove the goal with the replacement.
- prove that the replaced term and its replacement are equivalent.
Goal
forall n:nat,
n + 0 = n.
Proof.
intro n.
replace (n+0) with (0+n).
- reflexivity.
- simpl.
induction n; try reflexivity.
+ simpl.
rewrite <- IHn.
reflexivity.
Qed.
Here, we first considered 0 + n same as the n + 0 to prove the goal. Then we showed that both 0 + n and n + 0 are equivalent.
DONE remember
Give a name to an expression that you might need to use later on and add it to the set of hypotheses.
Goal
forall n m:nat, n + n + m = m + n + n.
Proof.
intros n m.
(*
1 subgoal
n, m : nat
========================= (1 / 1)
n + n + m = m + n + n
*)
remember (n+n) as n2.
(*
1 subgoal
n, m, n2 : nat
Heqn2 : n2 = n + n
========================= (1 / 1)
n2 + m = m + n + n
*)
To given an explicit name to the hypothesis generated by remember, we could've done:
remember (n+n) as n2 eqn:H.
Apparently, can't be used if the term appears in the goal. Once got this error: Conclusion depends on the bodies of Heqp (where Heqp would've been the new hypothesis).
DONE split
Can be used when the type has only one constructor.
Types like /\ (ie, and) or Streams.ForAll.
Goal
forall p q:Prop, p = True -> q = True -> p /\ q.
Proof.
intros p q Hp Hq.
(*
1 subgoal
p, q : Prop
Hp : p = True
Hq : q = True
========================= (1 / 1)
p /\ q
*)
split.
(*
2 subgoals
p, q : Prop
Hp : p = True
Hq : q = True
========================= (1 / 2)
p
========================= (2 / 2)
q
*)
Print and.
(*
Inductive and (A B : Prop) : Prop := conj : A -> B -> A /\ B.
*)
Qed.
Another example:
DONE pose
Add a definition to the list of hypotheses.
Goal
forall n:nat, n+0=n.
Proof.
intros n.
(*
1 subgoal
n : nat
========================= (1 / 1)
n + 0 = n
*)
pose 3.
(*
1 subgoal
n : nat
n0 := 3 : nat
========================= (1 / 1)
n + 0 = n
*)
DONE contradiction
Sees if False can be derived from the list of hypotheses.
Goal
forall p q:Prop, p /\ ~p -> q.
Proof.
intros p q [Hp Hnp].
unfold not in Hnp.
(*
1 subgoal
p, q : Prop
Hp : p
Hnp : p -> False
========================= (1 / 1)
q
*)
contradiction.
(*
0 subgoals
All goals completed.
*)
Qed.
DONE exfalso
Implements the "ex falso quodlibet" logical principle.
ie, if False is provable, any proposition can be proved.
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.
Goal
forall p q:Prop, p /\ ~p -> q.
Proof.
intros p q [Hp Hnp].
(*
1 subgoal
p, q : Prop
Hp : p
Hnp : ~ p
========================= (1 / 1)
q
*)
exfalso.
(*
1 subgoal
p, q : Prop
Hp : p
Hnp : ~ p
========================= (1 / 1)
False
*)
apply (Hnp Hp).
Qed.
Here, upon applying exfalso, goal became False and now we have to derive False from the available hypotheses to complete the proof.
At least in this case, it's sort of similar to constradiction tactic.
DONE shelve and Unshelve
shelve can be used to Postpone current goal and proceed with the next goal.
Unshelve can be used to bring the shelved goal back.
Goal
forall n:nat, n = 0 \/ n <> 0.
Proof.
intros n.
induction n.
(*
2 subgoals
========================= (1 / 2)
0 = 0 \/ 0 <> 0
========================= (2 / 2)
S n = 0 \/ S n <> 0
*)
shelve.
(*
1 subgoal
1 shelved
n : nat
IHn : n = 0 \/ n <> 0
========================= (1 / 1)
S n = 0 \/ S n <> 0
*)
right; auto.
Unshelve.
left; auto.
If we try to end a proof when there are shelved goals remaining, we would get an error like this:
The proof has remaining shelved goals [remaining-shelved-goals,
tactics]
Some unresolved existential variables remain
CAUTION: Unshelve and unshelve are different tactics.
DONE give_up
'Give up' the goals which are currently in focus.
Given up goals cannot be brought back later and hence the proof cannot be ended.
Goal
forall n:nat, n+0 = n.
Proof.
intro n; induction n.
- auto.
- give_up.
(*
0 subgoals
1 admitted
All goals completed.
*)
DONE transitivity
When we have
H1: a = b
H2: b = c
we can use the common term via transitivity tactic to find equality between the other two terms.
Example:
Goal forall a b c: nat,
a = b -> b = c -> a = c.
Proof.
intros a b c H1 H2.
(*
1 subgoal
A : Type
a, b, c : nat
H1 : a = b
H2 : b = c
========================= (1 / 1)
a = c
*)
transitivity b.
(*
2 subgoals
A : Type
a, b, c : nat
H1 : a = b
H2 : b = c
========================= (1 / 2)
a = b
========================= (2 / 2)
b = c
*)
all: assumption.
Qed.
DONE rename
Change name of a variable.
Goal forall a: nat,
a = 0.
Proof.
intro a.
rename a into x.
TODO inversion
Among other things, can be used to prove that something which cannot be derived from the constructors of a type cannot be proven.
For example:
Inductive fooDenote : list nat -> Type :=
| FooDenote: fooDenote nil.
Goal
(* [fooDenote nil] is the only possible type.
So any another fooDenote is not derivable *)
fooDenote (cons 3 nil) -> False.
Proof.
intros H.
inversion H.
Qed.
Inversion is done on a hypothesis.
—
Special usage: inversion n where the nat refers to the nth hypothesis from the last.
TODO refine
Allows to leave holes in the proof that we can fill in later one by one.
Generates as many subgoals as the number of holes.
Quite helpful to allow us to focus on one thing at a time.
TODO constructor
Apply constructor once to break down the value.
For example, applying
Goal
1 <= 3.
Proof.
constructor.
constructor.
constructor.
Qed.
TODO move
Change the order of hyotheses in the context.
Goal
forall n:nat, 0 + n = n -> n + 0 = n -> S n = n + 1.
Proof.
intros n H1 H2.
move H1 after H2.
TODO apply
Attempts to match current goal with conclusion of argument.
TODO case
An older, more basic version of destruct. Coq docs suggest using destruct instead.
Unlike destruct, case cannot modify local context (just like the relation between elim and induction).
TODO destruct
For case analysis.
Some use cases:
- usable kind of like induction without the induction hypothesis being available.
- bring the
existsto the assumptions side
TODO congruence
Some level of automation.
TODO intros
A special use:
- intros until <nat>
TODO lia
For inequalities.
Stands for 'linear integer arithmetic' ??
There was a sort of related tactic named omega, but this has now been removed from coq default installation.
Needs Require Import Lia.
TODO lra
- Like
liabut for real number domain. - Needs
Require Import Lra.
Tacticals
https://coq.inria.fr/refman/proof-engine/ltac.html
TODO all:
Apply a tactic to all remaining goals
DONE repeat
Repeatedly apply a tactic to goal till end of proof or a failure.
Goal
1 <= 4.
Proof.
constructor.
constructor.
constructor.
constructor.
Qed.
With repeat:
Goal
1 <= 4.
Proof.
repeat constructor.
Qed.
TODO first
Use the first tactic to succeed from among a list of tactics.
first [ left | right ]
Ltac1
Redefining a tactic
A tactic that has already been defined can be redefined using ::=.
Ltac left ::= right. │~
(* Redefine [left] to mean the same as [right] *)
Misc
| Description | Example |
|---|---|
| Backtracking (OR) | left + right |
| Branching | left │ right |
Ltac2
Ltac2 has an ML-style type system.
- Refer to hypothesis
H:&H - Refer to gallina constructor named
Hi:$Hi - Use ltac1:
ltac1:(idtac)ʳ - Kind of like ltac1's
idtacfor ltac2:()
Doubts
- How to restart only current sub-goal?
- How to shelve only current sub-goal?