The first time I heard Coq was in college. Since then I always wanted to learn Coq but didn’t know how to. Lots ofhypotheses the tutorials are about logic, which doesn’t seem interesting to me.

I took UW CSE505 last quarter. Prof. Zach Tatlock and the TA Talia Ringer made some wonderful homework to help us learn Coq. While in this course, we proved more practical things, like a programming language interpreter and a regular expression matcher. I actually found myself feeling quite good about proving things in Coq (writing specifications is a completely different other thing), at least when doing homework.

If you are teaching yourself Coq, I’d suggest the following resources:

• Homework of UW CSE505
• Formal Reasoning About Programs is the textbook we used in class. It’s a short textbook with big margins and lots of whitespaces. It comes with detailed Coq code for each chapter and a very powerful Coq library `frap`.
• Software Foundations is the material for you if you are really into verification.

I’m quite happy that I completed Coq in my wish list. But I’m not a huge believer of machine-checked proof or verification. Before I fully forgot Coq, let me write down some beginner-level tricks I learned when doing homework, just in case you might find it useful or I come back to Coq some decades later.

## Tactics

Although I cannot understand most part of it, the Coq manual can still be your best friend: https://coq.inria.fr/refman/coq-tacindex.html.

### `intros`

`intros` introduces hypotheses in order, from the goal. Each time it consumes a free variable in `forall` or a proposition before `->` (a precondition). For example,

``````Theorem Transform_transform:
forall c1 c2,
Transform c1 c2 ->
transform c1 = c2.
``````

After `intros c1 c2 H.`:

``````c1, c2 : cmd
H : Transform c1 c2
______________________________________(1/1)
transform c1 = c2
``````

Alternatively, `intros.` introduces everything and name them automatically.

### `simpl`

`simpl.` simplifies the goal. `simpl in H.` simplifies hypothesis `H`. `simpl in *.` simplifies all hypotheses and the goal. When you don’t know what to do, try `simpl in *.`, then see if anything happens.

### `simplify` (Frap Tactic)

`simplify.` is a stronger version of `simpl in *.` from the `frap` library. I prefer `simplify` to `simpl` if possible.

### `destruct`

When you `destruct x.` where `x` is an inductive type, Coq generates a subgoal for each constructor. In other words, `destruct` gives you the ability to discuss all possible cases.

Let’s first look at a simple example. Suppose we have such a inductive type:

``````Inductive cmd :=
| Skip
| Assign (x : var) (e : arith)
| Sequence (c1 c2 : cmd)
| If (e : arith) (then_ else_ : cmd)
| While (e : arith) (body : cmd).
``````

And we would like to prove:

``````Theorem transform_Transform:
forall c1 c2,
transform c1 = c2 ->
Transform c1 c2.
``````

If we `destruct c2.`, we’ll have `c2` replaced with each constructor:

``````5 subgoals
c1 : cmd
______________________________________(1/5)
transform c1 = Skip -> Transform c1 Skip
______________________________________(2/5)
transform c1 = (Assign x e) -> Transform c1 (Assign x e)
______________________________________(3/5)
transform c1 = (Sequence c2_1 c2_2) -> Transform c1 (Sequence c2_1 c2_2)
______________________________________(4/5)
transform c1 = (If e c2_1 c2_2) -> Transform c1 (If e c2_1 c2_2)
______________________________________(5/5)
transform c1 = (While e c2) -> Transform c1 (While e c2)
``````

Notice that, lots of things are actually inductive types, which means you can you `destruct` to open them. Another example:

``````H : exists a : Set, In a (wl ++ adjacent t g) /\ Reachable g a b
``````

Now that hypothesis `H` tells us there is an `a` satisfying the proposition, how do we get that witness out of the existential quantification? If we turn off the notation display, we can see that `H` is actually

``````H : ex (fun a : Set => and (In a (app wl (adjacent t g))) (Reachable g a b))
``````

And if you `Print ex.`:

``````Inductive ex (A : Type) (P : forall _ : A, Prop) : Prop :=
ex_intro : forall (x : A) (_ : P x), ex P
``````

`ex` is an inductive type! Therefore, we can use `destruct H.` to get the witness:

``````x : Set
H : In x (wl ++ adjacent t g) /\ Reachable g x b
``````

