Might be a beginner question. basically I found me repeating myself if I want to make modules more compositional instead of just layer-on-layer, detailed question in this Coq snippet ~90 lines. Can someone enlight me of the standard practice here?

```
Module Type SIG.
Parameter X Y : Type.
End SIG.
Module A (SIG: SIG).
Import SIG.
Inductive T :=
| FromX : X -> T
| FromY : Y -> T
.
End A.
(* I state some theorems in one module to reuse elsewhere. *)
Module A_THEOREMS (SIG: SIG).
Module MyA := A SIG.
Import MyA.
Theorem T_theorem1 : forall t: T, True. auto. Qed.
End A_THEOREMS.
(* A failed reusing example. *)
Module A_THEOREMS'_FAIL (SIG: SIG).
Module MyA := A SIG.
Import MyA.
Module A_T := A_THEOREMS SIG.
(* Failed because A_tT.MyA is not MyA *)
Theorem T_theorem2 : forall t: T, True. assert_fails (apply A_T.T_theorem1). Abort.
End A_THEOREMS'_FAIL.
(* This would work but requires linear/layer-on-layer composition of modules *)
Module A_THEOREMS'_WORK (SIG: SIG).
Module A_T := A_THEOREMS SIG.
Import A_T.
Theorem T_theorem2 : forall t: MyA.T, True. apply T_theorem1. Qed.
End A_THEOREMS'_WORK.
(* Another Try: Ideally I should just use Module Type, making T also in signature. *)
Module Type B (SIG: SIG).
Import SIG.
(* Constructors needed here because the proofs may be specific to the way
T is defined. So not making T a Parameter here. *)
Inductive T :=
| FromX : X -> T
| FromY : Y -> T
.
End B.
Module B_THEOREMS (SIG: SIG) (MyB : B SIG).
Import MyB.
Theorem T_theorem1 : forall t: T, True. auto. Qed.
End B_THEOREMS.
Module B_THEOREMS' (SIG: SIG) (MyB: B SIG).
Import MyB.
Module B_T := B_THEOREMS SIG MyB.
Theorem T_theorem2 : forall t: T, True. apply B_T.T_theorem1. Qed.
End B_THEOREMS'.
Module Sig1 <: SIG.
Definition X := nat.
Definition Y := nat.
End Sig1.
Module BM <: B Sig1.
Import Sig1.
Inductive T :=
| FromX : X -> T
| FromY : Y -> T
. (* The problem is : why I have to repeat myself here?
I don't wanna make T opaque in B for the reason stated above.
*)
End BM.
Module BT' := B_THEOREMS' Sig1 BM.
Theorem T_theorem3 : forall t: BM.T, True. apply BT'.T_theorem2. Qed.
```

BM can use `Include (B Sig1)`

.

That will avoid the need to redefine T in BM.

ah, no parens needed, even `Include B Sig1`

works

But I am not sure what the problem is with A_THEOREMS'_WORK. That seems simpler, no?

Paolo G. Giarrusso said:

But I am not sure what the problem is with A_THEOREMS'_WORK. That seems simpler, no?

Hi, thanks for the help! The problem with the 1st approach is that it would create dependencies that is logically unnecessary. Say I have module A1 and A1' which are independent to each other, but I can't do that:

```
Module A1 (SIG: SIG).
Module MyA := A SIG.
Parameter A1_property: MyA.T -> Prop.
Axiom T_theorem1 : forall t, A1_property t.
End A1.
Module A1' (SIG: SIG).
Module MyA := A SIG.
Parameter A2_property: MyA.T -> Prop.
Axiom T_theorem2 : forall t, A2_property t.
End A1'.
Module A2 (SIG: SIG).
Module A1 := A1 SIG.
Module A2 := A1' SIG.
(* The next line would generate an Error *)
Theorem A1: forall t, A1.A1_property t /\ A2.A2_property t.
End A2.
```

instead I need to have A1' include A1, and A2 include A1'. Though A1' are independet from A1.

Ah, very good point!

Caveat: Keep in mind that `Include`

will create a _copy_ of the included definitions. That's still pretty fast, but I guess it has limits.

In general, using Coq modules isn't easy and this isn't a beginner question.

After understanding the theory, I learned how to use them from Coq's natural number hierarchy. It's not a very didactic introduction, but I am not sure what else to recommend.

I guess one could start navigating the code from `theories/Numbers/NatInt/NZAxioms.v`

in the coq sources, and seeing how those definitions are used.

(I mean the modules and module types, not their contents)

Thanks for the suggestion! I'll take a look.

Last updated: Jun 18 2024 at 23:01 UTC