Tactic index

Authors:

Yannick Forster

Théo Winterhalter

Display all goals and responses

In this document we illustrate various Rocq tactics that appear in the course. They are not ordered alphabetically but rather follow an order more or less in line with the lecture notes.

`intro`

Usage: intro h, where h is a new name.

intro h introduces hypothesis h into the context It works when the goal is equivalent to A -> B or forall (x : A), B, in which case h is of type A and the goal becomes B (where x is replaced by h when it appears).

Goal forall (P : nat -> Prop) (x : nat), P x -> P (0 + x).forall (P : nat -> Prop) (x : nat), P x -> P (0 + x)
Proof.forall (P : nat -> Prop) (x : nat), P x -> P (0 + x)
  intro Q.Q: nat -> Prop
forall x : nat, Q x -> Q (0 + x)
  intro y.Q: nat -> Prop
y: nat
Q y -> Q (0 + y)
  intro h.Q: nat -> Prop
y: nat
h: Q y
Q (0 + y)
Abort.

`split`

Usage: split.

Applies when the goal is morally a conjunction of subgoals and asks the user to prove those subgoals instead. This works for conjunction (A /\ B) and nullary-conjunction (True):

Goal True /\ (True /\ True).True /\ True /\ True
Proof.True /\ True /\ True
  split.True
True /\ True
  -True split.
  -True /\ True split.True
True
    +True split.
    +True split.
Abort.

More advanced. It in fact applies whenever the goal is an inductive type which has exactly one constructor and requires you to give its arguments one by one.

Goal unit * (0 = 0).unit * (0 = 0)
Proof.unit * (0 = 0)
  split.unit
0 = 0
  -unit split.
  -0 = 0 split.
Abort.

`destruct`

Usage: destruct t as p, where t is an expression (often a variable) and p is an intropattern (explained below).

Performs case analysis on t, generating as many goals as possible ways to construct t (for instance, for t : bool, there are two such cases), and replacing t in the goal by the corresponding constructions (so true and false in the bool case).

As a first approximation, you can see p as the list of cases, separated by pipes (|), and for each of them you provide the names to be used for the introduced constants, separated by spaces. See for instance, case analysis on natural numbers:

Goal forall (P : nat -> Prop) n, P n.forall (P : nat -> Prop) (n : nat), P n
Proof.forall (P : nat -> Prop) (n : nat), P n
  intro P.P: nat -> Prop
forall n : nat, P n intro n.P: nat -> Prop
n: nat
P n
  destruct n as [| m].P: nat -> Prop
P 0
P: nat -> Prop
m: nat
P (S m)
Abort.

The intropattern contains no name for the 0 case, since 0 takes no argument, and exactly one for the successor case, since S takes one argument.

Tip

You may recursively use the intropattern notation to further destruct subterms.

Goal forall (P : nat -> Prop) k, P k.forall (P : nat -> Prop) (k : nat), P k
Proof.forall (P : nat -> Prop) (k : nat), P k
  intro P.P: nat -> Prop
forall k : nat, P k intro k.P: nat -> Prop
k: nat
P k
  destruct k as [| [| m]].P: nat -> Prop
P 0
P: nat -> Prop
P 1
P: nat -> Prop
m: nat
P (S (S m))
Abort.

Variant: destruct t1 as p1, t2 as p2, …, tn as pn. Lets you run several destruct in parallel. Gives you all possible combinations as goals.

Goal forall P (x y : bool) (n : nat), P x y n.forall (P : bool -> bool -> nat -> Type) (x y : bool) (n : nat), P x y n
Proof.forall (P : bool -> bool -> nat -> Type) (x y : bool) (n : nat), P x y n
  destruct x, y, n as [| m].P: bool -> bool -> nat -> Type
P true true 0
P: bool -> bool -> nat -> Type
m: nat
P true true (S m)
P: bool -> bool -> nat -> Type
P true false 0
P: bool -> bool -> nat -> Type
m: nat
P true false (S m)
P: bool -> bool -> nat -> Type
P false true 0
P: bool -> bool -> nat -> Type
m: nat
P false true (S m)
P: bool -> bool -> nat -> Type
P false false 0
P: bool -> bool -> nat -> Type
m: nat
P false false (S m)
Abort.

Advanced variant: destruct t as p eqn:e. This version lets you additionally record an equality e : t = _ where _ stands for the construction in each goal.

Goal forall (P : bool -> Prop) b, P b.forall (P : bool -> Prop) (b : bool), P b
Proof.forall (P : bool -> Prop) (b : bool), P b
  intro p.p: bool -> Prop
forall b : bool, p b intro b.p: bool -> Prop
b: bool
p b
  destruct b as [] eqn: e.p: bool -> Prop
b: bool
e: b = true
p true
p: bool -> Prop
b: bool
e: b = false
p false
Abort.

`intros`

Usage: intros p1 p2 ... pN, where each pI is an intropattern, the list can be empty.

At first glance, it behaves like a succession of intro: indeed, intros a b c. is equivalent to intro a. intro b. intro c. When no argument is provided, it introduces as much as it can, using auto-generated names. intros can in fact do much more, since intropatterns can be used to also perform case analysis.

Goal forall P (b : bool) (n : nat), P b n.forall (P : bool -> nat -> Type) (b : bool) (n : nat), P b n
Proof.forall (P : bool -> nat -> Type) (b : bool) (n : nat), P b n
  intros P [] [| [| k]].P: bool -> nat -> Type
P true 0
P: bool -> nat -> Type
P true 1
P: bool -> nat -> Type
k: nat
P true (S (S k))
P: bool -> nat -> Type
P false 0
P: bool -> nat -> Type
P false 1
P: bool -> nat -> Type
k: nat
P false (S (S k))
Abort.

`apply`

Usage: apply t, where t is an expression (often a lemma or an assumption).

Unifies the type of t with the goal to attempt to conclude using t. If successful, the resulting goals will correspond to arguments to t that must be provided to conclude, or none if t is sufficient.

From Stdlib Require Import List.

Goal forall A (l : list A), l ++ nil = l.forall (A : Type) (l : list A), l ++ nil = l
Proof.forall (A : Type) (l : list A), l ++ nil = l
  intros A l.A: Type
l: list A
l ++ nil = l
  apply app_nil_r.
Abort.

Goal forall P Q R, (P -> Q -> R) -> R.forall P Q R : Type, (P -> Q -> R) -> R
Proof.forall P Q R : Type, (P -> Q -> R) -> R
  intros P Q R h.P, Q, R: Type
h: P -> Q -> R
R
  apply h.P, Q, R: Type
h: P -> Q -> R
P
P, Q, R: Type
h: P -> Q -> R
Q
Abort.

Variant: apply f in h where h is an hypothesis.

This time it tries to unify the type of h with one of the arguments of f.

Goal forall P Q, (forall n, P n -> Q 5 -> Q (n + 2)) -> P 10 -> Q 12.forall P Q : nat -> Type,
(forall n : nat, P n -> Q 5 -> Q (n + 2)) -> P 10 -> Q 12
Proof.forall P Q : nat -> Type,
(forall n : nat, P n -> Q 5 -> Q (n + 2)) -> P 10 -> Q 12
  intros P Q hPQ hP.P, Q: nat -> Type
hPQ: forall n : nat, P n -> Q 5 -> Q (n + 2)
hP: P 10
Q 12
  apply hPQ in hP.P, Q: nat -> Type
hPQ: forall n : nat, P n -> Q 5 -> Q (n + 2)
hP: Q (10 + 2)
Q 12
P, Q: nat -> Type
hPQ: forall n : nat, P n -> Q 5 -> Q (n + 2)
hP: P 10
Q 5
Abort.

Variant: apply f in h as g, lets you additionally give a new name (g) to the generated hypothesis, while keeping h in scope.

Goal forall P Q, (forall n, P n -> Q 5 -> Q (n + 2)) -> P 10 -> Q 12.forall P Q : nat -> Type,
(forall n : nat, P n -> Q 5 -> Q (n + 2)) -> P 10 -> Q 12
Proof.forall P Q : nat -> Type,
(forall n : nat, P n -> Q 5 -> Q (n + 2)) -> P 10 -> Q 12
  intros P Q hPQ hP.P, Q: nat -> Type
hPQ: forall n : nat, P n -> Q 5 -> Q (n + 2)
hP: P 10
Q 12
  apply hPQ in hP as hQ.P, Q: nat -> Type
hPQ: forall n : nat, P n -> Q 5 -> Q (n + 2)
hP: P 10
hQ: Q (10 + 2)
Q 12
P, Q: nat -> Type
hPQ: forall n : nat, P n -> Q 5 -> Q (n + 2)
hP: P 10
Q 5
Abort.

Variant: apply f,g,h, lets you chain several apply in a row by separating them with commas.

Goal forall P Q R, (P -> Q) -> (Q -> R) -> P -> R.forall P Q R : Type, (P -> Q) -> (Q -> R) -> P -> R
Proof.forall P Q R : Type, (P -> Q) -> (Q -> R) -> P -> R
  intros P Q R hPQ hQR hP.P, Q, R: Type
hPQ: P -> Q
hQR: Q -> R
hP: P
R
  apply hQR, hPQ, hP.
Abort.

Variant: apply f with u.

This variant lets you provide arguments that cannot be inferred from unification with the goal alone. In the example below, f takes n as argument, which doesn't appear in its conclusion so apply f fails, telling you it's missing n. We can provide it with apply f with 3 or apply f with (n := 2) to be explicit about the argument being provided.

