The Coq mailing list

[Vincent Siles <vsiles AT lix.polytechnique.fr>]

On 26/07/2010 14:54, Michael wrote:
> 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?
>    
Change can only exchange term which are ``convertible'' according to
Coq's conversion. If you need to prove that those term are equal, you will
have to use replace instead of change.

And I think you have the syntax wrong: to change A by B, you have to enter
change A with B.  (replace uses the same syntax).

Here is a simple example:

  x : nat
  ============================
   1 + x = S x

Unnamed_thm < change (1+x) with (S x).
1 subgoal

  x : nat
  ============================
   S x = S x

1 + x will compute to S x since plus pattern matches on the first argument.
Both terms are \beta equal.

  x : nat
  ============================
   x + 1 = S x

Unnamed_thm < change (x+1) with (S x).
Toplevel input, characters 0-23:
> change (x+1) with (S x).
> ^^^^^^^^^^^^^^^^^^^^^^^
Error: Not convertible.


This time, you need to *prove* that x+1 is the same thing at S x (by 
induction on x or whatever),
this is not direct by computation.

Hope it helps,
Vincent


> Sincerely,
> Michael
>