search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
745 stars 68 forks source link

Improve the performance of normalize by simplifing the lemma. #8

Closed gmalecha closed 6 years ago

gmalecha commented 6 years ago

This improves the performance of the normalize tactic by 22x on the example from ~2.9s to ~0.13s. The key is to make Coq do as little work as possible during unification, so you need to make sure that the form of the lemma syntactically matches the form of the goal.

This works out pretty well for what you're doing, but this doesn't follow the standard recipe for computational reflection. For this problem, it doesn't bite you, but if you were working in a concrete category, the vm_compute at the end of this tactic would unfold all of the definitions in your category making a term that is very inefficient. The general way to solve this problem is to use an equation to control reduction, though this does make things a little bit less efficient in some instances.

Lemma apply_simplify : forall e a b,
  simplify e a = b ->
  denote b ->
  denote a.

To apply this lemma, you vm_compute the simplify, and then use eq_refl. Then you just simpl (or cbv with controlled simplification) on the denote premise so that you don't unfold any definitions that occur in your environment.

jwiegley commented 6 years ago

Thanks, Greg!

jwiegley commented 6 years ago

I just tried this tactic on a real example (where rewrite !comp_assoc takes 5.4s), I ran into exactly what you said about vm_compute going too far.

jwiegley commented 6 years ago

What's the best approach to quickly computing away the scaffolding around the reified terms, but leaving those terms alone? Is there any kind of wrapper I can put around them that will block vm_compute?

gmalecha commented 6 years ago

Unfortunately there is not a wrapper, it would be really great if there was one though. It might be worth trying to implement it for performance purposes, but in general it would require modifying Coq's kernel (the implementation of vm_compute).

The easiest way is what I suggested above. It is the recipe that I wrote in section 4.3.1 of my dissertation. You will vm_compute to reduce the equality, the result of which should be purely syntax. Then you can cbv the hypothesis with a whitelist of symbols for your denotation function. This still isn't ideal though because you want to make sure that no term that you want to reduce in your denotation function is used in your environment. When you work with lists, the usual culprit is nth_error and plus, but you probably won't run into this problem, at least for now.