The Coq mailing list

[CREGUT Pierre FTRD/DTL/LAN <pierre.cregut AT rd.francetelecom.com>]

One short solution is the following, but it does not show the structure
of the elimination of Zcompare :

    Intro j; Generalize good_n; Case j; Unfold Zcompare; [
      Intros; Omega
    | Intro p; Generalize (POS_gt_ZERO p); Intros; Omega
    | Compute; Tauto ].

A better way is to use this almost trivial theorem that summarizes that there
are only three cases for comparison and that if the result is EGAL then
terms are really equal.

    Theorem Zcompare_correctness: 
       (x,y:Z) ((Zcompare x y)=EGAL /\ x=y) \/ 
               ((Zcompare x y)=SUPERIEUR /\ `x>y`) \/
               ((Zcompare x y)=INFERIEUR /\ `x<y`).

    Intros; Unfold Zgt Zlt;
    Generalize (Zcompare_EGAL x y);  Generalize (Dcompare_inf (Zcompare x y));
    Intros [[H | H] | H];  Tauto.
    Save.

Now you can use the result in an almost short proof :

    Intro;
    (* the two next lines can be declared as a reusable tactic *)
    Generalize (Zcompare_correctness j `0`); 
    Intros [(Haux, E) | [(Haux, E) | (Haux, E)]]; Rewrite Haux; Clear Haux;
    (***)
    Intros; Omega.

The reusable part eliminates (Zcompare x y) and replaces it with three cases
x=y, x<y and x>y. In fact the last two are defined as respectively (Zcompare x
y)=SUPERIEUR and (Zcompare x y)=INFERIEUR.

P. Crégut

Quoting Frédéric Gava 
(frederic.gava AT wanadoo.fr):
> Bonjour,
> 
> Pour mes demos je suis obliger de démontrer ce petits lemmes:
> 
> Lemma a_faire: (j:Z) `0<=j<n` ->
> `0 <=
>       (Cases (Zcompare j `0`) of
>            EGAL => `n-1`
>        |  _          => `j-1 end) < n`.
> 
> Bien sur on a l'axiome 
> 
> Axiom good_n:`0<n`.
> 
> En fait, mon pb est plus général: comment faire passer dans les hypothèses 
> la comparaison et puis faire tous les sous cas...
> 
> Pour certain je fais des démos par NewInduction. Mais la, je n'y arrive 
> pas...
> 
> Merci par avance.
> 
> Frédéric Gava
> 
> 
> [[HTML alternate version deleted]]

-- 
Pierre Cregut - 
pierre.cregut AT rd.francetelecom.com
 - +33 2 96 05 16 28
FTR&D - DTL/TAL - 2 avenue Pierre Marzin - 22307 Lannion Cedex - France