The fact that a module signature can not only contain the signature
of an inductive or of a function, but also its body, was new to me,
thanks for explaining, Michael!
To compare the approach of putting Inductives outside modules (as
advocated by Adam) and the approach of putting them inside a
module type functor (as advocated by Michael), I wrote a somewhat
longer example (apologies if it's too long...).
You can search for comments beginning with "Quirk" to find spots
where I'm not satisified with the solution, and spots where a
solution does better than the other are marked with "NoQuirk",
while questions are marked with "Question".
Overall it seems that putting the Inductives inside a module type
functor has much fewer quirks, but requires a somewhat heretical
feature not present in Standard ML's module system, namely to
"Include" a signature inside a module; it seems to me that this
mixes two worlds which should be separate.
Below follows some Coq code which can be pasted directly into one
file, but it actually represents several files.
The "APPROACH_" and "FILE_" prefixes are just to keep different
approaches in separate namespaces, and to mark what would go into
separate files, but these prefixes would not show up in an actual
development.
(* ------------------------------------------------------------------ *)
Require Import Coq.omega.Omega.
Module APPROACH_Inductive_outside_Module.
Module FILE_MyLang.
Section Expression.
Variable word: Set.
Variable varname: Set.
Variable bopname: Set.
Context {varname_eq_dec: forall (x y: varname), {x = y} + {x <> y}}.
Context {bopname_eq_dec: forall (x y: bopname), {x = y} + {x <> y}}.
Inductive expr0: Set :=
| ELit0(v: word)
| EVar0(x: varname)
| EOp0(op: bopname)(e1 e: expr0).
End Expression.
Module Type PARAMETERS.
Parameter word: Set.
Parameter varname: Set.
Parameter bopname: Set.
Axiom varname_eq_dec: forall (x y: varname), {x = y} + {x <> y}.
Axiom bopname_eq_dec: forall (x y: bopname), {x = y} + {x <> y}.
End PARAMETERS.
Module Lang(P: PARAMETERS).
Import P.
(* Quirk: Here's some "once and for all" boilerplate.
Quesion: Can I get rid of this? *)
Definition expr: Set := expr0 word varname bopname.
Definition ELit: word -> expr :=
ELit0 word varname bopname.
Definition EVar: varname -> expr :=
EVar0 word varname bopname.
Definition EOp: bopname -> expr -> expr -> expr :=
EOp0 word varname bopname.
(* Quirk: More boilerplate: To match on an expr, we don't want
to match on the type arguments, so let's make them implicit.
Question: Can we do the above with Notations and reuse
the notations for pattern matching?
(I couldn't get it to work): *)
Arguments ELit0 {_} {_} {_}.
Arguments EVar0 {_} {_} {_}.
Arguments EOp0 {_} {_} {_}.
(* Quirk/Question: Can we use ELit instead of ELit0 here? *)
Fixpoint expr_size(e: expr): nat :=
match e with
| ELit0 _ => 1
| EVar0 _ => 1
| EOp0 _ e1 e2 => S (expr_size e1 + expr_size e2)
end.
End Lang.
End FILE_MyLang.
Module FILE_LibSize.
Import FILE_MyLang.
Module LibSize(P: PARAMETERS).
Module Import LangInst := Lang P.
Lemma expr_size_pos: forall (e: expr), expr_size e > 0.
Proof. induction e; simpl; omega. Qed.
End LibSize.
End FILE_LibSize.
Module FILE_LibSizeAlt.
Import FILE_MyLang.
Import FILE_LibSize.
Module LibSizeAlt(P: PARAMETERS).
Module Import LangInst := Lang P.
Module LibSizeInst := LibSize P.
Lemma expr_size_pos_alt: forall (e: expr), 0 < expr_size e.
Proof.
intros.
pose proof (LibSizeInst.expr_size_pos e).
Fail omega.
(* Quirk/Question: do I really have to do this? *)
change LibSizeInst.LangInst.expr_size with expr_size in H.
omega.
Qed.
End LibSizeAlt.
End FILE_LibSizeAlt.
Module FILE_NatNameLemmas.
Import FILE_MyLang.
Module Type PARAMETERS_NAT_NAMES <: PARAMETERS.
Parameter word: Set.
Definition varname := nat.
Definition bopname := nat.
Definition varname_eq_dec := Nat.eq_dec.
Definition bopname_eq_dec := Nat.eq_dec.
End PARAMETERS_NAT_NAMES.
Module NatNameLemmas(P: PARAMETERS_NAT_NAMES).
(* module subtyping at work: *)
Module Import LangInst := Lang P.
Fixpoint meaningless_sum(e: expr): nat :=
match e with
| ELit0 n => 0
| EVar0 x => x
| EOp0 op e1 e2 => op + meaningless_sum e1 + meaningless_sum e2
end.
End NatNameLemmas.
End FILE_NatNameLemmas.
Module FILE_CombineDifferentSpecializationLevels.
Import FILE_MyLang.
Import FILE_LibSizeAlt.
Import FILE_NatNameLemmas.
Module Combination(P: PARAMETERS_NAT_NAMES).
(* Quirk/Question: Can we avoid having one module instantiation
line for each file imported above? *)
Module Import LangInst := Lang P.
Module Import LibSizeAltInst := LibSizeAlt P.
Module Import NatNameLemmasInst := NatNameLemmas P.
Definition silly(e: expr): nat := expr_size e + meaningless_sum e.
Lemma silly_pos: forall e, 0 < silly e.
Proof.
intros. unfold silly.
pose proof (expr_size_pos_alt e).
Fail omega.
change LibSizeAltInst.LangInst.expr_size with expr_size in *.
omega.
Qed.
End Combination.
End FILE_CombineDifferentSpecializationLevels.
Module FILE_AllConcrete.
Import FILE_MyLang.
Import FILE_NatNameLemmas.
Import FILE_CombineDifferentSpecializationLevels.
(* Note: We do not do this:
Module Import MyParameters: PARAMETERS_NAT_NAMES.
Because if we did, "word" would be opaque in the remainder of this
file. Instead, we use transparent ascription: *)
Module Import MyParameters <: PARAMETERS_NAT_NAMES.
Definition word := { x: nat | 0 <= x < 256 }.
(* Quirk/Question: Why do I have to repeat all these definitions?
There's nothing unknown or unspecified. *)
Definition varname := nat.
Definition bopname := nat.
Definition varname_eq_dec := Nat.eq_dec.
Definition bopname_eq_dec := Nat.eq_dec.
End MyParameters.
Module Import LangInst := Lang MyParameters.
Module Import CombinationInst := Combination MyParameters.
Definition word_two: word.
refine (exist _ 2 _); abstract omega.
Defined.
Definition test_expr: nat := silly (EOp 3 (ELit word_two) (EVar 5)).
Eval cbv in test_expr.
Lemma test_expr_pos: 0 < test_expr.
Proof. apply silly_pos. Qed.
End FILE_AllConcrete.
End APPROACH_Inductive_outside_Module.
(* ------------------------------------------------------------------ *)
Module APPROACH_Inductive_inside_Module_Type.
Module FILE_MyLang.
Module Type PARAMETERS.
Parameter word: Set.
Parameter varname: Set.
Parameter bopname: Set.
Axiom varname_eq_dec: forall (x y: varname), {x = y} + {x <> y}.
Axiom bopname_eq_dec: forall (x y: bopname), {x = y} + {x <> y}.
End PARAMETERS.
Module Type LANG(P: PARAMETERS).
Import P.
Inductive expr: Set :=
| ELit(v: word)
| EVar(x: varname)
| EOp(op: bopname)(e1 e: expr).
(* Other modules will depend on the implementation of
this, therefore we put it in the signature *)
Fixpoint expr_size(e: expr): nat :=
match e with
| ELit _ => 1
| EVar _ => 1
| EOp _ e1 e2 => S (expr_size e1 + expr_size e2)
end.
End LANG.
Module Lang(P: PARAMETERS): LANG P.
Include (LANG P).
End Lang.
End FILE_MyLang.
Module FILE_LibSize.
Import FILE_MyLang.
(* Here we also parameterize over LANG rather than over
PARAMETERS only, because we should not instantiate Lang several
times, because if we do, we get different copies of expr. *)
Module LibSize(P: PARAMETERS)(L: LANG P).
Import P.
Import L.
(* Question: We could also have declared "L: Lang", and then do
Module Import LInst := L P.
instead of "Import L". What's the difference? *)
Lemma expr_size_pos: forall (e: expr), expr_size e > 0.
Proof. induction e; simpl; omega. Qed.
End LibSize.
End FILE_LibSize.
Module FILE_LibSizeAlt.
Import FILE_MyLang.
Import FILE_LibSize.
Module LibSizeAlt(P: PARAMETERS)(L: LANG P).
Import P.
Import L.
Module Import LibSizeInst := LibSize P L.
Lemma expr_size_pos_alt: forall (e: expr), 0 < expr_size e.
Proof.
intros.
pose proof (expr_size_pos e).
(* NoQuirk:
Here, omega works directly, without "change" before. *)
omega.
Qed.
End LibSizeAlt.
End FILE_LibSizeAlt.
Module FILE_NatNameLemmas.
Import FILE_MyLang.
Module Type PARAMETERS_NAT_NAMES <: PARAMETERS.
Parameter word: Set.
Definition varname := nat.
Definition bopname := nat.
Definition varname_eq_dec := Nat.eq_dec.
Definition bopname_eq_dec := Nat.eq_dec.
End PARAMETERS_NAT_NAMES.
Module NatNameLemmas(P: PARAMETERS_NAT_NAMES)(L: LANG P).
Import P.
Import L.
(* NoQuirk: Here we can use ELit instead of ELit0 etc *)
Fixpoint meaningless_sum(e: expr): nat :=
match e with
| ELit n => 0
| EVar x => x
| EOp op e1 e2 => op + meaningless_sum e1 + meaningless_sum e2
end.
End NatNameLemmas.
End FILE_NatNameLemmas.
Module FILE_CombineDifferentSpecializationLevels.
Import FILE_MyLang.
Import FILE_LibSizeAlt.
Import FILE_NatNameLemmas.
Module Combination(P: PARAMETERS_NAT_NAMES)(L: LANG P).
Import P.
(* Quirk/Question: Can we avoid having one module instantiation
line for each file imported above? *)
Import L.
Module Import LibSizeAltInst := LibSizeAlt P L.
Module Import NatNameLemmasInst := NatNameLemmas P L.
Definition silly(e: expr): nat := expr_size e + meaningless_sum e.
Lemma silly_pos: forall e, 0 < silly e.
Proof.
intros. unfold silly.
pose proof (expr_size_pos_alt e).
(* NoQuirk: omega works directly *)
omega.
Qed.
End Combination.
End FILE_CombineDifferentSpecializationLevels.
Module FILE_AllConcrete.
Import FILE_MyLang.
Import FILE_NatNameLemmas.
Import FILE_CombineDifferentSpecializationLevels.
(* Note: We do not do this:
Module Import MyParameters: PARAMETERS_NAT_NAMES.
Because if we did, "word" would be opaque in the remainder of this
file. Instead, we use transparent ascription: *)
Module Import MyParameters <: PARAMETERS_NAT_NAMES.
Definition word := { x: nat | 0 <= x < 256 }.
(* Quirk/Question: Why do I have to repeat all these definitions?
There's nothing unknown or unspecified. *)
Definition varname := nat.
Definition bopname := nat.
Definition varname_eq_dec := Nat.eq_dec.
Definition bopname_eq_dec := Nat.eq_dec.
End MyParameters.
Module Import LangInst := Lang MyParameters.
Module Import CombinationInst := Combination MyParameters LangInst.
Definition word_two: word.
refine (exist _ 2 _); abstract omega.
Defined.
Definition test_expr: nat := silly (EOp 3 (ELit word_two) (EVar 5)).
Eval cbv in test_expr.
Lemma test_expr_pos: 0 < test_expr.
Proof. apply silly_pos. Qed.
End FILE_AllConcrete.
End APPROACH_Inductive_inside_Module_Type.
(* -----------------------------------------