Goal forall P, (forall n m, P n -> P m) -> P 10.forall P : nat -> Type, (forall n m : nat, P n -> P m) -> P 10
Proof.forall P : nat -> Type, (forall n m : nat, P n -> P m) -> P 10
  intros P f.P: nat -> Type
f: forall n m : nat, P n -> P m
P 10
  Fail apply f.The command has indeed failed with message:
Unable to find an instance for the variable n.
P: nat -> Type
f: forall n m : nat, P n -> P m
P 10
  apply f with 3.P: nat -> Type
f: forall n m : nat, P n -> P m
P 3
  apply f with (n := 2).P: nat -> Type
f: forall n m : nat, P n -> P m
P 2
Abort.

`assumption`

Usage: assumption.

Concludes the goal if one of the assumptions matches it exactly.

Goal forall P Q R, (P -> Q -> R) -> P /\ Q -> R.forall (P Q : Prop) (R : Type), (P -> Q -> R) -> P /\ Q -> R
Proof.forall (P Q : Prop) (R : Type), (P -> Q -> R) -> P /\ Q -> R
  intros P Q R hPQR [hP hQ].P, Q: Prop
R: Type
hPQR: P -> Q -> R
hP: P
hQ: Q
R
  apply hPQR.P, Q: Prop
R: Type
hPQR: P -> Q -> R
hP: P
hQ: Q
P
P, Q: Prop
R: Type
hPQR: P -> Q -> R
hP: P
hQ: Q
Q
  -P, Q: Prop
R: Type
hPQR: P -> Q -> R
hP: P
hQ: Q
P assumption.
  -P, Q: Prop
R: Type
hPQR: P -> Q -> R
hP: P
hQ: Q
Q assumption.
Abort.

`left`

Usage: left.

Lets you prove a goal of the form A \/ B by requiring you to prove A instead.

Goal forall A B, A \/ B.forall A B : Prop, A \/ B
Proof.forall A B : Prop, A \/ B
  intros A B.A, B: Prop
A \/ B
  left.A, B: Prop
A
Abort.

Note

It actually applies to any inductive type with two constructors, left choosing the first constructor.

Goal bool * (nat + bool).bool * (nat + bool)
Proof.bool * (nat + bool)
  split.bool
nat + bool
  -bool left.
  -nat + bool left.nat
    left.
Abort.

`right`

Usage: right.

Lets you prove a goal of the form A \/ B by requiring you to prove B instead. Basically the same as left, but going right instead.

Goal forall A B, A \/ B.forall A B : Prop, A \/ B
Proof.forall A B : Prop, A \/ B
  intros A B.A, B: Prop
A \/ B
  right.A, B: Prop
B
Abort.

`exfalso`

Usage: exfalso.

Replaces the current goal with False, using the ex falso quod libet principle, also known as principle of explosion: you can deduce anything from False.

Goal forall P Q, P -> ~ P -> Q.forall (P : Prop) (Q : Type), P -> ~ P -> Q
Proof.forall (P : Prop) (Q : Type), P -> ~ P -> Q
  intros P Q hP hnP.P: Prop
Q: Type
hP: P
hnP: ~ P
Q
  exfalso.P: Prop
Q: Type
hP: P
hnP: ~ P
False
Abort.

`simpl`

Usage: simpl.

Performs computation in the current goal to "simplify" it (in some sense).

Goal forall P, P 10 -> P (4 + 6).forall P : nat -> Type, P 10 -> P (4 + 6)
Proof.forall P : nat -> Type, P 10 -> P (4 + 6)
  intros P hP.P: nat -> Type
hP: P 10
P (4 + 6)
  simpl.P: nat -> Type
hP: P 10
P 10
Abort.

Variant: simpl in h, where h is an assumption.

Goal forall P, P (7 + 3) -> P 10.forall P : nat -> Type, P (7 + 3) -> P 10
Proof.forall P : nat -> Type, P (7 + 3) -> P 10
  intros P hP.P: nat -> Type
hP: P (7 + 3)
P 10
  simpl in hP.P: nat -> Type
hP: P 10
P 10
Abort.

Tip

You may in fact use simpl in more than one hypothesis at the same time, by separating them by commas.

Goal forall P, P (2 + 2) -> P (4 + 8) -> True.forall P : nat -> Type, P (2 + 2) -> P (4 + 8) -> True
Proof.forall P : nat -> Type, P (2 + 2) -> P (4 + 8) -> True
  intros P h4 h12.P: nat -> Type
h4: P (2 + 2)
h12: P (4 + 8)
True
  simpl in h4, h12.P: nat -> Type
h4: P 4
h12: P 12
True
Abort.

Variant: simpl in *.

Simplifies all hypotheses and the goal at once.

