## Stream: Coq users

### Topic: use Qed for Acc proofs?

#### Ali Caglayan (Nov 28 2021 at 14:03):

https://github.com/coq/coq/pull/15254

Let's continue the discussion here.

#### Paolo Giarrusso (Nov 28 2021 at 14:11):

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

#### Paolo Giarrusso (Nov 28 2021 at 14:12):

I think both `reflexivity` and `apply` ignore opacity; `compute` respects it, but `vm_compute` ignores it.

#### Ali Caglayan (Nov 28 2021 at 14:12):

But `Opaque` isn't meant to be a `Qed`.

#### Ali Caglayan (Nov 28 2021 at 14:12):

Sometimes people use Qed trickery inside proofs to stop unfolding

#### Ali Caglayan (Nov 28 2021 at 14:12):

Opaque allows this and to keep definitional equalities

#### Ali Caglayan (Nov 28 2021 at 14:13):

The performance however can be poor

#### Ali Caglayan (Nov 28 2021 at 14:13):

Qed isn't really any different to an axiom

#### Paolo Giarrusso (Nov 28 2021 at 14:13):

I’m not discussing performance, just information hiding.

#### Karl Palmskog (Nov 28 2021 at 14:13):

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

#### Paolo Giarrusso (Nov 28 2021 at 14:14):

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

#### Gaëtan Gilbert (Nov 28 2021 at 14:16):

`Proof` with a term is Qed though ;)

#### Ali Caglayan (Nov 28 2021 at 14:17):

I was not aware that was even possible!

#### Karl Palmskog (Nov 28 2021 at 14:18):

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?

#### Ali Caglayan (Nov 28 2021 at 14:19):

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

#### Paolo Giarrusso (Nov 28 2021 at 14:19):

indeed, the only downside is you can’t stick to the `Theorem` keyword (but there’s a CEP for that).

#### Gaëtan Gilbert (Nov 28 2021 at 14:19):

personnally I don't mind Defined with tactics

#### Paolo Giarrusso (Nov 28 2021 at 14:19):

Karl: at least, proof terms or safe tactics are necessary for `Defined` for information hiding. There might be performance questions.

#### Ali Caglayan (Nov 28 2021 at 14:20):

The performance issues don't really arise unless you are really unfolding the opaque terms.

#### Ali Caglayan (Nov 28 2021 at 14:21):

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.

#### Karl Palmskog (Nov 28 2021 at 14:21):

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.

#### Paolo Giarrusso (Nov 28 2021 at 14:22):

I was talking about `Defined`, not `Defined + Opaque`, Ali.

#### Ali Caglayan (Nov 28 2021 at 14:22):

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?

#### Paolo Giarrusso (Nov 28 2021 at 14:22):

HoTT is special since `Qed` isn’t reasonable there, and even then `Opaque` is probably not the perfect tool.

#### Paolo Giarrusso (Nov 28 2021 at 14:23):

@Ali Caglayan a formal semantics for `Opaque` :-)

#### Paolo Giarrusso (Nov 28 2021 at 14:24):

if I wanted to use features that work 50%, 70%, 90% of the time, I’d program PHP.

#### Ali Caglayan (Nov 28 2021 at 14:24):

Isn't it supposed to be an explicit flag for reductions that do delta, saying "please don't unfold me until you get stuck"?

#### Karl Palmskog (Nov 28 2021 at 14:24):

I'm just looking for some heuristics that work for most ordinary libraries / verification projects, HoTT is neither of those

#### Paolo Giarrusso (Nov 28 2021 at 14:25):

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

#### Karl Palmskog (Nov 28 2021 at 14:25):

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.

#### Paolo Giarrusso (Nov 28 2021 at 14:26):

just to clarify what I mean by “information hiding”:

#### Paolo Giarrusso (Nov 28 2021 at 14:27):

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.

#### Karl Palmskog (Nov 28 2021 at 14:28):

a.k.a abstraction barrier

#### Ali Caglayan (Nov 28 2021 at 14:28):

Right but Qed has two uses:

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

I think opaque is trying to do the first no?

#### Paolo Giarrusso (Nov 28 2021 at 14:29):

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.

#### Paolo Giarrusso (Nov 28 2021 at 14:30):

but I agree Opaque is _trying_ something like that, but it’s failing, and then my instinct is to reach for a flamethrower :-|.

#### Ali Caglayan (Nov 28 2021 at 14:31):

Do you have an example where `apply` unfold Qed?

#### Ali Caglayan (Nov 28 2021 at 14:31):

Also does this happen if the Qed is imported from a module or if it is in the same module?

#### Paolo Giarrusso (Nov 28 2021 at 14:31):

no it unfolds `Opaque`

#### Ali Caglayan (Nov 28 2021 at 14:32):

Yes that is intended

#### Ali Caglayan (Nov 28 2021 at 14:32):

Opaque just delays the priority of unfolding

#### Ali Caglayan (Nov 28 2021 at 14:32):

Which is great if you have some big fat proof terms that are useless during a proof

#### Ali Caglayan (Nov 28 2021 at 14:33):

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

#### Ali Caglayan (Nov 28 2021 at 14:35):

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.

#### Paolo Giarrusso (Nov 28 2021 at 14:35):

“delay priority” is what `Strategy` is for, AFAIK.

#### Paolo Giarrusso (Nov 28 2021 at 14:36):

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…

#### Karl Palmskog (Nov 28 2021 at 14:36):

across MathComp itself, fourcolor and odd-order there are fewer than 10 `Defined`

#### Ali Caglayan (Nov 28 2021 at 14:36):

The question is, are these Props or Types?

#### Karl Palmskog (Nov 28 2021 at 14:36):

to me, this is a strong signal that `Defined` is mostly for foundational research stuff, not for formalizing math or program verification

#### Ali Caglayan (Nov 28 2021 at 14:37):

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.

#### Ali Caglayan (Nov 28 2021 at 14:38):

<s>On the other hand, Acc really isn't a Prop</s>

#### Ali Caglayan (Nov 28 2021 at 14:39):

so the question of using Qed seems to be a trial-and-error thing.

#### Karl Palmskog (Nov 28 2021 at 14:39):

that seems like Coq metatheory to me. Acc is a Prop inside Coq.

#### Paolo Giarrusso (Nov 28 2021 at 14:39):

but it’s as much as `Prop` as `eq`, right? Both enjoy subsingleton elimination, which is why this question arises

#### Gaëtan Gilbert (Nov 28 2021 at 14:39):

Ali Caglayan said:

On the other hand, Acc really isn't a Prop

what

#### Ali Caglayan (Nov 28 2021 at 14:40):

Nevermind I misremembered

#### Ali Caglayan (Nov 28 2021 at 14:42):

I got confused with the Equations version. Anyhow, I don't know much about Acc. I just wanted to share some thoughts about Qed.

#### Paolo Giarrusso (Nov 28 2021 at 14:43):

(here’s `apply` vs `Opaque` https://github.com/coq/coq/issues/9135#issue-387409471)

#### Karl Palmskog (Nov 28 2021 at 14:43):

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.

#### Paolo Giarrusso (Nov 28 2021 at 14:43):

@Karl Palmskog but for a more radical question, do you have transparent well-founded definitions?

#### Gaëtan Gilbert (Nov 28 2021 at 14:43):

there's no general trick for eq though

#### Ali Caglayan (Nov 28 2021 at 14:44):

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

#### Karl Palmskog (Nov 28 2021 at 14:44):

so far I use `Defined` for well-founded definitions usually. But trying to figure out whether to change that.

#### Karl Palmskog (Nov 28 2021 at 14:45):

I think the `eq` opaque issue comes up less frequently than well-foundedness though?

#### Ali Caglayan (Nov 28 2021 at 14:46):

At least for eq there is a canonical proof

#### Ali Caglayan (Nov 28 2021 at 14:46):

Is there one for Acc? I don't think so...

#### Gaëtan Gilbert (Nov 28 2021 at 14:47):

Ali Caglayan said:

At least for eq there is a canonical proof

is there?

reflexivity no?

#### Gaëtan Gilbert (Nov 28 2021 at 14:47):

but you can't plug in refl when reducing some arbitrary thing

#### Paolo Giarrusso (Nov 28 2021 at 14:49):

I don’t see anybody proposing that?

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:50):

