<div dir="ltr"><div dir="ltr">On Fri, Apr 26, 2024 at 4:05 AM Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:</div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I've recently optimised<br>
code with similar characteristics. Perhaps you can do something similar:<br>
<br>
* Prove suitable inversion lemmas for one of the two types.<br>
<br>
* Instead of matching on both arguments, match on one, and use inversion<br>
  lemmas for the other argument.<br>
<br></blockquote><div><br></div><div>Wow! That made a huge difference, thank you! That technique took me from 7.5 minutes down to 12 seconds (plus another 2 seconds to check the file with all the inversion lemmas)! That's more than a 35x speed up. Amazing! </div></div><div class="gmail_quote"><br></div><div class="gmail_quote">Also it turns out, I didn't have 2 connected arguments, it was actually 3. (One is an evaluation context and the other two are proofs of decompositions, so the case split on the two decompositions was replaced by the inversion lemmas.)  And now that I get the idea, I'm seeing opportunities for this in more places, in this codebase too (not that anything was that slow)!<br></div><div class="gmail_quote"><br></div><div class="gmail_quote">Thanks again!<br></div><div class="gmail_quote"> <div><br></div><div>Robby</div><div><br></div></div></div>