The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I am also sympathetic to the other side of the story. To that side, let me add that CoqIde's asynchronous editing also depends on Qed-ed things not influencing transparent definitions.

However, with the ability to reify opaque definitions, we have already lost that invariant:

(* assuming template-coq is installed *)

Require Import Template.Template.

Require Import Template.Ast.

Open Scope string_scope.

Lemma snd : forall A B : Set, A * B -> B.

Proof.

  intros ? ? p. destruct p. assumption.

Qed.

Eval vm_compute in (snd _ _ (1,2)). (*stuck*)

Quote Recursively Definition pp := snd.

Print pp.

Fixpoint getFirstConstr (p:program) : option term :=

match p with

| PConstr _ t _ => Some t

| PType _ _ _ p => getFirstConstr p

| PAxiom _ t p => getFirstConstr p

| PIn _ => None

end.

(* getFirstConstr extracts the definition reified of snd *)

Eval compute in (getFirstConstr pp).

(*

     = Some

         (tLambda (nNamed "A") (tSort sSet)

            (tLambda (nNamed "B") (tSort sSet)

               (tLambda (nNamed "p")

                  (tApp (tInd (mkInd "Coq.Init.Datatypes.prod" 0))

                     (tRel 1 :: (tRel 0 :: nil)%list))

                  (tCase (mkInd "Coq.Init.Datatypes.prod" 0, 2)

                     (tLambda (nNamed "p")

                        (tApp (tInd (mkInd "Coq.Init.Datatypes.prod" 0))

                           (tRel 2 :: (tRel 1 :: nil)%list)) (tRel 2)) 

                     (tRel 0)

                     ((2,

                      tLambda (nNamed "a") (tRel 2) (tLambda (nNamed "b") (tRel 2) (tRel 0)))

                      :: nil)))))

     : option term

*)

Ltac computeExtract f:=

(let t:= eval compute in f in 

match t with

|Some ?xx => constr:xx

end).

Make Definition snd_t := 

  ltac:(let t:= computeExtract (getFirstConstr pp) in exact t).

Print snd_t.

(*

snd = fun (A B : Set) (p : A * B) => let (_, b) := p in b

     : forall A B : Set, A * B -> B

*)

In summary, I agree that there is a drawback to losing the invariant about the irrelevance of opaque bodies.

Nevertheless, I would let the user be able to, in certain parts of their development, sacrifice that invariant for something they may value more.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, Nov 15, 2016 at 2:25 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

Although I am sympathetic to Abhishek's use case, I think there is another side to this story.

Currently, lemmas ended with Qed have the property that, during maintenance, one knows that their proofs can be altered without consequences elsewhere so long as each lemma's type is preserved. This is especially important to proofs done with Ltac, as since the semantics of Ltac is ephemeral (a euphemism, if ever there was one), the exact proof term (or even equivalence up to convertibility) might be altered from version to version of Coq even if the tactical proof itself remains valid.  If a mechanism such as the one Abhishek is asking for is provided, then its use would diminish maintainability in such cases.

As for cases from the standard library that are proved via Ltac but for which transparency may be desirable, perhaps these should be made transparent via Defined and then unit tested for equivalence to the desired proof term (although, then, why use Ltac at all here, if the exact proof term is available?  Perhaps just for pedagogic reasons?), so that the impact of tactic-based proof term variation across versions of Coq would then be immediately felt at unit test time, giving more work to Coq devo but less work to users.

-- Jonathan

On 11/15/2016 01:48 PM, Abhishek Anand wrote:

Hi Maxime,

I often end up with functions that don't compute because they use opaque
definitions/lemmas (saved using Qed) at critical places, e.g. discriminees
of match, guards of fixpoints.
Also, I vaguely remember instances when Coq's productivity check rejected
my proofs because of the opacity of some subcomponents.

I am not the only one with such misfortune of not being able to use (e.g.
for proof by computation) what has been paid for (by constructive proofs):
https://sympa.inria.fr/sympa/arc/coq-club/2013-09/msg00033.html
https://sympa.inria.fr/sympa/arc/coq-club/2015-02/msg00075.html
https://sympa.inria.fr/sympa/arc/coq-club/2015-11/msg00173.html

On this list, there have been many discussions about workarounds for
specific cases, particularly when the opaque lemmas/definitions are about
decidable properties:
https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00081.html

Even in those cases, some manual work is needed : one needs to identify the
critical opaque parts and redefine them.
I want something that effortlessly always restores canonicity.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/

On Tue, Nov 15, 2016 at 12:09 PM, Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi Abishek,

Can you share a bit of context about your use case?

Thanks!

Maxime.

On 11/15/16 18:03, Abhishek Anand wrote:

My understanding is that once a definition is saved with Qed, there is
no way to make it transparent.
Is that true?

If so, has someone written a plugin/tool to take a definition (say of X)
with possibly opaque parts and recursively transparently duplicate those
parts to create a new totally transparent definition (say X_t)?

Perhaps no new Coq plugin is needed -- template-coq
<https://github.com/gmalecha/template-coq>'s `Quote Recursively` already
reifies opaque bodies. Also, it has "Make Definition" to reflect back
encodings of definitions. It seems possible to write Ltac/Gallina
functions that use template-coq commands to achieve the above-mentioned
transparentification. Am I overlooking some difficulty?

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/~aa755/>