in that respect, SProp is much better behaved

#### Paolo Giarrusso (Nov 28 2021 at 14:50):

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

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:50):

also, there is a trick for opaque equality but it's not universal

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:51):

if you only eliminate decidable equalities you're safe

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:51):

(so essentially use SProp undercover)

#### Karl Palmskog (Nov 28 2021 at 14:51):

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

#### Ali Caglayan (Nov 28 2021 at 14:51):

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?

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:52):

let's say we had two vectors

IMO you've already lost by tthat point

#### Ali Caglayan (Nov 28 2021 at 14:53):

I'm not following?

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:53):

using dependent types is frowned upon by a good chunk of the Coq community

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:53):

instead, the mathcomp way seems to scale much more

#### Paolo Giarrusso (Nov 28 2021 at 14:54):

can we remember Ali’s work has different tradeoffs?

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:54):

(and it will probably be even better when SProp is properly handled by tactics unification and whatnot)

#### Ali Caglayan (Nov 28 2021 at 14:54):

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

#### Paolo Giarrusso (Nov 28 2021 at 14:55):

Ali: basically Coq-HoTT and Coq are disjoint ecosystems with somewhat disjoint heuristics.

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:56):

Indeed, HoTT (and even more unimath) are doing things that are very non-standard compared to your average Coq development

#### Ali Caglayan (Nov 28 2021 at 14:56):

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.

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:56):

but the mathcomp approach could also be used in the HoTT world, it's not incompatible

#### Karl Palmskog (Nov 28 2021 at 14:57):

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

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:57):

well, obviously you critically need dependent types to prove anything, but the point is that you should flee away from indexed types

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:57):

Back on track: the magical-refl stuff is essentially what SProp does

#### Paolo Giarrusso (Nov 28 2021 at 14:57):

(so my colorful comments against `Opaque` are not addressed at all at Coq-HoTT)

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:58):

but SProp (without the dreaded UIP flag) only lets you eliminate when the equality is decidable essentially

#### Kenji Maillard (Nov 28 2021 at 14:59):

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.

#### Paolo Giarrusso (Nov 28 2021 at 14:59):

@Pierre-Marie Pédrot could one use `SAcc` in `SProp`? I never learned the exact `SProp` restrictions…

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

I love SProp because it clearly exposes the issues with Prop, namely singleton elimination

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

@Paolo Giarrusso nope

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

and that's not a bug but a feature

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

there are three archetypal singleton in Prop: False, eq and Acc

#### Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

but in SProp only False is eliminable

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:00):

Acc breaks decidability of type-checking, and eq is sulphurous

#### Ali Caglayan (Nov 28 2021 at 15:00):

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?

#### Paolo Giarrusso (Nov 28 2021 at 15:00):

but then given an `seq` I can’t even `subst` it in `Type`

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:00):

@Ali Caglayan no, that you can eliminate a proof of Acc to produce something that lives in Type

#### Paolo Giarrusso (Nov 28 2021 at 15:01):

@Ali Caglayan because it has a single constructor, and that’s enough for subsingleton elimination

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:01):

@Paolo Giarrusso yes, you can precisely when the equality is decidable

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:01):

so SProp is a way to clearly delineate the stuff that is relevant

#### Karl Palmskog (Nov 28 2021 at 15:02):

so for regular Coq libraries, should one switch to `SProp` everywhere? Or how would `Prop` and `SProp` ideally coexist?

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:02):

Hard to tell, but there are people working on that.

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:02):

Prop does many things at the same time.

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:02):

For instance, for extraction you definitely want Acc to be erased

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:03):

Also the current support for SProp is terrible (and I can personally testify)

