The Coq mailing list

[Vincent Aravantinos <vincent.aravantinos AT yahoo.fr>]

Hi,

Le 17 nov. 07 à 09:37, Christine Paulin a écrit :

> Hi,
>
> This kind of problem is usually solved by finding the right  
> generalization of your goal.
>
> In your case, probably somethink like
>    forall x, P x -> x=C1 ->  ....
> (be sure that what you want to prove is true by induction)
> then use an induction on P.
> then use discriminate in order to get rid of the useless cases  
> (this is what inversion does except it uses pattern-matching, not  
> induction.

this is exactly what I needed, thank you very much !
Furthermore, it improves my understanding of inversion.

Thanks again.

Le 17 nov. 07 à 10:05, Lionel Elie Mamane a écrit :
> On Sat, Nov 17, 2007 at 03:16:22AM +0100, Vincent Aravantinos wrote:
> > My goal has the form:
> >
> > ... P C1 ...
>
> I don't understand what the "..." in the goal are supposed to be
> filled with.

Just that the goal involves P C1, but this is actually a useless  
piece of information, sorry.

> Please post to the mailing list a complete proof script
> that leads to a place where your problem shows. Then, people can paste
> it into their Coq and see what you mean much easier.

Yeah... I was hoping the informal explanation would be sufficient; I  
must admit I've been a bit lazy on this, apologies.


--
Vincent