search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.77k stars 638 forks source link

selectively bypassing opacity in reduction #4916

Open coqbot opened 8 years ago

coqbot commented 8 years ago

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4916 From: @jonleivent Reported version: 8.5

See also: BZ#4639

coqbot commented 8 years ago

Comment author: @jonleivent

When writing complex tactics, it sometimes makes sense to wrap various parts of a goal first in an opaque id function to protect them from tactics, then remove this id function later.

For most cases, it works to do:

Definition block {T}(a:T) := a. Opaque block.

and then do various "change X with (block X) in ...", then the opposite direction changes to undo. Note that without the "Opaque block", some tactics could accidentally reduce blocks away.

However, sometimes a block goes under binders where it cannot be reached via "change (block X) with X". In such cases, it would be nice to be able to temporarily make block transparent, as with something like:

"cbv Delta [block]"

where the capitalized Delta denotes the desire to bypass opacity for the constants mentioned in []'s.

coqbot commented 8 years ago

Comment author: @jonleivent

Nevermind...

I realized one can do

Definition ublock {T}(a:T} :=a.

then do "change @ block with @ ublock; unfold ublock".

Oh - that's probably also the answer to 4639 - create another constant with the Argument setting one wants, then change between them...