The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Pierre Casteran wrote:
> Hello Stefan,
>
>   You can find in Coq's standard library the module
>
> Coq.Wellfounded.Lexicographic_Product
>
> which proves that the lexicogrqphic product of two wf sets
> is wf.
>
> If you want to work with Z, you can use the order
>  Zwf (c x y:Z) := c <= y /\ x < y.
>
> which is wf too (see library Coq.ZArith.Zwf)




In fact, the lexicographic order defined in the Lexicographic_Product 
library deals with dependent pairs (the most genear case).

So, you don't work in Z*Z, but in sigS (fun _ : Z => Z),
i.e. {z:Z & Z}, which is quite the same :

Definition flatten : sigS (fun _ : Z => Z) -> Z * Z.
 destruct 1.
 exact (x,z).
Defined.

Definition make_sigS : Z * Z -> sigS (fun _ : Z => Z).
 intros (x,z).
 exists x.
 exact z.
Defined.

Lemma bij1 : forall s : sigS (fun _ : Z => Z), make_sigS (flatten s)=s.
 destruct s;simpl;auto.
Qed.

Lemma bij2 : forall x z, flatten(make_sigS (x,z)) = (x,z).
 simpl;auto.
Qed.



Another solution to define and use a non dependent lexicographic 
product, prove it respects well foundedness, and use it to define
directly Ackerman's function (with well_founded_induction)

Pierre

--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran