https://github.com/coq/coq/pull/15254
Let's continue the discussion here.
re Opaque
doesn’t work: Opaque foo
is not equivalent to Qed
ing foo’s body (and it can’t be: removing the definitional equality could make existing terms ill-typed), and it doesn’t prevent all tactics from seeing through foo
’s definition (and it could, except for backward compatibility).
I think both reflexivity
and apply
ignore opacity; compute
respects it, but vm_compute
ignores it.
But Opaque
isn't meant to be a Qed
.
Sometimes people use Qed trickery inside proofs to stop unfolding
Opaque allows this and to keep definitional equalities
The performance however can be poor
Qed isn't really any different to an axiom
I’m not discussing performance, just information hiding.
I'm not sure I fully understand Pierre-Marie's position though. Is it OK to be transparent everywhere for well_founded
as long as you're not using tactics? For example, if I wrote all my proofs like this I could/should be transparent?
Theorem op_inv_r_ex
: forall x : E, exists y : E, op_is_inv_r x y.
Proof
fun x
=> ex_ind
(fun (y : E) (H : op_is_inv_l x y)
=> ex_intro
(op_is_inv_r x)
y
(H || a = 0 @a by op_is_comm x y))
(op_inv_l_ex x).
(https://github.com/llee454/functional-algebra/blob/master/abelian_group.v#L191-L201)
@Ali Caglayan I agree Opaque
isn’t Qed
, but I challenge you to give a specification that is (a) reasonable (b) correct for the current implementation.
Proof
with a term is Qed though ;)
I was not aware that was even possible!
OK, but let's say then:
Theorem op_inv_r_ex
: forall x : E, exists y : E, op_is_inv_r x y.
Proof.
refine (fun x
=> ex_ind
(fun (y : E) (H : op_is_inv_l x y)
=> ex_intro
(op_is_inv_r x)
y
(H || a = 0 @a by op_is_comm x y))
(op_inv_l_ex x)).
Defined.
Is this what we should be doing?
You can also just make that a definition and inline it completely. The line between definition and theorem isn't so clear. Just an arbitrary syntactic restriction IMO
indeed, the only downside is you can’t stick to the Theorem
keyword (but there’s a CEP for that).
personnally I don't mind Defined with tactics
Karl: at least, proof terms or safe tactics are necessary for Defined
for information hiding. There might be performance questions.
The performance issues don't really arise unless you are really unfolding the opaque terms.
For example, in the HoTT library almost all our definitions/theorems etc. are Defined. There are a few places where we explicitly mark things as opaque to discourage coq from uselessly unfolding large proof terms.
I think the main reason to even introduce Qed
opaqueness was to lower memory use, i.e., don't keep proof terms in memory etc.
I was talking about Defined
, not Defined + Opaque
, Ali.
Paolo Giarrusso said:
Ali Caglayan I agree
Opaque
isn’tQed
, but I challenge you to give a specification that is (a) reasonable (b) correct for the current implementation.
@Paolo Giarrusso Sorry I have misunderstood. What are you asking here?
HoTT is special since Qed
isn’t reasonable there, and even then Opaque
is probably not the perfect tool.
@Ali Caglayan a formal semantics for Opaque
:-)
if I wanted to use features that work 50%, 70%, 90% of the time, I’d program PHP.
Isn't it supposed to be an explicit flag for reductions that do delta, saying "please don't unfold me until you get stuck"?
I'm just looking for some heuristics that work for most ordinary libraries / verification projects, HoTT is neither of those
“until you get stuck”? that sounds like simpl never
— which is misnamed since simpl never
definitions will be unfolded by simpl
if forced by a surrounding match.
for example, if you don't use Qed you can't get the benefits of vio/vos/vok. And your memory use will be through the roof for long files, ruling out using x32 (32-bit pointer) Coq which is much faster in CI than regular 64-bit Coq.
just to clarify what I mean by “information hiding”:
changes to Qed proofs are safe _because nobody else can depend on the details_. That’s information hiding, and that’s useful when maintaining large projects.
a.k.a abstraction barrier
Right but Qed has two uses:
I think opaque is trying to do the first no?
right, but then why can apply bar
unfold foo
if needed for typechecking? Answer: this is a bug, but it’s hard to fix for backward compatibility.
but I agree Opaque is _trying_ something like that, but it’s failing, and then my instinct is to reach for a flamethrower :-|.
Do you have an example where apply
unfold Qed?
Also does this happen if the Qed is imported from a module or if it is in the same module?
no it unfolds Opaque
Yes that is intended
Opaque just delays the priority of unfolding
Which is great if you have some big fat proof terms that are useless during a proof
But there are still real situations where this fat proof term needs to be compared later, which is where Qed doesn't fit the bill
However coming back to the original topic, I don't have too much experience with Acc but since people have been coming up with tricks to hide large proof terms (for performance reasons). I suspect that using Qed for those parts is fine.
“delay priority” is what Strategy
is for, AFAIK.
I wasn’t aware that eauto
ignored Opaque
https://github.com/coq/coq/issues/11502, I’m less surprised by inversion
https://github.com/coq/coq/issues/10920…
across MathComp itself, fourcolor and odd-order there are fewer than 10 Defined
The question is, are these Props or Types?
to me, this is a strong signal that Defined
is mostly for foundational research stuff, not for formalizing math or program verification
Since Prop is intended to be proof-irrelevant there is no harm in making every Prop Qed, until you start comparing proofs which is why UIP appears. This can be avoided (I think) with SProp.
<s>On the other hand, Acc really isn't a Prop</s>
so the question of using Qed seems to be a trial-and-error thing.
that seems like Coq metatheory to me. Acc is a Prop inside Coq.
but it’s as much as Prop
as eq
, right? Both enjoy subsingleton elimination, which is why this question arises
Ali Caglayan said:
On the other hand, Acc really isn't a Prop
what
Nevermind I misremembered
I got confused with the Equations version. Anyhow, I don't know much about Acc. I just wanted to share some thoughts about Qed.
(here’s apply
vs Opaque
https://github.com/coq/coq/issues/9135#issue-387409471)
unfortunately it's all connected. I try to use Qed whenever I can but well_founded and Qed prevents some simple reductions. But if Coq devs are blessing the well_founded reduction trick (2^32 unfoldings OK), then I think we can go (nearly) full Qed.
@Karl Palmskog but for a more radical question, do you have transparent well-founded definitions?
there's no general trick for eq though
Paolo Giarrusso said:
(here’s
apply
vsOpaque
https://github.com/coq/coq/issues/9135#issue-387409471)
Oh I remember reading that. It's weird that it's only for compatibility for CoRN
so far I use Defined
for well-founded definitions usually. But trying to figure out whether to change that.
I think the eq
opaque issue comes up less frequently than well-foundedness though?
At least for eq there is a canonical proof
Is there one for Acc? I don't think so...
Ali Caglayan said:
At least for eq there is a canonical proof
is there?
reflexivity no?
but you can't plug in refl when reducing some arbitrary thing
I don’t see anybody proposing that?
in that respect, SProp is much better behaved
For Acc
, there’s the “unfolding trick” we’ve referenced without explaining, which works for concrete computations; I agree eq
won’t block computation unless you really use indexed types, and even there you can often use a proof of K (for types with decidable equality).
also, there is a trick for opaque equality but it's not universal
if you only eliminate decidable equalities you're safe
(so essentially use SProp undercover)
some may recall this on the general problem of evaluation/opaqueness in program verification: http://gallium.inria.fr/blog/coq-eval/ ("Using Coq's evaluation mechanisms in anger")
So let's say we had two vectors Vector.t (n + m)
and Vector.t (m + n)
. We show that there is a conversion function, but we use a Qed commutativity proof. If we plug in a closed term, it won't compute since there is a Qed. But if your reduction could turn the Qed proof into refl would there be any problem?
let's say we had two vectors
IMO you've already lost by tthat point
I'm not following?
using dependent types is frowned upon by a good chunk of the Coq community
instead, the mathcomp way seems to scale much more
can we remember Ali’s work has different tradeoffs?
(and it will probably be even better when SProp is properly handled by tactics unification and whatnot)
Pierre-Marie Pédrot said:
using dependent types is frowned upon by a good chunk of the Coq community
Honestly I am surprised anyone would claim this
Ali: basically Coq-HoTT and Coq are disjoint ecosystems with somewhat disjoint heuristics.
Indeed, HoTT (and even more unimath) are doing things that are very non-standard compared to your average Coq development
Right, I do work a lot in HoTT where these things are important. But I do not agree that dependent types are useless in plain Coq.
but the mathcomp approach could also be used in the HoTT world, it's not incompatible
MathComp does not use much dependent/indexed types, and if I recall correctly Adam Chlipala wrote his nearly dependent/indexed types free book (http://adam.chlipala.net/frap/) partly in response to seeing student disasters with dependent types
well, obviously you critically need dependent types to prove anything, but the point is that you should flee away from indexed types
Back on track: the magical-refl stuff is essentially what SProp does
(so my colorful comments against Opaque
are not addressed at all at Coq-HoTT)
but SProp (without the dreaded UIP flag) only lets you eliminate when the equality is decidable essentially
Ali Caglayan said:
So let's say we had two vectors
Vector.t (n + m)
andVector.t (m + n)
. We show that there is a conversion function, but we use a Qed commutativity proof. If we plug in a closed term, it won't compute since there is a Qed. But if your reduction could turn the Qed proof into refl would there be any problem?
You could achieve something along these lines using equality witnesses in SProp: once n,m
are instantiated by concrete natural numbers your "non-reducing" equality proofs will become convertible.
@Pierre-Marie Pédrot could one use SAcc
in SProp
? I never learned the exact SProp
restrictions…
I love SProp because it clearly exposes the issues with Prop, namely singleton elimination
@Paolo Giarrusso nope
and that's not a bug but a feature
there are three archetypal singleton in Prop: False, eq and Acc
but in SProp only False is eliminable
Acc breaks decidability of type-checking, and eq is sulphurous
Pierre-Marie Pédrot said:
there are three archetypal singleton in Prop: False, eq and Acc
Are you saying there is a canonical proof of Acc?
but then given an seq
I can’t even subst
it in Type
@Ali Caglayan no, that you can eliminate a proof of Acc to produce something that lives in Type
@Ali Caglayan because it has a single constructor, and that’s enough for subsingleton elimination
@Paolo Giarrusso yes, you can precisely when the equality is decidable
so SProp is a way to clearly delineate the stuff that is relevant
so for regular Coq libraries, should one switch to SProp
everywhere? Or how would Prop
and SProp
ideally coexist?
Hard to tell, but there are people working on that.
Prop does many things at the same time.
For instance, for extraction you definitely want Acc to be erased
Also the current support for SProp is terrible (and I can personally testify)
is SProp
not erasable?
remember the good old 8.5 days when you would get random universe errors at Qed because of broken univpoly tactics? Basically that's where we're at with SProp.
SProp
is erasable indeed
and SProp
is not in MetaCoq yet, right? I was hoping to have erasure inside Coq.
hm, it's at least partially there
I don't know what you mean by "erasure inside Coq" but it's probably never going to satisfy you
erasure is not -- and never will be -- type-preserving in CIC
@Pierre-Marie Pédrot so don’t erase to CIC?
I meant something very operational, defining a sigma type and then just getting a function that has the computational part and a separate lemma that the function output has the property
so we’re talking of Eval untyped_vm_compute in foo
I guess?
well then this is not correct in general, you may write partial program translations for that but it will never be total
I know Lean does that, but it's utter nonsense
you can get real garbage, typically when going under inconsistent contexts
but if you want to do it externally you already have extraction
I am not sure what use case you have in mind, actually
thanks for reminding me I’m talking about _evaluation_ not normalization :-)
so, imagine foo
is a closed term of “ground” type — say nat
, but even a Coq/mathcomp Vector — and I want to get the concrete value.
you mean head normalization? That's already problematic enough
what's this value for exactly?
I mean evaluation, as for OCaml. I’d be happy if this used extraction maybe, as long as it’s seamless.
I repeat: what do you need this value for?
just printing on the toplevel?
Yes
well, then probably you could hack something with the extraction or so
but then the problem still holds that this value is essentially unrelated to the original term if you happened to erase anything there
to be clear, the example use-case is that I wrote a program in Coq and I want to test it on a concrete input to look at the result :-)
OK, so this is UI problem, not a kernel one
we could even peek into Qed proofs for this evaluator
yep! I never talked about the kernel… and I wonder if this is _one_ of the things that Lean does
the only _other_ thing I can imagine (again, purely UX-level) is asserting the result coincides with some other value… Eval untyped_vm_compute (or whatever) in (foo =? expected) =? true.
as long as the command has hardcoded support for comparing booleans, it’s good.
what if the program uses an axiom?
and peeking into Qed or such would be nice if I wanted to look through locked terms.
well, the semantics I’d hope for are (untyped/weakly typed) extraction + execution: the axiom would extract as throw “not_implemented”
or such?
I hope this means that axioms/Qed on Acc
/eq
aren’t a problem
well not always, but a sensible variant
hm, but then if you just had unfolding of Qed + clever evaluation of singleton eliminations, you'd also get what you want, am I wrong?
Axiom nope : bool = nat
probably wouldn’t work, but an axiom/admitted proof in the size of a vector should probably be erased first?
(assuming you only care about Prop erasure)
obviously this would be incompatible with any fancy axiom like univalence but well you can't have it both ways
depends on “clever evaluation” and details are tricky, but “extraction to realizers” should be the right spec…
I agree the answer is (likely) yes if you’re willing to do the Lean thing here
IMHO, if people want to replace n: a = b
by refl
automatically, they’re probably talking of CBV evaluation of realizers, even if they might not know any of those words.
Last updated: Oct 13 2024 at 01:02 UTC