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’t`Qed`

, 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:

- stopping definitions from being unfolded (because they simply can't)
- using proofs like an axiom

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`

vs`Opaque`

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

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?

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: Jan 29 2023 at 06:02 UTC