Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] repeat inversion ; without infinite looping

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] repeat inversion ; without infinite looping


Chronological Thread 
  • From: gallais <guillaume.allais AT strath.ac.uk>
  • To: t x <txrev319 AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] repeat inversion ; without infinite looping
  • Date: Mon, 26 Aug 2013 11:53:58 +0100

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!




Archive powered by MHonArc 2.6.18.

Top of Page