The Coq mailing list

[julien <julien.tesson AT univ-orleans.fr>]

Michael a écrit :
> Hello,
>
> I'm trying to proof an inequality like the following:
>
> Lemma lem1:
> forall (x:Z),
> (x * 64 / 8 + 1) >= x * 8.
>
> I tried to start changing the term:
> change ((x * 8 + 1) >= x * 8).
> but I receive the error message "Error: not convertible". It seems to have
> something to do with the brackets. If the statement is (x * (64 / 8) ...), I
> can easily change the term, and prove it.
>
> My first thought was, it might be because of x being of type Z, so in 
> general,
> x * y / z <> x * (y / z), if x * y is not a multiple of z. I then tried 
> another
> Lemma:
>
> Lemma lem2:
> forall (x:Z),
> x - 5 + 3 = x - 2.
>
> In this simple example, I could of couse prove it with intuition in a single
> step. But even here, "change (x - 2 = x - 2)" fails already.
>
> Why can't I change the terms in those 2 cases?
> In general, what is the best approach to simplify more complex inequalities 
> of
> such type?
>
> Sincerely,
> Michael
>   

Hello,

Actually, your two terms are not convertible, so you need auxilary
lemmas to prove the transformation.
I such case you can use the replace tactic :

 Require Import Omega.

Lemma lem1:
forall (x:Z),
(x * 64 / 8 + 1) >= x * 8 +1.
  intros x.
   replace (x * 64 / 8)with(x * 8) .
    (* this replace (x * 64 / 8) with (x * 8) in the goal an add a new
goal asking to prove x * 64 / 8= x * 8 *)
   omega. (* here I use omega to solve  (x * 64 / 8 + 1) >= (x * 64 / 8
+ 1) because Zge seems to not be proved reflexive)
    (* for proving x * 64 / 8= x * 8 you have to use Zdiv_mult_cancel_r
which need something in the form (x*z/y*z =x/y), I find it using Search
Pattern ( ?x*?y/?z = _ ) *)
   replace (64) with (8*8) by (simpl; reflexivity).
   replace (x*(8*8)) with (x*8*8) by (auto with zarith).
...
Qed.

Sincerly,
Julien.