The Coq mailing list

[gallais <guillaume.allais AT strath.ac.uk>]

Hi,

Here is a naïve solution:

https://sympa.inria.fr/sympa/arc/coq-club/2012-11/msg00187.html

As you can see in the following emails in the same thread, it is
clearly more interesting to implement the tactic in Ocaml (+ you'll
be able to use clever implementations of sets rather than plain old
lists).

Cheers,

On 22/08/13 22:54, t x 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!