Parameterizing a type system over an abstract data type with Coq's module system

Using Coq
1

I want to parameterize my type system over an abstract data type. The goal is to show that the system is type sound for all instances of the abstract data type. However, there are some special properties that only hold for specific instances. It’s unclear to me how to use Coq’s module system to structure my development. Here’s a minimal example that illustrates the problem I ran into with modules:

Module Type num_sig.

Parameter num_type : Type.
Parameter add_num : num_type -> num_type -> num_type.

End num_sig.

Module syntax (Import n : num_sig).
  Inductive tm : Type :=
  | Const : num_type -> tm
  | Add : tm -> tm -> tm.

  Fixpoint eval_tm (t : tm) : num_type :=
    match t with
    | Const n => n
    | Add t1 t2 => add_num (eval_tm t1) (eval_tm t2)
    end.
End syntax.

Module eval_add (Import n : num_sig).
  Module syntax_n := syntax n.
  Import syntax_n.
  Lemma eval_Add_eq :
    forall t1 t2, eval_tm (Add t1 t2) = add_num (eval_tm t1) (eval_tm t2).
  Proof. intros; reflexivity. Qed.
End eval_add.

Module eval_const (Import n : num_sig).
  Module syntax_n := syntax n.
  Import syntax_n.
  Lemma eval_const_eq :
    forall t1, eval_tm (Const t1) = t1.
  Proof. intros; reflexivity. Qed.
End eval_const.

Module nat_num : num_sig.
  Definition num_type := nat.
  Definition add_num x y := x + y.
End nat_num.

Module syntax_nat_num := syntax nat_num.
(* There is no way to instantiate eval_const or eval_add to make the
lemmas eval_const and eval_add available to the module syntax_nat_num! *)
(* eval_const and eval_add both make their own copies of syntax nat_num!! *)

The syntax module is defined as a functor that takes a num_sig so I can later choose to instantiate to more specific instances of num_sig if I want to. The issue is that I can’t really split the properties about the syntax into different modules. I can instantiate syntax with the nat_num instance, but I can’t use the proofs from eval_const or eval_add because each of them has its own copy of syntax instantiated to nat_num.

I’ve avoided typeclasses because my use case requires a trivial resolution algorithm. Each file will only refer to the one abstract data type declared at the top level. Using implicit arguments seems to be an overkill and brings a lot of headaches related to unification.

2

After some digging, I found this old post that describes the exact same problem that I ran into: https://coq-club.inria.narkive.com/ux8RG4m7/module-best-practices

The idea is to change the syntax into a module type and use Include to avoid duplicating the definitions. Here’s the revised code that is able to use the lemmas defined in the module eval_add:

Module Type num_sig.

Parameter num_type : Type.
Parameter add_num : num_type -> num_type -> num_type.

End num_sig.

Module Type syntax (Import n : num_sig).
  Inductive tm : Type :=
  | Const : num_type -> tm
  | Add : tm -> tm -> tm.

  Fixpoint eval_tm (t : tm) : num_type :=
    match t with
    | Const n => n
    | Add t1 t2 => add_num (eval_tm t1) (eval_tm t2)
    end.
End syntax.

Module eval_add
  (Import n : num_sig)
  (Import s : syntax n).
  Lemma eval_Add_eq :
    forall t1 t2, eval_tm (Add t1 t2) = add_num (eval_tm t1) (eval_tm t2).
  Proof. intros; reflexivity. Qed.
End eval_add.

Module eval_const
  (Import n : num_sig)
  (Import s : syntax n).
  Lemma eval_const_eq :
    forall t1, eval_tm (Const t1) = t1.
  Proof. intros; reflexivity. Qed.
End eval_const.

Module nat_num : num_sig.
  Definition num_type := nat.
  Definition add_num x y := x + y.
End nat_num.

Module syntax_nat_num : syntax nat_num.
  Include syntax nat_num.
End syntax_nat_num.

Module M1 := eval_add nat_num syntax_nat_num.
Module M2 := eval_const nat_num syntax_nat_num.
Lemma const_add1_eq :
  forall (n1 n2 : nat_num.num_type),
    syntax_nat_num.eval_tm
      (syntax_nat_num.Add
         (syntax_nat_num.Const n1)
         (syntax_nat_num.Const n2)) = nat_num.add_num n1 n2.
Proof.
  intros.
  rewrite M1.eval_Add_eq.
  reflexivity.
Qed.