Heyo all,

Is there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts.

I understand why Coq doesn’t do this by default, and guess it would probably interact in unfavourable ways with proof irrelevance. My aim is not to use this computation as part of a proof, but rather purely for debugging/meta-analysis - much like how the Print command can display the proof terms associated with lemmas, even if they are actually opaque.

Is it possible, using the Coq api if necassary, to perform computation ignoring opaqueness of terms?

Think something like a PrintReduced command that reduces its argument as much as possible (until it reaches constructors, existential variables or axioms - things for which the definition doesn’t exist at all).

Is this possible while reusing Coq's existing evaluation mechanisms (a flag perchance)? or is this something that would require a much larger architectural shift?

TLDR today: If opaque means Qed, there's no way; if opaque means Opaque (a very different thing), just use vm_compute.

also this has nothing to do with proof irrelevance

But if you're talking about Qed, there might be alternatives, depending on why you need this.

(ah, just saw the cross-post to https://coq.discourse.group/t/how-to-evaluate-proof-terms-through-opaque-definitions/1664)

You can definitely hack a plugin to do that.

I'm not sure it'd be added as a proper command though, because it goes in the wrong direction w.r.t. the invariants we want to have on Qed proofs

I don't know how it interacts with Opaque / Qed, but maybe look into QuickChick. It can generate examples from your code and test properties by randomly generating such examples.

Thanks for the advice, I guess I was mistaken about the interaction with proof irrelevance. Opaque in this context specifically refers to proofs completed with Qed. I understand Coq doesn't do that by default or through any of the standard commands, but I'm willing to write a plugin to do this if needed.

@Pierre-Marie Pédrot , you mention it would be possible to hack a plugin to do that - what would be the best way of implementing this? I was thinking of just folding over Constr.t terms and then updating any instance of opaque constants with their definitions, but this seems a bit hacky - is there an easier way to do this? a flag in Coq's evaluator?

pick your favorite evaluator from lazy/cbn/cbv and replace calls to Environ.constant_value_in by something which works on OpaqueDef

there is no flag

Gaëtan Gilbert said:

also this has nothing to do with proof irrelevance

Does it really have nothing to do with proof irrelevance? Why does Coq not allow expanding Qed definitions? I thought proof irrelevance meant that proofs do not need to care exactly how the witness for a particular proposition is constructed (which may not be the case if the proofs could reflect on the particular witness by expanding Qed defined terms), and hence why Qed is so hard to compute through.

and btw if someone does opaqueness through modules like

```
Module Type hide.
Parameter v : nat.
End hide.
Module M : hide.
Definition v := 0.
End M.
```

it's much harder to write something to reduce it

Kiran Gopinathan said:

Gaëtan Gilbert said:

also this has nothing to do with proof irrelevance

Does it really have nothing to do with proof irrelevance? Why does Coq not allow expanding Qed definitions? I thought proof irrelevance meant that proofs do not need to care exactly how the witness for a particular proposition is constructed (which may not be the case if the proofs could reflect on the particular witness by expanding Qed defined terms), and hence why Qed is so hard to compute through.

you don't have to use proof irrelevance to use qed and vice versa

Gaëtan Gilbert said:

pick your favorite evaluator from lazy/cbn/cbv and replace calls to Environ.constant_value_in by something which works on OpaqueDef

Perfect thanks, got it!

Gaëtan Gilbert said:

you don't have to use proof irrelevance to use qed and vice versa

Good point, yes, that makes sense - I guess it is a misuse of terminology to use Proof irrelevance to refer to Qed and opaqueness.

Out of curiosity then, why is there no easy way to reduce terms that use opaque definitions?

because the point of being opaque is that you can't reduce them

it's like asking why there isn't an easy way to call private methods of a class in some object oriented language

Proof irrelevance is an axiom:

```
Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
```

(I got the feeling it was possibly you were using the term to mean something else, sorry if not.)

Yup, thanks everyone, that all makes sense.

actually, I have seen learning materials stating a relation with (another meaning of) proof irrelevance

that is, usually, in mathematics, you're not supposed to _need_ to look into a proof, because of "proof irrelevance" as a design principle — which is why Qed usually works well.

EDIT: I should say I _don't know_ if this is good terminology, but I'm not sure/can't say it's "wrong"

Out of curiosity then, why is there no easy way to reduce terms that use opaque definitions?

Beyond what Gaëtan said, it's also because it's often unlikely to terminate quickly

@Paolo Giarrusso it's worse than that, in first-order logic (and therefore in ZF) proofs are not even proper objects of the theory

Maybe I am missing something, but didn't the OP ask essentially for Transparent and/or with_strategy?

hmm, I don't think proofs are considered theory objects even in HOL? They are more like an implementation-level phenomenon

@Karl Palmskog indeed, HOL doesn't treat proofs as first-class objects either. That's a landmark of dependent types.

Michael Soegtrop said:

Maybe I am missing something, but didn't the OP ask essentially for Transparent and/or with_strategy?

Transparent doesn't allow reducing theorems ended with Qed - it can be used to "undo" making definitions opaque using `Opaque`

, but not Qed.

@Michael Soegtrop "`Qed`

-opaque" != "`Opaque`

-opaque", so "opaque" is basically an anti-word here: it maximizes misunderstandings rather than communication :-(

I've used "`Qed`

ed constants" and I'd love a better one. @Pierre-Marie Pédrot do you have an acceptable word here?

I'd call it abstract or something (by analogy with functor arguments), but that's not the accepted terminology.

was thinking of that, but here we need to say "abstract definitions with a body" — how's that "non-body body" called?

`Print`

talks about "opaque proofs" IIRC :thinking:

As a dev I'd call `Qed`

constants "opaque" and `Opaque`

constants something else

There is a whole spectrum for the latter since you can specify a number for priority

and they're not really opaque, the kernel is perfectly allowed to unfold them (this is required) and the upper layers tend to disregard it anyways (that's a "historical design choice")

