Will Wu (Jul 03 2020 at 03:41): 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.
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: Oct 13 2024 at 01:02 UTC