coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: "Satrajit Roy" <satrajit.roy AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Re: Help with a seemingly obvious proof.
Date: Thu, 30 Oct 2008 15:08:07 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type; b=lBQfliZg8tLSR52UA3Il+wTsu9xnZxmksGEOyt/MGamWKtao6Eip08PsfjM4dGXpkb KKBVSJewmh/8V70o5RQuwwvR16gewvrK2M1ab6s6mcWj2/QGQikyaRvGfNoPyd8C8tqR kzuP8vb70YD4YpvSQTi8vdr2TKkheVf95AVro=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi folks,

I cannot prove the following with the tactics that I know of, although the goal seems pretty obvious.

argc : int32
H1 : integer_of_int32 argc > 0
HW_28 : integer_of_int32 argc = 1 -> False
HW_38 : integer_of_int32 argc = 2 -> False

______________________________________(1/1)
4 * (integer_of_int32 argc - 1) / 4 - 1 >= 0

I think, somehow I need to reduce the goal to a form where I can apply Z_div_ge0, but I cannot find a tactic to do so.

By the way, this is part of a proof obligation generated by Frama-C. If you need more information, please let me know.

Thanks again.

[Coq-Club] Re: Help with a seemingly obvious proof., Satrajit Roy
- Re: [Coq-Club] Re: Help with a seemingly obvious proof., Andrew McCreight
  - Re: [Coq-Club] Re: Help with a seemingly obvious proof., Pierre Letouzey
    - Re: [Coq-Club] Re: Help with a seemingly obvious proof., Satrajit Roy