coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Tie Cheng <chengtie AT gmail.com>
- To: Viktor Vafeiadis <viktor AT mpi-sws.org>
- Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq"
- Date: Thu, 17 Feb 2011 22:31:59 +0100
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=mvyW7IKmr/wejnsJ8IUEBwlNl7opbXwP4Mc6jZvYE4OEbHHKhLLuX/oV8TfzOT9t/C /yV6msmYAkxoM1xVXRAZEKQKPtkJl+ku99pRH0zf9ig3HPO38p7MhQghBigoJolKGo/w VSPpgQG+E5Nzdc3LD9Frz5jYeqjSObX7JOzJw=
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
- [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", Tie Cheng
- Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq",
Viktor Vafeiadis
- Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", Tie Cheng
- Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", gallais @ EnsL.org
- Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", Stéphane Lescuyer
- Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", Tie Cheng
- Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq",
Viktor Vafeiadis
Archive powered by MhonArc 2.6.16.