introintrosrevertclearexfalsoshelve
/ Unshelveunshelvecongruencediscriminatedestructconstructorinductioncutfoldunfoldsetrewritesimplcbnexistsreflexivityinjectioninversionapplysplitcaseelimassumptionsymmetryposeenoughassertspecializegeneralizesubstreplacerememberexactrefineleft /
rightcontradictiontrivialautof_equalgive_uptransitivity~rename~changeringfieldlialraeautoeposeTacticals:
repeatexactProvide a value of the goal type.
Say that goal type matches type of provided value exactly.
Goal
nat.
Proof.
exact 1.
Qed.
assertState 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.
enoughAlmost 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.
f_equalIf 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.
revertMoves 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. ⁵
reflexivityA 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.
symmetryChange 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 *)
inductionPerform induction over a term of an inductive type. Generates two sub-goals:
For example, for nat,
Goal
forall n:nat,
n + 0 = n.
Proof.
intro n.
induction n.
- reflexivity.
- simpl.
rewrite IHn.
reflexivity.
Qed.
discriminateIf 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.
elimSomething 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.
assumptionRoughly 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.
existsWhen 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.
left / rightApplicable 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 2An 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.
injectionTakes 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.
clearRemove 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
setGive 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.
cutProvide 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.
replaceReplace a term with another term.
Generates two sub-goals and involves the following steps:
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.
rememberGive 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).
splitCan 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:
poseAdd 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
*)
contradictionSees 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.
exfalsoImplements 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.
shelve and Unshelveshelve 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.
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.
*)
transitivityWhen 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.
renameChange name of a variable.
Goal forall a: nat,
a = 0.
Proof.
intro a.
rename a into x.
inversionAmong 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.
refineAllows 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.
constructorApply constructor once to break down the value.
For example, applying
Goal
1 <= 3.
Proof.
constructor.
constructor.
constructor.
Qed.
moveChange 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.
applyAttempts to match current goal with conclusion of argument.
caseAn 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).
destructFor case analysis.
Some use cases:
exists to the assumptions sidecongruenceSome level of automation.
A special use:
liaFor 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.
lralia but for real number domain.Require Import Lra.https://coq.inria.fr/refman/proof-engine/ltac.html
all:Apply a tactic to all remaining goals
repeatRepeatedly 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.
firstUse the first tactic to succeed from among a list of tactics.
first [ left | right ]
A tactic that has already been defined can be redefined using
::=.
Ltac left ::= right. │~
(* Redefine [left] to mean the same as [right] *)
| Description | Example |
|---|---|
| Backtracking (OR) | left + right |
| Branching | left │ right |
Ltac2 has an ML-style type system.
H: &HHi:
$Hiltac1:(idtac) ʳidtac for ltac2:
()