The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

Dear Alexandre,

> There seems to be a difference of opacity between a definition that is
> made opaque, and a Qed at the end of a lemma:

Indeed.

> Is there a good reason for that?

My understanding is that it is not so simple to allow the existence of such a
command, labelling  some reductions that used to be allowed but should be
blocked from now on.
Actually you might meanwhile have defined some other (well-typed) terms whose
type-checking depend on the reduction you now decide to block.

Suppose you define a function:

  Definition f (x : nat) := x.

and prove

  Lemma foo : f 0 = 0.

or even define a dependent term whose type depends on (f 0) being convertible
with 0.

I do not know what should be the status of such terms "after" a
"RealOpaque f" declaration. Do they become ill-typed?

 And if not, what would be a
> "RealOpaque" command, to avoid ma opaque constant to be "basically
> transparent"?

I have however learned from Georges Gonthier some tricks that may help you to
achieve what you ask for.

The first solution is to tag terms with explicitly blocked cases:

First define an opaque tt:

  Lemma master_key : unit. Proof. exact tt. Qed.

Now this function turns a term of type A into a "locked" one:

  Definition locked A := let 'tt := master_key in fun x : A => x.

From now on, (locked t) and t are provably equal but not convertible, since 
the
iota-reduction is blocked by the opaque status of master_key:

  Lemma lock A x : x = locked x :> A.
  Proof. now unfold locked; case master_key. Qed.

An other option is to use the module system to "opacify" your definition.
Suppose I want an opaque version of the identity function on nat:

I start by defining a signature for my opaque identity, which specifies the 
type
of the constant and what this constant should be provably equal to:

  Module Type fDefSig.
  Parameter f : nat -> nat.
  Axiom fEdef : f = (fun n : nat => n).
  End fDefSig.

Then I provide an implementation of this interface:

  Module fDef : fDefSig.
  Definition f : nat -> nat := (fun n : nat => n).
  Definition fEdef := refl_equal f.
  End fDef.

And finally I export the module:
  Export fDef.

Hope this helps.

Best,

assia