coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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!
- [Coq-Club] repeat inversion ; without infinite looping, t x, 08/22/2013
- [Coq-Club] Re: repeat inversion ; without infinite looping, t x, 08/23/2013
- Re: [Coq-Club] Re: repeat inversion ; without infinite looping, Jason Gross, 08/25/2013
- Re: [Coq-Club] Re: repeat inversion ; without infinite looping, t x, 08/25/2013
- Re: [Coq-Club] repeat inversion ; without infinite looping, Jason Gross, 08/25/2013
- Re: [Coq-Club] Re: repeat inversion ; without infinite looping, t x, 08/25/2013
- Re: [Coq-Club] Re: repeat inversion ; without infinite looping, Jason Gross, 08/25/2013
- Re: [Coq-Club] repeat inversion ; without infinite looping, Kristopher Micinski, 08/23/2013
- Re: [Coq-Club] repeat inversion ; without infinite looping, t x, 08/24/2013
- Re: [Coq-Club] repeat inversion ; without infinite looping, gallais, 08/26/2013
- [Coq-Club] Re: repeat inversion ; without infinite looping, t x, 08/23/2013
Archive powered by MHonArc 2.6.18.