The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Ashish,

First the notations p~1 and p~0 are introduced in BinPos and denote
respectively (xI p) and (xO p), ie 2*p+1 and 2*p.
They allow one to write positives in a standard binary fashion,
instead of writing them backwards with the constructors xI and xO.

As far as your goal is concerned, you're proving a conjunct of the
form A /\ B /\ C where A and B are consequences of C so proving C
should be enough here. If you still want to keep your goal unchanged,
then you should start with a cut :

Require Import Omega ZArith.
Open Local Scope Z_scope.

Goal forall x y:Z, (x <> 0) -> (y <> 0) -> (x+y = 0) ->
   (~(Zabs x < Zabs y)) /\  (~(Zabs y < Zabs x)) /\ (Zabs x = Zabs y).
Proof.
  intros x y Hx Hy H.
  cut (Zabs x  = Zabs y); [intro Hcut|].
  ...

This leaves you with two goals, the first amounts to proving that the
first two conjuncts are a consequence of the last one, which is easily
discharged by omega.

  ...
  repeat split; omega.
  ...

And the second one is the real lemma you're trying to prove. Instead
of resorting to induction on positives, I suggest you use the
definition of the Zabs function in order to transform your goal in two
simple arithmetic goals that, once again, can be discharged by omega.
More often than not, induction is not the right way to go when proving
things on positives (at least, not structural induction) ; try to find
some helpful results about your problem in the library first and then
use omega to clean up "obvious" subgoals.

  ...
  destruct (Zabs_spec x); destruct (Zabs_spec y); omega.
Qed.

Hope this helps,

Stéphane L.

On Sun, Feb 8, 2009 at 1:36 PM, Ashish Darbari
<ashish_darbariuk AT yahoo.co.uk>
 wrote:
> I'm trying to prove the following:
> Goal forall x y:Z, (x <> 0) -> (y <> 0) -> (x+y = 0) ->
>    (~(Zabs x < Zabs y)) /\  (~(Zabs y < Zabs x)) /\ (Zabs x = Zabs y).
> After typing in the following:
> intros;induction x;induction y.
> contradiction.
> contradiction.
> contradiction.
> contradiction.
> unfold Zabs.
> split.
> induction p;induction p0.
> I end up with 14 subgoals on positives. But I don't quite understand
> the notation p~1, what is ~?
> Is there a possible proof without having to induct on p and p0?
>
> Thanks
> Ashish
> 14 subgoals
>
>   p : positive
>   p0 : positive
>   H : Zpos p~1 <> 0
>   H0 : Zpos p0~1 <> 0
>   H1 : Zpos p~1 + Zpos p0~1 = 0
>   IHp : Zpos p <> 0 -> Zpos p + Zpos p0~1 = 0 -> ~ Zpos p < Zpos p0~1
>   IHp0 : Zpos p0 <> 0 ->
>          Zpos p~1 + Zpos p0 = 0 ->
>          (Zpos p <> 0 -> Zpos p + Zpos p0 = 0 -> ~ Zpos p < Zpos p0) ->
>          ~ Zpos p~1 < Zpos p0
>   ============================
>    ~ Zpos p~1 < Zpos p0~1
> ....
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06