The Coq mailing list

[t x <txrev319 AT gmail.com>]

1) You want "inversion H0" ; in particular, you want to tell Coq "generate for me all possible ways the proof for H0 could have been constructed."

2) One useful heuristic is to load up http://adam.chlipala.net/itp/tactic-reference.html and try random (tactic _variable_name_) combinations until something moves. This works well until issues of dependent types / abstracting Foo over Bar induces XYZ which is ill-typed.

On Sun, Sep 8, 2013 at 12:22 AM, Shigeo Nishi <shigeonishi AT hotmail.com> wrote:

I'm reading some chapters from Pierce's and started reading CPDT book. I'm currently interested in using Coq for program verification, so I came up with this question.

Thanks a lot.

---

Date: Sat, 7 Sep 2013 20:06:54 -0400
From: adamc AT csail.mit.edu
To: shigeonishi AT hotmail.com
CC: coq-club AT inria.fr

Subject: Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however .....

On 09/07/2013 08:01 PM, Shigeo Nishi wrote:

I'm a Coq beginner, but I think I have a question that has to do with this thread since I'm trying to prove that an inductive proposition with the wrong "evidence" is evaluated to False.

[...]

I'm stuck in this goal:

1 subgoals
H0 : isof2 (1 :: nil)
______________________________________(1/1)
False

What source are you using to learn Coq?  I expect most will introduce the tools you need here, probably as part of an introduction to inductive predicates.