Now we have the witness, although it’s called `x` instead of `a`. And how do we break the `/\`? `destruct H.` again!

``````x : Set
H : In x (wl ++ adjacent t g)
H1 : Reachable g x b
``````

This is because `and` is also an inductive type! Check it with `Print and.`:

``````Inductive and (A B : Prop) : Prop :=
| conj : A -> B -> A /\ B.
``````

What about `\/` then? `Print or.`:

``````Inductive or (A B : Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B.
``````

Therefore, when you `destruct` a `\/`, it becomes two subgoals. This makes sense. Logically, when you know `A \/ B` is true, you need to discuss two cases: `A` is true and `B` is true.

### `induction`

`induction` is one of the most important tactics to prove things. You can `induction` on an inductive type. There are usually as many subgoals as the constructors of the inductive type. If a constructor calls another of the same inductive type, there will be a induction hypothesis for that.

At first, I confused `induction` with mathematical induction. To prove a proposition `P` using mathematical induction, you first prove a base case `P(0)` and then prove a induction step `P(n+1)` given that `P(n)` holds. But there is no “base case” or “induction step” in `induction` and the number of cases is not necessarily two, depending on the inductive type.

Later, I found that you can think of `induction` as a generalization of mathematical induction. Mathematical induction works on natrual numbers, which is a recursive-defined inductive type:

``````Inductive nat : Set :=
| O : nat
| S : nat -> nat.
``````

Therefore, when you `induction` on a `nat`, it’s exactly mathematical induction. On the other hand, you can think of `induction` working generally on structures.

Let’s first look at a simple example:

``````Lemma len_repeat:
forall s n,
String.length (repeat s n) = n * String.length s.
``````

When `induction` an variable, Coq `intros` until that variable appears. So, we can directly `induction n.`, which has the same effect as `intros s n. induction n.`.

``````s : var
______________________________________(1/2)
String.length (repeat s 0) = 0 * String.length s
______________________________________(2/2)
String.length (repeat s (S n)) = S n * String.length s
``````

You can see there are two cases. One is `0` and one is `S n`. Notice that there are no induction hypothesis in the first case, because `O` is not recursively defined. Once you finishes the first case, we’ll have the second case:

``````s : var
n : nat
IHn : String.length (repeat s n) = n * String.length s
______________________________________(1/1)
String.length (repeat s (S n)) = S n * String.length s
``````

Since `S` is recursively defined, there is an induction hypothesis `IHn`.

Let’s look at another example:

``````Inductive Transform  : cmd -> cmd -> Prop :=
| TransformSkip:
Transform Skip Skip
| TransformAssign: forall v e,
Transform (Assign v e) (Assign v e)
| TransformSeq: forall c1 c2 tc1 tc2,
Transform c1 tc1 ->
Transform c2 tc2 ->
Transform (Sequence c1 c2) (Sequence tc1 tc2)
| TransformIf: forall e then_ else_ tthen telse,
Transform then_ tthen ->
Transform else_ telse ->
Transform (If e then_ else_) (If e telse tthen)
| TransformWhile: forall e body tbody,
Transform body tbody ->
Transform (While e body) (While e tbody).

Theorem Transform_transform:
forall c1 c2,
Transform c1 c2 ->
transform c1 = c2.
``````

We can start the proof with `induction 1`. `induction n.` keeps `intros`-ing until the `n`th proposition in the theorem comes out and then inducts on that proposition. In this case, `induction 1` is the same as `intros c1 c2 H. induction H.`. Then we got

``````5 subgoals
______________________________________(1/5)
transform Skip = Skip
______________________________________(2/5)
transform (Assign v e) = Assign v e
______________________________________(3/5)
transform (Sequence c1 c2) = Sequence tc1 tc2
______________________________________(4/5)
transform (If e then_ else_) = If e telse tthen
______________________________________(5/5)
transform (While e body) = While e tbody
``````

There is one subgoal for each `Transform` constructor. Let’s focus on the 4th subgoal:

``````e : arith
then_, else_, tthen, telse : cmd
H : Transform then_ tthen
H0 : Transform else_ telse
IHTransform1 : transform then_ = tthen
IHTransform2 : transform else_ = telse
______________________________________(1/1)
transform (If e then_ else_) = If e telse tthen
``````

We can see that there are two induction hypotheses (`IHTransform1` and `IHTransform2`) because the constructor `TransformIf` has two recursively defined preconditions.

### `inversion`

In my opinion, `inversion` is one of the most powerful and most frequent-used tactics. The way I understand `inversion H.` is that it asks Coq to figure out what else need to be true to make `H` true, where `H` is an inductive type. It might add more propositions to the hypotheses. It might also add more subgoals.

A common use case is that you have an equation of the same constructor of an inductive type in your hypotheses and you want to say that their corresponding parts must be equal. Another way to think of `inversion` is like “opening the box”. For example, `If` here is a constructor of an inductive type:

``````H : If e (transform c1_2) (transform c1_1) = If e0 c2_1 c2_2
______________________________________(1/1)
Transform (If e c1_1 c1_2) (If e0 c2_1 c2_2)
``````

After `inversion H.`:

``````H : If e (transform c1_2) (transform c1_1) = If e0 c2_1 c2_2
H1 : e = e0
H2 : transform c1_2 = c2_1
H3 : transform c1_1 = c2_2
______________________________________(1/1)
Transform (If e0 c1_1 c1_2) (If e0 (transform c1_2) (transform c1_1))

``````

Coq found some very useful relations for us. By the way, `inversion` works better with `subst` because it makes hypotheses clearer by substituting equations found by `inversion`. Also, if after `inversion H; subst.` you found the only changes to the hypotheses is a duplication of `H`, then you know `inversion H.` doesn’t help at all.

Actually, there is nothing special about `=` because it’s simply an inductive type called `eq`. Let’s look at a slightly more complicated example:

``````Inductive Transform  : cmd -> cmd -> Prop :=
| TransformSkip:
Transform Skip Skip
| TransformSeq: forall c1 c2 tc1 tc2,
Transform c1 tc1 ->
Transform c2 tc2 ->
Transform (Sequence c1 c2) (Sequence tc1 tc2)
| TransformIf: forall e then_ else_ tthen telse,
Transform then_ tthen ->
Transform else_ telse ->
Transform (If e then_ else_) (If e telse tthen)
(* Other constructors omitted *).

Inductive step_buggy : valuation * cmd -> valuation * cmd -> Prop :=
| StepBuggySeq1 : forall v c1 c2 v' c1',
step_buggy (v, c1) (v', c1')
-> step_buggy (v, Sequence c1 c2) (v', Sequence c1' c2)
| StepBuggySeq2 : forall v c2,
step_buggy (v, Sequence Skip c2) (v, c2)
(* Other constructors omitted *).
``````

And suppose that we have:

``````1 subgoal
v : valuation
c2, c1', c2' : cmd
H : Transform (Sequence Skip c2) c1'
H0 : step_buggy (v, c1') (v, c2')
______________________________________(1/1)
Transform c2 c2'
``````

After `inversion H; subst.`:

``````v : valuation
c2, c2', tc1, tc2 : cmd
H : Transform (Sequence Skip c2) (Sequence tc1 tc2)
H0 : step_buggy (v, (Sequence tc1 tc2)) (v, c2')
H3 : Transform Skip tc1
H5 : Transform c2 tc2
______________________________________(1/1)
Transform c2 c2'
``````

Let me explain what happened. `H` matches the `TransformSeq` constructor, therefore, we have two preconditions to be true (`H3` and `H5`) and from the constructor we know that `c1'` must also be a `Sequence`, thus `c1'` has been replaced with `(Sequence tc1 tc2)`. Now let’s `inversion H3; subst.`:

``````v : valuation
c2, c2', tc2 : cmd
H : Transform (Sequence Skip c2) (Sequence Skip tc2)
H0 : step_buggy (v, (Sequence Skip tc2)) (v, c2')
H3 : Transform Skip Skip
H5 : Transform c2 tc2
______________________________________(1/1)
Transform c2 c2'
``````

We can see that `tc1` has been replaced by `Skip` because to have `H3 : Transform Skip tc1` to be true, the only match is the `TransformSkip` constructor which says `tc1` is `Skip`. Now let’s `inversion H0; subst.`:

``````v : valuation
c2, tc2, c1' : cmd
H : Transform (Sequence Skip c2) (Sequence Skip tc2)
H0 : step_buggy (v, (Sequence Skip tc2)) (v, (Sequence c1' tc2))
H2 : step_buggy (v, Skip) (v, c1')
H3 : Transform Skip Skip
H5 : Transform c2 tc2
______________________________________(1/2)
Transform c2 (Sequence c1' tc2)
______________________________________(2/2)
Transform c2 c2'
``````

Because there are two `step_buggy` constructors that match `H0`, we need to discuss both cases, thus there are two subgoals. This case discussion is like `destruct`.

What if there is no any matching constructor? Let’s look a the following example:

``````H : None = Some true
``````

In this case, you can finish this case with `inversion H.` because what it says can never happen.

### `f_equal`

When the goal is an equation of the same constructor of an inductive type, you can use `f_equal.` to instead prove the corresponding parts to be equal. For example,

``````v : valuation
e : arith
body, tbody : cmd
______________________________________(1/1)
Sequence (transform body) (While e (transform body)) =
Sequence tbody            (While e tbody)
``````

and you run `f_equal.`, it becomes:

``````v : valuation
e : arith
body, tbody : cmd
______________________________________(1/2)
transform body = tbody
______________________________________(2/2)
While e (transform body) = While e tbody
``````

Obviously, if you run `f_equal.` on the second subgoal, it will further transform into:

``````______________________________________(1/1)
transform body = tbody
``````

Notice that, although `f_equal` can decompose the goal into smaller problems, make sure you know that the corresponding parts are truly equal. Let me give you an incorrect example:

``````s : var
______________________________________(1/1)
String.length (reverse s) = String.length s
``````

In this case, we would want to prove that the length of the reverse of a string equals the length of the original string. If we run `f_equal.` here:

``````s : var
______________________________________(1/1)
reverse s = s
``````

The resulting goal does not make sense at all (How can the reverse equal to the original one for an arbitrary string?).

### `assumption`

If the goal is already in the hypotheses, use `assumption.` to finish the proof. Alternatively, you can also use `auto` or `exact`.

### `constructor`

When the goal is a inductive type, the usual way to finish it is to build an instance of that inductive type by calling its constructor (maybe the only other way is to use some lemma?). `constructor.` will try each constructor of the inductive type in the order of the definition until one of them matches.

Since `constructor.` uses the first matched constructor, it might not be the correct one. In this case, you need to use `apply`.

A simple example: Let’s say we have this inductive type:

``````Inductive eval_unop : op1 -> val -> val -> Prop :=
| eval_neg : forall i,
eval_unop Oneg (Vint i) (Vint (Z.opp i))
| eval_not : forall b,
eval_unop Onot (Vbool b) (Vbool (negb b)).
``````

And now we have the following:

``````b : bool
v' : val
______________________________________(1/1)
eval_unop Onot (Vbool b) (Vbool (negb b))
``````

Then we run `consturctor.` and Coq will match the second constructor `eval_not`.

### `apply`

`apply` can also be used to apply constructors. In fact, you can `apply` any lemmas and you can think of constructors as lemmas. For example, in the previous `constructor` example, you can also `apply eval_not.` instead of `constructor.`

Let me walk you through `apply` using a slightly more complicated example. Let’s say we have this inductive type and a lemma:

``````Inductive eval_e (s : store) (h : heap) :
expr -> val -> Prop :=
(* Omitted *).

Inductive eval_s (env : env) :
store -> heap -> stmt -> store -> heap -> Prop :=
| eval_ifelse_t :
forall s h e p1 p2 s' h',
eval_e s h e (Vbool true)                  ->
eval_s  env  s h p1                  s' h' ->
eval_s  env  s h (Sifelse e p1 p2)   s' h'
| eval_ifelse_f :
forall s h e p1 p2 s' h',
eval_e s h e (Vbool false)                 ->
eval_s  env  s h p2                  s' h' ->
eval_s  env  s h (Sifelse e p1 p2)   s' h'
| eval_seq :
forall s1 h1 p1 s2 h2 p2 s3 h3,
eval_s  env  s1 h1 p1             s2 h2 ->
eval_s  env  s2 h2 p2             s3 h3 ->
eval_s  env  s1 h1 (Sseq p1 p2)   s3 h3.

Lemma interp_e_eval_e :
forall s h e v,
interp_e s h e = Some v ->
eval_e s h e v.
``````

And now we have the following:

``````IHfuel : forall (env : env) (s : store) (h : heap) (p : stmt) (s' : store) (h' : heap),
interp_s fuel env s h p = Some (s', h') ->
eval_s env s h p s' h'
Heqo : interp_e s h e = Some (Vbool true)
H : interp_s fuel env s h p1 = Some (s', h')
______________________________________(1/1)
eval_s env s h (Sifelse e p1 p2) s' h'
``````

There are some `->` in the constructors, which might seem scary if you are new to Coq, but once you understand the way `apply` and `constructor` work, it becomes easy.

In this case, we know we want the `eval_ifelse_t` constructor. How? First, look at the goal, which is a `eval_s`, so we need to look into the constructors of `eval_s`. How do we know it’s not `eval_seq`? Becase our goal doesn’t match `eval_seq` structurally. But `eval_ifelse_t` and `eval_ifelse_f` have exactly the same form `eval_s env s h (Sifelse e p1 p2) s' h'`. And how do we deal with the preconditions?

Logically, to use `eval_ifelse_t`, we need to prove its preconditions. In fact, if you run `constructor.` or `apply eval_ifelse_t.`, it will become two subgoals, which fits the logic, as what we expected:

``````______________________________________(1/2)
eval_e s h e (Vbool true)
______________________________________(2/2)
eval_s env s h p1 s' h'
``````

Note that the second subgoal is trivial. You can prove the second subgoal by `apply IHfuel. hypothesis.`. Let me go through this trivial case to strengthen your understanding of `apply`. The form of the last proposition in `IHfuel` (` eval_s env s h p s' h'`) matches the form of our second goal (`eval_s env s h p1 s' h'`). And notice that there is a `forall` in `IHfuel`. Coq can figure out what those free variables are when you `apply IHfuel.`. Thus the second subgoal becomes `interp_s fuel env s h p1 = Some (s', h')`, which is exactly `Heqo`.

I said the second subgoal is trivial because instead of `apply IHfuel. hypothesis.`, you can simply put an `auto.`. Even better, if you use `constructor; auto.` or `apply eval_ifelse_t; auto.` at the first place, Coq won’t even show you two subgoals.

And about the first subgoal, we can finish it by `apply interp_e_eval_e. hypothesis.`. Think about how this works. It’s the same.

Besides transforming the goal, `apply` can also work on hypotheses, adding `in H`. For example,

``````Theorem Transform_transform:
forall c1 c2,
Transform c1 c2 ->
transform c1 = c2.
``````

and given

``````H : Transform (Assign x e) c1'
``````

running `apply Transform_transform in H.` transforms `H` into:

``````H : transform (Assign x e) = c1'
``````

### `exists`

One way to prove an existential quantification is to tell Coq what exactly those variables are. For example,

``````H3 : String a s1 =~ EmptySet
H4 : s2 =~ re1
H0 : String a s1 ++ s2 = String a (s1 ++ s2)
______________________________________(1/1)
exists s0 s3 : string, s1 ++ s2 = s0 ++ s3 /\
(String a s0 =~ EmptySet) /\ s3 =~ re1
``````

We can tell Coq `exists s1, s2.`:

``````H3 : String a s1 =~ EmptySet
H4 : s2 =~ re1
H0 : String a s1 ++ s2 = String a (s1 ++ s2)
______________________________________(1/1)
s1 ++ s2 = s1 ++ s2 /\ (String a s1 =~ EmptySet) /\ s2 =~ re1
``````

Then a `first_order` finishes the proof.

### `reflexivity`

As the name suggests, when the goal is like `x = x`, use `reflexivity.`.

### `discriminate`

If there is an equation in the hypotheses that have structurally different left and right hand side, use `discriminate.` to finish the prove, no matter what the goal is, because a false hypothesis can imply anything. For example,

``````H : None = Some v'
______________________________________(1/1)
eval_unop Oneg (Vbool b) v'
``````

`discriminate.` gives you `Qed.` (or not yet, but finishes this subgoal).

Another example:

``````c1_1, c1_2, c2 : cmd
H : Sequence (transform c1_1) (transform c1_2) = c2
______________________________________(1/1)
Transform (Sequence c1_1 c1_2) c2
``````

where `cmd` is an inductive type and `Sequence` is one of the constructors. Obviously, `c2` should be also a `Sequence`. If you run `destruct c2; try discriminate.`:

``````c1_1, c1_2, c2_1, c2_2 : cmd
H : Sequence (transform c1_1) (transform c1_2) = Sequence c2_1 c2_2
______________________________________(1/1)
Transform (Sequence c1_1 c1_2) (Sequence c2_1 c2_2)
``````

This is what we expected. By the way, alternatively, you can also use `inversion H; subst.` to get a similar effect.

### `congruence`

I found `congruence` seems to be a stronger version of `discriminate`. You can achieve the same effect from my previous `discriminate` examples with `congruence`. But you can do more with `congruence`. For example,

``````H : x1 <> x1
______________________________________(1/1)
Some t2 = Some t1
``````

in this case, `congruence.` finds that `H` is false, thus finishing the case, while `discriminate.` cannot because it’s structurally the same.

### `auto`

At first I thought `auto` is a very powerful tactic, but later I found it can only figure out some trivial cases. The way I understand it is treating it like repeatly trying `hypotheses`, `reflexivity`, `congruence`, and applying known lemmas.

### `econstructor` / `eapply` / `eauto` / `edestruct` / `eexists`

The `e` version tactics do the same thing as non-`e` version ones do, except that when some variables cannot be found, they introduce existential variables instead of failing.

### `rewrite`

If you have an equation, you can use it to rewrite other hypotheses and/or the goal.

`rewrite H.` replace the left hand side of `H` with the right hand side of `H` in the goal. To make it work on the other way around, use `rewrite <- H.`.

If you want to rewrite an hypothesis `H1` instead of the goal, use `rewrite H in H1.`. And if you want to rewrite all the hypotheses and the goal, use `in *`.

For example,

``````H1 : length h = length ht
______________________________________(1/1)
length h < length (snoc ht t0)
``````

After `rewrite H1.`:

``````H1 : length h = length ht
______________________________________(1/1)
length ht < length (snoc ht t0)
``````

Another example,

``````H1 : length h = length ht
H8 : nth (length ht) (snoc ht t0) TBool = t0
``````

After `rewrite <-H1 in H8.`:

``````H1 : length h = length ht
H8 : nth (length h) (snoc ht t0) TBool = t0
``````

By the way, if you are not sure about which side to rewrite, like me, just try both with and without `<-` and one of them will work.

### `unfold`

Sometimes a proposition is written in some abstract definition. To remove the abstract, use `unfold`. For example,

``````1 subgoal
______________________________________(1/1)
derives derive
``````

There is no tactic that can make progress. But after `unfold derives.`:

``````______________________________________(1/1)
forall (a : ascii) (re : reg_exp), is_der re a (derive a re)
``````

This looks better. We can further `unfold is_der.`:

``````______________________________________(1/1)
forall (a : ascii) (re : reg_exp) (s : string),
String a s =~ re <-> s =~ derive a re
``````

Now we know what to do (`intros. split.`).

Similar to `rewrite`, `unfold` applies to the goal by default. To apply on an hypothesis `H`, use `in H`. And `in *` if all hypotheses and the goal.

### `specialize`

If there is an hypothesis that begins with `forall`, you can use `specialize` to fill in the free variable.

If there is an hypothesis that consists of several propositions joined by `->` and you happen to have the proofs of the prefix propositions, use `specialize` to strip those “preconditions”.

For example,

``````IHstep : forall c1' : cmd,
c1' = c1' ->
Transform c1 c1' ->
exists c2' : cmd, step_buggy (v, c1') (v', c2')
H3 : Transform c1 tc1
``````

After `specialize (IHstep tc1).`:

``````IHstep : tc1 = tc1 ->
Transform c1 tc1 ->
exists c2' : cmd, step_buggy (v, tc1) (v', c2')
H3 : Transform c1 tc1
``````

If you instead run `specialize (IHstep tc1 (eq_refl tc1) H3).`:

``````IHstep : exists c2' : cmd, step_buggy (v, tc1) (v', c2')
H3 : Transform c1 tc1
``````

### `pose proof`

`pose proof` can do things `specialize` can do but with a slight difference that `pose proof` adds a new hypothesis and keeps the original hypothesis untouched while `specialize` transforms the hypothesis in place.

Since `pose proof` adds new hypotheses, it can do more things than `specialize`. Especially, you can add an hypothesis by using a lemma. Some examples:

• `pose proof (IHstep tc1 (eq_refl tc1) H3).`
• `pose proof (step_step_buggy p1 p2 H c1' H0).`

### `split`

When the goal consists of several proposition joined by `/\`, i.e. a conjunction form, use `split.` to break them into several subgoals.

When you have a iff `<->`, you can also use `split.` to break it into two directions.

### `left` / `right`

On the other hand, if the goal is a disjunction form, use `left.` or `right.` to choose which side to prove.

### `exact`

If your goal is already in the hypotheses, use `exact` to tell Coq that. Alternatively, you can also `exact` without `pose proof`. Examples:

• `exact H7.`
• `exact (ReachRefl g b).`

### `assert`

`assert` can be used to add a proposition to hypotheses. Of course, you will have to prove it. `assert P.` results in two subgoals: one is to prove `P` given what you already know and the other is the original goal but with `P` in the hypotheses.

The motivation for this might be that you want to duplicate a known hypothesis because you need to transform it later while keeping its original form. A more common case is that there is something you know in mind but Coq does not.

A few examples:

• `assert (H8 := Heqo0).`
• `assert (a < length h); try omega.`
• `assert ("" = "" ++ ""). equality.`
• `assert (~ free e1 x).`

### `first_order`

`first_order` can be used to break `/\`, `\/`, `->`, `<->`, and lots of stuffs in hypotheses and goals. For example, given

``````H : ("" =~ re1) /\ String a s =~ re2 \/
(exists s0 s1 : string, s = s0 ++ s1 /\
(String a s0 =~ re1) /\ s1 =~ re2)
H0 : "" =~ re1 <-> true = true
______________________________________(1/1)
s =~ Union (derive a re2) (App (derive a re1) re2)
``````

`first_order` will break the complicated `H` and `H0`. Because there is a `\/` in `H`, it results in two cases:

``````H1, H : "" =~ re1
H2 : String a s =~ re2
H0 : true = true
______________________________________(1/1)
s =~ Union (derive a re2) (App (derive a re1) re2)
``````

and

``````H1 : "" =~ re1
x, x0 : string
H : s = x ++ x0
H2 : String a x =~ re1
H3 : x0 =~ re2
H0 : true = true
______________________________________(1/1)
s =~ Union (derive a re2) (App (derive a re1) re2)
``````

Another example, given

``````H4 : heap_typ_extends x ht /\ typed E0 x e' t0 /\ heap_typed x h'
______________________________________(1/1)
heap_typ_extends x ht /\ typed E0 x (ref e') (TRef t0) /\ heap_typed x h'
``````

`first_order` will result in

``````H4 : heap_typ_extends x ht
H7 : typed E0 x e' t0
H8 : heap_typed x h'
______________________________________(1/1)
typed E0 x (ref e') (TRef t0)
``````

Although the original goal consists of three propositions, `first_order` only results in one goal instead of three, because the other two are already known in `H4` which also breaks into three. By the way, Coq actually further breaks `heap_typed`, but I just pretend it doesn’t here for simplicity.

### `admit`

When there are multiple subgoals, sometimes you may want to skip a few cases, maybe because you don’t know how to prove it, probably because it’s too easy and you don’t bother prove it now, or because you are not sure whether this is the correct way and want to see what the rest of subgoals looks like.

In this case, `admit.`. Of course, once you `admit.`, you cannot get a `Qed.`, you can only `Admitted`.

### `symmetry`

If the goal is an equality and you want to flip it, use `symmetry.`. For example,

``````______________________________________(1/1)
env2 x = Some t
``````

After `symmetry`:

``````______________________________________(1/1)
Some t = env2 x
``````

### `revert`

`revert` is used to put back something you `intros`-ed before. Why would you want to do that? Because that makes induction hypotheses stronger. For example,

``````Lemma extends_lookup :
forall h h' a,
a < length h ->
heap_typ_extends h' h ->
lookup_typ h' a = lookup_typ h a.
``````

If we directly `induction a; intros.`, the second subgoal will be:

``````h : list typ
h' : heap_typ
a : nat
IHa : a < length h ->
heap_typ_extends h' h ->
lookup_typ h' a = lookup_typ h a
H : S a < length h
H0 : heap_typ_extends h' h
______________________________________(1/1)
lookup_typ h' (S a) = lookup_typ h (S a)

``````

However, if we `intros h h' a. revert h h'. induction a; intros.`, we will get the following second subgoal:

``````a : nat
IHa : forall (h : list typ) (h' : heap_typ),
a < length h ->
heap_typ_extends h' h ->
lookup_typ h' a = lookup_typ h a
h : list typ
h' : heap_typ
H : S a < length h
H0 : heap_typ_extends h' h
______________________________________(1/1)
lookup_typ h' (S a) = lookup_typ h (S a)
``````

As you can see, the induction hypothesis `IHa` is stronger with `revert`. Without `revert`, `IHa` will not be strong enough to finish the proof (I spent a lot time here).

So how do we know whether we should `revert` or not? I’d say let’s first keep things simple and don’t `revert`. Once you notice that the induction hypotheses are not strong enough, start thinking about `revert`.

### `remember`

Another issue with `induction` I ran into is:

``````a : ascii
s : string
re : reg_exp
H : String a s =~ Star re
______________________________________(1/1)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Star re
``````

To clarify, here, `=~` is just a notation for a inductive type. `x =~ y` means `exp_match x y`. Although intuitively, we know we need to induct on `H`, if we directly `induction H`, we will get dozens of unprovable things:

``````8 subgoals
a : ascii
s : string
re : reg_exp
______________________________________(1/8)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ EmptyStr
______________________________________(2/8)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Char x
______________________________________(3/8)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Dot
______________________________________(4/8)
exists s0 s3 : string, s = s0 ++ s3 /\ (String a s0 =~ re) /\ s3 =~ App re1 re2
______________________________________(5/8)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Union re1 re2
______________________________________(6/8)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Union re1 re2
______________________________________(7/8)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Star re0
______________________________________(8/8)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Star re0
``````

I heard this is because `induction` behaves badly if the parameters to the constructor are not variable. `String a s` and `Star re` are expressions, not variables.

In this case, we can use `remember (String a s). remember (Star re).` to replace those two expressions with variables:

``````a : ascii
s : string
re : reg_exp
s0 : string
Heqs0 : s0 = String a s
r : reg_exp
Heqr : r = Star re
H : s0 =~ r
______________________________________(1/1)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ r
``````

Now, we can `induction H; try discriminate.` and only one reasonable subgoal left:

``````a : ascii
s : string
re : reg_exp
s0, sk : string
Heqs0 : sk ++ s0 = String a s
re0 : reg_exp
Heqr : Star re0 = Star re
H : s0 =~ Star re0
H0 : sk =~ re0
IHexp_match1 : s0 = String a s ->
Star re0 = Star re ->
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Star re0
IHexp_match2 : sk = String a s ->
re0 = Star re ->
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ re0
______________________________________(1/1)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Star re0
``````

### `induct` (Frap Tactic)

`induct` is a stronger version of `induction` from the `frap` library. You don’t need to `remember` before `induct` and you can get even stronger hypotheses. For the previous example, if we directly `induct H.`, we’ll have:

``````re : reg_exp
s0, sk : string
H : s0 =~ Star re
H0 : sk =~ re
IHexp_match1 : forall (a : ascii) (s : string) (re0 : reg_exp),
s0 = String a s ->
Star re = Star re0 ->
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re0) /\ s1 =~ Star re0
IHexp_match2 : forall (a : ascii) (s : string) (re0 : reg_exp),
sk = String a s ->
re = Star re0 ->
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re0) /\ s1 =~ Star re0
a : ascii
s : string
x : sk ++ s0 = String a s
______________________________________(1/1)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Star re
``````

Easier and stronger! So I’d use `induct` to replace `induction` if possible.

## Vernacular Commands

### `Print`

You can use `Print` to check definitions. For example, `Print or.`:

``````Inductive or (A B : Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B.
``````

Knowing which built-in lemma to apply is always a headache. Once I ran into a case that I need to flip a not-equal relation:

``````H1 : x1 <> x2
H5 : x2 <> x1 -> ~ free e1 x2
``````

This might seem trivial for a human, but not for Coq. Later, I found I can use `Search` to find the name of the lemma as long as I can guess how to express that lemma in Coq. In this case, the lemma I wanted is:

``````Search (forall a b, a <> b -> b <> a).
``````

Then Coq can magically understand and tell me:

``````not_eq_sym: forall (A : Type) (x y : A), x <> y -> y <> x
``````

Another silly case I ran into is:

``````IHtyped : E0 = E0 ->
heap_typed ht h ->
(exists (e' : expr) (h' : heap), h; e ==> h'; e') \/ isValue e
``````

Coq, how do I tell you that everything is equal to itself?

``````Search (forall x, x = x).
``````

Then Coq says:

``````eq_refl: forall (A : Type) (x : A), x = x
``````

But sometimes you don’t know how to write the lemma (for example, I didn’t know how to express “it must be true that either `x = y` or `x <> y`”). In this case, you can search the name, like `Search "eq".`, and go through all the lemmas that have `eq` in it.

## Tricks

### Induct on what?

Induction usually reflects the definition.

``````Lemma len_app_plus:
forall s1 s2,
String.length (s1 ++ s2) = String.length s1 + String.length s2.
``````

To prove `len_app_plus `, induct on `s1` because `String.length` consumes the first character of a string on a single iteration. When you are inducting on `s1`, the second case will be `s1 = String ch s`, i.e. a character followed by a string, which fits the definition of `String.length`, thus we can unfold it and apply the induction hypothesis.

``````Lemma len_repeat:
forall s n,
String.length (repeat s n) = n * String.length s.
``````

Similarly, to prove `len_repeat`, induct on `n` because `repeat` is a recursion on `n`.

### Idention, Bullet Points

I’m not sure about how Coq community think about the indention, but coming from a strong programming background, I’d prefer my proofs have indention to reflect the structure of the proofs.

Coq ignores all white spaces, including new lines, but it does provide bullet points to distinguish subgoals: `+`, `-`, `*`, repeated bullet points (`++`, `***`, …), and the pair of `{}`. So, you can write proofs like this:

``````Proof.
tactic.             (* become two subgoals after this *)
+ tactic.           (* enter "+", level 1, focus only one subgoal *)
tactic.           (* become three subgoals after this *)
- tactic.         (* enter "-", level 2, focus only one subgoal, and prove it *)
- tactic.         (* focus another level 2 subgoal, and prove it *)
- tactic.         (* focus another L2 subgoal, become two subgoals after this *)
* tactic.       (* enter "*", level 3, focus only one subgoal *)
tactic.       (* become two subgoals after this *)
{ tactic.     (* enter "{}", level 4, focus only one subgoal *)
tactic.     (* become two subgoals after this *)
- tactic.   (* enter "-" inside "{}", level 5, focus only one subgoal *)
tactic.
+ tactic. (* level 6 *)
+ tactic.
- tactic. } (* prove another "-" inside "{}" and finish the first "{}" *)
{ tactic.     (* enter another "{}" subgoal *)
tactic. }   (* finish the subgoal *)
* tactic.
+ tactic.           (* come back to the very first level *)
Qed.
``````

Although you can prove without using any bullet points, I found it very helpful to keep track of the structure of the proof. When you enter a bullet point, there will be only one goal. And after you finish the prove of a subgoal, Coq will tell you how many subgoals remaining to prove.

In addition, I personally would like to avoid branching on trivial cases because otherwise the proof might look very skewed:

``````+ tactic.
+ tactic.
- tactic.
- tactic.
* tactic.
* tactic.
++ tactic.
++ tactic.
** tactic.
** tactic.
-- tactic.
-- tactic.
{ tactic. }
{ tactic.
+ tactic.
+ tactic.
- tactic.
- tactic. }
``````

There are several ways to avoid this kind of trivial branching.

• If there are multiple cases but only one is non-trivial
• Use `;` and `try`, like `destruct c2; try discriminate.`
• If there are exactly two cases
• If the trivial case is the first case, just prove it without branching.
• If the trivial case is the second case, use `2:` to focus on the second case, like `destruct s2. 2: inversion x.` and `cases (ascii_dec a0 a0). 2: congruence.`

### Multiple tactics in a single line

I found sometimes it is more clear to group a few logically related tactics in a single line then starting a new line for each one. For example,

``````inversion H. subst.
cases (ascii_dec a0 a0). 2: congruence.
econstructor; eauto.
``````

looks better than

``````inversion H.
subst.
cases (ascii_dec a0 a0).
2: congruence.
econstructor.
eauto.
``````

especially when the proof gets longer and bullet points become more.

### Forward Proof and Backwards Proof

There are two style of proving things, forward and backward. Forward proof is to keep on adding hypothesis until the goal is in the hypotheses. Backwards proof is to keep on transform the goal into easier/smaller problems until it’s in the hypotheses.

Usually you might want to mix both, because sometimes it’s easier to `pose proof` something, and sometimes it’s easier to `apply` a lemma or use `e-` variant tactics and let Coq figure things out.

### Toggle Notation Display

It can be quite scary when you see a symbol in Coq that you don’t recognize. Most of them are just notations. Don’t think them as some special cases or black magics. You can even add notations for inductive types on your own.

When the notations get in your way to understand things, just don’t display them. In CoqIDE, it’s in View / Display notations.

## FAQ

### When I have `Some x = Some y`, how do I get `x = y`?

`inversion`.

### When I need to prove `Some x = Some y`, how do I instead prove `x = y`?

`f_equal`.

### Given `x <> y`, how do I get `y <> x`?

``````Search (forall a b, a <> b -> b <> a).

not_eq_sym: forall (A : Type) (x y : A), x <> y -> y <> x
``````

### How do I say either `x = y` or `x <> y`.

This is usually called something `_dec`. For example,

• `ascii_dec`
• `string_dec`
• `Nat.eq_dec`

You can use `destruct (string_dec x y).` to discuss the two cases.

### What if my assumtions have `/\` and/or `\/`?

`first_order` or `destruct`.

### What if the goal have `/\` or `<->`?

`first_order` or `split`.

### What if the goal have `\/`?

Use `left.` or `right.` to prove either one of them.

### How do I duplicate an hypothesis?

`assert`.

### How do I add a proposition to hypotheses?

`assert`.

### What if there is a contradiction in hypotheses?

Let’s say you have a `H : False` or anything that can be turned into `False` (for example, `Some x = None`, `1 = 2`, or `True = False`). Then congratulations! Try `discriminate.` or `congruence.`, then the goal should be proven.

The reason for this is that logically, a false hypothesis can imply anything.

### What if there is a contradiction in the preconditions of an hypothesis?

Let’s say you have a `H : Some x = None -> P`, then you can `clear H.` because you will never be able to use `H`. Unlike the previous case, since you will never be able to prove `Some x = None`, you cannot get rid of the precondition of `P` in `H`.

### What if the goal is a contradiction or not provable?

If your goal is `False` or `Some x = None` or anything like that, which is not provable, don’t panic. First check if there is any contradiction in the hypotheses because a false hypothesis can imply anything, including a false goal.

If all the hypotheses make sense, even after a few transformation, then you know you did something wrong in the previous part of the proof. Find that, and come up with a better idea.

### What if the goal has `->`?

`intros`.

### What if the goal starts with `forall`?

`intros`.

### What if the goal starts with `exists`?

Usually I use `exists` to tell Coq what those variables are. But alternatively, you can also uses `eexists.` to push the proof forward, then Coq might be able to figure out what variables are some time later.

### What if an hypothesis starts with `forall`?

`specialize` or `pose proof`.

### What if an hypothesis starts with `exists`?

`destruct` to get the witness out.

### What if an hypothesis has `->`?

`specialize` or `pose proof`.

`admit`.