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.