The Coq mailing list

[Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>]

Hi Michael,


have you tried something like:

~~~~
Set Implicit Arguments.

Definition opaque X (P : X) := P.
Arguments opaque X {P}.

Check @opaque _ (ltac:(omega) : 1 < 2).
~~~~

which gives

~~~~
opaque (1 < 2)
     : 1 < 2
~~~~

(Alternatively, if you construct the term using a proof script, `apply
opaque` also works.)


However, this doesn't really remove the proof from the proof term, it
just "hides" the proof while printing, I.e. if you use `Set Printing
Implicit`, the proof term is still shown.

If you want to make the actual proof "opaque" in the sense of "Qed.",
you could use the tactical `abstract`, for example:

~~~~~
Example ex : 1 < 2.
Proof.
  abstract omega.
Defined.

Print ex.

ex = ex_subproof
     : 1 < 2
~~~~~

However, this only works (AFAIK), if the proof consists of just one tactic.


Then, there are other possibilities, for example using Program.


Sincerely
Maximilian



On 05/15/2018 06:10 PM, Soegtrop, Michael wrote:
> Dear Coq Users/Team,
> 
>  
> 
> I did some experiments with dependent types again, and I think the thing
> I am sometimes missing is an opaquify operator. Terms of dependent types
> usually contain a mixture of “data” expressions one is interested in and
> “proof” expressions for which just the type is interesting. The idea is
> that if I have a term, opaquify(term) makes the term as such opaque,
> only the type remains visible. The term cannot be unified any more, only
> its type.  When printing an opaquified term, it is printed as something
> like opaque:<type> or maybe just opaque in case the type can be inferred.
> 
>  
> 
> I can use notations and to a certain extent opaque proofs to hide the
> proof parts of terms of dependent type, but sometimes I think it might
> also help Coq’s performance to know that it should never look into the
> term as such, just as if it would be an opaque proof term. Another
> benefit would be less distraction and maybe a better understanding of
> the users.
> 
>  
> 
> My question: am I doing something wrong when I end up at this thought?
> How are others handling this?
> 
>  
> 
> Best regards,
> 
>  
> 
> Michael
> 
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928
>