Coq Tricks for Beginners with Too Many Examples

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

`Search`

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.

How do I focus other subgoals first?

admit.

Tactics

intros

simpl

simplify (Frap Tactic)

destruct

induction

inversion

f_equal

assumption

constructor

apply

exists

reflexivity

discriminate

congruence

auto

econstructor / eapply / eauto / edestruct / eexists

rewrite

unfold

specialize

pose proof

split

left / right

exact

assert

first_order

admit

symmetry

revert

remember

induct (Frap Tactic)