The Coq mailing list

[Tie Cheng <chengtie AT gmail.com>]

Effectively "destruct a; try discriminate e." works. Thank you all.

Tie

2011/2/17 Stéphane Lescuyer <stephane.lescuyer AT inria.fr>

The comparison on Z is computational, and the equality test in your
hypothesis e will fail as soon as a starts with a constructor other
than Z0.
So you can simply destruct a, remove two of the three resulting cases
by contradiction and the only one that remains has a replaced by 0 :

destruct a; try discriminate e.

If you are unsure about lemmas, it's sometimes good to go back to definitions :)
Hope this helps

Stéphane

On Thu, Feb 17, 2011 at 10:31 PM, Tie Cheng <chengtie AT gmail.com> wrote:
> Hello Viktor,
> Thanks for your reply.
> If I do "apply Zcompare_Eq_eq", it changes the goal to "(a * something
> ?=0)%Z = Eq" which is not what I want. I want the goal to be "(0 *
> something)%Z = 0%Z". Is there a better way to use Zcompare_Eq_eq?
> Regards
> Tie
>
> On Thu, Feb 17, 2011 at 9:25 PM, Viktor Vafeiadis <viktor AT mpi-sws.org>
> wrote:
>>
>> Second lemma in Zcompare standard library.
>> Zcompare_Eq_eq
>>
>>
>> On 17 Feb 2011, at 21:20, Tie Cheng <chengtie AT gmail.com> wrote:
>>
>> > hello all,
>> >
>> > I have a hypothesis "e: (a ?=0)%Z = Eq", my goal is " (a * something)%Z
>> > = 0%Z".
>> >
>> > Does anyone know how I could use the hypothesis? Is there a lemma to say
>> > "(a ?=0)%Z = Eq -> a=0%Z"?
>> >
>> > Thanks and regards
>> >
>> > Tie
>
>

--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06