The Coq mailing list

[Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>]

Hello dear Coq users,

I recently discovered something that tricked me a bit. Indeed, modules
are presented as a way to have a “massive abstraction” as stated in the
manual, and I agree that hiding everything under an opaque layer is a
valuable safety net.

Yet this neat opacity is itself problematic, as a Print Assumptions
command on a term using contents from an abstracted module contains
those abstracted terms, without any considerations to the way they are
defined.

The following example makes things clearer:

(** Excerpt **)

Module Type Infinite.
Parameter t : Type.
Parameter fresh : forall l : list t, {x : t | ~ In x l}.
End Infinite.

Module Infinite_nat : Infinite.
Definition t := nat.
Definition fresh := (* insert the expected axiom-free code here *).
End Infinite_nat.

Definition fresh' := Infinite_nat.fresh.

Print Assumptions fresh'.

(* Here we get Infinite_nat.t and Infinite_nat.fresh even though they
are closed in the global context. *)

(** End of excerpt **)

I assume that I want somehow to have my cake and eat it, but abstracting
everything is in my opinion the only usefulness of modules which can
otherwise be emulated through records (and well, they can tactics).

So my questions are the following:

1. Can we achieve the same thing and still get the correct Assumptions?
(with the same ease as modules, i.e. without using a bunch of Opaque...)
2. To Coq devs: can the Print Assumptions command be patched to go
through the content of modules and not stop at the root?

I assume that the compiled files of modules still contains the code
(coqcheck can still check, right?) so I imagine that the second point
can and should be fixed. Maybe I should file a bug report?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature