Stream: Coq users

Topic: ✔ Computing through opaque definitions


view this post on Zulip Kiran Gopinathan (May 30 2022 at 09:10):

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?

view this post on Zulip Paolo Giarrusso (May 30 2022 at 10:16):

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

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 10:18):

also this has nothing to do with proof irrelevance

view this post on Zulip Paolo Giarrusso (May 30 2022 at 10:19):

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

view this post on Zulip Paolo Giarrusso (May 30 2022 at 10:20):

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

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 10:21):

You can definitely hack a plugin to do that.

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 10:22):

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

view this post on Zulip Ana de Almeida Borges (May 30 2022 at 10:44):

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.

view this post on Zulip Kiran Gopinathan (May 30 2022 at 11:08):

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.

view this post on Zulip Kiran Gopinathan (May 30 2022 at 11:09):

@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?

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 11:11):

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

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 11:11):

there is no flag

view this post on Zulip Kiran Gopinathan (May 30 2022 at 11:12):

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.

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 11:13):

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

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 11:14):

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

view this post on Zulip Kiran Gopinathan (May 30 2022 at 11:15):

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!

view this post on Zulip Kiran Gopinathan (May 30 2022 at 11:16):

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?

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 11:18):

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

view this post on Zulip Ana de Almeida Borges (May 30 2022 at 11:19):

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.)

view this post on Zulip Kiran Gopinathan (May 30 2022 at 11:21):

Yup, thanks everyone, that all makes sense.

view this post on Zulip Paolo Giarrusso (May 30 2022 at 11:59):

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

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:01):

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"

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:02):

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

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 12:02):

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

view this post on Zulip Michael Soegtrop (May 30 2022 at 12:09):

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

view this post on Zulip Karl Palmskog (May 30 2022 at 12:09):

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

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 12:11):

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

view this post on Zulip Kiran Gopinathan (May 30 2022 at 12:12):

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.

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:18):

@Michael Soegtrop "Qed-opaque" != "Opaque-opaque", so "opaque" is basically an anti-word here: it maximizes misunderstandings rather than communication :-(

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:20):

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

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 12:21):

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

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:22):

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

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:23):

Print talks about "opaque proofs" IIRC :thinking:

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 12:23):

As a dev I'd call Qed constants "opaque" and Opaque constants something else

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 12:24):

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

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 12:25):

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")

view this post on Zulip Kenji Maillard (May 30 2022 at 12:26):

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

view this post on Zulip Ali Caglayan (May 30 2022 at 12:27):

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

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:35):

@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.

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 12:37):

I agree, I was just reminding the dev jargon

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:40):

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

view this post on Zulip Michael Soegtrop (May 30 2022 at 15:45):

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.

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 15:49):

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

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 15:49):

(module subtyping treats Qed proofs as axioms)

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 15:51):

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

view this post on Zulip Ali Caglayan (May 30 2022 at 16:30):

Any good reason why we don't already?

view this post on Zulip Michael Soegtrop (May 30 2022 at 16:37):

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 ...

view this post on Zulip Paolo Giarrusso (May 30 2022 at 17:18):

@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)

view this post on Zulip Paolo Giarrusso (May 30 2022 at 17:19):

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

view this post on Zulip Paolo Giarrusso (May 30 2022 at 17:20):

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).

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 17:22):

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.

view this post on Zulip Paolo Giarrusso (May 30 2022 at 17:23):

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

view this post on Zulip Notification Bot (May 31 2022 at 05:26):

Kiran Gopinathan has marked this topic as resolved.

view this post on Zulip Michael Soegtrop (May 31 2022 at 07:05):

@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: Jun 20 2024 at 13:02 UTC