Goal forall P, P (2 + 2) -> P (4 + 8) -> P (27 + 5).forall P : nat -> Type, P (2 + 2) -> P (4 + 8) -> P (27 + 5)
Proof.forall P : nat -> Type, P (2 + 2) -> P (4 + 8) -> P (27 + 5)
  intros P h4 h12.P: nat -> Type
h4: P (2 + 2)
h12: P (4 + 8)
P (27 + 5)
  simpl in *.P: nat -> Type
h4: P 4
h12: P 12
P 32
Abort.

Variant: simpl n, where n is a constant name.

Perform computation only for n.

Goal (10 + 2) - (3 + 5) = 19.10 + 2 - (3 + 5) = 19
Proof.10 + 2 - (3 + 5) = 19
  simpl "+".12 - 8 = 19
Abort.

`reflexivity`

Usage: reflexivity.

Prove goals of the shape t = t, it thus corresponds to reflexivity of equality.

Tip

It works up to computation (simpl) and up to introductions (intros).

Goal forall n, n > 0 -> n = 0 + n.forall n : nat, n > 0 -> n = 0 + n
Proof.forall n : nat, n > 0 -> n = 0 + n
  reflexivity.
Abort.

`f_equal`

Usage: f_equal.

Turns a goal of the shape f x y … z = f x' y' … z' into x = x', y = y' and z = z'.

