Difference between Definition and Let in Coq

Question

What is the difference between a Defintion and 'Let' in Coq? Why do some definitions require proofs? For eg. This is a piece of code from g1.v in Group theory.

Definition exp : Z -> U -> U.
Proof.
intros n a.
elim n; clear n.
exact e.
intro n.
 elim n; clear n.
exact a.
intros n valrec.
exact (star a valrec).
intro n; elim n; clear n.
exact (inv a).
intros n valrec.
exact (star (inv a) valrec).
Defined.

What is the aim of this proof?

Answer 1

I think what you're asking isn't really related to the difference between the Definition and Let commands in Coq. Instead, you seem to be wondering about why some definitions in Coq contain proof scripts.

One interesting feature of Coq is that the language that one uses for writing proofs and programs is actually the same. This language is known as Gallina, which is the programming language people work with when using Coq. When you write something like fun x => x + 5, that is a program in Gallina.

When doing proofs, however, people usually use another language, called Ltac. This is the language that appears in your exp example. This could lead you to believe that proofs in Coq are represented in a different language, but this is not true: what Ltac scripts do is to actually build proof terms in Gallina. You can see that by using the Print command, e.g.

Print exp.

The reason for having a separate language for writing proofs, even if proofs and programs are written in the same language, is that Gallina is a bit hard to use directly when writing proofs. Try using the Print command directly over a complicated theorem to see how hard that can be.

Now, even though Ltac is mostly meant for writing proofs, nothing forbids you from using it to write normal programs, since the end product is the same: a Gallina term. Usually, people prefer to use Gallina when writing programs because it is easier to read. However, people might resort to Ltac for writing programs when doing it directly in Gallina would be too cumbersome. I personally would prefer to use Gallina directly for writing functions such as exp in your example, although that's arguably a matter of taste.