Comment importer une preuve d'un fichier.v dans un autre?

[fr] Rocq en français
1

Je viens de débuter en coq et j’ai conçu de nombreuses preuves dans plusieurs fichiers. Je voudrais les utiliser dans une preuve principale.

2

Je suppose que tu sais te servir d’une ligne de commande sous Linux ou Mac, parce que si t’es sous Windows je sais pas faire.

  1. Pour l’exemple, disons que tu as deux fichiers Fichier1.v et Fichier2.v.
    1. Fichier1.v définit quelque chose:
      Definition a := 0.
    2. Fichier2.v importe Fichier1 pour utiliser sa définition:
      From Waf Require Import Fichier1.
Print a.
  2. Crée un fichier _CoqProject avec ce contenu (où Fichier1.v, Fichier2.v seront à remplacer par tes noms de fichiers):
    -Q . Waf
Fichier1.v
Fichier2.v
  3. Au final ton dossier ressemble à ça:
    mondossier/
  _CoqProject
  Fichier1.v
  Fichier2.v
  4. Une fois le dossier en place, il y a deux commandes à connaître:

    1. Commande à lancer à chaque fois que tu modifies _CoqProject, typiquement pour rajouter d’autres fichiers:

      rocq makefile -f _CoqProject -o Makefile

    2. Commande à lancer à chaque fois qu’un .v est modifié:

      make

Si tout compile bien, tu peux ouvrir un fichier dans ton éditeur préféré et ça devrait marcher.

3

Merci beaucoup mais je suis sur windows