Kiran Gopinathan (May 30 2022 at 09:10): 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?
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.
Gaëtan Gilbert (May 30 2022 at 10:18):also this has nothing to do with proof irrelevance
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.
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)
Pierre-Marie Pédrot (May 30 2022 at 10:21):You can definitely hack a plugin to do that.
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
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.
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.
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?
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
Gaëtan Gilbert (May 30 2022 at 11:11):there is no flag
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.
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
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
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!
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?
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
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.)
Kiran Gopinathan (May 30 2022 at 11:21):Yup, thanks everyone, that all makes sense.
Paolo Giarrusso (May 30 2022 at 11:59):actually, I have seen learning materials stating a relation with (another meaning of) proof irrelevance
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"
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
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
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?
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
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.
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.
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 :-(
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?
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.
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?
Paolo Giarrusso (May 30 2022 at 12:23):Print talks about "opaque proofs" IIRC :thinking:
Pierre-Marie Pédrot (May 30 2022 at 12:23):As a dev I'd call Qed constants "opaque" and Opaque constants something else
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
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")
Kenji Maillard (May 30 2022 at 12:26):When you say required, you mean for metatheoretical properties such as subject reduction/canonicity I guess ?
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
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.
Pierre-Marie Pédrot (May 30 2022 at 12:37):I agree, I was just reminding the dev jargon
Paolo Giarrusso (May 30 2022 at 12:40):thanks, that's all I could ask for from you :-)
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.
Pierre-Marie Pédrot (May 30 2022 at 15:49):Probably not the reason, but you could break soundness using fancy functors
Pierre-Marie Pédrot (May 30 2022 at 15:49):(module subtyping treats Qed proofs as axioms)
Pierre-Marie Pédrot (May 30 2022 at 15:51):that's a feature, we ought to treat Qed proofs as axioms essentially everywhere
Ali Caglayan (May 30 2022 at 16:30):Any good reason why we don't already?
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 ...
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)
Paolo Giarrusso (May 30 2022 at 17:19):and module subtyping allows to implement an opaque a := 1 via a := 2
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).
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.
oh thanks, I was wondering how to actually get the paradox
Notification Bot (May 31 2022 at 05:26):Kiran Gopinathan has marked this topic as resolved.
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: Oct 05 2023 at 02:01 UTC