Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Tuning opaqueness

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tuning opaqueness


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: AUGER Cédric <sedrikov AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Tuning opaqueness
  • Date: Mon, 9 Jul 2012 15:29:06 -0400

Yes, this is exactly what I want, except that putting the relevant definitions in the Record breaks sort-polymorphism, because only inductive definitions get sort-polymorphism, not definitions and let statements.

-Jason

On Mon, Jul 9, 2012 at 1:57 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:
Le Sat, 7 Jul 2012 19:20:34 -0400,
Jason Gross <jasongross9 AT gmail.com> a écrit :

> Hi,
> Is there a way to make a constant opaque or transparent within a
> tactic? Relatedly, is there a way to state that a constant should
> usually be opaque, unless its first few arguments match a specific
> pattern?
>
> The context is that I've moved some [Record] fields to parameters, so
> that I get sort-polymorphism, but I want to pretend that these things
> are record fields, so that I can build tactics that match on them and
> so that the "fields that are really parameters" carry along the
> information of what record they come from.  So I generally want these
> things to be opaque, so that [simpl] and [hnf] don't unfold them, but
> I sometimes need to see inside them.  (Currently, there seems to be a
> theorem that I can only [eapply] if I make these transparent.)  So I
> either want to tune how opaque these constants are, and/or I want to
> be able to flip opaqueness back and forth inside of tactics.
>
> Thanks!
>
> -Jason

Not sure if it is useful, but Records accepts definitions as fields.

For instance you can define:

Record foo (x : nat) :=
{ n : nat
; from_param := x + n
; o : nat
; spec : o = from_param
}.

Which is the same as
Record foo (x : nat) :=
{ n : nat
; o : nat
; spec : o = x + n
}.
Definition from_param x (r:foo x) := x + (n r).

But in the first example, "from_param" is folded in the definition of
the record, which may be what you whish.

If I well remember, it was not documented in 8.3, and I didn't checked
if it was in 8.4.




Archive powered by MHonArc 2.6.18.

Top of Page