Some tips for poor programmers who have to use Coq for their projects.
Coq's dependent pattern matching is very simple but hard to use. There is a plugin called Coq-Equations which lets you write dependent functions more easily. (That syntax is pretty similar to Agda)
Naming in Coq is a messy chaos. I personally use following convention.
PascalCase
for typescamelCase
for propositions and functionssnake_case
for lemmas and theoremsSCREAMING_SNAKE_CASE
for local hypothesis in proof mode
This gives sane name especially for lemmas involving several functions. e.g. zipWith_length
instead of zip_with_length
Coq has a notion of existential variables, and they can be introduced in a proof mode by using tactics prefixed by e
such as eapply
, eauto
, etc.
Some existential variables can be instantiated automatically by unification, but you have to manually instantiate it occasionally.
The instantiate
tactic can be used in such case.
Axiom Foo : forall (A : Type), (A -> A) -> nat.
Lemma foo : nat.
Proof.
eapply Foo.
instantiate (1 := nat).
exact S.
Qed.
A significant drawback of instantiate
is that it takes position of the existential variable (which is a natural number), not it's name.
This leads to fragile proof since introduction of new existential variable may change the position number.
An alternative approach is using the unify
tactic.
Lemma foo : nat.
Proof.
eapply Foo.
match goal with [|- ?A -> ?A ] => unify A nat end.
exact S.
Qed.
In this way, you can avoid referring an existential variable by natural number.
You cannot refer an existential variable by automatically generated name.
Lemma foo : nat.
Proof.
eapply Foo.
unify ?A nat. (* fail *)
Abort.
You can name an existential variable by using ?[A]
syntax.
Lemma foo : nat.
Proof.
eapply (Foo ?[A]).
unify ?A nat.
exact S.
Qed.
is_evar
is a useful tactic for dealing with existential variables.
You may encounter a mysterious failure of unification. e.g. eapply
fails though the conclusion of the given term and the goal seems to match.
In that case, try using Set Printing All
to disable all notation and implicit arguments.
Sometimes the term you want to refer which is contained in the context or the proof goal is syntactically too huge.
match
and match goal
tactics are very useful in such situation.
If you want to refer a subterm of the goal, use match goal
.
match goal with
| ... => ...
end
If you want to refer a subterm of the type of a variable in the context, use combination of match
and type of
.
match type of H with
| ... => ...
end.
Coq has no special syntax for updating record. So you have to enumerate every fields of the record even if you're updating just a single field. Lens (which is prevalent in Haskell projects) is a useful tool in such case. You can automatically generate lenses by using packages like coq-lens.
The meaning of :>
when it is used in a record definition is completely different from the meaning when it is used in a class definition.
- In record definition, it declares the field as a coercion.
- In class definition, it declares the field as an instance of it's type (when the type of that field is also a class).
Note that this syntax is a subject to change. The
::
syntax will replace the usage of:>
for instance declaration.
See also defining-record-types
There are several useful features for mixing tactics with manually written proof terms.
Similar to exact
, but holes are allowed.
Use this to leave holes in a definition, or to obligate the proof of the termination of recursive definition.
This is used for filling a hole in an expression by invoking a tactic.
Qed
adds the proof term as an opaque constant.
So when you use proof mode for defining computable functions, you must end the proof with Defined
instead of Qed
.
Otherwise, it won't reduce.
lia
generates opaque proof term.
Lemma one_le_one : 1 <= 1.
Proof. lia. Defined.
Goal one_le_one = le_n 1.
Proof. reflexivity. (* fail *) Qed.
In Coq, there is an infinite and cumulative hierarchy of universes.
For convenience, Coq employs typical ambiguity. So you don't need to specify the universe levels explicitly.
However, typical ambiguity is not a polymorphism. For example, you can't use generic types in this way.
Inductive Maybe (A : Type) : Type :=
| just : A -> Maybe A
| nothing : Maybe A
.
Check just (Maybe nat). (* fail *)
But there is no problem with option
, which is a predefined type in Coq standard library.
Check Some (option nat). (* pass *)
This is because option
is defined as a template polymorphic type.
#[universes(template)]
Inductive option (A:Type) : Type :=
| Some : A -> option A
| None : option A.
universe-polymorphism is a new alternative for template polymorphism, but it is experimental.
Set Printing Universes
and Print Universes
are useful for debugging universe problems.
Types defined by Definition
are not a subject to template polymorphism.
Use Record
or Inductive
instead of Definition
for wrapping generic types (i.e. types that quantify over Type
universes).
Notation
can also be an alternative solution.
See the following example.
Definition mylist1 := list. (* No template polymorphism. Shares universe with list *)
Definition mylist2 (A : Type) := list A. (* No template polymorphism, but has its own universe level *)
Record mylist3 (A : Type) := { car : list A; }. (* Template polymorphic definition *)
Check [mylist1 nat] : list Type. (* fail *)
Check [mylist2 nat] : list Type. (* pass *)
Check mylist2 nat : Set. (* fail *)
Check mylist3 nat : Set. (* pass *)