The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

I don't know about "everything possible" but I will say that this is a basic idea in Chlipala's crush tactic, if you haven't already taken a look at its internals.

Kris

On Thu, Aug 22, 2013 at 5:54 PM, t x <txrev319 AT gmail.com> wrote:

Hi,

  I'm trying to design a tactic that inverts everything possible to invert.

  Here is my minimal failure case:

https://gist.github.com/anonymous/6313270

  My current code infinite loops. Two "obvious solutions seems to be"

(1) if there is a way to separate "Consrtructor" from "Function", then, the infinite loop is easy to fix.

(2) If there is a way detect "is result of 'inversion' same as Hypothesis?' --> and force a fail

Can anyone tell me how to do either (1) or (2)?

Thanks!