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.

Thanks.

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)

I hope this could explain of what it is needed.

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?

Thank you in advance for explanation.

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.

?

About the file extension and interactive use vs compilation: https://coq.inria.fr/distrib/current/refman/practical-tools/coq-commands.html?highlight=coqc

About recursive function: https://coq.inria.fr/distrib/current/refman/language/core/inductive.html#top-level-recursive-functions

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]).
```

Last updated: Jan 28 2023 at 06:30 UTC