How to create a bibliography source file in coq

Question

I want to create a file bibliography in coq, i have a model of an automaton,

Record automaton :Type:=
   mk_auto {
       states : Set;
       actions :Set;
       initial : states;
       transitions : states -> actions -> list states
     }.

(*States*)
Inductive st :Set:= q0 | q1 | q2.

(*Actions*)
Inductive acts:Set:= a | b | c.

(*Transitions*)
Definition trans (q:st)(x:acts) :list st :=
match q, x with
     | q0, a =>  cons q1 nil
     | q1, b =>  cons q0 nil
     | q1, c =>  cons q2 nil
     | _,_ =>    nil (A:=_)
end.

 (* Automate A1 *)
 Definition A1 := mk_auto st acts q0 trans.
 Print A1.

I want to use the record model in different files.

Record automaton :Type:=
mk_auto {
    states : Set;
    ctions :Set;
    initial : states;
    transitions : states -> actions -> list states
}.

Thanks for your response.

Vinz · Answer 1 · 2014-04-15T09:39:54.293

0

I am not sure what you mean by "bibliography" file, but if you want to make a library that you can Import from other file, you just have to make a .v file with your Record definition, and compile it with coqc. It will create a .vo file that you can reuse through the Require Import your_file. scheme. You can put the .vo file in the same folder as your current .v file, or refer to the documentation to add search path to Coq (Add LoadPath if I remember correctly).

Cheers, V.

EDIT: after your comment, here is my attempt at building the library, it might help you check what goes wrong:

vinz@####:/tmp/foo$ cat test.v
Record automaton :Type:= mk_auto {
    states : Set;
    actions :Set;
    initial : states;
    transitions : states -> actions -> list states
}.
vinz@####:/tmp/foo$ ls
test.v
vinz@####:/tmp/foo$ coqc test.v
vinz@####:/tmp/foo$ ls
test.glob  test.v  test.vo

EDIT2: if the .vo file is in the same directory as the .v you are currently editing, coqide seems to be happy. The general scheme is to write Add Loadpath "/path/to/the/vo/file". before the Require Import. This should cover your last issue

edited Apr 15 '14 at 09:39

answered Apr 15 '14 at 08:55

Vinz

5,997
1
31
52

I try with that, by it does not work, i make two files in the same directory, the frist file is automod.v . Record automaton :Type:= mk_auto { states : Set; actions :Set; initial : states; transitions : states -> actions -> list states }. And the second file is auto.v. Require Import automod. I compile the first one, the file automod.vo is creating. but it does not work ?!. the message is: Error: Cannot find library automod in loadpath. – NAAS1425 Apr 15 '14 at 09:16
You need to start your ``coqide/coqtop`` in the same directory where you compiled the ``.vo`` file. If you start it from another location, you have to tell Coq where to look, with the ``LoadPath`` vernacular. Please read the documentation or check SO for related issues, like http://stackoverflow.com/questions/16202666/coqide-cant-load-modules-from-same-folder for example. – Vinz Apr 15 '14 at 09:32
thank you very much for your help, the code is working now :) – NAAS1425 Apr 15 '14 at 12:03
Glad I could be of help. Do not forget to validate the answer to tag the question as "solved". – Vinz Apr 15 '14 at 12:28

How to create a bibliography source file in coq

1 Answers1