The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Can't you use something like:

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

-- 
JH




Le 24/02/2016 14:13, Robbert Krebbers a écrit :
> 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
>>>
>>

Attachment: signature.asc
Description: OpenPGP digital signature