The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

Unfortunately, in my experience proving even obvious things involving division can be fairly tedious.  Some tactics that help are ring, which will prove equality between terms involving basic algebraic reasoning (addition, subtraction, and multiplication), and omega, which will prove things for Presburger arithmetic.  Really, though, you have to look through Zdiv and puzzle out which combination of lemmas will solve your task.  Ring and omega just make it easier to get the goal into a state where you can apply one of those lemmas, so maybe that is the answer to your question.

Your particular theorem can be solved like this:

Goal forall x,
  x > 0 ->
  x <> 1 ->
  x <> 2 ->
  (4 * (x - 1)) / 4 - 1 >= 0.
Proof.
  intros x H1 H2 H3.
  replace (4 * (x - 1)) with (x * 4 + (- 1 * 4)) by ring.
  rewrite Z_div_plus. 2:omega.
  rewrite Z_div_mult. 2:omega.
  omega.
Qed.

Figuring out what exactly the replace line should be took me a couple of rounds of iteration, and the goal is really to massage things into a form that the built in lemmas can digest.  Omega cleans up the odds and ends.

If there's a better way to prove these sorts of things, I'd love to know about it.

-Andrew

On Thu, Oct 30, 2008 at 12:08 PM, Satrajit Roy <satrajit.roy AT gmail.com> wrote:

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.