The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi,

  This is a problem I'm running into while trying to manage ~2K loc
Coq project. I want to:

  1. separate statement of lemma from proof of lemma
  2. separate type declaration of Function from definition of Function

In particular, I would like to have a file structure that looks something 
like:

=== BEGIN ===

Require Import ....

(* Just declarations *)
Function foo1 (args) : output-type.
Function foo2 (args) : output-type.

(* Just a statement *)
Lemma lem1:
  something involving foo1 and foo2.


Function foo1 (args) : output-type :=
  (* definition of foo1 *)

Function foo2 (args): output-type :=
  (* definition of foo2 *)

Lemma lem1:
  lem1 statement, proof of lem1.

=== END ===

Now, I realize there are two problems with this approach:

  1) I'm repeating myself. I can accept this. Ideally, I'd like Coq to
check and make sure that the two definitions are the same.

  2) This 'destroys' the interactive flow. When I add a new function
foo2 at the top of the file. The parts of code for foo1, foo2, and
lem1 becomes invalid. This is okay. I don't mind this when I add new
declarations.

I'm okay with both of the above. Is there anyway to have what I want
above? (mainly, I want a single place where all the Functions / Lemmas
so that when I'm searching for a particular function/lemma, I can only
look through the declarations without seeing the proofs).

Lastly, if the "right" way to do this to use some external tool which
looks at a *.v file and generates a separate file with the
declarations, I'm okay with that too.

Thanks!