## Stream: Coq users

### Topic: module system composition

#### Will Wu (Jul 03 2020 at 03:41):

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.
``````

#### Paolo Giarrusso (Jul 03 2020 at 10:05):

BM can use `Include (B Sig1)`.

#### Paolo Giarrusso (Jul 03 2020 at 10:06):

That will avoid the need to redefine T in BM.

#### Paolo Giarrusso (Jul 03 2020 at 10:08):

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

#### Paolo Giarrusso (Jul 03 2020 at 10:10):

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

#### Will Wu (Jul 03 2020 at 17:05):

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.

#### Paolo Giarrusso (Jul 04 2020 at 11:19):

Ah, very good point!

#### Paolo Giarrusso (Jul 04 2020 at 11:22):

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.

#### Paolo Giarrusso (Jul 04 2020 at 11:22):

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.

#### Paolo Giarrusso (Jul 04 2020 at 11:23):

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

#### Will Wu (Jul 06 2020 at 01:45):

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

Last updated: Jun 18 2024 at 23:01 UTC