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 facts 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.

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 seprating 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.

`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 to inductive types 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: exfalso.

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 musn'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.

`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.

`specialize`

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

Replaces hyopthesis 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.