coq-tricks

coq-tricks copied to clipboard

Suppose we have something like

(* file_1.v*)
Module A.
    Inductive Ind_1 : Set :=
    | TERM_1
    | TERM_2
    .
End A.

And we want to import this module in another file:

(* file_2.v *)
Require file_1.A.
(* For brevity we rename this module in this new file *)
Module A := file_1.A.

Everything should work fine.

However if we have more content, for example, the Schemes in the Coq:

(* file_1.v *)
Module A.
    Inductive Ind_1 : Set :=
    | TERM_1
    | TERM_2
    .
    Scheme Boolean Equality for Ind_1. 
End.

It turns out that file_2 doesn't import the generated scheme as supposed and we cannot use it in file_2.

The correct solution is a slightly different way to import the module:

(* file_2.v *)
Require file_1.A.
Module A.
  Include file_1.A.
End A.

Previously I have referred to the official documentation, and the official introduction to the Module system says that these two ways should be completely equivalent. Turns out to be not, and turns out that this can be a pretty special Coq trick.