Théo Zimmermann edited this page Apr 23, 2018 · 2 revisions

(Part of the Coq FAQ)

Can you explain me what an evaluable constant is?

An evaluable constant is a constant which is unfoldable.

What is a goal?

A goal is a statement to be proved.

What is a meta variable?

A meta variable in Coq represents a “hole”, i.e. a part of a proof that is still unknown.

What is Gallina?

Gallina is the specification language of Coq. Complete documentation of this language can be found in the Reference Manual.

What is The Vernacular?

It is the language of Gallina commands; i.e. definitions, lemmas, ...

What is a dependent type?

A dependent type is a type which depends on some term. For instance "vector of size n" is a dependent type representing all the vectors of size n. Its type depends on n.

What is a proof by reflection?

This is a proof generated by some computation which is done using the internal reduction of Coq (not using the tactic language of Coq (Ltac) nor the implementation language for Coq). An example of a tactic using the reflection mechanism is the ring tactic. The reflection method consist in reflecting a subset of Coq language (for example the arithmetical expressions) into an object of the Coq language itself (in this case an inductive type denoting arithmetical expressions). For more information see [1], [2], and [3] below and the last chapter of the Coq’Art book.

What is intuitionistic logic?

This is any logic which does not assume that "A or not A".

What is proof-irrelevance?

See this part of the FAQ.

What is the difference between opaque and transparent?

Opaque definitions can not be unfolded but transparent ones can.


[1] Doug Howe. Computation meta theory in nuprl. In E. Lusk and R. Overbeek, editors, The Proceedings of the Ninth International Conference of Autom ated Deduction, volume 310, pages 238–257. Springer-Verlag, 1988.

[2] John Harrison. Meta theory and reflection in theorem proving:a survey and cri tique. Technical Report CRC-053, SRI International Cambridge Computer Science Research Center, 1995.

[3] Samuel Boutin. Using reflection to build efficient and certified decision pro cedures. In M. Abadi and T. Ito, editors, Proceedings of TACS'97, volume 1281 of LNCS. Springer-Verlag, 1997.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.