Try a homomorphic destruct before a standard destruct

[isovector]

This is the first of three PRs cleaning up how Wingman approaches its proof search. It now attempts to synthesize homomorphic case splits if possible, and will only fall back to a regular split if the homomorphic one didn't lead to any solutions. This aggressively prunes the search tree in most cases, and means we have more auto gas to spend on harder proofs. As a result, we can now synthesize a solution to zip, which was previously too expensive to find.

[santiweight]

I'll just take the opportunity here since it seems convenient! I don't know what a homomorphic split is. I know what a homomorphism is I believe (mapping functors and maintaining structure?) but I can't see what a homomorphic split would be - as a result I refrain from/am scared of using it since I don't understand it!

I'll add out that I'm a pretty advanced Haskell user wrt to types and am familiar with some Category Theory: in other words the situation would likely (unless my experience is entirely unique) be far worse for a beginner.

My thought is that the name should be unintimidating and reflect the consequence of the action :)

[santiweight]

Loving Wingman btw :)

[isovector]

@santiweight fair enough! A homomorphic split here is a transformation that pattern matches on a data type and produces the same data constructors in the holes. Eg, something of the form:

case x of
  Left e -> Left _
  Right a -> Right _

[santiweight]

@isovector That's probably what I would have guessed. I wonder whether you can name based on the functor's type: in that case:

x :: Either e a

asking for commands at x would have a "Wingman: map from Either to Either". It says the same thing, but it's explicit (not sure when the command name is requested.

[isovector]

@santiweight that's a good idea. If you don't mind filing an issue, I'd be happy to implement it.