When you say required, you mean for metatheoretical properties such as subject reduction/canonicity I guess ?

Pierre-Marie Pédrot said:

and they're not really opaque, the kernel is perfectly allowed to unfold them (this is required) and the upper layers tend to disregard it anyways (that's a "historical design choice")

For things unfolding Qed see: https://github.com/coq/coq/issues/15874

@Pierre-Marie Pédrot I understand but unless we deprecate the `Opaque`

command, reserving "opaque" for `Qed`

won't work well. Imagine writing the docs for `Opaque`

.

I agree, I was just reminding the dev jargon

thanks, that's all I could ask for from you :-)

Is there a good reason why one can't make Qeded things transparent again? The .vo files do contain the proof terms since Print can load them, so why can't Transparent load them? Interesting that I never ran into this - but then I am using Defined were I might need it.

Probably not the reason, but you could break soundness using fancy functors

(module subtyping treats Qed proofs as axioms)

that's a feature, we ought to treat Qed proofs as axioms essentially everywhere

Any good reason why we don't already?

It is somehow too much for my physicist brains to understand how giving an explicit witness for something which has been treated as axiom so far can break soundness. Can't one create similar effects with using defines and transparent vs. opaque module ascription? Hmm - I darkly remember there was some soundness bug around this ...

@Michael Soegtrop postulating `a = b`

is sound if they are axioms but it is not if they are also equal to other things (say `a := 1`

and `b := 2`

)

and module subtyping allows to implement an opaque `a := 1`

via `a := 2`

e.g. I think PMP’s saying that if a module interface has `Definition a : nat. Proof. exact 1. Qed.`

, the implementation can use `Definition a := 2.`

(and I think I’ve used this).

soundness issues with modules usually means functors are involved

something like

```
Module Type T.
Definition v : bool.
Proof. exact false. Qed.
End T.
Module F(X:T).
Deopacify X.v.
Lemma bad : X.v = false.
Proof. reflexivity. Qed.
End F.
Module M.
Definition v := true.
End M.
Module FM := F M.
Check FM.bad : true = false.
```

oh thanks, I was wondering how to actually get the paradox

Kiran Gopinathan has marked this topic as resolved.

@Gaëtan Gilbert : thanks for the nice example! To summarize: if I replace the `Qed`

for `T.v`

with `Defined`

, `M`

fails to type check as argument for `F`

. But if I close `T.v`

with `Qed`

, `F M`

does type check and this means it must not be allowed to undo the opaqueness of `T.v`

. Not easy to get these things right, as it looks ...

Last updated: Oct 05 2023 at 02:01 UTC