The Coq mailing list

[frederic.blanqui AT inria.fr]

On Sun, 20 Jul 2008, Sunil Kothari wrote:

> Hello Coq Users,

>   I am trying to show that a 3-tuple of type nat* nat * nat is well-founded 
> for lexicographic ordering. I know there have been discussions on this 
> mailing-list before on lexicographic ordering on pairs in the context of 
> Ackermann's function.

> For instance, the discussion in 2004 between Stefan Karrmann and Pierre 
> Casteran http://pauillac.inria.fr/pipermail/coq-club/2004/001343.html

> I tried using their code since a 3-product can be considered as a product of 
> a pair and an element but I am stuck. The script is below:

Dear Sunil, you can also try to reuse the formalizations done in CoLoR 
http://color.loria.fr/:

- Util/Relations/Lexico: non-dependent lexicographic product using parameters 
gtA, eqA and gtB.

- Util/Pair/LexOrder: non-dependent lexicographic product on setoids using 
modules.

NB. in CoLoR, SN (strong normalization) is defined as the inverse (transp) of 
Coq's wellfoundedness. see Util/Relation/SN.v for conversions between both.

Hope it can help you. Cheers.