The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Dear Jeehoon,

Opaque is merely a hint to the kernel and some tactics to avoid 
unfolding definitions. Many tactics, as well as unification, do not 
really respect Opaque. For example:

Definition foo := 0.
Opaque foo.

Goal foo = 0.
  Fail unfold foo. (* Error: Cannot coerce foo to an evaluable 
reference. *)
  reflexivity. (* succeeds, reflexivity does not care about Opaque *)
Qed.

Best,

Robbert

On 02/24/2016 02:05 PM, Jeehoon Kang wrote:
> Did you try Opaque?  I am not sure it is what you want, but it controls the
> visibility of the definitions.
>
> https://coq.inria.fr/refman/Reference-Manual008.html#hevea_command141
> 2016. 2. 24. 오후 9:52에 "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