Goal forall A B C D (f : A -> B -> C -> D) x y z x' y' z', f x y z = f x' y' z'.forall (A B C D : Type) (f : A -> B -> C -> D) (x : A) 
  (y : B) (z : C) (x' : A) (y' : B) (z' : C),
f x y z = f x' y' z'
Proof.forall (A B C D : Type) (f : A -> B -> C -> D) (x : A) 
  (y : B) (z : C) (x' : A) (y' : B) (z' : C),
f x y z = f x' y' z'
  intros A B C D f x y z x' y' z'.A, B, C, D: Type
f: A -> B -> C -> D
x: A
y: B
z: C
x': A
y': B
z': C
f x y z = f x' y' z'
  f_equal.A, B, C, D: Type
f: A -> B -> C -> D
x: A
y: B
z: C
x': A
y': B
z': C
x = x'
A, B, C, D: Type
f: A -> B -> C -> D
x: A
y: B
z: C
x': A
y': B
z': C
y = y'
A, B, C, D: Type
f: A -> B -> C -> D
x: A
y: B
z: C
x': A
y': B
z': C
z = z'
Abort.

Caution!

There is a lemma from the standard library called f_equal too. It is very related, but you mustn't confuse the two.

About f_equal.f_equal : forall [A B : Type] (f : A -> B) [x y : A], x = y -> f x = f y

f_equal is not universe polymorphic
Arguments f_equal [A B]%_type_scope f%_function_scope [x y] _
f_equal is transparent
Expands to: Constant Corelib.Init.Logic.f_equal
Declared in library Corelib.Init.Logic, line 445, characters 12-19

`induction`

Usage: induction t as p.

This works a bit like destruct except that it uses the induction principle corresponding to the type of t and additionally gives induction hypotheses in the recursive cases. The intropattern p must also name said induction hypotheses.

Goal forall n, n + 0 = n.forall n : nat, n + 0 = n
Proof.forall n : nat, n + 0 = n
  intros n.n: nat
n + 0 = n
  induction n as [| m ih].0 + 0 = 0
m: nat
ih: m + 0 = m
S m + 0 = S m
  -0 + 0 = 0 reflexivity.
  -m: nat
ih: m + 0 = m
S m + 0 = S m cbn.m: nat
ih: m + 0 = m
S (m + 0) = S m f_equal.m: nat
ih: m + 0 = m
m + 0 = m apply ih.
Abort.

Variant: induction t as p in x, y, …, z |- *, where x, y, …, z is a comma-separated sequence of assumptions (in the context) to generalise over.

It works like induction above but produce a stronger induction hypothesis by generalising over the listed constants.

Lemma mult_distr n m k :
  k * (n + m) = k * n + k * m.n, m, k: nat
k * (n + m) = k * n + k * m
Proof.n, m, k: nat
k * (n + m) = k * n + k * m
  induction k as [| k ihk] in n, m |- *.n, m: nat
0 * (n + m) = 0 * n + 0 * m
n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
S k * (n + m) = S k * n + S k * m
  -n, m: nat
0 * (n + m) = 0 * n + 0 * m simpl.n, m: nat
0 = 0 reflexivity.
  - (* ihk generalises over `n` and `m`. *)n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
S k * (n + m) = S k * n + S k * m
Abort.

Advanced variant: induction t as p using ind.

Performs induction using a custom induction principle provided by ind.

From Stdlib Require Import Lia.

Lemma nat_ind_2 :
  forall (P : nat -> Prop),
    P 0 ->
    P 1 ->
    (forall n, P n -> P (S n) -> P (S (S n))) ->
    forall n, P n.forall P : nat -> Prop,
P 0 ->
P 1 -> (forall n : nat, P n -> P (S n) -> P (S (S n))) -> forall n : nat, P n
Proof.forall P : nat -> Prop,
P 0 ->
P 1 -> (forall n : nat, P n -> P (S n) -> P (S (S n))) -> forall n : nat, P n
  intros P h0 h1 hSS n.P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
P n
  assert (h : P n /\ P (S n)).P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
P n /\ P (S n)
P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
h: P n /\ P (S n)
P n
  {P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
P n /\ P (S n) induction n as [| n [ih1 ih2]].P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
P 0 /\ P 1
P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
ih1: P n
ih2: P (S n)
P (S n) /\ P (S (S n))
    -P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
P 0 /\ P 1 split.P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
P 0
P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
P 1 all: assumption.
    -P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
ih1: P n
ih2: P (S n)
P (S n) /\ P (S (S n)) split.P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
ih1: P n
ih2: P (S n)
P (S n)
P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
ih1: P n
ih2: P (S n)
P (S (S n))
      +P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
ih1: P n
ih2: P (S n)
P (S n) assumption.
      +P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
ih1: P n
ih2: P (S n)
P (S (S n)) apply hSS.P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
ih1: P n
ih2: P (S n)
P n
P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
ih1: P n
ih2: P (S n)
P (S n) all: assumption.
  }P: nat -> Prop
h0: P 0
h1: P 1
hSS: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
h: P n /\ P (S n)
P n
  apply h.
Qed.

Fixpoint fib n : nat :=
  match n with
  | 0 | 1 => 1
  | S (S n as m) => fib m + fib n
  end.

Lemma fib_superlinear n :
  n <= fib n.n: nat
n <= fib n
Proof.n: nat
n <= fib n
  induction n as [| | n hn hSn] using nat_ind_2.0 <= fib 0
1 <= fib 1
n: nat
hn: n <= fib n
hSn: S n <= fib (S n)
S (S n) <= fib (S (S n))
  -0 <= fib 0 simpl.0 <= 1 lia.
  -1 <= fib 1 simpl.1 <= 1 lia.
  -n: nat
hn: n <= fib n
hSn: S n <= fib (S n)
S (S n) <= fib (S (S n)) change (fib (S (S n))) with (fib (S n) + fib n).n: nat
hn: n <= fib n
hSn: S n <= fib (S n)
S (S n) <= fib (S n) + fib n
    destruct n.hn: 0 <= fib 0
hSn: 1 <= fib 1
2 <= fib 1 + fib 0
n: nat
hn: S n <= fib (S n)
hSn: S (S n) <= fib (S (S n))
S (S (S n)) <= fib (S (S n)) + fib (S n)
    +hn: 0 <= fib 0
hSn: 1 <= fib 1
2 <= fib 1 + fib 0 simpl.hn: 0 <= fib 0
hSn: 1 <= fib 1
2 <= 2 lia.
    +n: nat
hn: S n <= fib (S n)
hSn: S (S n) <= fib (S (S n))
S (S (S n)) <= fib (S (S n)) + fib (S n) lia.
Qed.

`rewrite`

Usage: rewrite t, where t is a term (for instance lemma or assumption).

Assuming t is a (possibly universally quantified) equality lhs = rhs, replaces occurrences of lhs in the goal by rhs.

Goal forall A P (a b : A), a = b -> P b -> P a.forall (A : Type) (P : A -> Type) (a b : A), a = b -> P b -> P a
Proof.forall (A : Type) (P : A -> Type) (a b : A), a = b -> P b -> P a
  intros A P a b e h.A: Type
P: A -> Type
a, b: A
e: a = b
h: P b
P a
  rewrite e.A: Type
P: A -> Type
a, b: A
e: a = b
h: P b
P b
Abort.

Variant: rewrite <- t.

Similar, but replaces rhs by lhs instead.

Goal forall A P (a b : A), a = b -> P a -> P b.forall (A : Type) (P : A -> Type) (a b : A), a = b -> P a -> P b
Proof.forall (A : Type) (P : A -> Type) (a b : A), a = b -> P a -> P b
  intros A P a b e h.A: Type
P: A -> Type
a, b: A
e: a = b
h: P a
P b
  rewrite <- e.A: Type
P: A -> Type
a, b: A
e: a = b
h: P a
P a
Abort.

Variant: rewrite t in h, where h is an assumption.

Similarly, but the replacement is done in h.

Goal forall A P (a b : A), a = b -> P a -> P b.forall (A : Type) (P : A -> Type) (a b : A), a = b -> P a -> P b
Proof.forall (A : Type) (P : A -> Type) (a b : A), a = b -> P a -> P b
  intros A P a b e h.A: Type
P: A -> Type
a, b: A
e: a = b
h: P a
P b
  rewrite e in h.A: Type
P: A -> Type
a, b: A
e: a = b
h: P b
P b
Abort.

Tip

You can also use it with <- and with a list of assumptions, including the goal itself. See below.

Lemma foo A P Q R (a b : A) (e : a = b) (p : P a) (q : Q a b) : R a b.A: Type
P: A -> Type
Q, R: A -> A -> Type
a, b: A
e: a = b
p: P a
q: Q a b
R a b
Proof.A: Type
P: A -> Type
Q, R: A -> A -> Type
a, b: A
e: a = b
p: P a
q: Q a b
R a b
  rewrite e in p, q.A: Type
P: A -> Type
Q, R: A -> A -> Type
a, b: A
e: a = b
p: P b
q: Q b b
R a b
  rewrite <- e in p, q |- *.A: Type
P: A -> Type
Q, R: A -> A -> Type
a, b: A
e: a = b
p: P a
q: Q a a
R a a
Abort.

Variant: rewrite rs, where rs is a list of rewrites such as t or <- t.

Performs several rewrites in succession.

Lemma foo X P (a b c : X) (e : a = b) (e' : c = b) : P a.X: Type
P: X -> Type
a, b, c: X
e: a = b
e': c = b
P a
Proof.X: Type
P: X -> Type
a, b, c: X
e: a = b
e': c = b
P a
  rewrite e, <- e'.X: Type
P: X -> Type
a, b, c: X
e: a = b
e': c = b
P c
Abort.

Variant: rewrite !t.

Rewrites using t several times in a row until it no longer can.

Lemma reassoc X (a b c d e f : list X) :
  a ++ b ++ c ++ d ++ e ++ f = ((((a ++ b) ++ c) ++ d) ++ e) ++ f.X: Type
a, b, c, d, e, f: list X
a ++ b ++ c ++ d ++ e ++ f = ((((a ++ b) ++ c) ++ d) ++ e) ++ f
Proof.X: Type
a, b, c, d, e, f: list X
a ++ b ++ c ++ d ++ e ++ f = ((((a ++ b) ++ c) ++ d) ++ e) ++ f
  rewrite app_assoc.X: Type
a, b, c, d, e, f: list X
(a ++ b) ++ c ++ d ++ e ++ f = ((((a ++ b) ++ c) ++ d) ++ e) ++ f
  rewrite 2!app_assoc.X: Type
a, b, c, d, e, f: list X
(((a ++ b) ++ c) ++ d) ++ e ++ f = ((((a ++ b) ++ c) ++ d) ++ e) ++ f
  rewrite !app_assoc.X: Type
a, b, c, d, e, f: list X
((((a ++ b) ++ c) ++ d) ++ e) ++ f = ((((a ++ b) ++ c) ++ d) ++ e) ++ f
  reflexivity.
Qed.

`specialize`

Usage: specialize (h u v … w), where h is an assumption, and u, v, … w are terms.

Replaces hypothesis h with its instantiation with the provided arguments.

Lemma foo X Y Z A (h : X -> Y -> Z -> A) : X -> (Y -> Z) -> Y -> A.X, Y, Z, A: Type
h: X -> Y -> Z -> A
X -> (Y -> Z) -> Y -> A
Proof.X, Y, Z, A: Type
h: X -> Y -> Z -> A
X -> (Y -> Z) -> Y -> A
  intros x z y.X, Y, Z, A: Type
h: X -> Y -> Z -> A
x: X
z: Y -> Z
y: Y
A
  specialize (h x).X, Y, Z, A: Type
h: Y -> Z -> A
x: X
z: Y -> Z
y: Y
A
  specialize (z y).X, Y, Z, A: Type
h: Y -> Z -> A
x: X
z: Z
y: Y
A
  specialize (h y z).X, Y, Z, A: Type
h: A
x: X
z: Z
y: Y
A
Abort.

Variant: specialize (h u v … w) as g, where g is a new name.

Produce a new hypothesis g corresponding to the instantiation of h with the provided arguments. h is left unchanged.

Lemma foo X Y Z A (h : X -> Y -> Z -> A) : X -> (Y -> Z) -> Y -> A.X, Y, Z, A: Type
h: X -> Y -> Z -> A
X -> (Y -> Z) -> Y -> A
Proof.X, Y, Z, A: Type
h: X -> Y -> Z -> A
X -> (Y -> Z) -> Y -> A
  intros x z y.X, Y, Z, A: Type
h: X -> Y -> Z -> A
x: X
z: Y -> Z
y: Y
A
  specialize (h x) as h'.X, Y, Z, A: Type
h: X -> Y -> Z -> A
x: X
z: Y -> Z
y: Y
h': Y -> Z -> A
A
  specialize (z y) as z'.X, Y, Z, A: Type
h: X -> Y -> Z -> A
x: X
z: Y -> Z
y: Y
h': Y -> Z -> A
z': Z
A
  specialize (h' y z').X, Y, Z, A: Type
h: X -> Y -> Z -> A
x: X
z: Y -> Z
y: Y
h': A
z': Z
A
Abort.

Variant: specialize (h u v … w) as p, where p is an intropattern.

Behaves like specialize (h u v … w) followed by destruct h as p.

Lemma foo (h : nat -> nat) : nat.h: nat -> nat
nat
Proof.h: nat -> nat
nat
  specialize (h 12) as [| m].nat
m: nat
nat
Abort.

`exists`

Usage: exists t, where t is a term.

Applies to goals for the form exists x, P x and replaces it with goal P t.

Goal exists n, n = 0.exists n : nat, n = 0
Proof.exists n : nat, n = 0
  exists 0.0 = 0
Abort.

Variant: exists u,v,w taking a list of terms.

Works like a succession of exists: exists u then exists v then existts w.

Goal exists a b c, a + b = b + c.exists a b c : nat, a + b = b + c
Proof.exists a b c : nat, a + b = b + c
  exists 1, 2, 3.1 + 2 = 2 + 3
Abort.

`symmetry`

Usage: symmetry.

Applies to a goal of the form u = v and replaces it with goal v = u, exploiting the fact that equality is symmetric.

Goal forall A (u v : A), u = v.forall (A : Type) (u v : A), u = v
Proof.forall (A : Type) (u v : A), u = v
  intros A u v.A: Type
u, v: A
u = v
  symmetry.A: Type
u, v: A
v = u
Abort.

Variant: symmetry in h, where h is an hypothesis.

Applies symmetry to hypothesis h.

Lemma foo A (u v : A) (e : u = v) : v = u.A: Type
u, v: A
e: u = v
v = u
Proof.A: Type
u, v: A
e: u = v
v = u
  symmetry in e.A: Type
u, v: A
e: v = u
v = u
Abort.

`assert`

Usage: assert (h : P) or equivalently assert (P) as h, where P is a statement (or type) and h is name of your choice.

When the goal is G, yield two goals: a first one where you have to prove P in the same context, and one where you prove G but with extra hypothesis h : P.

Lemma foo (P Q : Prop) :
  (P -> ~ P) -> False.P, Q: Prop
(P -> ~ P) -> False
Proof.P, Q: Prop
(P -> ~ P) -> False
  intros h.P, Q: Prop
h: P -> ~ P
False
  assert (nP : ~ P).P, Q: Prop
h: P -> ~ P
~ P
P, Q: Prop
h: P -> ~ P
nP: ~ P
False
  {P, Q: Prop
h: P -> ~ P
~ P intros p.P, Q: Prop
h: P -> ~ P
p: P
False apply h.P, Q: Prop
h: P -> ~ P
p: P
P
P, Q: Prop
h: P -> ~ P
p: P
P all: assumption. }P, Q: Prop
h: P -> ~ P
nP: ~ P
False
Abort.

`unfold`

Usage: unfold d where d is the name of a definition.

Replaces occurrences of d in the goal with its definition. It works both for global definitions (such as defined with Definition) and for local definitions (stemming for a let).

Definition test x := x + x.

Lemma foo :
  let bar := test 0 + test 1 in
  bar + test 2 = test 3.let bar := test 0 + test 1 in bar + test 2 = test 3
Proof.let bar := test 0 + test 1 in bar + test 2 = test 3
  intros bok.bok:= test 0 + test 1: nat
bok + test 2 = test 3
  unfold test.bok:= test 0 + test 1: nat
bok + (2 + 2) = 3 + 3
  unfold bok.bok:= test 0 + test 1: nat
test 0 + test 1 + (2 + 2) = 3 + 3
Abort.

Variant: unfold d in h where h is an hypothesis.

Unfold definition d inside h.

Lemma foo :
  let bar := test 0 + test 1 in
  bar + test 2 = test 3.let bar := test 0 + test 1 in bar + test 2 = test 3
Proof.let bar := test 0 + test 1 in bar + test 2 = test 3
  intros bok.bok:= test 0 + test 1: nat
bok + test 2 = test 3
  unfold test in bok.bok:= 0 + 0 + (1 + 1): nat
bok + test 2 = test 3
Abort.

`contradiction`

Usage: contradiction.

Concludes the goal by finding obviously contradicting hypotheses such as P and ~ P.

Goal forall P, P -> ~ P -> bool.forall P : Prop, P -> ~ P -> bool
Proof.forall P : Prop, P -> ~ P -> bool
  intros P h hn.P: Prop
h: P
hn: ~ P
bool
  contradiction.
Abort.

Tip

It also works if you do not introduce the contradicting hypotheses.

Goal forall P, P -> ~ P -> bool.forall P : Prop, P -> ~ P -> bool
Proof.forall P : Prop, P -> ~ P -> bool
  contradiction.
Abort.

`lia`

Usage: lia.

Solves a goal that involves linear integer arithmetic (essentially addition and multiplication by a constant, equality and inequality). This is a decidable theory, so its output is predictable and reliable: the best kind of automation.

Note

To use it you need to have the Lia module loaded.

From Stdlib Require Import Lia.

Lemma foo n m k :
  n = 2 * k ->
  m = k + 1 ->
  m < 2 + n.n, m, k: nat
n = 2 * k -> m = k + 1 -> m < 2 + n
Proof.n, m, k: nat
n = 2 * k -> m = k + 1 -> m < 2 + n
  lia.
Abort.

Tip

It also applies to conclude False from inconsistent assumptions.

Lemma foo n m k :
  n = 2 * k ->
  m < k ->
  m > n ->
  False.n, m, k: nat
n = 2 * k -> m < k -> m > n -> False
Proof.n, m, k: nat
n = 2 * k -> m < k -> m > n -> False
  lia.
Abort.

`change`

Usage: change t, where t is a term.

Replaces the whole goal with t, provided the goal and t are convertible: that is, equal up to computation.

Goal true <> false.true <> false
Proof.true <> false
  intros h.h: true = false
False
  change (if true then False else True).h: true = false
if true then False else True
Abort.

Variant change t in h, where h is an hypothesis.

Replaces the type of h with t if they are convertible.

Goal forall P n, P n -> P (0 + n).forall (P : nat -> Type) (n : nat), P n -> P (0 + n)
Proof.forall (P : nat -> Type) (n : nat), P n -> P (0 + n)
  intros P n h.P: nat -> Type
n: nat
h: P n
P (0 + n)
  change (P (0 + n)) in h.P: nat -> Type
n: nat
h: P (0 + n)
P (0 + n)
Abort.

Variant change t with u, where u is a term.

In the goal, replaces occurrences of t with u, assuming they are convertible.

Goal forall P a b c, P (a + b) (S b) (c * a).forall (P : nat -> nat -> nat -> Type) (a b c : nat), P (a + b) (S b) (c * a)
Proof.forall (P : nat -> nat -> nat -> Type) (a b c : nat), P (a + b) (S b) (c * a)
  intros P a b c.P: nat -> nat -> nat -> Type
a, b, c: nat
P (a + b) (S b) (c * a)
  pose (f := fun x => 0 + x).P: nat -> nat -> nat -> Type
a, b, c: nat
f:= fun x : nat => 0 + x: nat -> nat
P (a + b) (S b) (c * a)
  change a with (f a).P: nat -> nat -> nat -> Type
a, b, c: nat
f:= fun x : nat => 0 + x: nat -> nat
P (f a + b) (S b) (c * f a)
Abort.

`discriminate`

Usage: discriminate.

Closes a goal that assumes an equality between different constructors of an inductive type.

Goal true <> false.true <> false
Proof.true <> false
  discriminate.
Abort.

Variant: discriminate h where h is an hypothesis.

Instructs discriminate that the inconsistent equality is h.

Lemma foo A (e : true = false) : A.A: Type
e: true = false
A
Proof.A: Type
e: true = false
A
  discriminate e.
Abort.

`inversion`

`congruence`

`constructor`

Usage: constructor.

Applies the first constructor that applies to the current goal.

Definition abool : bool.bool
Proof.bool
  constructor.
Defined.

Print abool. (* true *)abool = true
     : bool

Variant: constructor n where n is a numeral (a concrete natural number).

Applies the n-th constructor corresponding to the goal.

Definition another : bool.bool
Proof.bool
  constructor 2.
Defined.

Print another. (* false *)another = false
     : bool

Important

The constructor version is one of those tactics that have several successes, which is relevant when using backtracking. If the constructor it picked leads to a failure in a subsequent step, it will backtrack and pick the next constructor that applies, until it exhausts them or succeed.

The example below already uses semicolon (;), unshelve and eexists, explained later.

Goal exists b, b = false.exists b : bool, b = false
Proof.exists b : bool, b = false
  unshelve eexists ; constructor.
  Show Proof. (* It picked `false`. *)(ex_intro (fun b : bool => b = false) false eq_refl)
Abort.

Tactic index

`intro`

`split`

`destruct`

`intros`

`apply`

`assumption`

`left`

`right`

`exfalso`

`simpl`

`reflexivity`

`f_equal`

`induction`

`rewrite`

`specialize`

`exists`

`symmetry`

`assert`

`unfold`

`contradiction`

`lia`

`change`

`discriminate`

`inversion`

`congruence`

`constructor`

`generalize`

`enough`

`clear`

`cbn`

`tac1 ; tac2`

`remember`

`subst`

`revert`

`replace`

`eapply`

`eexists`

`econstructor`

`unshelve`