Structuration Coq code

Question

J'ai la configuration habituelle: d'abord je définis certains types, puis certaines fonctions de ces types. Cependant, comme il y a plusieurs façons de formaliser ce que je fais, je le ferai en 3 versions. Pour la simplicité (et pour maintenir une vue d'ensemble), je veux mon code dans un dossier. Je veux également minimiser le code répétitif. À cette fin, une installation w/3 Module s pour des choses spécifiques et définitions générales devant eux pourraient travailler - mais pas dans le type de situation décrite ci-dessous:

1. Une Definition générale de la fonction f: A -> B, accessible dans toutes les sections (ou modules)

2. module- (ou section-) des définitions spécifiques des A

3. f doivent être calculable dans toutes les sections (ou modules)

Quelle configuration me recommandez-vous d'utiliser?

Answer 1

Require Import Arith. 

(* Create a module type for some type A with some general properties. *) 
Module Type ModA. 
    Parameter A: Type. 
    Axiom a_dec: forall a b:A, {a=b}+{a<>b}. 
End ModA. 

(* Define the function that uses the A type in another module 
    that imports a ModA type module *) 

Module FMod (AM: (ModA)). 
    Import AM. 
    Definition f (a1 a2:A) := if a_dec a1 a2 then 1 else 2. 
End FMod. 

(* Here's how to use f in another module *) 
Module FTheory (AM:ModA). 
    Module M := FMod AM. 
    Import M. 
    Import AM. 

    Theorem f_theorem: forall a, f a a = 1. 
    intros. compute. destruct (a_dec _ _). 
    auto. congruence. 
    Qed. 
End FTheory. 

(* Eventually, instatiate the type A in some way, 
    using subtyping '<:'. *) 

Module ModANat <: ModA. 
    Definition A := nat. 
    Theorem a_dec: forall a b:A, {a=b}+{a<>b}. 
    apply eq_nat_dec. 
    Qed. 
End ModANat. 

(* Here we use f for your particular type A *) 
Module FModNat := FMod ModANat. 

Compute (FModNat.f 3 4). 

Recursive Extraction FModNat.f. 

Goal FModNat.f 3 3 = 1. 
    Module M := FTheory ModANat. 
    apply M.f_theorem. 
Qed.