#### Paolo Giarrusso (Nov 28 2021 at 15:03):

is `SProp` not erasable?

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:03):

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.

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:04):

`SProp` is erasable indeed

#### Karl Palmskog (Nov 28 2021 at 15:04):

and `SProp` is not in MetaCoq yet, right? I was hoping to have erasure inside Coq.

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:04):

hm, it's at least partially there

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:05):

I don't know what you mean by "erasure inside Coq" but it's probably never going to satisfy you

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:05):

erasure is not -- and never will be -- type-preserving in CIC

#### Paolo Giarrusso (Nov 28 2021 at 15:05):

@Pierre-Marie Pédrot so don’t erase to CIC?

#### Karl Palmskog (Nov 28 2021 at 15:05):

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

#### Paolo Giarrusso (Nov 28 2021 at 15:06):

so we’re talking of `Eval untyped_vm_compute in foo` I guess?

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:06):

well then this is not correct in general, you may write partial program translations for that but it will never be total

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:06):

I know Lean does that, but it's utter nonsense

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:06):

you can get real garbage, typically when going under inconsistent contexts

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:07):

but if you want to do it externally you already have extraction

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:07):

I am not sure what use case you have in mind, actually

#### Paolo Giarrusso (Nov 28 2021 at 15:07):

thanks for reminding me I’m talking about _evaluation_ not normalization :-)

#### Paolo Giarrusso (Nov 28 2021 at 15:08):

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.

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:09):

what's this value for exactly?

#### Paolo Giarrusso (Nov 28 2021 at 15:09):

I mean evaluation, as for OCaml. I’d be happy if this used extraction maybe, as long as it’s seamless.

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:10):

I repeat: what do you need this value for?

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:10):

just printing on the toplevel?

Yes

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:10):

well, then probably you could hack something with the extraction or so

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:11):

but then the problem still holds that this value is essentially unrelated to the original term if you happened to erase anything there

#### Paolo Giarrusso (Nov 28 2021 at 15:11):

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

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:11):

OK, so this is UI problem, not a kernel one

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:12):

we could even peek into Qed proofs for this evaluator

#### Paolo Giarrusso (Nov 28 2021 at 15:12):

yep! I never talked about the kernel… and I wonder if this is _one_ of the things that Lean does

#### Paolo Giarrusso (Nov 28 2021 at 15:15):

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

#### Paolo Giarrusso (Nov 28 2021 at 15:15):

as long as the command has hardcoded support for comparing booleans, it’s good.

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:16):

what if the program uses an axiom?

#### Paolo Giarrusso (Nov 28 2021 at 15:16):

and peeking into Qed or such would be nice if I wanted to look through locked terms.

#### Paolo Giarrusso (Nov 28 2021 at 15:17):

well, the semantics I’d hope for are (untyped/weakly typed) extraction + execution: the axiom would extract as `throw “not_implemented”` or such?

#### Paolo Giarrusso (Nov 28 2021 at 15:18):

I hope this means that axioms/Qed on `Acc`/`eq` aren’t a problem

#### Paolo Giarrusso (Nov 28 2021 at 15:18):

well not always, but a sensible variant

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:19):

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?

#### Paolo Giarrusso (Nov 28 2021 at 15:19):

`Axiom nope : bool = nat` probably wouldn’t work, but an axiom/admitted proof in the size of a vector should probably be erased first?

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:20):

(assuming you only care about Prop erasure)

#### Pierre-Marie Pédrot (Nov 28 2021 at 15:21):

obviously this would be incompatible with any fancy axiom like univalence but well you can't have it both ways

#### Paolo Giarrusso (Nov 28 2021 at 15:21):

depends on “clever evaluation” and details are tricky, but “extraction to realizers” should be the right spec…

#### Paolo Giarrusso (Nov 28 2021 at 15:22):

I agree the answer is (likely) yes if you’re willing to do the Lean thing here

#### Paolo Giarrusso (Nov 28 2021 at 15:24):

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: Jun 18 2024 at 22:01 UTC