coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Feature Request: Sealed definitions

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Feature Request: Sealed definitions
Date: Wed, 24 Feb 2016 14:44:24 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:fNSTQBe80wttCZlCyG/Dnn7WlGMj4u6mDksu8pMizoh2WeGdxc64bR7h7PlgxGXEQZ/co6odzbGG7Oa9CSddut6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcCDKFgTzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB18flhQAIRXD41muXIr3vQP/rus4wzaBe8rsQuZnCnyZ8653RUqw2288PDkj/TSPhw==

Hi,

> 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.

How would I selectively unroll this definition in order to prove any
lemmas about it?
I was unable to make that happen.

Kind regards,
Ralf

Re: [Coq-Club] Feature Request: Sealed definitions, (continued)