The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

In order to prevent the Coq unifier from diverging on failing to unify
certain terms, we started sealing some of our definitions with modules.
This usually looks roughly as follows:

> Definition heap_mapsto_def `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang 
> Σ :=
>   auth_own heap_name {[ l := Excl v ]}.
> (* Perform sealing *)
> Module Type HeapMapstoSig.
>   Parameter heap_mapsto : ∀ `{heapG Σ} (l : loc) (v: val), iPropG heap_lang 
> Σ.
>   Axiom heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def.
> End HeapMapstoSig.
> Module Export HeapMapsto : HeapMapstoSig.
>   Definition heap_mapsto := @heap_mapsto_def.
>   Definition heap_mapsto_eq := Logic.eq_refl (@heap_mapsto).
> End HeapMapsto. 

We copied this trick from ssreflect. I would not be surprised to hear
that other larger developments are using something similar.

So I wonder, would it be worth adding a feature to Coq where I could
write something like

Sealed Definition heap_mapsto `{heapG Σ} (l : loc) (v: val):
           iPropG heap_lang Σ :=
   auth_own heap_name {[ l := Excl v ]}.

and it would automatically add "heap_mapsto" of appropriate type, make
it as opaque as "Qed."-Lemmas (or as opaque as fields sealed via a
signature, I am not sure if there is any difference), and add a term
"heap_mapsto_eq" or "heap_mapsto_def" that proves that "heap_mapsto" is
equal to its definition?
That would significantly reduce the syntactic overhead and redundancy
associated with the trick that we have to pull off now, to get Coq to
behave. As a bonus, it should work within sections.

Kind regards,
Ralf