The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Yves Bertot a écrit :
> Hello,
>
> Pierre's answer is probably what you want.  Here are a few more ideas:
>
>
> 1/ You may also wish to show that the order you defined is included in 
> the order Pierre defined,
> and use the lemma wf_incl from the file Wellfounded/Inclusion.v to 
> prove that yours
> is wellfounded.
Yes, in fact the order I proposed is logically equivalent to an 
intuitive (i.e. non dependent)
version of the lexicographic order on nat*(nat*nat) :


   forall t1 t2 : nat*(nat*nat),
             lt_npq (mk3 t1) (mk3 t2) <->
             (fst t1 < fst  t2 \/
               (fst t1 = fst t2 /\
                 (fst (snd t1) < fst (snd t2) \/
                                         (fst (snd t1) = fst (snd t2) /\
                                           snd (snd t1) < snd (snd t2))))).
Pierre



> > --------------------------------------------------------
> > Bug reports: http://logical.futurs.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >          http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club