compile files · Coq users · Zulip Chat Archive

I have a newbie question.
I need to do the following.
To write to a file (module) Foo (the file name extension?) my simple program in Coq (Gallina?).
For example, the function 1) size for the length of a list,
2) the function rev for reversing a list, 3) a proof size_rev : size (rev xs) == size xs,
to write to the file Main.? the function f that evaluates size (rev [1 .. 10000]) and prints it to screen.
Then to load these from files and run the function f.
Then to compile this project (if possible) (by applying what? something composed with OCaml?)
to load it, and to apply the compiled f.
How do these modules look, how does their import look?
Where are explained all these features?

I see various manuals on Coq, and I am somewhat unlucky, find only the dialogue mode for doing everything. But in this dialogue I cannot create program modules, to edit this source with fixing errors, and to save them to files.

Sergei Meshveliani (Jul 04 2021 at 09:41):

I see now
"Le Coq’ Art (V8)",
with its
11 * Extraction et programmes impératifs
...
13 * Le système de modules
...
13.2.3 Modules paramétriques (foncteurs)

Sergei Meshveliani (Jul 04 2021 at 11:48):

Then, I look into its 11 * Extraction et programmes impératifs,
and have an impression that making an executable program presents a problem.
Does it?
There are rather complex explanations.

Please, consider the example.
Let it be a program module that presents the following
(all the functions with their explicit definition).
(1) The function length returning the length of a list.
(2) The function ++ for concatenation of two lists.
(3) The function
lemma : ... -> length (xs ++ ys) == length xs + length ys
as a proof for this property of ++ and length.
(4) The function main for printing out the example of computing length:
Print (length [100, 99, 98 ... 0]).

How can this be programmed in files, in one or two modules, the proof to be verified,
then, the whole thing to be somehow compiled to the executable `main', and to run?

Sergei Meshveliani (Jul 04 2021 at 19:58):

Well, the first approach can be applying the command Compute.
It remains to (1) set the definitions in appropriately written modules in the files,
(2) load the definitions from these files.
And I do not see how Coq can do this with the programs in files.
?

Pierre Courtieu (Jul 06 2021 at 07:43):

In short: Coq can be seen as a programming language but it is not its primary use. By default it behaves more like an interactive tool. A tool to write mathematical definitions, statements and proofs. It is not designed to produce "main programs" like in C.

It is however possible to define programs in coq. There are several ways to do so but the simplest one is to use the fact that the underlying formalism of coq (calculus of inductive constructions) is actually itself a programming language.

To do what you want you need to write in a file with .v extension, things like

Require Import List.
Import List.ListNotations.

Fixpoint length A (l:list A)  {struct l} :=
  match l with
  | nil => 0
  | x :: l' => 1 + length A l'
end.

Then, with a IDE (coqide for instance) you can enter an interactive coq session and "run" the script above by opening the file and using the scripting commands.

To test your function you can add the following commands and script to evaluate the function on particular values:

Eval compute in (length _ [2;4;5]).
Eval compute in (length _ [true;false;false;true]).

Stream: Coq users

Topic: compile files

Sergei Meshveliani (Jul 04 2021 at 09:14):

Sergei Meshveliani (Jul 04 2021 at 09:41):

Sergei Meshveliani (Jul 04 2021 at 11:48):

Sergei Meshveliani (Jul 04 2021 at 19:58):

Pierre Courtieu (Jul 06 2021 at 07:43):