The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi Jason,

  1) I've actually seen this in either cpdt or ltamer; but I don't understand. Can you explain why this actually works?

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

  I understand lines 2 & 3, but I don't see how 1 or 4 works.

  2) I need fail 2 because I have (try (try ... )) so I need "fail 2" to break out of both try's and fail the match.

On Sat, Aug 24, 2013 at 11:53 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Rather than "pose proof (H1 = H2)", you can do one of the following:
[let dummy_check := constr:(H1 = H2) in idtac]
[let T1 := type of H1 in
let T2 := type of H2 in
unify T1 T2]

Also, I think you might want fail 1 (or perhaps even fail 0) rather than fail 2, but I haven't looked too carefully.

-Jason

On Aug 22, 2013 7:06 PM, "t x" <txrev319 AT gmail.com> wrote:

I think I have solved this :

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

via a complete abuse of tactics.

"bad thing" = after inversion,

  * only one term is generated

  * the term that generated is the same as the old term

==> therefore, pose proof (H1 = H2) should type check

whereas, if the newly generated term is different from the old term, then pose proof (H1 = H2) should not type check since H1 and H2 are different terms.

However, if anyone has a cleaner solution, I'd appreciate it too. :-)

On Thu, Aug 22, 2013 at 9: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!