I'm writing a paper and I want to claim that rewriting with propositional equality is more performant (in terms of type-checking time) than rewriting with setoid equality. Is that even true, and if so what paper can I cite to support this claim?

Also, I would be happy to include any other arguments advocating for usage of prop. equality (whenever that possible).

there are very few performance analyses of ITP related techniques. Your best bet might be Jason Gross's PhD thesis, but I'm not sure he covers this particular case. From my recollection, his general conclusion is that all forms of rewriting are slow except possibly when implemented by reflection.

ping @Jason Gross to check if this is an accurate summary. Basically I think setoid-vs-other-rewrite differences are dwarfed by reflective-vs-non-reflective.

If by setoid you mean the stuff provided by the `setoid_rewrite`

tactic, then yes, it is in general way slower than propositional rewriting, although I don't have a paper to quote.

There are at least two distinct sources of slowness: 1. enlarged proof size and 2. typeclass proof search.

from my personal experience, 2. is by far the major responsible for this slowness

And that also covers the normal `rewrite`

and ssreflect's `rewrite`

tactics, when using setoid rewriting, no?

yes, but this is ambiguous (as you mention, it's context-dependent)

my point of comparison was with a theory which would have had a native setoid equality à la SetoidTT

@Pierre-Marie Pédrot You are missing 3. evar instance allocation, which often comes been 1 and 2 in performance. (In fact evar allocation is responsible for much slowness in non-ssr-rewrite, not just in setoid rewrite).

@Karl Palmskog your summary is accurate

@Evgeniy Moiseenko you want chapter 4 of my thesis, particularly figure 4-4(a)--(c). On the following 2.5 pages there's the bit titled "Performance Bottlenecks of Proof-Producing Rewriting", which includes my analysis. You may also be interested in the performance graphs of the readme of https://github.com/coq-community/coq-performance-tests

(anything including "rewrite")

For example,. rewrite_repeated_app_autorewrite_noop shows that even when there is no actually rewriting to be done, prior to Coq 8.15, only ssr rewrite achieves linear performance of rewrite in the size of the goal; everything else is at least quadratic due to evars. This is fixed in master / 8.15 ( @Pierre-Marie Pédrot was this deliberate, or a side-effect of some other performance improvement you (or someone else?) made?)

Some of the plots measure the time it takes to run `abstract rewrite`

as well as `rewrite`

, and the difference between these is a good estimate of how big of an impact the proof term size / complexity has.

so ssr rewrite doesn't do any evar instance allocation?

ssr rewrite does matching without evar allocation, I believe

And for terms with sufficiently many head-symbol matches without any actual matches, this was the bottleneck in non-ssr-rewrite

Following up on my previous list of examples: For example, rewrite_repeated_app_fast_rewrite_ltac2 shows that even with a custom proof term that is linear in size in the number of rewrites *plus* the size of the proof term (something that no other rewriting algorithm achieves, AFAIK), typechecking the proof term is still quadratic.

@Jason Gross I did a bit of tinkering around evar allocation and rewriting, the linearization is probably a consequence of that.

Also, @Pierre-Marie Pédrot , typeclass insurance search is only a severe bottleneck when the typeclass database is poorly tuned. Granted, it's so hard to get the right instances at the right priorities that I've only ever bothered to fully optimize the instances for performance testing, and in every real-world case I've seen where I haven't spent a couple hours performance-optimizing it for some benchmark, instance search is a significant bottleneck. (Do you have any stats on the extent to which typeclass insurance search is itself bottlenecked on evar instance allocation/manipulation?)

The stdlib setoid rewriting database is terrible. I've been looking a bit at it and it has funny exponential blowups

any non-trivial rewrite I've ever seen is just monstruous

Funny thing is that I was thinking about this precisely this weekend

(I should clarify that by "fully optimize" I mean "add every single insurance required to ensure that every tc resolution problem is solved in one step")

and I wonder why we don't have a canonical-structure-based setoid rewriting

Also @Pierre-Marie Pédrot we should probably close the corresponding issue claiming that autorewrite is super linear even when there are no instances to rewrite (unless you already closed it?)

(I mean, it's not that hard to implement but I wonder if there would be users.)

@Jason Gross please do it if you find it, I always have trouble skimming through the ocean of issues

I would probably be a user, since I've stayed away from setoid rewriting mainly due to the unpredictability of typeclass resolution

Note also that evar blowup is problematic only when you start to have big contexts, whereas poor tc resolution bites you immediately.

Is ssr rewrite not already based on canonical structure matching? Would CS rewrite have any benefit over ssr rewrite? (Would it allow extending ssr rewrite to run under binders?)

AFAIK ssr rewrite uses setoid rewriting under the hood? The only difference is the pattern algorithm which is reputed to be better.

Or maybe just the non-setoid one from Equality.

A big problem in TC search should be fixed by Matthieu’s MR to change Reflexive’s mode.

But yeah, the ssr rewrite is mostly about picking patterns, not so much about anything else (and in any case setoid or CS is orthogonal to that)

@Paolo Giarrusso this is true, but logic programming is always there to try to hit you in the head when you're not aware

CS-based rewriting is the best of both worlds

Logic programming does not require backtracking, ask @Robbert Krebbers.

Well, then it's not quite LP anymore...

Syntax-directed proof search is still proof search?

I've also heard Robbert claim that one reason (the reason?) Iris uses typeclasses is because it definitely needs setoids. (Lots of setoids).

When the search is deterministic I don't think you can call that a search. It's called pattern-matching.

(the autorewrite issue has been closed: https://github.com/coq/coq/issues/12600)

(it looks like #14253 closed it in June)

Open-world pattern matching? Maybe. Regardless of how we call it, Iris Proof Mode uses typeclasses but mostly (or fully?) without backtracking (again, ask Robbert for the details).

OK, so it'd be a good candidate for CS setoid rewriting.

having a project with both an extensive CS packaged class hierarchy and *then also* going full-on typeclasses and TC setoid rewriting... I tip my hat to that, but very few projects can set it up.

To clarify, the IPM interface doesn't use rewrite, but the implementation (and the ecosystem) does.

(@Jason Gross incidentally, as discussed in the issue, the source of slowness is not evar allocation but [something related to] pattern selection)

I'd be interested in CS-based rewriting. In particular if it can handle https://github.com/coq-community/coq-performance-tests/blob/master/src/fiat_crypto_via_setoid_rewrite_standalone.v better than the currently-required dozen or so calls to rewite_strat, that would be a very significant improvement in the feasibility of using rewrite at scale

Oh, it's not evar allocation for pattern selection? I guess I misremembered.

It's not hard to misremember, given that we have that many quadractic-cubic-quartic algorithms spread around. When it's not the famous one that kills you, you're maimed by another one.

@Jason Gross thank you for pointing out a reference, this is exactly what I was looking for.

Also many thanks to others for this discussion.

@Evgeniy Moiseenko glad to help (and thanks @Karl Palmskog for tagging me, I would have missed this otherwise)

@Pierre-Marie Pédrot is there any hope of eliminating all of these algorithms? (I have a stalled paper in the works that lays out the proof engine primitives that need to have good enough performance (I guess I need to add "constant time is_ground"), and calls for a proof engine that achieves all of these)

don't hold your breath, but there is still a bit of hope though

Should we all just switch to Jason's technique? I've heard that might be difficult unless your rewrite rules are just right, but I haven't looked any close...

The reason I haven't released a non-dev version of the rewriter I built is that (a) it's way too restrictive for everyday use (it basically doesn't support dependent types at all, and even container types like list and option have to be hard-coded by hand), and (b) the proofs are kind of unmaintainable. I think there are a couple insights to be had:

1 (already known). Reflective rewriting is necessary for efficiency. (I do have an (unpunished, mostly just on paper) variant of the rewrite_strat algorithm that, by careful accounting, ought to generate proof terms linear the sum of the number of rewrites and the size of the term, even in the presence of binders, but I have yet to find any way to get Coq to typecheck such a term in linear time (due to quadratic substitutions when typechecking nested let's/lambdas).). Hence it would be quite useful to have some out-of-the-box-usable axiom-free reflective rewriting package. I'd bet that something like MetaCoq would be a good starting point for what to base this on.

- The best rewrite order when binders is involved is the reduction order of NbE. rewrite_strat should support this order, and any new reflective rewriter should have this support as well
- By paying an upfront cost at hint-database-creation time, reflective rewriters can be specialized to the task at hand, and this can net performance benefits (around 8x in my examples, IIRC)
- Issues of denotation-function-completeness (e.g., not having support for particular inductive types or for a limited number of universes) can be solved by having the tactic automatically emit some definitions (ideally some inductive types as well) and some light-weight proofs, and parameterizing the overall denotation function and its proofs over such parameters

one aspect I've wondered about: even though the HOL family has only very limited reflection (in Isabelle), they seem to do quite well performance-wise with the rewriting they have. So it seems like a harsh tradeoff to skip dependent types to get good rewriting performance in Coq.

@Karl Palmskog I think dependent types are a red herring. As I understand it, when they use rewriting on terms with sufficiently many binders, they run into the same asymptotic performance issues that are present in Coq. Furthermore, most of the bottlenecks in Coq's rewriting engine have very little to do with dependent types (see the aforementioned typeclass search, closedness-checking, and evar instance allocation bottlenecks). And dependent types are hard to manage in reflection, AIIUI, sort-of only because the expressive power of your metatheory needs to be strictly greater than the expressive power of your object theory, if you want to handle everything.

@Karl Palmskog term size for HOL is 0, that's a major speedup they get from not having universes :smiling_imp:

or fixpoints, ahem

(Isabelle _could_ produce proof terms, but Coq _can't_ skip them AFAIK, simply because Coq typechecking is not compositional, due at least to universes and guardedness checking)

yes, proof terms are seldom recorded in HOL workflows, but they are there if you want them

my point is that it's a significant performance boost, which Coq only has when using definitional equality

No, I don't think this is such a big performance boost. There are *some* developments where the bottleneck is Qed-time (but even then, the most common bottleneck is either universe checking or conversion being slow because `simpl`

doesn't insert enough information in the proof term, and neither of these is really about leaving behind proof terms). But most of the time, there's not much performance difference between running `abstract <your tactic>`

vs running your tactic + running `abstract admit`

(which counts the time it takes to typecheck the type of the goal). This suggests that typechecking the proof term doesn't take much.

Moreover, the bottleneck that forces naive rewrite to be super-linear in the number of binders arises as soon as there's a proof witness that can name its type / what it's a witness of, regardless of whether or not an entire proof term is kept. AFAIK, HOL does in fact keep around abstract proof witnesses that can name their type.

I thought only guardedness/productivity checking was non-compositional? Typechecking of universes is compositional in the monad of universe constraints.

Jason Gross said:

I thought only guardedness/productivity checking was non-compositional? Typechecking of universes is compositional in the monad of universe constraints.

what does that mean?

I guess that's the writer monad over the monoid of constraints under merge?

and I see your point: Universes violate separate typechecking enough to prevent full checking `vos/vok`

, but it _could_ still be compositional, if the constraints are just an output — separate compilation is just stricter.

Last updated: May 24 2024 at 22:02 UTC