Stream: Coq users

Topic: module system composition


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 03 2020 at 10:05):

BM can use Include (B Sig1).

view this post on Zulip Paolo Giarrusso (Jul 03 2020 at 10:06):

That will avoid the need to redefine T in BM.

view this post on Zulip Paolo Giarrusso (Jul 03 2020 at 10:08):

ah, no parens needed, even Include B Sig1 works

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 11:19):

Ah, very good point!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 11:23):

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

view this post on Zulip Will Wu (Jul 06 2020 at 01:45):

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


Last updated: Jan 29 2023 at 06:02 UTC