Rewriting is slow

[Lysxia]

Instance search keeps reproving the same goals, which take time because of the way we currently compose structures, so we have to repeatedly reconstruct them.

Solution: specialize structures more, e.g., don't declare ktree notation for Kleisli itree, but make it a definition of its own. Derive the various instances with some copy-paste boilerplate.

A more long-term solution would be to implement caching in type class search. Our constraints are Haskell-like, so they're not too wild (we shouldn't have to worry about existential variables). Universe polymorphism might become a problem though. In any case, it's a lot of work.

---

The proof of Imp2AsmCorrectness.seq_asm_correct provides a small (enough for debugging) but still noticeably slow rewrite (0.2s) (there are probably many others earlier...).

In particular, looking at rewrite app_asm_correct line 455.

InteractionTrees/tutorial/Imp2AsmCorrectness.v

Line 455 in f140f0b

rewrite loop_asm_correct, relabel_asm_correct, app_asm_correct.

The goal looks like this:

loop (subpure swap >>> denote_asm (app_asm ab bc) >>> subpure (id_ (B + C)))
  ⩯ denote_asm ab >>> denote_asm bc

And we're rewriting using

app_asm_correct : denote_asm (app_asm ab cd) ⩯ bimap (denote_asm ab) (denote_asm cd)

That spawns the ridiculous tree search summarized below, but basically, the same goals keep on reappearing.

---

1. Proper-ness of the context subpure swap >>> _, which is solved by properness of cat (>>>)...

   1. This also requires reflexivity of equivalence of arrows eq2 (to ensure here that subpure swap is "proper")

      1. eq2 is an Equivalence (...)

   2. Properness of cat solved by category_proper_cat, requiring

      1. sub (ktree E) is a Category, requiring

         1. ktree E is a Category, requiring

            1. itree E is a lawful monad (MonadLaws, EqMProps)

2. Proper-ness of the context _ >>> subpure (id_ (B + C))), which basically spawns the same search (...)

3. Proper-ness of loop, requiring

   1. eq2 is an Equivalence (...)

   2. sub (ktree E) is a Category (...)

   3. sub (ktree E) is an Iterative category, which in turn requires

      1. eq2 is an Equivalence (fourth time!) (...)

      2. ktree E is a Category (fourth time!) (...)

      3. ktree E has a Coproduct, requiring again that itree E is a monad, for at least the fifth time (others hidden in Category constraints)

(Related to #83)